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-ran8x32.opb
MD5SUM	ff0017de67077abd1f68238274b64e50
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	1695644
Optimality of the best value was proved	NO
Number of terms in the objective function	5376
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	1517603678
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	1517603678
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.03
Number of variables	5376
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	640
Trace number 17597

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc7 THE 2005-04-21 10:51:06 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=19367 boxname=wulflinc7 idbench=1490 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  ff0017de67077abd1f68238274b64e50  /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran8x32.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran8x32.opb /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-13-7-ran8x32.opb
IDLAUNCH: 19367
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.050
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	: 2
cpu MHz		: 451.050
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:        688788 kB
Buffers:         10532 kB
Cached:         313212 kB
SwapCached:          4 kB
Active:         155036 kB
Inactive:       171584 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        688536 kB
SwapTotal:     2097136 kB
SwapFree:      2097128 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6936 kB
Slab:            13532 kB
Committed_AS:    63592 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 11:11:08 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 19367 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 336 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ########################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 334]---> Adder-cost: 646   maxlim: 45920   bits: 16/16
c ---[ 332]---> Adder-cost: 670   maxlim: 69856   bits: 17/17
c ---[ 330]---> Adder-cost: 670   maxlim: 67552   bits: 17/17
c ---[ 328]---> Adder-cost: 670   maxlim: 71392   bits: 17/17
c ---[ 326]---> Adder-cost: 670   maxlim: 71904   bits: 17/17
c ---[ 324]---> Adder-cost: 670   maxlim: 71904   bits: 17/17
c ---[ 322]---> Adder-cost: 670   maxlim: 70368   bits: 17/17
c ---[ 320]---> Adder-cost: 670   maxlim: 64608   bits: 17/16
c ---[ 318]---> Adder-cost: 126   maxlim: 3832   bits: 12/12
c ---[ 316]---> Adder-cost: 154   maxlim: 14968   bits: 14/14
c ---[ 314]---> Adder-cost: 140   maxlim: 7416   bits: 13/13
c ---[ 312]---> Adder-cost: 182   maxlim: 53880   bits: 16/16
c ---[ 310]---> Adder-cost: 168   maxlim: 27896   bits: 15/15
c ---[ 308]---> Adder-cost: 154   maxlim: 15224   bits: 14/14
c ---[ 306]---> Adder-cost: 154   maxlim: 15352   bits: 14/14
c ---[ 304]---> Adder-cost: 140   maxlim: 7288   bits: 13/13
c ---[ 302]---> Adder-cost: 154   maxlim: 15096   bits: 14/14
c ---[ 300]---> Adder-cost: 112   maxlim: 1912   bits: 11/11
c ---[ 298]---> Adder-cost: 168   maxlim: 28408   bits: 15/15
c ---[ 296]---> Adder-cost: 140   maxlim: 7672   bits: 13/13
c ---[ 294]---> Adder-cost: 182   maxlim: 53752   bits: 16/16
c ---[ 292]---> Adder-cost: 126   maxlim: 3704   bits: 12/12
c ---[ 290]---> Adder-cost: 140   maxlim: 7544   bits: 13/13
c ---[ 288]---> Adder-cost: 140   maxlim: 7288   bits: 13/13
c ---[ 286]---> Adder-cost: 168   maxlim: 26744   bits: 15/15
c ---[ 284]---> Adder-cost: 154   maxlim: 15224   bits: 14/14
c ---[ 282]---> Adder-cost: 126   maxlim: 3832   bits: 12/12
c ---[ 280]---> Adder-cost: 140   maxlim: 7416   bits: 13/13
c ---[ 278]---> Adder-cost: 140   maxlim: 7416   bits: 13/13
c ---[ 276]---> Adder-cost: 182   maxlim: 55032   bits: 16/16
c ---[ 274]---> Adder-cost: 154   maxlim: 15224   bits: 14/14
c ---[ 272]---> Adder-cost: 126   maxlim: 3704   bits: 12/12
c ---[ 270]---> Adder-cost: 154   maxlim: 15224   bits: 14/14
c ---[ 268]---> Adder-cost: 154   maxlim: 14712   bits: 14/14
c ---[ 266]---> Adder-cost: 168   maxlim: 28408   bits: 15/15
c ---[ 264]---> Adder-cost: 140   maxlim: 7288   bits: 13/13
c ---[ 262]---> Adder-cost: 126   maxlim: 3832   bits: 12/12
c ---[ 260]---> Adder-cost: 168   maxlim: 28408   bits: 15/15
c ---[ 258]---> Adder-cost: 154   maxlim: 14584   bits: 14/14
c ---[ 256]---> Adder-cost: 154   maxlim: 15224   bits: 14/14
c ---[ 255]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 254]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 253]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 252]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 251]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 250]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 249]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 248]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 247]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 246]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 245]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[ 244]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 243]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 242]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 241]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 240]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 239]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 238]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 237]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 236]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 235]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 234]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 233]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 232]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 231]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 230]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 229]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 228]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 227]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 226]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 225]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 224]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 223]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 222]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 221]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 220]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 219]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 218]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 217]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 216]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 215]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 214]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 213]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 212]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 211]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 210]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 209]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 208]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 207]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 206]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 205]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 204]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 203]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 202]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 201]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 200]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 199]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 198]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 197]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 196]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 195]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 194]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 193]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 192]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 191]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 190]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 189]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 188]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 187]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 186]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 185]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 184]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 183]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 182]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 181]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 180]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 179]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 178]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 177]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 176]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 175]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 174]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 173]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 172]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 171]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 170]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 169]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 168]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 167]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 166]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 165]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 164]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 163]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 162]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 161]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 160]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 159]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 158]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 156]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 155]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 154]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 153]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 152]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 151]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 150]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 149]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 148]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 147]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 146]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 145]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 144]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 143]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 142]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 141]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 140]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 139]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 138]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 137]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 136]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 135]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 134]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 133]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 132]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 131]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 130]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 129]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 128]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 127]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 126]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 125]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 124]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 123]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 122]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 121]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 120]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 119]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[ 118]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 117]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 114]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 113]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[ 112]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 111]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 110]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 109]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 108]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[ 107]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 106]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 105]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 104]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 103]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[ 102]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 101]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 100]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  99]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  98]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  97]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  96]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  95]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  94]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  92]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  91]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  90]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  89]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  88]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  87]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  86]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  85]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  84]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  83]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  82]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  81]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  80]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  79]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  78]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  77]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  76]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  75]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  74]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  73]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  72]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  71]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[  70]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  69]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  68]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  67]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  66]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  65]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  64]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  63]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  62]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  61]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  60]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  59]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  58]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  57]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  56]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  54]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  53]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  52]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  51]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  50]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  49]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  48]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  47]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  46]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  45]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  44]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  43]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  42]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[  41]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  37]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 8   maxlim: 8190   bits: 14/13
c ---[  35]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  34]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  33]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  32]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  31]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  30]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  29]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  28]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  26]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  25]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  24]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  23]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  22]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  21]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  20]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  18]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  17]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  16]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  15]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  14]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[  13]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  12]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  11]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[  10]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   8]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[   7]---> Adder-cost: 10   maxlim: 8190   bits: 14/13
c ---[   6]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   5]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   4]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   3]---> Adder-cost: 2   maxlim: 510   bits: 10/9
c ---[   2]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 6   maxlim: 8190   bits: 14/13
c ---[   0]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   77223   283835 |   25741       0        0     nan |  0.000 % |
c |       100 |   77223   283835 |   28315     100      282     2.8 | 30.795 % |
c |       250 |   77182   283692 |   31146     247      752     3.0 | 30.829 % |
c |       475 |   77168   283646 |   34261     470     1597     3.4 | 30.839 % |
c |       812 |   77126   283498 |   37687     798     3113     3.9 | 30.874 % |
c |      1318 |   77058   283268 |   41456    1289     5356     4.2 | 30.928 % |
c |      2077 |   76894   282724 |   45601    2020     8602     4.3 | 31.076 % |
c |      3216 |   76730   282170 |   50161    3134    14129     4.5 | 31.219 % |
c |      4924 |   76582   281672 |   55178    4817    22605     4.7 | 31.337 % |
c |      7486 |   76175   280301 |   60695    7321    34994     4.8 | 31.691 % |
c |     11330 |   75857   279227 |   66765   11108    54717     4.9 | 31.987 % |
c |     17097 |   75387   277655 |   73442   16806    84704     5.0 | 32.416 % |
c |     25746 |   75242   277158 |   80786   25440   134728     5.3 | 32.549 % |
c |     38720 |   75003   276367 |   88864   38380   228972     6.0 | 32.770 % |
c |     58181 |   74812   275730 |   97751   57812   483170     8.4 | 32.938 % |
c |     87375 |   74778   275620 |  107526   87000  1693519    19.5 | 32.972 % |
c |    131164 |   74677   275289 |  118279   44486   817884    18.4 | 33.071 % |
c |    196848 |   74661   275237 |  130107  110168  2349718    21.3 | 33.085 % |
c |    295374 |   74661   275237 |  143117   92826  2933890    31.6 | 33.085 % |
c |    443163 |   74661   275237 |  157429  122212  3710157    30.4 | 33.085 % |
c |    664846 |   74661   275237 |  173172   58176  6773123   116.4 | 33.085 % |
#### 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.80 0.93 0.90 2/54 5169
Raw data (stat): 5169 (runsolver) R 5168 22932 22931 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 486280521 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.037 s]
Raw data (loadavg): 0.83 0.93 0.90 5/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 2352 0 0 0 987 4 0 0 25 0 1 0 486280521 12001280 2277 4294967295 134512640 134672761 3221224544 3221223680 134565096 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2930 2277 603 41 0 2889 0
vsize: 11720
[startup+20.0454 s]
Raw data (loadavg): 0.85 0.93 0.90 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 2436 0 0 0 1987 4 0 0 25 0 1 0 486280521 12271616 2361 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 2996 2361 603 41 0 2955 0
vsize: 11984
[startup+30.045 s]
Raw data (loadavg): 0.87 0.93 0.90 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 2524 0 0 0 2987 5 0 0 25 0 1 0 486280521 12754944 2449 4294967295 134512640 134672761 3221224544 3221223744 134557895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3114 2449 603 41 0 3073 0
vsize: 12456
[startup+40.045 s]
Raw data (loadavg): 0.89 0.93 0.90 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 2611 0 0 0 3987 5 0 0 25 0 1 0 486280521 13025280 2536 4294967295 134512640 134672761 3221224544 3221223744 134557897 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3180 2536 603 41 0 3139 0
vsize: 12720
[startup+50.0453 s]
Raw data (loadavg): 0.91 0.94 0.90 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 2702 0 0 0 4986 6 0 0 25 0 1 0 486280521 13430784 2627 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3279 2627 603 41 0 3238 0
vsize: 13116
[startup+60.0449 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 2801 0 0 0 5986 6 0 0 25 0 1 0 486280521 13963264 2726 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3409 2726 603 41 0 3368 0
vsize: 13636
[startup+70.0462 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 2893 0 0 0 6986 6 0 0 25 0 1 0 486280521 14233600 2818 4294967295 134512640 134672761 3221224544 3221223728 134558925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3475 2818 603 41 0 3434 0
vsize: 13900
[startup+80.0462 s]
Raw data (loadavg): 0.94 0.94 0.90 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 3148 0 0 0 7985 7 0 0 25 0 1 0 486280521 15314944 3073 4294967295 134512640 134672761 3221224544 3221223668 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3739 3073 603 41 0 3698 0
vsize: 14956
[startup+90.0458 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 3270 0 0 0 8985 8 0 0 25 0 1 0 486280521 15720448 3195 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3195 603 41 0 3797 0
vsize: 15352
[startup+100.046 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 3418 0 0 0 9985 8 0 0 25 0 1 0 486280521 16388096 3343 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4001 3343 603 41 0 3960 0
vsize: 16004
[startup+110.045 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 3661 0 0 0 10985 9 0 0 25 0 1 0 486280521 17596416 3586 4294967295 134512640 134672761 3221224544 3221223500 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4296 3586 603 41 0 4255 0
vsize: 17184
[startup+120.045 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 4541 0 0 0 11983 11 0 0 25 0 1 0 486280521 21082112 4466 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5147 4466 603 41 0 5106 0
vsize: 20588
[startup+130.045 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 4932 0 0 0 12982 12 0 0 25 0 1 0 486280521 22704128 4857 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5543 4857 603 41 0 5502 0
vsize: 22172
[startup+140.046 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 5214 0 0 0 13981 13 0 0 25 0 1 0 486280521 23785472 5139 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5807 5139 603 41 0 5766 0
vsize: 23228
[startup+150.046 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6249 0 0 0 14978 16 0 0 25 0 1 0 486280521 27959296 6174 4294967295 134512640 134672761 3221224544 3221223716 134556651 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6826 6174 603 41 0 6785 0
vsize: 27304
[startup+160.046 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6491 0 0 0 15977 17 0 0 25 0 1 0 486280521 28901376 6416 4294967295 134512640 134672761 3221224544 3221223760 134558229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7056 6416 603 41 0 7015 0
vsize: 28224
[startup+170.046 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 16977 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223732 134557991 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+180.046 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 17977 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223712 134561148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+190.046 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 18977 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+200.046 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 19977 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+210.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 20977 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+220.045 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 21977 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+230.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 22978 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+240.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 23978 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+250.046 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 24978 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+260.045 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 25978 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223808 134562156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+270.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6521 0 0 0 26978 18 0 0 25 0 1 0 486280521 29036544 6446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6446 603 41 0 7048 0
vsize: 28356
[startup+280.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6528 0 0 0 27978 18 0 0 25 0 1 0 486280521 29036544 6453 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7089 6453 603 41 0 7048 0
vsize: 28356
[startup+290.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 6889 0 0 0 28977 19 0 0 25 0 1 0 486280521 30519296 6814 4294967295 134512640 134672761 3221224544 3221223668 134566080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7451 6814 603 41 0 7410 0
vsize: 29804
[startup+300.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 29975 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221222368 134565775 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+310.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 30975 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223712 134564636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+320.044 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 31976 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223728 134557999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+330.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 32976 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+340.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 33976 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+350.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 34976 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+360.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 35976 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+370.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 36976 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223744 134557800 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+380.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 37977 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223712 134561156 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+390.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7557 0 0 0 38976 21 0 0 25 0 1 0 486280521 33742848 7482 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8238 7482 603 41 0 8197 0
vsize: 32952
[startup+400.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 7600 0 0 0 39976 21 0 0 25 0 1 0 486280521 33878016 7525 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8271 7525 603 41 0 8230 0
vsize: 33084
[startup+410.044 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 8285 0 0 0 40975 23 0 0 25 0 1 0 486280521 36708352 8210 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8962 8210 603 41 0 8921 0
vsize: 35848
[startup+420.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 8780 0 0 0 41974 24 0 0 25 0 1 0 486280521 38719488 8705 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9453 8705 603 41 0 9412 0
vsize: 37812
[startup+430.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9005 0 0 0 42973 25 0 0 25 0 1 0 486280521 39665664 8930 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9684 8930 603 41 0 9643 0
vsize: 38736
[startup+440.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9210 0 0 0 43972 26 0 0 25 0 1 0 486280521 40468480 9135 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9880 9135 603 41 0 9839 0
vsize: 39520
[startup+450.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 44972 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+460.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 45973 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223684 134560556 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+470.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 46973 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+480.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 47973 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223668 134566059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+490.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 48973 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+500.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 49973 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+510.045 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 50974 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+520.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 51974 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+530.046 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 5169
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 52974 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223648 134560412 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+540.048 s]
Raw data (loadavg): 0.99 0.97 0.91 3/57 5205
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 53974 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+550.049 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 5222
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 54974 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+560.049 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 5222
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 55974 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+570.049 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 5222
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9242 0 0 0 56974 26 0 0 25 0 1 0 486280521 40599552 9167 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9912 9167 603 41 0 9871 0
vsize: 39648
[startup+580.049 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 5222
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9380 0 0 0 57974 26 0 0 25 0 1 0 486280521 41140224 9305 4294967295 134512640 134672761 3221224544 3221223696 134565056 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10044 9305 603 41 0 10003 0
vsize: 40176
[startup+590.05 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5222
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 9501 0 0 0 58974 27 0 0 25 0 1 0 486280521 41676800 9426 4294967295 134512640 134672761 3221224544 3221223792 134562294 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10175 9426 603 41 0 10134 0
vsize: 40700
[startup+600.049 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 5222
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10040 0 0 0 59973 28 0 0 25 0 1 0 486280521 43819008 9965 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10698 9965 603 41 0 10657 0
vsize: 42792
[startup+610.049 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 60972 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+620.05 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 61973 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+630.05 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 62973 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223712 134564746 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+640.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 63973 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223668 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+650.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 64973 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223696 134565070 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+660.05 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 65973 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+670.051 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 66974 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223712 134564705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+680.05 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 67974 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+690.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 68974 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+700.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 69974 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+710.051 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10338 0 0 0 70975 29 0 0 25 0 1 0 486280521 45035520 10263 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10995 10263 603 41 0 10954 0
vsize: 43980
[startup+720.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10511 0 0 0 71974 29 0 0 25 0 1 0 486280521 45711360 10436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11160 10436 603 41 0 11119 0
vsize: 44640
[startup+730.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 10688 0 0 0 72974 30 0 0 25 0 1 0 486280521 46518272 10613 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11357 10613 603 41 0 11316 0
vsize: 45428
[startup+740.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 11142 0 0 0 73974 30 0 0 25 0 1 0 486280521 48271360 11067 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11785 11067 603 41 0 11744 0
vsize: 47140
[startup+750.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 11283 0 0 0 74974 31 0 0 25 0 1 0 486280521 48943104 11208 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11949 11208 603 41 0 11908 0
vsize: 47796
[startup+760.052 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 11435 0 0 0 75973 31 0 0 25 0 1 0 486280521 49479680 11360 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12080 11360 603 41 0 12039 0
vsize: 48320
[startup+770.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 12010 0 0 0 76972 33 0 0 25 0 1 0 486280521 51904512 11935 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12672 11935 603 41 0 12631 0
vsize: 50688
[startup+780.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 12260 0 0 0 77972 33 0 0 25 0 1 0 486280521 52846592 12185 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12902 12185 603 41 0 12861 0
vsize: 51608
[startup+790.053 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 12602 0 0 0 78971 34 0 0 25 0 1 0 486280521 54329344 12527 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13264 12527 603 41 0 13223 0
vsize: 53056
[startup+800.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13583 0 0 0 79969 36 0 0 25 0 1 0 486280521 58368000 13508 4294967295 134512640 134672761 3221224544 3221223280 134565768 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13508 603 41 0 14209 0
vsize: 57000
[startup+810.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13584 0 0 0 80969 36 0 0 25 0 1 0 486280521 58368000 13509 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13509 603 41 0 14209 0
vsize: 57000
[startup+820.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 81969 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+830.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 82970 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+840.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5224
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 83970 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+850.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 84970 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+860.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 85970 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+870.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 86970 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+880.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 87970 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+890.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 88971 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+900.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 89970 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+910.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 13586 0 0 0 90970 36 0 0 25 0 1 0 486280521 58368000 13511 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14250 13511 603 41 0 14209 0
vsize: 57000
[startup+920.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 14082 0 0 0 91969 37 0 0 25 0 1 0 486280521 60395520 14007 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14745 14007 603 41 0 14704 0
vsize: 58980
[startup+930.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 14730 0 0 0 92968 39 0 0 25 0 1 0 486280521 63094784 14655 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15404 14655 603 41 0 15363 0
vsize: 61616
[startup+940.055 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 14762 0 0 0 93968 39 0 0 25 0 1 0 486280521 63229952 14687 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15437 14687 603 41 0 15396 0
vsize: 61748
[startup+950.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 14856 0 0 0 94968 39 0 0 25 0 1 0 486280521 63635456 14781 4294967295 134512640 134672761 3221224544 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15536 14781 603 41 0 15495 0
vsize: 62144
[startup+960.054 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 14959 0 0 0 95968 39 0 0 25 0 1 0 486280521 64040960 14884 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15635 14884 603 41 0 15594 0
vsize: 62540
[startup+970.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 15061 0 0 0 96970 40 0 0 25 0 1 0 486280521 64446464 14986 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15734 14986 603 41 0 15693 0
vsize: 62936
[startup+980.074 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 15422 0 0 0 97969 41 0 0 25 0 1 0 486280521 65929216 15347 4294967295 134512640 134672761 3221224544 3221223712 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16096 15347 603 41 0 16055 0
vsize: 64384
[startup+990.075 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 15607 0 0 0 98968 42 0 0 25 0 1 0 486280521 66740224 15532 4294967295 134512640 134672761 3221224544 3221223668 134566128 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16294 15532 603 41 0 16253 0
vsize: 65176
[startup+1000.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 15831 0 0 0 99967 43 0 0 25 0 1 0 486280521 67543040 15756 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16490 15756 603 41 0 16449 0
vsize: 65960
[startup+1010.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16031 0 0 0 100967 44 0 0 25 0 1 0 486280521 68345856 15956 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16686 15956 603 41 0 16645 0
vsize: 66744
[startup+1020.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16282 0 0 0 101966 44 0 0 25 0 1 0 486280521 69427200 16207 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16950 16207 603 41 0 16909 0
vsize: 67800
[startup+1030.07 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16603 0 0 0 102966 45 0 0 25 0 1 0 486280521 70770688 16528 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17278 16528 603 41 0 17237 0
vsize: 69112
[startup+1040.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 103966 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1050.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 104966 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1060.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 105966 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1070.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 106966 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1080.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 107967 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1090.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 108967 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1100.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 109967 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1110.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 110967 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1120.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 111967 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223808 134562262 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1130.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 112968 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223776 134564644 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1140.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 113968 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1150.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 114968 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1160.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 115968 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1170.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 116968 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1180.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 117969 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223712 134564682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1190.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 118969 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 5226
Raw data (stat): 5169 (minisat+) R 5168 22932 22931 0 -1 0 16846 0 0 0 119969 45 0 0 25 0 1 0 486280521 71716864 16771 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17509 16771 603 41 0 17468 0
vsize: 70036
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.11 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 5226
Raw data (stat): 5169 (minisat+) Z 5168 22932 22931 0 -1 12 16848 0 0 0 119969 48 0 0 25 0 1 0 486280521 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.11
CPU time (s): 1200.18
CPU user time (s): 1199.69
CPU system time (s): 0.489925
CPU usage (%): 100.006
Max. virtual memory (Kb): 70036
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####