Name | normalized-opb/web/www.nlsde.buaa.edu.cn/~kexu/benchmarks/frb35-17-opb/normalized-frb35-17-4.opb |
MD5SUM | e3892e1941a878802a8ccbbd36201a02 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | -27 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 595 |
Biggest coefficient in the objective function | 1 |
Number of bits for the biggest coefficient in the objective function | 1 |
Sum of the numbers in the objective function | 595 |
Number of bits of the sum of numbers in the objective function | 10 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 595 |
Number of bits of the biggest sum of numbers | 10 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.05 |
Number of variables | 595 |
Total number of constraints | 27842 |
Number of constraints which are clauses | 27842 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 2 |
Maximum length of a constraint | 2 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-04-14 00:55:42 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4082 boxname=wulflinc6 idbench=322 idsolver=11 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: e3892e1941a878802a8ccbbd36201a02 /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-4.opb REAL COMMAND: minisat+ -S /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-4.opb /oldhome/oroussel/tmp/wulflinc6/normalized-frb35-17-4.opb IDLAUNCH: 4082 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 893136 kB Buffers: 35760 kB Cached: 83520 kB SwapCached: 2644 kB Active: 52868 kB Inactive: 71920 kB HighTotal: 131008 kB HighFree: 43512 kB LowTotal: 903652 kB LowFree: 849624 kB SwapTotal: 2097136 kB SwapFree: 2094492 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 11140 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 01:15:44 (client local time) WITH STATUS 10 IN 1200.37 SECONDS stats: 4082 7 1200.37 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 27842 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): .................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................. c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 27842 55684 | 8352 0 0 nan | 0.000 % | c -- subsuming c | 0 | 27842 55684 | 11136 0 0 nan | 0.000 % | c ============================================================================== c (current CPU-time: 1.07883 s) c ============================================================================== c [1mFound solution: -26[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost:26814 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 0 | 56138 122140 | 16841 0 0 nan | 0.000 % | c -- subsuming c -- var.elim.: 1000/19347 c -- var.elim.: 2000/19347 c -- var.elim.: 3000/19347 c -- var.elim.: 4000/19347 c -- var.elim.: 5000/19347 c -- var.elim.: 6000/19347 c -- var.elim.: 7000/19347 c -- var.elim.: 8000/19347 c -- var.elim.: 9000/19347 c -- var.elim.: 10000/19347 c -- var.elim.: 11000/19347 c -- var.elim.: 12000/19347 c -- var.elim.: 13000/19347 c -- var.elim.: 14000/19347 c -- var.elim.: 15000/19347 c -- var.elim.: 16000/19347 c -- var.elim.: 17000/19347 c -- var.elim.: 18000/19347 c -- var.elim.: 19000/19347 c -- var.elim.: 19347/19347 c -- var.elim.: 1000/9850 c -- var.elim.: 2000/9850 c -- var.elim.: 3000/9850 c -- var.elim.: 4000/9850 c -- var.elim.: 5000/9850 c -- var.elim.: 6000/9850 c -- var.elim.: 7000/9850 c -- var.elim.: 8000/9850 c -- var.elim.: 9000/9850 c -- var.elim.: 9850/9850 c -- var.elim.: 85/85 c -- var.elim.: 37/37 c -- subsuming c -- var.elim.: 1000/3837 c -- var.elim.: 2000/3837 c -- var.elim.: 3000/3837 c -- var.elim.: 3837/3837 c -- var.elim.: 259/259 c | 0 | 36204 121513 | -- 0 -- -- | -- | -19929/-612 c | 0 | 36204 121513 | 14481 0 0 nan | 0.000 % | c | 100 | 36204 121513 | 15929 100 11105 111.0 | 52.803 % | c | 251 | 36204 121513 | 17522 251 38043 151.6 | 52.802 % | c | 476 | 36136 120915 | 19238 471 69831 148.3 | 53.118 % | c | 813 | 36078 120463 | 21128 803 129943 161.8 | 53.414 % | c | 1319 | 36048 120261 | 23222 1307 197266 150.9 | 53.567 % | c | 2078 | 36046 120243 | 25543 2062 324725 157.5 | 53.577 % | c | 3217 | 35981 119681 | 28046 3189 567627 178.0 | 53.903 % | c ============================================================================== c (current CPU-time: 43.9683 s) c ============================================================================== c [1mFound solution: -27[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 4354 | 38859 127504 | 11657 4326 773508 178.8 | 53.903 % | c -- subsuming c -- var.elim.: 1000/6410 c -- var.elim.: 2000/6410 c -- var.elim.: 3000/6410 c -- var.elim.: 4000/6410 c -- var.elim.: 5000/6410 c -- var.elim.: 6000/6410 c -- var.elim.: 6410/6410 c -- var.elim.: 1000/2061 c -- var.elim.: 2000/2061 c -- var.elim.: 2061/2061 c -- var.elim.: 4/4 c | 4354 | 36076 125611 | -- 4326 -- -- | -- | -2775/-1876 c | 4354 | 36076 125611 | 14430 4326 773508 178.8 | 53.903 % | c | 4454 | 36014 125079 | 15846 4424 789746 178.5 | 58.140 % | c | 4604 | 36014 125079 | 17430 4574 812983 177.7 | 58.140 % | c | 4829 | 36014 125079 | 19173 4799 848071 176.7 | 58.140 % | c | 5166 | 36014 125079 | 21091 5136 933143 181.7 | 58.140 % | c | 5672 | 35948 124476 | 23157 5626 1039529 184.8 | 58.436 % | c | 6432 | 35906 124168 | 25443 6381 1216910 190.7 | 58.602 % | c | 7571 | 35758 122733 | 27872 7503 1488201 198.3 | 59.212 % | c | 9280 | 35637 121920 | 30556 9179 1885112 205.4 | 59.684 % | c | 11843 | 35445 120374 | 33430 11705 2437295 208.2 | 60.516 % | c ============================================================================== c (current CPU-time: 66.7599 s) c ============================================================================== c [1mFound solution: -28[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 11909 | 35551 120702 | 10665 11771 2441797 207.4 | 60.516 % | c -- subsuming c -- var.elim.: 1000/4284 c -- var.elim.: 2000/4284 c -- var.elim.: 3000/4284 c -- var.elim.: 4000/4284 c -- var.elim.: 4284/4284 c -- var.elim.: 319/319 c | 11909 | 35429 119901 | -- 11771 -- -- | -- | -110/-542 c | 11909 | 35429 119901 | 14171 9866 1201036 121.7 | 60.516 % | c | 12009 | 35429 119901 | 15588 9966 1220359 122.5 | 60.637 % | c | 12159 | 35429 119901 | 17147 10116 1245107 123.1 | 60.636 % | c | 12386 | 35399 119646 | 18846 10332 1282260 124.1 | 60.775 % | c | 12723 | 35399 119646 | 20731 10669 1361660 127.6 | 60.775 % | c | 13229 | 35368 119424 | 22784 11072 1456322 131.5 | 60.914 % | c | 13988 | 35219 118186 | 24957 11805 1615127 136.8 | 61.598 % | c | 15127 | 35181 117818 | 27423 12936 1936030 149.7 | 61.774 % | c | 16835 | 35003 116244 | 30012 14603 2344044 160.5 | 62.579 % | c | 19397 | 34703 113556 | 32731 17114 3018479 176.4 | 63.948 % | c | 23241 | 34621 112788 | 35919 20902 4152111 198.6 | 64.317 % | c | 29007 | 34203 108993 | 39034 26528 5847459 220.4 | 66.241 % | c ============================================================================== c (current CPU-time: 118.698 s) c ============================================================================== c [1mFound solution: -29[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 29143 | 34432 109636 | 10329 26664 5888140 220.8 | 66.241 % | c -- subsuming c -- var.elim.: 1000/3370 c -- var.elim.: 2000/3370 c -- var.elim.: 3000/3370 c -- var.elim.: 3370/3370 c -- var.elim.: 227/227 c | 29143 | 34252 109221 | -- 26664 -- -- | -- | -180/-414 c | 29143 | 34252 109221 | 13700 26183 5728293 218.8 | 66.241 % | c | 29243 | 34190 108712 | 15043 15306 3227646 210.9 | 66.559 % | c | 29393 | 34190 108712 | 16547 15456 3252692 210.4 | 66.560 % | c | 29618 | 34164 108484 | 18188 15670 3301693 210.7 | 66.670 % | c | 29955 | 34162 108463 | 20006 16003 3380013 211.2 | 66.679 % | c | 30461 | 34100 107934 | 21967 16496 3467426 210.2 | 66.965 % | c | 31220 | 34076 107733 | 24147 17248 3669107 212.7 | 67.076 % | c | 32359 | 34033 107466 | 26528 18382 4018138 218.6 | 67.260 % | c | 34067 | 33997 107191 | 29150 20085 4449496 221.5 | 67.426 % | c | 36629 | 33728 104936 | 31811 22534 5151079 228.6 | 68.661 % | c | 40473 | 33555 103320 | 34813 26333 6207552 235.7 | 69.426 % | c | 46239 | 33460 102443 | 38186 32063 7898211 246.3 | 69.859 % | c | 54888 | 33406 101902 | 41936 40700 10382271 255.1 | 70.108 % | c ============================================================================== c (current CPU-time: 258.208 s) c ============================================================================== c [1mFound solution: -30[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 66552 | 33135 98883 | 9940 20698 4150539 200.5 | 70.108 % | c -- subsuming c -- var.elim.: 1000/3094 c -- var.elim.: 2000/3094 c -- var.elim.: 3000/3094 c -- var.elim.: 3094/3094 c -- var.elim.: 230/230 c -- var.elim.: 5/5 c | 66552 | 33022 96561 | -- 20698 -- -- | -- | -90/-303 c | 66552 | 33022 96561 | 13208 16191 1459480 90.1 | 70.108 % | c | 66652 | 32990 96265 | 14515 16290 1469036 90.2 | 72.000 % | c | 66802 | 32990 96265 | 15967 16440 1511440 91.9 | 72.000 % | c | 67027 | 32990 96265 | 17563 16665 1553519 93.2 | 72.000 % | c | 67364 | 32990 96265 | 19320 17002 1617358 95.1 | 72.000 % | c | 67870 | 32990 96265 | 21252 17508 1745478 99.7 | 72.000 % | c | 68630 | 32990 96265 | 23377 18268 1905302 104.3 | 72.000 % | c | 69771 | 32990 96265 | 25715 19409 2217793 114.3 | 72.001 % | c | 71479 | 32931 95761 | 28236 21103 2644011 125.3 | 72.268 % | c | 74042 | 32931 95761 | 31059 23666 3312257 140.0 | 72.268 % | c | 77886 | 32931 95761 | 34165 27510 4452456 161.8 | 72.268 % | c | 83653 | 32931 95761 | 37582 33277 6107331 183.5 | 72.267 % | c | 92302 | 32775 94439 | 41144 41892 8506948 203.1 | 72.950 % | c | 105276 | 32669 93588 | 45112 23339 4786051 205.1 | 73.438 % | c ============================================================================== c (current CPU-time: 438.748 s) c ============================================================================== c [1mFound solution: -31[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 0 Base: c =================================[SATELITE+]================================== c | | ORIGINAL | LEARNT | | c | Conflicts | Clauses Literals | Limit Clauses Literals Lit/Cl | Progress | c ============================================================================== c | 123935 | 34915 98548 | 10474 41958 9975199 237.7 | 73.438 % | c -- subsuming c -- var.elim.: 1000/4553 c -- var.elim.: 2000/4553 c -- var.elim.: 3000/4553 c -- var.elim.: 4000/4553 c -- var.elim.: 4553/4553 c -- var.elim.: 1000/1533 c -- var.elim.: 1533/1533 c | 123935 | 32587 95618 | -- 41958 -- -- | -- | -2321/-2915 c | 123935 | 32587 95618 | 13034 41958 9975199 237.7 | 73.438 % | c | 124035 | 32587 95618 | 14338 18463 3544937 192.0 | 80.308 % | c | 124185 | 32561 95378 | 15759 18609 3559296 191.3 | 80.398 % | c | 124411 | 32561 95378 | 17335 18835 3602053 191.2 | 80.398 % | c | 124749 | 32559 95357 | 19067 19170 3715947 193.8 | 80.405 % | c | 125255 | 32559 95357 | 20974 19676 3807968 193.5 | 80.405 % | c | 126014 | 32533 95098 | 23053 20431 3964797 194.1 | 80.496 % | c | 127153 | 32501 94845 | 25334 21562 4233993 196.4 | 80.593 % | c | 128862 | 32459 94479 | 27831 23262 4595586 197.6 | 80.739 % | c | 131425 | 32437 94310 | 30593 25802 5309387 205.8 | 80.816 % | c | 135269 | 32100 91479 | 33303 29523 6097468 206.5 | 81.937 % | c | 141035 | 31858 89251 | 36357 35094 7538736 214.8 | 82.723 % | c | 149684 | 31612 87239 | 39684 43605 9636249 221.0 | 83.489 % | c | 162658 | 31296 84776 | 43216 23455 4421942 188.5 | 84.443 % | c | 182119 | 31081 82875 | 47212 42843 9202365 214.8 | 85.166 % | c | 211311 | 30797 80361 | 51458 29700 6117782 206.0 | 86.134 % | c | 255100 | 30691 79402 | 56409 27315 5704563 208.8 | 86.503 % | c | 320784 | 30516 77858 | 61696 40031 9233583 230.7 | 87.095 % | c c *** TERMINATED *** s SATISFIABLE v -C595 -C594 -C593 -C592 -C591 -C590 -C589 -C588 -C587 -C586 -C585 -C584 -C583 C582 -C581 -C580 -C579 -C578 C577 -C576 -C575 -C574 -C573 -C572 -C571 -C570 -C569 -C568 -C567 -C566 -C565 -C564 -C563 -C562 -C561 -C560 -C559 -C558 -C557 -C556 -C555 -C554 -C553 C552 -C551 -C550 -C549 -C548 -C547 -C546 -C545 -C544 -C543 C542 -C541 -C540 -C539 -C538 -C537 -C536 -C535 -C534 -C533 -C532 -C531 -C530 -C529 -C528 -C527 -C526 -C525 -C524 -C523 -C522 -C521 -C520 -C519 -C518 -C517 -C516 -C515 -C514 -C513 -C512 -C511 -C510 -C509 -C508 -C507 -C506 -C505 -C504 -C503 -C502 -C501 -C500 -C499 -C498 -C497 -C496 -C495 C494 -C493 -C492 -C491 -C490 -C489 -C488 -C487 -C486 -C485 -C484 -C483 -C482 -C481 -C480 C479 -C478 -C477 -C476 -C475 -C474 -C473 -C472 -C471 -C470 -C469 -C468 -C467 -C466 -C465 -C464 -C463 -C462 -C461 -C460 -C459 -C458 -C457 -C456 -C455 C454 -C453 -C452 -C451 -C450 -C449 -C448 -C447 -C446 -C445 -C444 -C443 -C442 -C441 -C440 -C439 -C438 -C437 -C436 -C435 -C434 C433 -C432 -C431 -C430 -C429 -C428 -C427 -C426 -C425 -C424 -C423 -C422 -C421 -C420 -C419 -C418 C417 -C416 -C415 -C414 -C413 -C412 -C411 -C410 -C409 -C408 -C407 -C406 -C405 -C404 -C403 -C402 C401 -C400 -C399 -C398 -C397 -C396 -C395 -C394 -C393 -C392 -C391 -C390 -C389 -C388 -C387 -C386 -C385 -C384 -C383 -C382 -C381 -C380 -C379 -C378 -C377 -C376 C375 -C374 -C373 -C372 -C371 -C370 -C369 C368 -C367 -C366 -C365 -C364 -C363 -C362 -C361 -C360 -C359 -C358 -C357 C356 -C355 -C354 -C353 -C352 -C351 -C350 -C349 -C348 -C347 -C346 -C345 -C344 -C343 -C342 -C341 -C340 -C339 -C338 -C337 -C336 -C335 -C334 -C333 -C332 -C331 -C330 -C329 -C328 -C327 -C326 -C325 -C324 -C323 -C322 -C321 -C320 C319 -C318 -C317 -C316 -C315 -C314 -C313 -C312 -C311 -C310 -C309 -C308 -C307 -C306 -C305 -C304 -C303 -C302 -C301 -C300 -C299 -C298 -C297 -C296 -C295 C294 -C293 -C292 -C291 -C290 -C289 -C288 -C287 -C286 -C285 -C284 -C283 -C282 -C281 -C280 -C279 -C278 -C277 -C276 C275 -C274 -C273 -C272 -C271 -C270 -C269 -C268 -C267 C266 -C265 -C264 -C263 -C262 -C261 -C260 -C259 -C258 -C257 -C256 -C255 -C254 -C253 -C252 -C251 -C250 -C249 -C248 -C247 -C246 -C245 -C244 -C243 -C242 -C241 -C240#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (runsolver) R 1247 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422214026 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0007 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 3648 0 0 0 985 14 0 0 25 0 1 0 422214026 17821696 3626 4294967295 134512640 134672761 3221224560 3221222992 134604645 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4351 3626 603 41 0 4310 0 vsize: 17404 [startup+20.0023 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 3664 0 0 0 1985 14 0 0 25 0 1 0 422214026 17965056 3642 4294967295 134512640 134672761 3221224560 3221222636 134566531 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4386 3642 603 41 0 4345 0 vsize: 17544 [startup+30.003 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 3694 0 0 0 2985 14 0 0 25 0 1 0 422214026 18161664 3672 4294967295 134512640 134672761 3221224560 3221223008 134643624 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4434 3672 603 41 0 4393 0 vsize: 17736 [startup+40.0031 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 3841 0 0 0 3984 14 0 0 25 0 1 0 422214026 18161664 3709 4294967295 134512640 134672761 3221224560 3221223728 134564746 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 4434 3709 603 41 0 4393 0 vsize: 17736 [startup+50.0047 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 5193 0 0 0 4971 28 0 0 25 0 1 0 422214026 22220800 4702 4294967295 134512640 134672761 3221224560 3221223008 134643954 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 5425 4702 603 41 0 5384 0 vsize: 21700 [startup+60.0054 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 5910 0 0 0 5969 30 0 0 25 0 1 0 422214026 24961024 5419 4294967295 134512640 134672761 3221224560 3221223704 134616299 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 6094 5419 603 41 0 6053 0 vsize: 24376 [startup+70.0065 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 7330 0 0 0 6963 37 0 0 25 0 1 0 422214026 29233152 6452 4294967295 134512640 134672761 3221224560 3221223008 134643580 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7137 6452 603 41 0 7096 0 vsize: 28548 [startup+80.0082 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 7331 0 0 0 7963 37 0 0 25 0 1 0 422214026 29233152 6453 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7137 6453 603 41 0 7096 0 vsize: 28548 [startup+90.0089 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 7561 0 0 0 8963 37 0 0 25 0 1 0 422214026 30101504 6683 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7349 6683 603 41 0 7308 0 vsize: 29396 [startup+100.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 8795 0 0 0 9960 41 0 0 25 0 1 0 422214026 35188736 7917 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 8591 7917 603 41 0 8550 0 vsize: 34364 [startup+110.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 9548 0 0 0 10958 43 0 0 25 0 1 0 422214026 38178816 8670 4294967295 134512640 134672761 3221224560 3221223704 134616123 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 9321 8670 603 41 0 9280 0 vsize: 37284 [startup+120.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11270 0 0 0 11950 50 0 0 25 0 1 0 422214026 43859968 10003 4294967295 134512640 134672761 3221224560 3221223104 134621164 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10708 10003 603 41 0 10667 0 vsize: 42832 [startup+130.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11270 0 0 0 12950 51 0 0 25 0 1 0 422214026 43859968 10003 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10708 10003 603 41 0 10667 0 vsize: 42832 [startup+140.013 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11271 0 0 0 13950 51 0 0 25 0 1 0 422214026 43859968 10004 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10708 10004 603 41 0 10667 0 vsize: 42832 [startup+150.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11271 0 0 0 14950 51 0 0 25 0 1 0 422214026 43859968 10004 4294967295 134512640 134672761 3221224560 3221223704 134616247 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10708 10004 603 41 0 10667 0 vsize: 42832 [startup+160.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 11439 0 0 0 15950 52 0 0 25 0 1 0 422214026 44380160 10172 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10835 10172 603 41 0 10794 0 vsize: 43340 [startup+170.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 12371 0 0 0 16947 55 0 0 25 0 1 0 422214026 48185344 11104 4294967295 134512640 134672761 3221224560 3221223600 134612608 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11764 11104 603 41 0 11723 0 vsize: 47056 [startup+180.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 13233 0 0 0 17944 58 0 0 25 0 1 0 422214026 51826688 11966 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12653 11966 603 41 0 12612 0 vsize: 50612 [startup+190.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 14041 0 0 0 18942 60 0 0 25 0 1 0 422214026 55078912 12774 4294967295 134512640 134672761 3221224560 3221223744 134616004 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13447 12774 603 41 0 13406 0 vsize: 53788 [startup+200.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 15041 0 0 0 19938 64 0 0 25 0 1 0 422214026 59129856 13774 4294967295 134512640 134672761 3221224560 3221223600 134614141 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14436 13774 603 41 0 14395 0 vsize: 57744 [startup+210.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 15848 0 0 0 20936 66 0 0 25 0 1 0 422214026 62521344 14581 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15264 14581 603 41 0 15223 0 vsize: 61056 [startup+220.016 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 16409 0 0 0 21935 67 0 0 25 0 1 0 422214026 64704512 15142 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15797 15142 603 41 0 15756 0 vsize: 63188 [startup+230.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 16890 0 0 0 22934 68 0 0 25 0 1 0 422214026 66678784 15623 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16279 15623 603 41 0 16238 0 vsize: 65116 [startup+240.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 17592 0 0 0 23932 71 0 0 25 0 1 0 422214026 69533696 16325 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16976 16325 603 41 0 16935 0 vsize: 67904 [startup+250.015 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 18289 0 0 0 24929 73 0 0 25 0 1 0 422214026 72413184 17022 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17679 17022 603 41 0 17638 0 vsize: 70716 [startup+260.014 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1248 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 25924 79 0 0 25 0 1 0 422214026 74280960 17479 4294967295 134512640 134672761 3221224560 3221223104 134621122 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18135 17479 603 41 0 18094 0 vsize: 72540 [startup+270.014 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 1304 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 26916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17369 603 41 0 17974 0 vsize: 72060 [startup+280.014 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 1304 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 27916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223600 134612827 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17369 603 41 0 17974 0 vsize: 72060 [startup+290.013 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 1304 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 28916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17369 603 41 0 17974 0 vsize: 72060 [startup+300.013 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 1304 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 29916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17369 603 41 0 17974 0 vsize: 72060 [startup+310.013 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 1304 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19331 0 0 0 30916 86 0 0 25 0 1 0 422214026 73789440 17369 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17369 603 41 0 17974 0 vsize: 72060 [startup+320.012 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 1304 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 31917 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223600 134612614 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+330.013 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 1304 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 32917 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+340.012 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 33917 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+350.013 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 34918 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+360.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 35918 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+370.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19332 0 0 0 36918 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+380.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 37919 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+390.014 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 38919 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+400.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 39919 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+410.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 40920 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+420.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 41920 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223744 134616001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+430.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 19382 0 0 0 42920 86 0 0 25 0 1 0 422214026 73789440 17370 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18015 17370 603 41 0 17974 0 vsize: 72060 [startup+440.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20084 0 0 0 43916 91 0 0 25 0 1 0 422214026 74739712 17608 4294967295 134512640 134672761 3221224560 3221223052 134642759 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18247 17608 603 41 0 18206 0 vsize: 72988 [startup+450.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 44911 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223600 134614261 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17498 603 41 0 18006 0 vsize: 72188 [startup+460.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 45911 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223712 134565116 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17498 603 41 0 18006 0 vsize: 72188 [startup+470.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 46911 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18047 17498 603 41 0 18006 0 vsize: 72188 [startup+480.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 47911 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17498 603 41 0 18006 0 vsize: 72188 [startup+490.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20125 0 0 0 48912 96 0 0 25 0 1 0 422214026 73920512 17498 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17498 603 41 0 18006 0 vsize: 72188 [startup+500.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 49912 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17499 603 41 0 18006 0 vsize: 72188 [startup+510.012 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 50912 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615529 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17499 603 41 0 18006 0 vsize: 72188 [startup+520.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 51913 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17499 603 41 0 18006 0 vsize: 72188 [startup+530.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 52913 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17499 603 41 0 18006 0 vsize: 72188 [startup+540.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 53913 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17499 603 41 0 18006 0 vsize: 72188 [startup+550.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 54913 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17499 603 41 0 18006 0 vsize: 72188 [startup+560.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20126 0 0 0 55914 96 0 0 25 0 1 0 422214026 73920512 17499 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17499 603 41 0 18006 0 vsize: 72188 [startup+570.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1306 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 56914 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223600 134613748 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+580.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 57914 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+590.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 58915 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+600.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 59915 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+610.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 60915 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+620.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 61916 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+630.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 62916 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+640.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 63916 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+650.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 64917 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223704 134616233 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+660.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 65917 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+670.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 66917 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+680.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20178 0 0 0 67917 96 0 0 25 0 1 0 422214026 73920512 17500 4294967295 134512640 134672761 3221224560 3221223408 134604652 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17500 603 41 0 18006 0 vsize: 72188 [startup+690.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20180 0 0 0 68918 96 0 0 25 0 1 0 422214026 73920512 17502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17502 603 41 0 18006 0 vsize: 72188 [startup+700.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20182 0 0 0 69918 96 0 0 25 0 1 0 422214026 73920512 17504 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18047 17504 603 41 0 18006 0 vsize: 72188 [startup+710.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 20391 0 0 0 70918 97 0 0 25 0 1 0 422214026 74846208 17713 4294967295 134512640 134672761 3221224560 3221223744 134615660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18273 17713 603 41 0 18232 0 vsize: 73092 [startup+720.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21012 0 0 0 71916 99 0 0 25 0 1 0 422214026 77328384 18334 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18879 18334 603 41 0 18838 0 vsize: 75516 [startup+730.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21331 0 0 0 72916 100 0 0 25 0 1 0 422214026 78344192 18593 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18593 603 41 0 19086 0 vsize: 76508 [startup+740.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21331 0 0 0 73916 100 0 0 25 0 1 0 422214026 78344192 18593 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18593 603 41 0 19086 0 vsize: 76508 [startup+750.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21331 0 0 0 74917 100 0 0 25 0 1 0 422214026 78344192 18593 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18593 603 41 0 19086 0 vsize: 76508 [startup+760.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 75917 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615801 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+770.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 76917 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+780.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 77917 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+790.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 78918 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+800.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 79918 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+810.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 80918 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+820.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 81919 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+830.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 82919 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+840.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 83920 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+850.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 84920 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+860.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 85920 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+870.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21332 0 0 0 86921 100 0 0 25 0 1 0 422214026 78344192 18594 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19127 18594 603 41 0 19086 0 vsize: 76508 [startup+880.011 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21567 0 0 0 87921 100 0 0 25 0 1 0 422214026 79392768 18829 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19383 18829 603 41 0 19342 0 vsize: 77532 [startup+890.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 21986 0 0 0 88920 101 0 0 25 0 1 0 422214026 81108992 19248 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19802 19248 603 41 0 19761 0 vsize: 79208 [startup+900.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 89919 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+910.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 90919 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134616042 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+920.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 91919 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+930.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 92920 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+940.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 93920 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223708 134614482 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+950.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 94920 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223704 134616161 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+960.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 95921 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+970.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 96921 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+980.008 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 97921 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+990.009 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22545 0 0 0 98922 102 0 0 25 0 1 0 422214026 83058688 19744 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19744 603 41 0 20237 0 vsize: 81112 [startup+1000.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 99922 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19745 603 41 0 20237 0 vsize: 81112 [startup+1010.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 100922 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19745 603 41 0 20237 0 vsize: 81112 [startup+1020.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 101923 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19745 603 41 0 20237 0 vsize: 81112 [startup+1030.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 102923 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19745 603 41 0 20237 0 vsize: 81112 [startup+1040.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22546 0 0 0 103923 102 0 0 25 0 1 0 422214026 83058688 19745 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20278 19745 603 41 0 20237 0 vsize: 81112 [startup+1050.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 22547 0 0 0 104924 102 0 0 25 0 1 0 422214026 83193856 19746 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20311 19746 603 41 0 20270 0 vsize: 81244 [startup+1060.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 23164 0 0 0 105922 104 0 0 25 0 1 0 422214026 85684224 20363 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20919 20363 603 41 0 20878 0 vsize: 83676 [startup+1070.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 23727 0 0 0 106921 106 0 0 25 0 1 0 422214026 88178688 20926 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21528 20926 603 41 0 21487 0 vsize: 86112 [startup+1080.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24285 0 0 0 107920 107 0 0 25 0 1 0 422214026 90546176 21484 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22106 21484 603 41 0 22065 0 vsize: 88424 [startup+1090.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 108919 108 0 0 25 0 1 0 422214026 92917760 22029 4294967295 134512640 134672761 3221224560 3221223656 134616347 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22685 22029 603 41 0 22644 0 vsize: 90740 [startup+1100.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 109919 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223600 134612684 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1110.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 110920 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1120.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 111920 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1130.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 112920 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1140.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 113921 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1150.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 114921 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1160.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 115921 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1170.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 116922 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1180.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 117922 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1190.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 118922 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134616004 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 [startup+1200.01 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1308 Raw data (stat): 1248 (minisat+) R 1247 29653 29652 0 -1 0 24862 0 0 0 119923 108 0 0 25 0 1 0 422214026 92393472 21960 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22557 21960 603 41 0 22516 0 vsize: 90228 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 1.00 0.99 0.91 1/54 1308 Raw data (stat): 1248 (minisat+) Z 1247 29653 29652 0 -1 12 24863 0 0 0 119923 113 0 0 25 0 1 0 422214026 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 10 Real time (s): 1200.07 CPU time (s): 1200.37 CPU user time (s): 1199.23 CPU system time (s): 1.13783 CPU usage (%): 100.026 Max. virtual memory (Kb): 90740 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####