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:3-13,25,26.opb
MD5SUM	85cf0fb6ed84e77eea7ef88259fe2fe8
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	104
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	16.5575
Number of variables	4644
Total number of constraints	35898
Number of constraints which are clauses	30228
Number of constraints which are cardinality constraints (but not clauses)	5592
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 6458

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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:        837260 kB
Buffers:         35276 kB
Cached:         124832 kB
SwapCached:       3160 kB
Active:          72388 kB
Inactive:        93784 kB
HighTotal:      131008 kB
HighFree:         2744 kB
LowTotal:       903652 kB
LowFree:        834516 kB
SwapTotal:     2097892 kB
SwapFree:      2094732 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6924 kB
Slab:            25820 kB
Committed_AS:    63480 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:23:14 (client local time) WITH STATUS 0 IN 1200.19 SECONDS
stats: 4873 7 1200.19 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 31428 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[31427]---> BDD-cost:   56
c ---[31426]---> BDD-cost:   56
c ---[31425]---> BDD-cost:   56
c ---[31424]---> BDD-cost:   56
c ---[31423]---> BDD-cost:   56
c ---[31422]---> BDD-cost:   56
c ---[31421]---> BDD-cost:  100
c ---[31420]---> BDD-cost:  100
c ---[31419]---> BDD-cost:  100
c ---[31418]---> BDD-cost:  100
c ---[31417]---> BDD-cost:  100
c ---[31416]---> BDD-cost:  100
c ---[31415]---> BDD-cost:  122
c ---[31414]---> BDD-cost:  122
c ---[31413]---> BDD-cost:  122
c ---[31412]---> BDD-cost:  122
c ---[31411]---> BDD-cost:  122
c ---[31410]---> BDD-cost:  122
c ---[31409]---> BDD-cost:  122
c ---[31408]---> BDD-cost:  122
c ---[31407]---> BDD-cost:  122
c ---[31406]---> BDD-cost:  122
c ---[31405]---> BDD-cost:  122
c ---[31404]---> BDD-cost:  122
c ---[31403]---> BDD-cost:  122
c ---[31402]---> BDD-cost:  122
c ---[31401]---> BDD-cost:  122
c ---[31400]---> BDD-cost:  122
c ---[31399]---> BDD-cost:  122
c ---[31398]---> BDD-cost:  122
c ---[31397]---> BDD-cost:  132
c ---[31396]---> BDD-cost:  132
c ---[31395]---> BDD-cost:  132
c ---[31394]---> BDD-cost:  132
c ---[31393]---> BDD-cost:  132
c ---[31392]---> BDD-cost:  132
c ---[31391]---> BDD-cost:  122
c ---[31390]---> BDD-cost:  122
c ---[31389]---> BDD-cost:  122
c ---[31388]---> BDD-cost:  122
c ---[31387]---> BDD-cost:  122
c ---[31386]---> BDD-cost:  122
c ---[31385]---> BDD-cost:  122
c ---[31384]---> BDD-cost:  122
c ---[31383]---> BDD-cost:  122
c ---[31382]---> BDD-cost:  122
c ---[31381]---> BDD-cost:  122
c ---[31380]---> BDD-cost:  122
c ---[31379]---> BDD-cost:  122
c ---[31378]---> BDD-cost:  122
c ---[31377]---> BDD-cost:  122
c ---[31376]---> BDD-cost:  122
c ---[31375]---> BDD-cost:  122
c ---[31374]---> BDD-cost:  122
c ---[31373]---> Sorter-cost:  524     Base: 2 2
c ---[31372]---> Sorter-cost:  524     Base: 2 2
c ---[31371]---> Sorter-cost:  524     Base: 2 2
c ---[31370]---> Sorter-cost:  524     Base: 2 2
c ---[31369]---> Sorter-cost:  524     Base: 2 2
c ---[31368]---> Sorter-cost:  524     Base: 2 2
c ---[31367]---> Sorter-cost:  524     Base: 2 2
c ---[31366]---> Sorter-cost:  524     Base: 2 2
c ---[31365]---> Sorter-cost:  524     Base: 2 2
c ---[31364]---> Sorter-cost:  524     Base: 2 2
c ---[31363]---> Sorter-cost:  524     Base: 2 2
c ---[31362]---> Sorter-cost:  524     Base: 2 2
c ---[31361]---> BDD-cost:   64
c ---[31360]---> BDD-cost:   64
c ---[31359]---> BDD-cost:   64
c ---[31358]---> BDD-cost:   64
c ---[31357]---> BDD-cost:   64
c ---[31356]---> BDD-cost:   64
c ---[31355]---> BDD-cost:   64
c ---[31354]---> BDD-cost:   64
c ---[31353]---> BDD-cost:   64
c ---[31352]---> BDD-cost:   64
c ---[31351]---> BDD-cost:   64
c ---[31350]---> BDD-cost:   64
c ---[31348]---> BDD-cost:   23
c ---[31346]---> BDD-cost:   23
c ---[31344]---> BDD-cost:   23
c ---[31342]---> BDD-cost:   23
c ---[31340]---> BDD-cost:   23
c ---[31338]---> BDD-cost:   23
c ---[31336]---> BDD-cost:   23
c ---[31334]---> BDD-cost:   23
c ---[31332]---> BDD-cost:   23
c ---[31330]---> BDD-cost:   23
c ---[31328]---> BDD-cost:   23
c ---[31326]---> BDD-cost:   23
c ---[31324]---> BDD-cost:   23
c ---[31322]---> BDD-cost:   23
c ---[31320]---> BDD-cost:   23
c ---[31318]---> BDD-cost:   23
c ---[31316]---> BDD-cost:   23
c ---[31314]---> BDD-cost:   23
c ---[31312]---> BDD-cost:   21
c ---[31310]---> BDD-cost:   21
c ---[31308]---> BDD-cost:   21
c ---[31306]---> BDD-cost:   21
c ---[31304]---> BDD-cost:   21
c ---[31302]---> BDD-cost:   21
c ---[31300]---> BDD-cost:   23
c ---[31298]---> BDD-cost:   23
c ---[31296]---> BDD-cost:   23
c ---[31294]---> BDD-cost:   23
c ---[31292]---> BDD-cost:   23
c ---[31290]---> BDD-cost:   23
c ---[31288]---> BDD-cost:   23
c ---[31286]---> BDD-cost:   23
c ---[31284]---> BDD-cost:   23
c ---[31282]---> BDD-cost:   23
c ---[31280]---> BDD-cost:   23
c ---[31278]---> BDD-cost:   23
c ---[31276]---> BDD-cost:   21
c ---[31274]---> BDD-cost:   21
c ---[31272]---> BDD-cost:   21
c ---[31270]---> BDD-cost:   21
c ---[31268]---> BDD-cost:   21
c ---[31266]---> BDD-cost:   21
c ---[31264]---> BDD-cost:   17
c ---[31262]---> BDD-cost:   17
c ---[31260]---> BDD-cost:   17
c ---[31258]---> BDD-cost:   17
c ---[31256]---> BDD-cost:   17
c ---[31254]---> BDD-cost:   17
c ---[31252]---> BDD-cost:   23
c ---[31250]---> BDD-cost:   23
c ---[31248]---> BDD-cost:   23
c ---[31246]---> BDD-cost:   23
c ---[31244]---> BDD-cost:   23
c ---[31242]---> BDD-cost:   23
c ---[31240]---> BDD-cost:   23
c ---[31238]---> BDD-cost:   23
c ---[31236]---> BDD-cost:   23
c ---[31234]---> BDD-cost:   23
c ---[31232]---> BDD-cost:   23
c ---[31230]---> BDD-cost:   23
c ---[31228]---> BDD-cost:   23
c ---[31226]---> BDD-cost:   23
c ---[31224]---> BDD-cost:   23
c ---[31222]---> BDD-cost:   23
c ---[31220]---> BDD-cost:   23
c ---[31218]---> BDD-cost:   23
c ---[31216]---> BDD-cost:   21
c ---[31214]---> BDD-cost:   21
c ---[31212]---> BDD-cost:   21
c ---[31210]---> BDD-cost:   21
c ---[31208]---> BDD-cost:   21
c ---[31206]---> BDD-cost:   21
c ---[31204]---> BDD-cost:   23
c ---[31202]---> BDD-cost:   23
c ---[31200]---> BDD-cost:   23
c ---[31198]---> BDD-cost:   23
c ---[31196]---> BDD-cost:   23
c ---[31194]---> BDD-cost:   23
c ---[31192]---> BDD-cost:   23
c ---[31190]---> BDD-cost:   23
c ---[31188]---> BDD-cost:   23
c ---[31186]---> BDD-cost:   23
c ---[31184]---> BDD-cost:   23
c ---[31182]---> BDD-cost:   23
c ---[31180]---> BDD-cost:   23
c ---[31178]---> BDD-cost:   23
c ---[31176]---> BDD-cost:   23
c ---[31174]---> BDD-cost:   23
c ---[31172]---> BDD-cost:   23
c ---[31170]---> BDD-cost:   23
c ---[31168]---> BDD-cost:   23
c ---[31166]---> BDD-cost:   23
c ---[31164]---> BDD-cost:   23
c ---[31162]---> BDD-cost:   23
c ---[31160]---> BDD-cost:   23
c ---[31158]---> BDD-cost:   23
c ---[31156]---> BDD-cost:   23
c ---[31154]---> BDD-cost:   23
c ---[31152]---> BDD-cost:   23
c ---[31150]---> BDD-cost:   23
c ---[31148]---> BDD-cost:   23
c ---[31146]---> BDD-cost:   23
c ---[31144]---> BDD-cost:   23
c ---[31142]---> BDD-cost:   23
c ---[31140]---> BDD-cost:   23
c ---[31138]---> BDD-cost:   23
c ---[31136]---> BDD-cost:   23
c ---[31134]---> BDD-cost:   23
c ---[31132]---> BDD-cost:   23
c ---[31130]---> BDD-cost:   23
c ---[31128]---> BDD-cost:   23
c ---[31126]---> BDD-cost:   23
c ---[31124]---> BDD-cost:   23
c ---[31122]---> BDD-cost:   23
c ---[31120]---> BDD-cost:   23
c ---[31118]---> BDD-cost:   23
c ---[31116]---> BDD-cost:   23
c ---[31114]---> BDD-cost:   23
c ---[31112]---> BDD-cost:   23
c ---[31110]---> BDD-cost:   23
c ---[31108]---> BDD-cost:   23
c ---[31106]---> BDD-cost:   23
c ---[31104]---> BDD-cost:   23
c ---[31102]---> BDD-cost:   23
c ---[31100]---> BDD-cost:   23
c ---[31098]---> BDD-cost:   23
c ---[31096]---> BDD-cost:   23
c ---[31094]---> BDD-cost:   23
c ---[31092]---> BDD-cost:   23
c ---[31090]---> BDD-cost:   23
c ---[31088]---> BDD-cost:   23
c ---[31086]---> BDD-cost:   23
c ---[31084]---> BDD-cost:   23
c ---[31082]---> BDD-cost:   23
c ---[31080]---> BDD-cost:   23
c ---[31078]---> BDD-cost:   23
c ---[31076]---> BDD-cost:   23
c ---[31074]---> BDD-cost:   23
c ---[31072]---> BDD-cost:   23
c ---[31070]---> BDD-cost:   23
c ---[31068]---> BDD-cost:   23
c ---[31066]---> BDD-cost:   23
c ---[31064]---> BDD-cost:   23
c ---[31062]---> BDD-cost:   23
c ---[31060]---> BDD-cost:   23
c ---[31058]---> BDD-cost:   23
c ---[31056]---> BDD-cost:   23
c ---[31054]---> BDD-cost:   23
c ---[31052]---> BDD-cost:   23
c ---[31050]---> BDD-cost:   23
c ---[31048]---> BDD-cost:   17
c ---[31046]---> BDD-cost:   17
c ---[31044]---> BDD-cost:   17
c ---[31042]---> BDD-cost:   17
c ---[31040]---> BDD-cost:   17
c ---[31038]---> BDD-cost:   17
c ---[31036]---> BDD-cost:   23
c ---[31034]---> BDD-cost:   23
c ---[31032]---> BDD-cost:   23
c ---[31030]---> BDD-cost:   23
c ---[31028]---> BDD-cost:   23
c ---[31026]---> BDD-cost:   23
c ---[31024]---> BDD-cost:   23
c ---[31022]---> BDD-cost:   23
c ---[31020]---> BDD-cost:   23
c ---[31018]---> BDD-cost:   23
c ---[31016]---> BDD-cost:   23
c ---[31014]---> BDD-cost:   23
c ---[31012]---> BDD-cost:   23
c ---[31010]---> BDD-cost:   23
c ---[31008]---> BDD-cost:   23
c ---[31006]---> BDD-cost:   23
c ---[31004]---> BDD-cost:   23
c ---[31002]---> BDD-cost:   23
c ---[31001]---> BDD-cost:    9
c ---[31000]---> BDD-cost:    9
c ---[30999]---> BDD-cost:    9
c ---[30998]---> BDD-cost:    9
c ---[30997]---> BDD-cost:    9
c ---[30996]---> BDD-cost:    9
c ---[30995]---> BDD-cost:    9
c ---[30994]---> BDD-cost:    9
c ---[30993]---> BDD-cost:    9
c ---[30992]---> BDD-cost:    9
c ---[30991]---> BDD-cost:    9
c ---[30990]---> BDD-cost:    9
c ---[30989]---> BDD-cost:    9
c ---[30988]---> BDD-cost:    9
c ---[30987]---> BDD-cost:    9
c ---[30986]---> BDD-cost:    9
c ---[30985]---> BDD-cost:    9
c ---[30984]---> BDD-cost:    9
c ---[30983]---> BDD-cost:    9
c ---[30982]---> BDD-cost:    9
c ---[30981]---> BDD-cost:    9
c ---[30980]---> BDD-cost:    9
c ---[30979]---> BDD-cost:    9
c ---[30978]---> BDD-cost:    9
c ---[30977]---> BDD-cost:    9
c ---[30976]---> BDD-cost:    9
c ---[30975]---> BDD-cost:    9
c ---[30974]---> BDD-cost:    9
c ---[30973]---> BDD-cost:    9
c ---[30972]---> BDD-cost:    9
c ---[30971]---> BDD-cost:    9
c ---[30970]---> BDD-cost:    9
c ---[30969]---> BDD-cost:    9
c ---[30968]---> BDD-cost:    9
c ---[30967]---> BDD-cost:    9
c ---[30966]---> BDD-cost:    9
c ---[30965]---> BDD-cost:    9
c ---[30964]---> BDD-cost:    9
c ---[30963]---> BDD-cost:    9
c ---[30962]---> BDD-cost:    9
c ---[30961]---> BDD-cost:    9
c ---[30960]---> BDD-cost:    9
c ---[30959]---> BDD-cost:    9
c ---[30958]---> BDD-cost:    9
c ---[30957]---> BDD-cost:    9
c ---[30956]---> BDD-cost:    9
c ---[30955]---> BDD-cost:    9
c ---[30954]---> BDD-cost:    9
c ---[30953]---> BDD-cost:    9
c ---[30952]---> BDD-cost:    9
c ---[30951]---> BDD-cost:    9
c ---[30950]---> BDD-cost:    9
c ---[30949]---> BDD-cost:    9
c ---[30948]---> BDD-cost:    9
c ---[30947]---> BDD-cost:    9
c ---[30946]---> BDD-cost:    9
c ---[30945]---> BDD-cost:    9
c ---[30944]---> BDD-cost:    9
c ---[30943]---> BDD-cost:    9
c ---[30942]---> BDD-cost:    9
c ---[30941]---> BDD-cost:    9
c ---[30940]---> BDD-cost:    9
c ---[30939]---> BDD-cost:    9
c ---[30938]---> BDD-cost:    9
c ---[30937]---> BDD-cost:    9
c ---[30936]---> BDD-cost:    9
c ---[30935]---> BDD-cost:    9
c ---[30934]---> BDD-cost:    9
c ---[30933]---> BDD-cost:    9
c ---[30932]---> BDD-cost:    9
c ---[30931]---> BDD-cost:    9
c ---[30930]---> BDD-cost:    9
c ---[30929]---> BDD-cost:    9
c ---[30928]---> BDD-cost:    9
c ---[30927]---> BDD-cost:    9
c ---[30926]---> BDD-cost:    9
c ---[30925]---> BDD-cost:    9
c ---[30924]---> BDD-cost:    9
c ---[30923]---> BDD-cost:    9
c ---[30922]---> BDD-cost:    9
c ---[30921]---> BDD-cost:    9
c ---[30920]---> BDD-cost:    9
c ---[30919]---> BDD-cost:    9
c ---[30918]---> BDD-cost:    9
c ---[30917]---> BDD-cost:    9
c ---[30916]---> BDD-cost:    9
c ---[30915]---> BDD-cost:    9
c ---[30914]---> BDD-cost:    9
c ---[30913]---> BDD-cost:    9
c ---[30912]---> BDD-cost:    9
c ---[30911]---> BDD-cost:    9
c ---[30910]---> BDD-cost:    9
c ---[30909]---> BDD-cost:    9
c ---[30908]---> BDD-cost:    9
c ---[30907]---> BDD-cost:    9
c ---[30906]---> BDD-cost:    9
c ---[30905]---> BDD-cost:    9
c ---[30904]---> BDD-cost:    9
c ---[30903]---> BDD-cost:    9
c ---[30902]---> BDD-cost:    9
c ---[30901]---> BDD-cost:    9
c ---[30900]---> BDD-cost:    9
c ---[30899]---> BDD-cost:    9
c ---[30898]---> BDD-cost:    9
c ---[30897]---> BDD-cost:    9
c ---[30896]---> BDD-cost:    9
c ---[30895]---> BDD-cost:    9
c ---[30894]---> BDD-cost:    9
c ---[30893]---> BDD-cost:    9
c ---[30892]---> BDD-cost:    9
c ---[30891]---> BDD-cost:    9
c ---[30890]---> BDD-cost:    9
c ---[30889]---> BDD-cost:    9
c ---[30888]---> BDD-cost:    9
c ---[30887]---> BDD-cost:    9
c ---[30886]---> BDD-cost:    9
c ---[30885]---> BDD-cost:    9
c ---[30884]---> BDD-cost:    9
c ---[30883]---> BDD-cost:    9
c ---[30882]---> BDD-cost:    9
c ---[30881]---> BDD-cost:    9
c ---[30880]---> BDD-cost:    9
c ---[30879]---> BDD-cost:    9
c ---[30878]---> BDD-cost:    9
c ---[30877]---> BDD-cost:    9
c ---[30876]---> BDD-cost:    9
c ---[30875]---> BDD-cost:    9
c ---[30874]---> BDD-cost:    9
c ---[30873]---> BDD-cost:    9
c ---[30872]---> BDD-cost:    9
c ---[30871]---> BDD-cost:    9
c ---[30870]---> BDD-cost:    9
c ---[30869]---> BDD-cost:    9
c ---[30868]---> BDD-cost:    9
c ---[30867]---> BDD-cost:    9
c ---[30866]---> BDD-cost:    9
c ---[30865]---> BDD-cost:    9
c ---[30864]---> BDD-cost:    9
c ---[30863]---> BDD-cost:    9
c ---[30862]---> BDD-cost:    9
c ---[30861]---> BDD-cost:    9
c ---[30860]---> BDD-cost:    9
c ---[30859]---> BDD-cost:    9
c ---[30858]---> BDD-cost:    9
c ---[30857]---> BDD-cost:    9
c ---[30856]---> BDD-cost:    9
c ---[30855]---> BDD-cost:    9
c ---[30854]---> BDD-cost:    9
c ---[30853]---> BDD-cost:    9
c ---[30852]---> BDD-cost:    9
c ---[30851]---> BDD-cost:    9
c ---[30850]---> BDD-cost:    9
c ---[30849]---> BDD-cost:    9
c ---[30848]---> BDD-cost:    9
c ---[30847]---> BDD-cost:    9
c ---[30846]---> BDD-cost:    9
c ---[30845]---> BDD-cost:    9
c ---[30844]---> BDD-cost:    9
c ---[30843]---> BDD-cost:    9
c ---[30842]---> BDD-cost:    9
c ---[30841]---> BDD-cost:    9
c ---[30840]---> BDD-cost:    9
c ---[30839]---> BDD-cost:    9
c ---[30838]---> BDD-cost:    9
c ---[30837]---> BDD-cost:    9
c ---[30836]---> BDD-cost:    9
c ---[30835]---> BDD-cost:    9
c ---[30834]---> BDD-cost:    9
c ---[30833]---> BDD-cost:    9
c ---[30832]---> BDD-cost:    9
c ---[30831]---> BDD-cost:    9
c ---[30830]---> BDD-cost:    9
c ---[30829]---> BDD-cost:    9
c ---[30828]---> BDD-cost:    9
c ---[30827]---> BDD-cost:    9
c ---[30826]---> BDD-cost:    9
c ---[30825]---> BDD-cost:    9
c ---[30824]---> BDD-cost:    9
c ---[30823]---> BDD-cost:    9
c ---[30822]---> BDD-cost:    9
c ---[30821]---> BDD-cost:    9
c ---[30820]---> BDD-cost:    9
c ---[30819]---> BDD-cost:    9
c ---[30818]---> BDD-cost:    9
c ---[30817]---> BDD-cost:    9
c ---[30816]---> BDD-cost:    9
c ---[30815]---> BDD-cost:    9
c ---[30814]---> BDD-cost:    9
c ---[30813]---> BDD-cost:    9
c ---[30812]---> BDD-cost:    9
c ---[30811]---> BDD-cost:    9
c ---[30810]---> BDD-cost:    9
c ---[30809]---> BDD-cost:    9
c ---[30808]---> BDD-cost:    9
c ---[30807]---> BDD-cost:    9
c ---[30806]---> BDD-cost:    9
c ---[30805]---> BDD-cost:    9
c ---[30804]---> BDD-cost:    9
c ---[30803]---> BDD-cost:    9
c ---[30802]---> BDD-cost:    9
c ---[30801]---> BDD-cost:    9
c ---[30800]---> BDD-cost:    9
c ---[30799]---> BDD-cost:    9
c ---[30798]---> BDD-cost:    9
c ---[30797]---> BDD-cost:    9
c ---[30796]---> BDD-cost:    9
c ---[30795]---> BDD-cost:    9
c ---[30794]---> BDD-cost:    9
c ---[30793]---> BDD-cost:    9
c ---[30792]---> BDD-cost:    9
c ---[30791]---> BDD-cost:    9
c ---[30790]---> BDD-cost:    9
c ---[30789]---> BDD-cost:    9
c ---[30788]---> BDD-cost:    9
c ---[30787]---> BDD-cost:    9
c ---[30786]---> BDD-cost:    9
c ---[30785]---> BDD-cost:    9
c ---[30784]---> BDD-cost:    9
c ---[30783]---> BDD-cost:    9
c ---[30782]---> BDD-cost:    9
c ---[30781]---> BDD-cost:    9
c ---[30780]---> BDD-cost:    9
c ---[30779]---> BDD-cost:    9
c ---[30778]---> BDD-cost:    9
c ---[30777]---> BDD-cost:    9
c ---[30776]---> BDD-cost:    9
c ---[30775]---> BDD-cost:    9
c ---[30774]---> BDD-cost:    9
c ---[30773]---> BDD-cost:    9
c ---[30772]---> BDD-cost:    9
c ---[30771]---> BDD-cost:    9
c ---[30770]---> BDD-cost:    9
c ---[30769]---> BDD-cost:    9
c ---[30768]---> BDD-cost:    9
c ---[30767]---> BDD-cost:    9
c ---[30766]---> BDD-cost:    9
c ---[30765]---> BDD-cost:    9
c ---[30764]---> BDD-cost:    9
c ---[30763]---> BDD-cost:    9
c ---[30762]---> BDD-cost:    9
c ---[30761]---> BDD-cost:    9
c ---[30760]---> BDD-cost:    9
c ---[30759]---> BDD-cost:    9
c ---[30758]---> BDD-cost:    9
c ---[30757]---> BDD-cost:    9
c ---[30756]---> BDD-cost:    9
c ---[30755]---> BDD-cost:    9
c ---[30754]---> BDD-cost:    9
c ---[30753]---> BDD-cost:    9
c ---[30752]---> BDD-cost:    9
c ---[30751]---> BDD-cost:    9
c ---[30750]---> BDD-cost:    9
c ---[30749]---> BDD-cost:    9
c ---[30748]---> BDD-cost:    9
c ---[30747]---> BDD-cost:    9
c ---[30746]---> BDD-cost:    9
c ---[30745]---> BDD-cost:    9
c ---[30744]---> BDD-cost:    9
c ---[30743]---> BDD-cost:    9
c ---[30742]---> BDD-cost:    9
c ---[30741]---> BDD-cost:    9
c ---[30740]---> BDD-cost:    9
c ---[30739]---> BDD-cost:    9
c ---[30738]---> BDD-cost:    9
c ---[30737]---> BDD-cost:    9
c ---[30736]---> BDD-cost:    9
c ---[30735]---> BDD-cost:    9
c ---[30734]---> BDD-cost:    9
c ---[30733]---> BDD-cost:    9
c ---[30732]---> BDD-cost:    9
c ---[30731]---> BDD-cost:    9
c ---[30730]---> BDD-cost:    9
c ---[30729]---> BDD-cost:    9
c ---[30728]---> BDD-cost:    9
c ---[30727]---> BDD-cost:    9
c ---[30726]---> BDD-cost:    9
c ---[30725]---> BDD-cost:    9
c ---[30724]---> BDD-cost:    9
c ---[30723]---> BDD-cost:    9
c ---[30722]---> BDD-cost:    9
c ---[30721]---> BDD-cost:    9
c ---[30720]---> BDD-cost:    9
c ---[30719]---> BDD-cost:    9
c ---[30718]---> BDD-cost:    9
c ---[30717]---> BDD-cost:    9
c ---[30716]---> BDD-cost:    9
c ---[30715]---> BDD-cost:    9
c ---[30714]---> BDD-cost:    9
c ---[30713]---> BDD-cost:    9
c ---[30712]---> BDD-cost:    9
c ---[30711]---> BDD-cost:    9
c ---[30710]---> BDD-cost:    9
c ---[30709]---> BDD-cost:    9
c ---[30708]---> BDD-cost:    9
c ---[30707]---> BDD-cost:    9
c ---[30706]---> BDD-cost:    9
c ---[30705]---> BDD-cost:    9
c ---[30704]---> BDD-cost:    9
c ---[30703]---> BDD-cost:    9
c ---[30702]---> BDD-cost:    9
c ---[30701]---> BDD-cost:    9
c ---[30700]---> BDD-cost:    9
c ---[30699]---> BDD-cost:    9
c ---[30698]---> BDD-cost:    9
c ---[30697]---> BDD-cost:    9
c ---[30696]---> BDD-cost:    9
c ---[30695]---> BDD-cost:    9
c ---[30694]---> BDD-cost:    9
c ---[30693]---> BDD-cost:    9
c ---[30692]---> BDD-cost:    9
c ---[30691]---> BDD-cost:    9
c ---[30690]---> BDD-cost:    9
c ---[30689]---> BDD-cost:    9
c ---[30688]---> BDD-cost:    9
c ---[30687]---> BDD-cost:    9
c ---[30686]---> BDD-cost:    9
c ---[30685]---> BDD-cost:    9
c ---[30684]---> BDD-cost:    9
c ---[30683]---> BDD-cost:    9
c ---[30682]---> BDD-cost:    9
c ---[30681]---> BDD-cost:    9
c ---[30680]---> BDD-cost:    9
c ---[30679]---> BDD-cost:    9
c ---[30678]---> BDD-cost:    9
c ---[30677]---> BDD-cost:    9
c ---[30676]---> BDD-cost:    9
c ---[30675]---> BDD-cost:    9
c ---[30674]---> BDD-cost:    9
c ---[30673]---> BDD-cost:    9
c ---[30672]---> BDD-cost:    9
c ---[30671]---> BDD-cost:    9
c ---[30670]---> BDD-cost:    9
c ---[30669]---> BDD-cost:    9
c ---[30668]---> BDD-cost:    9
c ---[30667]---> BDD-cost:    9
c ---[30666]---> BDD-cost:    9
c ---[30665]---> BDD-cost:    9
c ---[30664]---> BDD-cost:    9
c ---[30663]---> BDD-cost:    9
c ---[30662]---> BDD-cost:    9
c ---[30661]---> BDD-cost:    9
c ---[30660]---> BDD-cost:    9
c ---[30659]---> BDD-cost:    9
c ---[30658]---> BDD-cost:    9
c ---[30657]---> BDD-cost:    9
c ---[30656]---> BDD-cost:    9
c ---[30655]---> BDD-cost:    9
c ---[30654]---> BDD-cost:    9
c ---[30653]---> BDD-cost:    9
c ---[30652]---> BDD-cost:    9
c ---[30651]---> BDD-cost:    9
c ---[30650]---> BDD-cost:    9
c ---[30649]---> BDD-cost:    9
c ---[30648]---> BDD-cost:    9
c ---[30647]---> BDD-cost:    9
c ---[30646]---> BDD-cost:    9
c ---[30645]---> BDD-cost:    9
c ---[30644]---> BDD-cost:    9
c ---[30643]---> BDD-cost:    9
c ---[30642]---> BDD-cost:    9
c ---[30641]---> BDD-cost:    9
c ---[30640]---> BDD-cost:    9
c ---[30639]---> BDD-cost:    9
c ---[30638]---> BDD-cost:    9
c ---[30637]---> BDD-cost:    9
c ---[30636]---> BDD-cost:    9
c ---[30635]---> BDD-cost:    9
c ---[30634]---> 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 |  118548   331488 |   39516       0        0     nan |  0.000 % |
c |       100 |  118428   331128 |   43467      54      171     3.2 |  4.086 % |
c |       251 |  118167   330408 |   47814     132      482     3.7 |  4.308 % |
c |       477 |  117951   329830 |   52595     286     1183     4.1 |  4.502 % |
c |       815 |  117612   328935 |   57855     517     2289     4.4 |  4.817 % |
c |      1321 |  117176   327861 |   63640     802     3711     4.6 |  5.264 % |
c |      2080 |  116472   326146 |   70005    1290     6358     4.9 |  6.080 % |
c |      3221 |  116432   326026 |   77005    2347    24847    10.6 |  6.112 % |
c |      4929 |  115999   324858 |   84706    3776    57280    15.2 |  6.551 % |
c |      7492 |  115944   324693 |   93176    6291   141353    22.5 |  6.594 % |
c |     11336 |  115731   324126 |  102494    9956   265348    26.7 |  6.792 % |
c |     17103 |  115087   322350 |  112743   15157   381202    25.2 |  7.352 % |
c |     25753 |  114206   319889 |  124018   23151   611901    26.4 |  8.145 % |
c |     38727 |  113608   318233 |  136419   35762  1128500    31.6 |  8.720 % |
c |     58189 |  113246   317192 |  150061   54957  1952545    35.5 |  9.027 % |
c |     87383 |  112389   314933 |  165068   83713  3207412    38.3 |  9.906 % |
c |    131173 |  108826   305175 |  181574  125384  4665079    37.2 | 13.319 % |
c |    196857 |  106962   299762 |  199732   21446   703812    32.8 | 14.855 % |
c |    295387 |  105159   294634 |  219705  119085  4671187    39.2 | 16.422 % |
c |    443176 |  102834   288189 |  241676   60350  2275118    37.7 | 18.583 % |
#### 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.86 0.97 0.91 2/54 25355
Raw data (stat): 25355 (runsolver) R 25354 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481918707 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.88 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 3101 0 0 0 989 9 0 0 25 0 1 0 481918707 14364672 3030 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3507 3030 603 41 0 3466 0
vsize: 14028
[startup+20.0005 s]
Raw data (loadavg): 0.90 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 3470 0 0 0 1987 10 0 0 25 0 1 0 481918707 15839232 3399 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3867 3399 603 41 0 3826 0
vsize: 15468
[startup+30.0016 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 3655 0 0 0 2986 11 0 0 25 0 1 0 481918707 16756736 3584 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4091 3584 603 41 0 4050 0
vsize: 16364
[startup+40.0018 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 3988 0 0 0 3984 12 0 0 25 0 1 0 481918707 17969152 3917 4294967295 134512640 134672761 3221224560 3221223664 134560418 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4387 3917 603 41 0 4346 0
vsize: 17548
[startup+50.0019 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 4296 0 0 0 4984 13 0 0 25 0 1 0 481918707 19312640 4225 4294967295 134512640 134672761 3221224560 3221223696 134565045 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4715 4225 603 41 0 4674 0
vsize: 18860
[startup+60.0027 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 4816 0 0 0 5982 14 0 0 25 0 1 0 481918707 21446656 4745 4294967295 134512640 134672761 3221224560 3221223728 134560900 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5236 4745 603 41 0 5195 0
vsize: 20944
[startup+70.0032 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 5309 0 0 0 6981 16 0 0 25 0 1 0 481918707 23453696 5238 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5726 5238 603 41 0 5685 0
vsize: 22904
[startup+80.0044 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 5681 0 0 0 7981 16 0 0 25 0 1 0 481918707 24932352 5610 4294967295 134512640 134672761 3221224560 3221223728 134560882 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6087 5610 603 41 0 6046 0
vsize: 24348
[startup+90.0042 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 6107 0 0 0 8980 18 0 0 25 0 1 0 481918707 26673152 6036 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6512 6036 603 41 0 6471 0
vsize: 26048
[startup+100.004 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 6479 0 0 0 9978 19 0 0 25 0 1 0 481918707 28409856 6408 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6936 6408 603 41 0 6895 0
vsize: 27744
[startup+110.005 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 6750 0 0 0 10978 20 0 0 25 0 1 0 481918707 29478912 6679 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7197 6679 603 41 0 7156 0
vsize: 28788
[startup+120.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 7111 0 0 0 11978 21 0 0 25 0 1 0 481918707 30957568 7040 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7558 7040 603 41 0 7517 0
vsize: 30232
[startup+130.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 7347 0 0 0 12977 22 0 0 25 0 1 0 481918707 31895552 7276 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7787 7276 603 41 0 7746 0
vsize: 31148
[startup+140.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 7488 0 0 0 13977 22 0 0 25 0 1 0 481918707 32440320 7417 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7920 7417 603 41 0 7879 0
vsize: 31680
[startup+150.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25355
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 7531 0 0 0 14977 22 0 0 25 0 1 0 481918707 32706560 7460 4294967295 134512640 134672761 3221224560 3221223744 134558687 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7985 7460 603 41 0 7944 0
vsize: 31940
[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 7632 0 0 0 15977 22 0 0 25 0 1 0 481918707 33107968 7561 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8083 7561 603 41 0 8042 0
vsize: 32332
[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 7877 0 0 0 16977 23 0 0 25 0 1 0 481918707 34045952 7806 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8312 7806 603 41 0 8271 0
vsize: 33248
[startup+180.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 7980 0 0 0 17976 23 0 0 25 0 1 0 481918707 34451456 7909 4294967295 134512640 134672761 3221224560 3221223652 1075346528 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8411 7909 603 41 0 8370 0
vsize: 33644
[startup+190.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 8160 0 0 0 18976 23 0 0 25 0 1 0 481918707 35250176 8089 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8606 8089 603 41 0 8565 0
vsize: 34424
[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 8285 0 0 0 19976 24 0 0 25 0 1 0 481918707 35651584 8214 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8704 8214 603 41 0 8663 0
vsize: 34816
[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 8380 0 0 0 20976 24 0 0 25 0 1 0 481918707 36057088 8309 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8803 8309 603 41 0 8762 0
vsize: 35212
[startup+220.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 8640 0 0 0 21976 24 0 0 25 0 1 0 481918707 37130240 8569 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9065 8569 603 41 0 9024 0
vsize: 36260
[startup+230.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 8790 0 0 0 22976 25 0 0 25 0 1 0 481918707 37666816 8719 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9196 8719 603 41 0 9155 0
vsize: 36784
[startup+240.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 8843 0 0 0 23976 25 0 0 25 0 1 0 481918707 37937152 8772 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9262 8772 603 41 0 9221 0
vsize: 37048
[startup+250.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 8922 0 0 0 24976 25 0 0 25 0 1 0 481918707 38207488 8851 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9328 8851 603 41 0 9287 0
vsize: 37312
[startup+260.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 9034 0 0 0 25976 25 0 0 25 0 1 0 481918707 38748160 8963 4294967295 134512640 134672761 3221224560 3221223732 134556596 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9460 8963 603 41 0 9419 0
vsize: 37840
[startup+270.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 9188 0 0 0 26975 26 0 0 25 0 1 0 481918707 39288832 9117 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9592 9117 603 41 0 9551 0
vsize: 38368
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 9397 0 0 0 27973 27 0 0 25 0 1 0 481918707 40095744 9326 4294967295 134512640 134672761 3221224560 3221223664 134559883 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9789 9326 603 41 0 9748 0
vsize: 39156
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 9679 0 0 0 28973 28 0 0 25 0 1 0 481918707 41832448 9608 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10213 9608 603 41 0 10172 0
vsize: 40852
[startup+300.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 9927 0 0 0 29972 29 0 0 25 0 1 0 481918707 42766336 9856 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10441 9856 603 41 0 10400 0
vsize: 41764
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 10124 0 0 0 30972 29 0 0 25 0 1 0 481918707 43577344 10053 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10639 10053 603 41 0 10598 0
vsize: 42556
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 10341 0 0 0 31971 30 0 0 25 0 1 0 481918707 44515328 10270 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10868 10270 603 41 0 10827 0
vsize: 43472
[startup+330.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 10395 0 0 0 32971 30 0 0 25 0 1 0 481918707 44650496 10324 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10901 10324 603 41 0 10860 0
vsize: 43604
[startup+340.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 10430 0 0 0 33971 30 0 0 25 0 1 0 481918707 44785664 10359 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10934 10359 603 41 0 10893 0
vsize: 43736
[startup+350.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 10568 0 0 0 34971 31 0 0 25 0 1 0 481918707 45457408 10497 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11098 10497 603 41 0 11057 0
vsize: 44392
[startup+360.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 10636 0 0 0 35971 31 0 0 25 0 1 0 481918707 45727744 10565 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11164 10565 603 41 0 11123 0
vsize: 44656
[startup+370.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 10932 0 0 0 36971 32 0 0 25 0 1 0 481918707 46804992 10861 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11427 10861 603 41 0 11386 0
vsize: 45708
[startup+380.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 11149 0 0 0 37970 32 0 0 25 0 1 0 481918707 47742976 11078 4294967295 134512640 134672761 3221224560 3221223728 134560876 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11656 11078 603 41 0 11615 0
vsize: 46624
[startup+390.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 11342 0 0 0 38970 32 0 0 25 0 1 0 481918707 48558080 11271 4294967295 134512640 134672761 3221224560 3221223776 134561990 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11855 11271 603 41 0 11814 0
vsize: 47420
[startup+400.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 11590 0 0 0 39970 33 0 0 25 0 1 0 481918707 49504256 11519 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12086 11519 603 41 0 12045 0
vsize: 48344
[startup+410.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 11780 0 0 0 40969 34 0 0 25 0 1 0 481918707 50302976 11709 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12281 11709 603 41 0 12240 0
vsize: 49124
[startup+420.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12076 0 0 0 41969 35 0 0 25 0 1 0 481918707 51511296 12005 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12576 12005 603 41 0 12535 0
vsize: 50304
[startup+430.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12331 0 0 0 42968 35 0 0 25 0 1 0 481918707 52457472 12260 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12807 12260 603 41 0 12766 0
vsize: 51228
[startup+440.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12422 0 0 0 43968 36 0 0 25 0 1 0 481918707 52867072 12351 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12907 12351 603 41 0 12866 0
vsize: 51628
[startup+450.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 44967 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+460.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 45967 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+470.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 46967 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134561275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+480.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 47967 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+490.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 48967 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+500.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 49967 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223732 134556632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+510.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 50968 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+520.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 51968 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223744 134558645 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+530.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 52968 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+540.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 53968 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+550.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 54968 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223744 134559254 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+560.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 55968 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+570.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 56969 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+580.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 57969 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+590.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 58969 36 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+600.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 59969 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+610.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 60969 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223696 134560608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+620.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 61969 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223744 134559340 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+630.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 62969 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223744 134559569 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+640.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 63969 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+650.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 64969 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+660.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 65970 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+670.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 66970 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+680.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 67970 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223696 134565080 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+690.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 68970 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+700.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12508 0 0 0 69970 37 0 0 25 0 1 0 481918707 53137408 12437 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12973 12437 603 41 0 12932 0
vsize: 51892
[startup+710.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12558 0 0 0 70970 37 0 0 25 0 1 0 481918707 53407744 12487 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13039 12487 603 41 0 12998 0
vsize: 52156
[startup+720.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12767 0 0 0 71970 37 0 0 25 0 1 0 481918707 54353920 12696 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13270 12696 603 41 0 13229 0
vsize: 53080
[startup+730.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 12910 0 0 0 72970 38 0 0 25 0 1 0 481918707 54890496 12839 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13401 12839 603 41 0 13360 0
vsize: 53604
[startup+740.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 13013 0 0 0 73970 38 0 0 25 0 1 0 481918707 55296000 12942 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13500 12942 603 41 0 13459 0
vsize: 54000
[startup+750.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 13260 0 0 0 74969 39 0 0 25 0 1 0 481918707 56365056 13189 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13761 13189 603 41 0 13720 0
vsize: 55044
[startup+760.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 13453 0 0 0 75968 40 0 0 25 0 1 0 481918707 57184256 13382 4294967295 134512640 134672761 3221224560 3221223728 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13961 13382 603 41 0 13920 0
vsize: 55844
[startup+770.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 13720 0 0 0 76967 41 0 0 25 0 1 0 481918707 58273792 13649 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14227 13649 603 41 0 14186 0
vsize: 56908
[startup+780.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 13882 0 0 0 77967 42 0 0 25 0 1 0 481918707 58859520 13811 4294967295 134512640 134672761 3221224560 3221223728 134561266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14370 13811 603 41 0 14329 0
vsize: 57480
[startup+790.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 14244 0 0 0 78966 43 0 0 25 0 1 0 481918707 60354560 14173 4294967295 134512640 134672761 3221224560 3221223664 134560025 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14735 14173 603 41 0 14694 0
vsize: 58940
[startup+800.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 14532 0 0 0 79965 44 0 0 25 0 1 0 481918707 61562880 14461 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15030 14461 603 41 0 14989 0
vsize: 60120
[startup+810.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 14669 0 0 0 80965 44 0 0 25 0 1 0 481918707 62099456 14598 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15161 14598 603 41 0 15120 0
vsize: 60644
[startup+820.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 14825 0 0 0 81965 44 0 0 25 0 1 0 481918707 62763008 14754 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15323 14754 603 41 0 15282 0
vsize: 61292
[startup+830.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15000 0 0 0 82964 45 0 0 25 0 1 0 481918707 63426560 14929 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15485 14929 603 41 0 15444 0
vsize: 61940
[startup+840.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15207 0 0 0 83964 46 0 0 25 0 1 0 481918707 64237568 15136 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15683 15136 603 41 0 15642 0
vsize: 62732
[startup+850.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15471 0 0 0 84963 46 0 0 25 0 1 0 481918707 65310720 15400 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15945 15400 603 41 0 15904 0
vsize: 63780
[startup+860.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 85962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223664 134554671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+870.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 86962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+880.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 87962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+890.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 88962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+900.031 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 89962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223760 134557895 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+910.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 90962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223744 134558332 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+920.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 91962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+930.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 92962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+940.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 93962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+950.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 94962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+960.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 95962 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+970.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 96963 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+980.032 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 97963 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223664 134560174 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+990.033 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 98963 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560948 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 99963 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223696 134560688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 100963 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 101963 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 102964 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 103964 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 104964 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 105964 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 106964 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 107964 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 108965 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 109965 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 110965 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1120.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 111965 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1130.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 112966 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1140.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 113966 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1150.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 114966 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1160.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15832 0 0 0 115966 48 0 0 25 0 1 0 481918707 66781184 15761 4294967295 134512640 134672761 3221224560 3221223664 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16304 15761 603 41 0 16263 0
vsize: 65216
[startup+1170.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 15865 0 0 0 116966 48 0 0 25 0 1 0 481918707 66912256 15794 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16336 15794 603 41 0 16295 0
vsize: 65344
[startup+1180.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 16104 0 0 0 117965 49 0 0 25 0 1 0 481918707 67846144 16033 4294967295 134512640 134672761 3221224560 3221223732 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16564 16033 603 41 0 16523 0
vsize: 66256
[startup+1190.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 16352 0 0 0 118965 50 0 0 25 0 1 0 481918707 68907008 16281 4294967295 134512640 134672761 3221224560 3221223664 134559862 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16823 16281 603 41 0 16782 0
vsize: 67292
[startup+1200.04 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25357
Raw data (stat): 25355 (minisat+) R 25354 18865 18864 0 -1 0 16623 0 0 0 119964 51 0 0 25 0 1 0 481918707 69984256 16552 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17086 16552 603 41 0 17045 0
vsize: 68344
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 25357
Raw data (stat): 25355 (minisat+) Z 25354 18865 18864 0 -1 12 16625 0 0 0 119964 54 0 0 25 0 1 0 481918707 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.07
CPU time (s): 1200.19
CPU user time (s): 1199.65
CPU system time (s): 0.542917
CPU usage (%): 100.01
Max. virtual memory (Kb): 68344
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####