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 6035

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.085
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:      1034724 kB
MemFree:        701092 kB
Buffers:         35244 kB
Cached:         186448 kB
SwapCached:       1212 kB
Active:         147728 kB
Inactive:       154316 kB
HighTotal:      131072 kB
HighFree:          256 kB
LowTotal:       903652 kB
LowFree:        700836 kB
SwapTotal:     2097892 kB
SwapFree:      2096680 kB
Dirty:            2340 kB
Writeback:           0 kB
Mapped:          81768 kB
Slab:            25756 kB
Committed_AS:   174000 kB
PageTables:        432 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 03:31:58 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 4495 7 1200.26 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]---> BDD-cost:  151
c ---[30297]---> BDD-cost:  151
c ---[30296]---> BDD-cost:  151
c ---[30295]---> BDD-cost:  151
c ---[30294]---> BDD-cost:  151
c ---[30293]---> BDD-cost:  151
c ---[30292]---> BDD-cost:  151
c ---[30291]---> BDD-cost:  151
c ---[30290]---> BDD-cost:  151
c ---[30289]---> BDD-cost:  151
c ---[30288]---> BDD-cost:  151
c ---[30287]---> BDD-cost:  151
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 |   75483   211391 |   25161       0        0     nan |  0.000 % |
c |       100 |   75483   211391 |   27677     100     1802    18.0 |  4.480 % |
c |       250 |   75483   211391 |   30444     250     5667    22.7 |  4.480 % |
c |       475 |   75483   211391 |   33489     475     8574    18.1 |  4.480 % |
c |       814 |   75483   211391 |   36838     814    31913    39.2 |  4.481 % |
c |      1322 |   75483   211391 |   40522    1322    52718    39.9 |  4.480 % |
c |      2082 |   75483   211391 |   44574    2082    83887    40.3 |  4.480 % |
c |      3221 |   75483   211391 |   49031    3221   133934    41.6 |  4.480 % |
c |      4930 |   75483   211391 |   53934    4930   234193    47.5 |  4.481 % |
c |      7494 |   75483   211391 |   59328    7494   380846    50.8 |  4.480 % |
c |     11338 |   75483   211391 |   65261   11338   493456    43.5 |  4.480 % |
c |     17105 |   75483   211391 |   71787   17105   734042    42.9 |  4.480 % |
c |     25754 |   75483   211391 |   78965   25754  1206665    46.9 |  4.480 % |
c |     38730 |   75483   211391 |   86862   38730  1828879    47.2 |  4.481 % |
c |     58191 |   75483   211391 |   95548   58191  2633511    45.3 |  4.481 % |
c |     87384 |   75483   211391 |  105103   87384  4475037    51.2 |  4.481 % |
c |    131176 |   75483   211391 |  115614   31370  2885966    92.0 |  4.480 % |
c |    196861 |   75483   211391 |  127175   97055  7713072    79.5 |  4.480 % |
c |    295390 |   75483   211391 |  139893   82254  3745351    45.5 |  4.481 % |
c |    443179 |   75483   211391 |  153882  101552  7075718    69.7 |  4.480 % |
#### 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.92 2/53 14597
Raw data (stat): 14597 (runsolver) R 14596 7987 7986 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481248799 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 0 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0009 s]
Raw data (loadavg): 0.87 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 3581 0 0 0 988 10 0 0 25 0 1 0 481248799 16613376 3555 4294967295 134512640 134672761 3221224544 3221223648 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4056 3555 603 41 0 4015 0
vsize: 16224
[startup+20.0017 s]
Raw data (loadavg): 0.89 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 4468 0 0 0 1984 13 0 0 25 0 1 0 481248799 20250624 4442 4294967295 134512640 134672761 3221224544 3221223712 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4944 4442 603 41 0 4903 0
vsize: 19776
[startup+30.0025 s]
Raw data (loadavg): 0.91 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 5156 0 0 0 2982 15 0 0 25 0 1 0 481248799 23076864 5130 4294967295 134512640 134672761 3221224544 3221223712 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5634 5130 603 41 0 5593 0
vsize: 22536
[startup+40.0033 s]
Raw data (loadavg): 0.92 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 5761 0 0 0 3981 17 0 0 25 0 1 0 481248799 25632768 5735 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6258 5735 603 41 0 6217 0
vsize: 25032
[startup+50.004 s]
Raw data (loadavg): 0.93 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 6231 0 0 0 4979 18 0 0 25 0 1 0 481248799 27504640 6205 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6715 6205 603 41 0 6674 0
vsize: 26860
[startup+60.0047 s]
Raw data (loadavg): 0.94 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 7063 0 0 0 5977 21 0 0 25 0 1 0 481248799 31129600 7037 4294967295 134512640 134672761 3221224544 3221223648 134559925 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7600 7037 603 41 0 7559 0
vsize: 30400
[startup+70.0055 s]
Raw data (loadavg): 0.95 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 7977 0 0 0 6974 24 0 0 25 0 1 0 481248799 34758656 7951 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8486 7951 603 41 0 8445 0
vsize: 33944
[startup+80.0063 s]
Raw data (loadavg): 0.96 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 9060 0 0 0 7970 27 0 0 25 0 1 0 481248799 39223296 9034 4294967295 134512640 134672761 3221224544 3221223712 134561154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9576 9034 603 41 0 9535 0
vsize: 38304
[startup+90.0071 s]
Raw data (loadavg): 0.96 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10071 0 0 0 8967 30 0 0 25 0 1 0 481248799 43261952 10045 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10562 10045 603 41 0 10521 0
vsize: 42248
[startup+100.008 s]
Raw data (loadavg): 0.97 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10756 0 0 0 9966 31 0 0 25 0 1 0 481248799 46088192 10730 4294967295 134512640 134672761 3221224544 3221223680 134565070 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11252 10730 603 41 0 11211 0
vsize: 45008
[startup+110.009 s]
Raw data (loadavg): 0.97 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10876 0 0 0 10966 32 0 0 25 0 1 0 481248799 46624768 10850 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10850 603 41 0 11342 0
vsize: 45532
[startup+120.009 s]
Raw data (loadavg): 0.98 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10876 0 0 0 11966 32 0 0 25 0 1 0 481248799 46624768 10850 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10850 603 41 0 11342 0
vsize: 45532
[startup+130.01 s]
Raw data (loadavg): 0.98 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 12966 32 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+140.011 s]
Raw data (loadavg): 0.98 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 13965 33 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223728 134559038 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+150.012 s]
Raw data (loadavg): 0.98 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 14965 33 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+160.013 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 15965 33 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223648 134560405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+170.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 16965 33 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+180.014 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 17965 33 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+190.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 18965 33 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223648 134560022 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+200.015 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 19966 33 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+210.016 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 10877 0 0 0 20966 33 0 0 25 0 1 0 481248799 46624768 10851 4294967295 134512640 134672761 3221224544 3221223712 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11383 10851 603 41 0 11342 0
vsize: 45532
[startup+220.017 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 11086 0 0 0 21965 34 0 0 25 0 1 0 481248799 47427584 11060 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11579 11060 603 41 0 11538 0
vsize: 46316
[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 11381 0 0 0 22965 35 0 0 25 0 1 0 481248799 48640000 11355 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11875 11355 603 41 0 11834 0
vsize: 47500
[startup+240.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 11718 0 0 0 23964 35 0 0 25 0 1 0 481248799 50204672 11692 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12257 11692 603 41 0 12216 0
vsize: 49028
[startup+250.019 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 11990 0 0 0 24964 36 0 0 25 0 1 0 481248799 51277824 11964 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12519 11964 603 41 0 12478 0
vsize: 50076
[startup+260.02 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 12405 0 0 0 25963 37 0 0 25 0 1 0 481248799 53104640 12379 4294967295 134512640 134672761 3221224544 3221223648 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12965 12379 603 41 0 12924 0
vsize: 51860
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 13057 0 0 0 26960 39 0 0 25 0 1 0 481248799 55816192 13031 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13627 13031 603 41 0 13586 0
vsize: 54508
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 13471 0 0 0 27959 40 0 0 25 0 1 0 481248799 57462784 13445 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14029 13445 603 41 0 13988 0
vsize: 56116
[startup+290.022 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 13863 0 0 0 28959 41 0 0 25 0 1 0 481248799 59105280 13837 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14430 13837 603 41 0 14389 0
vsize: 57720
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14062 0 0 0 29958 42 0 0 25 0 1 0 481248799 59920384 14036 4294967295 134512640 134672761 3221224544 3221223540 1075351179 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14036 603 41 0 14588 0
vsize: 58516
[startup+310.025 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14064 0 0 0 30958 42 0 0 25 0 1 0 481248799 59920384 14038 4294967295 134512640 134672761 3221224544 3221223700 134561032 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14038 603 41 0 14588 0
vsize: 58516
[startup+320.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14066 0 0 0 31959 42 0 0 25 0 1 0 481248799 59920384 14040 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14040 603 41 0 14588 0
vsize: 58516
[startup+330.026 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14068 0 0 0 32959 42 0 0 25 0 1 0 481248799 59920384 14042 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14042 603 41 0 14588 0
vsize: 58516
[startup+340.027 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14068 0 0 0 33959 42 0 0 25 0 1 0 481248799 59920384 14042 4294967295 134512640 134672761 3221224544 3221223712 134561201 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14042 603 41 0 14588 0
vsize: 58516
[startup+350.028 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14068 0 0 0 34959 42 0 0 25 0 1 0 481248799 59920384 14042 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14042 603 41 0 14588 0
vsize: 58516
[startup+360.029 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14070 0 0 0 35960 42 0 0 25 0 1 0 481248799 59920384 14044 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14044 603 41 0 14588 0
vsize: 58516
[startup+370.03 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14070 0 0 0 36960 42 0 0 25 0 1 0 481248799 59920384 14044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14044 603 41 0 14588 0
vsize: 58516
[startup+380.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14070 0 0 0 37959 42 0 0 25 0 1 0 481248799 59920384 14044 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14629 14044 603 41 0 14588 0
vsize: 58516
[startup+390.031 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14070 0 0 0 38959 43 0 0 25 0 1 0 481248799 59920384 14044 4294967295 134512640 134672761 3221224544 3221223648 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14629 14044 603 41 0 14588 0
vsize: 58516
[startup+400.032 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14070 0 0 0 39958 43 0 0 25 0 1 0 481248799 59920384 14044 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14044 603 41 0 14588 0
vsize: 58516
[startup+410.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14071 0 0 0 40958 43 0 0 25 0 1 0 481248799 59920384 14045 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14045 603 41 0 14588 0
vsize: 58516
[startup+420.033 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14071 0 0 0 41959 43 0 0 25 0 1 0 481248799 59920384 14045 4294967295 134512640 134672761 3221224544 3221223712 134561190 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14045 603 41 0 14588 0
vsize: 58516
[startup+430.034 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14071 0 0 0 42959 43 0 0 25 0 1 0 481248799 59920384 14045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14045 603 41 0 14588 0
vsize: 58516
[startup+440.035 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14071 0 0 0 43959 43 0 0 25 0 1 0 481248799 59920384 14045 4294967295 134512640 134672761 3221224544 3221223712 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14045 603 41 0 14588 0
vsize: 58516
[startup+450.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14071 0 0 0 44959 43 0 0 25 0 1 0 481248799 59920384 14045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14045 603 41 0 14588 0
vsize: 58516
[startup+460.036 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14071 0 0 0 45960 43 0 0 25 0 1 0 481248799 59920384 14045 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14045 603 41 0 14588 0
vsize: 58516
[startup+470.037 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14071 0 0 0 46960 43 0 0 25 0 1 0 481248799 59920384 14045 4294967295 134512640 134672761 3221224544 3221223712 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14629 14045 603 41 0 14588 0
vsize: 58516
[startup+480.038 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14134 0 0 0 47960 43 0 0 25 0 1 0 481248799 60190720 14108 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14695 14108 603 41 0 14654 0
vsize: 58780
[startup+490.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14472 0 0 0 48959 44 0 0 25 0 1 0 481248799 61595648 14446 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15038 14446 603 41 0 14997 0
vsize: 60152
[startup+500.039 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 14843 0 0 0 49959 45 0 0 25 0 1 0 481248799 63639552 14817 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15537 14817 603 41 0 15496 0
vsize: 62148
[startup+510.04 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15247 0 0 0 50958 46 0 0 25 0 1 0 481248799 65306624 15221 4294967295 134512640 134672761 3221224544 3221223712 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15944 15221 603 41 0 15903 0
vsize: 63776
[startup+520.041 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 51958 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223648 134554656 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+530.042 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 52958 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223728 134559422 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+540.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 53958 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560976 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+550.043 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 54958 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223648 134560529 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+560.044 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 55959 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+570.045 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 56959 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+580.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 57959 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+590.046 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 58959 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+600.047 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 59960 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+610.049 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 60960 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+620.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 61960 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560871 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+630.05 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 62961 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+640.051 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 63961 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+650.052 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 64961 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+660.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 65961 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+670.053 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 66962 46 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134561188 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+680.054 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 67962 47 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560839 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+690.055 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 68962 47 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+700.056 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 69962 47 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+710.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 70962 47 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+720.057 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 71962 47 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223712 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+730.058 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15501 0 0 0 72962 47 0 0 25 0 1 0 481248799 66375680 15475 4294967295 134512640 134672761 3221224544 3221223648 134560154 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16205 15475 603 41 0 16164 0
vsize: 64820
[startup+740.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 15541 0 0 0 73962 47 0 0 25 0 1 0 481248799 66510848 15515 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16238 15515 603 41 0 16197 0
vsize: 64952
[startup+750.059 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 16347 0 0 0 74961 49 0 0 25 0 1 0 481248799 69885952 16321 4294967295 134512640 134672761 3221224544 3221223712 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17062 16321 603 41 0 17021 0
vsize: 68248
[startup+760.06 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 17031 0 0 0 75958 51 0 0 25 0 1 0 481248799 72720384 17005 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17754 17005 603 41 0 17713 0
vsize: 71016
[startup+770.061 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 17606 0 0 0 76957 53 0 0 25 0 1 0 481248799 75034624 17580 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18319 17580 603 41 0 18278 0
vsize: 73276
[startup+780.062 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18084 0 0 0 77956 54 0 0 25 0 1 0 481248799 76972032 18058 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18792 18058 603 41 0 18751 0
vsize: 75168
[startup+790.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18542 0 0 0 78954 56 0 0 25 0 1 0 481248799 78848000 18516 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19250 18516 603 41 0 19209 0
vsize: 77000
[startup+800.064 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18921 0 0 0 79953 57 0 0 25 0 1 0 481248799 80470016 18895 4294967295 134512640 134672761 3221224544 3221223648 134554668 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19646 18895 603 41 0 19605 0
vsize: 78584
[startup+810.065 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18923 0 0 0 80953 57 0 0 25 0 1 0 481248799 80470016 18897 4294967295 134512640 134672761 3221224544 3221223712 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19646 18897 603 41 0 19605 0
vsize: 78584
[startup+820.066 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18924 0 0 0 81954 57 0 0 25 0 1 0 481248799 80470016 18898 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19646 18898 603 41 0 19605 0
vsize: 78584
[startup+830.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18926 0 0 0 82954 57 0 0 25 0 1 0 481248799 80470016 18900 4294967295 134512640 134672761 3221224544 3221223744 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19646 18900 603 41 0 19605 0
vsize: 78584
[startup+840.067 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18929 0 0 0 83954 57 0 0 25 0 1 0 481248799 80470016 18903 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19646 18903 603 41 0 19605 0
vsize: 78584
[startup+850.068 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18930 0 0 0 84954 57 0 0 25 0 1 0 481248799 80470016 18904 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19646 18904 603 41 0 19605 0
vsize: 78584
[startup+860.069 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18932 0 0 0 85955 57 0 0 25 0 1 0 481248799 80470016 18906 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19646 18906 603 41 0 19605 0
vsize: 78584
[startup+870.07 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18932 0 0 0 86955 57 0 0 25 0 1 0 481248799 80470016 18906 4294967295 134512640 134672761 3221224544 3221223712 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19646 18906 603 41 0 19605 0
vsize: 78584
[startup+880.071 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18950 0 0 0 87955 57 0 0 25 0 1 0 481248799 80674816 18924 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19696 18924 603 41 0 19655 0
vsize: 78784
[startup+890.071 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18972 0 0 0 88955 57 0 0 25 0 1 0 481248799 80674816 18946 4294967295 134512640 134672761 3221224544 3221223712 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19696 18946 603 41 0 19655 0
vsize: 78784
[startup+900.072 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18978 0 0 0 89956 57 0 0 25 0 1 0 481248799 80674816 18952 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19696 18952 603 41 0 19655 0
vsize: 78784
[startup+910.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18981 0 0 0 90956 57 0 0 25 0 1 0 481248799 80674816 18955 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19696 18955 603 41 0 19655 0
vsize: 78784
[startup+920.074 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 18983 0 0 0 91956 57 0 0 25 0 1 0 481248799 80674816 18957 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19696 18957 603 41 0 19655 0
vsize: 78784
[startup+930.075 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19021 0 0 0 92957 57 0 0 25 0 1 0 481248799 80936960 18995 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19760 18995 603 41 0 19719 0
vsize: 79040
[startup+940.076 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19023 0 0 0 93957 57 0 0 25 0 1 0 481248799 80936960 18997 4294967295 134512640 134672761 3221224544 3221223712 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19760 18997 603 41 0 19719 0
vsize: 79040
[startup+950.077 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19024 0 0 0 94957 57 0 0 25 0 1 0 481248799 80936960 18998 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19760 18998 603 41 0 19719 0
vsize: 79040
[startup+960.078 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19026 0 0 0 95957 57 0 0 25 0 1 0 481248799 80936960 19000 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19760 19000 603 41 0 19719 0
vsize: 79040
[startup+970.078 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19027 0 0 0 96958 57 0 0 25 0 1 0 481248799 80936960 19001 4294967295 134512640 134672761 3221224544 3221223728 134558662 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19760 19001 603 41 0 19719 0
vsize: 79040
[startup+980.079 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19028 0 0 0 97958 57 0 0 25 0 1 0 481248799 80936960 19002 4294967295 134512640 134672761 3221224544 3221223712 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19760 19002 603 41 0 19719 0
vsize: 79040
[startup+990.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19028 0 0 0 98958 57 0 0 25 0 1 0 481248799 80936960 19002 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19760 19002 603 41 0 19719 0
vsize: 79040
[startup+1000.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19028 0 0 0 99958 57 0 0 25 0 1 0 481248799 80936960 19002 4294967295 134512640 134672761 3221224544 3221223712 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19760 19002 603 41 0 19719 0
vsize: 79040
[startup+1010.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19045 0 0 0 100959 57 0 0 25 0 1 0 481248799 81195008 19019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19823 19019 603 41 0 19782 0
vsize: 79292
[startup+1020.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19045 0 0 0 101959 57 0 0 25 0 1 0 481248799 81195008 19019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19823 19019 603 41 0 19782 0
vsize: 79292
[startup+1030.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19045 0 0 0 102959 57 0 0 25 0 1 0 481248799 81195008 19019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19823 19019 603 41 0 19782 0
vsize: 79292
[startup+1040.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19045 0 0 0 103959 57 0 0 25 0 1 0 481248799 81195008 19019 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19823 19019 603 41 0 19782 0
vsize: 79292
[startup+1050.08 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19091 0 0 0 104960 57 0 0 25 0 1 0 481248799 81457152 19065 4294967295 134512640 134672761 3221224544 3221223648 134560483 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19887 19065 603 41 0 19846 0
vsize: 79548
[startup+1060.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19129 0 0 0 105960 57 0 0 25 0 1 0 481248799 81719296 19103 4294967295 134512640 134672761 3221224544 3221223712 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19951 19103 603 41 0 19910 0
vsize: 79804
[startup+1070.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19135 0 0 0 106960 58 0 0 25 0 1 0 481248799 81719296 19109 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19951 19109 603 41 0 19910 0
vsize: 79804
[startup+1080.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19206 0 0 0 107960 58 0 0 25 0 1 0 481248799 81981440 19180 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20015 19180 603 41 0 19974 0
vsize: 80060
[startup+1090.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19210 0 0 0 108960 58 0 0 25 0 1 0 481248799 81981440 19184 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20015 19184 603 41 0 19974 0
vsize: 80060
[startup+1100.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19215 0 0 0 109960 58 0 0 25 0 1 0 481248799 81981440 19189 4294967295 134512640 134672761 3221224544 3221223680 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20015 19189 603 41 0 19974 0
vsize: 80060
[startup+1110.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19236 0 0 0 110961 58 0 0 25 0 1 0 481248799 82243584 19210 4294967295 134512640 134672761 3221224544 3221223712 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20079 19210 603 41 0 20038 0
vsize: 80316
[startup+1120.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19238 0 0 0 111961 58 0 0 25 0 1 0 481248799 82243584 19212 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20079 19212 603 41 0 20038 0
vsize: 80316
[startup+1130.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19243 0 0 0 112961 58 0 0 25 0 1 0 481248799 82243584 19217 4294967295 134512640 134672761 3221224544 3221223712 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20079 19217 603 41 0 20038 0
vsize: 80316
[startup+1140.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19369 0 0 0 113960 59 0 0 25 0 1 0 481248799 82649088 19343 4294967295 134512640 134672761 3221224544 3221223712 134560876 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20178 19343 603 41 0 20137 0
vsize: 80712
[startup+1150.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19573 0 0 0 114960 59 0 0 25 0 1 0 481248799 83652608 19547 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20423 19547 603 41 0 20382 0
vsize: 81692
[startup+1160.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19776 0 0 0 115960 60 0 0 25 0 1 0 481248799 84467712 19750 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20622 19750 603 41 0 20581 0
vsize: 82488
[startup+1170.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 19965 0 0 0 116960 60 0 0 25 0 1 0 481248799 85278720 19939 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20820 19939 603 41 0 20779 0
vsize: 83280
[startup+1180.09 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 20168 0 0 0 117960 61 0 0 25 0 1 0 481248799 86089728 20142 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21018 20142 603 41 0 20977 0
vsize: 84072
[startup+1190.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 20383 0 0 0 118959 61 0 0 25 0 1 0 481248799 87035904 20357 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21249 20357 603 41 0 21208 0
vsize: 84996
[startup+1200.1 s]
Raw data (loadavg): 0.99 0.97 0.92 2/53 14597
Raw data (stat): 14597 (minisat+) R 14596 7987 7986 0 -1 0 20564 0 0 0 119959 62 0 0 25 0 1 0 481248799 87711744 20538 4294967295 134512640 134672761 3221224544 3221223712 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21414 20538 603 41 0 21373 0
vsize: 85656
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.15 s]
Raw data (loadavg): 0.99 0.97 0.92 1/53 14597
Raw data (stat): 14597 (minisat+) Z 14596 7987 7986 0 -1 12 20567 0 0 0 119959 66 0 0 25 0 1 0 481248799 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.15
CPU time (s): 1200.26
CPU user time (s): 1199.6
CPU system time (s): 0.661899
CPU usage (%): 100.009
Max. virtual memory (Kb): 85656
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####