PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib/normalized-mps-v2-13-7-mod010.opb
MD5SUM	4f0cac14ed3568050c2c57bb69fdb664
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	6571
Optimality of the best value was proved	NO
Number of terms in the objective function	2655
Biggest coefficient in the objective function	266
Number of bits for the biggest coefficient in the objective function	9
Sum of the numbers in the objective function	489211
Number of bits of the sum of numbers in the objective function	19
Biggest number in a constraint	266
Number of bits of the biggest number in a constraint	9
Biggest sum of numbers in a constraint	489211
Number of bits of the biggest sum of numbers	19
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1175.78
Number of variables	2655
Total number of constraints	2801
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	2800
Number of constraints which are nor clauses,nor cardinality constraints	1
Minimum length of a constraint	1
Maximum length of a constraint	2655
Trace number 19101

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 17:48:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17041 boxname=wulflinc12 idbench=1311 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-mod010.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 17041
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        756640 kB
Buffers:         29148 kB
Cached:         227724 kB
SwapCached:        508 kB
Active:          58460 kB
Inactive:       200528 kB
HighTotal:      131008 kB
HighFree:        15036 kB
LowTotal:       903652 kB
LowFree:        741604 kB
SwapTotal:     2097136 kB
SwapFree:      2095888 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5276 kB
Slab:            13588 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 18:08:26 (client local time) WITH STATUS 0 IN 1200.35 SECONDS
stats: 17041 7 1200.35 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 291 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################################################################################################################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 289]---> BDD-cost:   67
c ---[ 287]---> BDD-cost:  113
c ---[ 285]---> BDD-cost:  181
c ---[ 283]---> BDD-cost:  115
c ---[ 281]---> BDD-cost:   69
c ---[ 279]---> BDD-cost:  125
c ---[ 277]---> BDD-cost:  155
c ---[ 275]---> BDD-cost:   87
c ---[ 273]---> BDD-cost:   97
c ---[ 271]---> BDD-cost:   73
c ---[ 269]---> BDD-cost:  119
c ---[ 267]---> BDD-cost:   45
c ---[ 265]---> BDD-cost:  171
c ---[ 263]---> BDD-cost:  111
c ---[ 261]---> BDD-cost:  149
c ---[ 259]---> BDD-cost:  195
c ---[ 257]---> BDD-cost:  131
c ---[ 255]---> BDD-cost:  123
c ---[ 253]---> BDD-cost:  167
c ---[ 251]---> BDD-cost:  101
c ---[ 249]---> BDD-cost:   97
c ---[ 247]---> BDD-cost:   23
c ---[ 245]---> BDD-cost:  135
c ---[ 243]---> BDD-cost:   59
c ---[ 241]---> BDD-cost:   95
c ---[ 239]---> BDD-cost:   59
c ---[ 237]---> BDD-cost:  133
c ---[ 235]---> BDD-cost:   99
c ---[ 233]---> BDD-cost:  179
c ---[ 231]---> BDD-cost:  111
c ---[ 229]---> BDD-cost:   23
c ---[ 227]---> BDD-cost:   89
c ---[ 225]---> BDD-cost:   95
c ---[ 223]---> BDD-cost:  117
c ---[ 221]---> BDD-cost:   23
c ---[ 219]---> BDD-cost:   51
c ---[ 217]---> BDD-cost:  311
c ---[ 215]---> BDD-cost:  259
c ---[ 213]---> BDD-cost:  169
c ---[ 211]---> BDD-cost:  131
c ---[ 209]---> BDD-cost:  155
c ---[ 207]---> BDD-cost:   89
c ---[ 205]---> BDD-cost:   51
c ---[ 203]---> BDD-cost:  165
c ---[ 201]---> BDD-cost:   75
c ---[ 199]---> BDD-cost:  139
c ---[ 197]---> BDD-cost:   67
c ---[ 195]---> BDD-cost:  173
c ---[ 193]---> BDD-cost:  235
c ---[ 191]---> BDD-cost:  185
c ---[ 189]---> BDD-cost:  127
c ---[ 187]---> BDD-cost:   37
c ---[ 185]---> BDD-cost:   37
c ---[ 183]---> BDD-cost:   91
c ---[ 181]---> BDD-cost:   77
c ---[ 179]---> BDD-cost:   29
c ---[ 177]---> BDD-cost:   77
c ---[ 175]---> BDD-cost:   77
c ---[ 173]---> BDD-cost:  101
c ---[ 171]---> BDD-cost:  131
c ---[ 169]---> BDD-cost:  155
c ---[ 167]---> BDD-cost:  177
c ---[ 165]---> BDD-cost:  143
c ---[ 163]---> BDD-cost:   93
c ---[ 161]---> BDD-cost:   79
c ---[ 159]---> BDD-cost:   53
c ---[ 157]---> BDD-cost:   71
c ---[ 155]---> BDD-cost:  127
c ---[ 153]---> BDD-cost:  127
c ---[ 151]---> BDD-cost:   67
c ---[ 149]---> BDD-cost:   83
c ---[ 147]---> BDD-cost:   47
c ---[ 145]---> BDD-cost:   63
c ---[ 143]---> BDD-cost:  121
c ---[ 141]---> BDD-cost:  155
c ---[ 139]---> BDD-cost:   87
c ---[ 137]---> BDD-cost:   91
c ---[ 135]---> BDD-cost:   47
c ---[ 133]---> BDD-cost:   67
c ---[ 131]---> BDD-cost:   33
c ---[ 129]---> BDD-cost:   91
c ---[ 127]---> BDD-cost:   69
c ---[ 125]---> BDD-cost:    5
c ---[ 123]---> BDD-cost:   47
c ---[ 121]---> BDD-cost:   45
c ---[ 119]---> BDD-cost:   37
c ---[ 117]---> BDD-cost:  117
c ---[ 115]---> BDD-cost:   97
c ---[ 113]---> BDD-cost:   77
c ---[ 111]---> BDD-cost:   97
c ---[ 109]---> BDD-cost:  137
c ---[ 107]---> BDD-cost:  125
c ---[ 105]---> BDD-cost:   79
c ---[ 103]---> BDD-cost:  133
c ---[ 101]---> BDD-cost:  153
c ---[  99]---> BDD-cost:  139
c ---[  97]---> BDD-cost:  125
c ---[  95]---> BDD-cost:    5
c ---[  93]---> BDD-cost:   73
c ---[  91]---> BDD-cost:  157
c ---[  89]---> BDD-cost:  127
c ---[  87]---> BDD-cost:  199
c ---[  85]---> BDD-cost:  121
c ---[  83]---> BDD-cost:  107
c ---[  81]---> BDD-cost:  169
c ---[  79]---> BDD-cost:  113
c ---[  77]---> BDD-cost:  103
c ---[  75]---> BDD-cost:   75
c ---[  73]---> BDD-cost:   97
c ---[  71]---> BDD-cost:  151
c ---[  69]---> BDD-cost:  199
c ---[  67]---> BDD-cost:  109
c ---[  65]---> BDD-cost:  131
c ---[  63]---> BDD-cost:  113
c ---[  61]---> BDD-cost:  173
c ---[  59]---> BDD-cost:  119
c ---[  57]---> BDD-cost:  173
c ---[  55]---> BDD-cost:  119
c ---[  53]---> BDD-cost:   71
c ---[  51]---> BDD-cost:  179
c ---[  49]---> BDD-cost:  241
c ---[  47]---> BDD-cost:  201
c ---[  45]---> BDD-cost:  173
c ---[  43]---> BDD-cost:  147
c ---[  41]---> BDD-cost:  157
c ---[  39]---> BDD-cost:  201
c ---[  37]---> BDD-cost:  129
c ---[  35]---> BDD-cost:  117
c ---[  33]---> BDD-cost:  177
c ---[  31]---> BDD-cost:  123
c ---[  29]---> BDD-cost:  131
c ---[  27]---> BDD-cost:  115
c ---[  25]---> BDD-cost:   51
c ---[  23]---> BDD-cost:  123
c ---[  21]---> BDD-cost:   55
c ---[  19]---> BDD-cost:    5
c ---[  17]---> BDD-cost:   99
c ---[  15]---> BDD-cost:   85
c ---[  13]---> BDD-cost:  109
c ---[  11]---> BDD-cost:  153
c ---[   9]---> BDD-cost:  201
c ---[   7]---> BDD-cost:  133
c ---[   5]---> BDD-cost:  121
c ---[   3]---> BDD-cost:  171
c ---[   1]---> Adder-cost: 5294   maxlim: 2609   bits: 12/12
c ---[   0]---> BDD-cost:  751
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   79345   242433 |   23803       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24557          
c   -- var.elim.:  2000/24557          
c   -- var.elim.:  3000/24557          
c   -- var.elim.:  4000/24557          
c   -- var.elim.:  5000/24557          
c   -- var.elim.:  6000/24557          
c   -- var.elim.:  7000/24557          
c   -- var.elim.:  8000/24557          
c   -- var.elim.:  9000/24557          
c   -- var.elim.:  10000/24557          
c   -- var.elim.:  11000/24557          
c   -- var.elim.:  12000/24557          
c   -- var.elim.:  13000/24557          
c   -- var.elim.:  14000/24557          
c   -- var.elim.:  15000/24557          
c   -- var.elim.:  16000/24557          
c   -- var.elim.:  17000/24557          
c   -- var.elim.:  18000/24557          
c   -- var.elim.:  19000/24557          
c   -- var.elim.:  20000/24557          
c   -- var.elim.:  21000/24557          
c   -- var.elim.:  22000/24557          
c   -- var.elim.:  23000/24557          
c   -- var.elim.:  24000/24557          
c   -- var.elim.:  24557/24557          
c   -- var.elim.:  1000/1319          
c   -- var.elim.:  1319/1319          
c   -- subsuming                       
c   -- var.elim.:  800/800          
c   -- var.elim.:  521/521          
c   -- subsuming                       
c   -- var.elim.:  404/404          
c |         0 |   77662   236266 |      --       0       --      -- |     --   | -1623/-5431
c |         0 |   77662   236266 |   31064       0        0     nan |  0.000 % |
c |       100 |   77662   236266 |   34171     100     1478    14.8 |  1.152 % |
c |       250 |   77662   236266 |   37588     250    15746    63.0 |  1.152 % |
c |       479 |   77662   236266 |   41347     479    29944    62.5 |  1.152 % |
c |       817 |   77662   236266 |   45481     817    34358    42.1 |  1.152 % |
c |      1325 |   77662   236266 |   50030    1325   108050    81.5 |  1.152 % |
c |      2085 |   77662   236266 |   55033    2085   218520   104.8 |  1.152 % |
c |      3224 |   77662   236266 |   60536    3224   620750   192.5 |  1.152 % |
c |      4932 |   77662   236266 |   66590    4932  1154502   234.1 |  1.152 % |
c |      7494 |   77662   236266 |   73249    7494  1593540   212.6 |  1.152 % |
c |     11339 |   77646   236208 |   80557   11327  2172565   191.8 |  1.156 % |
c |     17108 |   77646   236208 |   88613   17096  3462215   202.5 |  1.156 % |
c |     25760 |   77646   236208 |   97474   25748  7101412   275.8 |  1.156 % |
c |     38736 |   77646   236208 |  107222   38724 12654935   326.8 |  1.156 % |
c |     58197 |   77634   236163 |  117925   58168 18476828   317.6 |  1.160 % |
c |     87390 |   77615   236088 |  129686   87351 33733879   386.2 |  1.177 % |
c |    131181 |   77615   236088 |  142655  131142 58172080   443.6 |  1.177 % |
c |    196865 |   77547   235804 |  156783   75294 41748380   554.5 |  1.198 % |
c 
c *** TERMINATE#### 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.84 0.94 0.90 2/54 32550
Raw data (stat): 32550 (runsolver) R 32549 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 488776101 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.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 7615 0 0 0 979 19 0 0 25 0 1 0 488776101 30494720 6522 4294967295 134512640 134672761 3221224544 3221223536 134565149 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7445 6522 603 41 0 7404 0
vsize: 29780
[startup+20.0016 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 8812 0 0 0 1975 22 0 0 25 0 1 0 488776101 35385344 7719 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8639 7719 603 41 0 8598 0
vsize: 34556
[startup+30.0024 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 9651 0 0 0 2974 24 0 0 25 0 1 0 488776101 38809600 8558 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9475 8558 603 41 0 9434 0
vsize: 37900
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 10618 0 0 0 3971 27 0 0 25 0 1 0 488776101 42881024 9525 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10469 9525 603 41 0 10428 0
vsize: 41876
[startup+50.002 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 11901 0 0 0 4968 29 0 0 25 0 1 0 488776101 48050176 10808 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11731 10808 603 41 0 11690 0
vsize: 46924
[startup+60.0029 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 13463 0 0 0 5965 33 0 0 25 0 1 0 488776101 54493184 12370 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13304 12370 603 41 0 13263 0
vsize: 53216
[startup+70.0034 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 14593 0 0 0 6963 36 0 0 25 0 1 0 488776101 59105280 13500 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14430 13500 603 41 0 14389 0
vsize: 57720
[startup+80.0046 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 15636 0 0 0 7960 38 0 0 25 0 1 0 488776101 63352832 14543 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15467 14543 603 41 0 15426 0
vsize: 61868
[startup+90.0044 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 17143 0 0 0 8957 42 0 0 25 0 1 0 488776101 69521408 16050 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16973 16050 603 41 0 16932 0
vsize: 67892
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 18239 0 0 0 9955 44 0 0 25 0 1 0 488776101 74129408 17146 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18098 17146 603 41 0 18057 0
vsize: 72392
[startup+110.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 19832 0 0 0 10952 47 0 0 25 0 1 0 488776101 80539648 18739 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19663 18739 603 41 0 19622 0
vsize: 78652
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 20757 0 0 0 11950 49 0 0 25 0 1 0 488776101 84344832 19664 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20592 19664 603 41 0 20551 0
vsize: 82368
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 21798 0 0 0 12947 53 0 0 25 0 1 0 488776101 88686592 20705 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21652 20705 603 41 0 21611 0
vsize: 86608
[startup+140.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 22738 0 0 0 13945 55 0 0 25 0 1 0 488776101 92520448 21645 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22588 21645 603 41 0 22547 0
vsize: 90352
[startup+150.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 23449 0 0 0 14943 57 0 0 25 0 1 0 488776101 95420416 22356 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23296 22356 603 41 0 23255 0
vsize: 93184
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 24297 0 0 0 15941 59 0 0 25 0 1 0 488776101 98828288 23204 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24128 23204 603 41 0 24087 0
vsize: 96512
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 25393 0 0 0 16938 62 0 0 25 0 1 0 488776101 103297024 24300 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25219 24300 603 41 0 25178 0
vsize: 100876
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 26268 0 0 0 17936 64 0 0 25 0 1 0 488776101 106835968 25175 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26083 25175 603 41 0 26042 0
vsize: 104332
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 27005 0 0 0 18935 65 0 0 25 0 1 0 488776101 109858816 25912 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26821 25912 603 41 0 26780 0
vsize: 107284
[startup+200.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 28504 0 0 0 19934 67 0 0 25 0 1 0 488776101 115990528 27411 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28318 27411 603 41 0 28277 0
vsize: 113272
[startup+210.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 29268 0 0 0 20932 70 0 0 25 0 1 0 488776101 119148544 28175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29089 28175 603 41 0 29048 0
vsize: 116356
[startup+220.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 29984 0 0 0 21930 71 0 0 25 0 1 0 488776101 122327040 28891 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29865 28891 603 41 0 29824 0
vsize: 119460
[startup+230.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 30821 0 0 0 22928 74 0 0 25 0 1 0 488776101 125763584 29728 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30704 29728 603 41 0 30663 0
vsize: 122816
[startup+240.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 31619 0 0 0 23926 76 0 0 25 0 1 0 488776101 129048576 30526 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31506 30526 603 41 0 31465 0
vsize: 126024
[startup+250.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 32794 0 0 0 24923 79 0 0 25 0 1 0 488776101 133775360 31701 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32660 31701 603 41 0 32619 0
vsize: 130640
[startup+260.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 34125 0 0 0 25920 82 0 0 25 0 1 0 488776101 139276288 33032 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34003 33032 603 41 0 33962 0
vsize: 136012
[startup+270.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 35475 0 0 0 26917 85 0 0 25 0 1 0 488776101 144756736 34382 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35341 34382 603 41 0 35300 0
vsize: 141364
[startup+280.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 36863 0 0 0 27914 89 0 0 25 0 1 0 488776101 150421504 35770 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36724 35770 603 41 0 36683 0
vsize: 146896
[startup+290.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 38135 0 0 0 28911 92 0 0 25 0 1 0 488776101 155684864 37042 4294967295 134512640 134672761 3221224544 3221223552 134522549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38009 37042 603 41 0 37968 0
vsize: 152036
[startup+300.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 39221 0 0 0 29909 94 0 0 25 0 1 0 488776101 160100352 38128 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39087 38128 603 41 0 39046 0
vsize: 156348
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 40405 0 0 0 30906 97 0 0 25 0 1 0 488776101 164978688 39312 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40278 39312 603 41 0 40237 0
vsize: 161112
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 41646 0 0 0 31903 101 0 0 25 0 1 0 488776101 169963520 40553 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41495 40553 603 41 0 41454 0
vsize: 165980
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 42659 0 0 0 32901 103 0 0 25 0 1 0 488776101 174182400 41566 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42525 41566 603 41 0 42484 0
vsize: 170100
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 43397 0 0 0 33899 105 0 0 25 0 1 0 488776101 177115136 42304 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43241 42304 603 41 0 43200 0
vsize: 172964
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 43970 0 0 0 34898 106 0 0 25 0 1 0 488776101 179486720 42877 4294967295 134512640 134672761 3221224544 3221223728 134615767 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43820 42877 603 41 0 43779 0
vsize: 175280
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 44780 0 0 0 35896 108 0 0 25 0 1 0 488776101 182771712 43687 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44622 43687 603 41 0 44581 0
vsize: 178488
[startup+370.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 45982 0 0 0 36893 111 0 0 25 0 1 0 488776101 187777024 44889 4294967295 134512640 134672761 3221224544 3221223728 134615749 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45844 44889 603 41 0 45803 0
vsize: 183376
[startup+380.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 46969 0 0 0 37892 113 0 0 25 0 1 0 488776101 191725568 45876 4294967295 134512640 134672761 3221224544 3221223744 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46808 45876 603 41 0 46767 0
vsize: 187232
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 48405 0 0 0 38889 116 0 0 25 0 1 0 488776101 197668864 47312 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48259 47312 603 41 0 48218 0
vsize: 193036
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 49488 0 0 0 39887 118 0 0 25 0 1 0 488776101 202027008 48395 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49323 48395 603 41 0 49282 0
vsize: 197292
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 50561 0 0 0 40885 120 0 0 25 0 1 0 488776101 206491648 49468 4294967295 134512640 134672761 3221224544 3221223744 134610669 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50413 49468 603 41 0 50372 0
vsize: 201652
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 51474 0 0 0 41883 123 0 0 25 0 1 0 488776101 210186240 50381 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51315 50381 603 41 0 51274 0
vsize: 205260
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 52295 0 0 0 42881 125 0 0 25 0 1 0 488776101 213471232 51202 4294967295 134512640 134672761 3221224544 3221223584 134613118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52117 51202 603 41 0 52076 0
vsize: 208468
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 53282 0 0 0 43879 127 0 0 25 0 1 0 488776101 217579520 52189 4294967295 134512640 134672761 3221224544 3221223584 134612614 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53120 52189 603 41 0 53079 0
vsize: 212480
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 54078 0 0 0 44876 130 0 0 25 0 1 0 488776101 220880896 52985 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53926 52985 603 41 0 53885 0
vsize: 215704
[startup+460.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 54960 0 0 0 45875 131 0 0 25 0 1 0 488776101 224444416 53867 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54796 53867 603 41 0 54755 0
vsize: 219184
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 56512 0 0 0 46871 135 0 0 25 0 1 0 488776101 230731776 55419 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56331 55419 603 41 0 56290 0
vsize: 225324
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 57875 0 0 0 47869 138 0 0 25 0 1 0 488776101 236331008 56782 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57698 56782 603 41 0 57657 0
vsize: 230792
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 58881 0 0 0 48867 140 0 0 25 0 1 0 488776101 240537600 57788 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58725 57788 603 41 0 58684 0
vsize: 234900
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 59863 0 0 0 49865 142 0 0 25 0 1 0 488776101 244457472 58770 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59682 58770 603 41 0 59641 0
vsize: 238728
[startup+510.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 60515 0 0 0 50864 144 0 0 25 0 1 0 488776101 247218176 59422 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60356 59422 603 41 0 60315 0
vsize: 241424
[startup+520.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 61593 0 0 0 51861 147 0 0 25 0 1 0 488776101 251555840 60500 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61415 60500 603 41 0 61374 0
vsize: 245660
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 62464 0 0 0 52859 148 0 0 25 0 1 0 488776101 255082496 61371 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62276 61371 603 41 0 62235 0
vsize: 249104
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 63168 0 0 0 53858 150 0 0 25 0 1 0 488776101 257978368 62075 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62983 62075 603 41 0 62942 0
vsize: 251932
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 63842 0 0 0 54857 151 0 0 25 0 1 0 488776101 260743168 62749 4294967295 134512640 134672761 3221224544 3221223584 134612653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63658 62749 603 41 0 63617 0
vsize: 254632
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 64548 0 0 0 55855 153 0 0 25 0 1 0 488776101 263655424 63455 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64369 63455 603 41 0 64328 0
vsize: 257476
[startup+570.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 65775 0 0 0 56853 156 0 0 25 0 1 0 488776101 268623872 64682 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65582 64682 603 41 0 65541 0
vsize: 262328
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 66666 0 0 0 57850 159 0 0 25 0 1 0 488776101 272801792 65573 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66602 65573 603 41 0 66561 0
vsize: 266408
[startup+590.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 67510 0 0 0 58848 161 0 0 25 0 1 0 488776101 276328448 66417 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67463 66417 603 41 0 67422 0
vsize: 269852
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 68180 0 0 0 59847 162 0 0 25 0 1 0 488776101 279085056 67087 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68136 67087 603 41 0 68095 0
vsize: 272544
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 68672 0 0 0 60845 164 0 0 25 0 1 0 488776101 281071616 67579 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68621 67579 603 41 0 68580 0
vsize: 274484
[startup+620.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 69731 0 0 0 61843 166 0 0 25 0 1 0 488776101 285417472 68638 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69682 68638 603 41 0 69641 0
vsize: 278728
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 70367 0 0 0 62842 167 0 0 25 0 1 0 488776101 287952896 69274 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70301 69274 603 41 0 70260 0
vsize: 281204
[startup+640.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71143 0 0 0 63840 169 0 0 25 0 1 0 488776101 291127296 70050 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71076 70050 603 41 0 71035 0
vsize: 284304
[startup+650.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71540 0 0 0 64839 170 0 0 25 0 1 0 488776101 292720640 70447 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71465 70447 603 41 0 71424 0
vsize: 285860
[startup+660.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71772 0 0 0 65839 171 0 0 25 0 1 0 488776101 294109184 70679 4294967295 134512640 134672761 3221224544 3221222976 134645502 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71804 70679 603 41 0 71763 0
vsize: 287216
[startup+670.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 66839 171 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 67839 171 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 32550
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 68839 171 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+700.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 32551
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 69840 171 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+710.029 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 32603
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 70819 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223744 134610644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+720.029 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 32603
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 71819 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+730.03 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 32603
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 72819 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+740.031 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 32603
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 73820 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+750.031 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32603
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 74820 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+760.031 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 32603
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 75820 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+770.032 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32603
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 76820 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+780.033 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 77820 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+790.033 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 78821 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+800.033 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 79821 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+810.034 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 80821 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+820.035 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 81821 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+830.036 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 82821 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+840.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 83822 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+850.036 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 84822 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+860.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 85822 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+870.037 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 86822 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+880.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 87823 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+890.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 88823 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+900.038 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 89823 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+910.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 90823 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+920.039 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 91823 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+930.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 92823 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+940.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 93824 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+950.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 94824 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+960.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 95824 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+970.041 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 96824 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+980.042 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 97824 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+990.043 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 98825 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616320 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1000.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 99825 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1010.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 100825 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612684 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1020.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 101826 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223744 134610602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1030.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32605
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 102826 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1040.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 103826 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1050.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 104826 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1060.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 105827 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1070.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 106827 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1080.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 107827 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1090.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 108827 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1100.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 109827 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1110.05 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 110828 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1120.05 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 111828 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616286 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1130.05 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 112828 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1140.06 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 113828 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223680 134614670 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1150.06 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 114828 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1160.06 s]
Raw data (loadavg): 1.03 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 115829 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1170.06 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 116829 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1180.06 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 117829 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1190.06 s]
Raw data (loadavg): 1.02 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 118829 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616366 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1200.06 s]
Raw data (loadavg): 1.01 1.00 0.92 2/54 32607
Raw data (stat): 32550 (minisat+) R 32549 25285 25284 0 -1 0 71891 0 0 0 119830 191 0 0 25 0 1 0 488776101 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.19 s]
Raw data (loadavg): 1.01 1.00 0.92 1/54 32607
Raw data (stat): 32550 (minisat+) Z 32549 25285 25284 0 -1 12 71891 0 0 0 119830 204 0 0 25 0 1 0 488776101 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.19
CPU time (s): 1200.35
CPU user time (s): 1198.3
CPU system time (s): 2.04569
CPU usage (%): 100.013
Max. virtual memory (Kb): 287216
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####