Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/milp/normalized-mps-v2-20-10-markshare2_1.opb |
MD5SUM | a84a96a9314212f3d8ecd5227c500cef |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 91392 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 210 |
Biggest coefficient in the objective function | 536870912 |
Number of bits for the biggest coefficient in the objective function | 30 |
Sum of the numbers in the objective function | 7516192761 |
Number of bits of the sum of numbers in the objective function | 33 |
Biggest number in a constraint | 536870912 |
Number of bits of the biggest number in a constraint | 30 |
Biggest sum of numbers in a constraint | 7516192761 |
Number of bits of the biggest sum of numbers | 33 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1202.31 |
Number of variables | 330 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 54 |
Number of constraints which are nor clauses,nor cardinality constraints | 13 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 150 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc20 THE 2005-04-20 21:13:50 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=14494 boxname=wulflinc20 idbench=1115 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: a84a96a9314212f3d8ecd5227c500cef /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare2_1.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare2_1.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-20-10-markshare2_1.opb IDLAUNCH: 14494 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.215 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 : 3 cpu MHz : 451.215 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 725496 kB Buffers: 33768 kB Cached: 249808 kB SwapCached: 528 kB Active: 163676 kB Inactive: 121880 kB HighTotal: 131008 kB HighFree: 980 kB LowTotal: 903652 kB LowFree: 724516 kB SwapTotal: 2097892 kB SwapFree: 2096468 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5112 kB Slab: 17876 kB Committed_AS: 63584 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-20 21:33:53 (client local time) WITH STATUS 10 IN 1200.37 SECONDS stats: 14494 7 1200.37 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 20 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 19]---> BDD-cost: 10 c ---[ 18]---> BDD-cost: 10 c ---[ 17]---> BDD-cost: 10 c ---[ 16]---> BDD-cost: 10 c ---[ 15]---> BDD-cost: 10 c ---[ 14]---> BDD-cost: 10 c ---[ 12]---> BDD-cost:75277 c ---[ 10]---> BDD-cost:110257 c ---[ 8]---> BDD-cost:99901 c ---[ 6]---> BDD-cost:112483 c ---[ 4]---> BDD-cost:82177 c ---[ 2]---> BDD-cost:116705 c ---[ 0]---> BDD-cost:69441 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 1906914 5553068 | 635638 0 0 nan | 0.000 % | c ============================================================================== c [1mFound solution: 10303321[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 2159 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 61 | 1912357 5565815 | 637452 59 2568 43.5 | 0.000 % | c ============================================================================== c [1mFound solution: 8257359[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 21 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 66 | 1912404 5566011 | 637468 64 2644 41.3 | 0.000 % | c | 170 | 1912404 5566011 | 701214 168 30730 182.9 | 0.018 % | c | 321 | 1912404 5566011 | 771336 319 40443 126.8 | 0.018 % | c | 546 | 1912404 5566011 | 848469 544 51337 94.4 | 0.018 % | c | 883 | 1912404 5566011 | 933316 881 124886 141.8 | 0.018 % | c | 1390 | 1912404 5566011 | 1026648 1388 159195 114.7 | 0.018 % | c ============================================================================== c [1mFound solution: 8170590[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 19 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1499 | 1912426 5566064 | 637475 1497 164057 109.6 | 0.018 % | c ============================================================================== c [1mFound solution: 6944472[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 1501 | 1912455 5566143 | 637485 1499 164093 109.5 | 0.018 % | c | 1603 | 1912455 5566143 | 701233 1601 189894 118.6 | 0.019 % | c | 1753 | 1912455 5566143 | 771356 1751 196656 112.3 | 0.019 % | c | 1978 | 1912455 5566143 | 848492 1976 213529 108.1 | 0.019 % | c | 2317 | 1912455 5566143 | 933341 2315 227568 98.3 | 0.019 % | c | 2825 | 1912455 5566143 | 1026675 2823 263097 93.2 | 0.019 % | c | 3585 | 1912455 5566143 | 1129343 3583 302077 84.3 | 0.019 % | c ============================================================================== c [1mFound solution: 6819989[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 20 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 3604 | 1912481 5566205 | 637493 3602 303059 84.1 | 0.019 % | c | 3705 | 1912481 5566205 | 701242 3703 308842 83.4 | 0.019 % | c | 3857 | 1912481 5566205 | 771366 3855 339437 88.1 | 0.019 % | c | 4082 | 1912481 5566205 | 848503 4080 351848 86.2 | 0.019 % | c ============================================================================== c [1mFound solution: 6788725[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 17 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 4168 | 1912497 5566247 | 637499 4166 355871 85.4 | 0.019 % | c | 4269 | 1912497 5566247 | 701248 4267 380365 89.1 | 0.019 % | c | 4420 | 1912497 5566247 | 771373 4418 390683 88.4 | 0.019 % | c | 4647 | 1912497 5566247 | 848511 4645 403739 86.9 | 0.019 % | c | 4984 | 1912497 5566247 | 933362 4982 429461 86.2 | 0.019 % | c | 5490 | 1912497 5566247 | 1026698 5488 470098 85.7 | 0.019 % | c | 6249 | 1912497 5566247 | 1129368 6247 519979 83.2 | 0.019 % | c | 7389 | 1912497 5566247 | 1242305 7387 597583 80.9 | 0.019 % | c | 9098 | 1912497 5566247 | 1366535 9096 690914 76.0 | 0.019 % | #### 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.74 0.86 0.87 2/54 23283 Raw data (stat): 23283 (runsolver) R 23282 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 539592019 1052672 99 4294967295 134512640 135381576 3221224416 3221219660 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+9.99993 s] Raw data (loadavg): 0.78 0.86 0.87 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 54458 0 0 0 875 124 0 0 25 0 1 0 539592019 244772864 49803 4294967295 134512640 134672761 3221224528 3221205744 134566692 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 59759 49803 603 41 0 59718 0 vsize: 239036 [startup+19.9995 s] Raw data (loadavg): 0.81 0.87 0.87 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61120 0 0 0 1858 141 0 0 25 0 1 0 539592019 266805248 56465 4294967295 134512640 134672761 3221224528 3221223860 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 65138 56465 603 41 0 65097 0 vsize: 260552 [startup+30.0007 s] Raw data (loadavg): 0.84 0.87 0.87 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61206 0 0 0 2857 142 0 0 25 0 1 0 539592019 269873152 56551 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 65887 56551 603 41 0 65846 0 vsize: 263548 [startup+40 s] Raw data (loadavg): 0.86 0.87 0.87 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61376 0 0 0 3856 142 0 0 25 0 1 0 539592019 270790656 56716 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 66111 56716 603 41 0 66070 0 vsize: 264444 [startup+50.0007 s] Raw data (loadavg): 0.96 0.89 0.88 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61382 0 0 0 4856 143 0 0 25 0 1 0 539592019 270921728 56722 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 66143 56722 603 41 0 66102 0 vsize: 264572 [startup+60.0008 s] Raw data (loadavg): 1.04 0.91 0.89 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61392 0 0 0 5856 143 0 0 25 0 1 0 539592019 270921728 56732 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 66143 56732 603 41 0 66102 0 vsize: 264572 [startup+70.0011 s] Raw data (loadavg): 1.04 0.91 0.89 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61443 0 0 0 6856 143 0 0 25 0 1 0 539592019 271056896 56783 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 66176 56783 603 41 0 66135 0 vsize: 264704 [startup+80.0018 s] Raw data (loadavg): 1.03 0.92 0.89 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61488 0 0 0 7856 143 0 0 25 0 1 0 539592019 271331328 56828 4294967295 134512640 134672761 3221224528 3221223668 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 66243 56828 603 41 0 66202 0 vsize: 264972 [startup+90.002 s] Raw data (loadavg): 1.02 0.92 0.89 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61500 0 0 0 8856 144 0 0 25 0 1 0 539592019 271331328 56840 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 66243 56840 603 41 0 66202 0 vsize: 264972 [startup+100.002 s] Raw data (loadavg): 1.02 0.92 0.89 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61510 0 0 0 9855 144 0 0 25 0 1 0 539592019 271331328 56850 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66243 56850 603 41 0 66202 0 vsize: 264972 [startup+110.002 s] Raw data (loadavg): 1.02 0.92 0.89 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61518 0 0 0 10855 144 0 0 25 0 1 0 539592019 271462400 56858 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66275 56858 603 41 0 66234 0 vsize: 265100 [startup+120.002 s] Raw data (loadavg): 1.01 0.92 0.89 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61525 0 0 0 11855 144 0 0 25 0 1 0 539592019 271462400 56865 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66275 56865 603 41 0 66234 0 vsize: 265100 [startup+130.002 s] Raw data (loadavg): 1.01 0.93 0.89 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61554 0 0 0 12856 144 0 0 25 0 1 0 539592019 271462400 56894 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66275 56894 603 41 0 66234 0 vsize: 265100 [startup+140.002 s] Raw data (loadavg): 1.01 0.93 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61575 0 0 0 13855 145 0 0 25 0 1 0 539592019 271597568 56915 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66308 56915 603 41 0 66267 0 vsize: 265232 [startup+150.019 s] Raw data (loadavg): 1.01 0.93 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61581 0 0 0 14857 145 0 0 25 0 1 0 539592019 271597568 56921 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66308 56921 603 41 0 66267 0 vsize: 265232 [startup+160.019 s] Raw data (loadavg): 1.01 0.93 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61587 0 0 0 15857 145 0 0 25 0 1 0 539592019 271597568 56927 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66308 56927 603 41 0 66267 0 vsize: 265232 [startup+170.02 s] Raw data (loadavg): 1.00 0.93 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61594 0 0 0 16857 145 0 0 25 0 1 0 539592019 271597568 56934 4294967295 134512640 134672761 3221224528 3221223632 134560250 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66308 56934 603 41 0 66267 0 vsize: 265232 [startup+180.02 s] Raw data (loadavg): 1.00 0.94 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61602 0 0 0 17857 145 0 0 25 0 1 0 539592019 271732736 56942 4294967295 134512640 134672761 3221224528 3221223664 134560688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66341 56942 603 41 0 66300 0 vsize: 265364 [startup+190.024 s] Raw data (loadavg): 1.00 0.94 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61612 0 0 0 18858 145 0 0 25 0 1 0 539592019 271732736 56952 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66341 56952 603 41 0 66300 0 vsize: 265364 [startup+200.024 s] Raw data (loadavg): 1.00 0.94 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61622 0 0 0 19858 145 0 0 25 0 1 0 539592019 271732736 56962 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66341 56962 603 41 0 66300 0 vsize: 265364 [startup+210.024 s] Raw data (loadavg): 1.00 0.94 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61630 0 0 0 20858 145 0 0 25 0 1 0 539592019 271867904 56970 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66374 56970 603 41 0 66333 0 vsize: 265496 [startup+220.033 s] Raw data (loadavg): 1.00 0.94 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61642 0 0 0 21859 145 0 0 25 0 1 0 539592019 271867904 56982 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66374 56982 603 41 0 66333 0 vsize: 265496 [startup+230.032 s] Raw data (loadavg): 1.00 0.94 0.90 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61647 0 0 0 22859 145 0 0 25 0 1 0 539592019 271867904 56987 4294967295 134512640 134672761 3221224528 3221223728 134557885 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66374 56987 603 41 0 66333 0 vsize: 265496 [startup+240.032 s] Raw data (loadavg): 1.00 0.94 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61654 0 0 0 23859 145 0 0 25 0 1 0 539592019 271867904 56994 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66374 56994 603 41 0 66333 0 vsize: 265496 [startup+250.033 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61662 0 0 0 24859 145 0 0 25 0 1 0 539592019 271867904 57002 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66374 57002 603 41 0 66333 0 vsize: 265496 [startup+260.038 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61669 0 0 0 25860 145 0 0 25 0 1 0 539592019 271998976 57009 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66406 57009 603 41 0 66365 0 vsize: 265624 [startup+270.075 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61676 0 0 0 26864 145 0 0 25 0 1 0 539592019 271998976 57016 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66406 57016 603 41 0 66365 0 vsize: 265624 [startup+280.075 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61685 0 0 0 27864 145 0 0 25 0 1 0 539592019 271998976 57025 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66406 57025 603 41 0 66365 0 vsize: 265624 [startup+290.076 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61693 0 0 0 28864 145 0 0 25 0 1 0 539592019 271998976 57033 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66406 57033 603 41 0 66365 0 vsize: 265624 [startup+300.076 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61697 0 0 0 29864 145 0 0 25 0 1 0 539592019 272130048 57037 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66438 57037 603 41 0 66397 0 vsize: 265752 [startup+310.075 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61703 0 0 0 30864 145 0 0 25 0 1 0 539592019 272130048 57043 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66438 57043 603 41 0 66397 0 vsize: 265752 [startup+320.075 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61710 0 0 0 31865 145 0 0 25 0 1 0 539592019 272130048 57050 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66438 57050 603 41 0 66397 0 vsize: 265752 [startup+330.076 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61717 0 0 0 32865 145 0 0 25 0 1 0 539592019 272130048 57057 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 66438 57057 603 41 0 66397 0 vsize: 265752 [startup+340.075 s] Raw data (loadavg): 1.00 0.95 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61731 0 0 0 33864 145 0 0 25 0 1 0 539592019 272130048 57071 4294967295 134512640 134672761 3221224528 3221223664 134560677 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66438 57071 603 41 0 66397 0 vsize: 265752 [startup+350.076 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61765 0 0 0 34864 145 0 0 25 0 1 0 539592019 272265216 57105 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66471 57105 603 41 0 66430 0 vsize: 265884 [startup+360.091 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61769 0 0 0 35866 145 0 0 25 0 1 0 539592019 272400384 57109 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66504 57109 603 41 0 66463 0 vsize: 266016 [startup+370.092 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61781 0 0 0 36866 145 0 0 25 0 1 0 539592019 272400384 57121 4294967295 134512640 134672761 3221224528 3221223632 134560260 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66504 57121 603 41 0 66463 0 vsize: 266016 [startup+380.095 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61810 0 0 0 37867 145 0 0 25 0 1 0 539592019 272535552 57150 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66537 57150 603 41 0 66496 0 vsize: 266148 [startup+390.095 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61817 0 0 0 38867 146 0 0 25 0 1 0 539592019 272535552 57157 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66537 57157 603 41 0 66496 0 vsize: 266148 [startup+400.096 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61824 0 0 0 39867 146 0 0 25 0 1 0 539592019 272535552 57164 4294967295 134512640 134672761 3221224528 3221223712 134559038 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66537 57164 603 41 0 66496 0 vsize: 266148 [startup+410.106 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61832 0 0 0 40868 146 0 0 25 0 1 0 539592019 272666624 57172 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66569 57172 603 41 0 66528 0 vsize: 266276 [startup+420.107 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61838 0 0 0 41868 146 0 0 25 0 1 0 539592019 272666624 57178 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66569 57178 603 41 0 66528 0 vsize: 266276 [startup+430.111 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61849 0 0 0 42868 146 0 0 25 0 1 0 539592019 272666624 57189 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66569 57189 603 41 0 66528 0 vsize: 266276 [startup+440.11 s] Raw data (loadavg): 1.00 0.96 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61859 0 0 0 43868 146 0 0 25 0 1 0 539592019 272666624 57199 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66569 57199 603 41 0 66528 0 vsize: 266276 [startup+450.11 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61867 0 0 0 44858 146 0 0 25 0 1 0 539592019 272801792 57207 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66602 57207 603 41 0 66561 0 vsize: 266408 [startup+460.11 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61876 0 0 0 45858 146 0 0 25 0 1 0 539592019 272801792 57216 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66602 57216 603 41 0 66561 0 vsize: 266408 [startup+470.111 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61886 0 0 0 46858 146 0 0 25 0 1 0 539592019 272801792 57226 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66602 57226 603 41 0 66561 0 vsize: 266408 [startup+480.131 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61897 0 0 0 47860 146 0 0 25 0 1 0 539592019 272928768 57237 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66633 57237 603 41 0 66592 0 vsize: 266532 [startup+490.136 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61904 0 0 0 48861 146 0 0 25 0 1 0 539592019 272928768 57244 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66633 57244 603 41 0 66592 0 vsize: 266532 [startup+500.137 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61911 0 0 0 49861 146 0 0 25 0 1 0 539592019 272928768 57251 4294967295 134512640 134672761 3221224528 3221223696 134561378 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66633 57251 603 41 0 66592 0 vsize: 266532 [startup+510.136 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61922 0 0 0 50861 146 0 0 25 0 1 0 539592019 272928768 57262 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66633 57262 603 41 0 66592 0 vsize: 266532 [startup+520.137 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61930 0 0 0 51861 146 0 0 25 0 1 0 539592019 273059840 57270 4294967295 134512640 134672761 3221224528 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66665 57270 603 41 0 66624 0 vsize: 266660 [startup+530.138 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61940 0 0 0 52861 146 0 0 25 0 1 0 539592019 273059840 57280 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66665 57280 603 41 0 66624 0 vsize: 266660 [startup+540.138 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61947 0 0 0 53862 146 0 0 25 0 1 0 539592019 273059840 57287 4294967295 134512640 134672761 3221224528 3221223728 134557897 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66665 57287 603 41 0 66624 0 vsize: 266660 [startup+550.14 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61955 0 0 0 54862 146 0 0 25 0 1 0 539592019 273059840 57295 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66665 57295 603 41 0 66624 0 vsize: 266660 [startup+560.14 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61963 0 0 0 55862 146 0 0 25 0 1 0 539592019 273195008 57303 4294967295 134512640 134672761 3221224528 3221223632 134560287 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66698 57303 603 41 0 66657 0 vsize: 266792 [startup+570.139 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61969 0 0 0 56862 146 0 0 25 0 1 0 539592019 273195008 57309 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66698 57309 603 41 0 66657 0 vsize: 266792 [startup+580.139 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61974 0 0 0 57862 146 0 0 25 0 1 0 539592019 273195008 57314 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66698 57314 603 41 0 66657 0 vsize: 266792 [startup+590.139 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61980 0 0 0 58862 146 0 0 25 0 1 0 539592019 273195008 57320 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66698 57320 603 41 0 66657 0 vsize: 266792 [startup+600.14 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61985 0 0 0 59863 146 0 0 25 0 1 0 539592019 273195008 57325 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66698 57325 603 41 0 66657 0 vsize: 266792 [startup+610.141 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61989 0 0 0 60863 147 0 0 25 0 1 0 539592019 273195008 57329 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66698 57329 603 41 0 66657 0 vsize: 266792 [startup+620.141 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 61995 0 0 0 61863 147 0 0 25 0 1 0 539592019 273330176 57335 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66731 57335 603 41 0 66690 0 vsize: 266924 [startup+630.157 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62002 0 0 0 62865 147 0 0 25 0 1 0 539592019 273330176 57342 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66731 57342 603 41 0 66690 0 vsize: 266924 [startup+640.178 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62010 0 0 0 63867 147 0 0 25 0 1 0 539592019 273330176 57350 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66731 57350 603 41 0 66690 0 vsize: 266924 [startup+650.178 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62020 0 0 0 64867 147 0 0 25 0 1 0 539592019 273330176 57360 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66731 57360 603 41 0 66690 0 vsize: 266924 [startup+660.178 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62023 0 0 0 65867 147 0 0 25 0 1 0 539592019 273330176 57363 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66731 57363 603 41 0 66690 0 vsize: 266924 [startup+670.178 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62030 0 0 0 66867 147 0 0 25 0 1 0 539592019 273461248 57370 4294967295 134512640 134672761 3221224528 3221223712 134559033 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66763 57370 603 41 0 66722 0 vsize: 267052 [startup+680.178 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62034 0 0 0 67868 147 0 0 25 0 1 0 539592019 273461248 57374 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66763 57374 603 41 0 66722 0 vsize: 267052 [startup+690.178 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62039 0 0 0 68868 147 0 0 25 0 1 0 539592019 273461248 57379 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66763 57379 603 41 0 66722 0 vsize: 267052 [startup+700.179 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62044 0 0 0 69868 147 0 0 25 0 1 0 539592019 273461248 57384 4294967295 134512640 134672761 3221224528 3221223632 134560198 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66763 57384 603 41 0 66722 0 vsize: 267052 [startup+710.179 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62056 0 0 0 70867 147 0 0 25 0 1 0 539592019 273461248 57396 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66763 57396 603 41 0 66722 0 vsize: 267052 [startup+720.179 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62065 0 0 0 71867 147 0 0 25 0 1 0 539592019 273592320 57405 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66795 57405 603 41 0 66754 0 vsize: 267180 [startup+730.181 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62075 0 0 0 72867 147 0 0 25 0 1 0 539592019 273592320 57415 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66795 57415 603 41 0 66754 0 vsize: 267180 [startup+740.18 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62085 0 0 0 73867 148 0 0 25 0 1 0 539592019 273592320 57425 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66795 57425 603 41 0 66754 0 vsize: 267180 [startup+750.183 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62101 0 0 0 74868 148 0 0 25 0 1 0 539592019 273727488 57441 4294967295 134512640 134672761 3221224528 3221223664 134560596 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66828 57441 603 41 0 66787 0 vsize: 267312 [startup+760.183 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62106 0 0 0 75868 148 0 0 25 0 1 0 539592019 273727488 57446 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66828 57446 603 41 0 66787 0 vsize: 267312 [startup+770.183 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62117 0 0 0 76868 148 0 0 25 0 1 0 539592019 273727488 57457 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66828 57457 603 41 0 66787 0 vsize: 267312 [startup+780.184 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62127 0 0 0 77868 148 0 0 25 0 1 0 539592019 273862656 57467 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66861 57467 603 41 0 66820 0 vsize: 267444 [startup+790.183 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62139 0 0 0 78868 148 0 0 25 0 1 0 539592019 273862656 57479 4294967295 134512640 134672761 3221224528 3221223728 134557849 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66861 57479 603 41 0 66820 0 vsize: 267444 [startup+800.184 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62154 0 0 0 79868 148 0 0 25 0 1 0 539592019 274001920 57494 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 66895 57494 603 41 0 66854 0 vsize: 267580 [startup+810.185 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62280 0 0 0 80868 148 0 0 25 0 1 0 539592019 274444288 57620 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67003 57620 603 41 0 66962 0 vsize: 268012 [startup+820.184 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62439 0 0 0 81868 148 0 0 25 0 1 0 539592019 275140608 57779 4294967295 134512640 134672761 3221224528 3221223680 134561040 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67173 57779 603 41 0 67132 0 vsize: 268692 [startup+830.185 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62584 0 0 0 82868 149 0 0 25 0 1 0 539592019 275705856 57924 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67311 57924 603 41 0 67270 0 vsize: 269244 [startup+840.185 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62748 0 0 0 83867 150 0 0 25 0 1 0 539592019 276393984 58088 4294967295 134512640 134672761 3221224528 3221223696 134561127 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67479 58088 603 41 0 67438 0 vsize: 269916 [startup+850.186 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 62891 0 0 0 84867 150 0 0 25 0 1 0 539592019 276938752 58231 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67612 58231 603 41 0 67571 0 vsize: 270448 [startup+860.186 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63005 0 0 0 85867 151 0 0 25 0 1 0 539592019 277368832 58345 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67717 58345 603 41 0 67676 0 vsize: 270868 [startup+870.186 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63093 0 0 0 86867 151 0 0 25 0 1 0 539592019 277774336 58433 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67816 58433 603 41 0 67775 0 vsize: 271264 [startup+880.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63255 0 0 0 87867 151 0 0 25 0 1 0 539592019 278495232 58595 4294967295 134512640 134672761 3221224528 3221223632 134560154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 67992 58595 603 41 0 67951 0 vsize: 271968 [startup+890.186 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63366 0 0 0 88867 151 0 0 25 0 1 0 539592019 278913024 58706 4294967295 134512640 134672761 3221224528 3221223696 134560895 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68094 58706 603 41 0 68053 0 vsize: 272376 [startup+900.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63423 0 0 0 89867 151 0 0 25 0 1 0 539592019 279207936 58763 4294967295 134512640 134672761 3221224528 3221223632 134560303 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68166 58763 603 41 0 68125 0 vsize: 272664 [startup+910.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63438 0 0 0 90867 151 0 0 25 0 1 0 539592019 279207936 58778 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68166 58778 603 41 0 68125 0 vsize: 272664 [startup+920.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63453 0 0 0 91867 151 0 0 25 0 1 0 539592019 279207936 58793 4294967295 134512640 134672761 3221224528 3221223632 134560291 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68166 58793 603 41 0 68125 0 vsize: 272664 [startup+930.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63473 0 0 0 92867 151 0 0 25 0 1 0 539592019 279351296 58813 4294967295 134512640 134672761 3221224528 3221223632 134559835 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68201 58813 603 41 0 68160 0 vsize: 272804 [startup+940.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63508 0 0 0 93867 152 0 0 25 0 1 0 539592019 279490560 58848 4294967295 134512640 134672761 3221224528 3221223632 134560267 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68235 58848 603 41 0 68194 0 vsize: 272940 [startup+950.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63557 0 0 0 94867 152 0 0 25 0 1 0 539592019 279642112 58897 4294967295 134512640 134672761 3221224528 3221223632 134559869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68272 58897 603 41 0 68231 0 vsize: 273088 [startup+960.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63572 0 0 0 95868 152 0 0 25 0 1 0 539592019 279781376 58912 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68306 58912 603 41 0 68265 0 vsize: 273224 [startup+970.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63601 0 0 0 96867 152 0 0 25 0 1 0 539592019 279920640 58941 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68340 58941 603 41 0 68299 0 vsize: 273360 [startup+980.187 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63627 0 0 0 97868 152 0 0 25 0 1 0 539592019 280055808 58967 4294967295 134512640 134672761 3221224528 3221223632 134559853 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68373 58967 603 41 0 68332 0 vsize: 273492 [startup+990.188 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63647 0 0 0 98867 152 0 0 25 0 1 0 539592019 280055808 58987 4294967295 134512640 134672761 3221224528 3221223632 134560529 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68373 58987 603 41 0 68332 0 vsize: 273492 [startup+1000.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63667 0 0 0 99868 152 0 0 25 0 1 0 539592019 280199168 59007 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68408 59007 603 41 0 68367 0 vsize: 273632 [startup+1010.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63686 0 0 0 100868 152 0 0 25 0 1 0 539592019 280199168 59026 4294967295 134512640 134672761 3221224528 3221223632 134560405 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68408 59026 603 41 0 68367 0 vsize: 273632 [startup+1020.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63715 0 0 0 101868 152 0 0 25 0 1 0 539592019 280322048 59055 4294967295 134512640 134672761 3221224528 3221223632 134560237 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68438 59055 603 41 0 68397 0 vsize: 273752 [startup+1030.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63736 0 0 0 102868 152 0 0 25 0 1 0 539592019 280469504 59076 4294967295 134512640 134672761 3221224528 3221223632 134559902 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68474 59076 603 41 0 68433 0 vsize: 273896 [startup+1040.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63756 0 0 0 103868 153 0 0 25 0 1 0 539592019 280469504 59096 4294967295 134512640 134672761 3221224528 3221223632 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68474 59096 603 41 0 68433 0 vsize: 273896 [startup+1050.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63771 0 0 0 104868 153 0 0 25 0 1 0 539592019 280612864 59111 4294967295 134512640 134672761 3221224528 3221223632 134560054 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68509 59111 603 41 0 68468 0 vsize: 274036 [startup+1060.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63791 0 0 0 105868 153 0 0 25 0 1 0 539592019 280612864 59131 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68509 59131 603 41 0 68468 0 vsize: 274036 [startup+1070.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63806 0 0 0 106868 153 0 0 25 0 1 0 539592019 280756224 59146 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68544 59146 603 41 0 68503 0 vsize: 274176 [startup+1080.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63826 0 0 0 107868 153 0 0 25 0 1 0 539592019 280756224 59166 4294967295 134512640 134672761 3221224528 3221223632 134560201 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68544 59166 603 41 0 68503 0 vsize: 274176 [startup+1090.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63842 0 0 0 108869 153 0 0 25 0 1 0 539592019 280903680 59182 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68580 59182 603 41 0 68539 0 vsize: 274320 [startup+1100.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63874 0 0 0 109869 153 0 0 25 0 1 0 539592019 281055232 59214 4294967295 134512640 134672761 3221224528 3221223632 134559851 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68617 59214 603 41 0 68576 0 vsize: 274468 [startup+1110.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63894 0 0 0 110869 153 0 0 25 0 1 0 539592019 281055232 59234 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68617 59234 603 41 0 68576 0 vsize: 274468 [startup+1120.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63910 0 0 0 111869 153 0 0 25 0 1 0 539592019 281198592 59250 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68652 59250 603 41 0 68611 0 vsize: 274608 [startup+1130.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63930 0 0 0 112869 154 0 0 25 0 1 0 539592019 281198592 59270 4294967295 134512640 134672761 3221224528 3221223632 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68652 59270 603 41 0 68611 0 vsize: 274608 [startup+1140.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63951 0 0 0 113869 154 0 0 25 0 1 0 539592019 281341952 59291 4294967295 134512640 134672761 3221224528 3221223632 134560504 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68687 59291 603 41 0 68646 0 vsize: 274748 [startup+1150.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63968 0 0 0 114869 154 0 0 25 0 1 0 539592019 281341952 59308 4294967295 134512640 134672761 3221224528 3221223632 134559887 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68687 59308 603 41 0 68646 0 vsize: 274748 [startup+1160.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 63983 0 0 0 115869 154 0 0 25 0 1 0 539592019 281477120 59323 4294967295 134512640 134672761 3221224528 3221223632 134560492 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68720 59323 603 41 0 68679 0 vsize: 274880 [startup+1170.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 64005 0 0 0 116869 154 0 0 25 0 1 0 539592019 281477120 59345 4294967295 134512640 134672761 3221224528 3221223632 134560008 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68720 59345 603 41 0 68679 0 vsize: 274880 [startup+1180.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 64026 0 0 0 117869 154 0 0 25 0 1 0 539592019 281612288 59366 4294967295 134512640 134672761 3221224528 3221223632 134559949 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68753 59366 603 41 0 68712 0 vsize: 275012 [startup+1190.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 64041 0 0 0 118870 154 0 0 25 0 1 0 539592019 281612288 59381 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68753 59381 603 41 0 68712 0 vsize: 275012 [startup+1200.19 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 23283 Raw data (stat): 23283 (minisat+) R 23282 27565 27564 0 -1 0 64061 0 0 0 119870 154 0 0 25 0 1 0 539592019 281755648 59401 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 68788 59401 603 41 0 68747 0 vsize: 275152 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.31 s] Raw data (loadavg): 1.00 0.97 0.91 1/54 23283 Raw data (stat): 23283 (minisat+) Z 23282 27565 27564 0 -1 12 64064 0 0 0 119870 166 0 0 25 0 1 0 539592019 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.31 CPU time (s): 1200.37 CPU user time (s): 1198.7 CPU system time (s): 1.66575 CPU usage (%): 100.005 Max. virtual memory (Kb): 275152 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####