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-pp08aCUTS.opb
MD5SUM	fa6454a9831f2da4180d8bfab7c0a21b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(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	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.037993
Number of variables	3288
Total number of constraints	310
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	310
Minimum length of a constraint	14
Maximum length of a constraint	123
Trace number 18100

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc5 THE 2005-04-21 13:32:52 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18771 boxname=wulflinc5 idbench=1444 idsolver=12 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fa6454a9831f2da4180d8bfab7c0a21b  /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-pp08aCUTS.opb
REAL COMMAND:  minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-pp08aCUTS.opb /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-13-7-pp08aCUTS.opb
IDLAUNCH: 18771
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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:        583396 kB
Buffers:         20368 kB
Cached:         408656 kB
SwapCached:        328 kB
Active:          58096 kB
Inactive:       373480 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        583144 kB
SwapTotal:     2097136 kB
SwapFree:      2096444 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5728 kB
Slab:            14040 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 13:52:54 (client local time) WITH STATUS 0 IN 1200.32 SECONDS
stats: 18771 7 1200.32 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 ---[ 437]---> BDD-cost: 1143
c ---[ 436]---> BDD-cost: 1143
c ---[ 435]---> BDD-cost: 1143
c ---[ 434]---> BDD-cost: 1165
c ---[ 433]---> BDD-cost: 1165
c ---[ 432]---> BDD-cost: 1165
c ---[ 431]---> BDD-cost: 1165
c ---[ 430]---> BDD-cost: 1176
c ---[ 428]---> BDD-cost:  158
c ---[ 426]---> BDD-cost:  585
c ---[ 424]---> BDD-cost:  585
c ---[ 422]---> BDD-cost:  580
c ---[ 420]---> BDD-cost:  580
c ---[ 418]---> BDD-cost:  570
c ---[ 416]---> BDD-cost:  537
c ---[ 414]---> BDD-cost:  183
c ---[ 412]---> BDD-cost:  178
c ---[ 410]---> BDD-cost:  566
c ---[ 408]---> BDD-cost:  576
c ---[ 406]---> BDD-cost:  576
c ---[ 404]---> BDD-cost:  576
c ---[ 402]---> BDD-cost:  529
c ---[ 400]---> BDD-cost:  566
c ---[ 398]---> BDD-cost:  181
c ---[ 396]---> BDD-cost:  180
c ---[ 394]---> BDD-cost:  585
c ---[ 392]---> BDD-cost:  537
c ---[ 390]---> BDD-cost:  580
c ---[ 388]---> BDD-cost:  575
c ---[ 386]---> BDD-cost:  570
c ---[ 384]---> BDD-cost:  585
c ---[ 382]---> BDD-cost:  174
c ---[ 380]---> BDD-cost:  158
c ---[ 378]---> BDD-cost:  580
c ---[ 376]---> BDD-cost:  580
c ---[ 374]---> BDD-cost:  585
c ---[ 372]---> BDD-cost:  565
c ---[ 370]---> BDD-cost:  585
c ---[ 368]---> BDD-cost:  580
c ---[ 366]---> BDD-cost:  183
c ---[ 364]---> BDD-cost:  181
c ---[ 362]---> BDD-cost:  529
c ---[ 360]---> BDD-cost:  571
c ---[ 358]---> BDD-cost:  566
c ---[ 356]---> BDD-cost:  576
c ---[ 354]---> BDD-cost:  576
c ---[ 352]---> BDD-cost:  571
c ---[ 350]---> BDD-cost:  181
c ---[ 348]---> BDD-cost:  186
c ---[ 346]---> BDD-cost:  575
c ---[ 344]---> BDD-cost:  575
c ---[ 342]---> BDD-cost:  575
c ---[ 340]---> BDD-cost:  580
c ---[ 338]---> BDD-cost:  580
c ---[ 336]---> BDD-cost:  575
c ---[ 334]---> BDD-cost:  186
c ---[ 332]---> BDD-cost:  154
c ---[ 330]---> BDD-cost:  571
c ---[ 328]---> BDD-cost:  576
c ---[ 326]---> BDD-cost:  576
c ---[ 324]---> BDD-cost:  571
c ---[ 322]---> BDD-cost:  571
c ---[ 320]---> BDD-cost:  566
c ---[ 318]---> BDD-cost:  175
c ---[ 316]---> BDD-cost:  176
c ---[ 314]---> BDD-cost:  562
c ---[ 312]---> BDD-cost:  521
c ---[ 310]---> BDD-cost:  521
c ---[ 308]---> BDD-cost:  567
c ---[ 306]---> BDD-cost:  567
c ---[ 304]---> BDD-cost:  562
c ---[ 302]---> BDD-cost:  176
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    6
c ---[ 297]---> BDD-cost:    6
c ---[ 296]---> BDD-cost:    6
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    8
c ---[ 293]---> BDD-cost:   19
c ---[ 292]---> BDD-cost:   19
c ---[ 291]---> BDD-cost:   19
c ---[ 290]---> BDD-cost:   19
c ---[ 289]---> BDD-cost:   19
c ---[ 288]---> BDD-cost:   19
c ---[ 287]---> BDD-cost:   19
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    6
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:    6
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:   23
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    6
c ---[ 272]---> BDD-cost:    6
c ---[ 271]---> BDD-cost:    6
c ---[ 270]---> BDD-cost:   23
c ---[ 269]---> BDD-cost:    4
c ---[ 268]---> BDD-cost:    4
c ---[ 267]---> BDD-cost:    4
c ---[ 266]---> BDD-cost:    4
c ---[ 265]---> BDD-cost:    4
c ---[ 264]---> BDD-cost:    4
c ---[ 263]---> BDD-cost:    4
c ---[ 262]---> BDD-cost:    4
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    6
c ---[ 257]---> BDD-cost:    6
c ---[ 256]---> BDD-cost:    6
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    6
c ---[ 253]---> BDD-cost:   19
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:   19
c ---[ 250]---> BDD-cost:   19
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   19
c ---[ 247]---> BDD-cost:   19
c ---[ 246]---> BDD-cost:   19
c ---[ 245]---> BDD-cost:    6
c ---[ 244]---> BDD-cost:    6
c ---[ 243]---> BDD-cost:    6
c ---[ 242]---> BDD-cost:    6
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    6
c ---[ 239]---> BDD-cost:    6
c ---[ 238]---> BDD-cost:    6
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:  167
c ---[ 107]---> BDD-cost:   59
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:  149
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:  152
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:  152
c ---[ 100]---> BDD-cost:   38
c ---[  99]---> BDD-cost:  149
c ---[  98]---> BDD-cost:    4
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   62
c ---[  95]---> BDD-cost:   73
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:   62
c ---[  92]---> BDD-cost:   41
c ---[  91]---> BDD-cost:  158
c ---[  90]---> BDD-cost:   45
c ---[  89]---> BDD-cost:  182
c ---[  88]---> BDD-cost:   40
c ---[  87]---> BDD-cost:  203
c ---[  86]---> BDD-cost:  173
c ---[  85]---> BDD-cost:   35
c ---[  84]---> BDD-cost:  164
c ---[  83]---> BDD-cost:   41
c ---[  82]---> BDD-cost:  158
c ---[  81]---> BDD-cost:    5
c ---[  80]---> BDD-cost:   70
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:   65
c ---[  77]---> BDD-cost:   45
c ---[  76]---> BDD-cost:   45
c ---[  75]---> BDD-cost:  194
c ---[  74]---> BDD-cost:   48
c ---[  73]---> BDD-cost:  191
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:  170
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:  167
c ---[  68]---> BDD-cost:   50
c ---[  67]---> BDD-cost:  203
c ---[  66]---> BDD-cost:    3
c ---[  65]---> BDD-cost:  194
c ---[  64]---> BDD-cost:   61
c ---[  63]---> BDD-cost:   48
c ---[  62]---> BDD-cost:  191
c ---[  61]---> BDD-cost:   48
c ---[  60]---> BDD-cost:  191
c ---[  59]---> BDD-cost:   55
c ---[  58]---> BDD-cost:  209
c ---[  57]---> BDD-cost:   47
c ---[  56]---> BDD-cost:  161
c ---[  55]---> BDD-cost:   50
c ---[  54]---> BDD-cost:   48
c ---[  53]---> BDD-cost:  203
c ---[  52]---> BDD-cost:   48
c ---[  51]---> BDD-cost:  191
c ---[  50]---> BDD-cost:    5
c ---[  49]---> BDD-cost:   73
c ---[  48]---> BDD-cost:    5
c ---[  47]---> BDD-cost:   70
c ---[  46]---> BDD-cost:   38
c ---[  45]---> BDD-cost:  161
c ---[  44]---> BDD-cost:   41
c ---[  43]---> BDD-cost:  191
c ---[  42]---> BDD-cost:  158
c ---[  41]---> BDD-cost:   35
c ---[  40]---> BDD-cost:  164
c ---[  39]---> BDD-cost:   35
c ---[  38]---> BDD-cost:  164
c ---[  37]---> BDD-cost:   38
c ---[  36]---> BDD-cost:  161
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   64
c ---[  33]---> BDD-cost:    6
c ---[  32]---> BDD-cost:   38
c ---[  31]---> BDD-cost:   78
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:  170
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:  170
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:  170
c ---[  24]---> BDD-cost:   48
c ---[  23]---> BDD-cost:  191
c ---[  22]---> BDD-cost:   38
c ---[  21]---> BDD-cost:  173
c ---[  20]---> BDD-cost:  173
c ---[  19]---> BDD-cost:   41
c ---[  18]---> BDD-cost:  170
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:   75
c ---[  15]---> BDD-cost:   38
c ---[  14]---> BDD-cost:  161
c ---[  13]---> BDD-cost:   45
c ---[  12]---> BDD-cost:  182
c ---[  11]---> BDD-cost:   35
c ---[  10]---> BDD-cost:   44
c ---[   9]---> BDD-cost:  164
c ---[   8]---> BDD-cost:   38
c ---[   7]---> BDD-cost:  161
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:  170
c ---[   4]---> BDD-cost:   41
c ---[   3]---> BDD-cost:  158
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:   60
c ---[   0]---> BDD-cost:    3
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      799     8.0 |  0.600 % |
c |       250 |  129110   364299 |   52073     250     2158     8.6 |  0.600 % |
c |       475 |  129110   364299 |   57280     475     5727    12.1 |  0.600 % |
c |       813 |  129110   364299 |   63009     813     9886    12.2 |  0.600 % |
c |      1319 |  129110   364299 |   69309    1319    17297    13.1 |  0.600 % |
c |      2078 |  129110   364299 |   76240    2078    25817    12.4 |  0.600 % |
c |      3219 |  129110   364299 |   83864    3219    42596    13.2 |  0.600 % |
c |      4928 |  129110   364299 |   92251    4928    84040    17.1 |  0.600 % |
c |      7490 |  129110   364299 |  101476    7490   136362    18.2 |  0.600 % |
c |     11334 |  129110   364299 |  111624   11334   219706    19.4 |  0.600 % |
c |     17101 |  129110   364299 |  122786   17101   379653    22.2 |  0.600 % |
c |     25750 |  129110   364299 |  135065   25750   611736    23.8 |  0.600 % |
c |     38724 |  129110   364299 |  148571   38724  1063573    27.5 |  0.600 % |
c |     58185 |  129093   364265 |  163429   58184  1402464    24.1 |  0.614 % |
c |     87377 |  129093   364265 |  179772   87376  2050371    23.5 |  0.614 % |
c |    131166 |  129086   364251 |  197749  131163  3100075    23.6 |  0.620 % |
c |    196850 |  129086   364251 |  217524  196847  5126454    26.0 |  0.620 % |
c |    295376 |  129086   364251 |  239276   83822  2179340    26.0 |  0.620 % |
c |    443165 |  129086   364251 |  263204  231611  5859007    25.3 |  0.620 % |
c |    664848 |  129086   364251 |  289524  206876  6741461    32.6 |  0.620 % |
c |    997373 |  129082   364243 |  318477  271910  6657993    24.5 |  0.623 % |
#### 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): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (runsolver) R 23045 24215 24214 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487246575 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.0001 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 5497 0 0 0 985 13 0 0 25 0 1 0 487246575 24506368 5334 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5983 5334 603 41 0 5942 0
vsize: 23932
[startup+20.0008 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 6477 0 0 0 1982 15 0 0 25 0 1 0 487246575 28545024 6314 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6969 6314 603 41 0 6928 0
vsize: 27876
[startup+30.0012 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 7357 0 0 0 2980 17 0 0 25 0 1 0 487246575 32432128 7194 4294967295 134512640 134672761 3221224528 3221223664 134560661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7918 7194 603 41 0 7877 0
vsize: 31672
[startup+40.0013 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 7969 0 0 0 3978 19 0 0 25 0 1 0 487246575 34848768 7806 4294967295 134512640 134672761 3221224528 3221223696 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8508 7806 603 41 0 8467 0
vsize: 34032
[startup+50.002 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 8669 0 0 0 4977 21 0 0 25 0 1 0 487246575 37691392 8506 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9202 8506 603 41 0 9161 0
vsize: 36808
[startup+60.0016 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 9283 0 0 0 5975 23 0 0 25 0 1 0 487246575 40628224 9120 4294967295 134512640 134672761 3221224528 3221223664 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9919 9120 603 41 0 9878 0
vsize: 39676
[startup+70.0026 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 10037 0 0 0 6973 24 0 0 25 0 1 0 487246575 43589632 9874 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10642 9874 603 41 0 10601 0
vsize: 42568
[startup+80.0033 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 10673 0 0 0 7970 27 0 0 25 0 1 0 487246575 46157824 10510 4294967295 134512640 134672761 3221224528 3221223696 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11269 10510 603 41 0 11228 0
vsize: 45076
[startup+90.0027 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 11157 0 0 0 8969 29 0 0 25 0 1 0 487246575 48214016 10994 4294967295 134512640 134672761 3221224528 3221223712 134558632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11771 10994 603 41 0 11730 0
vsize: 47084
[startup+100.003 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 11588 0 0 0 9967 30 0 0 25 0 1 0 487246575 49995776 11425 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12206 11425 603 41 0 12165 0
vsize: 48824
[startup+110.004 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 11921 0 0 0 10967 31 0 0 25 0 1 0 487246575 51388416 11758 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12546 11758 603 41 0 12505 0
vsize: 50184
[startup+120.004 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12248 0 0 0 11966 32 0 0 25 0 1 0 487246575 52596736 12085 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12841 12085 603 41 0 12800 0
vsize: 51364
[startup+130.004 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12675 0 0 0 12965 33 0 0 25 0 1 0 487246575 54329344 12512 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13264 12512 603 41 0 13223 0
vsize: 53056
[startup+140.004 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12844 0 0 0 13965 33 0 0 25 0 1 0 487246575 55070720 12681 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12681 603 41 0 13404 0
vsize: 53780
[startup+150.004 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12844 0 0 0 14965 33 0 0 25 0 1 0 487246575 55070720 12681 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12681 603 41 0 13404 0
vsize: 53780
[startup+160.004 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12844 0 0 0 15965 33 0 0 25 0 1 0 487246575 55070720 12681 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12681 603 41 0 13404 0
vsize: 53780
[startup+170.005 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12844 0 0 0 16966 33 0 0 25 0 1 0 487246575 55070720 12681 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12681 603 41 0 13404 0
vsize: 53780
[startup+180.006 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12844 0 0 0 17966 33 0 0 25 0 1 0 487246575 55070720 12681 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12681 603 41 0 13404 0
vsize: 53780
[startup+190.006 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12844 0 0 0 18966 33 0 0 25 0 1 0 487246575 55070720 12681 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12681 603 41 0 13404 0
vsize: 53780
[startup+200.006 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 19966 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223664 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+210.007 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 20967 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223696 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+220.008 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 21967 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+230.007 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 22967 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223696 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+240.007 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 23967 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223672 134560630 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+250.008 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 24967 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223712 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+260.008 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 25967 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+270.008 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 26968 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+280.008 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 27968 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+290.008 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12845 0 0 0 28968 33 0 0 25 0 1 0 487246575 55070720 12682 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13445 12682 603 41 0 13404 0
vsize: 53780
[startup+300.009 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 12929 0 0 0 29968 34 0 0 25 0 1 0 487246575 55525376 12766 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13556 12766 603 41 0 13515 0
vsize: 54224
[startup+310.009 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 13094 0 0 0 30967 34 0 0 25 0 1 0 487246575 56201216 12931 4294967295 134512640 134672761 3221224528 3221223680 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13721 12931 603 41 0 13680 0
vsize: 54884
[startup+320.009 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 13253 0 0 0 31967 35 0 0 25 0 1 0 487246575 56909824 13090 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13894 13090 603 41 0 13853 0
vsize: 55576
[startup+330.01 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 13443 0 0 0 32966 36 0 0 25 0 1 0 487246575 57733120 13280 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14095 13280 603 41 0 14054 0
vsize: 56380
[startup+340.01 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 13605 0 0 0 33966 37 0 0 25 0 1 0 487246575 58351616 13442 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14246 13442 603 41 0 14205 0
vsize: 56984
[startup+350.01 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 13777 0 0 0 34965 38 0 0 25 0 1 0 487246575 59166720 13614 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14445 13614 603 41 0 14404 0
vsize: 57780
[startup+360.01 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 13943 0 0 0 35965 38 0 0 25 0 1 0 487246575 59838464 13780 4294967295 134512640 134672761 3221224528 3221223712 134559424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14609 13780 603 41 0 14568 0
vsize: 58436
[startup+370.011 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 14458 0 0 0 36963 39 0 0 25 0 1 0 487246575 61886464 14295 4294967295 134512640 134672761 3221224528 3221223696 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15109 14295 603 41 0 15068 0
vsize: 60436
[startup+380.012 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 14971 0 0 0 37963 40 0 0 25 0 1 0 487246575 63885312 14808 4294967295 134512640 134672761 3221224528 3221223728 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15597 14808 603 41 0 15556 0
vsize: 62388
[startup+390.011 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15050 0 0 0 38963 40 0 0 25 0 1 0 487246575 65339392 14887 4294967295 134512640 134672761 3221224528 3221223632 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14887 603 41 0 15911 0
vsize: 63808
[startup+400.012 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15050 0 0 0 39963 40 0 0 25 0 1 0 487246575 65339392 14887 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14887 603 41 0 15911 0
vsize: 63808
[startup+410.012 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15054 0 0 0 40963 40 0 0 25 0 1 0 487246575 65339392 14891 4294967295 134512640 134672761 3221224528 3221223696 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14891 603 41 0 15911 0
vsize: 63808
[startup+420.013 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15054 0 0 0 41963 40 0 0 25 0 1 0 487246575 65339392 14891 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14891 603 41 0 15911 0
vsize: 63808
[startup+430.013 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15054 0 0 0 42963 40 0 0 25 0 1 0 487246575 65339392 14891 4294967295 134512640 134672761 3221224528 3221223696 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14891 603 41 0 15911 0
vsize: 63808
[startup+440.013 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15054 0 0 0 43964 40 0 0 25 0 1 0 487246575 65339392 14891 4294967295 134512640 134672761 3221224528 3221223696 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14891 603 41 0 15911 0
vsize: 63808
[startup+450.014 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15054 0 0 0 44964 40 0 0 25 0 1 0 487246575 65339392 14891 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14891 603 41 0 15911 0
vsize: 63808
[startup+460.014 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15055 0 0 0 45964 40 0 0 25 0 1 0 487246575 65339392 14892 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14892 603 41 0 15911 0
vsize: 63808
[startup+470.014 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15055 0 0 0 46964 40 0 0 25 0 1 0 487246575 65339392 14892 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14892 603 41 0 15911 0
vsize: 63808
[startup+480.015 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15055 0 0 0 47965 40 0 0 25 0 1 0 487246575 65339392 14892 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14892 603 41 0 15911 0
vsize: 63808
[startup+490.015 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15061 0 0 0 48965 40 0 0 25 0 1 0 487246575 65339392 14898 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14898 603 41 0 15911 0
vsize: 63808
[startup+500.015 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15070 0 0 0 49965 40 0 0 25 0 1 0 487246575 65339392 14907 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15952 14907 603 41 0 15911 0
vsize: 63808
[startup+510.015 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15089 0 0 0 50965 40 0 0 25 0 1 0 487246575 65527808 14926 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15998 14926 603 41 0 15957 0
vsize: 63992
[startup+520.016 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15360 0 0 0 51964 41 0 0 25 0 1 0 487246575 66596864 15197 4294967295 134512640 134672761 3221224528 3221223652 134566054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16259 15197 603 41 0 16218 0
vsize: 65036
[startup+530.016 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 15684 0 0 0 52964 42 0 0 25 0 1 0 487246575 67952640 15521 4294967295 134512640 134672761 3221224528 3221223696 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16590 15521 603 41 0 16549 0
vsize: 66360
[startup+540.016 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 16313 0 0 0 53961 44 0 0 25 0 1 0 487246575 70492160 16150 4294967295 134512640 134672761 3221224528 3221223720 134557982 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17210 16150 603 41 0 17169 0
vsize: 68840
[startup+550.016 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 16537 0 0 0 54959 46 0 0 25 0 1 0 487246575 71446528 16374 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17443 16374 603 41 0 17402 0
vsize: 69772
[startup+560.016 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 16715 0 0 0 55959 46 0 0 25 0 1 0 487246575 72253440 16552 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17640 16552 603 41 0 17599 0
vsize: 70560
[startup+570.017 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 16919 0 0 0 56959 47 0 0 25 0 1 0 487246575 73056256 16756 4294967295 134512640 134672761 3221224528 3221223696 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17836 16756 603 41 0 17795 0
vsize: 71344
[startup+580.018 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 17313 0 0 0 57958 48 0 0 25 0 1 0 487246575 74682368 17150 4294967295 134512640 134672761 3221224528 3221223632 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18233 17150 603 41 0 18192 0
vsize: 72932
[startup+590.017 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 17568 0 0 0 58958 48 0 0 25 0 1 0 487246575 75755520 17405 4294967295 134512640 134672761 3221224528 3221223692 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18495 17406 603 41 0 18454 0
vsize: 73980
[startup+600.017 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 17925 0 0 0 59957 49 0 0 25 0 1 0 487246575 77086720 17762 4294967295 134512640 134672761 3221224528 3221223632 134560177 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18820 17762 603 41 0 18779 0
vsize: 75280
[startup+610.018 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18330 0 0 0 60957 50 0 0 25 0 1 0 487246575 78704640 18167 4294967295 134512640 134672761 3221224528 3221223696 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19215 18167 603 41 0 19174 0
vsize: 76860
[startup+620.018 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 61956 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223632 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+630.018 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 62957 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+640.018 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 63957 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+650.019 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 64957 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+660.019 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 65957 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+670.019 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 66957 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+680.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 67958 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223632 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+690.019 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 68958 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223704 134559668 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+700.019 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 69958 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223712 134559415 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+710.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 70958 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223632 134559847 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+720.021 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 71958 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223652 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+730.022 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 72959 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+740.021 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 73959 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134561261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+750.022 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 74959 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223712 134559417 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+760.022 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 75959 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+770.022 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 76959 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+780.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 77960 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+790.023 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18447 0 0 0 78960 50 0 0 25 0 1 0 487246575 79286272 18284 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18284 603 41 0 19316 0
vsize: 77428
[startup+800.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18450 0 0 0 79960 50 0 0 25 0 1 0 487246575 79286272 18287 4294967295 134512640 134672761 3221224528 3221223696 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18287 603 41 0 19316 0
vsize: 77428
[startup+810.023 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18450 0 0 0 80960 50 0 0 25 0 1 0 487246575 79286272 18287 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18287 603 41 0 19316 0
vsize: 77428
[startup+820.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18461 0 0 0 81960 51 0 0 25 0 1 0 487246575 79286272 18298 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19357 18298 603 41 0 19316 0
vsize: 77428
[startup+830.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18461 0 0 0 82960 51 0 0 25 0 1 0 487246575 79286272 18298 4294967295 134512640 134672761 3221224528 3221223696 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18298 603 41 0 19316 0
vsize: 77428
[startup+840.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 18472 0 0 0 83960 51 0 0 25 0 1 0 487246575 79286272 18309 4294967295 134512640 134672761 3221224528 3221223696 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 18309 603 41 0 19316 0
vsize: 77428
[startup+850.025 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19011 0 0 0 84959 52 0 0 25 0 1 0 487246575 81444864 18848 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19884 18848 603 41 0 19843 0
vsize: 79536
[startup+860.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 85957 53 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223616 134565852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+870.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 86957 53 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223696 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+880.025 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 87958 53 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223712 134559622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+890.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 88958 53 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223692 134565030 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+900.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 89958 54 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223696 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+910.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 90958 54 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223696 134561406 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+920.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 91958 54 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223744 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+930.023 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 92958 54 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223652 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+940.023 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 93959 54 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+950.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19561 0 0 0 94959 54 0 0 25 0 1 0 487246575 83730432 19398 4294967295 134512640 134672761 3221224528 3221223696 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20442 19398 603 41 0 20401 0
vsize: 81768
[startup+960.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19573 0 0 0 95959 54 0 0 25 0 1 0 487246575 83865600 19410 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20475 19410 603 41 0 20434 0
vsize: 81900
[startup+970.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19575 0 0 0 96959 54 0 0 25 0 1 0 487246575 83865600 19412 4294967295 134512640 134672761 3221224528 3221223664 134560619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20475 19412 603 41 0 20434 0
vsize: 81900
[startup+980.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19575 0 0 0 97959 54 0 0 25 0 1 0 487246575 83865600 19412 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20475 19412 603 41 0 20434 0
vsize: 81900
[startup+990.024 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19576 0 0 0 98959 54 0 0 25 0 1 0 487246575 83865600 19413 4294967295 134512640 134672761 3221224528 3221223696 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20475 19413 603 41 0 20434 0
vsize: 81900
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19587 0 0 0 99960 54 0 0 25 0 1 0 487246575 83865600 19424 4294967295 134512640 134672761 3221224528 3221223696 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20475 19424 603 41 0 20434 0
vsize: 81900
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19597 0 0 0 100960 54 0 0 25 0 1 0 487246575 83865600 19434 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20475 19434 603 41 0 20434 0
vsize: 81900
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19607 0 0 0 101960 54 0 0 25 0 1 0 487246575 84013056 19444 4294967295 134512640 134672761 3221224528 3221223696 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20511 19444 603 41 0 20470 0
vsize: 82044
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19626 0 0 0 102960 54 0 0 25 0 1 0 487246575 84013056 19463 4294967295 134512640 134672761 3221224528 3221223696 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20511 19463 603 41 0 20470 0
vsize: 82044
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19644 0 0 0 103960 54 0 0 25 0 1 0 487246575 84176896 19481 4294967295 134512640 134672761 3221224528 3221223696 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20551 19481 603 41 0 20510 0
vsize: 82204
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19658 0 0 0 104960 54 0 0 25 0 1 0 487246575 84176896 19495 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20551 19495 603 41 0 20510 0
vsize: 82204
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19674 0 0 0 105960 54 0 0 25 0 1 0 487246575 84340736 19511 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20591 19511 603 41 0 20550 0
vsize: 82364
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19688 0 0 0 106960 54 0 0 25 0 1 0 487246575 84340736 19525 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20591 19525 603 41 0 20550 0
vsize: 82364
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19720 0 0 0 107960 54 0 0 25 0 1 0 487246575 84504576 19557 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20631 19557 603 41 0 20590 0
vsize: 82524
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19780 0 0 0 108960 54 0 0 25 0 1 0 487246575 84766720 19617 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20695 19617 603 41 0 20654 0
vsize: 82780
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19793 0 0 0 109960 55 0 0 25 0 1 0 487246575 84766720 19630 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20695 19630 603 41 0 20654 0
vsize: 82780
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19832 0 0 0 110960 55 0 0 25 0 1 0 487246575 85028864 19669 4294967295 134512640 134672761 3221224528 3221223696 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20759 19669 603 41 0 20718 0
vsize: 83036
[startup+1120.03 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19880 0 0 0 111961 55 0 0 25 0 1 0 487246575 85291008 19717 4294967295 134512640 134672761 3221224528 3221223696 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20823 19717 603 41 0 20782 0
vsize: 83292
[startup+1130.13 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19886 0 0 0 112971 55 0 0 25 0 1 0 487246575 85291008 19723 4294967295 134512640 134672761 3221224528 3221223696 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20823 19723 603 41 0 20782 0
vsize: 83292
[startup+1140.13 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19891 0 0 0 113971 55 0 0 25 0 1 0 487246575 85291008 19728 4294967295 134512640 134672761 3221224528 3221223696 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20823 19728 603 41 0 20782 0
vsize: 83292
[startup+1150.13 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19945 0 0 0 114971 55 0 0 25 0 1 0 487246575 85553152 19782 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20887 19782 603 41 0 20846 0
vsize: 83548
[startup+1160.13 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19947 0 0 0 115972 55 0 0 25 0 1 0 487246575 85553152 19784 4294967295 134512640 134672761 3221224528 3221223696 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20887 19784 603 41 0 20846 0
vsize: 83548
[startup+1170.13 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19947 0 0 0 116972 55 0 0 25 0 1 0 487246575 85553152 19784 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20887 19784 603 41 0 20846 0
vsize: 83548
[startup+1180.13 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19956 0 0 0 117972 55 0 0 25 0 1 0 487246575 85749760 19793 4294967295 134512640 134672761 3221224528 3221223696 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20935 19793 603 41 0 20894 0
vsize: 83740
[startup+1190.13 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 19992 0 0 0 118972 55 0 0 25 0 1 0 487246575 85880832 19829 4294967295 134512640 134672761 3221224528 3221223696 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20967 19829 603 41 0 20926 0
vsize: 83868
[startup+1200.13 s]
Raw data (loadavg): 1.00 0.97 0.95 2/54 23046
Raw data (stat): 23046 (minisat+) R 23045 24215 24214 0 -1 0 20196 0 0 0 119971 56 0 0 25 0 1 0 487246575 86691840 20033 4294967295 134512640 134672761 3221224528 3221223632 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21165 20033 603 41 0 21124 0
vsize: 84660
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.97 0.95 1/54 23046
Raw data (stat): 23046 (minisat+) Z 23045 24215 24214 0 -1 12 20198 0 0 0 119971 60 0 0 25 0 1 0 487246575 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.17
CPU time (s): 1200.32
CPU user time (s): 1199.72
CPU system time (s): 0.602908
CPU usage (%): 100.013
Max. virtual memory (Kb): 84660
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####