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/miplib/normalized-mps-v2-13-7-dcmulti.opb
MD5SUM	6ffc4ed72f4dd993b121ae0a2045731e
Bench Category	optimization, big integers (OPTBIGINT)
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	9505
Biggest coefficient in the objective function	697303040
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	66656504525
Number of bits of the sum of numbers in the objective function	36
Biggest number in a constraint	697303040
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	66656504525
Number of bits of the biggest sum of numbers	36
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.087986
Number of variables	9535
Total number of constraints	365
Number of constraints which are clauses	27
Number of constraints which are cardinality constraints (but not clauses)	80
Number of constraints which are nor clauses,nor cardinality constraints	258
Minimum length of a constraint	1
Maximum length of a constraint	280
Trace number 15719

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc11 THE 2005-04-21 05:40:37 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16762 boxname=wulflinc11 idbench=1290 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  6ffc4ed72f4dd993b121ae0a2045731e  /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-dcmulti.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc11/normalized-mps-v2-13-7-dcmulti.opb
IDLAUNCH: 16762
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.028
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.028
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:        836832 kB
Buffers:         27220 kB
Cached:         149580 kB
SwapCached:          0 kB
Active:          77812 kB
Inactive:       101776 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        836580 kB
SwapTotal:     2097136 kB
SwapFree:      2097048 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6816 kB
Slab:            12576 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 06:00:39 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 16762 7 1200.36 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 368 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss
c ---[ 427]---> BDD-cost:   14
c ---[ 426]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> BDD-cost:   15
c ---[ 421]---> BDD-cost:   14
c ---[ 420]---> BDD-cost:   14
c ---[ 419]---> BDD-cost:   13
c ---[ 418]---> BDD-cost:   14
c ---[ 416]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 415]---> BDD-cost:   14
c ---[ 413]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 411]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 409]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 407]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 405]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 403]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 401]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 399]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 397]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 395]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> BDD-cost:   13
c ---[ 392]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   16
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:   15
c ---[ 388]---> BDD-cost:    4
c ---[ 386]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> BDD-cost:   24
c ---[ 384]---> BDD-cost:    6
c ---[ 381]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> BDD-cost:   14
c ---[ 378]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> BDD-cost:   16
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:   15
c ---[ 374]---> BDD-cost:    4
c ---[ 372]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> BDD-cost:   23
c ---[ 370]---> BDD-cost:    8
c ---[ 367]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 363]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> BDD-cost:   15
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   14
c ---[ 359]---> BDD-cost:    3
c ---[ 357]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> BDD-cost:   23
c ---[ 355]---> BDD-cost:    6
c ---[ 352]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 348]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> BDD-cost:   16
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:   15
c ---[ 344]---> BDD-cost:    4
c ---[ 342]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> BDD-cost:   24
c ---[ 340]---> BDD-cost:    6
c ---[ 337]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 333]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:   15
c ---[ 329]---> BDD-cost:    4
c ---[ 327]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> BDD-cost:   19
c ---[ 322]---> BDD-cost:   33
c ---[ 320]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 308]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 296]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 293]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> BDD-cost:   15
c ---[ 285]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 282]---> BDD-cost:   14
c ---[ 281]---> BDD-cost:   14
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   14
c ---[ 277]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 275]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 273]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 271]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 269]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 267]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 265]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 263]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 261]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 259]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 257]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 255]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:    4
c ---[ 247]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 245]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> BDD-cost:   24
c ---[ 243]---> BDD-cost:    6
c ---[ 240]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:    7
c ---[ 235]---> BDD-cost:   15
c ---[ 234]---> BDD-cost:    4
c ---[ 232]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 230]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> BDD-cost:   23
c ---[ 228]---> BDD-cost:    8
c ---[ 225]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> BDD-cost:   15
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:   14
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:    6
c ---[ 210]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 208]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> BDD-cost:   16
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:   15
c ---[ 204]---> BDD-cost:    4
c ---[ 202]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> BDD-cost:   24
c ---[ 198]---> BDD-cost:    6
c ---[ 195]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> BDD-cost:   16
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:    4
c ---[ 188]---> BDD-cost:   16
c ---[ 186]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:    7
c ---[ 164]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    4
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> BDD-cost:   24
c ---[ 146]---> BDD-cost:    6
c ---[ 143]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> BDD-cost:   16
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:    4
c ---[ 136]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:    8
c ---[ 129]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:   14
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:    6
c ---[ 115]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:    7
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:    4
c ---[ 108]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:    6
c ---[ 101]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> BDD-cost:   16
c ---[  97]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:    4
c ---[  94]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   33
c ---[  70]---> BDD-cost:   15
c ---[  62]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> BDD-cost:   12
c ---[  58]---> BDD-cost:    5
c ---[  57]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  847     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  862     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> Sorter-cost:  714     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  773     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  773     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  834     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> BDD-cost:   12
c ---[  38]---> BDD-cost:    5
c ---[  37]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  798     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  714     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> BDD-cost:    5
c ---[  18]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> BDD-cost:   12
c ---[  16]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  860     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  704     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  650     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  798     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  660     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  333790   886289 |  111263       0        0     nan |  0.000 % |
c |       100 |  333689   886069 |  122389      82      264     3.2 |  4.481 % |
c |       250 |  333597   885869 |  134628     210      689     3.3 |  4.507 % |
c |       475 |  333435   885515 |  148091     408     1295     3.2 |  4.555 % |
c |       812 |  333059   884679 |  162900     700     2234     3.2 |  4.662 % |
c |      1318 |  332410   883226 |  179190    1143     3825     3.3 |  4.838 % |
c |      2077 |  331562   881336 |  197109    1802     6121     3.4 |  5.075 % |
c |      3216 |  330950   879975 |  216820    2845     9983     3.5 |  5.238 % |
c |      4924 |  329404   876535 |  238502    4329    15698     3.6 |  5.665 % |
c |      7486 |  328443   874392 |  262352    6713    48826     7.3 |  5.924 % |
c |     11330 |  326869   870869 |  288587   10302    92482     9.0 |  6.350 % |
c |     17097 |  325584   867960 |  317446   15919   219879    13.8 |  6.707 % |
c |     25747 |  324551   865655 |  349190   24424   431973    17.7 |  6.984 % |
c |     38721 |  323989   864389 |  384110   37319   890114    23.9 |  7.138 % |
c |     58186 |  323535   863367 |  422521   56730  1652421    29.1 |  7.264 % |
c |     87378 |  322070   860086 |  464773   85698  2899355    33.8 |  7.675 % |
c |    131168 |  320907   857454 |  511250  129348  4534053    35.1 |  7.995 % |
c |    196852 |  319545   854363 |  562375  194804  7383330    37.9 |  8.366 % |
c |    295380 |  318648   852328 |  618613  293155 11490253    39.2 |  8.620 % |
c |    443173 |  317986   850831 |  680474  440861 18651400    42.3 |  8.807 % |
#### 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.75 0.87 0.89 2/54 28798
Raw data (stat): 28798 (runsolver) R 28797 32461 32460 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 484409906 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 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.0013 s]
Raw data (loadavg): 0.79 0.87 0.89 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 9646 0 0 0 976 22 0 0 25 0 1 0 484409906 41910272 9251 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10232 9251 603 41 0 10191 0
vsize: 40928
[startup+20.0016 s]
Raw data (loadavg): 0.82 0.88 0.89 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 9678 0 0 0 1976 22 0 0 25 0 1 0 484409906 42045440 9283 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10265 9283 603 41 0 10224 0
vsize: 41060
[startup+30.0018 s]
Raw data (loadavg): 0.85 0.88 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 9721 0 0 0 2976 23 0 0 25 0 1 0 484409906 42180608 9326 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10298 9326 603 41 0 10257 0
vsize: 41192
[startup+40.0021 s]
Raw data (loadavg): 0.87 0.88 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 9757 0 0 0 3975 23 0 0 25 0 1 0 484409906 42180608 9362 4294967295 134512640 134672761 3221224624 3221223748 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10298 9362 603 41 0 10257 0
vsize: 41192
[startup+50.0023 s]
Raw data (loadavg): 0.89 0.89 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 9817 0 0 0 4975 24 0 0 25 0 1 0 484409906 42446848 9422 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10363 9422 603 41 0 10322 0
vsize: 41452
[startup+60.003 s]
Raw data (loadavg): 0.91 0.89 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 9884 0 0 0 5975 24 0 0 25 0 1 0 484409906 42717184 9489 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10429 9489 603 41 0 10388 0
vsize: 41716
[startup+70.0034 s]
Raw data (loadavg): 0.92 0.89 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 9999 0 0 0 6975 24 0 0 25 0 1 0 484409906 43253760 9604 4294967295 134512640 134672761 3221224624 3221223748 134566080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10560 9604 603 41 0 10519 0
vsize: 42240
[startup+80.0035 s]
Raw data (loadavg): 0.93 0.90 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 10196 0 0 0 7975 24 0 0 25 0 1 0 484409906 43974656 9801 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10736 9801 603 41 0 10695 0
vsize: 42944
[startup+90.0043 s]
Raw data (loadavg): 0.94 0.90 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 10362 0 0 0 8974 25 0 0 25 0 1 0 484409906 44650496 9967 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10901 9967 603 41 0 10860 0
vsize: 43604
[startup+100.004 s]
Raw data (loadavg): 0.95 0.90 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 10746 0 0 0 9973 27 0 0 25 0 1 0 484409906 46387200 10351 4294967295 134512640 134672761 3221224624 3221223804 134556674 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11325 10351 603 41 0 11284 0
vsize: 45300
[startup+110.005 s]
Raw data (loadavg): 0.96 0.90 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 11041 0 0 0 10972 27 0 0 25 0 1 0 484409906 47591424 10646 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 10646 603 41 0 11578 0
vsize: 46476
[startup+120.006 s]
Raw data (loadavg): 0.96 0.91 0.90 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 11451 0 0 0 11972 28 0 0 25 0 1 0 484409906 49197056 11056 4294967295 134512640 134672761 3221224624 3221223808 134559385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12011 11056 603 41 0 11970 0
vsize: 48044
[startup+130.005 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 11910 0 0 0 12970 30 0 0 25 0 1 0 484409906 51052544 11515 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12464 11515 603 41 0 12423 0
vsize: 49856
[startup+140.005 s]
Raw data (loadavg): 0.97 0.91 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 12235 0 0 0 13970 30 0 0 25 0 1 0 484409906 52387840 11840 4294967295 134512640 134672761 3221224624 3221223796 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12790 11840 603 41 0 12749 0
vsize: 51160
[startup+150.006 s]
Raw data (loadavg): 0.98 0.91 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 12684 0 0 0 14969 32 0 0 25 0 1 0 484409906 54394880 12289 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13280 12289 603 41 0 13239 0
vsize: 53120
[startup+160.006 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 12985 0 0 0 15968 33 0 0 25 0 1 0 484409906 55603200 12590 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13575 12590 603 41 0 13534 0
vsize: 54300
[startup+170.007 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 13089 0 0 0 16968 33 0 0 25 0 1 0 484409906 56008704 12694 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13674 12694 603 41 0 13633 0
vsize: 54696
[startup+180.006 s]
Raw data (loadavg): 0.98 0.92 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 13349 0 0 0 17968 34 0 0 25 0 1 0 484409906 57069568 12954 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13933 12954 603 41 0 13892 0
vsize: 55732
[startup+190.007 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 13498 0 0 0 18968 34 0 0 25 0 1 0 484409906 57733120 13103 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14095 13103 603 41 0 14054 0
vsize: 56380
[startup+200.007 s]
Raw data (loadavg): 0.99 0.92 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 13781 0 0 0 19967 34 0 0 25 0 1 0 484409906 58793984 13386 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14354 13386 603 41 0 14313 0
vsize: 57416
[startup+210.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 13909 0 0 0 20967 35 0 0 25 0 1 0 484409906 59318272 13514 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14482 13514 603 41 0 14441 0
vsize: 57928
[startup+220.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 14141 0 0 0 21966 36 0 0 25 0 1 0 484409906 60256256 13746 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14711 13746 603 41 0 14670 0
vsize: 58844
[startup+230.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 14561 0 0 0 22965 38 0 0 25 0 1 0 484409906 61997056 14166 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15136 14166 603 41 0 15095 0
vsize: 60544
[startup+240.009 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 14882 0 0 0 23964 38 0 0 25 0 1 0 484409906 63213568 14487 4294967295 134512640 134672761 3221224624 3221223792 134560833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15433 14487 603 41 0 15392 0
vsize: 61732
[startup+250.008 s]
Raw data (loadavg): 0.99 0.93 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 15203 0 0 0 24963 39 0 0 25 0 1 0 484409906 64552960 14808 4294967295 134512640 134672761 3221224624 3221223792 134561385 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15760 14808 603 41 0 15719 0
vsize: 63040
[startup+260.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 15414 0 0 0 25963 39 0 0 25 0 1 0 484409906 65359872 15019 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15957 15019 603 41 0 15916 0
vsize: 63828
[startup+270.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 15769 0 0 0 26962 41 0 0 25 0 1 0 484409906 67346432 15374 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16442 15374 603 41 0 16401 0
vsize: 65768
[startup+280.009 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 16234 0 0 0 27960 43 0 0 25 0 1 0 484409906 69222400 15839 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16900 15839 603 41 0 16859 0
vsize: 67600
[startup+290.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 16667 0 0 0 28959 44 0 0 25 0 1 0 484409906 70967296 16272 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17326 16272 603 41 0 17285 0
vsize: 69304
[startup+300.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 16989 0 0 0 29958 45 0 0 25 0 1 0 484409906 72306688 16594 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17653 16594 603 41 0 17612 0
vsize: 70612
[startup+310.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 17295 0 0 0 30957 47 0 0 25 0 1 0 484409906 73515008 16900 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17948 16900 603 41 0 17907 0
vsize: 71792
[startup+320.01 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 17511 0 0 0 31957 47 0 0 25 0 1 0 484409906 74317824 17116 4294967295 134512640 134672761 3221224624 3221223824 134557809 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18144 17116 603 41 0 18103 0
vsize: 72576
[startup+330.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 17727 0 0 0 32956 48 0 0 25 0 1 0 484409906 75259904 17332 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18374 17332 603 41 0 18333 0
vsize: 73496
[startup+340.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 17995 0 0 0 33955 49 0 0 25 0 1 0 484409906 76324864 17600 4294967295 134512640 134672761 3221224624 3221223728 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18634 17600 603 41 0 18593 0
vsize: 74536
[startup+350.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 18271 0 0 0 34955 50 0 0 25 0 1 0 484409906 77385728 17876 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18893 17876 603 41 0 18852 0
vsize: 75572
[startup+360.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 18384 0 0 0 35955 50 0 0 25 0 1 0 484409906 77918208 17989 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19023 17989 603 41 0 18982 0
vsize: 76092
[startup+370.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 18636 0 0 0 36954 50 0 0 25 0 1 0 484409906 78856192 18241 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19252 18241 603 41 0 19211 0
vsize: 77008
[startup+380.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 19032 0 0 0 37954 51 0 0 25 0 1 0 484409906 80461824 18637 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19644 18637 603 41 0 19603 0
vsize: 78576
[startup+390.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 19326 0 0 0 38952 52 0 0 25 0 1 0 484409906 81661952 18931 4294967295 134512640 134672761 3221224624 3221223792 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19937 18931 603 41 0 19896 0
vsize: 79748
[startup+400.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 19702 0 0 0 39951 54 0 0 25 0 1 0 484409906 83140608 19307 4294967295 134512640 134672761 3221224624 3221223792 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20298 19307 603 41 0 20257 0
vsize: 81192
[startup+410.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 19977 0 0 0 40950 55 0 0 25 0 1 0 484409906 84213760 19582 4294967295 134512640 134672761 3221224624 3221223760 134565119 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20560 19582 603 41 0 20519 0
vsize: 82240
[startup+420.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 20224 0 0 0 41949 55 0 0 25 0 1 0 484409906 85282816 19829 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20821 19829 603 41 0 20780 0
vsize: 83284
[startup+430.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 20604 0 0 0 42948 56 0 0 25 0 1 0 484409906 86761472 20209 4294967295 134512640 134672761 3221224624 3221223792 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21182 20209 603 41 0 21141 0
vsize: 84728
[startup+440.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 20966 0 0 0 43947 58 0 0 25 0 1 0 484409906 88236032 20571 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21542 20571 603 41 0 21501 0
vsize: 86168
[startup+450.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 21170 0 0 0 44946 59 0 0 25 0 1 0 484409906 89059328 20775 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21743 20775 603 41 0 21702 0
vsize: 86972
[startup+460.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 21311 0 0 0 45946 60 0 0 25 0 1 0 484409906 89595904 20916 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21874 20916 603 41 0 21833 0
vsize: 87496
[startup+470.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 21677 0 0 0 46944 61 0 0 25 0 1 0 484409906 91082752 21282 4294967295 134512640 134672761 3221224624 3221223728 134560402 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22237 21282 603 41 0 22196 0
vsize: 88948
[startup+480.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 21982 0 0 0 47943 63 0 0 25 0 1 0 484409906 92307456 21587 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22536 21587 603 41 0 22495 0
vsize: 90144
[startup+490.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 22263 0 0 0 48943 63 0 0 25 0 1 0 484409906 93519872 21868 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22832 21868 603 41 0 22791 0
vsize: 91328
[startup+500.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 22547 0 0 0 49942 64 0 0 25 0 1 0 484409906 95645696 22152 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23351 22152 603 41 0 23310 0
vsize: 93404
[startup+510.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 22823 0 0 0 50941 65 0 0 25 0 1 0 484409906 96714752 22428 4294967295 134512640 134672761 3221224624 3221223808 134559254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23612 22428 603 41 0 23571 0
vsize: 94448
[startup+520.015 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 23029 0 0 0 51941 65 0 0 25 0 1 0 484409906 97652736 22634 4294967295 134512640 134672761 3221224624 3221223796 134559125 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23841 22634 603 41 0 23800 0
vsize: 95364
[startup+530.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 23286 0 0 0 52941 66 0 0 25 0 1 0 484409906 98594816 22891 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24071 22891 603 41 0 24030 0
vsize: 96284
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 23661 0 0 0 53939 67 0 0 25 0 1 0 484409906 100196352 23266 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24462 23266 603 41 0 24421 0
vsize: 97848
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 23964 0 0 0 54939 68 0 0 25 0 1 0 484409906 101412864 23569 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24759 23569 603 41 0 24718 0
vsize: 99036
[startup+560.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 24236 0 0 0 55938 69 0 0 25 0 1 0 484409906 102469632 23841 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25017 23841 603 41 0 24976 0
vsize: 100068
[startup+570.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 24351 0 0 0 56937 70 0 0 25 0 1 0 484409906 103006208 23956 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25148 23956 603 41 0 25107 0
vsize: 100592
[startup+580.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 24622 0 0 0 57936 71 0 0 25 0 1 0 484409906 104083456 24227 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25411 24227 603 41 0 25370 0
vsize: 101644
[startup+590.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 24928 0 0 0 58935 72 0 0 25 0 1 0 484409906 105283584 24533 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25704 24533 603 41 0 25663 0
vsize: 102816
[startup+600.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 25318 0 0 0 59934 73 0 0 25 0 1 0 484409906 106889216 24923 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26096 24923 603 41 0 26055 0
vsize: 104384
[startup+610.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 25617 0 0 0 60933 74 0 0 25 0 1 0 484409906 108101632 25222 4294967295 134512640 134672761 3221224624 3221223792 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26392 25222 603 41 0 26351 0
vsize: 105568
[startup+620.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 25791 0 0 0 61933 75 0 0 25 0 1 0 484409906 108769280 25396 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26555 25396 603 41 0 26514 0
vsize: 106220
[startup+630.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 26001 0 0 0 62933 75 0 0 25 0 1 0 484409906 109572096 25606 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26751 25606 603 41 0 26710 0
vsize: 107004
[startup+640.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 26289 0 0 0 63932 75 0 0 25 0 1 0 484409906 110776320 25894 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27045 25894 603 41 0 27004 0
vsize: 108180
[startup+650.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 26493 0 0 0 64932 76 0 0 25 0 1 0 484409906 111583232 26098 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27242 26098 603 41 0 27201 0
vsize: 108968
[startup+660.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 26790 0 0 0 65931 77 0 0 25 0 1 0 484409906 112783360 26395 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27535 26395 603 41 0 27494 0
vsize: 110140
[startup+670.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 27114 0 0 0 66930 78 0 0 25 0 1 0 484409906 114118656 26719 4294967295 134512640 134672761 3221224624 3221223748 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27861 26719 603 41 0 27820 0
vsize: 111444
[startup+680.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 27497 0 0 0 67928 80 0 0 25 0 1 0 484409906 115597312 27102 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28222 27102 603 41 0 28181 0
vsize: 112888
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 27692 0 0 0 68928 80 0 0 25 0 1 0 484409906 116404224 27297 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28419 27297 603 41 0 28378 0
vsize: 113676
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 27861 0 0 0 69928 81 0 0 25 0 1 0 484409906 117075968 27466 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28583 27466 603 41 0 28542 0
vsize: 114332
[startup+710.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 28130 0 0 0 70927 82 0 0 25 0 1 0 484409906 118140928 27735 4294967295 134512640 134672761 3221224624 3221223760 134565127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28843 27735 603 41 0 28802 0
vsize: 115372
[startup+720.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 28405 0 0 0 71927 83 0 0 25 0 1 0 484409906 119349248 28010 4294967295 134512640 134672761 3221224624 3221223808 134559332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29138 28010 603 41 0 29097 0
vsize: 116552
[startup+730.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 28721 0 0 0 72926 83 0 0 25 0 1 0 484409906 120557568 28326 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29433 28326 603 41 0 29392 0
vsize: 117732
[startup+740.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 28916 0 0 0 73925 84 0 0 25 0 1 0 484409906 121364480 28521 4294967295 134512640 134672761 3221224624 3221223796 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29630 28521 603 41 0 29589 0
vsize: 118520
[startup+750.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 29210 0 0 0 74925 85 0 0 25 0 1 0 484409906 122572800 28815 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29925 28815 603 41 0 29884 0
vsize: 119700
[startup+760.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 29432 0 0 0 75924 86 0 0 25 0 1 0 484409906 123506688 29037 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30153 29037 603 41 0 30112 0
vsize: 120612
[startup+770.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 29653 0 0 0 76924 86 0 0 25 0 1 0 484409906 124305408 29258 4294967295 134512640 134672761 3221224624 3221223792 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30348 29258 603 41 0 30307 0
vsize: 121392
[startup+780.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 29795 0 0 0 77923 87 0 0 25 0 1 0 484409906 124977152 29400 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30512 29400 603 41 0 30471 0
vsize: 122048
[startup+790.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 30006 0 0 0 78923 87 0 0 25 0 1 0 484409906 125784064 29611 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30709 29611 603 41 0 30668 0
vsize: 122836
[startup+800.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 30268 0 0 0 79923 88 0 0 25 0 1 0 484409906 126857216 29873 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30971 29873 603 41 0 30930 0
vsize: 123884
[startup+810.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 30519 0 0 0 80923 88 0 0 25 0 1 0 484409906 127827968 30124 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31208 30124 603 41 0 31167 0
vsize: 124832
[startup+820.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 30758 0 0 0 81922 89 0 0 25 0 1 0 484409906 128761856 30363 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31436 30363 603 41 0 31395 0
vsize: 125744
[startup+830.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 30930 0 0 0 82922 89 0 0 25 0 1 0 484409906 129568768 30535 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31633 30535 603 41 0 31592 0
vsize: 126532
[startup+840.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 31128 0 0 0 83922 90 0 0 25 0 1 0 484409906 130371584 30733 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31829 30733 603 41 0 31788 0
vsize: 127316
[startup+850.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 31441 0 0 0 84921 91 0 0 25 0 1 0 484409906 131567616 31046 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32121 31046 603 41 0 32080 0
vsize: 128484
[startup+860.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 31772 0 0 0 85920 92 0 0 25 0 1 0 484409906 132915200 31377 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32450 31377 603 41 0 32409 0
vsize: 129800
[startup+870.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 32084 0 0 0 86920 92 0 0 25 0 1 0 484409906 134127616 31689 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32746 31689 603 41 0 32705 0
vsize: 130984
[startup+880.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 32420 0 0 0 87919 93 0 0 25 0 1 0 484409906 135610368 32025 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33108 32025 603 41 0 33067 0
vsize: 132432
[startup+890.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 32650 0 0 0 88918 95 0 0 25 0 1 0 484409906 136564736 32255 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33341 32255 603 41 0 33300 0
vsize: 133364
[startup+900.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 32883 0 0 0 89918 95 0 0 25 0 1 0 484409906 137519104 32488 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33574 32488 603 41 0 33533 0
vsize: 134296
[startup+910.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 33105 0 0 0 90917 96 0 0 25 0 1 0 484409906 138326016 32710 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33771 32710 603 41 0 33730 0
vsize: 135084
[startup+920.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 33252 0 0 0 91915 97 0 0 25 0 1 0 484409906 138997760 32857 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33935 32857 603 41 0 33894 0
vsize: 135740
[startup+930.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 33413 0 0 0 92915 97 0 0 25 0 1 0 484409906 139677696 33018 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34101 33018 603 41 0 34060 0
vsize: 136404
[startup+940.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 33583 0 0 0 93915 98 0 0 25 0 1 0 484409906 140386304 33188 4294967295 134512640 134672761 3221224624 3221223792 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34274 33188 603 41 0 34233 0
vsize: 137096
[startup+950.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 33700 0 0 0 94915 98 0 0 25 0 1 0 484409906 140787712 33305 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34372 33305 603 41 0 34331 0
vsize: 137488
[startup+960.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 34057 0 0 0 95914 99 0 0 25 0 1 0 484409906 142270464 33662 4294967295 134512640 134672761 3221224624 3221223772 134560552 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34734 33662 603 41 0 34693 0
vsize: 138936
[startup+970.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 34311 0 0 0 96913 99 0 0 25 0 1 0 484409906 143204352 33916 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34962 33916 603 41 0 34921 0
vsize: 139848
[startup+980.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 34518 0 0 0 97912 101 0 0 25 0 1 0 484409906 144015360 34123 4294967295 134512640 134672761 3221224624 3221223580 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35160 34123 603 41 0 35119 0
vsize: 140640
[startup+990.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 34643 0 0 0 98912 101 0 0 25 0 1 0 484409906 144556032 34248 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35292 34248 603 41 0 35251 0
vsize: 141168
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 34838 0 0 0 99911 102 0 0 25 0 1 0 484409906 145362944 34443 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35489 34443 603 41 0 35448 0
vsize: 141956
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 35240 0 0 0 100910 103 0 0 25 0 1 0 484409906 146968576 34845 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35881 34845 603 41 0 35840 0
vsize: 143524
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 35577 0 0 0 101910 104 0 0 25 0 1 0 484409906 148312064 35182 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36209 35182 603 41 0 36168 0
vsize: 144836
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 35961 0 0 0 102909 105 0 0 25 0 1 0 484409906 149925888 35566 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36603 35566 603 41 0 36562 0
vsize: 146412
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 36333 0 0 0 103908 106 0 0 25 0 1 0 484409906 151416832 35938 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36967 35938 603 41 0 36926 0
vsize: 147868
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 36488 0 0 0 104908 106 0 0 25 0 1 0 484409906 152084480 36093 4294967295 134512640 134672761 3221224624 3221223808 134559182 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37130 36093 603 41 0 37089 0
vsize: 148520
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 37030 0 0 0 105906 108 0 0 25 0 1 0 484409906 154238976 36635 4294967295 134512640 134672761 3221224624 3221223728 134560260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37656 36635 603 41 0 37615 0
vsize: 150624
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 37557 0 0 0 106905 109 0 0 25 0 1 0 484409906 156364800 37162 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38175 37162 603 41 0 38134 0
vsize: 152700
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 37991 0 0 0 107904 111 0 0 25 0 1 0 484409906 158105600 37596 4294967295 134512640 134672761 3221224624 3221223776 134561249 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38600 37596 603 41 0 38559 0
vsize: 154400
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 38110 0 0 0 108904 111 0 0 25 0 1 0 484409906 158646272 37715 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38732 37715 603 41 0 38691 0
vsize: 154928
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 38311 0 0 0 109903 112 0 0 25 0 1 0 484409906 159449088 37916 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38928 37916 603 41 0 38887 0
vsize: 155712
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 38587 0 0 0 110902 113 0 0 25 0 1 0 484409906 162627584 38192 4294967295 134512640 134672761 3221224624 3221223728 134559966 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39704 38192 603 41 0 39663 0
vsize: 158816
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 38940 0 0 0 111902 113 0 0 25 0 1 0 484409906 164110336 38545 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40066 38545 603 41 0 40025 0
vsize: 160264
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 39085 0 0 0 112902 114 0 0 25 0 1 0 484409906 164659200 38690 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40200 38690 603 41 0 40159 0
vsize: 160800
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 39334 0 0 0 113901 115 0 0 25 0 1 0 484409906 165605376 38939 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40431 38939 603 41 0 40390 0
vsize: 161724
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 39576 0 0 0 114901 115 0 0 25 0 1 0 484409906 166547456 39181 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40661 39181 603 41 0 40620 0
vsize: 162644
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 28798
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 39800 0 0 0 115900 116 0 0 25 0 1 0 484409906 167477248 39405 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40888 39405 603 41 0 40847 0
vsize: 163552
[startup+1170.03 s]
Raw data (loadavg): 1.07 0.99 0.91 2/56 28837
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 40037 0 0 0 116900 116 0 0 25 0 1 0 484409906 168550400 39642 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41150 39642 603 41 0 41109 0
vsize: 164600
[startup+1180.03 s]
Raw data (loadavg): 1.14 1.00 0.92 2/54 28851
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 40273 0 0 0 117899 117 0 0 25 0 1 0 484409906 169476096 39878 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41376 39878 603 41 0 41335 0
vsize: 165504
[startup+1190.14 s]
Raw data (loadavg): 1.11 1.00 0.92 2/54 28851
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 40505 0 0 0 118910 117 0 0 25 0 1 0 484409906 170418176 40110 4294967295 134512640 134672761 3221224624 3221223728 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41606 40110 603 41 0 41565 0
vsize: 166424
[startup+1200.14 s]
Raw data (loadavg): 1.10 1.00 0.92 2/54 28851
Raw data (stat): 28798 (minisat+) R 28797 32461 32460 0 -1 0 40733 0 0 0 119909 118 0 0 25 0 1 0 484409906 171356160 40338 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41835 40338 603 41 0 41794 0
vsize: 167340
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 1.10 1.00 0.92 1/54 28851
Raw data (stat): 28798 (minisat+) Z 28797 32461 32460 0 -1 12 40735 0 0 0 119909 126 0 0 25 0 1 0 484409906 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.22
CPU time (s): 1200.36
CPU user time (s): 1199.09
CPU system time (s): 1.26581
CPU usage (%): 100.012
Max. virtual memory (Kb): 167340
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####