Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-nw04.opb |
MD5SUM | 5a18ff1f45b144b201f1f80233dc9b6b |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 30407 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 87482 |
Biggest coefficient in the objective function | 5220 |
Number of bits for the biggest coefficient in the objective function | 13 |
Sum of the numbers in the objective function | 120189580 |
Number of bits of the sum of numbers in the objective function | 27 |
Biggest number in a constraint | 5220 |
Number of bits of the biggest number in a constraint | 13 |
Biggest sum of numbers in a constraint | 120189580 |
Number of bits of the biggest sum of numbers | 27 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1197.16 |
Number of variables | 87482 |
Total number of constraints | 87518 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 87518 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 42032 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc30 THE 2005-04-22 01:02:22 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=12869 boxname=wulflinc30 idbench=990 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 5a18ff1f45b144b201f1f80233dc9b6b /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-nw04.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-nw04.opb /oldhome/oroussel/tmp/wulflinc30/normalized-mps-v2-20-10-nw04.opb IDLAUNCH: 12869 /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: 748384 kB Buffers: 11672 kB Cached: 248416 kB SwapCached: 352 kB Active: 39368 kB Inactive: 223408 kB HighTotal: 131008 kB HighFree: 18816 kB LowTotal: 903652 kB LowFree: 729568 kB SwapTotal: 2097892 kB SwapFree: 2097328 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5980 kB Slab: 17788 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-22 01:20:54 (client local time) WITH STATUS 0 IN 1112.27 SECONDS stats: 12869 7 1112.27 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### #### 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.87 0.96 0.91 2/54 1087 Raw data (stat): 1087 (runsolver) R 1086 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 549602281 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.89 0.96 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 22973 0 0 0 935 64 0 0 25 0 1 0 549602281 64581632 7176 4294967295 134512640 134672761 3221224544 3220374768 134594217 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15767 7176 603 41 0 15726 0 vsize: 63068 [startup+19.9994 s] Raw data (loadavg): 0.91 0.96 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 22973 0 0 0 1934 64 0 0 25 0 1 0 549602281 64581632 7176 4294967295 134512640 134672761 3221224544 3220759920 134594214 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15767 7176 603 41 0 15726 0 vsize: 63068 [startup+29.9994 s] Raw data (loadavg): 0.92 0.96 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 23318 0 0 0 2932 65 0 0 25 0 1 0 549602281 65994752 7521 4294967295 134512640 134672761 3221224544 3220667280 134594217 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16112 7521 603 41 0 16071 0 vsize: 64448 [startup+40.0083 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 23706 0 0 0 3932 66 0 0 25 0 1 0 549602281 69140480 7909 4294967295 134512640 134672761 3221224544 3220517248 134594124 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16880 7909 603 41 0 16839 0 vsize: 67520 [startup+50.0088 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 23947 0 0 0 4931 67 0 0 25 0 1 0 549602281 69771264 8150 4294967295 134512640 134672761 3221224544 3220456480 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17034 8150 603 41 0 16993 0 vsize: 68136 [startup+60.0086 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 24667 0 0 0 5930 69 0 0 25 0 1 0 549602281 71118848 8540 4294967295 134512640 134672761 3221224544 3220355760 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17363 8540 603 41 0 17322 0 vsize: 69452 [startup+70.0088 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 24761 0 0 0 6930 69 0 0 25 0 1 0 549602281 71118848 8634 4294967295 134512640 134672761 3221224544 3220639360 134594101 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17363 8634 603 41 0 17322 0 vsize: 69452 [startup+80.0092 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 24841 0 0 0 7930 69 0 0 25 0 1 0 549602281 71118848 8714 4294967295 134512640 134672761 3221224544 3220276000 134594101 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17363 8714 603 41 0 17322 0 vsize: 69452 [startup+90.009 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 25087 0 0 0 8930 70 0 0 25 0 1 0 549602281 74571776 8877 4294967295 134512640 134672761 3221224544 3220957216 134594131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18206 8877 603 41 0 18165 0 vsize: 72824 [startup+100.009 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 25448 0 0 0 9929 70 0 0 25 0 1 0 549602281 75153408 9113 4294967295 134512640 134672761 3221224544 3220616208 134594220 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18348 9113 603 41 0 18307 0 vsize: 73392 [startup+110.01 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 25611 0 0 0 10929 70 0 0 25 0 1 0 549602281 75456512 9234 4294967295 134512640 134672761 3221224544 3220140144 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18422 9234 603 41 0 18381 0 vsize: 73688 [startup+120.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27436 0 0 0 11925 74 0 0 25 0 1 0 549602281 79650816 10317 4294967295 134512640 134672761 3221224544 3220228656 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19446 10317 603 41 0 19405 0 vsize: 77784 [startup+130.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27580 0 0 0 12925 75 0 0 25 0 1 0 549602281 79953920 10419 4294967295 134512640 134672761 3221224544 3220971600 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19520 10419 603 41 0 19479 0 vsize: 78080 [startup+140.009 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27601 0 0 0 13925 75 0 0 25 0 1 0 549602281 79953920 10440 4294967295 134512640 134672761 3221224544 3220281856 134594092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19520 10440 603 41 0 19479 0 vsize: 78080 [startup+150.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27601 0 0 0 14926 75 0 0 25 0 1 0 549602281 79953920 10440 4294967295 134512640 134672761 3221224544 3219288544 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19520 10440 603 41 0 19479 0 vsize: 78080 [startup+160.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 27987 0 0 0 15925 75 0 0 25 0 1 0 549602281 80965632 10743 4294967295 134512640 134672761 3221224544 3220599888 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19767 10743 603 41 0 19726 0 vsize: 79068 [startup+170.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28230 0 0 0 16924 76 0 0 25 0 1 0 549602281 81002496 10821 4294967295 134512640 134672761 3221224544 3220302576 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19776 10821 603 41 0 19735 0 vsize: 79104 [startup+180.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28384 0 0 0 17924 77 0 0 25 0 1 0 549602281 81305600 10933 4294967295 134512640 134672761 3221224544 3221161200 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19850 10933 603 41 0 19809 0 vsize: 79400 [startup+190.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28389 0 0 0 18924 77 0 0 25 0 1 0 549602281 81305600 10938 4294967295 134512640 134672761 3221224544 3220110880 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19850 10938 603 41 0 19809 0 vsize: 79400 [startup+200.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1087 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28708 0 0 0 19924 77 0 0 25 0 1 0 549602281 82046976 11174 4294967295 134512640 134672761 3221224544 3220678896 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20031 11174 603 41 0 19990 0 vsize: 80124 [startup+210.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 28935 0 0 0 20923 78 0 0 25 0 1 0 549602281 82001920 11236 4294967295 134512640 134672761 3221224544 3220825680 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20020 11236 603 41 0 19979 0 vsize: 80080 [startup+220.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29050 0 0 0 21923 78 0 0 25 0 1 0 549602281 82305024 11309 4294967295 134512640 134672761 3221224544 3220611328 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20094 11309 603 41 0 20053 0 vsize: 80376 [startup+230.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29381 0 0 0 22923 79 0 0 25 0 1 0 549602281 83046400 11557 4294967295 134512640 134672761 3221224544 3221163408 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20275 11557 603 41 0 20234 0 vsize: 81100 [startup+240.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29593 0 0 0 23922 79 0 0 25 0 1 0 549602281 83025920 11604 4294967295 134512640 134672761 3221224544 3220692240 134594261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20270 11604 603 41 0 20229 0 vsize: 81080 [startup+250.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29721 0 0 0 24922 80 0 0 25 0 1 0 549602281 83329024 11690 4294967295 134512640 134672761 3221224544 3220629952 134594124 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20344 11690 603 41 0 20303 0 vsize: 81376 [startup+260.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 29721 0 0 0 25922 80 0 0 25 0 1 0 549602281 83329024 11690 4294967295 134512640 134672761 3221224544 3219735712 134594084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20344 11690 603 41 0 20303 0 vsize: 81376 [startup+270.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30059 0 0 0 26921 81 0 0 25 0 1 0 549602281 90361856 11945 4294967295 134512640 134672761 3221224544 3220818672 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22061 11945 603 41 0 22020 0 vsize: 88244 [startup+280.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30279 0 0 0 27921 81 0 0 25 0 1 0 549602281 90275840 12000 4294967295 134512640 134672761 3221224544 3220386192 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22040 12000 603 41 0 21999 0 vsize: 88160 [startup+290.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30422 0 0 0 28921 82 0 0 25 0 1 0 549602281 90714112 12101 4294967295 134512640 134672761 3221224544 3221123088 134594217 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22147 12101 603 41 0 22106 0 vsize: 88588 [startup+300.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30431 0 0 0 29921 82 0 0 25 0 1 0 549602281 90714112 12110 4294967295 134512640 134672761 3221224544 3220144864 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22147 12110 603 41 0 22106 0 vsize: 88588 [startup+310.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30523 0 0 0 30921 82 0 0 25 0 1 0 549602281 90849280 12202 4294967295 134512640 134672761 3221224544 3219768816 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22180 12202 603 41 0 22139 0 vsize: 88720 [startup+320.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 30906 0 0 0 31921 82 0 0 25 0 1 0 549602281 91197440 12337 4294967295 134512640 134672761 3221224544 3219553872 134594252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22265 12337 603 41 0 22224 0 vsize: 89060 [startup+330.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31111 0 0 0 32920 83 0 0 25 0 1 0 549602281 91672576 12500 4294967295 134512640 134672761 3221224544 3220776048 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22381 12500 603 41 0 22340 0 vsize: 89524 [startup+340.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31148 0 0 0 33920 83 0 0 25 0 1 0 549602281 91807744 12537 4294967295 134512640 134672761 3221224544 3220518400 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22414 12537 603 41 0 22373 0 vsize: 89656 [startup+350.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31148 0 0 0 34920 83 0 0 25 0 1 0 549602281 91807744 12537 4294967295 134512640 134672761 3221224544 3219660256 134594089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22414 12537 603 41 0 22373 0 vsize: 89656 [startup+360.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31481 0 0 0 35920 84 0 0 25 0 1 0 549602281 92549120 12787 4294967295 134512640 134672761 3221224544 3220671408 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22595 12787 603 41 0 22554 0 vsize: 90380 [startup+370.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31702 0 0 0 36920 84 0 0 25 0 1 0 549602281 92479488 12843 4294967295 134512640 134672761 3221224544 3220136688 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22578 12843 603 41 0 22537 0 vsize: 90312 [startup+380.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31852 0 0 0 37919 85 0 0 25 0 1 0 549602281 92782592 12951 4294967295 134512640 134672761 3221224544 3220943184 134594229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22652 12951 603 41 0 22611 0 vsize: 90608 [startup+390.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31874 0 0 0 38919 85 0 0 25 0 1 0 549602281 92917760 12973 4294967295 134512640 134672761 3221224544 3220323232 134594124 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22685 12973 603 41 0 22644 0 vsize: 90740 [startup+400.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 31874 0 0 0 39920 85 0 0 25 0 1 0 549602281 92917760 12973 4294967295 134512640 134672761 3221224544 3219250240 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 22685 12973 603 41 0 22644 0 vsize: 90740 [startup+410.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 34848 0 0 0 40914 91 0 0 25 0 1 0 549602281 99061760 14546 4294967295 134512640 134672761 3221224544 3220621584 134594217 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24185 14546 603 41 0 24144 0 vsize: 96740 [startup+420.009 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35105 0 0 0 41913 92 0 0 25 0 1 0 549602281 99180544 14638 4294967295 134512640 134672761 3221224544 3219935280 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24214 14638 603 41 0 24173 0 vsize: 96856 [startup+430.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35258 0 0 0 42913 92 0 0 25 0 1 0 549602281 99483648 14749 4294967295 134512640 134672761 3221224544 3220787760 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24288 14749 603 41 0 24247 0 vsize: 97152 [startup+440.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35294 0 0 0 43913 92 0 0 25 0 1 0 549602281 99618816 14785 4294967295 134512640 134672761 3221224544 3220398976 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24321 14785 603 41 0 24280 0 vsize: 97284 [startup+450.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35294 0 0 0 44913 92 0 0 25 0 1 0 549602281 99618816 14785 4294967295 134512640 134672761 3221224544 3219785056 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24321 14785 603 41 0 24280 0 vsize: 97284 [startup+460.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35356 0 0 0 45913 92 0 0 25 0 1 0 549602281 99753984 14847 4294967295 134512640 134672761 3221224544 3219172944 134594229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24354 14847 603 41 0 24313 0 vsize: 97416 [startup+470.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 35680 0 0 0 46913 93 0 0 25 0 1 0 549602281 100495360 15088 4294967295 134512640 134672761 3221224544 3221118768 134594217 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24535 15088 603 41 0 24494 0 vsize: 98140 [startup+480.01 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36042 0 0 0 47913 93 0 0 25 0 1 0 549602281 101081088 15285 4294967295 134512640 134672761 3221224544 3219748560 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24678 15285 603 41 0 24637 0 vsize: 98712 [startup+490.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36179 0 0 0 48913 93 0 0 25 0 1 0 549602281 101384192 15380 4294967295 134512640 134672761 3221224544 3220407216 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24752 15380 603 41 0 24711 0 vsize: 99008 [startup+500.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36217 0 0 0 49913 94 0 0 25 0 1 0 549602281 101519360 15418 4294967295 134512640 134672761 3221224544 3220870512 134594212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24785 15418 603 41 0 24744 0 vsize: 99140 [startup+510.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36246 0 0 0 50913 94 0 0 25 0 1 0 549602281 101519360 15447 4294967295 134512640 134672761 3221224544 3220685728 134594101 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24785 15447 603 41 0 24744 0 vsize: 99140 [startup+520.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36246 0 0 0 51913 94 0 0 25 0 1 0 549602281 101519360 15447 4294967295 134512640 134672761 3221224544 3219577600 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24785 15447 603 41 0 24744 0 vsize: 99140 [startup+530.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36246 0 0 0 52913 94 0 0 25 0 1 0 549602281 101519360 15447 4294967295 134512640 134672761 3221224544 3219129088 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24785 15447 603 41 0 24744 0 vsize: 99140 [startup+540.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36246 0 0 0 53913 94 0 0 25 0 1 0 549602281 101519360 15447 4294967295 134512640 134672761 3221224544 3218250976 134594084 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24785 15447 603 41 0 24744 0 vsize: 99140 [startup+550.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36575 0 0 0 54913 95 0 0 25 0 1 0 549602281 102260736 15693 4294967295 134512640 134672761 3221224544 3219805968 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 24966 15693 603 41 0 24925 0 vsize: 99864 [startup+560.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36701 0 0 0 55913 95 0 0 25 0 1 0 549602281 102666240 15819 4294967295 134512640 134672761 3221224544 3220909776 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25065 15819 603 41 0 25024 0 vsize: 100260 [startup+570.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 36948 0 0 0 56913 95 0 0 25 0 1 0 549602281 102727680 15901 4294967295 134512640 134672761 3221224544 3219275952 134594252 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25080 15901 603 41 0 25039 0 vsize: 100320 [startup+580.012 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37096 0 0 0 57912 95 0 0 25 0 1 0 549602281 103165952 16007 4294967295 134512640 134672761 3221224544 3220080144 134594234 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25187 16007 603 41 0 25146 0 vsize: 100748 [startup+590.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37139 0 0 0 58912 95 0 0 25 0 1 0 549602281 103165952 16050 4294967295 134512640 134672761 3221224544 3220592208 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25187 16050 603 41 0 25146 0 vsize: 100748 [startup+600.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37171 0 0 0 59912 95 0 0 25 0 1 0 549602281 103301120 16082 4294967295 134512640 134672761 3221224544 3220987440 134594212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25220 16082 603 41 0 25179 0 vsize: 100880 [startup+610.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37190 0 0 0 60912 96 0 0 25 0 1 0 549602281 103301120 16101 4294967295 134512640 134672761 3221224544 3219963520 134594101 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25220 16101 603 41 0 25179 0 vsize: 100880 [startup+620.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37190 0 0 0 61912 96 0 0 25 0 1 0 549602281 103301120 16101 4294967295 134512640 134672761 3221224544 3219411232 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25220 16101 603 41 0 25179 0 vsize: 100880 [startup+630.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37190 0 0 0 62912 96 0 0 25 0 1 0 549602281 103301120 16101 4294967295 134512640 134672761 3221224544 3218997664 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25220 16101 603 41 0 25179 0 vsize: 100880 [startup+640.011 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37190 0 0 0 63912 96 0 0 25 0 1 0 549602281 103301120 16101 4294967295 134512640 134672761 3221224544 3218196640 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25220 16101 603 41 0 25179 0 vsize: 100880 [startup+650.012 s] Raw data (loadavg): 1.07 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37489 0 0 0 64912 97 0 0 25 0 1 0 549602281 104042496 16317 4294967295 134512640 134672761 3221224544 3219298608 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25401 16317 603 41 0 25360 0 vsize: 101604 [startup+660.011 s] Raw data (loadavg): 1.06 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37597 0 0 0 65911 97 0 0 25 0 1 0 549602281 104312832 16425 4294967295 134512640 134672761 3221224544 3220609776 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25467 16425 603 41 0 25426 0 vsize: 101868 [startup+670.011 s] Raw data (loadavg): 1.05 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37748 0 0 0 66911 97 0 0 25 0 1 0 549602281 104103936 16411 4294967295 134512640 134672761 3221224544 3218650128 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25416 16411 603 41 0 25375 0 vsize: 101664 [startup+680.012 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 37958 0 0 0 67911 98 0 0 25 0 1 0 549602281 104579072 16579 4294967295 134512640 134672761 3221224544 3219939504 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25532 16579 603 41 0 25491 0 vsize: 102128 [startup+690.012 s] Raw data (loadavg): 1.04 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38008 0 0 0 68911 98 0 0 25 0 1 0 549602281 104714240 16629 4294967295 134512640 134672761 3221224544 3220531632 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25565 16629 603 41 0 25524 0 vsize: 102260 [startup+700.012 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38043 0 0 0 69911 98 0 0 25 0 1 0 549602281 104849408 16664 4294967295 134512640 134672761 3221224544 3220965168 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16664 603 41 0 25557 0 vsize: 102392 [startup+710.012 s] Raw data (loadavg): 1.03 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38064 0 0 0 70911 98 0 0 25 0 1 0 549602281 104849408 16685 4294967295 134512640 134672761 3221224544 3219962176 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16685 603 41 0 25557 0 vsize: 102392 [startup+720.012 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38064 0 0 0 71911 98 0 0 25 0 1 0 549602281 104849408 16685 4294967295 134512640 134672761 3221224544 3219479200 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16685 603 41 0 25557 0 vsize: 102392 [startup+730.012 s] Raw data (loadavg): 1.02 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38064 0 0 0 72912 98 0 0 25 0 1 0 549602281 104849408 16685 4294967295 134512640 134672761 3221224544 3219001792 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16685 603 41 0 25557 0 vsize: 102392 [startup+740.012 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38064 0 0 0 73912 98 0 0 25 0 1 0 549602281 104849408 16685 4294967295 134512640 134672761 3221224544 3218078464 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25598 16685 603 41 0 25557 0 vsize: 102392 [startup+750.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38421 0 0 0 74911 99 0 0 25 0 1 0 549602281 105725952 16959 4294967295 134512640 134672761 3221224544 3220130928 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25812 16959 603 41 0 25771 0 vsize: 103248 [startup+760.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38497 0 0 0 75911 99 0 0 25 0 1 0 549602281 105861120 17035 4294967295 134512640 134672761 3221224544 3221070288 134594212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25845 17035 603 41 0 25804 0 vsize: 103380 [startup+770.012 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38704 0 0 0 76911 99 0 0 25 0 1 0 549602281 105762816 17077 4294967295 134512640 134672761 3221224544 3219643248 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25821 17077 603 41 0 25780 0 vsize: 103284 [startup+780.013 s] Raw data (loadavg): 1.01 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38844 0 0 0 77911 100 0 0 25 0 1 0 549602281 106201088 17175 4294967295 134512640 134672761 3221224544 3220341264 134594261 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25928 17175 603 41 0 25887 0 vsize: 103712 [startup+790.013 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38884 0 0 0 78911 100 0 0 25 0 1 0 549602281 106201088 17215 4294967295 134512640 134672761 3221224544 3220819536 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25928 17215 603 41 0 25887 0 vsize: 103712 [startup+800.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38915 0 0 0 79911 100 0 0 25 0 1 0 549602281 106336256 17246 4294967295 134512640 134672761 3221224544 3221196816 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25961 17246 603 41 0 25920 0 vsize: 103844 [startup+810.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38916 0 0 0 80911 100 0 0 25 0 1 0 549602281 106336256 17247 4294967295 134512640 134672761 3221224544 3219623872 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25961 17247 603 41 0 25920 0 vsize: 103844 [startup+820.014 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38916 0 0 0 81911 100 0 0 25 0 1 0 549602281 106336256 17247 4294967295 134512640 134672761 3221224544 3219192736 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25961 17247 603 41 0 25920 0 vsize: 103844 [startup+830.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 38916 0 0 0 82912 100 0 0 25 0 1 0 549602281 106336256 17247 4294967295 134512640 134672761 3221224544 3218356000 134594089 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25961 17247 603 41 0 25920 0 vsize: 103844 [startup+840.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39224 0 0 0 83911 101 0 0 25 0 1 0 549602281 107077632 17472 4294967295 134512640 134672761 3221224544 3219541488 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26142 17472 603 41 0 26101 0 vsize: 104568 [startup+850.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39326 0 0 0 84911 101 0 0 25 0 1 0 549602281 107347968 17574 4294967295 134512640 134672761 3221224544 3220784016 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 26208 17574 603 41 0 26167 0 vsize: 104832 [startup+860.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39521 0 0 0 85911 102 0 0 25 0 1 0 549602281 119758848 17604 4294967295 134512640 134672761 3221224544 3219205680 134594234 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29238 17604 603 41 0 29197 0 vsize: 116952 [startup+870.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39679 0 0 0 86910 102 0 0 25 0 1 0 549602281 120061952 17720 4294967295 134512640 134672761 3221224544 3220132464 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29312 17720 603 41 0 29271 0 vsize: 117248 [startup+880.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39724 0 0 0 87911 102 0 0 25 0 1 0 549602281 120197120 17765 4294967295 134512640 134672761 3221224544 3220669680 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29345 17765 603 41 0 29304 0 vsize: 117380 [startup+890.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39757 0 0 0 88911 102 0 0 25 0 1 0 549602281 120332288 17798 4294967295 134512640 134672761 3221224544 3221077488 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17798 603 41 0 29337 0 vsize: 117512 [startup+900.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39768 0 0 0 89911 102 0 0 25 0 1 0 549602281 120332288 17809 4294967295 134512640 134672761 3221224544 3219756064 134594101 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17809 603 41 0 29337 0 vsize: 117512 [startup+910.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39768 0 0 0 90911 102 0 0 25 0 1 0 549602281 120332288 17809 4294967295 134512640 134672761 3221224544 3219354688 134594106 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17809 603 41 0 29337 0 vsize: 117512 [startup+920.015 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39768 0 0 0 91911 102 0 0 25 0 1 0 549602281 120332288 17809 4294967295 134512640 134672761 3221224544 3218794528 134594092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29378 17809 603 41 0 29337 0 vsize: 117512 [startup+930.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 39986 0 0 0 92911 103 0 0 25 0 1 0 549602281 120803328 17944 4294967295 134512640 134672761 3221224544 3218462832 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29493 17944 603 41 0 29452 0 vsize: 117972 [startup+940.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40156 0 0 0 93911 103 0 0 25 0 1 0 549602281 121208832 18114 4294967295 134512640 134672761 3221224544 3220531536 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29592 18114 603 41 0 29551 0 vsize: 118368 [startup+950.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40422 0 0 0 94911 103 0 0 25 0 1 0 549602281 121425920 18215 4294967295 134512640 134672761 3221224544 3218018160 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29645 18215 603 41 0 29604 0 vsize: 118580 [startup+960.017 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40633 0 0 0 95910 104 0 0 25 0 1 0 549602281 122036224 18384 4294967295 134512640 134672761 3221224544 3219319920 134594212 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29794 18384 603 41 0 29753 0 vsize: 119176 [startup+970.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40683 0 0 0 96911 104 0 0 25 0 1 0 549602281 122171392 18434 4294967295 134512640 134672761 3221224544 3219913488 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29827 18434 603 41 0 29786 0 vsize: 119308 [startup+980.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40718 0 0 0 97910 104 0 0 25 0 1 0 549602281 122171392 18469 4294967295 134512640 134672761 3221224544 3220347504 134594259 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29827 18469 603 41 0 29786 0 vsize: 119308 [startup+990.016 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40748 0 0 0 98911 104 0 0 25 0 1 0 549602281 122306560 18499 4294967295 134512640 134672761 3221224544 3220699728 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29860 18499 603 41 0 29819 0 vsize: 119440 [startup+1000.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40772 0 0 0 99911 104 0 0 25 0 1 0 549602281 122306560 18523 4294967295 134512640 134672761 3221224544 3220997328 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29860 18523 603 41 0 29819 0 vsize: 119440 [startup+1010.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 100911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3220339168 134594101 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+1020.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 101911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3219153088 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+1030.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 102911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3218874208 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+1040.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 103911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3218554048 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+1050.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 104911 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3218134144 134594086 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+1060.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 40790 0 0 0 105912 104 0 0 25 0 1 0 549602281 122441728 18541 4294967295 134512640 134672761 3221224544 3217521088 134594131 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 29893 18541 603 41 0 29852 0 vsize: 119572 [startup+1070.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 41105 0 0 0 106911 105 0 0 25 0 1 0 549602281 123183104 18773 4294967295 134512640 134672761 3221224544 3219012816 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30074 18773 603 41 0 30033 0 vsize: 120296 [startup+1080.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 41204 0 0 0 107911 105 0 0 25 0 1 0 549602281 123453440 18872 4294967295 134512640 134672761 3221224544 3220217904 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30140 18872 603 41 0 30099 0 vsize: 120560 [startup+1090.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 41282 0 0 0 108911 105 0 0 25 0 1 0 549602281 123588608 18950 4294967295 134512640 134672761 3221224544 3220888176 134594214 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30173 18950 603 41 0 30132 0 vsize: 120692 [startup+1100.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 41623 0 0 0 109910 107 0 0 25 0 1 0 549602281 123748352 19084 4294967295 134512640 134672761 3221224544 3221192128 134594101 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30212 19084 603 41 0 30171 0 vsize: 120848 [startup+1110.02 s] Raw data (loadavg): 1.00 0.99 0.91 2/54 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 56067 0 0 0 110878 139 0 0 25 0 1 0 549602281 146100224 30838 4294967295 134512640 134672761 3221224544 3216366976 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35669 30840 603 41 0 35628 0 vsize: 142676 [startup+1112.11 s] Raw data (loadavg): 1.00 0.99 0.91 1/53 1089 Raw data (stat): 1087 (minisat+) R 1086 11931 11930 0 -1 0 56067 0 0 0 110878 139 0 0 25 0 1 0 549602281 146100224 30838 4294967295 134512640 134672761 3221224544 3216366976 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35669 30840 603 41 0 35628 0 vsize: 0 Child ended because it received signal 11 (SIGSEGV) Real time (s): 1112.11 CPU time (s): 1112.27 CPU user time (s): 1110.46 CPU system time (s): 1.80472 CPU usage (%): 100.014 Max. virtual memory (Kb): 142676 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####