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/miplib3/normalized-mps-v2-13-7-mod010.opb
MD5SUM	ef7064a9be2b712276f7b600af28e2b0
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.18
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 18062

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 13:18:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18640 boxname=wulflinc23 idbench=1434 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ef7064a9be2b712276f7b600af28e2b0  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-mod010.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-mod010.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-mod010.opb
IDLAUNCH: 18640
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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.037
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:        205840 kB
Buffers:         31504 kB
Cached:         769044 kB
SwapCached:        492 kB
Active:         390396 kB
Inactive:       412252 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        205588 kB
SwapTotal:     2097136 kB
SwapFree:      2095852 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5224 kB
Slab:            20592 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:38:21 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 18640 7 1200.24 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.50 0.79 0.85 2/54 5698
Raw data (stat): 5698 (runsolver) R 5697 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545379859 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.57 0.80 0.85 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 7601 0 0 0 982 16 0 0 25 0 1 0 545379859 30363648 6508 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7413 6508 603 41 0 7372 0
vsize: 29652
[startup+20.0015 s]
Raw data (loadavg): 0.64 0.81 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 8810 0 0 0 1980 19 0 0 25 0 1 0 545379859 35385344 7717 4294967295 134512640 134672761 3221224544 3221223688 134616373 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.0016 s]
Raw data (loadavg): 0.69 0.81 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 9617 0 0 0 2978 21 0 0 25 0 1 0 545379859 38678528 8524 4294967295 134512640 134672761 3221224544 3221223728 134615560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9443 8524 603 41 0 9402 0
vsize: 37772
[startup+40.0016 s]
Raw data (loadavg): 0.74 0.82 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 10499 0 0 0 3976 23 0 0 25 0 1 0 545379859 42229760 9406 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10310 9406 603 41 0 10269 0
vsize: 41240
[startup+50.0021 s]
Raw data (loadavg): 0.78 0.82 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 11675 0 0 0 4973 26 0 0 25 0 1 0 545379859 47124480 10582 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11505 10582 603 41 0 11464 0
vsize: 46020
[startup+60.0025 s]
Raw data (loadavg): 0.81 0.83 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 13150 0 0 0 5969 30 0 0 25 0 1 0 545379859 53174272 12057 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12982 12057 603 41 0 12941 0
vsize: 51928
[startup+70.0025 s]
Raw data (loadavg): 0.84 0.83 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 14415 0 0 0 6966 34 0 0 25 0 1 0 545379859 58306560 13322 4294967295 134512640 134672761 3221224544 3221223728 134615683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14235 13322 603 41 0 14194 0
vsize: 56940
[startup+80.0033 s]
Raw data (loadavg): 0.87 0.84 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 15259 0 0 0 7963 36 0 0 25 0 1 0 545379859 61751296 14166 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15076 14166 603 41 0 15035 0
vsize: 60304
[startup+90.0035 s]
Raw data (loadavg): 0.89 0.84 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 16768 0 0 0 8960 40 0 0 25 0 1 0 545379859 67960832 15675 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16592 15675 603 41 0 16551 0
vsize: 66368
[startup+100.003 s]
Raw data (loadavg): 0.90 0.85 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 17684 0 0 0 9959 42 0 0 25 0 1 0 545379859 71766016 16591 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17521 16591 603 41 0 17480 0
vsize: 70084
[startup+110.004 s]
Raw data (loadavg): 0.92 0.85 0.86 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 19284 0 0 0 10955 46 0 0 25 0 1 0 545379859 78315520 18191 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19120 18191 603 41 0 19079 0
vsize: 76480
[startup+120.003 s]
Raw data (loadavg): 0.93 0.86 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 20393 0 0 0 11952 49 0 0 25 0 1 0 545379859 82903040 19300 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20240 19300 603 41 0 20199 0
vsize: 80960
[startup+130.004 s]
Raw data (loadavg): 0.94 0.86 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 21347 0 0 0 12949 52 0 0 25 0 1 0 545379859 86839296 20254 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21201 20254 603 41 0 21160 0
vsize: 84804
[startup+140.005 s]
Raw data (loadavg): 0.95 0.87 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 22218 0 0 0 13947 54 0 0 25 0 1 0 545379859 90267648 21125 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22038 21125 603 41 0 21997 0
vsize: 88152
[startup+150.004 s]
Raw data (loadavg): 0.96 0.87 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 23144 0 0 0 14946 56 0 0 25 0 1 0 545379859 94089216 22051 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22971 22051 603 41 0 22930 0
vsize: 91884
[startup+160.004 s]
Raw data (loadavg): 0.96 0.87 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 23776 0 0 0 15944 57 0 0 25 0 1 0 545379859 96751616 22683 4294967295 134512640 134672761 3221224544 3221223728 134615679 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23621 22683 603 41 0 23580 0
vsize: 94484
[startup+170.005 s]
Raw data (loadavg): 0.97 0.88 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 24696 0 0 0 16942 60 0 0 25 0 1 0 545379859 100413440 23603 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24515 23603 603 41 0 24474 0
vsize: 98060
[startup+180.006 s]
Raw data (loadavg): 0.97 0.88 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 25730 0 0 0 17939 62 0 0 25 0 1 0 545379859 104734720 24637 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25570 24637 603 41 0 25529 0
vsize: 102280
[startup+190.006 s]
Raw data (loadavg): 0.98 0.88 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 26289 0 0 0 18938 64 0 0 25 0 1 0 545379859 106967040 25196 4294967295 134512640 134672761 3221224544 3221223680 134614739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26115 25196 603 41 0 26074 0
vsize: 104460
[startup+200.006 s]
Raw data (loadavg): 0.98 0.89 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 27324 0 0 0 19936 67 0 0 25 0 1 0 545379859 111165440 26231 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27140 26231 603 41 0 27099 0
vsize: 108560
[startup+210.006 s]
Raw data (loadavg): 0.98 0.89 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 28581 0 0 0 20933 70 0 0 25 0 1 0 545379859 116383744 27488 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28414 27488 603 41 0 28373 0
vsize: 113656
[startup+220.006 s]
Raw data (loadavg): 0.98 0.89 0.87 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 29314 0 0 0 21931 72 0 0 25 0 1 0 545379859 119545856 28221 4294967295 134512640 134672761 3221224544 3221223584 134614258 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29186 28221 603 41 0 29145 0
vsize: 116744
[startup+230.007 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 30026 0 0 0 22929 74 0 0 25 0 1 0 545379859 122458112 28933 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29897 28933 603 41 0 29856 0
vsize: 119588
[startup+240.006 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 30829 0 0 0 23927 76 0 0 25 0 1 0 545379859 125763584 29736 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30704 29736 603 41 0 30663 0
vsize: 122816
[startup+250.006 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 31593 0 0 0 24925 79 0 0 25 0 1 0 545379859 128917504 30500 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31474 30500 603 41 0 31433 0
vsize: 125896
[startup+260.007 s]
Raw data (loadavg): 0.99 0.90 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 32689 0 0 0 25922 82 0 0 25 0 1 0 545379859 133394432 31596 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32567 31596 603 41 0 32526 0
vsize: 130268
[startup+270.007 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 33990 0 0 0 26919 85 0 0 25 0 1 0 545379859 138629120 32897 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33845 32897 603 41 0 33804 0
vsize: 135380
[startup+280.008 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 35238 0 0 0 27916 88 0 0 25 0 1 0 545379859 143843328 34145 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35118 34145 603 41 0 35077 0
vsize: 140472
[startup+290.009 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 36562 0 0 0 28913 91 0 0 25 0 1 0 545379859 149237760 35469 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36435 35469 603 41 0 36394 0
vsize: 145740
[startup+300.008 s]
Raw data (loadavg): 0.99 0.91 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 37761 0 0 0 29911 94 0 0 25 0 1 0 545379859 154112000 36668 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37625 36668 603 41 0 37584 0
vsize: 150500
[startup+310.009 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 38899 0 0 0 30908 97 0 0 25 0 1 0 545379859 158806016 37806 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38771 37806 603 41 0 38730 0
vsize: 155084
[startup+320.009 s]
Raw data (loadavg): 0.99 0.92 0.88 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 39996 0 0 0 31905 100 0 0 25 0 1 0 545379859 163266560 38903 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39860 38903 603 41 0 39819 0
vsize: 159440
[startup+330.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 41144 0 0 0 32903 102 0 0 25 0 1 0 545379859 167989248 40051 4294967295 134512640 134672761 3221224544 3221223584 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41013 40051 603 41 0 40972 0
vsize: 164052
[startup+340.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 42149 0 0 0 33901 104 0 0 25 0 1 0 545379859 172081152 41056 4294967295 134512640 134672761 3221224544 3221223584 134603512 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42012 41056 603 41 0 41971 0
vsize: 168048
[startup+350.009 s]
Raw data (loadavg): 0.99 0.92 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 43031 0 0 0 34900 105 0 0 25 0 1 0 545379859 175648768 41938 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42883 41938 603 41 0 42842 0
vsize: 171532
[startup+360.009 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 43624 0 0 0 35899 107 0 0 25 0 1 0 545379859 178036736 42531 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43466 42531 603 41 0 43425 0
vsize: 173864
[startup+370.009 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 44342 0 0 0 36896 109 0 0 25 0 1 0 545379859 181067776 43249 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44206 43249 603 41 0 44165 0
vsize: 176824
[startup+380.01 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 45039 0 0 0 37895 111 0 0 25 0 1 0 545379859 183836672 43946 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44882 43946 603 41 0 44841 0
vsize: 179528
[startup+390.01 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 46355 0 0 0 38892 114 0 0 25 0 1 0 545379859 189222912 45262 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46197 45262 603 41 0 46156 0
vsize: 184788
[startup+400.01 s]
Raw data (loadavg): 0.99 0.93 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 47560 0 0 0 39888 117 0 0 25 0 1 0 545379859 194134016 46467 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47396 46467 603 41 0 47355 0
vsize: 189584
[startup+410.01 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 48665 0 0 0 40886 120 0 0 25 0 1 0 545379859 198733824 47572 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48519 47572 603 41 0 48478 0
vsize: 194076
[startup+420.01 s]
Raw data (loadavg): 0.99 0.94 0.89 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 49674 0 0 0 41883 122 0 0 25 0 1 0 545379859 202846208 48581 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49523 48581 603 41 0 49482 0
vsize: 198092
[startup+430.01 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 50727 0 0 0 42881 124 0 0 25 0 1 0 545379859 207142912 49634 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50572 49634 603 41 0 50531 0
vsize: 202288
[startup+440.012 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 51526 0 0 0 43880 126 0 0 25 0 1 0 545379859 210448384 50433 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51379 50433 603 41 0 51338 0
vsize: 205516
[startup+450.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 52333 0 0 0 44878 128 0 0 25 0 1 0 545379859 213737472 51240 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52182 51240 603 41 0 52141 0
vsize: 208728
[startup+460.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 53276 0 0 0 45876 129 0 0 25 0 1 0 545379859 217579520 52183 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53120 52183 603 41 0 53079 0
vsize: 212480
[startup+470.011 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 54036 0 0 0 46875 131 0 0 25 0 1 0 545379859 220606464 52943 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53859 52943 603 41 0 53818 0
vsize: 215436
[startup+480.012 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 54835 0 0 0 47873 132 0 0 25 0 1 0 545379859 223928320 53742 4294967295 134512640 134672761 3221224544 3221223744 134610622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54670 53742 603 41 0 54629 0
vsize: 218680
[startup+490.012 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 56272 0 0 0 48869 136 0 0 25 0 1 0 545379859 229855232 55179 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56117 55179 603 41 0 56076 0
vsize: 224468
[startup+500.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 57576 0 0 0 49865 139 0 0 25 0 1 0 545379859 235188224 56483 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57419 56483 603 41 0 57378 0
vsize: 229676
[startup+510.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 58631 0 0 0 50861 143 0 0 25 0 1 0 545379859 239501312 57538 4294967295 134512640 134672761 3221224544 3221223584 134612604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58472 57538 603 41 0 58431 0
vsize: 233888
[startup+520.013 s]
Raw data (loadavg): 0.99 0.95 0.90 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 59667 0 0 0 51858 145 0 0 25 0 1 0 545379859 243658752 58574 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59487 58574 603 41 0 59446 0
vsize: 237948
[startup+530.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 60285 0 0 0 52856 146 0 0 25 0 1 0 545379859 246169600 59192 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60100 59192 603 41 0 60059 0
vsize: 240400
[startup+540.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 61157 0 0 0 53853 149 0 0 25 0 1 0 545379859 249729024 60064 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60969 60065 603 41 0 60928 0
vsize: 243876
[startup+550.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 62154 0 0 0 54851 151 0 0 25 0 1 0 545379859 253886464 61061 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61984 61061 603 41 0 61943 0
vsize: 247936
[startup+560.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 62807 0 0 0 55849 153 0 0 25 0 1 0 545379859 256548864 61714 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62634 61714 603 41 0 62593 0
vsize: 250536
[startup+570.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 63544 0 0 0 56847 155 0 0 25 0 1 0 545379859 259543040 62451 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63365 62451 603 41 0 63324 0
vsize: 253460
[startup+580.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 64123 0 0 0 57846 156 0 0 25 0 1 0 545379859 261939200 63030 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 63950 63030 603 41 0 63909 0
vsize: 255800
[startup+590.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 64926 0 0 0 58844 157 0 0 25 0 1 0 545379859 265232384 63833 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 64754 63833 603 41 0 64713 0
vsize: 259016
[startup+600.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 66087 0 0 0 59842 160 0 0 25 0 1 0 545379859 269934592 64994 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 65902 64994 603 41 0 65861 0
vsize: 263608
[startup+610.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 66952 0 0 0 60839 162 0 0 25 0 1 0 545379859 273981440 65859 4294967295 134512640 134672761 3221224544 3221223584 134614256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 66890 65859 603 41 0 66849 0
vsize: 267560
[startup+620.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 67702 0 0 0 61838 164 0 0 25 0 1 0 545379859 277118976 66609 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 67656 66609 603 41 0 67615 0
vsize: 270624
[startup+630.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 68319 0 0 0 62836 165 0 0 25 0 1 0 545379859 279613440 67226 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68265 67226 603 41 0 68224 0
vsize: 273060
[startup+640.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 68856 0 0 0 63835 166 0 0 25 0 1 0 545379859 281726976 67763 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 68781 67763 603 41 0 68740 0
vsize: 275124
[startup+650.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 69783 0 0 0 64832 168 0 0 25 0 1 0 545379859 285548544 68690 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 69714 68690 603 41 0 69673 0
vsize: 278856
[startup+660.017 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 70390 0 0 0 65830 171 0 0 25 0 1 0 545379859 288083968 69297 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 70333 69297 603 41 0 70292 0
vsize: 281332
[startup+670.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71127 0 0 0 66828 173 0 0 25 0 1 0 545379859 291127296 70034 4294967295 134512640 134672761 3221224544 3221223416 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71076 70035 603 41 0 71035 0
vsize: 284304
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71525 0 0 0 67828 173 0 0 25 0 1 0 545379859 292720640 70432 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71465 70432 603 41 0 71424 0
vsize: 285860
[startup+690.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71598 0 0 0 68828 173 0 0 25 0 1 0 545379859 292982784 70505 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71529 70505 603 41 0 71488 0
vsize: 286116
[startup+700.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 69827 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 70827 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 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.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 71827 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 72827 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223668 134566128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+740.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 73827 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+750.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 74827 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+760.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 75828 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612835 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+770.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 76828 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+780.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 77828 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+790.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 78828 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+800.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 79828 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+810.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 80828 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+820.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 81829 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 82829 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+840.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 83829 174 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+850.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 84829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+860.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 85829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 86829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 87829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 88829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+900.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 89829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 90829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+920.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 91829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615801 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 92829 175 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 93830 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 94830 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223704 134614477 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 95830 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 96830 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+980.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 97830 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 98830 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 99830 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 100831 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 101831 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 102831 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 103831 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 104831 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 105831 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 106831 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223584 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 107832 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 108832 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 109832 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 110832 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 111832 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616108 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 112832 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 113832 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616373 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 114833 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 115833 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 116833 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 117833 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 118833 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5698
Raw data (stat): 5698 (minisat+) R 5697 3260 3259 0 -1 0 71891 0 0 0 119833 176 0 0 25 0 1 0 545379859 293584896 70656 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 71676 70656 603 41 0 71635 0
vsize: 286704
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 5698
Raw data (stat): 5698 (minisat+) Z 5697 3260 3259 0 -1 12 71891 0 0 0 119833 189 0 0 25 0 1 0 545379859 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.15
CPU time (s): 1200.24
CPU user time (s): 1198.34
CPU system time (s): 1.89871
CPU usage (%): 100.007
Max. virtual memory (Kb): 286704
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####