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 6456

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc8 THE 2005-04-14 05:02:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4871 boxname=wulflinc8 idbench=359 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  552cc7fcebca47ae66a3cb1c13679513  /oldhome/oroussel/tmp/wulflinc8/normalized-ppp:1-11,19,21.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc8/normalized-ppp:1-11,19,21.opb /oldhome/oroussel/tmp/wulflinc8/normalized-ppp:1-11,19,21.opb
IDLAUNCH: 4871
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.007
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.007
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:        872012 kB
Buffers:         37772 kB
Cached:         103124 kB
SwapCached:          0 kB
Active:          78116 kB
Inactive:        67476 kB
HighTotal:      131008 kB
HighFree:        22176 kB
LowTotal:       903652 kB
LowFree:        849836 kB
SwapTotal:     2097136 kB
SwapFree:      2097136 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6932 kB
Slab:            11616 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:22:57 (client local time) WITH STATUS 0 IN 1200.17 SECONDS
stats: 4871 7 1200.17 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30353 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30352]---> BDD-cost:   56
c ---[30351]---> BDD-cost:   56
c ---[30350]---> BDD-cost:   56
c ---[30349]---> BDD-cost:   56
c ---[30348]---> BDD-cost:   56
c ---[30347]---> BDD-cost:   56
c ---[30346]---> BDD-cost:   56
c ---[30345]---> BDD-cost:   56
c ---[30344]---> BDD-cost:   56
c ---[30343]---> BDD-cost:   56
c ---[30342]---> BDD-cost:   56
c ---[30341]---> BDD-cost:   56
c ---[30340]---> BDD-cost:  123
c ---[30339]---> BDD-cost:  123
c ---[30338]---> BDD-cost:  123
c ---[30337]---> BDD-cost:  123
c ---[30336]---> BDD-cost:  123
c ---[30335]---> BDD-cost:  123
c ---[30334]---> BDD-cost:  123
c ---[30333]---> BDD-cost:  123
c ---[30332]---> BDD-cost:  123
c ---[30331]---> BDD-cost:  123
c ---[30330]---> BDD-cost:  123
c ---[30329]---> BDD-cost:  123
c ---[30328]---> BDD-cost:  123
c ---[30327]---> BDD-cost:  123
c ---[30326]---> BDD-cost:  123
c ---[30325]---> BDD-cost:  123
c ---[30324]---> BDD-cost:  123
c ---[30323]---> BDD-cost:  123
c ---[30322]---> BDD-cost:  133
c ---[30321]---> BDD-cost:  133
c ---[30320]---> BDD-cost:  133
c ---[30319]---> BDD-cost:  133
c ---[30318]---> BDD-cost:  133
c ---[30317]---> BDD-cost:  133
c ---[30316]---> BDD-cost:  123
c ---[30315]---> BDD-cost:  123
c ---[30314]---> BDD-cost:  123
c ---[30313]---> BDD-cost:  123
c ---[30312]---> BDD-cost:  123
c ---[30311]---> BDD-cost:  123
c ---[30310]---> BDD-cost:  123
c ---[30309]---> BDD-cost:  123
c ---[30308]---> BDD-cost:  123
c ---[30307]---> BDD-cost:  123
c ---[30306]---> BDD-cost:  123
c ---[30305]---> BDD-cost:  123
c ---[30304]---> BDD-cost:  123
c ---[30303]---> BDD-cost:  123
c ---[30302]---> BDD-cost:  123
c ---[30301]---> BDD-cost:  123
c ---[30300]---> BDD-cost:  123
c ---[30299]---> BDD-cost:  123
c ---[30298]---> Sorter-cost:  550     Base: 2 2
c ---[30297]---> Sorter-cost:  550     Base: 2 2
c ---[30296]---> Sorter-cost:  550     Base: 2 2
c ---[30295]---> Sorter-cost:  550     Base: 2 2
c ---[30294]---> Sorter-cost:  550     Base: 2 2
c ---[30293]---> Sorter-cost:  550     Base: 2 2
c ---[30292]---> Sorter-cost:  550     Base: 2 2
c ---[30291]---> Sorter-cost:  550     Base: 2 2
c ---[30290]---> Sorter-cost:  550     Base: 2 2
c ---[30289]---> Sorter-cost:  550     Base: 2 2
c ---[30288]---> Sorter-cost:  550     Base: 2 2
c ---[30287]---> Sorter-cost:  550     Base: 2 2
c ---[30286]---> BDD-cost:   86
c ---[30285]---> BDD-cost:   86
c ---[30284]---> BDD-cost:   86
c ---[30283]---> BDD-cost:   86
c ---[30282]---> BDD-cost:   86
c ---[30281]---> BDD-cost:   86
c ---[30280]---> BDD-cost:   56
c ---[30279]---> BDD-cost:   56
c ---[30278]---> BDD-cost:   56
c ---[30277]---> BDD-cost:   56
c ---[30276]---> BDD-cost:   56
c ---[30275]---> BDD-cost:   56
c ---[30273]---> BDD-cost:   23
c ---[30271]---> BDD-cost:   23
c ---[30269]---> BDD-cost:   23
c ---[30267]---> BDD-cost:   23
c ---[30265]---> BDD-cost:   23
c ---[30263]---> BDD-cost:   23
c ---[30261]---> BDD-cost:   23
c ---[30259]---> BDD-cost:   23
c ---[30257]---> BDD-cost:   23
c ---[30255]---> BDD-cost:   23
c ---[30253]---> BDD-cost:   23
c ---[30251]---> BDD-cost:   23
c ---[30249]---> BDD-cost:   23
c ---[30247]---> BDD-cost:   23
c ---[30245]---> BDD-cost:   23
c ---[30243]---> BDD-cost:   23
c ---[30241]---> BDD-cost:   23
c ---[30239]---> BDD-cost:   23
c ---[30237]---> BDD-cost:   17
c ---[30235]---> BDD-cost:   17
c ---[30233]---> BDD-cost:   17
c ---[30231]---> BDD-cost:   17
c ---[30229]---> BDD-cost:   17
c ---[30227]---> BDD-cost:   17
c ---[30225]---> BDD-cost:   23
c ---[30223]---> BDD-cost:   23
c ---[30221]---> BDD-cost:   23
c ---[30219]---> BDD-cost:   23
c ---[30217]---> BDD-cost:   23
c ---[30215]---> BDD-cost:   23
c ---[30213]---> BDD-cost:   23
c ---[30211]---> BDD-cost:   23
c ---[30209]---> BDD-cost:   23
c ---[30207]---> BDD-cost:   23
c ---[30205]---> BDD-cost:   23
c ---[30203]---> BDD-cost:   23
c ---[30201]---> BDD-cost:   17
c ---[30199]---> BDD-cost:   17
c ---[30197]---> BDD-cost:   17
c ---[30195]---> BDD-cost:   17
c ---[30193]---> BDD-cost:   17
c ---[30191]---> BDD-cost:   17
c ---[30189]---> BDD-cost:   15
c ---[30187]---> BDD-cost:   15
c ---[30185]---> BDD-cost:   15
c ---[30183]---> BDD-cost:   15
c ---[30181]---> BDD-cost:   15
c ---[30179]---> BDD-cost:   15
c ---[30177]---> BDD-cost:   23
c ---[30175]---> BDD-cost:   23
c ---[30173]---> BDD-cost:   23
c ---[30171]---> BDD-cost:   23
c ---[30169]---> BDD-cost:   23
c ---[30167]---> BDD-cost:   23
c ---[30165]---> BDD-cost:   23
c ---[30163]---> BDD-cost:   23
c ---[30161]---> BDD-cost:   23
c ---[30159]---> BDD-cost:   23
c ---[30157]---> BDD-cost:   23
c ---[30155]---> BDD-cost:   23
c ---[30153]---> BDD-cost:   23
c ---[30151]---> BDD-cost:   23
c ---[30149]---> BDD-cost:   23
c ---[30147]---> BDD-cost:   23
c ---[30145]---> BDD-cost:   23
c ---[30143]---> BDD-cost:   23
c ---[30141]---> BDD-cost:   23
c ---[30139]---> BDD-cost:   23
c ---[30137]---> BDD-cost:   23
c ---[30135]---> BDD-cost:   23
c ---[30133]---> BDD-cost:   23
c ---[30131]---> BDD-cost:   23
c ---[30129]---> BDD-cost:   23
c ---[30127]---> BDD-cost:   23
c ---[30125]---> BDD-cost:   23
c ---[30123]---> BDD-cost:   23
c ---[30121]---> BDD-cost:   23
c ---[30119]---> BDD-cost:   23
c ---[30117]---> BDD-cost:   23
c ---[30115]---> BDD-cost:   23
c ---[30113]---> BDD-cost:   23
c ---[30111]---> BDD-cost:   23
c ---[30109]---> BDD-cost:   23
c ---[30107]---> BDD-cost:   23
c ---[30105]---> BDD-cost:   23
c ---[30103]---> BDD-cost:   23
c ---[30101]---> BDD-cost:   23
c ---[30099]---> BDD-cost:   23
c ---[30097]---> BDD-cost:   23
c ---[30095]---> BDD-cost:   23
c ---[30093]---> BDD-cost:   23
c ---[30091]---> BDD-cost:   23
c ---[30089]---> BDD-cost:   23
c ---[30087]---> BDD-cost:   23
c ---[30085]---> BDD-cost:   23
c ---[30083]---> BDD-cost:   23
c ---[30081]---> BDD-cost:   23
c ---[30079]---> BDD-cost:   23
c ---[30077]---> BDD-cost:   23
c ---[30075]---> BDD-cost:   23
c ---[30073]---> BDD-cost:   23
c ---[30071]---> BDD-cost:   23
c ---[30069]---> BDD-cost:   23
c ---[30067]---> BDD-cost:   23
c ---[30065]---> BDD-cost:   23
c ---[30063]---> BDD-cost:   23
c ---[30061]---> BDD-cost:   23
c ---[30059]---> BDD-cost:   23
c ---[30057]---> BDD-cost:   17
c ---[30055]---> BDD-cost:   17
c ---[30053]---> BDD-cost:   17
c ---[30051]---> BDD-cost:   17
c ---[30049]---> BDD-cost:   17
c ---[30047]---> BDD-cost:   17
c ---[30045]---> BDD-cost:   23
c ---[30043]---> BDD-cost:   23
c ---[30041]---> BDD-cost:   23
c ---[30039]---> BDD-cost:   23
c ---[30037]---> BDD-cost:   23
c ---[30035]---> BDD-cost:   23
c ---[30033]---> BDD-cost:   23
c ---[30031]---> BDD-cost:   23
c ---[30029]---> BDD-cost:   23
c ---[30027]---> BDD-cost:   23
c ---[30025]---> BDD-cost:   23
c ---[30023]---> BDD-cost:   23
c ---[30021]---> BDD-cost:   23
c ---[30019]---> BDD-cost:   23
c ---[30017]---> BDD-cost:   23
c ---[30015]---> BDD-cost:   23
c ---[30013]---> BDD-cost:   23
c ---[30011]---> BDD-cost:   23
c ---[30009]---> BDD-cost:   23
c ---[30007]---> BDD-cost:   23
c ---[30005]---> BDD-cost:   23
c ---[30003]---> BDD-cost:   23
c ---[30001]---> BDD-cost:   23
c ---[29999]---> BDD-cost:   23
c ---[29997]---> BDD-cost:   23
c ---[29995]---> BDD-cost:   23
c ---[29993]---> BDD-cost:   23
c ---[29991]---> BDD-cost:   23
c ---[29989]---> BDD-cost:   23
c ---[29987]---> BDD-cost:   23
c ---[29985]---> BDD-cost:   17
c ---[29983]---> BDD-cost:   17
c ---[29981]---> BDD-cost:   17
c ---[29979]---> BDD-cost:   17
c ---[29977]---> BDD-cost:   17
c ---[29975]---> BDD-cost:   17
c ---[29973]---> BDD-cost:   23
c ---[29971]---> BDD-cost:   23
c ---[29969]---> BDD-cost:   23
c ---[29967]---> BDD-cost:   23
c ---[29965]---> BDD-cost:   23
c ---[29963]---> BDD-cost:   23
c ---[29961]---> BDD-cost:   23
c ---[29959]---> BDD-cost:   23
c ---[29957]---> BDD-cost:   23
c ---[29955]---> BDD-cost:   23
c ---[29953]---> BDD-cost:   23
c ---[29951]---> BDD-cost:   23
c ---[29949]---> BDD-cost:   23
c ---[29947]---> BDD-cost:   23
c ---[29945]---> BDD-cost:   23
c ---[29943]---> BDD-cost:   23
c ---[29941]---> BDD-cost:   23
c ---[29939]---> BDD-cost:   23
c ---[29937]---> BDD-cost:   23
c ---[29935]---> BDD-cost:   23
c ---[29933]---> BDD-cost:   23
c ---[29931]---> BDD-cost:   23
c ---[29929]---> BDD-cost:   23
c ---[29927]---> BDD-cost:   23
c ---[29926]---> BDD-cost:    9
c ---[29925]---> BDD-cost:    9
c ---[29924]---> BDD-cost:    9
c ---[29923]---> BDD-cost:    9
c ---[29922]---> BDD-cost:    9
c ---[29921]---> BDD-cost:    9
c ---[29920]---> BDD-cost:    9
c ---[29919]---> BDD-cost:    9
c ---[29918]---> BDD-cost:    9
c ---[29917]---> BDD-cost:    9
c ---[29916]---> BDD-cost:    9
c ---[29915]---> BDD-cost:    9
c ---[29914]---> BDD-cost:    9
c ---[29913]---> BDD-cost:    9
c ---[29912]---> BDD-cost:    9
c ---[29911]---> BDD-cost:    9
c ---[29910]---> BDD-cost:    9
c ---[29909]---> BDD-cost:    9
c ---[29908]---> BDD-cost:    9
c ---[29907]---> BDD-cost:    9
c ---[29906]---> BDD-cost:    9
c ---[29905]---> BDD-cost:    9
c ---[29904]---> BDD-cost:    9
c ---[29903]---> BDD-cost:    9
c ---[29902]---> BDD-cost:    9
c ---[29901]---> BDD-cost:    9
c ---[29900]---> BDD-cost:    9
c ---[29899]---> BDD-cost:    9
c ---[29898]---> BDD-cost:    9
c ---[29897]---> BDD-cost:    9
c ---[29896]---> BDD-cost:    9
c ---[29895]---> BDD-cost:    9
c ---[29894]---> BDD-cost:    9
c ---[29893]---> BDD-cost:    9
c ---[29892]---> BDD-cost:    9
c ---[29891]---> BDD-cost:    9
c ---[29890]---> BDD-cost:    9
c ---[29889]---> BDD-cost:    9
c ---[29888]---> BDD-cost:    9
c ---[29887]---> BDD-cost:    9
c ---[29886]---> BDD-cost:    9
c ---[29885]---> BDD-cost:    9
c ---[29884]---> BDD-cost:    9
c ---[29883]---> BDD-cost:    9
c ---[29882]---> BDD-cost:    9
c ---[29881]---> BDD-cost:    9
c ---[29880]---> BDD-cost:    9
c ---[29879]---> BDD-cost:    9
c ---[29878]---> BDD-cost:    9
c ---[29877]---> BDD-cost:    9
c ---[29876]---> BDD-cost:    9
c ---[29875]---> BDD-cost:    9
c ---[29874]---> BDD-cost:    9
c ---[29873]---> BDD-cost:    9
c ---[29872]---> BDD-cost:    9
c ---[29871]---> BDD-cost:    9
c ---[29870]---> BDD-cost:    9
c ---[29869]---> BDD-cost:    9
c ---[29868]---> BDD-cost:    9
c ---[29867]---> BDD-cost:    9
c ---[29866]---> BDD-cost:    9
c ---[29865]---> BDD-cost:    9
c ---[29864]---> BDD-cost:    9
c ---[29863]---> BDD-cost:    9
c ---[29862]---> BDD-cost:    9
c ---[29861]---> BDD-cost:    9
c ---[29860]---> BDD-cost:    9
c ---[29859]---> BDD-cost:    9
c ---[29858]---> BDD-cost:    9
c ---[29857]---> BDD-cost:    9
c ---[29856]---> BDD-cost:    9
c ---[29855]---> BDD-cost:    9
c ---[29854]---> BDD-cost:    9
c ---[29853]---> BDD-cost:    9
c ---[29852]---> BDD-cost:    9
c ---[29851]---> BDD-cost:    9
c ---[29850]---> BDD-cost:    9
c ---[29849]---> BDD-cost:    9
c ---[29848]---> BDD-cost:    9
c ---[29847]---> BDD-cost:    9
c ---[29846]---> BDD-cost:    9
c ---[29845]---> BDD-cost:    9
c ---[29844]---> BDD-cost:    9
c ---[29843]---> BDD-cost:    9
c ---[29842]---> BDD-cost:    9
c ---[29841]---> BDD-cost:    9
c ---[29840]---> BDD-cost:    9
c ---[29839]---> BDD-cost:    9
c ---[29838]---> BDD-cost:    9
c ---[29837]---> BDD-cost:    9
c ---[29836]---> BDD-cost:    9
c ---[29835]---> BDD-cost:    9
c ---[29834]---> BDD-cost:    9
c ---[29833]---> BDD-cost:    9
c ---[29832]---> BDD-cost:    9
c ---[29831]---> BDD-cost:    9
c ---[29830]---> BDD-cost:    9
c ---[29829]---> BDD-cost:    9
c ---[29828]---> BDD-cost:    9
c ---[29827]---> BDD-cost:    9
c ---[29826]---> BDD-cost:    9
c ---[29825]---> BDD-cost:    9
c ---[29824]---> BDD-cost:    9
c ---[29823]---> BDD-cost:    9
c ---[29822]---> BDD-cost:    9
c ---[29821]---> BDD-cost:    9
c ---[29820]---> BDD-cost:    9
c ---[29819]---> BDD-cost:    9
c ---[29818]---> BDD-cost:    9
c ---[29817]---> BDD-cost:    9
c ---[29816]---> BDD-cost:    9
c ---[29815]---> BDD-cost:    9
c ---[29814]---> BDD-cost:    9
c ---[29813]---> BDD-cost:    9
c ---[29812]---> BDD-cost:    9
c ---[29811]---> BDD-cost:    9
c ---[29810]---> BDD-cost:    9
c ---[29809]---> BDD-cost:    9
c ---[29808]---> BDD-cost:    9
c ---[29807]---> BDD-cost:    9
c ---[29806]---> BDD-cost:    9
c ---[29805]---> BDD-cost:    9
c ---[29804]---> BDD-cost:    9
c ---[29803]---> BDD-cost:    9
c ---[29802]---> BDD-cost:    9
c ---[29801]---> BDD-cost:    9
c ---[29800]---> BDD-cost:    9
c ---[29799]---> BDD-cost:    9
c ---[29798]---> BDD-cost:    9
c ---[29797]---> BDD-cost:    9
c ---[29796]---> BDD-cost:    9
c ---[29795]---> BDD-cost:    9
c ---[29794]---> BDD-cost:    9
c ---[29793]---> BDD-cost:    9
c ---[29792]---> BDD-cost:    9
c ---[29791]---> BDD-cost:    9
c ---[29790]---> BDD-cost:    9
c ---[29789]---> BDD-cost:    9
c ---[29788]---> BDD-cost:    9
c ---[29787]---> BDD-cost:    9
c ---[29786]---> BDD-cost:    9
c ---[29785]---> BDD-cost:    9
c ---[29784]---> BDD-cost:    9
c ---[29783]---> BDD-cost:    9
c ---[29782]---> BDD-cost:    9
c ---[29781]---> BDD-cost:    9
c ---[29780]---> BDD-cost:    9
c ---[29779]---> BDD-cost:    9
c ---[29778]---> BDD-cost:    9
c ---[29777]---> BDD-cost:    9
c ---[29776]---> BDD-cost:    9
c ---[29775]---> BDD-cost:    9
c ---[29774]---> BDD-cost:    9
c ---[29773]---> BDD-cost:    9
c ---[29772]---> BDD-cost:    9
c ---[29771]---> BDD-cost:    9
c ---[29770]---> BDD-cost:    9
c ---[29769]---> BDD-cost:    9
c ---[29768]---> BDD-cost:    9
c ---[29767]---> BDD-cost:    9
c ---[29766]---> BDD-cost:    9
c ---[29765]---> BDD-cost:    9
c ---[29764]---> BDD-cost:    9
c ---[29763]---> BDD-cost:    9
c ---[29762]---> BDD-cost:    9
c ---[29761]---> BDD-cost:    9
c ---[29760]---> BDD-cost:    9
c ---[29759]---> BDD-cost:    9
c ---[29758]---> BDD-cost:    9
c ---[29757]---> BDD-cost:    9
c ---[29756]---> BDD-cost:    9
c ---[29755]---> BDD-cost:    9
c ---[29754]---> BDD-cost:    9
c ---[29753]---> BDD-cost:    9
c ---[29752]---> BDD-cost:    9
c ---[29751]---> BDD-cost:    9
c ---[29750]---> BDD-cost:    9
c ---[29749]---> BDD-cost:    9
c ---[29748]---> BDD-cost:    9
c ---[29747]---> BDD-cost:    9
c ---[29746]---> BDD-cost:    9
c ---[29745]---> BDD-cost:    9
c ---[29744]---> BDD-cost:    9
c ---[29743]---> BDD-cost:    9
c ---[29742]---> BDD-cost:    9
c ---[29741]---> BDD-cost:    9
c ---[29740]---> BDD-cost:    9
c ---[29739]---> BDD-cost:    9
c ---[29738]---> BDD-cost:    9
c ---[29737]---> BDD-cost:    9
c ---[29736]---> BDD-cost:    9
c ---[29735]---> BDD-cost:    9
c ---[29734]---> BDD-cost:    9
c ---[29733]---> BDD-cost:    9
c ---[29732]---> BDD-cost:    9
c ---[29731]---> BDD-cost:    9
c ---[29730]---> BDD-cost:    9
c ---[29729]---> BDD-cost:    9
c ---[29728]---> BDD-cost:    9
c ---[29727]---> BDD-cost:    9
c ---[29726]---> BDD-cost:    9
c ---[29725]---> BDD-cost:    9
c ---[29724]---> BDD-cost:    9
c ---[29723]---> BDD-cost:    9
c ---[29722]---> BDD-cost:    9
c ---[29721]---> BDD-cost:    9
c ---[29720]---> BDD-cost:    9
c ---[29719]---> BDD-cost:    9
c ---[29718]---> BDD-cost:    9
c ---[29717]---> BDD-cost:    9
c ---[29716]---> BDD-cost:    9
c ---[29715]---> BDD-cost:    9
c ---[29714]---> BDD-cost:    9
c ---[29713]---> BDD-cost:    9
c ---[29712]---> BDD-cost:    9
c ---[29711]---> BDD-cost:    9
c ---[29710]---> BDD-cost:    9
c ---[29709]---> BDD-cost:    9
c ---[29708]---> BDD-cost:    9
c ---[29707]---> BDD-cost:    9
c ---[29706]---> BDD-cost:    9
c ---[29705]---> BDD-cost:    9
c ---[29704]---> BDD-cost:    9
c ---[29703]---> BDD-cost:    9
c ---[29702]---> BDD-cost:    9
c ---[29701]---> BDD-cost:    9
c ---[29700]---> BDD-cost:    9
c ---[29699]---> BDD-cost:    9
c ---[29698]---> BDD-cost:    9
c ---[29697]---> BDD-cost:    9
c ---[29696]---> BDD-cost:    9
c ---[29695]---> BDD-cost:    9
c ---[29694]---> BDD-cost:    9
c ---[29693]---> BDD-cost:    9
c ---[29692]---> BDD-cost:    9
c ---[29691]---> BDD-cost:    9
c ---[29690]---> BDD-cost:    9
c ---[29689]---> BDD-cost:    9
c ---[29688]---> BDD-cost:    9
c ---[29687]---> BDD-cost:    9
c ---[29686]---> BDD-cost:    9
c ---[29685]---> BDD-cost:    9
c ---[29684]---> BDD-cost:    9
c ---[29683]---> BDD-cost:    9
c ---[29682]---> BDD-cost:    9
c ---[29681]---> BDD-cost:    9
c ---[29680]---> BDD-cost:    9
c ---[29679]---> BDD-cost:    9
c ---[29678]---> BDD-cost:    9
c ---[29677]---> BDD-cost:    9
c ---[29676]---> BDD-cost:    9
c ---[29675]---> BDD-cost:    9
c ---[29674]---> BDD-cost:    9
c ---[29673]---> BDD-cost:    9
c ---[29672]---> BDD-cost:    9
c ---[29671]---> BDD-cost:    9
c ---[29670]---> BDD-cost:    9
c ---[29669]---> BDD-cost:    9
c ---[29668]---> BDD-cost:    9
c ---[29667]---> BDD-cost:    9
c ---[29666]---> BDD-cost:    9
c ---[29665]---> BDD-cost:    9
c ---[29664]---> BDD-cost:    9
c ---[29663]---> BDD-cost:    9
c ---[29662]---> BDD-cost:    9
c ---[29661]---> BDD-cost:    9
c ---[29660]---> BDD-cost:    9
c ---[29659]---> BDD-cost:    9
c ---[29658]---> BDD-cost:    9
c ---[29657]---> BDD-cost:    9
c ---[29656]---> BDD-cost:    9
c ---[29655]---> BDD-cost:    9
c ---[29654]---> BDD-cost:    9
c ---[29653]---> BDD-cost:    9
c ---[29652]---> BDD-cost:    9
c ---[29651]---> BDD-cost:    9
c ---[29650]---> BDD-cost:    9
c ---[29649]---> BDD-cost:    9
c ---[29648]---> BDD-cost:    9
c ---[29647]---> BDD-cost:    9
c ---[29646]---> BDD-cost:    9
c ---[29645]---> BDD-cost:    9
c ---[29644]---> BDD-cost:    9
c ---[29643]---> BDD-cost:    9
c ---[29642]---> BDD-cost:    9
c ---[29641]---> BDD-cost:    9
c ---[29640]---> BDD-cost:    9
c ---[29639]---> BDD-cost:    9
c ---[29638]---> BDD-cost:    9
c ---[29637]---> BDD-cost:    9
c ---[29636]---> BDD-cost:    9
c ---[29635]---> BDD-cost:    9
c ---[29634]---> BDD-cost:    9
c ---[29633]---> BDD-cost:    9
c ---[29632]---> BDD-cost:    9
c ---[29631]---> BDD-cost:    9
c ---[29630]---> BDD-cost:    9
c ---[29629]---> BDD-cost:    9
c ---[29628]---> BDD-cost:    9
c ---[29627]---> BDD-cost:    9
c ---[29626]---> BDD-cost:    9
c ---[29625]---> BDD-cost:    9
c ---[29624]---> BDD-cost:    9
c ---[29623]---> BDD-cost:    9
c ---[29622]---> BDD-cost:    9
c ---[29621]---> BDD-cost:    9
c ---[29620]---> BDD-cost:    9
c ---[29619]---> BDD-cost:    9
c ---[29618]---> BDD-cost:    9
c ---[29617]---> BDD-cost:    9
c ---[29616]---> BDD-cost:    9
c ---[29615]---> BDD-cost:    9
c ---[29614]---> BDD-cost:    9
c ---[29613]---> BDD-cost:    9
c ---[29612]---> BDD-cost:    9
c ---[29611]---> BDD-cost:    9
c ---[29610]---> BDD-cost:    9
c ---[29609]---> BDD-cost:    9
c ---[29608]---> BDD-cost:    9
c ---[29607]---> BDD-cost:    9
c ---[29606]---> BDD-cost:    9
c ---[29605]---> BDD-cost:    9
c ---[29604]---> BDD-cost:    9
c ---[29603]---> BDD-cost:    9
c ---[29602]---> BDD-cost:    9
c ---[29601]---> BDD-cost:    9
c ---[29600]---> BDD-cost:    9
c ---[29599]---> BDD-cost:    9
c ---[29598]---> BDD-cost:    9
c ---[29597]---> BDD-cost:    9
c ---[29596]---> BDD-cost:    9
c ---[29595]---> BDD-cost:    9
c ---[29594]---> BDD-cost:    9
c ---[29593]---> BDD-cost:    9
c ---[29592]---> BDD-cost:    9
c ---[29591]---> BDD-cost:    9
c ---[29590]---> BDD-cost:    9
c ---[29589]---> BDD-cost:    9
c ---[29588]---> BDD-cost:    9
c ---[29587]---> BDD-cost:    9
c ---[29586]---> BDD-cost:    9
c ---[29585]---> BDD-cost:    9
c ---[29584]---> BDD-cost:    9
c ---[29583]---> BDD-cost:    9
c ---[29582]---> BDD-cost:    9
c ---[29581]---> BDD-cost:    9
c ---[29580]---> BDD-cost:    9
c ---[29579]---> BDD-cost:    9
c ---[29578]---> BDD-cost:    9
c ---[29577]---> BDD-cost:    9
c ---[29576]---> BDD-cost:    9
c ---[29575]---> BDD-cost:    9
c ---[29574]---> BDD-cost:    9
c ---[29573]---> BDD-cost:    9
c ---[29572]---> BDD-cost:    9
c ---[29571]---> BDD-cost:    9
c ---[29570]---> BDD-cost:    9
c ---[29569]---> BDD-cost:    9
c ---[29568]---> BDD-cost:    9
c ---[29567]---> BDD-cost:    9
c ---[29566]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:    9
c ---[ 402]---> BDD-cost:    9
c ---[ 401]---> BDD-cost:    9
c ---[ 400]---> BDD-cost:    9
c ---[ 399]---> BDD-cost:    9
c ---[ 398]---> BDD-cost:    9
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    9
c ---[ 395]---> BDD-cost:    9
c ---[ 394]---> BDD-cost:    9
c ---[ 393]---> BDD-cost:    9
c ---[ 392]---> BDD-cost:    9
c ---[ 391]---> BDD-cost:    9
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:    9
c ---[ 386]---> BDD-cost:    9
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    9
c ---[ 383]---> BDD-cost:    9
c ---[ 382]---> BDD-cost:    9
c ---[ 381]---> BDD-cost:    9
c ---[ 380]---> BDD-cost:    9
c ---[ 379]---> BDD-cost:    9
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    9
c ---[ 375]---> BDD-cost:    9
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 372]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:    9
c ---[ 369]---> BDD-cost:    9
c ---[ 368]---> BDD-cost:    9
c ---[ 367]---> BDD-cost:    9
c ---[ 366]---> BDD-cost:    9
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:    9
c ---[ 362]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    9
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:    9
c ---[ 354]---> BDD-cost:    9
c ---[ 353]---> BDD-cost:    9
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    9
c ---[ 350]---> BDD-cost:    9
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:    9
c ---[ 347]---> BDD-cost:    9
c ---[ 346]---> BDD-cost:    9
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    9
c ---[ 343]---> BDD-cost:    9
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:    9
c ---[ 338]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    9
c ---[ 336]---> BDD-cost:    9
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:    9
c ---[ 332]---> BDD-cost:    9
c ---[ 331]---> BDD-cost:    9
c ---[ 330]---> BDD-cost:    9
c ---[ 329]---> BDD-cost:    9
c ---[ 328]---> BDD-cost:    9
c ---[ 327]---> BDD-cost:    9
c ---[ 326]---> BDD-cost:    9
c ---[ 325]---> BDD-cost:    9
c ---[ 324]---> BDD-cost:    9
c ---[ 323]---> BDD-cost:    9
c ---[ 322]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    9
c ---[ 320]---> BDD-cost:    9
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    9
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    9
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    9
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:    9
c ---[ 306]---> BDD-cost:    9
c ---[ 305]---> BDD-cost:    9
c ---[ 304]---> BDD-cost:    9
c ---[ 303]---> BDD-cost:    9
c ---[ 302]---> BDD-cost:    9
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    9
c ---[ 297]---> BDD-cost:    9
c ---[ 296]---> BDD-cost:    9
c ---[ 295]---> BDD-cost:    9
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:    9
c ---[ 290]---> BDD-cost:    9
c ---[ 289]---> BDD-cost:    9
c ---[ 288]---> BDD-cost:    9
c ---[ 287]---> BDD-cost:    9
c ---[ 286]---> BDD-cost:    9
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    9
c ---[ 281]---> BDD-cost:    9
c ---[ 280]---> BDD-cost:    9
c ---[ 279]---> BDD-cost:    9
c ---[ 278]---> BDD-cost:    9
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    9
c ---[ 273]---> BDD-cost:    9
c ---[ 272]---> BDD-cost:    9
c ---[ 271]---> BDD-cost:    9
c ---[ 270]---> BDD-cost:    9
c ---[ 269]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:    9
c ---[ 267]---> BDD-cost:    9
c ---[ 266]---> BDD-cost:    9
c ---[ 265]---> BDD-cost:    9
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    9
c ---[ 257]---> BDD-cost:    9
c ---[ 256]---> BDD-cost:    9
c ---[ 255]---> BDD-cost:    9
c ---[ 254]---> BDD-cost:    9
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:    9
c ---[ 249]---> BDD-cost:    9
c ---[ 248]---> BDD-cost:    9
c ---[ 247]---> BDD-cost:    9
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:    9
c ---[ 241]---> BDD-cost:    9
c ---[ 240]---> BDD-cost:    9
c ---[ 239]---> BDD-cost:    9
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:    9
c ---[ 236]---> BDD-cost:    9
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:    9
c ---[ 233]---> BDD-cost:    9
c ---[ 232]---> BDD-cost:    9
c ---[ 231]---> BDD-cost:    9
c ---[ 230]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:    9
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:    9
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:    9
c ---[ 222]---> BDD-cost:    9
c ---[ 221]---> BDD-cost:    9
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:    9
c ---[ 218]---> BDD-cost:    9
c ---[ 217]---> BDD-cost:    9
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:    9
c ---[ 209]---> BDD-cost:    9
c ---[ 208]---> BDD-cost:    9
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:    9
c ---[ 204]---> BDD-cost:    9
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:    9
c ---[ 201]---> BDD-cost:    9
c ---[ 200]---> BDD-cost:    9
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:    9
c ---[ 194]---> BDD-cost:    9
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:    9
c ---[ 191]---> BDD-cost:    9
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:    9
c ---[ 188]---> BDD-cost:    9
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:    9
c ---[ 185]---> BDD-cost:    9
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:    9
c ---[ 182]---> BDD-cost:    9
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:    9
c ---[ 178]---> BDD-cost:    9
c ---[ 177]---> BDD-cost:    9
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:    9
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:    9
c ---[ 170]---> BDD-cost:    9
c ---[ 169]---> BDD-cost:    9
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    9
c ---[ 159]---> BDD-cost:    9
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    9
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:    9
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:    9
c ---[ 146]---> BDD-cost:    9
c ---[ 145]---> BDD-cost:    9
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:    9
c ---[ 142]---> BDD-cost:    9
c ---[ 141]---> BDD-cost:    9
c ---[ 140]---> BDD-cost:    9
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    9
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    9
c ---[ 134]---> BDD-cost:    9
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:    9
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    9
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:    9
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:    9
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:    9
c ---[ 108]---> BDD-cost:    9
c ---[ 107]---> BDD-cost:    9
c ---[ 106]---> BDD-cost:    9
c ---[ 105]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:    9
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    9
c ---[  98]---> BDD-cost:    9
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    9
c ---[  93]---> BDD-cost:    9
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:    9
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:    9
c ---[  87]---> BDD-cost:    9
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:    9
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:    9
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:    9
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    9
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:    9
c ---[  64]---> BDD-cost:    9
c ---[  63]---> BDD-cost:    9
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:    9
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:    9
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    9
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:    9
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:    9
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:    9
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:    9
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:    9
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:    9
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:    9
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    9
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  118866   331288 |   39622       0        0     nan |  0.000 % |
c |       100 |  118587   330538 |   43584      42      212     5.0 |  4.138 % |
c |       250 |  118437   330088 |   47942     145      689     4.8 |  4.252 % |
c |       475 |  118095   329259 |   52736     312     1525     4.9 |  4.584 % |
c |       812 |  117970   328884 |   58010     595     2945     4.9 |  4.680 % |
c |      1318 |  117748   328334 |   63811    1051     6157     5.9 |  4.924 % |
c |      2077 |  117587   327856 |   70192    1739    12288     7.1 |  5.050 % |
c |      3217 |  117423   327419 |   77212    2684    41225    15.4 |  5.195 % |
c |      4926 |  117294   327056 |   84933    4130    96944    23.5 |  5.306 % |
c |      7488 |  116924   326012 |   93426    6433   145105    22.6 |  5.611 % |
c |     11333 |  116634   325214 |  102769   10035   271236    27.0 |  5.863 % |
c |     17099 |  116286   324207 |  113046   15565   441974    28.4 |  6.149 % |
c |     25751 |  115754   322709 |  124350   23872   753168    31.6 |  6.603 % |
c |     38726 |  115060   320795 |  136785   36166  1168768    32.3 |  7.210 % |
c |     58188 |  114352   318898 |  150464   55328  1920030    34.7 |  7.848 % |
c |     87382 |  113964   317783 |  165510   84301  3103794    36.8 |  8.172 % |
c |    131173 |  113134   315592 |  182062  127681  4880522    38.2 |  8.966 % |
c |    196857 |  111778   311868 |  200268   28168   859698    30.5 | 10.180 % |
c |    295383 |  109620   305945 |  220295  125832  4485320    35.6 | 12.107 % |
c |    443172 |  107441   300084 |  242324   70813  2471061    34.9 | 14.168 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 2029
Raw data (stat): 2029 (runsolver) R 2028 26667 26666 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 410133515 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.0012 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 3196 0 0 0 991 8 0 0 25 0 1 0 410133515 14712832 3128 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3592 3128 603 41 0 3551 0
vsize: 14368
[startup+20.0015 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 3481 0 0 0 1990 9 0 0 25 0 1 0 410133515 15925248 3413 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3888 3413 603 41 0 3847 0
vsize: 15552
[startup+30.0023 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 3962 0 0 0 2988 11 0 0 25 0 1 0 410133515 17907712 3894 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4372 3894 603 41 0 4331 0
vsize: 17488
[startup+40.0026 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 4203 0 0 0 3986 12 0 0 25 0 1 0 410133515 18849792 4135 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4602 4135 603 41 0 4561 0
vsize: 18408
[startup+50.0029 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 4527 0 0 0 4985 14 0 0 25 0 1 0 410133515 20328448 4459 4294967295 134512640 134672761 3221224560 3221223716 134561241 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4963 4459 603 41 0 4922 0
vsize: 19852
[startup+60.0027 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 4750 0 0 0 5984 14 0 0 25 0 1 0 410133515 21270528 4682 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5193 4682 603 41 0 5152 0
vsize: 20772
[startup+70.0028 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 5174 0 0 0 6982 16 0 0 25 0 1 0 410133515 22884352 5106 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5587 5106 603 41 0 5546 0
vsize: 22348
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 5544 0 0 0 7981 18 0 0 25 0 1 0 410133515 24363008 5476 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5948 5476 603 41 0 5907 0
vsize: 23792
[startup+90.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 5967 0 0 0 8979 20 0 0 25 0 1 0 410133515 26120192 5899 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6377 5899 603 41 0 6336 0
vsize: 25508
[startup+100.003 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 6232 0 0 0 9978 21 0 0 25 0 1 0 410133515 27459584 6164 4294967295 134512640 134672761 3221224560 3221223732 134556641 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6704 6164 603 41 0 6663 0
vsize: 26816
[startup+110.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 6503 0 0 0 10977 22 0 0 25 0 1 0 410133515 28536832 6435 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6967 6435 603 41 0 6926 0
vsize: 27868
[startup+120.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 6841 0 0 0 11976 23 0 0 25 0 1 0 410133515 29880320 6773 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7295 6773 603 41 0 7254 0
vsize: 29180
[startup+130.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 7098 0 0 0 12975 24 0 0 25 0 1 0 410133515 30953472 7030 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7557 7030 603 41 0 7516 0
vsize: 30228
[startup+140.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 7348 0 0 0 13974 25 0 0 25 0 1 0 410133515 31895552 7280 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7787 7280 603 41 0 7746 0
vsize: 31148
[startup+150.005 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 7644 0 0 0 14972 27 0 0 25 0 1 0 410133515 33107968 7576 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8083 7576 603 41 0 8042 0
vsize: 32332
[startup+160.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 7821 0 0 0 15971 27 0 0 25 0 1 0 410133515 33783808 7753 4294967295 134512640 134672761 3221224560 3221223728 134560803 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8248 7753 603 41 0 8207 0
vsize: 32992
[startup+170.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 8130 0 0 0 16970 29 0 0 25 0 1 0 410133515 35123200 8062 4294967295 134512640 134672761 3221224560 3221223696 134560632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8575 8062 603 41 0 8534 0
vsize: 34300
[startup+180.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 8340 0 0 0 17969 29 0 0 25 0 1 0 410133515 35930112 8272 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8772 8272 603 41 0 8731 0
vsize: 35088
[startup+190.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 8584 0 0 0 18968 31 0 0 25 0 1 0 410133515 36872192 8516 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9002 8516 603 41 0 8961 0
vsize: 36008
[startup+200.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 8787 0 0 0 19967 31 0 0 25 0 1 0 410133515 37683200 8719 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9200 8719 603 41 0 9159 0
vsize: 36800
[startup+210.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2029
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 8967 0 0 0 20966 33 0 0 25 0 1 0 410133515 38502400 8899 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9400 8899 603 41 0 9359 0
vsize: 37600
[startup+220.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 9082 0 0 0 21965 33 0 0 25 0 1 0 410133515 38903808 9014 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9498 9014 603 41 0 9457 0
vsize: 37992
[startup+230.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 9282 0 0 0 22964 34 0 0 25 0 1 0 410133515 39710720 9214 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9695 9214 603 41 0 9654 0
vsize: 38780
[startup+240.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 9456 0 0 0 23963 35 0 0 25 0 1 0 410133515 40386560 9388 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9860 9388 603 41 0 9819 0
vsize: 39440
[startup+250.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 9560 0 0 0 24963 35 0 0 25 0 1 0 410133515 40919040 9492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9990 9492 603 41 0 9949 0
vsize: 39960
[startup+260.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 9765 0 0 0 25961 36 0 0 25 0 1 0 410133515 42258432 9697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10317 9697 603 41 0 10276 0
vsize: 41268
[startup+270.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 9892 0 0 0 26961 37 0 0 25 0 1 0 410133515 42663936 9824 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10416 9824 603 41 0 10375 0
vsize: 41664
[startup+280.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 9997 0 0 0 27960 38 0 0 25 0 1 0 410133515 43196416 9929 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10546 9929 603 41 0 10505 0
vsize: 42184
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 10264 0 0 0 28960 39 0 0 25 0 1 0 410133515 44261376 10196 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10806 10196 603 41 0 10765 0
vsize: 43224
[startup+300.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 10471 0 0 0 29959 39 0 0 25 0 1 0 410133515 45051904 10403 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10999 10403 603 41 0 10958 0
vsize: 43996
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 10686 0 0 0 30959 40 0 0 25 0 1 0 410133515 46002176 10618 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11231 10618 603 41 0 11190 0
vsize: 44924
[startup+320.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 10848 0 0 0 31958 41 0 0 25 0 1 0 410133515 46542848 10780 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11363 10780 603 41 0 11322 0
vsize: 45452
[startup+330.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 10953 0 0 0 32958 41 0 0 25 0 1 0 410133515 47091712 10885 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11497 10885 603 41 0 11456 0
vsize: 45988
[startup+340.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 10956 0 0 0 33958 41 0 0 25 0 1 0 410133515 47091712 10888 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11497 10888 603 41 0 11456 0
vsize: 45988
[startup+350.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 11078 0 0 0 34958 42 0 0 25 0 1 0 410133515 47489024 11010 4294967295 134512640 134672761 3221224560 3221223664 134560492 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11594 11010 603 41 0 11553 0
vsize: 46376
[startup+360.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 11208 0 0 0 35958 42 0 0 25 0 1 0 410133515 48037888 11140 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11728 11140 603 41 0 11687 0
vsize: 46912
[startup+370.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 11361 0 0 0 36957 42 0 0 25 0 1 0 410133515 48701440 11293 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11890 11293 603 41 0 11849 0
vsize: 47560
[startup+380.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 11511 0 0 0 37957 43 0 0 25 0 1 0 410133515 49238016 11443 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12021 11443 603 41 0 11980 0
vsize: 48084
[startup+390.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 11707 0 0 0 38956 44 0 0 25 0 1 0 410133515 50044928 11639 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12218 11639 603 41 0 12177 0
vsize: 48872
[startup+400.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 11812 0 0 0 39956 44 0 0 25 0 1 0 410133515 50450432 11744 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12317 11744 603 41 0 12276 0
vsize: 49268
[startup+410.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 11917 0 0 0 40956 44 0 0 25 0 1 0 410133515 51003392 11849 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12452 11849 603 41 0 12411 0
vsize: 49808
[startup+420.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12069 0 0 0 41956 45 0 0 25 0 1 0 410133515 51539968 12001 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12583 12001 603 41 0 12542 0
vsize: 50332
[startup+430.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12229 0 0 0 42955 46 0 0 25 0 1 0 410133515 52207616 12161 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12746 12161 603 41 0 12705 0
vsize: 50984
[startup+440.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12375 0 0 0 43955 46 0 0 25 0 1 0 410133515 52875264 12307 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12909 12307 603 41 0 12868 0
vsize: 51636
[startup+450.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12556 0 0 0 44955 46 0 0 25 0 1 0 410133515 53571584 12488 4294967295 134512640 134672761 3221224560 3221223684 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13079 12488 603 41 0 13038 0
vsize: 52316
[startup+460.01 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12608 0 0 0 45955 46 0 0 25 0 1 0 410133515 53706752 12540 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12540 603 41 0 13071 0
vsize: 52448
[startup+470.011 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12608 0 0 0 46955 46 0 0 25 0 1 0 410133515 53706752 12540 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13112 12540 603 41 0 13071 0
vsize: 52448
[startup+480.012 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12608 0 0 0 47955 46 0 0 25 0 1 0 410133515 53706752 12540 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12540 603 41 0 13071 0
vsize: 52448
[startup+490.012 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12608 0 0 0 48955 46 0 0 25 0 1 0 410133515 53706752 12540 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12540 603 41 0 13071 0
vsize: 52448
[startup+500.011 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12608 0 0 0 49955 46 0 0 25 0 1 0 410133515 53706752 12540 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12540 603 41 0 13071 0
vsize: 52448
[startup+510.012 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12608 0 0 0 50955 46 0 0 25 0 1 0 410133515 53706752 12540 4294967295 134512640 134672761 3221224560 3221223732 134556618 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12540 603 41 0 13071 0
vsize: 52448
[startup+520.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12609 0 0 0 51955 46 0 0 25 0 1 0 410133515 53706752 12541 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12541 603 41 0 13071 0
vsize: 52448
[startup+530.012 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12609 0 0 0 52955 46 0 0 25 0 1 0 410133515 53706752 12541 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12541 603 41 0 13071 0
vsize: 52448
[startup+540.013 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12609 0 0 0 53956 47 0 0 25 0 1 0 410133515 53706752 12541 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12541 603 41 0 13071 0
vsize: 52448
[startup+550.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12609 0 0 0 54956 47 0 0 25 0 1 0 410133515 53706752 12541 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12541 603 41 0 13071 0
vsize: 52448
[startup+560.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12610 0 0 0 55956 47 0 0 25 0 1 0 410133515 53706752 12542 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12542 603 41 0 13071 0
vsize: 52448
[startup+570.013 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12610 0 0 0 56956 47 0 0 25 0 1 0 410133515 53706752 12542 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12542 603 41 0 13071 0
vsize: 52448
[startup+580.012 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12611 0 0 0 57956 47 0 0 25 0 1 0 410133515 53706752 12543 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12543 603 41 0 13071 0
vsize: 52448
[startup+590.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12611 0 0 0 58956 47 0 0 25 0 1 0 410133515 53706752 12543 4294967295 134512640 134672761 3221224560 3221223728 134560871 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12543 603 41 0 13071 0
vsize: 52448
[startup+600.012 s]
Raw data (loadavg): 1.08 1.00 0.92 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12611 0 0 0 59957 47 0 0 25 0 1 0 410133515 53706752 12543 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12543 603 41 0 13071 0
vsize: 52448
[startup+610.013 s]
Raw data (loadavg): 1.07 1.00 0.92 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12612 0 0 0 60957 47 0 0 25 0 1 0 410133515 53706752 12544 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12544 603 41 0 13071 0
vsize: 52448
[startup+620.013 s]
Raw data (loadavg): 1.06 1.00 0.92 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12612 0 0 0 61957 47 0 0 25 0 1 0 410133515 53706752 12544 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12544 603 41 0 13071 0
vsize: 52448
[startup+630.013 s]
Raw data (loadavg): 1.05 1.00 0.92 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12612 0 0 0 62957 47 0 0 25 0 1 0 410133515 53706752 12544 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12544 603 41 0 13071 0
vsize: 52448
[startup+640.013 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12613 0 0 0 63957 47 0 0 25 0 1 0 410133515 53706752 12545 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12545 603 41 0 13071 0
vsize: 52448
[startup+650.013 s]
Raw data (loadavg): 1.04 1.00 0.92 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12613 0 0 0 64958 47 0 0 25 0 1 0 410133515 53706752 12545 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12545 603 41 0 13071 0
vsize: 52448
[startup+660.014 s]
Raw data (loadavg): 1.11 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12613 0 0 0 65958 47 0 0 25 0 1 0 410133515 53706752 12545 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12545 603 41 0 13071 0
vsize: 52448
[startup+670.013 s]
Raw data (loadavg): 1.17 1.03 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12614 0 0 0 66958 47 0 0 25 0 1 0 410133515 53706752 12546 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12546 603 41 0 13071 0
vsize: 52448
[startup+680.014 s]
Raw data (loadavg): 1.14 1.03 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12614 0 0 0 67958 47 0 0 25 0 1 0 410133515 53706752 12546 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12546 603 41 0 13071 0
vsize: 52448
[startup+690.014 s]
Raw data (loadavg): 1.12 1.03 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12614 0 0 0 68958 47 0 0 25 0 1 0 410133515 53706752 12546 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12546 603 41 0 13071 0
vsize: 52448
[startup+700.014 s]
Raw data (loadavg): 1.10 1.03 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12614 0 0 0 69958 47 0 0 25 0 1 0 410133515 53706752 12546 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12546 603 41 0 13071 0
vsize: 52448
[startup+710.015 s]
Raw data (loadavg): 1.08 1.03 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12615 0 0 0 70958 47 0 0 25 0 1 0 410133515 53706752 12547 4294967295 134512640 134672761 3221224560 3221223664 134559784 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12547 603 41 0 13071 0
vsize: 52448
[startup+720.015 s]
Raw data (loadavg): 1.07 1.03 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12615 0 0 0 71958 47 0 0 25 0 1 0 410133515 53706752 12547 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12547 603 41 0 13071 0
vsize: 52448
[startup+730.015 s]
Raw data (loadavg): 1.06 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12615 0 0 0 72958 47 0 0 25 0 1 0 410133515 53706752 12547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12547 603 41 0 13071 0
vsize: 52448
[startup+740.015 s]
Raw data (loadavg): 1.05 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12616 0 0 0 73958 47 0 0 25 0 1 0 410133515 53706752 12548 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12548 603 41 0 13071 0
vsize: 52448
[startup+750.015 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12617 0 0 0 74959 47 0 0 25 0 1 0 410133515 53706752 12549 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12549 603 41 0 13071 0
vsize: 52448
[startup+760.014 s]
Raw data (loadavg): 1.04 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12619 0 0 0 75959 47 0 0 25 0 1 0 410133515 53706752 12551 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12551 603 41 0 13071 0
vsize: 52448
[startup+770.014 s]
Raw data (loadavg): 1.03 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12620 0 0 0 76959 47 0 0 25 0 1 0 410133515 53706752 12552 4294967295 134512640 134672761 3221224560 3221223696 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12552 603 41 0 13071 0
vsize: 52448
[startup+780.015 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12621 0 0 0 77959 47 0 0 25 0 1 0 410133515 53706752 12553 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12553 603 41 0 13071 0
vsize: 52448
[startup+790.015 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12622 0 0 0 78959 47 0 0 25 0 1 0 410133515 53706752 12554 4294967295 134512640 134672761 3221224560 3221223728 134560970 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12554 603 41 0 13071 0
vsize: 52448
[startup+800.015 s]
Raw data (loadavg): 1.02 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12622 0 0 0 79959 47 0 0 25 0 1 0 410133515 53706752 12554 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12554 603 41 0 13071 0
vsize: 52448
[startup+810.015 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12622 0 0 0 80960 47 0 0 25 0 1 0 410133515 53706752 12554 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12554 603 41 0 13071 0
vsize: 52448
[startup+820.015 s]
Raw data (loadavg): 1.01 1.02 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12622 0 0 0 81960 47 0 0 25 0 1 0 410133515 53706752 12554 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12554 603 41 0 13071 0
vsize: 52448
[startup+830.015 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12622 0 0 0 82960 47 0 0 25 0 1 0 410133515 53706752 12554 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12554 603 41 0 13071 0
vsize: 52448
[startup+840.015 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12623 0 0 0 83960 47 0 0 25 0 1 0 410133515 53706752 12555 4294967295 134512640 134672761 3221224560 3221223776 134561979 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12555 603 41 0 13071 0
vsize: 52448
[startup+850.014 s]
Raw data (loadavg): 1.01 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12623 0 0 0 84960 47 0 0 25 0 1 0 410133515 53706752 12555 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12555 603 41 0 13071 0
vsize: 52448
[startup+860.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12623 0 0 0 85960 47 0 0 25 0 1 0 410133515 53706752 12555 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12555 603 41 0 13071 0
vsize: 52448
[startup+870.014 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12623 0 0 0 86961 47 0 0 25 0 1 0 410133515 53706752 12555 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12555 603 41 0 13071 0
vsize: 52448
[startup+880.014 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12624 0 0 0 87961 47 0 0 25 0 1 0 410133515 53706752 12556 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13112 12556 603 41 0 13071 0
vsize: 52448
[startup+890.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12636 0 0 0 88961 47 0 0 25 0 1 0 410133515 53903360 12568 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13160 12568 603 41 0 13119 0
vsize: 52640
[startup+900.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12636 0 0 0 89961 47 0 0 25 0 1 0 410133515 53903360 12568 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13160 12568 603 41 0 13119 0
vsize: 52640
[startup+910.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12636 0 0 0 90961 47 0 0 25 0 1 0 410133515 53903360 12568 4294967295 134512640 134672761 3221224560 3221223728 134560895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13160 12568 603 41 0 13119 0
vsize: 52640
[startup+920.015 s]
Raw data (loadavg): 1.00 1.01 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12637 0 0 0 91962 47 0 0 25 0 1 0 410133515 53903360 12569 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13160 12569 603 41 0 13119 0
vsize: 52640
[startup+930.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12660 0 0 0 92962 47 0 0 25 0 1 0 410133515 53903360 12592 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13160 12592 603 41 0 13119 0
vsize: 52640
[startup+940.015 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12800 0 0 0 93961 48 0 0 25 0 1 0 410133515 54566912 12732 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13322 12732 603 41 0 13281 0
vsize: 53288
[startup+950.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 12900 0 0 0 94961 48 0 0 25 0 1 0 410133515 54972416 12832 4294967295 134512640 134672761 3221224560 3221223744 134556675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13421 12832 603 41 0 13380 0
vsize: 53684
[startup+960.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 13029 0 0 0 95961 48 0 0 25 0 1 0 410133515 55533568 12961 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13558 12961 603 41 0 13517 0
vsize: 54232
[startup+970.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 13131 0 0 0 96961 49 0 0 25 0 1 0 410133515 55930880 13063 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13655 13063 603 41 0 13614 0
vsize: 54620
[startup+980.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 13208 0 0 0 97961 49 0 0 25 0 1 0 410133515 56201216 13140 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13721 13140 603 41 0 13680 0
vsize: 54884
[startup+990.016 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 13348 0 0 0 98961 49 0 0 25 0 1 0 410133515 56868864 13280 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13884 13280 603 41 0 13843 0
vsize: 55536
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 13440 0 0 0 99960 49 0 0 25 0 1 0 410133515 57139200 13372 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13950 13372 603 41 0 13909 0
vsize: 55800
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 13590 0 0 0 100960 50 0 0 25 0 1 0 410133515 57815040 13522 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14115 13522 603 41 0 14074 0
vsize: 56460
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 13728 0 0 0 101960 50 0 0 25 0 1 0 410133515 58351616 13660 4294967295 134512640 134672761 3221224560 3221223728 134560797 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14246 13660 603 41 0 14205 0
vsize: 56984
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 13904 0 0 0 102960 50 0 0 25 0 1 0 410133515 59158528 13836 4294967295 134512640 134672761 3221224560 3221223664 134560523 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14443 13836 603 41 0 14402 0
vsize: 57772
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14013 0 0 0 103960 51 0 0 25 0 1 0 410133515 59564032 13945 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14542 13945 603 41 0 14501 0
vsize: 58168
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14105 0 0 0 104960 51 0 0 25 0 1 0 410133515 59969536 14037 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14641 14037 603 41 0 14600 0
vsize: 58564
[startup+1060.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14211 0 0 0 105960 51 0 0 25 0 1 0 410133515 60370944 14143 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14739 14143 603 41 0 14698 0
vsize: 58956
[startup+1070.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14245 0 0 0 106960 51 0 0 25 0 1 0 410133515 60514304 14177 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14774 14177 603 41 0 14733 0
vsize: 59096
[startup+1080.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14367 0 0 0 107960 52 0 0 25 0 1 0 410133515 61050880 14299 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14905 14299 603 41 0 14864 0
vsize: 59620
[startup+1090.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14446 0 0 0 108960 52 0 0 25 0 1 0 410133515 61317120 14378 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14970 14378 603 41 0 14929 0
vsize: 59880
[startup+1100.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14508 0 0 0 109959 52 0 0 25 0 1 0 410133515 61587456 14440 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15036 14440 603 41 0 14995 0
vsize: 60144
[startup+1110.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 110959 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221222288 134565868 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1120.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 111959 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1130.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 112960 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1140.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 113960 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1150.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 114960 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1160.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 115960 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1170.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 116960 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223696 134560709 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1180.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 117960 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1190.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 118960 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
[startup+1200.02 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 2031
Raw data (stat): 2029 (minisat+) R 2028 26667 26666 0 -1 0 14648 0 0 0 119960 53 0 0 25 0 1 0 410133515 62255104 14580 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15199 14580 603 41 0 15158 0
vsize: 60796
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 2031
Raw data (stat): 2029 (minisat+) Z 2028 26667 26666 0 -1 12 14650 0 0 0 119960 56 0 0 25 0 1 0 410133515 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.17
CPU user time (s): 1199.61
CPU system time (s): 0.563914
CPU usage (%): 100.01
Max. virtual memory (Kb): 60796
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####