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 18482

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        862600 kB
Buffers:          3168 kB
Cached:         146908 kB
SwapCached:          0 kB
Active:          27520 kB
Inactive:       125472 kB
HighTotal:      131008 kB
HighFree:        78092 kB
LowTotal:       903652 kB
LowFree:        784508 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6952 kB
Slab:            13348 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 15:34:45 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 17914 7 1200.24 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  242059   593973 |   80686       0        0     nan |  0.000 % |
c |       100 |  242057   593969 |   88754      99      785     7.9 |  4.757 % |
c |       250 |  242022   593893 |   97630     241     1354     5.6 |  4.772 % |
c |       475 |  241844   593501 |  107393     440     2259     5.1 |  4.839 % |
c |       812 |  241504   592749 |  118132     725     3264     4.5 |  4.963 % |
c |      1318 |  241275   592241 |  129945    1194     5789     4.8 |  5.047 % |
c |      2078 |  240855   591303 |  142940    1887     8714     4.6 |  5.203 % |
c |      3217 |  239919   589215 |  157234    2886    12396     4.3 |  5.526 % |
c |      4926 |  238981   587113 |  172957    4486    18229     4.1 |  5.850 % |
c |      7488 |  238227   585426 |  190253    6947    28790     4.1 |  6.114 % |
c |     11332 |  237367   583504 |  209278   10682    46406     4.3 |  6.415 % |
c |     17099 |  235780   579943 |  230206   16256    74798     4.6 |  6.985 % |
c |     25748 |  234062   576092 |  253227   24709   121215     4.9 |  7.597 % |
c |     38722 |  233089   573909 |  278549   37552   207662     5.5 |  7.939 % |
c |     58183 |  232398   572347 |  306404   56909   403740     7.1 |  8.182 % |
c |     87375 |  231526   570372 |  337045   85955   709517     8.3 |  8.508 % |
c |    131166 |  230884   568914 |  370749  129667  1288968     9.9 |  8.748 % |
c |    196851 |  230624   568325 |  407824  195318  2511008    12.9 |  8.848 % |
c |    295377 |  230164   567286 |  448607  293773  5665799    19.3 |  9.008 % |
#### 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.85 0.97 0.91 2/55 13157
Raw data (stat): 13157 (runsolver) R 13156 30927 30926 0 -1 64 0 0 0 0 0 0 0 0 20 0 1 0 423342535 1052672 97 4294967295 134512640 135381576 3221224432 3221219860 135011389 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 97 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.87 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7294 0 0 0 980 19 0 0 25 0 1 0 423342535 33878016 6955 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 6955 603 41 0 8230 0
vsize: 33084
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7318 0 0 0 1980 19 0 0 25 0 1 0 423342535 33878016 6979 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8271 6979 603 41 0 8230 0
vsize: 33084
[startup+30.0019 s]
Raw data (loadavg): 0.91 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7349 0 0 0 2980 19 0 0 25 0 1 0 423342535 34013184 7010 4294967295 134512640 134672761 3221224544 3221223668 134566122 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8304 7010 603 41 0 8263 0
vsize: 33216
[startup+40.0016 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7389 0 0 0 3980 19 0 0 25 0 1 0 423342535 34148352 7050 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8337 7050 603 41 0 8296 0
vsize: 33348
[startup+50.0028 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7412 0 0 0 4980 19 0 0 25 0 1 0 423342535 34283520 7073 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8370 7073 603 41 0 8329 0
vsize: 33480
[startup+60.003 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7440 0 0 0 5980 19 0 0 25 0 1 0 423342535 34283520 7101 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8370 7101 603 41 0 8329 0
vsize: 33480
[startup+70.0037 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7464 0 0 0 6980 20 0 0 25 0 1 0 423342535 34418688 7125 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8403 7125 603 41 0 8362 0
vsize: 33612
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7493 0 0 0 7980 20 0 0 25 0 1 0 423342535 34631680 7154 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8455 7154 603 41 0 8414 0
vsize: 33820
[startup+90.004 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7521 0 0 0 8980 20 0 0 25 0 1 0 423342535 34631680 7182 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8455 7182 603 41 0 8414 0
vsize: 33820
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7544 0 0 0 9980 20 0 0 25 0 1 0 423342535 34762752 7205 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8487 7205 603 41 0 8446 0
vsize: 33948
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7576 0 0 0 10980 20 0 0 25 0 1 0 423342535 34893824 7237 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8519 7237 603 41 0 8478 0
vsize: 34076
[startup+120.004 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7609 0 0 0 11980 20 0 0 25 0 1 0 423342535 35024896 7270 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8551 7270 603 41 0 8510 0
vsize: 34204
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7644 0 0 0 12980 20 0 0 25 0 1 0 423342535 35160064 7305 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8584 7305 603 41 0 8543 0
vsize: 34336
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7702 0 0 0 13980 21 0 0 25 0 1 0 423342535 35422208 7363 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8648 7363 603 41 0 8607 0
vsize: 34592
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7713 0 0 0 14980 21 0 0 25 0 1 0 423342535 35553280 7374 4294967295 134512640 134672761 3221224544 3221223744 134557842 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8680 7374 603 41 0 8639 0
vsize: 34720
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7755 0 0 0 15980 21 0 0 25 0 1 0 423342535 35688448 7416 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8713 7416 603 41 0 8672 0
vsize: 34852
[startup+170.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7793 0 0 0 16979 21 0 0 25 0 1 0 423342535 35823616 7454 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8746 7454 603 41 0 8705 0
vsize: 34984
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7885 0 0 0 17979 22 0 0 25 0 1 0 423342535 36229120 7546 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8845 7546 603 41 0 8804 0
vsize: 35380
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7925 0 0 0 18979 22 0 0 25 0 1 0 423342535 36364288 7586 4294967295 134512640 134672761 3221224544 3221223680 134560557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8878 7586 603 41 0 8837 0
vsize: 35512
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 7982 0 0 0 19978 23 0 0 25 0 1 0 423342535 36499456 7643 4294967295 134512640 134672761 3221224544 3221223744 134557959 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8911 7643 603 41 0 8870 0
vsize: 35644
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8020 0 0 0 20979 23 0 0 25 0 1 0 423342535 36769792 7681 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8977 7681 603 41 0 8936 0
vsize: 35908
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8070 0 0 0 21979 23 0 0 25 0 1 0 423342535 36904960 7731 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9010 7731 603 41 0 8969 0
vsize: 36040
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8131 0 0 0 22979 23 0 0 25 0 1 0 423342535 37171200 7792 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9075 7792 603 41 0 9034 0
vsize: 36300
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8171 0 0 0 23979 23 0 0 25 0 1 0 423342535 37302272 7832 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9107 7832 603 41 0 9066 0
vsize: 36428
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8236 0 0 0 24979 23 0 0 25 0 1 0 423342535 37568512 7897 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9172 7897 603 41 0 9131 0
vsize: 36688
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8284 0 0 0 25979 23 0 0 25 0 1 0 423342535 37961728 7945 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9268 7945 603 41 0 9227 0
vsize: 37072
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8336 0 0 0 26979 23 0 0 25 0 1 0 423342535 38232064 7997 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9334 7997 603 41 0 9293 0
vsize: 37336
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8380 0 0 0 27979 23 0 0 25 0 1 0 423342535 38367232 8041 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9367 8041 603 41 0 9326 0
vsize: 37468
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8428 0 0 0 28979 24 0 0 25 0 1 0 423342535 38502400 8089 4294967295 134512640 134672761 3221224544 3221223716 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9400 8089 603 41 0 9359 0
vsize: 37600
[startup+300.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8477 0 0 0 29979 24 0 0 25 0 1 0 423342535 38768640 8138 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9465 8138 603 41 0 9424 0
vsize: 37860
[startup+310.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8541 0 0 0 30979 24 0 0 25 0 1 0 423342535 39034880 8202 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9530 8202 603 41 0 9489 0
vsize: 38120
[startup+320.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8606 0 0 0 31979 24 0 0 25 0 1 0 423342535 39170048 8267 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9563 8267 603 41 0 9522 0
vsize: 38252
[startup+330.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8658 0 0 0 32979 25 0 0 25 0 1 0 423342535 39436288 8319 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9628 8319 603 41 0 9587 0
vsize: 38512
[startup+340.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8733 0 0 0 33979 25 0 0 25 0 1 0 423342535 39706624 8394 4294967295 134512640 134672761 3221224544 3221223680 134560686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9694 8394 603 41 0 9653 0
vsize: 38776
[startup+350.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8801 0 0 0 34979 25 0 0 25 0 1 0 423342535 39972864 8462 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9759 8462 603 41 0 9718 0
vsize: 39036
[startup+360.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8882 0 0 0 35979 25 0 0 25 0 1 0 423342535 40374272 8543 4294967295 134512640 134672761 3221224544 3221223680 134560654 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9857 8543 603 41 0 9816 0
vsize: 39428
[startup+370.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8937 0 0 0 36979 25 0 0 25 0 1 0 423342535 40509440 8598 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9890 8598 603 41 0 9849 0
vsize: 39560
[startup+380.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 8980 0 0 0 37979 25 0 0 25 0 1 0 423342535 40644608 8641 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9923 8641 603 41 0 9882 0
vsize: 39692
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9030 0 0 0 38979 25 0 0 25 0 1 0 423342535 40914944 8691 4294967295 134512640 134672761 3221224544 3221223668 134566100 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9989 8691 603 41 0 9948 0
vsize: 39956
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9091 0 0 0 39979 26 0 0 25 0 1 0 423342535 41185280 8752 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10055 8752 603 41 0 10014 0
vsize: 40220
[startup+410.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9173 0 0 0 40979 26 0 0 25 0 1 0 423342535 41455616 8834 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10121 8834 603 41 0 10080 0
vsize: 40484
[startup+420.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9237 0 0 0 41979 27 0 0 25 0 1 0 423342535 41717760 8898 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10185 8898 603 41 0 10144 0
vsize: 40740
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9296 0 0 0 42979 27 0 0 25 0 1 0 423342535 41984000 8957 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10250 8957 603 41 0 10209 0
vsize: 41000
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9355 0 0 0 43979 27 0 0 25 0 1 0 423342535 42115072 9016 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10282 9016 603 41 0 10241 0
vsize: 41128
[startup+450.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9428 0 0 0 44978 27 0 0 25 0 1 0 423342535 42385408 9089 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10348 9089 603 41 0 10307 0
vsize: 41392
[startup+460.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9502 0 0 0 45978 28 0 0 25 0 1 0 423342535 42790912 9163 4294967295 134512640 134672761 3221224544 3221223680 134560667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10447 9163 603 41 0 10406 0
vsize: 41788
[startup+470.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9568 0 0 0 46978 28 0 0 25 0 1 0 423342535 42926080 9229 4294967295 134512640 134672761 3221224544 3221223808 134562218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10480 9229 603 41 0 10439 0
vsize: 41920
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9649 0 0 0 47978 28 0 0 25 0 1 0 423342535 43331584 9310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10579 9310 603 41 0 10538 0
vsize: 42316
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9710 0 0 0 48978 28 0 0 25 0 1 0 423342535 44126208 9371 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10773 9371 603 41 0 10732 0
vsize: 43092
[startup+500.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9777 0 0 0 49978 29 0 0 25 0 1 0 423342535 44396544 9438 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10839 9438 603 41 0 10798 0
vsize: 43356
[startup+510.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9870 0 0 0 50977 29 0 0 25 0 1 0 423342535 44666880 9531 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10905 9531 603 41 0 10864 0
vsize: 43620
[startup+520.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9929 0 0 0 51977 29 0 0 25 0 1 0 423342535 44937216 9590 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10971 9590 603 41 0 10930 0
vsize: 43884
[startup+530.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 9995 0 0 0 52977 29 0 0 25 0 1 0 423342535 45207552 9656 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11037 9656 603 41 0 10996 0
vsize: 44148
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 10056 0 0 0 53977 30 0 0 25 0 1 0 423342535 45477888 9717 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11103 9717 603 41 0 11062 0
vsize: 44412
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 10165 0 0 0 54977 30 0 0 25 0 1 0 423342535 45879296 9826 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11201 9826 603 41 0 11160 0
vsize: 44804
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 10320 0 0 0 55976 31 0 0 25 0 1 0 423342535 46415872 9981 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11332 9981 603 41 0 11291 0
vsize: 45328
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 10394 0 0 0 56976 31 0 0 25 0 1 0 423342535 46821376 10055 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11431 10055 603 41 0 11390 0
vsize: 45724
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 10541 0 0 0 57975 32 0 0 25 0 1 0 423342535 47362048 10202 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11563 10202 603 41 0 11522 0
vsize: 46252
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 10645 0 0 0 58975 32 0 0 25 0 1 0 423342535 47763456 10306 4294967295 134512640 134672761 3221224544 3221223784 134557737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11661 10306 603 41 0 11620 0
vsize: 46644
[startup+600.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 10767 0 0 0 59975 33 0 0 25 0 1 0 423342535 48300032 10428 4294967295 134512640 134672761 3221224544 3221223688 134565969 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11792 10428 603 41 0 11751 0
vsize: 47168
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 10953 0 0 0 60974 34 0 0 25 0 1 0 423342535 48971776 10614 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11956 10614 603 41 0 11915 0
vsize: 47824
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 11044 0 0 0 61974 34 0 0 25 0 1 0 423342535 49373184 10705 4294967295 134512640 134672761 3221224544 3221223680 134560596 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12054 10705 603 41 0 12013 0
vsize: 48216
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 11102 0 0 0 62974 34 0 0 25 0 1 0 423342535 49643520 10763 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12120 10763 603 41 0 12079 0
vsize: 48480
[startup+640.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 11146 0 0 0 63974 34 0 0 25 0 1 0 423342535 49778688 10807 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12153 10807 603 41 0 12112 0
vsize: 48612
[startup+650.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 11292 0 0 0 64973 35 0 0 25 0 1 0 423342535 50315264 10953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12284 10953 603 41 0 12243 0
vsize: 49136
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 11468 0 0 0 65973 36 0 0 25 0 1 0 423342535 50987008 11129 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12448 11129 603 41 0 12407 0
vsize: 49792
[startup+670.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 11568 0 0 0 66972 36 0 0 25 0 1 0 423342535 51392512 11229 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12547 11229 603 41 0 12506 0
vsize: 50188
[startup+680.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 11810 0 0 0 67972 37 0 0 25 0 1 0 423342535 52465664 11471 4294967295 134512640 134672761 3221224544 3221223696 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12809 11471 603 41 0 12768 0
vsize: 51236
[startup+690.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 12043 0 0 0 68971 38 0 0 25 0 1 0 423342535 53268480 11704 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13005 11704 603 41 0 12964 0
vsize: 52020
[startup+700.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 12153 0 0 0 69970 39 0 0 25 0 1 0 423342535 53809152 11814 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13137 11814 603 41 0 13096 0
vsize: 52548
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 12315 0 0 0 70970 39 0 0 25 0 1 0 423342535 54476800 11976 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 11976 603 41 0 13259 0
vsize: 53200
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 12408 0 0 0 71970 40 0 0 25 0 1 0 423342535 54747136 12069 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13366 12069 603 41 0 13325 0
vsize: 53464
[startup+730.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 12683 0 0 0 72969 41 0 0 25 0 1 0 423342535 55955456 12344 4294967295 134512640 134672761 3221224544 3221223680 134565089 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13661 12344 603 41 0 13620 0
vsize: 54644
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 12887 0 0 0 73969 41 0 0 25 0 1 0 423342535 56766464 12548 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13859 12548 603 41 0 13818 0
vsize: 55436
[startup+750.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13038 0 0 0 74968 42 0 0 25 0 1 0 423342535 57303040 12699 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13990 12699 603 41 0 13949 0
vsize: 55960
[startup+760.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13121 0 0 0 75968 42 0 0 25 0 1 0 423342535 57704448 12782 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14088 12782 603 41 0 14047 0
vsize: 56352
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13211 0 0 0 76968 42 0 0 25 0 1 0 423342535 57970688 12872 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14153 12872 603 41 0 14112 0
vsize: 56612
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13315 0 0 0 77968 43 0 0 25 0 1 0 423342535 58368000 12976 4294967295 134512640 134672761 3221224544 3221223648 134559805 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14250 12976 603 41 0 14209 0
vsize: 57000
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13393 0 0 0 78968 43 0 0 25 0 1 0 423342535 58769408 13054 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14348 13054 603 41 0 14307 0
vsize: 57392
[startup+800.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13479 0 0 0 79967 44 0 0 25 0 1 0 423342535 59039744 13140 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14414 13140 603 41 0 14373 0
vsize: 57656
[startup+810.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13612 0 0 0 80967 44 0 0 25 0 1 0 423342535 59568128 13273 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14543 13273 603 41 0 14502 0
vsize: 58172
[startup+820.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13681 0 0 0 81967 44 0 0 25 0 1 0 423342535 59838464 13342 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14609 13342 603 41 0 14568 0
vsize: 58436
[startup+830.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 13741 0 0 0 82967 44 0 0 25 0 1 0 423342535 60108800 13402 4294967295 134512640 134672761 3221224544 3221223712 134561278 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14675 13402 603 41 0 14634 0
vsize: 58700
[startup+840.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 14003 0 0 0 83967 45 0 0 25 0 1 0 423342535 61173760 13664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14935 13664 603 41 0 14894 0
vsize: 59740
[startup+850.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 14110 0 0 0 84966 45 0 0 25 0 1 0 423342535 61579264 13771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15034 13771 603 41 0 14993 0
vsize: 60136
[startup+860.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 14411 0 0 0 85965 47 0 0 25 0 1 0 423342535 63840256 14072 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15586 14072 603 41 0 15545 0
vsize: 62344
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 14923 0 0 0 86964 48 0 0 25 0 1 0 423342535 65863680 14584 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16080 14584 603 41 0 16039 0
vsize: 64320
[startup+880.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 15081 0 0 0 87964 49 0 0 25 0 1 0 423342535 66543616 14742 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16246 14742 603 41 0 16205 0
vsize: 64984
[startup+890.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 15485 0 0 0 88963 49 0 0 25 0 1 0 423342535 68149248 15146 4294967295 134512640 134672761 3221224544 3221223696 134561244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16638 15146 603 41 0 16597 0
vsize: 66552
[startup+900.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 15626 0 0 0 89962 50 0 0 25 0 1 0 423342535 68689920 15287 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16770 15287 603 41 0 16729 0
vsize: 67080
[startup+910.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 15826 0 0 0 90961 51 0 0 25 0 1 0 423342535 69488640 15487 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16965 15487 603 41 0 16924 0
vsize: 67860
[startup+920.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 16030 0 0 0 91961 52 0 0 25 0 1 0 423342535 70291456 15691 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17161 15691 603 41 0 17120 0
vsize: 68644
[startup+930.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 16267 0 0 0 92960 53 0 0 25 0 1 0 423342535 71352320 15928 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17420 15928 603 41 0 17379 0
vsize: 69680
[startup+940.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 16398 0 0 0 93960 53 0 0 25 0 1 0 423342535 71753728 16059 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17518 16059 603 41 0 17477 0
vsize: 70072
[startup+950.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 16630 0 0 0 94959 54 0 0 25 0 1 0 423342535 72687616 16291 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17746 16291 603 41 0 17705 0
vsize: 70984
[startup+960.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 16853 0 0 0 95959 55 0 0 25 0 1 0 423342535 73629696 16514 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17976 16514 603 41 0 17935 0
vsize: 71904
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 17049 0 0 0 96958 55 0 0 25 0 1 0 423342535 74432512 16710 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18172 16710 603 41 0 18131 0
vsize: 72688
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 17193 0 0 0 97958 56 0 0 25 0 1 0 423342535 74969088 16854 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18303 16854 603 41 0 18262 0
vsize: 73212
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 17333 0 0 0 98957 56 0 0 25 0 1 0 423342535 75509760 16994 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18435 16994 603 41 0 18394 0
vsize: 73740
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 17487 0 0 0 99957 57 0 0 25 0 1 0 423342535 76177408 17148 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18598 17148 603 41 0 18557 0
vsize: 74392
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 17611 0 0 0 100957 57 0 0 25 0 1 0 423342535 76713984 17272 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18729 17272 603 41 0 18688 0
vsize: 74916
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 17786 0 0 0 101956 58 0 0 25 0 1 0 423342535 77389824 17447 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18894 17447 603 41 0 18853 0
vsize: 75576
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 18006 0 0 0 102956 59 0 0 25 0 1 0 423342535 78192640 17667 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19090 17667 603 41 0 19049 0
vsize: 76360
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 18149 0 0 0 103956 59 0 0 25 0 1 0 423342535 78864384 17810 4294967295 134512640 134672761 3221224544 3221223680 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19254 17810 603 41 0 19213 0
vsize: 77016
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 18370 0 0 0 104955 60 0 0 25 0 1 0 423342535 79667200 18031 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19450 18031 603 41 0 19409 0
vsize: 77800
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 18456 0 0 0 105955 61 0 0 25 0 1 0 423342535 80068608 18117 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19548 18117 603 41 0 19507 0
vsize: 78192
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 18566 0 0 0 106954 61 0 0 25 0 1 0 423342535 80474112 18227 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19647 18227 603 41 0 19606 0
vsize: 78588
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 18742 0 0 0 107954 62 0 0 25 0 1 0 423342535 81145856 18403 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19811 18403 603 41 0 19770 0
vsize: 79244
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 18860 0 0 0 108953 62 0 0 25 0 1 0 423342535 81682432 18521 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19942 18521 603 41 0 19901 0
vsize: 79768
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 19001 0 0 0 109952 63 0 0 25 0 1 0 423342535 82223104 18662 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20074 18662 603 41 0 20033 0
vsize: 80296
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 19120 0 0 0 110953 64 0 0 25 0 1 0 423342535 82759680 18781 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20205 18781 603 41 0 20164 0
vsize: 80820
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 19241 0 0 0 111952 64 0 0 25 0 1 0 423342535 83161088 18902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20303 18902 603 41 0 20262 0
vsize: 81212
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 19409 0 0 0 112952 65 0 0 25 0 1 0 423342535 83832832 19070 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20467 19070 603 41 0 20426 0
vsize: 81868
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 19563 0 0 0 113952 65 0 0 25 0 1 0 423342535 84500480 19224 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20630 19224 603 41 0 20589 0
vsize: 82520
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 19779 0 0 0 114950 66 0 0 25 0 1 0 423342535 85295104 19440 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20824 19440 603 41 0 20783 0
vsize: 83296
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 20019 0 0 0 115950 67 0 0 25 0 1 0 423342535 86360064 19680 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21084 19680 603 41 0 21043 0
vsize: 84336
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 20105 0 0 0 116950 68 0 0 25 0 1 0 423342535 86630400 19766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21150 19766 603 41 0 21109 0
vsize: 84600
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 20291 0 0 0 117949 68 0 0 25 0 1 0 423342535 87437312 19952 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21347 19952 603 41 0 21306 0
vsize: 85388
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 20645 0 0 0 118949 69 0 0 25 0 1 0 423342535 88784896 20306 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21676 20306 603 41 0 21635 0
vsize: 86704
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 13157
Raw data (stat): 13157 (minisat+) R 13156 30927 30926 0 -1 0 20748 0 0 0 119949 70 0 0 25 0 1 0 423342535 89190400 20409 4294967295 134512640 134672761 3221224544 3221223668 134566128 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21775 20409 603 41 0 21734 0
vsize: 87100
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 13157
Raw data (stat): 13157 (minisat+) Z 13156 30927 30926 0 -1 12 20750 0 0 0 119949 74 0 0 23 0 1 0 423342535 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.24
CPU user time (s): 1199.49
CPU system time (s): 0.744886
CPU usage (%): 100.013
Max. virtual memory (Kb): 87100
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####