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-ran12x21.opb
MD5SUM	0d744fe957d41a18692933adc6be4af7
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1493203
Optimality of the best value was proved	NO
Number of terms in the objective function	5292
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	1511880035
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	1511880035
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	5292
Total number of constraints	285
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	285
Minimum length of a constraint	21
Maximum length of a constraint	420
Trace number 17656

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc21 THE 2005-04-21 11:08:24 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19276 boxname=wulflinc21 idbench=1483 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  0d744fe957d41a18692933adc6be4af7  /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-ran12x21.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-ran12x21.opb /oldhome/oroussel/tmp/wulflinc21/normalized-mps-v2-13-7-ran12x21.opb
IDLAUNCH: 19276
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.161
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:        503772 kB
Buffers:          3060 kB
Cached:         505104 kB
SwapCached:          0 kB
Active:          68080 kB
Inactive:       442968 kB
HighTotal:      131008 kB
HighFree:        19656 kB
LowTotal:       903652 kB
LowFree:        484116 kB
SwapTotal:     2097892 kB
SwapFree:      2097804 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            14164 kB
Committed_AS:    63796 kB
PageTables:        332 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:28:26 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 19276 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 318 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: #################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 316]---> Adder-cost: 428   maxlim: 44523   bits: 16/16
c ---[ 314]---> Adder-cost: 428   maxlim: 45163   bits: 16/16
c ---[ 312]---> Adder-cost: 434   maxlim: 55787   bits: 16/16
c ---[ 310]---> Adder-cost: 428   maxlim: 44395   bits: 16/16
c ---[ 308]---> Adder-cost: 428   maxlim: 43627   bits: 16/16
c ---[ 306]---> Adder-cost: 428   maxlim: 43755   bits: 16/16
c ---[ 304]---> Adder-cost: 428   maxlim: 44267   bits: 16/16
c ---[ 302]---> Adder-cost: 412   maxlim: 29419   bits: 15/15
c ---[ 300]---> Adder-cost: 428   maxlim: 44651   bits: 16/16
c ---[ 298]---> Adder-cost: 428   maxlim: 45035   bits: 16/16
c ---[ 296]---> Adder-cost: 434   maxlim: 51819   bits: 16/16
c ---[ 294]---> Adder-cost: 412   maxlim: 29547   bits: 15/15
c ---[ 292]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 290]---> Adder-cost: 242   maxlim: 23540   bits: 15/15
c ---[ 288]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 286]---> Adder-cost: 262   maxlim: 42356   bits: 16/16
c ---[ 284]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 282]---> Adder-cost: 262   maxlim: 41332   bits: 16/16
c ---[ 280]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 278]---> Adder-cost: 266   maxlim: 46836   bits: 16/16
c ---[ 276]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 274]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 272]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 270]---> Adder-cost: 220   maxlim: 11380   bits: 14/14
c ---[ 268]---> Adder-cost: 198   maxlim: 5876   bits: 13/13
c ---[ 266]---> Adder-cost: 262   maxlim: 41588   bits: 16/16
c ---[ 264]---> Adder-cost: 198   maxlim: 5748   bits: 13/13
c ---[ 262]---> Adder-cost: 262   maxlim: 42612   bits: 16/16
c ---[ 260]---> Adder-cost: 220   maxlim: 11636   bits: 14/14
c ---[ 258]---> Adder-cost: 242   maxlim: 22644   bits: 15/15
c ---[ 256]---> Adder-cost: 266   maxlim: 48372   bits: 16/16
c ---[ 254]---> Adder-cost: 266   maxlim: 49140   bits: 16/16
c ---[ 252]---> Adder-cost: 242   maxlim: 23412   bits: 15/15
c ---[ 251]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 250]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 249]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 248]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 247]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 246]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 245]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 244]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 243]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 242]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 241]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 240]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 239]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 238]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 237]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 236]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 235]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 234]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 233]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 232]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 231]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 230]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 229]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 228]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 227]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 226]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 225]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 224]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 223]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 222]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 221]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 220]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 219]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 218]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 217]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 216]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 215]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 214]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 213]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 212]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 211]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 210]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 209]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 208]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 207]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 206]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 205]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 204]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 203]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 202]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 201]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 200]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 199]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 198]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 197]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 196]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 195]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 194]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 193]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 192]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 191]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 190]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 189]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 188]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 187]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 186]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 185]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 184]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 183]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 182]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 181]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 180]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 179]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 178]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 177]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 176]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 175]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 174]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 173]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 172]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 171]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 170]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 169]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 168]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 167]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 166]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 165]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 164]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 163]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 162]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 161]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 160]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 159]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 158]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 156]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 155]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 154]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 153]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 152]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 151]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 150]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 149]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 148]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 147]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 146]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 145]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 144]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 143]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 142]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 141]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 140]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 139]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 138]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[ 137]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 136]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 135]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 134]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 132]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 131]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 130]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 129]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 127]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 126]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 125]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 124]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 123]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 122]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 121]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 120]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 119]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 118]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 117]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 114]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 113]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 112]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 111]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 110]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 109]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 108]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 107]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 106]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 105]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 104]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 103]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 102]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 101]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 100]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  99]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  98]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  97]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  96]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  95]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  94]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  93]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  92]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  91]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  90]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  89]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  88]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  87]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  86]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  85]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  83]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  82]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  81]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  80]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  79]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  78]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  77]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  76]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  75]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  74]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  73]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  72]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  71]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  70]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  69]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  68]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  67]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  66]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  65]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  64]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  63]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  62]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  61]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  60]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  59]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  58]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  57]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  56]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  54]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  53]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  52]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  51]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  50]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  49]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  48]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  47]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  46]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  45]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  44]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  42]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  41]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  40]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  39]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  38]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  37]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  36]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  35]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  34]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  33]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  32]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  31]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  30]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  29]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  28]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  27]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  26]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  25]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  24]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  23]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  22]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  21]---> Adder-cost: 4   maxlim: 4094   bits: 13/12
c ---[  20]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  19]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  18]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  17]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  16]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  15]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  14]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  13]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  12]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  11]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  10]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   8]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[   7]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   4]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   3]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   2]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[   1]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[   0]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77489   285151 |   25829       0        0     nan |  0.000 % |
c |       100 |   77489   285151 |   28411     100      277     2.8 | 30.173 % |
c |       250 |   77481   285121 |   31253     249     1120     4.5 | 30.178 % |
c |       475 |   77407   284873 |   34378     460     2102     4.6 | 30.243 % |
c |       812 |   77356   284700 |   37816     792     4619     5.8 | 30.288 % |
c |      1318 |   77214   284200 |   41597    1273     6725     5.3 | 30.398 % |
c |      2077 |   76878   283054 |   45757    1981     9617     4.9 | 30.701 % |
c |      3217 |   76647   282277 |   50333    3078    15060     4.9 | 30.911 % |
c |      4925 |   76458   281622 |   55366    4764    25150     5.3 | 31.075 % |
c |      7487 |   76290   281054 |   60903    7303    37607     5.1 | 31.224 % |
c |     11331 |   75836   279486 |   66993   11084    56883     5.1 | 31.623 % |
c |     17100 |   75636   278820 |   73693   16820    89408     5.3 | 31.792 % |
c |     25749 |   74902   276354 |   81062   25364   148843     5.9 | 32.430 % |
c |     38723 |   74628   275422 |   89168   38300   238432     6.2 | 32.684 % |
c |     58184 |   74473   274909 |   98085   57737   420827     7.3 | 32.824 % |
c |     87377 |   74409   274699 |  107894   86919  1238239    14.2 | 32.883 % |
c |    131166 |   74318   274392 |  118683   43360   402801     9.3 | 32.958 % |
c |    196850 |   74312   274372 |  130551  109043  2359469    21.6 | 32.963 % |
c |    295376 |   74312   274372 |  143607   99091  1626158    16.4 | 32.963 % |
c |    443165 |   74297   274321 |  157967  128132  2281840    17.8 | 32.973 % |
c |    664849 |   74288   274290 |  173764   75541  1451286    19.2 | 32.978 % |
c |    997374 |   74255   274179 |  191141  113265  2401751    21.2 | 33.008 % |
#### 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.93 0.97 0.91 2/55 10566
Raw data (stat): 10566 (runsolver) R 10565 30927 30926 0 -1 64 4 0 0 0 0 0 0 0 20 0 1 0 421864386 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0005 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 2357 0 0 0 994 5 0 0 25 0 1 0 421864386 11952128 2282 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2918 2282 603 41 0 2877 0
vsize: 11672
[startup+20.0012 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 2442 0 0 0 1993 5 0 0 25 0 1 0 421864386 12218368 2367 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 2983 2367 603 41 0 2942 0
vsize: 11932
[startup+30.0008 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 2531 0 0 0 2994 5 0 0 25 0 1 0 421864386 12705792 2456 4294967295 134512640 134672761 3221224544 3221223668 134566077 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3102 2456 603 41 0 3061 0
vsize: 12408
[startup+40.0005 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 2614 0 0 0 3993 6 0 0 25 0 1 0 421864386 12976128 2539 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3168 2539 603 41 0 3127 0
vsize: 12672
[startup+50.0007 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 2705 0 0 0 4993 6 0 0 25 0 1 0 421864386 13377536 2630 4294967295 134512640 134672761 3221224544 3221223784 134560737 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3266 2630 603 41 0 3225 0
vsize: 13064
[startup+60.0009 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 2818 0 0 0 5993 6 0 0 25 0 1 0 421864386 13910016 2743 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3396 2743 603 41 0 3355 0
vsize: 13584
[startup+70.0016 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 2921 0 0 0 6993 7 0 0 25 0 1 0 421864386 14315520 2846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3495 2846 603 41 0 3454 0
vsize: 13980
[startup+80.0013 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 3036 0 0 0 7992 7 0 0 25 0 1 0 421864386 14721024 2961 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3594 2961 603 41 0 3553 0
vsize: 14376
[startup+90.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 3195 0 0 0 8992 7 0 0 25 0 1 0 421864386 15396864 3120 4294967295 134512640 134672761 3221224544 3221223712 134560964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3759 3120 603 41 0 3718 0
vsize: 15036
[startup+100.001 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 3419 0 0 0 9992 8 0 0 25 0 1 0 421864386 16203776 3344 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3956 3344 603 41 0 3915 0
vsize: 15824
[startup+110.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 3927 0 0 0 10991 9 0 0 25 0 1 0 421864386 18481152 3852 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4512 3852 603 41 0 4471 0
vsize: 18048
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 4314 0 0 0 11990 10 0 0 25 0 1 0 421864386 20090880 4239 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4905 4239 603 41 0 4864 0
vsize: 19620
[startup+130.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 4536 0 0 0 12989 11 0 0 25 0 1 0 421864386 20897792 4461 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5102 4461 603 41 0 5061 0
vsize: 20408
[startup+140.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 4778 0 0 0 13989 12 0 0 25 0 1 0 421864386 21843968 4703 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5333 4703 603 41 0 5292 0
vsize: 21332
[startup+150.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5138 0 0 0 14987 13 0 0 25 0 1 0 421864386 23322624 5063 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5694 5063 603 41 0 5653 0
vsize: 22776
[startup+160.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5228 0 0 0 15987 13 0 0 25 0 1 0 421864386 23728128 5153 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5153 603 41 0 5752 0
vsize: 23172
[startup+170.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5228 0 0 0 16987 13 0 0 25 0 1 0 421864386 23728128 5153 4294967295 134512640 134672761 3221224544 3221223692 134560552 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5153 603 41 0 5752 0
vsize: 23172
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5228 0 0 0 17987 13 0 0 25 0 1 0 421864386 23728128 5153 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5153 603 41 0 5752 0
vsize: 23172
[startup+190.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5228 0 0 0 18988 13 0 0 25 0 1 0 421864386 23728128 5153 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5153 603 41 0 5752 0
vsize: 23172
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5228 0 0 0 19988 13 0 0 25 0 1 0 421864386 23728128 5153 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5153 603 41 0 5752 0
vsize: 23172
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5228 0 0 0 20988 13 0 0 25 0 1 0 421864386 23728128 5153 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5793 5153 603 41 0 5752 0
vsize: 23172
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5274 0 0 0 21988 14 0 0 25 0 1 0 421864386 23863296 5199 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5826 5199 603 41 0 5785 0
vsize: 23304
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 5932 0 0 0 22986 16 0 0 25 0 1 0 421864386 26550272 5857 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6482 5857 603 41 0 6441 0
vsize: 25928
[startup+240 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 6170 0 0 0 23985 17 0 0 25 0 1 0 421864386 27492352 6095 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6712 6095 603 41 0 6671 0
vsize: 26848
[startup+250 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 6621 0 0 0 24984 19 0 0 25 0 1 0 421864386 29376512 6546 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7172 6546 603 41 0 7131 0
vsize: 28688
[startup+260.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 6967 0 0 0 25983 19 0 0 25 0 1 0 421864386 31252480 6892 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7630 6892 603 41 0 7589 0
vsize: 30520
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 26983 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 27984 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223668 134566068 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 28984 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+300.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 29984 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223688 134565969 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+310.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 30984 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+320.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 31984 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 32984 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 33984 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 34985 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 35985 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 36985 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223648 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+380.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7065 0 0 0 37985 20 0 0 25 0 1 0 421864386 31657984 6990 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6990 603 41 0 7688 0
vsize: 30916
[startup+390.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7069 0 0 0 38985 20 0 0 25 0 1 0 421864386 31657984 6994 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 6994 603 41 0 7688 0
vsize: 30916
[startup+400.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7077 0 0 0 39985 20 0 0 25 0 1 0 421864386 31657984 7002 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7002 603 41 0 7688 0
vsize: 30916
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 40986 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223668 134566057 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 41986 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+430.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 42986 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 43986 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 44986 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+460.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 45986 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+470.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 46987 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 47987 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223696 134565048 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 48987 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 49987 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223728 134559601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 50987 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7079 0 0 0 51988 20 0 0 25 0 1 0 421864386 31657984 7004 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7729 7004 603 41 0 7688 0
vsize: 30916
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 7367 0 0 0 52988 20 0 0 25 0 1 0 421864386 32862208 7292 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8023 7292 603 41 0 7982 0
vsize: 32092
[startup+540.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8065 0 0 0 53986 21 0 0 25 0 1 0 421864386 35676160 7990 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8710 7990 603 41 0 8669 0
vsize: 34840
[startup+550.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 54986 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+560.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 55986 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+570.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 56987 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 57987 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 58987 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+600.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 59987 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 60987 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+620.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 61987 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+630.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 62988 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 63988 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8091 0 0 0 64988 22 0 0 25 0 1 0 421864386 35811328 8016 4294967295 134512640 134672761 3221224544 3221223712 134561378 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8743 8016 603 41 0 8702 0
vsize: 34972
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8398 0 0 0 65988 22 0 0 25 0 1 0 421864386 37019648 8323 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9038 8323 603 41 0 8997 0
vsize: 36152
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 8871 0 0 0 66987 23 0 0 25 0 1 0 421864386 38912000 8796 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9500 8796 603 41 0 9459 0
vsize: 38000
[startup+680.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9053 0 0 0 67986 24 0 0 25 0 1 0 421864386 39718912 8978 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9697 8978 603 41 0 9656 0
vsize: 38788
[startup+690.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9254 0 0 0 68986 25 0 0 25 0 1 0 421864386 40521728 9179 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9893 9179 603 41 0 9852 0
vsize: 39572
[startup+700.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9680 0 0 0 69985 26 0 0 25 0 1 0 421864386 42266624 9605 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10319 9605 603 41 0 10278 0
vsize: 41276
[startup+710.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 70985 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223668 134566118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+720.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 71985 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+730.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 72985 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+740.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 73986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+750.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 74986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+760.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 75986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+770.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 76986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+780.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 77986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223668 134566082 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 78986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 79986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223684 134565972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+810.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 80986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223688 134560553 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+820.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 81986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223728 134559516 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+830.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 82986 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+840.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 83987 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+850.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9733 0 0 0 84987 26 0 0 25 0 1 0 421864386 42536960 9658 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9658 603 41 0 10344 0
vsize: 41540
[startup+860.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9736 0 0 0 85987 26 0 0 25 0 1 0 421864386 42536960 9661 4294967295 134512640 134672761 3221224544 3221223712 134561161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9661 603 41 0 10344 0
vsize: 41540
[startup+870.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9744 0 0 0 86987 26 0 0 25 0 1 0 421864386 42536960 9669 4294967295 134512640 134672761 3221224544 3221223696 134565127 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9669 603 41 0 10344 0
vsize: 41540
[startup+880.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 87987 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+890.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 88987 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+900.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 89988 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+910.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 90988 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+920.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 91988 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+930.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 92988 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+940.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 93988 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+950.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 94988 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223680 134560703 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+960.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 95989 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223808 134562244 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+970.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 96989 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223728 134558934 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+980.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 97989 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+990.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 98989 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 99989 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 100989 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 101990 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 102990 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223668 134565995 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9748 0 0 0 103990 26 0 0 25 0 1 0 421864386 42536960 9673 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9673 603 41 0 10344 0
vsize: 41540
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 104990 26 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 105990 26 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 106990 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 107991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1090.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 108991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 109991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 110991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 111991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 112992 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1140.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 113992 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 114991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 115991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 116991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 117991 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1190.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 118992 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
[startup+1200.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 10566
Raw data (stat): 10566 (minisat+) R 10565 30927 30926 0 -1 0 9749 0 0 0 119992 27 0 0 25 0 1 0 421864386 42536960 9674 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10385 9674 603 41 0 10344 0
vsize: 41540
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 10566
Raw data (stat): 10566 (minisat+) Z 10565 30927 30926 0 -1 12 9751 0 0 0 119992 29 0 0 25 0 1 0 421864386 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.03
CPU time (s): 1200.22
CPU user time (s): 1199.92
CPU system time (s): 0.294955
CPU usage (%): 100.016
Max. virtual memory (Kb): 41540
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####