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:
  1. 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.
  2. SOLVER DATA
    This is the output of the solver (stdout and stderr).
  3. 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.
  4. 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

Namenormalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm2.opb
MD5SUMfae1fae180d772ad3ee6c1acfa1c8b4f
Bench Categoryoptimization, medium integers (OPTMEDINT)
Has Objective FunctionYES
SatisfiableYES
(Un)Satisfiability was provedYES
Best value of the objective function 122
Optimality of the best value was proved NO
Number of terms in the objective function 168
Biggest coefficient in the objective function 5
Number of bits for the biggest coefficient in the objective function 3
Sum of the numbers in the objective function 504
Number of bits of the sum of numbers in the objective function 9
Biggest number in a constraint 2000000
Number of bits of the biggest number in a constraint 21
Biggest sum of numbers in a constraint 30041153
Number of bits of the biggest sum of numbers25
Best result obtained on this benchmarkSAT
Best CPU time to get the best result obtained on this benchmark1189.01
Number of variables2124
Total number of constraints444
Number of constraints which are clauses0
Number of constraints which are cardinality constraints (but not clauses)0
Number of constraints which are nor clauses,nor cardinality constraints444
Minimum length of a constraint8
Maximum length of a constraint64

Trace number 17894 

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 12:29:07 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18954 boxname=wulflinc2 idbench=1458 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fae1fae180d772ad3ee6c1acfa1c8b4f  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 18954
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        683468 kB
Buffers:         20744 kB
Cached:         309368 kB
SwapCached:        504 kB
Active:          56748 kB
Inactive:       275616 kB
HighTotal:      131008 kB
HighFree:         3304 kB
LowTotal:       903652 kB
LowFree:        680164 kB
SwapTotal:     2097136 kB
SwapFree:      2095900 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5712 kB
Slab:            13252 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 12:49:09 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 18954 7 1200.23 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 1826     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 246]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 244]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 242]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 224]---> Sorter-cost: 1582     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 212]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 210]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Sorter-cost: 1882     Base: 2 2 2 2 5 5 2 2 2 5
c ---[ 198]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> BDD-cost:  110
c ---[ 190]---> BDD-cost:  237
c ---[ 189]---> BDD-cost:  236
c ---[ 188]---> BDD-cost:  393
c ---[ 187]---> BDD-cost:  495
c ---[ 186]---> BDD-cost:  488
c ---[ 185]---> BDD-cost:  131
c ---[ 184]---> BDD-cost:  262
c ---[ 183]---> BDD-cost:  261
c ---[ 182]---> BDD-cost:  448
c ---[ 181]---> BDD-cost:  550
c ---[ 180]---> BDD-cost:  549
c ---[ 179]---> Sorter-cost:  338     Base: 2 2 2 2 2 2 5
c ---[ 178]---> Sorter-cost:  867     Base: 2 2 5 2 2 2 2
c ---[ 177]---> Sorter-cost:  830     Base: 2 2 2 2 2 2 5
c ---[ 176]---> Sorter-cost: 1298     Base: 2 2 5 2 2 2 2
c ---[ 175]---> Sorter-cost: 1687     Base: 2 2 5 2 2 2 2
c ---[ 174]---> Sorter-cost: 1665     Base: 2 2 5 2 2 2 2
c ---[ 173]---> Sorter-cost:  196     Base: 2 2 2 2 2 2
c ---[ 172]---> Sorter-cost:  473     Base: 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  421     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  764     Base: 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  884     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1063     Base: 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    6
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  171914   438955 |   57304       0        0     nan |  0.000 % |
c |       101 |  171914   438955 |   63034     101     1001     9.9 |  5.566 % |
c |       252 |  171791   438675 |   69337     248     2345     9.5 |  5.623 % |
c |       477 |  171541   438100 |   76271     449     3928     8.7 |  5.744 % |
c |       814 |  171187   437302 |   83898     775     7562     9.8 |  5.924 % |
c |      1321 |  170829   436477 |   92288    1271    13765    10.8 |  6.106 % |
c |      2080 |  170598   435950 |  101517    2021    21656    10.7 |  6.216 % |
c |      3220 |  170530   435797 |  111669    3156    55001    17.4 |  6.247 % |
c |      4930 |  170429   435550 |  122836    4862    93655    19.3 |  6.294 % |
c |      7493 |  169823   434126 |  135119    7404   145332    19.6 |  6.602 % |
c |     11337 |  169637   433669 |  148631   11228   383378    34.1 |  6.688 % |
c |     17103 |  168492   431021 |  163494   16646   515757    31.0 |  7.263 % |
c |     25755 |  168025   429942 |  179844   25264   732209    29.0 |  7.495 % |
c |     38729 |  167812   429389 |  197828   38217  1140055    29.8 |  7.586 % |
c |     58190 |  167747   429234 |  217611   57667  1865338    32.3 |  7.620 % |
c |     87382 |  166979   427431 |  239373   86776  2824138    32.5 |  8.023 % |
c |    131174 |  165780   424621 |  263310  130431  4861292    37.3 |  8.615 % |
c |    196858 |  163183   418614 |  289641  195819  7393699    37.8 |  9.952 % |
c |    295384 |  161917   415676 |  318605  294054 11827548    40.2 | 10.638 % |
#### 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.84 0.95 0.92 2/54 27359
Raw data (stat): 27359 (runsolver) R 27358 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486865759 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99947 s]
Raw data (loadavg): 0.87 0.95 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 5130 0 0 0 985 12 0 0 25 0 1 0 486865759 22867968 4950 4294967295 134512640 134672761 3221224560 3221223696 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5583 4950 603 41 0 5542 0
vsize: 22332
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.95 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 5493 0 0 0 1984 14 0 0 25 0 1 0 486865759 24363008 5313 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5948 5313 603 41 0 5907 0
vsize: 23792
[startup+30.0012 s]
Raw data (loadavg): 0.90 0.95 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 5724 0 0 0 2981 16 0 0 25 0 1 0 486865759 25292800 5544 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6175 5544 603 41 0 6134 0
vsize: 24700
[startup+40.001 s]
Raw data (loadavg): 0.92 0.95 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 5891 0 0 0 3981 17 0 0 25 0 1 0 486865759 25960448 5711 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6338 5711 603 41 0 6297 0
vsize: 25352
[startup+50.0012 s]
Raw data (loadavg): 0.93 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 6330 0 0 0 4980 18 0 0 25 0 1 0 486865759 27951104 6150 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6824 6150 603 41 0 6783 0
vsize: 27296
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 6653 0 0 0 5979 19 0 0 25 0 1 0 486865759 29138944 6473 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7114 6473 603 41 0 7073 0
vsize: 28456
[startup+70.0017 s]
Raw data (loadavg): 0.95 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 6946 0 0 0 6979 20 0 0 25 0 1 0 486865759 30343168 6766 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7408 6766 603 41 0 7367 0
vsize: 29632
[startup+80.0024 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 7165 0 0 0 7978 20 0 0 25 0 1 0 486865759 31285248 6985 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7638 6985 603 41 0 7597 0
vsize: 30552
[startup+90.0024 s]
Raw data (loadavg): 0.96 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 7384 0 0 0 8978 21 0 0 25 0 1 0 486865759 32227328 7204 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7868 7204 603 41 0 7827 0
vsize: 31472
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 7604 0 0 0 9977 22 0 0 25 0 1 0 486865759 33021952 7424 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8062 7424 603 41 0 8021 0
vsize: 32248
[startup+110.002 s]
Raw data (loadavg): 0.97 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 7788 0 0 0 10977 22 0 0 25 0 1 0 486865759 34082816 7608 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8321 7608 603 41 0 8280 0
vsize: 33284
[startup+120.003 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 8073 0 0 0 11977 23 0 0 25 0 1 0 486865759 35278848 7893 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8613 7893 603 41 0 8572 0
vsize: 34452
[startup+130.003 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 8240 0 0 0 12976 23 0 0 25 0 1 0 486865759 35831808 8060 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8748 8060 603 41 0 8707 0
vsize: 34992
[startup+140.003 s]
Raw data (loadavg): 0.98 0.96 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 8383 0 0 0 13976 24 0 0 25 0 1 0 486865759 36556800 8203 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8925 8203 603 41 0 8884 0
vsize: 35700
[startup+150.004 s]
Raw data (loadavg): 0.98 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 8538 0 0 0 14975 25 0 0 25 0 1 0 486865759 37113856 8358 4294967295 134512640 134672761 3221224560 3221223724 134565030 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9061 8358 603 41 0 9020 0
vsize: 36244
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 8785 0 0 0 15974 25 0 0 25 0 1 0 486865759 38043648 8605 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9288 8605 603 41 0 9247 0
vsize: 37152
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 9192 0 0 0 16974 26 0 0 25 0 1 0 486865759 39772160 9012 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9710 9012 603 41 0 9669 0
vsize: 38840
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 9505 0 0 0 17973 28 0 0 25 0 1 0 486865759 40972288 9325 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10003 9325 603 41 0 9962 0
vsize: 40012
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 9740 0 0 0 18973 28 0 0 25 0 1 0 486865759 41930752 9560 4294967295 134512640 134672761 3221224560 3221223728 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10237 9560 603 41 0 10196 0
vsize: 40948
[startup+200.004 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 10024 0 0 0 19971 29 0 0 25 0 1 0 486865759 43118592 9844 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10527 9844 603 41 0 10486 0
vsize: 42108
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 10286 0 0 0 20971 30 0 0 25 0 1 0 486865759 44179456 10106 4294967295 134512640 134672761 3221224560 3221223664 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10786 10106 603 41 0 10745 0
vsize: 43144
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 10510 0 0 0 21970 31 0 0 25 0 1 0 486865759 45113344 10330 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11014 10330 603 41 0 10973 0
vsize: 44056
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 10714 0 0 0 22970 32 0 0 25 0 1 0 486865759 45912064 10534 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11209 10534 603 41 0 11168 0
vsize: 44836
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 10903 0 0 0 23969 32 0 0 25 0 1 0 486865759 46735360 10723 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11410 10723 603 41 0 11369 0
vsize: 45640
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 11056 0 0 0 24969 33 0 0 25 0 1 0 486865759 47271936 10876 4294967295 134512640 134672761 3221224560 3221223760 134557806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11541 10876 603 41 0 11500 0
vsize: 46164
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 11251 0 0 0 25967 33 0 0 25 0 1 0 486865759 48611328 11071 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11868 11071 603 41 0 11827 0
vsize: 47472
[startup+270.011 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 11463 0 0 0 26967 35 0 0 25 0 1 0 486865759 49545216 11283 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12096 11283 603 41 0 12055 0
vsize: 48384
[startup+280.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 11666 0 0 0 27967 35 0 0 25 0 1 0 486865759 50348032 11486 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12292 11486 603 41 0 12251 0
vsize: 49168
[startup+290.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 11856 0 0 0 28966 36 0 0 25 0 1 0 486865759 51146752 11676 4294967295 134512640 134672761 3221224560 3221223656 1075347141 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12487 11676 603 41 0 12446 0
vsize: 49948
[startup+300.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 12050 0 0 0 29966 37 0 0 25 0 1 0 486865759 51814400 11870 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12650 11870 603 41 0 12609 0
vsize: 50600
[startup+310.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 12215 0 0 0 30965 38 0 0 25 0 1 0 486865759 52600832 12035 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12842 12035 603 41 0 12801 0
vsize: 51368
[startup+320.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 12359 0 0 0 31965 38 0 0 25 0 1 0 486865759 53153792 12179 4294967295 134512640 134672761 3221224560 3221223708 134559754 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12977 12179 603 41 0 12936 0
vsize: 51908
[startup+330.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 12441 0 0 0 32965 38 0 0 25 0 1 0 486865759 53424128 12261 4294967295 134512640 134672761 3221224560 3221223696 134560622 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13043 12261 603 41 0 13002 0
vsize: 52172
[startup+340.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 12584 0 0 0 33965 39 0 0 25 0 1 0 486865759 53952512 12404 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13172 12404 603 41 0 13131 0
vsize: 52688
[startup+350.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 12737 0 0 0 34964 39 0 0 25 0 1 0 486865759 54611968 12557 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13333 12557 603 41 0 13292 0
vsize: 53332
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 12910 0 0 0 35964 40 0 0 25 0 1 0 486865759 55308288 12730 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13503 12730 603 41 0 13462 0
vsize: 54012
[startup+370.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 13077 0 0 0 36964 40 0 0 25 0 1 0 486865759 55980032 12897 4294967295 134512640 134672761 3221224560 3221223664 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13667 12897 603 41 0 13626 0
vsize: 54668
[startup+380.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 13203 0 0 0 37964 41 0 0 25 0 1 0 486865759 56512512 13023 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13797 13023 603 41 0 13756 0
vsize: 55188
[startup+390.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 13335 0 0 0 38963 41 0 0 25 0 1 0 486865759 57040896 13155 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13926 13155 603 41 0 13885 0
vsize: 55704
[startup+400.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 13438 0 0 0 39963 41 0 0 25 0 1 0 486865759 57442304 13258 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14024 13258 603 41 0 13983 0
vsize: 56096
[startup+410.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 13562 0 0 0 40963 42 0 0 25 0 1 0 486865759 57991168 13382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14158 13382 603 41 0 14117 0
vsize: 56632
[startup+420.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 13661 0 0 0 41963 42 0 0 25 0 1 0 486865759 58388480 13481 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14255 13481 603 41 0 14214 0
vsize: 57020
[startup+430.024 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 13756 0 0 0 42963 42 0 0 25 0 1 0 486865759 58650624 13576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14319 13576 603 41 0 14278 0
vsize: 57276
[startup+440.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 13870 0 0 0 43963 42 0 0 25 0 1 0 486865759 59187200 13690 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14450 13690 603 41 0 14409 0
vsize: 57800
[startup+450.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 14000 0 0 0 44963 43 0 0 25 0 1 0 486865759 59723776 13820 4294967295 134512640 134672761 3221224560 3221223684 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14581 13820 603 41 0 14540 0
vsize: 58324
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 14113 0 0 0 45963 43 0 0 25 0 1 0 486865759 60121088 13933 4294967295 134512640 134672761 3221224560 3221223728 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14678 13933 603 41 0 14637 0
vsize: 58712
[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 14392 0 0 0 46962 44 0 0 25 0 1 0 486865759 61325312 14212 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14972 14212 603 41 0 14931 0
vsize: 59888
[startup+480.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 14551 0 0 0 47961 45 0 0 25 0 1 0 486865759 61861888 14371 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15103 14371 603 41 0 15062 0
vsize: 60412
[startup+490.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 14690 0 0 0 48960 45 0 0 25 0 1 0 486865759 62521344 14510 4294967295 134512640 134672761 3221224560 3221223760 134557822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15264 14510 603 41 0 15223 0
vsize: 61056
[startup+500.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 14816 0 0 0 49960 46 0 0 25 0 1 0 486865759 62918656 14636 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15361 14636 603 41 0 15320 0
vsize: 61444
[startup+510.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 14939 0 0 0 50960 46 0 0 25 0 1 0 486865759 63451136 14759 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15491 14759 603 41 0 15450 0
vsize: 61964
[startup+520.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 15083 0 0 0 51960 47 0 0 25 0 1 0 486865759 64028672 14903 4294967295 134512640 134672761 3221224560 3221223664 134560039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15632 14903 603 41 0 15591 0
vsize: 62528
[startup+530.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 15222 0 0 0 52959 47 0 0 25 0 1 0 486865759 64684032 15042 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 15042 603 41 0 15751 0
vsize: 63168
[startup+540.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 15353 0 0 0 53959 48 0 0 25 0 1 0 486865759 65212416 15173 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15921 15173 603 41 0 15880 0
vsize: 63684
[startup+550.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 15460 0 0 0 54959 48 0 0 25 0 1 0 486865759 65605632 15280 4294967295 134512640 134672761 3221224560 3221223744 134558341 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16017 15281 603 41 0 15976 0
vsize: 64068
[startup+560.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 15581 0 0 0 55958 49 0 0 25 0 1 0 486865759 66138112 15401 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16147 15401 603 41 0 16106 0
vsize: 64588
[startup+570.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 15707 0 0 0 56958 49 0 0 25 0 1 0 486865759 66666496 15527 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16276 15527 603 41 0 16235 0
vsize: 65104
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 15807 0 0 0 57958 49 0 0 25 0 1 0 486865759 67076096 15627 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16376 15627 603 41 0 16335 0
vsize: 65504
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 15908 0 0 0 58957 50 0 0 25 0 1 0 486865759 67477504 15728 4294967295 134512640 134672761 3221224560 3221223760 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16474 15728 603 41 0 16433 0
vsize: 65896
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16055 0 0 0 59957 51 0 0 25 0 1 0 486865759 68014080 15875 4294967295 134512640 134672761 3221224560 3221223664 134559835 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16605 15875 603 41 0 16564 0
vsize: 66420
[startup+610.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16189 0 0 0 60957 51 0 0 25 0 1 0 486865759 68612096 16009 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16751 16009 603 41 0 16710 0
vsize: 67004
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16322 0 0 0 61957 51 0 0 25 0 1 0 486865759 69144576 16142 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16881 16142 603 41 0 16840 0
vsize: 67524
[startup+630.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16456 0 0 0 62957 52 0 0 25 0 1 0 486865759 69677056 16276 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17011 16276 603 41 0 16970 0
vsize: 68044
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16557 0 0 0 63956 52 0 0 25 0 1 0 486865759 70074368 16377 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17108 16377 603 41 0 17067 0
vsize: 68432
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16657 0 0 0 64956 53 0 0 25 0 1 0 486865759 70475776 16477 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17206 16477 603 41 0 17165 0
vsize: 68824
[startup+660.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16760 0 0 0 65956 53 0 0 25 0 1 0 486865759 70922240 16580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17315 16580 603 41 0 17274 0
vsize: 69260
[startup+670.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16860 0 0 0 66955 53 0 0 25 0 1 0 486865759 71315456 16680 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17411 16680 603 41 0 17370 0
vsize: 69644
[startup+680.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 16949 0 0 0 67955 54 0 0 25 0 1 0 486865759 71712768 16769 4294967295 134512640 134672761 3221224560 3221223664 134560002 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17508 16769 603 41 0 17467 0
vsize: 70032
[startup+690.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17045 0 0 0 68955 54 0 0 25 0 1 0 486865759 72105984 16865 4294967295 134512640 134672761 3221224560 3221223744 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17604 16865 603 41 0 17563 0
vsize: 70416
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17145 0 0 0 69955 55 0 0 25 0 1 0 486865759 72531968 16965 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17708 16965 603 41 0 17667 0
vsize: 70832
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17274 0 0 0 70954 55 0 0 25 0 1 0 486865759 73076736 17094 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17841 17094 603 41 0 17800 0
vsize: 71364
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17370 0 0 0 71954 56 0 0 25 0 1 0 486865759 73474048 17190 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17938 17190 603 41 0 17897 0
vsize: 71752
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17466 0 0 0 72954 56 0 0 25 0 1 0 486865759 73883648 17286 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18038 17286 603 41 0 17997 0
vsize: 72152
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17555 0 0 0 73954 56 0 0 25 0 1 0 486865759 74145792 17375 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18102 17375 603 41 0 18061 0
vsize: 72408
[startup+750.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17637 0 0 0 74954 56 0 0 25 0 1 0 486865759 74543104 17457 4294967295 134512640 134672761 3221224560 3221223720 134561240 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18199 17457 603 41 0 18158 0
vsize: 72796
[startup+760.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17723 0 0 0 75954 57 0 0 25 0 1 0 486865759 74936320 17543 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18295 17543 603 41 0 18254 0
vsize: 73180
[startup+770.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17808 0 0 0 76954 57 0 0 25 0 1 0 486865759 75198464 17628 4294967295 134512640 134672761 3221224560 3221223744 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18359 17628 603 41 0 18318 0
vsize: 73436
[startup+780.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 17882 0 0 0 77954 57 0 0 25 0 1 0 486865759 75464704 17702 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18424 17702 603 41 0 18383 0
vsize: 73696
[startup+790.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 18029 0 0 0 78953 58 0 0 25 0 1 0 486865759 77189120 17849 4294967295 134512640 134672761 3221224560 3221223744 134559342 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18845 17849 603 41 0 18804 0
vsize: 75380
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 18234 0 0 0 79953 59 0 0 25 0 1 0 486865759 77987840 18054 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19040 18054 603 41 0 18999 0
vsize: 76160
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 18392 0 0 0 80952 59 0 0 25 0 1 0 486865759 78651392 18212 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19202 18212 603 41 0 19161 0
vsize: 76808
[startup+820.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 18517 0 0 0 81951 60 0 0 25 0 1 0 486865759 79175680 18337 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19330 18337 603 41 0 19289 0
vsize: 77320
[startup+830.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 18646 0 0 0 82951 60 0 0 25 0 1 0 486865759 79704064 18466 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19459 18466 603 41 0 19418 0
vsize: 77836
[startup+840.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 18763 0 0 0 83951 61 0 0 25 0 1 0 486865759 80101376 18583 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19556 18583 603 41 0 19515 0
vsize: 78224
[startup+850.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 18946 0 0 0 84950 62 0 0 25 0 1 0 486865759 80900096 18766 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19751 18766 603 41 0 19710 0
vsize: 79004
[startup+860.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 19103 0 0 0 85950 62 0 0 25 0 1 0 486865759 81559552 18923 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19912 18923 603 41 0 19871 0
vsize: 79648
[startup+870.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 19204 0 0 0 86950 63 0 0 25 0 1 0 486865759 81965056 19024 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20011 19024 603 41 0 19970 0
vsize: 80044
[startup+880.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 19330 0 0 0 87950 63 0 0 25 0 1 0 486865759 82370560 19150 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20110 19150 603 41 0 20069 0
vsize: 80440
[startup+890.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 19487 0 0 0 88949 63 0 0 25 0 1 0 486865759 83050496 19307 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20276 19307 603 41 0 20235 0
vsize: 81104
[startup+900.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 19588 0 0 0 89949 64 0 0 25 0 1 0 486865759 83451904 19408 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20374 19408 603 41 0 20333 0
vsize: 81496
[startup+910.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 19704 0 0 0 90949 64 0 0 25 0 1 0 486865759 83984384 19524 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20504 19524 603 41 0 20463 0
vsize: 82016
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 19822 0 0 0 91949 64 0 0 25 0 1 0 486865759 84393984 19642 4294967295 134512640 134672761 3221224560 3221223744 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20604 19642 603 41 0 20563 0
vsize: 82416
[startup+930.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 19913 0 0 0 92949 64 0 0 25 0 1 0 486865759 84799488 19733 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20703 19733 603 41 0 20662 0
vsize: 82812
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20018 0 0 0 93948 65 0 0 25 0 1 0 486865759 85200896 19838 4294967295 134512640 134672761 3221224560 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20801 19838 603 41 0 20760 0
vsize: 83204
[startup+950.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20143 0 0 0 94948 65 0 0 25 0 1 0 486865759 85741568 19963 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20933 19963 603 41 0 20892 0
vsize: 83732
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20233 0 0 0 95948 66 0 0 25 0 1 0 486865759 86183936 20053 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21041 20053 603 41 0 21000 0
vsize: 84164
[startup+970.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20350 0 0 0 96947 66 0 0 25 0 1 0 486865759 86581248 20170 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21138 20170 603 41 0 21097 0
vsize: 84552
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20431 0 0 0 97948 66 0 0 25 0 1 0 486865759 86982656 20251 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21236 20251 603 41 0 21195 0
vsize: 84944
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20549 0 0 0 98947 67 0 0 25 0 1 0 486865759 87379968 20369 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21333 20369 603 41 0 21292 0
vsize: 85332
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20644 0 0 0 99947 67 0 0 25 0 1 0 486865759 87773184 20464 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21429 20464 603 41 0 21388 0
vsize: 85716
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20751 0 0 0 100947 67 0 0 25 0 1 0 486865759 88166400 20571 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21525 20571 603 41 0 21484 0
vsize: 86100
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20840 0 0 0 101947 68 0 0 25 0 1 0 486865759 88559616 20660 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21621 20660 603 41 0 21580 0
vsize: 86484
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 20936 0 0 0 102947 68 0 0 25 0 1 0 486865759 88956928 20756 4294967295 134512640 134672761 3221224560 3221223728 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21718 20756 603 41 0 21677 0
vsize: 86872
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21280 0 0 0 103946 69 0 0 25 0 1 0 486865759 90284032 21100 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22042 21100 603 41 0 22001 0
vsize: 88168
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21417 0 0 0 104946 69 0 0 25 0 1 0 486865759 90955776 21237 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22206 21237 603 41 0 22165 0
vsize: 88824
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21494 0 0 0 105946 70 0 0 25 0 1 0 486865759 91217920 21314 4294967295 134512640 134672761 3221224560 3221223744 134559363 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22270 21314 603 41 0 22229 0
vsize: 89080
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21576 0 0 0 106946 70 0 0 25 0 1 0 486865759 91484160 21396 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22335 21396 603 41 0 22294 0
vsize: 89340
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21647 0 0 0 107946 70 0 0 25 0 1 0 486865759 91750400 21467 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22400 21467 603 41 0 22359 0
vsize: 89600
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21722 0 0 0 108946 70 0 0 25 0 1 0 486865759 92147712 21542 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22497 21542 603 41 0 22456 0
vsize: 89988
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 109946 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223664 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 110946 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 111946 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 112946 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 113947 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 114947 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 115947 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 116947 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 117947 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223656 1075347227 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 118948 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/54 27359
Raw data (stat): 27359 (minisat+) R 27358 20937 20936 0 -1 0 21759 0 0 0 119948 70 0 0 25 0 1 0 486865759 92311552 21579 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22537 21579 603 41 0 22496 0
vsize: 90148
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.92 1/54 27359
Raw data (stat): 27359 (minisat+) Z 27358 20937 20936 0 -1 12 21761 0 0 0 119948 74 0 0 25 0 1 0 486865759 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.23
CPU user time (s): 1199.48
CPU system time (s): 0.748886
CPU usage (%): 100.013
Max. virtual memory (Kb): 90148
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####