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 5655

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        898688 kB
Buffers:         34972 kB
Cached:          80080 kB
SwapCached:          4 kB
Active:          58076 kB
Inactive:        59832 kB
HighTotal:      131008 kB
HighFree:        47124 kB
LowTotal:       903652 kB
LowFree:        851564 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              32 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12488 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:38:11 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 4119 7 1200.24 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   83535   228011 |   25060       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/25180          
c   -- var.elim.:  2000/25180          
c   -- var.elim.:  3000/25180          
c   -- var.elim.:  4000/25180          
c   -- var.elim.:  5000/25180          
c   -- var.elim.:  6000/25180          
c   -- var.elim.:  7000/25180          
c   -- var.elim.:  8000/25180          
c   -- var.elim.:  9000/25180          
c   -- var.elim.:  10000/25180          
c   -- var.elim.:  11000/25180          
c   -- var.elim.:  12000/25180          
c   -- var.elim.:  13000/25180          
c   -- var.elim.:  14000/25180          
c   -- var.elim.:  15000/25180          
c   -- var.elim.:  16000/25180          
c   -- var.elim.:  17000/25180          
c   -- var.elim.:  18000/25180          
c   -- var.elim.:  19000/25180          
c   -- var.elim.:  20000/25180          
c   -- var.elim.:  21000/25180          
c   -- var.elim.:  22000/25180          
c   -- var.elim.:  23000/25180          
c   -- var.elim.:  24000/25180          
c   -- var.elim.:  25000/25180          
c   -- var.elim.:  25180/25180          
c   -- var.elim.:  1000/11006          
c   -- var.elim.:  2000/11006          
c   -- var.elim.:  3000/11006          
c   -- var.elim.:  4000/11006          
c   -- var.elim.:  5000/11006          
c   -- var.elim.:  6000/11006          
c   -- var.elim.:  7000/11006          
c   -- var.elim.:  8000/11006          
c   -- var.elim.:  9000/11006          
c   -- var.elim.:  10000/11006          
c   -- var.elim.:  11000/11006          
c   -- var.elim.:  11006/11006          
c   -- var.elim.:  148/148          
c   -- subsuming                       
c   -- var.elim.:  1000/9073          
c   -- var.elim.:  2000/9073          
c   -- var.elim.:  3000/9073          
c   -- var.elim.:  4000/9073          
c   -- var.elim.:  5000/9073          
c   -- var.elim.:  6000/9073          
c   -- var.elim.:  7000/9073          
c   -- var.elim.:  8000/9073          
c   -- var.elim.:  9000/9073          
c   -- var.elim.:  9073/9073          
c   -- var.elim.:  1000/8644          
c   -- var.elim.:  2000/8644          
c   -- var.elim.:  3000/8644          
c   -- var.elim.:  4000/8644          
c   -- var.elim.:  5000/8644          
c   -- var.elim.:  6000/8644          
c   -- var.elim.:  7000/8644          
c   -- var.elim.:  8000/8644          
c   -- var.elim.:  8644/8644          
c   -- var.elim.:  116/116          
c   -- subsuming                       
c   -- var.elim.:  1000/5874          
c   -- var.elim.:  2000/5874          
c   -- var.elim.:  3000/5874          
c   -- var.elim.:  4000/5874          
c   -- var.elim.:  5000/5874          
c   -- var.elim.:  5874/5874          
c   -- var.elim.:  1000/3861          
c   -- var.elim.:  2000/3861          
c   -- var.elim.:  3000/3861          
c   -- var.elim.:  3861/3861          
c   -- subsuming                       
c   -- var.elim.:  1000/3865          
c   -- var.elim.:  2000/3865          
c   -- var.elim.:  3000/3865          
c   -- var.elim.:  3865/3865          
c   -- var.elim.:  961/961          
c   -- var.elim.:  78/78          
c   -- subsuming                       
c   -- var.elim.:  39/39       #### 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.80 0.92 0.90 2/54 24590
Raw data (stat): 24590 (runsolver) R 24589 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422351033 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.83 0.93 0.90 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 5715 0 0 0 980 17 0 0 25 0 1 0 422351033 22982656 4889 4294967295 134512640 134672761 3221224560 3221223728 134615859 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5611 4889 603 41 0 5570 0
vsize: 22444
[startup+20.0004 s]
Raw data (loadavg): 0.86 0.93 0.90 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 7019 0 0 0 1977 21 0 0 25 0 1 0 422351033 28340224 6193 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6919 6193 603 41 0 6878 0
vsize: 27676
[startup+30.0015 s]
Raw data (loadavg): 0.88 0.93 0.90 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 8169 0 0 0 2974 24 0 0 25 0 1 0 422351033 33124352 7343 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8087 7343 603 41 0 8046 0
vsize: 32348
[startup+40.0009 s]
Raw data (loadavg): 0.90 0.93 0.90 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 9247 0 0 0 3971 28 0 0 25 0 1 0 422351033 37507072 8421 4294967295 134512640 134672761 3221224560 3221223744 134615505 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9157 8421 603 41 0 9116 0
vsize: 36628
[startup+50.0005 s]
Raw data (loadavg): 0.91 0.93 0.90 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 10075 0 0 0 4968 30 0 0 25 0 1 0 422351033 40955904 9249 4294967295 134512640 134672761 3221224560 3221223760 134610667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9999 9249 603 41 0 9958 0
vsize: 39996
[startup+60.0006 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 10931 0 0 0 5966 32 0 0 25 0 1 0 422351033 44650496 10105 4294967295 134512640 134672761 3221224560 3221223600 134613012 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10901 10105 603 41 0 10860 0
vsize: 43604
[startup+70.0013 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 12281 0 0 0 6963 36 0 0 25 0 1 0 422351033 50073600 11455 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12225 11455 603 41 0 12184 0
vsize: 48900
[startup+80.0016 s]
Raw data (loadavg): 0.94 0.94 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 13320 0 0 0 7960 39 0 0 25 0 1 0 422351033 54329344 12494 4294967295 134512640 134672761 3221224560 3221223600 134614263 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13264 12494 603 41 0 13223 0
vsize: 53056
[startup+90.0017 s]
Raw data (loadavg): 0.95 0.94 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 14126 0 0 0 8958 41 0 0 25 0 1 0 422351033 57634816 13300 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14071 13300 603 41 0 14030 0
vsize: 56284
[startup+100.001 s]
Raw data (loadavg): 0.96 0.94 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 14822 0 0 0 9956 43 0 0 25 0 1 0 422351033 60399616 13996 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14746 13996 603 41 0 14705 0
vsize: 58984
[startup+110.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 15602 0 0 0 10954 46 0 0 25 0 1 0 422351033 63574016 14776 4294967295 134512640 134672761 3221224560 3221223760 134610319 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15521 14776 603 41 0 15480 0
vsize: 62084
[startup+120.002 s]
Raw data (loadavg): 0.97 0.94 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 16418 0 0 0 11952 48 0 0 25 0 1 0 422351033 66887680 15592 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16330 15592 603 41 0 16289 0
vsize: 65320
[startup+130.002 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17072 0 0 0 12951 49 0 0 25 0 1 0 422351033 69664768 16246 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17008 16246 603 41 0 16967 0
vsize: 68032
[startup+140.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 13950 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+150.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 14950 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+160.002 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 15950 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+170.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 16951 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+180.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 17951 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+190.002 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 18951 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+200.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 19951 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+210.001 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 20951 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+220 s]
Raw data (loadavg): 0.99 0.95 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 21951 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+230 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 22952 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+240 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 23952 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+250 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 24952 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+260 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 25952 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+270 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 26952 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+280 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17394 0 0 0 27952 50 0 0 25 0 1 0 422351033 70418432 16443 4294967295 134512640 134672761 3221224560 3221223744 134615779 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16443 603 41 0 17151 0
vsize: 68768
[startup+289.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17395 0 0 0 28952 50 0 0 25 0 1 0 422351033 70418432 16444 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16444 603 41 0 17151 0
vsize: 68768
[startup+299.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17395 0 0 0 29953 50 0 0 25 0 1 0 422351033 70418432 16444 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17192 16444 603 41 0 17151 0
vsize: 68768
[startup+309.999 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 17602 0 0 0 30952 50 0 0 25 0 1 0 422351033 71340032 16651 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17417 16651 603 41 0 17376 0
vsize: 69668
[startup+319.998 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 18286 0 0 0 31951 52 0 0 25 0 1 0 422351033 74117120 17335 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18095 17335 603 41 0 18054 0
vsize: 72380
[startup+329.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 18843 0 0 0 32949 54 0 0 25 0 1 0 422351033 76378112 17892 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18647 17892 603 41 0 18606 0
vsize: 74588
[startup+339.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 19307 0 0 0 33948 55 0 0 25 0 1 0 422351033 78245888 18356 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19103 18356 603 41 0 19062 0
vsize: 76412
[startup+349.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 19749 0 0 0 34947 56 0 0 25 0 1 0 422351033 80637952 18798 4294967295 134512640 134672761 3221224560 3221223744 134615649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19687 18798 603 41 0 19646 0
vsize: 78748
[startup+359.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 20355 0 0 0 35946 58 0 0 25 0 1 0 422351033 83161088 19404 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20303 19405 603 41 0 20262 0
vsize: 81212
[startup+369.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 20967 0 0 0 36944 60 0 0 25 0 1 0 422351033 85544960 20016 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20885 20016 603 41 0 20844 0
vsize: 83540
[startup+380 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21561 0 0 0 37944 60 0 0 25 0 1 0 422351033 87764992 20458 4294967295 134512640 134672761 3221224560 3221223516 1075350790 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20458 603 41 0 21386 0
vsize: 85708
[startup+389.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21564 0 0 0 38944 60 0 0 25 0 1 0 422351033 87764992 20461 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20461 603 41 0 21386 0
vsize: 85708
[startup+399.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21564 0 0 0 39944 60 0 0 25 0 1 0 422351033 87764992 20461 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20461 603 41 0 21386 0
vsize: 85708
[startup+409.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21565 0 0 0 40944 60 0 0 25 0 1 0 422351033 87764992 20462 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20462 603 41 0 21386 0
vsize: 85708
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 41944 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223568 134522555 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+429.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 42945 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+439.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 43945 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+449.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 44945 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+459.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 45945 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+469.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 46945 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223600 134612981 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+479.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 47945 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+489.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 48945 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+499.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 49946 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223600 134603558 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+509.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 50946 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+519.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 51946 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+529.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 52946 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+539.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 53946 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+549.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 54946 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+559.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21567 0 0 0 55947 60 0 0 25 0 1 0 422351033 87764992 20464 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21427 20464 603 41 0 21386 0
vsize: 85708
[startup+569.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 21624 0 0 0 56947 61 0 0 25 0 1 0 422351033 88031232 20521 4294967295 134512640 134672761 3221224560 3221223600 134612665 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21492 20521 603 41 0 21451 0
vsize: 85968
[startup+579.996 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 22147 0 0 0 57945 62 0 0 25 0 1 0 422351033 90157056 21044 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22011 21044 603 41 0 21970 0
vsize: 88044
[startup+589.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 22635 0 0 0 58944 63 0 0 25 0 1 0 422351033 92168192 21532 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22502 21532 603 41 0 22461 0
vsize: 90008
[startup+599.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23095 0 0 0 59943 65 0 0 25 0 1 0 422351033 94162944 21992 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22989 21992 603 41 0 22948 0
vsize: 91956
[startup+609.995 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23750 0 0 0 60941 67 0 0 25 0 1 0 422351033 96956416 22615 4294967295 134512640 134672761 3221224560 3221223616 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23671 22615 603 41 0 23630 0
vsize: 94684
[startup+619.994 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23761 0 0 0 61941 67 0 0 25 0 1 0 422351033 95907840 22462 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22462 603 41 0 23374 0
vsize: 93660
[startup+629.994 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23761 0 0 0 62941 67 0 0 25 0 1 0 422351033 95907840 22462 4294967295 134512640 134672761 3221224560 3221223684 134566071 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22462 603 41 0 23374 0
vsize: 93660
[startup+639.994 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23761 0 0 0 63942 67 0 0 25 0 1 0 422351033 95907840 22462 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22462 603 41 0 23374 0
vsize: 93660
[startup+649.994 s]
Raw data (loadavg): 1.05 0.99 0.91 3/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23761 0 0 0 64942 67 0 0 25 0 1 0 422351033 95907840 22462 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22462 603 41 0 23374 0
vsize: 93660
[startup+659.993 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23761 0 0 0 65942 67 0 0 25 0 1 0 422351033 95907840 22462 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22462 603 41 0 23374 0
vsize: 93660
[startup+669.993 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23761 0 0 0 66942 67 0 0 25 0 1 0 422351033 95907840 22462 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22462 603 41 0 23374 0
vsize: 93660
[startup+679.994 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23761 0 0 0 67942 67 0 0 25 0 1 0 422351033 95907840 22462 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22462 603 41 0 23374 0
vsize: 93660
[startup+689.993 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23762 0 0 0 68942 67 0 0 25 0 1 0 422351033 95907840 22463 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22463 603 41 0 23374 0
vsize: 93660
[startup+699.993 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 69943 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+709.994 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 70943 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+719.993 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 71943 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+729.994 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 72943 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+739.994 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 73943 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+749.994 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 74944 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+759.993 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 75944 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+769.993 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 76944 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+779.993 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 77944 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+789.993 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 78944 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+799.992 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 79944 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+809.992 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 80944 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+819.991 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 81944 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+829.992 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 82945 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+839.992 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 83945 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+849.992 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 84945 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+859.992 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 23764 0 0 0 85945 67 0 0 25 0 1 0 422351033 95907840 22465 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23415 22465 603 41 0 23374 0
vsize: 93660
[startup+869.992 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 24006 0 0 0 86945 67 0 0 25 0 1 0 422351033 96972800 22707 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23675 22707 603 41 0 23634 0
vsize: 94700
[startup+879.993 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 24327 0 0 0 87944 68 0 0 25 0 1 0 422351033 98336768 23028 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24008 23028 603 41 0 23967 0
vsize: 96032
[startup+889.993 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 24586 0 0 0 88944 69 0 0 25 0 1 0 422351033 99409920 23287 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24270 23287 603 41 0 24229 0
vsize: 97080
[startup+899.993 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 24846 0 0 0 89942 70 0 0 25 0 1 0 422351033 100487168 23547 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24533 23547 603 41 0 24492 0
vsize: 98132
[startup+909.994 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 25114 0 0 0 90942 71 0 0 25 0 1 0 422351033 101548032 23815 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24792 23815 603 41 0 24751 0
vsize: 99168
[startup+919.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 25377 0 0 0 91942 72 0 0 25 0 1 0 422351033 102678528 24078 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25068 24078 603 41 0 25027 0
vsize: 100272
[startup+929.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 25665 0 0 0 92941 72 0 0 25 0 1 0 422351033 103866368 24366 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25358 24366 603 41 0 25317 0
vsize: 101432
[startup+939.994 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 25942 0 0 0 93940 73 0 0 25 0 1 0 422351033 105160704 24643 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25674 24643 603 41 0 25633 0
vsize: 102696
[startup+949.994 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 26269 0 0 0 94939 75 0 0 25 0 1 0 422351033 106483712 24970 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25997 24970 603 41 0 25956 0
vsize: 103988
[startup+959.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 26681 0 0 0 95938 76 0 0 25 0 1 0 422351033 108077056 25382 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26386 25382 603 41 0 26345 0
vsize: 105544
[startup+969.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27277 0 0 0 96937 77 0 0 25 0 1 0 422351033 110804992 25978 4294967295 134512640 134672761 3221224560 3221222896 134645372 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27052 25978 603 41 0 27011 0
vsize: 108208
[startup+979.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27292 0 0 0 97937 77 0 0 25 0 1 0 422351033 109756416 25813 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25813 603 41 0 26755 0
vsize: 107184
[startup+989.996 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27293 0 0 0 98937 77 0 0 25 0 1 0 422351033 109756416 25814 4294967295 134512640 134672761 3221224560 3221223600 134612608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25814 603 41 0 26755 0
vsize: 107184
[startup+999.995 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27293 0 0 0 99938 77 0 0 25 0 1 0 422351033 109756416 25814 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25814 603 41 0 26755 0
vsize: 107184
[startup+1009.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27293 0 0 0 100938 77 0 0 25 0 1 0 422351033 109756416 25814 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25814 603 41 0 26755 0
vsize: 107184
[startup+1019.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27294 0 0 0 101938 77 0 0 25 0 1 0 422351033 109756416 25815 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25815 603 41 0 26755 0
vsize: 107184
[startup+1030 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27294 0 0 0 102938 77 0 0 25 0 1 0 422351033 109756416 25815 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25815 603 41 0 26755 0
vsize: 107184
[startup+1040 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27294 0 0 0 103938 77 0 0 25 0 1 0 422351033 109756416 25815 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25815 603 41 0 26755 0
vsize: 107184
[startup+1050 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27294 0 0 0 104938 77 0 0 25 0 1 0 422351033 109756416 25815 4294967295 134512640 134672761 3221224560 3221223744 134615703 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25815 603 41 0 26755 0
vsize: 107184
[startup+1060 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27294 0 0 0 105939 77 0 0 25 0 1 0 422351033 109756416 25815 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25815 603 41 0 26755 0
vsize: 107184
[startup+1070 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27294 0 0 0 106939 77 0 0 25 0 1 0 422351033 109756416 25815 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25815 603 41 0 26755 0
vsize: 107184
[startup+1080 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27294 0 0 0 107939 77 0 0 25 0 1 0 422351033 109756416 25815 4294967295 134512640 134672761 3221224560 3221223600 134612845 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25815 603 41 0 26755 0
vsize: 107184
[startup+1089.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27294 0 0 0 108939 77 0 0 25 0 1 0 422351033 109756416 25815 4294967295 134512640 134672761 3221224560 3221223744 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25815 603 41 0 26755 0
vsize: 107184
[startup+1099.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27296 0 0 0 109939 77 0 0 25 0 1 0 422351033 109756416 25817 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25817 603 41 0 26755 0
vsize: 107184
[startup+1109.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27296 0 0 0 110939 77 0 0 25 0 1 0 422351033 109756416 25817 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25817 603 41 0 26755 0
vsize: 107184
[startup+1119.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27296 0 0 0 111940 77 0 0 25 0 1 0 422351033 109756416 25817 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25817 603 41 0 26755 0
vsize: 107184
[startup+1129.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27296 0 0 0 112940 77 0 0 25 0 1 0 422351033 109756416 25817 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25817 603 41 0 26755 0
vsize: 107184
[startup+1139.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27297 0 0 0 113940 77 0 0 25 0 1 0 422351033 109756416 25818 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25818 603 41 0 26755 0
vsize: 107184
[startup+1149.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27297 0 0 0 114940 77 0 0 25 0 1 0 422351033 109756416 25818 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25818 603 41 0 26755 0
vsize: 107184
[startup+1159.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27297 0 0 0 115940 77 0 0 25 0 1 0 422351033 109756416 25818 4294967295 134512640 134672761 3221224560 3221223744 134615689 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25818 603 41 0 26755 0
vsize: 107184
[startup+1169.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27297 0 0 0 116941 77 0 0 25 0 1 0 422351033 109756416 25818 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25818 603 41 0 26755 0
vsize: 107184
[startup+1180 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27297 0 0 0 117941 77 0 0 25 0 1 0 422351033 109756416 25818 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25818 603 41 0 26755 0
vsize: 107184
[startup+1189.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27297 0 0 0 118941 77 0 0 25 0 1 0 422351033 109756416 25818 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25818 603 41 0 26755 0
vsize: 107184
[startup+1199.99 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 24590
Raw data (stat): 24590 (minisat+) R 24589 20937 20936 0 -1 0 27297 0 0 0 119941 77 0 0 25 0 1 0 422351033 109756416 25818 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26796 25818 603 41 0 26755 0
vsize: 107184
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 24590
Raw data (stat): 24590 (minisat+) Z 24589 20937 20936 0 -1 12 27297 0 0 0 119941 82 0 0 25 0 1 0 422351033 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.24
CPU user time (s): 1199.42
CPU system time (s): 0.827874
CPU usage (%): 100.016
Max. virtual memory (Kb): 108208
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####