Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-markshare2.opb |
MD5SUM | 3b5121187baf09367bd50bdc4d869d21 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 8448 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 140 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 7340025 |
Number of bits of the sum of numbers in the objective function | 23 |
Biggest number in a constraint | 524288 |
Number of bits of the biggest number in a constraint | 20 |
Biggest sum of numbers in a constraint | 7340025 |
Number of bits of the biggest sum of numbers | 23 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1175.43 |
Number of variables | 200 |
Total number of constraints | 67 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 60 |
Number of constraints which are nor clauses,nor cardinality constraints | 7 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 80 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc24 THE 2005-04-21 04:17:13 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17653 boxname=wulflinc24 idbench=1358 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 3b5121187baf09367bd50bdc4d869d21 /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-13-7-markshare2.opb IDLAUNCH: 17653 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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 : 890.88 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.080 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: 595944 kB Buffers: 4688 kB Cached: 406280 kB SwapCached: 432 kB Active: 23844 kB Inactive: 389268 kB HighTotal: 131008 kB HighFree: 4256 kB LowTotal: 903652 kB LowFree: 591688 kB SwapTotal: 2097892 kB SwapFree: 2096708 kB Dirty: 40 kB Writeback: 0 kB Mapped: 5932 kB Slab: 19904 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 04:37:15 (client local time) WITH STATUS 10 IN 1200.39 SECONDS stats: 17653 7 1200.39 10 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 14 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ####### c -- Clauses(.)/Splits(s): (none) c ---[ 12]---> BDD-cost:33297 c ---[ 10]---> BDD-cost:39178 c ---[ 8]---> BDD-cost:34986 c ---[ 6]---> BDD-cost:41587 c ---[ 4]---> BDD-cost:41667 c ---[ 2]---> BDD-cost:41235 c ---[ 0]---> BDD-cost:35324 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 774400 2270366 | 258133 0 0 nan | 0.000 % | c | 100 | 774400 2270366 | 283946 100 9452 94.5 | 0.008 % | c ============================================================================== c [1mFound solution: 1159424[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 1831 Base: 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 | 103 | 779065 2281260 | 259688 103 9521 92.4 | 0.008 % | c ============================================================================== c [1mFound solution: 1091328[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 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 | 106 | 779085 2281332 | 259695 106 9583 90.4 | 0.008 % | c ============================================================================== c [1mFound solution: 1085440[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 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 | 135 | 779100 2281371 | 259700 135 10953 81.1 | 0.008 % | c | 236 | 779100 2281371 | 285670 236 16182 68.6 | 0.009 % | c | 388 | 779100 2281371 | 314237 388 24371 62.8 | 0.009 % | c ============================================================================== c [1mFound solution: 1079936[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 12 Base: 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 | 505 | 779117 2281412 | 259705 505 30585 60.6 | 0.009 % | c ============================================================================== c [1mFound solution: 1076480[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 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 | 532 | 779128 2281439 | 259709 532 32305 60.7 | 0.009 % | c ============================================================================== c [1mFound solution: 1060480[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 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 | 625 | 779138 2281463 | 259712 625 37233 59.6 | 0.009 % | c ============================================================================== c [1mFound solution: 1056384[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 7 Base: 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 | 712 | 779146 2281481 | 259715 712 41686 58.5 | 0.009 % | c ============================================================================== c [1mFound solution: 961664[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 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 | 713 | 779162 2281520 | 259720 713 41751 58.6 | 0.009 % | c | 813 | 779162 2281520 | 285692 813 46693 57.4 | 0.011 % | c | 965 | 779162 2281520 | 314261 965 54953 56.9 | 0.011 % | c ============================================================================== c [1mFound solution: 953600[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 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 | 992 | 779170 2281538 | 259723 992 56372 56.8 | 0.011 % | c ============================================================================== c [1mFound solution: 948480[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 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 | 1064 | 779178 2281559 | 259726 1064 59130 55.6 | 0.011 % | c ============================================================================== c [1mFound solution: 928256[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 10 Base: 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 | 1068 | 779193 2281593 | 259731 1068 59470 55.7 | 0.011 % | c | 1168 | 779193 2281593 | 285704 1168 64070 54.9 | 0.012 % | c | 1318 | 779193 2281593 | 314274 1318 70952 53.8 | 0.012 % | c | 1543 | 779193 2281593 | 345701 1543 84455 54.7 | 0.012 % | c | 1880 | 779193 2281593 | 380272 1880 104095 55.4 | 0.012 % | c ============================================================================== c [1mFound solution: 907904[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 6 Base: 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 | 1929 | 779212 2281644 | 259737 1929 106696 55.3 | 0.012 % | c | 2031 | 779212 2281644 | 285710 2031 110666 54.5 | 0.012 % | c | 2183 | 779212 2281644 | 314281 2183 119905 54.9 | 0.012 % | c | 2408 | 779212 2281644 | 345709 2408 131349 54.5 | 0.012 % | c ============================================================================== c [1mFound solution: 876032[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 9 Base: 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 | 2411 | 779223 2281675 | 259741 2411 131543 54.6 | 0.012 % | c | 2511 | 779223 2281675 | 285715 2511 137169 54.6 | 0.013 % | c | 2663 | 779223 2281675 | 314286 2663 144243 54.2 | 0.013 % | c | 2888 | 779223 2281675 | 345715 2888 158492 54.9 | 0.013 % | c ============================================================================== c [1mFound solution: 864000[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 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 | 2918 | 779234 2281701 | 259744 2918 160062 54.9 | 0.013 % | c | 3018 | 779234 2281701 | 285718 3018 165023 54.7 | 0.013 % | c ============================================================================== c [1mFound solution: 848384[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 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 | 3047 | 779241 2281720 | 259747 3047 166723 54.7 | 0.013 % | c ============================================================================== c [1mFound solution: 845440[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 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 | 3141 | 779250 2281743 | 259750 3141 171715 54.7 | 0.013 % | c | 3242 | 779250 2281743 | 285725 3242 177415 54.7 | 0.014 % | c | 3392 | 779250 2281743 | 314297 3392 186259 54.9 | 0.014 % | c | 3617 | 779250 2281743 | 345727 3617 199709 55.2 | 0.014 % | c | 3954 | 779250 2281743 | 380299 3954 219820 55.6 | 0.014 % | c ============================================================================== c [1mFound solution: 839552[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 11 Base: 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 | 4285 | 779259 2281768 | 259753 4285 236652 55.2 | 0.014 % | c | 4385 | 779259 2281768 | 285728 4385 241366 55.0 | 0.014 % | c | 4535 | 779259 2281768 | 314301 4535 250113 55.2 | 0.014 % | c | 4760 | 779259 2281768 | 345731 4760 262030 55.0 | 0.014 % | c ============================================================================== c [1mFound solution: 825344[0m c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): (none) c ---[ 0]---> Sorter-cost: 8 Base: 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 | 4866 | 779271 2281796 | 259757 4866 267684 55.0 | 0.014 % | c | 4966 | 779271 2281796 | 285732 4966 272049 54.8 | 0.015 % | c | 5116 | 779271 2281796 | 314305 5116 282890 55.3 | 0.015 % | c | 5341 | 779271 2281796 | 345736 5341 296320 55.5 | 0.015 % | c | 5678 | 779271 2281796 | 380310 5678 313256 55.2 | 0.015 % | c | 6184 | 779271 2281796 | 418341 6184 341829 55.3 | 0.015 % | c | 6943 | 779271 2281796 | 460175 6943 391438 56.4 | 0.015 % | c | 8084 | 779271 2281796 | 506192 8084 471022 58.3 | 0.015 % | c | 9792 | 779271 2281796 | 556812 9792 607154 62.0 | 0.015 % | c | 12355 | 779271 2281796 | 612493 12355 771229 62.4 | 0.015 % | c | 16199 | 779271 2281796 | 673742 16199 1017250 62.8 | 0.015 % | #### 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.86 0.97 0.92 2/54 24284 Raw data (stat): 24284 (runsolver) R 24283 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542129944 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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+10.0007 s] Raw data (loadavg): 0.88 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 24239 0 0 0 942 57 0 0 25 0 1 0 542129944 117608448 22668 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28713 22668 603 41 0 28672 0 vsize: 114852 [startup+20.0014 s] Raw data (loadavg): 0.90 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 24918 0 0 0 1940 59 0 0 25 0 1 0 542129944 121098240 23320 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29565 23320 603 41 0 29524 0 vsize: 118260 [startup+30.0017 s] Raw data (loadavg): 0.91 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 24964 0 0 0 2940 59 0 0 25 0 1 0 542129944 121581568 23366 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29683 23366 603 41 0 29642 0 vsize: 118732 [startup+40.0017 s] Raw data (loadavg): 0.92 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 24977 0 0 0 3939 59 0 0 25 0 1 0 542129944 121716736 23379 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29716 23379 603 41 0 29675 0 vsize: 118864 [startup+50.0024 s] Raw data (loadavg): 0.94 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25000 0 0 0 4939 60 0 0 25 0 1 0 542129944 121716736 23402 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29716 23402 603 41 0 29675 0 vsize: 118864 [startup+60.0017 s] Raw data (loadavg): 0.95 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25012 0 0 0 5939 60 0 0 25 0 1 0 542129944 121847808 23414 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29748 23414 603 41 0 29707 0 vsize: 118992 [startup+70.0028 s] Raw data (loadavg): 0.95 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25023 0 0 0 6939 60 0 0 25 0 1 0 542129944 121847808 23425 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29748 23425 603 41 0 29707 0 vsize: 118992 [startup+80.0034 s] Raw data (loadavg): 0.96 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25040 0 0 0 7938 61 0 0 25 0 1 0 542129944 121982976 23442 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29781 23442 603 41 0 29740 0 vsize: 119124 [startup+90.0174 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25046 0 0 0 8939 62 0 0 25 0 1 0 542129944 121982976 23448 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29781 23448 603 41 0 29740 0 vsize: 119124 [startup+100.018 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25059 0 0 0 9938 62 0 0 25 0 1 0 542129944 121982976 23461 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29781 23461 603 41 0 29740 0 vsize: 119124 [startup+110.018 s] Raw data (loadavg): 0.97 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25069 0 0 0 10938 62 0 0 25 0 1 0 542129944 121982976 23471 4294967295 134512640 134672761 3221224528 3221223696 134560825 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29781 23471 603 41 0 29740 0 vsize: 119124 [startup+120.019 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25078 0 0 0 11938 63 0 0 25 0 1 0 542129944 122114048 23480 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29813 23480 603 41 0 29772 0 vsize: 119252 [startup+130.02 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25087 0 0 0 12938 63 0 0 25 0 1 0 542129944 122114048 23489 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29813 23489 603 41 0 29772 0 vsize: 119252 [startup+140.019 s] Raw data (loadavg): 0.98 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25100 0 0 0 13938 63 0 0 25 0 1 0 542129944 122114048 23502 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29813 23502 603 41 0 29772 0 vsize: 119252 [startup+150.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25111 0 0 0 14937 64 0 0 25 0 1 0 542129944 122245120 23513 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29845 23513 603 41 0 29804 0 vsize: 119380 [startup+160.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25121 0 0 0 15937 64 0 0 25 0 1 0 542129944 122245120 23523 4294967295 134512640 134672761 3221224528 3221223652 134566120 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29845 23523 603 41 0 29804 0 vsize: 119380 [startup+170.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25129 0 0 0 16937 64 0 0 25 0 1 0 542129944 122245120 23531 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29845 23531 603 41 0 29804 0 vsize: 119380 [startup+180.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25138 0 0 0 17937 64 0 0 25 0 1 0 542129944 122380288 23540 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29878 23540 603 41 0 29837 0 vsize: 119512 [startup+190.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25148 0 0 0 18938 64 0 0 25 0 1 0 542129944 122380288 23550 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29878 23550 603 41 0 29837 0 vsize: 119512 [startup+200.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25159 0 0 0 19938 64 0 0 25 0 1 0 542129944 122380288 23561 4294967295 134512640 134672761 3221224528 3221223664 134560647 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29878 23561 603 41 0 29837 0 vsize: 119512 [startup+210.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25167 0 0 0 20938 64 0 0 25 0 1 0 542129944 122380288 23569 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29878 23569 603 41 0 29837 0 vsize: 119512 [startup+220.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25175 0 0 0 21938 64 0 0 25 0 1 0 542129944 122515456 23577 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29911 23577 603 41 0 29870 0 vsize: 119644 [startup+230.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25184 0 0 0 22938 64 0 0 25 0 1 0 542129944 122515456 23586 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29911 23586 603 41 0 29870 0 vsize: 119644 [startup+240.02 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25193 0 0 0 23938 64 0 0 25 0 1 0 542129944 122515456 23595 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29911 23595 603 41 0 29870 0 vsize: 119644 [startup+250.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25203 0 0 0 24939 64 0 0 25 0 1 0 542129944 122650624 23605 4294967295 134512640 134672761 3221224528 3221223728 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29944 23605 603 41 0 29903 0 vsize: 119776 [startup+260.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25213 0 0 0 25939 64 0 0 25 0 1 0 542129944 122650624 23615 4294967295 134512640 134672761 3221224528 3221223632 134560418 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29944 23615 603 41 0 29903 0 vsize: 119776 [startup+270.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25223 0 0 0 26939 64 0 0 25 0 1 0 542129944 122650624 23625 4294967295 134512640 134672761 3221224528 3221223632 134560212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29944 23625 603 41 0 29903 0 vsize: 119776 [startup+280.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25234 0 0 0 27939 64 0 0 25 0 1 0 542129944 122798080 23636 4294967295 134512640 134672761 3221224528 3221223680 134561035 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29980 23636 603 41 0 29939 0 vsize: 119920 [startup+290.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25243 0 0 0 28939 64 0 0 25 0 1 0 542129944 122798080 23645 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29980 23645 603 41 0 29939 0 vsize: 119920 [startup+300.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25253 0 0 0 29939 64 0 0 25 0 1 0 542129944 122798080 23655 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29980 23655 603 41 0 29939 0 vsize: 119920 [startup+310.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25265 0 0 0 30939 64 0 0 25 0 1 0 542129944 122798080 23667 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29980 23667 603 41 0 29939 0 vsize: 119920 [startup+320.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25276 0 0 0 31939 65 0 0 25 0 1 0 542129944 122933248 23678 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30013 23678 603 41 0 29972 0 vsize: 120052 [startup+330.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25287 0 0 0 32939 65 0 0 25 0 1 0 542129944 122933248 23689 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30013 23689 603 41 0 29972 0 vsize: 120052 [startup+340.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25300 0 0 0 33940 65 0 0 25 0 1 0 542129944 122933248 23702 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30013 23702 603 41 0 29972 0 vsize: 120052 [startup+350.021 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25311 0 0 0 34940 65 0 0 25 0 1 0 542129944 123064320 23713 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30045 23713 603 41 0 30004 0 vsize: 120180 [startup+360.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25322 0 0 0 35940 65 0 0 25 0 1 0 542129944 123064320 23724 4294967295 134512640 134672761 3221224528 3221223696 134560871 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30045 23724 603 41 0 30004 0 vsize: 120180 [startup+370.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25332 0 0 0 36940 65 0 0 25 0 1 0 542129944 123064320 23734 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30045 23734 603 41 0 30004 0 vsize: 120180 [startup+380.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25339 0 0 0 37940 65 0 0 25 0 1 0 542129944 123199488 23741 4294967295 134512640 134672761 3221224528 3221223696 134560888 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30078 23741 603 41 0 30037 0 vsize: 120312 [startup+390.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25350 0 0 0 38940 65 0 0 25 0 1 0 542129944 123199488 23752 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30078 23752 603 41 0 30037 0 vsize: 120312 [startup+400.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25360 0 0 0 39940 65 0 0 25 0 1 0 542129944 123199488 23762 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30078 23762 603 41 0 30037 0 vsize: 120312 [startup+410.022 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25370 0 0 0 40940 66 0 0 25 0 1 0 542129944 123330560 23772 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30110 23772 603 41 0 30069 0 vsize: 120440 [startup+420.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25379 0 0 0 41940 66 0 0 25 0 1 0 542129944 123330560 23781 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30110 23781 603 41 0 30069 0 vsize: 120440 [startup+430.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25387 0 0 0 42940 66 0 0 25 0 1 0 542129944 123330560 23789 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30110 23789 603 41 0 30069 0 vsize: 120440 [startup+440.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25399 0 0 0 43940 66 0 0 25 0 1 0 542129944 123330560 23801 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30110 23801 603 41 0 30069 0 vsize: 120440 [startup+450.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25408 0 0 0 44940 66 0 0 25 0 1 0 542129944 123461632 23810 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30142 23810 603 41 0 30101 0 vsize: 120568 [startup+460.023 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25417 0 0 0 45941 66 0 0 25 0 1 0 542129944 123461632 23819 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30142 23819 603 41 0 30101 0 vsize: 120568 [startup+470.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25426 0 0 0 46941 66 0 0 25 0 1 0 542129944 123461632 23828 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30142 23828 603 41 0 30101 0 vsize: 120568 [startup+480.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25436 0 0 0 47941 66 0 0 25 0 1 0 542129944 123592704 23838 4294967295 134512640 134672761 3221224528 3221223632 134560246 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30174 23838 603 41 0 30133 0 vsize: 120696 [startup+490.024 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25445 0 0 0 48941 66 0 0 25 0 1 0 542129944 123592704 23847 4294967295 134512640 134672761 3221224528 3221223632 134560218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30174 23847 603 41 0 30133 0 vsize: 120696 [startup+500.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25456 0 0 0 49941 66 0 0 25 0 1 0 542129944 123592704 23858 4294967295 134512640 134672761 3221224528 3221223696 134560979 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30174 23858 603 41 0 30133 0 vsize: 120696 [startup+510.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25466 0 0 0 50941 66 0 0 25 0 1 0 542129944 123723776 23868 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30206 23868 603 41 0 30165 0 vsize: 120824 [startup+520.025 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25475 0 0 0 51942 66 0 0 25 0 1 0 542129944 123723776 23877 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30206 23877 603 41 0 30165 0 vsize: 120824 [startup+530.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25485 0 0 0 52942 66 0 0 25 0 1 0 542129944 123723776 23887 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30206 23887 603 41 0 30165 0 vsize: 120824 [startup+540.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25497 0 0 0 53942 67 0 0 25 0 1 0 542129944 123871232 23899 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30242 23899 603 41 0 30201 0 vsize: 120968 [startup+550.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25506 0 0 0 54942 67 0 0 25 0 1 0 542129944 123871232 23908 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30242 23908 603 41 0 30201 0 vsize: 120968 [startup+560.026 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25518 0 0 0 55942 67 0 0 25 0 1 0 542129944 123871232 23920 4294967295 134512640 134672761 3221224528 3221223632 134559875 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30242 23920 603 41 0 30201 0 vsize: 120968 [startup+570.027 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25530 0 0 0 56942 67 0 0 25 0 1 0 542129944 124026880 23932 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30280 23932 603 41 0 30239 0 vsize: 121120 [startup+580.027 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25543 0 0 0 57942 67 0 0 25 0 1 0 542129944 124026880 23945 4294967295 134512640 134672761 3221224528 3221223696 134561161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30280 23945 603 41 0 30239 0 vsize: 121120 [startup+590.031 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25555 0 0 0 58943 67 0 0 25 0 1 0 542129944 124026880 23957 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30280 23957 603 41 0 30239 0 vsize: 121120 [startup+600.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25565 0 0 0 59943 67 0 0 25 0 1 0 542129944 124157952 23967 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30312 23967 603 41 0 30271 0 vsize: 121248 [startup+610.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25576 0 0 0 60943 67 0 0 25 0 1 0 542129944 124157952 23978 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30312 23978 603 41 0 30271 0 vsize: 121248 [startup+620.033 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25588 0 0 0 61943 67 0 0 25 0 1 0 542129944 124157952 23990 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30312 23990 603 41 0 30271 0 vsize: 121248 [startup+630.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25600 0 0 0 62943 67 0 0 25 0 1 0 542129944 124289024 24002 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30344 24002 603 41 0 30303 0 vsize: 121376 [startup+640.032 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25611 0 0 0 63943 67 0 0 25 0 1 0 542129944 124289024 24013 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30344 24013 603 41 0 30303 0 vsize: 121376 [startup+650.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25625 0 0 0 64957 67 0 0 25 0 1 0 542129944 124424192 24027 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30377 24027 603 41 0 30336 0 vsize: 121508 [startup+660.169 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25634 0 0 0 65957 67 0 0 25 0 1 0 542129944 124424192 24036 4294967295 134512640 134672761 3221224528 3221223632 134560402 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30377 24036 603 41 0 30336 0 vsize: 121508 [startup+670.169 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25645 0 0 0 66957 68 0 0 25 0 1 0 542129944 124424192 24047 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30377 24047 603 41 0 30336 0 vsize: 121508 [startup+680.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25658 0 0 0 67957 68 0 0 25 0 1 0 542129944 124424192 24060 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30377 24060 603 41 0 30336 0 vsize: 121508 [startup+690.169 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25669 0 0 0 68957 68 0 0 25 0 1 0 542129944 124555264 24071 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30409 24071 603 41 0 30368 0 vsize: 121636 [startup+700.169 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25678 0 0 0 69957 68 0 0 25 0 1 0 542129944 124555264 24080 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30409 24080 603 41 0 30368 0 vsize: 121636 [startup+710.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25689 0 0 0 70958 68 0 0 25 0 1 0 542129944 124686336 24091 4294967295 134512640 134672761 3221224528 3221223632 134560235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30441 24091 603 41 0 30400 0 vsize: 121764 [startup+720.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25699 0 0 0 71958 68 0 0 25 0 1 0 542129944 124686336 24101 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30441 24101 603 41 0 30400 0 vsize: 121764 [startup+730.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25709 0 0 0 72958 68 0 0 25 0 1 0 542129944 124686336 24111 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30441 24111 603 41 0 30400 0 vsize: 121764 [startup+740.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25718 0 0 0 73958 68 0 0 25 0 1 0 542129944 124686336 24120 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30441 24120 603 41 0 30400 0 vsize: 121764 [startup+750.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25728 0 0 0 74958 68 0 0 25 0 1 0 542129944 124821504 24130 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30474 24130 603 41 0 30433 0 vsize: 121896 [startup+760.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25737 0 0 0 75958 68 0 0 25 0 1 0 542129944 124821504 24139 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30474 24139 603 41 0 30433 0 vsize: 121896 [startup+770.171 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25747 0 0 0 76959 68 0 0 25 0 1 0 542129944 124821504 24149 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30474 24149 603 41 0 30433 0 vsize: 121896 [startup+780.171 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25758 0 0 0 77959 68 0 0 25 0 1 0 542129944 124952576 24160 4294967295 134512640 134672761 3221224528 3221223728 134557836 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30506 24160 603 41 0 30465 0 vsize: 122024 [startup+790.171 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25766 0 0 0 78959 68 0 0 25 0 1 0 542129944 124952576 24168 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30506 24168 603 41 0 30465 0 vsize: 122024 [startup+800.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25775 0 0 0 79959 68 0 0 25 0 1 0 542129944 124952576 24177 4294967295 134512640 134672761 3221224528 3221223728 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30506 24177 603 41 0 30465 0 vsize: 122024 [startup+810.171 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25785 0 0 0 80959 68 0 0 25 0 1 0 542129944 124952576 24187 4294967295 134512640 134672761 3221224528 3221223696 134560882 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30506 24187 603 41 0 30465 0 vsize: 122024 [startup+820.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25793 0 0 0 81959 68 0 0 25 0 1 0 542129944 125083648 24195 4294967295 134512640 134672761 3221224528 3221223712 134559330 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30538 24195 603 41 0 30497 0 vsize: 122152 [startup+830.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25803 0 0 0 82959 68 0 0 25 0 1 0 542129944 125083648 24205 4294967295 134512640 134672761 3221224528 3221223632 134560410 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30538 24205 603 41 0 30497 0 vsize: 122152 [startup+840.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25812 0 0 0 83960 68 0 0 25 0 1 0 542129944 125083648 24214 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30538 24214 603 41 0 30497 0 vsize: 122152 [startup+850.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25821 0 0 0 84960 68 0 0 25 0 1 0 542129944 125210624 24223 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30569 24223 603 41 0 30528 0 vsize: 122276 [startup+860.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25828 0 0 0 85960 68 0 0 25 0 1 0 542129944 125210624 24230 4294967295 134512640 134672761 3221224528 3221223712 134559028 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30569 24230 603 41 0 30528 0 vsize: 122276 [startup+870.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25836 0 0 0 86960 69 0 0 25 0 1 0 542129944 125210624 24238 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30569 24238 603 41 0 30528 0 vsize: 122276 [startup+880.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25845 0 0 0 87960 69 0 0 25 0 1 0 542129944 125210624 24247 4294967295 134512640 134672761 3221224528 3221223728 134557895 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30569 24247 603 41 0 30528 0 vsize: 122276 [startup+890.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25852 0 0 0 88960 69 0 0 25 0 1 0 542129944 125345792 24254 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30602 24254 603 41 0 30561 0 vsize: 122408 [startup+900.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25864 0 0 0 89959 69 0 0 25 0 1 0 542129944 125345792 24266 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30602 24266 603 41 0 30561 0 vsize: 122408 [startup+910.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25875 0 0 0 90960 69 0 0 25 0 1 0 542129944 125345792 24277 4294967295 134512640 134672761 3221224528 3221223632 134560289 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30602 24277 603 41 0 30561 0 vsize: 122408 [startup+920.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25883 0 0 0 91960 69 0 0 25 0 1 0 542129944 125480960 24285 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30635 24285 603 41 0 30594 0 vsize: 122540 [startup+930.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25891 0 0 0 92960 69 0 0 25 0 1 0 542129944 125480960 24293 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30635 24293 603 41 0 30594 0 vsize: 122540 [startup+940.172 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25901 0 0 0 93960 69 0 0 25 0 1 0 542129944 125480960 24303 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30635 24303 603 41 0 30594 0 vsize: 122540 [startup+950.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25909 0 0 0 94960 69 0 0 25 0 1 0 542129944 125480960 24311 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30635 24311 603 41 0 30594 0 vsize: 122540 [startup+960.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25917 0 0 0 95960 69 0 0 25 0 1 0 542129944 125612032 24319 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30667 24319 603 41 0 30626 0 vsize: 122668 [startup+970.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25927 0 0 0 96960 69 0 0 25 0 1 0 542129944 125612032 24329 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30667 24329 603 41 0 30626 0 vsize: 122668 [startup+980.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25935 0 0 0 97961 69 0 0 25 0 1 0 542129944 125612032 24337 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30667 24337 603 41 0 30626 0 vsize: 122668 [startup+990.173 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25950 0 0 0 98960 70 0 0 25 0 1 0 542129944 125755392 24352 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30702 24352 603 41 0 30661 0 vsize: 122808 [startup+1000.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25961 0 0 0 99960 70 0 0 25 0 1 0 542129944 125755392 24363 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30702 24363 603 41 0 30661 0 vsize: 122808 [startup+1010.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25971 0 0 0 100960 70 0 0 25 0 1 0 542129944 125755392 24373 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30702 24373 603 41 0 30661 0 vsize: 122808 [startup+1020.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25978 0 0 0 101961 70 0 0 25 0 1 0 542129944 125755392 24380 4294967295 134512640 134672761 3221224528 3221223728 134557828 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30702 24380 603 41 0 30661 0 vsize: 122808 [startup+1030.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 25990 0 0 0 102961 70 0 0 25 0 1 0 542129944 125886464 24392 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30734 24392 603 41 0 30693 0 vsize: 122936 [startup+1040.17 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26003 0 0 0 103961 70 0 0 25 0 1 0 542129944 125886464 24405 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30734 24405 603 41 0 30693 0 vsize: 122936 [startup+1050.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26013 0 0 0 104961 70 0 0 25 0 1 0 542129944 126021632 24415 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30767 24415 603 41 0 30726 0 vsize: 123068 [startup+1060.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26024 0 0 0 105961 70 0 0 25 0 1 0 542129944 126021632 24426 4294967295 134512640 134672761 3221224528 3221223728 134557800 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30767 24426 603 41 0 30726 0 vsize: 123068 [startup+1070.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26032 0 0 0 106961 70 0 0 25 0 1 0 542129944 126021632 24434 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30767 24434 603 41 0 30726 0 vsize: 123068 [startup+1080.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26040 0 0 0 107962 70 0 0 25 0 1 0 542129944 126021632 24442 4294967295 134512640 134672761 3221224528 3221223728 134557842 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30767 24442 603 41 0 30726 0 vsize: 123068 [startup+1090.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26049 0 0 0 108962 70 0 0 25 0 1 0 542129944 126152704 24451 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30799 24451 603 41 0 30758 0 vsize: 123196 [startup+1100.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26057 0 0 0 109962 70 0 0 25 0 1 0 542129944 126152704 24459 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30799 24459 603 41 0 30758 0 vsize: 123196 [startup+1110.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26065 0 0 0 110962 70 0 0 25 0 1 0 542129944 126152704 24467 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30799 24467 603 41 0 30758 0 vsize: 123196 [startup+1120.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26073 0 0 0 111962 70 0 0 25 0 1 0 542129944 126152704 24475 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30799 24475 603 41 0 30758 0 vsize: 123196 [startup+1130.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26082 0 0 0 112962 70 0 0 25 0 1 0 542129944 126287872 24484 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30832 24484 603 41 0 30791 0 vsize: 123328 [startup+1140.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26089 0 0 0 113962 71 0 0 25 0 1 0 542129944 126287872 24491 4294967295 134512640 134672761 3221224528 3221223696 134560785 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30832 24491 603 41 0 30791 0 vsize: 123328 [startup+1150.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26097 0 0 0 114963 71 0 0 25 0 1 0 542129944 126287872 24499 4294967295 134512640 134672761 3221224528 3221223696 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30832 24499 603 41 0 30791 0 vsize: 123328 [startup+1160.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26108 0 0 0 115963 71 0 0 25 0 1 0 542129944 126287872 24510 4294967295 134512640 134672761 3221224528 3221223632 134560393 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30832 24510 603 41 0 30791 0 vsize: 123328 [startup+1170.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26117 0 0 0 116963 71 0 0 25 0 1 0 542129944 126418944 24519 4294967295 134512640 134672761 3221224528 3221223712 134559038 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30864 24519 603 41 0 30823 0 vsize: 123456 [startup+1180.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26126 0 0 0 117963 71 0 0 25 0 1 0 542129944 126418944 24528 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30864 24528 603 41 0 30823 0 vsize: 123456 [startup+1190.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26138 0 0 0 118963 71 0 0 25 0 1 0 542129944 126418944 24540 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30864 24540 603 41 0 30823 0 vsize: 123456 [startup+1200.18 s] Raw data (loadavg): 0.99 0.97 0.92 2/54 24284 Raw data (stat): 24284 (minisat+) R 24283 28546 28545 0 -1 0 26159 0 0 0 119961 72 0 0 25 0 1 0 542129944 126685184 24561 4294967295 134512640 134672761 3221224528 3221223712 134559045 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30929 24561 603 41 0 30888 0 vsize: 123716 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.23 s] Raw data (loadavg): 0.99 0.97 0.92 1/54 24284 Raw data (stat): 24284 (minisat+) Z 24283 28546 28545 0 -1 12 26162 0 0 0 119961 77 0 0 25 0 1 0 542129944 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 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.23 CPU time (s): 1200.39 CPU user time (s): 1199.62 CPU system time (s): 0.770882 CPU usage (%): 100.013 Max. virtual memory (Kb): 123716 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####