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/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1-11,19,21.opb
MD5SUM	552cc7fcebca47ae66a3cb1c13679513
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	10
Number of bits of the biggest number in a constraint	4
Biggest sum of numbers in a constraint	103
Number of bits of the biggest sum of numbers	7
Best result obtained on this benchmark
Best CPU time to get the best result obtained on this benchmark
Number of variables	4602
Total number of constraints	34781
Number of constraints which are clauses	29160
Number of constraints which are cardinality constraints (but not clauses)	5543
Number of constraints which are nor clauses,nor cardinality constraints	78
Minimum length of a constraint	1
Maximum length of a constraint	29
Trace number 5078

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc31 THE 2005-04-13 21:53:14 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3227 boxname=wulflinc31 idbench=359 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  552cc7fcebca47ae66a3cb1c13679513  /oldhome/oroussel/tmp/wulflinc31/normalized-ppp:1-11,19,21.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc31/normalized-ppp:1-11,19,21.opb
IDLAUNCH: 3227
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.153
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        908672 kB
Buffers:         34628 kB
Cached:          52564 kB
SwapCached:        392 kB
Active:          47692 kB
Inactive:        42748 kB
HighTotal:      131008 kB
HighFree:        74676 kB
LowTotal:       903652 kB
LowFree:        833996 kB
SwapTotal:     2097892 kB
SwapFree:      2097452 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6832 kB
Slab:            30024 kB
Committed_AS:    63488 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:13:16 (client local time) WITH STATUS 0 IN 1200.22 SECONDS
stats: 3227 7 1200.22 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30353 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30352]---> BDD-cost:   56
c ---[30351]---> BDD-cost:   56
c ---[30350]---> BDD-cost:   56
c ---[30349]---> BDD-cost:   56
c ---[30348]---> BDD-cost:   56
c ---[30347]---> BDD-cost:   56
c ---[30346]---> BDD-cost:   56
c ---[30345]---> BDD-cost:   56
c ---[30344]---> BDD-cost:   56
c ---[30343]---> BDD-cost:   56
c ---[30342]---> BDD-cost:   56
c ---[30341]---> BDD-cost:   56
c ---[30340]---> BDD-cost:  123
c ---[30339]---> BDD-cost:  123
c ---[30338]---> BDD-cost:  123
c ---[30337]---> BDD-cost:  123
c ---[30336]---> BDD-cost:  123
c ---[30335]---> BDD-cost:  123
c ---[30334]---> BDD-cost:  123
c ---[30333]---> BDD-cost:  123
c ---[30332]---> BDD-cost:  123
c ---[30331]---> BDD-cost:  123
c ---[30330]---> BDD-cost:  123
c ---[30329]---> BDD-cost:  123
c ---[30328]---> BDD-cost:  123
c ---[30327]---> BDD-cost:  123
c ---[30326]---> BDD-cost:  123
c ---[30325]---> BDD-cost:  123
c ---[30324]---> BDD-cost:  123
c ---[30323]---> BDD-cost:  123
c ---[30322]---> BDD-cost:  133
c ---[30321]---> BDD-cost:  133
c ---[30320]---> BDD-cost:  133
c ---[30319]---> BDD-cost:  133
c ---[30318]---> BDD-cost:  133
c ---[30317]---> BDD-cost:  133
c ---[30316]---> BDD-cost:  123
c ---[30315]---> BDD-cost:  123
c ---[30314]---> BDD-cost:  123
c ---[30313]---> BDD-cost:  123
c ---[30312]---> BDD-cost:  123
c ---[30311]---> BDD-cost:  123
c ---[30310]---> BDD-cost:  123
c ---[30309]---> BDD-cost:  123
c ---[30308]---> BDD-cost:  123
c ---[30307]---> BDD-cost:  123
c ---[30306]---> BDD-cost:  123
c ---[30305]---> BDD-cost:  123
c ---[30304]---> BDD-cost:  123
c ---[30303]---> BDD-cost:  123
c ---[30302]---> BDD-cost:  123
c ---[30301]---> BDD-cost:  123
c ---[30300]---> BDD-cost:  123
c ---[30299]---> BDD-cost:  123
c ---[30298]---> Sorter-cost:  550     Base: 2 2
c ---[30297]---> Sorter-cost:  550     Base: 2 2
c ---[30296]---> Sorter-cost:  550     Base: 2 2
c ---[30295]---> Sorter-cost:  550     Base: 2 2
c ---[30294]---> Sorter-cost:  550     Base: 2 2
c ---[30293]---> Sorter-cost:  550     Base: 2 2
c ---[30292]---> Sorter-cost:  550     Base: 2 2
c ---[30291]---> Sorter-cost:  550     Base: 2 2
c ---[30290]---> Sorter-cost:  550     Base: 2 2
c ---[30289]---> Sorter-cost:  550     Base: 2 2
c ---[30288]---> Sorter-cost:  550     Base: 2 2
c ---[30287]---> Sorter-cost:  550     Base: 2 2
c ---[30286]---> BDD-cost:   86
c ---[30285]---> BDD-cost:   86
c ---[30284]---> BDD-cost:   86
c ---[30283]---> BDD-cost:   86
c ---[30282]---> BDD-cost:   86
c ---[30281]---> BDD-cost:   86
c ---[30280]---> BDD-cost:   56
c ---[30279]---> BDD-cost:   56
c ---[30278]---> BDD-cost:   56
c ---[30277]---> BDD-cost:   56
c ---[30276]---> BDD-cost:   56
c ---[30275]---> BDD-cost:   56
c ---[30273]---> BDD-cost:   23
c ---[30271]---> BDD-cost:   23
c ---[30269]---> BDD-cost:   23
c ---[30267]---> BDD-cost:   23
c ---[30265]---> BDD-cost:   23
c ---[30263]---> BDD-cost:   23
c ---[30261]---> BDD-cost:   23
c ---[30259]---> BDD-cost:   23
c ---[30257]---> BDD-cost:   23
c ---[30255]---> BDD-cost:   23
c ---[30253]---> BDD-cost:   23
c ---[30251]---> BDD-cost:   23
c ---[30249]---> BDD-cost:   23
c ---[30247]---> BDD-cost:   23
c ---[30245]---> BDD-cost:   23
c ---[30243]---> BDD-cost:   23
c ---[30241]---> BDD-cost:   23
c ---[30239]---> BDD-cost:   23
c ---[30237]---> BDD-cost:   17
c ---[30235]---> BDD-cost:   17
c ---[30233]---> BDD-cost:   17
c ---[30231]---> BDD-cost:   17
c ---[30229]---> BDD-cost:   17
c ---[30227]---> BDD-cost:   17
c ---[30225]---> BDD-cost:   23
c ---[30223]---> BDD-cost:   23
c ---[30221]---> BDD-cost:   23
c ---[30219]---> BDD-cost:   23
c ---[30217]---> BDD-cost:   23
c ---[30215]---> BDD-cost:   23
c ---[30213]---> BDD-cost:   23
c ---[30211]---> BDD-cost:   23
c ---[30209]---> BDD-cost:   23
c ---[30207]---> BDD-cost:   23
c ---[30205]---> BDD-cost:   23
c ---[30203]---> BDD-cost:   23
c ---[30201]---> BDD-cost:   17
c ---[30199]---> BDD-cost:   17
c ---[30197]---> BDD-cost:   17
c ---[30195]---> BDD-cost:   17
c ---[30193]---> BDD-cost:   17
c ---[30191]---> BDD-cost:   17
c ---[30189]---> BDD-cost:   15
c ---[30187]---> BDD-cost:   15
c ---[30185]---> BDD-cost:   15
c ---[30183]---> BDD-cost:   15
c ---[30181]---> BDD-cost:   15
c ---[30179]---> BDD-cost:   15
c ---[30177]---> BDD-cost:   23
c ---[30175]---> BDD-cost:   23
c ---[30173]---> BDD-cost:   23
c ---[30171]---> BDD-cost:   23
c ---[30169]---> BDD-cost:   23
c ---[30167]---> BDD-cost:   23
c ---[30165]---> BDD-cost:   23
c ---[30163]---> BDD-cost:   23
c ---[30161]---> BDD-cost:   23
c ---[30159]---> BDD-cost:   23
c ---[30157]---> BDD-cost:   23
c ---[30155]---> BDD-cost:   23
c ---[30153]---> BDD-cost:   23
c ---[30151]---> BDD-cost:   23
c ---[30149]---> BDD-cost:   23
c ---[30147]---> BDD-cost:   23
c ---[30145]---> BDD-cost:   23
c ---[30143]---> BDD-cost:   23
c ---[30141]---> BDD-cost:   23
c ---[30139]---> BDD-cost:   23
c ---[30137]---> BDD-cost:   23
c ---[30135]---> BDD-cost:   23
c ---[30133]---> BDD-cost:   23
c ---[30131]---> BDD-cost:   23
c ---[30129]---> BDD-cost:   23
c ---[30127]---> BDD-cost:   23
c ---[30125]---> BDD-cost:   23
c ---[30123]---> BDD-cost:   23
c ---[30121]---> BDD-cost:   23
c ---[30119]---> BDD-cost:   23
c ---[30117]---> BDD-cost:   23
c ---[30115]---> BDD-cost:   23
c ---[30113]---> BDD-cost:   23
c ---[30111]---> BDD-cost:   23
c ---[30109]---> BDD-cost:   23
c ---[30107]---> BDD-cost:   23
c ---[30105]---> BDD-cost:   23
c ---[30103]---> BDD-cost:   23
c ---[30101]---> BDD-cost:   23
c ---[30099]---> BDD-cost:   23
c ---[30097]---> BDD-cost:   23
c ---[30095]---> BDD-cost:   23
c ---[30093]---> BDD-cost:   23
c ---[30091]---> BDD-cost:   23
c ---[30089]---> BDD-cost:   23
c ---[30087]---> BDD-cost:   23
c ---[30085]---> BDD-cost:   23
c ---[30083]---> BDD-cost:   23
c ---[30081]---> BDD-cost:   23
c ---[30079]---> BDD-cost:   23
c ---[30077]---> BDD-cost:   23
c ---[30075]---> BDD-cost:   23
c ---[30073]---> BDD-cost:   23
c ---[30071]---> BDD-cost:   23
c ---[30069]---> BDD-cost:   23
c ---[30067]---> BDD-cost:   23
c ---[30065]---> BDD-cost:   23
c ---[30063]---> BDD-cost:   23
c ---[30061]---> BDD-cost:   23
c ---[30059]---> BDD-cost:   23
c ---[30057]---> BDD-cost:   17
c ---[30055]---> BDD-cost:   17
c ---[30053]---> BDD-cost:   17
c ---[30051]---> BDD-cost:   17
c ---[30049]---> BDD-cost:   17
c ---[30047]---> BDD-cost:   17
c ---[30045]---> BDD-cost:   23
c ---[30043]---> BDD-cost:   23
c ---[30041]---> BDD-cost:   23
c ---[30039]---> BDD-cost:   23
c ---[30037]---> BDD-cost:   23
c ---[30035]---> BDD-cost:   23
c ---[30033]---> BDD-cost:   23
c ---[30031]---> BDD-cost:   23
c ---[30029]---> BDD-cost:   23
c ---[30027]---> BDD-cost:   23
c ---[30025]---> BDD-cost:   23
c ---[30023]---> BDD-cost:   23
c ---[30021]---> BDD-cost:   23
c ---[30019]---> BDD-cost:   23
c ---[30017]---> BDD-cost:   23
c ---[30015]---> BDD-cost:   23
c ---[30013]---> BDD-cost:   23
c ---[30011]---> BDD-cost:   23
c ---[30009]---> BDD-cost:   23
c ---[30007]---> BDD-cost:   23
c ---[30005]---> BDD-cost:   23
c ---[30003]---> BDD-cost:   23
c ---[30001]---> BDD-cost:   23
c ---[29999]---> BDD-cost:   23
c ---[29997]---> BDD-cost:   23
c ---[29995]---> BDD-cost:   23
c ---[29993]---> BDD-cost:   23
c ---[29991]---> BDD-cost:   23
c ---[29989]---> BDD-cost:   23
c ---[29987]---> BDD-cost:   23
c ---[29985]---> BDD-cost:   17
c ---[29983]---> BDD-cost:   17
c ---[29981]---> BDD-cost:   17
c ---[29979]---> BDD-cost:   17
c ---[29977]---> BDD-cost:   17
c ---[29975]---> BDD-cost:   17
c ---[29973]---> BDD-cost:   23
c ---[29971]---> BDD-cost:   23
c ---[29969]---> BDD-cost:   23
c ---[29967]---> BDD-cost:   23
c ---[29965]---> BDD-cost:   23
c ---[29963]---> BDD-cost:   23
c ---[29961]---> BDD-cost:   23
c ---[29959]---> BDD-cost:   23
c ---[29957]---> BDD-cost:   23
c ---[29955]---> BDD-cost:   23
c ---[29953]---> BDD-cost:   23
c ---[29951]---> BDD-cost:   23
c ---[29949]---> BDD-cost:   23
c ---[29947]---> BDD-cost:   23
c ---[29945]---> BDD-cost:   23
c ---[29943]---> BDD-cost:   23
c ---[29941]---> BDD-cost:   23
c ---[29939]---> BDD-cost:   23
c ---[29937]---> BDD-cost:   23
c ---[29935]---> BDD-cost:   23
c ---[29933]---> BDD-cost:   23
c ---[29931]---> BDD-cost:   23
c ---[29929]---> BDD-cost:   23
c ---[29927]---> BDD-cost:   23
c ---[29926]---> BDD-cost:    9
c ---[29925]---> BDD-cost:    9
c ---[29924]---> BDD-cost:    9
c ---[29923]---> BDD-cost:    9
c ---[29922]---> BDD-cost:    9
c ---[29921]---> BDD-cost:    9
c ---[29920]---> BDD-cost:    9
c ---[29919]---> BDD-cost:    9
c ---[29918]---> BDD-cost:    9
c ---[29917]---> BDD-cost:    9
c ---[29916]---> BDD-cost:    9
c ---[29915]---> BDD-cost:    9
c ---[29914]---> BDD-cost:    9
c ---[29913]---> BDD-cost:    9
c ---[29912]---> BDD-cost:    9
c ---[29911]---> BDD-cost:    9
c ---[29910]---> BDD-cost:    9
c ---[29909]---> BDD-cost:    9
c ---[29908]---> BDD-cost:    9
c ---[29907]---> BDD-cost:    9
c ---[29906]---> BDD-cost:    9
c ---[29905]---> BDD-cost:    9
c ---[29904]---> BDD-cost:    9
c ---[29903]---> BDD-cost:    9
c ---[29902]---> BDD-cost:    9
c ---[29901]---> BDD-cost:    9
c ---[29900]---> BDD-cost:    9
c ---[29899]---> BDD-cost:    9
c ---[29898]---> BDD-cost:    9
c ---[29897]---> BDD-cost:    9
c ---[29896]---> BDD-cost:    9
c ---[29895]---> BDD-cost:    9
c ---[29894]---> BDD-cost:    9
c ---[29893]---> BDD-cost:    9
c ---[29892]---> BDD-cost:    9
c ---[29891]---> BDD-cost:    9
c ---[29890]---> BDD-cost:    9
c ---[29889]---> BDD-cost:    9
c ---[29888]---> BDD-cost:    9
c ---[29887]---> BDD-cost:    9
c ---[29886]---> BDD-cost:    9
c ---[29885]---> BDD-cost:    9
c ---[29884]---> BDD-cost:    9
c ---[29883]---> BDD-cost:    9
c ---[29882]---> BDD-cost:    9
c ---[29881]---> BDD-cost:    9
c ---[29880]---> BDD-cost:    9
c ---[29879]---> BDD-cost:    9
c ---[29878]---> BDD-cost:    9
c ---[29877]---> BDD-cost:    9
c ---[29876]---> BDD-cost:    9
c ---[29875]---> BDD-cost:    9
c ---[29874]---> BDD-cost:    9
c ---[29873]---> BDD-cost:    9
c ---[29872]---> BDD-cost:    9
c ---[29871]---> BDD-cost:    9
c ---[29870]---> BDD-cost:    9
c ---[29869]---> BDD-cost:    9
c ---[29868]---> BDD-cost:    9
c ---[29867]---> BDD-cost:    9
c ---[29866]---> BDD-cost:    9
c ---[29865]---> BDD-cost:    9
c ---[29864]---> BDD-cost:    9
c ---[29863]---> BDD-cost:    9
c ---[29862]---> BDD-cost:    9
c ---[29861]---> BDD-cost:    9
c ---[29860]---> BDD-cost:    9
c ---[29859]---> BDD-cost:    9
c ---[29858]---> BDD-cost:    9
c ---[29857]---> BDD-cost:    9
c ---[29856]---> BDD-cost:    9
c ---[29855]---> BDD-cost:    9
c ---[29854]---> BDD-cost:    9
c ---[29853]---> BDD-cost:    9
c ---[29852]---> BDD-cost:    9
c ---[29851]---> BDD-cost:    9
c ---[29850]---> BDD-cost:    9
c ---[29849]---> BDD-cost:    9
c ---[29848]---> BDD-cost:    9
c ---[29847]---> BDD-cost:    9
c ---[29846]---> BDD-cost:    9
c ---[29845]---> BDD-cost:    9
c ---[29844]---> BDD-cost:    9
c ---[29843]---> BDD-cost:    9
c ---[29842]---> BDD-cost:    9
c ---[29841]---> BDD-cost:    9
c ---[29840]---> BDD-cost:    9
c ---[29839]---> BDD-cost:    9
c ---[29838]---> BDD-cost:    9
c ---[29837]---> BDD-cost:    9
c ---[29836]---> BDD-cost:    9
c ---[29835]---> BDD-cost:    9
c ---[29834]---> BDD-cost:    9
c ---[29833]---> BDD-cost:    9
c ---[29832]---> BDD-cost:    9
c ---[29831]---> BDD-cost:    9
c ---[29830]---> BDD-cost:    9
c ---[29829]---> BDD-cost:    9
c ---[29828]---> BDD-cost:    9
c ---[29827]---> BDD-cost:    9
c ---[29826]---> BDD-cost:    9
c ---[29825]---> BDD-cost:    9
c ---[29824]---> BDD-cost:    9
c ---[29823]---> BDD-cost:    9
c ---[29822]---> BDD-cost:    9
c ---[29821]---> BDD-cost:    9
c ---[29820]---> BDD-cost:    9
c ---[29819]---> BDD-cost:    9
c ---[29818]---> BDD-cost:    9
c ---[29817]---> BDD-cost:    9
c ---[29816]---> BDD-cost:    9
c ---[29815]---> BDD-cost:    9
c ---[29814]---> BDD-cost:    9
c ---[29813]---> BDD-cost:    9
c ---[29812]---> BDD-cost:    9
c ---[29811]---> BDD-cost:    9
c ---[29810]---> BDD-cost:    9
c ---[29809]---> BDD-cost:    9
c ---[29808]---> BDD-cost:    9
c ---[29807]---> BDD-cost:    9
c ---[29806]---> BDD-cost:    9
c ---[29805]---> BDD-cost:    9
c ---[29804]---> BDD-cost:    9
c ---[29803]---> BDD-cost:    9
c ---[29802]---> BDD-cost:    9
c ---[29801]---> BDD-cost:    9
c ---[29800]---> BDD-cost:    9
c ---[29799]---> BDD-cost:    9
c ---[29798]---> BDD-cost:    9
c ---[29797]---> BDD-cost:    9
c ---[29796]---> BDD-cost:    9
c ---[29795]---> BDD-cost:    9
c ---[29794]---> BDD-cost:    9
c ---[29793]---> BDD-cost:    9
c ---[29792]---> BDD-cost:    9
c ---[29791]---> BDD-cost:    9
c ---[29790]---> BDD-cost:    9
c ---[29789]---> BDD-cost:    9
c ---[29788]---> BDD-cost:    9
c ---[29787]---> BDD-cost:    9
c ---[29786]---> BDD-cost:    9
c ---[29785]---> BDD-cost:    9
c ---[29784]---> BDD-cost:    9
c ---[29783]---> BDD-cost:    9
c ---[29782]---> BDD-cost:    9
c ---[29781]---> BDD-cost:    9
c ---[29780]---> BDD-cost:    9
c ---[29779]---> BDD-cost:    9
c ---[29778]---> BDD-cost:    9
c ---[29777]---> BDD-cost:    9
c ---[29776]---> BDD-cost:    9
c ---[29775]---> BDD-cost:    9
c ---[29774]---> BDD-cost:    9
c ---[29773]---> BDD-cost:    9
c ---[29772]---> BDD-cost:    9
c ---[29771]---> BDD-cost:    9
c ---[29770]---> BDD-cost:    9
c ---[29769]---> BDD-cost:    9
c ---[29768]---> BDD-cost:    9
c ---[29767]---> BDD-cost:    9
c ---[29766]---> BDD-cost:    9
c ---[29765]---> BDD-cost:    9
c ---[29764]---> BDD-cost:    9
c ---[29763]---> BDD-cost:    9
c ---[29762]---> BDD-cost:    9
c ---[29761]---> BDD-cost:    9
c ---[29760]---> BDD-cost:    9
c ---[29759]---> BDD-cost:    9
c ---[29758]---> BDD-cost:    9
c ---[29757]---> BDD-cost:    9
c ---[29756]---> BDD-cost:    9
c ---[29755]---> BDD-cost:    9
c ---[29754]---> BDD-cost:    9
c ---[29753]---> BDD-cost:    9
c ---[29752]---> BDD-cost:    9
c ---[29751]---> BDD-cost:    9
c ---[29750]---> BDD-cost:    9
c ---[29749]---> BDD-cost:    9
c ---[29748]---> BDD-cost:    9
c ---[29747]---> BDD-cost:    9
c ---[29746]---> BDD-cost:    9
c ---[29745]---> BDD-cost:    9
c ---[29744]---> BDD-cost:    9
c ---[29743]---> BDD-cost:    9
c ---[29742]---> BDD-cost:    9
c ---[29741]---> BDD-cost:    9
c ---[29740]---> BDD-cost:    9
c ---[29739]---> BDD-cost:    9
c ---[29738]---> BDD-cost:    9
c ---[29737]---> BDD-cost:    9
c ---[29736]---> BDD-cost:    9
c ---[29735]---> BDD-cost:    9
c ---[29734]---> BDD-cost:    9
c ---[29733]---> BDD-cost:    9
c ---[29732]---> BDD-cost:    9
c ---[29731]---> BDD-cost:    9
c ---[29730]---> BDD-cost:    9
c ---[29729]---> BDD-cost:    9
c ---[29728]---> BDD-cost:    9
c ---[29727]---> BDD-cost:    9
c ---[29726]---> BDD-cost:    9
c ---[29725]---> BDD-cost:    9
c ---[29724]---> BDD-cost:    9
c ---[29723]---> BDD-cost:    9
c ---[29722]---> BDD-cost:    9
c ---[29721]---> BDD-cost:    9
c ---[29720]---> BDD-cost:    9
c ---[29719]---> BDD-cost:    9
c ---[29718]---> BDD-cost:    9
c ---[29717]---> BDD-cost:    9
c ---[29716]---> BDD-cost:    9
c ---[29715]---> BDD-cost:    9
c ---[29714]---> BDD-cost:    9
c ---[29713]---> BDD-cost:    9
c ---[29712]---> BDD-cost:    9
c ---[29711]---> BDD-cost:    9
c ---[29710]---> BDD-cost:    9
c ---[29709]---> BDD-cost:    9
c ---[29708]---> BDD-cost:    9
c ---[29707]---> BDD-cost:    9
c ---[29706]---> BDD-cost:    9
c ---[29705]---> BDD-cost:    9
c ---[29704]---> BDD-cost:    9
c ---[29703]---> BDD-cost:    9
c ---[29702]---> BDD-cost:    9
c ---[29701]---> BDD-cost:    9
c ---[29700]---> BDD-cost:    9
c ---[29699]---> BDD-cost:    9
c ---[29698]---> BDD-cost:    9
c ---[29697]---> BDD-cost:    9
c ---[29696]---> BDD-cost:    9
c ---[29695]---> BDD-cost:    9
c ---[29694]---> BDD-cost:    9
c ---[29693]---> BDD-cost:    9
c ---[29692]---> BDD-cost:    9
c ---[29691]---> BDD-cost:    9
c ---[29690]---> BDD-cost:    9
c ---[29689]---> BDD-cost:    9
c ---[29688]---> BDD-cost:    9
c ---[29687]---> BDD-cost:    9
c ---[29686]---> BDD-cost:    9
c ---[29685]---> BDD-cost:    9
c ---[29684]---> BDD-cost:    9
c ---[29683]---> BDD-cost:    9
c ---[29682]---> BDD-cost:    9
c ---[29681]---> BDD-cost:    9
c ---[29680]---> BDD-cost:    9
c ---[29679]---> BDD-cost:    9
c ---[29678]---> BDD-cost:    9
c ---[29677]---> BDD-cost:    9
c ---[29676]---> BDD-cost:    9
c ---[29675]---> BDD-cost:    9
c ---[29674]---> BDD-cost:    9
c ---[29673]---> BDD-cost:    9
c ---[29672]---> BDD-cost:    9
c ---[29671]---> BDD-cost:    9
c ---[29670]---> BDD-cost:    9
c ---[29669]---> BDD-cost:    9
c ---[29668]---> BDD-cost:    9
c ---[29667]---> BDD-cost:    9
c ---[29666]---> BDD-cost:    9
c ---[29665]---> BDD-cost:    9
c ---[29664]---> BDD-cost:    9
c ---[29663]---> BDD-cost:    9
c ---[29662]---> BDD-cost:    9
c ---[29661]---> BDD-cost:    9
c ---[29660]---> BDD-cost:    9
c ---[29659]---> BDD-cost:    9
c ---[29658]---> BDD-cost:    9
c ---[29657]---> BDD-cost:    9
c ---[29656]---> BDD-cost:    9
c ---[29655]---> BDD-cost:    9
c ---[29654]---> BDD-cost:    9
c ---[29653]---> BDD-cost:    9
c ---[29652]---> BDD-cost:    9
c ---[29651]---> BDD-cost:    9
c ---[29650]---> BDD-cost:    9
c ---[29649]---> BDD-cost:    9
c ---[29648]---> BDD-cost:    9
c ---[29647]---> BDD-cost:    9
c ---[29646]---> BDD-cost:    9
c ---[29645]---> BDD-cost:    9
c ---[29644]---> BDD-cost:    9
c ---[29643]---> BDD-cost:    9
c ---[29642]---> BDD-cost:    9
c ---[29641]---> BDD-cost:    9
c ---[29640]---> BDD-cost:    9
c ---[29639]---> BDD-cost:    9
c ---[29638]---> BDD-cost:    9
c ---[29637]---> BDD-cost:    9
c ---[29636]---> BDD-cost:    9
c ---[29635]---> BDD-cost:    9
c ---[29634]---> BDD-cost:    9
c ---[29633]---> BDD-cost:    9
c ---[29632]---> BDD-cost:    9
c ---[29631]---> BDD-cost:    9
c ---[29630]---> BDD-cost:    9
c ---[29629]---> BDD-cost:    9
c ---[29628]---> BDD-cost:    9
c ---[29627]---> BDD-cost:    9
c ---[29626]---> BDD-cost:    9
c ---[29625]---> BDD-cost:    9
c ---[29624]---> BDD-cost:    9
c ---[29623]---> BDD-cost:    9
c ---[29622]---> BDD-cost:    9
c ---[29621]---> BDD-cost:    9
c ---[29620]---> BDD-cost:    9
c ---[29619]---> BDD-cost:    9
c ---[29618]---> BDD-cost:    9
c ---[29617]---> BDD-cost:    9
c ---[29616]---> BDD-cost:    9
c ---[29615]---> BDD-cost:    9
c ---[29614]---> BDD-cost:    9
c ---[29613]---> BDD-cost:    9
c ---[29612]---> BDD-cost:    9
c ---[29611]---> BDD-cost:    9
c ---[29610]---> BDD-cost:    9
c ---[29609]---> BDD-cost:    9
c ---[29608]---> BDD-cost:    9
c ---[29607]---> BDD-cost:    9
c ---[29606]---> BDD-cost:    9
c ---[29605]---> BDD-cost:    9
c ---[29604]---> BDD-cost:    9
c ---[29603]---> BDD-cost:    9
c ---[29602]---> BDD-cost:    9
c ---[29601]---> BDD-cost:    9
c ---[29600]---> BDD-cost:    9
c ---[29599]---> BDD-cost:    9
c ---[29598]---> BDD-cost:    9
c ---[29597]---> BDD-cost:    9
c ---[29596]---> BDD-cost:    9
c ---[29595]---> BDD-cost:    9
c ---[29594]---> BDD-cost:    9
c ---[29593]---> BDD-cost:    9
c ---[29592]---> BDD-cost:    9
c ---[29591]---> BDD-cost:    9
c ---[29590]---> BDD-cost:    9
c ---[29589]---> BDD-cost:    9
c ---[29588]---> BDD-cost:    9
c ---[29587]---> BDD-cost:    9
c ---[29586]---> BDD-cost:    9
c ---[29585]---> BDD-cost:    9
c ---[29584]---> BDD-cost:    9
c ---[29583]---> BDD-cost:    9
c ---[29582]---> BDD-cost:    9
c ---[29581]---> BDD-cost:    9
c ---[29580]---> BDD-cost:    9
c ---[29579]---> BDD-cost:    9
c ---[29578]---> BDD-cost:    9
c ---[29577]---> BDD-cost:    9
c ---[29576]---> BDD-cost:    9
c ---[29575]---> BDD-cost:    9
c ---[29574]---> BDD-cost:    9
c ---[29573]---> BDD-cost:    9
c ---[29572]---> BDD-cost:    9
c ---[29571]---> BDD-cost:    9
c ---[29570]---> BDD-cost:    9
c ---[29569]---> BDD-cost:    9
c ---[29568]---> BDD-cost:    9
c ---[29567]---> BDD-cost:    9
c ---[29566]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:    9
c ---[ 402]---> BDD-cost:    9
c ---[ 401]---> BDD-cost:    9
c ---[ 400]---> BDD-cost:    9
c ---[ 399]---> BDD-cost:    9
c ---[ 398]---> BDD-cost:    9
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    9
c ---[ 395]---> BDD-cost:    9
c ---[ 394]---> BDD-cost:    9
c ---[ 393]---> BDD-cost:    9
c ---[ 392]---> BDD-cost:    9
c ---[ 391]---> BDD-cost:    9
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:    9
c ---[ 386]---> BDD-cost:    9
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    9
c ---[ 383]---> BDD-cost:    9
c ---[ 382]---> BDD-cost:    9
c ---[ 381]---> BDD-cost:    9
c ---[ 380]---> BDD-cost:    9
c ---[ 379]---> BDD-cost:    9
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    9
c ---[ 375]---> BDD-cost:    9
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 372]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:    9
c ---[ 369]---> BDD-cost:    9
c ---[ 368]---> BDD-cost:    9
c ---[ 367]---> BDD-cost:    9
c ---[ 366]---> BDD-cost:    9
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:    9
c ---[ 362]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    9
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:    9
c ---[ 354]---> BDD-cost:    9
c ---[ 353]---> BDD-cost:    9
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    9
c ---[ 350]---> BDD-cost:    9
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:    9
c ---[ 347]---> BDD-cost:    9
c ---[ 346]---> BDD-cost:    9
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    9
c ---[ 343]---> BDD-cost:    9
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:    9
c ---[ 338]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    9
c ---[ 336]---> BDD-cost:    9
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:    9
c ---[ 332]---> BDD-cost:    9
c ---[ 331]---> BDD-cost:    9
c ---[ 330]---> BDD-cost:    9
c ---[ 329]---> BDD-cost:    9
c ---[ 328]---> BDD-cost:    9
c ---[ 327]---> BDD-cost:    9
c ---[ 326]---> BDD-cost:    9
c ---[ 325]---> BDD-cost:    9
c ---[ 324]---> BDD-cost:    9
c ---[ 323]---> BDD-cost:    9
c ---[ 322]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    9
c ---[ 320]---> BDD-cost:    9
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    9
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    9
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    9
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:    9
c ---[ 306]---> BDD-cost:    9
c ---[ 305]---> BDD-cost:    9
c ---[ 304]---> BDD-cost:    9
c ---[ 303]---> BDD-cost:    9
c ---[ 302]---> BDD-cost:    9
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    9
c ---[ 297]---> BDD-cost:    9
c ---[ 296]---> BDD-cost:    9
c ---[ 295]---> BDD-cost:    9
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:    9
c ---[ 290]---> BDD-cost:    9
c ---[ 289]---> BDD-cost:    9
c ---[ 288]---> BDD-cost:    9
c ---[ 287]---> BDD-cost:    9
c ---[ 286]---> BDD-cost:    9
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    9
c ---[ 281]---> BDD-cost:    9
c ---[ 280]---> BDD-cost:    9
c ---[ 279]---> BDD-cost:    9
c ---[ 278]---> BDD-cost:    9
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    9
c ---[ 273]---> BDD-cost:    9
c ---[ 272]---> BDD-cost:    9
c ---[ 271]---> BDD-cost:    9
c ---[ 270]---> BDD-cost:    9
c ---[ 269]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:    9
c ---[ 267]---> BDD-cost:    9
c ---[ 266]---> BDD-cost:    9
c ---[ 265]---> BDD-cost:    9
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    9
c ---[ 257]---> BDD-cost:    9
c ---[ 256]---> BDD-cost:    9
c ---[ 255]---> BDD-cost:    9
c ---[ 254]---> BDD-cost:    9
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:    9
c ---[ 249]---> BDD-cost:    9
c ---[ 248]---> BDD-cost:    9
c ---[ 247]---> BDD-cost:    9
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:    9
c ---[ 241]---> BDD-cost:    9
c ---[ 240]---> BDD-cost:    9
c ---[ 239]---> BDD-cost:    9
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:    9
c ---[ 236]---> BDD-cost:    9
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:    9
c ---[ 233]---> BDD-cost:    9
c ---[ 232]---> BDD-cost:    9
c ---[ 231]---> BDD-cost:    9
c ---[ 230]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:    9
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:    9
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:    9
c ---[ 222]---> BDD-cost:    9
c ---[ 221]---> BDD-cost:    9
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:    9
c ---[ 218]---> BDD-cost:    9
c ---[ 217]---> BDD-cost:    9
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:    9
c ---[ 209]---> BDD-cost:    9
c ---[ 208]---> BDD-cost:    9
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:    9
c ---[ 204]---> BDD-cost:    9
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:    9
c ---[ 201]---> BDD-cost:    9
c ---[ 200]---> BDD-cost:    9
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:    9
c ---[ 194]---> BDD-cost:    9
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:    9
c ---[ 191]---> BDD-cost:    9
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:    9
c ---[ 188]---> BDD-cost:    9
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:    9
c ---[ 185]---> BDD-cost:    9
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:    9
c ---[ 182]---> BDD-cost:    9
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:    9
c ---[ 178]---> BDD-cost:    9
c ---[ 177]---> BDD-cost:    9
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:    9
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:    9
c ---[ 170]---> BDD-cost:    9
c ---[ 169]---> BDD-cost:    9
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    9
c ---[ 159]---> BDD-cost:    9
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    9
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:    9
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:    9
c ---[ 146]---> BDD-cost:    9
c ---[ 145]---> BDD-cost:    9
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:    9
c ---[ 142]---> BDD-cost:    9
c ---[ 141]---> BDD-cost:    9
c ---[ 140]---> BDD-cost:    9
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    9
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    9
c ---[ 134]---> BDD-cost:    9
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:    9
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    9
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:    9
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:    9
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:    9
c ---[ 108]---> BDD-cost:    9
c ---[ 107]---> BDD-cost:    9
c ---[ 106]---> BDD-cost:    9
c ---[ 105]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:    9
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    9
c ---[  98]---> BDD-cost:    9
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    9
c ---[  93]---> BDD-cost:    9
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:    9
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:    9
c ---[  87]---> BDD-cost:    9
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:    9
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:    9
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:    9
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    9
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:    9
c ---[  64]---> BDD-cost:    9
c ---[  63]---> BDD-cost:    9
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:    9
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:    9
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    9
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:    9
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:    9
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:    9
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:    9
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:    9
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:    9
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:    9
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    9
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |   83535   228011 |   27845       0        0     nan |  0.000 % |
c |       100 |   83535   228011 |   30629     100     1070    10.7 |  3.889 % |
c |       250 |   83535   228011 |   33692     250     3441    13.8 |  3.889 % |
c |       475 |   83535   228011 |   37061     475     9847    20.7 |  3.889 % |
c |       814 |   83535   228011 |   40767     814    28879    35.5 |  3.889 % |
c |      1321 |   83535   228011 |   44844    1321    44590    33.8 |  3.889 % |
c |      2081 |   83535   228011 |   49329    2081    78277    37.6 |  3.889 % |
c |      3220 |   83524   227987 |   54262    3218   120756    37.5 |  3.901 % |
c |      4928 |   83524   227987 |   59688    4926   220995    44.9 |  3.901 % |
c |      7492 |   83524   227987 |   65657    7490   371810    49.6 |  3.901 % |
c |     11336 |   83520   227978 |   72222   11333   494615    43.6 |  3.905 % |
c |     17103 |   83520   227978 |   79445   17100   724286    42.4 |  3.905 % |
c |     25753 |   83520   227978 |   87389   25750  1164533    45.2 |  3.905 % |
c |     38727 |   83520   227978 |   96128   38724  1975579    51.0 |  3.905 % |
c |     58188 |   83467   227860 |  105741   58170  3206352    55.1 |  3.962 % |
c |     87382 |   83467   227860 |  116315   87364  4690359    53.7 |  3.962 % |
c |    131171 |   83437   227792 |  127947   25557  2394112    93.7 |  3.996 % |
c |    196856 |   83359   227618 |  140741   91230  6401200    70.2 |  4.084 % |
c |    295383 |   83347   227591 |  154815   61316  4231123    69.0 |  4.096 % |
c |    443174 |   83295   227474 |  170297   59270  5074663    85.6 |  4.149 % |
#### 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.84 0.94 0.90 2/54 26030
Raw data (stat): 26030 (runsolver) R 26029 23176 23175 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479328093 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0005 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 3725 0 0 0 987 10 0 0 25 0 1 0 479328093 16830464 3656 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4109 3656 603 41 0 4068 0
vsize: 16436
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 4638 0 0 0 1983 13 0 0 25 0 1 0 479328093 20611072 4569 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5032 4569 603 41 0 4991 0
vsize: 20128
[startup+30.0027 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 5504 0 0 0 2981 16 0 0 25 0 1 0 479328093 24231936 5435 4294967295 134512640 134672761 3221224624 3221223808 134559397 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5916 5435 603 41 0 5875 0
vsize: 23664
[startup+40.0037 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 6422 0 0 0 3977 20 0 0 25 0 1 0 479328093 27996160 6353 4294967295 134512640 134672761 3221224624 3221223792 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6835 6353 603 41 0 6794 0
vsize: 27340
[startup+50.004 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 7334 0 0 0 4974 22 0 0 25 0 1 0 479328093 31895552 7265 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7787 7265 603 41 0 7746 0
vsize: 31148
[startup+60.004 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 8014 0 0 0 5972 24 0 0 25 0 1 0 479328093 34643968 7945 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8458 7945 603 41 0 8417 0
vsize: 33832
[startup+70.0042 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 8504 0 0 0 6972 25 0 0 25 0 1 0 479328093 36728832 8435 4294967295 134512640 134672761 3221224624 3221223728 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8967 8435 603 41 0 8926 0
vsize: 35868
[startup+80.0048 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 9175 0 0 0 7970 27 0 0 25 0 1 0 479328093 39411712 9106 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9622 9106 603 41 0 9581 0
vsize: 38488
[startup+90.0048 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 9786 0 0 0 8969 28 0 0 25 0 1 0 479328093 41848832 9717 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10217 9717 603 41 0 10176 0
vsize: 40868
[startup+100.005 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 10375 0 0 0 9967 30 0 0 25 0 1 0 479328093 44269568 10306 4294967295 134512640 134672761 3221224624 3221223792 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10808 10306 603 41 0 10767 0
vsize: 43232
[startup+110.006 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 10965 0 0 0 10966 31 0 0 25 0 1 0 479328093 46698496 10896 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11401 10896 603 41 0 11360 0
vsize: 45604
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11509 0 0 0 11964 33 0 0 25 0 1 0 479328093 49016832 11440 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11967 11440 603 41 0 11926 0
vsize: 47868
[startup+130.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11623 0 0 0 12964 34 0 0 25 0 1 0 479328093 49422336 11554 4294967295 134512640 134672761 3221224624 3221223728 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11554 603 41 0 12025 0
vsize: 48264
[startup+140.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11624 0 0 0 13964 34 0 0 25 0 1 0 479328093 49422336 11555 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11555 603 41 0 12025 0
vsize: 48264
[startup+150.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11624 0 0 0 14965 34 0 0 25 0 1 0 479328093 49422336 11555 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11555 603 41 0 12025 0
vsize: 48264
[startup+160.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11624 0 0 0 15965 34 0 0 25 0 1 0 479328093 49422336 11555 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11555 603 41 0 12025 0
vsize: 48264
[startup+170.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11624 0 0 0 16965 34 0 0 25 0 1 0 479328093 49422336 11555 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11555 603 41 0 12025 0
vsize: 48264
[startup+180.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11624 0 0 0 17965 34 0 0 25 0 1 0 479328093 49422336 11555 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11555 603 41 0 12025 0
vsize: 48264
[startup+190.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11624 0 0 0 18965 34 0 0 25 0 1 0 479328093 49422336 11555 4294967295 134512640 134672761 3221224624 3221223808 134558938 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11555 603 41 0 12025 0
vsize: 48264
[startup+200.005 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11625 0 0 0 19965 34 0 0 25 0 1 0 479328093 49422336 11556 4294967295 134512640 134672761 3221224624 3221223808 134558374 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11556 603 41 0 12025 0
vsize: 48264
[startup+210.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11625 0 0 0 20966 34 0 0 25 0 1 0 479328093 49422336 11556 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11556 603 41 0 12025 0
vsize: 48264
[startup+220.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11625 0 0 0 21966 34 0 0 25 0 1 0 479328093 49422336 11556 4294967295 134512640 134672761 3221224624 3221223808 134558883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11556 603 41 0 12025 0
vsize: 48264
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11625 0 0 0 22966 34 0 0 25 0 1 0 479328093 49422336 11556 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11556 603 41 0 12025 0
vsize: 48264
[startup+240.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11625 0 0 0 23966 34 0 0 25 0 1 0 479328093 49422336 11556 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12066 11556 603 41 0 12025 0
vsize: 48264
[startup+250.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 11937 0 0 0 24966 34 0 0 25 0 1 0 479328093 50663424 11868 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12369 11868 603 41 0 12328 0
vsize: 49476
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 12222 0 0 0 25965 35 0 0 25 0 1 0 479328093 51871744 12153 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12664 12153 603 41 0 12623 0
vsize: 50656
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 12470 0 0 0 26964 36 0 0 25 0 1 0 479328093 52957184 12401 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12929 12401 603 41 0 12888 0
vsize: 51716
[startup+280.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 12724 0 0 0 27963 37 0 0 25 0 1 0 479328093 53960704 12655 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13174 12655 603 41 0 13133 0
vsize: 52696
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 12972 0 0 0 28963 38 0 0 25 0 1 0 479328093 55050240 12903 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13440 12903 603 41 0 13399 0
vsize: 53760
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 13209 0 0 0 29961 39 0 0 25 0 1 0 479328093 56037376 13140 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13681 13140 603 41 0 13640 0
vsize: 54724
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 13423 0 0 0 30961 40 0 0 25 0 1 0 479328093 56893440 13354 4294967295 134512640 134672761 3221224624 3221223624 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13890 13354 603 41 0 13849 0
vsize: 55560
[startup+320.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 13639 0 0 0 31960 41 0 0 25 0 1 0 479328093 58363904 13570 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13570 603 41 0 14208 0
vsize: 56996
[startup+330.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 13846 0 0 0 32960 41 0 0 25 0 1 0 479328093 59199488 13777 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14453 13777 603 41 0 14412 0
vsize: 57812
[startup+340.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14041 0 0 0 33960 42 0 0 25 0 1 0 479328093 60002304 13972 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14649 13972 603 41 0 14608 0
vsize: 58596
[startup+350.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14244 0 0 0 34959 43 0 0 25 0 1 0 479328093 60997632 14175 4294967295 134512640 134672761 3221224624 3221223792 134560994 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14892 14175 603 41 0 14851 0
vsize: 59568
[startup+360.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 35959 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223728 134554673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+370.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 36959 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+380.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 37960 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+390.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 38960 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+400.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 26030
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 39960 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+410.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 26031
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 40960 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+420.014 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 26083
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 41960 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+430.014 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 26083
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 42961 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+440.015 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 26083
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 43961 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+450.014 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 26083
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 44961 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+460.015 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 26083
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 45961 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+470.015 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 26083
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 46961 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+480.017 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 26083
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14332 0 0 0 47961 43 0 0 25 0 1 0 479328093 61263872 14263 4294967295 134512640 134672761 3221224624 3221223748 134566059 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14957 14263 603 41 0 14916 0
vsize: 59828
[startup+490.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14354 0 0 0 48961 43 0 0 25 0 1 0 479328093 61489152 14285 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15012 14285 603 41 0 14971 0
vsize: 60048
[startup+500.017 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14354 0 0 0 49962 43 0 0 25 0 1 0 479328093 61489152 14285 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15012 14285 603 41 0 14971 0
vsize: 60048
[startup+510.018 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14354 0 0 0 50962 43 0 0 25 0 1 0 479328093 61489152 14285 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15012 14285 603 41 0 14971 0
vsize: 60048
[startup+520.019 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14354 0 0 0 51962 43 0 0 25 0 1 0 479328093 61489152 14285 4294967295 134512640 134672761 3221224624 3221223792 134561139 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15012 14285 603 41 0 14971 0
vsize: 60048
[startup+530.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14354 0 0 0 52962 43 0 0 25 0 1 0 479328093 61489152 14285 4294967295 134512640 134672761 3221224624 3221223792 134561025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15012 14285 603 41 0 14971 0
vsize: 60048
[startup+540.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14354 0 0 0 53962 43 0 0 25 0 1 0 479328093 61489152 14285 4294967295 134512640 134672761 3221224624 3221223824 134557887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15012 14285 603 41 0 14971 0
vsize: 60048
[startup+550.02 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14354 0 0 0 54963 43 0 0 25 0 1 0 479328093 61489152 14285 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15012 14285 603 41 0 14971 0
vsize: 60048
[startup+560.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14556 0 0 0 55962 44 0 0 25 0 1 0 479328093 62300160 14487 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15210 14487 603 41 0 15169 0
vsize: 60840
[startup+570.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 14878 0 0 0 56961 45 0 0 25 0 1 0 479328093 63528960 14809 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15510 14809 603 41 0 15469 0
vsize: 62040
[startup+580.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 15210 0 0 0 57960 46 0 0 25 0 1 0 479328093 65003520 15141 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15870 15141 603 41 0 15829 0
vsize: 63480
[startup+590.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 15533 0 0 0 58959 47 0 0 25 0 1 0 479328093 66342912 15464 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16197 15464 603 41 0 16156 0
vsize: 64788
[startup+600.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 15870 0 0 0 59957 49 0 0 25 0 1 0 479328093 67727360 15801 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16535 15801 603 41 0 16494 0
vsize: 66140
[startup+610.021 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 16463 0 0 0 60955 51 0 0 25 0 1 0 479328093 70193152 16394 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17137 16394 603 41 0 17096 0
vsize: 68548
[startup+620.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17250 0 0 0 61953 54 0 0 25 0 1 0 479328093 73293824 17181 4294967295 134512640 134672761 3221224624 3221223808 134559161 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17894 17181 603 41 0 17853 0
vsize: 71576
[startup+630.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17881 0 0 0 62952 55 0 0 25 0 1 0 479328093 75878400 17812 4294967295 134512640 134672761 3221224624 3221222476 134565698 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17812 603 41 0 18484 0
vsize: 74100
[startup+640.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17883 0 0 0 63952 55 0 0 25 0 1 0 479328093 75878400 17814 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17814 603 41 0 18484 0
vsize: 74100
[startup+650.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17883 0 0 0 64952 55 0 0 25 0 1 0 479328093 75878400 17814 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17814 603 41 0 18484 0
vsize: 74100
[startup+660.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17883 0 0 0 65952 55 0 0 25 0 1 0 479328093 75878400 17814 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17814 603 41 0 18484 0
vsize: 74100
[startup+670.022 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17883 0 0 0 66952 55 0 0 25 0 1 0 479328093 75878400 17814 4294967295 134512640 134672761 3221224624 3221223792 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17814 603 41 0 18484 0
vsize: 74100
[startup+680.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17883 0 0 0 67953 55 0 0 25 0 1 0 479328093 75878400 17814 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17814 603 41 0 18484 0
vsize: 74100
[startup+690.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 68953 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134561003 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+700.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 69953 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+710.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26085
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 70953 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+720.023 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 71953 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+730.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 72953 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223760 134560560 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+740.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 73953 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223808 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+750.024 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 74953 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223728 134559883 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+760.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 75953 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+770.025 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 76954 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+780.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 77954 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+790.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 78954 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223808 134559405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+800.026 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 79954 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+810.027 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 80954 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+820.028 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 81955 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223776 134542696 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+830.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 82955 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+840.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 83955 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+850.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 84955 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+860.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 17885 0 0 0 85955 55 0 0 25 0 1 0 479328093 75878400 17816 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18525 17816 603 41 0 18484 0
vsize: 74100
[startup+870.029 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 18125 0 0 0 86955 56 0 0 25 0 1 0 479328093 76947456 18056 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18786 18056 603 41 0 18745 0
vsize: 75144
[startup+880.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 18423 0 0 0 87954 57 0 0 25 0 1 0 479328093 78159872 18354 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19082 18354 603 41 0 19041 0
vsize: 76328
[startup+890.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 18713 0 0 0 88953 58 0 0 25 0 1 0 479328093 79368192 18644 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19377 18644 603 41 0 19336 0
vsize: 77508
[startup+900.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 18979 0 0 0 89953 58 0 0 25 0 1 0 479328093 80445440 18910 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19640 18910 603 41 0 19599 0
vsize: 78560
[startup+910.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 19254 0 0 0 90953 59 0 0 25 0 1 0 479328093 81506304 19185 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19899 19185 603 41 0 19858 0
vsize: 79596
[startup+920.031 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 19512 0 0 0 91952 59 0 0 25 0 1 0 479328093 82579456 19443 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20161 19443 603 41 0 20120 0
vsize: 80644
[startup+930.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 19796 0 0 0 92952 60 0 0 25 0 1 0 479328093 83808256 19727 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20461 19727 603 41 0 20420 0
vsize: 81844
[startup+940.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 20100 0 0 0 93951 61 0 0 25 0 1 0 479328093 85053440 20031 4294967295 134512640 134672761 3221224624 3221223808 134559354 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20765 20031 603 41 0 20724 0
vsize: 83060
[startup+950.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 20374 0 0 0 94951 61 0 0 25 0 1 0 479328093 86269952 20305 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21062 20305 603 41 0 21021 0
vsize: 84248
[startup+960.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 20626 0 0 0 95950 62 0 0 25 0 1 0 479328093 87224320 20557 4294967295 134512640 134672761 3221224624 3221223728 134560054 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21295 20557 603 41 0 21254 0
vsize: 85180
[startup+970.032 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 20918 0 0 0 96950 63 0 0 25 0 1 0 479328093 88424448 20849 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21588 20849 603 41 0 21547 0
vsize: 86352
[startup+980.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 21214 0 0 0 97949 64 0 0 25 0 1 0 479328093 89632768 21145 4294967295 134512640 134672761 3221224624 3221223792 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21883 21145 603 41 0 21842 0
vsize: 87532
[startup+990.033 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 21452 0 0 0 98948 65 0 0 25 0 1 0 479328093 90566656 21383 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22111 21383 603 41 0 22070 0
vsize: 88444
[startup+1000.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 21686 0 0 0 99948 65 0 0 25 0 1 0 479328093 91648000 21617 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22375 21617 603 41 0 22334 0
vsize: 89500
[startup+1010.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 21903 0 0 0 100947 66 0 0 25 0 1 0 479328093 92446720 21834 4294967295 134512640 134672761 3221224624 3221223792 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22570 21834 603 41 0 22529 0
vsize: 90280
[startup+1020.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 22145 0 0 0 101947 67 0 0 25 0 1 0 479328093 93548544 22076 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22839 22076 603 41 0 22798 0
vsize: 91356
[startup+1030.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 22390 0 0 0 102946 67 0 0 25 0 1 0 479328093 94638080 22321 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23105 22321 603 41 0 23064 0
vsize: 92420
[startup+1040.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 22616 0 0 0 103945 68 0 0 25 0 1 0 479328093 95576064 22547 4294967295 134512640 134672761 3221224624 3221223792 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23334 22547 603 41 0 23293 0
vsize: 93336
[startup+1050.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 22802 0 0 0 104945 69 0 0 25 0 1 0 479328093 96407552 22733 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23537 22733 603 41 0 23496 0
vsize: 94148
[startup+1060.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 22952 0 0 0 105944 69 0 0 25 0 1 0 479328093 97075200 22883 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23700 22883 603 41 0 23659 0
vsize: 94800
[startup+1070.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23124 0 0 0 106944 70 0 0 25 0 1 0 479328093 97878016 23055 4294967295 134512640 134672761 3221224624 3221223792 134561391 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23896 23055 603 41 0 23855 0
vsize: 95584
[startup+1080.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23305 0 0 0 107944 70 0 0 25 0 1 0 479328093 98553856 23236 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24061 23236 603 41 0 24020 0
vsize: 96244
[startup+1090.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23527 0 0 0 108943 71 0 0 25 0 1 0 479328093 99495936 23458 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23458 603 41 0 24250 0
vsize: 97164
[startup+1100.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23542 0 0 0 109944 71 0 0 25 0 1 0 479328093 99495936 23473 4294967295 134512640 134672761 3221224624 3221223728 134554662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23473 603 41 0 24250 0
vsize: 97164
[startup+1110.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23542 0 0 0 110944 71 0 0 25 0 1 0 479328093 99495936 23473 4294967295 134512640 134672761 3221224624 3221223728 134554677 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23473 603 41 0 24250 0
vsize: 97164
[startup+1120.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23542 0 0 0 111944 71 0 0 25 0 1 0 479328093 99495936 23473 4294967295 134512640 134672761 3221224624 3221223728 134559805 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23473 603 41 0 24250 0
vsize: 97164
[startup+1130.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23542 0 0 0 112944 71 0 0 25 0 1 0 479328093 99495936 23473 4294967295 134512640 134672761 3221224624 3221223728 134559979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23473 603 41 0 24250 0
vsize: 97164
[startup+1140.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23542 0 0 0 113944 71 0 0 25 0 1 0 479328093 99495936 23473 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23473 603 41 0 24250 0
vsize: 97164
[startup+1150.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23542 0 0 0 114945 71 0 0 25 0 1 0 479328093 99495936 23473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23473 603 41 0 24250 0
vsize: 97164
[startup+1160.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23542 0 0 0 115945 71 0 0 25 0 1 0 479328093 99495936 23473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23473 603 41 0 24250 0
vsize: 97164
[startup+1170.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23544 0 0 0 116945 71 0 0 25 0 1 0 479328093 99495936 23475 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23475 603 41 0 24250 0
vsize: 97164
[startup+1180.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23544 0 0 0 117945 71 0 0 25 0 1 0 479328093 99495936 23475 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23475 603 41 0 24250 0
vsize: 97164
[startup+1190.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23544 0 0 0 118946 71 0 0 25 0 1 0 479328093 99495936 23475 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23475 603 41 0 24250 0
vsize: 97164
[startup+1200.04 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26087
Raw data (stat): 26030 (minisat+) R 26029 23176 23175 0 -1 0 23544 0 0 0 119946 71 0 0 25 0 1 0 479328093 99495936 23475 4294967295 134512640 134672761 3221224624 3221223792 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24291 23475 603 41 0 24250 0
vsize: 97164
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.09 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 26087
Raw data (stat): 26030 (minisat+) Z 26029 23176 23175 0 -1 12 23546 0 0 0 119946 76 0 0 25 0 1 0 479328093 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.09
CPU time (s): 1200.22
CPU user time (s): 1199.46
CPU system time (s): 0.760884
CPU usage (%): 100.011
Max. virtual memory (Kb): 97164
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####