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/miplib2003/normalized-mps-v2-13-7-pp08aCUTS.opb
MD5SUM	d1b87efc35bcd73acfc5183bbe3df4f0
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	2304
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	178464600
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	178464600
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	3288
Total number of constraints	374
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	64
Number of constraints which are nor clauses,nor cardinality constraints	310
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 15323

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc3 THE 2005-04-21 03:56:02 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17913 boxname=wulflinc3 idbench=1378 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d1b87efc35bcd73acfc5183bbe3df4f0  /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-pp08aCUTS.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-pp08aCUTS.opb /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-pp08aCUTS.opb
IDLAUNCH: 17913
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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	: 2
cpu MHz		: 451.190
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:        517900 kB
Buffers:         33864 kB
Cached:         459420 kB
SwapCached:         56 kB
Active:          33620 kB
Inactive:       462540 kB
HighTotal:      131008 kB
HighFree:        42616 kB
LowTotal:       903652 kB
LowFree:        475284 kB
SwapTotal:     2097136 kB
SwapFree:      2096992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6840 kB
Slab:            14924 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 04:16:05 (client local time) WITH STATUS 0 IN 1200.07 SECONDS
stats: 17913 7 1200.07 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 374 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[ 501]---> BDD-cost:   15
c ---[ 500]---> BDD-cost:   15
c ---[ 499]---> BDD-cost:   15
c ---[ 498]---> BDD-cost:   15
c ---[ 497]---> BDD-cost:   15
c ---[ 496]---> BDD-cost:   15
c ---[ 495]---> BDD-cost:   15
c ---[ 494]---> BDD-cost:   15
c ---[ 485]---> BDD-cost:   15
c ---[ 484]---> BDD-cost:   15
c ---[ 483]---> BDD-cost:   15
c ---[ 482]---> BDD-cost:   15
c ---[ 481]---> BDD-cost:   15
c ---[ 480]---> BDD-cost:   15
c ---[ 479]---> BDD-cost:   15
c ---[ 477]---> BDD-cost:   15
c ---[ 476]---> BDD-cost:   15
c ---[ 475]---> BDD-cost:   15
c ---[ 474]---> BDD-cost:   15
c ---[ 473]---> BDD-cost:   15
c ---[ 472]---> BDD-cost:   15
c ---[ 471]---> BDD-cost:   15
c ---[ 469]---> BDD-cost:   14
c ---[ 468]---> BDD-cost:   14
c ---[ 467]---> BDD-cost:   14
c ---[ 466]---> BDD-cost:   14
c ---[ 465]---> BDD-cost:   14
c ---[ 464]---> BDD-cost:   14
c ---[ 463]---> BDD-cost:   14
c ---[ 462]---> BDD-cost:   14
c ---[ 461]---> BDD-cost:   15
c ---[ 460]---> BDD-cost:   15
c ---[ 459]---> BDD-cost:   15
c ---[ 458]---> BDD-cost:   15
c ---[ 457]---> BDD-cost:   15
c ---[ 456]---> BDD-cost:   15
c ---[ 455]---> BDD-cost:   15
c ---[ 454]---> BDD-cost:   15
c ---[ 445]---> BDD-cost:   13
c ---[ 444]---> BDD-cost:   13
c ---[ 443]---> BDD-cost:   13
c ---[ 442]---> BDD-cost:   13
c ---[ 441]---> BDD-cost:   13
c ---[ 440]---> BDD-cost:   13
c ---[ 439]---> BDD-cost:   13
c ---[ 438]---> BDD-cost:   13
c ---[ 436]---> BDD-cost:  158
c ---[ 434]---> BDD-cost:  566
c ---[ 433]---> BDD-cost:    6
c ---[ 432]---> BDD-cost:    6
c ---[ 431]---> BDD-cost:    6
c ---[ 430]---> BDD-cost:    6
c ---[ 429]---> BDD-cost:   23
c ---[ 428]---> BDD-cost:    4
c ---[ 427]---> BDD-cost:    4
c ---[ 426]---> BDD-cost:    4
c ---[ 425]---> BDD-cost:    4
c ---[ 424]---> BDD-cost:    4
c ---[ 422]---> BDD-cost:  576
c ---[ 421]---> BDD-cost:    4
c ---[ 420]---> BDD-cost:    4
c ---[ 419]---> BDD-cost:    4
c ---[ 418]---> BDD-cost:    9
c ---[ 417]---> BDD-cost:    9
c ---[ 416]---> BDD-cost:    9
c ---[ 415]---> BDD-cost:    6
c ---[ 414]---> BDD-cost:    6
c ---[ 413]---> BDD-cost:    6
c ---[ 412]---> BDD-cost:    6
c ---[ 410]---> BDD-cost:  576
c ---[ 409]---> BDD-cost:    6
c ---[ 408]---> BDD-cost:   19
c ---[ 407]---> BDD-cost:   19
c ---[ 406]---> BDD-cost:   19
c ---[ 405]---> BDD-cost:   19
c ---[ 404]---> BDD-cost:   19
c ---[ 403]---> BDD-cost:   19
c ---[ 402]---> BDD-cost:   19
c ---[ 401]---> BDD-cost:   19
c ---[ 400]---> BDD-cost:    6
c ---[ 398]---> BDD-cost:  576
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    6
c ---[ 394]---> BDD-cost:    6
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    6
c ---[ 386]---> BDD-cost:  529
c ---[ 374]---> BDD-cost:  566
c ---[ 362]---> BDD-cost:  181
c ---[ 350]---> BDD-cost:  180
c ---[ 338]---> BDD-cost:  585
c ---[ 326]---> BDD-cost:  537
c ---[ 314]---> BDD-cost:  585
c ---[ 312]---> BDD-cost:  580
c ---[ 300]---> BDD-cost:  575
c ---[ 288]---> BDD-cost:  570
c ---[ 276]---> BDD-cost:  585
c ---[ 264]---> BDD-cost:  174
c ---[ 255]---> BDD-cost:  158
c ---[ 253]---> BDD-cost:  580
c ---[ 251]---> BDD-cost:  580
c ---[ 249]---> BDD-cost:  585
c ---[ 247]---> BDD-cost:  565
c ---[ 245]---> BDD-cost:  585
c ---[ 243]---> BDD-cost:  585
c ---[ 241]---> BDD-cost:  580
c ---[ 239]---> BDD-cost:  183
c ---[ 237]---> BDD-cost:  181
c ---[ 235]---> BDD-cost:  529
c ---[ 233]---> BDD-cost:  571
c ---[ 231]---> BDD-cost:  566
c ---[ 229]---> BDD-cost:  576
c ---[ 227]---> BDD-cost:  576
c ---[ 225]---> BDD-cost:  571
c ---[ 223]---> BDD-cost:  580
c ---[ 221]---> BDD-cost:  181
c ---[ 219]---> BDD-cost:  186
c ---[ 217]---> BDD-cost:  575
c ---[ 215]---> BDD-cost:  575
c ---[ 213]---> BDD-cost:  575
c ---[ 211]---> BDD-cost:  580
c ---[ 209]---> BDD-cost:  580
c ---[ 207]---> BDD-cost:  575
c ---[ 205]---> BDD-cost:  186
c ---[ 203]---> BDD-cost:  154
c ---[ 201]---> BDD-cost:  580
c ---[ 199]---> BDD-cost:  571
c ---[ 197]---> BDD-cost:  576
c ---[ 195]---> BDD-cost:  576
c ---[ 193]---> BDD-cost:  571
c ---[ 191]---> BDD-cost:  571
c ---[ 189]---> BDD-cost:  566
c ---[ 187]---> BDD-cost:  175
c ---[ 185]---> BDD-cost:  176
c ---[ 183]---> BDD-cost:  562
c ---[ 181]---> BDD-cost:  521
c ---[ 179]---> BDD-cost:  570
c ---[ 177]---> BDD-cost:  521
c ---[ 175]---> BDD-cost:  567
c ---[ 173]---> BDD-cost:  567
c ---[ 171]---> BDD-cost:  562
c ---[ 169]---> BDD-cost:  176
c ---[ 168]---> BDD-cost: 1143
c ---[ 167]---> BDD-cost: 1143
c ---[ 166]---> BDD-cost: 1143
c ---[ 165]---> BDD-cost: 1165
c ---[ 164]---> BDD-cost: 1165
c ---[ 162]---> BDD-cost:  537
c ---[ 161]---> BDD-cost: 1165
c ---[ 160]---> BDD-cost: 1165
c ---[ 159]---> BDD-cost: 1176
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    6
c ---[ 154]---> BDD-cost:    6
c ---[ 153]---> BDD-cost:    6
c ---[ 152]---> BDD-cost:    6
c ---[ 150]---> BDD-cost:  183
c ---[ 149]---> BDD-cost:    8
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:   19
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   19
c ---[ 142]---> BDD-cost:   19
c ---[ 141]---> BDD-cost:   19
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:  178
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    6
c ---[ 134]---> BDD-cost:    6
c ---[ 133]---> BDD-cost:    6
c ---[ 132]---> BDD-cost:    6
c ---[ 131]---> BDD-cost:   23
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:   50
c ---[ 108]---> BDD-cost:  203
c ---[ 107]---> BDD-cost:   45
c ---[ 106]---> BDD-cost:  194
c ---[ 105]---> BDD-cost:   48
c ---[ 104]---> BDD-cost:  191
c ---[ 103]---> BDD-cost:   38
c ---[ 102]---> BDD-cost:  173
c ---[ 101]---> BDD-cost:   44
c ---[ 100]---> BDD-cost:  167
c ---[  99]---> BDD-cost:    5
c ---[  98]---> BDD-cost:   73
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:   62
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:  158
c ---[  93]---> BDD-cost:   45
c ---[  92]---> BDD-cost:  182
c ---[  91]---> BDD-cost:   40
c ---[  90]---> BDD-cost:  173
c ---[  89]---> BDD-cost:   35
c ---[  88]---> BDD-cost:  164
c ---[  87]---> BDD-cost:   41
c ---[  86]---> BDD-cost:  158
c ---[  85]---> BDD-cost:    5
c ---[  84]---> BDD-cost:   70
c ---[  83]---> BDD-cost:    3
c ---[  82]---> BDD-cost:   65
c ---[  81]---> BDD-cost:   45
c ---[  80]---> BDD-cost:  194
c ---[  79]---> BDD-cost:   48
c ---[  78]---> BDD-cost:  191
c ---[  77]---> BDD-cost:   41
c ---[  76]---> BDD-cost:  170
c ---[  75]---> BDD-cost:   44
c ---[  74]---> BDD-cost:  167
c ---[  73]---> BDD-cost:   50
c ---[  72]---> BDD-cost:  203
c ---[  71]---> BDD-cost:    3
c ---[  70]---> BDD-cost:   61
c ---[  69]---> BDD-cost:   48
c ---[  68]---> BDD-cost:  191
c ---[  67]---> BDD-cost:   48
c ---[  66]---> BDD-cost:  191
c ---[  65]---> BDD-cost:   55
c ---[  64]---> BDD-cost:  209
c ---[  63]---> BDD-cost:   47
c ---[  62]---> BDD-cost:  161
c ---[  61]---> BDD-cost:   50
c ---[  60]---> BDD-cost:  203
c ---[  59]---> BDD-cost:   48
c ---[  58]---> BDD-cost:  191
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   73
c ---[  55]---> BDD-cost:    5
c ---[  54]---> BDD-cost:   70
c ---[  53]---> BDD-cost:   38
c ---[  52]---> BDD-cost:  161
c ---[  51]---> BDD-cost:   41
c ---[  50]---> BDD-cost:  158
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:  164
c ---[  47]---> BDD-cost:   35
c ---[  46]---> BDD-cost:  164
c ---[  45]---> BDD-cost:   38
c ---[  44]---> BDD-cost:  161
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:   64
c ---[  41]---> BDD-cost:    6
c ---[  40]---> BDD-cost:   78
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:  170
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:  170
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:  170
c ---[  33]---> BDD-cost:   48
c ---[  32]---> BDD-cost:  191
c ---[  31]---> BDD-cost:   38
c ---[  30]---> BDD-cost:  173
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:  170
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:   75
c ---[  25]---> BDD-cost:   38
c ---[  24]---> BDD-cost:  161
c ---[  23]---> BDD-cost:   45
c ---[  22]---> BDD-cost:  182
c ---[  21]---> BDD-cost:   35
c ---[  20]---> BDD-cost:  164
c ---[  19]---> BDD-cost:   38
c ---[  18]---> BDD-cost:  161
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:  170
c ---[  15]---> BDD-cost:   41
c ---[  14]---> BDD-cost:  158
c ---[  13]---> BDD-cost:    3
c ---[  12]---> BDD-cost:   60
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:   59
c ---[   9]---> BDD-cost:   38
c ---[   8]---> BDD-cost:  149
c ---[   7]---> BDD-cost:   35
c ---[   6]---> BDD-cost:  152
c ---[   5]---> BDD-cost:   35
c ---[   4]---> BDD-cost:  152
c ---[   3]---> BDD-cost:   38
c ---[   2]---> BDD-cost:  149
c ---[   1]---> BDD-cost:    4
c ---[   0]---> BDD-cost:   62
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  129110   364299 |   43036       0        0     nan |  0.000 % |
c |       100 |  129110   364299 |   47339     100      618     6.2 |  0.600 % |
c |       250 |  129110   364299 |   52073     250     1908     7.6 |  0.600 % |
c |       475 |  129110   364299 |   57280     475     3860     8.1 |  0.600 % |
c |       812 |  129110   364299 |   63009     812     6314     7.8 |  0.600 % |
c |      1320 |  129100   364279 |   69309    1319    16712    12.7 |  0.608 % |
c |      2080 |  129100   364279 |   76240    2079    25947    12.5 |  0.608 % |
c |      3221 |  129100   364279 |   83864    3220    46674    14.5 |  0.608 % |
c |      4929 |  129100   364279 |   92251    4928    64860    13.2 |  0.608 % |
c |      7492 |  129100   364279 |  101476    7491   112044    15.0 |  0.608 % |
c |     11337 |  129100   364279 |  111624   11336   198430    17.5 |  0.608 % |
c |     17105 |  129100   364279 |  122786   17104   290443    17.0 |  0.608 % |
c |     25755 |  129100   364279 |  135065   25754   521886    20.3 |  0.608 % |
c |     38729 |  129100   364279 |  148571   38728   758349    19.6 |  0.608 % |
c |     58190 |  129100   364279 |  163429   58189  1513648    26.0 |  0.608 % |
c |     87382 |  129100   364279 |  179772   87381  2387504    27.3 |  0.608 % |
c |    131171 |  129100   364279 |  197749  131170  3645871    27.8 |  0.608 % |
c |    196856 |  129100   364279 |  217524  196855  5799812    29.5 |  0.608 % |
c |    295382 |  129080   364236 |  239276   96045  1909577    19.9 |  0.623 % |
c |    443171 |  129073   364222 |  263204  243831  6453582    26.5 |  0.629 % |
c |    664854 |  129053   364179 |  289524  223057  6311998    28.3 |  0.645 % |
c |    997379 |  129037   364138 |  318477  290404  8482006    29.2 |  0.656 % |
#### 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.86 0.97 0.91 2/54 4416
Raw data (stat): 4416 (runsolver) R 4415 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483780431 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0003 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 5402 0 0 0 982 16 0 0 25 0 1 0 483780431 24059904 5231 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5874 5231 603 41 0 5833 0
vsize: 23496
[startup+20.0013 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 6011 0 0 0 1980 18 0 0 25 0 1 0 483780431 26722304 5840 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6524 5840 603 41 0 6483 0
vsize: 26096
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 6768 0 0 0 2977 21 0 0 25 0 1 0 483780431 29814784 6597 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7279 6597 603 41 0 7238 0
vsize: 29116
[startup+40.0026 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 7487 0 0 0 3974 24 0 0 25 0 1 0 483780431 32907264 7316 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8034 7316 603 41 0 7993 0
vsize: 32136
[startup+50.0037 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 8108 0 0 0 4972 26 0 0 25 0 1 0 483780431 35340288 7937 4294967295 134512640 134672761 3221224528 3221223696 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8628 7937 603 41 0 8587 0
vsize: 34512
[startup+60.0032 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 8789 0 0 0 5969 29 0 0 25 0 1 0 483780431 38158336 8618 4294967295 134512640 134672761 3221224528 3221223632 134559818 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8618 603 41 0 9275 0
vsize: 37264
[startup+70.0041 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 9497 0 0 0 6966 32 0 0 25 0 1 0 483780431 40984576 9326 4294967295 134512640 134672761 3221224528 3221223696 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10006 9326 603 41 0 9965 0
vsize: 40024
[startup+80.0043 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 9897 0 0 0 7965 33 0 0 25 0 1 0 483780431 43122688 9726 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10528 9726 603 41 0 10487 0
vsize: 42112
[startup+90.0048 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 10980 0 0 0 8961 37 0 0 25 0 1 0 483780431 47419392 10809 4294967295 134512640 134672761 3221224528 3221223712 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11577 10809 603 41 0 11536 0
vsize: 46308
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 11951 0 0 0 9959 40 0 0 25 0 1 0 483780431 51347456 11780 4294967295 134512640 134672761 3221224528 3221223744 134557662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12536 11780 603 41 0 12495 0
vsize: 50144
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 12597 0 0 0 10957 41 0 0 25 0 1 0 483780431 54038528 12426 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13193 12426 603 41 0 13152 0
vsize: 52772
[startup+120.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 12965 0 0 0 11956 43 0 0 25 0 1 0 483780431 55508992 12794 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13552 12794 603 41 0 13511 0
vsize: 54208
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 12956 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223712 134559498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 13956 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223652 134566125 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 14956 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+160.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 15956 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 16956 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223652 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 17957 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 18957 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 19957 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223696 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 20957 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223680 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 21957 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223696 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 22958 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+240.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4416
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13175 0 0 0 23958 43 0 0 25 0 1 0 483780431 56311808 13004 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13004 603 41 0 13707 0
vsize: 54992
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4469
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13176 0 0 0 24958 43 0 0 25 0 1 0 483780431 56311808 13005 4294967295 134512640 134672761 3221224528 3221223652 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13005 603 41 0 13707 0
vsize: 54992
[startup+260.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4469
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13176 0 0 0 25958 43 0 0 25 0 1 0 483780431 56311808 13005 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13005 603 41 0 13707 0
vsize: 54992
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4469
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13176 0 0 0 26958 43 0 0 25 0 1 0 483780431 56311808 13005 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13005 603 41 0 13707 0
vsize: 54992
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4469
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13176 0 0 0 27958 43 0 0 25 0 1 0 483780431 56311808 13005 4294967295 134512640 134672761 3221224528 3221223696 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13748 13005 603 41 0 13707 0
vsize: 54992
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4469
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13430 0 0 0 28958 45 0 0 25 0 1 0 483780431 57389056 13259 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14011 13259 603 41 0 13970 0
vsize: 56044
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4469
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 13723 0 0 0 29957 45 0 0 25 0 1 0 483780431 58478592 13552 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14277 13552 603 41 0 14236 0
vsize: 57108
[startup+310.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4469
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 14024 0 0 0 30956 46 0 0 25 0 1 0 483780431 59830272 13853 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14607 13853 603 41 0 14566 0
vsize: 58428
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 14250 0 0 0 31956 47 0 0 25 0 1 0 483780431 60727296 14079 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14826 14079 603 41 0 14785 0
vsize: 59304
[startup+330.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 14579 0 0 0 32956 47 0 0 25 0 1 0 483780431 62074880 14408 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15155 14408 603 41 0 15114 0
vsize: 60620
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15049 0 0 0 33954 49 0 0 25 0 1 0 483780431 63963136 14878 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15616 14878 603 41 0 15575 0
vsize: 62464
[startup+350.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15316 0 0 0 34954 49 0 0 25 0 1 0 483780431 66088960 15145 4294967295 134512640 134672761 3221224528 3221223696 134561637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16135 15145 603 41 0 16094 0
vsize: 64540
[startup+360.008 s]
Raw data (loadavg): 1.07 0.99 0.92 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15316 0 0 0 35954 49 0 0 25 0 1 0 483780431 66088960 15145 4294967295 134512640 134672761 3221224528 3221223696 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16135 15145 603 41 0 16094 0
vsize: 64540
[startup+370.008 s]
Raw data (loadavg): 1.06 0.99 0.92 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15316 0 0 0 36954 49 0 0 25 0 1 0 483780431 66088960 15145 4294967295 134512640 134672761 3221224528 3221223696 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16135 15145 603 41 0 16094 0
vsize: 64540
[startup+380.008 s]
Raw data (loadavg): 1.05 0.99 0.92 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15316 0 0 0 37954 49 0 0 25 0 1 0 483780431 66088960 15145 4294967295 134512640 134672761 3221224528 3221223632 134559866 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16135 15145 603 41 0 16094 0
vsize: 64540
[startup+390.009 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15316 0 0 0 38954 49 0 0 25 0 1 0 483780431 66088960 15145 4294967295 134512640 134672761 3221224528 3221223632 134560390 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16135 15145 603 41 0 16094 0
vsize: 64540
[startup+400.01 s]
Raw data (loadavg): 1.04 0.99 0.92 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15326 0 0 0 39955 49 0 0 25 0 1 0 483780431 66277376 15155 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16181 15155 603 41 0 16140 0
vsize: 64724
[startup+410.01 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15352 0 0 0 40955 49 0 0 25 0 1 0 483780431 66277376 15181 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16181 15181 603 41 0 16140 0
vsize: 64724
[startup+420.009 s]
Raw data (loadavg): 1.03 0.99 0.92 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15389 0 0 0 41955 49 0 0 25 0 1 0 483780431 66605056 15218 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16261 15218 603 41 0 16220 0
vsize: 65044
[startup+430.022 s]
Raw data (loadavg): 1.10 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15389 0 0 0 42956 49 0 0 25 0 1 0 483780431 66605056 15218 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16261 15218 603 41 0 16220 0
vsize: 65044
[startup+440.023 s]
Raw data (loadavg): 1.08 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15411 0 0 0 43957 49 0 0 25 0 1 0 483780431 66605056 15240 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16261 15240 603 41 0 16220 0
vsize: 65044
[startup+450.023 s]
Raw data (loadavg): 1.07 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15446 0 0 0 44957 49 0 0 25 0 1 0 483780431 66768896 15275 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16301 15275 603 41 0 16260 0
vsize: 65204
[startup+460.023 s]
Raw data (loadavg): 1.06 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15458 0 0 0 45957 49 0 0 25 0 1 0 483780431 66932736 15287 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16341 15287 603 41 0 16300 0
vsize: 65364
[startup+470.024 s]
Raw data (loadavg): 1.05 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15461 0 0 0 46957 49 0 0 25 0 1 0 483780431 66932736 15290 4294967295 134512640 134672761 3221224528 3221223696 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16341 15290 603 41 0 16300 0
vsize: 65364
[startup+480.023 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15469 0 0 0 47957 49 0 0 25 0 1 0 483780431 66932736 15298 4294967295 134512640 134672761 3221224528 3221223664 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16341 15298 603 41 0 16300 0
vsize: 65364
[startup+490.024 s]
Raw data (loadavg): 1.04 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15481 0 0 0 48957 49 0 0 25 0 1 0 483780431 66932736 15310 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16341 15310 603 41 0 16300 0
vsize: 65364
[startup+500.025 s]
Raw data (loadavg): 1.03 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15533 0 0 0 49957 49 0 0 25 0 1 0 483780431 67260416 15362 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16421 15362 603 41 0 16380 0
vsize: 65684
[startup+510.025 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15586 0 0 0 50957 50 0 0 25 0 1 0 483780431 67620864 15415 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16509 15415 603 41 0 16468 0
vsize: 66036
[startup+520.025 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15637 0 0 0 51957 50 0 0 25 0 1 0 483780431 67817472 15466 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16557 15466 603 41 0 16516 0
vsize: 66228
[startup+530.024 s]
Raw data (loadavg): 1.02 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15736 0 0 0 52956 50 0 0 25 0 1 0 483780431 68227072 15565 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16657 15565 603 41 0 16616 0
vsize: 66628
[startup+540.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 15915 0 0 0 53955 51 0 0 25 0 1 0 483780431 68902912 15744 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16822 15744 603 41 0 16781 0
vsize: 67288
[startup+550.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4471
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 16042 0 0 0 54955 52 0 0 25 0 1 0 483780431 69439488 15871 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16953 15871 603 41 0 16912 0
vsize: 67812
[startup+560.025 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 16185 0 0 0 55955 52 0 0 25 0 1 0 483780431 70160384 16014 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17129 16014 603 41 0 17088 0
vsize: 68516
[startup+570.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 16317 0 0 0 56955 53 0 0 25 0 1 0 483780431 70709248 16146 4294967295 134512640 134672761 3221224528 3221223712 134559592 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17263 16146 603 41 0 17222 0
vsize: 69052
[startup+580.026 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 16429 0 0 0 57954 53 0 0 25 0 1 0 483780431 71147520 16258 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17370 16258 603 41 0 17329 0
vsize: 69480
[startup+590.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 16580 0 0 0 58954 53 0 0 25 0 1 0 483780431 71831552 16409 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17537 16409 603 41 0 17496 0
vsize: 70148
[startup+600.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 16739 0 0 0 59954 54 0 0 25 0 1 0 483780431 72552448 16568 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17713 16568 603 41 0 17672 0
vsize: 70852
[startup+610.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17091 0 0 0 60953 55 0 0 25 0 1 0 483780431 73891840 16920 4294967295 134512640 134672761 3221224528 3221223664 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18040 16920 603 41 0 17999 0
vsize: 72160
[startup+620.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17329 0 0 0 61953 55 0 0 25 0 1 0 483780431 75010048 17158 4294967295 134512640 134672761 3221224528 3221223696 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18313 17158 603 41 0 18272 0
vsize: 73252
[startup+630.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17488 0 0 0 62953 56 0 0 25 0 1 0 483780431 75587584 17317 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18454 17317 603 41 0 18413 0
vsize: 73816
[startup+640.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17701 0 0 0 63951 57 0 0 25 0 1 0 483780431 76554240 17530 4294967295 134512640 134672761 3221224528 3221223652 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18690 17530 603 41 0 18649 0
vsize: 74760
[startup+650.027 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17749 0 0 0 64951 57 0 0 25 0 1 0 483780431 76689408 17578 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17578 603 41 0 18682 0
vsize: 74892
[startup+660.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17749 0 0 0 65951 57 0 0 25 0 1 0 483780431 76689408 17578 4294967295 134512640 134672761 3221224528 3221223528 1075349905 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17578 603 41 0 18682 0
vsize: 74892
[startup+670.026 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17749 0 0 0 66952 57 0 0 25 0 1 0 483780431 76689408 17578 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17578 603 41 0 18682 0
vsize: 74892
[startup+680.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 67952 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223652 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+690.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 68953 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+700.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 69953 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+710.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 70953 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+720.034 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 71953 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+730.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 72953 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223712 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+740.035 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 73954 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223696 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+750.036 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 74954 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+760.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17750 0 0 0 75954 57 0 0 25 0 1 0 483780431 76689408 17579 4294967295 134512640 134672761 3221224528 3221223680 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18723 17579 603 41 0 18682 0
vsize: 74892
[startup+770.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17767 0 0 0 76954 58 0 0 25 0 1 0 483780431 76828672 17596 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18757 17596 603 41 0 18716 0
vsize: 75028
[startup+780.041 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17801 0 0 0 77955 58 0 0 25 0 1 0 483780431 76992512 17630 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18797 17630 603 41 0 18756 0
vsize: 75188
[startup+790.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17814 0 0 0 78955 58 0 0 25 0 1 0 483780431 76992512 17643 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18797 17643 603 41 0 18756 0
vsize: 75188
[startup+800.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17832 0 0 0 79955 58 0 0 25 0 1 0 483780431 77189120 17661 4294967295 134512640 134672761 3221224528 3221223664 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18845 17661 603 41 0 18804 0
vsize: 75380
[startup+810.044 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17865 0 0 0 80955 58 0 0 25 0 1 0 483780431 77352960 17694 4294967295 134512640 134672761 3221224528 3221223696 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18885 17694 603 41 0 18844 0
vsize: 75540
[startup+820.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17886 0 0 0 81955 58 0 0 25 0 1 0 483780431 77516800 17715 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18925 17715 603 41 0 18884 0
vsize: 75700
[startup+830.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17901 0 0 0 82956 58 0 0 25 0 1 0 483780431 77516800 17730 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18925 17730 603 41 0 18884 0
vsize: 75700
[startup+840.045 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17925 0 0 0 83956 58 0 0 25 0 1 0 483780431 77713408 17754 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18973 17754 603 41 0 18932 0
vsize: 75892
[startup+850.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17935 0 0 0 84956 58 0 0 25 0 1 0 483780431 77713408 17764 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18973 17764 603 41 0 18932 0
vsize: 75892
[startup+860.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17949 0 0 0 85956 58 0 0 25 0 1 0 483780431 77713408 17778 4294967295 134512640 134672761 3221224528 3221223696 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18973 17778 603 41 0 18932 0
vsize: 75892
[startup+870.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17957 0 0 0 86956 58 0 0 25 0 1 0 483780431 77713408 17786 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18973 17786 603 41 0 18932 0
vsize: 75892
[startup+880.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17971 0 0 0 87956 58 0 0 25 0 1 0 483780431 77910016 17800 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19021 17800 603 41 0 18980 0
vsize: 76084
[startup+890.048 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 17973 0 0 0 88957 58 0 0 25 0 1 0 483780431 77910016 17802 4294967295 134512640 134672761 3221224528 3221223696 134560926 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19021 17802 603 41 0 18980 0
vsize: 76084
[startup+900.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 18023 0 0 0 89957 58 0 0 25 0 1 0 483780431 78106624 17852 4294967295 134512640 134672761 3221224528 3221223696 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19069 17852 603 41 0 19028 0
vsize: 76276
[startup+910.047 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 18031 0 0 0 90957 58 0 0 25 0 1 0 483780431 78106624 17860 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19069 17860 603 41 0 19028 0
vsize: 76276
[startup+920.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 18036 0 0 0 91958 58 0 0 25 0 1 0 483780431 78106624 17865 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19069 17865 603 41 0 19028 0
vsize: 76276
[startup+930.059 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 18216 0 0 0 92958 59 0 0 25 0 1 0 483780431 78909440 18045 4294967295 134512640 134672761 3221224528 3221223664 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19265 18045 603 41 0 19224 0
vsize: 77060
[startup+940.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 18488 0 0 0 93958 59 0 0 25 0 1 0 483780431 80027648 18317 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19538 18317 603 41 0 19497 0
vsize: 78152
[startup+950.061 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 18778 0 0 0 94958 59 0 0 25 0 1 0 483780431 81248256 18607 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19836 18607 603 41 0 19795 0
vsize: 79344
[startup+960.06 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 19096 0 0 0 95957 60 0 0 25 0 1 0 483780431 82599936 18925 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20166 18925 603 41 0 20125 0
vsize: 80664
[startup+970.07 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 19544 0 0 0 96921 61 0 0 25 0 1 0 483780431 84488192 19373 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20627 19373 603 41 0 20586 0
vsize: 82508
[startup+980.09 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20231 0 0 0 97920 63 0 0 25 0 1 0 483780431 87158784 20060 4294967295 134512640 134672761 3221224528 3221223696 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21279 20060 603 41 0 21238 0
vsize: 85116
[startup+990.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20633 0 0 0 98920 65 0 0 25 0 1 0 483780431 88817664 20462 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21684 20462 603 41 0 21643 0
vsize: 86736
[startup+1000.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20791 0 0 0 99920 66 0 0 25 0 1 0 483780431 89493504 20620 4294967295 134512640 134672761 3221224528 3221223632 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20620 603 41 0 21808 0
vsize: 87396
[startup+1010.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20791 0 0 0 100920 66 0 0 25 0 1 0 483780431 89493504 20620 4294967295 134512640 134672761 3221224528 3221223664 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20620 603 41 0 21808 0
vsize: 87396
[startup+1020.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20791 0 0 0 101920 66 0 0 25 0 1 0 483780431 89493504 20620 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20620 603 41 0 21808 0
vsize: 87396
[startup+1030.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20791 0 0 0 102920 66 0 0 25 0 1 0 483780431 89493504 20620 4294967295 134512640 134672761 3221224528 3221223696 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20620 603 41 0 21808 0
vsize: 87396
[startup+1040.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20793 0 0 0 103921 66 0 0 25 0 1 0 483780431 89493504 20622 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20622 603 41 0 21808 0
vsize: 87396
[startup+1050.11 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20796 0 0 0 104921 66 0 0 25 0 1 0 483780431 89493504 20625 4294967295 134512640 134672761 3221224528 3221223632 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20625 603 41 0 21808 0
vsize: 87396
[startup+1060.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20800 0 0 0 105922 66 0 0 25 0 1 0 483780431 89493504 20629 4294967295 134512640 134672761 3221224528 3221223632 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20629 603 41 0 21808 0
vsize: 87396
[startup+1070.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20801 0 0 0 106922 66 0 0 25 0 1 0 483780431 89493504 20630 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20630 603 41 0 21808 0
vsize: 87396
[startup+1080.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20804 0 0 0 107923 66 0 0 25 0 1 0 483780431 89493504 20633 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20633 603 41 0 21808 0
vsize: 87396
[startup+1090.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20804 0 0 0 108923 66 0 0 25 0 1 0 483780431 89493504 20633 4294967295 134512640 134672761 3221224528 3221223652 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20633 603 41 0 21808 0
vsize: 87396
[startup+1100.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20805 0 0 0 109923 66 0 0 25 0 1 0 483780431 89493504 20634 4294967295 134512640 134672761 3221224528 3221223696 134564686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20634 603 41 0 21808 0
vsize: 87396
[startup+1110.12 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20805 0 0 0 110923 66 0 0 25 0 1 0 483780431 89493504 20634 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20634 603 41 0 21808 0
vsize: 87396
[startup+1120.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20805 0 0 0 111923 66 0 0 25 0 1 0 483780431 89493504 20634 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20634 603 41 0 21808 0
vsize: 87396
[startup+1130.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20806 0 0 0 112924 66 0 0 25 0 1 0 483780431 89493504 20635 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20635 603 41 0 21808 0
vsize: 87396
[startup+1140.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20806 0 0 0 113924 66 0 0 25 0 1 0 483780431 89493504 20635 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20635 603 41 0 21808 0
vsize: 87396
[startup+1150.13 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20809 0 0 0 114924 66 0 0 25 0 1 0 483780431 89493504 20638 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20638 603 41 0 21808 0
vsize: 87396
[startup+1160.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20815 0 0 0 115925 66 0 0 25 0 1 0 483780431 89493504 20644 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20644 603 41 0 21808 0
vsize: 87396
[startup+1170.14 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20818 0 0 0 116925 66 0 0 25 0 1 0 483780431 89493504 20647 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20647 603 41 0 21808 0
vsize: 87396
[startup+1180.24 s]
Raw data (loadavg): 1.00 1.00 0.93 3/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20818 0 0 0 117936 66 0 0 25 0 1 0 483780431 89493504 20647 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20647 603 41 0 21808 0
vsize: 87396
[startup+1190.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20818 0 0 0 118936 66 0 0 25 0 1 0 483780431 89493504 20647 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20647 603 41 0 21808 0
vsize: 87396
[startup+1200.24 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 4473
Raw data (stat): 4416 (minisat+) R 4415 10720 10719 0 -1 0 20818 0 0 0 119936 66 0 0 25 0 1 0 483780431 89493504 20647 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21849 20647 603 41 0 21808 0
vsize: 87396
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.28 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 4473
Raw data (stat): 4416 (minisat+) Z 4415 10720 10719 0 -1 12 20820 0 0 0 119936 70 0 0 25 0 1 0 483780431 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.28
CPU time (s): 1200.07
CPU user time (s): 1199.37
CPU system time (s): 0.703892
CPU usage (%): 99.9824
Max. virtual memory (Kb): 87396
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####