PB'05 competition: run trace

Some explanations

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

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-dcmulti.opb
MD5SUM	28123830d5f7e3646d18978bb347487c
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.085986
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 18291

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc19 THE 2005-04-21 14:13:53 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18291 boxname=wulflinc19 idbench=1407 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  28123830d5f7e3646d18978bb347487c  /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-dcmulti.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-dcmulti.opb /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-dcmulti.opb
IDLAUNCH: 18291
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.037
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:        760416 kB
Buffers:         22432 kB
Cached:         227252 kB
SwapCached:        556 kB
Active:          36444 kB
Inactive:       215268 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        760164 kB
SwapTotal:     2097892 kB
SwapFree:      2096388 kB
Dirty:              36 kB
Writeback:           0 kB
Mapped:           5164 kB
Slab:            16740 kB
Committed_AS:    63820 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:33:56 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 18291 7 1200.25 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.79 0.95 0.94 2/55 1816
Raw data (stat): 1816 (runsolver) R 1815 22929 22928 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545708747 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.001 s]
Raw data (loadavg): 0.82 0.96 0.94 2/55 1816
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 9689 0 0 0 976 22 0 0 25 0 1 0 545708747 41967616 9294 4294967295 134512640 134672761 3221224544 3221223680 134560588 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.0016 s]
Raw data (loadavg): 0.85 0.96 0.94 2/55 1816
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 9709 0 0 0 1976 23 0 0 25 0 1 0 545708747 41967616 9314 4294967295 134512640 134672761 3221224544 3221223716 134556667 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.0021 s]
Raw data (loadavg): 0.87 0.96 0.94 2/55 1816
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 9756 0 0 0 2975 24 0 0 25 0 1 0 545708747 42102784 9361 4294967295 134512640 134672761 3221224544 3221223716 134556632 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.0023 s]
Raw data (loadavg): 0.89 0.96 0.94 2/55 1816
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 9799 0 0 0 3974 24 0 0 25 0 1 0 545708747 42237952 9404 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10312 9404 603 41 0 10271 0
vsize: 41248
[startup+50.0031 s]
Raw data (loadavg): 0.91 0.96 0.94 2/55 1816
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 9835 0 0 0 4974 25 0 0 25 0 1 0 545708747 42369024 9440 4294967295 134512640 134672761 3221224544 3221223716 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10344 9440 603 41 0 10303 0
vsize: 41376
[startup+60.004 s]
Raw data (loadavg): 0.92 0.96 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 10009 0 0 0 5973 26 0 0 25 0 1 0 545708747 43188224 9614 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10544 9614 603 41 0 10503 0
vsize: 42176
[startup+70.005 s]
Raw data (loadavg): 0.93 0.96 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 10353 0 0 0 6972 27 0 0 25 0 1 0 545708747 44556288 9958 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10878 9958 603 41 0 10837 0
vsize: 43512
[startup+80.0065 s]
Raw data (loadavg): 0.94 0.96 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 10744 0 0 0 7971 29 0 0 25 0 1 0 545708747 46166016 10349 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11271 10349 603 41 0 11230 0
vsize: 45084
[startup+90.006 s]
Raw data (loadavg): 0.95 0.96 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 11046 0 0 0 8970 30 0 0 25 0 1 0 545708747 47505408 10651 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11598 10651 603 41 0 11557 0
vsize: 46392
[startup+100.007 s]
Raw data (loadavg): 0.96 0.96 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 11315 0 0 0 9969 31 0 0 25 0 1 0 545708747 48574464 10920 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11859 10920 603 41 0 11818 0
vsize: 47436
[startup+110.008 s]
Raw data (loadavg): 0.96 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 11717 0 0 0 10968 32 0 0 25 0 1 0 545708747 50184192 11322 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12252 11322 603 41 0 12211 0
vsize: 49008
[startup+120.008 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 11896 0 0 0 11967 33 0 0 25 0 1 0 545708747 50978816 11501 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12446 11501 603 41 0 12405 0
vsize: 49784
[startup+130.009 s]
Raw data (loadavg): 0.97 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 12235 0 0 0 12966 34 0 0 25 0 1 0 545708747 52314112 11840 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12772 11840 603 41 0 12731 0
vsize: 51088
[startup+140.009 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 12458 0 0 0 13965 35 0 0 25 0 1 0 545708747 53116928 12063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12968 12063 603 41 0 12927 0
vsize: 51872
[startup+150.01 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 12550 0 0 0 14965 36 0 0 25 0 1 0 545708747 53780480 12155 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13130 12155 603 41 0 13089 0
vsize: 52520
[startup+160.01 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 12697 0 0 0 15964 37 0 0 25 0 1 0 545708747 54308864 12302 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13259 12302 603 41 0 13218 0
vsize: 53036
[startup+170.01 s]
Raw data (loadavg): 0.98 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 12907 0 0 0 16963 38 0 0 25 0 1 0 545708747 55250944 12512 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13489 12512 603 41 0 13448 0
vsize: 53956
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 13087 0 0 0 17963 38 0 0 25 0 1 0 545708747 55914496 12692 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13651 12692 603 41 0 13610 0
vsize: 54604
[startup+190.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 13372 0 0 0 18962 39 0 0 25 0 1 0 545708747 57126912 12977 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13947 12977 603 41 0 13906 0
vsize: 55788
[startup+200.012 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 13588 0 0 0 19961 40 0 0 25 0 1 0 545708747 57937920 13193 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14145 13193 603 41 0 14104 0
vsize: 56580
[startup+210.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 14060 0 0 0 20959 42 0 0 25 0 1 0 545708747 59801600 13665 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14600 13665 603 41 0 14559 0
vsize: 58400
[startup+220.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 14176 0 0 0 21959 42 0 0 25 0 1 0 545708747 60342272 13781 4294967295 134512640 134672761 3221224544 3221223748 134561964 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14732 13781 603 41 0 14691 0
vsize: 58928
[startup+230.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 14330 0 0 0 22959 43 0 0 25 0 1 0 545708747 60878848 13935 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14863 13935 603 41 0 14822 0
vsize: 59452
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 14473 0 0 0 23958 43 0 0 25 0 1 0 545708747 61542400 14078 4294967295 134512640 134672761 3221224544 3221223680 134560604 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15025 14078 603 41 0 14984 0
vsize: 60100
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 14980 0 0 0 24956 45 0 0 25 0 1 0 545708747 63561728 14585 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15518 14585 603 41 0 15477 0
vsize: 62072
[startup+260.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 15410 0 0 0 25955 47 0 0 25 0 1 0 545708747 65306624 15015 4294967295 134512640 134672761 3221224544 3221223716 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15944 15015 603 41 0 15903 0
vsize: 63776
[startup+270.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 15502 0 0 0 26955 47 0 0 25 0 1 0 545708747 65708032 15107 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16042 15107 603 41 0 16001 0
vsize: 64168
[startup+280.013 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 15674 0 0 0 27955 48 0 0 25 0 1 0 545708747 66371584 15279 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16204 15279 603 41 0 16163 0
vsize: 64816
[startup+290.014 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 15777 0 0 0 28955 48 0 0 25 0 1 0 545708747 67297280 15382 4294967295 134512640 134672761 3221224544 3221223712 134561385 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16430 15382 603 41 0 16389 0
vsize: 65720
[startup+300.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 16029 0 0 0 29955 48 0 0 25 0 1 0 545708747 68222976 15634 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16656 15634 603 41 0 16615 0
vsize: 66624
[startup+310.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 16231 0 0 0 30954 49 0 0 25 0 1 0 545708747 69165056 15836 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16886 15836 603 41 0 16845 0
vsize: 67544
[startup+320.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 16606 0 0 0 31953 50 0 0 25 0 1 0 545708747 70639616 16211 4294967295 134512640 134672761 3221224544 3221223712 134560867 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17246 16211 603 41 0 17205 0
vsize: 68984
[startup+330.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 16858 0 0 0 32953 50 0 0 25 0 1 0 545708747 71577600 16463 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17475 16463 603 41 0 17434 0
vsize: 69900
[startup+340.015 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 17128 0 0 0 33952 51 0 0 25 0 1 0 545708747 72650752 16733 4294967295 134512640 134672761 3221224544 3221223728 134559330 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17737 16733 603 41 0 17696 0
vsize: 70948
[startup+350.017 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1818
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 17556 0 0 0 34951 53 0 0 25 0 1 0 545708747 74391552 17161 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18162 17161 603 41 0 18121 0
vsize: 72648
[startup+360.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 17775 0 0 0 35950 54 0 0 25 0 1 0 545708747 75333632 17380 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18392 17380 603 41 0 18351 0
vsize: 73568
[startup+370.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 18124 0 0 0 36949 55 0 0 25 0 1 0 545708747 76677120 17729 4294967295 134512640 134672761 3221224544 3221223484 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18720 17729 603 41 0 18679 0
vsize: 74880
[startup+380.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 18300 0 0 0 37949 56 0 0 25 0 1 0 545708747 77479936 17905 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 17905 603 41 0 18875 0
vsize: 75664
[startup+390.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 18497 0 0 0 38948 57 0 0 25 0 1 0 545708747 78270464 18102 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19109 18102 603 41 0 19068 0
vsize: 76436
[startup+400.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 18834 0 0 0 39947 58 0 0 25 0 1 0 545708747 79593472 18439 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19432 18439 603 41 0 19391 0
vsize: 77728
[startup+410.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 19106 0 0 0 40946 59 0 0 25 0 1 0 545708747 80662528 18711 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19693 18711 603 41 0 19652 0
vsize: 78772
[startup+420.018 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 19446 0 0 0 41945 60 0 0 25 0 1 0 545708747 82001920 19051 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20020 19051 603 41 0 19979 0
vsize: 80080
[startup+430.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 19735 0 0 0 42944 61 0 0 25 0 1 0 545708747 83202048 19340 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20313 19340 603 41 0 20272 0
vsize: 81252
[startup+440.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 20013 0 0 0 43944 61 0 0 25 0 1 0 545708747 84287488 19618 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20578 19618 603 41 0 20537 0
vsize: 82312
[startup+450.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 20558 0 0 0 44942 64 0 0 25 0 1 0 545708747 86564864 20163 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21134 20163 603 41 0 21093 0
vsize: 84536
[startup+460.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 20836 0 0 0 45941 65 0 0 25 0 1 0 545708747 87646208 20441 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21398 20441 603 41 0 21357 0
vsize: 85592
[startup+470.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 21087 0 0 0 46940 65 0 0 25 0 1 0 545708747 88715264 20692 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21659 20692 603 41 0 21618 0
vsize: 86636
[startup+480.019 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 21142 0 0 0 47940 66 0 0 25 0 1 0 545708747 88850432 20747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21692 20747 603 41 0 21651 0
vsize: 86768
[startup+490.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 21506 0 0 0 48939 66 0 0 25 0 1 0 545708747 90329088 21111 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22053 21111 603 41 0 22012 0
vsize: 88212
[startup+500.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 21864 0 0 0 49938 68 0 0 25 0 1 0 545708747 91787264 21469 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22409 21469 603 41 0 22368 0
vsize: 89636
[startup+510.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 22162 0 0 0 50937 69 0 0 25 0 1 0 545708747 92995584 21767 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22704 21767 603 41 0 22663 0
vsize: 90816
[startup+520.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 22277 0 0 0 51937 69 0 0 25 0 1 0 545708747 93532160 21882 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22835 21882 603 41 0 22794 0
vsize: 91340
[startup+530.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 22580 0 0 0 52937 70 0 0 25 0 1 0 545708747 94740480 22185 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23130 22185 603 41 0 23089 0
vsize: 92520
[startup+540.02 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 22723 0 0 0 53936 70 0 0 25 0 1 0 545708747 95297536 22328 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23266 22328 603 41 0 23225 0
vsize: 93064
[startup+550.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 22973 0 0 0 54936 71 0 0 25 0 1 0 545708747 96366592 22578 4294967295 134512640 134672761 3221224544 3221223712 134560874 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23527 22578 603 41 0 23486 0
vsize: 94108
[startup+560.022 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 23214 0 0 0 55935 72 0 0 25 0 1 0 545708747 97304576 22819 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23756 22819 603 41 0 23715 0
vsize: 95024
[startup+570.021 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 23527 0 0 0 56935 73 0 0 25 0 1 0 545708747 99557376 23132 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24306 23132 603 41 0 24265 0
vsize: 97224
[startup+580.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 23643 0 0 0 57935 73 0 0 25 0 1 0 545708747 100089856 23248 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24436 23248 603 41 0 24395 0
vsize: 97744
[startup+590.028 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 23893 0 0 0 58934 74 0 0 25 0 1 0 545708747 101044224 23498 4294967295 134512640 134672761 3221224544 3221223500 1075349771 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24669 23498 603 41 0 24628 0
vsize: 98676
[startup+600.029 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 24089 0 0 0 59934 75 0 0 25 0 1 0 545708747 101851136 23694 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24866 23694 603 41 0 24825 0
vsize: 99464
[startup+610.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 24528 0 0 0 60933 76 0 0 25 0 1 0 545708747 103600128 24133 4294967295 134512640 134672761 3221224544 3221223648 134559890 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25293 24133 603 41 0 25252 0
vsize: 101172
[startup+620.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 24779 0 0 0 61932 77 0 0 25 0 1 0 545708747 104677376 24384 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25556 24384 603 41 0 25515 0
vsize: 102224
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 24998 0 0 0 62932 78 0 0 25 0 1 0 545708747 105488384 24603 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25754 24603 603 41 0 25713 0
vsize: 103016
[startup+640.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 25247 0 0 0 63931 78 0 0 25 0 1 0 545708747 106561536 24852 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26016 24852 603 41 0 25975 0
vsize: 104064
[startup+650.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1820
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 25509 0 0 0 64930 79 0 0 25 0 1 0 545708747 107634688 25114 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26278 25114 603 41 0 26237 0
vsize: 105112
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 25707 0 0 0 65929 80 0 0 25 0 1 0 545708747 108441600 25312 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26475 25312 603 41 0 26434 0
vsize: 105900
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 25906 0 0 0 66929 80 0 0 25 0 1 0 545708747 109236224 25511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26669 25511 603 41 0 26628 0
vsize: 106676
[startup+680.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 26096 0 0 0 67929 80 0 0 25 0 1 0 545708747 110043136 25701 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26866 25701 603 41 0 26825 0
vsize: 107464
[startup+690.031 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 26278 0 0 0 68929 81 0 0 25 0 1 0 545708747 110710784 25883 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27029 25883 603 41 0 26988 0
vsize: 108116
[startup+700.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 26481 0 0 0 69928 81 0 0 25 0 1 0 545708747 111529984 26086 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27229 26086 603 41 0 27188 0
vsize: 108916
[startup+710.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 26643 0 0 0 70928 82 0 0 25 0 1 0 545708747 112214016 26248 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27396 26248 603 41 0 27355 0
vsize: 109584
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 26976 0 0 0 71927 82 0 0 25 0 1 0 545708747 113561600 26581 4294967295 134512640 134672761 3221224544 3221223648 134560254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27725 26581 603 41 0 27684 0
vsize: 110900
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 27234 0 0 0 72926 84 0 0 25 0 1 0 545708747 114638848 26839 4294967295 134512640 134672761 3221224544 3221223728 134559390 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27988 26839 603 41 0 27947 0
vsize: 111952
[startup+740.032 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 27464 0 0 0 73925 85 0 0 25 0 1 0 545708747 115580928 27069 4294967295 134512640 134672761 3221224544 3221223716 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28218 27069 603 41 0 28177 0
vsize: 112872
[startup+750.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 27666 0 0 0 74926 85 0 0 25 0 1 0 545708747 116277248 27271 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28388 27271 603 41 0 28347 0
vsize: 113552
[startup+760.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 27869 0 0 0 75925 85 0 0 25 0 1 0 545708747 117211136 27474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28616 27474 603 41 0 28575 0
vsize: 114464
[startup+770.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 28126 0 0 0 76925 86 0 0 25 0 1 0 545708747 118149120 27731 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28845 27731 603 41 0 28804 0
vsize: 115380
[startup+780.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 28607 0 0 0 77924 87 0 0 25 0 1 0 545708747 120164352 28212 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29337 28212 603 41 0 29296 0
vsize: 117348
[startup+790.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 28810 0 0 0 78923 88 0 0 25 0 1 0 545708747 120991744 28415 4294967295 134512640 134672761 3221224544 3221223712 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29539 28415 603 41 0 29498 0
vsize: 118156
[startup+800.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 29191 0 0 0 79922 89 0 0 25 0 1 0 545708747 122470400 28796 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29900 28796 603 41 0 29859 0
vsize: 119600
[startup+810.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 29458 0 0 0 80922 90 0 0 25 0 1 0 545708747 123670528 29063 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30193 29063 603 41 0 30152 0
vsize: 120772
[startup+820.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 29623 0 0 0 81922 90 0 0 25 0 1 0 545708747 124334080 29228 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30355 29228 603 41 0 30314 0
vsize: 121420
[startup+830.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 29764 0 0 0 82921 90 0 0 25 0 1 0 545708747 124870656 29369 4294967295 134512640 134672761 3221224544 3221223704 134561238 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30486 29369 603 41 0 30445 0
vsize: 121944
[startup+840.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 29998 0 0 0 83921 91 0 0 25 0 1 0 545708747 125800448 29603 4294967295 134512640 134672761 3221224544 3221223716 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30713 29603 603 41 0 30672 0
vsize: 122852
[startup+850.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 30072 0 0 0 84921 91 0 0 25 0 1 0 545708747 126066688 29677 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30778 29677 603 41 0 30737 0
vsize: 123112
[startup+860.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 30192 0 0 0 85921 92 0 0 25 0 1 0 545708747 126611456 29797 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30911 29797 603 41 0 30870 0
vsize: 123644
[startup+870.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 30424 0 0 0 86920 92 0 0 25 0 1 0 545708747 127545344 30029 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31139 30029 603 41 0 31098 0
vsize: 124556
[startup+880.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 30703 0 0 0 87920 93 0 0 25 0 1 0 545708747 128626688 30308 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31403 30308 603 41 0 31362 0
vsize: 125612
[startup+890.033 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 30929 0 0 0 88919 94 0 0 25 0 1 0 545708747 129568768 30534 4294967295 134512640 134672761 3221224544 3221223648 134560504 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31633 30534 603 41 0 31592 0
vsize: 126532
[startup+900.034 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 31284 0 0 0 89919 95 0 0 25 0 1 0 545708747 131043328 30889 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31993 30889 603 41 0 31952 0
vsize: 127972
[startup+910.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 31649 0 0 0 90918 95 0 0 25 0 1 0 545708747 132513792 31254 4294967295 134512640 134672761 3221224544 3221223648 134560264 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32352 31254 603 41 0 32311 0
vsize: 129408
[startup+920.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 31941 0 0 0 91917 97 0 0 25 0 1 0 545708747 133713920 31546 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32645 31546 603 41 0 32604 0
vsize: 130580
[startup+930.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 32183 0 0 0 92916 97 0 0 25 0 1 0 545708747 134651904 31788 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32874 31788 603 41 0 32833 0
vsize: 131496
[startup+940.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 32370 0 0 0 93916 98 0 0 25 0 1 0 545708747 135450624 31975 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33069 31975 603 41 0 33028 0
vsize: 132276
[startup+950.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1822
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 32459 0 0 0 94916 98 0 0 25 0 1 0 545708747 135716864 32064 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33134 32064 603 41 0 33093 0
vsize: 132536
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 32760 0 0 0 95915 99 0 0 25 0 1 0 545708747 137052160 32365 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33460 32365 603 41 0 33419 0
vsize: 133840
[startup+970.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 33051 0 0 0 96914 100 0 0 25 0 1 0 545708747 138121216 32656 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33721 32656 603 41 0 33680 0
vsize: 134884
[startup+980.037 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 33255 0 0 0 97914 101 0 0 25 0 1 0 545708747 138932224 32860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33919 32860 603 41 0 33878 0
vsize: 135676
[startup+990.036 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 33435 0 0 0 98913 102 0 0 25 0 1 0 545708747 139755520 33040 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34120 33040 603 41 0 34079 0
vsize: 136480
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 33564 0 0 0 99913 102 0 0 25 0 1 0 545708747 140283904 33169 4294967295 134512640 134672761 3221224544 3221223648 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34249 33169 603 41 0 34208 0
vsize: 136996
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 33920 0 0 0 100913 102 0 0 25 0 1 0 545708747 141750272 33525 4294967295 134512640 134672761 3221224544 3221223648 134559866 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34607 33525 603 41 0 34566 0
vsize: 138428
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 34226 0 0 0 101912 104 0 0 25 0 1 0 545708747 142970880 33831 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34905 33831 603 41 0 34864 0
vsize: 139620
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 34593 0 0 0 102911 105 0 0 25 0 1 0 545708747 144449536 34198 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35266 34198 603 41 0 35225 0
vsize: 141064
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 34931 0 0 0 103910 106 0 0 25 0 1 0 545708747 145776640 34536 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35590 34536 603 41 0 35549 0
vsize: 142360
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 35176 0 0 0 104908 107 0 0 25 0 1 0 545708747 146857984 34781 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35854 34781 603 41 0 35813 0
vsize: 143416
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 35400 0 0 0 105907 108 0 0 25 0 1 0 545708747 147660800 35005 4294967295 134512640 134672761 3221224544 3221223696 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36050 35005 603 41 0 36009 0
vsize: 144200
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 35630 0 0 0 106906 109 0 0 25 0 1 0 545708747 148602880 35235 4294967295 134512640 134672761 3221224544 3221223728 134558937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36280 35235 603 41 0 36239 0
vsize: 145120
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 35933 0 0 0 107905 110 0 0 25 0 1 0 545708747 149827584 35538 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36579 35538 603 41 0 36538 0
vsize: 146316
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 36080 0 0 0 108904 111 0 0 25 0 1 0 545708747 150503424 35685 4294967295 134512640 134672761 3221224544 3221223680 134560726 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36744 35685 603 41 0 36703 0
vsize: 146976
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 36202 0 0 0 109904 111 0 0 25 0 1 0 545708747 150908928 35807 4294967295 134512640 134672761 3221224544 3221223716 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36843 35807 603 41 0 36802 0
vsize: 147372
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 36257 0 0 0 110904 111 0 0 25 0 1 0 545708747 151179264 35862 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36909 35862 603 41 0 36868 0
vsize: 147636
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 36463 0 0 0 111904 112 0 0 25 0 1 0 545708747 151977984 36068 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37104 36068 603 41 0 37063 0
vsize: 148416
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 36739 0 0 0 112903 113 0 0 25 0 1 0 545708747 153182208 36344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37398 36344 603 41 0 37357 0
vsize: 149592
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 36960 0 0 0 113903 113 0 0 25 0 1 0 545708747 153980928 36565 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37593 36565 603 41 0 37552 0
vsize: 150372
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 37145 0 0 0 114903 114 0 0 25 0 1 0 545708747 154787840 36750 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37790 36750 603 41 0 37749 0
vsize: 151160
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 37351 0 0 0 115902 114 0 0 25 0 1 0 545708747 155590656 36956 4294967295 134512640 134672761 3221224544 3221223716 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37986 36956 603 41 0 37945 0
vsize: 151944
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 37442 0 0 0 116902 114 0 0 25 0 1 0 545708747 156008448 37047 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38088 37047 603 41 0 38047 0
vsize: 152352
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 37728 0 0 0 117902 115 0 0 25 0 1 0 545708747 157065216 37333 4294967295 134512640 134672761 3221224544 3221223712 134560825 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38346 37333 603 41 0 38305 0
vsize: 153384
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 37784 0 0 0 118902 115 0 0 25 0 1 0 545708747 157335552 37389 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38412 37389 603 41 0 38371 0
vsize: 153648
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.94 2/55 1824
Raw data (stat): 1816 (minisat+) R 1815 22929 22928 0 -1 0 37892 0 0 0 119902 115 0 0 25 0 1 0 545708747 157863936 37497 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38541 37497 603 41 0 38500 0
vsize: 154164
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.94 1/55 1824
Raw data (stat): 1816 (minisat+) Z 1815 22929 22928 0 -1 12 37894 0 0 0 119902 122 0 0 25 0 1 0 545708747 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.12
CPU time (s): 1200.25
CPU user time (s): 1199.02
CPU system time (s): 1.22981
CPU usage (%): 100.012
Max. virtual memory (Kb): 154164
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####