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 18501

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-21 15:16:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17906 boxname=wulflinc2 idbench=1378 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  d1b87efc35bcd73acfc5183bbe3df4f0  /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-pp08aCUTS.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc2/normalized-mps-v2-13-7-pp08aCUTS.opb
IDLAUNCH: 17906
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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:        894504 kB
Buffers:         15316 kB
Cached:         104388 kB
SwapCached:        588 kB
Active:          18800 kB
Inactive:       102916 kB
HighTotal:      131008 kB
HighFree:        43204 kB
LowTotal:       903652 kB
LowFree:        851300 kB
SwapTotal:     2097136 kB
SwapFree:      2095664 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5108 kB
Slab:            12780 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:36:20 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 17906 7 1200.18 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 |  215438   519594 |   71812       0        0     nan |  0.000 % |
c |       101 |  215326   519346 |   78993      79      271     3.4 |  4.796 % |
c |       251 |  215165   518988 |   86892     203      739     3.6 |  4.854 % |
c |       476 |  215013   518651 |   95581     405     1451     3.6 |  4.912 % |
c |       814 |  214882   518363 |  105139     718     2555     3.6 |  4.964 % |
c |      1320 |  214188   516814 |  115653    1138     3953     3.5 |  5.212 % |
c |      2079 |  213603   515514 |  127219    1804     6333     3.5 |  5.426 % |
c |      3218 |  213209   514630 |  139941    2898    10656     3.7 |  5.562 % |
c |      4926 |  212696   513482 |  153935    4545    17723     3.9 |  5.742 % |
c |      7488 |  211648   511137 |  169328    6973    28093     4.0 |  6.108 % |
c |     11332 |  210588   508770 |  186261   10695    45175     4.2 |  6.481 % |
c |     17098 |  208970   505150 |  204888   16237    70107     4.3 |  7.050 % |
c |     25747 |  207655   502206 |  225376   24727   121042     4.9 |  7.504 % |
c |     38721 |  206711   500085 |  247914   37579   208692     5.6 |  7.832 % |
c |     58183 |  206122   498761 |  272705   56950   373165     6.6 |  8.033 % |
c |     87375 |  206065   498634 |  299976   86132  1052463    12.2 |  8.053 % |
c |    131164 |  205853   498158 |  329974  129888  2014357    15.5 |  8.128 % |
c |    196848 |  205590   497567 |  362971  195540  3544352    18.1 |  8.217 % |
c |    295374 |  205512   497392 |  399268  294054  6084326    20.7 |  8.247 % |
c |    443164 |  205325   496976 |  439195   68442   994490    14.5 |  8.316 % |
#### 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.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (runsolver) R 29842 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487868985 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0008 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7157 0 0 0 981 17 0 0 25 0 1 0 487868985 33501184 6824 4294967295 134512640 134672761 3221224624 3221223792 134561264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8179 6824 603 41 0 8138 0
vsize: 32716
[startup+20.0011 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7189 0 0 0 1980 17 0 0 25 0 1 0 487868985 33636352 6856 4294967295 134512640 134672761 3221224624 3221223748 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8212 6856 603 41 0 8171 0
vsize: 32848
[startup+30.0016 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7226 0 0 0 2979 18 0 0 25 0 1 0 487868985 33787904 6893 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8249 6893 603 41 0 8208 0
vsize: 32996
[startup+40.0021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7261 0 0 0 3979 18 0 0 25 0 1 0 487868985 33923072 6928 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8282 6928 603 41 0 8241 0
vsize: 33128
[startup+50.0022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7291 0 0 0 4977 19 0 0 25 0 1 0 487868985 34058240 6958 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8315 6958 603 41 0 8274 0
vsize: 33260
[startup+60.0021 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7319 0 0 0 5977 19 0 0 25 0 1 0 487868985 34193408 6986 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8348 6986 603 41 0 8307 0
vsize: 33392
[startup+70.0029 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7359 0 0 0 6977 19 0 0 25 0 1 0 487868985 34406400 7026 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8400 7026 603 41 0 8359 0
vsize: 33600
[startup+80.0022 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7393 0 0 0 7977 19 0 0 25 0 1 0 487868985 34406400 7060 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8400 7060 603 41 0 8359 0
vsize: 33600
[startup+90.0027 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7418 0 0 0 8977 19 0 0 25 0 1 0 487868985 34541568 7085 4294967295 134512640 134672761 3221224624 3221223824 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8433 7085 603 41 0 8392 0
vsize: 33732
[startup+100.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7447 0 0 0 9977 20 0 0 25 0 1 0 487868985 34676736 7114 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8466 7114 603 41 0 8425 0
vsize: 33864
[startup+110.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7479 0 0 0 10976 20 0 0 25 0 1 0 487868985 34811904 7146 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8499 7146 603 41 0 8458 0
vsize: 33996
[startup+120.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7514 0 0 0 11976 20 0 0 25 0 1 0 487868985 34942976 7181 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8531 7181 603 41 0 8490 0
vsize: 34124
[startup+130.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7572 0 0 0 12976 21 0 0 25 0 1 0 487868985 35205120 7239 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8595 7239 603 41 0 8554 0
vsize: 34380
[startup+140.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7583 0 0 0 13976 21 0 0 25 0 1 0 487868985 35340288 7250 4294967295 134512640 134672761 3221224624 3221223748 134566052 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8628 7250 603 41 0 8587 0
vsize: 34512
[startup+150.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7625 0 0 0 14976 21 0 0 25 0 1 0 487868985 35475456 7292 4294967295 134512640 134672761 3221224624 3221223748 134566098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8661 7292 603 41 0 8620 0
vsize: 34644
[startup+160.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7670 0 0 0 15976 21 0 0 25 0 1 0 487868985 35606528 7337 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8693 7337 603 41 0 8652 0
vsize: 34772
[startup+170.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7715 0 0 0 16976 21 0 0 25 0 1 0 487868985 35741696 7382 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8726 7382 603 41 0 8685 0
vsize: 34904
[startup+180.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7774 0 0 0 17976 22 0 0 25 0 1 0 487868985 36012032 7441 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8792 7441 603 41 0 8751 0
vsize: 35168
[startup+190.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7814 0 0 0 18976 22 0 0 25 0 1 0 487868985 36147200 7481 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8825 7481 603 41 0 8784 0
vsize: 35300
[startup+200.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7855 0 0 0 19976 22 0 0 25 0 1 0 487868985 36278272 7522 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8857 7522 603 41 0 8816 0
vsize: 35428
[startup+210.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 7918 0 0 0 20976 22 0 0 25 0 1 0 487868985 36544512 7585 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8922 7585 603 41 0 8881 0
vsize: 35688
[startup+220.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 8294 0 0 0 21975 23 0 0 25 0 1 0 487868985 38281216 7961 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9346 7961 603 41 0 9305 0
vsize: 37384
[startup+230.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 8786 0 0 0 22973 26 0 0 25 0 1 0 487868985 40296448 8453 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9838 8453 603 41 0 9797 0
vsize: 39352
[startup+240.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 9042 0 0 0 23972 27 0 0 25 0 1 0 487868985 41369600 8709 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10100 8709 603 41 0 10059 0
vsize: 40400
[startup+250.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 9193 0 0 0 24972 27 0 0 25 0 1 0 487868985 41910272 8860 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10232 8860 603 41 0 10191 0
vsize: 40928
[startup+260.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 9273 0 0 0 25972 27 0 0 25 0 1 0 487868985 42307584 8940 4294967295 134512640 134672761 3221224624 3221223764 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10329 8940 603 41 0 10288 0
vsize: 41316
[startup+270.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 9405 0 0 0 26971 28 0 0 25 0 1 0 487868985 42713088 9072 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10428 9072 603 41 0 10387 0
vsize: 41712
[startup+280.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 9626 0 0 0 27971 28 0 0 25 0 1 0 487868985 43655168 9293 4294967295 134512640 134672761 3221224624 3221223748 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10658 9293 603 41 0 10617 0
vsize: 42632
[startup+290.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 9726 0 0 0 28971 29 0 0 25 0 1 0 487868985 44056576 9393 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10756 9393 603 41 0 10715 0
vsize: 43024
[startup+300.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 9873 0 0 0 29970 30 0 0 25 0 1 0 487868985 44597248 9540 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10888 9540 603 41 0 10847 0
vsize: 43552
[startup+310.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 10164 0 0 0 30969 31 0 0 25 0 1 0 487868985 45793280 9831 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11180 9831 603 41 0 11139 0
vsize: 44720
[startup+320.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 10286 0 0 0 31969 31 0 0 25 0 1 0 487868985 46346240 9953 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11315 9953 603 41 0 11274 0
vsize: 45260
[startup+330.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 10439 0 0 0 32969 32 0 0 25 0 1 0 487868985 47403008 10106 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11573 10106 603 41 0 11532 0
vsize: 46292
[startup+340.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 10662 0 0 0 33969 32 0 0 25 0 1 0 487868985 48340992 10329 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11802 10329 603 41 0 11761 0
vsize: 47208
[startup+350.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 10800 0 0 0 34968 32 0 0 25 0 1 0 487868985 48889856 10467 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11936 10467 603 41 0 11895 0
vsize: 47744
[startup+360.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 10855 0 0 0 35968 33 0 0 25 0 1 0 487868985 49160192 10522 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12002 10522 603 41 0 11961 0
vsize: 48008
[startup+370.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11010 0 0 0 36968 34 0 0 25 0 1 0 487868985 49704960 10677 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12135 10677 603 41 0 12094 0
vsize: 48540
[startup+380.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11155 0 0 0 37968 34 0 0 25 0 1 0 487868985 50380800 10822 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12300 10822 603 41 0 12259 0
vsize: 49200
[startup+390.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11266 0 0 0 38967 34 0 0 25 0 1 0 487868985 50778112 10933 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12397 10933 603 41 0 12356 0
vsize: 49588
[startup+400.005 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11478 0 0 0 39967 35 0 0 25 0 1 0 487868985 51585024 11145 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12594 11145 603 41 0 12553 0
vsize: 50376
[startup+410.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11605 0 0 0 40967 35 0 0 25 0 1 0 487868985 52121600 11272 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12725 11272 603 41 0 12684 0
vsize: 50900
[startup+420.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11669 0 0 0 41967 35 0 0 25 0 1 0 487868985 52387840 11336 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12790 11336 603 41 0 12749 0
vsize: 51160
[startup+430.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11746 0 0 0 42966 36 0 0 25 0 1 0 487868985 52658176 11413 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12856 11413 603 41 0 12815 0
vsize: 51424
[startup+440.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11810 0 0 0 43966 36 0 0 25 0 1 0 487868985 52928512 11477 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12922 11477 603 41 0 12881 0
vsize: 51688
[startup+450.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 11963 0 0 0 44965 37 0 0 25 0 1 0 487868985 53596160 11630 4294967295 134512640 134672761 3221224624 3221223748 134566089 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13085 11630 603 41 0 13044 0
vsize: 52340
[startup+460.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12074 0 0 0 45965 37 0 0 25 0 1 0 487868985 54001664 11741 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13184 11741 603 41 0 13143 0
vsize: 52736
[startup+470.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12228 0 0 0 46965 38 0 0 25 0 1 0 487868985 54677504 11895 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13349 11895 603 41 0 13308 0
vsize: 53396
[startup+480.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12373 0 0 0 47964 39 0 0 25 0 1 0 487868985 55218176 12040 4294967295 134512640 134672761 3221224624 3221223824 134557913 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13481 12040 603 41 0 13440 0
vsize: 53924
[startup+490.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12468 0 0 0 48964 39 0 0 25 0 1 0 487868985 55619584 12135 4294967295 134512640 134672761 3221224624 3221223776 134565121 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13579 12135 603 41 0 13538 0
vsize: 54316
[startup+500.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12568 0 0 0 49963 40 0 0 25 0 1 0 487868985 56020992 12235 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13677 12235 603 41 0 13636 0
vsize: 54708
[startup+510.004 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12638 0 0 0 50963 40 0 0 25 0 1 0 487868985 56291328 12305 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13743 12305 603 41 0 13702 0
vsize: 54972
[startup+520.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12702 0 0 0 51963 40 0 0 25 0 1 0 487868985 56557568 12369 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13808 12369 603 41 0 13767 0
vsize: 55232
[startup+530.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12809 0 0 0 52963 41 0 0 25 0 1 0 487868985 56958976 12476 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13906 12476 603 41 0 13865 0
vsize: 55624
[startup+540.003 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12860 0 0 0 53962 41 0 0 25 0 1 0 487868985 57094144 12527 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13939 12527 603 41 0 13898 0
vsize: 55756
[startup+550.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 12967 0 0 0 54962 41 0 0 25 0 1 0 487868985 57491456 12634 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14036 12634 603 41 0 13995 0
vsize: 56144
[startup+560.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 13094 0 0 0 55962 42 0 0 25 0 1 0 487868985 58032128 12761 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14168 12761 603 41 0 14127 0
vsize: 56672
[startup+570.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 13249 0 0 0 56962 42 0 0 25 0 1 0 487868985 58703872 12916 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14332 12916 603 41 0 14291 0
vsize: 57328
[startup+580.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 13384 0 0 0 57961 43 0 0 25 0 1 0 487868985 59273216 13051 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14471 13051 603 41 0 14430 0
vsize: 57884
[startup+590.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 13496 0 0 0 58961 43 0 0 25 0 1 0 487868985 59674624 13163 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14569 13163 603 41 0 14528 0
vsize: 58276
[startup+600.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 13636 0 0 0 59961 43 0 0 25 0 1 0 487868985 60207104 13303 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14699 13303 603 41 0 14658 0
vsize: 58796
[startup+610 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 13760 0 0 0 60961 44 0 0 25 0 1 0 487868985 60743680 13427 4294967295 134512640 134672761 3221224624 3221223808 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14830 13427 603 41 0 14789 0
vsize: 59320
[startup+620 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 13884 0 0 0 61960 44 0 0 25 0 1 0 487868985 61276160 13551 4294967295 134512640 134672761 3221224624 3221223808 134559542 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14960 13551 603 41 0 14919 0
vsize: 59840
[startup+630 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 13960 0 0 0 62960 45 0 0 25 0 1 0 487868985 61538304 13627 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15024 13627 603 41 0 14983 0
vsize: 60096
[startup+640 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 14041 0 0 0 63960 45 0 0 25 0 1 0 487868985 61800448 13708 4294967295 134512640 134672761 3221224624 3221223808 134558667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15088 13708 603 41 0 15047 0
vsize: 60352
[startup+650 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 14177 0 0 0 64959 46 0 0 25 0 1 0 487868985 62468096 13844 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15251 13844 603 41 0 15210 0
vsize: 61004
[startup+660 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 14278 0 0 0 65959 47 0 0 25 0 1 0 487868985 62873600 13945 4294967295 134512640 134672761 3221224624 3221223748 134566018 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15350 13945 603 41 0 15309 0
vsize: 61400
[startup+670.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 14347 0 0 0 66959 47 0 0 25 0 1 0 487868985 63008768 14014 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15383 14014 603 41 0 15342 0
vsize: 61532
[startup+680 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 14556 0 0 0 67958 48 0 0 25 0 1 0 487868985 63942656 14223 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15611 14223 603 41 0 15570 0
vsize: 62444
[startup+690 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 14654 0 0 0 68958 48 0 0 25 0 1 0 487868985 65388544 14321 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15964 14321 603 41 0 15923 0
vsize: 63856
[startup+700 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 14761 0 0 0 69958 48 0 0 25 0 1 0 487868985 65789952 14428 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16062 14428 603 41 0 16021 0
vsize: 64248
[startup+710 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 15220 0 0 0 70957 50 0 0 25 0 1 0 487868985 67661824 14887 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16519 14887 603 41 0 16478 0
vsize: 66076
[startup+720 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 15615 0 0 0 71956 50 0 0 25 0 1 0 487868985 69267456 15282 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16911 15282 603 41 0 16870 0
vsize: 67644
[startup+730 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 15688 0 0 0 72956 51 0 0 25 0 1 0 487868985 69537792 15355 4294967295 134512640 134672761 3221224624 3221223780 134564777 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16977 15355 603 41 0 16936 0
vsize: 67908
[startup+740 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 15798 0 0 0 73956 51 0 0 25 0 1 0 487868985 69939200 15465 4294967295 134512640 134672761 3221224624 3221223792 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17075 15465 603 41 0 17034 0
vsize: 68300
[startup+750.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 15987 0 0 0 74955 52 0 0 25 0 1 0 487868985 70746112 15654 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17272 15654 603 41 0 17231 0
vsize: 69088
[startup+760.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 16097 0 0 0 75954 53 0 0 25 0 1 0 487868985 71151616 15764 4294967295 134512640 134672761 3221224624 3221223792 134560785 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17371 15764 603 41 0 17330 0
vsize: 69484
[startup+770.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 16283 0 0 0 76953 53 0 0 25 0 1 0 487868985 71815168 15950 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17533 15950 603 41 0 17492 0
vsize: 70132
[startup+780 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 16373 0 0 0 77952 54 0 0 25 0 1 0 487868985 72216576 16040 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17631 16040 603 41 0 17590 0
vsize: 70524
[startup+790 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 16483 0 0 0 78952 55 0 0 25 0 1 0 487868985 72617984 16150 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17729 16150 603 41 0 17688 0
vsize: 70916
[startup+800 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 16587 0 0 0 79952 55 0 0 25 0 1 0 487868985 73015296 16254 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17826 16254 603 41 0 17785 0
vsize: 71304
[startup+810.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 16678 0 0 0 80952 55 0 0 25 0 1 0 487868985 73420800 16345 4294967295 134512640 134672761 3221224624 3221223748 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17925 16345 603 41 0 17884 0
vsize: 71700
[startup+820 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 16955 0 0 0 81951 56 0 0 25 0 1 0 487868985 74489856 16622 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18186 16622 603 41 0 18145 0
vsize: 72744
[startup+830 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17073 0 0 0 82951 56 0 0 25 0 1 0 487868985 75026432 16740 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18317 16740 603 41 0 18276 0
vsize: 73268
[startup+840 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17216 0 0 0 83951 56 0 0 25 0 1 0 487868985 75558912 16883 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18447 16883 603 41 0 18406 0
vsize: 73788
[startup+849.999 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17325 0 0 0 84951 57 0 0 25 0 1 0 487868985 75964416 16992 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18546 16992 603 41 0 18505 0
vsize: 74184
[startup+860 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17430 0 0 0 85950 58 0 0 25 0 1 0 487868985 76369920 17097 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18645 17097 603 41 0 18604 0
vsize: 74580
[startup+870 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17518 0 0 0 86950 58 0 0 25 0 1 0 487868985 76775424 17185 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18744 17185 603 41 0 18703 0
vsize: 74976
[startup+879.999 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17578 0 0 0 87950 58 0 0 25 0 1 0 487868985 77037568 17245 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18808 17245 603 41 0 18767 0
vsize: 75232
[startup+889.999 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17692 0 0 0 88950 58 0 0 25 0 1 0 487868985 77434880 17359 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18905 17359 603 41 0 18864 0
vsize: 75620
[startup+899.999 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17814 0 0 0 89950 59 0 0 25 0 1 0 487868985 77971456 17481 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19036 17481 603 41 0 18995 0
vsize: 76144
[startup+909.999 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 17956 0 0 0 90950 59 0 0 25 0 1 0 487868985 78508032 17623 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19167 17623 603 41 0 19126 0
vsize: 76668
[startup+920 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 18204 0 0 0 91949 60 0 0 25 0 1 0 487868985 79446016 17871 4294967295 134512640 134672761 3221224624 3221223776 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19396 17871 603 41 0 19355 0
vsize: 77584
[startup+930 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 18362 0 0 0 92948 61 0 0 25 0 1 0 487868985 80117760 18029 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19560 18029 603 41 0 19519 0
vsize: 78240
[startup+940 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 18506 0 0 0 93948 62 0 0 25 0 1 0 487868985 80650240 18173 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19690 18173 603 41 0 19649 0
vsize: 78760
[startup+950 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 18647 0 0 0 94947 62 0 0 25 0 1 0 487868985 81321984 18314 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19854 18314 603 41 0 19813 0
vsize: 79416
[startup+960.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 18795 0 0 0 95947 63 0 0 25 0 1 0 487868985 81883136 18462 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19991 18462 603 41 0 19950 0
vsize: 79964
[startup+970.001 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 18936 0 0 0 96947 63 0 0 25 0 1 0 487868985 82456576 18603 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20131 18603 603 41 0 20090 0
vsize: 80524
[startup+980 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 19090 0 0 0 97947 63 0 0 25 0 1 0 487868985 83202048 18757 4294967295 134512640 134672761 3221224624 3221223716 1075352576 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20313 18757 603 41 0 20272 0
vsize: 81252
[startup+990.002 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 19228 0 0 0 98947 64 0 0 25 0 1 0 487868985 83738624 18895 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20444 18895 603 41 0 20403 0
vsize: 81776
[startup+1000 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 19373 0 0 0 99947 64 0 0 25 0 1 0 487868985 84344832 19040 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20592 19040 603 41 0 20551 0
vsize: 82368
[startup+1010 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 19523 0 0 0 100946 65 0 0 25 0 1 0 487868985 84881408 19190 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20723 19190 603 41 0 20682 0
vsize: 82892
[startup+1020 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 19682 0 0 0 101946 65 0 0 25 0 1 0 487868985 85544960 19349 4294967295 134512640 134672761 3221224624 3221223792 134565153 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20885 19349 603 41 0 20844 0
vsize: 83540
[startup+1030 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 19804 0 0 0 102946 65 0 0 25 0 1 0 487868985 86081536 19471 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21016 19471 603 41 0 20975 0
vsize: 84064
[startup+1040 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 19937 0 0 0 103945 66 0 0 25 0 1 0 487868985 86614016 19604 4294967295 134512640 134672761 3221224624 3221223760 134560634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21146 19604 603 41 0 21105 0
vsize: 84584
[startup+1050 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20222 0 0 0 104944 68 0 0 25 0 1 0 487868985 87691264 19889 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21409 19889 603 41 0 21368 0
vsize: 85636
[startup+1060 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 105944 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1070 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 106944 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1080 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 107944 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223768 134560630 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1090 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 108945 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1100 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 109945 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 110945 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 111945 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1130 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 112945 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1140 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 113945 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1150 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 114944 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 115944 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 116944 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223760 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 117944 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 118945 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.99 0.91 2/54 29843
Raw data (stat): 29843 (minisat+) R 29842 20937 20936 0 -1 0 20313 0 0 0 119945 68 0 0 25 0 1 0 487868985 88088576 19980 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21506 19980 603 41 0 21465 0
vsize: 86024
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.99 0.91 1/54 29843
Raw data (stat): 29843 (minisat+) Z 29842 20937 20936 0 -1 12 20315 0 0 0 119945 72 0 0 25 0 1 0 487868985 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.05
CPU time (s): 1200.18
CPU user time (s): 1199.45
CPU system time (s): 0.724889
CPU usage (%): 100.011
Max. virtual memory (Kb): 86024
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####