PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm1.opb
MD5SUM	ec9e3281577e2d3f7b25c1cc88cac9ea
Bench Category	optimization, small integers (OPTSMALLINT)
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	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.06884
Number of variables	2124
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	64
Trace number 17999

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc18 THE 2005-04-21 13:04:08 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18939 boxname=wulflinc18 idbench=1457 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ec9e3281577e2d3f7b25c1cc88cac9ea  /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-vpm1.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-vpm1.opb /oldhome/oroussel/tmp/wulflinc18/normalized-mps-v2-13-7-vpm1.opb
IDLAUNCH: 18939
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.177
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	: 3
cpu MHz		: 451.177
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:        884544 kB
Buffers:          7836 kB
Cached:         119324 kB
SwapCached:        748 kB
Active:          27592 kB
Inactive:       101560 kB
HighTotal:      131008 kB
HighFree:        28812 kB
LowTotal:       903652 kB
LowFree:        855732 kB
SwapTotal:     2097892 kB
SwapFree:      2096168 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5100 kB
Slab:            15324 kB
Committed_AS:    63816 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 13:24:11 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 18939 7 1200.28 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> BDD-cost:    7
c ---[ 484]---> BDD-cost:    7
c ---[ 483]---> BDD-cost:    7
c ---[ 482]---> BDD-cost:    7
c ---[ 481]---> BDD-cost:    7
c ---[ 480]---> BDD-cost:    7
c ---[ 479]---> BDD-cost:    7
c ---[ 478]---> BDD-cost:    7
c ---[ 477]---> BDD-cost:    7
c ---[ 474]---> BDD-cost:    7
c ---[ 473]---> BDD-cost:    7
c ---[ 472]---> BDD-cost:    7
c ---[ 471]---> BDD-cost:    7
c ---[ 468]---> BDD-cost:    7
c ---[ 467]---> BDD-cost:    7
c ---[ 466]---> BDD-cost:    7
c ---[ 465]---> BDD-cost:    7
c ---[ 462]---> BDD-cost:    7
c ---[ 459]---> BDD-cost:    7
c ---[ 458]---> BDD-cost:    7
c ---[ 457]---> BDD-cost:    7
c ---[ 454]---> BDD-cost:    7
c ---[ 453]---> BDD-cost:    7
c ---[ 452]---> BDD-cost:    7
c ---[ 451]---> BDD-cost:    7
c ---[ 450]---> BDD-cost:    7
c ---[ 448]---> BDD-cost:    7
c ---[ 447]---> BDD-cost:    7
c ---[ 446]---> BDD-cost:    7
c ---[ 445]---> BDD-cost:    7
c ---[ 444]---> BDD-cost:    7
c ---[ 441]---> BDD-cost:    7
c ---[ 440]---> BDD-cost:    7
c ---[ 439]---> BDD-cost:    7
c ---[ 433]---> BDD-cost:    7
c ---[ 427]---> BDD-cost:    7
c ---[ 422]---> BDD-cost:    7
c ---[ 421]---> BDD-cost:    7
c ---[ 415]---> BDD-cost:    7
c ---[ 409]---> BDD-cost:    7
c ---[ 408]---> BDD-cost:    7
c ---[ 402]---> BDD-cost:    7
c ---[ 397]---> BDD-cost:    7
c ---[ 396]---> BDD-cost:    7
c ---[ 391]---> BDD-cost:    7
c ---[ 390]---> BDD-cost:    7
c ---[ 386]---> BDD-cost:    7
c ---[ 385]---> BDD-cost:    7
c ---[ 384]---> BDD-cost:    7
c ---[ 380]---> BDD-cost:    7
c ---[ 379]---> BDD-cost:    7
c ---[ 378]---> BDD-cost:    7
c ---[ 374]---> BDD-cost:    7
c ---[ 373]---> BDD-cost:    7
c ---[ 372]---> BDD-cost:    7
c ---[ 368]---> BDD-cost:    7
c ---[ 367]---> BDD-cost:    7
c ---[ 366]---> BDD-cost:    7
c ---[ 365]---> BDD-cost:    7
c ---[ 364]---> BDD-cost:    7
c ---[ 359]---> BDD-cost:    7
c ---[ 353]---> BDD-cost:    7
c ---[ 347]---> BDD-cost:    7
c ---[ 339]---> BDD-cost:    7
c ---[ 333]---> BDD-cost:    7
c ---[ 327]---> BDD-cost:    7
c ---[ 321]---> BDD-cost:    7
c ---[ 317]---> BDD-cost:   14
c ---[ 316]---> BDD-cost:   14
c ---[ 315]---> BDD-cost:   14
c ---[ 314]---> BDD-cost:   14
c ---[ 313]---> BDD-cost:   14
c ---[ 312]---> BDD-cost:   14
c ---[ 310]---> BDD-cost:   14
c ---[ 309]---> BDD-cost:   14
c ---[ 308]---> BDD-cost:   14
c ---[ 307]---> BDD-cost:   14
c ---[ 306]---> BDD-cost:   14
c ---[ 302]---> BDD-cost:   13
c ---[ 301]---> BDD-cost:   13
c ---[ 300]---> BDD-cost:   13
c ---[ 295]---> BDD-cost:   13
c ---[ 294]---> BDD-cost:   13
c ---[ 290]---> BDD-cost:   15
c ---[ 289]---> BDD-cost:   15
c ---[ 288]---> BDD-cost:   15
c ---[ 287]---> BDD-cost:   13
c ---[ 286]---> BDD-cost:   13
c ---[ 285]---> BDD-cost:   13
c ---[ 284]---> BDD-cost:   13
c ---[ 283]---> BDD-cost:   13
c ---[ 282]---> BDD-cost:   13
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   13
c ---[ 278]---> BDD-cost:   13
c ---[ 277]---> BDD-cost:   13
c ---[ 276]---> BDD-cost:   13
c ---[ 274]---> Sorter-cost: 1988     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 264]---> Sorter-cost: 1826     Base: 2 2 2 5 5 2 2 2 3 2 2 2
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 254]---> Sorter-cost: 2565     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Sorter-cost: 1411     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 248]---> Sorter-cost: 2230     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 246]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 244]---> Sorter-cost: 2232     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 242]---> Sorter-cost: 2159     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[ 236]---> Sorter-cost: 1318     Base: 2 2 2 2 5 5 2 2 2 2 2
c ---[ 234]---> Sorter-cost: 2540     Base: 2 2 2 2 5 5 2 2 2 2 2 2
c ---[ 232]---> Sorter-cost: 1903     Base: 2 2 2 2 2 2 2 2 2 2 2 3
c ---[ 224]---> Sorter-cost: 1582     Base: 2 2 2 5 5 2 2 2 2 2 3
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Sorter-cost: 1742     Base: 2 2 2 5 5 2 2 2 2 2 2
c ---[ 214]---> Sorter-cost: 2471     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 212]---> Sorter-cost: 2473     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2
c ---[ 210]---> Sorter-cost: 3095     Base: 2 2 2 2 2 3 5 2 2 2 5
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Sorter-cost: 1882     Base: 2 2 2 2 5 5 2 2 2 5
c ---[ 198]---> Sorter-cost: 3211     Base: 2 2 2 2 5 5 2 2 2 2 5
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> BDD-cost:   33
c ---[ 190]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 188]---> Sorter-cost:  540     Base: 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  761     Base: 2 2 2 2 2 2
c ---[ 186]---> Sorter-cost:  655     Base: 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   33
c ---[ 184]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost:  283     Base: 2 2 2 2 2 2
c ---[ 182]---> Sorter-cost:  520     Base: 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost:  707     Base: 2 2 2 2 2 2
c ---[ 180]---> Sorter-cost:  705     Base: 2 2 2 2 2 2
c ---[ 179]---> BDD-cost:   33
c ---[ 178]---> Sorter-cost:  269     Base: 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 176]---> Sorter-cost:  527     Base: 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost:  720     Base: 2 2 2 2 2 2
c ---[ 174]---> Sorter-cost:  692     Base: 2 2 2 2 2 2
c ---[ 173]---> BDD-cost:   33
c ---[ 172]---> Sorter-cost:  253     Base: 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost:  274     Base: 2 2 2 2 2 2
c ---[ 170]---> Sorter-cost:  486     Base: 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  695     Base: 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost:  625     Base: 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:    7
c ---[ 157]---> BDD-cost:    7
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    3
c ---[ 152]---> BDD-cost:    7
c ---[ 151]---> BDD-cost:    7
c ---[ 150]---> BDD-cost:    3
c ---[ 149]---> BDD-cost:    3
c ---[ 148]---> BDD-cost:    3
c ---[ 147]---> BDD-cost:    3
c ---[ 146]---> BDD-cost:    7
c ---[ 145]---> BDD-cost:    7
c ---[ 144]---> BDD-cost:    3
c ---[ 142]---> BDD-cost:    7
c ---[ 141]---> BDD-cost:    3
c ---[ 140]---> BDD-cost:    3
c ---[ 139]---> BDD-cost:    3
c ---[ 138]---> BDD-cost:    7
c ---[ 136]---> BDD-cost:    3
c ---[ 135]---> BDD-cost:    3
c ---[ 134]---> BDD-cost:    3
c ---[ 133]---> BDD-cost:    3
c ---[ 132]---> BDD-cost:    3
c ---[ 130]---> BDD-cost:    3
c ---[ 129]---> BDD-cost:    3
c ---[ 128]---> BDD-cost:    3
c ---[ 127]---> BDD-cost:    3
c ---[ 126]---> BDD-cost:    3
c ---[ 124]---> BDD-cost:    7
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> BDD-cost:    3
c ---[ 121]---> BDD-cost:    3
c ---[ 120]---> BDD-cost:    7
c ---[ 116]---> BDD-cost:    7
c ---[ 115]---> BDD-cost:    3
c ---[ 114]---> BDD-cost:    6
c ---[ 110]---> BDD-cost:    7
c ---[ 109]---> BDD-cost:    3
c ---[ 108]---> BDD-cost:    6
c ---[ 104]---> BDD-cost:    3
c ---[ 103]---> BDD-cost:    3
c ---[ 102]---> BDD-cost:    5
c ---[  98]---> BDD-cost:    7
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:    6
c ---[  91]---> BDD-cost:    3
c ---[  90]---> BDD-cost:    3
c ---[  85]---> BDD-cost:    7
c ---[  84]---> BDD-cost:    3
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:    3
c ---[  73]---> BDD-cost:    3
c ---[  72]---> BDD-cost:    3
c ---[  68]---> BDD-cost:    3
c ---[  67]---> BDD-cost:    3
c ---[  66]---> BDD-cost:    3
c ---[  62]---> BDD-cost:    3
c ---[  61]---> BDD-cost:    3
c ---[  60]---> BDD-cost:    3
c ---[  56]---> BDD-cost:    3
c ---[  55]---> BDD-cost:    3
c ---[  54]---> BDD-cost:    3
c ---[  50]---> BDD-cost:    3
c ---[  49]---> BDD-cost:    3
c ---[  48]---> BDD-cost:    3
c ---[  47]---> BDD-cost:    3
c ---[  46]---> BDD-cost:    3
c ---[  45]---> BDD-cost:    6
c ---[  44]---> BDD-cost:    6
c ---[  43]---> BDD-cost:    6
c ---[  42]---> BDD-cost:    6
c ---[  41]---> BDD-cost:    3
c ---[  40]---> BDD-cost:    7
c ---[  39]---> BDD-cost:    6
c ---[  38]---> BDD-cost:    6
c ---[  37]---> BDD-cost:    6
c ---[  36]---> BDD-cost:    6
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:    7
c ---[  33]---> BDD-cost:    5
c ---[  32]---> BDD-cost:    5
c ---[  31]---> BDD-cost:    5
c ---[  30]---> BDD-cost:    5
c ---[  29]---> BDD-cost:    3
c ---[  28]---> BDD-cost:    7
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:    5
c ---[  25]---> BDD-cost:    5
c ---[  24]---> BDD-cost:    5
c ---[  22]---> BDD-cost:    7
c ---[  21]---> BDD-cost:    3
c ---[  20]---> BDD-cost:    6
c ---[  19]---> BDD-cost:    6
c ---[  18]---> BDD-cost:    6
c ---[  16]---> BDD-cost:    7
c ---[  15]---> BDD-cost:    3
c ---[  14]---> BDD-cost:    6
c ---[  13]---> BDD-cost:    6
c ---[  12]---> BDD-cost:    6
c ---[  10]---> BDD-cost:    7
c ---[   9]---> BDD-cost:    3
c ---[   8]---> BDD-cost:    6
c ---[   7]---> BDD-cost:    6
c ---[   6]---> BDD-cost:    6
c ---[   4]---> BDD-cost:    6
c ---[   3]---> BDD-cost:    3
c ---[   2]---> BDD-cost:    5
c ---[   1]---> BDD-cost:    5
c ---[   0]---> BDD-cost:    5
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  150816   377413 |   45244       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/46036          
c   -- var.elim.:  2000/46036          
c   -- var.elim.:  3000/46036          
c   -- var.elim.:  4000/46036          
c   -- var.elim.:  5000/46036          
c   -- var.elim.:  6000/46036          
c   -- var.elim.:  7000/46036          
c   -- var.elim.:  8000/46036          
c   -- var.elim.:  9000/46036          
c   -- var.elim.:  10000/46036          
c   -- var.elim.:  11000/46036          
c   -- var.elim.:  12000/46036          
c   -- var.elim.:  13000/46036          
c   -- var.elim.:  14000/46036          
c   -- var.elim.:  15000/46036          
c   -- var.elim.:  16000/46036          
c   -- var.elim.:  17000/46036          
c   -- var.elim.:  18000/46036          
c   -- var.elim.:  19000/46036          
c   -- var.elim.:  20000/46036          
c   -- var.elim.:  21000/46036          
c   -- var.elim.:  22000/46036          
c   -- var.elim.:  23000/46036          
c   -- var.elim.:  24000/46036          
c   -- var.elim.:  25000/46036          
c   -- var.elim.:  26000/46036          
c   -- var.elim.:  27000/46036          
c   -- var.elim.:  28000/46036          
c   -- var.elim.:  29000/46036          
c   -- var.elim.:  30000/46036          
c   -- var.elim.:  31000/46036          
c   -- var.elim.:  32000/46036          
c   -- var.elim.:  33000/46036          
c   -- var.elim.:  34000/46036          
c   -- var.elim.:  35000/46036          
c   -- var.elim.:  36000/46036          
c   -- var.elim.:  37000/46036          
c   -- var.elim.:  38000/46036          
c   -- var.elim.:  39000/46036          
c   -- var.elim.:  40000/460#### 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.95 0.90 2/55 29804
Raw data (stat): 29804 (runsolver) R 29803 20024 20023 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545286571 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.95 0.90 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 8802 0 0 0 970 28 0 0 25 0 1 0 545286571 35987456 7584 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8786 7584 603 41 0 8745 0
vsize: 35144
[startup+20.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 9209 0 0 0 1967 30 0 0 25 0 1 0 545286571 37638144 7991 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9189 7991 603 41 0 9148 0
vsize: 36756
[startup+30.0034 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 9895 0 0 0 2966 32 0 0 25 0 1 0 545286571 40394752 8677 4294967295 134512640 134672761 3221224544 3221223744 134610528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9862 8677 603 41 0 9821 0
vsize: 39448
[startup+40.0033 s]
Raw data (loadavg): 0.95 0.96 0.91 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 10825 0 0 0 3963 34 0 0 25 0 1 0 545286571 44240896 9607 4294967295 134512640 134672761 3221224544 3221223584 134612659 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10801 9607 603 41 0 10760 0
vsize: 43204
[startup+50.0037 s]
Raw data (loadavg): 0.96 0.96 0.91 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 11472 0 0 0 4961 36 0 0 25 0 1 0 545286571 46886912 10254 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11447 10254 603 41 0 11406 0
vsize: 45788
[startup+60.0039 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 12604 0 0 0 5958 38 0 0 25 0 1 0 545286571 51503104 11386 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12574 11386 603 41 0 12533 0
vsize: 50296
[startup+70.0048 s]
Raw data (loadavg): 0.97 0.96 0.91 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 13330 0 0 0 6956 41 0 0 25 0 1 0 545286571 54538240 12112 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13315 12112 603 41 0 13274 0
vsize: 53260
[startup+80.0055 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 14302 0 0 0 7954 43 0 0 25 0 1 0 545286571 58630144 13084 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14314 13084 603 41 0 14273 0
vsize: 57256
[startup+90.0059 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29804
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 15011 0 0 0 8953 45 0 0 25 0 1 0 545286571 61526016 13793 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15021 13793 603 41 0 14980 0
vsize: 60084
[startup+100.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29806
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 16107 0 0 0 9949 49 0 0 25 0 1 0 545286571 65994752 14889 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16112 14889 603 41 0 16071 0
vsize: 64448
[startup+110.007 s]
Raw data (loadavg): 0.98 0.96 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 16789 0 0 0 10947 51 0 0 25 0 1 0 545286571 68784128 15571 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16793 15571 603 41 0 16752 0
vsize: 67172
[startup+120.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 17443 0 0 0 11946 52 0 0 25 0 1 0 545286571 71442432 16225 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17442 16225 603 41 0 17401 0
vsize: 69768
[startup+130.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 18030 0 0 0 12945 54 0 0 25 0 1 0 545286571 73822208 16812 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18023 16812 603 41 0 17982 0
vsize: 72092
[startup+140.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 18475 0 0 0 13944 55 0 0 25 0 1 0 545286571 75694080 17257 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18480 17257 603 41 0 18439 0
vsize: 73920
[startup+150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 18905 0 0 0 14943 56 0 0 25 0 1 0 545286571 77406208 17687 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18898 17687 603 41 0 18857 0
vsize: 75592
[startup+160.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 19203 0 0 0 15943 56 0 0 25 0 1 0 545286571 78602240 17985 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19190 17985 603 41 0 19149 0
vsize: 76760
[startup+170.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 19571 0 0 0 16942 58 0 0 25 0 1 0 545286571 80048128 18353 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19543 18353 603 41 0 19502 0
vsize: 78172
[startup+180.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 19941 0 0 0 17941 59 0 0 25 0 1 0 545286571 81629184 18723 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19929 18723 603 41 0 19888 0
vsize: 79716
[startup+190.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 20385 0 0 0 18939 60 0 0 25 0 1 0 545286571 83386368 19167 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20358 19167 603 41 0 20317 0
vsize: 81432
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 20683 0 0 0 19938 62 0 0 25 0 1 0 545286571 84713472 19465 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20682 19465 603 41 0 20641 0
vsize: 82728
[startup+210.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 20993 0 0 0 20937 63 0 0 25 0 1 0 545286571 86425600 19775 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21100 19775 603 41 0 21059 0
vsize: 84400
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 21304 0 0 0 21936 64 0 0 25 0 1 0 545286571 87736320 20086 4294967295 134512640 134672761 3221224544 3221223536 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21420 20086 603 41 0 21379 0
vsize: 85680
[startup+230.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 21658 0 0 0 22935 66 0 0 25 0 1 0 545286571 89182208 20440 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21773 20440 603 41 0 21732 0
vsize: 87092
[startup+240.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 22018 0 0 0 23933 67 0 0 25 0 1 0 545286571 90636288 20800 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22128 20800 603 41 0 22087 0
vsize: 88512
[startup+250.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 22363 0 0 0 24933 68 0 0 25 0 1 0 545286571 92078080 21145 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22480 21145 603 41 0 22439 0
vsize: 89920
[startup+260.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 23063 0 0 0 25931 70 0 0 25 0 1 0 545286571 94851072 21845 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23157 21845 603 41 0 23116 0
vsize: 92628
[startup+270.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 23807 0 0 0 26929 72 0 0 25 0 1 0 545286571 97890304 22589 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23899 22590 603 41 0 23858 0
vsize: 95596
[startup+280.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 24508 0 0 0 27927 74 0 0 25 0 1 0 545286571 100777984 23290 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24604 23290 603 41 0 24563 0
vsize: 98416
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 25140 0 0 0 28925 76 0 0 25 0 1 0 545286571 103313408 23922 4294967295 134512640 134672761 3221224544 3221223536 134565137 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25223 23922 603 41 0 25182 0
vsize: 100892
[startup+300.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 25771 0 0 0 29924 78 0 0 25 0 1 0 545286571 105955328 24553 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25868 24553 603 41 0 25827 0
vsize: 103472
[startup+310.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 26353 0 0 0 30923 79 0 0 25 0 1 0 545286571 108331008 25135 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26448 25135 603 41 0 26407 0
vsize: 105792
[startup+320.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 26895 0 0 0 31922 80 0 0 25 0 1 0 545286571 110575616 25677 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26996 25677 603 41 0 26955 0
vsize: 107984
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 27353 0 0 0 32920 82 0 0 25 0 1 0 545286571 112414720 26135 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27445 26135 603 41 0 27404 0
vsize: 109780
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 27787 0 0 0 33919 83 0 0 25 0 1 0 545286571 114126848 26569 4294967295 134512640 134672761 3221224544 3221223728 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27863 26569 603 41 0 27822 0
vsize: 111452
[startup+350.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 28216 0 0 0 34918 84 0 0 25 0 1 0 545286571 115970048 26998 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28313 26998 603 41 0 28272 0
vsize: 113252
[startup+360.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 28634 0 0 0 35917 85 0 0 25 0 1 0 545286571 117678080 27416 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28730 27416 603 41 0 28689 0
vsize: 114920
[startup+370.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 28923 0 0 0 36916 87 0 0 25 0 1 0 545286571 118870016 27705 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29021 27705 603 41 0 28980 0
vsize: 116084
[startup+380.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 29128 0 0 0 37916 87 0 0 25 0 1 0 545286571 119660544 27910 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29214 27910 603 41 0 29173 0
vsize: 116856
[startup+390.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29808
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 29333 0 0 0 38915 88 0 0 25 0 1 0 545286571 120496128 28115 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29418 28115 603 41 0 29377 0
vsize: 117672
[startup+400.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 29676 0 0 0 39915 89 0 0 25 0 1 0 545286571 121970688 28458 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29778 28458 603 41 0 29737 0
vsize: 119112
[startup+410.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 29959 0 0 0 40914 90 0 0 25 0 1 0 545286571 123035648 28741 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30038 28741 603 41 0 29997 0
vsize: 120152
[startup+420.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 30245 0 0 0 41912 92 0 0 25 0 1 0 545286571 124215296 29027 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30326 29027 603 41 0 30285 0
vsize: 121304
[startup+430.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 30490 0 0 0 42912 92 0 0 25 0 1 0 545286571 125276160 29272 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30585 29272 603 41 0 30544 0
vsize: 122340
[startup+440.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 30755 0 0 0 43912 93 0 0 25 0 1 0 545286571 126361600 29537 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30850 29537 603 41 0 30809 0
vsize: 123400
[startup+450.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 31030 0 0 0 44911 94 0 0 25 0 1 0 545286571 127442944 29812 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31114 29812 603 41 0 31073 0
vsize: 124456
[startup+460.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 31318 0 0 0 45910 94 0 0 25 0 1 0 545286571 128634880 30100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31405 30100 603 41 0 31364 0
vsize: 125620
[startup+470.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 31610 0 0 0 46910 95 0 0 25 0 1 0 545286571 129863680 30392 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31705 30392 603 41 0 31664 0
vsize: 126820
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 31899 0 0 0 47909 96 0 0 25 0 1 0 545286571 131043328 30681 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31993 30681 603 41 0 31952 0
vsize: 127972
[startup+490.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 32087 0 0 0 48908 97 0 0 25 0 1 0 545286571 131702784 30869 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32154 30869 603 41 0 32113 0
vsize: 128616
[startup+500.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 32380 0 0 0 49907 98 0 0 25 0 1 0 545286571 132882432 31162 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32442 31162 603 41 0 32401 0
vsize: 129768
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 32660 0 0 0 50906 99 0 0 25 0 1 0 545286571 134066176 31442 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32731 31442 603 41 0 32690 0
vsize: 130924
[startup+520.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 32911 0 0 0 51906 100 0 0 25 0 1 0 545286571 135114752 31693 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32987 31693 603 41 0 32946 0
vsize: 131948
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 33181 0 0 0 52905 101 0 0 25 0 1 0 545286571 136163328 31963 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33243 31963 603 41 0 33202 0
vsize: 132972
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 33455 0 0 0 53905 102 0 0 25 0 1 0 545286571 137216000 32237 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33500 32237 603 41 0 33459 0
vsize: 134000
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 33749 0 0 0 54904 103 0 0 25 0 1 0 545286571 138436608 32531 4294967295 134512640 134672761 3221224544 3221223496 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33798 32531 603 41 0 33757 0
vsize: 135192
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 34041 0 0 0 55903 103 0 0 25 0 1 0 545286571 139661312 32823 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34097 32823 603 41 0 34056 0
vsize: 136388
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 34322 0 0 0 56902 105 0 0 25 0 1 0 545286571 140832768 33104 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34383 33104 603 41 0 34342 0
vsize: 137532
[startup+580.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 34552 0 0 0 57901 105 0 0 25 0 1 0 545286571 141811712 33334 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34622 33334 603 41 0 34581 0
vsize: 138488
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 34844 0 0 0 58901 106 0 0 25 0 1 0 545286571 142995456 33626 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34911 33626 603 41 0 34870 0
vsize: 139644
[startup+600.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 35115 0 0 0 59899 108 0 0 25 0 1 0 545286571 144179200 33897 4294967295 134512640 134672761 3221224544 3221223728 134615660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35200 33898 603 41 0 35159 0
vsize: 140800
[startup+610.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 35325 0 0 0 60899 109 0 0 25 0 1 0 545286571 144973824 34107 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35394 34107 603 41 0 35353 0
vsize: 141576
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 35537 0 0 0 61898 109 0 0 25 0 1 0 545286571 145891328 34319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35618 34319 603 41 0 35577 0
vsize: 142472
[startup+630.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 35661 0 0 0 62898 110 0 0 25 0 1 0 545286571 146477056 34443 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35761 34443 603 41 0 35720 0
vsize: 143044
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 36072 0 0 0 63897 111 0 0 25 0 1 0 545286571 148062208 34854 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36148 34854 603 41 0 36107 0
vsize: 144592
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 36672 0 0 0 64896 113 0 0 25 0 1 0 545286571 150560768 35454 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36758 35454 603 41 0 36717 0
vsize: 147032
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 36901 0 0 0 65895 114 0 0 25 0 1 0 545286571 151478272 35683 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36982 35683 603 41 0 36941 0
vsize: 147928
[startup+670.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 37152 0 0 0 66894 114 0 0 25 0 1 0 545286571 152526848 35934 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37238 35934 603 41 0 37197 0
vsize: 148952
[startup+680.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 37446 0 0 0 67894 115 0 0 25 0 1 0 545286571 153710592 36228 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37527 36228 603 41 0 37486 0
vsize: 150108
[startup+690.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29810
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 37745 0 0 0 68893 116 0 0 25 0 1 0 545286571 154890240 36527 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37815 36527 603 41 0 37774 0
vsize: 151260
[startup+700.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 38070 0 0 0 69892 117 0 0 25 0 1 0 545286571 156205056 36852 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38136 36852 603 41 0 38095 0
vsize: 152544
[startup+710.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 38338 0 0 0 70891 118 0 0 25 0 1 0 545286571 157265920 37120 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38395 37120 603 41 0 38354 0
vsize: 153580
[startup+720.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 38537 0 0 0 71891 118 0 0 25 0 1 0 545286571 158101504 37319 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38599 37319 603 41 0 38558 0
vsize: 154396
[startup+730.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 38722 0 0 0 72891 119 0 0 25 0 1 0 545286571 158887936 37504 4294967295 134512640 134672761 3221224544 3221223584 134614225 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38791 37504 603 41 0 38750 0
vsize: 155164
[startup+740.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 38937 0 0 0 73890 120 0 0 25 0 1 0 545286571 159817728 37719 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39018 37719 603 41 0 38977 0
vsize: 156072
[startup+750.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39536 0 0 0 74888 122 0 0 25 0 1 0 545286571 162201600 38286 4294967295 134512640 134672761 3221224544 3221223600 134644240 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39600 38286 603 41 0 39559 0
vsize: 158400
[startup+760.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 75888 122 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+770.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 76889 122 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+780.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 77889 122 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+790.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 78889 122 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+800.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 79889 122 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+810.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 80889 122 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+820.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 81890 122 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+830.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 82890 123 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+840.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39654 0 0 0 83890 123 0 0 25 0 1 0 545286571 161677312 38153 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38153 603 41 0 39431 0
vsize: 157888
[startup+850.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39657 0 0 0 84890 123 0 0 25 0 1 0 545286571 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+860.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39657 0 0 0 85890 123 0 0 25 0 1 0 545286571 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+870.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39657 0 0 0 86890 123 0 0 25 0 1 0 545286571 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134616017 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+880.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39657 0 0 0 87890 123 0 0 25 0 1 0 545286571 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+890.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39657 0 0 0 88891 123 0 0 25 0 1 0 545286571 161677312 38156 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38156 603 41 0 39431 0
vsize: 157888
[startup+900.038 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39658 0 0 0 89891 123 0 0 25 0 1 0 545286571 161677312 38157 4294967295 134512640 134672761 3221224544 3221223584 134612811 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+910.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39658 0 0 0 90891 123 0 0 25 0 1 0 545286571 161677312 38157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+920.039 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39658 0 0 0 91891 123 0 0 25 0 1 0 545286571 161677312 38157 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+930.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39658 0 0 0 92891 123 0 0 25 0 1 0 545286571 161677312 38157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+940.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39658 0 0 0 93892 123 0 0 25 0 1 0 545286571 161677312 38157 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38157 603 41 0 39431 0
vsize: 157888
[startup+950.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39660 0 0 0 94892 123 0 0 25 0 1 0 545286571 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+960.041 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39660 0 0 0 95892 123 0 0 25 0 1 0 545286571 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+970.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39660 0 0 0 96892 123 0 0 25 0 1 0 545286571 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+980.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39660 0 0 0 97892 123 0 0 25 0 1 0 545286571 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+990.042 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29812
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39660 0 0 0 98892 123 0 0 25 0 1 0 545286571 161677312 38159 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38159 603 41 0 39431 0
vsize: 157888
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39665 0 0 0 99893 123 0 0 25 0 1 0 545286571 161677312 38164 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38164 603 41 0 39431 0
vsize: 157888
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39666 0 0 0 100893 123 0 0 25 0 1 0 545286571 161677312 38165 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38165 603 41 0 39431 0
vsize: 157888
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39667 0 0 0 101893 123 0 0 25 0 1 0 545286571 161677312 38166 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38166 603 41 0 39431 0
vsize: 157888
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39667 0 0 0 102892 123 0 0 25 0 1 0 545286571 161677312 38166 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38166 603 41 0 39431 0
vsize: 157888
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39670 0 0 0 103893 123 0 0 25 0 1 0 545286571 161677312 38169 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38169 603 41 0 39431 0
vsize: 157888
[startup+1050.04 s]
Raw data (loadavg): 1.15 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39670 0 0 0 104893 123 0 0 25 0 1 0 545286571 161677312 38169 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38169 603 41 0 39431 0
vsize: 157888
[startup+1060.05 s]
Raw data (loadavg): 1.12 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39671 0 0 0 105893 123 0 0 25 0 1 0 545286571 161677312 38170 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38170 603 41 0 39431 0
vsize: 157888
[startup+1070.04 s]
Raw data (loadavg): 1.10 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39671 0 0 0 106893 123 0 0 25 0 1 0 545286571 161677312 38170 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38170 603 41 0 39431 0
vsize: 157888
[startup+1080.04 s]
Raw data (loadavg): 1.09 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39671 0 0 0 107893 123 0 0 25 0 1 0 545286571 161677312 38170 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38170 603 41 0 39431 0
vsize: 157888
[startup+1090.05 s]
Raw data (loadavg): 1.07 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39672 0 0 0 108894 123 0 0 25 0 1 0 545286571 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1100.05 s]
Raw data (loadavg): 1.06 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39672 0 0 0 109894 123 0 0 25 0 1 0 545286571 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1110.05 s]
Raw data (loadavg): 1.05 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39672 0 0 0 110894 123 0 0 25 0 1 0 545286571 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1120.05 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39672 0 0 0 111894 123 0 0 25 0 1 0 545286571 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1130.05 s]
Raw data (loadavg): 1.04 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39672 0 0 0 112894 123 0 0 25 0 1 0 545286571 161677312 38171 4294967295 134512640 134672761 3221224544 3221223728 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38171 603 41 0 39431 0
vsize: 157888
[startup+1140.05 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39673 0 0 0 113895 123 0 0 25 0 1 0 545286571 161677312 38172 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38172 603 41 0 39431 0
vsize: 157888
[startup+1150.05 s]
Raw data (loadavg): 1.03 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39673 0 0 0 114895 123 0 0 25 0 1 0 545286571 161677312 38172 4294967295 134512640 134672761 3221224544 3221223688 134616275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38172 603 41 0 39431 0
vsize: 157888
[startup+1160.05 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39675 0 0 0 115895 123 0 0 25 0 1 0 545286571 161677312 38174 4294967295 134512640 134672761 3221224544 3221223480 1075350155 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38174 603 41 0 39431 0
vsize: 157888
[startup+1170.05 s]
Raw data (loadavg): 1.02 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39676 0 0 0 116895 123 0 0 25 0 1 0 545286571 161677312 38175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38175 603 41 0 39431 0
vsize: 157888
[startup+1180.05 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39676 0 0 0 117895 123 0 0 25 0 1 0 545286571 161677312 38175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38175 603 41 0 39431 0
vsize: 157888
[startup+1190.05 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39676 0 0 0 118896 123 0 0 25 0 1 0 545286571 161677312 38175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38175 603 41 0 39431 0
vsize: 157888
[startup+1200.05 s]
Raw data (loadavg): 1.01 1.00 0.92 2/55 29814
Raw data (stat): 29804 (minisat+) R 29803 20024 20023 0 -1 0 39676 0 0 0 119895 124 0 0 25 0 1 0 545286571 161677312 38175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39472 38175 603 41 0 39431 0
vsize: 157888
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.13 s]
Raw data (loadavg): 1.01 1.00 0.92 1/55 29814
Raw data (stat): 29804 (minisat+) Z 29803 20024 20023 0 -1 12 39676 0 0 0 119895 131 0 0 25 0 1 0 545286571 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.13
CPU time (s): 1200.28
CPU user time (s): 1198.96
CPU system time (s): 1.3188
CPU usage (%): 100.012
Max. virtual memory (Kb): 158400
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####