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/miplib/normalized-mps-v2-13-7-vpm1.opb
MD5SUM	96fe6be9d2b9e3e89a4b05733b0daf45
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	20
Optimality of the best value was proved	NO
Number of terms in the objective function	168
Biggest coefficient in the objective function	1
Number of bits for the biggest coefficient in the objective function	1
Sum of the numbers in the objective function	168
Number of bits of the sum of numbers in the objective function	8
Biggest number in a constraint	102400
Number of bits of the biggest number in a constraint	17
Biggest sum of numbers in a constraint	615983
Number of bits of the biggest sum of numbers	20
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	1.07084
Number of variables	2124
Total number of constraints	612
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	168
Number of constraints which are nor clauses,nor cardinality constraints	444
Minimum length of a constraint	1
Maximum length of a constraint	64
Trace number 18919

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-21 17:01:16 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=17365 boxname=wulflinc26 idbench=1336 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  96fe6be9d2b9e3e89a4b05733b0daf45  /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-vpm1.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-vpm1.opb /oldhome/oroussel/tmp/wulflinc26/normalized-mps-v2-13-7-vpm1.opb
IDLAUNCH: 17365
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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.061
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:        628152 kB
Buffers:         31276 kB
Cached:         347824 kB
SwapCached:         68 kB
Active:          67408 kB
Inactive:       314588 kB
HighTotal:      131008 kB
HighFree:         1708 kB
LowTotal:       903652 kB
LowFree:        626444 kB
SwapTotal:     2097892 kB
SwapFree:      2097800 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6876 kB
Slab:            19004 kB
Committed_AS:    63728 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-21 17:21:18 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 17365 7 1200.22 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: 16   maxlim: 381   bits: 9/9
c ---[ 190]---> Adder-cost: 46   maxlim: 635   bits: 10/10
c ---[ 189]---> Adder-cost: 48   maxlim: 699   bits: 10/10
c ---[ 188]---> Adder-cost: 70   maxlim: 889   bits: 10/10
c ---[ 187]---> Adder-cost: 90   maxlim: 1272   bits: 11/11
c ---[ 186]---> Adder-cost: 88   maxlim: 952   bits: 11/10
c ---[ 185]---> Adder-cost: 16   maxlim: 381   bits: 9/9
c ---[ 184]---> Adder-cost: 46   maxlim: 635   bits: 10/10
c ---[ 183]---> Adder-cost: 48   maxlim: 699   bits: 10/10
c ---[ 182]---> Adder-cost: 70   maxlim: 761   bits: 10/10
c ---[ 181]---> Adder-cost: 88   maxlim: 1016   bits: 11/10
c ---[ 180]---> Adder-cost: 88   maxlim: 1080   bits: 11/11
c ---[ 179]---> Adder-cost: 16   maxlim: 381   bits: 9/9
c ---[ 178]---> Adder-cost: 46   maxlim: 635   bits: 10/10
c ---[ 177]---> Adder-cost: 48   maxlim: 667   bits: 10/10
c ---[ 176]---> Adder-cost: 70   maxlim: 857   bits: 10/10
c ---[ 175]---> Adder-cost: 88   maxlim: 1112   bits: 11/11
c ---[ 174]---> Adder-cost: 88   maxlim: 1048   bits: 11/11
c ---[ 173]---> Adder-cost: 16   maxlim: 381   bits: 9/9
c ---[ 172]---> Adder-cost: 46   maxlim: 507   bits: 10/9
c ---[ 171]---> Adder-cost: 48   maxlim: 667   bits: 10/10
c ---[ 170]---> Adder-cost: 68   maxlim: 697   bits: 10/10
c ---[ 169]---> Adder-cost: 86   maxlim: 1080   bits: 11/11
c ---[ 168]---> Adder-cost: 78   maxlim: 888   bits: 10/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 |   74826   270067 |   24942       0        0     nan |  0.000 % |
c |       100 |   74775   269904 |   27436      92      383     4.2 | 23.181 % |
c |       250 |   74754   269838 |   30179     237     1448     6.1 | 23.200 % |
c |       476 |   74740   269791 |   33197     461     3338     7.2 | 23.212 % |
c |       813 |   74732   269765 |   36517     797     8121    10.2 | 23.219 % |
c |      1320 |   74724   269739 |   40169    1303    17352    13.3 | 23.225 % |
c |      2079 |   74709   269690 |   44186    2060    31569    15.3 | 23.237 % |
c |      3218 |   74679   269592 |   48604    3194    50324    15.8 | 23.268 % |
c |      4926 |   74672   269569 |   53465    4901    85714    17.5 | 23.275 % |
c |      7489 |   74623   269412 |   58811    7457   127242    17.1 | 23.331 % |
c |     11335 |   74607   269360 |   64693   11301   232513    20.6 | 23.349 % |
c |     17104 |   74540   269142 |   71162   17061   385436    22.6 | 23.418 % |
c |     25753 |   74467   268907 |   78278   25701   563219    21.9 | 23.499 % |
c |     38727 |   74296   268350 |   86106   38644   802935    20.8 | 23.654 % |
c |     58189 |   74272   268272 |   94717   58103  1417408    24.4 | 23.679 % |
c |     87382 |   74241   268167 |  104188   87291  2231893    25.6 | 23.704 % |
c |    131171 |   74218   268092 |  114607   36851   957821    26.0 | 23.729 % |
c |    196855 |   74171   267941 |  126068  102527  2937819    28.7 | 23.772 % |
c |    295381 |   74157   267895 |  138675   85446  2227531    26.1 | 23.785 % |
c |    443173 |   74093   267681 |  152543  107691  2862673    26.6 | 23.841 % |
#### 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.87 0.95 0.90 2/54 2572
Raw data (stat): 2572 (runsolver) R 2571 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546723281 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+10.0008 s]
Raw data (loadavg): 0.89 0.95 0.90 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 2745 0 0 0 992 7 0 0 25 0 1 0 546723281 12890112 2668 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3147 2668 603 41 0 3106 0
vsize: 12588
[startup+20.0014 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 3273 0 0 0 1990 8 0 0 25 0 1 0 546723281 15167488 3196 4294967295 134512640 134672761 3221224544 3221223728 134559327 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3703 3196 603 41 0 3662 0
vsize: 14812
[startup+30.0017 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 3958 0 0 0 2987 11 0 0 25 0 1 0 546723281 17858560 3881 4294967295 134512640 134672761 3221224544 3221223712 134560813 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4360 3881 603 41 0 4319 0
vsize: 17440
[startup+40.0018 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 4541 0 0 0 3986 13 0 0 25 0 1 0 546723281 20541440 4464 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5015 4464 603 41 0 4974 0
vsize: 20060
[startup+50.0024 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 4907 0 0 0 4984 14 0 0 25 0 1 0 546723281 21999616 4830 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5371 4830 603 41 0 5330 0
vsize: 21484
[startup+60.0027 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 5186 0 0 0 5983 16 0 0 25 0 1 0 546723281 23089152 5109 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5637 5109 603 41 0 5596 0
vsize: 22548
[startup+70.0028 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 5551 0 0 0 6982 17 0 0 25 0 1 0 546723281 24592384 5474 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6004 5474 603 41 0 5963 0
vsize: 24016
[startup+80.0034 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 5796 0 0 0 7981 18 0 0 25 0 1 0 546723281 25661440 5719 4294967295 134512640 134672761 3221224544 3221223544 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6265 5719 603 41 0 6224 0
vsize: 25060
[startup+90.0026 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 5985 0 0 0 8980 19 0 0 25 0 1 0 546723281 26456064 5908 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6459 5908 603 41 0 6418 0
vsize: 25836
[startup+100.003 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6061 0 0 0 9980 19 0 0 25 0 1 0 546723281 26718208 5984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6523 5984 603 41 0 6482 0
vsize: 26092
[startup+110.003 s]
Raw data (loadavg): 0.98 0.96 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6083 0 0 0 10980 19 0 0 25 0 1 0 546723281 26861568 6006 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6006 603 41 0 6517 0
vsize: 26232
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6088 0 0 0 11980 19 0 0 25 0 1 0 546723281 26861568 6011 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6011 603 41 0 6517 0
vsize: 26232
[startup+130.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6094 0 0 0 12980 20 0 0 25 0 1 0 546723281 26861568 6017 4294967295 134512640 134672761 3221224544 3221223728 134558654 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6017 603 41 0 6517 0
vsize: 26232
[startup+140.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6094 0 0 0 13980 20 0 0 25 0 1 0 546723281 26861568 6017 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6017 603 41 0 6517 0
vsize: 26232
[startup+150.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6094 0 0 0 14981 20 0 0 25 0 1 0 546723281 26861568 6017 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6558 6017 603 41 0 6517 0
vsize: 26232
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6107 0 0 0 15981 20 0 0 25 0 1 0 546723281 27025408 6030 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6598 6030 603 41 0 6557 0
vsize: 26392
[startup+170.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6113 0 0 0 16981 20 0 0 25 0 1 0 546723281 27025408 6036 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6598 6036 603 41 0 6557 0
vsize: 26392
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6113 0 0 0 17981 20 0 0 25 0 1 0 546723281 27025408 6036 4294967295 134512640 134672761 3221224544 3221223648 134559829 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6598 6036 603 41 0 6557 0
vsize: 26392
[startup+190.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6254 0 0 0 18981 20 0 0 25 0 1 0 546723281 27557888 6177 4294967295 134512640 134672761 3221224544 3221223712 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6728 6177 603 41 0 6687 0
vsize: 26912
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6413 0 0 0 19980 21 0 0 25 0 1 0 546723281 28254208 6336 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6898 6336 603 41 0 6857 0
vsize: 27592
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6599 0 0 0 20980 21 0 0 25 0 1 0 546723281 29065216 6522 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7096 6522 603 41 0 7055 0
vsize: 28384
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6753 0 0 0 21980 21 0 0 25 0 1 0 546723281 29601792 6676 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7227 6676 603 41 0 7186 0
vsize: 28908
[startup+230.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 6893 0 0 0 22980 21 0 0 25 0 1 0 546723281 30269440 6816 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7390 6816 603 41 0 7349 0
vsize: 29560
[startup+240.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7019 0 0 0 23980 22 0 0 25 0 1 0 546723281 30666752 6942 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7487 6942 603 41 0 7446 0
vsize: 29948
[startup+250.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7139 0 0 0 24980 22 0 0 25 0 1 0 546723281 31195136 7062 4294967295 134512640 134672761 3221224544 3221223712 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7616 7062 603 41 0 7575 0
vsize: 30464
[startup+260.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2572
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7252 0 0 0 25980 23 0 0 25 0 1 0 546723281 31649792 7175 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7727 7175 603 41 0 7686 0
vsize: 30908
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7365 0 0 0 26979 23 0 0 25 0 1 0 546723281 32047104 7288 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7824 7288 603 41 0 7783 0
vsize: 31296
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7414 0 0 0 27979 23 0 0 25 0 1 0 546723281 32845824 7337 4294967295 134512640 134672761 3221224544 3221223728 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7337 603 41 0 7978 0
vsize: 32076
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7414 0 0 0 28979 23 0 0 25 0 1 0 546723281 32845824 7337 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7337 603 41 0 7978 0
vsize: 32076
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7421 0 0 0 29980 23 0 0 25 0 1 0 546723281 32845824 7344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7344 603 41 0 7978 0
vsize: 32076
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7431 0 0 0 30980 23 0 0 25 0 1 0 546723281 32845824 7354 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8019 7354 603 41 0 7978 0
vsize: 32076
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7439 0 0 0 31980 23 0 0 25 0 1 0 546723281 32993280 7362 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8055 7362 603 41 0 8014 0
vsize: 32220
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7440 0 0 0 32980 23 0 0 25 0 1 0 546723281 32993280 7363 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8055 7363 603 41 0 8014 0
vsize: 32220
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7464 0 0 0 33980 23 0 0 25 0 1 0 546723281 32993280 7387 4294967295 134512640 134672761 3221224544 3221223648 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8055 7387 603 41 0 8014 0
vsize: 32220
[startup+350.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7474 0 0 0 34980 23 0 0 25 0 1 0 546723281 33189888 7397 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7397 603 41 0 8062 0
vsize: 32412
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7476 0 0 0 35981 23 0 0 25 0 1 0 546723281 33189888 7399 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7399 603 41 0 8062 0
vsize: 32412
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7489 0 0 0 36981 23 0 0 25 0 1 0 546723281 33189888 7412 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8103 7412 603 41 0 8062 0
vsize: 32412
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7504 0 0 0 37981 23 0 0 25 0 1 0 546723281 33353728 7427 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7427 603 41 0 8102 0
vsize: 32572
[startup+390.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7505 0 0 0 38981 23 0 0 25 0 1 0 546723281 33353728 7428 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7428 603 41 0 8102 0
vsize: 32572
[startup+400.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7509 0 0 0 39981 23 0 0 25 0 1 0 546723281 33353728 7432 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7432 603 41 0 8102 0
vsize: 32572
[startup+410.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7528 0 0 0 40981 23 0 0 25 0 1 0 546723281 33353728 7451 4294967295 134512640 134672761 3221224544 3221223728 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7451 603 41 0 8102 0
vsize: 32572
[startup+420.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7530 0 0 0 41982 23 0 0 25 0 1 0 546723281 33353728 7453 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7453 603 41 0 8102 0
vsize: 32572
[startup+430.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7532 0 0 0 42982 23 0 0 25 0 1 0 546723281 33353728 7455 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8143 7455 603 41 0 8102 0
vsize: 32572
[startup+440.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7595 0 0 0 43982 24 0 0 25 0 1 0 546723281 33746944 7518 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8239 7518 603 41 0 8198 0
vsize: 32956
[startup+450.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7600 0 0 0 44981 24 0 0 25 0 1 0 546723281 33746944 7523 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8239 7523 603 41 0 8198 0
vsize: 32956
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7632 0 0 0 45981 24 0 0 25 0 1 0 546723281 33943552 7555 4294967295 134512640 134672761 3221224544 3221223716 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8287 7555 603 41 0 8246 0
vsize: 33148
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7651 0 0 0 46981 24 0 0 25 0 1 0 546723281 33943552 7574 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8287 7574 603 41 0 8246 0
vsize: 33148
[startup+480.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7658 0 0 0 47982 24 0 0 25 0 1 0 546723281 33943552 7581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8287 7581 603 41 0 8246 0
vsize: 33148
[startup+490.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7661 0 0 0 48982 24 0 0 25 0 1 0 546723281 33943552 7584 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8287 7584 603 41 0 8246 0
vsize: 33148
[startup+500.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7667 0 0 0 49982 24 0 0 25 0 1 0 546723281 34107392 7590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7590 603 41 0 8286 0
vsize: 33308
[startup+510.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7667 0 0 0 50982 24 0 0 25 0 1 0 546723281 34107392 7590 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7590 603 41 0 8286 0
vsize: 33308
[startup+520.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7668 0 0 0 51982 24 0 0 25 0 1 0 546723281 34107392 7591 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7591 603 41 0 8286 0
vsize: 33308
[startup+530.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7669 0 0 0 52983 24 0 0 25 0 1 0 546723281 34107392 7592 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7592 603 41 0 8286 0
vsize: 33308
[startup+540.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7679 0 0 0 53983 24 0 0 25 0 1 0 546723281 34107392 7602 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7602 603 41 0 8286 0
vsize: 33308
[startup+550.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7680 0 0 0 54983 24 0 0 25 0 1 0 546723281 34107392 7603 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7603 603 41 0 8286 0
vsize: 33308
[startup+560.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7686 0 0 0 55983 24 0 0 25 0 1 0 546723281 34107392 7609 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7609 603 41 0 8286 0
vsize: 33308
[startup+570.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7689 0 0 0 56983 24 0 0 25 0 1 0 546723281 34107392 7612 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7612 603 41 0 8286 0
vsize: 33308
[startup+580.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7691 0 0 0 57983 24 0 0 25 0 1 0 546723281 34107392 7614 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8327 7614 603 41 0 8286 0
vsize: 33308
[startup+590.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7758 0 0 0 58983 24 0 0 25 0 1 0 546723281 34377728 7681 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8393 7681 603 41 0 8352 0
vsize: 33572
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7821 0 0 0 59984 24 0 0 25 0 1 0 546723281 34648064 7744 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8459 7744 603 41 0 8418 0
vsize: 33836
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7896 0 0 0 60984 24 0 0 25 0 1 0 546723281 34942976 7819 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8531 7819 603 41 0 8490 0
vsize: 34124
[startup+620.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7936 0 0 0 61984 24 0 0 25 0 1 0 546723281 35078144 7859 4294967295 134512640 134672761 3221224544 3221223648 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8564 7859 603 41 0 8523 0
vsize: 34256
[startup+630.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7941 0 0 0 62984 24 0 0 25 0 1 0 546723281 35213312 7864 4294967295 134512640 134672761 3221224544 3221223712 134560845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7864 603 41 0 8556 0
vsize: 34388
[startup+640.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7944 0 0 0 63984 24 0 0 25 0 1 0 546723281 35213312 7867 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7867 603 41 0 8556 0
vsize: 34388
[startup+650.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7960 0 0 0 64984 25 0 0 25 0 1 0 546723281 35213312 7883 4294967295 134512640 134672761 3221224544 3221223712 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7883 603 41 0 8556 0
vsize: 34388
[startup+660.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7962 0 0 0 65984 25 0 0 25 0 1 0 546723281 35213312 7885 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7885 603 41 0 8556 0
vsize: 34388
[startup+670.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7977 0 0 0 66984 25 0 0 25 0 1 0 546723281 35213312 7900 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8597 7900 603 41 0 8556 0
vsize: 34388
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7993 0 0 0 67984 25 0 0 25 0 1 0 546723281 35409920 7916 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7916 603 41 0 8604 0
vsize: 34580
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7994 0 0 0 68984 26 0 0 25 0 1 0 546723281 35409920 7917 4294967295 134512640 134672761 3221224544 3221223712 134561127 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7917 603 41 0 8604 0
vsize: 34580
[startup+700.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7995 0 0 0 69984 26 0 0 25 0 1 0 546723281 35409920 7918 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7918 603 41 0 8604 0
vsize: 34580
[startup+710.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 7996 0 0 0 70984 26 0 0 25 0 1 0 546723281 35409920 7919 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7919 603 41 0 8604 0
vsize: 34580
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8001 0 0 0 71984 26 0 0 25 0 1 0 546723281 35409920 7924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7924 603 41 0 8604 0
vsize: 34580
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8002 0 0 0 72985 26 0 0 25 0 1 0 546723281 35409920 7925 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7925 603 41 0 8604 0
vsize: 34580
[startup+740.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8003 0 0 0 73985 26 0 0 25 0 1 0 546723281 35409920 7926 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7926 603 41 0 8604 0
vsize: 34580
[startup+750.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8004 0 0 0 74985 26 0 0 25 0 1 0 546723281 35409920 7927 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7927 603 41 0 8604 0
vsize: 34580
[startup+760.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8005 0 0 0 75985 26 0 0 25 0 1 0 546723281 35409920 7928 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7928 603 41 0 8604 0
vsize: 34580
[startup+770.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8007 0 0 0 76985 26 0 0 25 0 1 0 546723281 35409920 7930 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8645 7930 603 41 0 8604 0
vsize: 34580
[startup+780.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8031 0 0 0 77985 26 0 0 25 0 1 0 546723281 35606528 7954 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7954 603 41 0 8652 0
vsize: 34772
[startup+790.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8038 0 0 0 78985 26 0 0 25 0 1 0 546723281 35606528 7961 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7961 603 41 0 8652 0
vsize: 34772
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8042 0 0 0 79986 26 0 0 25 0 1 0 546723281 35606528 7965 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7965 603 41 0 8652 0
vsize: 34772
[startup+810.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8045 0 0 0 80986 26 0 0 25 0 1 0 546723281 35606528 7968 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7968 603 41 0 8652 0
vsize: 34772
[startup+820.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8047 0 0 0 81986 26 0 0 25 0 1 0 546723281 35606528 7970 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7970 603 41 0 8652 0
vsize: 34772
[startup+830.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8050 0 0 0 82986 26 0 0 25 0 1 0 546723281 35606528 7973 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7973 603 41 0 8652 0
vsize: 34772
[startup+840.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8051 0 0 0 83986 26 0 0 25 0 1 0 546723281 35606528 7974 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7974 603 41 0 8652 0
vsize: 34772
[startup+850.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8051 0 0 0 84987 26 0 0 25 0 1 0 546723281 35606528 7974 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7974 603 41 0 8652 0
vsize: 34772
[startup+860.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8052 0 0 0 85987 26 0 0 25 0 1 0 546723281 35606528 7975 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7975 603 41 0 8652 0
vsize: 34772
[startup+870.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8061 0 0 0 86987 26 0 0 25 0 1 0 546723281 35606528 7984 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8693 7984 603 41 0 8652 0
vsize: 34772
[startup+880.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8112 0 0 0 87987 26 0 0 25 0 1 0 546723281 35835904 8035 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8749 8035 603 41 0 8708 0
vsize: 34996
[startup+890.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8179 0 0 0 88987 26 0 0 25 0 1 0 546723281 36229120 8102 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8845 8102 603 41 0 8804 0
vsize: 35380
[startup+900.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8182 0 0 0 89987 26 0 0 25 0 1 0 546723281 36229120 8105 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8845 8105 603 41 0 8804 0
vsize: 35380
[startup+910.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8215 0 0 0 90987 26 0 0 25 0 1 0 546723281 36425728 8138 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8893 8138 603 41 0 8852 0
vsize: 35572
[startup+920.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8216 0 0 0 91987 26 0 0 25 0 1 0 546723281 36425728 8139 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8893 8139 603 41 0 8852 0
vsize: 35572
[startup+930.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8225 0 0 0 92987 27 0 0 25 0 1 0 546723281 36425728 8148 4294967295 134512640 134672761 3221224544 3221223712 134560968 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8893 8148 603 41 0 8852 0
vsize: 35572
[startup+940.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8255 0 0 0 93987 27 0 0 25 0 1 0 546723281 36622336 8178 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8178 603 41 0 8900 0
vsize: 35764
[startup+950.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8267 0 0 0 94987 27 0 0 25 0 1 0 546723281 36622336 8190 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8190 603 41 0 8900 0
vsize: 35764
[startup+960.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8268 0 0 0 95987 27 0 0 25 0 1 0 546723281 36622336 8191 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8191 603 41 0 8900 0
vsize: 35764
[startup+970.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8269 0 0 0 96988 27 0 0 25 0 1 0 546723281 36622336 8192 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8941 8192 603 41 0 8900 0
vsize: 35764
[startup+980.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8311 0 0 0 97988 27 0 0 25 0 1 0 546723281 36884480 8234 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8234 603 41 0 8964 0
vsize: 36020
[startup+990.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8314 0 0 0 98988 27 0 0 25 0 1 0 546723281 36884480 8237 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8237 603 41 0 8964 0
vsize: 36020
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8315 0 0 0 99988 27 0 0 25 0 1 0 546723281 36884480 8238 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8238 603 41 0 8964 0
vsize: 36020
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8328 0 0 0 100988 27 0 0 25 0 1 0 546723281 36884480 8251 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8251 603 41 0 8964 0
vsize: 36020
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8328 0 0 0 101988 27 0 0 25 0 1 0 546723281 36884480 8251 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8251 603 41 0 8964 0
vsize: 36020
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8329 0 0 0 102988 27 0 0 25 0 1 0 546723281 36884480 8252 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9005 8252 603 41 0 8964 0
vsize: 36020
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8353 0 0 0 103989 27 0 0 25 0 1 0 546723281 37081088 8276 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9053 8276 603 41 0 9012 0
vsize: 36212
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8587 0 0 0 104988 28 0 0 25 0 1 0 546723281 38088704 8510 4294967295 134512640 134672761 3221224544 3221223648 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9299 8510 603 41 0 9258 0
vsize: 37196
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8670 0 0 0 105988 28 0 0 25 0 1 0 546723281 38359040 8593 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8670 0 0 0 106988 28 0 0 25 0 1 0 546723281 38359040 8593 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8670 0 0 0 107988 28 0 0 25 0 1 0 546723281 38359040 8593 4294967295 134512640 134672761 3221224544 3221223712 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8670 0 0 0 108989 28 0 0 25 0 1 0 546723281 38359040 8593 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8670 0 0 0 109989 28 0 0 25 0 1 0 546723281 38359040 8593 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8593 603 41 0 9324 0
vsize: 37460
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8671 0 0 0 110990 28 0 0 25 0 1 0 546723281 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8671 0 0 0 111990 28 0 0 25 0 1 0 546723281 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8671 0 0 0 112990 28 0 0 25 0 1 0 546723281 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8671 0 0 0 113990 28 0 0 25 0 1 0 546723281 38359040 8594 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8594 603 41 0 9324 0
vsize: 37460
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8676 0 0 0 114990 28 0 0 25 0 1 0 546723281 38359040 8599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9365 8599 603 41 0 9324 0
vsize: 37460
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8683 0 0 0 115991 28 0 0 25 0 1 0 546723281 38522880 8606 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8606 603 41 0 9364 0
vsize: 37620
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8685 0 0 0 116991 28 0 0 25 0 1 0 546723281 38522880 8608 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8608 603 41 0 9364 0
vsize: 37620
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8692 0 0 0 117991 28 0 0 25 0 1 0 546723281 38522880 8615 4294967295 134512640 134672761 3221224544 3221223640 134555595 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8615 603 41 0 9364 0
vsize: 37620
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8701 0 0 0 118991 28 0 0 25 0 1 0 546723281 38522880 8624 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8624 603 41 0 9364 0
vsize: 37620
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2574
Raw data (stat): 2572 (minisat+) R 2571 22612 22611 0 -1 0 8706 0 0 0 119991 28 0 0 25 0 1 0 546723281 38522880 8629 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9405 8629 603 41 0 9364 0
vsize: 37620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 2574
Raw data (stat): 2572 (minisat+) Z 2571 22612 22611 0 -1 12 8708 0 0 0 119991 30 0 0 25 0 1 0 546723281 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.04
CPU time (s): 1200.22
CPU user time (s): 1199.92
CPU system time (s): 0.302953
CPU usage (%): 100.015
Max. virtual memory (Kb): 37620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####