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/miplib2003/normalized-mps-v2-13-7-vpm2.opb
MD5SUM	8c44064d4224b1d41c28f152218dd39f
Bench Category	optimization, small integers (OPTSMALLINT)
Has Objective Function	YES
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	98
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	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.05084
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 18383

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.169
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:        838596 kB
Buffers:         21600 kB
Cached:         153204 kB
SwapCached:        364 kB
Active:          13536 kB
Inactive:       163716 kB
HighTotal:      131008 kB
HighFree:       113848 kB
LowTotal:       903652 kB
LowFree:        724748 kB
SwapTotal:     2097136 kB
SwapFree:      2096356 kB
Dirty:              40 kB
Writeback:           0 kB
Mapped:           6388 kB
Slab:            13160 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 15:02:22 (client local time) WITH STATUS 0 IN 1200.42 SECONDS
stats: 18132 7 1200.42 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 486 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
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: 262   maxlim: 300367   bits: 19/19
c ---[ 272]---> Adder-cost: 208   maxlim: 210867   bits: 18/18
c ---[ 271]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 270]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 269]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 267]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 266]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 265]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 264]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 263]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 259]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 258]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 257]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 256]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 255]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[ 251]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 250]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 247]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 243]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 242]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 241]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 236]---> Adder-cost: 196   maxlim: 203300   bits: 18/18
c ---[ 235]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 234]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 233]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 229]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 228]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 227]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 224]---> Adder-cost: 232   maxlim: 322083   bits: 19/19
c ---[ 220]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 219]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 214]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 212]---> Adder-cost: 180   maxlim: 110883   bits: 17/17
c ---[ 211]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 206]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 205]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 198]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 197]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 193]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 192]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 191]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 185]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 184]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 183]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 179]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 178]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 175]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 171]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 170]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 169]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 168]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 167]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 166]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 164]---> Adder-cost: 228   maxlim: 229200   bits: 19/18
c ---[ 163]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 162]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 161]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 160]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 159]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 158]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 157]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 156]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 155]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 154]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 152]---> Adder-cost: 262   maxlim: 300367   bits: 19/19
c ---[ 150]---> Adder-cost: 260   maxlim: 219983   bits: 19/18
c ---[ 149]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 148]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 147]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 146]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 145]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 144]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 143]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 142]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 141]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 140]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 137]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 135]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 134]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 133]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 132]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 131]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 129]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 128]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 125]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 124]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 123]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 121]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 120]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 119]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 118]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 117]---> Adder-cost: 0   maxlim: 62   bits: 7/6
c ---[ 114]---> Adder-cost: 202   maxlim: 152900   bits: 18/18
c ---[ 113]---> Adder-cost: 0   maxlim: 126   bits: 8/7
c ---[ 112]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[ 111]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 110]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 109]---> Adder-cost: 0   maxlim: 30   bits: 6/5
c ---[ 107]---> Adder-cost: 234   maxlim: 244035   bits: 19/18
c ---[ 105]---> Adder-cost: 234   maxlim: 231235   bits: 19/18
c ---[ 103]---> Adder-cost: 278   maxlim: 283183   bits: 19/19
c ---[ 101]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  99]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  97]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  95]---> Adder-cost: 238   maxlim: 210767   bits: 18/18
c ---[  93]---> Adder-cost: 222   maxlim: 103983   bits: 17/17
c ---[  91]---> Adder-cost: 280   maxlim: 228400   bits: 19/18
c ---[  89]---> Adder-cost: 332   maxlim: 462383   bits: 20/19
c ---[  87]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  85]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  83]---> Adder-cost: 254   maxlim: 123183   bits: 18/17
c ---[  81]---> Adder-cost: 232   maxlim: 267600   bits: 19/19
c ---[  73]---> Adder-cost: 238   maxlim: 210767   bits: 18/18
c ---[  69]---> Adder-cost: 288   maxlim: 420400   bits: 20/19
c ---[  66]---> Adder-cost: 200   maxlim: 50101   bits: 17/16
c ---[  65]---> Adder-cost: 328   maxlim: 81851   bits: 17/17
c ---[  64]---> Adder-cost: 326   maxlim: 89851   bits: 17/17
c ---[  63]---> Adder-cost: 396   maxlim: 113601   bits: 17/17
c ---[  62]---> Adder-cost: 530   maxlim: 161476   bits: 18/18
c ---[  61]---> Adder-cost: 508   maxlim: 121476   bits: 18/17
c ---[  60]---> Adder-cost: 64   maxlim: 2133   bits: 12/12
c ---[  58]---> Adder-cost: 262   maxlim: 261967   bits: 19/18
c ---[  57]---> Adder-cost: 114   maxlim: 3403   bits: 12/12
c ---[  56]---> Adder-cost: 122   maxlim: 3723   bits: 13/12
c ---[  55]---> Adder-cost: 156   maxlim: 4033   bits: 13/12
c ---[  54]---> Adder-cost: 186   maxlim: 5308   bits: 13/13
c ---[  53]---> Adder-cost: 188   maxlim: 5628   bits: 13/13
c ---[  52]---> Adder-cost: 62   maxlim: 2357   bits: 12/12
c ---[  51]---> Adder-cost: 120   maxlim: 3627   bits: 13/12
c ---[  50]---> Adder-cost: 114   maxlim: 3787   bits: 13/12
c ---[  49]---> Adder-cost: 156   maxlim: 4737   bits: 13/13
c ---[  48]---> Adder-cost: 182   maxlim: 6012   bits: 13/13
c ---[  46]---> Adder-cost: 184   maxlim: 165300   bits: 18/18
c ---[  45]---> Adder-cost: 182   maxlim: 5692   bits: 13/13
c ---[  44]---> Adder-cost: 34   maxlim: 493   bits: 10/9
c ---[  43]---> Adder-cost: 60   maxlim: 619   bits: 10/10
c ---[  42]---> Adder-cost: 62   maxlim: 779   bits: 10/10
c ---[  41]---> Adder-cost: 82   maxlim: 809   bits: 10/10
c ---[  40]---> Adder-cost: 102   maxlim: 1192   bits: 11/11
c ---[  39]---> Adder-cost: 98   maxlim: 1000   bits: 11/10
c ---[  38]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  37]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  36]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  34]---> Adder-cost: 224   maxlim: 287667   bits: 19/19
c ---[  33]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  32]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  31]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  30]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  29]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  28]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  27]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  26]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  25]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  24]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  22]---> Adder-cost: 224   maxlim: 262067   bits: 19/18
c ---[  21]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  20]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  19]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  18]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  17]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  16]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  15]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  14]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[  13]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  12]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[  10]---> Adder-cost: 224   maxlim: 262067   bits: 19/18
c ---[   9]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   7]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[   6]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   5]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   4]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   3]---> Adder-cost: 14   maxlim: 126   bits: 8/7
c ---[   1]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ---[   0]---> Adder-cost: 2   maxlim: 254   bits: 9/8
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   91851   330985 |   30617       0        0     nan |  0.000 % |
c |       100 |   91814   330866 |   33678      95      696     7.3 | 20.180 % |
c |       252 |   91806   330840 |   37046     246     1649     6.7 | 20.186 % |
c |       477 |   91790   330788 |   40751     469     3404     7.3 | 20.196 % |
c |       815 |   91775   330743 |   44826     804     6665     8.3 | 20.213 % |
c |      1321 |   91775   330743 |   49308    1310    12548     9.6 | 20.213 % |
c |      2080 |   91751   330663 |   54239    2064    21294    10.3 | 20.229 % |
c |      3219 |   91735   330609 |   59663    3199    35655    11.1 | 20.240 % |
c |      4928 |   91703   330511 |   65630    4904    63152    12.9 | 20.277 % |
c |      7490 |   91665   330387 |   72193    7461   104474    14.0 | 20.310 % |
c |     11334 |   91581   330111 |   79412   11289   181161    16.0 | 20.380 % |
c |     17100 |   91492   329800 |   87353   16987   300639    17.7 | 20.412 % |
c |     25752 |   91492   329800 |   96089   25639   478462    18.7 | 20.412 % |
c |     38727 |   91483   329769 |  105698   38609   829071    21.5 | 20.418 % |
c |     58193 |   91460   329693 |  116268   58072  1381741    23.8 | 20.439 % |
c |     87386 |   91460   329693 |  127894   87265  2217399    25.4 | 20.439 % |
c |    131175 |   91273   329062 |  140684  130990  3217346    24.6 | 20.542 % |
c |    196859 |   91265   329040 |  154752   68276  2335690    34.2 | 20.553 % |
c |    295386 |   91073   328397 |  170227   27883   593770    21.3 | 20.677 % |
c |    443175 |   91032   328266 |  187250   20108   431274    21.4 | 20.709 % |
c |    664858 |   90944   327974 |  205975   68023  2395882    35.2 | 20.785 % |
#### 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.85 0.97 0.93 2/54 9652
Raw data (stat): 9652 (runsolver) R 9651 5897 5896 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 487658640 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.0015 s]
Raw data (loadavg): 0.87 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 3112 0 0 0 990 8 0 0 25 0 1 0 487658640 14962688 3030 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3653 3030 603 41 0 3612 0
vsize: 14612
[startup+20.0019 s]
Raw data (loadavg): 0.89 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 3636 0 0 0 1988 10 0 0 25 0 1 0 487658640 17104896 3554 4294967295 134512640 134672761 3221224544 3221223712 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4176 3554 603 41 0 4135 0
vsize: 16704
[startup+30.0022 s]
Raw data (loadavg): 0.91 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 4119 0 0 0 2986 13 0 0 25 0 1 0 487658640 19128320 4037 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4670 4037 603 41 0 4629 0
vsize: 18680
[startup+40.0031 s]
Raw data (loadavg): 0.92 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 4438 0 0 0 3984 14 0 0 25 0 1 0 487658640 20332544 4356 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4964 4356 603 41 0 4923 0
vsize: 19856
[startup+50.0035 s]
Raw data (loadavg): 0.93 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 4834 0 0 0 4983 16 0 0 25 0 1 0 487658640 22196224 4752 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5419 4752 603 41 0 5378 0
vsize: 21676
[startup+60.0049 s]
Raw data (loadavg): 0.94 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 5106 0 0 0 5982 17 0 0 25 0 1 0 487658640 23298048 5024 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5688 5024 603 41 0 5647 0
vsize: 22752
[startup+70.0056 s]
Raw data (loadavg): 0.95 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 5611 0 0 0 6980 19 0 0 25 0 1 0 487658640 25337856 5529 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6186 5529 603 41 0 6145 0
vsize: 24744
[startup+80.006 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 5809 0 0 0 7978 20 0 0 25 0 1 0 487658640 26169344 5727 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6389 5727 603 41 0 6348 0
vsize: 25556
[startup+90.0099 s]
Raw data (loadavg): 0.96 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 5985 0 0 0 8978 21 0 0 25 0 1 0 487658640 26845184 5903 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6554 5903 603 41 0 6513 0
vsize: 26216
[startup+100.02 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6164 0 0 0 9979 21 0 0 25 0 1 0 487658640 27693056 6082 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6761 6082 603 41 0 6720 0
vsize: 27044
[startup+110.038 s]
Raw data (loadavg): 0.97 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6308 0 0 0 10980 22 0 0 25 0 1 0 487658640 28295168 6226 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6908 6226 603 41 0 6867 0
vsize: 27632
[startup+120.06 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6496 0 0 0 11981 23 0 0 25 0 1 0 487658640 28962816 6414 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7071 6414 603 41 0 7030 0
vsize: 28284
[startup+130.075 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6663 0 0 0 12982 24 0 0 25 0 1 0 487658640 29642752 6581 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7237 6581 603 41 0 7196 0
vsize: 28948
[startup+140.075 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6799 0 0 0 13981 24 0 0 25 0 1 0 487658640 30318592 6717 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7402 6717 603 41 0 7361 0
vsize: 29608
[startup+150.088 s]
Raw data (loadavg): 0.98 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 6951 0 0 0 14981 26 0 0 25 0 1 0 487658640 31379456 6869 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7661 6869 603 41 0 7620 0
vsize: 30644
[startup+160.088 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7173 0 0 0 15979 27 0 0 25 0 1 0 487658640 32305152 7091 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7887 7091 603 41 0 7846 0
vsize: 31548
[startup+170.088 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7355 0 0 0 16979 28 0 0 25 0 1 0 487658640 33112064 7273 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8084 7273 603 41 0 8043 0
vsize: 32336
[startup+180.088 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7418 0 0 0 17978 29 0 0 25 0 1 0 487658640 33247232 7336 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8117 7336 603 41 0 8076 0
vsize: 32468
[startup+190.09 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7419 0 0 0 18978 29 0 0 25 0 1 0 487658640 33247232 7337 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8117 7337 603 41 0 8076 0
vsize: 32468
[startup+200.089 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7422 0 0 0 19978 29 0 0 25 0 1 0 487658640 33247232 7340 4294967295 134512640 134672761 3221224544 3221223724 134559056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8117 7340 603 41 0 8076 0
vsize: 32468
[startup+210.091 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7437 0 0 0 20978 29 0 0 25 0 1 0 487658640 33423360 7355 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8160 7355 603 41 0 8119 0
vsize: 32640
[startup+220.091 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7454 0 0 0 21978 29 0 0 25 0 1 0 487658640 33423360 7372 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8160 7372 603 41 0 8119 0
vsize: 32640
[startup+230.091 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7469 0 0 0 22978 30 0 0 25 0 1 0 487658640 33619968 7387 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8208 7387 603 41 0 8167 0
vsize: 32832
[startup+240.092 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7493 0 0 0 23978 30 0 0 25 0 1 0 487658640 33619968 7411 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8208 7411 603 41 0 8167 0
vsize: 32832
[startup+250.092 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7501 0 0 0 24978 30 0 0 25 0 1 0 487658640 33619968 7419 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8208 7419 603 41 0 8167 0
vsize: 32832
[startup+260.093 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7545 0 0 0 25978 30 0 0 25 0 1 0 487658640 33816576 7463 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8256 7463 603 41 0 8215 0
vsize: 33024
[startup+270.093 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7545 0 0 0 26977 31 0 0 25 0 1 0 487658640 33816576 7463 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8256 7463 603 41 0 8215 0
vsize: 33024
[startup+280.092 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7571 0 0 0 27977 31 0 0 25 0 1 0 487658640 34013184 7489 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 7489 603 41 0 8263 0
vsize: 33216
[startup+290.093 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7574 0 0 0 28977 32 0 0 25 0 1 0 487658640 34013184 7492 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 7492 603 41 0 8263 0
vsize: 33216
[startup+300.094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7574 0 0 0 29977 32 0 0 25 0 1 0 487658640 34013184 7492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 7492 603 41 0 8263 0
vsize: 33216
[startup+310.094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7574 0 0 0 30976 32 0 0 25 0 1 0 487658640 34013184 7492 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 7492 603 41 0 8263 0
vsize: 33216
[startup+320.094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7575 0 0 0 31976 33 0 0 25 0 1 0 487658640 34013184 7493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8304 7493 603 41 0 8263 0
vsize: 33216
[startup+330.094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7602 0 0 0 32976 33 0 0 25 0 1 0 487658640 34209792 7520 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8352 7520 603 41 0 8311 0
vsize: 33408
[startup+340.094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7603 0 0 0 33976 33 0 0 25 0 1 0 487658640 34209792 7521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8352 7521 603 41 0 8311 0
vsize: 33408
[startup+350.094 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7614 0 0 0 34976 33 0 0 25 0 1 0 487658640 34209792 7532 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8352 7532 603 41 0 8311 0
vsize: 33408
[startup+360.096 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7625 0 0 0 35976 33 0 0 25 0 1 0 487658640 34209792 7543 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8352 7543 603 41 0 8311 0
vsize: 33408
[startup+370.096 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7638 0 0 0 36976 34 0 0 25 0 1 0 487658640 34406400 7556 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8400 7556 603 41 0 8359 0
vsize: 33600
[startup+380.096 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7670 0 0 0 37976 34 0 0 25 0 1 0 487658640 34541568 7588 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8433 7588 603 41 0 8392 0
vsize: 33732
[startup+390.096 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7740 0 0 0 38976 34 0 0 25 0 1 0 487658640 34811904 7658 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8499 7658 603 41 0 8458 0
vsize: 33996
[startup+400.096 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7824 0 0 0 39976 34 0 0 25 0 1 0 487658640 35082240 7742 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8565 7742 603 41 0 8524 0
vsize: 34260
[startup+410.096 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7899 0 0 0 40976 34 0 0 25 0 1 0 487658640 35487744 7817 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8664 7817 603 41 0 8623 0
vsize: 34656
[startup+420.097 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 7978 0 0 0 41976 35 0 0 25 0 1 0 487658640 35758080 7896 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8730 7896 603 41 0 8689 0
vsize: 34920
[startup+430.097 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8325 0 0 0 42975 36 0 0 25 0 1 0 487658640 37228544 8243 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9089 8243 603 41 0 9048 0
vsize: 36356
[startup+440.097 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8478 0 0 0 43974 37 0 0 25 0 1 0 487658640 37888000 8396 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9250 8396 603 41 0 9209 0
vsize: 37000
[startup+450.097 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8555 0 0 0 44974 37 0 0 25 0 1 0 487658640 38158336 8473 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9316 8473 603 41 0 9275 0
vsize: 37264
[startup+460.098 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8639 0 0 0 45974 37 0 0 25 0 1 0 487658640 38428672 8557 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9382 8557 603 41 0 9341 0
vsize: 37528
[startup+470.098 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8718 0 0 0 46974 37 0 0 25 0 1 0 487658640 38879232 8636 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9492 8636 603 41 0 9451 0
vsize: 37968
[startup+480.115 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8793 0 0 0 47976 38 0 0 25 0 1 0 487658640 39186432 8711 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9567 8711 603 41 0 9526 0
vsize: 38268
[startup+490.115 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8865 0 0 0 48976 38 0 0 25 0 1 0 487658640 39456768 8783 4294967295 134512640 134672761 3221224544 3221223360 134565852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9633 8783 603 41 0 9592 0
vsize: 38532
[startup+500.116 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8865 0 0 0 49976 38 0 0 25 0 1 0 487658640 39456768 8783 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9633 8783 603 41 0 9592 0
vsize: 38532
[startup+510.122 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8867 0 0 0 50977 38 0 0 25 0 1 0 487658640 39456768 8785 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9633 8785 603 41 0 9592 0
vsize: 38532
[startup+520.122 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8883 0 0 0 51977 38 0 0 25 0 1 0 487658640 39456768 8801 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9633 8801 603 41 0 9592 0
vsize: 38532
[startup+530.122 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8909 0 0 0 52977 38 0 0 25 0 1 0 487658640 39604224 8827 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9669 8827 603 41 0 9628 0
vsize: 38676
[startup+540.133 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8924 0 0 0 53978 38 0 0 25 0 1 0 487658640 39604224 8842 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9669 8842 603 41 0 9628 0
vsize: 38676
[startup+550.235 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8956 0 0 0 54988 38 0 0 25 0 1 0 487658640 39784448 8874 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9713 8874 603 41 0 9672 0
vsize: 38852
[startup+560.235 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8978 0 0 0 55988 38 0 0 25 0 1 0 487658640 39931904 8896 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9749 8896 603 41 0 9708 0
vsize: 38996
[startup+570.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8978 0 0 0 56990 38 0 0 25 0 1 0 487658640 39931904 8896 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9749 8896 603 41 0 9708 0
vsize: 38996
[startup+580.252 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8981 0 0 0 57990 38 0 0 25 0 1 0 487658640 39931904 8899 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9749 8899 603 41 0 9708 0
vsize: 38996
[startup+590.253 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8984 0 0 0 58991 38 0 0 25 0 1 0 487658640 39931904 8902 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9749 8902 603 41 0 9708 0
vsize: 38996
[startup+600.254 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8984 0 0 0 59991 38 0 0 25 0 1 0 487658640 39931904 8902 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9749 8902 603 41 0 9708 0
vsize: 38996
[startup+610.255 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8985 0 0 0 60991 38 0 0 25 0 1 0 487658640 39931904 8903 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9749 8903 603 41 0 9708 0
vsize: 38996
[startup+620.254 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 8993 0 0 0 61991 38 0 0 25 0 1 0 487658640 39931904 8911 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9749 8911 603 41 0 9708 0
vsize: 38996
[startup+630.254 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9025 0 0 0 62991 38 0 0 25 0 1 0 487658640 40259584 8943 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9829 8943 603 41 0 9788 0
vsize: 39316
[startup+640.255 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9027 0 0 0 63992 38 0 0 25 0 1 0 487658640 40259584 8945 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9829 8945 603 41 0 9788 0
vsize: 39316
[startup+650.255 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9028 0 0 0 64992 38 0 0 25 0 1 0 487658640 40259584 8946 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9829 8946 603 41 0 9788 0
vsize: 39316
[startup+660.258 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9029 0 0 0 65992 38 0 0 25 0 1 0 487658640 40259584 8947 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9829 8947 603 41 0 9788 0
vsize: 39316
[startup+670.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9031 0 0 0 66993 38 0 0 25 0 1 0 487658640 40259584 8949 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9829 8949 603 41 0 9788 0
vsize: 39316
[startup+680.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9032 0 0 0 67993 38 0 0 25 0 1 0 487658640 40259584 8950 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9829 8950 603 41 0 9788 0
vsize: 39316
[startup+690.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9035 0 0 0 68993 38 0 0 25 0 1 0 487658640 40259584 8953 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9829 8953 603 41 0 9788 0
vsize: 39316
[startup+700.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9153 0 0 0 69993 38 0 0 25 0 1 0 487658640 40660992 9071 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9927 9071 603 41 0 9886 0
vsize: 39708
[startup+710.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9259 0 0 0 70993 39 0 0 25 0 1 0 487658640 41066496 9177 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10026 9177 603 41 0 9985 0
vsize: 40104
[startup+720.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9355 0 0 0 71993 39 0 0 25 0 1 0 487658640 41467904 9273 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10124 9273 603 41 0 10083 0
vsize: 40496
[startup+730.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9441 0 0 0 72993 39 0 0 25 0 1 0 487658640 41873408 9359 4294967295 134512640 134672761 3221224544 3221223648 134554665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10223 9359 603 41 0 10182 0
vsize: 40892
[startup+740.261 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9441 0 0 0 73993 39 0 0 25 0 1 0 487658640 41873408 9359 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10223 9359 603 41 0 10182 0
vsize: 40892
[startup+750.261 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9441 0 0 0 74993 39 0 0 25 0 1 0 487658640 41873408 9359 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10223 9359 603 41 0 10182 0
vsize: 40892
[startup+760.261 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9452 0 0 0 75993 39 0 0 25 0 1 0 487658640 41873408 9370 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10223 9370 603 41 0 10182 0
vsize: 40892
[startup+770.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9455 0 0 0 76993 39 0 0 25 0 1 0 487658640 41873408 9373 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10223 9373 603 41 0 10182 0
vsize: 40892
[startup+780.26 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9464 0 0 0 77993 39 0 0 25 0 1 0 487658640 41873408 9382 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10223 9382 603 41 0 10182 0
vsize: 40892
[startup+790.261 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9497 0 0 0 78993 39 0 0 25 0 1 0 487658640 42012672 9415 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10257 9415 603 41 0 10216 0
vsize: 41028
[startup+800.261 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9499 0 0 0 79993 39 0 0 25 0 1 0 487658640 42012672 9417 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10257 9417 603 41 0 10216 0
vsize: 41028
[startup+810.262 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9506 0 0 0 80994 39 0 0 25 0 1 0 487658640 42176512 9424 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10297 9424 603 41 0 10256 0
vsize: 41188
[startup+820.262 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9508 0 0 0 81994 39 0 0 25 0 1 0 487658640 42176512 9426 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10297 9426 603 41 0 10256 0
vsize: 41188
[startup+830.261 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9517 0 0 0 82994 39 0 0 25 0 1 0 487658640 42176512 9435 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10297 9435 603 41 0 10256 0
vsize: 41188
[startup+840.262 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9571 0 0 0 83994 39 0 0 25 0 1 0 487658640 42569728 9489 4294967295 134512640 134672761 3221224544 3221223712 134561145 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10393 9489 603 41 0 10352 0
vsize: 41572
[startup+850.263 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9573 0 0 0 84994 39 0 0 25 0 1 0 487658640 42569728 9491 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10393 9491 603 41 0 10352 0
vsize: 41572
[startup+860.263 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9603 0 0 0 85995 39 0 0 25 0 1 0 487658640 42733568 9521 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10433 9521 603 41 0 10392 0
vsize: 41732
[startup+870.263 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9636 0 0 0 86995 39 0 0 25 0 1 0 487658640 42897408 9554 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10473 9554 603 41 0 10432 0
vsize: 41892
[startup+880.263 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9664 0 0 0 87995 39 0 0 25 0 1 0 487658640 43061248 9582 4294967295 134512640 134672761 3221224544 3221223560 1075353072 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10513 9582 603 41 0 10472 0
vsize: 42052
[startup+890.264 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9669 0 0 0 88995 39 0 0 25 0 1 0 487658640 43061248 9587 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10513 9587 603 41 0 10472 0
vsize: 42052
[startup+900.264 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9692 0 0 0 89995 39 0 0 25 0 1 0 487658640 43225088 9610 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10553 9610 603 41 0 10512 0
vsize: 42212
[startup+910.265 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9702 0 0 0 90995 39 0 0 25 0 1 0 487658640 43225088 9620 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10553 9620 603 41 0 10512 0
vsize: 42212
[startup+920.264 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9702 0 0 0 91996 39 0 0 25 0 1 0 487658640 43225088 9620 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10553 9620 603 41 0 10512 0
vsize: 42212
[startup+930.264 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9702 0 0 0 92996 39 0 0 25 0 1 0 487658640 43225088 9620 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10553 9620 603 41 0 10512 0
vsize: 42212
[startup+940.265 s]
Raw data (loadavg): 0.99 0.97 0.93 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9707 0 0 0 93996 39 0 0 25 0 1 0 487658640 43225088 9625 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10553 9625 603 41 0 10512 0
vsize: 42212
[startup+950.265 s]
Raw data (loadavg): 1.15 1.00 0.94 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9746 0 0 0 94996 39 0 0 25 0 1 0 487658640 43360256 9664 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10586 9664 603 41 0 10545 0
vsize: 42344
[startup+960.265 s]
Raw data (loadavg): 1.20 1.02 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 9900 0 0 0 95996 40 0 0 25 0 1 0 487658640 44036096 9818 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10751 9818 603 41 0 10710 0
vsize: 43004
[startup+970.266 s]
Raw data (loadavg): 1.17 1.02 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10063 0 0 0 96996 40 0 0 25 0 1 0 487658640 44707840 9981 4294967295 134512640 134672761 3221224544 3221223712 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10915 9981 603 41 0 10874 0
vsize: 43660
[startup+980.265 s]
Raw data (loadavg): 1.14 1.02 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10219 0 0 0 97996 40 0 0 25 0 1 0 487658640 45375488 10137 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11078 10137 603 41 0 11037 0
vsize: 44312
[startup+990.265 s]
Raw data (loadavg): 1.12 1.02 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10351 0 0 0 98996 40 0 0 25 0 1 0 487658640 45821952 10269 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11187 10269 603 41 0 11146 0
vsize: 44748
[startup+1000.27 s]
Raw data (loadavg): 1.10 1.02 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10486 0 0 0 99995 41 0 0 25 0 1 0 487658640 46358528 10404 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11318 10404 603 41 0 11277 0
vsize: 45272
[startup+1010.27 s]
Raw data (loadavg): 1.09 1.01 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10623 0 0 0 100995 41 0 0 25 0 1 0 487658640 46899200 10541 4294967295 134512640 134672761 3221224544 3221223712 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11450 10541 603 41 0 11409 0
vsize: 45800
[startup+1020.27 s]
Raw data (loadavg): 1.07 1.01 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10751 0 0 0 101995 42 0 0 25 0 1 0 487658640 47480832 10669 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11592 10669 603 41 0 11551 0
vsize: 46368
[startup+1030.27 s]
Raw data (loadavg): 1.06 1.01 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10848 0 0 0 102994 42 0 0 25 0 1 0 487658640 47886336 10766 4294967295 134512640 134672761 3221224544 3221223648 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11691 10766 603 41 0 11650 0
vsize: 46764
[startup+1040.27 s]
Raw data (loadavg): 1.05 1.01 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10848 0 0 0 103995 42 0 0 25 0 1 0 487658640 47886336 10766 4294967295 134512640 134672761 3221224544 3221223728 134559492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11691 10766 603 41 0 11650 0
vsize: 46764
[startup+1050.27 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10848 0 0 0 104995 42 0 0 25 0 1 0 487658640 47886336 10766 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11691 10766 603 41 0 11650 0
vsize: 46764
[startup+1060.27 s]
Raw data (loadavg): 1.04 1.01 0.95 2/54 9652
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10855 0 0 0 105995 42 0 0 25 0 1 0 487658640 47886336 10773 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11691 10773 603 41 0 11650 0
vsize: 46764
[startup+1070.27 s]
Raw data (loadavg): 1.11 1.03 0.95 2/54 9705
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10873 0 0 0 106994 43 0 0 25 0 1 0 487658640 48033792 10791 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11727 10791 603 41 0 11686 0
vsize: 46908
[startup+1080.27 s]
Raw data (loadavg): 1.09 1.02 0.95 2/54 9705
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10889 0 0 0 107994 43 0 0 25 0 1 0 487658640 48033792 10807 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11727 10807 603 41 0 11686 0
vsize: 46908
[startup+1090.27 s]
Raw data (loadavg): 1.08 1.02 0.95 2/54 9705
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10905 0 0 0 108994 43 0 0 25 0 1 0 487658640 48197632 10823 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11767 10823 603 41 0 11726 0
vsize: 47068
[startup+1100.27 s]
Raw data (loadavg): 1.07 1.02 0.95 2/54 9705
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10928 0 0 0 109994 43 0 0 25 0 1 0 487658640 48361472 10846 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11807 10846 603 41 0 11766 0
vsize: 47228
[startup+1110.27 s]
Raw data (loadavg): 1.06 1.02 0.95 2/54 9705
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10928 0 0 0 110993 44 0 0 25 0 1 0 487658640 48361472 10846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11807 10846 603 41 0 11766 0
vsize: 47228
[startup+1120.27 s]
Raw data (loadavg): 1.05 1.02 0.95 2/54 9705
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10928 0 0 0 111994 44 0 0 25 0 1 0 487658640 48361472 10846 4294967295 134512640 134672761 3221224544 3221223680 134560608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11807 10846 603 41 0 11766 0
vsize: 47228
[startup+1130.27 s]
Raw data (loadavg): 1.04 1.02 0.95 2/54 9705
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10928 0 0 0 112994 44 0 0 25 0 1 0 487658640 48361472 10846 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11807 10846 603 41 0 11766 0
vsize: 47228
[startup+1140.27 s]
Raw data (loadavg): 1.03 1.02 0.95 2/54 9707
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10938 0 0 0 113994 44 0 0 25 0 1 0 487658640 48361472 10856 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11807 10856 603 41 0 11766 0
vsize: 47228
[startup+1150.27 s]
Raw data (loadavg): 1.03 1.02 0.95 2/54 9707
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10951 0 0 0 114994 44 0 0 25 0 1 0 487658640 48508928 10869 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11843 10869 603 41 0 11802 0
vsize: 47372
[startup+1160.27 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 9707
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10961 0 0 0 115994 44 0 0 25 0 1 0 487658640 48508928 10879 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11843 10879 603 41 0 11802 0
vsize: 47372
[startup+1170.27 s]
Raw data (loadavg): 1.02 1.02 0.95 2/54 9707
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10962 0 0 0 116994 44 0 0 25 0 1 0 487658640 48508928 10880 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11843 10880 603 41 0 11802 0
vsize: 47372
[startup+1180.27 s]
Raw data (loadavg): 1.02 1.01 0.95 2/54 9707
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10962 0 0 0 117995 44 0 0 25 0 1 0 487658640 48508928 10880 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11843 10880 603 41 0 11802 0
vsize: 47372
[startup+1190.27 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 9707
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10972 0 0 0 118995 44 0 0 25 0 1 0 487658640 48508928 10890 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11843 10890 603 41 0 11802 0
vsize: 47372
[startup+1200.27 s]
Raw data (loadavg): 1.01 1.01 0.95 2/54 9707
Raw data (stat): 9652 (minisat+) R 9651 5897 5896 0 -1 0 10972 0 0 0 119995 44 0 0 25 0 1 0 487658640 48508928 10890 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11843 10890 603 41 0 11802 0
vsize: 47372
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.3 s]
Raw data (loadavg): 1.01 1.01 0.95 1/54 9707
Raw data (stat): 9652 (minisat+) Z 9651 5897 5896 0 -1 12 10974 0 0 0 119995 46 0 0 25 0 1 0 487658640 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.3
CPU time (s): 1200.42
CPU user time (s): 1199.96
CPU system time (s): 0.465929
CPU usage (%): 100.01
Max. virtual memory (Kb): 47372
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####