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/miplib2003/normalized-mps-v2-20-10-vpm2.opb
MD5SUM	c1b4c3ad409db732d2b559e570b6f24c
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	138
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	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	1189.01
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	84
Trace number 21697

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc1 THE 2005-04-22 00:37:25 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=13135 boxname=wulflinc1 idbench=1011 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  c1b4c3ad409db732d2b559e570b6f24c  /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-vpm2.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc1/normalized-mps-v2-20-10-vpm2.opb
IDLAUNCH: 13135
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.053
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.053
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:        526032 kB
Buffers:          3760 kB
Cached:         479584 kB
SwapCached:          0 kB
Active:         110520 kB
Inactive:       375988 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        525780 kB
SwapTotal:     2097136 kB
SwapFree:      2096968 kB
Dirty:              24 kB
Writeback:           0 kB
Mapped:           7172 kB
Slab:            16312 kB
Committed_AS:    92820 kB
PageTables:        344 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-22 00:57:27 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 13135 7 1200.28 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 272]---> Adder-cost: 288   maxlim: 1694643   bits: 21/21
c ---[ 271]---> BDD-cost:    3
c ---[ 270]---> BDD-cost:    3
c ---[ 269]---> BDD-cost:    3
c ---[ 267]---> BDD-cost:    3
c ---[ 266]---> BDD-cost:    3
c ---[ 265]---> BDD-cost:    3
c ---[ 264]---> BDD-cost:    3
c ---[ 263]---> BDD-cost:    3
c ---[ 259]---> BDD-cost:   10
c ---[ 258]---> BDD-cost:    3
c ---[ 257]---> BDD-cost:    3
c ---[ 256]---> BDD-cost:    3
c ---[ 255]---> BDD-cost:   10
c ---[ 251]---> BDD-cost:   10
c ---[ 250]---> BDD-cost:    3
c ---[ 247]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:   10
c ---[ 242]---> BDD-cost:    3
c ---[ 241]---> BDD-cost:    9
c ---[ 236]---> Sorter-cost: 2294     Base: 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[ 235]---> BDD-cost:    3
c ---[ 234]---> BDD-cost:    3
c ---[ 233]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:   10
c ---[ 228]---> BDD-cost:    3
c ---[ 227]---> BDD-cost:    9
c ---[ 224]---> Adder-cost: 312   maxlim: 2587171   bits: 22/22
c ---[ 220]---> BDD-cost:    3
c ---[ 219]---> BDD-cost:    3
c ---[ 214]---> BDD-cost:   10
c ---[ 212]---> Adder-cost: 260   maxlim: 897571   bits: 20/20
c ---[ 211]---> BDD-cost:    3
c ---[ 206]---> BDD-cost:    3
c ---[ 205]---> BDD-cost:    3
c ---[ 198]---> BDD-cost:    3
c ---[ 197]---> BDD-cost:    3
c ---[ 193]---> BDD-cost:    3
c ---[ 192]---> BDD-cost:    3
c ---[ 191]---> BDD-cost:    3
c ---[ 185]---> BDD-cost:    3
c ---[ 184]---> BDD-cost:    3
c ---[ 183]---> BDD-cost:    3
c ---[ 179]---> BDD-cost:    3
c ---[ 178]---> BDD-cost:    3
c ---[ 175]---> BDD-cost:    3
c ---[ 171]---> BDD-cost:    3
c ---[ 170]---> BDD-cost:    3
c ---[ 169]---> BDD-cost:    3
c ---[ 168]---> BDD-cost:    3
c ---[ 167]---> BDD-cost:    3
c ---[ 166]---> BDD-cost:    9
c ---[ 164]---> Sorter-cost: 2815     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    3
c ---[ 159]---> BDD-cost:   10
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    3
c ---[ 152]---> Adder-cost: 352   maxlim: 2411343   bits: 22/22
c ---[ 150]---> Adder-cost: 350   maxlim: 1768271   bits: 22/21
c ---[ 149]---> BDD-cost:   10
c ---[ 148]---> BDD-cost:    8
c ---[ 147]---> BDD-cost:    8
c ---[ 146]---> BDD-cost:    8
c ---[ 145]---> BDD-cost:    8
c ---[ 144]---> BDD-cost:    3
c ---[ 143]---> BDD-cost:   10
c ---[ 142]---> BDD-cost:    8
c ---[ 141]---> BDD-cost:    8
c ---[ 140]---> BDD-cost:    8
c ---[ 137]---> BDD-cost:    8
c ---[ 135]---> BDD-cost:   10
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:   10
c ---[ 128]---> BDD-cost:    3
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:   10
c ---[ 120]---> BDD-cost:    3
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 114]---> Adder-cost: 274   maxlim: 1228100   bits: 21/21
c ---[ 113]---> BDD-cost:   10
c ---[ 112]---> BDD-cost:    3
c ---[ 111]---> BDD-cost:    8
c ---[ 110]---> BDD-cost:    8
c ---[ 109]---> BDD-cost:    8
c ---[ 107]---> Adder-cost: 312   maxlim: 1957187   bits: 22/21
c ---[ 105]---> Adder-cost: 312   maxlim: 1854787   bits: 22/21
c ---[ 103]---> Adder-cost: 390   maxlim: 2279471   bits: 22/22
c ---[ 101]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  99]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  97]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  95]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  93]---> Adder-cost: 332   maxlim: 845871   bits: 20/20
c ---[  91]---> Sorter-cost: 3240     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5
c ---[  89]---> Adder-cost: 440   maxlim: 3713071   bits: 23/22
c ---[  87]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  85]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  83]---> Adder-cost: 368   maxlim: 999471   bits: 21/20
c ---[  81]---> Sorter-cost: 3227     Base: 2 2 2 5 5 2 2 2 2 2 2 2 2 3
c ---[  73]---> Adder-cost: 330   maxlim: 1694543   bits: 21/21
c ---[  69]---> Sorter-cost: 3277     Base: 2 2 2 5 5 2 2 2 2 2 2 3 2 2 2
c ---[  66]---> BDD-cost:  230
c ---[  65]---> BDD-cost:  661
c ---[  64]---> BDD-cost:  660
c ---[  63]---> Sorter-cost: 1990     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  62]---> Sorter-cost: 2375     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 2299     Base: 5 5 5 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost:  417     Base: 2 2 2 2 2 2 2 2 5 2
c ---[  58]---> Adder-cost: 352   maxlim: 2104143   bits: 22/22
c ---[  57]---> Sorter-cost: 1129     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost: 1147     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost: 1626     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost: 1906     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost: 1910     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  449     Base: 2 2 2 2 2 2 2 2 2 5
c ---[  51]---> Sorter-cost: 1242     Base: 2 2 2 2 2 5 2 2 2 2
c ---[  50]---> Sorter-cost: 1199     Base: 2 2 2 2 2 2 2 2 2 5
c ---[  49]---> Sorter-cost: 1719     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost: 2067     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost: 2487     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2
c ---[  45]---> Sorter-cost: 2045     Base: 5 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  223     Base: 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  590     Base: 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  538     Base: 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost: 1025     Base: 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost: 1211     Base: 2 2 2 2 2 2 2 2 2
c ---[  39]---> Sorter-cost: 1390     Base: 2 2 2 2 2 2 2 2
c ---[  38]---> BDD-cost:    3
c ---[  37]---> BDD-cost:    3
c ---[  36]---> BDD-cost:    3
c ---[  34]---> Adder-cost: 304   maxlim: 2309043   bits: 22/22
c ---[  33]---> BDD-cost:    3
c ---[  32]---> BDD-cost:    3
c ---[  31]---> BDD-cost:    3
c ---[  30]---> BDD-cost:    3
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    3
c ---[  27]---> BDD-cost:   10
c ---[  26]---> BDD-cost:   10
c ---[  25]---> BDD-cost:    3
c ---[  24]---> BDD-cost:    3
c ---[  22]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    3
c ---[  19]---> BDD-cost:   10
c ---[  18]---> BDD-cost:   10
c ---[  17]---> BDD-cost:    3
c ---[  16]---> BDD-cost:    3
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    3
c ---[  13]---> BDD-cost:   10
c ---[  12]---> BDD-cost:   10
c ---[  10]---> Adder-cost: 304   maxlim: 2104243   bits: 22/22
c ---[   9]---> BDD-cost:    3
c ---[   7]---> BDD-cost:   10
c ---[   6]---> BDD-cost:    3
c ---[   5]---> BDD-cost:    3
c ---[   4]---> BDD-cost:    3
c ---[   3]---> BDD-cost:   10
c ---[   1]---> BDD-cost:    3
c ---[   0]---> BDD-cost:    3
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  171009   465211 |   57003       0        0     nan |  0.000 % |
c |       100 |  171009   465211 |   62703     100      301     3.0 |  5.013 % |
c |       250 |  170955   465030 |   68973     248     1123     4.5 |  5.021 % |
c |       475 |  170889   464804 |   75870     469     2572     5.5 |  5.034 % |
c |       812 |  170889   464804 |   83458     806     5643     7.0 |  5.034 % |
c |      1318 |  170889   464804 |   91803    1312     9532     7.3 |  5.034 % |
c |      2078 |  170770   464537 |  100984    2057    17078     8.3 |  5.095 % |
c |      3217 |  170670   464277 |  111082    3191    36361    11.4 |  5.133 % |
c |      4925 |  170452   463665 |  122190    4883    68664    14.1 |  5.204 % |
c |      7487 |  170381   463426 |  134410    7441   140965    18.9 |  5.217 % |
c |     11331 |  170337   463326 |  147851   11280   270345    24.0 |  5.240 % |
c |     17097 |  170184   462861 |  162636   17027   454231    26.7 |  5.286 % |
c |     25747 |  169999   462378 |  178899   25671   760361    29.6 |  5.355 % |
c |     38722 |  169930   462215 |  196789   38642  1187419    30.7 |  5.386 % |
c |     58183 |  169144   460315 |  216468   58035  1779672    30.7 |  5.754 % |
c |     87376 |  168771   459239 |  238115   87199  2667089    30.6 |  5.879 % |
c |    131165 |  168490   458593 |  261927  130929  4223792    32.3 |  6.022 % |
c |    196850 |  168358   458196 |  288119  196605  7204223    36.6 |  6.066 % |
c |    295377 |  167808   456898 |  316931  295051 11243254    38.1 |  6.376 % |
c |    443167 |  167180   455351 |  348625  132107  4751906    36.0 |  6.695 % |
#### 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.56 0.81 0.85 2/56 7642
Raw data (stat): 7642 (runsolver) R 7641 12452 12451 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 434379096 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.0001 s]
Raw data (loadavg): 0.63 0.81 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 5314 0 0 0 988 11 0 0 25 0 1 0 434379096 24494080 5130 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5980 5130 603 41 0 5939 0
vsize: 23920
[startup+20.0008 s]
Raw data (loadavg): 0.69 0.82 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 5782 0 0 0 1986 13 0 0 25 0 1 0 434379096 26357760 5598 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6435 5598 603 41 0 6394 0
vsize: 25740
[startup+30.0016 s]
Raw data (loadavg): 0.73 0.83 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 6061 0 0 0 2986 13 0 0 25 0 1 0 434379096 27435008 5877 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6698 5877 603 41 0 6657 0
vsize: 26792
[startup+40.0014 s]
Raw data (loadavg): 0.77 0.83 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 6379 0 0 0 3984 15 0 0 25 0 1 0 434379096 28897280 6195 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7055 6195 603 41 0 7014 0
vsize: 28220
[startup+50.0012 s]
Raw data (loadavg): 0.81 0.84 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 6645 0 0 0 4983 16 0 0 25 0 1 0 434379096 29974528 6461 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7318 6461 603 41 0 7277 0
vsize: 29272
[startup+60.0015 s]
Raw data (loadavg): 0.84 0.84 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 6884 0 0 0 5983 17 0 0 25 0 1 0 434379096 30912512 6700 4294967295 134512640 134672761 3221224624 3221223792 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7547 6700 603 41 0 7506 0
vsize: 30188
[startup+70.0017 s]
Raw data (loadavg): 0.86 0.85 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 7128 0 0 0 6982 18 0 0 25 0 1 0 434379096 31985664 6944 4294967295 134512640 134672761 3221224624 3221223792 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7809 6944 603 41 0 7768 0
vsize: 31236
[startup+80.0026 s]
Raw data (loadavg): 0.88 0.85 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 7374 0 0 0 7980 19 0 0 25 0 1 0 434379096 32919552 7190 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8037 7190 603 41 0 7996 0
vsize: 32148
[startup+90.0023 s]
Raw data (loadavg): 0.90 0.85 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 7615 0 0 0 8980 20 0 0 25 0 1 0 434379096 34111488 7431 4294967295 134512640 134672761 3221224624 3221223728 134559929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8328 7431 603 41 0 8287 0
vsize: 33312
[startup+100.002 s]
Raw data (loadavg): 0.91 0.86 0.86 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 7892 0 0 0 9979 21 0 0 25 0 1 0 434379096 35176448 7708 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8588 7708 603 41 0 8547 0
vsize: 34352
[startup+110.003 s]
Raw data (loadavg): 0.93 0.86 0.87 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 8154 0 0 0 10978 22 0 0 25 0 1 0 434379096 36237312 7970 4294967295 134512640 134672761 3221224624 3221223792 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8847 7970 603 41 0 8806 0
vsize: 35388
[startup+120.044 s]
Raw data (loadavg): 0.94 0.87 0.87 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 8496 0 0 0 11981 23 0 0 25 0 1 0 434379096 37576704 8312 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9174 8312 603 41 0 9133 0
vsize: 36696
[startup+130.044 s]
Raw data (loadavg): 0.95 0.87 0.87 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 8786 0 0 0 12979 24 0 0 25 0 1 0 434379096 38789120 8602 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9470 8602 603 41 0 9429 0
vsize: 37880
[startup+140.044 s]
Raw data (loadavg): 0.95 0.87 0.87 2/56 7642
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 9027 0 0 0 13979 24 0 0 25 0 1 0 434379096 39735296 8843 4294967295 134512640 134672761 3221224624 3221223760 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9701 8843 603 41 0 9660 0
vsize: 38804
[startup+150.044 s]
Raw data (loadavg): 0.96 0.88 0.87 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 9277 0 0 0 14978 25 0 0 25 0 1 0 434379096 40812544 9093 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9964 9093 603 41 0 9923 0
vsize: 39856
[startup+160.044 s]
Raw data (loadavg): 0.97 0.88 0.87 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 9495 0 0 0 15977 26 0 0 25 0 1 0 434379096 41627648 9311 4294967295 134512640 134672761 3221224624 3221223760 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10163 9311 603 41 0 10122 0
vsize: 40652
[startup+170.043 s]
Raw data (loadavg): 0.97 0.89 0.87 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 9703 0 0 0 16976 27 0 0 25 0 1 0 434379096 42557440 9519 4294967295 134512640 134672761 3221224624 3221223776 134565213 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10390 9519 603 41 0 10349 0
vsize: 41560
[startup+180.043 s]
Raw data (loadavg): 0.98 0.89 0.87 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 9906 0 0 0 17976 28 0 0 25 0 1 0 434379096 43368448 9722 4294967295 134512640 134672761 3221224624 3221223760 134560637 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10588 9722 603 41 0 10547 0
vsize: 42352
[startup+190.044 s]
Raw data (loadavg): 0.98 0.89 0.87 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 10094 0 0 0 18976 28 0 0 25 0 1 0 434379096 44044288 9910 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10753 9910 603 41 0 10712 0
vsize: 43012
[startup+200.044 s]
Raw data (loadavg): 0.98 0.89 0.87 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 10291 0 0 0 19975 29 0 0 25 0 1 0 434379096 44838912 10107 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10947 10107 603 41 0 10906 0
vsize: 43788
[startup+210.044 s]
Raw data (loadavg): 0.98 0.90 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 10473 0 0 0 20975 29 0 0 25 0 1 0 434379096 45662208 10289 4294967295 134512640 134672761 3221224624 3221223824 134557959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11148 10289 603 41 0 11107 0
vsize: 44592
[startup+220.043 s]
Raw data (loadavg): 0.99 0.90 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 10675 0 0 0 21975 30 0 0 25 0 1 0 434379096 47009792 10491 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11477 10491 603 41 0 11436 0
vsize: 45908
[startup+230.044 s]
Raw data (loadavg): 0.99 0.90 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 10791 0 0 0 22974 30 0 0 25 0 1 0 434379096 47443968 10607 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11583 10607 603 41 0 11542 0
vsize: 46332
[startup+240.045 s]
Raw data (loadavg): 0.99 0.91 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 10919 0 0 0 23974 31 0 0 25 0 1 0 434379096 47992832 10735 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11717 10735 603 41 0 11676 0
vsize: 46868
[startup+250.044 s]
Raw data (loadavg): 0.99 0.91 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 11056 0 0 0 24973 31 0 0 25 0 1 0 434379096 48521216 10872 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11846 10872 603 41 0 11805 0
vsize: 47384
[startup+260.045 s]
Raw data (loadavg): 0.99 0.91 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 11191 0 0 0 25973 32 0 0 25 0 1 0 434379096 49057792 11007 4294967295 134512640 134672761 3221224624 3221223792 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11977 11007 603 41 0 11936 0
vsize: 47908
[startup+270.044 s]
Raw data (loadavg): 0.99 0.91 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 11343 0 0 0 26973 32 0 0 25 0 1 0 434379096 49729536 11159 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12141 11159 603 41 0 12100 0
vsize: 48564
[startup+280.045 s]
Raw data (loadavg): 0.99 0.92 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 11465 0 0 0 27973 33 0 0 25 0 1 0 434379096 50151424 11281 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12244 11281 603 41 0 12203 0
vsize: 48976
[startup+290.046 s]
Raw data (loadavg): 0.99 0.92 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 11571 0 0 0 28973 33 0 0 25 0 1 0 434379096 50683904 11387 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12374 11387 603 41 0 12333 0
vsize: 49496
[startup+300.046 s]
Raw data (loadavg): 0.99 0.92 0.88 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 11702 0 0 0 29973 33 0 0 25 0 1 0 434379096 51216384 11518 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12504 11518 603 41 0 12463 0
vsize: 50016
[startup+310.046 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 11824 0 0 0 30973 33 0 0 25 0 1 0 434379096 51617792 11640 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12602 11640 603 41 0 12561 0
vsize: 50408
[startup+320.046 s]
Raw data (loadavg): 0.99 0.92 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 11929 0 0 0 31973 33 0 0 25 0 1 0 434379096 52056064 11745 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12709 11745 603 41 0 12668 0
vsize: 50836
[startup+330.047 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 12029 0 0 0 32973 34 0 0 25 0 1 0 434379096 52457472 11845 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12807 11845 603 41 0 12766 0
vsize: 51228
[startup+340.047 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 12126 0 0 0 33973 34 0 0 25 0 1 0 434379096 52854784 11942 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12904 11942 603 41 0 12863 0
vsize: 51616
[startup+350.047 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 12260 0 0 0 34972 34 0 0 25 0 1 0 434379096 53452800 12076 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13050 12076 603 41 0 13009 0
vsize: 52200
[startup+360.048 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 12355 0 0 0 35972 35 0 0 25 0 1 0 434379096 53923840 12171 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13165 12171 603 41 0 13124 0
vsize: 52660
[startup+370.047 s]
Raw data (loadavg): 0.99 0.93 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 12466 0 0 0 36972 35 0 0 25 0 1 0 434379096 54325248 12282 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13263 12282 603 41 0 13222 0
vsize: 53052
[startup+380.048 s]
Raw data (loadavg): 0.99 0.94 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 12626 0 0 0 37971 36 0 0 25 0 1 0 434379096 54988800 12442 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13425 12442 603 41 0 13384 0
vsize: 53700
[startup+390.048 s]
Raw data (loadavg): 0.99 0.94 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 12776 0 0 0 38971 37 0 0 25 0 1 0 434379096 55685120 12592 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13595 12592 603 41 0 13554 0
vsize: 54380
[startup+400.048 s]
Raw data (loadavg): 0.99 0.94 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 12934 0 0 0 39971 37 0 0 25 0 1 0 434379096 56221696 12750 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13726 12750 603 41 0 13685 0
vsize: 54904
[startup+410.047 s]
Raw data (loadavg): 0.99 0.94 0.89 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13030 0 0 0 40970 37 0 0 25 0 1 0 434379096 56619008 12846 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13823 12846 603 41 0 13782 0
vsize: 55292
[startup+420.047 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13140 0 0 0 41970 38 0 0 25 0 1 0 434379096 57020416 12956 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13921 12956 603 41 0 13880 0
vsize: 55684
[startup+430.048 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13265 0 0 0 42970 38 0 0 25 0 1 0 434379096 57569280 13081 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14055 13081 603 41 0 14014 0
vsize: 56220
[startup+440.048 s]
Raw data (loadavg): 0.99 0.94 0.90 2/56 7644
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13386 0 0 0 43970 39 0 0 25 0 1 0 434379096 58105856 13202 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14186 13202 603 41 0 14145 0
vsize: 56744
[startup+450.048 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13516 0 0 0 44969 39 0 0 25 0 1 0 434379096 58642432 13332 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14317 13332 603 41 0 14276 0
vsize: 57268
[startup+460.047 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13630 0 0 0 45969 39 0 0 25 0 1 0 434379096 59043840 13446 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14415 13446 603 41 0 14374 0
vsize: 57660
[startup+470.047 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13755 0 0 0 46969 40 0 0 25 0 1 0 434379096 59580416 13571 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14546 13571 603 41 0 14505 0
vsize: 58184
[startup+480.047 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13870 0 0 0 47969 40 0 0 25 0 1 0 434379096 60108800 13686 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14675 13686 603 41 0 14634 0
vsize: 58700
[startup+490.047 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 13976 0 0 0 48968 41 0 0 25 0 1 0 434379096 60506112 13792 4294967295 134512640 134672761 3221224624 3221223728 134555175 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14772 13792 603 41 0 14731 0
vsize: 59088
[startup+500.046 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 14073 0 0 0 49968 41 0 0 25 0 1 0 434379096 60899328 13889 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14868 13889 603 41 0 14827 0
vsize: 59472
[startup+510.046 s]
Raw data (loadavg): 0.99 0.95 0.90 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 14238 0 0 0 50968 42 0 0 25 0 1 0 434379096 61599744 14054 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15039 14054 603 41 0 14998 0
vsize: 60156
[startup+520.046 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 14338 0 0 0 51967 42 0 0 25 0 1 0 434379096 62017536 14154 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15141 14154 603 41 0 15100 0
vsize: 60564
[startup+530.047 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 14485 0 0 0 52967 43 0 0 25 0 1 0 434379096 62545920 14301 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15270 14301 603 41 0 15229 0
vsize: 61080
[startup+540.048 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 14620 0 0 0 53967 43 0 0 25 0 1 0 434379096 63074304 14436 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15399 14436 603 41 0 15358 0
vsize: 61596
[startup+550.048 s]
Raw data (loadavg): 0.99 0.95 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 14749 0 0 0 54966 44 0 0 25 0 1 0 434379096 63602688 14565 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15528 14565 603 41 0 15487 0
vsize: 62112
[startup+560.047 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 15002 0 0 0 55965 45 0 0 25 0 1 0 434379096 64667648 14818 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15788 14818 603 41 0 15747 0
vsize: 63152
[startup+570.048 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 15087 0 0 0 56965 45 0 0 25 0 1 0 434379096 65069056 14903 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15886 14903 603 41 0 15845 0
vsize: 63544
[startup+580.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 15203 0 0 0 57965 46 0 0 25 0 1 0 434379096 65466368 15019 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15983 15019 603 41 0 15942 0
vsize: 63932
[startup+590.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 15319 0 0 0 58964 47 0 0 25 0 1 0 434379096 66019328 15135 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16118 15135 603 41 0 16077 0
vsize: 64472
[startup+600.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 15455 0 0 0 59963 48 0 0 25 0 1 0 434379096 66564096 15271 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16251 15271 603 41 0 16210 0
vsize: 65004
[startup+610.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 15624 0 0 0 60962 48 0 0 25 0 1 0 434379096 67227648 15440 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16413 15440 603 41 0 16372 0
vsize: 65652
[startup+620.049 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 15796 0 0 0 61962 49 0 0 25 0 1 0 434379096 68026368 15612 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16608 15612 603 41 0 16567 0
vsize: 66432
[startup+630.05 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 15916 0 0 0 62962 49 0 0 25 0 1 0 434379096 68431872 15732 4294967295 134512640 134672761 3221224624 3221223792 134564673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16707 15732 603 41 0 16666 0
vsize: 66828
[startup+640.051 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 16151 0 0 0 63962 50 0 0 25 0 1 0 434379096 69365760 15967 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16935 15967 603 41 0 16894 0
vsize: 67740
[startup+650.05 s]
Raw data (loadavg): 0.99 0.96 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 16281 0 0 0 64961 50 0 0 25 0 1 0 434379096 69955584 16097 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17079 16097 603 41 0 17038 0
vsize: 68316
[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 16394 0 0 0 65961 51 0 0 25 0 1 0 434379096 70356992 16210 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17177 16210 603 41 0 17136 0
vsize: 68708
[startup+670.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 16516 0 0 0 66961 51 0 0 25 0 1 0 434379096 70914048 16332 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17313 16332 603 41 0 17272 0
vsize: 69252
[startup+680.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 16609 0 0 0 67961 52 0 0 25 0 1 0 434379096 71315456 16425 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17411 16425 603 41 0 17370 0
vsize: 69644
[startup+690.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 16717 0 0 0 68960 52 0 0 25 0 1 0 434379096 71712768 16533 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17508 16533 603 41 0 17467 0
vsize: 70032
[startup+700.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 16837 0 0 0 69960 52 0 0 25 0 1 0 434379096 72237056 16653 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17636 16653 603 41 0 17595 0
vsize: 70544
[startup+710.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 16944 0 0 0 70960 53 0 0 25 0 1 0 434379096 72671232 16760 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17742 16760 603 41 0 17701 0
vsize: 70968
[startup+720.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 17058 0 0 0 71960 53 0 0 25 0 1 0 434379096 73076736 16874 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17841 16874 603 41 0 17800 0
vsize: 71364
[startup+730.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 17161 0 0 0 72960 54 0 0 25 0 1 0 434379096 73478144 16977 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17939 16977 603 41 0 17898 0
vsize: 71756
[startup+740.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7646
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 17259 0 0 0 73960 54 0 0 25 0 1 0 434379096 73879552 17075 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18037 17075 603 41 0 17996 0
vsize: 72148
[startup+750.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 17385 0 0 0 74960 54 0 0 25 0 1 0 434379096 74420224 17201 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18169 17201 603 41 0 18128 0
vsize: 72676
[startup+760.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 17628 0 0 0 75959 55 0 0 25 0 1 0 434379096 75481088 17444 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18428 17444 603 41 0 18387 0
vsize: 73712
[startup+770.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 17791 0 0 0 76958 55 0 0 25 0 1 0 434379096 77201408 17607 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18848 17607 603 41 0 18807 0
vsize: 75392
[startup+780.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 17890 0 0 0 77958 56 0 0 25 0 1 0 434379096 77467648 17706 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18913 17706 603 41 0 18872 0
vsize: 75652
[startup+790.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 17991 0 0 0 78958 56 0 0 25 0 1 0 434379096 77881344 17807 4294967295 134512640 134672761 3221224624 3221223792 134561161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19014 17807 603 41 0 18973 0
vsize: 76056
[startup+800.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 18099 0 0 0 79958 56 0 0 25 0 1 0 434379096 78413824 17915 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19144 17915 603 41 0 19103 0
vsize: 76576
[startup+810.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 18290 0 0 0 80958 57 0 0 25 0 1 0 434379096 79241216 18106 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19346 18106 603 41 0 19305 0
vsize: 77384
[startup+820.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 18441 0 0 0 81958 57 0 0 25 0 1 0 434379096 79773696 18257 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19476 18257 603 41 0 19435 0
vsize: 77904
[startup+830.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 18605 0 0 0 82958 57 0 0 25 0 1 0 434379096 80449536 18421 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19641 18421 603 41 0 19600 0
vsize: 78564
[startup+840.053 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 18704 0 0 0 83958 57 0 0 25 0 1 0 434379096 80850944 18520 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19739 18520 603 41 0 19698 0
vsize: 78956
[startup+850.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 18804 0 0 0 84957 58 0 0 25 0 1 0 434379096 81252352 18620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19837 18620 603 41 0 19796 0
vsize: 79348
[startup+860.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 18893 0 0 0 85957 58 0 0 25 0 1 0 434379096 81657856 18709 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19936 18709 603 41 0 19895 0
vsize: 79744
[startup+870.052 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 18987 0 0 0 86957 59 0 0 25 0 1 0 434379096 82059264 18803 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20034 18803 603 41 0 19993 0
vsize: 80136
[startup+880.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 19063 0 0 0 87957 59 0 0 25 0 1 0 434379096 82325504 18879 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20099 18879 603 41 0 20058 0
vsize: 80396
[startup+890.055 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 19152 0 0 0 88957 59 0 0 25 0 1 0 434379096 82722816 18968 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20196 18968 603 41 0 20155 0
vsize: 80784
[startup+900.061 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 19264 0 0 0 89957 59 0 0 25 0 1 0 434379096 83144704 19080 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20299 19080 603 41 0 20258 0
vsize: 81196
[startup+910.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 19469 0 0 0 90957 60 0 0 25 0 1 0 434379096 83955712 19285 4294967295 134512640 134672761 3221224624 3221223728 134560226 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20497 19285 603 41 0 20456 0
vsize: 81988
[startup+920.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 19705 0 0 0 91956 61 0 0 25 0 1 0 434379096 85012480 19521 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20755 19521 603 41 0 20714 0
vsize: 83020
[startup+930.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 19804 0 0 0 92955 61 0 0 25 0 1 0 434379096 85454848 19620 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20863 19620 603 41 0 20822 0
vsize: 83452
[startup+940.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 19869 0 0 0 93955 62 0 0 25 0 1 0 434379096 85585920 19685 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20895 19685 603 41 0 20854 0
vsize: 83580
[startup+950.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 19982 0 0 0 94954 62 0 0 25 0 1 0 434379096 86110208 19798 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21023 19798 603 41 0 20982 0
vsize: 84092
[startup+960.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 20075 0 0 0 95954 63 0 0 25 0 1 0 434379096 86511616 19891 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21121 19891 603 41 0 21080 0
vsize: 84484
[startup+970.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 20324 0 0 0 96954 63 0 0 25 0 1 0 434379096 87453696 20140 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21351 20140 603 41 0 21310 0
vsize: 85404
[startup+980.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 20521 0 0 0 97954 64 0 0 25 0 1 0 434379096 88264704 20337 4294967295 134512640 134672761 3221224624 3221223760 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21549 20337 603 41 0 21508 0
vsize: 86196
[startup+990.071 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 20766 0 0 0 98953 65 0 0 25 0 1 0 434379096 89333760 20582 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21810 20582 603 41 0 21769 0
vsize: 87240
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 20941 0 0 0 99953 65 0 0 25 0 1 0 434379096 90005504 20757 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21974 20757 603 41 0 21933 0
vsize: 87896
[startup+1010.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21120 0 0 0 100953 66 0 0 25 0 1 0 434379096 90664960 20936 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22135 20936 603 41 0 22094 0
vsize: 88540
[startup+1020.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 101953 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1030.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 102953 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1040.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7648
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 103953 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223728 134560248 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 104954 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1060.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 105954 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1070.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 106954 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1080.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 107954 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1090.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 108954 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1100.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21221 0 0 0 109954 66 0 0 25 0 1 0 434379096 91066368 21037 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21037 603 41 0 22192 0
vsize: 88932
[startup+1110.08 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21222 0 0 0 110955 66 0 0 25 0 1 0 434379096 91066368 21038 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21038 603 41 0 22192 0
vsize: 88932
[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21223 0 0 0 111956 66 0 0 25 0 1 0 434379096 91066368 21039 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21039 603 41 0 22192 0
vsize: 88932
[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21223 0 0 0 112956 66 0 0 25 0 1 0 434379096 91066368 21039 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21039 603 41 0 22192 0
vsize: 88932
[startup+1140.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21223 0 0 0 113957 66 0 0 25 0 1 0 434379096 91066368 21039 4294967295 134512640 134672761 3221224624 3221223792 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21039 603 41 0 22192 0
vsize: 88932
[startup+1150.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21223 0 0 0 114957 66 0 0 25 0 1 0 434379096 91066368 21039 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21039 603 41 0 22192 0
vsize: 88932
[startup+1160.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21223 0 0 0 115958 66 0 0 25 0 1 0 434379096 91066368 21039 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21039 603 41 0 22192 0
vsize: 88932
[startup+1170.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21223 0 0 0 116958 66 0 0 25 0 1 0 434379096 91066368 21039 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21039 603 41 0 22192 0
vsize: 88932
[startup+1180.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21225 0 0 0 117958 66 0 0 25 0 1 0 434379096 91066368 21041 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21041 603 41 0 22192 0
vsize: 88932
[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21225 0 0 0 118959 66 0 0 25 0 1 0 434379096 91066368 21041 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22233 21041 603 41 0 22192 0
vsize: 88932
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.91 2/56 7650
Raw data (stat): 7642 (minisat+) R 7641 12452 12451 0 -1 0 21225 0 0 0 119957 66 0 0 25 0 1 0 434379096 91066368 21041 4294967295 134512640 134672761 3221224624 3221223728 134559937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22233 21041 603 41 0 22192 0
vsize: 88932
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 0.99 0.97 0.91 1/56 7650
Raw data (stat): 7642 (minisat+) Z 7641 12452 12451 0 -1 12 21227 0 0 0 119957 70 0 0 24 0 1 0 434379096 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.17
CPU time (s): 1200.28
CPU user time (s): 1199.57
CPU system time (s): 0.705892
CPU usage (%): 100.009
Max. virtual memory (Kb): 88932
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####