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 14985

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc13 THE 2005-04-21 02:20:19 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18772 boxname=wulflinc13 idbench=1444 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fa6454a9831f2da4180d8bfab7c0a21b  /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-pp08aCUTS.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-pp08aCUTS.opb /oldhome/oroussel/tmp/wulflinc13/normalized-mps-v2-13-7-pp08aCUTS.opb
IDLAUNCH: 18772
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.242
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.242
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        813212 kB
Buffers:         32864 kB
Cached:         166132 kB
SwapCached:        176 kB
Active:          34696 kB
Inactive:       167068 kB
HighTotal:      131008 kB
HighFree:        25928 kB
LowTotal:       903652 kB
LowFree:        787284 kB
SwapTotal:     2097136 kB
SwapFree:      2096860 kB
Dirty:               4 kB
Writeback:           0 kB
Mapped:           6808 kB
Slab:            13992 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:22 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 18772 7 1200.22 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 ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  242059   593973 |   80686       0        0     nan |  0.000 % |
c |       101 |  242044   593940 |   88754     100      687     6.9 |  4.761 % |
c |       251 |  241960   593754 |   97630     242     1140     4.7 |  4.791 % |
c |       476 |  241911   593646 |  107393     462     1959     4.2 |  4.808 % |
c |       813 |  241746   593278 |  118132     778     3299     4.2 |  4.868 % |
c |      1319 |  241413   592536 |  129945    1223     4903     4.0 |  4.986 % |
c |      2078 |  240871   591323 |  142940    1902     7544     4.0 |  5.176 % |
c |      3217 |  240055   589506 |  157234    2943    11985     4.1 |  5.466 % |
c |      4925 |  239541   588361 |  172957    4575    19897     4.3 |  5.652 % |
c |      7487 |  238966   587079 |  190253    7054    36369     5.2 |  5.860 % |
c |     11331 |  237500   583795 |  209278   10714    56406     5.3 |  6.378 % |
c |     17098 |  236462   581467 |  230206   16340    89395     5.5 |  6.744 % |
c |     25747 |  235014   578232 |  253227   24803   136636     5.5 |  7.251 % |
c |     38721 |  233303   574378 |  278549   37550   223644     6.0 |  7.868 % |
c |     58182 |  231872   571153 |  306404   56839   366110     6.4 |  8.372 % |
c |     87376 |  231313   569894 |  337045   85971   684401     8.0 |  8.573 % |
c |    131165 |  230744   568607 |  370749  129683  1306941    10.1 |  8.787 % |
c |    196849 |  230387   567794 |  407824  195292  2453751    12.6 |  8.928 % |
c |    295377 |  230330   567667 |  448607  293813  5254920    17.9 |  8.953 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.92 0.98 0.92 2/54 28892
Raw data (stat): 28892 (runsolver) R 28891 30701 30700 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 483214663 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+9.99959 s]
Raw data (loadavg): 0.93 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7315 0 0 0 976 21 0 0 25 0 1 0 483214663 33918976 6976 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8281 6976 603 41 0 8240 0
vsize: 33124
[startup+20.001 s]
Raw data (loadavg): 0.94 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7354 0 0 0 1976 21 0 0 25 0 1 0 483214663 34054144 7015 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8314 7015 603 41 0 8273 0
vsize: 33256
[startup+30.0014 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7422 0 0 0 2976 22 0 0 25 0 1 0 483214663 34369536 7083 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8391 7083 603 41 0 8350 0
vsize: 33564
[startup+40.0015 s]
Raw data (loadavg): 0.95 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7440 0 0 0 3976 22 0 0 25 0 1 0 483214663 34369536 7101 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8391 7101 603 41 0 8350 0
vsize: 33564
[startup+50.0012 s]
Raw data (loadavg): 0.96 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7465 0 0 0 4976 22 0 0 25 0 1 0 483214663 34504704 7126 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8424 7126 603 41 0 8383 0
vsize: 33696
[startup+60.0012 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7507 0 0 0 5976 22 0 0 25 0 1 0 483214663 34635776 7168 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8456 7168 603 41 0 8415 0
vsize: 33824
[startup+70.0018 s]
Raw data (loadavg): 0.97 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7544 0 0 0 6976 22 0 0 25 0 1 0 483214663 34799616 7205 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8496 7205 603 41 0 8455 0
vsize: 33984
[startup+80.0025 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7574 0 0 0 7976 22 0 0 25 0 1 0 483214663 34930688 7235 4294967295 134512640 134672761 3221224544 3221223680 134565119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8528 7235 603 41 0 8487 0
vsize: 34112
[startup+90.0031 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7603 0 0 0 8976 22 0 0 25 0 1 0 483214663 35061760 7264 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8560 7264 603 41 0 8519 0
vsize: 34240
[startup+100.003 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7628 0 0 0 9976 22 0 0 25 0 1 0 483214663 35061760 7289 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8560 7289 603 41 0 8519 0
vsize: 34240
[startup+110.002 s]
Raw data (loadavg): 0.98 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7667 0 0 0 10975 23 0 0 25 0 1 0 483214663 35196928 7328 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8593 7328 603 41 0 8552 0
vsize: 34372
[startup+120.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7696 0 0 0 11976 23 0 0 25 0 1 0 483214663 35332096 7357 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8626 7357 603 41 0 8585 0
vsize: 34504
[startup+130.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7745 0 0 0 12976 23 0 0 25 0 1 0 483214663 35729408 7406 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8723 7406 603 41 0 8682 0
vsize: 34892
[startup+140.003 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7772 0 0 0 13976 23 0 0 25 0 1 0 483214663 35729408 7433 4294967295 134512640 134672761 3221224544 3221223744 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8723 7433 603 41 0 8682 0
vsize: 34892
[startup+150.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7806 0 0 0 14976 23 0 0 25 0 1 0 483214663 35864576 7467 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8756 7467 603 41 0 8715 0
vsize: 35024
[startup+160.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7830 0 0 0 15976 23 0 0 25 0 1 0 483214663 35999744 7491 4294967295 134512640 134672761 3221224544 3221223740 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8789 7491 603 41 0 8748 0
vsize: 35156
[startup+170.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7859 0 0 0 16976 23 0 0 25 0 1 0 483214663 36134912 7520 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8822 7520 603 41 0 8781 0
vsize: 35288
[startup+180.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7893 0 0 0 17976 23 0 0 25 0 1 0 483214663 36270080 7554 4294967295 134512640 134672761 3221224544 3221223712 134561256 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8855 7554 603 41 0 8814 0
vsize: 35420
[startup+190.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7933 0 0 0 18977 23 0 0 25 0 1 0 483214663 36405248 7594 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8888 7594 603 41 0 8847 0
vsize: 35552
[startup+200.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 7973 0 0 0 19977 23 0 0 25 0 1 0 483214663 36536320 7634 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8920 7634 603 41 0 8879 0
vsize: 35680
[startup+210.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8009 0 0 0 20977 23 0 0 25 0 1 0 483214663 36671488 7670 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8953 7670 603 41 0 8912 0
vsize: 35812
[startup+220.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8052 0 0 0 21977 23 0 0 25 0 1 0 483214663 36806656 7713 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8986 7713 603 41 0 8945 0
vsize: 35944
[startup+230.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8091 0 0 0 22977 23 0 0 25 0 1 0 483214663 36937728 7752 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9018 7752 603 41 0 8977 0
vsize: 36072
[startup+240.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8142 0 0 0 23977 24 0 0 25 0 1 0 483214663 37208064 7803 4294967295 134512640 134672761 3221224544 3221223696 134565110 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9084 7803 603 41 0 9043 0
vsize: 36336
[startup+250.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8185 0 0 0 24977 24 0 0 25 0 1 0 483214663 37343232 7846 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9117 7846 603 41 0 9076 0
vsize: 36468
[startup+260.004 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8229 0 0 0 25977 24 0 0 25 0 1 0 483214663 37740544 7890 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9214 7890 603 41 0 9173 0
vsize: 36856
[startup+270.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8278 0 0 0 26977 24 0 0 25 0 1 0 483214663 38002688 7939 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9278 7939 603 41 0 9237 0
vsize: 37112
[startup+280.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8401 0 0 0 27977 25 0 0 25 0 1 0 483214663 38404096 8062 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9376 8062 603 41 0 9335 0
vsize: 37504
[startup+290.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8454 0 0 0 28977 25 0 0 25 0 1 0 483214663 38670336 8115 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9441 8115 603 41 0 9400 0
vsize: 37764
[startup+300.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8502 0 0 0 29977 25 0 0 25 0 1 0 483214663 38801408 8163 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9473 8163 603 41 0 9432 0
vsize: 37892
[startup+310.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8549 0 0 0 30977 25 0 0 25 0 1 0 483214663 39071744 8210 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9539 8210 603 41 0 9498 0
vsize: 38156
[startup+320.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8600 0 0 0 31977 25 0 0 25 0 1 0 483214663 39202816 8261 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9571 8261 603 41 0 9530 0
vsize: 38284
[startup+330.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8652 0 0 0 32977 26 0 0 25 0 1 0 483214663 39337984 8313 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9604 8313 603 41 0 9563 0
vsize: 38416
[startup+340.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8698 0 0 0 33977 26 0 0 25 0 1 0 483214663 39604224 8359 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9669 8359 603 41 0 9628 0
vsize: 38676
[startup+350.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8761 0 0 0 34977 26 0 0 25 0 1 0 483214663 39870464 8422 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9734 8422 603 41 0 9693 0
vsize: 38936
[startup+360.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8827 0 0 0 35977 26 0 0 25 0 1 0 483214663 40140800 8488 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9800 8488 603 41 0 9759 0
vsize: 39200
[startup+370.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8895 0 0 0 36977 26 0 0 25 0 1 0 483214663 40411136 8556 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9866 8556 603 41 0 9825 0
vsize: 39464
[startup+380.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 8951 0 0 0 37977 27 0 0 25 0 1 0 483214663 40546304 8612 4294967295 134512640 134672761 3221224544 3221223744 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9899 8612 603 41 0 9858 0
vsize: 39596
[startup+390.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9003 0 0 0 38976 27 0 0 25 0 1 0 483214663 40812544 8664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9964 8664 603 41 0 9923 0
vsize: 39856
[startup+400.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9105 0 0 0 39976 28 0 0 25 0 1 0 483214663 41213952 8766 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10062 8766 603 41 0 10021 0
vsize: 40248
[startup+410.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9266 0 0 0 40976 28 0 0 25 0 1 0 483214663 41750528 8927 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10193 8927 603 41 0 10152 0
vsize: 40772
[startup+420.005 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9326 0 0 0 41976 28 0 0 25 0 1 0 483214663 42012672 8987 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10257 8987 603 41 0 10216 0
vsize: 41028
[startup+430.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9419 0 0 0 42976 28 0 0 25 0 1 0 483214663 42418176 9080 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10356 9080 603 41 0 10315 0
vsize: 41424
[startup+440.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9474 0 0 0 43976 29 0 0 25 0 1 0 483214663 42684416 9135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10421 9135 603 41 0 10380 0
vsize: 41684
[startup+450.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9530 0 0 0 44976 29 0 0 25 0 1 0 483214663 42815488 9191 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10453 9191 603 41 0 10412 0
vsize: 41812
[startup+460.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9663 0 0 0 45976 29 0 0 25 0 1 0 483214663 43356160 9324 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10585 9324 603 41 0 10544 0
vsize: 42340
[startup+470.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9727 0 0 0 46975 30 0 0 25 0 1 0 483214663 44146688 9388 4294967295 134512640 134672761 3221224544 3221223696 134565073 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10778 9388 603 41 0 10737 0
vsize: 43112
[startup+480.006 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9828 0 0 0 47975 30 0 0 25 0 1 0 483214663 44548096 9489 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10876 9489 603 41 0 10835 0
vsize: 43504
[startup+490.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 9947 0 0 0 48974 31 0 0 25 0 1 0 483214663 44949504 9608 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10974 9608 603 41 0 10933 0
vsize: 43896
[startup+500.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10019 0 0 0 49974 31 0 0 25 0 1 0 483214663 45350912 9680 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11072 9680 603 41 0 11031 0
vsize: 44288
[startup+510.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10074 0 0 0 50974 31 0 0 25 0 1 0 483214663 45481984 9735 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11104 9735 603 41 0 11063 0
vsize: 44416
[startup+520.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10148 0 0 0 51975 31 0 0 25 0 1 0 483214663 45744128 9809 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11168 9809 603 41 0 11127 0
vsize: 44672
[startup+530.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10212 0 0 0 52975 31 0 0 25 0 1 0 483214663 46010368 9873 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11233 9873 603 41 0 11192 0
vsize: 44932
[startup+540.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10366 0 0 0 53974 32 0 0 25 0 1 0 483214663 46686208 10027 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11398 10027 603 41 0 11357 0
vsize: 45592
[startup+550.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10524 0 0 0 54974 32 0 0 25 0 1 0 483214663 47357952 10185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11562 10185 603 41 0 11521 0
vsize: 46248
[startup+560.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10601 0 0 0 55974 32 0 0 25 0 1 0 483214663 47624192 10262 4294967295 134512640 134672761 3221224544 3221223696 134565064 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11627 10262 603 41 0 11586 0
vsize: 46508
[startup+570.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10700 0 0 0 56974 33 0 0 25 0 1 0 483214663 48029696 10361 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11726 10361 603 41 0 11685 0
vsize: 46904
[startup+580.007 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10765 0 0 0 57974 33 0 0 25 0 1 0 483214663 48300032 10426 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11792 10426 603 41 0 11751 0
vsize: 47168
[startup+590.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10816 0 0 0 58974 33 0 0 25 0 1 0 483214663 48435200 10477 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11825 10477 603 41 0 11784 0
vsize: 47300
[startup+600.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10881 0 0 0 59974 33 0 0 25 0 1 0 483214663 48705536 10542 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11891 10542 603 41 0 11850 0
vsize: 47564
[startup+610.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 10964 0 0 0 60975 33 0 0 25 0 1 0 483214663 48967680 10625 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11955 10625 603 41 0 11914 0
vsize: 47820
[startup+620.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 11064 0 0 0 61975 33 0 0 25 0 1 0 483214663 49369088 10725 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12053 10725 603 41 0 12012 0
vsize: 48212
[startup+630.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 11162 0 0 0 62975 33 0 0 25 0 1 0 483214663 49774592 10823 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12152 10823 603 41 0 12111 0
vsize: 48608
[startup+640.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 11286 0 0 0 63975 33 0 0 25 0 1 0 483214663 50315264 10947 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12284 10947 603 41 0 12243 0
vsize: 49136
[startup+650.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 11375 0 0 0 64974 34 0 0 25 0 1 0 483214663 50585600 11036 4294967295 134512640 134672761 3221224544 3221223712 134565153 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12350 11036 603 41 0 12309 0
vsize: 49400
[startup+660.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 11577 0 0 0 65974 34 0 0 25 0 1 0 483214663 51511296 11238 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12576 11238 603 41 0 12535 0
vsize: 50304
[startup+670.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 11692 0 0 0 66973 35 0 0 25 0 1 0 483214663 51916800 11353 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12675 11353 603 41 0 12634 0
vsize: 50700
[startup+680.008 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 11775 0 0 0 67973 35 0 0 25 0 1 0 483214663 52187136 11436 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12741 11436 603 41 0 12700 0
vsize: 50964
[startup+690.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 11891 0 0 0 68973 35 0 0 25 0 1 0 483214663 52727808 11552 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12873 11552 603 41 0 12832 0
vsize: 51492
[startup+700.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12010 0 0 0 69972 36 0 0 25 0 1 0 483214663 53133312 11671 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12972 11671 603 41 0 12931 0
vsize: 51888
[startup+710.009 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12102 0 0 0 70972 36 0 0 25 0 1 0 483214663 53530624 11763 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13069 11763 603 41 0 13028 0
vsize: 52276
[startup+720.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12263 0 0 0 71972 37 0 0 25 0 1 0 483214663 54198272 11924 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 11924 603 41 0 13191 0
vsize: 52928
[startup+730.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12345 0 0 0 72972 37 0 0 25 0 1 0 483214663 54468608 12006 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13298 12006 603 41 0 13257 0
vsize: 53192
[startup+740.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12523 0 0 0 73972 37 0 0 25 0 1 0 483214663 55267328 12184 4294967295 134512640 134672761 3221224544 3221223696 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13493 12184 603 41 0 13452 0
vsize: 53972
[startup+750.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12707 0 0 0 74971 38 0 0 25 0 1 0 483214663 55939072 12368 4294967295 134512640 134672761 3221224544 3221223668 134566029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13657 12368 603 41 0 13616 0
vsize: 54628
[startup+760.01 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12788 0 0 0 75971 38 0 0 25 0 1 0 483214663 56209408 12449 4294967295 134512640 134672761 3221224544 3221223684 134566156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13723 12449 603 41 0 13682 0
vsize: 54892
[startup+770.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12906 0 0 0 76971 39 0 0 25 0 1 0 483214663 56741888 12567 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13853 12567 603 41 0 13812 0
vsize: 55412
[startup+780.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 12986 0 0 0 77971 39 0 0 25 0 1 0 483214663 57008128 12647 4294967295 134512640 134672761 3221224544 3221223700 134564777 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13918 12647 603 41 0 13877 0
vsize: 55672
[startup+790.011 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 13074 0 0 0 78971 39 0 0 25 0 1 0 483214663 57413632 12735 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14017 12735 603 41 0 13976 0
vsize: 56068
[startup+800.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 13295 0 0 0 79970 40 0 0 25 0 1 0 483214663 58351616 12956 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14246 12956 603 41 0 14205 0
vsize: 56984
[startup+810.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 13424 0 0 0 80970 40 0 0 25 0 1 0 483214663 58753024 13085 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14344 13085 603 41 0 14303 0
vsize: 57376
[startup+820.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 13579 0 0 0 81970 41 0 0 25 0 1 0 483214663 59420672 13240 4294967295 134512640 134672761 3221224544 3221223712 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14507 13240 603 41 0 14466 0
vsize: 58028
[startup+830.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 13720 0 0 0 82970 41 0 0 25 0 1 0 483214663 59957248 13381 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14638 13381 603 41 0 14597 0
vsize: 58552
[startup+840.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 13924 0 0 0 83970 41 0 0 25 0 1 0 483214663 61812736 13585 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15091 13585 603 41 0 15050 0
vsize: 60364
[startup+850.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 14062 0 0 0 84969 42 0 0 25 0 1 0 483214663 62353408 13723 4294967295 134512640 134672761 3221224544 3221223680 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15223 13723 603 41 0 15182 0
vsize: 60892
[startup+860.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 14155 0 0 0 85969 42 0 0 25 0 1 0 483214663 62754816 13816 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15321 13816 603 41 0 15280 0
vsize: 61284
[startup+870.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 14520 0 0 0 86967 44 0 0 25 0 1 0 483214663 64233472 14181 4294967295 134512640 134672761 3221224544 3221223712 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15682 14181 603 41 0 15641 0
vsize: 62728
[startup+880.012 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 14844 0 0 0 87966 45 0 0 25 0 1 0 483214663 65585152 14505 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16012 14505 603 41 0 15971 0
vsize: 64048
[startup+890.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 15356 0 0 0 88965 46 0 0 25 0 1 0 483214663 67588096 15017 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16501 15017 603 41 0 16460 0
vsize: 66004
[startup+900.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 15471 0 0 0 89964 47 0 0 25 0 1 0 483214663 68128768 15132 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16633 15132 603 41 0 16592 0
vsize: 66532
[startup+910.013 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 15649 0 0 0 90964 47 0 0 25 0 1 0 483214663 68800512 15310 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16797 15310 603 41 0 16756 0
vsize: 67188
[startup+920.014 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 15898 0 0 0 91963 48 0 0 25 0 1 0 483214663 69738496 15559 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17026 15559 603 41 0 16985 0
vsize: 68104
[startup+930.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 16112 0 0 0 92963 48 0 0 25 0 1 0 483214663 70680576 15773 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17256 15773 603 41 0 17215 0
vsize: 69024
[startup+940.015 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 16297 0 0 0 93963 48 0 0 25 0 1 0 483214663 71348224 15958 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17419 15958 603 41 0 17378 0
vsize: 69676
[startup+950.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 16562 0 0 0 94962 49 0 0 25 0 1 0 483214663 72417280 16223 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17680 16223 603 41 0 17639 0
vsize: 70720
[startup+960.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 16704 0 0 0 95962 50 0 0 25 0 1 0 483214663 72953856 16365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17811 16365 603 41 0 17770 0
vsize: 71244
[startup+970.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 16812 0 0 0 96962 50 0 0 25 0 1 0 483214663 73355264 16473 4294967295 134512640 134672761 3221224544 3221223712 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17909 16473 603 41 0 17868 0
vsize: 71636
[startup+980.016 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 17113 0 0 0 97961 51 0 0 25 0 1 0 483214663 74686464 16774 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18234 16774 603 41 0 18193 0
vsize: 72936
[startup+990.017 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 17388 0 0 0 98961 52 0 0 25 0 1 0 483214663 75751424 17049 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18494 17049 603 41 0 18453 0
vsize: 73976
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 17882 0 0 0 99959 53 0 0 25 0 1 0 483214663 77770752 17543 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18987 17543 603 41 0 18946 0
vsize: 75948
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 18167 0 0 0 100958 54 0 0 25 0 1 0 483214663 78831616 17828 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19246 17828 603 41 0 19205 0
vsize: 76984
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 18254 0 0 0 101958 55 0 0 25 0 1 0 483214663 79233024 17915 4294967295 134512640 134672761 3221224544 3221223680 134565121 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19344 17915 603 41 0 19303 0
vsize: 77376
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 18422 0 0 0 102958 55 0 0 25 0 1 0 483214663 79908864 18083 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19509 18083 603 41 0 19468 0
vsize: 78036
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 18529 0 0 0 103958 55 0 0 25 0 1 0 483214663 80314368 18190 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19608 18190 603 41 0 19567 0
vsize: 78432
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 18638 0 0 0 104958 55 0 0 25 0 1 0 483214663 80715776 18299 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19706 18299 603 41 0 19665 0
vsize: 78824
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 18888 0 0 0 105958 56 0 0 25 0 1 0 483214663 81788928 18549 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19968 18549 603 41 0 19927 0
vsize: 79872
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 18976 0 0 0 106958 56 0 0 25 0 1 0 483214663 82051072 18637 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20032 18637 603 41 0 19991 0
vsize: 80128
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19063 0 0 0 107958 56 0 0 25 0 1 0 483214663 82452480 18724 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20130 18724 603 41 0 20089 0
vsize: 80520
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19202 0 0 0 108958 57 0 0 25 0 1 0 483214663 82989056 18863 4294967295 134512640 134672761 3221224544 3221223640 1075347141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20261 18863 603 41 0 20220 0
vsize: 81044
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19275 0 0 0 109957 57 0 0 25 0 1 0 483214663 83255296 18936 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20326 18936 603 41 0 20285 0
vsize: 81304
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19341 0 0 0 110958 57 0 0 25 0 1 0 483214663 83525632 19002 4294967295 134512640 134672761 3221224544 3221223744 134557913 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20392 19002 603 41 0 20351 0
vsize: 81568
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19409 0 0 0 111958 57 0 0 25 0 1 0 483214663 83795968 19070 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20458 19070 603 41 0 20417 0
vsize: 81832
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19544 0 0 0 112958 58 0 0 25 0 1 0 483214663 84328448 19205 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20588 19205 603 41 0 20547 0
vsize: 82352
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19629 0 0 0 113957 58 0 0 25 0 1 0 483214663 84729856 19290 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20686 19290 603 41 0 20645 0
vsize: 82744
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19778 0 0 0 114957 59 0 0 25 0 1 0 483214663 85266432 19439 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20817 19439 603 41 0 20776 0
vsize: 83268
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 19945 0 0 0 115957 59 0 0 25 0 1 0 483214663 85938176 19606 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20981 19606 603 41 0 20940 0
vsize: 83924
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 20139 0 0 0 116956 60 0 0 25 0 1 0 483214663 86736896 19800 4294967295 134512640 134672761 3221224544 3221223648 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21176 19800 603 41 0 21135 0
vsize: 84704
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 20232 0 0 0 117956 60 0 0 25 0 1 0 483214663 87138304 19893 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21274 19893 603 41 0 21233 0
vsize: 85096
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 20355 0 0 0 118956 61 0 0 25 0 1 0 483214663 87670784 20016 4294967295 134512640 134672761 3221224544 3221223648 134560364 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21404 20016 603 41 0 21363 0
vsize: 85616
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.98 0.92 2/54 28892
Raw data (stat): 28892 (minisat+) R 28891 30701 30700 0 -1 0 20551 0 0 0 119955 62 0 0 25 0 1 0 483214663 88342528 20212 4294967295 134512640 134672761 3221224544 3221223728 134559581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21568 20212 603 41 0 21527 0
vsize: 86272
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.98 0.92 1/54 28892
Raw data (stat): 28892 (minisat+) Z 28891 30701 30700 0 -1 12 20553 0 0 0 119955 66 0 0 25 0 1 0 483214663 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.06
CPU time (s): 1200.22
CPU user time (s): 1199.55
CPU system time (s): 0.660899
CPU usage (%): 100.013
Max. virtual memory (Kb): 86272
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####