Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-misc04.opb |
MD5SUM | 7b42190d864979953c47e5a92736f365 |
Bench Category | optimization, big integers (OPTBIGINT) |
Has Objective Function | YES |
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 | 31 |
Biggest coefficient in the objective function | 1073741824 |
Number of bits for the biggest coefficient in the objective function | 31 |
Sum of the numbers in the objective function | 2147483647 |
Number of bits of the sum of numbers in the objective function | 31 |
Biggest number in a constraint | 43188899594881916928 |
Number of bits of the biggest number in a constraint | 66 |
Biggest sum of numbers in a constraint | 133861748414790074368 |
Number of bits of the biggest sum of numbers | 67 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 4.12137 |
Number of variables | 146276 |
Total number of constraints | 1755 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 45 |
Number of constraints which are nor clauses,nor cardinality constraints | 1710 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 5071 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc6 THE 2005-05-25 18:45:44 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=22106 boxname=wulflinc6 idbench=922 idsolver=15 numberseed=0 MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814 /oldhome/oroussel/solvers/minisat+_script MD5SUM BENCH: 7b42190d864979953c47e5a92736f365 /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-misc04.opb REAL COMMAND: minisat+_script /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-20-10-misc04.opb IDLAUNCH: 22106 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.042 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.042 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: 646924 kB Buffers: 34616 kB Cached: 327684 kB SwapCached: 412 kB Active: 102620 kB Inactive: 261960 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 646672 kB SwapTotal: 2097136 kB SwapFree: 2096036 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5696 kB Slab: 17516 kB Committed_AS: 63736 kB PageTables: 320 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 19:06:17 (client local time) WITH STATUS 152 IN 1232.74 SECONDS stats: 22106 7 1232.74 152 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c PARSE ERROR! [line 6477] Integer overflow. Use BigNum-version. c OK -- Running BigNum-version instead... c Parsing PB file... c Converting 1985 PB-constraints to clauses... c -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ################################################################################################################################################################################################################################################################################################################ c -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss c ---[1999]---> Sorter-cost: 2992 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 c ---[1998]---> Sorter-cost: 2992 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 c ---[1997]---> Sorter-cost: 2992 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 c ---[1996]---> Sorter-cost: 2992 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 c ---[1995]---> Sorter-cost: 2590 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 c ---[1994]---> Sorter-cost: 2590 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 c ---[1993]---> Sorter-cost: 2590 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 c ---[1992]---> Sorter-cost: 2590 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 c ---[1991]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[1990]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[1989]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[1988]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[1987]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[1986]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[1985]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[1984]---> Sorter-cost: 1116 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3 c ---[1983]---> Sorter-cost: 1086 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[1982]---> Sorter-cost: 1086 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[1981]---> Sorter-cost: 1086 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[1980]---> Sorter-cost: 1086 Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 c ---[1979]---> Adder-cost: 608 maxlim: 1212396 bits: 21/21 c ---[1978]---> Adder-cost: 608 maxlim: 1212396 bits: 21/21 c ---[1977]---> Adder-cost: 608 maxlim: 1212396 bits: 21/21 c ---[1976]---> Adder-cost: 608 maxlim: 1212396 bits: 21/21 c ---[1975]---> Adder-cost: 608 maxlim: 1212396 bits: 21/21 c ---[1974]---> Adder-cost: 608 maxlim: 1212396 bits: 21/21 c ---[1973]---> Adder-cost: 608 maxlim: 1212396 bits: 21/21 c ---[1972]---> Adder-cost: 608 maxlim: 1212396 bits: 21/21 c ---[1971]---> Adder-cost: 570 maxlim: 606188 bits: 20/20 c ---[1970]---> Adder-cost: 570 maxlim: 606188 bits: 20/20 c ---[1969]---> Adder-cost: 570 maxlim: 606188 bits: 20/20 c ---[1968]---> Adder-cost: 570 maxlim: 606188 bits: 20/20 c ---[1967]---> Sorter-cost:27397 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1966]---> Sorter-cost:27397 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1965]---> Sorter-cost:27454 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1964]---> Sorter-cost:27454 Base: 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1963]---> Sorter-cost: 4322 Base: 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 c ---[1962]---> Sorter-cost: 4322 Base: 2 2 2 2 2 5/oldhome/oroussel/solvers/minisat+_script: line 16: 10200 CPU time limit exceeded $XDIR/minisat+_bignum_static* "$@" #### 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.85 0.97 0.95 2/54 10195 Raw data (stat): 10195 (runsolver) R 10194 25568 25567 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 782922427 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 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+9.9998 s] Raw data (loadavg): 0.87 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+19.9999 s] Raw data (loadavg): 0.89 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+30.0001 s] Raw data (loadavg): 0.91 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+40.0002 s] Raw data (loadavg): 0.92 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+50.0003 s] Raw data (loadavg): 0.93 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+60.0009 s] Raw data (loadavg): 0.94 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+70.0006 s] Raw data (loadavg): 0.95 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+80.0008 s] Raw data (loadavg): 0.96 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+90.0009 s] Raw data (loadavg): 0.96 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+100.001 s] Raw data (loadavg): 0.97 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+110.001 s] Raw data (loadavg): 0.97 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+120.002 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+130.001 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+140.001 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+150.002 s] Raw data (loadavg): 0.98 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+160.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+170.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+180.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+190.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+200.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+210.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+220.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+230.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+240 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+250 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+260 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+270 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+280 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+290 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+299.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+309.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+319.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+329.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+340 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+349.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+360 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+370 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+380 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+389.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+400 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+409.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+419.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+429.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+439.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+449.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+459.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+469.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+479.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+489.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+499.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+509.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+519.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+529.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+539.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+549.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+559.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+569.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+579.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+589.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+599.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+610 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+619.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+629.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+639.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+649.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+659.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+669.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+679.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+689.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+699.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+709.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+719.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+729.998 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+739.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+749.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+759.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+769.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+779.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+789.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+799.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+809.999 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+820 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+830 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+840 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+850.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10200 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+860.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/58 10203 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+870.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10253 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+880.001 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10253 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+890.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10253 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+900.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10253 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+910.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10253 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+920.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10253 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+930.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+940.002 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+950.003 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+960.003 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+970.003 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+980.003 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+990.003 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1000 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1010 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1020 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1030 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1040 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1050.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1060.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1070.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1080.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1090.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1100.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1110.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1120.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1130.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1140.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1150.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1160.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1170.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10255 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1180.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10257 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1190.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10257 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1200.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10257 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1210.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10257 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1220.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10257 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1230.01 s] Raw data (loadavg): 0.99 0.97 0.95 2/55 10257 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 2128 [startup+1232.94 s] Raw data (loadavg): 0.99 0.97 0.95 1/53 10257 Raw data (stat): 10195 (minisat+_script) S 10194 25568 25567 0 -1 0 300 8598 0 0 0 0 260 27 19 0 1 0 782922427 2179072 234 4294967295 134512640 135087896 3221224544 3221223432 1074634510 0 65536 5 65538 3222414538 0 0 17 0 0 0 Raw data (statm): 532 234 485 147 0 385 0 vsize: 0 Child status: 152 Real time (s): 1232.94 CPU time (s): 1232.74 CPU user time (s): 1231.42 CPU system time (s): 1.3228 CPU usage (%): 99.984 Max. virtual memory (Kb): 2128 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####