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,3-13,19.opb
MD5SUM	fa67033d6a242cf79309b3804f79a4fe
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
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	102
Number of bits of the biggest sum of numbers	7
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	15.8556
Number of variables	4608
Total number of constraints	34956
Number of constraints which are clauses	29328
Number of constraints which are cardinality constraints (but not clauses)	5550
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 6457

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        886356 kB
Buffers:         35088 kB
Cached:          70188 kB
SwapCached:        192 kB
Active:          56560 kB
Inactive:        51744 kB
HighTotal:      131008 kB
HighFree:        57064 kB
LowTotal:       903652 kB
LowFree:        829292 kB
SwapTotal:     2097136 kB
SwapFree:      2096944 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6908 kB
Slab:            34396 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:23:11 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4872 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30522 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30521]---> BDD-cost:   57
c ---[30520]---> BDD-cost:   57
c ---[30519]---> BDD-cost:   57
c ---[30518]---> BDD-cost:   57
c ---[30517]---> BDD-cost:   57
c ---[30516]---> BDD-cost:   57
c ---[30515]---> BDD-cost:  100
c ---[30514]---> BDD-cost:  100
c ---[30513]---> BDD-cost:  100
c ---[30512]---> BDD-cost:  100
c ---[30511]---> BDD-cost:  100
c ---[30510]---> BDD-cost:  100
c ---[30509]---> BDD-cost:  122
c ---[30508]---> BDD-cost:  122
c ---[30507]---> BDD-cost:  122
c ---[30506]---> BDD-cost:  122
c ---[30505]---> BDD-cost:  122
c ---[30504]---> BDD-cost:  122
c ---[30503]---> BDD-cost:  122
c ---[30502]---> BDD-cost:  122
c ---[30501]---> BDD-cost:  122
c ---[30500]---> BDD-cost:  122
c ---[30499]---> BDD-cost:  122
c ---[30498]---> BDD-cost:  122
c ---[30497]---> BDD-cost:  122
c ---[30496]---> BDD-cost:  122
c ---[30495]---> BDD-cost:  122
c ---[30494]---> BDD-cost:  122
c ---[30493]---> BDD-cost:  122
c ---[30492]---> BDD-cost:  122
c ---[30491]---> BDD-cost:  131
c ---[30490]---> BDD-cost:  131
c ---[30489]---> BDD-cost:  131
c ---[30488]---> BDD-cost:  131
c ---[30487]---> BDD-cost:  131
c ---[30486]---> BDD-cost:  131
c ---[30485]---> BDD-cost:  122
c ---[30484]---> BDD-cost:  122
c ---[30483]---> BDD-cost:  122
c ---[30482]---> BDD-cost:  122
c ---[30481]---> BDD-cost:  122
c ---[30480]---> BDD-cost:  122
c ---[30479]---> BDD-cost:  122
c ---[30478]---> BDD-cost:  122
c ---[30477]---> BDD-cost:  122
c ---[30476]---> BDD-cost:  122
c ---[30475]---> BDD-cost:  122
c ---[30474]---> BDD-cost:  122
c ---[30473]---> BDD-cost:  122
c ---[30472]---> BDD-cost:  122
c ---[30471]---> BDD-cost:  122
c ---[30470]---> BDD-cost:  122
c ---[30469]---> BDD-cost:  122
c ---[30468]---> BDD-cost:  122
c ---[30467]---> Sorter-cost:  544     Base: 2 2
c ---[30466]---> Sorter-cost:  544     Base: 2 2
c ---[30465]---> Sorter-cost:  544     Base: 2 2
c ---[30464]---> Sorter-cost:  544     Base: 2 2
c ---[30463]---> Sorter-cost:  544     Base: 2 2
c ---[30462]---> Sorter-cost:  544     Base: 2 2
c ---[30461]---> Sorter-cost:  544     Base: 2 2
c ---[30460]---> Sorter-cost:  544     Base: 2 2
c ---[30459]---> Sorter-cost:  544     Base: 2 2
c ---[30458]---> Sorter-cost:  544     Base: 2 2
c ---[30457]---> Sorter-cost:  544     Base: 2 2
c ---[30456]---> Sorter-cost:  544     Base: 2 2
c ---[30455]---> BDD-cost:   57
c ---[30454]---> BDD-cost:   57
c ---[30453]---> BDD-cost:   57
c ---[30452]---> BDD-cost:   57
c ---[30451]---> BDD-cost:   57
c ---[30450]---> BDD-cost:   57
c ---[30449]---> BDD-cost:   57
c ---[30448]---> BDD-cost:   57
c ---[30447]---> BDD-cost:   57
c ---[30446]---> BDD-cost:   57
c ---[30445]---> BDD-cost:   57
c ---[30444]---> BDD-cost:   57
c ---[30442]---> BDD-cost:   23
c ---[30440]---> BDD-cost:   23
c ---[30438]---> BDD-cost:   23
c ---[30436]---> BDD-cost:   23
c ---[30434]---> BDD-cost:   23
c ---[30432]---> BDD-cost:   23
c ---[30430]---> BDD-cost:   23
c ---[30428]---> BDD-cost:   23
c ---[30426]---> BDD-cost:   23
c ---[30424]---> BDD-cost:   23
c ---[30422]---> BDD-cost:   23
c ---[30420]---> BDD-cost:   23
c ---[30418]---> BDD-cost:   23
c ---[30416]---> BDD-cost:   23
c ---[30414]---> BDD-cost:   23
c ---[30412]---> BDD-cost:   23
c ---[30410]---> BDD-cost:   23
c ---[30408]---> BDD-cost:   23
c ---[30406]---> BDD-cost:   17
c ---[30404]---> BDD-cost:   17
c ---[30402]---> BDD-cost:   17
c ---[30400]---> BDD-cost:   17
c ---[30398]---> BDD-cost:   17
c ---[30396]---> BDD-cost:   17
c ---[30394]---> BDD-cost:   23
c ---[30392]---> BDD-cost:   23
c ---[30390]---> BDD-cost:   23
c ---[30388]---> BDD-cost:   23
c ---[30386]---> BDD-cost:   23
c ---[30384]---> BDD-cost:   23
c ---[30382]---> BDD-cost:   23
c ---[30380]---> BDD-cost:   23
c ---[30378]---> BDD-cost:   23
c ---[30376]---> BDD-cost:   23
c ---[30374]---> BDD-cost:   23
c ---[30372]---> BDD-cost:   23
c ---[30370]---> BDD-cost:   17
c ---[30368]---> BDD-cost:   17
c ---[30366]---> BDD-cost:   17
c ---[30364]---> BDD-cost:   17
c ---[30362]---> BDD-cost:   17
c ---[30360]---> BDD-cost:   17
c ---[30358]---> BDD-cost:   17
c ---[30356]---> BDD-cost:   17
c ---[30354]---> BDD-cost:   17
c ---[30352]---> BDD-cost:   17
c ---[30350]---> BDD-cost:   17
c ---[30348]---> BDD-cost:   17
c ---[30346]---> BDD-cost:   23
c ---[30344]---> BDD-cost:   23
c ---[30342]---> BDD-cost:   23
c ---[30340]---> BDD-cost:   23
c ---[30338]---> BDD-cost:   23
c ---[30336]---> BDD-cost:   23
c ---[30334]---> BDD-cost:   23
c ---[30332]---> BDD-cost:   23
c ---[30330]---> BDD-cost:   23
c ---[30328]---> BDD-cost:   23
c ---[30326]---> BDD-cost:   23
c ---[30324]---> BDD-cost:   23
c ---[30322]---> BDD-cost:   23
c ---[30320]---> BDD-cost:   23
c ---[30318]---> BDD-cost:   23
c ---[30316]---> BDD-cost:   23
c ---[30314]---> BDD-cost:   23
c ---[30312]---> BDD-cost:   23
c ---[30310]---> BDD-cost:   17
c ---[30308]---> BDD-cost:   17
c ---[30306]---> BDD-cost:   17
c ---[30304]---> BDD-cost:   17
c ---[30302]---> BDD-cost:   17
c ---[30300]---> BDD-cost:   17
c ---[30298]---> BDD-cost:   23
c ---[30296]---> BDD-cost:   23
c ---[30294]---> BDD-cost:   23
c ---[30292]---> BDD-cost:   23
c ---[30290]---> BDD-cost:   23
c ---[30288]---> BDD-cost:   23
c ---[30286]---> BDD-cost:   23
c ---[30284]---> BDD-cost:   23
c ---[30282]---> BDD-cost:   23
c ---[30280]---> BDD-cost:   23
c ---[30278]---> BDD-cost:   23
c ---[30276]---> BDD-cost:   23
c ---[30274]---> BDD-cost:   23
c ---[30272]---> BDD-cost:   23
c ---[30270]---> BDD-cost:   23
c ---[30268]---> BDD-cost:   23
c ---[30266]---> BDD-cost:   23
c ---[30264]---> BDD-cost:   23
c ---[30262]---> BDD-cost:   23
c ---[30260]---> BDD-cost:   23
c ---[30258]---> BDD-cost:   23
c ---[30256]---> BDD-cost:   23
c ---[30254]---> BDD-cost:   23
c ---[30252]---> BDD-cost:   23
c ---[30250]---> BDD-cost:   23
c ---[30248]---> BDD-cost:   23
c ---[30246]---> BDD-cost:   23
c ---[30244]---> BDD-cost:   23
c ---[30242]---> BDD-cost:   23
c ---[30240]---> BDD-cost:   23
c ---[30238]---> BDD-cost:   23
c ---[30236]---> BDD-cost:   23
c ---[30234]---> BDD-cost:   23
c ---[30232]---> BDD-cost:   23
c ---[30230]---> BDD-cost:   23
c ---[30228]---> BDD-cost:   23
c ---[30226]---> BDD-cost:   23
c ---[30224]---> BDD-cost:   23
c ---[30222]---> BDD-cost:   23
c ---[30220]---> BDD-cost:   23
c ---[30218]---> BDD-cost:   23
c ---[30216]---> BDD-cost:   23
c ---[30214]---> BDD-cost:   23
c ---[30212]---> BDD-cost:   23
c ---[30210]---> BDD-cost:   23
c ---[30208]---> BDD-cost:   23
c ---[30206]---> BDD-cost:   23
c ---[30204]---> BDD-cost:   23
c ---[30202]---> BDD-cost:   23
c ---[30200]---> BDD-cost:   23
c ---[30198]---> BDD-cost:   23
c ---[30196]---> BDD-cost:   23
c ---[30194]---> BDD-cost:   23
c ---[30192]---> BDD-cost:   23
c ---[30190]---> BDD-cost:   23
c ---[30188]---> BDD-cost:   23
c ---[30186]---> BDD-cost:   23
c ---[30184]---> BDD-cost:   23
c ---[30182]---> BDD-cost:   23
c ---[30180]---> BDD-cost:   23
c ---[30178]---> BDD-cost:   23
c ---[30176]---> BDD-cost:   23
c ---[30174]---> BDD-cost:   23
c ---[30172]---> BDD-cost:   23
c ---[30170]---> BDD-cost:   23
c ---[30168]---> BDD-cost:   23
c ---[30166]---> BDD-cost:   23
c ---[30164]---> BDD-cost:   23
c ---[30162]---> BDD-cost:   23
c ---[30160]---> BDD-cost:   23
c ---[30158]---> BDD-cost:   23
c ---[30156]---> BDD-cost:   23
c ---[30154]---> BDD-cost:   23
c ---[30152]---> BDD-cost:   23
c ---[30150]---> BDD-cost:   23
c ---[30148]---> BDD-cost:   23
c ---[30146]---> BDD-cost:   23
c ---[30144]---> BDD-cost:   23
c ---[30142]---> BDD-cost:   23
c ---[30140]---> BDD-cost:   23
c ---[30138]---> BDD-cost:   23
c ---[30136]---> BDD-cost:   23
c ---[30134]---> BDD-cost:   23
c ---[30132]---> BDD-cost:   23
c ---[30130]---> BDD-cost:   23
c ---[30128]---> BDD-cost:   23
c ---[30126]---> BDD-cost:   23
c ---[30124]---> BDD-cost:   23
c ---[30122]---> BDD-cost:   23
c ---[30120]---> BDD-cost:   23
c ---[30118]---> BDD-cost:   17
c ---[30116]---> BDD-cost:   17
c ---[30114]---> BDD-cost:   17
c ---[30112]---> BDD-cost:   17
c ---[30110]---> BDD-cost:   17
c ---[30108]---> BDD-cost:   17
c ---[30106]---> BDD-cost:   23
c ---[30104]---> BDD-cost:   23
c ---[30102]---> BDD-cost:   23
c ---[30100]---> BDD-cost:   23
c ---[30098]---> BDD-cost:   23
c ---[30096]---> BDD-cost:   23
c ---[30095]---> BDD-cost:    9
c ---[30094]---> BDD-cost:    9
c ---[30093]---> BDD-cost:    9
c ---[30092]---> BDD-cost:    9
c ---[30091]---> BDD-cost:    9
c ---[30090]---> BDD-cost:    9
c ---[30089]---> BDD-cost:    9
c ---[30088]---> BDD-cost:    9
c ---[30087]---> BDD-cost:    9
c ---[30086]---> BDD-cost:    9
c ---[30085]---> BDD-cost:    9
c ---[30084]---> BDD-cost:    9
c ---[30083]---> BDD-cost:    9
c ---[30082]---> BDD-cost:    9
c ---[30081]---> BDD-cost:    9
c ---[30080]---> BDD-cost:    9
c ---[30079]---> BDD-cost:    9
c ---[30078]---> BDD-cost:    9
c ---[30077]---> BDD-cost:    9
c ---[30076]---> BDD-cost:    9
c ---[30075]---> BDD-cost:    9
c ---[30074]---> BDD-cost:    9
c ---[30073]---> BDD-cost:    9
c ---[30072]---> BDD-cost:    9
c ---[30071]---> BDD-cost:    9
c ---[30070]---> BDD-cost:    9
c ---[30069]---> BDD-cost:    9
c ---[30068]---> BDD-cost:    9
c ---[30067]---> BDD-cost:    9
c ---[30066]---> BDD-cost:    9
c ---[30065]---> BDD-cost:    9
c ---[30064]---> BDD-cost:    9
c ---[30063]---> BDD-cost:    9
c ---[30062]---> BDD-cost:    9
c ---[30061]---> BDD-cost:    9
c ---[30060]---> BDD-cost:    9
c ---[30059]---> BDD-cost:    9
c ---[30058]---> BDD-cost:    9
c ---[30057]---> BDD-cost:    9
c ---[30056]---> BDD-cost:    9
c ---[30055]---> BDD-cost:    9
c ---[30054]---> BDD-cost:    9
c ---[30053]---> BDD-cost:    9
c ---[30052]---> BDD-cost:    9
c ---[30051]---> BDD-cost:    9
c ---[30050]---> BDD-cost:    9
c ---[30049]---> BDD-cost:    9
c ---[30048]---> BDD-cost:    9
c ---[30047]---> BDD-cost:    9
c ---[30046]---> BDD-cost:    9
c ---[30045]---> BDD-cost:    9
c ---[30044]---> BDD-cost:    9
c ---[30043]---> BDD-cost:    9
c ---[30042]---> BDD-cost:    9
c ---[30041]---> BDD-cost:    9
c ---[30040]---> BDD-cost:    9
c ---[30039]---> BDD-cost:    9
c ---[30038]---> BDD-cost:    9
c ---[30037]---> BDD-cost:    9
c ---[30036]---> BDD-cost:    9
c ---[30035]---> BDD-cost:    9
c ---[30034]---> BDD-cost:    9
c ---[30033]---> BDD-cost:    9
c ---[30032]---> BDD-cost:    9
c ---[30031]---> BDD-cost:    9
c ---[30030]---> BDD-cost:    9
c ---[30029]---> BDD-cost:    9
c ---[30028]---> BDD-cost:    9
c ---[30027]---> BDD-cost:    9
c ---[30026]---> BDD-cost:    9
c ---[30025]---> BDD-cost:    9
c ---[30024]---> BDD-cost:    9
c ---[30023]---> BDD-cost:    9
c ---[30022]---> BDD-cost:    9
c ---[30021]---> BDD-cost:    9
c ---[30020]---> BDD-cost:    9
c ---[30019]---> BDD-cost:    9
c ---[30018]---> BDD-cost:    9
c ---[30017]---> BDD-cost:    9
c ---[30016]---> BDD-cost:    9
c ---[30015]---> BDD-cost:    9
c ---[30014]---> BDD-cost:    9
c ---[30013]---> BDD-cost:    9
c ---[30012]---> BDD-cost:    9
c ---[30011]---> BDD-cost:    9
c ---[30010]---> BDD-cost:    9
c ---[30009]---> BDD-cost:    9
c ---[30008]---> BDD-cost:    9
c ---[30007]---> BDD-cost:    9
c ---[30006]---> BDD-cost:    9
c ---[30005]---> BDD-cost:    9
c ---[30004]---> BDD-cost:    9
c ---[30003]---> BDD-cost:    9
c ---[30002]---> BDD-cost:    9
c ---[30001]---> BDD-cost:    9
c ---[30000]---> BDD-cost:    9
c ---[29999]---> BDD-cost:    9
c ---[29998]---> BDD-cost:    9
c ---[29997]---> BDD-cost:    9
c ---[29996]---> BDD-cost:    9
c ---[29995]---> BDD-cost:    9
c ---[29994]---> BDD-cost:    9
c ---[29993]---> BDD-cost:    9
c ---[29992]---> BDD-cost:    9
c ---[29991]---> BDD-cost:    9
c ---[29990]---> BDD-cost:    9
c ---[29989]---> BDD-cost:    9
c ---[29988]---> BDD-cost:    9
c ---[29987]---> BDD-cost:    9
c ---[29986]---> BDD-cost:    9
c ---[29985]---> BDD-cost:    9
c ---[29984]---> BDD-cost:    9
c ---[29983]---> BDD-cost:    9
c ---[29982]---> BDD-cost:    9
c ---[29981]---> BDD-cost:    9
c ---[29980]---> BDD-cost:    9
c ---[29979]---> BDD-cost:    9
c ---[29978]---> BDD-cost:    9
c ---[29977]---> BDD-cost:    9
c ---[29976]---> BDD-cost:    9
c ---[29975]---> BDD-cost:    9
c ---[29974]---> BDD-cost:    9
c ---[29973]---> BDD-cost:    9
c ---[29972]---> BDD-cost:    9
c ---[29971]---> BDD-cost:    9
c ---[29970]---> BDD-cost:    9
c ---[29969]---> BDD-cost:    9
c ---[29968]---> BDD-cost:    9
c ---[29967]---> BDD-cost:    9
c ---[29966]---> BDD-cost:    9
c ---[29965]---> BDD-cost:    9
c ---[29964]---> BDD-cost:    9
c ---[29963]---> BDD-cost:    9
c ---[29962]---> BDD-cost:    9
c ---[29961]---> BDD-cost:    9
c ---[29960]---> BDD-cost:    9
c ---[29959]---> BDD-cost:    9
c ---[29958]---> BDD-cost:    9
c ---[29957]---> BDD-cost:    9
c ---[29956]---> BDD-cost:    9
c ---[29955]---> BDD-cost:    9
c ---[29954]---> BDD-cost:    9
c ---[29953]---> BDD-cost:    9
c ---[29952]---> BDD-cost:    9
c ---[29951]---> BDD-cost:    9
c ---[29950]---> BDD-cost:    9
c ---[29949]---> BDD-cost:    9
c ---[29948]---> BDD-cost:    9
c ---[29947]---> BDD-cost:    9
c ---[29946]---> BDD-cost:    9
c ---[29945]---> BDD-cost:    9
c ---[29944]---> BDD-cost:    9
c ---[29943]---> BDD-cost:    9
c ---[29942]---> BDD-cost:    9
c ---[29941]---> BDD-cost:    9
c ---[29940]---> BDD-cost:    9
c ---[29939]---> BDD-cost:    9
c ---[29938]---> BDD-cost:    9
c ---[29937]---> BDD-cost:    9
c ---[29936]---> BDD-cost:    9
c ---[29935]---> BDD-cost:    9
c ---[29934]---> BDD-cost:    9
c ---[29933]---> BDD-cost:    9
c ---[29932]---> BDD-cost:    9
c ---[29931]---> BDD-cost:    9
c ---[29930]---> BDD-cost:    9
c ---[29929]---> BDD-cost:    9
c ---[29928]---> BDD-cost:    9
c ---[29927]---> BDD-cost:    9
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 ---[ 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 |  118860   331608 |   39620       0        0     nan |  0.000 % |
c |       101 |  118715   331173 |   43582      57      327     5.7 |  4.025 % |
c |       251 |  118565   330723 |   47940      99      543     5.5 |  4.140 % |
c |       477 |  118395   330213 |   52734     243     1464     6.0 |  4.270 % |
c |       815 |  118247   329807 |   58007     529     3962     7.5 |  4.397 % |
c |      1322 |  118172   329582 |   63808     943    11538    12.2 |  4.454 % |
c |      2082 |  118107   329387 |   70189    1610    22802    14.2 |  4.504 % |
c |      3222 |  118047   329207 |   77208    2639    41562    15.7 |  4.550 % |
c |      4930 |  117890   328761 |   84928    4233    84457    20.0 |  4.680 % |
c |      7493 |  117518   327706 |   93421    6625   152628    23.0 |  4.987 % |
c |     11338 |  117249   326940 |  102764   10243   262139    25.6 |  5.209 % |
c |     17107 |  116737   325422 |  113040   15300   435441    28.5 |  5.608 % |
c |     25757 |  115915   323159 |  124344   23370   693811    29.7 |  6.340 % |
c |     38732 |  114674   319822 |  136778   35311  1160576    32.9 |  7.467 % |
c |     58194 |  113779   317297 |  150456   54362  1976680    36.4 |  8.226 % |
c |     87386 |  112684   314261 |  165502   82823  3376526    40.8 |  9.177 % |
c |    131176 |  110160   307445 |  182052  124909  5195439    41.6 | 11.530 % |
c |    196860 |  107541   300283 |  200258   20938   795564    38.0 | 13.949 % |
c |    295386 |  105581   294795 |  220283  118522  5064231    42.7 | 15.685 % |
c |    443178 |  103998   290359 |  242312   60759  2478326    40.8 | 17.104 % |
#### 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.93 0.99 0.93 2/54 8723
Raw data (stat): 8723 (runsolver) R 8722 3260 3259 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481919666 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.94 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 3164 0 0 0 989 9 0 0 25 0 1 0 481919666 14602240 3092 4294967295 134512640 134672761 3221224560 3221223696 134560642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3565 3092 603 41 0 3524 0
vsize: 14260
[startup+20.0014 s]
Raw data (loadavg): 0.95 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 3456 0 0 0 1988 10 0 0 25 0 1 0 481919666 15872000 3384 4294967295 134512640 134672761 3221224560 3221223696 134560697 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3875 3384 603 41 0 3834 0
vsize: 15500
[startup+30.0016 s]
Raw data (loadavg): 0.96 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 3710 0 0 0 2987 12 0 0 25 0 1 0 481919666 16973824 3638 4294967295 134512640 134672761 3221224560 3221223712 134561244 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4144 3638 603 41 0 4103 0
vsize: 16576
[startup+40.0026 s]
Raw data (loadavg): 0.96 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 3969 0 0 0 3986 13 0 0 25 0 1 0 481919666 17911808 3897 4294967295 134512640 134672761 3221224560 3221223732 134556641 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4373 3897 603 41 0 4332 0
vsize: 17492
[startup+50.0032 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 4119 0 0 0 4985 14 0 0 25 0 1 0 481919666 18583552 4047 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4537 4047 603 41 0 4496 0
vsize: 18148
[startup+60.0025 s]
Raw data (loadavg): 0.97 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 4496 0 0 0 5983 15 0 0 25 0 1 0 481919666 20189184 4424 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4929 4424 603 41 0 4888 0
vsize: 19716
[startup+70.0035 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 4842 0 0 0 6982 17 0 0 25 0 1 0 481919666 21532672 4770 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5257 4770 603 41 0 5216 0
vsize: 21028
[startup+80.0043 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 5251 0 0 0 7981 18 0 0 25 0 1 0 481919666 23285760 5179 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5685 5179 603 41 0 5644 0
vsize: 22740
[startup+90.0044 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 5589 0 0 0 8979 19 0 0 25 0 1 0 481919666 24625152 5517 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6012 5517 603 41 0 5971 0
vsize: 24048
[startup+100.005 s]
Raw data (loadavg): 0.98 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 5782 0 0 0 9979 20 0 0 25 0 1 0 481919666 25427968 5710 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6208 5710 603 41 0 6167 0
vsize: 24832
[startup+110.005 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 6058 0 0 0 10977 22 0 0 25 0 1 0 481919666 26501120 5986 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6470 5986 603 41 0 6429 0
vsize: 25880
[startup+120.005 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 6322 0 0 0 11976 23 0 0 25 0 1 0 481919666 27828224 6250 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6794 6250 603 41 0 6753 0
vsize: 27176
[startup+130.005 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 6761 0 0 0 12975 24 0 0 25 0 1 0 481919666 29573120 6689 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7220 6689 603 41 0 7179 0
vsize: 28880
[startup+140.006 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 7152 0 0 0 13974 25 0 0 25 0 1 0 481919666 31182848 7080 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7613 7080 603 41 0 7572 0
vsize: 30452
[startup+150.006 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 7440 0 0 0 14973 27 0 0 25 0 1 0 481919666 32256000 7368 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7875 7368 603 41 0 7834 0
vsize: 31500
[startup+160.006 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 7605 0 0 0 15972 27 0 0 25 0 1 0 481919666 32931840 7533 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8040 7533 603 41 0 7999 0
vsize: 32160
[startup+170.007 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 7751 0 0 0 16972 27 0 0 25 0 1 0 481919666 33599488 7679 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8203 7679 603 41 0 8162 0
vsize: 32812
[startup+180.006 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 7862 0 0 0 17972 28 0 0 25 0 1 0 481919666 34000896 7790 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8301 7790 603 41 0 8260 0
vsize: 33204
[startup+190.007 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 7959 0 0 0 18972 28 0 0 25 0 1 0 481919666 34402304 7887 4294967295 134512640 134672761 3221224560 3221223664 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8399 7887 603 41 0 8358 0
vsize: 33596
[startup+200.007 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8723
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 8145 0 0 0 19971 29 0 0 25 0 1 0 481919666 35209216 8073 4294967295 134512640 134672761 3221224560 3221223472 1075358820 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8596 8073 603 41 0 8555 0
vsize: 34384
[startup+210.006 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 8338 0 0 0 20971 30 0 0 25 0 1 0 481919666 35872768 8266 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8758 8266 603 41 0 8717 0
vsize: 35032
[startup+220.007 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 8486 0 0 0 21971 30 0 0 25 0 1 0 481919666 36544512 8414 4294967295 134512640 134672761 3221224560 3221223664 134559949 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8922 8414 603 41 0 8881 0
vsize: 35688
[startup+230.007 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 8754 0 0 0 22970 31 0 0 25 0 1 0 481919666 37625856 8682 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9186 8682 603 41 0 9145 0
vsize: 36744
[startup+240.007 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 8925 0 0 0 23970 31 0 0 25 0 1 0 481919666 38297600 8853 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9350 8853 603 41 0 9309 0
vsize: 37400
[startup+250.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 9118 0 0 0 24970 32 0 0 25 0 1 0 481919666 39108608 9046 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9548 9046 603 41 0 9507 0
vsize: 38192
[startup+260.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 9295 0 0 0 25969 32 0 0 25 0 1 0 481919666 39780352 9223 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9712 9223 603 41 0 9671 0
vsize: 38848
[startup+270.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 9521 0 0 0 26969 33 0 0 25 0 1 0 481919666 40722432 9449 4294967295 134512640 134672761 3221224560 3221223728 134561156 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9942 9449 603 41 0 9901 0
vsize: 39768
[startup+280.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 9709 0 0 0 27968 33 0 0 25 0 1 0 481919666 41390080 9637 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10105 9637 603 41 0 10064 0
vsize: 40420
[startup+290.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 9884 0 0 0 28968 34 0 0 25 0 1 0 481919666 42192896 9812 4294967295 134512640 134672761 3221224560 3221223732 134556646 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10301 9812 603 41 0 10260 0
vsize: 41204
[startup+300.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 10053 0 0 0 29967 34 0 0 25 0 1 0 481919666 43388928 9981 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10593 9981 603 41 0 10552 0
vsize: 42372
[startup+310.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 10129 0 0 0 30967 35 0 0 25 0 1 0 481919666 43655168 10057 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10658 10057 603 41 0 10617 0
vsize: 42632
[startup+320.009 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 10265 0 0 0 31967 35 0 0 25 0 1 0 481919666 44191744 10193 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10789 10193 603 41 0 10748 0
vsize: 43156
[startup+330.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 10380 0 0 0 32966 36 0 0 25 0 1 0 481919666 44728320 10308 4294967295 134512640 134672761 3221224560 3221223664 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10920 10308 603 41 0 10879 0
vsize: 43680
[startup+340.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 10606 0 0 0 33966 36 0 0 25 0 1 0 481919666 45535232 10534 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11117 10534 603 41 0 11076 0
vsize: 44468
[startup+350.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 10756 0 0 0 34966 37 0 0 25 0 1 0 481919666 46202880 10684 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11280 10684 603 41 0 11239 0
vsize: 45120
[startup+360.008 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 10884 0 0 0 35965 38 0 0 25 0 1 0 481919666 46735360 10812 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11410 10812 603 41 0 11369 0
vsize: 45640
[startup+370.009 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 11172 0 0 0 36965 38 0 0 25 0 1 0 481919666 47816704 11100 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11674 11100 603 41 0 11633 0
vsize: 46696
[startup+380.009 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 11382 0 0 0 37964 39 0 0 25 0 1 0 481919666 48750592 11310 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11902 11310 603 41 0 11861 0
vsize: 47608
[startup+390.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 11493 0 0 0 38964 39 0 0 25 0 1 0 481919666 49152000 11421 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12000 11421 603 41 0 11959 0
vsize: 48000
[startup+400.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 11574 0 0 0 39964 40 0 0 25 0 1 0 481919666 49422336 11502 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12066 11502 603 41 0 12025 0
vsize: 48264
[startup+410.009 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 11842 0 0 0 40963 41 0 0 25 0 1 0 481919666 50495488 11770 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12328 11770 603 41 0 12287 0
vsize: 49312
[startup+420.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 12000 0 0 0 41963 41 0 0 25 0 1 0 481919666 51163136 11928 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12491 11928 603 41 0 12450 0
vsize: 49964
[startup+430.009 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 12153 0 0 0 42962 42 0 0 25 0 1 0 481919666 51830784 12081 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12654 12081 603 41 0 12613 0
vsize: 50616
[startup+440.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 12214 0 0 0 43962 42 0 0 25 0 1 0 481919666 52101120 12142 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12720 12142 603 41 0 12679 0
vsize: 50880
[startup+450.009 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 12322 0 0 0 44962 43 0 0 25 0 1 0 481919666 52506624 12250 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12819 12250 603 41 0 12778 0
vsize: 51276
[startup+460.009 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 12454 0 0 0 45961 43 0 0 25 0 1 0 481919666 53039104 12382 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12949 12382 603 41 0 12908 0
vsize: 51796
[startup+470.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 12645 0 0 0 46961 44 0 0 25 0 1 0 481919666 53841920 12573 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13145 12573 603 41 0 13104 0
vsize: 52580
[startup+480.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 12912 0 0 0 47961 44 0 0 25 0 1 0 481919666 54910976 12840 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13406 12840 603 41 0 13365 0
vsize: 53624
[startup+490.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13023 0 0 0 48961 45 0 0 25 0 1 0 481919666 55308288 12951 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13503 12951 603 41 0 13462 0
vsize: 54012
[startup+500.011 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13255 0 0 0 49960 45 0 0 25 0 1 0 481919666 56250368 13183 4294967295 134512640 134672761 3221224560 3221223728 134561220 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13733 13183 603 41 0 13692 0
vsize: 54932
[startup+510.011 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 50959 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223744 134558694 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+520.011 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 51959 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+530.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 52959 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+540.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 53959 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+550.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 54959 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+560.011 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 55959 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+570.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 56959 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223724 134561235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+580.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 57960 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+590.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 58960 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+600.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 59960 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223732 134556602 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+610.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 60960 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+620.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 61960 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+630.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 62961 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+640.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 63961 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+650.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 64960 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+660.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 65961 46 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+670.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 66960 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+680.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 67959 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+690.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 68959 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+700.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 69959 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+710.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 70959 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+720.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 71959 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+730.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 72960 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+740.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 73960 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223664 134560410 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+750.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 74960 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+760.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13310 0 0 0 75960 47 0 0 25 0 1 0 481919666 56520704 13238 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13799 13238 603 41 0 13758 0
vsize: 55196
[startup+770.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13448 0 0 0 76960 47 0 0 25 0 1 0 481919666 57061376 13376 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13931 13376 603 41 0 13890 0
vsize: 55724
[startup+780.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13647 0 0 0 77960 48 0 0 25 0 1 0 481919666 57872384 13575 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14129 13575 603 41 0 14088 0
vsize: 56516
[startup+790.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 13843 0 0 0 78960 48 0 0 25 0 1 0 481919666 58683392 13771 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14327 13771 603 41 0 14286 0
vsize: 57308
[startup+800.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 14049 0 0 0 79959 49 0 0 25 0 1 0 481919666 59482112 13977 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14522 13977 603 41 0 14481 0
vsize: 58088
[startup+810.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 14187 0 0 0 80959 49 0 0 25 0 1 0 481919666 60030976 14115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14656 14115 603 41 0 14615 0
vsize: 58624
[startup+820.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 14358 0 0 0 81959 50 0 0 25 0 1 0 481919666 60837888 14286 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14853 14286 603 41 0 14812 0
vsize: 59412
[startup+830.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 14507 0 0 0 82958 50 0 0 25 0 1 0 481919666 61378560 14435 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14985 14435 603 41 0 14944 0
vsize: 59940
[startup+840.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 14774 0 0 0 83958 51 0 0 25 0 1 0 481919666 62459904 14702 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15249 14702 603 41 0 15208 0
vsize: 60996
[startup+850.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 15091 0 0 0 84956 52 0 0 25 0 1 0 481919666 63795200 15019 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15575 15019 603 41 0 15534 0
vsize: 62300
[startup+860.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 15346 0 0 0 85956 53 0 0 25 0 1 0 481919666 64737280 15274 4294967295 134512640 134672761 3221224560 3221223664 134560025 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15805 15274 603 41 0 15764 0
vsize: 63220
[startup+870.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 15564 0 0 0 86955 54 0 0 25 0 1 0 481919666 65679360 15492 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16035 15492 603 41 0 15994 0
vsize: 64140
[startup+880.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 15779 0 0 0 87955 55 0 0 25 0 1 0 481919666 66490368 15707 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16233 15707 603 41 0 16192 0
vsize: 64932
[startup+890.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 15946 0 0 0 88954 55 0 0 25 0 1 0 481919666 67162112 15874 4294967295 134512640 134672761 3221224560 3221223744 134559405 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16397 15874 603 41 0 16356 0
vsize: 65588
[startup+900.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16180 0 0 0 89954 56 0 0 25 0 1 0 481919666 68120576 16108 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16631 16108 603 41 0 16590 0
vsize: 66524
[startup+910.012 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16354 0 0 0 90953 56 0 0 25 0 1 0 481919666 68788224 16282 4294967295 134512640 134672761 3221224560 3221223684 134566065 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16794 16282 603 41 0 16753 0
vsize: 67176
[startup+920.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16605 0 0 0 91953 57 0 0 25 0 1 0 481919666 69865472 16533 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17057 16533 603 41 0 17016 0
vsize: 68228
[startup+930.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 92953 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+940.013 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 93953 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+950.014 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 94953 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+960.014 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 95954 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223684 134566122 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+970.014 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 96953 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+980.015 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 97954 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+990.014 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 98954 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1000.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 99954 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1010.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 100954 57 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223664 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1020.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 101954 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223744 134559415 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1030.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 102954 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223696 134565080 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1040.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 103955 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1050.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 104955 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1060.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 105955 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223768 134561962 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1070.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 106955 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1080.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 107955 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 108956 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223744 134559354 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1100.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 109956 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1110.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 110956 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1120.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 111956 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1130.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 112956 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 113956 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1150.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 114957 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1160.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 115957 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1170.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 116957 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1180.01 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 117957 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223664 134559908 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 118957 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223728 134561234 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.99 0.93 2/54 8725
Raw data (stat): 8723 (minisat+) R 8722 3260 3259 0 -1 0 16668 0 0 0 119957 58 0 0 25 0 1 0 481919666 70131712 16596 4294967295 134512640 134672761 3221224560 3221223744 134559613 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17122 16596 603 41 0 17081 0
vsize: 68488
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 0.99 0.93 1/54 8725
Raw data (stat): 8723 (minisat+) Z 8722 3260 3259 0 -1 12 16670 0 0 0 119958 61 0 0 25 0 1 0 481919666 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.05
CPU time (s): 1200.19
CPU user time (s): 1199.58
CPU system time (s): 0.613906
CPU usage (%): 100.012
Max. virtual memory (Kb): 68488
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####