Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-pp08a.opb |
MD5SUM | d14265fdf4e5a3ef733af1f15b884cbe |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | YES |
(Un)Satisfiability was proved | YES |
Best value of the objective function | 6661373 |
Optimality of the best value was proved | NO |
Number of terms in the objective function | 2304 |
Biggest coefficient in the objective function | 1048576 |
Number of bits for the biggest coefficient in the objective function | 21 |
Sum of the numbers in the objective function | 178464600 |
Number of bits of the sum of numbers in the objective function | 28 |
Biggest number in a constraint | 1048576 |
Number of bits of the biggest number in a constraint | 21 |
Biggest sum of numbers in a constraint | 178464600 |
Number of bits of the biggest sum of numbers | 28 |
Best result obtained on this benchmark | SAT |
Best CPU time to get the best result obtained on this benchmark | 1189.02 |
Number of variables | 3584 |
Total number of constraints | 136 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 136 |
Minimum length of a constraint | 21 |
Maximum length of a constraint | 160 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc28 THE 2005-04-21 02:19:57 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=18777 boxname=wulflinc28 idbench=1445 idsolver=5 numberseed=0 MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4 /oldhome/oroussel/solvers/minisat+ MD5SUM BENCH: d14265fdf4e5a3ef733af1f15b884cbe /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-pp08a.opb REAL COMMAND: minisat+ /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-pp08a.opb IDLAUNCH: 18777 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.077 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.077 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: 699948 kB Buffers: 4288 kB Cached: 302492 kB SwapCached: 104 kB Active: 50464 kB Inactive: 258660 kB HighTotal: 131008 kB HighFree: 40880 kB LowTotal: 903652 kB LowFree: 659068 kB SwapTotal: 2097640 kB SwapFree: 2097068 kB Dirty: 40 kB Writeback: 0 kB Mapped: 6052 kB Slab: 19808 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 02:39:59 (client local time) WITH STATUS 0 IN 1200.25 SECONDS stats: 18777 7 1200.25 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 200 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: ################################################################ c -- Clauses(.)/Splits(s): (none) c ---[ 199]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 198]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 197]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 196]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 195]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 194]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 193]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 192]---> Sorter-cost: 1961 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 190]---> BDD-cost: 158 c ---[ 188]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 186]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 184]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 182]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 180]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 178]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 176]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 174]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 172]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 170]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 168]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 166]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 164]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 162]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 160]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 158]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 156]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 154]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 152]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 150]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 148]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 146]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 144]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 142]---> BDD-cost: 158 c ---[ 140]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 138]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 136]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 134]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 132]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 130]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 128]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 126]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 124]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 122]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 120]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 118]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 116]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 114]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 112]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 110]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 108]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 106]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 104]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 102]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 100]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 98]---> Sorter-cost: 1179 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 96]---> Sorter-cost: 427 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 94]---> BDD-cost: 154 c ---[ 92]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 90]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 88]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 86]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 84]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 82]---> Sorter-cost: 1160 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 80]---> Sorter-cost: 418 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 78]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 76]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 74]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 72]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 70]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 68]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 66]---> Sorter-cost: 1141 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 64]---> Sorter-cost: 409 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[ 63]---> BDD-cost: 24 c ---[ 62]---> BDD-cost: 24 c ---[ 61]---> BDD-cost: 24 c ---[ 60]---> BDD-cost: 21 c ---[ 59]---> BDD-cost: 21 c ---[ 58]---> BDD-cost: 21 c ---[ 57]---> BDD-cost: 21 c ---[ 56]---> BDD-cost: 23 c ---[ 55]---> BDD-cost: 19 c ---[ 54]---> BDD-cost: 19 c ---[ 53]---> BDD-cost: 19 c ---[ 52]---> BDD-cost: 19 c ---[ 51]---> BDD-cost: 19 c ---[ 50]---> BDD-cost: 19 c ---[ 49]---> BDD-cost: 19 c ---[ 48]---> BDD-cost: 19 c ---[ 47]---> BDD-cost: 24 c ---[ 46]---> BDD-cost: 24 c ---[ 45]---> BDD-cost: 24 c ---[ 44]---> BDD-cost: 21 c ---[ 43]---> BDD-cost: 21 c ---[ 42]---> BDD-cost: 21 c ---[ 41]---> BDD-cost: 21 c ---[ 40]---> BDD-cost: 23 c ---[ 39]---> BDD-cost: 24 c ---[ 38]---> BDD-cost: 24 c ---[ 37]---> BDD-cost: 24 c ---[ 36]---> BDD-cost: 21 c ---[ 35]---> BDD-cost: 21 c ---[ 34]---> BDD-cost: 21 c ---[ 33]---> BDD-cost: 21 c ---[ 32]---> BDD-cost: 23 c ---[ 31]---> BDD-cost: 18 c ---[ 30]---> BDD-cost: 18 c ---[ 29]---> BDD-cost: 18 c ---[ 28]---> BDD-cost: 18 c ---[ 27]---> BDD-cost: 18 c ---[ 26]---> BDD-cost: 18 c ---[ 25]---> BDD-cost: 18 c ---[ 24]---> BDD-cost: 18 c ---[ 23]---> BDD-cost: 24 c ---[ 22]---> BDD-cost: 24 c ---[ 21]---> BDD-cost: 24 c ---[ 20]---> BDD-cost: 21 c ---[ 19]---> BDD-cost: 21 c ---[ 18]---> BDD-cost: 21 c ---[ 17]---> BDD-cost: 21 c ---[ 16]---> BDD-cost: 21 c ---[ 15]---> BDD-cost: 19 c ---[ 14]---> BDD-cost: 19 c ---[ 13]---> BDD-cost: 19 c ---[ 12]---> BDD-cost: 19 c ---[ 11]---> BDD-cost: 19 c ---[ 10]---> BDD-cost: 19 c ---[ 9]---> BDD-cost: 19 c ---[ 8]---> BDD-cost: 19 c ---[ 7]---> BDD-cost: 19 c ---[ 6]---> BDD-cost: 19 c ---[ 5]---> BDD-cost: 19 c ---[ 4]---> BDD-cost: 19 c ---[ 3]---> BDD-cost: 19 c ---[ 2]---> BDD-cost: 19 c ---[ 1]---> BDD-cost: 19 c ---[ 0]---> BDD-cost: 19 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 192439 454988 | 64146 0 0 nan | 0.000 % | c | 100 | 192239 454543 | 70560 73 246 3.4 | 5.672 % | c | 250 | 192206 454471 | 77616 216 748 3.5 | 5.687 % | c | 475 | 192016 454049 | 85378 412 1679 4.1 | 5.767 % | c | 812 | 191856 453691 | 93916 721 3004 4.2 | 5.829 % | c | 1319 | 191699 453343 | 103307 1205 7766 6.4 | 5.895 % | c | 2079 | 191487 452868 | 113638 1929 14801 7.7 | 5.980 % | c | 3219 | 191290 452428 | 125002 3045 26101 8.6 | 6.059 % | c | 4927 | 191115 452036 | 137502 4729 52510 11.1 | 6.130 % | c | 7490 | 190810 451355 | 151252 7247 81997 11.3 | 6.249 % | c | 11334 | 189963 449458 | 166378 10976 116451 10.6 | 6.584 % | c | 17100 | 189884 449279 | 183016 16736 248554 14.9 | 6.614 % | c | 25749 | 189706 448881 | 201317 25359 431867 17.0 | 6.685 % | c | 38724 | 189201 447754 | 221449 38259 749831 19.6 | 6.890 % | c | 58187 | 188976 447252 | 243594 57689 1288213 22.3 | 6.979 % | c | 87379 | 187270 443439 | 267953 86663 1918714 22.1 | 7.664 % | c | 131168 | 186149 440936 | 294749 130304 3171694 24.3 | 8.119 % | c | 196855 | 183362 434691 | 324224 195633 4851184 24.8 | 9.223 % | c | 295384 | 182771 433365 | 356646 294057 7348160 25.0 | 9.461 % | #### 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.90 0.94 0.90 2/54 14821 Raw data (stat): 14821 (runsolver) R 14820 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541434431 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0003 s] Raw data (loadavg): 0.91 0.94 0.90 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 6133 0 0 0 982 17 0 0 25 0 1 0 541434431 30937088 5968 4294967295 134512640 134672761 3221224624 3221223796 134556653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7553 5968 603 41 0 7512 0 vsize: 30212 [startup+20.0006 s] Raw data (loadavg): 0.93 0.94 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 6344 0 0 0 1981 18 0 0 25 0 1 0 541434431 31748096 6179 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7751 6179 603 41 0 7710 0 vsize: 31004 [startup+30.0013 s] Raw data (loadavg): 0.94 0.94 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 6779 0 0 0 2979 20 0 0 25 0 1 0 541434431 33525760 6614 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8185 6614 603 41 0 8144 0 vsize: 32740 [startup+40.0014 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 7114 0 0 0 3977 21 0 0 25 0 1 0 541434431 35000320 6949 4294967295 134512640 134672761 3221224624 3221223792 134560828 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8545 6949 603 41 0 8504 0 vsize: 34180 [startup+50.0017 s] Raw data (loadavg): 0.95 0.94 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 7448 0 0 0 4977 22 0 0 25 0 1 0 541434431 36343808 7283 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8873 7283 603 41 0 8832 0 vsize: 35492 [startup+60.0014 s] Raw data (loadavg): 0.96 0.94 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 7836 0 0 0 5975 24 0 0 25 0 1 0 541434431 37957632 7671 4294967295 134512640 134672761 3221224624 3221223772 134566158 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9267 7671 603 41 0 9226 0 vsize: 37068 [startup+70.0025 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8096 0 0 0 6974 25 0 0 25 0 1 0 541434431 38907904 7931 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9499 7931 603 41 0 9458 0 vsize: 37996 [startup+80.0032 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8272 0 0 0 7974 25 0 0 25 0 1 0 541434431 39976960 8107 4294967295 134512640 134672761 3221224624 3221223784 134561238 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9760 8107 603 41 0 9719 0 vsize: 39040 [startup+90.0024 s] Raw data (loadavg): 0.97 0.95 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8388 0 0 0 8973 26 0 0 25 0 1 0 541434431 40374272 8223 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9857 8223 603 41 0 9816 0 vsize: 39428 [startup+100.002 s] Raw data (loadavg): 0.98 0.95 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8482 0 0 0 9973 27 0 0 25 0 1 0 541434431 40775680 8317 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9955 8317 603 41 0 9914 0 vsize: 39820 [startup+110.003 s] Raw data (loadavg): 1.06 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8714 0 0 0 10972 28 0 0 25 0 1 0 541434431 41713664 8549 4294967295 134512640 134672761 3221224624 3221223748 134566068 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10184 8549 603 41 0 10143 0 vsize: 40736 [startup+120.004 s] Raw data (loadavg): 1.05 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 8960 0 0 0 11971 29 0 0 25 0 1 0 541434431 42651648 8795 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10413 8795 603 41 0 10372 0 vsize: 41652 [startup+130.005 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9194 0 0 0 12970 30 0 0 25 0 1 0 541434431 43610112 9029 4294967295 134512640 134672761 3221224624 3221223776 134565070 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10647 9029 603 41 0 10606 0 vsize: 42588 [startup+140.004 s] Raw data (loadavg): 1.04 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9322 0 0 0 13969 31 0 0 25 0 1 0 541434431 44158976 9157 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10781 9157 603 41 0 10740 0 vsize: 43124 [startup+150.005 s] Raw data (loadavg): 1.03 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9492 0 0 0 14969 32 0 0 25 0 1 0 541434431 44830720 9327 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10945 9327 603 41 0 10904 0 vsize: 43780 [startup+160.005 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9591 0 0 0 15968 32 0 0 25 0 1 0 541434431 45236224 9426 4294967295 134512640 134672761 3221224624 3221223776 134565127 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11044 9426 603 41 0 11003 0 vsize: 44176 [startup+170.005 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 9839 0 0 0 16967 34 0 0 25 0 1 0 541434431 46170112 9674 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11272 9674 603 41 0 11231 0 vsize: 45088 [startup+180.006 s] Raw data (loadavg): 1.02 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10157 0 0 0 17966 35 0 0 25 0 1 0 541434431 47513600 9992 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11600 9992 603 41 0 11559 0 vsize: 46400 [startup+190.006 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10389 0 0 0 18965 36 0 0 25 0 1 0 541434431 48345088 10224 4294967295 134512640 134672761 3221224624 3221223792 134560874 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11803 10224 603 41 0 11762 0 vsize: 47212 [startup+200.006 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10581 0 0 0 19964 37 0 0 25 0 1 0 541434431 49696768 10416 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12133 10416 603 41 0 12092 0 vsize: 48532 [startup+210.005 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10618 0 0 0 20965 37 0 0 25 0 1 0 541434431 49827840 10453 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12165 10453 603 41 0 12124 0 vsize: 48660 [startup+220.006 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10669 0 0 0 21965 37 0 0 25 0 1 0 541434431 49987584 10504 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12204 10504 603 41 0 12163 0 vsize: 48816 [startup+230.006 s] Raw data (loadavg): 1.01 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10782 0 0 0 22964 37 0 0 25 0 1 0 541434431 50524160 10617 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12335 10617 603 41 0 12294 0 vsize: 49340 [startup+240.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 10870 0 0 0 23964 37 0 0 25 0 1 0 541434431 50814976 10705 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12406 10705 603 41 0 12365 0 vsize: 49624 [startup+250.006 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11055 0 0 0 24964 38 0 0 25 0 1 0 541434431 51634176 10890 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12606 10890 603 41 0 12565 0 vsize: 50424 [startup+260.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11255 0 0 0 25964 38 0 0 25 0 1 0 541434431 52441088 11090 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12803 11090 603 41 0 12762 0 vsize: 51212 [startup+270.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11365 0 0 0 26964 39 0 0 25 0 1 0 541434431 52862976 11200 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12906 11200 603 41 0 12865 0 vsize: 51624 [startup+280.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11422 0 0 0 27963 39 0 0 25 0 1 0 541434431 53133312 11257 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 12972 11257 603 41 0 12931 0 vsize: 51888 [startup+290.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11534 0 0 0 28964 39 0 0 25 0 1 0 541434431 53665792 11369 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13102 11369 603 41 0 13061 0 vsize: 52408 [startup+300.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11704 0 0 0 29963 40 0 0 25 0 1 0 541434431 54226944 11539 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13239 11539 603 41 0 13198 0 vsize: 52956 [startup+310.007 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11866 0 0 0 30963 40 0 0 25 0 1 0 541434431 55058432 11701 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13442 11701 603 41 0 13401 0 vsize: 53768 [startup+320.008 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 11927 0 0 0 31963 40 0 0 25 0 1 0 541434431 55328768 11762 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13508 11762 603 41 0 13467 0 vsize: 54032 [startup+330.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12090 0 0 0 32963 41 0 0 25 0 1 0 541434431 56008704 11925 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13674 11925 603 41 0 13633 0 vsize: 54696 [startup+340.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12116 0 0 0 33963 41 0 0 25 0 1 0 541434431 56008704 11951 4294967295 134512640 134672761 3221224624 3221223792 134560867 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13674 11951 603 41 0 13633 0 vsize: 54696 [startup+350.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12201 0 0 0 34963 41 0 0 25 0 1 0 541434431 56414208 12036 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13773 12036 603 41 0 13732 0 vsize: 55092 [startup+360.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12340 0 0 0 35963 41 0 0 25 0 1 0 541434431 56971264 12175 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 13909 12175 603 41 0 13868 0 vsize: 55636 [startup+370.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12413 0 0 0 36963 42 0 0 25 0 1 0 541434431 57368576 12248 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14006 12248 603 41 0 13965 0 vsize: 56024 [startup+380.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12456 0 0 0 37963 42 0 0 25 0 1 0 541434431 57507840 12291 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14040 12291 603 41 0 13999 0 vsize: 56160 [startup+390.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12544 0 0 0 38963 42 0 0 25 0 1 0 541434431 57815040 12379 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14115 12379 603 41 0 14074 0 vsize: 56460 [startup+400.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12600 0 0 0 39963 42 0 0 25 0 1 0 541434431 58093568 12435 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14183 12435 603 41 0 14142 0 vsize: 56732 [startup+410.009 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12636 0 0 0 40963 42 0 0 25 0 1 0 541434431 58228736 12471 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14216 12471 603 41 0 14175 0 vsize: 56864 [startup+420.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12703 0 0 0 41963 42 0 0 25 0 1 0 541434431 58499072 12538 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14282 12538 603 41 0 14241 0 vsize: 57128 [startup+430.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12883 0 0 0 42963 43 0 0 25 0 1 0 541434431 59166720 12718 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14445 12718 603 41 0 14404 0 vsize: 57780 [startup+440.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 12973 0 0 0 43962 43 0 0 25 0 1 0 541434431 59588608 12808 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14548 12808 603 41 0 14507 0 vsize: 58192 [startup+450.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13024 0 0 0 44962 43 0 0 25 0 1 0 541434431 59719680 12859 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14580 12859 603 41 0 14539 0 vsize: 58320 [startup+460.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13125 0 0 0 45962 43 0 0 25 0 1 0 541434431 60153856 12960 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14686 12960 603 41 0 14645 0 vsize: 58744 [startup+470.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13285 0 0 0 46962 44 0 0 25 0 1 0 541434431 60829696 13120 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14851 13120 603 41 0 14810 0 vsize: 59404 [startup+480.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13418 0 0 0 47962 44 0 0 25 0 1 0 541434431 61227008 13253 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 14948 13253 603 41 0 14907 0 vsize: 59792 [startup+490.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13473 0 0 0 48961 45 0 0 25 0 1 0 541434431 61497344 13308 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15014 13308 603 41 0 14973 0 vsize: 60056 [startup+500.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13529 0 0 0 49962 45 0 0 25 0 1 0 541434431 61632512 13364 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15047 13364 603 41 0 15006 0 vsize: 60188 [startup+510.01 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13612 0 0 0 50962 45 0 0 25 0 1 0 541434431 62033920 13447 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15145 13447 603 41 0 15104 0 vsize: 60580 [startup+520.011 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13713 0 0 0 51962 45 0 0 25 0 1 0 541434431 62435328 13548 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15243 13548 603 41 0 15202 0 vsize: 60972 [startup+530.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13796 0 0 0 52962 45 0 0 25 0 1 0 541434431 62701568 13631 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15308 13631 603 41 0 15267 0 vsize: 61232 [startup+540.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13870 0 0 0 53962 46 0 0 25 0 1 0 541434431 62963712 13705 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15372 13705 603 41 0 15331 0 vsize: 61488 [startup+550.012 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13910 0 0 0 54962 46 0 0 25 0 1 0 541434431 63234048 13745 4294967295 134512640 134672761 3221224624 3221223808 134556675 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15438 13745 603 41 0 15397 0 vsize: 61752 [startup+560.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 13968 0 0 0 55962 46 0 0 25 0 1 0 541434431 63365120 13803 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15470 13803 603 41 0 15429 0 vsize: 61880 [startup+570.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14064 0 0 0 56962 46 0 0 25 0 1 0 541434431 63770624 13899 4294967295 134512640 134672761 3221224624 3221223824 134557830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15569 13899 603 41 0 15528 0 vsize: 62276 [startup+580.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14136 0 0 0 57962 46 0 0 25 0 1 0 541434431 64102400 13971 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15650 13971 603 41 0 15609 0 vsize: 62600 [startup+590.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14284 0 0 0 58962 47 0 0 25 0 1 0 541434431 64655360 14119 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15785 14119 603 41 0 15744 0 vsize: 63140 [startup+600.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14379 0 0 0 59962 47 0 0 25 0 1 0 541434431 65064960 14214 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15885 14214 603 41 0 15844 0 vsize: 63540 [startup+610.013 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14490 0 0 0 60961 47 0 0 25 0 1 0 541434431 65470464 14325 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 15984 14325 603 41 0 15943 0 vsize: 63936 [startup+620.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14602 0 0 0 61961 48 0 0 25 0 1 0 541434431 65871872 14437 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16082 14437 603 41 0 16041 0 vsize: 64328 [startup+630.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14772 0 0 0 62961 48 0 0 25 0 1 0 541434431 66547712 14607 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16247 14607 603 41 0 16206 0 vsize: 64988 [startup+640.014 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14902 0 0 0 63961 49 0 0 25 0 1 0 541434431 67084288 14737 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16378 14737 603 41 0 16337 0 vsize: 65512 [startup+650.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 14980 0 0 0 64961 49 0 0 25 0 1 0 541434431 67485696 14815 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16476 14815 603 41 0 16435 0 vsize: 65904 [startup+660.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15023 0 0 0 65961 49 0 0 25 0 1 0 541434431 67620864 14858 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16509 14858 603 41 0 16468 0 vsize: 66036 [startup+670.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15127 0 0 0 66961 49 0 0 25 0 1 0 541434431 69070848 14962 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16863 14962 603 41 0 16822 0 vsize: 67452 [startup+680.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15205 0 0 0 67961 49 0 0 25 0 1 0 541434431 69337088 15040 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 16928 15040 603 41 0 16887 0 vsize: 67712 [startup+690.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15317 0 0 0 68961 50 0 0 25 0 1 0 541434431 69763072 15152 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17032 15152 603 41 0 16991 0 vsize: 68128 [startup+700.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15407 0 0 0 69961 50 0 0 25 0 1 0 541434431 70184960 15242 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17135 15242 603 41 0 17094 0 vsize: 68540 [startup+710.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15503 0 0 0 70961 50 0 0 25 0 1 0 541434431 70590464 15338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17234 15338 603 41 0 17193 0 vsize: 68936 [startup+720.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15588 0 0 0 71960 51 0 0 25 0 1 0 541434431 70856704 15423 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17299 15423 603 41 0 17258 0 vsize: 69196 [startup+730.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15659 0 0 0 72960 51 0 0 25 0 1 0 541434431 71127040 15494 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17365 15494 603 41 0 17324 0 vsize: 69460 [startup+740.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15739 0 0 0 73960 51 0 0 25 0 1 0 541434431 71532544 15574 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17464 15574 603 41 0 17423 0 vsize: 69856 [startup+750.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15827 0 0 0 74960 51 0 0 25 0 1 0 541434431 71819264 15662 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17534 15662 603 41 0 17493 0 vsize: 70136 [startup+760.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 15926 0 0 0 75960 51 0 0 25 0 1 0 541434431 72282112 15761 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17647 15761 603 41 0 17606 0 vsize: 70588 [startup+770.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16030 0 0 0 76960 52 0 0 25 0 1 0 541434431 72814592 15865 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17777 15865 603 41 0 17736 0 vsize: 71108 [startup+780.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16142 0 0 0 77960 52 0 0 25 0 1 0 541434431 73216000 15977 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 17875 15977 603 41 0 17834 0 vsize: 71500 [startup+790.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16269 0 0 0 78960 52 0 0 25 0 1 0 541434431 73744384 16104 4294967295 134512640 134672761 3221224624 3221223748 134566031 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18004 16104 603 41 0 17963 0 vsize: 72016 [startup+800.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16332 0 0 0 79959 53 0 0 25 0 1 0 541434431 73879552 16167 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18037 16167 603 41 0 17996 0 vsize: 72148 [startup+810.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16463 0 0 0 80959 53 0 0 25 0 1 0 541434431 74416128 16298 4294967295 134512640 134672761 3221224624 3221223748 134566109 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18168 16298 603 41 0 18127 0 vsize: 72672 [startup+820.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16536 0 0 0 81959 53 0 0 25 0 1 0 541434431 74682368 16371 4294967295 134512640 134672761 3221224624 3221223748 134566100 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18233 16371 603 41 0 18192 0 vsize: 72932 [startup+830.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16603 0 0 0 82959 53 0 0 25 0 1 0 541434431 74948608 16438 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18298 16438 603 41 0 18257 0 vsize: 73192 [startup+840.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16692 0 0 0 83958 54 0 0 25 0 1 0 541434431 75345920 16527 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18395 16527 603 41 0 18354 0 vsize: 73580 [startup+850.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16783 0 0 0 84958 54 0 0 25 0 1 0 541434431 75747328 16618 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18493 16618 603 41 0 18452 0 vsize: 73972 [startup+860.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 16912 0 0 0 85958 54 0 0 25 0 1 0 541434431 76279808 16747 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18623 16747 603 41 0 18582 0 vsize: 74492 [startup+870.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17002 0 0 0 86958 55 0 0 25 0 1 0 541434431 76546048 16837 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18688 16837 603 41 0 18647 0 vsize: 74752 [startup+880.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17079 0 0 0 87959 55 0 0 25 0 1 0 541434431 76951552 16914 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18787 16914 603 41 0 18746 0 vsize: 75148 [startup+890.015 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17152 0 0 0 88959 55 0 0 25 0 1 0 541434431 77217792 16987 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18852 16987 603 41 0 18811 0 vsize: 75408 [startup+900.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17223 0 0 0 89958 55 0 0 25 0 1 0 541434431 77479936 17058 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 18916 17058 603 41 0 18875 0 vsize: 75664 [startup+910.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17394 0 0 0 90957 56 0 0 25 0 1 0 541434431 78151680 17229 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19080 17229 603 41 0 19039 0 vsize: 76320 [startup+920.016 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17456 0 0 0 91958 56 0 0 25 0 1 0 541434431 78422016 17291 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19146 17291 603 41 0 19105 0 vsize: 76584 [startup+930.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17547 0 0 0 92958 56 0 0 25 0 1 0 541434431 78807040 17382 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19240 17382 603 41 0 19199 0 vsize: 76960 [startup+940.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17631 0 0 0 93958 57 0 0 25 0 1 0 541434431 79077376 17466 4294967295 134512640 134672761 3221224624 3221223776 134565070 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19306 17466 603 41 0 19265 0 vsize: 77224 [startup+950.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17730 0 0 0 94958 57 0 0 25 0 1 0 541434431 79478784 17565 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19404 17565 603 41 0 19363 0 vsize: 77616 [startup+960.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17834 0 0 0 95958 57 0 0 25 0 1 0 541434431 80031744 17669 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19539 17669 603 41 0 19498 0 vsize: 78156 [startup+970.018 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 17941 0 0 0 96958 57 0 0 25 0 1 0 541434431 80535552 17776 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19662 17776 603 41 0 19621 0 vsize: 78648 [startup+980.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18049 0 0 0 97957 58 0 0 25 0 1 0 541434431 80830464 17884 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19734 17884 603 41 0 19693 0 vsize: 78936 [startup+990.017 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18165 0 0 0 98957 58 0 0 25 0 1 0 541434431 81399808 18000 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19873 18000 603 41 0 19832 0 vsize: 79492 [startup+1000.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18255 0 0 0 99957 58 0 0 25 0 1 0 541434431 81797120 18090 4294967295 134512640 134672761 3221224624 3221223792 134560806 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 19970 18090 603 41 0 19929 0 vsize: 79880 [startup+1010.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18344 0 0 0 100957 58 0 0 25 0 1 0 541434431 82063360 18179 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20035 18179 603 41 0 19994 0 vsize: 80140 [startup+1020.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18461 0 0 0 101957 59 0 0 25 0 1 0 541434431 82677760 18296 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20185 18296 603 41 0 20144 0 vsize: 80740 [startup+1030.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18572 0 0 0 102957 59 0 0 25 0 1 0 541434431 83083264 18407 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20284 18407 603 41 0 20243 0 vsize: 81136 [startup+1040.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18694 0 0 0 103957 60 0 0 25 0 1 0 541434431 83656704 18529 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20424 18529 603 41 0 20383 0 vsize: 81696 [startup+1050.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18783 0 0 0 104956 60 0 0 25 0 1 0 541434431 83927040 18618 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20490 18618 603 41 0 20449 0 vsize: 81960 [startup+1060.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 18912 0 0 0 105956 60 0 0 25 0 1 0 541434431 84463616 18747 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20621 18747 603 41 0 20580 0 vsize: 82484 [startup+1070.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19019 0 0 0 106956 61 0 0 25 0 1 0 541434431 84869120 18854 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20720 18854 603 41 0 20679 0 vsize: 82880 [startup+1080.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19150 0 0 0 107956 61 0 0 25 0 1 0 541434431 85528576 18985 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20881 18985 603 41 0 20840 0 vsize: 83524 [startup+1090.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19256 0 0 0 108955 62 0 0 25 0 1 0 541434431 85946368 19091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 20983 19091 603 41 0 20942 0 vsize: 83932 [startup+1100.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 109956 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1110.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 110956 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1120.02 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 111956 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1130.03 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 112957 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1140.03 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 113957 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1150.03 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 114957 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223760 134560726 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1160.03 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 115957 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1170.03 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 116958 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1180.03 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 117958 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1190.03 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 118958 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 [startup+1200.03 s] Raw data (loadavg): 1.00 0.97 0.91 2/54 14821 Raw data (stat): 14821 (minisat+) R 14820 10614 10613 0 -1 0 19306 0 0 0 119958 62 0 0 25 0 1 0 541434431 86077440 19141 4294967295 134512640 134672761 3221224624 3221223792 134561400 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 21015 19141 603 41 0 20974 0 vsize: 84060 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 1.00 0.97 0.91 1/54 14821 Raw data (stat): 14821 (minisat+) Z 14820 10614 10613 0 -1 12 19308 0 0 0 119958 66 0 0 25 0 1 0 541434431 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: 0 Real time (s): 1200.07 CPU time (s): 1200.25 CPU user time (s): 1199.59 CPU system time (s): 0.660899 CPU usage (%): 100.015 Max. virtual memory (Kb): 84060 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####