PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/mps-v2-13-7/MIPLIB/miplib3/normalized-mps-v2-13-7-vpm2.opb
MD5SUM	fae1fae180d772ad3ee6c1acfa1c8b4f
Bench Category	optimization, medium integers (OPTMEDINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	122
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	5
Number of bits for the biggest coefficient in the objective function	3
Sum of the numbers in the objective function	504
Number of bits of the sum of numbers in the objective function	9
Biggest number in a constraint	2000000
Number of bits of the biggest number in a constraint	21
Biggest sum of numbers in a constraint	30041153
Number of bits of the biggest sum of numbers	25
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1189.01
Number of variables	2124
Total number of constraints	444
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	444
Minimum length of a constraint	8
Maximum length of a constraint	64
Trace number 17884

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc28 THE 2005-04-21 12:28:36 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=18951 boxname=wulflinc28 idbench=1458 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  fae1fae180d772ad3ee6c1acfa1c8b4f  /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-vpm2.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-vpm2.opb /oldhome/oroussel/tmp/wulflinc28/normalized-mps-v2-13-7-vpm2.opb
IDLAUNCH: 18951
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.077
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.077
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:        529760 kB
Buffers:         30416 kB
Cached:         447452 kB
SwapCached:        104 kB
Active:         186072 kB
Inactive:       294176 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        529508 kB
SwapTotal:     2097640 kB
SwapFree:      2097068 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6056 kB
Slab:            18900 kB
Committed_AS:    63632 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 12:48:38 (client local time) WITH STATUS 0 IN 1200.18 SECONDS
stats: 18951 7 1200.18 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################
c   -- Clauses(.)/Splits(s): (none)
c ---[ 485]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 484]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 483]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 482]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 481]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 480]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 479]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 478]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 477]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 474]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 473]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 472]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 471]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 468]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 467]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 466]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 465]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 462]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 459]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 458]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 457]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 454]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 453]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 452]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 451]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 450]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 448]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 447]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 446]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 445]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 444]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 441]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 440]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 439]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 433]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 427]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 422]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 421]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 415]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 409]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 408]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 402]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 397]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 396]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 391]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 390]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 386]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 385]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 384]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 380]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 379]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 378]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 374]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 373]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 372]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 368]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 367]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 366]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 365]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 364]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 359]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 353]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 347]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 339]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 333]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 327]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 321]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 317]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 316]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 315]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 314]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 313]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 312]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 310]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 309]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 308]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 307]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 306]---> Adder-cost: 49   maxlim: 7166   bits: 14/13
c ---[ 302]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 301]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 300]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 295]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 294]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 290]---> Adder-cost: 30   maxlim: 27134   bits: 16/15
c ---[ 289]---> Adder-cost: 30   maxlim: 27134   bits: 16/15
c ---[ 288]---> Adder-cost: 30   maxlim: 27134   bits: 16/15
c ---[ 287]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 286]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 285]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 284]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 283]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 282]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 280]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 279]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 278]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 277]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 276]---> Adder-cost: 45   maxlim: 3582   bits: 13/12
c ---[ 274]---> Adder-cost: 232   maxlim: 267600   bits: 19/19
c ---[ 264]---> Adder-cost: 288   maxlim: 420400   bits: 20/19
c ---[ 260]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 258]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 256]---> Adder-cost: 238   maxlim: 210767   bits: 18/18
c ---[ 254]---> Adder-cost: 238   maxlim: 210767   bits: 18/18
c ---[ 252]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[ 250]---> Adder-cost: 184   maxlim: 165300   bits: 18/18
c ---[ 248]---> Adder-cost: 224   maxlim: 287667   bits: 19/19
c ---[ 246]---> Adder-cost: 224   maxlim: 262067   bits: 19/18
c ---[ 244]---> Adder-cost: 224   maxlim: 262067   bits: 19/18
c ---[ 242]---> Adder-cost: 208   maxlim: 210867   bits: 18/18
c ---[ 236]---> Adder-cost: 196   maxlim: 203300   bits: 18/18
c ---[ 234]---> Adder-cost: 232   maxlim: 322083   bits: 19/19
c ---[ 232]---> Adder-cost: 180   maxlim: 110883   bits: 17/17
c ---[ 224]---> Adder-cost: 228   maxlim: 229200   bits: 19/18
c ---[ 222]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 216]---> Adder-cost: 202   maxlim: 152900   bits: 18/18
c ---[ 214]---> Adder-cost: 234   maxlim: 244035   bits: 19/18
c ---[ 212]---> Adder-cost: 234   maxlim: 231235   bits: 19/18
c ---[ 210]---> Adder-cost: 278   maxlim: 283183   bits: 19/19
c ---[ 208]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 206]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 204]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 202]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[ 200]---> Adder-cost: 280   maxlim: 228400   bits: 19/18
c ---[ 198]---> Adder-cost: 332   maxlim: 462383   bits: 20/19
c ---[ 196]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 194]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 192]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[ 191]---> Adder-cost: 220   maxlim: 6119277   bits: 23/23
c ---[ 190]---> Adder-cost: 382   maxlim: 10088027   bits: 24/24
c ---[ 189]---> Adder-cost: 382   maxlim: 11088027   bits: 24/24
c ---[ 188]---> Adder-cost: 460   maxlim: 14056777   bits: 24/24
c ---[ 187]---> Adder-cost: 632   maxlim: 20041152   bits: 25/25
c ---[ 186]---> Adder-cost: 604   maxlim: 15041152   bits: 25/24
c ---[ 185]---> Adder-cost: 174   maxlim: 1251093   bits: 21/21
c ---[ 184]---> Adder-cost: 310   maxlim: 2044843   bits: 22/21
c ---[ 183]---> Adder-cost: 306   maxlim: 2244843   bits: 22/22
c ---[ 182]---> Adder-cost: 368   maxlim: 2438593   bits: 22/22
c ---[ 181]---> Adder-cost: 490   maxlim: 3235468   bits: 22/22
c ---[ 180]---> Adder-cost: 494   maxlim: 3435468   bits: 22/22
c ---[ 179]---> Adder-cost: 62   maxlim: 2357   bits: 12/12
c ---[ 178]---> Adder-cost: 120   maxlim: 3627   bits: 13/12
c ---[ 177]---> Adder-cost: 114   maxlim: 3787   bits: 13/12
c ---[ 176]---> Adder-cost: 156   maxlim: 4737   bits: 13/13
c ---[ 175]---> Adder-cost: 182   maxlim: 6012   bits: 13/13
c ---[ 174]---> Adder-cost: 182   maxlim: 5692   bits: 13/13
c ---[ 173]---> Adder-cost: 34   maxlim: 493   bits: 10/9
c ---[ 172]---> Adder-cost: 60   maxlim: 619   bits: 10/10
c ---[ 171]---> Adder-cost: 62   maxlim: 779   bits: 10/10
c ---[ 170]---> Adder-cost: 82   maxlim: 809   bits: 10/10
c ---[ 169]---> Adder-cost: 102   maxlim: 1192   bits: 11/11
c ---[ 168]---> Adder-cost: 98   maxlim: 1000   bits: 11/10
c ---[ 167]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 166]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 165]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 164]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 163]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 162]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 161]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 160]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 159]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 158]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 157]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 156]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 155]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 154]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 153]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 152]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 151]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 150]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 149]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 148]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 147]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 146]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 145]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 144]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 142]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 141]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 140]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 139]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 138]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 136]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 135]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 134]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 133]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 132]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 130]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 129]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 128]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 127]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 126]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 124]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 123]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 122]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 121]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 120]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 116]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 115]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 114]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[ 110]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 109]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 108]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[ 104]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 103]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 102]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  98]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  97]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  96]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  91]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  90]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  85]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  84]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  79]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  78]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  73]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  72]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  68]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  67]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  66]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  62]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  61]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  60]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  56]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  55]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  54]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  50]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  49]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  48]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  47]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  46]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  45]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  44]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  43]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  42]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  41]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  40]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  39]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  38]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  37]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  36]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  35]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  34]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  33]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  32]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  31]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  30]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  29]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  28]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  27]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  26]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  25]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  24]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[  22]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  21]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  20]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  19]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  18]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  16]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  15]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  14]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  13]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  12]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[  10]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[   9]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   8]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[   7]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[   6]---> Adder-cost: 12   maxlim: 62   bits: 7/6
c ---[   4]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[   3]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   2]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[   1]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ---[   0]---> Adder-cost: 10   maxlim: 30   bits: 6/5
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  106413   383231 |   35471       0        0     nan |  0.000 % |
c |       100 |  106413   383231 |   39018     100      856     8.6 | 18.133 % |
c |       250 |  106405   383205 |   42919     249     1928     7.7 | 18.138 % |
c |       476 |  106365   383079 |   47211     470     3998     8.5 | 18.171 % |
c |       813 |  106358   383056 |   51933     804     7476     9.3 | 18.176 % |
c |      1320 |  106293   382823 |   57126    1300    12727     9.8 | 18.181 % |
c |      2080 |  106293   382823 |   62839    2060    23082    11.2 | 18.181 % |
c |      3219 |  106253   382694 |   69122    3190    40161    12.6 | 18.210 % |
c |      4927 |  106241   382655 |   76035    4896    75368    15.4 | 18.219 % |
c |      7490 |  106216   382574 |   83638    7453   125219    16.8 | 18.243 % |
c |     11334 |  105931   381607 |   92002   11263   181777    16.1 | 18.426 % |
c |     17102 |  105903   381512 |  101202   17025   325114    19.1 | 18.445 % |
c |     25752 |  105860   381371 |  111323   25667   517541    20.2 | 18.474 % |
c |     38727 |  105765   381036 |  122455   38604   828782    21.5 | 18.493 % |
c |     58188 |  105680   380737 |  134701   58053  1303774    22.5 | 18.513 % |
c |     87380 |  105640   380607 |  148171   87240  2212640    25.4 | 18.537 % |
c |    131171 |  105617   380532 |  162988  131028  3218704    24.6 | 18.556 % |
c |    196856 |  105493   380097 |  179287   44538  1663449    37.3 | 18.585 % |
c |    295383 |  105235   379208 |  197215  143029  3991277    27.9 | 18.700 % |
c |    443173 |  104349   376122 |  216937  105819  3035452    28.7 | 19.008 % |
c |    664858 |  104264   375825 |  238631  118410  3126978    26.4 | 19.027 % |
#### 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.91 0.95 0.90 2/54 25709
Raw data (stat): 25709 (runsolver) R 25708 10614 10613 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 545086787 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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+9.99968 s]
Raw data (loadavg): 0.93 0.95 0.90 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 3245 0 0 0 992 6 0 0 25 0 1 0 545086787 15884288 3161 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3878 3161 603 41 0 3837 0
vsize: 15512
[startup+20.0004 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 3745 0 0 0 1990 7 0 0 25 0 1 0 545086787 18014208 3661 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4398 3661 603 41 0 4357 0
vsize: 17592
[startup+30.0004 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 4199 0 0 0 2989 9 0 0 25 0 1 0 545086787 19890176 4115 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4856 4115 603 41 0 4815 0
vsize: 19424
[startup+40.0008 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 4492 0 0 0 3988 10 0 0 25 0 1 0 545086787 21016576 4408 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5131 4408 603 41 0 5090 0
vsize: 20524
[startup+50.0014 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 5071 0 0 0 4988 10 0 0 25 0 1 0 545086787 23703552 4987 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5787 4987 603 41 0 5746 0
vsize: 23148
[startup+60.0013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 5409 0 0 0 5987 11 0 0 25 0 1 0 545086787 25055232 5325 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6117 5325 603 41 0 6076 0
vsize: 24468
[startup+70.0018 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 5814 0 0 0 6986 12 0 0 25 0 1 0 545086787 26669056 5730 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6511 5730 603 41 0 6470 0
vsize: 26044
[startup+80.0015 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 5961 0 0 0 7986 12 0 0 25 0 1 0 545086787 27209728 5877 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6643 5877 603 41 0 6602 0
vsize: 26572
[startup+90.0024 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 6119 0 0 0 8986 13 0 0 25 0 1 0 545086787 27910144 6035 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6814 6035 603 41 0 6773 0
vsize: 27256
[startup+100.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 6246 0 0 0 9986 13 0 0 25 0 1 0 545086787 28475392 6162 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6952 6162 603 41 0 6911 0
vsize: 27808
[startup+110.002 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 6364 0 0 0 10986 13 0 0 25 0 1 0 545086787 28880896 6280 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7051 6280 603 41 0 7010 0
vsize: 28204
[startup+120.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 6494 0 0 0 11985 15 0 0 25 0 1 0 545086787 29466624 6410 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7194 6410 603 41 0 7153 0
vsize: 28776
[startup+130.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 6618 0 0 0 12985 15 0 0 25 0 1 0 545086787 30093312 6534 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7347 6534 603 41 0 7306 0
vsize: 29388
[startup+140.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 6715 0 0 0 13985 15 0 0 25 0 1 0 545086787 30363648 6631 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7413 6631 603 41 0 7372 0
vsize: 29652
[startup+150.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 6824 0 0 0 14985 15 0 0 25 0 1 0 545086787 30937088 6740 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7553 6740 603 41 0 7512 0
vsize: 30212
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 6919 0 0 0 15985 15 0 0 25 0 1 0 545086787 31207424 6835 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7619 6835 603 41 0 7578 0
vsize: 30476
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7006 0 0 0 16985 15 0 0 25 0 1 0 545086787 31608832 6922 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7717 6922 603 41 0 7676 0
vsize: 30868
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7129 0 0 0 17985 16 0 0 25 0 1 0 545086787 32182272 7045 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7857 7045 603 41 0 7816 0
vsize: 31428
[startup+190.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7240 0 0 0 18985 16 0 0 25 0 1 0 545086787 33112064 7156 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8084 7156 603 41 0 8043 0
vsize: 32336
[startup+200.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7330 0 0 0 19985 17 0 0 25 0 1 0 545086787 33517568 7246 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8183 7246 603 41 0 8142 0
vsize: 32732
[startup+210.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7428 0 0 0 20984 17 0 0 25 0 1 0 545086787 33800192 7344 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8252 7344 603 41 0 8211 0
vsize: 33008
[startup+220.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7517 0 0 0 21984 17 0 0 25 0 1 0 545086787 34324480 7433 4294967295 134512640 134672761 3221224544 3221223712 134561220 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8380 7433 603 41 0 8339 0
vsize: 33520
[startup+230.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7645 0 0 0 22984 18 0 0 25 0 1 0 545086787 34721792 7561 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8477 7561 603 41 0 8436 0
vsize: 33908
[startup+240.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7720 0 0 0 23984 18 0 0 25 0 1 0 545086787 34992128 7636 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8543 7636 603 41 0 8502 0
vsize: 34172
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7798 0 0 0 24984 18 0 0 25 0 1 0 545086787 35397632 7714 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8642 7714 603 41 0 8601 0
vsize: 34568
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 7873 0 0 0 25984 19 0 0 25 0 1 0 545086787 35663872 7789 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8707 7789 603 41 0 8666 0
vsize: 34828
[startup+270.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8433 0 0 0 26981 21 0 0 25 0 1 0 545086787 38006784 8349 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8349 603 41 0 9238 0
vsize: 37116
[startup+280.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8433 0 0 0 27982 21 0 0 25 0 1 0 545086787 38006784 8349 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8349 603 41 0 9238 0
vsize: 37116
[startup+290.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8433 0 0 0 28982 21 0 0 25 0 1 0 545086787 38006784 8349 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8349 603 41 0 9238 0
vsize: 37116
[startup+300.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8433 0 0 0 29983 21 0 0 25 0 1 0 545086787 38006784 8349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8349 603 41 0 9238 0
vsize: 37116
[startup+310.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8433 0 0 0 30980 21 0 0 25 0 1 0 545086787 38006784 8349 4294967295 134512640 134672761 3221224544 3221223712 134561003 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9279 8349 603 41 0 9238 0
vsize: 37116
[startup+320.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8433 0 0 0 31979 22 0 0 25 0 1 0 545086787 38006784 8349 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8349 603 41 0 9238 0
vsize: 37116
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8433 0 0 0 32980 22 0 0 25 0 1 0 545086787 38006784 8349 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8349 603 41 0 9238 0
vsize: 37116
[startup+340.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8433 0 0 0 33980 22 0 0 25 0 1 0 545086787 38006784 8349 4294967295 134512640 134672761 3221224544 3221223712 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8349 603 41 0 9238 0
vsize: 37116
[startup+350.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8434 0 0 0 34980 22 0 0 25 0 1 0 545086787 38006784 8350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8350 603 41 0 9238 0
vsize: 37116
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8434 0 0 0 35980 22 0 0 25 0 1 0 545086787 38006784 8350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8350 603 41 0 9238 0
vsize: 37116
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8434 0 0 0 36980 22 0 0 25 0 1 0 545086787 38006784 8350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8350 603 41 0 9238 0
vsize: 37116
[startup+380.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8438 0 0 0 37980 22 0 0 25 0 1 0 545086787 38006784 8354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8354 603 41 0 9238 0
vsize: 37116
[startup+390.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8439 0 0 0 38981 22 0 0 25 0 1 0 545086787 38006784 8355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8355 603 41 0 9238 0
vsize: 37116
[startup+400.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8439 0 0 0 39981 22 0 0 25 0 1 0 545086787 38006784 8355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9279 8355 603 41 0 9238 0
vsize: 37116
[startup+410.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8464 0 0 0 40981 22 0 0 25 0 1 0 545086787 38162432 8380 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9317 8380 603 41 0 9276 0
vsize: 37268
[startup+420.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8476 0 0 0 41981 22 0 0 25 0 1 0 545086787 38162432 8392 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9317 8392 603 41 0 9276 0
vsize: 37268
[startup+430.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8556 0 0 0 42981 22 0 0 25 0 1 0 545086787 38621184 8472 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9429 8472 603 41 0 9388 0
vsize: 37716
[startup+440.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 8722 0 0 0 43981 22 0 0 25 0 1 0 545086787 39206912 8638 4294967295 134512640 134672761 3221224544 3221223680 134560729 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9572 8638 603 41 0 9531 0
vsize: 38288
[startup+450.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 9301 0 0 0 44979 24 0 0 25 0 1 0 545086787 41623552 9217 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10162 9217 603 41 0 10121 0
vsize: 40648
[startup+460.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 9594 0 0 0 45977 25 0 0 25 0 1 0 545086787 42831872 9510 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10457 9510 603 41 0 10416 0
vsize: 41828
[startup+470.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 9892 0 0 0 46976 26 0 0 25 0 1 0 545086787 44040192 9808 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10752 9808 603 41 0 10711 0
vsize: 43008
[startup+480.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10311 0 0 0 47974 29 0 0 25 0 1 0 545086787 45801472 10227 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11182 10227 603 41 0 11141 0
vsize: 44728
[startup+490.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10821 0 0 0 48972 30 0 0 25 0 1 0 545086787 47820800 10737 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11675 10737 603 41 0 11634 0
vsize: 46700
[startup+500.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10950 0 0 0 49972 31 0 0 25 0 1 0 545086787 48361472 10866 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10866 603 41 0 11766 0
vsize: 47228
[startup+510.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 50972 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+520.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 51972 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+530.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 52972 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223728 134559392 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+540.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 53973 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+550.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 54973 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223716 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+560.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 55973 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+570.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 56973 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+580.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 57973 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+590.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 58974 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+600.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 59974 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+610.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 60974 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+620.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 61974 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+630.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 62974 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+640.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10951 0 0 0 63974 31 0 0 25 0 1 0 545086787 48361472 10867 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11807 10867 603 41 0 11766 0
vsize: 47228
[startup+650.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 10979 0 0 0 64975 31 0 0 25 0 1 0 545086787 48529408 10895 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11848 10895 603 41 0 11807 0
vsize: 47392
[startup+660.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 11054 0 0 0 65975 31 0 0 25 0 1 0 545086787 48799744 10970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11914 10970 603 41 0 11873 0
vsize: 47656
[startup+670.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 11188 0 0 0 66974 32 0 0 25 0 1 0 545086787 49373184 11104 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12054 11104 603 41 0 12013 0
vsize: 48216
[startup+680.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 11334 0 0 0 67974 32 0 0 25 0 1 0 545086787 50040832 11250 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12217 11250 603 41 0 12176 0
vsize: 48868
[startup+690.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 11686 0 0 0 68973 34 0 0 25 0 1 0 545086787 51527680 11602 4294967295 134512640 134672761 3221224544 3221223692 134565968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12580 11602 603 41 0 12539 0
vsize: 50320
[startup+700.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12262 0 0 0 69971 36 0 0 25 0 1 0 545086787 53813248 12178 4294967295 134512640 134672761 3221224544 3221223728 134559031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13138 12178 603 41 0 13097 0
vsize: 52552
[startup+710.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12411 0 0 0 70970 37 0 0 25 0 1 0 545086787 54476800 12327 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12327 603 41 0 13259 0
vsize: 53200
[startup+720.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12412 0 0 0 71970 37 0 0 25 0 1 0 545086787 54476800 12328 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12328 603 41 0 13259 0
vsize: 53200
[startup+730.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 72971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+740.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 73971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+750.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 74971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+760.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 75971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+770.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 76971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+780.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 77971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+790.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 78971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+800.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 79971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+810.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12414 0 0 0 80971 37 0 0 25 0 1 0 545086787 54476800 12330 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12330 603 41 0 13259 0
vsize: 53200
[startup+820.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12415 0 0 0 81971 38 0 0 25 0 1 0 545086787 54476800 12331 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13300 12331 603 41 0 13259 0
vsize: 53200
[startup+830.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12439 0 0 0 82971 38 0 0 25 0 1 0 545086787 54665216 12355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12355 603 41 0 13305 0
vsize: 53384
[startup+840.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12442 0 0 0 83971 38 0 0 25 0 1 0 545086787 54665216 12358 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12358 603 41 0 13305 0
vsize: 53384
[startup+850.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12444 0 0 0 84972 38 0 0 25 0 1 0 545086787 54665216 12360 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12360 603 41 0 13305 0
vsize: 53384
[startup+860.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12445 0 0 0 85972 38 0 0 25 0 1 0 545086787 54665216 12361 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12361 603 41 0 13305 0
vsize: 53384
[startup+870.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12446 0 0 0 86972 38 0 0 25 0 1 0 545086787 54665216 12362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12362 603 41 0 13305 0
vsize: 53384
[startup+880.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12446 0 0 0 87972 38 0 0 25 0 1 0 545086787 54665216 12362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12362 603 41 0 13305 0
vsize: 53384
[startup+890.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12447 0 0 0 88972 38 0 0 25 0 1 0 545086787 54665216 12363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12363 603 41 0 13305 0
vsize: 53384
[startup+900.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12447 0 0 0 89972 38 0 0 25 0 1 0 545086787 54665216 12363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12363 603 41 0 13305 0
vsize: 53384
[startup+910.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12447 0 0 0 90972 38 0 0 25 0 1 0 545086787 54665216 12363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12363 603 41 0 13305 0
vsize: 53384
[startup+920.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12447 0 0 0 91973 38 0 0 25 0 1 0 545086787 54665216 12363 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12363 603 41 0 13305 0
vsize: 53384
[startup+930.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12447 0 0 0 92973 38 0 0 25 0 1 0 545086787 54665216 12363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12363 603 41 0 13305 0
vsize: 53384
[startup+940.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12448 0 0 0 93973 38 0 0 25 0 1 0 545086787 54665216 12364 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13346 12364 603 41 0 13305 0
vsize: 53384
[startup+950.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12482 0 0 0 94973 38 0 0 25 0 1 0 545086787 54861824 12398 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13394 12398 603 41 0 13353 0
vsize: 53576
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12526 0 0 0 95973 38 0 0 25 0 1 0 545086787 55255040 12442 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13490 12442 603 41 0 13449 0
vsize: 53960
[startup+970.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12527 0 0 0 96973 38 0 0 25 0 1 0 545086787 55255040 12443 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13490 12443 603 41 0 13449 0
vsize: 53960
[startup+980.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12544 0 0 0 97973 38 0 0 25 0 1 0 545086787 55255040 12460 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13490 12460 603 41 0 13449 0
vsize: 53960
[startup+990.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12566 0 0 0 98973 38 0 0 25 0 1 0 545086787 55517184 12482 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13554 12482 603 41 0 13513 0
vsize: 54216
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12567 0 0 0 99974 38 0 0 25 0 1 0 545086787 55517184 12483 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13554 12483 603 41 0 13513 0
vsize: 54216
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12587 0 0 0 100974 38 0 0 25 0 1 0 545086787 55517184 12503 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13554 12503 603 41 0 13513 0
vsize: 54216
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12607 0 0 0 101972 39 0 0 25 0 1 0 545086787 55681024 12523 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13594 12523 603 41 0 13553 0
vsize: 54376
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12619 0 0 0 102972 39 0 0 25 0 1 0 545086787 55681024 12535 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 12535 603 41 0 13553 0
vsize: 54376
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12621 0 0 0 103972 39 0 0 25 0 1 0 545086787 55681024 12537 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 12537 603 41 0 13553 0
vsize: 54376
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12621 0 0 0 104972 39 0 0 25 0 1 0 545086787 55681024 12537 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 12537 603 41 0 13553 0
vsize: 54376
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12621 0 0 0 105973 39 0 0 25 0 1 0 545086787 55681024 12537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 12537 603 41 0 13553 0
vsize: 54376
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12621 0 0 0 106973 39 0 0 25 0 1 0 545086787 55681024 12537 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 12537 603 41 0 13553 0
vsize: 54376
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12622 0 0 0 107973 39 0 0 25 0 1 0 545086787 55681024 12538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13594 12538 603 41 0 13553 0
vsize: 54376
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12632 0 0 0 108973 39 0 0 25 0 1 0 545086787 55844864 12548 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13634 12548 603 41 0 13593 0
vsize: 54536
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12634 0 0 0 109973 39 0 0 25 0 1 0 545086787 55844864 12550 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13634 12550 603 41 0 13593 0
vsize: 54536
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12666 0 0 0 110973 39 0 0 25 0 1 0 545086787 56008704 12582 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13674 12582 603 41 0 13633 0
vsize: 54696
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12673 0 0 0 111974 39 0 0 25 0 1 0 545086787 56008704 12589 4294967295 134512640 134672761 3221224544 3221223712 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13674 12589 603 41 0 13633 0
vsize: 54696
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12693 0 0 0 112974 39 0 0 25 0 1 0 545086787 56172544 12609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12609 603 41 0 13673 0
vsize: 54856
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12703 0 0 0 113974 39 0 0 25 0 1 0 545086787 56172544 12619 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12619 603 41 0 13673 0
vsize: 54856
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12716 0 0 0 114974 39 0 0 25 0 1 0 545086787 56172544 12632 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12632 603 41 0 13673 0
vsize: 54856
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12717 0 0 0 115974 39 0 0 25 0 1 0 545086787 56172544 12633 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12633 603 41 0 13673 0
vsize: 54856
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12719 0 0 0 116975 39 0 0 25 0 1 0 545086787 56172544 12635 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12635 603 41 0 13673 0
vsize: 54856
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12719 0 0 0 117975 39 0 0 25 0 1 0 545086787 56172544 12635 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12635 603 41 0 13673 0
vsize: 54856
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12720 0 0 0 118975 39 0 0 25 0 1 0 545086787 56172544 12636 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12636 603 41 0 13673 0
vsize: 54856
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25709
Raw data (stat): 25709 (minisat+) R 25708 10614 10613 0 -1 0 12720 0 0 0 119975 39 0 0 25 0 1 0 545086787 56172544 12636 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13714 12636 603 41 0 13673 0
vsize: 54856
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25709
Raw data (stat): 25709 (minisat+) Z 25708 10614 10613 0 -1 12 12722 0 0 0 119975 42 0 0 25 0 1 0 545086787 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.05
CPU time (s): 1200.18
CPU user time (s): 1199.76
CPU system time (s): 0.421935
CPU usage (%): 100.011
Max. virtual memory (Kb): 54856
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####