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-dcmulti.opb
MD5SUM	6ffc4ed72f4dd993b121ae0a2045731e
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	9505
Biggest coefficient in the objective function	697303040
Number of bits for the biggest coefficient in the objective function	30
Sum of the numbers in the objective function	66656504525
Number of bits of the sum of numbers in the objective function	36
Biggest number in a constraint	697303040
Number of bits of the biggest number in a constraint	30
Biggest sum of numbers in a constraint	66656504525
Number of bits of the biggest sum of numbers	36
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.087986
Number of variables	9535
Total number of constraints	365
Number of constraints which are clauses	27
Number of constraints which are cardinality constraints (but not clauses)	80
Number of constraints which are nor clauses,nor cardinality constraints	258
Minimum length of a constraint	1
Maximum length of a constraint	280
Trace number 19322

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-21 18:49:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=16767 boxname=wulflinc15 idbench=1290 idsolver=10 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  6ffc4ed72f4dd993b121ae0a2045731e  /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-dcmulti.opb
REAL COMMAND:  minisat+ -ca /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-dcmulti.opb /oldhome/oroussel/tmp/wulflinc15/normalized-mps-v2-13-7-dcmulti.opb
IDLAUNCH: 16767
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        572672 kB
Buffers:         33124 kB
Cached:         406940 kB
SwapCached:        440 kB
Active:          78276 kB
Inactive:       363988 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        572420 kB
SwapTotal:     2097136 kB
SwapFree:      2095984 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5360 kB
Slab:            14040 kB
Committed_AS:    63476 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-21 19:09:06 (client local time) WITH STATUS 0 IN 1200.35 SECONDS
stats: 16767 7 1200.35 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 368 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ##############################################################################
c   -- Clauses(.)/Splits(s): s....s.....sssssssssssssssssss....s.....ssssssssssssssssss....s.....sssssssssssssssssss
c ---[ 427]---> Adder-cost: 43   maxlim: 6270   bits: 14/13
c ---[ 426]---> Adder-cost: 140   maxlim: 81914   bits: 17/17
c ---[ 425]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 424]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 422]---> Adder-cost: 30   maxlim: 31614   bits: 16/15
c ---[ 421]---> Adder-cost: 43   maxlim: 6270   bits: 14/13
c ---[ 420]---> Adder-cost: 28   maxlim: 14846   bits: 15/14
c ---[ 419]---> Adder-cost: 41   maxlim: 2302   bits: 13/12
c ---[ 418]---> Adder-cost: 28   maxlim: 15486   bits: 15/14
c ---[ 416]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 415]---> Adder-cost: 28   maxlim: 14846   bits: 15/14
c ---[ 413]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 411]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 409]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 407]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 405]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 403]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 401]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 399]---> Adder-cost: 445   maxlim: 262140   bits: 19/18
c ---[ 397]---> Adder-cost: 445   maxlim: 212988   bits: 19/18
c ---[ 395]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 394]---> Adder-cost: 41   maxlim: 2302   bits: 13/12
c ---[ 392]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 391]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 390]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 389]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 388]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 386]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 385]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 384]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 381]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 380]---> Adder-cost: 28   maxlim: 15486   bits: 15/14
c ---[ 378]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 377]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 376]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 375]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 374]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 372]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 371]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 370]---> Adder-cost: 16   maxlim: 44799   bits: 17/16
c ---[ 367]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 365]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 363]---> Adder-cost: 114   maxlim: 32766   bits: 16/15
c ---[ 362]---> Adder-cost: 11   maxlim: 32766   bits: 16/15
c ---[ 361]---> Adder-cost: 12   maxlim: 23039   bits: 16/15
c ---[ 360]---> Adder-cost: 11   maxlim: 16382   bits: 15/14
c ---[ 359]---> Adder-cost: 6   maxlim: 10239   bits: 15/14
c ---[ 357]---> Adder-cost: 115   maxlim: 32767   bits: 16/15
c ---[ 356]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 355]---> Adder-cost: 15   maxlim: 12799   bits: 15/14
c ---[ 352]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 350]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 348]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 347]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 346]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 345]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 344]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 342]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 341]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 340]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 337]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 335]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 333]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 332]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 331]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 330]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 329]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 327]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 326]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 322]---> Adder-cost: 16   maxlim: 5   bits: 4/3
c ---[ 320]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 308]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 296]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 293]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 292]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 291]---> Adder-cost: 160   maxlim: 327674   bits: 19/19
c ---[ 290]---> Adder-cost: 140   maxlim: 81914   bits: 17/17
c ---[ 289]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 288]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 286]---> Adder-cost: 30   maxlim: 31614   bits: 16/15
c ---[ 285]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 283]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 282]---> Adder-cost: 43   maxlim: 6270   bits: 14/13
c ---[ 281]---> Adder-cost: 28   maxlim: 14846   bits: 15/14
c ---[ 280]---> Adder-cost: 41   maxlim: 2302   bits: 13/12
c ---[ 279]---> Adder-cost: 28   maxlim: 15486   bits: 15/14
c ---[ 277]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 275]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 273]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 271]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 269]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 267]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 265]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 263]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 261]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 259]---> Adder-cost: 428   maxlim: 393212   bits: 20/19
c ---[ 257]---> Adder-cost: 428   maxlim: 344060   bits: 20/19
c ---[ 255]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 253]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 252]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 251]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 250]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 249]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 247]---> Adder-cost: 391   maxlim: 131069   bits: 18/17
c ---[ 245]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 244]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 243]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 240]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 238]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 237]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 236]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 235]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 234]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 232]---> Adder-cost: 391   maxlim: 81917   bits: 18/17
c ---[ 230]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 229]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 228]---> Adder-cost: 16   maxlim: 44799   bits: 17/16
c ---[ 225]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 223]---> Adder-cost: 114   maxlim: 32766   bits: 16/15
c ---[ 222]---> Adder-cost: 11   maxlim: 32766   bits: 16/15
c ---[ 221]---> Adder-cost: 12   maxlim: 23039   bits: 16/15
c ---[ 220]---> Adder-cost: 11   maxlim: 16382   bits: 15/14
c ---[ 219]---> Adder-cost: 6   maxlim: 10239   bits: 15/14
c ---[ 217]---> Adder-cost: 92   maxlim: 131070   bits: 18/17
c ---[ 215]---> Adder-cost: 115   maxlim: 32767   bits: 16/15
c ---[ 214]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 213]---> Adder-cost: 15   maxlim: 12799   bits: 15/14
c ---[ 210]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 208]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 207]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 206]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 205]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 204]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 202]---> Adder-cost: 91   maxlim: 65534   bits: 17/16
c ---[ 200]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 199]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 198]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 195]---> Adder-cost: 122   maxlim: 131070   bits: 18/17
c ---[ 193]---> Adder-cost: 119   maxlim: 65534   bits: 17/16
c ---[ 192]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 191]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 190]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 189]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 188]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 186]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 185]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[ 181]---> Adder-cost: 16   maxlim: 5   bits: 4/3
c ---[ 175]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 164]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 156]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 155]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 154]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 153]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 152]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 151]---> Adder-cost: 2   maxlim: 1   bits: 2/1
c ---[ 150]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 148]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 147]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 146]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 143]---> Adder-cost: 92   maxlim: 131070   bits: 18/17
c ---[ 141]---> Adder-cost: 91   maxlim: 65534   bits: 17/16
c ---[ 140]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 139]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 138]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 137]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 136]---> Adder-cost: 160   maxlim: 327674   bits: 19/19
c ---[ 134]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 133]---> Adder-cost: 14   maxlim: 65534   bits: 17/16
c ---[ 132]---> Adder-cost: 16   maxlim: 44799   bits: 17/16
c ---[ 129]---> Adder-cost: 89   maxlim: 65534   bits: 17/16
c ---[ 127]---> Adder-cost: 86   maxlim: 32766   bits: 16/15
c ---[ 126]---> Adder-cost: 11   maxlim: 32766   bits: 16/15
c ---[ 125]---> Adder-cost: 12   maxlim: 23039   bits: 16/15
c ---[ 124]---> Adder-cost: 11   maxlim: 16382   bits: 15/14
c ---[ 123]---> Adder-cost: 6   maxlim: 10239   bits: 15/14
c ---[ 122]---> Adder-cost: 140   maxlim: 81914   bits: 17/17
c ---[ 120]---> Adder-cost: 115   maxlim: 32767   bits: 16/15
c ---[ 119]---> Adder-cost: 16   maxlim: 32766   bits: 16/15
c ---[ 118]---> Adder-cost: 15   maxlim: 12799   bits: 15/14
c ---[ 115]---> Adder-cost: 92   maxlim: 131070   bits: 18/17
c ---[ 113]---> Adder-cost: 91   maxlim: 65534   bits: 17/16
c ---[ 112]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[ 111]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[ 110]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[ 109]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[ 108]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[ 106]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[ 105]---> Adder-cost: 16   maxlim: 65534   bits: 17/16
c ---[ 104]---> Adder-cost: 15   maxlim: 25599   bits: 16/15
c ---[ 101]---> Adder-cost: 92   maxlim: 131070   bits: 18/17
c ---[  99]---> Adder-cost: 91   maxlim: 65534   bits: 17/16
c ---[  98]---> Adder-cost: 13   maxlim: 65534   bits: 17/16
c ---[  97]---> Adder-cost: 19   maxlim: 23039   bits: 16/15
c ---[  96]---> Adder-cost: 13   maxlim: 32766   bits: 16/15
c ---[  95]---> Adder-cost: 9   maxlim: 10239   bits: 15/14
c ---[  94]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[  92]---> Adder-cost: 123   maxlim: 65535   bits: 17/16
c ---[  91]---> Adder-cost: 6   maxlim: 65534   bits: 17/16
c ---[  87]---> Adder-cost: 16   maxlim: 5   bits: 4/3
c ---[  70]---> Adder-cost: 30   maxlim: 31614   bits: 16/15
c ---[  62]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[  61]---> Adder-cost: 150   maxlim: 163834   bits: 18/18
c ---[  60]---> Adder-cost: 160   maxlim: 327674   bits: 19/19
c ---[  59]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[  58]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  57]---> Adder-cost: 114   maxlim: 4223   bits: 14/13
c ---[  56]---> Adder-cost: 104   maxlim: 2687   bits: 13/12
c ---[  55]---> Adder-cost: 114   maxlim: 6015   bits: 14/13
c ---[  54]---> Adder-cost: 102   maxlim: 3839   bits: 13/12
c ---[  53]---> Adder-cost: 120   maxlim: 8703   bits: 15/14
c ---[  52]---> Adder-cost: 114   maxlim: 5247   bits: 14/13
c ---[  51]---> Adder-cost: 104   maxlim: 3711   bits: 13/12
c ---[  50]---> Adder-cost: 100   maxlim: 2559   bits: 13/12
c ---[  49]---> Adder-cost: 104   maxlim: 3967   bits: 13/12
c ---[  48]---> Adder-cost: 94   maxlim: 1919   bits: 12/11
c ---[  47]---> Adder-cost: 120   maxlim: 9727   bits: 15/14
c ---[  46]---> Adder-cost: 104   maxlim: 3967   bits: 13/12
c ---[  45]---> Adder-cost: 114   maxlim: 4991   bits: 14/13
c ---[  44]---> Adder-cost: 104   maxlim: 2687   bits: 13/12
c ---[  43]---> Adder-cost: 94   maxlim: 4095   bits: 13/12
c ---[  42]---> Adder-cost: 92   maxlim: 1791   bits: 12/11
c ---[  41]---> Adder-cost: 124   maxlim: 9087   bits: 15/14
c ---[  40]---> Adder-cost: 114   maxlim: 4223   bits: 14/13
c ---[  39]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[  38]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  37]---> Adder-cost: 112   maxlim: 4863   bits: 14/13
c ---[  36]---> Adder-cost: 102   maxlim: 3327   bits: 13/12
c ---[  35]---> Adder-cost: 110   maxlim: 6655   bits: 14/13
c ---[  34]---> Adder-cost: 114   maxlim: 4479   bits: 14/13
c ---[  33]---> Adder-cost: 124   maxlim: 9343   bits: 15/14
c ---[  32]---> Adder-cost: 112   maxlim: 5887   bits: 14/13
c ---[  31]---> Adder-cost: 112   maxlim: 4351   bits: 14/13
c ---[  30]---> Adder-cost: 104   maxlim: 3199   bits: 13/12
c ---[  29]---> Adder-cost: 110   maxlim: 4607   bits: 14/13
c ---[  28]---> Adder-cost: 100   maxlim: 2559   bits: 13/12
c ---[  27]---> Adder-cost: 124   maxlim: 10367   bits: 15/14
c ---[  26]---> Adder-cost: 110   maxlim: 4607   bits: 14/13
c ---[  25]---> Adder-cost: 110   maxlim: 5631   bits: 14/13
c ---[  24]---> Adder-cost: 102   maxlim: 3327   bits: 13/12
c ---[  23]---> Adder-cost: 114   maxlim: 4735   bits: 14/13
c ---[  22]---> Adder-cost: 104   maxlim: 2431   bits: 13/12
c ---[  21]---> Adder-cost: 120   maxlim: 9727   bits: 15/14
c ---[  20]---> Adder-cost: 112   maxlim: 4863   bits: 14/13
c ---[  19]---> Adder-cost: 10   maxlim: 12799   bits: 15/14
c ---[  18]---> Adder-cost: 100   maxlim: 3583   bits: 13/12
c ---[  17]---> Adder-cost: 24   maxlim: 3326   bits: 13/12
c ---[  16]---> Adder-cost: 86   maxlim: 2047   bits: 12/11
c ---[  15]---> Adder-cost: 112   maxlim: 5375   bits: 14/13
c ---[  14]---> Adder-cost: 104   maxlim: 3199   bits: 13/12
c ---[  13]---> Adder-cost: 114   maxlim: 8063   bits: 14/13
c ---[  12]---> Adder-cost: 110   maxlim: 4607   bits: 14/13
c ---[  11]---> Adder-cost: 98   maxlim: 3071   bits: 13/12
c ---[  10]---> Adder-cost: 94   maxlim: 1919   bits: 12/11
c ---[   9]---> Adder-cost: 110   maxlim: 4607   bits: 14/13
c ---[   8]---> Adder-cost: 92   maxlim: 1279   bits: 12/11
c ---[   7]---> Adder-cost: 124   maxlim: 9087   bits: 15/14
c ---[   6]---> Adder-cost: 102   maxlim: 3327   bits: 13/12
c ---[   5]---> Adder-cost: 112   maxlim: 4351   bits: 14/13
c ---[   4]---> Adder-cost: 86   maxlim: 2047   bits: 12/11
c ---[   3]---> Adder-cost: 104   maxlim: 3455   bits: 13/12
c ---[   2]---> Adder-cost: 94   maxlim: 1151   bits: 12/11
c ---[   1]---> Adder-cost: 122   maxlim: 8447   bits: 15/14
c ---[   0]---> Adder-cost: 100   maxlim: 3583   bits: 13/12
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  176871   635589 |   58957       0        0     nan |  0.000 % |
c |       100 |  176871   635589 |   64852     100      465     4.7 | 15.209 % |
c |       250 |  176871   635589 |   71337     250     1029     4.1 | 15.209 % |
c |       476 |  176863   635563 |   78471     475     1978     4.2 | 15.211 % |
c |       814 |  176846   635508 |   86318     811     3923     4.8 | 15.219 % |
c |      1320 |  176803   635369 |   94950    1312     6339     4.8 | 15.239 % |
c |      2080 |  176762   635236 |  104445    2067    10315     5.0 | 15.254 % |
c |      3219 |  176713   635077 |  114890    3200    16410     5.1 | 15.272 % |
c |      4930 |  176649   634869 |  126379    4903    38319     7.8 | 15.292 % |
c |      7492 |  176585   634658 |  139017    7457    54892     7.4 | 15.312 % |
c |     11336 |  176497   634367 |  152919   11285    82187     7.3 | 15.338 % |
c |     17102 |  176391   634019 |  168211   17017   123051     7.2 | 15.371 % |
c |     25751 |  176297   633713 |  185032   25647   350043    13.6 | 15.401 % |
c |     38726 |  176281   633661 |  203535   38620   962057    24.9 | 15.406 % |
c |     58191 |  176195   633383 |  223889   58066  1412628    24.3 | 15.436 % |
c |     87383 |  175993   632702 |  246278   87226  2010274    23.0 | 15.492 % |
c |    131172 |  175888   632337 |  270905  130906  5212455    39.8 | 15.522 % |
c |    196856 |  175842   632187 |  297996  196572  8844740    45.0 | 15.538 % |
c |    295383 |  175674   631622 |  327796  295051 13097987    44.4 | 15.591 % |
c |    443172 |  175621   631443 |  360575  130471  6023894    46.2 | 15.606 % |
#### 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.73 0.91 0.89 2/54 12911
Raw data (stat): 12911 (runsolver) R 12910 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 489140217 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10 s]
Raw data (loadavg): 0.77 0.91 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 4689 0 0 0 986 12 0 0 25 0 1 0 489140217 21725184 4453 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5304 4453 603 41 0 5263 0
vsize: 21216
[startup+20.0008 s]
Raw data (loadavg): 0.81 0.91 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 4844 0 0 0 1985 13 0 0 25 0 1 0 489140217 22503424 4608 4294967295 134512640 134672761 3221224544 3221223668 134566043 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5494 4608 603 41 0 5453 0
vsize: 21976
[startup+30.0015 s]
Raw data (loadavg): 0.84 0.92 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 5223 0 0 0 2983 15 0 0 25 0 1 0 489140217 23973888 4987 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5853 4987 603 41 0 5812 0
vsize: 23412
[startup+40.002 s]
Raw data (loadavg): 0.86 0.92 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 5949 0 0 0 3982 16 0 0 25 0 1 0 489140217 27058176 5713 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6606 5713 603 41 0 6565 0
vsize: 26424
[startup+50.0033 s]
Raw data (loadavg): 0.88 0.92 0.89 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 6221 0 0 0 4980 17 0 0 25 0 1 0 489140217 28135424 5985 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6869 5985 603 41 0 6828 0
vsize: 27476
[startup+60.0028 s]
Raw data (loadavg): 0.90 0.92 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 6604 0 0 0 5979 19 0 0 25 0 1 0 489140217 29614080 6368 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7230 6368 603 41 0 7189 0
vsize: 28920
[startup+70.0039 s]
Raw data (loadavg): 0.92 0.92 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 6708 0 0 0 6979 19 0 0 25 0 1 0 489140217 30015488 6472 4294967295 134512640 134672761 3221224544 3221223712 134560988 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7328 6472 603 41 0 7287 0
vsize: 29312
[startup+80.0048 s]
Raw data (loadavg): 0.93 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 6919 0 0 0 7978 20 0 0 25 0 1 0 489140217 31223808 6683 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7623 6683 603 41 0 7582 0
vsize: 30492
[startup+90.0042 s]
Raw data (loadavg): 0.94 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 7199 0 0 0 8978 20 0 0 25 0 1 0 489140217 32296960 6963 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7885 6963 603 41 0 7844 0
vsize: 31540
[startup+100.005 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 8096 0 0 0 9975 23 0 0 25 0 1 0 489140217 35921920 7860 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8770 7860 603 41 0 8729 0
vsize: 35080
[startup+110.005 s]
Raw data (loadavg): 0.95 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 8970 0 0 0 10973 26 0 0 25 0 1 0 489140217 39440384 8734 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9629 8734 603 41 0 9588 0
vsize: 38516
[startup+120.006 s]
Raw data (loadavg): 0.96 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 9693 0 0 0 11971 27 0 0 25 0 1 0 489140217 42422272 9457 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10357 9457 603 41 0 10316 0
vsize: 41428
[startup+130.006 s]
Raw data (loadavg): 0.97 0.93 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 10225 0 0 0 12969 30 0 0 25 0 1 0 489140217 44601344 9989 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10889 9989 603 41 0 10848 0
vsize: 43556
[startup+140.005 s]
Raw data (loadavg): 0.97 0.94 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 10716 0 0 0 13968 31 0 0 25 0 1 0 489140217 46637056 10480 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11386 10480 603 41 0 11345 0
vsize: 45544
[startup+150.006 s]
Raw data (loadavg): 0.98 0.94 0.90 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 11038 0 0 0 14967 33 0 0 25 0 1 0 489140217 47968256 10802 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11711 10802 603 41 0 11670 0
vsize: 46844
[startup+160.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 11550 0 0 0 15965 34 0 0 25 0 1 0 489140217 50503680 11314 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12330 11314 603 41 0 12289 0
vsize: 49320
[startup+170.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 12075 0 0 0 16964 36 0 0 25 0 1 0 489140217 52666368 11839 4294967295 134512640 134672761 3221224544 3221223544 1075350746 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12858 11839 603 41 0 12817 0
vsize: 51432
[startup+180.007 s]
Raw data (loadavg): 0.98 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 12561 0 0 0 17963 37 0 0 25 0 1 0 489140217 54669312 12325 4294967295 134512640 134672761 3221224544 3221223680 134560577 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13347 12325 603 41 0 13306 0
vsize: 53388
[startup+190.007 s]
Raw data (loadavg): 0.99 0.94 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 12972 0 0 0 18962 38 0 0 25 0 1 0 489140217 56274944 12736 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13739 12736 603 41 0 13698 0
vsize: 54956
[startup+200.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 13321 0 0 0 19961 39 0 0 25 0 1 0 489140217 57761792 13085 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14102 13085 603 41 0 14061 0
vsize: 56408
[startup+210.007 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 13672 0 0 0 20959 41 0 0 25 0 1 0 489140217 59084800 13436 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14425 13436 603 41 0 14384 0
vsize: 57700
[startup+220.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 14084 0 0 0 21959 42 0 0 25 0 1 0 489140217 60862464 13848 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14859 13848 603 41 0 14818 0
vsize: 59436
[startup+230.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 14374 0 0 0 22958 43 0 0 25 0 1 0 489140217 61952000 14138 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15125 14138 603 41 0 15084 0
vsize: 60500
[startup+240.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 14710 0 0 0 23957 44 0 0 25 0 1 0 489140217 63291392 14474 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15452 14474 603 41 0 15411 0
vsize: 61808
[startup+250.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 15004 0 0 0 24956 45 0 0 25 0 1 0 489140217 64503808 14768 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15748 14768 603 41 0 15707 0
vsize: 62992
[startup+260.009 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 15271 0 0 0 25956 46 0 0 25 0 1 0 489140217 65581056 15035 4294967295 134512640 134672761 3221224544 3221223712 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16011 15035 603 41 0 15970 0
vsize: 64044
[startup+270.01 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 15520 0 0 0 26955 47 0 0 25 0 1 0 489140217 66662400 15284 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16275 15284 603 41 0 16234 0
vsize: 65100
[startup+280.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 15675 0 0 0 27954 47 0 0 25 0 1 0 489140217 67203072 15439 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16407 15439 603 41 0 16366 0
vsize: 65628
[startup+290.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 15916 0 0 0 28952 48 0 0 25 0 1 0 489140217 68276224 15680 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16669 15680 603 41 0 16628 0
vsize: 66676
[startup+300.011 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 16128 0 0 0 29952 49 0 0 25 0 1 0 489140217 69099520 15892 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16870 15892 603 41 0 16829 0
vsize: 67480
[startup+310.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 16239 0 0 0 30952 49 0 0 25 0 1 0 489140217 69636096 16003 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17001 16003 603 41 0 16960 0
vsize: 68004
[startup+320.011 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 16408 0 0 0 31951 50 0 0 25 0 1 0 489140217 70307840 16172 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17165 16172 603 41 0 17124 0
vsize: 68660
[startup+330.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 16607 0 0 0 32951 51 0 0 25 0 1 0 489140217 71110656 16371 4294967295 134512640 134672761 3221224544 3221223648 134560059 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17361 16371 603 41 0 17320 0
vsize: 69444
[startup+340.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 16835 0 0 0 33950 51 0 0 25 0 1 0 489140217 72052736 16599 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17591 16599 603 41 0 17550 0
vsize: 70364
[startup+350.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 17005 0 0 0 34950 52 0 0 25 0 1 0 489140217 72728576 16769 4294967295 134512640 134672761 3221224544 3221223712 134560917 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17756 16769 603 41 0 17715 0
vsize: 71024
[startup+360.012 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 17137 0 0 0 35950 52 0 0 25 0 1 0 489140217 73269248 16901 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17888 16901 603 41 0 17847 0
vsize: 71552
[startup+370.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 17567 0 0 0 36949 54 0 0 25 0 1 0 489140217 74997760 17331 4294967295 134512640 134672761 3221224544 3221223712 134560822 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18310 17331 603 41 0 18269 0
vsize: 73240
[startup+380.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 18392 0 0 0 37946 57 0 0 25 0 1 0 489140217 78233600 18156 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19100 18156 603 41 0 19059 0
vsize: 76400
[startup+390.013 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 18885 0 0 0 38945 58 0 0 25 0 1 0 489140217 81297408 18649 4294967295 134512640 134672761 3221224544 3221223728 134559161 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19848 18649 603 41 0 19807 0
vsize: 79392
[startup+400.014 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 19119 0 0 0 39944 59 0 0 25 0 1 0 489140217 82280448 18883 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20088 18883 603 41 0 20047 0
vsize: 80352
[startup+410.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 19304 0 0 0 40944 59 0 0 25 0 1 0 489140217 83091456 19068 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20286 19068 603 41 0 20245 0
vsize: 81144
[startup+420.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 19546 0 0 0 41943 60 0 0 25 0 1 0 489140217 84025344 19310 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20514 19310 603 41 0 20473 0
vsize: 82056
[startup+430.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 19911 0 0 0 42942 62 0 0 25 0 1 0 489140217 85508096 19675 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20876 19675 603 41 0 20835 0
vsize: 83504
[startup+440.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 20386 0 0 0 43940 64 0 0 25 0 1 0 489140217 87527424 20150 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21369 20150 603 41 0 21328 0
vsize: 85476
[startup+450.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 20526 0 0 0 44940 64 0 0 25 0 1 0 489140217 88068096 20290 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21501 20290 603 41 0 21460 0
vsize: 86004
[startup+460.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 20854 0 0 0 45939 65 0 0 25 0 1 0 489140217 89272320 20618 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21795 20618 603 41 0 21754 0
vsize: 87180
[startup+470.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 21035 0 0 0 46938 66 0 0 25 0 1 0 489140217 90079232 20799 4294967295 134512640 134672761 3221224544 3221223712 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21992 20799 603 41 0 21951 0
vsize: 87968
[startup+480.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 21330 0 0 0 47937 67 0 0 25 0 1 0 489140217 91283456 21094 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22286 21094 603 41 0 22245 0
vsize: 89144
[startup+490.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 21586 0 0 0 48936 68 0 0 25 0 1 0 489140217 92217344 21350 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22514 21350 603 41 0 22473 0
vsize: 90056
[startup+500.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 21899 0 0 0 49935 69 0 0 25 0 1 0 489140217 93569024 21663 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22844 21663 603 41 0 22803 0
vsize: 91376
[startup+510.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 22160 0 0 0 50935 70 0 0 25 0 1 0 489140217 94654464 21924 4294967295 134512640 134672761 3221224544 3221223712 134560926 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23109 21924 603 41 0 23068 0
vsize: 92436
[startup+520.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 22301 0 0 0 51934 70 0 0 25 0 1 0 489140217 95195136 22065 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23241 22065 603 41 0 23200 0
vsize: 92964
[startup+530.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 22419 0 0 0 52934 70 0 0 25 0 1 0 489140217 95596544 22183 4294967295 134512640 134672761 3221224544 3221223668 134566037 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23339 22183 603 41 0 23298 0
vsize: 93356
[startup+540.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 22729 0 0 0 53934 71 0 0 25 0 1 0 489140217 96948224 22493 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23669 22493 603 41 0 23628 0
vsize: 94676
[startup+550.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23006 0 0 0 54933 72 0 0 25 0 1 0 489140217 98017280 22770 4294967295 134512640 134672761 3221224544 3221223648 134560355 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23930 22770 603 41 0 23889 0
vsize: 95720
[startup+560.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23259 0 0 0 55932 73 0 0 25 0 1 0 489140217 99086336 23023 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24191 23023 603 41 0 24150 0
vsize: 96764
[startup+570.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 56932 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+580.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 57932 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+590.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 58933 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223728 134558899 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+600.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 59933 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223728 134559345 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+610.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 60933 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+620.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 61933 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+630.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 62934 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+640.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 63934 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+650.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12911
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23322 0 0 0 64934 73 0 0 25 0 1 0 489140217 99221504 23086 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23086 603 41 0 24183 0
vsize: 96896
[startup+660.022 s]
Raw data (loadavg): 0.99 0.97 0.91 3/56 12933
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 65934 73 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+670.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 66933 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+680.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 67933 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 68934 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+700.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 69934 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+710.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 70934 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+720.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 71934 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223648 134560410 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+730.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12964
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 72934 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+740.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 73934 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+750.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 74934 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223648 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+760.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 75934 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+770.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 76935 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561226 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+780.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 77935 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+790.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 78935 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+800.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 79935 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+810.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 80936 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+820.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 81936 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+830.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 82936 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 83936 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+850.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 84936 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+860.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 85937 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 86937 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 87937 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 88937 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+900.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 89937 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 90937 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 91938 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+930.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 92938 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+940.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 93938 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223680 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+950.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 94938 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+960.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 95938 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+970.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 96939 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+980.034 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 97939 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 98939 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1000.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 99940 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1010.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12966
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 100940 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1020.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 101940 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1030.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 102940 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1040.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23323 0 0 0 103941 74 0 0 25 0 1 0 489140217 99221504 23087 4294967295 134512640 134672761 3221224544 3221223680 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23087 603 41 0 24183 0
vsize: 96896
[startup+1050.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23325 0 0 0 104941 74 0 0 25 0 1 0 489140217 99221504 23089 4294967295 134512640 134672761 3221224544 3221223728 134558937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24224 23089 603 41 0 24183 0
vsize: 96896
[startup+1060.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23580 0 0 0 105940 75 0 0 25 0 1 0 489140217 100327424 23344 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24494 23344 603 41 0 24453 0
vsize: 97976
[startup+1070.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 23809 0 0 0 106940 76 0 0 25 0 1 0 489140217 101314560 23573 4294967295 134512640 134672761 3221224544 3221223704 134561029 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24735 23573 603 41 0 24694 0
vsize: 98940
[startup+1080.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 24050 0 0 0 107940 76 0 0 25 0 1 0 489140217 102252544 23814 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24964 23814 603 41 0 24923 0
vsize: 99856
[startup+1090.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 24294 0 0 0 108939 77 0 0 25 0 1 0 489140217 103321600 24058 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25225 24058 603 41 0 25184 0
vsize: 100900
[startup+1100.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 24547 0 0 0 109939 78 0 0 25 0 1 0 489140217 104411136 24311 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25491 24311 603 41 0 25450 0
vsize: 101964
[startup+1110.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 24791 0 0 0 110939 78 0 0 25 0 1 0 489140217 105394176 24555 4294967295 134512640 134672761 3221224544 3221223712 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25731 24555 603 41 0 25690 0
vsize: 102924
[startup+1120.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 25026 0 0 0 111937 79 0 0 25 0 1 0 489140217 106323968 24790 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25958 24790 603 41 0 25917 0
vsize: 103832
[startup+1130.05 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 25248 0 0 0 112937 80 0 0 25 0 1 0 489140217 107290624 25012 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26194 25012 603 41 0 26153 0
vsize: 104776
[startup+1140.05 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 25457 0 0 0 113936 81 0 0 25 0 1 0 489140217 108085248 25221 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26388 25221 603 41 0 26347 0
vsize: 105552
[startup+1150.05 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 25652 0 0 0 114936 81 0 0 25 0 1 0 489140217 108896256 25416 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26586 25416 603 41 0 26545 0
vsize: 106344
[startup+1160.05 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 25852 0 0 0 115936 82 0 0 25 0 1 0 489140217 109694976 25616 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26781 25616 603 41 0 26740 0
vsize: 107124
[startup+1170.05 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 26048 0 0 0 116935 82 0 0 25 0 1 0 489140217 110505984 25812 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26979 25812 603 41 0 26938 0
vsize: 107916
[startup+1180.05 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 26247 0 0 0 117935 83 0 0 25 0 1 0 489140217 111366144 26011 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27189 26011 603 41 0 27148 0
vsize: 108756
[startup+1190.05 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 26477 0 0 0 118935 83 0 0 25 0 1 0 489140217 112431104 26241 4294967295 134512640 134672761 3221224544 3221223712 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27449 26241 603 41 0 27408 0
vsize: 109796
[startup+1200.05 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 12968
Raw data (stat): 12911 (minisat+) R 12910 29151 29150 0 -1 0 26675 0 0 0 119934 84 0 0 25 0 1 0 489140217 113246208 26439 4294967295 134512640 134672761 3221224544 3221223712 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27648 26439 603 41 0 27607 0
vsize: 110592
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.23 s]
Raw data (loadavg): 1.02 0.99 0.91 1/54 12968
Raw data (stat): 12911 (minisat+) Z 12910 29151 29150 0 -1 12 26679 0 0 0 119945 89 0 0 23 0 1 0 489140217 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.23
CPU time (s): 1200.35
CPU user time (s): 1199.46
CPU system time (s): 0.895863
CPU usage (%): 100.01
Max. virtual memory (Kb): 110592
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####