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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-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.14
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 22141

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc24 THE 2005-04-22 02:18:50 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12049 boxname=wulflinc24 idbench=927 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4f0cac14ed3568050c2c57bb69fdb664  /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-mod010.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-mod010.opb /oldhome/oroussel/tmp/wulflinc24/normalized-mps-v2-20-10-mod010.opb
IDLAUNCH: 12049
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.080
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:        469000 kB
Buffers:         34940 kB
Cached:         506224 kB
SwapCached:        524 kB
Active:         217380 kB
Inactive:       325780 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        468748 kB
SwapTotal:     2097892 kB
SwapFree:      2096476 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            16776 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-22 02:38:53 (client local time) WITH STATUS 0 IN 1200.35 SECONDS
stats: 12049 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.72 0.91 0.89 2/54 22824
Raw data (stat): 22824 (runsolver) R 22823 28546 28545 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 550060777 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.76 0.91 0.89 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 7593 0 0 0 979 19 0 0 25 0 1 0 550060777 30363648 6500 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7413 6500 603 41 0 7372 0
vsize: 29652
[startup+20.0011 s]
Raw data (loadavg): 0.80 0.91 0.89 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 8810 0 0 0 1976 23 0 0 25 0 1 0 550060777 35385344 7717 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8639 7717 603 41 0 8598 0
vsize: 34556
[startup+30.0012 s]
Raw data (loadavg): 0.83 0.92 0.89 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 9619 0 0 0 2973 25 0 0 25 0 1 0 550060777 38678528 8526 4294967295 134512640 134672761 3221224544 3221223648 134604412 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9443 8526 603 41 0 9402 0
vsize: 37772
[startup+40.0019 s]
Raw data (loadavg): 0.85 0.92 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 10510 0 0 0 3971 27 0 0 25 0 1 0 550060777 42369024 9417 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10344 9417 603 41 0 10303 0
vsize: 41376
[startup+50.0022 s]
Raw data (loadavg): 0.87 0.92 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 11698 0 0 0 4968 31 0 0 25 0 1 0 550060777 47255552 10605 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11537 10605 603 41 0 11496 0
vsize: 46148
[startup+60.0023 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 13184 0 0 0 5964 35 0 0 25 0 1 0 550060777 53305344 12091 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13014 12091 603 41 0 12973 0
vsize: 52056
[startup+70.003 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 14440 0 0 0 6960 39 0 0 25 0 1 0 550060777 58437632 13347 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14267 13347 603 41 0 14226 0
vsize: 57068
[startup+80.0033 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 15286 0 0 0 7957 42 0 0 25 0 1 0 550060777 61882368 14193 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15108 14193 603 41 0 15067 0
vsize: 60432
[startup+90.0044 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 16803 0 0 0 8953 46 0 0 25 0 1 0 550060777 68087808 15710 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16623 15710 603 41 0 16582 0
vsize: 66492
[startup+100.005 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 17755 0 0 0 9951 48 0 0 25 0 1 0 550060777 72159232 16662 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17617 16662 603 41 0 17576 0
vsize: 70468
[startup+110.005 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 19329 0 0 0 10946 53 0 0 25 0 1 0 550060777 78573568 18236 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19183 18236 603 41 0 19142 0
vsize: 76732
[startup+120.005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 20464 0 0 0 11943 57 0 0 25 0 1 0 550060777 83161088 19371 4294967295 134512640 134672761 3221224544 3221223584 134612696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20303 19371 603 41 0 20262 0
vsize: 81212
[startup+130.005 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 21367 0 0 0 12941 58 0 0 25 0 1 0 550060777 86839296 20274 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21201 20274 603 41 0 21160 0
vsize: 84804
[startup+140.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 22306 0 0 0 13939 61 0 0 25 0 1 0 550060777 90664960 21213 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22135 21213 603 41 0 22094 0
vsize: 88540
[startup+150.005 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 23144 0 0 0 14937 64 0 0 25 0 1 0 550060777 94089216 22051 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22971 22051 603 41 0 22930 0
vsize: 91884
[startup+160.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 23902 0 0 0 15934 66 0 0 25 0 1 0 550060777 97239040 22809 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23740 22809 603 41 0 23699 0
vsize: 94960
[startup+170.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 24780 0 0 0 16932 69 0 0 25 0 1 0 550060777 100810752 23687 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24612 23687 603 41 0 24571 0
vsize: 98448
[startup+180.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 25892 0 0 0 17929 71 0 0 25 0 1 0 550060777 105402368 24799 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25733 24799 603 41 0 25692 0
vsize: 102932
[startup+190.005 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 26373 0 0 0 18928 73 0 0 25 0 1 0 550060777 107233280 25280 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26180 25280 603 41 0 26139 0
vsize: 104720
[startup+200.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 27636 0 0 0 19925 76 0 0 25 0 1 0 550060777 112476160 26543 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27460 26543 603 41 0 27419 0
vsize: 109840
[startup+210.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 28744 0 0 0 20922 79 0 0 25 0 1 0 550060777 117047296 27651 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28576 27651 603 41 0 28535 0
vsize: 114304
[startup+220.005 s]
Raw data (loadavg): 1.07 0.96 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 29438 0 0 0 21920 81 0 0 25 0 1 0 550060777 120078336 28345 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29316 28345 603 41 0 29275 0
vsize: 117264
[startup+230.005 s]
Raw data (loadavg): 1.06 0.96 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 30242 0 0 0 22918 83 0 0 25 0 1 0 550060777 123387904 29149 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30124 29149 603 41 0 30083 0
vsize: 120496
[startup+240.005 s]
Raw data (loadavg): 1.05 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 30915 0 0 0 23916 86 0 0 25 0 1 0 550060777 126156800 29822 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30800 29822 603 41 0 30759 0
vsize: 123200
[startup+250.005 s]
Raw data (loadavg): 1.04 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 31866 0 0 0 24914 88 0 0 25 0 1 0 550060777 129966080 30773 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31730 30773 603 41 0 31689 0
vsize: 126920
[startup+260.005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 33154 0 0 0 25910 92 0 0 25 0 1 0 550060777 135327744 32061 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33039 32061 603 41 0 32998 0
vsize: 132156
[startup+270.005 s]
Raw data (loadavg): 1.03 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 34353 0 0 0 26907 95 0 0 25 0 1 0 550060777 140210176 33260 4294967295 134512640 134672761 3221224544 3221223728 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34231 33260 603 41 0 34190 0
vsize: 136924
[startup+280.004 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 35666 0 0 0 27903 99 0 0 25 0 1 0 550060777 145555456 34573 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35536 34573 603 41 0 35495 0
vsize: 142144
[startup+290.005 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 37031 0 0 0 28900 102 0 0 25 0 1 0 550060777 151080960 35938 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36885 35938 603 41 0 36844 0
vsize: 147540
[startup+300.014 s]
Raw data (loadavg): 1.02 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 38255 0 0 0 29898 105 0 0 25 0 1 0 550060777 156078080 37162 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38105 37162 603 41 0 38064 0
vsize: 152420
[startup+310.016 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 39291 0 0 0 30897 108 0 0 25 0 1 0 550060777 160366592 38198 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39152 38198 603 41 0 39111 0
vsize: 156608
[startup+320.017 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 40451 0 0 0 31894 110 0 0 25 0 1 0 550060777 165109760 39358 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40310 39358 603 41 0 40269 0
vsize: 161240
[startup+330.017 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 41672 0 0 0 32892 112 0 0 25 0 1 0 550060777 170090496 40579 4294967295 134512640 134672761 3221224544 3221223584 134614171 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41526 40579 603 41 0 41485 0
vsize: 166104
[startup+340.017 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 42637 0 0 0 33890 114 0 0 25 0 1 0 550060777 174059520 41544 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42495 41544 603 41 0 42454 0
vsize: 169980
[startup+350.017 s]
Raw data (loadavg): 1.01 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 43367 0 0 0 34888 117 0 0 25 0 1 0 550060777 176979968 42274 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43208 42274 603 41 0 43167 0
vsize: 172832
[startup+360.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 43890 0 0 0 35886 119 0 0 25 0 1 0 550060777 179224576 42797 4294967295 134512640 134672761 3221224544 3221223584 134614266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43756 42797 603 41 0 43715 0
vsize: 175024
[startup+370.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 44705 0 0 0 36884 121 0 0 25 0 1 0 550060777 182505472 43612 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44557 43612 603 41 0 44516 0
vsize: 178228
[startup+380.016 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 45806 0 0 0 37882 123 0 0 25 0 1 0 550060777 186986496 44713 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45651 44713 603 41 0 45610 0
vsize: 182604
[startup+390.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 46702 0 0 0 38880 126 0 0 25 0 1 0 550060777 190676992 45609 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46552 45609 603 41 0 46511 0
vsize: 186208
[startup+400.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 48200 0 0 0 39877 129 0 0 25 0 1 0 550060777 196739072 47107 4294967295 134512640 134672761 3221224544 3221223584 134603506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48032 47107 603 41 0 47991 0
vsize: 192128
[startup+410.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 49281 0 0 0 40874 132 0 0 25 0 1 0 550060777 201236480 48188 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49130 48188 603 41 0 49089 0
vsize: 196520
[startup+420.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 50302 0 0 0 41871 135 0 0 25 0 1 0 550060777 205455360 49209 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50160 49209 603 41 0 50119 0
vsize: 200640
[startup+430.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 51276 0 0 0 42869 137 0 0 25 0 1 0 550060777 209391616 50183 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51121 50183 603 41 0 51080 0
vsize: 204484
[startup+440.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 51984 0 0 0 43867 139 0 0 25 0 1 0 550060777 212287488 50891 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51828 50891 603 41 0 51787 0
vsize: 207312
[startup+450.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 52949 0 0 0 44865 142 0 0 25 0 1 0 550060777 216240128 51856 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52793 51856 603 41 0 52752 0
vsize: 211172
[startup+460.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 53825 0 0 0 45862 145 0 0 25 0 1 0 550060777 219807744 52732 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53664 52732 603 41 0 53623 0
vsize: 214656
[startup+470.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 54610 0 0 0 46861 146 0 0 25 0 1 0 550060777 223006720 53517 4294967295 134512640 134672761 3221224544 3221223728 134616005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54445 53517 603 41 0 54404 0
vsize: 217780
[startup+480.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 55826 0 0 0 47858 149 0 0 25 0 1 0 550060777 228032512 54733 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55672 54733 603 41 0 55631 0
vsize: 222688
[startup+490.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 57276 0 0 0 48854 153 0 0 25 0 1 0 550060777 233910272 56183 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57107 56183 603 41 0 57066 0
vsize: 228428
[startup+500.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 58375 0 0 0 49852 156 0 0 25 0 1 0 550060777 238436352 57282 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58212 57282 603 41 0 58171 0
vsize: 232848
[startup+510.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 59361 0 0 0 50849 159 0 0 25 0 1 0 550060777 242475008 58268 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59198 58268 603 41 0 59157 0
vsize: 236792
[startup+520.017 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 60190 0 0 0 51847 161 0 0 25 0 1 0 550060777 245776384 59097 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60004 59097 603 41 0 59963 0
vsize: 240016
[startup+530.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 60930 0 0 0 52845 163 0 0 25 0 1 0 550060777 248807424 59837 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60744 59837 603 41 0 60703 0
vsize: 242976
[startup+540.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 61986 0 0 0 53843 165 0 0 25 0 1 0 550060777 253222912 60893 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 61822 60893 603 41 0 61781 0
vsize: 247288
[startup+550.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 62653 0 0 0 54843 166 0 0 25 0 1 0 550060777 255885312 61560 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 62472 61560 603 41 0 62431 0
vsize: 249888
[startup+560.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 63424 0 0 0 55841 168 0 0 25 0 1 0 550060777 259022848 62331 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63238 62331 603 41 0 63197 0
vsize: 252952
[startup+570.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 63998 0 0 0 56840 169 0 0 25 0 1 0 550060777 261398528 62905 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 63818 62905 603 41 0 63777 0
vsize: 255272
[startup+580.018 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 64771 0 0 0 57838 171 0 0 25 0 1 0 550060777 264577024 63678 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 64594 63678 603 41 0 64553 0
vsize: 258376
[startup+590.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 65967 0 0 0 58835 174 0 0 25 0 1 0 550060777 269406208 64874 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 65773 64874 603 41 0 65732 0
vsize: 263092
[startup+600.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 66835 0 0 0 59833 176 0 0 25 0 1 0 550060777 273461248 65742 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 66763 65742 603 41 0 66722 0
vsize: 267052
[startup+610.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 67620 0 0 0 60831 179 0 0 25 0 1 0 550060777 276725760 66527 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 67560 66527 603 41 0 67519 0
vsize: 270240
[startup+620.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 68308 0 0 0 61829 181 0 0 25 0 1 0 550060777 279613440 67215 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68265 67215 603 41 0 68224 0
vsize: 273060
[startup+630.019 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 68800 0 0 0 62829 182 0 0 25 0 1 0 550060777 281600000 67707 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 68750 67707 603 41 0 68709 0
vsize: 275000
[startup+640.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 69783 0 0 0 63827 183 0 0 25 0 1 0 550060777 285548544 68690 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 69714 68690 603 41 0 69673 0
vsize: 278856
[startup+650.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 70392 0 0 0 64826 185 0 0 25 0 1 0 550060777 288083968 69299 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 70333 69299 603 41 0 70292 0
vsize: 281332
[startup+660.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71143 0 0 0 65824 187 0 0 25 0 1 0 550060777 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+670.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71536 0 0 0 66824 187 0 0 25 0 1 0 550060777 292720640 70443 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71465 70443 603 41 0 71424 0
vsize: 285860
[startup+680.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71772 0 0 0 67823 188 0 0 25 0 1 0 550060777 294109184 70679 4294967295 134512640 134672761 3221224544 3221223600 134645408 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 71804 70679 603 41 0 71763 0
vsize: 287216
[startup+690.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 68823 188 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223536 134565076 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.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 69823 188 0 0 25 0 1 0 550060777 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+710.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 70823 188 0 0 25 0 1 0 550060777 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+720.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 71824 188 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615828 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.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 72824 188 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223680 134614701 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.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 73824 188 0 0 25 0 1 0 550060777 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+750.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 74824 188 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223536 134565045 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.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 75824 188 0 0 25 0 1 0 550060777 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+770.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 76824 189 0 0 25 0 1 0 550060777 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.021 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 77824 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223680 134614683 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.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 78825 189 0 0 25 0 1 0 550060777 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.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 79825 189 0 0 25 0 1 0 550060777 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.022 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 80825 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615739 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.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 81825 189 0 0 25 0 1 0 550060777 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.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 82825 189 0 0 25 0 1 0 550060777 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+840.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 83825 189 0 0 25 0 1 0 550060777 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.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 84825 189 0 0 25 0 1 0 550060777 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+860.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 85825 189 0 0 25 0 1 0 550060777 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+870.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 86825 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615643 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.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 87825 189 0 0 25 0 1 0 550060777 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+890.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 88826 189 0 0 25 0 1 0 550060777 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+900.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 89826 189 0 0 25 0 1 0 550060777 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+910.023 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 90826 189 0 0 25 0 1 0 550060777 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+920.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 91826 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223680 134614683 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.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 92826 189 0 0 25 0 1 0 550060777 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+940.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 93826 189 0 0 25 0 1 0 550060777 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+950.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 94827 189 0 0 25 0 1 0 550060777 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+960.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 95827 189 0 0 25 0 1 0 550060777 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+970.024 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 96827 189 0 0 25 0 1 0 550060777 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+980.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 97827 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615673 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.025 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 98827 189 0 0 25 0 1 0 550060777 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+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 99827 189 0 0 25 0 1 0 550060777 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.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 100828 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615929 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.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 101828 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616373 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.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 102828 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134614256 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 103828 189 0 0 25 0 1 0 550060777 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+1050.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 104828 189 0 0 25 0 1 0 550060777 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+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 105829 189 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615549 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 106829 190 0 0 25 0 1 0 550060777 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+1080.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 107829 190 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615767 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 108829 190 0 0 25 0 1 0 550060777 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+1100.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 109829 190 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616178 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 110830 190 0 0 25 0 1 0 550060777 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+1120.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 111830 190 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616339 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 112830 190 0 0 25 0 1 0 550060777 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+1140.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 113830 190 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615663 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 114830 190 0 0 25 0 1 0 550060777 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+1160.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 115830 190 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223680 134614701 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 116831 190 0 0 25 0 1 0 550060777 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615652 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.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 117831 190 0 0 25 0 1 0 550060777 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+1190.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 118831 190 0 0 25 0 1 0 550060777 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+1200.03 s]
Raw data (loadavg): 1.00 0.97 0.91 2/54 22824
Raw data (stat): 22824 (minisat+) R 22823 28546 28545 0 -1 0 71891 0 0 0 119831 190 0 0 25 0 1 0 550060777 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
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.97 0.91 1/54 22824
Raw data (stat): 22824 (minisat+) Z 22823 28546 28545 0 -1 12 71891 0 0 0 119831 203 0 0 25 0 1 0 550060777 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.17
CPU time (s): 1200.35
CPU user time (s): 1198.32
CPU system time (s): 2.03669
CPU usage (%): 100.016
Max. virtual memory (Kb): 287216
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####