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-ran17x17.opb
MD5SUM	4afffa77a031423497a8b9b377dd0292
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	689314
Optimality of the best value was proved	NO
Number of terms in the objective function	6069
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	1576985250
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	1576985250
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	6069
Total number of constraints	323
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	323
Minimum length of a constraint	21
Maximum length of a constraint	340
Trace number 17630

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.220
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        829800 kB
Buffers:         14688 kB
Cached:         170020 kB
SwapCached:        728 kB
Active:          56816 kB
Inactive:       129876 kB
HighTotal:      131008 kB
HighFree:        75068 kB
LowTotal:       903652 kB
LowFree:        754732 kB
SwapTotal:     2097892 kB
SwapFree:      2096220 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           4992 kB
Slab:            12576 kB
Committed_AS:    63588 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 11:21:36 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 19328 7 1200.25 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 357 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##################################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 355]---> Adder-cost: 338   maxlim: 28143   bits: 15/15
c ---[ 353]---> Adder-cost: 310   maxlim: 15599   bits: 14/14
c ---[ 351]---> Adder-cost: 338   maxlim: 27887   bits: 15/15
c ---[ 349]---> Adder-cost: 338   maxlim: 28399   bits: 15/15
c ---[ 347]---> Adder-cost: 360   maxlim: 46575   bits: 16/16
c ---[ 345]---> Adder-cost: 338   maxlim: 28527   bits: 15/15
c ---[ 343]---> Adder-cost: 338   maxlim: 28655   bits: 15/15
c ---[ 341]---> Adder-cost: 360   maxlim: 46575   bits: 16/16
c ---[ 339]---> Adder-cost: 362   maxlim: 53871   bits: 16/16
c ---[ 337]---> Adder-cost: 360   maxlim: 47215   bits: 16/16
c ---[ 335]---> Adder-cost: 360   maxlim: 46959   bits: 16/16
c ---[ 333]---> Adder-cost: 338   maxlim: 27759   bits: 15/15
c ---[ 331]---> Adder-cost: 362   maxlim: 54255   bits: 16/16
c ---[ 329]---> Adder-cost: 360   maxlim: 46703   bits: 16/16
c ---[ 327]---> Adder-cost: 360   maxlim: 47727   bits: 16/16
c ---[ 325]---> Adder-cost: 310   maxlim: 15727   bits: 14/14
c ---[ 323]---> Adder-cost: 310   maxlim: 15855   bits: 14/14
c ---[ 321]---> Adder-cost: 358   maxlim: 45935   bits: 16/16
c ---[ 319]---> Adder-cost: 320   maxlim: 16623   bits: 15/15
c ---[ 317]---> Adder-cost: 342   maxlim: 30703   bits: 15/15
c ---[ 315]---> Adder-cost: 320   maxlim: 16879   bits: 15/15
c ---[ 313]---> Adder-cost: 342   maxlim: 29807   bits: 15/15
c ---[ 311]---> Adder-cost: 358   maxlim: 46063   bits: 16/16
c ---[ 309]---> Adder-cost: 342   maxlim: 30191   bits: 15/15
c ---[ 307]---> Adder-cost: 362   maxlim: 52079   bits: 16/16
c ---[ 305]---> Adder-cost: 358   maxlim: 45679   bits: 16/16
c ---[ 303]---> Adder-cost: 288   maxlim: 8303   bits: 14/14
c ---[ 301]---> Adder-cost: 358   maxlim: 45551   bits: 16/16
c ---[ 299]---> Adder-cost: 358   maxlim: 44783   bits: 16/16
c ---[ 297]---> Adder-cost: 358   maxlim: 45167   bits: 16/16
c ---[ 295]---> Adder-cost: 362   maxlim: 51695   bits: 16/16
c ---[ 293]---> Adder-cost: 358   maxlim: 44271   bits: 16/16
c ---[ 291]---> Adder-cost: 288   maxlim: 8303   bits: 14/14
c ---[ 289]---> Adder-cost: 358   maxlim: 44399   bits: 16/16
c ---[ 288]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 287]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 286]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 285]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[ 284]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 283]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 282]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 281]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 280]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 279]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 278]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 277]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 276]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 275]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 274]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 273]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 272]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 271]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 270]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 269]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 268]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 267]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 266]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 265]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 264]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 263]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 262]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 261]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 260]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 259]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 258]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 257]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 256]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 255]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 254]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 253]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 252]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 251]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 250]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 249]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 248]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 247]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 246]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 245]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 244]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 243]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 242]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 241]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 240]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 239]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 238]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 237]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 236]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 235]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 234]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 233]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 232]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 231]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 230]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 229]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 228]---> Adder-cost: 6   maxlim: 1022   bits: 11/10
c ---[ 227]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 226]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 225]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 224]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 223]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 222]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 221]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 220]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 219]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 218]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 217]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 216]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 215]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 214]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 213]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 212]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 211]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 210]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 209]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 208]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 207]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 206]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 205]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 204]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 203]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 202]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 201]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 200]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 199]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 198]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 197]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 196]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 195]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 194]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 193]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 192]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 191]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 190]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 189]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 188]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 187]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 186]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 185]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 184]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 183]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 182]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 181]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 180]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 179]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 178]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 177]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 176]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 175]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 174]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 173]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 172]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 171]---> Adder-cost: 6   maxlim: 2046   bits: 12/11
c ---[ 170]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 169]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 168]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 167]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 166]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 165]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 164]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 163]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 162]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 161]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 160]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 159]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 158]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 157]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 156]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[ 155]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[ 154]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 153]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 152]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 151]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 150]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 149]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 148]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 147]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 146]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 145]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 144]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 143]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 142]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 141]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 140]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 139]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 138]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 137]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 136]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 135]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 134]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 133]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 132]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 131]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 130]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 129]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 128]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 127]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 126]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 125]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 124]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 123]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 122]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 121]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 120]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 119]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 118]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 117]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 116]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 115]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 114]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 113]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 112]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 111]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 110]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[ 109]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[ 108]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[ 107]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 106]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 105]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[ 104]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[ 103]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[ 102]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[ 101]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[ 100]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  99]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  98]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  97]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
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: 1022   bits: 11/10
c ---[  93]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  92]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  91]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  90]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  89]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  88]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  87]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  86]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  85]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  84]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  83]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  82]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  81]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  80]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  79]---> Adder-cost: 12   maxlim: 8190   bits: 14/13
c ---[  78]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  77]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  76]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  75]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  74]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  73]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  72]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  71]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  70]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  69]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  68]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  67]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  66]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  65]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  64]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  63]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  62]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  61]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  60]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  59]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  58]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  57]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  56]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  55]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  54]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  53]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  52]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  51]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  50]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  49]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  48]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  47]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  46]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  45]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  44]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  43]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  42]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  41]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  40]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  39]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  38]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[  37]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  36]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  35]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  34]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  33]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  32]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  31]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  30]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  29]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  28]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  27]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  26]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  25]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  24]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  23]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[  22]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[  21]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  20]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  19]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  18]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[  17]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  16]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[  15]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[  14]---> Adder-cost: 4   maxlim: 1022   bits: 11/10
c ---[  13]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[  12]---> Adder-cost: 6   maxlim: 4094   bits: 13/12
c ---[  11]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[  10]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ---[   9]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   8]---> Adder-cost: 2   maxlim: 8190   bits: 14/13
c ---[   7]---> Adder-cost: 8   maxlim: 4094   bits: 13/12
c ---[   6]---> Adder-cost: 4   maxlim: 510   bits: 10/9
c ---[   5]---> Adder-cost: 10   maxlim: 4094   bits: 13/12
c ---[   4]---> Adder-cost: 2   maxlim: 2046   bits: 12/11
c ---[   3]---> Adder-cost: 2   maxlim: 1022   bits: 11/10
c ---[   2]---> Adder-cost: 8   maxlim: 2046   bits: 12/11
c ---[   1]---> Adder-cost: 2   maxlim: 4094   bits: 13/12
c ---[   0]---> Adder-cost: 4   maxlim: 2046   bits: 12/11
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   89198   328955 |   29732       0        0     nan |  0.000 % |
c |       100 |   89198   328955 |   32705     100      275     2.8 | 29.805 % |
c |       250 |   89198   328955 |   35975     250      698     2.8 | 29.805 % |
c |       475 |   89117   328686 |   39573     469     2096     4.5 | 29.871 % |
c |       812 |   89020   328357 |   43530     793     3787     4.8 | 29.945 % |
c |      1318 |   88757   327460 |   47883    1257     5844     4.6 | 30.146 % |
c |      2077 |   88609   326934 |   52672    1994     8828     4.4 | 30.255 % |
c |      3216 |   88330   325975 |   57939    3086    13670     4.4 | 30.464 % |
c |      4924 |   87930   324633 |   63733    4735    21041     4.4 | 30.783 % |
c |      7486 |   87650   323689 |   70106    7258    33691     4.6 | 30.992 % |
c |     11330 |   87112   321855 |   77117   11027    53785     4.9 | 31.407 % |
c |     17096 |   86444   319595 |   84828   16694    82271     4.9 | 31.943 % |
c |     25745 |   85934   317881 |   93311   25266   132367     5.2 | 32.340 % |
c |     38719 |   85580   316683 |  102642   38190   226448     5.9 | 32.628 % |
c |     58180 |   85155   315246 |  112907   57590   420427     7.3 | 32.968 % |
c |     87372 |   84806   314069 |  124197   86732   758159     8.7 | 33.248 % |
c |    131162 |   84737   313834 |  136617  130512  2156078    16.5 | 33.304 % |
c |    196846 |   84737   313834 |  150279   79289  1153621    14.5 | 33.304 % |
c |    295372 |   84695   313688 |  165307   33738  2810773    83.3 | 33.335 % |
c |    443161 |   84688   313665 |  181838   34125   396766    11.6 | 33.339 % |
c |    664845 |   84649   313538 |  200022   92469  2505588    27.1 | 33.370 % |
#### 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.66 0.91 0.90 2/54 3303
Raw data (stat): 3303 (runsolver) R 3302 28099 28098 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 544570274 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.71 0.91 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 2602 0 0 0 993 6 0 0 25 0 1 0 544570274 12980224 2486 4294967295 134512640 134672761 3221224544 3221223680 134565973 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3169 2486 603 41 0 3128 0
vsize: 12676
[startup+20.0019 s]
Raw data (loadavg): 0.76 0.91 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 2664 0 0 0 1993 6 0 0 25 0 1 0 544570274 13271040 2548 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3240 2548 603 41 0 3199 0
vsize: 12960
[startup+30.0022 s]
Raw data (loadavg): 0.79 0.91 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 2710 0 0 0 2992 7 0 0 25 0 1 0 544570274 13545472 2594 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3307 2594 603 41 0 3266 0
vsize: 13228
[startup+40.0022 s]
Raw data (loadavg): 0.82 0.92 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 2765 0 0 0 3992 7 0 0 25 0 1 0 544570274 13774848 2649 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3363 2649 603 41 0 3322 0
vsize: 13452
[startup+50.0028 s]
Raw data (loadavg): 0.85 0.92 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 2820 0 0 0 4992 7 0 0 25 0 1 0 544570274 13910016 2704 4294967295 134512640 134672761 3221224544 3221223668 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3396 2704 603 41 0 3355 0
vsize: 13584
[startup+60.003 s]
Raw data (loadavg): 0.87 0.92 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 2873 0 0 0 5991 8 0 0 25 0 1 0 544570274 14180352 2757 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3462 2757 603 41 0 3421 0
vsize: 13848
[startup+70.004 s]
Raw data (loadavg): 0.89 0.92 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 2949 0 0 0 6992 8 0 0 25 0 1 0 544570274 14450688 2833 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3528 2833 603 41 0 3487 0
vsize: 14112
[startup+80.0049 s]
Raw data (loadavg): 0.91 0.92 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3046 0 0 0 7991 8 0 0 25 0 1 0 544570274 14983168 2930 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3658 2930 603 41 0 3617 0
vsize: 14632
[startup+90.0048 s]
Raw data (loadavg): 0.92 0.93 0.90 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3121 0 0 0 8991 9 0 0 25 0 1 0 544570274 15253504 3005 4294967295 134512640 134672761 3221224544 3221223668 134566012 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3724 3005 603 41 0 3683 0
vsize: 14896
[startup+100.006 s]
Raw data (loadavg): 0.93 0.93 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3201 0 0 0 9991 9 0 0 25 0 1 0 544570274 15523840 3085 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3790 3085 603 41 0 3749 0
vsize: 15160
[startup+110.006 s]
Raw data (loadavg): 0.94 0.93 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3301 0 0 0 10990 10 0 0 25 0 1 0 544570274 15929344 3185 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3889 3185 603 41 0 3848 0
vsize: 15556
[startup+120.007 s]
Raw data (loadavg): 0.95 0.93 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3446 0 0 0 11989 11 0 0 25 0 1 0 544570274 16470016 3330 4294967295 134512640 134672761 3221224544 3221223712 134553613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4021 3330 603 41 0 3980 0
vsize: 16084
[startup+130.007 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3566 0 0 0 12989 12 0 0 25 0 1 0 544570274 17010688 3450 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4153 3450 603 41 0 4112 0
vsize: 16612
[startup+140.008 s]
Raw data (loadavg): 0.96 0.93 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3693 0 0 0 13988 13 0 0 25 0 1 0 544570274 17551360 3577 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4285 3577 603 41 0 4244 0
vsize: 17140
[startup+150.007 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3823 0 0 0 14987 13 0 0 25 0 1 0 544570274 18219008 3707 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4448 3707 603 41 0 4407 0
vsize: 17792
[startup+160.007 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 3965 0 0 0 15987 14 0 0 25 0 1 0 544570274 18759680 3849 4294967295 134512640 134672761 3221224544 3221223744 134557811 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4580 3849 603 41 0 4539 0
vsize: 18320
[startup+170.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 4094 0 0 0 16986 15 0 0 25 0 1 0 544570274 19300352 3978 4294967295 134512640 134672761 3221224544 3221223712 134564448 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4712 3978 603 41 0 4671 0
vsize: 18848
[startup+180.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 4306 0 0 0 17985 16 0 0 25 0 1 0 544570274 20111360 4190 4294967295 134512640 134672761 3221224544 3221223696 134565098 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4910 4190 603 41 0 4869 0
vsize: 19640
[startup+190.009 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 4531 0 0 0 18983 18 0 0 25 0 1 0 544570274 21053440 4415 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5140 4415 603 41 0 5099 0
vsize: 20560
[startup+200.01 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 5294 0 0 0 19981 20 0 0 25 0 1 0 544570274 24150016 5178 4294967295 134512640 134672761 3221224544 3221223648 134554910 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5896 5178 603 41 0 5855 0
vsize: 23584
[startup+210.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 5797 0 0 0 20979 22 0 0 25 0 1 0 544570274 26169344 5681 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6389 5681 603 41 0 6348 0
vsize: 25556
[startup+220.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6073 0 0 0 21978 23 0 0 25 0 1 0 544570274 27246592 5957 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6652 5957 603 41 0 6611 0
vsize: 26608
[startup+230.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6535 0 0 0 22976 25 0 0 25 0 1 0 544570274 29659136 6419 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7241 6419 603 41 0 7200 0
vsize: 28964
[startup+240.012 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3303
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 23975 26 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+250.013 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 24975 27 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+260.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 25974 27 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+270.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 26974 28 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+280.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 27974 28 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223744 134557922 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+290.014 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 28973 29 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223668 134566109 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+300.015 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 29973 29 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223696 134565076 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+310.016 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 30973 29 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+320.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 31973 29 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+330.016 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 32973 29 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+340.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 33974 30 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223696 134565045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+350.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 6745 0 0 0 34974 30 0 0 25 0 1 0 544570274 30470144 6629 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7439 6629 603 41 0 7398 0
vsize: 29756
[startup+360.028 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 7285 0 0 0 35973 31 0 0 25 0 1 0 544570274 32620544 7169 4294967295 134512640 134672761 3221224544 3221223668 134566071 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7964 7169 603 41 0 7923 0
vsize: 31856
[startup+370.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 7552 0 0 0 36972 32 0 0 25 0 1 0 544570274 33697792 7436 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8227 7436 603 41 0 8186 0
vsize: 32908
[startup+380.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 8007 0 0 0 37970 35 0 0 25 0 1 0 544570274 35586048 7891 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8688 7891 603 41 0 8647 0
vsize: 34752
[startup+390.029 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 8252 0 0 0 38969 36 0 0 25 0 1 0 544570274 36532224 8136 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8919 8136 603 41 0 8878 0
vsize: 35676
[startup+400.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 9010 0 0 0 39967 38 0 0 25 0 1 0 544570274 39628800 8894 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9675 8894 603 41 0 9634 0
vsize: 38700
[startup+410.03 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10074 0 0 0 40963 42 0 0 25 0 1 0 544570274 43937792 9958 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10727 9958 603 41 0 10686 0
vsize: 42908
[startup+420.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 41963 42 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+430.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 42963 42 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+440.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 43963 42 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+450.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 44963 42 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223712 134564490 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+460.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 45963 43 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+470.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 46963 43 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+480.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 47963 43 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+490.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 48963 43 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223648 134560399 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+500.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 49963 44 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223728 134558880 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+510.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10157 0 0 0 50963 44 0 0 25 0 1 0 544570274 44343296 10041 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10826 10041 603 41 0 10785 0
vsize: 43304
[startup+520.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 10890 0 0 0 51960 47 0 0 25 0 1 0 544570274 47329280 10774 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11555 10774 603 41 0 11514 0
vsize: 46220
[startup+530.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 11432 0 0 0 52959 48 0 0 25 0 1 0 544570274 49614848 11316 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12113 11316 603 41 0 12072 0
vsize: 48452
[startup+540.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 11895 0 0 0 53957 49 0 0 25 0 1 0 544570274 51499008 11779 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12573 11779 603 41 0 12532 0
vsize: 50292
[startup+550.035 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 12480 0 0 0 54956 51 0 0 25 0 1 0 544570274 53792768 12364 4294967295 134512640 134672761 3221224544 3221223668 134566092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13133 12364 603 41 0 13092 0
vsize: 52532
[startup+560.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 12763 0 0 0 55955 52 0 0 25 0 1 0 544570274 55001088 12647 4294967295 134512640 134672761 3221224544 3221223648 134555357 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13428 12647 603 41 0 13387 0
vsize: 53712
[startup+570.036 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 13046 0 0 0 56955 53 0 0 25 0 1 0 544570274 56213504 12930 4294967295 134512640 134672761 3221224544 3221223728 134558687 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13724 12930 603 41 0 13683 0
vsize: 54896
[startup+580.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 13336 0 0 0 57953 54 0 0 25 0 1 0 544570274 57430016 13220 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14021 13220 603 41 0 13980 0
vsize: 56084
[startup+590.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 13628 0 0 0 58952 55 0 0 25 0 1 0 544570274 58503168 13512 4294967295 134512640 134672761 3221224544 3221223648 134555116 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14283 13512 603 41 0 14242 0
vsize: 57132
[startup+600.037 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14229 0 0 0 59950 58 0 0 25 0 1 0 544570274 61063168 14113 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14908 14113 603 41 0 14867 0
vsize: 59632
[startup+610.043 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14455 0 0 0 60950 58 0 0 25 0 1 0 544570274 62005248 14339 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15138 14339 603 41 0 15097 0
vsize: 60552
[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14683 0 0 0 61949 60 0 0 25 0 1 0 544570274 62816256 14567 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15336 14567 603 41 0 15295 0
vsize: 61344
[startup+630.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 62949 60 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 63949 60 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+650.051 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 64949 61 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+660.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 65949 61 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+670.056 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 66949 61 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+680.062 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 67949 62 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+690.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 68950 62 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+700.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 69949 62 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+710.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 70949 63 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223680 134560647 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+720.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 71949 63 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+730.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 72948 64 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223648 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+740.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 73948 64 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+750.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 74948 64 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+760.068 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 75948 64 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+770.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 76949 64 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+780.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 77949 64 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223744 134557852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+790.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14841 0 0 0 78949 64 0 0 25 0 1 0 544570274 63483904 14725 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14725 603 41 0 15458 0
vsize: 61996
[startup+800.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14843 0 0 0 79949 64 0 0 25 0 1 0 544570274 63483904 14727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14727 603 41 0 15458 0
vsize: 61996
[startup+810.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14852 0 0 0 80949 64 0 0 25 0 1 0 544570274 63483904 14736 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14736 603 41 0 15458 0
vsize: 61996
[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 81949 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+830.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 82950 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+840.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 83950 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+850.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 84950 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+860.067 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 85950 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223728 134559342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+870.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 86950 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+880.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 87951 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+890.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 88950 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+900.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 89951 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+910.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 90951 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+920.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 91951 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+930.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 92951 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+940.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 93951 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223696 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+950.066 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 94951 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+960.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 95952 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223728 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+970.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 96952 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223728 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+980.065 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 97952 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+990.064 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 98952 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223648 134559769 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+1000.07 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 99952 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+1010.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 14856 0 0 0 100952 64 0 0 25 0 1 0 544570274 63483904 14740 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15499 14740 603 41 0 15458 0
vsize: 61996
[startup+1020.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 15916 0 0 0 101950 67 0 0 25 0 1 0 544570274 67796992 15800 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16552 15800 603 41 0 16511 0
vsize: 66208
[startup+1030.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 16889 0 0 0 102947 69 0 0 25 0 1 0 544570274 71823360 16773 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17535 16773 603 41 0 17494 0
vsize: 70140
[startup+1040.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 17766 0 0 0 103945 72 0 0 25 0 1 0 544570274 75436032 17650 4294967295 134512640 134672761 3221224544 3221223648 134560252 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18417 17650 603 41 0 18376 0
vsize: 73668
[startup+1050.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 18671 0 0 0 104943 74 0 0 25 0 1 0 544570274 79077376 18555 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19306 18555 603 41 0 19265 0
vsize: 77224
[startup+1060.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 19624 0 0 0 105939 78 0 0 25 0 1 0 544570274 83083264 19508 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20284 19508 603 41 0 20243 0
vsize: 81136
[startup+1070.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 20565 0 0 0 106937 80 0 0 25 0 1 0 544570274 86933504 20449 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21224 20449 603 41 0 21183 0
vsize: 84896
[startup+1080.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 21459 0 0 0 107936 82 0 0 25 0 1 0 544570274 90533888 21343 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22103 21343 603 41 0 22062 0
vsize: 88412
[startup+1090.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 22164 0 0 0 108935 83 0 0 25 0 1 0 544570274 93483008 22048 4294967295 134512640 134672761 3221224544 3221223648 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22823 22048 603 41 0 22782 0
vsize: 91292
[startup+1100.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 22931 0 0 0 109932 86 0 0 25 0 1 0 544570274 96559104 22815 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23574 22815 603 41 0 23533 0
vsize: 94296
[startup+1110.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 23708 0 0 0 110931 87 0 0 25 0 1 0 544570274 99778560 23592 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24360 23592 603 41 0 24319 0
vsize: 97440
[startup+1120.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 24471 0 0 0 111929 89 0 0 25 0 1 0 544570274 102854656 24355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25111 24355 603 41 0 25070 0
vsize: 100444
[startup+1130.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 25236 0 0 0 112927 91 0 0 25 0 1 0 544570274 106061824 25120 4294967295 134512640 134672761 3221224544 3221223712 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25894 25120 603 41 0 25853 0
vsize: 103576
[startup+1140.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 25980 0 0 0 113924 94 0 0 25 0 1 0 544570274 109027328 25864 4294967295 134512640 134672761 3221224544 3221223648 134560506 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26618 25864 603 41 0 26577 0
vsize: 106472
[startup+1150.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 26751 0 0 0 114922 96 0 0 25 0 1 0 544570274 112128000 26635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27375 26635 603 41 0 27334 0
vsize: 109500
[startup+1160.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 27523 0 0 0 115920 98 0 0 25 0 1 0 544570274 115339264 27407 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28159 27407 603 41 0 28118 0
vsize: 112636
[startup+1170.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 28216 0 0 0 116919 99 0 0 25 0 1 0 544570274 118177792 28100 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28852 28100 603 41 0 28811 0
vsize: 115408
[startup+1180.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 28875 0 0 0 117917 101 0 0 25 0 1 0 544570274 120872960 28759 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 29510 28759 603 41 0 29469 0
vsize: 118040
[startup+1190.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 29594 0 0 0 118916 102 0 0 25 0 1 0 544570274 123789312 29478 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30222 29478 603 41 0 30181 0
vsize: 120888
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 3305
Raw data (stat): 3303 (minisat+) R 3302 28099 28098 0 -1 0 29628 0 0 0 119916 102 0 0 25 0 1 0 544570274 124051456 29512 4294967295 134512640 134672761 3221224544 3221223680 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 30286 29512 603 41 0 30245 0
vsize: 121144
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.12 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 3305
Raw data (stat): 3303 (minisat+) Z 3302 28099 28098 0 -1 12 29630 0 0 0 119916 108 0 0 25 0 1 0 544570274 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.12
CPU time (s): 1200.25
CPU user time (s): 1199.17
CPU system time (s): 1.08383
CPU usage (%): 100.011
Max. virtual memory (Kb): 121144
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####