PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-pp08aCUTS.opb
MD5SUM	fa6454a9831f2da4180d8bfab7c0a21b
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	NO
(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	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.037993
Number of variables	3288
Total number of constraints	310
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	310
Minimum length of a constraint	14
Maximum length of a constraint	123
Trace number 14989

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc12 THE 2005-04-21 02:20:34 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18770 boxname=wulflinc12 idbench=1444 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fa6454a9831f2da4180d8bfab7c0a21b  /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-pp08aCUTS.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-pp08aCUTS.opb /oldhome/oroussel/tmp/wulflinc12/normalized-mps-v2-13-7-pp08aCUTS.opb
IDLAUNCH: 18770
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.091
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.091
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:        830452 kB
Buffers:         20404 kB
Cached:         162200 kB
SwapCached:        316 kB
Active:          27372 kB
Inactive:       157496 kB
HighTotal:      131008 kB
HighFree:        38864 kB
LowTotal:       903652 kB
LowFree:        791588 kB
SwapTotal:     2097136 kB
SwapFree:      2096236 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5748 kB
Slab:            13792 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 02:40:36 (client local time) WITH STATUS 0 IN 1200.29 SECONDS
stats: 18770 7 1200.29 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 ---[ 437]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 436]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 435]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 434]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 433]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 432]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 431]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 430]---> Sorter-cost: 1961     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 428]---> BDD-cost:  158
c ---[ 426]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 420]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 418]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 416]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 414]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 412]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
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 ---[ 408]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 406]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 404]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 402]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 400]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 398]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 396]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 392]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 390]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 388]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 386]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 384]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 382]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> BDD-cost:  158
c ---[ 378]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 376]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 374]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 372]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 370]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 368]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 366]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 364]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 360]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 358]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 354]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 352]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 348]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 346]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 344]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 342]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 340]---> Sorter-cost: 1179     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 ---[ 336]---> Sorter-cost: 1179     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 334]---> Sorter-cost:  427     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:  154
c ---[ 330]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 328]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 324]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 322]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 320]---> Sorter-cost: 1160     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 318]---> Sorter-cost:  418     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 316]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 314]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 312]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 310]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 308]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 306]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 304]---> Sorter-cost: 1141     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 302]---> Sorter-cost:  409     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    6
c ---[ 297]---> BDD-cost:    6
c ---[ 296]---> BDD-cost:    6
c ---[ 295]---> BDD-cost:    6
c ---[ 294]---> BDD-cost:    8
c ---[ 293]---> BDD-cost:   19
c ---[ 292]---> BDD-cost:   19
c ---[ 291]---> BDD-cost:   19
c ---[ 290]---> BDD-cost:   19
c ---[ 289]---> BDD-cost:   19
c ---[ 288]---> BDD-cost:   19
c ---[ 287]---> BDD-cost:   19
c ---[ 286]---> BDD-cost:   19
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    6
c ---[ 281]---> BDD-cost:    6
c ---[ 280]---> BDD-cost:    6
c ---[ 279]---> BDD-cost:    6
c ---[ 278]---> BDD-cost:   23
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    6
c ---[ 273]---> BDD-cost:    6
c ---[ 272]---> BDD-cost:    6
c ---[ 271]---> BDD-cost:    6
c ---[ 270]---> BDD-cost:   23
c ---[ 269]---> BDD-cost:    4
c ---[ 268]---> BDD-cost:    4
c ---[ 267]---> BDD-cost:    4
c ---[ 266]---> BDD-cost:    4
c ---[ 265]---> BDD-cost:    4
c ---[ 264]---> BDD-cost:    4
c ---[ 263]---> BDD-cost:    4
c ---[ 262]---> BDD-cost:    4
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    6
c ---[ 257]---> BDD-cost:    6
c ---[ 256]---> BDD-cost:    6
c ---[ 255]---> BDD-cost:    6
c ---[ 254]---> BDD-cost:    6
c ---[ 253]---> BDD-cost:   19
c ---[ 252]---> BDD-cost:   19
c ---[ 251]---> BDD-cost:   19
c ---[ 250]---> BDD-cost:   19
c ---[ 249]---> BDD-cost:   19
c ---[ 248]---> BDD-cost:   19
c ---[ 247]---> BDD-cost:   19
c ---[ 246]---> BDD-cost:   19
c ---[ 245]---> BDD-cost:    6
c ---[ 244]---> BDD-cost:    6
c ---[ 243]---> BDD-cost:    6
c ---[ 242]---> BDD-cost:    6
c ---[ 241]---> BDD-cost:    6
c ---[ 240]---> BDD-cost:    6
c ---[ 239]---> BDD-cost:    6
c ---[ 238]---> BDD-cost:    6
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:  167
c ---[ 107]---> BDD-cost:   59
c ---[ 106]---> BDD-cost:   38
c ---[ 105]---> BDD-cost:  149
c ---[ 104]---> BDD-cost:   35
c ---[ 103]---> BDD-cost:  152
c ---[ 102]---> BDD-cost:   35
c ---[ 101]---> BDD-cost:  152
c ---[ 100]---> BDD-cost:   38
c ---[  99]---> BDD-cost:  149
c ---[  98]---> BDD-cost:    4
c ---[  97]---> BDD-cost:    5
c ---[  96]---> BDD-cost:   62
c ---[  95]---> BDD-cost:   73
c ---[  94]---> BDD-cost:    3
c ---[  93]---> BDD-cost:   62
c ---[  92]---> BDD-cost:   41
c ---[  91]---> BDD-cost:  158
c ---[  90]---> BDD-cost:   45
c ---[  89]---> BDD-cost:  182
c ---[  88]---> BDD-cost:   40
c ---[  87]---> BDD-cost:  203
c ---[  86]---> BDD-cost:  173
c ---[  85]---> BDD-cost:   35
c ---[  84]---> BDD-cost:  164
c ---[  83]---> BDD-cost:   41
c ---[  82]---> BDD-cost:  158
c ---[  81]---> BDD-cost:    5
c ---[  80]---> BDD-cost:   70
c ---[  79]---> BDD-cost:    3
c ---[  78]---> BDD-cost:   65
c ---[  77]---> BDD-cost:   45
c ---[  76]---> BDD-cost:   45
c ---[  75]---> BDD-cost:  194
c ---[  74]---> BDD-cost:   48
c ---[  73]---> BDD-cost:  191
c ---[  72]---> BDD-cost:   41
c ---[  71]---> BDD-cost:  170
c ---[  70]---> BDD-cost:   44
c ---[  69]---> BDD-cost:  167
c ---[  68]---> BDD-cost:   50
c ---[  67]---> BDD-cost:  203
c ---[  66]---> BDD-cost:    3
c ---[  65]---> BDD-cost:  194
c ---[  64]---> BDD-cost:   61
c ---[  63]---> BDD-cost:   48
c ---[  62]---> BDD-cost:  191
c ---[  61]---> BDD-cost:   48
c ---[  60]---> BDD-cost:  191
c ---[  59]---> BDD-cost:   55
c ---[  58]---> Sorter-cost:  751     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  57]---> BDD-cost:   47
c ---[  56]---> BDD-cost:  161
c ---[  55]---> BDD-cost:   50
c ---[  54]---> BDD-cost:   48
c ---[  53]---> BDD-cost:  203
c ---[  52]---> BDD-cost:   48
c ---[  51]---> BDD-cost:  191
c ---[  50]---> BDD-cost:    5
c ---[  49]---> BDD-cost:   73
c ---[  48]---> BDD-cost:    5
c ---[  47]---> BDD-cost:   70
c ---[  46]---> BDD-cost:   38
c ---[  45]---> BDD-cost:  161
c ---[  44]---> BDD-cost:   41
c ---[  43]---> BDD-cost:  191
c ---[  42]---> BDD-cost:  158
c ---[  41]---> BDD-cost:   35
c ---[  40]---> BDD-cost:  164
c ---[  39]---> BDD-cost:   35
c ---[  38]---> BDD-cost:  164
c ---[  37]---> BDD-cost:   38
c ---[  36]---> BDD-cost:  161
c ---[  35]---> BDD-cost:    3
c ---[  34]---> BDD-cost:   64
c ---[  33]---> BDD-cost:    6
c ---[  32]---> BDD-cost:   38
c ---[  31]---> BDD-cost:   78
c ---[  30]---> BDD-cost:   41
c ---[  29]---> BDD-cost:  170
c ---[  28]---> BDD-cost:   41
c ---[  27]---> BDD-cost:  170
c ---[  26]---> BDD-cost:   41
c ---[  25]---> BDD-cost:  170
c ---[  24]---> BDD-cost:   48
c ---[  23]---> BDD-cost:  191
c ---[  22]---> BDD-cost:   38
c ---[  21]---> BDD-cost:  173
c ---[  20]---> BDD-cost:  173
c ---[  19]---> BDD-cost:   41
c ---[  18]---> BDD-cost:  170
c ---[  17]---> BDD-cost:    5
c ---[  16]---> BDD-cost:   75
c ---[  15]---> BDD-cost:   38
c ---[  14]---> BDD-cost:  161
c ---[  13]---> BDD-cost:   45
c ---[  12]---> BDD-cost:  182
c ---[  11]---> BDD-cost:   35
c ---[  10]---> BDD-cost:   44
c ---[   9]---> BDD-cost:  164
c ---[   8]---> BDD-cost:   38
c ---[   7]---> BDD-cost:  161
c ---[   6]---> BDD-cost:   43
c ---[   5]---> BDD-cost:  170
c ---[   4]---> BDD-cost:   41
c ---[   3]---> BDD-cost:  158
c ---[   2]---> BDD-cost:    3
c ---[   1]---> BDD-cost:   60
c ---[   0]---> BDD-cost:    3
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  226352   543670 |   67905       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/76417          
c   -- var.elim.:  2000/76417          
c   -- var.elim.:  3000/76417          
c   -- var.elim.:  4000/76417          
c   -- var.elim.:  5000/76417          
c   -- var.elim.:  6000/76417          
c   -- var.elim.:  7000/76417          
c   -- var.elim.:  8000/76417          
c   -- var.elim.:  9000/76417          
c   -- var.elim.:  10000/76417          
c   -- var.elim.:  11000/76417          
c   -- var.elim.:  12000/76417          
c   -- var.elim.:  13000/76417          
c   -- var.elim.:  14000/76417          
c   -- var.elim.:  15000/76417          
c   -- var.elim.:  16000/76417          
c   -- var.elim.:  17000/76417          
c   -- var.elim.:  18000/76417          
c   -- var.elim.:  19000/76417          
c   -- var.elim.:  20000/76417          
c   -- var.elim.:  21000/76417          
c   -- var.elim.:  22000/76417          
c   -- var.elim.:  23000/76417          
c   -- var.elim.:  24000/76417          
c   -- var.elim.:  25000/76417          
c   -- var.elim.:  26000/76417          
c   -- var.elim.:  27000/76417          
c   -- var.elim.:  28000/76417          
c   -- var.elim.:  29000/76417          
c   -- var.elim.:  30000/76417          
c   -- var.elim.:  31000/76417          
c   -- var.elim.:  32000/76417          
c   -- var.elim.:  33000/76417          
c   -- var.elim.:  34000/76417          
c   -- var.elim.:  35000/76417          
c   -- var.elim.:  36000/76417          
c   -- var.elim.:  37000/76417          
c   -- var.elim.:  38000/76417          
c   -- var.elim.:  39000/76417          
c   -- var.elim.:  40000/76417          
c   -- var.elim.:  41000/76417          
c   -- var.elim.:  42000/76417          
c   -- var.elim.:  43000/76417          
c   -- var.elim.:  44000/76417          
c   -- var.elim.:  45000/76417          
c   -- var.elim.:  46000/76417          
c   -- var.elim.:  47000/76417          
c   -- var.elim.:  48000/76417          
c   -- var.elim.:  49000/76417          
c   -- var.elim.:  50000/76417          
c   -- var.elim.:  51000/76417          
c   -- var.elim.:  52000/76417          
c   -- var.elim.:  53000/76417          
c   -- var.elim.:  54000/76417          
c   -- var.elim.:  55000/76417          
c   -- var.elim.:  56000/76417          
c   -- var.elim.:  57000/76417          
c   -- var.elim.:  58000/76417          
c   -- var.elim.:  59000/76417          
c   -- var.elim.:  60000/76417          
c   -- var.elim.:  61000/76417          
c   -- var.elim.:  62000/76417          
c   -- var.elim.:  63000/76417          
c   -- var.elim.:  64000/76417          
c   -- var.elim.:  65000/76417          
c   -- var.elim.:  66000/76417          
c   -- var.elim.:  67000/76417          
c   -- var.elim.:  68000/76417          
c   -- var.elim.:  69000/76417          
c   -- var.elim.:  70000/76417          
c   -- var.elim.:  71000/76417          
c   -- var.elim.:  72000/76417          
c   -- var.elim.:  73000/76417          
c   -- var.elim.:  74000/76417          
c   -- var.elim.:  75000/76417          
c   -- var.elim.:  76000/76417          
c   -- var.elim.:  76417/76417          
c   -- var.elim.:  1000/41915          
c   -- var.elim.:  2000/41915          
c   -- var.elim.:  3000/41915          
c   -- var.elim.:  4000/41915          
c   -- var.elim.:  5000/41915          
c   -- var.elim.:  6000/41915          
c   -- var.elim.:  7000/41915          
c   -- var.elim.:  8000/41915          
c   -- var.elim.:  9000/41915          
c   -- var.elim.:  10000/41915          
c   -- var.elim.:  11000/41915          
c   -- var.elim.:  12000/41915          
c   -- var.elim.:  13000/41915          
c   -- var.elim.:  14000/41915          
c   -- var.elim.:  15000/41915          
c   -- var.elim.:  16000/41915          
c   -- var.elim.:  17000/41915          
c   -- var.elim.:  18000/41915          
c   -- var.elim.:  19000/41915          
c   -- var.elim.:  20000/41915          
c   -- var.elim.:  21000/41915          
c   -- var.elim.:  22000/41915          
c   -- var.elim.:  23000/41915          
c   -- var.elim.:  24000/41915          
c   -- var.elim.:  25000/41915          
c   -- var.elim.:  26000/41915          
c   -- var.elim.:  27000/41915          
c   -- var.elim.:  28000/41915          
c   -- var.elim.:  29000/41915          
c   -- var.elim.:  30000/41915          
c   -- var.elim.:  31000/41915          
c   -- var.elim.:  32000/41915          
c   -- var.elim.:  33000/41915          
c   -- var.elim.:  34000/41915          
c   -- var.elim.:  35000/41915          
c   -- var.elim.:  36000/41915          
c   -- var.elim.:  37000/41915          
c   -- var.elim.:  38000/41915          
c   -- var.elim.:  39000/41915          
c   -- var.elim.:  40000/41915          
c   -- var.elim.:  41000/41915          
c   -- var.elim.:  41915/41915          
c   -- var.elim.:  439/439          
c   -- var.elim.:  221/221          
c   -- var.elim.:  286/286          
c   -- var.elim.:  338/338          
c   -- var.elim.:  299/299          
c   -- var.elim.:  351/351          
c   -- var.elim.:  302/302          
c   -- var.elim.:  176/176          
c   -- var.elim.:  82/82          
c   -- var.elim.:  37/37          
c   -- var.elim.:  20/20          
c   -- var.elim.:  5/5          
c   -- subsuming                       
c   -- var.elim.:  1000/7120          
c   -- var.elim.:  2000/7120          
c   -- var.elim.:  3000/7120          
c   -- var.elim.:  4000/7120          
c   -- var.elim.:  5000/7120          
c   -- var.elim.:  6000/7120          
c   -- var.elim.:  7000/7120          
c   -- var.elim.:  7120/7120          
c   -- var.elim.:  1000/2885          
c   -- var.elim.:  2000/2885          
c   -- var.elim.:  2885/2885          
c   -- var.elim.:  4/4          
c   -- subsuming                       
c   -- var.elim.:  1000/1180          
c   -- var.elim.:  1180/1180          
c   -- var.elim.:  87/87          
c |         0 |  181869   552702 |      --       0       --      -- |     --   | -33569/35725
c |         0 |  181869   552702 |   72747       0        0     nan |  0.000 % |
c |       100 |  181869   552702 |   80022     100      563     5.6 |  8.802 % |
c |       250 |  181779   552378 |   87981     246     1137     4.6 |  8.837 % |
c |       477 |  181638   551876 |   96704     453     1908     4.2 |  8.891 % |
c |       814 |  181475   551310 |  106279     766     3620     4.7 |  8.950 % |
c |      1320 |  181442   551191 |  116885    1270     5818     4.6 |  8.964 % |
c |      2079 |  181275   550609 |  128455    2017     9606     4.8 |  9.027 % |
c |      3218 |  180741   548731 |  140885    3100    14479     4.7 |  9.237 % #### 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.95 0.90 2/54 18806
Raw data (stat): 18806 (runsolver) R 18805 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483208394 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0003 s]
Raw data (loadavg): 0.87 0.95 0.90 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 12579 0 0 0 956 42 0 0 25 0 1 0 483208394 57065472 11942 4294967295 134512640 134672761 3221224544 3221223056 134635961 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13932 11942 603 41 0 13891 0
vsize: 55728
[startup+20.0007 s]
Raw data (loadavg): 0.89 0.95 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13331 0 0 0 1954 44 0 0 25 0 1 0 483208394 56803328 11914 4294967295 134512640 134672761 3221224544 3221223680 134614814 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13868 11914 603 41 0 13827 0
vsize: 55472
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.95 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13349 0 0 0 2954 44 0 0 25 0 1 0 483208394 56803328 11932 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13868 11932 603 41 0 13827 0
vsize: 55472
[startup+40.0017 s]
Raw data (loadavg): 0.92 0.95 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13355 0 0 0 3953 45 0 0 25 0 1 0 483208394 56803328 11938 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13868 11938 603 41 0 13827 0
vsize: 55472
[startup+50.0024 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13394 0 0 0 4953 45 0 0 25 0 1 0 483208394 57065472 11977 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13932 11977 603 41 0 13891 0
vsize: 55728
[startup+60.002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13401 0 0 0 5953 45 0 0 25 0 1 0 483208394 57065472 11984 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13932 11984 603 41 0 13891 0
vsize: 55728
[startup+70.0021 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13436 0 0 0 6953 45 0 0 25 0 1 0 483208394 57196544 11987 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13964 11987 603 41 0 13923 0
vsize: 55856
[startup+80.003 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13444 0 0 0 7954 45 0 0 25 0 1 0 483208394 57196544 11995 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13964 11995 603 41 0 13923 0
vsize: 55856
[startup+90.0025 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13447 0 0 0 8954 45 0 0 25 0 1 0 483208394 57196544 11998 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13964 11998 603 41 0 13923 0
vsize: 55856
[startup+100.004 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13451 0 0 0 9954 45 0 0 25 0 1 0 483208394 57196544 12002 4294967295 134512640 134672761 3221224544 3221223728 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13964 12002 603 41 0 13923 0
vsize: 55856
[startup+110.005 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13456 0 0 0 10954 45 0 0 25 0 1 0 483208394 57196544 12007 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13964 12007 603 41 0 13923 0
vsize: 55856
[startup+120.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13480 0 0 0 11954 45 0 0 25 0 1 0 483208394 57331712 12031 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13997 12031 603 41 0 13956 0
vsize: 55988
[startup+130.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13519 0 0 0 12954 45 0 0 25 0 1 0 483208394 57462784 12070 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14029 12070 603 41 0 13988 0
vsize: 56116
[startup+140.004 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13552 0 0 0 13954 45 0 0 25 0 1 0 483208394 57597952 12103 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14062 12103 603 41 0 14021 0
vsize: 56248
[startup+150.005 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13618 0 0 0 14954 46 0 0 25 0 1 0 483208394 58122240 12169 4294967295 134512640 134672761 3221224544 3221223704 134614557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14190 12169 603 41 0 14149 0
vsize: 56760
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13673 0 0 0 15954 46 0 0 25 0 1 0 483208394 58384384 12224 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14254 12224 603 41 0 14213 0
vsize: 57016
[startup+170.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13763 0 0 0 16954 46 0 0 25 0 1 0 483208394 58650624 12314 4294967295 134512640 134672761 3221224544 3221223744 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14319 12314 603 41 0 14278 0
vsize: 57276
[startup+180.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 13865 0 0 0 17954 46 0 0 25 0 1 0 483208394 59047936 12416 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14416 12416 603 41 0 14375 0
vsize: 57664
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 14189 0 0 0 18954 47 0 0 25 0 1 0 483208394 60379136 12740 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14741 12740 603 41 0 14700 0
vsize: 58964
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 14321 0 0 0 19954 47 0 0 25 0 1 0 483208394 60915712 12872 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14872 12872 603 41 0 14831 0
vsize: 59488
[startup+210.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 14588 0 0 0 20954 48 0 0 25 0 1 0 483208394 61980672 13139 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15132 13139 603 41 0 15091 0
vsize: 60528
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 14817 0 0 0 21953 49 0 0 25 0 1 0 483208394 62918656 13368 4294967295 134512640 134672761 3221224544 3221223728 134615994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15361 13368 603 41 0 15320 0
vsize: 61444
[startup+230.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 14946 0 0 0 22953 49 0 0 25 0 1 0 483208394 63459328 13497 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15493 13497 603 41 0 15452 0
vsize: 61972
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15103 0 0 0 23952 49 0 0 25 0 1 0 483208394 63995904 13654 4294967295 134512640 134672761 3221224544 3221223728 134615638 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15624 13654 603 41 0 15583 0
vsize: 62496
[startup+250.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15199 0 0 0 24952 50 0 0 25 0 1 0 483208394 64393216 13750 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15721 13750 603 41 0 15680 0
vsize: 62884
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15299 0 0 0 25952 50 0 0 25 0 1 0 483208394 64790528 13850 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15818 13850 603 41 0 15777 0
vsize: 63272
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15427 0 0 0 26952 50 0 0 25 0 1 0 483208394 65323008 13978 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15948 13978 603 41 0 15907 0
vsize: 63792
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15549 0 0 0 27952 51 0 0 25 0 1 0 483208394 65851392 14100 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16077 14100 603 41 0 16036 0
vsize: 64308
[startup+290.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15679 0 0 0 28951 51 0 0 25 0 1 0 483208394 66252800 14230 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16175 14230 603 41 0 16134 0
vsize: 64700
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15795 0 0 0 29951 52 0 0 25 0 1 0 483208394 67309568 14346 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16433 14346 603 41 0 16392 0
vsize: 65732
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15893 0 0 0 30951 52 0 0 25 0 1 0 483208394 67706880 14444 4294967295 134512640 134672761 3221224544 3221223728 134615498 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16530 14444 603 41 0 16489 0
vsize: 66120
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 15978 0 0 0 31951 52 0 0 25 0 1 0 483208394 67977216 14529 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16596 14529 603 41 0 16555 0
vsize: 66384
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 16071 0 0 0 32951 53 0 0 25 0 1 0 483208394 68374528 14622 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16693 14622 603 41 0 16652 0
vsize: 66772
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 16267 0 0 0 33951 53 0 0 25 0 1 0 483208394 69169152 14818 4294967295 134512640 134672761 3221224544 3221223688 134616279 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16887 14818 603 41 0 16846 0
vsize: 67548
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 16392 0 0 0 34951 53 0 0 25 0 1 0 483208394 69701632 14943 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17017 14943 603 41 0 16976 0
vsize: 68068
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 16499 0 0 0 35951 53 0 0 25 0 1 0 483208394 70098944 15050 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17114 15050 603 41 0 17073 0
vsize: 68456
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 16603 0 0 0 36951 54 0 0 25 0 1 0 483208394 70500352 15154 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17212 15154 603 41 0 17171 0
vsize: 68848
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 16699 0 0 0 37951 54 0 0 25 0 1 0 483208394 70901760 15250 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17310 15250 603 41 0 17269 0
vsize: 69240
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 16877 0 0 0 38951 54 0 0 25 0 1 0 483208394 71569408 15428 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17473 15428 603 41 0 17432 0
vsize: 69892
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 17011 0 0 0 39950 55 0 0 25 0 1 0 483208394 72105984 15562 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17604 15562 603 41 0 17563 0
vsize: 70416
[startup+410.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 17216 0 0 0 40950 55 0 0 25 0 1 0 483208394 72908800 15767 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17800 15767 603 41 0 17759 0
vsize: 71200
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 17398 0 0 0 41950 55 0 0 25 0 1 0 483208394 73711616 15949 4294967295 134512640 134672761 3221224544 3221223584 134612843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17996 15949 603 41 0 17955 0
vsize: 71984
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 17499 0 0 0 42950 56 0 0 25 0 1 0 483208394 74117120 16050 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18095 16050 603 41 0 18054 0
vsize: 72380
[startup+440.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 18003 0 0 0 43948 58 0 0 25 0 1 0 483208394 76103680 16554 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18580 16554 603 41 0 18539 0
vsize: 74320
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 18372 0 0 0 44947 59 0 0 25 0 1 0 483208394 77557760 16923 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18935 16923 603 41 0 18894 0
vsize: 75740
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 18491 0 0 0 45947 59 0 0 25 0 1 0 483208394 78090240 17042 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19065 17042 603 41 0 19024 0
vsize: 76260
[startup+470.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 18644 0 0 0 46947 59 0 0 25 0 1 0 483208394 78614528 17195 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19193 17195 603 41 0 19152 0
vsize: 76772
[startup+480.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 18784 0 0 0 47946 60 0 0 25 0 1 0 483208394 79286272 17335 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19357 17335 603 41 0 19316 0
vsize: 77428
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 18912 0 0 0 48946 61 0 0 25 0 1 0 483208394 79691776 17463 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19456 17463 603 41 0 19415 0
vsize: 77824
[startup+500.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 19072 0 0 0 49946 61 0 0 25 0 1 0 483208394 80355328 17623 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19618 17623 603 41 0 19577 0
vsize: 78472
[startup+510.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 19202 0 0 0 50946 61 0 0 25 0 1 0 483208394 80887808 17753 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19748 17753 603 41 0 19707 0
vsize: 78992
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 19382 0 0 0 51946 62 0 0 25 0 1 0 483208394 81686528 17933 4294967295 134512640 134672761 3221224544 3221223712 134564722 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19943 17933 603 41 0 19902 0
vsize: 79772
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 19535 0 0 0 52945 62 0 0 25 0 1 0 483208394 82219008 18086 4294967295 134512640 134672761 3221224544 3221223728 134616025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20073 18086 603 41 0 20032 0
vsize: 80292
[startup+540.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 19658 0 0 0 53945 62 0 0 25 0 1 0 483208394 82751488 18209 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20203 18209 603 41 0 20162 0
vsize: 80812
[startup+550.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 19814 0 0 0 54945 63 0 0 25 0 1 0 483208394 83288064 18365 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20334 18365 603 41 0 20293 0
vsize: 81336
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 19950 0 0 0 55945 63 0 0 25 0 1 0 483208394 83943424 18501 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20494 18501 603 41 0 20453 0
vsize: 81976
[startup+570.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 20208 0 0 0 56944 65 0 0 25 0 1 0 483208394 84869120 18759 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20720 18759 603 41 0 20679 0
vsize: 82880
[startup+580.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 20319 0 0 0 57944 65 0 0 25 0 1 0 483208394 85401600 18870 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20850 18870 603 41 0 20809 0
vsize: 83400
[startup+590.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 20481 0 0 0 58943 65 0 0 25 0 1 0 483208394 86065152 19032 4294967295 134512640 134672761 3221224544 3221223704 134614557 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21012 19032 603 41 0 20971 0
vsize: 84048
[startup+600.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 20568 0 0 0 59943 66 0 0 25 0 1 0 483208394 86335488 19119 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21078 19119 603 41 0 21037 0
vsize: 84312
[startup+610.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 20757 0 0 0 60943 66 0 0 25 0 1 0 483208394 87126016 19308 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21271 19308 603 41 0 21230 0
vsize: 85084
[startup+620.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 21376 0 0 0 61941 68 0 0 25 0 1 0 483208394 90685440 19927 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22140 19927 603 41 0 22099 0
vsize: 88560
[startup+630.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 22323 0 0 0 62939 70 0 0 25 0 1 0 483208394 94511104 20874 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23074 20874 603 41 0 23033 0
vsize: 92296
[startup+640.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 23341 0 0 0 63936 73 0 0 25 0 1 0 483208394 98734080 21892 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24105 21892 603 41 0 24064 0
vsize: 96420
[startup+650.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 24225 0 0 0 64935 75 0 0 25 0 1 0 483208394 102305792 22776 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24977 22776 603 41 0 24936 0
vsize: 99908
[startup+660.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 25078 0 0 0 65931 78 0 0 25 0 1 0 483208394 105771008 23629 4294967295 134512640 134672761 3221224544 3221223728 134616011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25823 23629 603 41 0 25782 0
vsize: 103292
[startup+670.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 25740 0 0 0 66929 81 0 0 25 0 1 0 483208394 108425216 24291 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26471 24291 603 41 0 26430 0
vsize: 105884
[startup+680.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 26465 0 0 0 67928 83 0 0 25 0 1 0 483208394 111456256 25016 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27211 25016 603 41 0 27170 0
vsize: 108844
[startup+690.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 26976 0 0 0 68927 84 0 0 25 0 1 0 483208394 113577984 25527 4294967295 134512640 134672761 3221224544 3221223728 134615591 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27729 25527 603 41 0 27688 0
vsize: 110916
[startup+700.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 27143 0 0 0 69926 84 0 0 25 0 1 0 483208394 114241536 25694 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27891 25694 603 41 0 27850 0
vsize: 111564
[startup+710.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 27367 0 0 0 70926 85 0 0 25 0 1 0 483208394 115175424 25918 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28119 25918 603 41 0 28078 0
vsize: 112476
[startup+720.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 27487 0 0 0 71926 85 0 0 25 0 1 0 483208394 115576832 26038 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28217 26038 603 41 0 28176 0
vsize: 112868
[startup+730.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 27645 0 0 0 72926 85 0 0 25 0 1 0 483208394 116248576 26196 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28381 26196 603 41 0 28340 0
vsize: 113524
[startup+740.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 27732 0 0 0 73926 86 0 0 25 0 1 0 483208394 116654080 26283 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28480 26283 603 41 0 28439 0
vsize: 113920
[startup+750.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 28308 0 0 0 74925 87 0 0 25 0 1 0 483208394 118898688 26859 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29028 26859 603 41 0 28987 0
vsize: 116112
[startup+760.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 29089 0 0 0 75922 90 0 0 25 0 1 0 483208394 122085376 27640 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29806 27640 603 41 0 29765 0
vsize: 119224
[startup+770.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 29521 0 0 0 76921 91 0 0 25 0 1 0 483208394 123809792 28072 4294967295 134512640 134672761 3221224544 3221223496 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30227 28072 603 41 0 30186 0
vsize: 120908
[startup+780.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 29872 0 0 0 77920 92 0 0 25 0 1 0 483208394 125276160 28423 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30585 28423 603 41 0 30544 0
vsize: 122340
[startup+790.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 29966 0 0 0 78920 92 0 0 25 0 1 0 483208394 125681664 28517 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30684 28517 603 41 0 30643 0
vsize: 122736
[startup+800.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 30123 0 0 0 79920 93 0 0 25 0 1 0 483208394 126214144 28674 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30814 28674 603 41 0 30773 0
vsize: 123256
[startup+810.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 30327 0 0 0 80920 93 0 0 25 0 1 0 483208394 127008768 28878 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31008 28878 603 41 0 30967 0
vsize: 124032
[startup+820.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 30486 0 0 0 81920 93 0 0 25 0 1 0 483208394 127676416 29037 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31171 29037 603 41 0 31130 0
vsize: 124684
[startup+830.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 30585 0 0 0 82920 94 0 0 25 0 1 0 483208394 128081920 29136 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31270 29136 603 41 0 31229 0
vsize: 125080
[startup+840.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 30777 0 0 0 83919 94 0 0 25 0 1 0 483208394 128876544 29328 4294967295 134512640 134672761 3221224544 3221223728 134615755 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31464 29328 603 41 0 31423 0
vsize: 125856
[startup+850.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 30889 0 0 0 84919 94 0 0 25 0 1 0 483208394 129290240 29440 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31565 29440 603 41 0 31524 0
vsize: 126260
[startup+860.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 31064 0 0 0 85919 95 0 0 25 0 1 0 483208394 130088960 29615 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31760 29615 603 41 0 31719 0
vsize: 127040
[startup+870.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 31228 0 0 0 86919 95 0 0 25 0 1 0 483208394 130617344 29779 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31889 29779 603 41 0 31848 0
vsize: 127556
[startup+880.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 31408 0 0 0 87919 95 0 0 25 0 1 0 483208394 131411968 29959 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32083 29959 603 41 0 32042 0
vsize: 128332
[startup+890.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 31496 0 0 0 88919 95 0 0 25 0 1 0 483208394 131817472 30047 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32182 30047 603 41 0 32141 0
vsize: 128728
[startup+900.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 31815 0 0 0 89918 96 0 0 25 0 1 0 483208394 133013504 30366 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32474 30366 603 41 0 32433 0
vsize: 129896
[startup+910.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 32029 0 0 0 90918 97 0 0 25 0 1 0 483208394 133939200 30580 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32700 30580 603 41 0 32659 0
vsize: 130800
[startup+920.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 32227 0 0 0 91917 97 0 0 25 0 1 0 483208394 134733824 30778 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32894 30778 603 41 0 32853 0
vsize: 131576
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 32365 0 0 0 92917 98 0 0 25 0 1 0 483208394 135270400 30916 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33025 30916 603 41 0 32984 0
vsize: 132100
[startup+940.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 93916 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+950.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 94916 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+960.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 95916 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+970.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 96916 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+980.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 97917 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223680 134614516 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+990.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 98917 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 99917 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 100917 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 101917 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223744 134617686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 102918 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 103918 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 104918 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134616014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 105918 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223668 134566106 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 106918 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 107919 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223744 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 108919 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 109920 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 110921 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 111921 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 112921 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1140.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 113921 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1150.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 114922 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1160.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 115922 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223744 134610661 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1170.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 116922 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1180.05 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 117922 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1190.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 118922 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223680 134614724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18806
Raw data (stat): 18806 (minisat+) R 18805 25285 25284 0 -1 0 33162 0 0 0 119923 99 0 0 25 0 1 0 483208394 137568256 31332 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33586 31332 603 41 0 33545 0
vsize: 134344
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 18806
Raw data (stat): 18806 (minisat+) Z 18805 25285 25284 0 -1 12 33162 0 0 0 119923 106 0 0 25 0 1 0 483208394 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.12
CPU time (s): 1200.29
CPU user time (s): 1199.23
CPU system time (s): 1.06384
CPU usage (%): 100.015
Max. virtual memory (Kb): 134344
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####