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 15188

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc23 THE 2005-04-21 03:18:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18289 boxname=wulflinc23 idbench=1407 idsolver=11 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  28123830d5f7e3646d18978bb347487c  /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-dcmulti.opb
REAL COMMAND:  minisat+ -S /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-dcmulti.opb /oldhome/oroussel/tmp/wulflinc23/normalized-mps-v2-13-7-dcmulti.opb
IDLAUNCH: 18289
/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:        750964 kB
Buffers:         16300 kB
Cached:         238248 kB
SwapCached:        520 kB
Active:          55540 kB
Inactive:       201080 kB
HighTotal:      131008 kB
HighFree:          784 kB
LowTotal:       903652 kB
LowFree:        750180 kB
SwapTotal:     2097136 kB
SwapFree:      2095824 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5220 kB
Slab:            21476 kB
Committed_AS:    63584 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 03:38:24 (client local time) WITH STATUS 0 IN 1200.34 SECONDS
stats: 18289 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.92 0.95 0.90 2/54 27884
Raw data (stat): 27884 (runsolver) R 27883 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 541779631 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+9.99997 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 17479 0 0 0 945 53 0 0 25 0 1 0 541779631 74272768 16541 4294967295 134512640 134672761 3221224544 3221222992 134643948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18133 16541 603 41 0 18092 0
vsize: 72532
[startup+20.0002 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 19388 0 0 0 1938 60 0 0 25 0 1 0 541779631 73461760 16354 4294967295 134512640 134672761 3221224544 3221223728 134615585 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.95 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 19451 0 0 0 2938 61 0 0 25 0 1 0 541779631 73723904 16417 4294967295 134512640 134672761 3221224544 3221223696 134565092 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.0009 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 19456 0 0 0 3938 61 0 0 25 0 1 0 541779631 73723904 16422 4294967295 134512640 134672761 3221224544 3221223728 134615705 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.0086 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 19753 0 0 0 4938 62 0 0 25 0 1 0 541779631 74928128 16719 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18293 16719 603 41 0 18252 0
vsize: 73172
[startup+60.0078 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 20164 0 0 0 5936 63 0 0 25 0 1 0 541779631 76775424 17130 4294967295 134512640 134672761 3221224544 3221223728 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18744 17130 603 41 0 18703 0
vsize: 74976
[startup+70.0109 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 20531 0 0 0 6935 65 0 0 25 0 1 0 541779631 78225408 17497 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19098 17497 603 41 0 19057 0
vsize: 76392
[startup+80.0115 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 20975 0 0 0 7933 67 0 0 25 0 1 0 541779631 80068608 17941 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19548 17941 603 41 0 19507 0
vsize: 78192
[startup+90.0118 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 21668 0 0 0 8930 69 0 0 25 0 1 0 541779631 82837504 18634 4294967295 134512640 134672761 3221224544 3221223728 134615676 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20224 18634 603 41 0 20183 0
vsize: 80896
[startup+100.012 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 22447 0 0 0 9928 72 0 0 25 0 1 0 541779631 86003712 19413 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20997 19413 603 41 0 20956 0
vsize: 83988
[startup+110.013 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 23102 0 0 0 10927 73 0 0 25 0 1 0 541779631 88928256 20068 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21711 20068 603 41 0 21670 0
vsize: 86844
[startup+120.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 23987 0 0 0 11924 76 0 0 25 0 1 0 541779631 92491776 20953 4294967295 134512640 134672761 3221224544 3221223536 134603141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22581 20953 603 41 0 22540 0
vsize: 90324
[startup+130.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 24414 0 0 0 12922 78 0 0 25 0 1 0 541779631 94203904 21380 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22999 21380 603 41 0 22958 0
vsize: 91996
[startup+140.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 24829 0 0 0 13921 80 0 0 25 0 1 0 541779631 95936512 21795 4294967295 134512640 134672761 3221224544 3221223688 134616139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23422 21795 603 41 0 23381 0
vsize: 93688
[startup+150.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 25372 0 0 0 14919 81 0 0 25 0 1 0 541779631 98058240 22338 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23940 22338 603 41 0 23899 0
vsize: 95760
[startup+160.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 25816 0 0 0 15918 82 0 0 25 0 1 0 541779631 99901440 22782 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24390 22782 603 41 0 24349 0
vsize: 97560
[startup+170.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 26495 0 0 0 16916 85 0 0 25 0 1 0 541779631 102666240 23461 4294967295 134512640 134672761 3221224544 3221223680 134614488 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25065 23461 603 41 0 25024 0
vsize: 100260
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 27057 0 0 0 17913 87 0 0 25 0 1 0 541779631 104902656 24023 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25611 24023 603 41 0 25570 0
vsize: 102444
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 27752 0 0 0 18913 88 0 0 25 0 1 0 541779631 107802624 24718 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26319 24718 603 41 0 26278 0
vsize: 105276
[startup+200.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 28143 0 0 0 19911 90 0 0 25 0 1 0 541779631 109387776 25109 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26706 25109 603 41 0 26665 0
vsize: 106824
[startup+210.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 28759 0 0 0 20908 93 0 0 25 0 1 0 541779631 111902720 25725 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27320 25725 603 41 0 27279 0
vsize: 109280
[startup+220.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 29410 0 0 0 21906 95 0 0 25 0 1 0 541779631 114536448 26376 4294967295 134512640 134672761 3221224544 3221223728 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27963 26376 603 41 0 27922 0
vsize: 111852
[startup+230.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 29835 0 0 0 22905 97 0 0 25 0 1 0 541779631 116260864 26801 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28384 26801 603 41 0 28343 0
vsize: 113536
[startup+240.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 30129 0 0 0 23903 98 0 0 25 0 1 0 541779631 117972992 27095 4294967295 134512640 134672761 3221224544 3221223700 134614480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28802 27095 603 41 0 28761 0
vsize: 115208
[startup+250.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 30538 0 0 0 24902 100 0 0 25 0 1 0 541779631 119685120 27504 4294967295 134512640 134672761 3221224544 3221223696 134565051 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29220 27504 603 41 0 29179 0
vsize: 116880
[startup+260.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 30932 0 0 0 25901 101 0 0 25 0 1 0 541779631 121266176 27898 4294967295 134512640 134672761 3221224544 3221223688 134616178 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29606 27898 603 41 0 29565 0
vsize: 118424
[startup+270.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 31308 0 0 0 26900 102 0 0 25 0 1 0 541779631 122716160 28274 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29960 28274 603 41 0 29919 0
vsize: 119840
[startup+280.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 31819 0 0 0 27899 103 0 0 25 0 1 0 541779631 124821504 28785 4294967295 134512640 134672761 3221224544 3221223728 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30474 28785 603 41 0 30433 0
vsize: 121896
[startup+290.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 32129 0 0 0 28897 105 0 0 25 0 1 0 541779631 126156800 29095 4294967295 134512640 134672761 3221224544 3221223688 134616183 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30800 29095 603 41 0 30759 0
vsize: 123200
[startup+300.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 32876 0 0 0 29896 107 0 0 25 0 1 0 541779631 129196032 29842 4294967295 134512640 134672761 3221224544 3221223536 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31542 29842 603 41 0 31501 0
vsize: 126168
[startup+310.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 33630 0 0 0 30894 109 0 0 25 0 1 0 541779631 132235264 30596 4294967295 134512640 134672761 3221224544 3221223728 134616023 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32284 30596 603 41 0 32243 0
vsize: 129136
[startup+320.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 34393 0 0 0 31891 112 0 0 25 0 1 0 541779631 135278592 31359 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33027 31359 603 41 0 32986 0
vsize: 132108
[startup+330.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 34873 0 0 0 32890 113 0 0 25 0 1 0 541779631 137277440 31839 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33515 31839 603 41 0 33474 0
vsize: 134060
[startup+340.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 35191 0 0 0 33890 113 0 0 25 0 1 0 541779631 138600448 32157 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33838 32157 603 41 0 33797 0
vsize: 135352
[startup+350.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 35523 0 0 0 34889 114 0 0 25 0 1 0 541779631 139923456 32489 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34161 32489 603 41 0 34120 0
vsize: 136644
[startup+360.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 36114 0 0 0 35888 115 0 0 25 0 1 0 541779631 142319616 33080 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 34746 33080 603 41 0 34705 0
vsize: 138984
[startup+370.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 36671 0 0 0 36887 117 0 0 25 0 1 0 541779631 144576512 33637 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35297 33637 603 41 0 35256 0
vsize: 141188
[startup+380.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 36896 0 0 0 37886 118 0 0 25 0 1 0 541779631 145510400 33862 4294967295 134512640 134672761 3221224544 3221223688 134616339 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35525 33862 603 41 0 35484 0
vsize: 142100
[startup+390.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 37049 0 0 0 38886 118 0 0 25 0 1 0 541779631 146051072 34015 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 35657 34015 603 41 0 35616 0
vsize: 142628
[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 37433 0 0 0 39886 119 0 0 25 0 1 0 541779631 147636224 34399 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36044 34399 603 41 0 36003 0
vsize: 144176
[startup+410.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 37919 0 0 0 40885 120 0 0 25 0 1 0 541779631 149618688 34885 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 36528 34885 603 41 0 36487 0
vsize: 146112
[startup+420.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 38485 0 0 0 41884 122 0 0 25 0 1 0 541779631 151994368 35451 4294967295 134512640 134672761 3221224544 3221223376 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37108 35451 603 41 0 37067 0
vsize: 148432
[startup+430.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 39023 0 0 0 42882 124 0 0 25 0 1 0 541779631 154103808 35989 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 37623 35989 603 41 0 37582 0
vsize: 150492
[startup+440.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 39465 0 0 0 43881 125 0 0 25 0 1 0 541779631 155942912 36431 4294967295 134512640 134672761 3221224544 3221223728 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38072 36431 603 41 0 38031 0
vsize: 152288
[startup+450.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 39776 0 0 0 44880 125 0 0 25 0 1 0 541779631 157134848 36742 4294967295 134512640 134672761 3221224544 3221223728 134615996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38363 36742 603 41 0 38322 0
vsize: 153452
[startup+460.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 39987 0 0 0 45880 126 0 0 25 0 1 0 541779631 158052352 36953 4294967295 134512640 134672761 3221224544 3221223688 134616296 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38587 36953 603 41 0 38546 0
vsize: 154348
[startup+470.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 40126 0 0 0 46880 127 0 0 25 0 1 0 541779631 158593024 37092 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38719 37092 603 41 0 38678 0
vsize: 154876
[startup+480.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 40301 0 0 0 47879 127 0 0 25 0 1 0 541779631 159264768 37267 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 38883 37267 603 41 0 38842 0
vsize: 155532
[startup+490.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 40667 0 0 0 48878 128 0 0 25 0 1 0 541779631 160759808 37633 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39248 37633 603 41 0 39207 0
vsize: 156992
[startup+500.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 41053 0 0 0 49877 130 0 0 25 0 1 0 541779631 162340864 38019 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 39634 38019 603 41 0 39593 0
vsize: 158536
[startup+510.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 41569 0 0 0 50876 131 0 0 25 0 1 0 541779631 164458496 38535 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40151 38535 603 41 0 40110 0
vsize: 160604
[startup+520.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 41826 0 0 0 51875 132 0 0 25 0 1 0 541779631 165527552 38792 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40412 38792 603 41 0 40371 0
vsize: 161648
[startup+530.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 42090 0 0 0 52874 133 0 0 25 0 1 0 541779631 166592512 39056 4294967295 134512640 134672761 3221224544 3221223744 134610646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40672 39056 603 41 0 40631 0
vsize: 162688
[startup+540.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 42341 0 0 0 53873 134 0 0 25 0 1 0 541779631 167649280 39307 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 40930 39307 603 41 0 40889 0
vsize: 163720
[startup+550.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 42622 0 0 0 54872 135 0 0 25 0 1 0 541779631 168710144 39588 4294967295 134512640 134672761 3221224544 3221223728 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41189 39588 603 41 0 41148 0
vsize: 164756
[startup+560.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 42953 0 0 0 55872 136 0 0 25 0 1 0 541779631 170029056 39919 4294967295 134512640 134672761 3221224544 3221223320 1075351254 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41511 39919 603 41 0 41470 0
vsize: 166044
[startup+570.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 43201 0 0 0 56871 137 0 0 25 0 1 0 541779631 171085824 40167 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 41769 40167 603 41 0 41728 0
vsize: 167076
[startup+580.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 43476 0 0 0 57870 138 0 0 25 0 1 0 541779631 173187072 40442 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42282 40442 603 41 0 42241 0
vsize: 169128
[startup+590.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 43679 0 0 0 58869 139 0 0 25 0 1 0 541779631 174120960 40645 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 42510 40645 603 41 0 42469 0
vsize: 170040
[startup+600.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 44340 0 0 0 59867 141 0 0 25 0 1 0 541779631 176762880 41306 4294967295 134512640 134672761 3221224544 3221223584 134612676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43155 41306 603 41 0 43114 0
vsize: 172620
[startup+610.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 45037 0 0 0 60865 143 0 0 25 0 1 0 541779631 179658752 42003 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 43862 42003 603 41 0 43821 0
vsize: 175448
[startup+620.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 45711 0 0 0 61863 146 0 0 25 0 1 0 541779631 182304768 42677 4294967295 134512640 134672761 3221224544 3221223728 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44508 42677 603 41 0 44467 0
vsize: 178032
[startup+630.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 46023 0 0 0 62863 146 0 0 25 0 1 0 541779631 183631872 42989 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 44832 42989 603 41 0 44791 0
vsize: 179328
[startup+640.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 46273 0 0 0 63863 146 0 0 25 0 1 0 541779631 184586240 43239 4294967295 134512640 134672761 3221224544 3221223648 134604297 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45065 43239 603 41 0 45024 0
vsize: 180260
[startup+650.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 46655 0 0 0 64861 148 0 0 25 0 1 0 541779631 186159104 43621 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45449 43621 603 41 0 45408 0
vsize: 181796
[startup+660.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 46866 0 0 0 65861 149 0 0 25 0 1 0 541779631 187080704 43832 4294967295 134512640 134672761 3221224544 3221223688 134616132 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45674 43832 603 41 0 45633 0
vsize: 182696
[startup+670.028 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 47165 0 0 0 66860 149 0 0 25 0 1 0 541779631 188260352 44131 4294967295 134512640 134672761 3221224544 3221223728 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 45962 44131 603 41 0 45921 0
vsize: 183848
[startup+680.029 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 47307 0 0 0 67861 150 0 0 25 0 1 0 541779631 188809216 44273 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46096 44273 603 41 0 46055 0
vsize: 184384
[startup+690.029 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 47504 0 0 0 68860 150 0 0 25 0 1 0 541779631 189603840 44470 4294967295 134512640 134672761 3221224544 3221223688 134616108 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46290 44470 603 41 0 46249 0
vsize: 185160
[startup+700.029 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 47814 0 0 0 69859 151 0 0 25 0 1 0 541779631 190926848 44780 4294967295 134512640 134672761 3221224544 3221223728 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 46613 44780 603 41 0 46572 0
vsize: 186452
[startup+710.029 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 48209 0 0 0 70858 152 0 0 25 0 1 0 541779631 192524288 45175 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47003 45175 603 41 0 46962 0
vsize: 188012
[startup+720.03 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 48670 0 0 0 71857 154 0 0 25 0 1 0 541779631 194375680 45636 4294967295 134512640 134672761 3221224544 3221223728 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47455 45636 603 41 0 47414 0
vsize: 189820
[startup+730.029 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 48774 0 0 0 72857 154 0 0 25 0 1 0 541779631 194822144 45740 4294967295 134512640 134672761 3221224544 3221223688 134616263 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47564 45740 603 41 0 47523 0
vsize: 190256
[startup+740.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 48922 0 0 0 73857 154 0 0 25 0 1 0 541779631 195485696 45888 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47726 45888 603 41 0 47685 0
vsize: 190904
[startup+750.03 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 49111 0 0 0 74857 155 0 0 25 0 1 0 541779631 196157440 46077 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 47890 46077 603 41 0 47849 0
vsize: 191560
[startup+760.03 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 49448 0 0 0 75856 156 0 0 25 0 1 0 541779631 197603328 46414 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48243 46414 603 41 0 48202 0
vsize: 192972
[startup+770.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 49827 0 0 0 76855 157 0 0 25 0 1 0 541779631 199184384 46793 4294967295 134512640 134672761 3221224544 3221223728 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48629 46793 603 41 0 48588 0
vsize: 194516
[startup+780.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 50005 0 0 0 77854 158 0 0 25 0 1 0 541779631 199843840 46971 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 48790 46971 603 41 0 48749 0
vsize: 195160
[startup+790.031 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 50300 0 0 0 78854 159 0 0 25 0 1 0 541779631 201031680 47266 4294967295 134512640 134672761 3221224544 3221223688 134616312 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49080 47266 603 41 0 49039 0
vsize: 196320
[startup+800.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 50735 0 0 0 79852 160 0 0 25 0 1 0 541779631 202752000 47701 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 49500 47701 603 41 0 49459 0
vsize: 198000
[startup+810.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 51238 0 0 0 80851 162 0 0 25 0 1 0 541779631 204849152 48204 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50012 48204 603 41 0 49971 0
vsize: 200048
[startup+820.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 51585 0 0 0 81850 163 0 0 25 0 1 0 541779631 206307328 48551 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50368 48551 603 41 0 50327 0
vsize: 201472
[startup+830.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 51974 0 0 0 82849 165 0 0 25 0 1 0 541779631 207888384 48940 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 50754 48940 603 41 0 50713 0
vsize: 203016
[startup+840.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 52304 0 0 0 83847 166 0 0 25 0 1 0 541779631 209199104 49270 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51074 49270 603 41 0 51033 0
vsize: 204296
[startup+850.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 52650 0 0 0 84847 167 0 0 25 0 1 0 541779631 210657280 49616 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51430 49616 603 41 0 51389 0
vsize: 205720
[startup+860.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 52862 0 0 0 85847 167 0 0 25 0 1 0 541779631 211451904 49828 4294967295 134512640 134672761 3221224544 3221223728 134615758 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51624 49828 603 41 0 51583 0
vsize: 206496
[startup+870.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 53110 0 0 0 86846 168 0 0 25 0 1 0 541779631 212537344 50076 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 51889 50076 603 41 0 51848 0
vsize: 207556
[startup+880.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 53376 0 0 0 87845 169 0 0 25 0 1 0 541779631 213594112 50342 4294967295 134512640 134672761 3221224544 3221223728 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52147 50342 603 41 0 52106 0
vsize: 208588
[startup+890.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 53705 0 0 0 88845 170 0 0 25 0 1 0 541779631 214921216 50671 4294967295 134512640 134672761 3221224544 3221223728 134615705 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52471 50671 603 41 0 52430 0
vsize: 209884
[startup+900.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 54056 0 0 0 89844 170 0 0 25 0 1 0 541779631 216379392 51022 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 52827 51022 603 41 0 52786 0
vsize: 211308
[startup+910.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 54413 0 0 0 90842 172 0 0 25 0 1 0 541779631 217837568 51379 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53183 51379 603 41 0 53142 0
vsize: 212732
[startup+920.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 54793 0 0 0 91841 173 0 0 25 0 1 0 541779631 219291648 51759 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53538 51759 603 41 0 53497 0
vsize: 214152
[startup+930.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 55039 0 0 0 92841 174 0 0 25 0 1 0 541779631 220356608 52005 4294967295 134512640 134672761 3221224544 3221223688 134616233 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 53798 52005 603 41 0 53757 0
vsize: 215192
[startup+940.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 55225 0 0 0 93840 175 0 0 25 0 1 0 541779631 221204480 52191 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54005 52191 603 41 0 53964 0
vsize: 216020
[startup+950.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 55553 0 0 0 94839 176 0 0 25 0 1 0 541779631 222519296 52519 4294967295 134512640 134672761 3221224544 3221223712 134615864 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54326 52519 603 41 0 54285 0
vsize: 217304
[startup+960.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 55652 0 0 0 95839 177 0 0 25 0 1 0 541779631 222924800 52618 4294967295 134512640 134672761 3221224544 3221223728 134615652 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54425 52618 603 41 0 54384 0
vsize: 217700
[startup+970.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 55799 0 0 0 96839 177 0 0 25 0 1 0 541779631 223625216 52765 4294967295 134512640 134672761 3221224544 3221223728 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54596 52765 603 41 0 54555 0
vsize: 218384
[startup+980.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 56021 0 0 0 97838 178 0 0 25 0 1 0 541779631 224473088 52987 4294967295 134512640 134672761 3221224544 3221223688 134616123 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54803 52987 603 41 0 54762 0
vsize: 219212
[startup+990.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 56130 0 0 0 98838 178 0 0 25 0 1 0 541779631 224997376 53096 4294967295 134512640 134672761 3221224544 3221223688 134616156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 54931 53096 603 41 0 54890 0
vsize: 219724
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 56252 0 0 0 99838 179 0 0 25 0 1 0 541779631 225394688 53218 4294967295 134512640 134672761 3221224544 3221223728 134615571 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55028 53218 603 41 0 54987 0
vsize: 220112
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 56588 0 0 0 100836 180 0 0 25 0 1 0 541779631 226844672 53554 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55382 53554 603 41 0 55341 0
vsize: 221528
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 56974 0 0 0 101835 181 0 0 25 0 1 0 541779631 228417536 53940 4294967295 134512640 134672761 3221224544 3221223728 134615671 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 55766 53940 603 41 0 55725 0
vsize: 223064
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 57331 0 0 0 102834 183 0 0 25 0 1 0 541779631 229863424 54297 4294967295 134512640 134672761 3221224544 3221223728 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56119 54297 603 41 0 56078 0
vsize: 224476
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 57704 0 0 0 103833 184 0 0 25 0 1 0 541779631 231309312 54670 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56472 54670 603 41 0 56431 0
vsize: 225888
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 58110 0 0 0 104831 186 0 0 25 0 1 0 541779631 233017344 55076 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 56889 55076 603 41 0 56848 0
vsize: 227556
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 58436 0 0 0 105830 187 0 0 25 0 1 0 541779631 234348544 55402 4294967295 134512640 134672761 3221224544 3221223728 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57214 55402 603 41 0 57173 0
vsize: 228856
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 58753 0 0 0 106830 188 0 0 25 0 1 0 541779631 235671552 55719 4294967295 134512640 134672761 3221224544 3221223716 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57537 55719 603 41 0 57496 0
vsize: 230148
[startup+1080.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 59057 0 0 0 107829 189 0 0 25 0 1 0 541779631 236855296 56023 4294967295 134512640 134672761 3221224544 3221223728 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57826 56023 603 41 0 57785 0
vsize: 231304
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 59159 0 0 0 108829 189 0 0 25 0 1 0 541779631 237252608 56125 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 57923 56125 603 41 0 57882 0
vsize: 231692
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 59355 0 0 0 109829 189 0 0 25 0 1 0 541779631 238051328 56321 4294967295 134512640 134672761 3221224544 3221223744 134610686 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58118 56321 603 41 0 58077 0
vsize: 232472
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 59648 0 0 0 110829 190 0 0 25 0 1 0 541779631 239247360 56614 4294967295 134512640 134672761 3221224544 3221223728 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58410 56614 603 41 0 58369 0
vsize: 233640
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 59794 0 0 0 111828 191 0 0 25 0 1 0 541779631 239910912 56760 4294967295 134512640 134672761 3221224544 3221223728 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58572 56760 603 41 0 58531 0
vsize: 234288
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 59873 0 0 0 112828 191 0 0 25 0 1 0 541779631 240201728 56839 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58643 56839 603 41 0 58602 0
vsize: 234572
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 60098 0 0 0 113828 192 0 0 25 0 1 0 541779631 241139712 57064 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 58872 57064 603 41 0 58831 0
vsize: 235488
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 60377 0 0 0 114828 192 0 0 25 0 1 0 541779631 242200576 57343 4294967295 134512640 134672761 3221224544 3221223728 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59131 57343 603 41 0 59090 0
vsize: 236524
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 60702 0 0 0 115827 193 0 0 25 0 1 0 541779631 243523584 57668 4294967295 134512640 134672761 3221224544 3221223584 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59454 57668 603 41 0 59413 0
vsize: 237816
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 60875 0 0 0 116826 194 0 0 25 0 1 0 541779631 244178944 57841 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59614 57841 603 41 0 59573 0
vsize: 238456
[startup+1180.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 61205 0 0 0 117826 195 0 0 25 0 1 0 541779631 245501952 58171 4294967295 134512640 134672761 3221224544 3221223728 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 59937 58171 603 41 0 59896 0
vsize: 239748
[startup+1190.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 61558 0 0 0 118825 197 0 0 25 0 1 0 541779631 246960128 58524 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60293 58524 603 41 0 60252 0
vsize: 241172
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 27884
Raw data (stat): 27884 (minisat+) R 27883 3260 3259 0 -1 0 61993 0 0 0 119824 197 0 0 25 0 1 0 541779631 248799232 58959 4294967295 134512640 134672761 3221224544 3221223728 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 60742 58959 603 41 0 60701 0
vsize: 242968
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.17 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 27884
Raw data (stat): 27884 (minisat+) Z 27883 3260 3259 0 -1 12 61993 0 0 0 119824 209 0 0 25 0 1 0 541779631 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.17
CPU time (s): 1200.34
CPU user time (s): 1198.24
CPU system time (s): 2.09768
CPU usage (%): 100.015
Max. virtual memory (Kb): 242968
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####