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/miplib2003/normalized-mps-v2-13-7-pp08aCUTS.opb
MD5SUM	d1b87efc35bcd73acfc5183bbe3df4f0
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	2304
Biggest coefficient in the objective function	1048576
Number of bits for the biggest coefficient in the objective function	21
Sum of the numbers in the objective function	178464600
Number of bits of the sum of numbers in the objective function	28
Biggest number in a constraint	1048576
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	178464600
Number of bits of the biggest sum of numbers	28
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	3288
Total number of constraints	374
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	64
Number of constraints which are nor clauses,nor cardinality constraints	310
Minimum length of a constraint	1
Maximum length of a constraint	123
Trace number 18483

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc20 THE 2005-04-21 15:14:47 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17912 boxname=wulflinc20 idbench=1378 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  d1b87efc35bcd73acfc5183bbe3df4f0  /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-pp08aCUTS.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-pp08aCUTS.opb /oldhome/oroussel/tmp/wulflinc20/normalized-mps-v2-13-7-pp08aCUTS.opb
IDLAUNCH: 17912
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.215
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.215
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        229388 kB
Buffers:         30032 kB
Cached:         750432 kB
SwapCached:        516 kB
Active:          61240 kB
Inactive:       721208 kB
HighTotal:      131008 kB
HighFree:         5768 kB
LowTotal:       903652 kB
LowFree:        223620 kB
SwapTotal:     2097892 kB
SwapFree:      2096480 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5116 kB
Slab:            17084 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:34:50 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 17912 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 374 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[ 501]---> BDD-cost:   15
c ---[ 500]---> BDD-cost:   15
c ---[ 499]---> BDD-cost:   15
c ---[ 498]---> BDD-cost:   15
c ---[ 497]---> BDD-cost:   15
c ---[ 496]---> BDD-cost:   15
c ---[ 495]---> BDD-cost:   15
c ---[ 494]---> BDD-cost:   15
c ---[ 485]---> BDD-cost:   15
c ---[ 484]---> BDD-cost:   15
c ---[ 483]---> BDD-cost:   15
c ---[ 482]---> BDD-cost:   15
c ---[ 481]---> BDD-cost:   15
c ---[ 480]---> BDD-cost:   15
c ---[ 479]---> BDD-cost:   15
c ---[ 477]---> BDD-cost:   15
c ---[ 476]---> BDD-cost:   15
c ---[ 475]---> BDD-cost:   15
c ---[ 474]---> BDD-cost:   15
c ---[ 473]---> BDD-cost:   15
c ---[ 472]---> BDD-cost:   15
c ---[ 471]---> BDD-cost:   15
c ---[ 469]---> BDD-cost:   14
c ---[ 468]---> BDD-cost:   14
c ---[ 467]---> BDD-cost:   14
c ---[ 466]---> BDD-cost:   14
c ---[ 465]---> BDD-cost:   14
c ---[ 464]---> BDD-cost:   14
c ---[ 463]---> BDD-cost:   14
c ---[ 462]---> BDD-cost:   14
c ---[ 461]---> BDD-cost:   15
c ---[ 460]---> BDD-cost:   15
c ---[ 459]---> BDD-cost:   15
c ---[ 458]---> BDD-cost:   15
c ---[ 457]---> BDD-cost:   15
c ---[ 456]---> BDD-cost:   15
c ---[ 455]---> BDD-cost:   15
c ---[ 454]---> BDD-cost:   15
c ---[ 445]---> BDD-cost:   13
c ---[ 444]---> BDD-cost:   13
c ---[ 443]---> BDD-cost:   13
c ---[ 442]---> BDD-cost:   13
c ---[ 441]---> BDD-cost:   13
c ---[ 440]---> BDD-cost:   13
c ---[ 439]---> BDD-cost:   13
c ---[ 438]---> BDD-cost:   13
c ---[ 436]---> BDD-cost:  158
c ---[ 434]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> BDD-cost:    6
c ---[ 432]---> BDD-cost:    6
c ---[ 431]---> BDD-cost:    6
c ---[ 430]---> BDD-cost:    6
c ---[ 429]---> BDD-cost:   23
c ---[ 428]---> BDD-cost:    4
c ---[ 427]---> BDD-cost:    4
c ---[ 426]---> BDD-cost:    4
c ---[ 425]---> BDD-cost:    4
c ---[ 424]---> BDD-cost:    4
c ---[ 422]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 421]---> BDD-cost:    4
c ---[ 420]---> BDD-cost:    4
c ---[ 419]---> BDD-cost:    4
c ---[ 418]---> BDD-cost:    9
c ---[ 417]---> BDD-cost:    9
c ---[ 416]---> BDD-cost:    9
c ---[ 415]---> BDD-cost:    6
c ---[ 414]---> BDD-cost:    6
c ---[ 413]---> BDD-cost:    6
c ---[ 412]---> BDD-cost:    6
c ---[ 410]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 409]---> BDD-cost:    6
c ---[ 408]---> BDD-cost:   19
c ---[ 407]---> BDD-cost:   19
c ---[ 406]---> BDD-cost:   19
c ---[ 405]---> BDD-cost:   19
c ---[ 404]---> BDD-cost:   19
c ---[ 403]---> BDD-cost:   19
c ---[ 402]---> BDD-cost:   19
c ---[ 401]---> BDD-cost:   19
c ---[ 400]---> BDD-cost:    6
c ---[ 398]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 397]---> BDD-cost:    6
c ---[ 396]---> BDD-cost:    6
c ---[ 395]---> BDD-cost:    6
c ---[ 394]---> BDD-cost:    6
c ---[ 393]---> BDD-cost:    6
c ---[ 392]---> BDD-cost:    6
c ---[ 391]---> BDD-cost:    6
c ---[ 386]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 338]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 300]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 276]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 264]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 255]---> BDD-cost:  158
c ---[ 253]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 251]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 249]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 247]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 245]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 243]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 241]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 239]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 235]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 233]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 231]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 227]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 225]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 221]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 219]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 217]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 213]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 211]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 209]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 205]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 203]---> BDD-cost:  154
c ---[ 201]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 197]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 195]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 191]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 189]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 187]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 183]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 181]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 179]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 177]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 175]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 173]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 171]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 169]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 168]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 167]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 166]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 165]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 164]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 162]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 161]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 160]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 159]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    6
c ---[ 154]---> BDD-cost:    6
c ---[ 153]---> BDD-cost:    6
c ---[ 152]---> BDD-cost:    6
c ---[ 150]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 149]---> BDD-cost:    8
c ---[ 148]---> BDD-cost:   19
c ---[ 147]---> BDD-cost:   19
c ---[ 146]---> BDD-cost:   19
c ---[ 145]---> BDD-cost:   19
c ---[ 144]---> BDD-cost:   19
c ---[ 143]---> BDD-cost:   19
c ---[ 142]---> BDD-cost:   19
c ---[ 141]---> BDD-cost:   19
c ---[ 140]---> BDD-cost:    9
c ---[ 138]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    6
c ---[ 134]---> BDD-cost:    6
c ---[ 133]---> BDD-cost:    6
c ---[ 132]---> BDD-cost:    6
c ---[ 131]---> BDD-cost:   23
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    1
c ---[ 126]---> BDD-cost:    1
c ---[ 125]---> BDD-cost:    1
c ---[ 124]---> BDD-cost:    1
c ---[ 123]---> BDD-cost:    1
c ---[ 122]---> BDD-cost:    1
c ---[ 121]---> BDD-cost:    1
c ---[ 120]---> BDD-cost:    1
c ---[ 119]---> BDD-cost:    1
c ---[ 118]---> BDD-cost:    1
c ---[ 117]---> BDD-cost:    1
c ---[ 116]---> BDD-cost:    1
c ---[ 115]---> BDD-cost:    1
c ---[ 114]---> BDD-cost:    1
c ---[ 113]---> BDD-cost:    1
c ---[ 112]---> BDD-cost:    1
c ---[ 111]---> BDD-cost:    1
c ---[ 110]---> BDD-cost:    1
c ---[ 109]---> BDD-cost:   50
c ---[ 108]---> BDD-cost:  203
c ---[ 107]---> BDD-cost:   45
c ---[ 106]---> BDD-cost:  194
c ---[ 105]---> BDD-cost:   48
c ---[ 104]---> BDD-cost:  191
c ---[ 103]---> BDD-cost:   38
c ---[ 102]---> BDD-cost:  173
c ---[ 101]---> BDD-cost:   44
c ---[ 100]---> BDD-cost:  167
c ---[  99]---> BDD-cost:    5
c ---[  98]---> BDD-cost:   73
c ---[  97]---> BDD-cost:    3
c ---[  96]---> BDD-cost:   62
c ---[  95]---> BDD-cost:   41
c ---[  94]---> BDD-cost:  158
c ---[  93]---> BDD-cost:   45
c ---[  92]---> BDD-cost:  182
c ---[  91]---> BDD-cost:   40
c ---[  90]---> BDD-cost:  173
c ---[  89]---> BDD-cost:   35
c ---[  88]---> BDD-cost:  164
c ---[  87]---> BDD-cost:   41
c ---[  86]---> BDD-cost:  158
c ---[  85]---> BDD-cost:    5
c ---[  84]---> BDD-cost:   70
c ---[  83]---> BDD-cost:    3
c ---[  82]---> BDD-cost:   65
c ---[  81]---> BDD-cost:   45
c ---[  80]---> BDD-cost:  194
c ---[  79]---> BDD-cost:   48
c ---[  78]---> BDD-cost:  191
c ---[  77]---> BDD-cost:   41
c ---[  76]---> BDD-cost:  170
c ---[  75]---> BDD-cost:   44
c ---[  74]---> BDD-cost:  167
c ---[  73]---> BDD-cost:   50
c ---[  72]---> BDD-cost:  203
c ---[  71]---> BDD-cost:    3
c ---[  70]---> BDD-cost:   61
c ---[  69]---> BDD-cost:   48
c ---[  68]---> BDD-cost:  191
c ---[  67]---> BDD-cost:   48
c ---[  66]---> BDD-cost:  191
c ---[  65]---> BDD-cost:   55
c ---[  64]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  63]---> BDD-cost:   47
c ---[  62]---> BDD-cost:  161
c ---[  61]---> BDD-cost:   50
c ---[  60]---> BDD-cost:  203
c ---[  59]---> BDD-cost:   48
c ---[  58]---> BDD-cost:  191
c ---[  57]---> BDD-cost:    5
c ---[  56]---> BDD-cost:   73
c ---[  55]---> BDD-cost:    5
c ---[  54]---> BDD-cost:   70
c ---[  53]---> BDD-cost:   38
c ---[  52]---> BDD-cost:  161
c ---[  51]---> BDD-cost:   41
c ---[  50]---> BDD-cost:  158
c ---[  49]---> BDD-cost:   35
c ---[  48]---> BDD-cost:  164
c ---[  47]---> BDD-cost:   35
c ---[  46]---> BDD-cost:  164
c ---[  45]---> BDD-cost:   38
c ---[  44]---> BDD-cost:  161
c ---[  43]---> BDD-cost:    3
c ---[  42]---> BDD-cost:   64
c ---[  41]---> BDD-cost:    6
c ---[  40]---> BDD-cost:   78
c ---[  39]---> BDD-cost:   41
c ---[  38]---> BDD-cost:  170
c ---[  37]---> BDD-cost:   41
c ---[  36]---> BDD-cost:  170
c ---[  35]---> BDD-cost:   41
c ---[  34]---> BDD-cost:  170
c ---[  33]---> BDD-cost:   48
c ---[  32]---> BDD-cost:  191
c ---[  31]---> BDD-cost:   38
c ---[  30]---> BDD-cost:  173
c ---[  29]---> BDD-cost:   41
c ---[  28]---> BDD-cost:  170
c ---[  27]---> BDD-cost:    5
c ---[  26]---> BDD-cost:   75
c ---[  25]---> BDD-cost:   38
c ---[  24]---> BDD-cost:  161
c ---[  23]---> BDD-cost:   45
c ---[  22]---> BDD-cost:  182
c ---[  21]---> BDD-cost:   35
c ---[  20]---> BDD-cost:  164
c ---[  19]---> BDD-cost:   38
c ---[  18]---> BDD-cost:  161
c ---[  17]---> BDD-cost:   43
c ---[  16]---> BDD-cost:  170
c ---[  15]---> BDD-cost:   41
c ---[  14]---> BDD-cost:  158
c ---[  13]---> BDD-cost:    3
c ---[  12]---> BDD-cost:   60
c ---[  11]---> BDD-cost:    3
c ---[  10]---> BDD-cost:   59
c ---[   9]---> BDD-cost:   38
c ---[   8]---> BDD-cost:  149
c ---[   7]---> BDD-cost:   35
c ---[   6]---> BDD-cost:  152
c ---[   5]---> BDD-cost:   35
c ---[   4]---> BDD-cost:  152
c ---[   3]---> BDD-cost:   38
c ---[   2]---> BDD-cost:  149
c ---[   1]---> BDD-cost:    4
c ---[   0]---> BDD-cost:   62
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  226352   543670 |   67905       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/76417          
c   -- var.elim.:  2000/76417          
c   -- var.elim.:  3000/76417          
c   -- var.elim.:  4000/76417          
c   -- var.elim.:  5000/76417          
c   -- var.elim.:  6000/76417          
c   -- var.elim.:  7000/76417          
c   -- var.elim.:  8000/76417          
c   -- var.elim.:  9000/76417          
c   -- var.elim.:  10000/76417          
c   -- var.elim.:  11000/76417          
c   -- var.elim.:  12000/76417          
c   -- var.elim.:  13000/76417          
c   -- var.elim.:  14000/76417          
c   -- var.elim.:  15000/76417          
c   -- var.elim.:  16000/76417          
c   -- var.elim.:  17000/76417          
c   -- var.elim.:  18000/76417          
c   -- var.elim.:  19000/76417          
c   -- var.elim.:  20000/76417          
c   -- var.elim.:  21000/76417          
c   -- var.elim.:  22000/76417          
c   -- var.elim.:  23000/76417          
c   -- var.elim.:  24000/76417          
c   -- var.elim.:  25000/76417          
c   -- var.elim.:  26000/76417          
c   -- var.elim.:  27000/76417          
c   -- var.elim.:  28000/76417          
c   -- var.elim.:  29000/76417          
c   -- var.elim.:  30000/76417          
c   -- var.elim.:  31000/76417          
c   -- var.elim.:  32000/76417          
c   -- var.elim.:  33000/76417          
c   -- var.elim.:  34000/76417          
c   -- var.elim.:  35000/76417          
c   -- var.elim.:  36000/76417          
c   -- var.elim.:  37000/76417          
c   -- var.elim.:  38000/76417          
c   -- var.elim.:  39000/76417          
c   -- var.elim.:  40000/76417          
c   -- var.elim.:  41000/76417          
c   -- var.elim.:  42000/76417          
c   -- var.elim.:  43000/76417          
c   -- var.elim.:  44000/76417          
c   -- var.elim.:  45000/76417          
c   -- var.elim.:  46000/76417          
c   -- var.elim.:  47000/76417          
c   -- var.elim.:  48000/76417          
c   -- var.elim.:  49000/76417          
c   -- var.elim.:  50000/76417          
c   -- var.elim.:  51000/76417          
c   -- var.elim.:  52000/76417          
c   -- var.elim.:  53000/76417          
c   -- var.elim.:  54000/76417          
c   -- var.elim.:  55000/76417          
c   -- var.elim.:  56000/76417          
c   -- var.elim.:  57000/76417          
c   -- var.elim.:  58000/76417          
c   -- var.elim.:  59000/76417          
c   -- var.elim.:  60000/76417          
c   -- var.elim.:  61000/76417          
c   -- var.elim.:  62000/76417          
c   -- var.elim.:  63000/76417          
c   -- var.elim.:  64000/76417          
c   -- var.elim.:  65000/76417          
c   -- var.elim.:  66000/76417          
c   -- var.elim.:  67000/76417          
c   -- var.elim.:  68000/76417          
c   -- var.elim.:  69000/76417          
c   -- var.elim.:  70000/76417          
c   -- var.elim.:  71000/76417          
c   -- var.elim.:  72000/76417          
c   -- var.elim.:  73000/76417          
c   -- var.elim.:  74000/76417          
c   -- var.elim.:  75000/76417          
c   -- var.elim.:  76000/76417          
c   -- var.elim.:  76417/76417          
c   -- var.elim.:  1000/41915          
c   -- var.elim.:  2000/41915          
c   -- var.elim.:  3000/41915          
c   -- var.elim.:  4000/41915          
c   -- var.elim.:  5000/41915          
c   -- var.elim.:  6000/41915          
c   -- var.elim.:  7000/41915          
c   -- var.elim.:  8000/41915          
c   -- var.elim.:  9000/41915          
c   -- var.elim.:  10000/41915          
c   -- var.elim.:  11000/41915          
c   -- var.elim.:  12000/41915          
c   -- var.elim.:  13000/41915          
c   -- var.elim.:  14000/41915          
c   -- var.elim.:  15000/41915          
c   -- var.elim.:  16000/41915          
c   -- var.elim.:  17000/41915          
c   -- var.elim.:  18000/41915          
c   -- var.elim.:  19000/41915          
c   -- var.elim.:  20000/41915          
c   -- var.elim.:  21000/41915          
c   -- var.elim.:  22000/41915          
c   -- var.elim.:  23000/41915          
c   -- var.elim.:  24000/41915          
c   -- var.elim.:  25000/41915          
c   -- var.elim.:  26000/41915          
c   -- var.elim.:  27000/41915          
c   -- var.elim.:  28000/41915          
c   -- var.elim.:  29000/41915          
c   -- var.elim.:  30000/41915          
c   -- var.elim.:  31000/41915          
c   -- var.elim.:  32000/41915          
c   -- var.elim.:  33000/41915          
c   -- var.elim.:  34000/41915          
c   -- var.elim.:  35000/41915          
c   -- var.elim.:  36000/41915          
c   -- var.elim.:  37000/41915          
c   -- var.elim.:  38000/41915          
c   -- var.elim.:  39000/41915          
c   -- var.elim.:  40000/41915          
c   -- var.elim.:  41000/41915          
c   -- var.elim.:  41915/41915          
c   -- var.elim.:  439/439          
c   -- var.elim.:  221/221          
c   -- var.elim.:  286/286          
c   -- var.elim.:  338/338          
c   -- var.elim.:  299/299          
c   -- var.elim.:  351/351          
c   -- var.elim.:  302/302          
c   -- var.elim.:  176/176          
c   -- var.elim.:  82/82          
c   -- var.elim.:  37/37          
c   -- var.elim.:  20/20          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  1000/7120          
c   -- var.elim.:  2000/7120          
c   -- var.elim.:  3000/7120          
c   -- var.elim.:  4000/7120          
c   -- var.elim.:  5000/7120          
c   -- var.elim.:  6000/7120          
c   -- var.elim.:  7000/7120          
c   -- var.elim.:  7120/7120          
c   -- var.elim.:  1000/2885          
c   -- var.elim.:  2000/2885          
c   -- var.elim.:  2885/2885          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/1180          
c   -- var.elim.:  1180/1180          
c   -- var.elim.:  87/87          
c |         0 |  181869   552702 |      --       0       --      -- |     --   | -33569/35725
c |         0 |  181869   552702 |   72747       0        0     nan |  0.000 % |
c |       100 |  181836   552583 |   80007      92      424     4.6 |  8.815 % |
c |       250 |  181774   552363 |   87978     236      980     4.2 |  8.837 % |
c |       475 |  181441   551174 |   96599     422     1648     3.9 |  8.968 % |
c |       812 |  181082   549896 |  106048     719     2899     4.0 |  9.104 % |
c |      1318 |  180983   549539 |  116589    1218     4972     4.1 |  9.143 % |
c |      2077 |  180594   548199 |  127973    1940     8279     4.3 |  9.294 % |
c |      3216 |  180190   546800 |  140455    3037    14076     4.6 |  9.452 % #### 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.92 0.97 0.93 2/54 8825
Raw data (stat): 8825 (runsolver) R 8824 27565 27564 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546078632 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0012 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 12558 0 0 0 960 38 0 0 25 0 1 0 546078632 56463360 11843 4294967295 134512640 134672761 3221224544 3221223008 134644235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13785 11843 603 41 0 13744 0
vsize: 55140
[startup+20.0014 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13292 0 0 0 1958 40 0 0 25 0 1 0 546078632 56659968 11871 4294967295 134512640 134672761 3221224544 3221223708 134614558 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13833 11871 603 41 0 13792 0
vsize: 55332
[startup+30.0025 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13296 0 0 0 2958 40 0 0 25 0 1 0 546078632 56659968 11875 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13833 11875 603 41 0 13792 0
vsize: 55332
[startup+40.0034 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13317 0 0 0 3958 40 0 0 25 0 1 0 546078632 56659968 11896 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13833 11896 603 41 0 13792 0
vsize: 55332
[startup+50.0036 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13323 0 0 0 4958 40 0 0 25 0 1 0 546078632 56659968 11902 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13833 11902 603 41 0 13792 0
vsize: 55332
[startup+60.0036 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13361 0 0 0 5958 40 0 0 25 0 1 0 546078632 56922112 11940 4294967295 134512640 134672761 3221224544 3221223680 134614727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13897 11940 603 41 0 13856 0
vsize: 55588
[startup+70.0043 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13401 0 0 0 6958 41 0 0 25 0 1 0 546078632 57053184 11948 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13929 11948 603 41 0 13888 0
vsize: 55716
[startup+80.0048 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13405 0 0 0 7958 41 0 0 25 0 1 0 546078632 57053184 11952 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13929 11952 603 41 0 13888 0
vsize: 55716
[startup+90.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13410 0 0 0 8959 41 0 0 25 0 1 0 546078632 57053184 11957 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13929 11957 603 41 0 13888 0
vsize: 55716
[startup+100.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13414 0 0 0 9959 41 0 0 25 0 1 0 546078632 57053184 11961 4294967295 134512640 134672761 3221224544 3221223680 134614736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13929 11961 603 41 0 13888 0
vsize: 55716
[startup+110.005 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13417 0 0 0 10959 41 0 0 25 0 1 0 546078632 57053184 11964 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13929 11964 603 41 0 13888 0
vsize: 55716
[startup+120.005 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13422 0 0 0 11959 41 0 0 25 0 1 0 546078632 57053184 11969 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13929 11969 603 41 0 13888 0
vsize: 55716
[startup+130.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13450 0 0 0 12959 41 0 0 25 0 1 0 546078632 57188352 11997 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13962 11997 603 41 0 13921 0
vsize: 55848
[startup+140.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13487 0 0 0 13959 41 0 0 25 0 1 0 546078632 57323520 12034 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13995 12034 603 41 0 13954 0
vsize: 55980
[startup+150.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13527 0 0 0 14959 41 0 0 25 0 1 0 546078632 57454592 12074 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14027 12074 603 41 0 13986 0
vsize: 56108
[startup+160.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13562 0 0 0 15960 41 0 0 25 0 1 0 546078632 57851904 12109 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14124 12109 603 41 0 14083 0
vsize: 56496
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13607 0 0 0 16960 41 0 0 25 0 1 0 546078632 58118144 12154 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14189 12154 603 41 0 14148 0
vsize: 56756
[startup+180.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13669 0 0 0 17959 42 0 0 25 0 1 0 546078632 58253312 12216 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14222 12216 603 41 0 14181 0
vsize: 56888
[startup+190.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13762 0 0 0 18959 42 0 0 25 0 1 0 546078632 58654720 12309 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14320 12309 603 41 0 14279 0
vsize: 57280
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13867 0 0 0 19959 42 0 0 25 0 1 0 546078632 59052032 12414 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14417 12414 603 41 0 14376 0
vsize: 57668
[startup+210.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 13973 0 0 0 20959 42 0 0 25 0 1 0 546078632 59453440 12520 4294967295 134512640 134672761 3221224544 3221223788 134564424 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14515 12520 603 41 0 14474 0
vsize: 58060
[startup+220.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 14224 0 0 0 21958 44 0 0 25 0 1 0 546078632 60514304 12771 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14774 12771 603 41 0 14733 0
vsize: 59096
[startup+230.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 14535 0 0 0 22958 44 0 0 25 0 1 0 546078632 61718528 13082 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15068 13082 603 41 0 15027 0
vsize: 60272
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 14626 0 0 0 23958 45 0 0 25 0 1 0 546078632 62115840 13173 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15165 13173 603 41 0 15124 0
vsize: 60660
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 14720 0 0 0 24957 45 0 0 25 0 1 0 546078632 62517248 13267 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15263 13267 603 41 0 15222 0
vsize: 61052
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 14911 0 0 0 25957 46 0 0 25 0 1 0 546078632 63307776 13458 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15456 13458 603 41 0 15415 0
vsize: 61824
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 15052 0 0 0 26957 46 0 0 25 0 1 0 546078632 63836160 13599 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15585 13599 603 41 0 15544 0
vsize: 62340
[startup+280.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 15144 0 0 0 27957 46 0 0 25 0 1 0 546078632 64106496 13691 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15651 13691 603 41 0 15610 0
vsize: 62604
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 15474 0 0 0 28956 48 0 0 25 0 1 0 546078632 65560576 14021 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16006 14021 603 41 0 15965 0
vsize: 64024
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 15577 0 0 0 29955 48 0 0 25 0 1 0 546078632 65957888 14124 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16103 14124 603 41 0 16062 0
vsize: 64412
[startup+310.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 15685 0 0 0 30955 49 0 0 25 0 1 0 546078632 66879488 14232 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16328 14232 603 41 0 16287 0
vsize: 65312
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 15803 0 0 0 31955 49 0 0 25 0 1 0 546078632 67280896 14350 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16426 14350 603 41 0 16385 0
vsize: 65704
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 15899 0 0 0 32955 49 0 0 25 0 1 0 546078632 67686400 14446 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16525 14446 603 41 0 16484 0
vsize: 66100
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 15988 0 0 0 33955 50 0 0 25 0 1 0 546078632 68091904 14535 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16624 14535 603 41 0 16583 0
vsize: 66496
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 16093 0 0 0 34954 50 0 0 25 0 1 0 546078632 68489216 14640 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16721 14640 603 41 0 16680 0
vsize: 66884
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 16244 0 0 0 35954 51 0 0 25 0 1 0 546078632 69025792 14791 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16852 14791 603 41 0 16811 0
vsize: 67408
[startup+370.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 16348 0 0 0 36954 51 0 0 25 0 1 0 546078632 69427200 14895 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16950 14895 603 41 0 16909 0
vsize: 67800
[startup+380.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 16452 0 0 0 37954 51 0 0 25 0 1 0 546078632 69959680 14999 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17080 14999 603 41 0 17039 0
vsize: 68320
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 16574 0 0 0 38953 52 0 0 25 0 1 0 546078632 70352896 15121 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17176 15121 603 41 0 17135 0
vsize: 68704
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 16654 0 0 0 39953 52 0 0 25 0 1 0 546078632 70754304 15201 4294967295 134512640 134672761 3221224544 3221223680 134614822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17274 15201 603 41 0 17233 0
vsize: 69096
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 16919 0 0 0 40953 52 0 0 25 0 1 0 546078632 71815168 15466 4294967295 134512640 134672761 3221224544 3221223728 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17533 15466 603 41 0 17492 0
vsize: 70132
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17024 0 0 0 41953 53 0 0 25 0 1 0 546078632 72212480 15571 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17630 15571 603 41 0 17589 0
vsize: 70520
[startup+430.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17098 0 0 0 42953 53 0 0 25 0 1 0 546078632 72597504 15645 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17724 15645 603 41 0 17683 0
vsize: 70896
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17181 0 0 0 43953 53 0 0 25 0 1 0 546078632 72867840 15728 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17790 15728 603 41 0 17749 0
vsize: 71160
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17243 0 0 0 44952 54 0 0 25 0 1 0 546078632 73134080 15790 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17855 15790 603 41 0 17814 0
vsize: 71420
[startup+460.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17344 0 0 0 45952 54 0 0 25 0 1 0 546078632 73527296 15891 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17951 15891 603 41 0 17910 0
vsize: 71804
[startup+470.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17504 0 0 0 46952 55 0 0 25 0 1 0 546078632 74190848 16051 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18113 16052 603 41 0 18072 0
vsize: 72452
[startup+480.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17591 0 0 0 47952 55 0 0 25 0 1 0 546078632 74457088 16138 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18178 16138 603 41 0 18137 0
vsize: 72712
[startup+490.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17701 0 0 0 48951 56 0 0 25 0 1 0 546078632 74854400 16248 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18275 16248 603 41 0 18234 0
vsize: 73100
[startup+500.009 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 17835 0 0 0 49951 56 0 0 25 0 1 0 546078632 75390976 16382 4294967295 134512640 134672761 3221224544 3221223584 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18406 16382 603 41 0 18365 0
vsize: 73624
[startup+510.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 18273 0 0 0 50950 57 0 0 25 0 1 0 546078632 77242368 16820 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18858 16820 603 41 0 18817 0
vsize: 75432
[startup+520.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 18403 0 0 0 51950 58 0 0 25 0 1 0 546078632 77778944 16950 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18989 16950 603 41 0 18948 0
vsize: 75956
[startup+530.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 18671 0 0 0 52949 58 0 0 25 0 1 0 546078632 78843904 17218 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19249 17218 603 41 0 19208 0
vsize: 76996
[startup+540.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 18871 0 0 0 53949 59 0 0 25 0 1 0 546078632 79634432 17418 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19442 17418 603 41 0 19401 0
vsize: 77768
[startup+550.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 19042 0 0 0 54948 60 0 0 25 0 1 0 546078632 80297984 17589 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19604 17589 603 41 0 19563 0
vsize: 78416
[startup+560.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 19179 0 0 0 55948 60 0 0 25 0 1 0 546078632 80830464 17726 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19734 17726 603 41 0 19693 0
vsize: 78936
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 19389 0 0 0 56948 60 0 0 25 0 1 0 546078632 81629184 17936 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19929 17936 603 41 0 19888 0
vsize: 79716
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 19505 0 0 0 57948 61 0 0 25 0 1 0 546078632 82161664 18052 4294967295 134512640 134672761 3221224544 3221223584 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20059 18052 603 41 0 20018 0
vsize: 80236
[startup+590.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 19640 0 0 0 58948 61 0 0 25 0 1 0 546078632 82690048 18187 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20188 18187 603 41 0 20147 0
vsize: 80752
[startup+600.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 19822 0 0 0 59947 62 0 0 25 0 1 0 546078632 83476480 18369 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20380 18369 603 41 0 20339 0
vsize: 81520
[startup+610.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 20003 0 0 0 60947 62 0 0 25 0 1 0 546078632 84140032 18550 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20542 18550 603 41 0 20501 0
vsize: 82168
[startup+620.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 20214 0 0 0 61947 63 0 0 25 0 1 0 546078632 84926464 18761 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20734 18761 603 41 0 20693 0
vsize: 82936
[startup+630.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 20396 0 0 0 62946 63 0 0 25 0 1 0 546078632 85725184 18943 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20929 18943 603 41 0 20888 0
vsize: 83716
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 20538 0 0 0 63946 64 0 0 25 0 1 0 546078632 86257664 19085 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21059 19085 603 41 0 21018 0
vsize: 84236
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 20717 0 0 0 64946 64 0 0 25 0 1 0 546078632 87048192 19264 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21252 19264 603 41 0 21211 0
vsize: 85008
[startup+660.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 20853 0 0 0 65945 64 0 0 25 0 1 0 546078632 88625152 19400 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21637 19400 603 41 0 21596 0
vsize: 86548
[startup+670.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 20951 0 0 0 66945 65 0 0 25 0 1 0 546078632 89030656 19498 4294967295 134512640 134672761 3221224544 3221223728 134615617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21736 19498 603 41 0 21695 0
vsize: 86944
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 21122 0 0 0 67944 66 0 0 25 0 1 0 546078632 89694208 19669 4294967295 134512640 134672761 3221224544 3221223680 134614688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21898 19669 603 41 0 21857 0
vsize: 87592
[startup+690.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 21267 0 0 0 68944 66 0 0 25 0 1 0 546078632 90226688 19814 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22028 19814 603 41 0 21987 0
vsize: 88112
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 21359 0 0 0 69944 66 0 0 25 0 1 0 546078632 90628096 19906 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22126 19906 603 41 0 22085 0
vsize: 88504
[startup+710.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 21505 0 0 0 70944 67 0 0 25 0 1 0 546078632 91156480 20052 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22255 20052 603 41 0 22214 0
vsize: 89020
[startup+720.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 21661 0 0 0 71944 67 0 0 25 0 1 0 546078632 91815936 20208 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22416 20208 603 41 0 22375 0
vsize: 89664
[startup+730.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 21842 0 0 0 72943 68 0 0 25 0 1 0 546078632 92487680 20389 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22580 20389 603 41 0 22539 0
vsize: 90320
[startup+740.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 21948 0 0 0 73943 69 0 0 25 0 1 0 546078632 93028352 20495 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22712 20495 603 41 0 22671 0
vsize: 90848
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 22186 0 0 0 74943 69 0 0 25 0 1 0 546078632 93958144 20733 4294967295 134512640 134672761 3221224544 3221223460 1075349617 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22939 20733 603 41 0 22898 0
vsize: 91756
[startup+760.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 22518 0 0 0 75942 70 0 0 25 0 1 0 546078632 95281152 21065 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23262 21065 603 41 0 23221 0
vsize: 93048
[startup+770.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 22698 0 0 0 76941 71 0 0 25 0 1 0 546078632 95948800 21245 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23425 21245 603 41 0 23384 0
vsize: 93700
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 22892 0 0 0 77940 72 0 0 25 0 1 0 546078632 96743424 21439 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23619 21439 603 41 0 23578 0
vsize: 94476
[startup+790.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 23052 0 0 0 78940 73 0 0 25 0 1 0 546078632 97402880 21599 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23780 21599 603 41 0 23739 0
vsize: 95120
[startup+800.013 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 23177 0 0 0 79939 73 0 0 25 0 1 0 546078632 97931264 21724 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23909 21724 603 41 0 23868 0
vsize: 95636
[startup+810.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 23410 0 0 0 80939 74 0 0 25 0 1 0 546078632 98861056 21957 4294967295 134512640 134672761 3221224544 3221223584 134612783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24136 21957 603 41 0 24095 0
vsize: 96544
[startup+820.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 23817 0 0 0 81938 75 0 0 25 0 1 0 546078632 100458496 22364 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24526 22364 603 41 0 24485 0
vsize: 98104
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 23940 0 0 0 82938 76 0 0 25 0 1 0 546078632 100990976 22487 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24656 22487 603 41 0 24615 0
vsize: 98624
[startup+840.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 24160 0 0 0 83937 76 0 0 25 0 1 0 546078632 101908480 22707 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24880 22707 603 41 0 24839 0
vsize: 99520
[startup+850.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 24373 0 0 0 84937 76 0 0 25 0 1 0 546078632 102707200 22920 4294967295 134512640 134672761 3221224544 3221223688 134616189 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25075 22920 603 41 0 25034 0
vsize: 100300
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 24655 0 0 0 85936 77 0 0 25 0 1 0 546078632 103895040 23202 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25365 23202 603 41 0 25324 0
vsize: 101460
[startup+870.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 25233 0 0 0 86936 78 0 0 25 0 1 0 546078632 106135552 23780 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25912 23780 603 41 0 25871 0
vsize: 103648
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 25619 0 0 0 87934 80 0 0 25 0 1 0 546078632 107720704 24166 4294967295 134512640 134672761 3221224544 3221223584 134614205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26299 24166 603 41 0 26258 0
vsize: 105196
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 26750 0 0 0 88931 83 0 0 25 0 1 0 546078632 112345088 25297 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27428 25297 603 41 0 27387 0
vsize: 109712
[startup+900.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 27802 0 0 0 89929 86 0 0 25 0 1 0 546078632 116690944 26349 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28489 26349 603 41 0 28448 0
vsize: 113956
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 28138 0 0 0 90928 87 0 0 25 0 1 0 546078632 118022144 26685 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28814 26685 603 41 0 28773 0
vsize: 115256
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 28295 0 0 0 91928 87 0 0 25 0 1 0 546078632 118689792 26842 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28977 26842 603 41 0 28936 0
vsize: 115908
[startup+930.014 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 28493 0 0 0 92927 88 0 0 25 0 1 0 546078632 119484416 27040 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29171 27040 603 41 0 29130 0
vsize: 116684
[startup+940.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 28963 0 0 0 93926 89 0 0 25 0 1 0 546078632 121339904 27510 4294967295 134512640 134672761 3221224544 3221223584 134612821 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29624 27510 603 41 0 29583 0
vsize: 118496
[startup+950.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 29114 0 0 0 94926 90 0 0 25 0 1 0 546078632 122003456 27661 4294967295 134512640 134672761 3221224544 3221223808 134617892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29786 27661 603 41 0 29745 0
vsize: 119144
[startup+960.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 29316 0 0 0 95925 90 0 0 25 0 1 0 546078632 122798080 27863 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29980 27863 603 41 0 29939 0
vsize: 119920
[startup+970.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 96923 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+980.015 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 97923 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 98923 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 99924 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 100924 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 101924 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 102924 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 103924 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 104924 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 105925 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 106925 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223696 134541816 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 107925 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223680 134614683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 108925 93 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 109924 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 110925 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 111925 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 112925 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 113925 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 114925 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223680 134614505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 115925 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 116926 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 117926 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223536 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 118926 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223696 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 8825
Raw data (stat): 8825 (minisat+) R 8824 27565 27564 0 -1 0 30152 0 0 0 119926 94 0 0 25 0 1 0 546078632 125083648 28286 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30538 28286 603 41 0 30497 0
vsize: 122152
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.93 1/54 8825
Raw data (stat): 8825 (minisat+) Z 8824 27565 27564 0 -1 12 30152 0 0 0 119926 100 0 0 25 0 1 0 546078632 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.08
CPU time (s): 1200.27
CPU user time (s): 1199.26
CPU system time (s): 1.00685
CPU usage (%): 100.016
Max. virtual memory (Kb): 122152
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####