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/plato.asu.edu/pub/fctp/normalized-mps-v2-13-7-ran10x26.opb
MD5SUM	f8a5d8e99e0f063cb10208b1e5f7bf38
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1277437
Optimality of the best value was proved	NO
Number of terms in the objective function	5460
Biggest coefficient in the objective function	5242880
Number of bits for the biggest coefficient in the objective function	23
Sum of the numbers in the objective function	1567797422
Number of bits of the sum of numbers in the objective function	31
Biggest number in a constraint	5242880
Number of bits of the biggest number in a constraint	23
Biggest sum of numbers in a constraint	1567797422
Number of bits of the biggest sum of numbers	31
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.04
Number of variables	5460
Total number of constraints	296
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	296
Minimum length of a constraint	21
Maximum length of a constraint	520
Trace number 17669

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc6 THE 2005-04-21 11:13:12 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19250 boxname=wulflinc6 idbench=1481 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  f8a5d8e99e0f063cb10208b1e5f7bf38  /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-ran10x26.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-ran10x26.opb /oldhome/oroussel/tmp/wulflinc6/normalized-mps-v2-13-7-ran10x26.opb
IDLAUNCH: 19250
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.042
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	: 2
cpu MHz		: 451.042
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:        509760 kB
Buffers:         24692 kB
Cached:         477684 kB
SwapCached:        552 kB
Active:          47688 kB
Inactive:       456696 kB
HighTotal:      131008 kB
HighFree:         3780 kB
LowTotal:       903652 kB
LowFree:        505980 kB
SwapTotal:     2097136 kB
SwapFree:      2095720 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5112 kB
Slab:            14824 kB
Committed_AS:    63596 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:33:14 (client local time) WITH STATUS 0 IN 1200.44 SECONDS
stats: 19250 7 1200.44 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 332 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ####################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 330]---> Adder-cost: 538   maxlim: 57062   bits: 16/16
c ---[ 328]---> Adder-cost: 536   maxlim: 52326   bits: 16/16
c ---[ 326]---> Adder-cost: 536   maxlim: 52582   bits: 16/16
c ---[ 324]---> Adder-cost: 536   maxlim: 53094   bits: 16/16
c ---[ 322]---> Adder-cost: 536   maxlim: 53606   bits: 16/16
c ---[ 320]---> Adder-cost: 538   maxlim: 58982   bits: 16/16
c ---[ 318]---> Adder-cost: 522   maxlim: 38502   bits: 16/16
c ---[ 316]---> Adder-cost: 538   maxlim: 57574   bits: 16/16
c ---[ 314]---> Adder-cost: 536   maxlim: 53990   bits: 16/16
c ---[ 312]---> Adder-cost: 538   maxlim: 56806   bits: 16/16
c ---[ 310]---> Adder-cost: 216   maxlim: 36214   bits: 16/16
c ---[ 308]---> Adder-cost: 198   maxlim: 19446   bits: 15/15
c ---[ 306]---> Adder-cost: 216   maxlim: 35190   bits: 16/16
c ---[ 304]---> Adder-cost: 222   maxlim: 48118   bits: 16/16
c ---[ 302]---> Adder-cost: 180   maxlim: 9718   bits: 14/14
c ---[ 300]---> Adder-cost: 180   maxlim: 9462   bits: 14/14
c ---[ 298]---> Adder-cost: 216   maxlim: 35446   bits: 16/16
c ---[ 296]---> Adder-cost: 162   maxlim: 4854   bits: 13/13
c ---[ 294]---> Adder-cost: 198   maxlim: 19446   bits: 15/15
c ---[ 292]---> Adder-cost: 198   maxlim: 19446   bits: 15/15
c ---[ 290]---> Adder-cost: 216   maxlim: 35062   bits: 16/16
c ---[ 288]---> Adder-cost: 198   maxlim: 19062   bits: 15/15
c ---[ 286]---> Adder-cost: 198   maxlim: 18678   bits: 15/15
c ---[ 284]---> Adder-cost: 180   maxlim: 9462   bits: 14/14
c ---[ 282]---> Adder-cost: 216   maxlim: 36854   bits: 16/16
c ---[ 280]---> Adder-cost: 222   maxlim: 51062   bits: 16/16
c ---[ 278]---> Adder-cost: 180   maxlim: 9718   bits: 14/14
c ---[ 276]---> Adder-cost: 180   maxlim: 9462   bits: 14/14
c ---[ 274]---> Adder-cost: 162   maxlim: 4726   bits: 13/13
c ---[ 272]---> Adder-cost: 198   maxlim: 19190   bits: 15/15
c ---[ 270]---> Adder-cost: 198   maxlim: 19062   bits: 15/15
c ---[ 268]---> Adder-cost: 216   maxlim: 36470   bits: 16/16
c ---[ 266]---> Adder-cost: 162   maxlim: 4726   bits: 13/13
c ---[ 264]---> Adder-cost: 180   maxlim: 9462   bits: 14/14
c ---[ 262]---> Adder-cost: 162   maxlim: 4854   bits: 13/13
c ---[ 260]---> Adder-cost: 180   maxlim: 9334   bits: 14/14
c ---[ 259]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 258]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 257]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 256]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 255]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 254]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 253]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 252]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 251]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 250]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 249]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 248]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 247]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 246]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 245]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 244]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 243]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 242]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 241]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 240]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 239]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 238]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 237]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 236]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 235]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 234]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 233]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 232]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 231]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 230]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 229]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 228]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 227]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 226]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 225]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 224]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 223]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 222]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 221]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 220]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 219]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 218]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 217]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 216]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 215]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 214]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 213]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 212]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 211]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 210]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 209]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 208]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 207]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 206]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 205]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 204]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 203]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 202]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 201]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 200]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 199]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 198]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 197]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 196]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 195]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 194]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 193]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 192]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 191]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 190]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 189]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 188]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 187]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 186]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 185]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 184]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 183]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 182]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 181]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 180]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 179]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 178]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 177]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 176]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 175]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 174]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 173]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 172]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 171]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 170]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 169]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 168]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 167]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 166]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 165]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 164]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 163]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 162]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 161]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 160]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 159]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 158]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 157]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 156]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 155]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 154]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 153]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 152]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 151]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 150]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 149]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 148]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 147]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 146]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 145]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 144]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 143]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 142]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 141]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 140]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 139]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 138]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 137]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 136]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 135]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 134]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 133]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 132]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 131]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 130]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 129]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 127]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 126]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 125]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 124]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 123]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 122]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 121]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 120]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 119]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 118]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 117]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 116]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 114]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 113]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 112]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 111]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 110]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 109]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 108]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 107]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 106]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 105]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 104]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 103]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 102]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 101]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 100]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  99]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  98]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  97]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  96]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[  95]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  94]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  92]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  91]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  90]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  89]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  88]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  87]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  86]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  85]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  84]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  83]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  82]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  80]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  79]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  77]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  76]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  75]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  74]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  73]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  72]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  71]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  70]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  69]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  68]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  67]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  66]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  65]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  64]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  63]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  62]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  61]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  59]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  58]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  57]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  56]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  55]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  54]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  53]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  52]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  51]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  50]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  49]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  48]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  47]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  45]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  44]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  42]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  41]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  40]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  39]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  38]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  37]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  36]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  35]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  34]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  32]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  31]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  30]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  28]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  27]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  26]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  25]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  24]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  23]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  22]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  21]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  20]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  18]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  17]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  16]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  15]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  13]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  12]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  11]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  10]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   9]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   7]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   5]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   4]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   3]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   2]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   0]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   78629   289855 |   26209       0        0     nan |  0.000 % |
c |       100 |   78629   289855 |   28829     100      279     2.8 | 30.890 % |
c |       250 |   78629   289855 |   31712     250      784     3.1 | 30.890 % |
c |       475 |   78498   289408 |   34884     461     1662     3.6 | 31.002 % |
c |       812 |   78480   289350 |   38372     796     3858     4.8 | 31.021 % |
c |      1318 |   78336   288870 |   42209    1288     7031     5.5 | 31.148 % |
c |      2077 |   78055   287917 |   46430    2016     9956     4.9 | 31.391 % |
c |      3216 |   77866   287286 |   51073    3131    16365     5.2 | 31.561 % |
c |      4924 |   77401   285697 |   56181    4765    24052     5.0 | 31.960 % |
c |      7486 |   77010   284354 |   61799    7278    36129     5.0 | 32.296 % |
c |     11330 |   76696   283280 |   67979   11082    54530     4.9 | 32.563 % |
c |     17096 |   76333   282047 |   74777   16804    83777     5.0 | 32.889 % |
c |     25745 |   76106   281308 |   82255   25418   140859     5.5 | 33.098 % |
c |     38719 |   75930   280726 |   90480   38365   243811     6.4 | 33.249 % |
c |     58180 |   75855   280465 |   99528   57813   432406     7.5 | 33.307 % |
c |     87372 |   75790   280252 |  109481   86994   828656     9.5 | 33.366 % |
c |    131163 |   75781   280223 |  120429   44183   365033     8.3 | 33.375 % |
c |    196847 |   75767   280177 |  132472  109865  1433929    13.1 | 33.385 % |
c |    295373 |   75742   280094 |  145719  101813  1504086    14.8 | 33.405 % |
c |    443162 |   75716   280004 |  160291  126580  1795660    14.2 | 33.424 % |
c |    664846 |   75668   279844 |  176321   78810   888580    11.3 | 33.468 % |
c |    997372 |   75652   279792 |  193953   93910  1507409    16.1 | 33.483 % |
#### 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.70 0.91 0.90 2/54 15778
Raw data (stat): 15778 (runsolver) R 15777 29653 29652 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486407552 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.75 0.91 0.90 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 2358 0 0 0 992 7 0 0 25 0 1 0 486407552 11841536 2283 4294967295 134512640 134672761 3221224544 3221223716 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2891 2283 603 41 0 2850 0
vsize: 11564
[startup+20.0006 s]
Raw data (loadavg): 0.79 0.91 0.90 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 2431 0 0 0 1991 7 0 0 25 0 1 0 486407552 12247040 2356 4294967295 134512640 134672761 3221224544 3221223716 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2990 2356 603 41 0 2949 0
vsize: 11960
[startup+30.0004 s]
Raw data (loadavg): 0.82 0.92 0.90 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 2517 0 0 0 2991 8 0 0 25 0 1 0 486407552 12595200 2442 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3075 2442 603 41 0 3034 0
vsize: 12300
[startup+40.001 s]
Raw data (loadavg): 0.85 0.92 0.90 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 2619 0 0 0 3990 9 0 0 25 0 1 0 486407552 13000704 2544 4294967295 134512640 134672761 3221224544 3221223668 134566062 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3174 2544 603 41 0 3133 0
vsize: 12696
[startup+50.0011 s]
Raw data (loadavg): 0.87 0.92 0.90 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 2766 0 0 0 4990 10 0 0 25 0 1 0 486407552 13537280 2691 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3305 2691 603 41 0 3264 0
vsize: 13220
[startup+60.0008 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 2900 0 0 0 5989 11 0 0 25 0 1 0 486407552 14204928 2825 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3468 2825 603 41 0 3427 0
vsize: 13872
[startup+70.0014 s]
Raw data (loadavg): 0.91 0.92 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 3075 0 0 0 6989 12 0 0 25 0 1 0 486407552 14880768 3000 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3633 3000 603 41 0 3592 0
vsize: 14532
[startup+80.0016 s]
Raw data (loadavg): 0.92 0.93 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 3256 0 0 0 7988 13 0 0 25 0 1 0 486407552 15556608 3181 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3798 3181 603 41 0 3757 0
vsize: 15192
[startup+90.0013 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 3447 0 0 0 8988 13 0 0 25 0 1 0 486407552 16367616 3372 4294967295 134512640 134672761 3221224544 3221223680 134560697 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3996 3372 603 41 0 3955 0
vsize: 15984
[startup+100.002 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 3614 0 0 0 9987 14 0 0 25 0 1 0 486407552 17305600 3539 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4225 3539 603 41 0 4184 0
vsize: 16900
[startup+110.002 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 3877 0 0 0 10987 15 0 0 25 0 1 0 486407552 18251776 3802 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4456 3802 603 41 0 4415 0
vsize: 17824
[startup+120.002 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4102 0 0 0 11987 16 0 0 25 0 1 0 486407552 19193856 4027 4294967295 134512640 134672761 3221224544 3221223708 134564520 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4686 4027 603 41 0 4645 0
vsize: 18744
[startup+130.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4437 0 0 0 12986 16 0 0 25 0 1 0 486407552 20541440 4362 4294967295 134512640 134672761 3221224544 3221223680 134565064 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5015 4362 603 41 0 4974 0
vsize: 20060
[startup+140.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4647 0 0 0 13985 17 0 0 25 0 1 0 486407552 21352448 4572 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5213 4572 603 41 0 5172 0
vsize: 20852
[startup+150.003 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 14985 18 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+160.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 15985 18 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+170.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 16985 19 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+180.004 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 17985 19 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+190.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 18985 19 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+200.004 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 19985 20 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223648 134560248 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+210.005 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 20985 20 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+220.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 21985 20 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+230.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 4813 0 0 0 22986 20 0 0 25 0 1 0 486407552 22028288 4738 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5378 4738 603 41 0 5337 0
vsize: 21512
[startup+240.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5045 0 0 0 23985 21 0 0 25 0 1 0 486407552 22970368 4970 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5608 4970 603 41 0 5567 0
vsize: 22432
[startup+250.006 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5194 0 0 0 24984 22 0 0 25 0 1 0 486407552 23511040 5119 4294967295 134512640 134672761 3221224544 3221223728 134559498 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5740 5119 603 41 0 5699 0
vsize: 22960
[startup+260.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5442 0 0 0 25984 24 0 0 25 0 1 0 486407552 24584192 5367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6002 5367 603 41 0 5961 0
vsize: 24008
[startup+270.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5645 0 0 0 26983 25 0 0 25 0 1 0 486407552 25780224 5570 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6294 5570 603 41 0 6253 0
vsize: 25176
[startup+280.008 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 27982 26 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+290.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 28982 26 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+300.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 29982 27 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+310.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 30982 27 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+320.009 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 31982 27 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+330.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 32982 27 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+340.01 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 33982 28 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+350.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 34982 28 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223668 134566031 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+360.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 35982 28 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+370.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 36983 28 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+380.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5822 0 0 0 37983 29 0 0 25 0 1 0 486407552 26583040 5747 4294967295 134512640 134672761 3221224544 3221223728 134558934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6490 5747 603 41 0 6449 0
vsize: 25960
[startup+390.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 5972 0 0 0 38982 29 0 0 25 0 1 0 486407552 27123712 5897 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6622 5897 603 41 0 6581 0
vsize: 26488
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6208 0 0 0 39982 30 0 0 25 0 1 0 486407552 28065792 6133 4294967295 134512640 134672761 3221224544 3221223712 134561372 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6852 6133 603 41 0 6811 0
vsize: 27408
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6368 0 0 0 40981 31 0 0 25 0 1 0 486407552 28741632 6293 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7017 6293 603 41 0 6976 0
vsize: 28068
[startup+420.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6545 0 0 0 41981 32 0 0 25 0 1 0 486407552 29417472 6470 4294967295 134512640 134672761 3221224544 3221223708 134565024 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7182 6470 603 41 0 7141 0
vsize: 28728
[startup+430.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 42981 32 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+440.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 43981 33 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+450.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 44981 33 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223680 134565039 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+460.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 45981 33 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+470.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 46981 33 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 47982 33 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+490.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 48982 33 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223792 134562294 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+500.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 49982 34 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+510.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 50982 34 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+520.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 51982 34 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+530.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 52982 34 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 53982 35 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+550.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6573 0 0 0 54982 35 0 0 25 0 1 0 486407552 29552640 6498 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6498 603 41 0 7174 0
vsize: 28860
[startup+560.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6578 0 0 0 55982 35 0 0 25 0 1 0 486407552 29552640 6503 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7215 6503 603 41 0 7174 0
vsize: 28860
[startup+570.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 6895 0 0 0 56982 36 0 0 25 0 1 0 486407552 30900224 6820 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7544 6820 603 41 0 7503 0
vsize: 30176
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 57981 37 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 58981 38 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 59981 38 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+610.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 60981 38 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+620.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 61981 39 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223648 134560514 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 62981 39 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+640.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 63981 39 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+650.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 64981 40 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223728 134559244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+660.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 65981 40 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+670.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 66981 40 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 67982 40 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 68982 40 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 69982 40 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+710.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7117 0 0 0 70983 40 0 0 25 0 1 0 486407552 31711232 7042 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7742 7042 603 41 0 7701 0
vsize: 30968
[startup+720.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7224 0 0 0 71983 41 0 0 25 0 1 0 486407552 32112640 7149 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7840 7149 603 41 0 7799 0
vsize: 31360
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 72982 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223708 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 73983 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 74983 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+760.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 75984 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+770.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 76984 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 77984 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 78984 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+800.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 79985 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223680 134565103 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+810.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 80985 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+820.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 81985 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+830.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7421 0 0 0 82986 41 0 0 25 0 1 0 486407552 32923648 7346 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8038 7346 603 41 0 7997 0
vsize: 32152
[startup+840.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 7453 0 0 0 83986 42 0 0 25 0 1 0 486407552 33058816 7378 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8071 7378 603 41 0 8030 0
vsize: 32284
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 8315 0 0 0 84983 45 0 0 25 0 1 0 486407552 36700160 8240 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8960 8240 603 41 0 8919 0
vsize: 35840
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 8925 0 0 0 85982 47 0 0 25 0 1 0 486407552 39116800 8850 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9550 8850 603 41 0 9509 0
vsize: 38200
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 9695 0 0 0 86979 50 0 0 25 0 1 0 486407552 42323968 9620 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10333 9620 603 41 0 10292 0
vsize: 41332
[startup+880.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 10638 0 0 0 87977 52 0 0 25 0 1 0 486407552 46215168 10563 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11283 10563 603 41 0 11242 0
vsize: 45132
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 11528 0 0 0 88974 55 0 0 25 0 1 0 486407552 49831936 11453 4294967295 134512640 134672761 3221224544 3221223696 134561040 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12166 11454 603 41 0 12125 0
vsize: 48664
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 12377 0 0 0 89973 57 0 0 25 0 1 0 486407552 53297152 12302 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13012 12302 603 41 0 12971 0
vsize: 52048
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13062 0 0 0 90971 59 0 0 25 0 1 0 486407552 56123392 12987 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13702 12987 603 41 0 13661 0
vsize: 54808
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13575 0 0 0 91970 61 0 0 25 0 1 0 486407552 58142720 13500 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14195 13500 603 41 0 14154 0
vsize: 56780
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13858 0 0 0 92969 61 0 0 25 0 1 0 486407552 59351040 13783 4294967295 134512640 134672761 3221224544 3221223728 134559663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14490 13783 603 41 0 14449 0
vsize: 57960
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 93970 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+950.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 94970 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+960.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 95970 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+970.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 96971 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223648 134559933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+980.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 97971 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+990.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 98971 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 99972 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 100972 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 101973 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 102973 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 103973 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 104974 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 105974 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1070.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 106975 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1080.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 107975 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1090.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 108975 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1100.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 109976 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1110.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 110976 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 111976 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 112977 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223680 134560590 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 113977 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 114977 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 115978 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223700 134561241 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 116978 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 117979 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1190.05 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 118979 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
[startup+1200.05 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 15778
Raw data (stat): 15778 (minisat+) R 15777 29653 29652 0 -1 0 13986 0 0 0 119979 62 0 0 25 0 1 0 486407552 59748352 13911 4294967295 134512640 134672761 3221224544 3221223668 134566047 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14587 13911 603 41 0 14546 0
vsize: 58348
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.06 0.99 0.91 1/54 15778
Raw data (stat): 15778 (minisat+) Z 15777 29653 29652 0 -1 12 13988 0 0 0 119979 64 0 0 25 0 1 0 486407552 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.08
CPU time (s): 1200.44
CPU user time (s): 1199.8
CPU system time (s): 0.648901
CPU usage (%): 100.031
Max. virtual memory (Kb): 58348
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####