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-20-10/MIPLIB/miplib/normalized-mps-v2-20-10-vpm1.opb
MD5SUM	9d68724ddc6098af63bcc619f21688cc
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	168
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	819200
Number of bits of the biggest number in a constraint	20
Biggest sum of numbers in a constraint	4941871
Number of bits of the biggest sum of numbers	23
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	459.704
Number of variables	2754
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	82
Trace number 16871

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-21 08:53:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=12368 boxname=wulflinc8 idbench=952 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  9d68724ddc6098af63bcc619f21688cc  /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-vpm1.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc8/normalized-mps-v2-20-10-vpm1.opb
IDLAUNCH: 12368
/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:        823344 kB
Buffers:         23404 kB
Cached:         165840 kB
SwapCached:          0 kB
Active:          59400 kB
Inactive:       132728 kB
HighTotal:      131008 kB
HighFree:        10556 kB
LowTotal:       903652 kB
LowFree:        812788 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            13644 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 09:13:14 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 12368 7 1200.2 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:   10
c ---[ 484]---> BDD-cost:   10
c ---[ 483]---> BDD-cost:   10
c ---[ 482]---> BDD-cost:   10
c ---[ 481]---> BDD-cost:   10
c ---[ 480]---> BDD-cost:   10
c ---[ 479]---> BDD-cost:   10
c ---[ 478]---> BDD-cost:   10
c ---[ 477]---> BDD-cost:   10
c ---[ 474]---> BDD-cost:   10
c ---[ 473]---> BDD-cost:   10
c ---[ 472]---> BDD-cost:   10
c ---[ 471]---> BDD-cost:   10
c ---[ 468]---> BDD-cost:   10
c ---[ 467]---> BDD-cost:   10
c ---[ 466]---> BDD-cost:   10
c ---[ 465]---> BDD-cost:   10
c ---[ 462]---> BDD-cost:   10
c ---[ 459]---> BDD-cost:   10
c ---[ 458]---> BDD-cost:   10
c ---[ 457]---> BDD-cost:   10
c ---[ 454]---> BDD-cost:   10
c ---[ 453]---> BDD-cost:   10
c ---[ 452]---> BDD-cost:   10
c ---[ 451]---> BDD-cost:   10
c ---[ 450]---> BDD-cost:   10
c ---[ 448]---> BDD-cost:   10
c ---[ 447]---> BDD-cost:   10
c ---[ 446]---> BDD-cost:   10
c ---[ 445]---> BDD-cost:   10
c ---[ 444]---> BDD-cost:   10
c ---[ 441]---> BDD-cost:   10
c ---[ 440]---> BDD-cost:   10
c ---[ 439]---> BDD-cost:   10
c ---[ 433]---> BDD-cost:   10
c ---[ 427]---> BDD-cost:   10
c ---[ 422]---> BDD-cost:   10
c ---[ 421]---> BDD-cost:   10
c ---[ 415]---> BDD-cost:   10
c ---[ 409]---> BDD-cost:   10
c ---[ 408]---> BDD-cost:   10
c ---[ 402]---> BDD-cost:   10
c ---[ 397]---> BDD-cost:   10
c ---[ 396]---> BDD-cost:   10
c ---[ 391]---> BDD-cost:   10
c ---[ 390]---> BDD-cost:   10
c ---[ 386]---> BDD-cost:   10
c ---[ 385]---> BDD-cost:   10
c ---[ 384]---> BDD-cost:   10
c ---[ 380]---> BDD-cost:   10
c ---[ 379]---> BDD-cost:   10
c ---[ 378]---> BDD-cost:   10
c ---[ 374]---> BDD-cost:   10
c ---[ 373]---> BDD-cost:   10
c ---[ 372]---> BDD-cost:   10
c ---[ 368]---> BDD-cost:   10
c ---[ 367]---> BDD-cost:   10
c ---[ 366]---> BDD-cost:   10
c ---[ 365]---> BDD-cost:   10
c ---[ 364]---> BDD-cost:   10
c ---[ 359]---> BDD-cost:   10
c ---[ 353]---> BDD-cost:   10
c ---[ 347]---> BDD-cost:   10
c ---[ 339]---> BDD-cost:   10
c ---[ 333]---> BDD-cost:   10
c ---[ 327]---> BDD-cost:   10
c ---[ 321]---> BDD-cost:   10
c ---[ 317]---> BDD-cost:   17
c ---[ 316]---> BDD-cost:   17
c ---[ 315]---> BDD-cost:   17
c ---[ 314]---> BDD-cost:   17
c ---[ 313]---> BDD-cost:   17
c ---[ 312]---> BDD-cost:   17
c ---[ 310]---> BDD-cost:   17
c ---[ 309]---> BDD-cost:   17
c ---[ 308]---> BDD-cost:   17
c ---[ 307]---> BDD-cost:   17
c ---[ 306]---> BDD-cost:   17
c ---[ 302]---> BDD-cost:   16
c ---[ 301]---> BDD-cost:   16
c ---[ 300]---> BDD-cost:   16
c ---[ 295]---> BDD-cost:   16
c ---[ 294]---> BDD-cost:   16
c ---[ 290]---> BDD-cost:   18
c ---[ 289]---> BDD-cost:   18
c ---[ 288]---> BDD-cost:   18
c ---[ 287]---> BDD-cost:   16
c ---[ 286]---> BDD-cost:   16
c ---[ 285]---> BDD-cost:   16
c ---[ 284]---> BDD-cost:   16
c ---[ 283]---> BDD-cost:   16
c ---[ 282]---> BDD-cost:   16
c ---[ 280]---> BDD-cost:   16
c ---[ 279]---> BDD-cost:   16
c ---[ 278]---> BDD-cost:   16
c ---[ 277]---> BDD-cost:   16
c ---[ 276]---> BDD-cost:   16
c ---[ 274]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 258]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 256]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 254]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[ 252]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[ 250]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[ 248]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[ 246]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 244]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[ 242]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 234]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 232]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 224]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 216]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 214]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 212]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 210]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 208]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 206]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 204]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 202]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[ 200]---> Sorter-cost: 3241     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[ 198]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[ 196]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 194]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 192]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[ 191]---> BDD-cost:   48
c ---[ 190]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost: 1088     Base: 2 2 2 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  982     Base: 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   48
c ---[ 184]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  400     Base: 2 2 2 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  781     Base: 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1034     Base: 2 2 2 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost: 1032     Base: 2 2 2 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   48
c ---[ 178]---> Sorter-cost:  386     Base: 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1047     Base: 2 2 2 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost: 1019     Base: 2 2 2 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   48
c ---[ 172]---> Sorter-cost:  370     Base: 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  391     Base: 2 2 2 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost: 1022     Base: 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  952     Base: 2 2 2 2 2 2 2 2 2
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    3
c ---[ 165]---> BDD-cost:    3
c ---[ 164]---> BDD-cost:    3
c ---[ 163]---> BDD-cost:    3
c ---[ 162]---> BDD-cost:    3
c ---[ 161]---> BDD-cost:    3
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:    3
c ---[ 158]---> BDD-cost:   10
c ---[ 157]---> BDD-cost:   10
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:   10
c ---[ 151]---> BDD-cost:   10
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:   10
c ---[ 145]---> BDD-cost:   10
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:   10
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:   10
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:   10
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:   10
c ---[ 116]---> BDD-cost:   10
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:   10
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    9
c ---[  98]---> BDD-cost:   10
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:   10
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:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:   10
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   10
c ---[  33]---> BDD-cost:    8
c ---[  32]---> BDD-cost:    8
c ---[  31]---> BDD-cost:    8
c ---[  30]---> BDD-cost:    8
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:   10
c ---[  27]---> BDD-cost:    8
c ---[  26]---> BDD-cost:    8
c ---[  25]---> BDD-cost:    8
c ---[  24]---> BDD-cost:    8
c ---[  22]---> BDD-cost:   10
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  16]---> BDD-cost:   10
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  10]---> BDD-cost:   10
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    8
c ---[   1]---> BDD-cost:    8
c ---[   0]---> BDD-cost:    8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  131984   372097 |   43994       0        0     nan |  0.000 % |
c |       100 |  131893   371869 |   48393      95      337     3.5 |  6.825 % |
c |       251 |  131833   371735 |   53232     243     1128     4.6 |  6.864 % |
c |       477 |  131829   371726 |   58556     468     2452     5.2 |  6.866 % |
c |       814 |  131829   371726 |   64411     805     5904     7.3 |  6.866 % |
c |      1320 |  131829   371726 |   70852    1311    10060     7.7 |  6.866 % |
c |      2080 |  131766   371585 |   77938    2067    16552     8.0 |  6.907 % |
c |      3219 |  131743   371526 |   85731    3204    31361     9.8 |  6.920 % |
c |      4927 |  131369   370664 |   94305    4894    54229    11.1 |  7.176 % |
c |      7489 |  131191   370240 |  103735    7441    89422    12.0 |  7.292 % |
c |     11334 |  130995   369791 |  114109   11272   134396    11.9 |  7.424 % |
c |     17100 |  130634   368964 |  125520   17026   227613    13.4 |  7.656 % |
c |     25749 |  130363   368341 |  138072   25650   343214    13.4 |  7.839 % |
c |     38724 |  130286   368151 |  151879   38609   624446    16.2 |  7.891 % |
c |     58185 |  130217   367957 |  167067   58063  1081641    18.6 |  7.930 % |
c |     87378 |  129973   367396 |  183773   87223  2028744    23.3 |  8.121 % |
c |    131167 |  129742   366846 |  202151  130997  3412336    26.0 |  8.296 % |
c |    196851 |  129657   366617 |  222366  196649  5557731    28.3 |  8.350 % |
c |    295378 |  129331   365820 |  244603   90242  2391247    26.5 |  8.577 % |
c |    443167 |  128851   364608 |  269063  237959  7047781    29.6 |  8.910 % |
c |    664850 |  128325   363313 |  295969  213696  6326538    29.6 |  9.280 % |
#### 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.91 0.93 0.94 2/54 26728
Raw data (stat): 26728 (runsolver) R 26727 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 472003172 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.93 0.93 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 4211 0 0 0 986 13 0 0 25 0 1 0 472003172 20299776 4034 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4956 4034 603 41 0 4915 0
vsize: 19824
[startup+20.0018 s]
Raw data (loadavg): 0.94 0.94 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 4561 0 0 0 1984 14 0 0 25 0 1 0 472003172 21811200 4384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5325 4384 603 41 0 5284 0
vsize: 21300
[startup+30.0026 s]
Raw data (loadavg): 0.95 0.94 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 5125 0 0 0 2983 16 0 0 25 0 1 0 472003172 24227840 4948 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5915 4948 603 41 0 5874 0
vsize: 23660
[startup+40.0018 s]
Raw data (loadavg): 0.95 0.94 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 5587 0 0 0 3981 18 0 0 25 0 1 0 472003172 25985024 5410 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6344 5410 603 41 0 6303 0
vsize: 25376
[startup+50.0031 s]
Raw data (loadavg): 0.96 0.94 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 6099 0 0 0 4979 19 0 0 25 0 1 0 472003172 28270592 5922 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6902 5922 603 41 0 6861 0
vsize: 27608
[startup+60.0041 s]
Raw data (loadavg): 0.97 0.94 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 6462 0 0 0 5978 21 0 0 25 0 1 0 472003172 29741056 6285 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7261 6285 603 41 0 7220 0
vsize: 29044
[startup+70.0052 s]
Raw data (loadavg): 0.97 0.94 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 6742 0 0 0 6977 22 0 0 25 0 1 0 472003172 30953472 6565 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7557 6565 603 41 0 7516 0
vsize: 30228
[startup+80.0064 s]
Raw data (loadavg): 0.98 0.94 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 7043 0 0 0 7975 24 0 0 25 0 1 0 472003172 32169984 6866 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7854 6866 603 41 0 7813 0
vsize: 31416
[startup+90.0062 s]
Raw data (loadavg): 0.98 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 7387 0 0 0 8974 26 0 0 25 0 1 0 472003172 33525760 7210 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8185 7210 603 41 0 8144 0
vsize: 32740
[startup+100.007 s]
Raw data (loadavg): 0.98 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 7648 0 0 0 9973 27 0 0 25 0 1 0 472003172 34607104 7471 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8449 7471 603 41 0 8408 0
vsize: 33796
[startup+110.008 s]
Raw data (loadavg): 0.98 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 7866 0 0 0 10972 28 0 0 25 0 1 0 472003172 35557376 7689 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8681 7689 603 41 0 8640 0
vsize: 34724
[startup+120.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 8079 0 0 0 11971 29 0 0 25 0 1 0 472003172 36368384 7902 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8879 7902 603 41 0 8838 0
vsize: 35516
[startup+130.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 8268 0 0 0 12971 29 0 0 25 0 1 0 472003172 37175296 8091 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9076 8091 603 41 0 9035 0
vsize: 36304
[startup+140.01 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 8429 0 0 0 13970 30 0 0 25 0 1 0 472003172 37715968 8252 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9208 8252 603 41 0 9167 0
vsize: 36832
[startup+150.011 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 8624 0 0 0 14970 31 0 0 25 0 1 0 472003172 38674432 8447 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9442 8447 603 41 0 9401 0
vsize: 37768
[startup+160.011 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 8943 0 0 0 15969 32 0 0 25 0 1 0 472003172 40411136 8766 4294967295 134512640 134672761 3221224624 3221223808 134559182 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9866 8766 603 41 0 9825 0
vsize: 39464
[startup+170.012 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 9267 0 0 0 16968 33 0 0 25 0 1 0 472003172 41783296 9090 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10201 9090 603 41 0 10160 0
vsize: 40804
[startup+180.014 s]
Raw data (loadavg): 0.99 0.95 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 9514 0 0 0 17967 34 0 0 25 0 1 0 472003172 42725376 9337 4294967295 134512640 134672761 3221224624 3221223760 134560675 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10431 9337 603 41 0 10390 0
vsize: 41724
[startup+190.013 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 9691 0 0 0 18967 34 0 0 25 0 1 0 472003172 43401216 9514 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10596 9514 603 41 0 10555 0
vsize: 42384
[startup+200.014 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 9848 0 0 0 19966 35 0 0 25 0 1 0 472003172 44064768 9671 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10758 9671 603 41 0 10717 0
vsize: 43032
[startup+210.014 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 10006 0 0 0 20966 35 0 0 25 0 1 0 472003172 44601344 9829 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10889 9829 603 41 0 10848 0
vsize: 43556
[startup+220.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 10160 0 0 0 21965 36 0 0 25 0 1 0 472003172 45264896 9983 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11051 9983 603 41 0 11010 0
vsize: 44204
[startup+230.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 10297 0 0 0 22965 37 0 0 25 0 1 0 472003172 45809664 10120 4294967295 134512640 134672761 3221224624 3221223792 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11184 10120 603 41 0 11143 0
vsize: 44736
[startup+240.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 10433 0 0 0 23964 37 0 0 25 0 1 0 472003172 46374912 10256 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11322 10256 603 41 0 11281 0
vsize: 45288
[startup+250.016 s]
Raw data (loadavg): 0.99 0.96 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 10556 0 0 0 24964 38 0 0 25 0 1 0 472003172 46931968 10379 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11458 10379 603 41 0 11417 0
vsize: 45832
[startup+260.017 s]
Raw data (loadavg): 1.07 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 10670 0 0 0 25964 39 0 0 25 0 1 0 472003172 47341568 10493 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11558 10493 603 41 0 11517 0
vsize: 46232
[startup+270.018 s]
Raw data (loadavg): 1.06 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 10793 0 0 0 26963 40 0 0 25 0 1 0 472003172 47898624 10616 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11694 10616 603 41 0 11653 0
vsize: 46776
[startup+280.018 s]
Raw data (loadavg): 1.05 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 10915 0 0 0 27962 40 0 0 25 0 1 0 472003172 48431104 10738 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11824 10738 603 41 0 11783 0
vsize: 47296
[startup+290.019 s]
Raw data (loadavg): 1.04 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 11038 0 0 0 28962 41 0 0 25 0 1 0 472003172 48836608 10861 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11923 10861 603 41 0 11882 0
vsize: 47692
[startup+300.02 s]
Raw data (loadavg): 1.04 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 11163 0 0 0 29961 41 0 0 25 0 1 0 472003172 49385472 10986 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12057 10986 603 41 0 12016 0
vsize: 48228
[startup+310.02 s]
Raw data (loadavg): 1.03 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 11262 0 0 0 30961 42 0 0 25 0 1 0 472003172 49811456 11085 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12161 11085 603 41 0 12120 0
vsize: 48644
[startup+320.021 s]
Raw data (loadavg): 1.03 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 11361 0 0 0 31960 43 0 0 25 0 1 0 472003172 50216960 11184 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12260 11184 603 41 0 12219 0
vsize: 49040
[startup+330.022 s]
Raw data (loadavg): 1.02 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 11545 0 0 0 32960 43 0 0 25 0 1 0 472003172 50884608 11368 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12423 11368 603 41 0 12382 0
vsize: 49692
[startup+340.022 s]
Raw data (loadavg): 1.02 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 11794 0 0 0 33959 44 0 0 25 0 1 0 472003172 51990528 11617 4294967295 134512640 134672761 3221224624 3221223728 134560034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12693 11617 603 41 0 12652 0
vsize: 50772
[startup+350.023 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12021 0 0 0 34958 45 0 0 25 0 1 0 472003172 53014528 11844 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12943 11844 603 41 0 12902 0
vsize: 51772
[startup+360.024 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12226 0 0 0 35956 47 0 0 25 0 1 0 472003172 53825536 12049 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13141 12049 603 41 0 13100 0
vsize: 52564
[startup+370.024 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12424 0 0 0 36955 49 0 0 25 0 1 0 472003172 54628352 12247 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13337 12247 603 41 0 13296 0
vsize: 53348
[startup+380.025 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12691 0 0 0 37954 50 0 0 25 0 1 0 472003172 55709696 12514 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13601 12514 603 41 0 13560 0
vsize: 54404
[startup+390.024 s]
Raw data (loadavg): 1.01 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12922 0 0 0 38952 51 0 0 25 0 1 0 472003172 56647680 12745 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13830 12745 603 41 0 13789 0
vsize: 55320
[startup+400.025 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12983 0 0 0 39952 52 0 0 25 0 1 0 472003172 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+410.03 s]
Raw data (loadavg): 1.00 0.98 0.94 2/54 26728
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12983 0 0 0 40953 52 0 0 25 0 1 0 472003172 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+420.032 s]
Raw data (loadavg): 1.08 1.00 0.95 2/57 26777
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12983 0 0 0 41952 52 0 0 25 0 1 0 472003172 56918016 12806 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+430.033 s]
Raw data (loadavg): 1.22 1.03 0.96 2/54 26781
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12983 0 0 0 42953 52 0 0 25 0 1 0 472003172 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+440.033 s]
Raw data (loadavg): 1.18 1.03 0.96 2/54 26781
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12983 0 0 0 43953 52 0 0 25 0 1 0 472003172 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+450.033 s]
Raw data (loadavg): 1.15 1.03 0.96 2/54 26781
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12983 0 0 0 44953 52 0 0 25 0 1 0 472003172 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+460.033 s]
Raw data (loadavg): 1.13 1.03 0.96 2/54 26781
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12983 0 0 0 45953 52 0 0 25 0 1 0 472003172 56918016 12806 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12806 603 41 0 13855 0
vsize: 55584
[startup+470.034 s]
Raw data (loadavg): 1.11 1.02 0.96 2/54 26781
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12984 0 0 0 46953 52 0 0 25 0 1 0 472003172 56918016 12807 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12807 603 41 0 13855 0
vsize: 55584
[startup+480.034 s]
Raw data (loadavg): 1.09 1.02 0.96 2/54 26781
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12984 0 0 0 47953 52 0 0 25 0 1 0 472003172 56918016 12807 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12807 603 41 0 13855 0
vsize: 55584
[startup+490.034 s]
Raw data (loadavg): 1.08 1.02 0.96 2/54 26781
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12985 0 0 0 48953 52 0 0 25 0 1 0 472003172 56918016 12808 4294967295 134512640 134672761 3221224624 3221223748 134566133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12808 603 41 0 13855 0
vsize: 55584
[startup+500.034 s]
Raw data (loadavg): 1.07 1.02 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12985 0 0 0 49953 52 0 0 25 0 1 0 472003172 56918016 12808 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12808 603 41 0 13855 0
vsize: 55584
[startup+510.034 s]
Raw data (loadavg): 1.06 1.02 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12985 0 0 0 50953 52 0 0 25 0 1 0 472003172 56918016 12808 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12808 603 41 0 13855 0
vsize: 55584
[startup+520.035 s]
Raw data (loadavg): 1.05 1.02 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12985 0 0 0 51954 52 0 0 25 0 1 0 472003172 56918016 12808 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12808 603 41 0 13855 0
vsize: 55584
[startup+530.035 s]
Raw data (loadavg): 1.04 1.02 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12986 0 0 0 52954 52 0 0 25 0 1 0 472003172 56918016 12809 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12809 603 41 0 13855 0
vsize: 55584
[startup+540.035 s]
Raw data (loadavg): 1.03 1.02 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12986 0 0 0 53954 52 0 0 25 0 1 0 472003172 56918016 12809 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12809 603 41 0 13855 0
vsize: 55584
[startup+550.035 s]
Raw data (loadavg): 1.03 1.02 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12989 0 0 0 54954 52 0 0 25 0 1 0 472003172 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+560.035 s]
Raw data (loadavg): 1.02 1.02 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12989 0 0 0 55954 52 0 0 25 0 1 0 472003172 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+570.036 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12989 0 0 0 56955 52 0 0 25 0 1 0 472003172 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+580.036 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12989 0 0 0 57955 52 0 0 25 0 1 0 472003172 56918016 12812 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+590.035 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12989 0 0 0 58955 52 0 0 25 0 1 0 472003172 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+600.035 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12989 0 0 0 59955 52 0 0 25 0 1 0 472003172 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+610.036 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12989 0 0 0 60955 52 0 0 25 0 1 0 472003172 56918016 12812 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12812 603 41 0 13855 0
vsize: 55584
[startup+620.037 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12990 0 0 0 61955 52 0 0 25 0 1 0 472003172 56918016 12813 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12813 603 41 0 13855 0
vsize: 55584
[startup+630.037 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12990 0 0 0 62956 52 0 0 25 0 1 0 472003172 56918016 12813 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12813 603 41 0 13855 0
vsize: 55584
[startup+640.036 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12991 0 0 0 63956 52 0 0 25 0 1 0 472003172 56918016 12814 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12814 603 41 0 13855 0
vsize: 55584
[startup+650.036 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12992 0 0 0 64956 52 0 0 25 0 1 0 472003172 56918016 12815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12815 603 41 0 13855 0
vsize: 55584
[startup+660.036 s]
Raw data (loadavg): 1.00 1.01 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12992 0 0 0 65956 52 0 0 25 0 1 0 472003172 56918016 12815 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12815 603 41 0 13855 0
vsize: 55584
[startup+670.037 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12992 0 0 0 66956 52 0 0 25 0 1 0 472003172 56918016 12815 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12815 603 41 0 13855 0
vsize: 55584
[startup+680.037 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 12994 0 0 0 67957 52 0 0 25 0 1 0 472003172 56918016 12817 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13896 12817 603 41 0 13855 0
vsize: 55584
[startup+690.037 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 13023 0 0 0 68957 52 0 0 25 0 1 0 472003172 57053184 12846 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13929 12846 603 41 0 13888 0
vsize: 55716
[startup+700.037 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 13187 0 0 0 69956 53 0 0 25 0 1 0 472003172 57724928 13010 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14093 13010 603 41 0 14052 0
vsize: 56372
[startup+710.037 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 13306 0 0 0 70956 53 0 0 25 0 1 0 472003172 58261504 13129 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14224 13129 603 41 0 14183 0
vsize: 56896
[startup+720.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26783
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 13474 0 0 0 71956 53 0 0 25 0 1 0 472003172 58929152 13297 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14387 13297 603 41 0 14346 0
vsize: 57548
[startup+730.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 13608 0 0 0 72956 54 0 0 25 0 1 0 472003172 59502592 13431 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14527 13431 603 41 0 14486 0
vsize: 58108
[startup+740.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 13735 0 0 0 73956 54 0 0 25 0 1 0 472003172 60035072 13558 4294967295 134512640 134672761 3221224624 3221223792 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14657 13558 603 41 0 14616 0
vsize: 58628
[startup+750.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 13911 0 0 0 74956 54 0 0 25 0 1 0 472003172 60846080 13734 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14855 13734 603 41 0 14814 0
vsize: 59420
[startup+760.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 14044 0 0 0 75956 55 0 0 25 0 1 0 472003172 61378560 13867 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14985 13867 603 41 0 14944 0
vsize: 59940
[startup+770.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 14323 0 0 0 76955 55 0 0 25 0 1 0 472003172 62459904 14146 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15249 14146 603 41 0 15208 0
vsize: 60996
[startup+780.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 14467 0 0 0 77955 56 0 0 25 0 1 0 472003172 63135744 14290 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15414 14290 603 41 0 15373 0
vsize: 61656
[startup+790.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 14572 0 0 0 78955 56 0 0 25 0 1 0 472003172 63537152 14395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15512 14395 603 41 0 15471 0
vsize: 62048
[startup+800.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 14670 0 0 0 79954 56 0 0 25 0 1 0 472003172 63938560 14493 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15610 14493 603 41 0 15569 0
vsize: 62440
[startup+810.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 14773 0 0 0 80954 56 0 0 25 0 1 0 472003172 64352256 14596 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15711 14596 603 41 0 15670 0
vsize: 62844
[startup+820.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 14869 0 0 0 81954 57 0 0 25 0 1 0 472003172 64761856 14692 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15811 14692 603 41 0 15770 0
vsize: 63244
[startup+830.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 14961 0 0 0 82954 57 0 0 25 0 1 0 472003172 66080768 14784 4294967295 134512640 134672761 3221224624 3221223792 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16133 14784 603 41 0 16092 0
vsize: 64532
[startup+840.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15196 0 0 0 83954 57 0 0 25 0 1 0 472003172 67162112 15019 4294967295 134512640 134672761 3221224624 3221223708 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16397 15019 603 41 0 16356 0
vsize: 65588
[startup+850.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15530 0 0 0 84953 58 0 0 25 0 1 0 472003172 68505600 15353 4294967295 134512640 134672761 3221224624 3221223616 134565819 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+860.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15530 0 0 0 85953 58 0 0 25 0 1 0 472003172 68505600 15353 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+870.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15530 0 0 0 86953 58 0 0 25 0 1 0 472003172 68505600 15353 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+880.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15530 0 0 0 87954 58 0 0 25 0 1 0 472003172 68505600 15353 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+890.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15530 0 0 0 88954 58 0 0 25 0 1 0 472003172 68505600 15353 4294967295 134512640 134672761 3221224624 3221223792 134561272 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15353 603 41 0 16684 0
vsize: 66900
[startup+900.039 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15537 0 0 0 89954 59 0 0 25 0 1 0 472003172 68505600 15360 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15360 603 41 0 16684 0
vsize: 66900
[startup+910.038 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15537 0 0 0 90954 59 0 0 25 0 1 0 472003172 68505600 15360 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15360 603 41 0 16684 0
vsize: 66900
[startup+920.038 s]
Raw data (loadavg): 1.08 1.02 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15537 0 0 0 91954 59 0 0 25 0 1 0 472003172 68505600 15360 4294967295 134512640 134672761 3221224624 3221223760 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15360 603 41 0 16684 0
vsize: 66900
[startup+930.038 s]
Raw data (loadavg): 1.07 1.02 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15537 0 0 0 92954 59 0 0 25 0 1 0 472003172 68505600 15360 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15360 603 41 0 16684 0
vsize: 66900
[startup+940.037 s]
Raw data (loadavg): 1.06 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15547 0 0 0 93954 59 0 0 25 0 1 0 472003172 68505600 15370 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15370 603 41 0 16684 0
vsize: 66900
[startup+950.038 s]
Raw data (loadavg): 1.05 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15548 0 0 0 94954 59 0 0 25 0 1 0 472003172 68505600 15371 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16725 15371 603 41 0 16684 0
vsize: 66900
[startup+960.038 s]
Raw data (loadavg): 1.04 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15560 0 0 0 95955 59 0 0 25 0 1 0 472003172 68665344 15383 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15383 603 41 0 16723 0
vsize: 67056
[startup+970.038 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15560 0 0 0 96955 59 0 0 25 0 1 0 472003172 68665344 15383 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15383 603 41 0 16723 0
vsize: 67056
[startup+980.038 s]
Raw data (loadavg): 1.03 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 97955 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+990.037 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 98955 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1000.04 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 99955 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1010.04 s]
Raw data (loadavg): 1.02 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 100955 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1020.04 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 101956 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1030.04 s]
Raw data (loadavg): 1.01 1.01 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 102956 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1040.04 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 103956 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1050.04 s]
Raw data (loadavg): 1.01 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 104956 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1060.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15561 0 0 0 105956 59 0 0 25 0 1 0 472003172 68665344 15384 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15384 603 41 0 16723 0
vsize: 67056
[startup+1070.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15562 0 0 0 106956 59 0 0 25 0 1 0 472003172 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1080.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15562 0 0 0 107956 59 0 0 25 0 1 0 472003172 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1090.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15562 0 0 0 108957 59 0 0 25 0 1 0 472003172 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1100.04 s]
Raw data (loadavg): 1.00 1.00 0.96 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15562 0 0 0 109957 59 0 0 25 0 1 0 472003172 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1110.04 s]
Raw data (loadavg): 1.07 1.02 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15562 0 0 0 110957 59 0 0 25 0 1 0 472003172 68665344 15385 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1120.04 s]
Raw data (loadavg): 1.06 1.02 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15562 0 0 0 111957 59 0 0 25 0 1 0 472003172 68665344 15385 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15385 603 41 0 16723 0
vsize: 67056
[startup+1130.04 s]
Raw data (loadavg): 1.05 1.01 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15572 0 0 0 112957 59 0 0 25 0 1 0 472003172 68665344 15395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15395 603 41 0 16723 0
vsize: 67056
[startup+1140.04 s]
Raw data (loadavg): 1.04 1.01 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15572 0 0 0 113957 59 0 0 25 0 1 0 472003172 68665344 15395 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15395 603 41 0 16723 0
vsize: 67056
[startup+1150.04 s]
Raw data (loadavg): 1.04 1.01 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15572 0 0 0 114958 59 0 0 25 0 1 0 472003172 68665344 15395 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15395 603 41 0 16723 0
vsize: 67056
[startup+1160.04 s]
Raw data (loadavg): 1.03 1.01 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15572 0 0 0 115958 59 0 0 25 0 1 0 472003172 68665344 15395 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15395 603 41 0 16723 0
vsize: 67056
[startup+1170.04 s]
Raw data (loadavg): 1.02 1.01 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15575 0 0 0 116958 59 0 0 25 0 1 0 472003172 68665344 15398 4294967295 134512640 134672761 3221224624 3221223776 134565119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16764 15398 603 41 0 16723 0
vsize: 67056
[startup+1180.04 s]
Raw data (loadavg): 1.02 1.01 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15586 0 0 0 117958 59 0 0 25 0 1 0 472003172 68829184 15409 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16804 15409 603 41 0 16763 0
vsize: 67216
[startup+1190.04 s]
Raw data (loadavg): 1.02 1.01 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15587 0 0 0 118957 59 0 0 25 0 1 0 472003172 68829184 15410 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16804 15410 603 41 0 16763 0
vsize: 67216
[startup+1200.04 s]
Raw data (loadavg): 1.01 1.01 0.97 2/54 26785
Raw data (stat): 26728 (minisat+) R 26727 26667 26666 0 -1 0 15597 0 0 0 119957 59 0 0 25 0 1 0 472003172 68829184 15420 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16804 15420 603 41 0 16763 0
vsize: 67216
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 1.01 1.01 0.97 1/54 26785
Raw data (stat): 26728 (minisat+) Z 26727 26667 26666 0 -1 12 15599 0 0 0 119957 62 0 0 25 0 1 0 472003172 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.07
CPU time (s): 1200.2
CPU user time (s): 1199.58
CPU system time (s): 0.624905
CPU usage (%): 100.011
Max. virtual memory (Kb): 67216
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####