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 19269

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-21 18:34:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16770 boxname=wulflinc31 idbench=1290 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6ffc4ed72f4dd993b121ae0a2045731e  /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-13-7-dcmulti.opb
IDLAUNCH: 16770
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
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	: 3
cpu MHz		: 451.153
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:        848896 kB
Buffers:         30996 kB
Cached:         129056 kB
SwapCached:        632 kB
Active:          15744 kB
Inactive:       146240 kB
HighTotal:      131008 kB
HighFree:        96740 kB
LowTotal:       903652 kB
LowFree:        752156 kB
SwapTotal:     2097892 kB
SwapFree:      2096356 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           5000 kB
Slab:            18084 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 18:54:35 (client local time) WITH STATUS 0 IN 1200.36 SECONDS
stats: 16770 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 |  348337   925039 |  116112       0        0     nan |  0.000 % |
c |       101 |  348197   924727 |  127723      80      247     3.1 |  4.487 % |
c |       251 |  348055   924412 |  140495     198      740     3.7 |  4.526 % |
c |       476 |  347475   923095 |  154545     365     1332     3.6 |  4.685 % |
c |       813 |  347098   922247 |  169999     657     2292     3.5 |  4.787 % |
c |      1319 |  346604   921144 |  186999    1083     3659     3.4 |  4.917 % |
c |      2078 |  345826   919399 |  205699    1748     6013     3.4 |  5.120 % |
c |      3217 |  345162   917906 |  226269    2804     9880     3.5 |  5.291 % |
c |      4925 |  344185   915712 |  248896    4388    17179     3.9 |  5.546 % |
c |      7487 |  343098   913270 |  273786    6808    33527     4.9 |  5.829 % |
c |     11331 |  342488   911888 |  301164   10581    98951     9.4 |  5.989 % |
c |     17097 |  341948   910647 |  331281   16298   237300    14.6 |  6.136 % |
c |     25748 |  341927   910600 |  364409   24947   523755    21.0 |  6.141 % |
c |     38724 |  340887   908244 |  400850   37774  1101211    29.2 |  6.419 % |
c |     58185 |  340320   906957 |  440935   57150  1836228    32.1 |  6.565 % |
c |     87379 |  338351   902516 |  485028   86115  2699853    31.4 |  7.098 % |
c |    131168 |  336463   898242 |  533531  129649  4545889    35.1 |  7.602 % |
c |    196852 |  334648   894103 |  586884  195074  7343806    37.6 |  8.103 % |
c |    295379 |  333606   891753 |  645573  293453 12504450    42.6 |  8.385 % |
c |    443169 |  332288   888676 |  710130  441082 20602089    46.7 |  8.747 % |
#### 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.69 0.88 0.88 2/54 30533
Raw data (stat): 30533 (runsolver) R 30532 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 547263839 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.74 0.89 0.88 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 9689 0 0 0 972 27 0 0 25 0 1 0 547263839 41967616 9294 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10246 9294 603 41 0 10205 0
vsize: 40984
[startup+20.0006 s]
Raw data (loadavg): 0.78 0.89 0.88 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 9709 0 0 0 1972 27 0 0 25 0 1 0 547263839 41967616 9314 4294967295 134512640 134672761 3221224544 3221223728 134558332 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10246 9314 603 41 0 10205 0
vsize: 40984
[startup+30.0049 s]
Raw data (loadavg): 0.81 0.89 0.88 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 9756 0 0 0 2972 27 0 0 25 0 1 0 547263839 42102784 9361 4294967295 134512640 134672761 3221224544 3221223760 134561999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10279 9361 603 41 0 10238 0
vsize: 41116
[startup+40.0054 s]
Raw data (loadavg): 0.84 0.89 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 9798 0 0 0 3971 28 0 0 25 0 1 0 547263839 42237952 9403 4294967295 134512640 134672761 3221224544 3221223736 134556585 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10312 9403 603 41 0 10271 0
vsize: 41248
[startup+50.0053 s]
Raw data (loadavg): 0.86 0.90 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 9827 0 0 0 4970 29 0 0 25 0 1 0 547263839 42369024 9432 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10344 9432 603 41 0 10303 0
vsize: 41376
[startup+60.0058 s]
Raw data (loadavg): 0.88 0.90 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 9962 0 0 0 5970 30 0 0 25 0 1 0 547263839 42917888 9567 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10478 9567 603 41 0 10437 0
vsize: 41912
[startup+70.0063 s]
Raw data (loadavg): 0.90 0.90 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 10284 0 0 0 6969 31 0 0 25 0 1 0 547263839 44285952 9889 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10812 9889 603 41 0 10771 0
vsize: 43248
[startup+80.0071 s]
Raw data (loadavg): 0.92 0.91 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 10739 0 0 0 7967 33 0 0 25 0 1 0 547263839 46166016 10344 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11271 10344 603 41 0 11230 0
vsize: 45084
[startup+90.0076 s]
Raw data (loadavg): 0.93 0.91 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 11036 0 0 0 8966 34 0 0 25 0 1 0 547263839 47505408 10641 4294967295 134512640 134672761 3221224544 3221223648 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11598 10641 603 41 0 11557 0
vsize: 46392
[startup+100.007 s]
Raw data (loadavg): 0.94 0.91 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 11227 0 0 0 9965 35 0 0 25 0 1 0 547263839 48173056 10832 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11761 10832 603 41 0 11720 0
vsize: 47044
[startup+110.008 s]
Raw data (loadavg): 0.95 0.91 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 11677 0 0 0 10964 37 0 0 25 0 1 0 547263839 50049024 11282 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12219 11282 603 41 0 12178 0
vsize: 48876
[startup+120.009 s]
Raw data (loadavg): 0.95 0.92 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 11843 0 0 0 11962 38 0 0 25 0 1 0 547263839 50712576 11448 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12381 11448 603 41 0 12340 0
vsize: 49524
[startup+130.01 s]
Raw data (loadavg): 0.96 0.92 0.89 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 12156 0 0 0 12961 40 0 0 25 0 1 0 547263839 51908608 11761 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12673 11761 603 41 0 12632 0
vsize: 50692
[startup+140.01 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 12436 0 0 0 13960 41 0 0 25 0 1 0 547263839 53116928 12041 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12968 12041 603 41 0 12927 0
vsize: 51872
[startup+150.01 s]
Raw data (loadavg): 0.97 0.92 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 12514 0 0 0 14959 41 0 0 25 0 1 0 547263839 53645312 12119 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13097 12119 603 41 0 13056 0
vsize: 52388
[startup+160.011 s]
Raw data (loadavg): 0.98 0.92 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 12662 0 0 0 15958 43 0 0 25 0 1 0 547263839 54177792 12267 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13227 12267 603 41 0 13186 0
vsize: 52908
[startup+170.011 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 12891 0 0 0 16957 44 0 0 25 0 1 0 547263839 55115776 12496 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13456 12496 603 41 0 13415 0
vsize: 53824
[startup+180.012 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 13031 0 0 0 17957 45 0 0 25 0 1 0 547263839 55648256 12636 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13586 12636 603 41 0 13545 0
vsize: 54344
[startup+190.012 s]
Raw data (loadavg): 0.98 0.93 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 13259 0 0 0 18956 46 0 0 25 0 1 0 547263839 56586240 12864 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13815 12864 603 41 0 13774 0
vsize: 55260
[startup+200.012 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 13532 0 0 0 19954 48 0 0 25 0 1 0 547263839 57667584 13137 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14079 13137 603 41 0 14038 0
vsize: 56316
[startup+210.013 s]
Raw data (loadavg): 0.99 0.93 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 13916 0 0 0 20952 50 0 0 25 0 1 0 547263839 59273216 13521 4294967295 134512640 134672761 3221224544 3221223680 134560611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14471 13521 603 41 0 14430 0
vsize: 57884
[startup+220.013 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 14109 0 0 0 21951 51 0 0 25 0 1 0 547263839 60071936 13714 4294967295 134512640 134672761 3221224544 3221223760 134561987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14666 13714 603 41 0 14625 0
vsize: 58664
[startup+230.014 s]
Raw data (loadavg): 0.99 0.94 0.90 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 14256 0 0 0 22950 52 0 0 25 0 1 0 547263839 60608512 13861 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14797 13861 603 41 0 14756 0
vsize: 59188
[startup+240.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 14415 0 0 0 23950 53 0 0 25 0 1 0 547263839 61276160 14020 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14960 14020 603 41 0 14919 0
vsize: 59840
[startup+250.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 14738 0 0 0 24948 54 0 0 25 0 1 0 547263839 62615552 14343 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15287 14343 603 41 0 15246 0
vsize: 61148
[startup+260.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 15247 0 0 0 25947 56 0 0 25 0 1 0 547263839 64634880 14852 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15780 14852 603 41 0 15739 0
vsize: 63120
[startup+270.015 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 15428 0 0 0 26946 57 0 0 25 0 1 0 547263839 65306624 15033 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15944 15033 603 41 0 15903 0
vsize: 63776
[startup+280.016 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 15646 0 0 0 27945 58 0 0 25 0 1 0 547263839 66236416 15251 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16171 15251 603 41 0 16130 0
vsize: 64684
[startup+290.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 15686 0 0 0 28945 58 0 0 25 0 1 0 547263839 66371584 15291 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16204 15291 603 41 0 16163 0
vsize: 64816
[startup+300.017 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 15921 0 0 0 29944 59 0 0 25 0 1 0 547263839 67829760 15526 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16560 15526 603 41 0 16519 0
vsize: 66240
[startup+310.018 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 16136 0 0 0 30943 60 0 0 25 0 1 0 547263839 68759552 15741 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16787 15741 603 41 0 16746 0
vsize: 67148
[startup+320.019 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 16365 0 0 0 31942 61 0 0 25 0 1 0 547263839 69701632 15970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17017 15970 603 41 0 16976 0
vsize: 68068
[startup+330.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 16769 0 0 0 32941 63 0 0 25 0 1 0 547263839 71307264 16374 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17409 16374 603 41 0 17368 0
vsize: 69636
[startup+340.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 16918 0 0 0 33940 64 0 0 25 0 1 0 547263839 71847936 16523 4294967295 134512640 134672761 3221224544 3221223664 134542667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17541 16523 603 41 0 17500 0
vsize: 70164
[startup+350.02 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 17229 0 0 0 34939 65 0 0 25 0 1 0 547263839 73175040 16834 4294967295 134512640 134672761 3221224544 3221223712 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17865 16834 603 41 0 17824 0
vsize: 71460
[startup+360.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 17565 0 0 0 35938 66 0 0 25 0 1 0 547263839 74526720 17170 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18195 17170 603 41 0 18154 0
vsize: 72780
[startup+370.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 17831 0 0 0 36936 68 0 0 25 0 1 0 547263839 75603968 17436 4294967295 134512640 134672761 3221224544 3221223712 134560855 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18458 17436 603 41 0 18417 0
vsize: 73832
[startup+380.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 18131 0 0 0 37936 69 0 0 25 0 1 0 547263839 76812288 17736 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18753 17736 603 41 0 18712 0
vsize: 75012
[startup+390.022 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 18312 0 0 0 38935 70 0 0 25 0 1 0 547263839 77479936 17917 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17917 603 41 0 18875 0
vsize: 75664
[startup+400.022 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 18497 0 0 0 39935 70 0 0 25 0 1 0 547263839 78270464 18102 4294967295 134512640 134672761 3221224544 3221223648 134560054 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19109 18102 603 41 0 19068 0
vsize: 76436
[startup+410.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 18823 0 0 0 40934 71 0 0 25 0 1 0 547263839 79593472 18428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19432 18428 603 41 0 19391 0
vsize: 77728
[startup+420.023 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 19099 0 0 0 41933 72 0 0 25 0 1 0 547263839 80662528 18704 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19693 18704 603 41 0 19652 0
vsize: 78772
[startup+430.024 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 19364 0 0 0 42932 73 0 0 25 0 1 0 547263839 81735680 18969 4294967295 134512640 134672761 3221224544 3221223648 134559875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19955 18969 603 41 0 19914 0
vsize: 79820
[startup+440.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 19694 0 0 0 43930 75 0 0 25 0 1 0 547263839 83070976 19299 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20281 19299 603 41 0 20240 0
vsize: 81124
[startup+450.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 19916 0 0 0 44930 76 0 0 25 0 1 0 547263839 83886080 19521 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20480 19521 603 41 0 20439 0
vsize: 81920
[startup+460.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 20364 0 0 0 45928 78 0 0 25 0 1 0 547263839 85766144 19969 4294967295 134512640 134672761 3221224544 3221223648 134560215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20939 19969 603 41 0 20898 0
vsize: 83756
[startup+470.025 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 20759 0 0 0 46927 79 0 0 25 0 1 0 547263839 87375872 20364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21332 20364 603 41 0 21291 0
vsize: 85328
[startup+480.026 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 20993 0 0 0 47926 80 0 0 25 0 1 0 547263839 88313856 20598 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21561 20598 603 41 0 21520 0
vsize: 86244
[startup+490.027 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 21136 0 0 0 48926 80 0 0 25 0 1 0 547263839 88850432 20741 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21692 20741 603 41 0 21651 0
vsize: 86768
[startup+500.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 21293 0 0 0 49925 81 0 0 25 0 1 0 547263839 89530368 20898 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21858 20898 603 41 0 21817 0
vsize: 87432
[startup+510.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 21679 0 0 0 50924 83 0 0 25 0 1 0 547263839 91131904 21284 4294967295 134512640 134672761 3221224544 3221223680 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22249 21284 603 41 0 22208 0
vsize: 88996
[startup+520.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 21980 0 0 0 51923 84 0 0 25 0 1 0 547263839 92319744 21585 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22539 21585 603 41 0 22498 0
vsize: 90156
[startup+530.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 22204 0 0 0 52922 85 0 0 25 0 1 0 547263839 93130752 21809 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22737 21809 603 41 0 22696 0
vsize: 90948
[startup+540.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 22360 0 0 0 53921 86 0 0 25 0 1 0 547263839 93802496 21965 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22901 21965 603 41 0 22860 0
vsize: 91604
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 22581 0 0 0 54921 86 0 0 25 0 1 0 547263839 94740480 22186 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23130 22186 603 41 0 23089 0
vsize: 92520
[startup+560.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 22779 0 0 0 55920 88 0 0 25 0 1 0 547263839 95567872 22384 4294967295 134512640 134672761 3221224544 3221223728 134558632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23332 22384 603 41 0 23291 0
vsize: 93328
[startup+570.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 23033 0 0 0 56919 89 0 0 25 0 1 0 547263839 96501760 22638 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23560 22638 603 41 0 23519 0
vsize: 94240
[startup+580.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 23254 0 0 0 57918 90 0 0 25 0 1 0 547263839 97435648 22859 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23788 22859 603 41 0 23747 0
vsize: 95152
[startup+590.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 23547 0 0 0 58917 91 0 0 25 0 1 0 547263839 99688448 23152 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24338 23152 603 41 0 24297 0
vsize: 97352
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 23648 0 0 0 59917 91 0 0 25 0 1 0 547263839 100089856 23253 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24436 23253 603 41 0 24395 0
vsize: 97744
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 23887 0 0 0 60916 92 0 0 25 0 1 0 547263839 101044224 23492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24669 23492 603 41 0 24628 0
vsize: 98676
[startup+620.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 24089 0 0 0 61915 93 0 0 25 0 1 0 547263839 101851136 23694 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24866 23694 603 41 0 24825 0
vsize: 99464
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 24484 0 0 0 62915 94 0 0 25 0 1 0 547263839 103464960 24089 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25260 24089 603 41 0 25219 0
vsize: 101040
[startup+640.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 24747 0 0 0 63924 95 0 0 25 0 1 0 547263839 104546304 24352 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25524 24352 603 41 0 25483 0
vsize: 102096
[startup+650.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 24961 0 0 0 64924 95 0 0 25 0 1 0 547263839 105353216 24566 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25721 24566 603 41 0 25680 0
vsize: 102884
[startup+660.132 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 25175 0 0 0 65923 96 0 0 25 0 1 0 547263839 106295296 24780 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25951 24780 603 41 0 25910 0
vsize: 103804
[startup+670.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 25390 0 0 0 66922 97 0 0 25 0 1 0 547263839 107102208 24995 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26148 24995 603 41 0 26107 0
vsize: 104592
[startup+680.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 25676 0 0 0 67921 98 0 0 25 0 1 0 547263839 108306432 25281 4294967295 134512640 134672761 3221224544 3221223680 134560709 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26442 25281 603 41 0 26401 0
vsize: 105768
[startup+690.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 25809 0 0 0 68921 99 0 0 25 0 1 0 547263839 108838912 25414 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26572 25414 603 41 0 26531 0
vsize: 106288
[startup+700.133 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 25986 0 0 0 69920 99 0 0 25 0 1 0 547263839 109506560 25591 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26735 25591 603 41 0 26694 0
vsize: 106940
[startup+710.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 26211 0 0 0 70919 100 0 0 25 0 1 0 547263839 110440448 25816 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26963 25816 603 41 0 26922 0
vsize: 107852
[startup+720.134 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 26368 0 0 0 71919 101 0 0 25 0 1 0 547263839 111116288 25973 4294967295 134512640 134672761 3221224544 3221223712 134560797 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27128 25973 603 41 0 27087 0
vsize: 108512
[startup+730.135 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 26545 0 0 0 72919 102 0 0 25 0 1 0 547263839 111800320 26150 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27295 26150 603 41 0 27254 0
vsize: 109180
[startup+740.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 26693 0 0 0 73918 102 0 0 25 0 1 0 547263839 112349184 26298 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27429 26298 603 41 0 27388 0
vsize: 109716
[startup+750.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 27056 0 0 0 74917 103 0 0 25 0 1 0 547263839 113827840 26661 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27790 26661 603 41 0 27749 0
vsize: 111160
[startup+760.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 27283 0 0 0 75916 104 0 0 25 0 1 0 547263839 114769920 26888 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28020 26888 603 41 0 27979 0
vsize: 112080
[startup+770.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 27498 0 0 0 76916 105 0 0 25 0 1 0 547263839 115716096 27103 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28251 27103 603 41 0 28210 0
vsize: 113004
[startup+780.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 27695 0 0 0 77915 106 0 0 25 0 1 0 547263839 116412416 27300 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28421 27300 603 41 0 28380 0
vsize: 113684
[startup+790.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 27879 0 0 0 78915 106 0 0 25 0 1 0 547263839 117211136 27484 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28616 27484 603 41 0 28575 0
vsize: 114464
[startup+800.136 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 28128 0 0 0 79914 107 0 0 25 0 1 0 547263839 118149120 27733 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28845 27733 603 41 0 28804 0
vsize: 115380
[startup+810.137 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 28585 0 0 0 80913 108 0 0 25 0 1 0 547263839 120029184 28190 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29304 28190 603 41 0 29263 0
vsize: 117216
[startup+820.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 28789 0 0 0 81912 109 0 0 25 0 1 0 547263839 120856576 28394 4294967295 134512640 134672761 3221224544 3221223692 134560631 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29506 28394 603 41 0 29465 0
vsize: 118024
[startup+830.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 29141 0 0 0 82912 110 0 0 25 0 1 0 547263839 122335232 28746 4294967295 134512640 134672761 3221224544 3221223500 1075349771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29867 28746 603 41 0 29826 0
vsize: 119468
[startup+840.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 29426 0 0 0 83911 111 0 0 25 0 1 0 547263839 123535360 29031 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30160 29031 603 41 0 30119 0
vsize: 120640
[startup+850.138 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 29573 0 0 0 84911 112 0 0 25 0 1 0 547263839 124067840 29178 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30290 29178 603 41 0 30249 0
vsize: 121160
[startup+860.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 29703 0 0 0 85910 112 0 0 25 0 1 0 547263839 124600320 29308 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30420 29308 603 41 0 30379 0
vsize: 121680
[startup+870.139 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 29928 0 0 0 86910 113 0 0 25 0 1 0 547263839 125534208 29533 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30648 29533 603 41 0 30607 0
vsize: 122592
[startup+880.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 30046 0 0 0 87909 114 0 0 25 0 1 0 547263839 125935616 29651 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30746 29651 603 41 0 30705 0
vsize: 122984
[startup+890.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 30112 0 0 0 88909 114 0 0 25 0 1 0 547263839 126214144 29717 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30814 29717 603 41 0 30773 0
vsize: 123256
[startup+900.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 30311 0 0 0 89909 114 0 0 25 0 1 0 547263839 127004672 29916 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31007 29916 603 41 0 30966 0
vsize: 124028
[startup+910.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 30567 0 0 0 90908 115 0 0 25 0 1 0 547263839 128086016 30172 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31271 30172 603 41 0 31230 0
vsize: 125084
[startup+920.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 30791 0 0 0 91908 116 0 0 25 0 1 0 547263839 129032192 30396 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31502 30396 603 41 0 31461 0
vsize: 126008
[startup+930.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 31061 0 0 0 92907 117 0 0 25 0 1 0 547263839 130105344 30666 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31764 30666 603 41 0 31723 0
vsize: 127056
[startup+940.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 31420 0 0 0 93906 118 0 0 25 0 1 0 547263839 131575808 31025 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32123 31025 603 41 0 32082 0
vsize: 128492
[startup+950.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 31744 0 0 0 94904 120 0 0 25 0 1 0 547263839 132915200 31349 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32450 31349 603 41 0 32409 0
vsize: 129800
[startup+960.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 32001 0 0 0 95903 121 0 0 25 0 1 0 547263839 133980160 31606 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32710 31606 603 41 0 32669 0
vsize: 130840
[startup+970.141 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 32241 0 0 0 96902 122 0 0 25 0 1 0 547263839 134918144 31846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32939 31846 603 41 0 32898 0
vsize: 131756
[startup+980.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 32390 0 0 0 97902 123 0 0 25 0 1 0 547263839 135450624 31995 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33069 31995 603 41 0 33028 0
vsize: 132276
[startup+990.142 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 32478 0 0 0 98902 123 0 0 25 0 1 0 547263839 135852032 32083 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33167 32083 603 41 0 33126 0
vsize: 132668
[startup+1000.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 32765 0 0 0 99901 124 0 0 25 0 1 0 547263839 137052160 32370 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33460 32370 603 41 0 33419 0
vsize: 133840
[startup+1010.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 33044 0 0 0 100900 125 0 0 25 0 1 0 547263839 138121216 32649 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33721 32649 603 41 0 33680 0
vsize: 134884
[startup+1020.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 33237 0 0 0 101899 126 0 0 25 0 1 0 547263839 138932224 32842 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33919 32842 603 41 0 33878 0
vsize: 135676
[startup+1030.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 33429 0 0 0 102899 127 0 0 25 0 1 0 547263839 139755520 33034 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34120 33034 603 41 0 34079 0
vsize: 136480
[startup+1040.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 33530 0 0 0 103899 127 0 0 25 0 1 0 547263839 140148736 33135 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34216 33135 603 41 0 34175 0
vsize: 136864
[startup+1050.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 33851 0 0 0 104898 128 0 0 25 0 1 0 547263839 141484032 33456 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34542 33456 603 41 0 34501 0
vsize: 138168
[startup+1060.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 34137 0 0 0 105898 128 0 0 25 0 1 0 547263839 142561280 33742 4294967295 134512640 134672761 3221224544 3221223744 134557830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34805 33742 603 41 0 34764 0
vsize: 139220
[startup+1070.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 34477 0 0 0 106897 129 0 0 25 0 1 0 547263839 143912960 34082 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35135 34082 603 41 0 35094 0
vsize: 140540
[startup+1080.14 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 34790 0 0 0 107896 130 0 0 25 0 1 0 547263839 145244160 34395 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35460 34395 603 41 0 35419 0
vsize: 141840
[startup+1090.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 35056 0 0 0 108895 131 0 0 25 0 1 0 547263839 146325504 34661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35724 34661 603 41 0 35683 0
vsize: 142896
[startup+1100.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 35295 0 0 0 109894 132 0 0 25 0 1 0 547263839 147263488 34900 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35953 34900 603 41 0 35912 0
vsize: 143812
[startup+1110.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 35462 0 0 0 110894 132 0 0 25 0 1 0 547263839 147931136 35067 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36116 35067 603 41 0 36075 0
vsize: 144464
[startup+1120.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 35748 0 0 0 111893 133 0 0 25 0 1 0 547263839 149151744 35353 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36414 35353 603 41 0 36373 0
vsize: 145656
[startup+1130.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 36006 0 0 0 112893 134 0 0 25 0 1 0 547263839 150233088 35611 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36678 35611 603 41 0 36637 0
vsize: 146712
[startup+1140.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 36093 0 0 0 113893 134 0 0 25 0 1 0 547263839 150503424 35698 4294967295 134512640 134672761 3221224544 3221223680 134560575 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36744 35698 603 41 0 36703 0
vsize: 146976
[startup+1150.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 36202 0 0 0 114893 135 0 0 25 0 1 0 547263839 150908928 35807 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36843 35807 603 41 0 36802 0
vsize: 147372
[startup+1160.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 36275 0 0 0 115893 135 0 0 25 0 1 0 547263839 151310336 35880 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36941 35880 603 41 0 36900 0
vsize: 147764
[startup+1170.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 36522 0 0 0 116892 135 0 0 25 0 1 0 547263839 152240128 36127 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37168 36127 603 41 0 37127 0
vsize: 148672
[startup+1180.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 36763 0 0 0 117892 136 0 0 25 0 1 0 547263839 153182208 36368 4294967295 134512640 134672761 3221224544 3221223648 134560285 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37398 36368 603 41 0 37357 0
vsize: 149592
[startup+1190.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 36978 0 0 0 118892 136 0 0 25 0 1 0 547263839 154116096 36583 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37626 36583 603 41 0 37585 0
vsize: 150504
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30533
Raw data (stat): 30533 (minisat+) R 30532 23176 23175 0 -1 0 37154 0 0 0 119891 137 0 0 25 0 1 0 547263839 154787840 36759 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37790 36759 603 41 0 37749 0
vsize: 151160
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.22 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30533
Raw data (stat): 30533 (minisat+) Z 30532 23176 23175 0 -1 12 37156 0 0 0 119892 144 0 0 25 0 1 0 547263839 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.22
CPU time (s): 1200.36
CPU user time (s): 1198.92
CPU system time (s): 1.44178
CPU usage (%): 100.012
Max. virtual memory (Kb): 151160
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####