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 18296

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc25 THE 2005-04-21 14:14:28 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18283 boxname=wulflinc25 idbench=1407 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  28123830d5f7e3646d18978bb347487c  /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-dcmulti.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc25/normalized-mps-v2-13-7-dcmulti.opb
IDLAUNCH: 18283
/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:        796616 kB
Buffers:         25040 kB
Cached:         193040 kB
SwapCached:        744 kB
Active:          73216 kB
Inactive:       146772 kB
HighTotal:      131008 kB
HighFree:        32228 kB
LowTotal:       903652 kB
LowFree:        764388 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12544 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 14:34:30 (client local time) WITH STATUS 0 IN 1200.27 SECONDS
stats: 18283 7 1200.27 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 368 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss
c ---[ 427]---> BDD-cost:   14
c ---[ 426]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 425]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 424]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 422]---> BDD-cost:   15
c ---[ 421]---> BDD-cost:   14
c ---[ 420]---> BDD-cost:   14
c ---[ 419]---> BDD-cost:   13
c ---[ 418]---> BDD-cost:   14
c ---[ 416]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 415]---> BDD-cost:   14
c ---[ 413]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 411]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 409]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 407]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 405]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 403]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 401]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 399]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 397]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 395]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 394]---> BDD-cost:   13
c ---[ 392]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 391]---> BDD-cost:   16
c ---[ 390]---> BDD-cost:    7
c ---[ 389]---> BDD-cost:   15
c ---[ 388]---> BDD-cost:    4
c ---[ 386]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 385]---> BDD-cost:   24
c ---[ 384]---> BDD-cost:    6
c ---[ 381]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 380]---> BDD-cost:   14
c ---[ 378]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 377]---> BDD-cost:   16
c ---[ 376]---> BDD-cost:    7
c ---[ 375]---> BDD-cost:   15
c ---[ 374]---> BDD-cost:    4
c ---[ 372]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 371]---> BDD-cost:   23
c ---[ 370]---> BDD-cost:    8
c ---[ 367]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 365]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 363]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 362]---> BDD-cost:   15
c ---[ 361]---> BDD-cost:    6
c ---[ 360]---> BDD-cost:   14
c ---[ 359]---> BDD-cost:    3
c ---[ 357]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 356]---> BDD-cost:   23
c ---[ 355]---> BDD-cost:    6
c ---[ 352]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 350]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 348]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 347]---> BDD-cost:   16
c ---[ 346]---> BDD-cost:    7
c ---[ 345]---> BDD-cost:   15
c ---[ 344]---> BDD-cost:    4
c ---[ 342]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 341]---> BDD-cost:   24
c ---[ 340]---> BDD-cost:    6
c ---[ 337]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 335]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 333]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 332]---> BDD-cost:   16
c ---[ 331]---> BDD-cost:    7
c ---[ 330]---> BDD-cost:   15
c ---[ 329]---> BDD-cost:    4
c ---[ 327]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 326]---> BDD-cost:   19
c ---[ 322]---> BDD-cost:   33
c ---[ 320]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 308]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 296]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 293]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 292]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 291]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 290]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 289]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 288]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 286]---> BDD-cost:   15
c ---[ 285]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 283]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 282]---> BDD-cost:   14
c ---[ 281]---> BDD-cost:   14
c ---[ 280]---> BDD-cost:   13
c ---[ 279]---> BDD-cost:   14
c ---[ 277]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 275]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 273]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 271]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 269]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 267]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 265]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 263]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 261]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 259]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 257]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 255]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 253]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 252]---> BDD-cost:   16
c ---[ 251]---> BDD-cost:    7
c ---[ 250]---> BDD-cost:   15
c ---[ 249]---> BDD-cost:    4
c ---[ 247]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 245]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 244]---> BDD-cost:   24
c ---[ 243]---> BDD-cost:    6
c ---[ 240]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 238]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 237]---> BDD-cost:   16
c ---[ 236]---> BDD-cost:    7
c ---[ 235]---> BDD-cost:   15
c ---[ 234]---> BDD-cost:    4
c ---[ 232]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 230]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 229]---> BDD-cost:   23
c ---[ 228]---> BDD-cost:    8
c ---[ 225]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 223]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 222]---> BDD-cost:   15
c ---[ 221]---> BDD-cost:    6
c ---[ 220]---> BDD-cost:   14
c ---[ 219]---> BDD-cost:    3
c ---[ 217]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 215]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 214]---> BDD-cost:   23
c ---[ 213]---> BDD-cost:    6
c ---[ 210]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 208]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 207]---> BDD-cost:   16
c ---[ 206]---> BDD-cost:    7
c ---[ 205]---> BDD-cost:   15
c ---[ 204]---> BDD-cost:    4
c ---[ 202]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 200]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 199]---> BDD-cost:   24
c ---[ 198]---> BDD-cost:    6
c ---[ 195]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 193]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 192]---> BDD-cost:   16
c ---[ 191]---> BDD-cost:    7
c ---[ 190]---> BDD-cost:   15
c ---[ 189]---> BDD-cost:    4
c ---[ 188]---> BDD-cost:   16
c ---[ 186]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 185]---> BDD-cost:   19
c ---[ 181]---> BDD-cost:   33
c ---[ 175]---> BDD-cost:    7
c ---[ 164]---> BDD-cost:   15
c ---[ 156]---> BDD-cost:    3
c ---[ 155]---> BDD-cost:    3
c ---[ 154]---> BDD-cost:    3
c ---[ 153]---> BDD-cost:    4
c ---[ 152]---> BDD-cost:    3
c ---[ 151]---> BDD-cost:    3
c ---[ 150]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 148]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 147]---> BDD-cost:   24
c ---[ 146]---> BDD-cost:    6
c ---[ 143]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 141]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 140]---> BDD-cost:   16
c ---[ 139]---> BDD-cost:    7
c ---[ 138]---> BDD-cost:   15
c ---[ 137]---> BDD-cost:    4
c ---[ 136]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 134]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 133]---> BDD-cost:   23
c ---[ 132]---> BDD-cost:    8
c ---[ 129]---> Sorter-cost:  915     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 127]---> Sorter-cost:  869     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 126]---> BDD-cost:   15
c ---[ 125]---> BDD-cost:    6
c ---[ 124]---> BDD-cost:   14
c ---[ 123]---> BDD-cost:    3
c ---[ 122]---> Sorter-cost: 1116     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 120]---> Sorter-cost:  859     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 119]---> BDD-cost:   23
c ---[ 118]---> BDD-cost:    6
c ---[ 115]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 113]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 112]---> BDD-cost:   16
c ---[ 111]---> BDD-cost:    7
c ---[ 110]---> BDD-cost:   15
c ---[ 109]---> BDD-cost:    4
c ---[ 108]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 106]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[ 105]---> BDD-cost:   24
c ---[ 104]---> BDD-cost:    6
c ---[ 101]---> Sorter-cost:  957     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  99]---> Sorter-cost:  943     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  98]---> BDD-cost:   16
c ---[  97]---> BDD-cost:    7
c ---[  96]---> BDD-cost:   15
c ---[  95]---> BDD-cost:    4
c ---[  94]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  92]---> Sorter-cost:  920     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  91]---> BDD-cost:   19
c ---[  87]---> BDD-cost:   33
c ---[  70]---> BDD-cost:   15
c ---[  62]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  61]---> Sorter-cost: 1203     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  60]---> Sorter-cost: 1290     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  59]---> BDD-cost:   12
c ---[  58]---> BDD-cost:    5
c ---[  57]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  56]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  55]---> Sorter-cost:  847     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  54]---> Sorter-cost:  750     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  53]---> Sorter-cost:  862     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  52]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  51]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  50]---> Sorter-cost:  714     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  49]---> Sorter-cost:  773     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  48]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  47]---> Sorter-cost:  875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  46]---> Sorter-cost:  773     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  45]---> Sorter-cost:  834     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  44]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  43]---> Sorter-cost:  694     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  42]---> Sorter-cost:  663     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  41]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  40]---> Sorter-cost:  808     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  39]---> BDD-cost:   12
c ---[  38]---> BDD-cost:    5
c ---[  37]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  36]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  35]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  34]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  33]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  32]---> Sorter-cost:  824     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  31]---> Sorter-cost:  798     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  30]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  29]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  28]---> Sorter-cost:  714     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  27]---> Sorter-cost:  895     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  26]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  25]---> Sorter-cost:  801     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  24]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  23]---> Sorter-cost:  821     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  22]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  21]---> Sorter-cost:  875     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  20]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  19]---> BDD-cost:    5
c ---[  18]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  17]---> BDD-cost:   12
c ---[  16]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[  15]---> Sorter-cost:  811     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  14]---> Sorter-cost:  747     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  13]---> Sorter-cost:  860     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  12]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[  11]---> Sorter-cost:  704     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[  10]---> Sorter-cost:  686     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   9]---> Sorter-cost:  788     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   8]---> Sorter-cost:  650     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   7]---> Sorter-cost:  908     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   6]---> Sorter-cost:  737     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   5]---> Sorter-cost:  798     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   4]---> Sorter-cost:  630     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   3]---> Sorter-cost:  760     Base: 2 2 2 2 2 2 2 2 2 2 2
c ---[   2]---> Sorter-cost:  660     Base: 2 2 2 2 2 2 2 2 2 2
c ---[   1]---> Sorter-cost:  872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[   0]---> Sorter-cost:  727     Base: 2 2 2 2 2 2 2 2 2 2 2
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  333790   886289 |  111263       0        0     nan |  0.000 % |
c |       100 |  333689   886069 |  122389      82      264     3.2 |  4.481 % |
c |       250 |  333597   885869 |  134628     210      689     3.3 |  4.507 % |
c |       475 |  333435   885515 |  148091     408     1295     3.2 |  4.555 % |
c |       812 |  333059   884679 |  162900     700     2234     3.2 |  4.662 % |
c |      1318 |  332410   883226 |  179190    1143     3825     3.3 |  4.838 % |
c |      2077 |  331562   881336 |  197109    1802     6121     3.4 |  5.075 % |
c |      3216 |  330950   879975 |  216820    2845     9983     3.5 |  5.238 % |
c |      4924 |  329404   876535 |  238502    4329    15698     3.6 |  5.665 % |
c |      7486 |  328443   874392 |  262352    6713    48826     7.3 |  5.924 % |
c |     11330 |  326869   870869 |  288587   10302    92482     9.0 |  6.350 % |
c |     17097 |  325584   867960 |  317446   15919   219879    13.8 |  6.707 % |
c |     25747 |  324551   865655 |  349190   24424   431973    17.7 |  6.984 % |
c |     38721 |  323989   864389 |  384110   37319   890114    23.9 |  7.138 % |
c |     58186 |  323535   863367 |  422521   56730  1652421    29.1 |  7.264 % |
c |     87378 |  322070   860086 |  464773   85698  2899355    33.8 |  7.675 % |
c |    131168 |  320907   857454 |  511250  129348  4534053    35.1 |  7.995 % |
c |    196852 |  319545   854363 |  562375  194804  7383330    37.9 |  8.366 % |
c |    295380 |  318648   852328 |  618613  293155 11490253    39.2 |  8.620 % |
c |    443173 |  317986   850831 |  680474  440861 18651400    42.3 |  8.807 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.82 0.92 0.90 2/54 7870
Raw data (stat): 7870 (runsolver) R 7869 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545727842 1052672 99 4294967295 134512640 135381576 3221224512 3221219756 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.85 0.92 0.90 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 9643 0 0 0 972 26 0 0 25 0 1 0 545727842 41910272 9248 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10232 9248 603 41 0 10191 0
vsize: 40928
[startup+20.0009 s]
Raw data (loadavg): 0.87 0.92 0.90 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 9674 0 0 0 1972 26 0 0 25 0 1 0 545727842 42045440 9279 4294967295 134512640 134672761 3221224624 3221223776 134565116 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10265 9279 603 41 0 10224 0
vsize: 41060
[startup+30.0004 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 9720 0 0 0 2972 26 0 0 25 0 1 0 545727842 42180608 9325 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10298 9325 603 41 0 10257 0
vsize: 41192
[startup+40.0003 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 9756 0 0 0 3971 26 0 0 25 0 1 0 545727842 42180608 9361 4294967295 134512640 134672761 3221224624 3221223816 134556677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10298 9361 603 41 0 10257 0
vsize: 41192
[startup+50.0006 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 9816 0 0 0 4972 26 0 0 25 0 1 0 545727842 42446848 9421 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10363 9421 603 41 0 10322 0
vsize: 41452
[startup+60.0002 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 9883 0 0 0 5972 27 0 0 25 0 1 0 545727842 42717184 9488 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10429 9488 603 41 0 10388 0
vsize: 41716
[startup+70.0014 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 9990 0 0 0 6971 27 0 0 25 0 1 0 545727842 43122688 9595 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10528 9595 603 41 0 10487 0
vsize: 42112
[startup+80.0015 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 10196 0 0 0 7970 28 0 0 25 0 1 0 545727842 43974656 9801 4294967295 134512640 134672761 3221224624 3221223828 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10736 9801 603 41 0 10695 0
vsize: 42944
[startup+90.001 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 10358 0 0 0 8970 28 0 0 25 0 1 0 545727842 44650496 9963 4294967295 134512640 134672761 3221224624 3221223776 1074744144 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10901 9963 603 41 0 10860 0
vsize: 43604
[startup+100.001 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 10706 0 0 0 9969 29 0 0 25 0 1 0 545727842 46125056 10311 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11261 10311 603 41 0 11220 0
vsize: 45044
[startup+110 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 11036 0 0 0 10968 31 0 0 25 0 1 0 545727842 47591424 10641 4294967295 134512640 134672761 3221224624 3221223728 134559925 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11619 10641 603 41 0 11578 0
vsize: 46476
[startup+120.001 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 11451 0 0 0 11967 32 0 0 25 0 1 0 545727842 49197056 11056 4294967295 134512640 134672761 3221224624 3221223760 134560596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12011 11056 603 41 0 11970 0
vsize: 48044
[startup+130.001 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 11914 0 0 0 12966 33 0 0 25 0 1 0 545727842 51052544 11519 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12464 11519 603 41 0 12423 0
vsize: 49856
[startup+140 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 12236 0 0 0 13965 34 0 0 25 0 1 0 545727842 52387840 11841 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12790 11841 603 41 0 12749 0
vsize: 51160
[startup+150.001 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 12699 0 0 0 14964 35 0 0 25 0 1 0 545727842 54525952 12304 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13312 12304 603 41 0 13271 0
vsize: 53248
[startup+160.001 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 12992 0 0 0 15964 36 0 0 25 0 1 0 545727842 55603200 12597 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13575 12597 603 41 0 13534 0
vsize: 54300
[startup+170.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 13102 0 0 0 16963 36 0 0 25 0 1 0 545727842 56143872 12707 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13707 12707 603 41 0 13666 0
vsize: 54828
[startup+180 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 13375 0 0 0 17963 37 0 0 25 0 1 0 545727842 57200640 12980 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13965 12980 603 41 0 13924 0
vsize: 55860
[startup+190 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 13509 0 0 0 18962 38 0 0 25 0 1 0 545727842 57733120 13114 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14095 13114 603 41 0 14054 0
vsize: 56380
[startup+200 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 13793 0 0 0 19961 39 0 0 25 0 1 0 545727842 58925056 13398 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14386 13398 603 41 0 14345 0
vsize: 57544
[startup+209.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 13917 0 0 0 20961 39 0 0 25 0 1 0 545727842 59318272 13522 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14482 13522 603 41 0 14441 0
vsize: 57928
[startup+220 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 14152 0 0 0 21961 39 0 0 25 0 1 0 545727842 60256256 13757 4294967295 134512640 134672761 3221224624 3221223796 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14711 13757 603 41 0 14670 0
vsize: 58844
[startup+229.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 14618 0 0 0 22960 41 0 0 25 0 1 0 545727842 62132224 14223 4294967295 134512640 134672761 3221224624 3221223824 134557836 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15169 14223 603 41 0 15128 0
vsize: 60676
[startup+239.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 14919 0 0 0 23960 41 0 0 25 0 1 0 545727842 63348736 14524 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15466 14524 603 41 0 15425 0
vsize: 61864
[startup+249.999 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 15256 0 0 0 24959 42 0 0 25 0 1 0 545727842 64688128 14861 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15793 14861 603 41 0 15752 0
vsize: 63172
[startup+259.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 15459 0 0 0 25959 42 0 0 25 0 1 0 545727842 65622016 15064 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16021 15064 603 41 0 15980 0
vsize: 64084
[startup+269.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 15805 0 0 0 26958 43 0 0 25 0 1 0 545727842 67477504 15410 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16474 15410 603 41 0 16433 0
vsize: 65896
[startup+279.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 16300 0 0 0 27956 45 0 0 25 0 1 0 545727842 69492736 15905 4294967295 134512640 134672761 3221224624 3221223776 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16966 15905 603 41 0 16925 0
vsize: 67864
[startup+289.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 16729 0 0 0 28955 46 0 0 25 0 1 0 545727842 71233536 16334 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17391 16334 603 41 0 17350 0
vsize: 69564
[startup+299.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 17009 0 0 0 29954 47 0 0 25 0 1 0 545727842 72306688 16614 4294967295 134512640 134672761 3221224624 3221223796 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17653 16614 603 41 0 17612 0
vsize: 70612
[startup+310 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 17301 0 0 0 30954 48 0 0 25 0 1 0 545727842 73515008 16906 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17948 16906 603 41 0 17907 0
vsize: 71792
[startup+320 s]
Raw data (loadavg): 1.07 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 17518 0 0 0 31954 48 0 0 25 0 1 0 545727842 74317824 17123 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18144 17123 603 41 0 18103 0
vsize: 72576
[startup+330 s]
Raw data (loadavg): 1.06 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 17729 0 0 0 32954 49 0 0 25 0 1 0 545727842 75259904 17334 4294967295 134512640 134672761 3221224624 3221223796 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18374 17334 603 41 0 18333 0
vsize: 73496
[startup+340 s]
Raw data (loadavg): 1.05 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 18070 0 0 0 33953 50 0 0 25 0 1 0 545727842 76591104 17675 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18699 17675 603 41 0 18658 0
vsize: 74796
[startup+350.001 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 18315 0 0 0 34952 51 0 0 25 0 1 0 545727842 77516800 17920 4294967295 134512640 134672761 3221224624 3221223772 134560631 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18925 17920 603 41 0 18884 0
vsize: 75700
[startup+360 s]
Raw data (loadavg): 1.04 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 18391 0 0 0 35952 51 0 0 25 0 1 0 545727842 77918208 17996 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19023 17996 603 41 0 18982 0
vsize: 76092
[startup+370.007 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 18664 0 0 0 36952 52 0 0 25 0 1 0 545727842 78987264 18269 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19284 18269 603 41 0 19243 0
vsize: 77136
[startup+380.007 s]
Raw data (loadavg): 1.03 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 19111 0 0 0 37951 53 0 0 25 0 1 0 545727842 80723968 18716 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19708 18716 603 41 0 19667 0
vsize: 78832
[startup+390.007 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 19376 0 0 0 38949 54 0 0 25 0 1 0 545727842 81797120 18981 4294967295 134512640 134672761 3221224624 3221223748 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19970 18981 603 41 0 19929 0
vsize: 79880
[startup+400.008 s]
Raw data (loadavg): 1.02 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 19747 0 0 0 39949 55 0 0 25 0 1 0 545727842 83406848 19352 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20363 19352 603 41 0 20322 0
vsize: 81452
[startup+410.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 20004 0 0 0 40948 56 0 0 25 0 1 0 545727842 84348928 19609 4294967295 134512640 134672761 3221224624 3221223840 134561997 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20593 19609 603 41 0 20552 0
vsize: 82372
[startup+420.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 20266 0 0 0 41947 57 0 0 25 0 1 0 545727842 85417984 19871 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20854 19871 603 41 0 20813 0
vsize: 83416
[startup+430.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 20658 0 0 0 42946 59 0 0 25 0 1 0 545727842 87031808 20263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21248 20263 603 41 0 21207 0
vsize: 84992
[startup+440.007 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 21011 0 0 0 43945 60 0 0 25 0 1 0 545727842 88383488 20616 4294967295 134512640 134672761 3221224624 3221223792 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21578 20616 603 41 0 21537 0
vsize: 86312
[startup+450.008 s]
Raw data (loadavg): 1.01 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 21192 0 0 0 44945 60 0 0 25 0 1 0 545727842 89194496 20797 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21776 20797 603 41 0 21735 0
vsize: 87104
[startup+460.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 21374 0 0 0 45944 61 0 0 25 0 1 0 545727842 89866240 20979 4294967295 134512640 134672761 3221224624 3221223808 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21940 20979 603 41 0 21899 0
vsize: 87760
[startup+470.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 21748 0 0 0 46943 62 0 0 25 0 1 0 545727842 91357184 21353 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22304 21353 603 41 0 22263 0
vsize: 89216
[startup+480.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 22051 0 0 0 47942 63 0 0 25 0 1 0 545727842 92577792 21656 4294967295 134512640 134672761 3221224624 3221223796 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22602 21656 603 41 0 22561 0
vsize: 90408
[startup+490.007 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 22319 0 0 0 48942 63 0 0 25 0 1 0 545727842 93650944 21924 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22864 21924 603 41 0 22823 0
vsize: 91456
[startup+500.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 22620 0 0 0 49941 65 0 0 25 0 1 0 545727842 95916032 22225 4294967295 134512640 134672761 3221224624 3221223792 134561378 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23417 22225 603 41 0 23376 0
vsize: 93668
[startup+510.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 22882 0 0 0 50941 65 0 0 25 0 1 0 545727842 96985088 22487 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23678 22487 603 41 0 23637 0
vsize: 94712
[startup+520.008 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 23076 0 0 0 51940 66 0 0 25 0 1 0 545727842 97787904 22681 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23874 22681 603 41 0 23833 0
vsize: 95496
[startup+530.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 23369 0 0 0 52940 67 0 0 25 0 1 0 545727842 98996224 22974 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24169 22974 603 41 0 24128 0
vsize: 96676
[startup+540.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 23741 0 0 0 53939 68 0 0 25 0 1 0 545727842 100466688 23346 4294967295 134512640 134672761 3221224624 3221223792 134560822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24528 23346 603 41 0 24487 0
vsize: 98112
[startup+550.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 24040 0 0 0 54938 69 0 0 25 0 1 0 545727842 101675008 23645 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24823 23645 603 41 0 24782 0
vsize: 99292
[startup+560.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 24264 0 0 0 55937 70 0 0 25 0 1 0 545727842 102600704 23869 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25049 23869 603 41 0 25008 0
vsize: 100196
[startup+570.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 24378 0 0 0 56936 71 0 0 25 0 1 0 545727842 103006208 23983 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25148 23983 603 41 0 25107 0
vsize: 100592
[startup+580.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 24677 0 0 0 57935 72 0 0 25 0 1 0 545727842 104218624 24282 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25444 24282 603 41 0 25403 0
vsize: 101776
[startup+590.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 25015 0 0 0 58935 73 0 0 25 0 1 0 545727842 105693184 24620 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25804 24620 603 41 0 25763 0
vsize: 103216
[startup+600.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 25420 0 0 0 59933 74 0 0 25 0 1 0 545727842 107294720 25025 4294967295 134512640 134672761 3221224624 3221223760 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26195 25025 603 41 0 26154 0
vsize: 104780
[startup+610.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 25683 0 0 0 60933 75 0 0 25 0 1 0 545727842 108367872 25288 4294967295 134512640 134672761 3221224624 3221223792 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26457 25288 603 41 0 26416 0
vsize: 105828
[startup+620.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 25826 0 0 0 61932 75 0 0 25 0 1 0 545727842 108904448 25431 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26588 25431 603 41 0 26547 0
vsize: 106352
[startup+630.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 26099 0 0 0 62931 76 0 0 25 0 1 0 545727842 109977600 25704 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26850 25704 603 41 0 26809 0
vsize: 107400
[startup+640.009 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 26325 0 0 0 63931 77 0 0 25 0 1 0 545727842 110911488 25930 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27078 25930 603 41 0 27037 0
vsize: 108312
[startup+650.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 26585 0 0 0 64930 78 0 0 25 0 1 0 545727842 111984640 26190 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27340 26190 603 41 0 27299 0
vsize: 109360
[startup+660.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 26908 0 0 0 65929 79 0 0 25 0 1 0 545727842 113319936 26513 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27666 26513 603 41 0 27625 0
vsize: 110664
[startup+670.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 27178 0 0 0 66929 79 0 0 25 0 1 0 545727842 114388992 26783 4294967295 134512640 134672761 3221224624 3221223808 134559345 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27927 26783 603 41 0 27886 0
vsize: 111708
[startup+680.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 27570 0 0 0 67929 80 0 0 25 0 1 0 545727842 115867648 27175 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28288 27175 603 41 0 28247 0
vsize: 113152
[startup+690.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 27758 0 0 0 68928 81 0 0 25 0 1 0 545727842 116674560 27363 4294967295 134512640 134672761 3221224624 3221223796 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28485 27363 603 41 0 28444 0
vsize: 113940
[startup+700.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 27948 0 0 0 69928 81 0 0 25 0 1 0 545727842 117473280 27553 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28680 27553 603 41 0 28639 0
vsize: 114720
[startup+710.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 28231 0 0 0 70927 83 0 0 25 0 1 0 545727842 118546432 27836 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28942 27836 603 41 0 28901 0
vsize: 115768
[startup+720.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 28518 0 0 0 71927 83 0 0 25 0 1 0 545727842 119754752 28123 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29237 28123 603 41 0 29196 0
vsize: 116948
[startup+730.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 28825 0 0 0 72926 84 0 0 25 0 1 0 545727842 120963072 28430 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29532 28430 603 41 0 29491 0
vsize: 118128
[startup+740.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 29003 0 0 0 73926 84 0 0 25 0 1 0 545727842 121769984 28608 4294967295 134512640 134672761 3221224624 3221223872 134562724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29729 28608 603 41 0 29688 0
vsize: 118916
[startup+750.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 29278 0 0 0 74925 85 0 0 25 0 1 0 545727842 122843136 28883 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29991 28883 603 41 0 29950 0
vsize: 119964
[startup+760.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 29540 0 0 0 75925 86 0 0 25 0 1 0 545727842 123908096 29145 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30251 29145 603 41 0 30210 0
vsize: 121004
[startup+770.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 29702 0 0 0 76925 86 0 0 25 0 1 0 545727842 124575744 29307 4294967295 134512640 134672761 3221224624 3221223748 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30414 29307 603 41 0 30373 0
vsize: 121656
[startup+780.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 29861 0 0 0 77924 86 0 0 25 0 1 0 545727842 125247488 29466 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30578 29466 603 41 0 30537 0
vsize: 122312
[startup+790.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 30114 0 0 0 78924 87 0 0 25 0 1 0 545727842 126189568 29719 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30808 29719 603 41 0 30767 0
vsize: 123232
[startup+800.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 30371 0 0 0 79923 88 0 0 25 0 1 0 545727842 127254528 29976 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31068 29976 603 41 0 31027 0
vsize: 124272
[startup+810.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 30625 0 0 0 80923 89 0 0 25 0 1 0 545727842 128221184 30230 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31304 30230 603 41 0 31263 0
vsize: 125216
[startup+820.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 30873 0 0 0 81922 89 0 0 25 0 1 0 545727842 129294336 30478 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31566 30478 603 41 0 31525 0
vsize: 126264
[startup+830.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 31009 0 0 0 82922 90 0 0 25 0 1 0 545727842 129839104 30614 4294967295 134512640 134672761 3221224624 3221223820 134556584 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31699 30614 603 41 0 31658 0
vsize: 126796
[startup+840.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 31276 0 0 0 83921 91 0 0 25 0 1 0 545727842 130904064 30881 4294967295 134512640 134672761 3221224624 3221223728 134555093 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 31959 30881 603 41 0 31918 0
vsize: 127836
[startup+850.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 31608 0 0 0 84921 91 0 0 25 0 1 0 545727842 132243456 31213 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32286 31213 603 41 0 32245 0
vsize: 129144
[startup+860.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 31920 0 0 0 85921 92 0 0 25 0 1 0 545727842 133582848 31525 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32613 31525 603 41 0 32572 0
vsize: 130452
[startup+870.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 32252 0 0 0 86920 93 0 0 25 0 1 0 545727842 134930432 31857 4294967295 134512640 134672761 3221224624 3221223760 134560642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 32942 31857 603 41 0 32901 0
vsize: 131768
[startup+880.013 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 32541 0 0 0 87919 94 0 0 25 0 1 0 545727842 136015872 32146 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33207 32146 603 41 0 33166 0
vsize: 132828
[startup+890.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 32769 0 0 0 88918 95 0 0 25 0 1 0 545727842 136970240 32374 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33440 32374 603 41 0 33399 0
vsize: 133760
[startup+900.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 33018 0 0 0 89918 95 0 0 25 0 1 0 545727842 138055680 32623 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33705 32623 603 41 0 33664 0
vsize: 134820
[startup+910.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 33135 0 0 0 90918 95 0 0 25 0 1 0 545727842 138461184 32740 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 33804 32740 603 41 0 33763 0
vsize: 135216
[startup+920.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 33380 0 0 0 91917 96 0 0 25 0 1 0 545727842 139542528 32985 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34068 32985 603 41 0 34027 0
vsize: 136272
[startup+930.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 33505 0 0 0 92917 96 0 0 25 0 1 0 545727842 139968512 33110 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34172 33110 603 41 0 34131 0
vsize: 136688
[startup+940.011 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 33650 0 0 0 93917 97 0 0 25 0 1 0 545727842 140525568 33255 4294967295 134512640 134672761 3221224624 3221223792 134560825 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34308 33255 603 41 0 34267 0
vsize: 137232
[startup+950.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 33843 0 0 0 94917 97 0 0 25 0 1 0 545727842 141328384 33448 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34504 33448 603 41 0 34463 0
vsize: 138016
[startup+960.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 34227 0 0 0 95916 98 0 0 25 0 1 0 545727842 142934016 33832 4294967295 134512640 134672761 3221224624 3221223760 134560606 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 34896 33832 603 41 0 34855 0
vsize: 139584
[startup+970.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 34501 0 0 0 96916 98 0 0 25 0 1 0 545727842 144015360 34106 4294967295 134512640 134672761 3221224624 3221223796 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35160 34106 603 41 0 35119 0
vsize: 140640
[startup+980.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 34549 0 0 0 97916 99 0 0 25 0 1 0 545727842 144150528 34154 4294967295 134512640 134672761 3221224624 3221223796 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35193 34154 603 41 0 35152 0
vsize: 140772
[startup+990.012 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 34738 0 0 0 98915 99 0 0 25 0 1 0 545727842 144961536 34343 4294967295 134512640 134672761 3221224624 3221223792 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35391 34343 603 41 0 35350 0
vsize: 141564
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 35073 0 0 0 99915 99 0 0 25 0 1 0 545727842 146296832 34678 4294967295 134512640 134672761 3221224624 3221223792 134560976 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 35717 34678 603 41 0 35676 0
vsize: 142868
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 35442 0 0 0 100914 101 0 0 25 0 1 0 545727842 147779584 35047 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36079 35047 603 41 0 36038 0
vsize: 144316
[startup+1020.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 35768 0 0 0 101913 102 0 0 25 0 1 0 545727842 149118976 35373 4294967295 134512640 134672761 3221224624 3221223808 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36406 35373 603 41 0 36365 0
vsize: 145624
[startup+1030.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 36258 0 0 0 102912 103 0 0 25 0 1 0 545727842 151146496 35863 4294967295 134512640 134672761 3221224624 3221223796 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 36901 35863 603 41 0 36860 0
vsize: 147604
[startup+1040.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 36412 0 0 0 103911 104 0 0 25 0 1 0 545727842 151683072 36017 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37032 36017 603 41 0 36991 0
vsize: 148128
[startup+1050.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 36798 0 0 0 104910 106 0 0 25 0 1 0 545727842 153292800 36403 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 37425 36403 603 41 0 37384 0
vsize: 149700
[startup+1060.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 37376 0 0 0 105909 107 0 0 25 0 1 0 545727842 155697152 36981 4294967295 134512640 134672761 3221224624 3221223728 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38012 36981 603 41 0 37971 0
vsize: 152048
[startup+1070.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 37847 0 0 0 106908 108 0 0 25 0 1 0 545727842 157564928 37452 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38468 37452 603 41 0 38427 0
vsize: 153872
[startup+1080.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 38078 0 0 0 107907 109 0 0 25 0 1 0 545727842 158511104 37683 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38699 37683 603 41 0 38658 0
vsize: 154796
[startup+1090.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 38259 0 0 0 108907 110 0 0 25 0 1 0 545727842 159182848 37864 4294967295 134512640 134672761 3221224624 3221223796 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 38863 37864 603 41 0 38822 0
vsize: 155452
[startup+1100.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 38454 0 0 0 109906 110 0 0 25 0 1 0 545727842 159989760 38059 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39060 38059 603 41 0 39019 0
vsize: 156240
[startup+1110.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 38842 0 0 0 110905 112 0 0 25 0 1 0 545727842 163704832 38447 4294967295 134512640 134672761 3221224624 3221223728 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 39967 38447 603 41 0 39926 0
vsize: 159868
[startup+1120.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 39067 0 0 0 111904 112 0 0 25 0 1 0 545727842 164511744 38672 4294967295 134512640 134672761 3221224624 3221223792 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40164 38672 603 41 0 40123 0
vsize: 160656
[startup+1130.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 39262 0 0 0 112904 113 0 0 25 0 1 0 545727842 165335040 38867 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40365 38867 603 41 0 40324 0
vsize: 161460
[startup+1140.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 39498 0 0 0 113904 113 0 0 25 0 1 0 545727842 166277120 39103 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40595 39103 603 41 0 40554 0
vsize: 162380
[startup+1150.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 39732 0 0 0 114904 114 0 0 25 0 1 0 545727842 167206912 39337 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 40822 39337 603 41 0 40781 0
vsize: 163288
[startup+1160.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 39977 0 0 0 115903 114 0 0 25 0 1 0 545727842 168288256 39582 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41086 39582 603 41 0 41045 0
vsize: 164344
[startup+1170.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 40207 0 0 0 116903 115 0 0 25 0 1 0 545727842 169213952 39812 4294967295 134512640 134672761 3221224624 3221223824 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41312 39812 603 41 0 41271 0
vsize: 165248
[startup+1180.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 40439 0 0 0 117902 116 0 0 25 0 1 0 545727842 170156032 40044 4294967295 134512640 134672761 3221224624 3221223760 134560683 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41542 40044 603 41 0 41501 0
vsize: 166168
[startup+1190.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 40675 0 0 0 118902 117 0 0 25 0 1 0 545727842 171089920 40280 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41770 40280 603 41 0 41729 0
vsize: 167080
[startup+1200.01 s]
Raw data (loadavg): 1.00 0.98 0.91 2/54 7870
Raw data (stat): 7870 (minisat+) R 7869 28099 28098 0 -1 0 40889 0 0 0 119901 117 0 0 25 0 1 0 545727842 171888640 40494 4294967295 134512640 134672761 3221224624 3221223760 134560566 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 41965 40494 603 41 0 41924 0
vsize: 167860
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.98 0.91 1/54 7870
Raw data (stat): 7870 (minisat+) Z 7869 28099 28098 0 -1 12 40891 0 0 0 119901 125 0 0 25 0 1 0 545727842 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.09
CPU time (s): 1200.27
CPU user time (s): 1199.02
CPU system time (s): 1.25081
CPU usage (%): 100.015
Max. virtual memory (Kb): 167860
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####