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 15716

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 05:39:57 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16768 boxname=wulflinc25 idbench=1290 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6ffc4ed72f4dd993b121ae0a2045731e  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-dcmulti.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-dcmulti.opb /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-dcmulti.opb
IDLAUNCH: 16768
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.220
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.220
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:        801012 kB
Buffers:         22388 kB
Cached:         190944 kB
SwapCached:        732 kB
Active:          40248 kB
Inactive:       175060 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        800760 kB
SwapTotal:     2097892 kB
SwapFree:      2096248 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5024 kB
Slab:            12464 kB
Committed_AS:    63576 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 06:00:00 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 16768 7 1200.34 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |  342763   915134 |  102828       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/104762          
c   -- var.elim.:  2000/104762          
c   -- var.elim.:  3000/104762          
c   -- var.elim.:  4000/104762          
c   -- var.elim.:  5000/104762          
c   -- var.elim.:  6000/104762          
c   -- var.elim.:  7000/104762          
c   -- var.elim.:  8000/104762          
c   -- var.elim.:  9000/104762          
c   -- var.elim.:  10000/104762          
c   -- var.elim.:  11000/104762          
c   -- var.elim.:  12000/104762          
c   -- var.elim.:  13000/104762          
c   -- var.elim.:  14000/104762          
c   -- var.elim.:  15000/104762          
c   -- var.elim.:  16000/104762          
c   -- var.elim.:  17000/104762          
c   -- var.elim.:  18000/104762          
c   -- var.elim.:  19000/104762          
c   -- var.elim.:  20000/104762          
c   -- var.elim.:  21000/104762          
c   -- var.elim.:  22000/104762          
c   -- var.elim.:  23000/104762          
c   -- var.elim.:  24000/104762          
c   -- var.elim.:  25000/104762          
c   -- var.elim.:  26000/104762          
c   -- var.elim.:  27000/104762          
c   -- var.elim.:  28000/104762          
c   -- var.elim.:  29000/104762          
c   -- var.elim.:  30000/104762          
c   -- var.elim.:  31000/104762          
c   -- var.elim.:  32000/104762          
c   -- var.elim.:  33000/104762          
c   -- var.elim.:  34000/104762          
c   -- var.elim.:  35000/104762          
c   -- var.elim.:  36000/104762          
c   -- var.elim.:  37000/104762          
c   -- var.elim.:  38000/104762          
c   -- var.elim.:  39000/104762          
c   -- var.elim.:  40000/104762          
c   -- var.elim.:  41000/104762          
c   -- var.elim.:  42000/104762          
c   -- var.elim.:  43000/104762          
c   -- var.elim.:  44000/104762          
c   -- var.elim.:  45000/104762          
c   -- var.elim.:  46000/104762          
c   -- var.elim.:  47000/104762          
c   -- var.elim.:  48000/104762          
c   -- var.elim.:  49000/104762          
c   -- var.elim.:  50000/104762          
c   -- var.elim.:  51000/104762          
c   -- var.elim.:  52000/104762          
c   -- var.elim.:  53000/104762          
c   -- var.elim.:  54000/104762          
c   -- var.elim.:  55000/104762          
c   -- var.elim.:  56000/104762          
c   -- var.elim.:  57000/104762          
c   -- var.elim.:  58000/104762          
c   -- var.elim.:  59000/104762          
c   -- var.elim.:  60000/104762          
c   -- var.elim.:  61000/104762          
c   -- var.elim.:  62000/104762          
c   -- var.elim.:  63000/104762          
c   -- var.elim.:  64000/104762          
c   -- var.elim.:  65000/104762          
c   -- var.elim.:  66000/104762          
c   -- var.elim.:  67000/104762          
c   -- var.elim.:  68000/104762          
c   -- var.elim.:  69000/104762          
c   -- var.elim.:  70000/104762          
c   -- var.elim.:  71000/104762          
c   -- var.elim.:  72000/104762          
c   -- var.elim.:  73000/104762          
c   -- var.elim.:  74000/104762          
c   -- var.elim.:  75000/104762          
c   -- var.elim.:  76000/104762          
c   -- var.elim.:  77000/104762          
c   -- var.elim.:  78000/104762          
c   -- var.elim.:  79000/104762          
c   -- var.elim.:  80000/104762          
c   -- var.elim.:  81000/104762          
c   -- var.elim.:  82000/104762          
c   -- var.elim.:  83000/104762          
c   -- var.elim.:  84000/104762          
c   -- var.elim.:  85000/104762          
c   -- var.elim.:  86000/104762          
c   -- var.elim.:  87000/104762          
c   -- var.elim.:  88000/104762          
c   -- var.elim.:  89000/104762          
c   -- var.elim.:  90000/104762          
c   -- var.elim.:  91000/104762          
c   -- var.elim.:  92000/104762          
c   -- var.elim.:  93000/104762          
c   -- var.elim.:  94000/104762          
c   -- var.elim.:  95000/104762          
c   -- var.elim.:  96000/104762          
c   -- var.elim.:  97000/104762          
c   -- var.elim.:  98000/104762          
c   -- var.elim.:  99000/104762          
c   -- var.elim.:  100000/104762          
c   -- var.elim.:  101000/104762          
c   -- var.elim.:  102000/104762          
c   -- var.elim.:  103000/104762          
c   -- var.elim.:  104000/104762          
c   -- var.elim.:  104762/104762          
c   -- var.elim.:  1000/51307          
c   -- var.elim.:  2000/51307          
c   -- var.elim.:  3000/51307          
c   -- var.elim.:  4000/51307          
c   -- var.elim.:  5000/51307          
c   -- var.elim.:  6000/51307          
c   -- var.elim.:  7000/51307          
c   -- var.elim.:  8000/51307          
c   -- var.elim.:  9000/51307          
c   -- var.elim.:  10000/51307          
c   -- var.elim.:  11000/51307          
c   -- var.elim.:  12000/51307          
c   -- var.elim.:  13000/51307          
c   -- var.elim.:  14000/51307          
c   -- var.elim.:  15000/51307          
c   -- var.elim.:  16000/51307          
c   -- var.elim.:  17000/51307          
c   -- var.elim.:  18000/51307          
c   -- var.elim.:  19000/51307          
c   -- var.elim.:  20000/51307          
c   -- var.elim.:  21000/51307          
c   -- var.elim.:  22000/51307          
c   -- var.elim.:  23000/51307          
c   -- var.elim.:  24000/51307          
c   -- var.elim.:  25000/51307          
c   -- var.elim.:  26000/51307          
c   -- var.elim.:  27000/51307          
c   -- var.elim.:  28000/51307          
c   -- var.elim.:  29000/51307          
c   -- var.elim.:  30000/51307          
c   -- var.elim.:  31000/51307          
c   -- var.elim.:  32000/51307          
c   -- var.elim.:  33000/51307          
c   -- var.elim.:  34000/51307          
c   -- var.elim.:  35000/51307          
c   -- var.elim.:  36000/51307          
c   -- var.elim.:  37000/51307          
c   -- var.elim.:  38000/51307          
c   -- var.eli#### 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.73 0.91 0.90 2/54 30104
Raw data (stat): 30104 (runsolver) R 30103 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 542640338 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0006 s]
Raw data (loadavg): 0.77 0.91 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 17479 0 0 0 948 50 0 0 25 0 1 0 542640338 74272768 16541 4294967295 134512640 134672761 3221224544 3221223040 134639295 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18133 16541 603 41 0 18092 0
vsize: 72532
[startup+20.001 s]
Raw data (loadavg): 0.80 0.91 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 19388 0 0 0 1940 58 0 0 25 0 1 0 542640338 73461760 16354 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17935 16354 603 41 0 17894 0
vsize: 71740
[startup+30.0003 s]
Raw data (loadavg): 0.83 0.91 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 19451 0 0 0 2940 58 0 0 25 0 1 0 542640338 73723904 16417 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17999 16417 603 41 0 17958 0
vsize: 71996
[startup+40.0002 s]
Raw data (loadavg): 0.86 0.92 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 19456 0 0 0 3940 58 0 0 25 0 1 0 542640338 73723904 16422 4294967295 134512640 134672761 3221224544 3221223728 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17999 16422 603 41 0 17958 0
vsize: 71996
[startup+50.0008 s]
Raw data (loadavg): 0.88 0.92 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 19762 0 0 0 4939 59 0 0 25 0 1 0 542640338 75063296 16728 4294967295 134512640 134672761 3221224544 3221223744 134610783 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18326 16728 603 41 0 18285 0
vsize: 73304
[startup+60.0011 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 20202 0 0 0 5938 60 0 0 25 0 1 0 542640338 76906496 17168 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18776 17168 603 41 0 18735 0
vsize: 75104
[startup+70.0012 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 20634 0 0 0 6937 62 0 0 25 0 1 0 542640338 78618624 17600 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19194 17600 603 41 0 19153 0
vsize: 76776
[startup+80.0013 s]
Raw data (loadavg): 0.93 0.92 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 21079 0 0 0 7936 63 0 0 25 0 1 0 542640338 80470016 18045 4294967295 134512640 134672761 3221224544 3221223680 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19646 18045 603 41 0 19605 0
vsize: 78584
[startup+90.0012 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 21794 0 0 0 8934 65 0 0 25 0 1 0 542640338 83361792 18760 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20352 18760 603 41 0 20311 0
vsize: 81408
[startup+100.001 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 22579 0 0 0 9932 67 0 0 25 0 1 0 542640338 86544384 19545 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21129 19545 603 41 0 21088 0
vsize: 84516
[startup+110.001 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 23182 0 0 0 10930 69 0 0 25 0 1 0 542640338 89190400 20148 4294967295 134512640 134672761 3221224544 3221223728 134615838 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21775 20148 603 41 0 21734 0
vsize: 87100
[startup+120.001 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 24097 0 0 0 11928 72 0 0 25 0 1 0 542640338 92889088 21063 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22678 21063 603 41 0 22637 0
vsize: 90712
[startup+130.001 s]
Raw data (loadavg): 0.97 0.93 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 24530 0 0 0 12927 73 0 0 25 0 1 0 542640338 94732288 21496 4294967295 134512640 134672761 3221224544 3221223728 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23128 21496 603 41 0 23087 0
vsize: 92512
[startup+140.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 24926 0 0 0 13926 74 0 0 25 0 1 0 542640338 96337920 21892 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23520 21892 603 41 0 23479 0
vsize: 94080
[startup+150.001 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 25467 0 0 0 14924 76 0 0 25 0 1 0 542640338 98455552 22433 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24037 22433 603 41 0 23996 0
vsize: 96148
[startup+160.001 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 26095 0 0 0 15923 77 0 0 25 0 1 0 542640338 101089280 23061 4294967295 134512640 134672761 3221224544 3221223728 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24680 23061 603 41 0 24639 0
vsize: 98720
[startup+170.002 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 26648 0 0 0 16922 79 0 0 25 0 1 0 542640338 103321600 23614 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25225 23614 603 41 0 25184 0
vsize: 100900
[startup+180.002 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 27398 0 0 0 17919 82 0 0 25 0 1 0 542640338 106352640 24364 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25965 24364 603 41 0 25924 0
vsize: 103860
[startup+190.002 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 27863 0 0 0 18918 83 0 0 25 0 1 0 542640338 108204032 24829 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26417 24829 603 41 0 26376 0
vsize: 105668
[startup+200.002 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 28421 0 0 0 19917 85 0 0 25 0 1 0 542640338 110575616 25387 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26996 25387 603 41 0 26955 0
vsize: 107984
[startup+210.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 29076 0 0 0 20915 87 0 0 25 0 1 0 542640338 113217536 26042 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27641 26042 603 41 0 27600 0
vsize: 110564
[startup+220.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 29687 0 0 0 21913 89 0 0 25 0 1 0 542640338 115728384 26653 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28254 26653 603 41 0 28213 0
vsize: 113016
[startup+230.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 29953 0 0 0 22912 90 0 0 25 0 1 0 542640338 116785152 26919 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28512 26919 603 41 0 28471 0
vsize: 114048
[startup+240.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 30388 0 0 0 23910 92 0 0 25 0 1 0 542640338 119021568 27354 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29058 27354 603 41 0 29017 0
vsize: 116232
[startup+250.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 30736 0 0 0 24910 93 0 0 25 0 1 0 542640338 120471552 27702 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29412 27702 603 41 0 29371 0
vsize: 117648
[startup+260.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 31065 0 0 0 25909 93 0 0 25 0 1 0 542640338 121794560 28031 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29735 28031 603 41 0 29694 0
vsize: 118940
[startup+270.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 31587 0 0 0 26908 95 0 0 25 0 1 0 542640338 123899904 28553 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30249 28553 603 41 0 30208 0
vsize: 120996
[startup+280.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 32021 0 0 0 27906 96 0 0 25 0 1 0 542640338 125620224 28987 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30669 28987 603 41 0 30628 0
vsize: 122676
[startup+290.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 32518 0 0 0 28906 97 0 0 25 0 1 0 542640338 127746048 29484 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31188 29484 603 41 0 31147 0
vsize: 124752
[startup+300.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 33375 0 0 0 29904 99 0 0 25 0 1 0 542640338 131178496 30341 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32026 30341 603 41 0 31985 0
vsize: 128104
[startup+310.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 34230 0 0 0 30902 102 0 0 25 0 1 0 542640338 134610944 31196 4294967295 134512640 134672761 3221224544 3221223728 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32864 31196 603 41 0 32823 0
vsize: 131456
[startup+320.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 34814 0 0 0 31901 103 0 0 25 0 1 0 542640338 137007104 31780 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33449 31780 603 41 0 33408 0
vsize: 133796
[startup+330.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 35112 0 0 0 32900 104 0 0 25 0 1 0 542640338 138199040 32078 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33740 32078 603 41 0 33699 0
vsize: 134960
[startup+340.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 35464 0 0 0 33899 105 0 0 25 0 1 0 542640338 139661312 32430 4294967295 134512640 134672761 3221224544 3221223728 134615843 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34097 32430 603 41 0 34056 0
vsize: 136388
[startup+350.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 36049 0 0 0 34897 108 0 0 25 0 1 0 542640338 142049280 33015 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34680 33015 603 41 0 34639 0
vsize: 138720
[startup+360.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 36624 0 0 0 35895 109 0 0 25 0 1 0 542640338 144445440 33590 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35265 33590 603 41 0 35224 0
vsize: 141060
[startup+370.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 36896 0 0 0 36895 110 0 0 25 0 1 0 542640338 145510400 33862 4294967295 134512640 134672761 3221224544 3221223688 134616170 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35525 33862 603 41 0 35484 0
vsize: 142100
[startup+380.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 37054 0 0 0 37894 110 0 0 25 0 1 0 542640338 146051072 34020 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35657 34020 603 41 0 35616 0
vsize: 142628
[startup+390.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 37466 0 0 0 38893 112 0 0 25 0 1 0 542640338 147767296 34432 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36076 34432 603 41 0 36035 0
vsize: 144304
[startup+400.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 37992 0 0 0 39891 114 0 0 25 0 1 0 542640338 149880832 34958 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36592 34958 603 41 0 36551 0
vsize: 146368
[startup+410.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 38585 0 0 0 40890 115 0 0 25 0 1 0 542640338 152387584 35551 4294967295 134512640 134672761 3221224544 3221223584 134614280 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37204 35551 603 41 0 37163 0
vsize: 148816
[startup+420.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 39117 0 0 0 41889 117 0 0 25 0 1 0 542640338 154501120 36083 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37720 36083 603 41 0 37679 0
vsize: 150880
[startup+430.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 39570 0 0 0 42888 118 0 0 25 0 1 0 542640338 156340224 36536 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38169 36536 603 41 0 38128 0
vsize: 152676
[startup+440.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 39858 0 0 0 43887 119 0 0 25 0 1 0 542640338 157528064 36824 4294967295 134512640 134672761 3221224544 3221223688 134616347 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38459 36824 603 41 0 38418 0
vsize: 153836
[startup+450.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 40020 0 0 0 44887 119 0 0 25 0 1 0 542640338 158187520 36986 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38620 36986 603 41 0 38579 0
vsize: 154480
[startup+460.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 40203 0 0 0 45887 120 0 0 25 0 1 0 542640338 158859264 37169 4294967295 134512640 134672761 3221224544 3221223688 134616317 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38784 37169 603 41 0 38743 0
vsize: 155136
[startup+470.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 40484 0 0 0 46886 120 0 0 25 0 1 0 542640338 160063488 37450 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39078 37450 603 41 0 39037 0
vsize: 156312
[startup+480.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 40823 0 0 0 47885 122 0 0 25 0 1 0 542640338 161419264 37789 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39409 37789 603 41 0 39368 0
vsize: 157636
[startup+490.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 41292 0 0 0 48884 123 0 0 25 0 1 0 542640338 163401728 38258 4294967295 134512640 134672761 3221224544 3221223584 134612799 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39893 38258 603 41 0 39852 0
vsize: 159572
[startup+500.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 41694 0 0 0 49883 124 0 0 25 0 1 0 542640338 164995072 38660 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40282 38660 603 41 0 40241 0
vsize: 161128
[startup+510.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 41976 0 0 0 50883 125 0 0 25 0 1 0 542640338 166060032 38942 4294967295 134512640 134672761 3221224544 3221223708 134564515 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40542 38942 603 41 0 40501 0
vsize: 162168
[startup+520.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 42297 0 0 0 51882 126 0 0 25 0 1 0 542640338 167378944 39263 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40864 39263 603 41 0 40823 0
vsize: 163456
[startup+530.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 42538 0 0 0 52881 126 0 0 25 0 1 0 542640338 168448000 39504 4294967295 134512640 134672761 3221224544 3221223584 134614333 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41125 39504 603 41 0 41084 0
vsize: 164500
[startup+540.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 42845 0 0 0 53881 127 0 0 25 0 1 0 542640338 169631744 39811 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41414 39811 603 41 0 41373 0
vsize: 165656
[startup+550.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 43156 0 0 0 54880 128 0 0 25 0 1 0 542640338 170954752 40122 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41737 40122 603 41 0 41696 0
vsize: 166948
[startup+560.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 43441 0 0 0 55879 129 0 0 25 0 1 0 542640338 173056000 40407 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42250 40407 603 41 0 42209 0
vsize: 169000
[startup+570.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 43622 0 0 0 56879 130 0 0 25 0 1 0 542640338 173858816 40588 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 42446 40588 603 41 0 42405 0
vsize: 169784
[startup+580.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 44285 0 0 0 57877 132 0 0 25 0 1 0 542640338 176500736 41251 4294967295 134512640 134672761 3221224544 3221223744 134610681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43091 41251 603 41 0 43050 0
vsize: 172364
[startup+590.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 45028 0 0 0 58875 134 0 0 25 0 1 0 542640338 179523584 41994 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 43829 41994 603 41 0 43788 0
vsize: 175316
[startup+600.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 45730 0 0 0 59873 136 0 0 25 0 1 0 542640338 182435840 42696 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44540 42696 603 41 0 44499 0
vsize: 178160
[startup+610.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 46038 0 0 0 60873 137 0 0 25 0 1 0 542640338 183631872 43004 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 44832 43004 603 41 0 44791 0
vsize: 179328
[startup+620.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 46361 0 0 0 61872 137 0 0 25 0 1 0 542640338 184979456 43327 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45161 43327 603 41 0 45120 0
vsize: 180644
[startup+630.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 46709 0 0 0 62871 138 0 0 25 0 1 0 542640338 186421248 43675 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45513 43675 603 41 0 45472 0
vsize: 182052
[startup+640.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 46931 0 0 0 63871 139 0 0 25 0 1 0 542640338 187342848 43897 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45738 43897 603 41 0 45697 0
vsize: 182952
[startup+650.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 47185 0 0 0 64870 140 0 0 25 0 1 0 542640338 188395520 44151 4294967295 134512640 134672761 3221224544 3221223688 134616336 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 45995 44151 603 41 0 45954 0
vsize: 183980
[startup+660.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 47309 0 0 0 65870 140 0 0 25 0 1 0 542640338 188809216 44275 4294967295 134512640 134672761 3221224544 3221223688 134616247 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46096 44275 603 41 0 46055 0
vsize: 184384
[startup+670.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 47539 0 0 0 66870 141 0 0 25 0 1 0 542640338 189743104 44505 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46324 44505 603 41 0 46283 0
vsize: 185296
[startup+680.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 47998 0 0 0 67869 141 0 0 25 0 1 0 542640338 191594496 44964 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 46776 44964 603 41 0 46735 0
vsize: 187104
[startup+690.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 48421 0 0 0 68868 143 0 0 25 0 1 0 542640338 193318912 45387 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47197 45387 603 41 0 47156 0
vsize: 188788
[startup+700.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 48703 0 0 0 69868 143 0 0 25 0 1 0 542640338 194543616 45669 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47496 45669 603 41 0 47455 0
vsize: 189984
[startup+710.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 48828 0 0 0 70868 143 0 0 25 0 1 0 542640338 195088384 45794 4294967295 134512640 134672761 3221224544 3221223356 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47629 45794 603 41 0 47588 0
vsize: 190516
[startup+720.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 49069 0 0 0 71867 144 0 0 25 0 1 0 542640338 196022272 46035 4294967295 134512640 134672761 3221224544 3221223744 134617686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 47857 46035 603 41 0 47816 0
vsize: 191428
[startup+730.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 49322 0 0 0 72867 145 0 0 25 0 1 0 542640338 197079040 46288 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48115 46288 603 41 0 48074 0
vsize: 192460
[startup+740.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 49741 0 0 0 73866 146 0 0 25 0 1 0 542640338 198791168 46707 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48533 46707 603 41 0 48492 0
vsize: 194132
[startup+750.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 49982 0 0 0 74866 146 0 0 25 0 1 0 542640338 199708672 46948 4294967295 134512640 134672761 3221224544 3221223688 134616293 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 48757 46948 603 41 0 48716 0
vsize: 195028
[startup+760.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 50300 0 0 0 75865 147 0 0 25 0 1 0 542640338 201031680 47266 4294967295 134512640 134672761 3221224544 3221223688 134616181 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49080 47266 603 41 0 49039 0
vsize: 196320
[startup+770.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 50628 0 0 0 76864 149 0 0 25 0 1 0 542640338 202354688 47594 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49403 47594 603 41 0 49362 0
vsize: 197612
[startup+780.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 51157 0 0 0 77862 151 0 0 25 0 1 0 542640338 204591104 48123 4294967295 134512640 134672761 3221224544 3221223728 134615643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 49949 48123 603 41 0 49908 0
vsize: 199796
[startup+790.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 51566 0 0 0 78861 151 0 0 25 0 1 0 542640338 206176256 48532 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50336 48532 603 41 0 50295 0
vsize: 201344
[startup+800.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 51971 0 0 0 79860 153 0 0 25 0 1 0 542640338 207888384 48937 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 50754 48937 603 41 0 50713 0
vsize: 203016
[startup+810.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 52328 0 0 0 80860 153 0 0 25 0 1 0 542640338 209330176 49294 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51106 49294 603 41 0 51065 0
vsize: 204424
[startup+820.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 52694 0 0 0 81860 154 0 0 25 0 1 0 542640338 210788352 49660 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51462 49660 603 41 0 51421 0
vsize: 205848
[startup+830.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 52910 0 0 0 82860 154 0 0 25 0 1 0 542640338 211714048 49876 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51688 49876 603 41 0 51647 0
vsize: 206752
[startup+840.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 53160 0 0 0 83859 155 0 0 25 0 1 0 542640338 212668416 50126 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 51921 50126 603 41 0 51880 0
vsize: 207684
[startup+850.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 53462 0 0 0 84858 155 0 0 25 0 1 0 542640338 213991424 50428 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52244 50428 603 41 0 52203 0
vsize: 208976
[startup+860.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 53808 0 0 0 85858 156 0 0 25 0 1 0 542640338 215318528 50774 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52568 50774 603 41 0 52527 0
vsize: 210272
[startup+870.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 54208 0 0 0 86857 157 0 0 25 0 1 0 542640338 216911872 51174 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 52957 51174 603 41 0 52916 0
vsize: 211828
[startup+880.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 54557 0 0 0 87856 158 0 0 25 0 1 0 542640338 218370048 51523 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53313 51523 603 41 0 53272 0
vsize: 213252
[startup+890.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 54944 0 0 0 88855 159 0 0 25 0 1 0 542640338 219959296 51910 4294967295 134512640 134672761 3221224544 3221223728 134615611 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53701 51910 603 41 0 53660 0
vsize: 214804
[startup+900.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 55112 0 0 0 89855 159 0 0 25 0 1 0 542640338 220622848 52078 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 53863 52078 603 41 0 53822 0
vsize: 215452
[startup+910.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 55397 0 0 0 90855 160 0 0 25 0 1 0 542640338 221859840 52363 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54165 52363 603 41 0 54124 0
vsize: 216660
[startup+920.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 55586 0 0 0 91854 161 0 0 25 0 1 0 542640338 222658560 52552 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54360 52552 603 41 0 54319 0
vsize: 217440
[startup+930.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 55708 0 0 0 92854 161 0 0 25 0 1 0 542640338 223195136 52674 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54491 52674 603 41 0 54450 0
vsize: 217964
[startup+940.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 55973 0 0 0 93854 162 0 0 25 0 1 0 542640338 224206848 52939 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54738 52939 603 41 0 54697 0
vsize: 218952
[startup+950.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 56089 0 0 0 94854 162 0 0 25 0 1 0 542640338 224735232 53055 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54867 53055 603 41 0 54826 0
vsize: 219468
[startup+960.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 56196 0 0 0 95854 162 0 0 25 0 1 0 542640338 225263616 53162 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 54996 53162 603 41 0 54955 0
vsize: 219984
[startup+970.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 56530 0 0 0 96853 163 0 0 25 0 1 0 542640338 226582528 53496 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55318 53496 603 41 0 55277 0
vsize: 221272
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 56935 0 0 0 97852 164 0 0 25 0 1 0 542640338 228286464 53901 4294967295 134512640 134672761 3221224544 3221223536 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 55734 53901 603 41 0 55693 0
vsize: 222936
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 57314 0 0 0 98851 165 0 0 25 0 1 0 542640338 229732352 54280 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56087 54280 603 41 0 56046 0
vsize: 224348
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 57708 0 0 0 99851 166 0 0 25 0 1 0 542640338 231440384 54674 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56504 54674 603 41 0 56463 0
vsize: 226016
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 58132 0 0 0 100850 167 0 0 25 0 1 0 542640338 233152512 55098 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 56922 55098 603 41 0 56881 0
vsize: 227688
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 58479 0 0 0 101849 168 0 0 25 0 1 0 542640338 234483712 55445 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57247 55445 603 41 0 57206 0
vsize: 228988
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 58806 0 0 0 102848 169 0 0 25 0 1 0 542640338 235802624 55772 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57569 55772 603 41 0 57528 0
vsize: 230276
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 59062 0 0 0 103847 170 0 0 25 0 1 0 542640338 236855296 56028 4294967295 134512640 134672761 3221224544 3221223688 134616296 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57826 56028 603 41 0 57785 0
vsize: 231304
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 59208 0 0 0 104847 171 0 0 25 0 1 0 542640338 237514752 56174 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 57987 56174 603 41 0 57946 0
vsize: 231948
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 59479 0 0 0 105846 172 0 0 25 0 1 0 542640338 238579712 56445 4294967295 134512640 134672761 3221224544 3221223584 134614346 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58247 56445 603 41 0 58206 0
vsize: 232988
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 59754 0 0 0 106845 173 0 0 25 0 1 0 542640338 239640576 56720 4294967295 134512640 134672761 3221224544 3221223688 134616261 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58506 56720 603 41 0 58465 0
vsize: 234024
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 59854 0 0 0 107845 174 0 0 25 0 1 0 542640338 240046080 56820 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58605 56820 603 41 0 58564 0
vsize: 234420
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 59976 0 0 0 108845 174 0 0 25 0 1 0 542640338 240611328 56942 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 58743 56942 603 41 0 58702 0
vsize: 234972
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 60236 0 0 0 109844 175 0 0 25 0 1 0 542640338 241668096 57202 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59001 57202 603 41 0 58960 0
vsize: 236004
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 60570 0 0 0 110843 176 0 0 25 0 1 0 542640338 242991104 57536 4294967295 134512640 134672761 3221224544 3221223728 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59324 57536 603 41 0 59283 0
vsize: 237296
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 60830 0 0 0 111843 177 0 0 25 0 1 0 542640338 244047872 57796 4294967295 134512640 134672761 3221224544 3221223688 134616123 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59582 57796 603 41 0 59541 0
vsize: 238328
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 61092 0 0 0 112841 178 0 0 25 0 1 0 542640338 245108736 58058 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 59841 58058 603 41 0 59800 0
vsize: 239364
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 61454 0 0 0 113841 179 0 0 25 0 1 0 542640338 246566912 58420 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60197 58420 603 41 0 60156 0
vsize: 240788
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 61895 0 0 0 114840 180 0 0 25 0 1 0 542640338 248401920 58861 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 60645 58861 603 41 0 60604 0
vsize: 242580
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 62359 0 0 0 115838 182 0 0 25 0 1 0 542640338 250261504 59325 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61099 59325 603 41 0 61058 0
vsize: 244396
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 62716 0 0 0 116837 183 0 0 25 0 1 0 542640338 251707392 59682 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61452 59682 603 41 0 61411 0
vsize: 245808
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 62815 0 0 0 117837 183 0 0 25 0 1 0 542640338 252125184 59781 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61554 59781 603 41 0 61513 0
vsize: 246216
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 63171 0 0 0 118837 184 0 0 25 0 1 0 542640338 253579264 60137 4294967295 134512640 134672761 3221224544 3221223728 134615998 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 61909 60137 603 41 0 61868 0
vsize: 247636
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30104
Raw data (stat): 30104 (minisat+) R 30103 28099 28098 0 -1 0 63368 0 0 0 119836 185 0 0 25 0 1 0 542640338 254418944 60334 4294967295 134512640 134672761 3221224544 3221223688 134616356 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 62114 60334 603 41 0 62073 0
vsize: 248456
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.14 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30104
Raw data (stat): 30104 (minisat+) Z 30103 28099 28098 0 -1 12 63368 0 0 0 119837 197 0 0 25 0 1 0 542640338 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.14
CPU time (s): 1200.34
CPU user time (s): 1198.37
CPU system time (s): 1.9737
CPU usage (%): 100.017
Max. virtual memory (Kb): 248456
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####