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-vpm1.opb
MD5SUM	ec9e3281577e2d3f7b25c1cc88cac9ea
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	168
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06884
Number of variables	2124
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	64
Trace number 17912

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 12:32:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18933 boxname=wulflinc21 idbench=1457 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  ec9e3281577e2d3f7b25c1cc88cac9ea  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-vpm1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-vpm1.opb
IDLAUNCH: 18933
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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.161
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:        877892 kB
Buffers:          1216 kB
Cached:         133220 kB
SwapCached:          0 kB
Active:          14436 kB
Inactive:       122876 kB
HighTotal:      131008 kB
HighFree:        91784 kB
LowTotal:       903652 kB
LowFree:        786108 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13656 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 12:52:38 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 18933 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 1826     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 246]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 244]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 242]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 224]---> Sorter-cost: 1582     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 212]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 210]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Sorter-cost: 1882     Base: 2 2 2 2 5 5 2 2 2 5
c ---[ 198]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> BDD-cost:   33
c ---[ 190]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  540     Base: 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  761     Base: 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  655     Base: 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   33
c ---[ 184]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  520     Base: 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  707     Base: 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost:  705     Base: 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   33
c ---[ 178]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  527     Base: 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  720     Base: 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  692     Base: 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   33
c ---[ 172]---> Sorter-cost:  253     Base: 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  486     Base: 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  695     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  625     Base: 2 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    6
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  144566   360910 |   48188       0        0     nan |  0.000 % |
c |       100 |  144514   360784 |   53006      98      499     5.1 |  6.116 % |
c |       251 |  144397   360518 |   58307     244     1686     6.9 |  6.175 % |
c |       476 |  144397   360518 |   64138     469     3339     7.1 |  6.175 % |
c |       813 |  144397   360518 |   70552     806     8685    10.8 |  6.175 % |
c |      1319 |  144337   360381 |   77607    1311    24858    19.0 |  6.206 % |
c |      2078 |  144191   360038 |   85367    2057    33401    16.2 |  6.281 % |
c |      3218 |  143818   359196 |   93904    3178    50467    15.9 |  6.486 % |
c |      4926 |  143287   357996 |  103295    4836    72661    15.0 |  6.777 % |
c |      7488 |  143182   357750 |  113624    7385   155213    21.0 |  6.834 % |
c |     11332 |  143082   357526 |  124987   11219   262443    23.4 |  6.886 % |
c |     17098 |  142936   357200 |  137485   16976   448398    26.4 |  6.966 % |
c |     25748 |  142359   355853 |  151234   25578   710280    27.8 |  7.281 % |
c |     38722 |  142203   355504 |  166358   38542  1139672    29.6 |  7.368 % |
c |     58183 |  141905   354826 |  182993   57975  1716418    29.6 |  7.528 % |
c |     87377 |  141473   353854 |  201293   87113  2764142    31.7 |  7.764 % |
c |    131169 |  140881   352461 |  221422  130846  4793681    36.6 |  8.089 % |
c |    196854 |  140827   352341 |  243564  196515  8908564    45.3 |  8.122 % |
c |    295381 |  139397   349113 |  267921   72533  2036665    28.1 |  8.941 % |
c |    443170 |  138341   346669 |  294713  220188  7897187    35.9 |  9.552 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.94 0.90 2/55 11349
Raw data (stat): 11349 (runsolver) R 11348 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 422369633 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99998 s]
Raw data (loadavg): 0.87 0.95 0.90 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 4719 0 0 0 987 11 0 0 25 0 1 0 422369633 21606400 4538 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5275 4538 603 41 0 5234 0
vsize: 21100
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 5114 0 0 0 1987 12 0 0 25 0 1 0 422369633 23298048 4933 4294967295 134512640 134672761 3221224624 3221223728 134559908 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5688 4933 603 41 0 5647 0
vsize: 22752
[startup+30.0013 s]
Raw data (loadavg): 0.91 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 5469 0 0 0 2986 13 0 0 25 0 1 0 422369633 24760320 5288 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6045 5288 603 41 0 6004 0
vsize: 24180
[startup+40.002 s]
Raw data (loadavg): 0.92 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 5840 0 0 0 3985 14 0 0 25 0 1 0 422369633 26353664 5659 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6434 5659 603 41 0 6393 0
vsize: 25736
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 6230 0 0 0 4983 16 0 0 25 0 1 0 422369633 27955200 6049 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6825 6049 603 41 0 6784 0
vsize: 27300
[startup+60.0027 s]
Raw data (loadavg): 0.94 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 6538 0 0 0 5982 17 0 0 25 0 1 0 422369633 29167616 6357 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7121 6357 603 41 0 7080 0
vsize: 28484
[startup+70.0029 s]
Raw data (loadavg): 0.95 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 6796 0 0 0 6981 18 0 0 25 0 1 0 422369633 30113792 6615 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7352 6615 603 41 0 7311 0
vsize: 29408
[startup+80.0036 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 7204 0 0 0 7981 18 0 0 25 0 1 0 422369633 32108544 7023 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7839 7023 603 41 0 7798 0
vsize: 31356
[startup+90.0043 s]
Raw data (loadavg): 0.96 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 7540 0 0 0 8980 19 0 0 25 0 1 0 422369633 33439744 7359 4294967295 134512640 134672761 3221224624 3221223788 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8164 7359 603 41 0 8123 0
vsize: 32656
[startup+100.004 s]
Raw data (loadavg): 0.97 0.95 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 7829 0 0 0 9979 21 0 0 25 0 1 0 422369633 34648064 7648 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8459 7648 603 41 0 8418 0
vsize: 33836
[startup+110.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 8120 0 0 0 10978 21 0 0 25 0 1 0 422369633 35704832 7939 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8717 7939 603 41 0 8676 0
vsize: 34868
[startup+120.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 8286 0 0 0 11978 22 0 0 25 0 1 0 422369633 36368384 8105 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8879 8105 603 41 0 8838 0
vsize: 35516
[startup+130.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 8440 0 0 0 12978 22 0 0 25 0 1 0 422369633 37048320 8259 4294967295 134512640 134672761 3221224624 3221223760 134560718 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9045 8259 603 41 0 9004 0
vsize: 36180
[startup+140.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 8733 0 0 0 13977 23 0 0 25 0 1 0 422369633 38260736 8552 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9341 8552 603 41 0 9300 0
vsize: 37364
[startup+150.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 8988 0 0 0 14976 24 0 0 25 0 1 0 422369633 39215104 8807 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9574 8807 603 41 0 9533 0
vsize: 38296
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 9301 0 0 0 15976 25 0 0 25 0 1 0 422369633 40542208 9120 4294967295 134512640 134672761 3221224624 3221223792 134561133 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9898 9120 603 41 0 9857 0
vsize: 39592
[startup+170.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 9688 0 0 0 16975 26 0 0 25 0 1 0 422369633 42123264 9507 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10284 9507 603 41 0 10243 0
vsize: 41136
[startup+180.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 10190 0 0 0 17973 28 0 0 25 0 1 0 422369633 44138496 10009 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10776 10009 603 41 0 10735 0
vsize: 43104
[startup+190.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 10694 0 0 0 18972 29 0 0 25 0 1 0 422369633 46649344 10513 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11389 10513 603 41 0 11348 0
vsize: 45556
[startup+200.004 s]
Raw data (loadavg): 0.99 0.96 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 11051 0 0 0 19971 30 0 0 25 0 1 0 422369633 48115712 10870 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11747 10870 603 41 0 11706 0
vsize: 46988
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 11349 0 0 0 20970 31 0 0 25 0 1 0 422369633 49307648 11168 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12038 11168 603 41 0 11997 0
vsize: 48152
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 11644 0 0 0 21970 32 0 0 25 0 1 0 422369633 50499584 11463 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12329 11463 603 41 0 12288 0
vsize: 49316
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 11909 0 0 0 22968 33 0 0 25 0 1 0 422369633 51560448 11728 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12588 11728 603 41 0 12547 0
vsize: 50352
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 12163 0 0 0 23967 35 0 0 25 0 1 0 422369633 52617216 11982 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12846 11982 603 41 0 12805 0
vsize: 51384
[startup+250.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 12389 0 0 0 24967 35 0 0 25 0 1 0 422369633 53534720 12208 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13070 12208 603 41 0 13029 0
vsize: 52280
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 12621 0 0 0 25966 36 0 0 25 0 1 0 422369633 54456320 12440 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13295 12440 603 41 0 13254 0
vsize: 53180
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 12879 0 0 0 26966 37 0 0 25 0 1 0 422369633 55508992 12698 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13552 12698 603 41 0 13511 0
vsize: 54208
[startup+280.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 13115 0 0 0 27965 38 0 0 25 0 1 0 422369633 56438784 12934 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13779 12934 603 41 0 13738 0
vsize: 55116
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 13343 0 0 0 28964 39 0 0 25 0 1 0 422369633 57364480 13162 4294967295 134512640 134672761 3221224624 3221223728 134560237 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14005 13162 603 41 0 13964 0
vsize: 56020
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 13583 0 0 0 29963 40 0 0 25 0 1 0 422369633 58417152 13402 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14262 13402 603 41 0 14221 0
vsize: 57048
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 13782 0 0 0 30963 40 0 0 25 0 1 0 422369633 59203584 13601 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14454 13601 603 41 0 14413 0
vsize: 57816
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 13957 0 0 0 31963 41 0 0 25 0 1 0 422369633 59858944 13776 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14614 13776 603 41 0 14573 0
vsize: 58456
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 14139 0 0 0 32962 41 0 0 25 0 1 0 422369633 60653568 13958 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14808 13958 603 41 0 14767 0
vsize: 59232
[startup+340.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 14347 0 0 0 33962 42 0 0 25 0 1 0 422369633 61464576 14166 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15006 14166 603 41 0 14965 0
vsize: 60024
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 14550 0 0 0 34961 43 0 0 25 0 1 0 422369633 62402560 14369 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15235 14369 603 41 0 15194 0
vsize: 60940
[startup+360.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 14712 0 0 0 35960 44 0 0 25 0 1 0 422369633 63074304 14531 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14531 603 41 0 15358 0
vsize: 61596
[startup+370.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 14871 0 0 0 36960 44 0 0 25 0 1 0 422369633 63741952 14690 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15562 14690 603 41 0 15521 0
vsize: 62248
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 15040 0 0 0 37960 45 0 0 25 0 1 0 422369633 64405504 14859 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15724 14859 603 41 0 15683 0
vsize: 62896
[startup+390.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 15252 0 0 0 38959 45 0 0 25 0 1 0 422369633 65196032 15071 4294967295 134512640 134672761 3221224624 3221223760 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15917 15071 603 41 0 15876 0
vsize: 63668
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 15387 0 0 0 39959 45 0 0 25 0 1 0 422369633 65748992 15206 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16052 15206 603 41 0 16011 0
vsize: 64208
[startup+410.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 15545 0 0 0 40959 46 0 0 25 0 1 0 422369633 66453504 15364 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16224 15364 603 41 0 16183 0
vsize: 64896
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 15682 0 0 0 41958 46 0 0 25 0 1 0 422369633 67014656 15501 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16361 15501 603 41 0 16320 0
vsize: 65444
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 15843 0 0 0 42958 47 0 0 25 0 1 0 422369633 67682304 15662 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16524 15662 603 41 0 16483 0
vsize: 66096
[startup+440.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 15975 0 0 0 43957 48 0 0 25 0 1 0 422369633 68214784 15794 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16654 15794 603 41 0 16613 0
vsize: 66616
[startup+450.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16110 0 0 0 44956 49 0 0 25 0 1 0 422369633 68739072 15929 4294967295 134512640 134672761 3221224624 3221223808 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16782 15929 603 41 0 16741 0
vsize: 67128
[startup+460.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16234 0 0 0 45956 49 0 0 25 0 1 0 422369633 69263360 16053 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16910 16053 603 41 0 16869 0
vsize: 67640
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16344 0 0 0 46955 50 0 0 25 0 1 0 422369633 69656576 16163 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17006 16163 603 41 0 16965 0
vsize: 68024
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16450 0 0 0 47955 50 0 0 25 0 1 0 422369633 70053888 16269 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17103 16269 603 41 0 17062 0
vsize: 68412
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16558 0 0 0 48955 50 0 0 25 0 1 0 422369633 70467584 16377 4294967295 134512640 134672761 3221224624 3221223808 134558648 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17204 16377 603 41 0 17163 0
vsize: 68816
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16681 0 0 0 49955 51 0 0 25 0 1 0 422369633 71012352 16500 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17337 16500 603 41 0 17296 0
vsize: 69348
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16786 0 0 0 50955 51 0 0 25 0 1 0 422369633 71553024 16605 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17469 16605 603 41 0 17428 0
vsize: 69876
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16892 0 0 0 51955 52 0 0 25 0 1 0 422369633 71946240 16711 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17565 16711 603 41 0 17524 0
vsize: 70260
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 16995 0 0 0 52954 52 0 0 25 0 1 0 422369633 72372224 16814 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17669 16814 603 41 0 17628 0
vsize: 70676
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 17092 0 0 0 53954 52 0 0 25 0 1 0 422369633 72773632 16911 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17767 16911 603 41 0 17726 0
vsize: 71068
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 17189 0 0 0 54953 53 0 0 25 0 1 0 422369633 73175040 17008 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17865 17008 603 41 0 17824 0
vsize: 71460
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 17279 0 0 0 55953 53 0 0 25 0 1 0 422369633 73441280 17098 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17930 17098 603 41 0 17889 0
vsize: 71720
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 17447 0 0 0 56952 54 0 0 25 0 1 0 422369633 74158080 17266 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18105 17266 603 41 0 18064 0
vsize: 72420
[startup+580.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 17590 0 0 0 57952 55 0 0 25 0 1 0 422369633 74825728 17409 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18268 17409 603 41 0 18227 0
vsize: 73072
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 17726 0 0 0 58952 55 0 0 25 0 1 0 422369633 75366400 17545 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18400 17545 603 41 0 18359 0
vsize: 73600
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 17883 0 0 0 59951 56 0 0 25 0 1 0 422369633 75907072 17702 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18532 17702 603 41 0 18491 0
vsize: 74128
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 17986 0 0 0 60951 56 0 0 25 0 1 0 422369633 76304384 17805 4294967295 134512640 134672761 3221224624 3221223728 134560008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18629 17805 603 41 0 18588 0
vsize: 74516
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18118 0 0 0 61951 57 0 0 25 0 1 0 422369633 76972032 17937 4294967295 134512640 134672761 3221224624 3221223728 134560376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18792 17937 603 41 0 18751 0
vsize: 75168
[startup+630.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18274 0 0 0 62950 57 0 0 25 0 1 0 422369633 77508608 18093 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18923 18093 603 41 0 18882 0
vsize: 75692
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 63950 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 64950 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+660.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 65950 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 66950 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 67951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 68951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+700.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 69951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 70951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 71951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223728 134555314 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 72951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 73951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 74951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+760.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18391 0 0 0 75951 58 0 0 25 0 1 0 422369633 78045184 18210 4294967295 134512640 134672761 3221224624 3221223728 134560224 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18210 603 41 0 19013 0
vsize: 76216
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18393 0 0 0 76952 58 0 0 25 0 1 0 422369633 78045184 18212 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18212 603 41 0 19013 0
vsize: 76216
[startup+780.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18393 0 0 0 77951 58 0 0 25 0 1 0 422369633 78045184 18212 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18212 603 41 0 19013 0
vsize: 76216
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18393 0 0 0 78951 58 0 0 25 0 1 0 422369633 78045184 18212 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18212 603 41 0 19013 0
vsize: 76216
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18393 0 0 0 79951 58 0 0 25 0 1 0 422369633 78045184 18212 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18212 603 41 0 19013 0
vsize: 76216
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18393 0 0 0 80951 59 0 0 25 0 1 0 422369633 78045184 18212 4294967295 134512640 134672761 3221224624 3221223728 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19054 18212 603 41 0 19013 0
vsize: 76216
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18394 0 0 0 81951 59 0 0 25 0 1 0 422369633 78045184 18213 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18213 603 41 0 19013 0
vsize: 76216
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18395 0 0 0 82951 59 0 0 25 0 1 0 422369633 78045184 18214 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18214 603 41 0 19013 0
vsize: 76216
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18398 0 0 0 83952 59 0 0 25 0 1 0 422369633 78045184 18217 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18217 603 41 0 19013 0
vsize: 76216
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18398 0 0 0 84952 59 0 0 25 0 1 0 422369633 78045184 18217 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18217 603 41 0 19013 0
vsize: 76216
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18400 0 0 0 85952 59 0 0 25 0 1 0 422369633 78045184 18219 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18219 603 41 0 19013 0
vsize: 76216
[startup+870.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18400 0 0 0 86952 59 0 0 25 0 1 0 422369633 78045184 18219 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18219 603 41 0 19013 0
vsize: 76216
[startup+880.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18409 0 0 0 87952 59 0 0 25 0 1 0 422369633 78045184 18228 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18228 603 41 0 19013 0
vsize: 76216
[startup+890.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18409 0 0 0 88953 59 0 0 25 0 1 0 422369633 78045184 18228 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18228 603 41 0 19013 0
vsize: 76216
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18409 0 0 0 89953 59 0 0 25 0 1 0 422369633 78045184 18228 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18228 603 41 0 19013 0
vsize: 76216
[startup+910.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18409 0 0 0 90954 59 0 0 25 0 1 0 422369633 78045184 18228 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18228 603 41 0 19013 0
vsize: 76216
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18409 0 0 0 91954 59 0 0 25 0 1 0 422369633 78045184 18228 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18228 603 41 0 19013 0
vsize: 76216
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18409 0 0 0 92954 59 0 0 25 0 1 0 422369633 78045184 18228 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18228 603 41 0 19013 0
vsize: 76216
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18409 0 0 0 93954 59 0 0 25 0 1 0 422369633 78045184 18228 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18228 603 41 0 19013 0
vsize: 76216
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18411 0 0 0 94954 59 0 0 25 0 1 0 422369633 78045184 18230 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18230 603 41 0 19013 0
vsize: 76216
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 95954 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 96955 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223728 134559902 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 97955 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 98955 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223728 134560191 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 99955 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223808 134558651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 100955 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 101955 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 102956 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 103956 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18412 0 0 0 104956 59 0 0 25 0 1 0 422369633 78045184 18231 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19054 18231 603 41 0 19013 0
vsize: 76216
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18426 0 0 0 105956 59 0 0 25 0 1 0 422369633 78217216 18245 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18245 603 41 0 19055 0
vsize: 76384
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18429 0 0 0 106956 59 0 0 25 0 1 0 422369633 78217216 18248 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18248 603 41 0 19055 0
vsize: 76384
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18429 0 0 0 107956 59 0 0 25 0 1 0 422369633 78217216 18248 4294967295 134512640 134672761 3221224624 3221223760 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18248 603 41 0 19055 0
vsize: 76384
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18429 0 0 0 108956 59 0 0 25 0 1 0 422369633 78217216 18248 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18248 603 41 0 19055 0
vsize: 76384
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18440 0 0 0 109956 59 0 0 25 0 1 0 422369633 78217216 18259 4294967295 134512640 134672761 3221224624 3221223780 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18259 603 41 0 19055 0
vsize: 76384
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18441 0 0 0 110956 59 0 0 25 0 1 0 422369633 78217216 18260 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18260 603 41 0 19055 0
vsize: 76384
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18441 0 0 0 111956 59 0 0 25 0 1 0 422369633 78217216 18260 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18260 603 41 0 19055 0
vsize: 76384
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18441 0 0 0 112956 59 0 0 25 0 1 0 422369633 78217216 18260 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18260 603 41 0 19055 0
vsize: 76384
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18441 0 0 0 113956 59 0 0 25 0 1 0 422369633 78217216 18260 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18260 603 41 0 19055 0
vsize: 76384
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18441 0 0 0 114956 60 0 0 25 0 1 0 422369633 78217216 18260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18260 603 41 0 19055 0
vsize: 76384
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18441 0 0 0 115956 60 0 0 25 0 1 0 422369633 78217216 18260 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18260 603 41 0 19055 0
vsize: 76384
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18442 0 0 0 116956 60 0 0 25 0 1 0 422369633 78217216 18261 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18261 603 41 0 19055 0
vsize: 76384
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18444 0 0 0 117956 60 0 0 25 0 1 0 422369633 78217216 18263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18263 603 41 0 19055 0
vsize: 76384
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18447 0 0 0 118956 60 0 0 25 0 1 0 422369633 78217216 18266 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18266 603 41 0 19055 0
vsize: 76384
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 11349
Raw data (stat): 11349 (minisat+) R 11348 30927 30926 0 -1 0 18450 0 0 0 119956 60 0 0 25 0 1 0 422369633 78217216 18269 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19096 18269 603 41 0 19055 0
vsize: 76384
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 11349
Raw data (stat): 11349 (minisat+) Z 11348 30927 30926 0 -1 12 18452 0 0 0 119956 64 0 0 25 0 1 0 422369633 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.06
CPU time (s): 1200.21
CPU user time (s): 1199.57
CPU system time (s): 0.641902
CPU usage (%): 100.013
Max. virtual memory (Kb): 76384
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####