Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-cracpb1.opb |
MD5SUM | 098fe473d82d5f7d4121673eb775be76 |
Bench Category | optimization, small integers (OPTSMALLINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 22199 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 572 |
Biggest coefficient in the objective function | 5000 |
Number of bits for the biggest coefficient in the objective function | 13 |
Sum of the numbers in the objective function | 547769 |
Number of bits of the sum of numbers in the objective function | 20 |
Biggest number in a constraint | 5000 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 547769 |
Number of bits of the biggest sum of numbers | 20 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 30.8603 |
Number of variables | 572 |
Total number of constraints | 716 |
Number of constraints which are clauses | 3 |
Number of constraints which are cardinality constraints (but not clauses) | 644 |
Number of constraints which are nor clauses,nor cardinality constraints | 69 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 518 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc30 THE 2005-04-21 18:49:36 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=16757 boxname=wulflinc30 idbench=1289 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 098fe473d82d5f7d4121673eb775be76 /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-cracpb1.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-cracpb1.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-13-7-cracpb1.opb IDLAUNCH: 16757 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.072 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.072 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: 838388 kB Buffers: 15676 kB Cached: 154024 kB SwapCached: 28 kB Active: 57264 kB Inactive: 115288 kB HighTotal: 131008 kB HighFree: 14364 kB LowTotal: 903652 kB LowFree: 824024 kB SwapTotal: 2097892 kB SwapFree: 2097796 kB Dirty: 24 kB Writeback: 0 kB Mapped: 6800 kB Slab: 18220 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 19:09:39 (client local time) WITH STATUS 0 IN 1200.22 SECONDS stats: 16757 7 1200.22 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 215 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ######################################################################################### c -- Clauses(.)/Splits(s): ... c ---[ 214]---> Adder-cost: 1416 maxlim: 2733 bits: 12/12 c ---[ 213]---> Sorter-cost: 634 Base: c ---[ 212]---> Sorter-cost: 238 Base: c ---[ 211]---> Sorter-cost: 238 Base: c ---[ 210]---> Sorter-cost: 206 Base: c ---[ 209]---> Sorter-cost: 356 Base: c ---[ 208]---> Sorter-cost: 356 Base: c ---[ 207]---> Sorter-cost: 264 Base: c ---[ 206]---> Sorter-cost: 126 Base: c ---[ 205]---> Sorter-cost: 356 Base: c ---[ 204]---> Sorter-cost: 106 Base: c ---[ 203]---> BDD-cost: 43 c ---[ 202]---> BDD-cost: 34 c ---[ 201]---> Sorter-cost: 170 Base: c ---[ 200]---> BDD-cost: 29 c ---[ 199]---> Sorter-cost: 180 Base: c ---[ 198]---> BDD-cost: 31 c ---[ 197]---> BDD-cost: 21 c ---[ 195]---> Sorter-cost: 561 Base: c ---[ 193]---> BDD-cost: 41 c ---[ 191]---> Sorter-cost: 255 Base: c ---[ 189]---> Sorter-cost: 207 Base: c ---[ 187]---> Sorter-cost: 491 Base: c ---[ 185]---> Sorter-cost: 239 Base: c ---[ 183]---> Sorter-cost: 281 Base: c ---[ 181]---> Sorter-cost: 181 Base: c ---[ 179]---> Sorter-cost: 291 Base: c ---[ 177]---> Sorter-cost: 127 Base: c ---[ 175]---> BDD-cost: 33 c ---[ 173]---> Sorter-cost: 207 Base: c ---[ 171]---> Sorter-cost: 117 Base: c ---[ 169]---> Sorter-cost: 77 Base: c ---[ 167]---> Sorter-cost: 171 Base: c ---[ 165]---> Sorter-cost: 127 Base: c ---[ 163]---> BDD-cost: 29 c ---[ 161]---> BDD-cost: 25 c ---[ 159]---> Adder-cost: 155 maxlim: 27 bits: 6/5 c ---[ 157]---> Sorter-cost: 631 Base: c ---[ 155]---> Sorter-cost: 689 Base: c ---[ 153]---> Sorter-cost: 609 Base: c ---[ 151]---> Sorter-cost: 971 Base: c ---[ 149]---> Sorter-cost: 991 Base: c ---[ 147]---> Sorter-cost: 755 Base: c ---[ 145]---> Sorter-cost: 371 Base: c ---[ 143]---> Sorter-cost: 927 Base: c ---[ 141]---> Sorter-cost: 355 Base: c ---[ 139]---> Sorter-cost: 313 Base: c ---[ 137]---> Sorter-cost: 279 Base: c ---[ 135]---> Sorter-cost: 501 Base: c ---[ 133]---> Sorter-cost: 225 Base: c ---[ 131]---> Sorter-cost: 517 Base: c ---[ 129]---> Sorter-cost: 197 Base: c ---[ 127]---> BDD-cost: 66 c ---[ 126]---> Adder-cost: 732 maxlim: 1601 bits: 12/11 c ---[ 125]---> Adder-cost: 1184 maxlim: 406 bits: 10/9 c ---[ 124]---> Adder-cost: 255 maxlim: 863 bits: 11/10 c ---[ 123]---> BDD-cost: 27 c ---[ 122]---> BDD-cost: 35 c ---[ 121]---> Sorter-cost: 172 Base: c ---[ 120]---> BDD-cost: 31 c ---[ 118]---> BDD-cost: 51 c ---[ 115]---> BDD-cost: 80 c ---[ 114]---> Sorter-cost: 238 Base: c ---[ 113]---> Sorter-cost: 478 Base: c ---[ 112]---> Sorter-cost: 254 Base: c ---[ 111]---> BDD-cost: 21 c ---[ 110]---> Sorter-cost: 474 Base: c ---[ 109]---> BDD-cost: 29 c ---[ 108]---> BDD-cost: 23 c ---[ 106]---> BDD-cost: 16 c ---[ 104]---> BDD-cost: 17 c ---[ 102]---> BDD-cost: 5 c ---[ 100]---> BDD-cost: 43 c ---[ 98]---> BDD-cost: 92 c ---[ 96]---> BDD-cost: 183 c ---[ 94]---> BDD-cost: 11 c ---[ 92]---> BDD-cost: 29 c ---[ 90]---> BDD-cost: 29 c ---[ 88]---> BDD-cost: 19 c ---[ 86]---> BDD-cost: 11 c ---[ 84]---> BDD-cost: 11 c ---[ 82]---> BDD-cost: 31 c ---[ 80]---> BDD-cost: 23 c ---[ 78]---> BDD-cost: 7 c ---[ 76]---> BDD-cost: 13 c ---[ 74]---> BDD-cost: 14 c ---[ 72]---> BDD-cost: 38 c ---[ 70]---> BDD-cost: 23 c ---[ 68]---> BDD-cost: 35 c ---[ 66]---> BDD-cost: 37 c ---[ 64]---> BDD-cost: 7 c ---[ 62]---> BDD-cost: 17 c ---[ 60]---> BDD-cost: 17 c ---[ 58]---> BDD-cost: 43 c ---[ 56]---> BDD-cost: 11 c ---[ 54]---> BDD-cost: 29 c ---[ 52]---> BDD-cost: 7 c ---[ 50]---> BDD-cost: 16 c ---[ 48]---> BDD-cost: 24 c ---[ 46]---> BDD-cost: 5 c ---[ 44]---> BDD-cost: 14 c ---[ 42]---> BDD-cost: 11 c ---[ 40]---> BDD-cost: 13 c ---[ 38]---> BDD-cost: 16 c ---[ 36]---> BDD-cost: 19 c ---[ 34]---> BDD-cost: 14 c ---[ 32]---> BDD-cost: 19 c ---[ 30]---> BDD-cost: 11 c ---[ 28]---> BDD-cost: 4 c ---[ 26]---> BDD-cost: 11 c ---[ 24]---> BDD-cost: 14 c ---[ 22]---> BDD-cost: 15 c ---[ 20]---> BDD-cost: 48 c ---[ 18]---> BDD-cost: 51 c ---[ 16]---> BDD-cost: 11 c ---[ 14]---> BDD-cost: 6 c ---[ 12]---> BDD-cost: 51 c ---[ 10]---> BDD-cost: 8 c ---[ 8]---> BDD-cost: 14 c ---[ 6]---> BDD-cost: 43 c ---[ 4]---> BDD-cost: 31 c ---[ 2]---> BDD-cost: 22 c ---[ 0]---> BDD-cost: 17 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 67939 195555 | 22646 0 0 nan | 0.000 % | c | 100 | 67862 195385 | 24910 96 1024 10.7 | 2.636 % | c | 250 | 67626 194856 | 27401 168 1418 8.4 | 3.012 % | c | 475 | 67213 193932 | 30141 362 3093 8.5 | 3.698 % | c | 812 | 67166 193828 | 33156 695 14012 20.2 | 3.772 % | c | 1318 | 66656 192653 | 36471 1147 23771 20.7 | 4.563 % | c | 2077 | 66084 191337 | 40118 1847 30811 16.7 | 5.422 % | c | 3216 | 65666 190398 | 44130 2926 85116 29.1 | 6.126 % | c | 4924 | 65289 189510 | 48543 4602 161836 35.2 | 6.697 % | c | 7486 | 64879 188564 | 53398 7110 452576 63.7 | 7.372 % | c | 11330 | 64473 187562 | 58737 10913 683305 62.6 | 7.983 % | c | 17096 | 63798 186003 | 64611 16614 1038263 62.5 | 9.074 % | c | 25745 | 63601 185525 | 71072 25238 1695999 67.2 | 9.379 % | c | 38720 | 63580 185480 | 78180 38210 2907699 76.1 | 9.414 % | c | 58183 | 63250 184652 | 85998 57643 5496284 95.4 | 9.904 % | c | 87378 | 63094 184239 | 94597 86809 9124448 105.1 | 10.123 % | c | 131168 | 62940 183865 | 104057 49841 5416549 108.7 | 10.354 % | c | 196852 | 62652 183106 | 114463 24518 1690817 69.0 | 10.741 % | c | 295380 | 62156 181879 | 125909 22629 1840136 81.3 | 11.502 % | #### 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.91 0.95 0.95 2/54 23382 Raw data (stat): 23382 (runsolver) R 23381 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547365419 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.93 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 2385 0 0 0 992 6 0 0 25 0 1 0 547365419 12300288 2305 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 3003 2305 603 41 0 2962 0 vsize: 12012 [startup+20.0003 s] Raw data (loadavg): 0.94 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 2947 0 0 0 1990 8 0 0 25 0 1 0 547365419 14626816 2867 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3571 2867 603 41 0 3530 0 vsize: 14284 [startup+30.001 s] Raw data (loadavg): 0.95 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 3361 0 0 0 2989 10 0 0 25 0 1 0 547365419 16379904 3281 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3999 3281 603 41 0 3958 0 vsize: 15996 [startup+40.0006 s] Raw data (loadavg): 0.95 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 3778 0 0 0 3987 11 0 0 25 0 1 0 547365419 17993728 3698 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4393 3698 603 41 0 4352 0 vsize: 17572 [startup+50.0023 s] Raw data (loadavg): 0.96 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 4197 0 0 0 4986 12 0 0 25 0 1 0 547365419 19734528 4117 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4818 4117 603 41 0 4777 0 vsize: 19272 [startup+60.0028 s] Raw data (loadavg): 0.97 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 4781 0 0 0 5985 14 0 0 25 0 1 0 547365419 22024192 4701 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5377 4701 603 41 0 5336 0 vsize: 21508 [startup+70.0029 s] Raw data (loadavg): 0.97 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 5339 0 0 0 6984 15 0 0 25 0 1 0 547365419 24432640 5259 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5965 5259 603 41 0 5924 0 vsize: 23860 [startup+80.004 s] Raw data (loadavg): 0.98 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 5645 0 0 0 7983 16 0 0 25 0 1 0 547365419 25767936 5565 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6291 5565 603 41 0 6250 0 vsize: 25164 [startup+90.0038 s] Raw data (loadavg): 0.98 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 6141 0 0 0 8982 17 0 0 25 0 1 0 547365419 27787264 6061 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6784 6061 603 41 0 6743 0 vsize: 27136 [startup+100.004 s] Raw data (loadavg): 0.98 0.96 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 6902 0 0 0 9981 19 0 0 25 0 1 0 547365419 30887936 6822 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7541 6822 603 41 0 7500 0 vsize: 30164 [startup+110.005 s] Raw data (loadavg): 0.98 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 7476 0 0 0 10980 20 0 0 25 0 1 0 547365419 33169408 7396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8098 7396 603 41 0 8057 0 vsize: 32392 [startup+120.004 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 8124 0 0 0 11977 22 0 0 25 0 1 0 547365419 35864576 8044 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8756 8044 603 41 0 8715 0 vsize: 35024 [startup+130.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 8570 0 0 0 12976 24 0 0 25 0 1 0 547365419 37613568 8490 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9183 8490 603 41 0 9142 0 vsize: 36732 [startup+140.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 8915 0 0 0 13975 25 0 0 25 0 1 0 547365419 38957056 8835 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9511 8835 603 41 0 9470 0 vsize: 38044 [startup+150.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 9282 0 0 0 14974 26 0 0 25 0 1 0 547365419 40837120 9202 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9970 9202 603 41 0 9929 0 vsize: 39880 [startup+160.005 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 9753 0 0 0 15973 27 0 0 25 0 1 0 547365419 42713088 9673 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10428 9673 603 41 0 10387 0 vsize: 41712 [startup+170.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 10261 0 0 0 16972 28 0 0 25 0 1 0 547365419 44724224 10181 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10919 10181 603 41 0 10878 0 vsize: 43676 [startup+180.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 10592 0 0 0 17971 30 0 0 25 0 1 0 547365419 46063616 10512 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11246 10512 603 41 0 11205 0 vsize: 44984 [startup+190.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 11049 0 0 0 18970 31 0 0 25 0 1 0 547365419 47947776 10969 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11706 10969 603 41 0 11665 0 vsize: 46824 [startup+200.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 11512 0 0 0 19969 32 0 0 25 0 1 0 547365419 49823744 11432 4294967295 134512640 134672761 3221224544 3221223648 134560160 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12164 11432 603 41 0 12123 0 vsize: 48656 [startup+210.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 11970 0 0 0 20968 34 0 0 25 0 1 0 547365419 51703808 11890 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12623 11890 603 41 0 12582 0 vsize: 50492 [startup+220.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 12309 0 0 0 21966 35 0 0 25 0 1 0 547365419 53047296 12229 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12951 12229 603 41 0 12910 0 vsize: 51804 [startup+230.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 12675 0 0 0 22965 36 0 0 25 0 1 0 547365419 54517760 12595 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13310 12595 603 41 0 13269 0 vsize: 53240 [startup+240.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13121 0 0 0 23963 38 0 0 25 0 1 0 547365419 56393728 13041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13768 13041 603 41 0 13727 0 vsize: 55072 [startup+250.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13578 0 0 0 24962 40 0 0 25 0 1 0 547365419 58277888 13498 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13498 603 41 0 14187 0 vsize: 56912 [startup+260.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 25962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223752 1075346913 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+270.006 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 26962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+280.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 27962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223696 134559753 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+290.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 28962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+300.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 29962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+310.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 30962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+320.007 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 31963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+330.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 32962 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560785 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+340.008 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 33963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+350.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 34963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+360.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 35963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+370.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 36963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+380.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 37963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223648 134560350 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 38963 40 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+400.009 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 39964 41 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+410.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 40964 41 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+420.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13597 0 0 0 41964 41 0 0 25 0 1 0 547365419 58277888 13517 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13517 603 41 0 14187 0 vsize: 56912 [startup+430.011 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 42964 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13519 603 41 0 14187 0 vsize: 56912 [startup+440.011 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 43964 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13519 603 41 0 14187 0 vsize: 56912 [startup+450.012 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 44965 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13519 603 41 0 14187 0 vsize: 56912 [startup+460.012 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 45965 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13519 603 41 0 14187 0 vsize: 56912 [startup+470.013 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13599 0 0 0 46965 41 0 0 25 0 1 0 547365419 58277888 13519 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14228 13519 603 41 0 14187 0 vsize: 56912 [startup+480.013 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 13666 0 0 0 47965 41 0 0 25 0 1 0 547365419 58548224 13586 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14294 13586 603 41 0 14253 0 vsize: 57176 [startup+490.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14058 0 0 0 48964 42 0 0 25 0 1 0 547365419 60157952 13978 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14687 13978 603 41 0 14646 0 vsize: 58748 [startup+500.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14365 0 0 0 49963 43 0 0 25 0 1 0 547365419 61370368 14285 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14983 14285 603 41 0 14942 0 vsize: 59932 [startup+510.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 50963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+520.013 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 51962 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+530.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 52962 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223680 134565127 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+540.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 53962 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+550.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 54963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+560.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 55963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+570.014 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 56963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560370 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+580.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 57963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+590.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 58963 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+600.016 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 59964 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+610.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 60964 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+620.015 s] Raw data (loadavg): 0.99 0.97 0.95 2/54 23382 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 61964 44 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+630.017 s] Raw data (loadavg): 1.23 1.02 0.96 3/57 23421 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 62963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+640.017 s] Raw data (loadavg): 1.20 1.02 0.96 2/54 23435 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 63963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+650.018 s] Raw data (loadavg): 1.17 1.02 0.96 2/54 23435 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 64963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+660.018 s] Raw data (loadavg): 1.14 1.02 0.96 2/54 23435 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 65963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+670.018 s] Raw data (loadavg): 1.12 1.02 0.96 2/54 23435 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 66963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+680.018 s] Raw data (loadavg): 1.10 1.02 0.96 2/54 23435 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 67963 45 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+690.018 s] Raw data (loadavg): 1.08 1.01 0.96 2/54 23435 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 68963 46 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+700.019 s] Raw data (loadavg): 1.07 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 69963 46 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+710.019 s] Raw data (loadavg): 1.06 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 70963 47 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+720.02 s] Raw data (loadavg): 1.05 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 71962 47 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+730.02 s] Raw data (loadavg): 1.04 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 72962 48 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+740.021 s] Raw data (loadavg): 1.04 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 73962 48 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+750.022 s] Raw data (loadavg): 1.03 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 74962 48 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+760.022 s] Raw data (loadavg): 1.02 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14587 0 0 0 75961 48 0 0 25 0 1 0 547365419 62312448 14507 4294967295 134512640 134672761 3221224544 3221223648 134560492 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14507 603 41 0 15172 0 vsize: 60852 [startup+770.023 s] Raw data (loadavg): 1.02 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14589 0 0 0 76961 49 0 0 25 0 1 0 547365419 62312448 14509 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14509 603 41 0 15172 0 vsize: 60852 [startup+780.023 s] Raw data (loadavg): 1.02 1.01 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14591 0 0 0 77961 49 0 0 25 0 1 0 547365419 62312448 14511 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15213 14511 603 41 0 15172 0 vsize: 60852 [startup+790.023 s] Raw data (loadavg): 1.01 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14679 0 0 0 78961 49 0 0 25 0 1 0 547365419 62713856 14599 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15311 14599 603 41 0 15270 0 vsize: 61244 [startup+800.024 s] Raw data (loadavg): 1.01 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 14945 0 0 0 79960 50 0 0 25 0 1 0 547365419 63782912 14865 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15572 14865 603 41 0 15531 0 vsize: 62288 [startup+810.025 s] Raw data (loadavg): 1.01 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 80959 52 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134559941 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+820.024 s] Raw data (loadavg): 1.01 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 81958 52 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+830.025 s] Raw data (loadavg): 1.01 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 82958 52 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559417 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+840.025 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 83958 53 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+850.026 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 84958 53 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+860.026 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 85958 53 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+870.027 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 86957 54 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223676 1075347104 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+880.027 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 87957 55 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560808 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+890.028 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 88957 55 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+900.028 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 89957 55 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+910.028 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 90956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560269 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+920.029 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 91956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+930.029 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 92956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+940.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 93956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559548 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+950.032 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 94956 56 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134560158 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+960.032 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23437 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 95956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134559862 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+970.032 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 96956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+980.032 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 97956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+990.032 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 98956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+1000.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 99956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+1010.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 100956 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+1020.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 101957 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+1030.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 102957 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223600 134565132 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+1040.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15068 0 0 0 103957 57 0 0 25 0 1 0 547365419 64344064 14988 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15709 14988 603 41 0 15668 0 vsize: 62836 [startup+1050.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15368 0 0 0 104956 58 0 0 25 0 1 0 547365419 65568768 15288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16008 15288 603 41 0 15967 0 vsize: 64032 [startup+1060.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 15739 0 0 0 105956 58 0 0 25 0 1 0 547365419 67072000 15659 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16375 15659 603 41 0 16334 0 vsize: 65500 [startup+1070.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 16092 0 0 0 106955 59 0 0 25 0 1 0 547365419 68554752 16012 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16737 16012 603 41 0 16696 0 vsize: 66948 [startup+1080.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 16441 0 0 0 107955 60 0 0 25 0 1 0 547365419 69906432 16361 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17067 16361 603 41 0 17026 0 vsize: 68268 [startup+1090.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 16786 0 0 0 108953 62 0 0 25 0 1 0 547365419 71438336 16706 4294967295 134512640 134672761 3221224544 3221223712 134561406 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17441 16706 603 41 0 17400 0 vsize: 69764 [startup+1100.03 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 17147 0 0 0 109952 63 0 0 25 0 1 0 547365419 72925184 17067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17804 17067 603 41 0 17763 0 vsize: 71216 [startup+1110.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 17518 0 0 0 110951 64 0 0 25 0 1 0 547365419 74407936 17438 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18166 17438 603 41 0 18125 0 vsize: 72664 [startup+1120.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 17917 0 0 0 111950 65 0 0 25 0 1 0 547365419 76017664 17837 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18559 17837 603 41 0 18518 0 vsize: 74236 [startup+1130.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 18275 0 0 0 112950 66 0 0 25 0 1 0 547365419 77492224 18195 4294967295 134512640 134672761 3221224544 3221223648 134560070 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18919 18195 603 41 0 18878 0 vsize: 75676 [startup+1140.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 18607 0 0 0 113949 67 0 0 25 0 1 0 547365419 78831616 18527 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19246 18527 603 41 0 19205 0 vsize: 76984 [startup+1150.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 18925 0 0 0 114949 68 0 0 25 0 1 0 547365419 80166912 18845 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19572 18845 603 41 0 19531 0 vsize: 78288 [startup+1160.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 19276 0 0 0 115947 69 0 0 25 0 1 0 547365419 81649664 19196 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19934 19196 603 41 0 19893 0 vsize: 79736 [startup+1170.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 19631 0 0 0 116946 71 0 0 25 0 1 0 547365419 83173376 19551 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20306 19551 603 41 0 20265 0 vsize: 81224 [startup+1180.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 19999 0 0 0 117945 71 0 0 25 0 1 0 547365419 84652032 19919 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20667 19919 603 41 0 20626 0 vsize: 82668 [startup+1190.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 20342 0 0 0 118945 72 0 0 25 0 1 0 547365419 85991424 20262 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20994 20262 603 41 0 20953 0 vsize: 83976 [startup+1200.04 s] Raw data (loadavg): 1.00 1.00 0.96 2/54 23439 Raw data (stat): 23382 (minisat+) R 23381 11931 11930 0 -1 0 20601 0 0 0 119944 73 0 0 25 0 1 0 547365419 87064576 20521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21256 20521 603 41 0 21215 0 vsize: 85024 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.08 s] Raw data (loadavg): 1.00 1.00 0.96 1/54 23439 Raw data (stat): 23382 (minisat+) Z 23381 11931 11930 0 -1 12 20603 0 0 0 119944 76 0 0 25 0 1 0 547365419 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: 0 Real time (s): 1200.08 CPU time (s): 1200.22 CPU user time (s): 1199.45 CPU system time (s): 0.768883 CPU usage (%): 100.012 Max. virtual memory (Kb): 85024 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####