Name | normalized-opb/submitted/aloul/FPGA_SAT05/normalized-chnl50_60_pb.cnf.cr.opb |
MD5SUM | 6968a43b42bba7df68b13fdfd3b616a1 |
Bench Category | no optimization function (SAT) |
Has Objective Function | NO |
Satisfiable | NO |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 0 |
Biggest coefficient in the objective function | 0 |
Number of bits for the biggest coefficient in the objective function | 0 |
Sum of the numbers in the objective function | 0 |
Number of bits of the sum of numbers in the objective function | 0 |
Biggest number in a constraint | 1 |
Number of bits of the biggest number in a constraint | 1 |
Biggest sum of numbers in a constraint | 61 |
Number of bits of the biggest sum of numbers | 6 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.187971 |
Number of variables | 6000 |
Total number of constraints | 220 |
Number of constraints which are clauses | 120 |
Number of constraints which are cardinality constraints (but not clauses) | 100 |
Number of constraints which are nor clauses,nor cardinality constraints | 0 |
Minimum length of a constraint | 50 |
Maximum length of a constraint | 60 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc13 THE 2005-04-14 03:33:25 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=4534 boxname=wulflinc13 idbench=22 idsolver=13 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 6968a43b42bba7df68b13fdfd3b616a1 /oldhome/oroussel/tmp/wulflinc13/normalized-chnl50_60_pb.cnf.cr.opb REAL COMMAND: minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-chnl50_60_pb.cnf.cr.opb /oldhome/oroussel/tmp/wulflinc13/normalized-chnl50_60_pb.cnf.cr.opb IDLAUNCH: 4534 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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 : 2 cpu MHz : 451.242 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: 890992 kB Buffers: 35388 kB Cached: 88524 kB SwapCached: 392 kB Active: 54904 kB Inactive: 72216 kB HighTotal: 131008 kB HighFree: 38612 kB LowTotal: 903652 kB LowFree: 852380 kB SwapTotal: 2097136 kB SwapFree: 2096744 kB Dirty: 28 kB Writeback: 0 kB Mapped: 6928 kB Slab: 10992 kB Committed_AS: 63484 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-04-14 03:53:27 (client local time) WITH STATUS 0 IN 1200.22 SECONDS stats: 4534 7 1200.22 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 220 PB-constraints to clauses... c -- Unit propagations: (none) c -- Detecting intervals from adjacent constraints: (none) c -- Clauses(.)/Splits(s): ........................................................................................................................ c ---[ 99]---> BDD-cost: 117 c ---[ 98]---> BDD-cost: 117 c ---[ 97]---> BDD-cost: 117 c ---[ 96]---> BDD-cost: 117 c ---[ 95]---> BDD-cost: 117 c ---[ 94]---> BDD-cost: 117 c ---[ 93]---> BDD-cost: 117 c ---[ 92]---> BDD-cost: 117 c ---[ 91]---> BDD-cost: 117 c ---[ 90]---> BDD-cost: 117 c ---[ 89]---> BDD-cost: 117 c ---[ 88]---> BDD-cost: 117 c ---[ 87]---> BDD-cost: 117 c ---[ 86]---> BDD-cost: 117 c ---[ 85]---> BDD-cost: 117 c ---[ 84]---> BDD-cost: 117 c ---[ 83]---> BDD-cost: 117 c ---[ 82]---> BDD-cost: 117 c ---[ 81]---> BDD-cost: 117 c ---[ 80]---> BDD-cost: 117 c ---[ 79]---> BDD-cost: 117 c ---[ 78]---> BDD-cost: 117 c ---[ 77]---> BDD-cost: 117 c ---[ 76]---> BDD-cost: 117 c ---[ 75]---> BDD-cost: 117 c ---[ 74]---> BDD-cost: 117 c ---[ 73]---> BDD-cost: 117 c ---[ 72]---> BDD-cost: 117 c ---[ 71]---> BDD-cost: 117 c ---[ 70]---> BDD-cost: 117 c ---[ 69]---> BDD-cost: 117 c ---[ 68]---> BDD-cost: 117 c ---[ 67]---> BDD-cost: 117 c ---[ 66]---> BDD-cost: 117 c ---[ 65]---> BDD-cost: 117 c ---[ 64]---> BDD-cost: 117 c ---[ 63]---> BDD-cost: 117 c ---[ 62]---> BDD-cost: 117 c ---[ 61]---> BDD-cost: 117 c ---[ 60]---> BDD-cost: 117 c ---[ 59]---> BDD-cost: 117 c ---[ 58]---> BDD-cost: 117 c ---[ 57]---> BDD-cost: 117 c ---[ 56]---> BDD-cost: 117 c ---[ 55]---> BDD-cost: 117 c ---[ 54]---> BDD-cost: 117 c ---[ 53]---> BDD-cost: 117 c ---[ 52]---> BDD-cost: 117 c ---[ 51]---> BDD-cost: 117 c ---[ 50]---> BDD-cost: 117 c ---[ 49]---> BDD-cost: 117 c ---[ 48]---> BDD-cost: 117 c ---[ 47]---> BDD-cost: 117 c ---[ 46]---> BDD-cost: 117 c ---[ 45]---> BDD-cost: 117 c ---[ 44]---> BDD-cost: 117 c ---[ 43]---> BDD-cost: 117 c ---[ 42]---> BDD-cost: 117 c ---[ 41]---> BDD-cost: 117 c ---[ 40]---> BDD-cost: 117 c ---[ 39]---> BDD-cost: 117 c ---[ 38]---> BDD-cost: 117 c ---[ 37]---> BDD-cost: 117 c ---[ 36]---> BDD-cost: 117 c ---[ 35]---> BDD-cost: 117 c ---[ 34]---> BDD-cost: 117 c ---[ 33]---> BDD-cost: 117 c ---[ 32]---> BDD-cost: 117 c ---[ 31]---> BDD-cost: 117 c ---[ 30]---> BDD-cost: 117 c ---[ 29]---> BDD-cost: 117 c ---[ 28]---> BDD-cost: 117 c ---[ 27]---> BDD-cost: 117 c ---[ 26]---> BDD-cost: 117 c ---[ 25]---> BDD-cost: 117 c ---[ 24]---> BDD-cost: 117 c ---[ 23]---> BDD-cost: 117 c ---[ 22]---> BDD-cost: 117 c ---[ 21]---> BDD-cost: 117 c ---[ 20]---> BDD-cost: 117 c ---[ 19]---> BDD-cost: 117 c ---[ 18]---> BDD-cost: 117 c ---[ 17]---> BDD-cost: 117 c ---[ 16]---> BDD-cost: 117 c ---[ 15]---> BDD-cost: 117 c ---[ 14]---> BDD-cost: 117 c ---[ 13]---> BDD-cost: 117 c ---[ 12]---> BDD-cost: 117 c ---[ 11]---> BDD-cost: 117 c ---[ 10]---> BDD-cost: 117 c ---[ 9]---> BDD-cost: 117 c ---[ 8]---> BDD-cost: 117 c ---[ 7]---> BDD-cost: 117 c ---[ 6]---> BDD-cost: 117 c ---[ 5]---> BDD-cost: 117 c ---[ 4]---> BDD-cost: 117 c ---[ 3]---> BDD-cost: 117 c ---[ 2]---> BDD-cost: 117 c ---[ 1]---> BDD-cost: 117 c ---[ 0]---> BDD-cost: 117 c ==================================[MINISAT+]================================== c | Conflicts | Original | Learnt | Progress | c | | Clauses Literals | Max Clauses Literals LPC | | c ============================================================================== c | 0 | 52320 150800 | 17440 0 0 nan | 0.000 % | c | 100 | 52120 150200 | 19184 21 70 3.3 | 0.797 % | c | 250 | 51825 149315 | 21102 59 275 4.7 | 1.124 % | c | 475 | 51250 147590 | 23212 58 178 3.1 | 1.780 % | c | 814 | 50480 145280 | 25533 69 207 3.0 | 2.650 % | c | 1320 | 49236 141550 | 28087 132 5156 39.1 | 4.056 % | c | 2080 | 48841 140365 | 30896 788 184217 233.8 | 4.497 % | c | 3221 | 47786 137200 | 33985 1559 386219 247.7 | 5.689 % | c | 4931 | 46506 133360 | 37384 2856 781496 273.6 | 7.136 % | c | 7493 | 44641 127765 | 41122 4788 1484263 310.0 | 9.243 % | c | 11338 | 41436 118150 | 45234 7554 2311239 306.0 | 12.864 % | c | 17109 | 39331 111835 | 49758 12673 4512736 356.1 | 15.243 % | c | 25760 | 34751 98095 | 54734 19839 7182049 362.0 | 20.418 % | c | 38734 | 31701 88945 | 60207 31859 12451796 390.8 | 23.864 % | c | 58198 | 30341 84865 | 66228 50932 20580185 404.1 | 25.401 % | #### 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.92 0.97 0.91 2/54 5455 Raw data (stat): 5455 (runsolver) R 5454 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423164625 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0002 s] Raw data (loadavg): 0.93 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 1862 0 0 0 994 4 0 0 25 0 1 0 423164625 9670656 1781 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2361 1781 603 41 0 2320 0 vsize: 9444 [startup+19.9998 s] Raw data (loadavg): 0.94 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 2167 0 0 0 1992 5 0 0 25 0 1 0 423164625 11022336 2086 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 2691 2086 603 41 0 2650 0 vsize: 10764 [startup+30.0007 s] Raw data (loadavg): 0.95 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 2544 0 0 0 2991 6 0 0 25 0 1 0 423164625 12500992 2463 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3052 2463 603 41 0 3011 0 vsize: 12208 [startup+40.0011 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3210 0 0 0 3989 8 0 0 25 0 1 0 423164625 15200256 3129 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3711 3129 603 41 0 3670 0 vsize: 14844 [startup+50.0007 s] Raw data (loadavg): 0.96 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3341 0 0 0 4989 9 0 0 25 0 1 0 423164625 15740928 3260 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 3843 3260 603 41 0 3802 0 vsize: 15372 [startup+60.0007 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3515 0 0 0 5989 9 0 0 25 0 1 0 423164625 16551936 3434 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4041 3434 603 41 0 4000 0 vsize: 16164 [startup+70.0011 s] Raw data (loadavg): 0.97 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3703 0 0 0 6988 10 0 0 25 0 1 0 423164625 17227776 3622 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4206 3622 603 41 0 4165 0 vsize: 16824 [startup+80.0007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 3973 0 0 0 7988 10 0 0 25 0 1 0 423164625 18440192 3892 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4502 3892 603 41 0 4461 0 vsize: 18008 [startup+90.0007 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 4304 0 0 0 8987 11 0 0 25 0 1 0 423164625 19787776 4223 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4831 4223 603 41 0 4790 0 vsize: 19324 [startup+100 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 4367 0 0 0 9987 11 0 0 25 0 1 0 423164625 19922944 4286 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4864 4286 603 41 0 4823 0 vsize: 19456 [startup+110.001 s] Raw data (loadavg): 0.98 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 4461 0 0 0 10988 11 0 0 25 0 1 0 423164625 20328448 4380 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 4963 4380 603 41 0 4922 0 vsize: 19852 [startup+120.001 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 4627 0 0 0 11987 11 0 0 25 0 1 0 423164625 21004288 4546 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 5128 4546 603 41 0 5087 0 vsize: 20512 [startup+130 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 5529 0 0 0 12986 13 0 0 25 0 1 0 423164625 24788992 5448 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6052 5448 603 41 0 6011 0 vsize: 24208 [startup+140 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 5624 0 0 0 13985 14 0 0 25 0 1 0 423164625 25194496 5543 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6151 5543 603 41 0 6110 0 vsize: 24604 [startup+150 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 5853 0 0 0 14985 14 0 0 25 0 1 0 423164625 26140672 5772 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6382 5772 603 41 0 6341 0 vsize: 25528 [startup+160 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 5892 0 0 0 15985 14 0 0 25 0 1 0 423164625 26275840 5811 4294967295 134512640 134672761 3221224544 3221223696 134565213 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 6415 5811 603 41 0 6374 0 vsize: 25660 [startup+170 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 6814 0 0 0 16984 16 0 0 25 0 1 0 423164625 30052352 6733 4294967295 134512640 134672761 3221224544 3221223692 1074733099 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7337 6733 603 41 0 7296 0 vsize: 29348 [startup+180 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 6898 0 0 0 17983 16 0 0 25 0 1 0 423164625 30322688 6817 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 7403 6817 603 41 0 7362 0 vsize: 29612 [startup+190 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7000 0 0 0 18982 17 0 0 25 0 1 0 423164625 30728192 6919 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7502 6919 603 41 0 7461 0 vsize: 30008 [startup+200 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7059 0 0 0 19982 17 0 0 25 0 1 0 423164625 30998528 6978 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7568 6978 603 41 0 7527 0 vsize: 30272 [startup+210 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7432 0 0 0 20981 18 0 0 25 0 1 0 423164625 32485376 7351 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7931 7351 603 41 0 7890 0 vsize: 31724 [startup+220 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7444 0 0 0 21981 18 0 0 25 0 1 0 423164625 32616448 7363 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 7963 7363 603 41 0 7922 0 vsize: 31852 [startup+230 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7517 0 0 0 22981 18 0 0 25 0 1 0 423164625 32882688 7436 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8028 7436 603 41 0 7987 0 vsize: 32112 [startup+240 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7598 0 0 0 23981 19 0 0 25 0 1 0 423164625 33280000 7517 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8125 7517 603 41 0 8084 0 vsize: 32500 [startup+249.999 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7746 0 0 0 24981 19 0 0 25 0 1 0 423164625 33816576 7665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8256 7665 603 41 0 8215 0 vsize: 33024 [startup+260 s] Raw data (loadavg): 0.99 0.97 0.91 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7746 0 0 0 25981 19 0 0 25 0 1 0 423164625 33816576 7665 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8256 7665 603 41 0 8215 0 vsize: 33024 [startup+270 s] Raw data (loadavg): 1.07 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 7884 0 0 0 26981 19 0 0 25 0 1 0 423164625 34353152 7803 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8387 7803 603 41 0 8346 0 vsize: 33548 [startup+279.999 s] Raw data (loadavg): 1.06 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 8208 0 0 0 27980 20 0 0 25 0 1 0 423164625 35696640 8127 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 8715 8127 603 41 0 8674 0 vsize: 34860 [startup+290 s] Raw data (loadavg): 1.05 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 8777 0 0 0 28979 21 0 0 25 0 1 0 423164625 38043648 8696 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9288 8696 603 41 0 9247 0 vsize: 37152 [startup+300 s] Raw data (loadavg): 1.04 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 8851 0 0 0 29979 21 0 0 25 0 1 0 423164625 38449152 8770 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9387 8770 603 41 0 9346 0 vsize: 37548 [startup+310 s] Raw data (loadavg): 1.04 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9185 0 0 0 30979 22 0 0 25 0 1 0 423164625 39800832 9104 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9717 9104 603 41 0 9676 0 vsize: 38868 [startup+320 s] Raw data (loadavg): 1.03 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9293 0 0 0 31979 22 0 0 25 0 1 0 423164625 40206336 9212 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9212 603 41 0 9775 0 vsize: 39264 [startup+330 s] Raw data (loadavg): 1.03 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9294 0 0 0 32979 22 0 0 25 0 1 0 423164625 40206336 9213 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 9816 9213 603 41 0 9775 0 vsize: 39264 [startup+340 s] Raw data (loadavg): 1.02 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9543 0 0 0 33979 22 0 0 25 0 1 0 423164625 41287680 9462 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10080 9462 603 41 0 10039 0 vsize: 40320 [startup+350 s] Raw data (loadavg): 1.02 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9680 0 0 0 34978 23 0 0 25 0 1 0 423164625 41828352 9599 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10212 9599 603 41 0 10171 0 vsize: 40848 [startup+360.001 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9779 0 0 0 35978 23 0 0 25 0 1 0 423164625 42233856 9698 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10311 9698 603 41 0 10270 0 vsize: 41244 [startup+370 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9782 0 0 0 36978 23 0 0 25 0 1 0 423164625 42233856 9701 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 10311 9701 603 41 0 10270 0 vsize: 41244 [startup+380 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 9813 0 0 0 37978 23 0 0 25 0 1 0 423164625 42369024 9732 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 10344 9732 603 41 0 10303 0 vsize: 41376 [startup+390.001 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 10508 0 0 0 38976 25 0 0 25 0 1 0 423164625 45203456 10427 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 11036 10427 603 41 0 10995 0 vsize: 44144 [startup+400.001 s] Raw data (loadavg): 1.01 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 11214 0 0 0 39973 27 0 0 25 0 1 0 423164625 48029696 11133 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11726 11133 603 41 0 11685 0 vsize: 46904 [startup+410.001 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 11249 0 0 0 40973 27 0 0 25 0 1 0 423164625 48164864 11168 4294967295 134512640 134672761 3221224544 3221223796 134562232 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11759 11168 603 41 0 11718 0 vsize: 47036 [startup+420 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 11472 0 0 0 41973 28 0 0 25 0 1 0 423164625 49111040 11391 4294967295 134512640 134672761 3221224544 3221223648 134559872 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 11990 11391 603 41 0 11949 0 vsize: 47960 [startup+430 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 11849 0 0 0 42972 28 0 0 25 0 1 0 423164625 50724864 11768 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 12384 11768 603 41 0 12343 0 vsize: 49536 [startup+440 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12820 0 0 0 43970 31 0 0 25 0 1 0 423164625 54640640 12739 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13340 12739 603 41 0 13299 0 vsize: 53360 [startup+450 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12823 0 0 0 44970 31 0 0 25 0 1 0 423164625 54640640 12742 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13340 12742 603 41 0 13299 0 vsize: 53360 [startup+460 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12824 0 0 0 45970 31 0 0 25 0 1 0 423164625 54640640 12743 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13340 12743 603 41 0 13299 0 vsize: 53360 [startup+470 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12824 0 0 0 46971 31 0 0 25 0 1 0 423164625 54640640 12743 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13340 12743 603 41 0 13299 0 vsize: 53360 [startup+479.999 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12824 0 0 0 47971 31 0 0 25 0 1 0 423164625 54640640 12743 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13340 12743 603 41 0 13299 0 vsize: 53360 [startup+490 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12825 0 0 0 48971 31 0 0 25 0 1 0 423164625 54640640 12744 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13340 12744 603 41 0 13299 0 vsize: 53360 [startup+500 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12827 0 0 0 49971 31 0 0 25 0 1 0 423164625 54640640 12746 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13340 12746 603 41 0 13299 0 vsize: 53360 [startup+510 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 12919 0 0 0 50971 31 0 0 25 0 1 0 423164625 55046144 12838 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13439 12838 603 41 0 13398 0 vsize: 53756 [startup+520 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13248 0 0 0 51971 32 0 0 25 0 1 0 423164625 56397824 13167 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13769 13167 603 41 0 13728 0 vsize: 55076 [startup+530 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13357 0 0 0 52971 32 0 0 25 0 1 0 423164625 56803328 13276 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 13868 13276 603 41 0 13827 0 vsize: 55472 [startup+540 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13838 0 0 0 53970 33 0 0 25 0 1 0 423164625 58826752 13757 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14362 13757 603 41 0 14321 0 vsize: 57448 [startup+550 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13847 0 0 0 54970 33 0 0 25 0 1 0 423164625 58826752 13766 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14362 13766 603 41 0 14321 0 vsize: 57448 [startup+560.001 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13932 0 0 0 55970 34 0 0 25 0 1 0 423164625 59232256 13851 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14461 13851 603 41 0 14420 0 vsize: 57844 [startup+570.001 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 13949 0 0 0 56970 34 0 0 25 0 1 0 423164625 59232256 13868 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14461 13868 603 41 0 14420 0 vsize: 57844 [startup+580.001 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 14296 0 0 0 57969 35 0 0 25 0 1 0 423164625 60715008 14215 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14823 14215 603 41 0 14782 0 vsize: 59292 [startup+590.001 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 14308 0 0 0 58969 35 0 0 25 0 1 0 423164625 60715008 14227 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14823 14227 603 41 0 14782 0 vsize: 59292 [startup+600.001 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 14309 0 0 0 59969 35 0 0 25 0 1 0 423164625 60715008 14228 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 14823 14228 603 41 0 14782 0 vsize: 59292 [startup+610.002 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 14505 0 0 0 60969 35 0 0 25 0 1 0 423164625 61526016 14424 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15021 14424 603 41 0 14980 0 vsize: 60084 [startup+620.002 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 15094 0 0 0 61969 36 0 0 25 0 1 0 423164625 63946752 15013 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15612 15013 603 41 0 15571 0 vsize: 62448 [startup+630.002 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 15250 0 0 0 62969 36 0 0 25 0 1 0 423164625 64618496 15169 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 15776 15169 603 41 0 15735 0 vsize: 63104 [startup+640.003 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 16043 0 0 0 63966 38 0 0 25 0 1 0 423164625 67981312 15962 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 16597 15962 603 41 0 16556 0 vsize: 66388 [startup+650.003 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 17033 0 0 0 64964 41 0 0 25 0 1 0 423164625 72036352 16952 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17587 16952 603 41 0 17546 0 vsize: 70348 [startup+660.003 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 17339 0 0 0 65963 42 0 0 25 0 1 0 423164625 73232384 17258 4294967295 134512640 134672761 3221224544 3221223648 134559847 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 17879 17258 603 41 0 17838 0 vsize: 71516 [startup+670.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 18013 0 0 0 66962 43 0 0 25 0 1 0 423164625 75927552 17932 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 18537 17932 603 41 0 18496 0 vsize: 74148 [startup+680.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19107 0 0 0 67960 45 0 0 25 0 1 0 423164625 80502784 19026 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19654 19026 603 41 0 19613 0 vsize: 78616 [startup+690.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19320 0 0 0 68960 46 0 0 25 0 1 0 423164625 81309696 19239 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 19851 19239 603 41 0 19810 0 vsize: 79404 [startup+700.005 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19524 0 0 0 69960 46 0 0 25 0 1 0 423164625 82120704 19443 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20049 19443 603 41 0 20008 0 vsize: 80196 [startup+710.005 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19524 0 0 0 70960 46 0 0 25 0 1 0 423164625 82120704 19443 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20049 19443 603 41 0 20008 0 vsize: 80196 [startup+720.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 19783 0 0 0 71959 47 0 0 25 0 1 0 423164625 83202048 19702 4294967295 134512640 134672761 3221224544 3221223648 134560510 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20313 19702 603 41 0 20272 0 vsize: 81252 [startup+730.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 20260 0 0 0 72958 48 0 0 25 0 1 0 423164625 85229568 20179 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 20808 20179 603 41 0 20767 0 vsize: 83232 [startup+740.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 21168 0 0 0 73957 50 0 0 25 0 1 0 423164625 88870912 21087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 21697 21087 603 41 0 21656 0 vsize: 86788 [startup+750.003 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 21880 0 0 0 74956 51 0 0 25 0 1 0 423164625 91844608 21799 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 22423 21799 603 41 0 22382 0 vsize: 89692 [startup+760.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 22551 0 0 0 75954 53 0 0 25 0 1 0 423164625 94535680 22470 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23080 22470 603 41 0 23039 0 vsize: 92320 [startup+770.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 22823 0 0 0 76954 53 0 0 25 0 1 0 423164625 95621120 22742 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23345 22742 603 41 0 23304 0 vsize: 93380 [startup+780.003 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 22824 0 0 0 77954 53 0 0 25 0 1 0 423164625 95621120 22743 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23345 22743 603 41 0 23304 0 vsize: 93380 [startup+790.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 22873 0 0 0 78954 53 0 0 25 0 1 0 423164625 95891456 22792 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23411 22792 603 41 0 23370 0 vsize: 93644 [startup+800.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23154 0 0 0 79953 54 0 0 25 0 1 0 423164625 96976896 23073 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23676 23073 603 41 0 23635 0 vsize: 94704 [startup+810.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23367 0 0 0 80953 55 0 0 25 0 1 0 423164625 97927168 23286 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 23908 23286 603 41 0 23867 0 vsize: 95632 [startup+820.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23603 0 0 0 81953 56 0 0 25 0 1 0 423164625 98869248 23522 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24138 23522 603 41 0 24097 0 vsize: 96552 [startup+830.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23723 0 0 0 82952 56 0 0 25 0 1 0 423164625 99274752 23642 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24237 23642 603 41 0 24196 0 vsize: 96948 [startup+840.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23733 0 0 0 83953 56 0 0 25 0 1 0 423164625 99409920 23652 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24270 23652 603 41 0 24229 0 vsize: 97080 [startup+850.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23733 0 0 0 84953 56 0 0 25 0 1 0 423164625 99409920 23652 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24270 23652 603 41 0 24229 0 vsize: 97080 [startup+860.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23743 0 0 0 85953 56 0 0 25 0 1 0 423164625 99409920 23662 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24270 23662 603 41 0 24229 0 vsize: 97080 [startup+870.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 23745 0 0 0 86953 56 0 0 25 0 1 0 423164625 99409920 23664 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24270 23664 603 41 0 24229 0 vsize: 97080 [startup+880.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 24219 0 0 0 87951 58 0 0 25 0 1 0 423164625 101294080 24138 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 24730 24138 603 41 0 24689 0 vsize: 98920 [startup+890.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 24758 0 0 0 88950 59 0 0 25 0 1 0 423164625 103587840 24677 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 25290 24677 603 41 0 25249 0 vsize: 101160 [startup+900.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 25195 0 0 0 89949 60 0 0 25 0 1 0 423164625 105345024 25114 4294967295 134512640 134672761 3221224544 3221223648 134559979 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 25719 25114 603 41 0 25678 0 vsize: 102876 [startup+910.005 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 25621 0 0 0 90948 61 0 0 25 0 1 0 423164625 107098112 25540 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26147 25540 603 41 0 26106 0 vsize: 104588 [startup+920.005 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 25812 0 0 0 91948 61 0 0 25 0 1 0 423164625 107909120 25731 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26345 25731 603 41 0 26304 0 vsize: 105380 [startup+930.004 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 25889 0 0 0 92948 61 0 0 25 0 1 0 423164625 108175360 25808 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26410 25808 603 41 0 26369 0 vsize: 105640 [startup+940.005 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 26131 0 0 0 93948 62 0 0 25 0 1 0 423164625 109256704 26050 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26674 26050 603 41 0 26633 0 vsize: 106696 [startup+950.005 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 26274 0 0 0 94947 62 0 0 25 0 1 0 423164625 109797376 26193 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 26806 26193 603 41 0 26765 0 vsize: 107224 [startup+960.005 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 26706 0 0 0 95947 63 0 0 25 0 1 0 423164625 111534080 26625 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27230 26625 603 41 0 27189 0 vsize: 108920 [startup+970.005 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 27464 0 0 0 96946 64 0 0 25 0 1 0 423164625 114626560 27383 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 27985 27383 603 41 0 27944 0 vsize: 111940 [startup+980.006 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 28085 0 0 0 97944 66 0 0 25 0 1 0 423164625 117190656 28004 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 28611 28004 603 41 0 28570 0 vsize: 114444 [startup+990.007 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 29052 0 0 0 98941 69 0 0 25 0 1 0 423164625 121102336 28971 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 29566 28971 603 41 0 29525 0 vsize: 118264 [startup+1000.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 29909 0 0 0 99939 72 0 0 25 0 1 0 423164625 124727296 29828 4294967295 134512640 134672761 3221224544 3221223648 134559966 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30451 29828 603 41 0 30410 0 vsize: 121804 [startup+1010.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30243 0 0 0 100939 72 0 0 25 0 1 0 423164625 126070784 30162 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30779 30162 603 41 0 30738 0 vsize: 123116 [startup+1020.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30382 0 0 0 101938 73 0 0 25 0 1 0 423164625 126611456 30301 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 30911 30301 603 41 0 30870 0 vsize: 123644 [startup+1030.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30713 0 0 0 102938 73 0 0 25 0 1 0 423164625 127954944 30632 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31239 30632 603 41 0 31198 0 vsize: 124956 [startup+1040.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30759 0 0 0 103938 73 0 0 25 0 1 0 423164625 128225280 30678 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31305 30678 603 41 0 31264 0 vsize: 125220 [startup+1050.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30779 0 0 0 104938 74 0 0 25 0 1 0 423164625 128225280 30698 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31305 30698 603 41 0 31264 0 vsize: 125220 [startup+1060.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30779 0 0 0 105938 74 0 0 25 0 1 0 423164625 128225280 30698 4294967295 134512640 134672761 3221224544 3221223716 134556641 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31305 30698 603 41 0 31264 0 vsize: 125220 [startup+1070.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 30872 0 0 0 106938 74 0 0 25 0 1 0 423164625 128630784 30791 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 31404 30791 603 41 0 31363 0 vsize: 125616 [startup+1080.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 31729 0 0 0 107936 76 0 0 25 0 1 0 423164625 132407296 31648 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32326 31648 603 41 0 32285 0 vsize: 129304 [startup+1090.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 31994 0 0 0 108935 77 0 0 25 0 1 0 423164625 133505024 31913 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32594 31913 603 41 0 32553 0 vsize: 130376 [startup+1100.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32147 0 0 0 109935 77 0 0 25 0 1 0 423164625 134184960 32066 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32760 32066 603 41 0 32719 0 vsize: 131040 [startup+1110.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32183 0 0 0 110935 77 0 0 25 0 1 0 423164625 134320128 32102 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32793 32102 603 41 0 32752 0 vsize: 131172 [startup+1120.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32195 0 0 0 111935 77 0 0 25 0 1 0 423164625 134320128 32114 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 32793 32114 603 41 0 32752 0 vsize: 131172 [startup+1130.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32546 0 0 0 112935 78 0 0 25 0 1 0 423164625 135802880 32465 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33155 32465 603 41 0 33114 0 vsize: 132620 [startup+1140.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 32958 0 0 0 113935 78 0 0 25 0 1 0 423164625 137412608 32877 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 33548 32877 603 41 0 33507 0 vsize: 134192 [startup+1150.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 33437 0 0 0 114934 80 0 0 25 0 1 0 423164625 139436032 33356 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34042 33356 603 41 0 34001 0 vsize: 136168 [startup+1160.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 33887 0 0 0 115933 81 0 0 25 0 1 0 423164625 141193216 33806 4294967295 134512640 134672761 3221224544 3221223648 134559869 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34471 33806 603 41 0 34430 0 vsize: 137884 [startup+1170.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 34297 0 0 0 116932 82 0 0 25 0 1 0 423164625 142950400 34216 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 34900 34216 603 41 0 34859 0 vsize: 139600 [startup+1180.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 34445 0 0 0 117932 82 0 0 25 0 1 0 423164625 143495168 34364 4294967295 134512640 134672761 3221224544 3221223716 134556680 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35033 34364 603 41 0 34992 0 vsize: 140132 [startup+1190.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 34445 0 0 0 118932 82 0 0 25 0 1 0 423164625 143495168 34364 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35033 34364 603 41 0 34992 0 vsize: 140132 [startup+1200.01 s] Raw data (loadavg): 1.00 0.99 0.92 2/54 5455 Raw data (stat): 5455 (minisat+) R 5454 30701 30700 0 -1 0 34445 0 0 0 119932 82 0 0 25 0 1 0 423164625 143495168 34364 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 35033 34364 603 41 0 34992 0 vsize: 140132 Maximum CPU time exceeded: sending SIGTERM and SIGKILL [startup+1200.07 s] Raw data (loadavg): 1.00 0.99 0.92 1/54 5455 Raw data (stat): 5455 (minisat+) Z 5454 30701 30700 0 -1 12 34447 0 0 0 119932 89 0 0 25 0 1 0 423164625 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0 Raw data (statm): 0 0 0 0 0 0 0 vsize: 0 Maximum CPU time exceeded: sending SIGTERM and SIGKILL Child status: 0 Real time (s): 1200.07 CPU time (s): 1200.22 CPU user time (s): 1199.33 CPU system time (s): 0.890864 CPU usage (%): 100.012 Max. virtual memory (Kb): 140132 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####