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 5658

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.190
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:        869552 kB
Buffers:         36116 kB
Cached:         105652 kB
SwapCached:       3276 kB
Active:          69696 kB
Inactive:        78204 kB
HighTotal:      131008 kB
HighFree:        21448 kB
LowTotal:       903652 kB
LowFree:        848104 kB
SwapTotal:     2097136 kB
SwapFree:      2093860 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11776 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:39:58 (client local time) WITH STATUS 0 IN 1200.25 SECONDS
stats: 4121 7 1200.25 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   79350   219108 |   23804       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24696          
c   -- var.elim.:  2000/24696          
c   -- var.elim.:  3000/24696          
c   -- var.elim.:  4000/24696          
c   -- var.elim.:  5000/24696          
c   -- var.elim.:  6000/24696          
c   -- var.elim.:  7000/24696          
c   -- var.elim.:  8000/24696          
c   -- var.elim.:  9000/24696          
c   -- var.elim.:  10000/24696          
c   -- var.elim.:  11000/24696          
c   -- var.elim.:  12000/24696          
c   -- var.elim.:  13000/24696          
c   -- var.elim.:  14000/24696          
c   -- var.elim.:  15000/24696          
c   -- var.elim.:  16000/24696          
c   -- var.elim.:  17000/24696          
c   -- var.elim.:  18000/24696          
c   -- var.elim.:  19000/24696          
c   -- var.elim.:  20000/24696          
c   -- var.elim.:  21000/24696          
c   -- var.elim.:  22000/24696          
c   -- var.elim.:  23000/24696          
c   -- var.elim.:  24000/24696          
c   -- var.elim.:  24696/24696          
c   -- var.elim.:  1000/10822          
c   -- var.elim.:  2000/10822          
c   -- var.elim.:  3000/10822          
c   -- var.elim.:  4000/10822          
c   -- var.elim.:  5000/10822          
c   -- var.elim.:  6000/10822          
c   -- var.elim.:  7000/10822          
c   -- var.elim.:  8000/10822          
c   -- var.elim.:  9000/10822          
c   -- var.elim.:  10000/10822          
c   -- var.elim.:  10822/10822          
c   -- var.elim.:  820/820          
c   -- subsuming                       
c   -- var.elim.:  1000/9814          
c   -- var.elim.:  2000/9814          
c   -- var.elim.:  3000/9814          
c   -- var.elim.:  4000/9814          
c   -- var.elim.:  5000/9814          
c   -- var.elim.:  6000/9814          
c   -- var.elim.:  7000/9814          
c   -- var.elim.:  8000/9814          
c   -- var.elim.:  9000/9#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.95 0.90 2/54 18470
Raw data (stat): 18470 (runsolver) R 18469 10720 10719 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422356115 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.87 0.95 0.90 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 5486 0 0 0 982 16 0 0 25 0 1 0 422356115 22540288 4742 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5503 4742 603 41 0 5462 0
vsize: 22012
[startup+20.0002 s]
Raw data (loadavg): 0.89 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 6769 0 0 0 1978 19 0 0 25 0 1 0 422356115 27770880 6025 4294967295 134512640 134672761 3221224560 3221223696 134614670 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6780 6025 603 41 0 6739 0
vsize: 27120
[startup+30.0017 s]
Raw data (loadavg): 0.91 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 7812 0 0 0 2975 23 0 0 25 0 1 0 422356115 32133120 7068 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7845 7068 603 41 0 7804 0
vsize: 31380
[startup+40.0019 s]
Raw data (loadavg): 0.92 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 8592 0 0 0 3972 26 0 0 25 0 1 0 422356115 35352576 7848 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8631 7848 603 41 0 8590 0
vsize: 34524
[startup+50.0027 s]
Raw data (loadavg): 0.93 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 9094 0 0 0 4971 28 0 0 25 0 1 0 422356115 37339136 8350 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9116 8350 603 41 0 9075 0
vsize: 36464
[startup+60.0029 s]
Raw data (loadavg): 0.94 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 9553 0 0 0 5970 28 0 0 25 0 1 0 422356115 39346176 8809 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9606 8809 603 41 0 9565 0
vsize: 38424
[startup+70.0024 s]
Raw data (loadavg): 0.95 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 10165 0 0 0 6969 30 0 0 25 0 1 0 422356115 41795584 9421 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10204 9422 603 41 0 10163 0
vsize: 40816
[startup+80.0033 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 10789 0 0 0 7967 31 0 0 25 0 1 0 422356115 44560384 10045 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10879 10045 603 41 0 10838 0
vsize: 43516
[startup+90.0122 s]
Raw data (loadavg): 0.96 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 11306 0 0 0 8967 33 0 0 25 0 1 0 422356115 46804992 10562 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11427 10562 603 41 0 11386 0
vsize: 45708
[startup+100.013 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 11791 0 0 0 9966 34 0 0 25 0 1 0 422356115 48693248 11047 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11888 11047 603 41 0 11847 0
vsize: 47552
[startup+110.014 s]
Raw data (loadavg): 0.97 0.96 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 12181 0 0 0 10964 36 0 0 25 0 1 0 422356115 50409472 11437 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12307 11437 603 41 0 12266 0
vsize: 49228
[startup+120.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 12522 0 0 0 11964 37 0 0 25 0 1 0 422356115 51765248 11778 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12638 11778 603 41 0 12597 0
vsize: 50552
[startup+130.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 12811 0 0 0 12963 38 0 0 25 0 1 0 422356115 52957184 12067 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12929 12067 603 41 0 12888 0
vsize: 51716
[startup+140.014 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 13262 0 0 0 13962 39 0 0 25 0 1 0 422356115 54820864 12518 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13384 12518 603 41 0 13343 0
vsize: 53536
[startup+150.016 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 13717 0 0 0 14961 40 0 0 25 0 1 0 422356115 56692736 12973 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13841 12973 603 41 0 13800 0
vsize: 55364
[startup+160.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 14132 0 0 0 15960 42 0 0 25 0 1 0 422356115 58413056 13388 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14261 13388 603 41 0 14220 0
vsize: 57044
[startup+170.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 14506 0 0 0 16959 43 0 0 25 0 1 0 422356115 59912192 13762 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14627 13762 603 41 0 14586 0
vsize: 58508
[startup+180.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 14945 0 0 0 17958 44 0 0 25 0 1 0 422356115 61775872 14201 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15082 14201 603 41 0 15041 0
vsize: 60328
[startup+190.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 15318 0 0 0 18957 45 0 0 25 0 1 0 422356115 63270912 14574 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15447 14574 603 41 0 15406 0
vsize: 61788
[startup+200.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 15729 0 0 0 19956 46 0 0 25 0 1 0 422356115 64864256 14985 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15836 14985 603 41 0 15795 0
vsize: 63344
[startup+210.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16246 0 0 0 20955 47 0 0 25 0 1 0 422356115 66981888 15502 4294967295 134512640 134672761 3221224560 3221223616 134644260 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15502 603 41 0 16312 0
vsize: 65412
[startup+220.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16348 0 0 0 21955 48 0 0 25 0 1 0 422356115 66981888 15488 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15488 603 41 0 16312 0
vsize: 65412
[startup+230.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16348 0 0 0 22955 48 0 0 25 0 1 0 422356115 66981888 15488 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15488 603 41 0 16312 0
vsize: 65412
[startup+240.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16349 0 0 0 23955 48 0 0 25 0 1 0 422356115 66981888 15489 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15489 603 41 0 16312 0
vsize: 65412
[startup+250.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16349 0 0 0 24955 48 0 0 25 0 1 0 422356115 66981888 15489 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15489 603 41 0 16312 0
vsize: 65412
[startup+260.018 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16349 0 0 0 25956 48 0 0 25 0 1 0 422356115 66981888 15489 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15489 603 41 0 16312 0
vsize: 65412
[startup+270.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16349 0 0 0 26956 48 0 0 25 0 1 0 422356115 66981888 15489 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15489 603 41 0 16312 0
vsize: 65412
[startup+280.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16351 0 0 0 27956 48 0 0 25 0 1 0 422356115 66981888 15491 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15491 603 41 0 16312 0
vsize: 65412
[startup+290.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 28956 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+300.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 29956 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+310.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 30956 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+320.019 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 31957 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615681 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+330.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 32957 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+340.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 33957 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+350.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 34957 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+360.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 35958 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+370.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16352 0 0 0 36958 48 0 0 25 0 1 0 422356115 66981888 15492 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16353 15492 603 41 0 16312 0
vsize: 65412
[startup+380.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 16493 0 0 0 37958 48 0 0 25 0 1 0 422356115 67637248 15633 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16513 15633 603 41 0 16472 0
vsize: 66052
[startup+390.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 17133 0 0 0 38956 50 0 0 25 0 1 0 422356115 70299648 16273 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17163 16273 603 41 0 17122 0
vsize: 68652
[startup+400.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 17616 0 0 0 39955 51 0 0 25 0 1 0 422356115 72273920 16756 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17645 16756 603 41 0 17604 0
vsize: 70580
[startup+410.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 18115 0 0 0 40954 52 0 0 25 0 1 0 422356115 74276864 17255 4294967295 134512640 134672761 3221224560 3221223600 134613748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18134 17255 603 41 0 18093 0
vsize: 72536
[startup+420.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 18564 0 0 0 41953 54 0 0 25 0 1 0 422356115 76124160 17704 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18585 17704 603 41 0 18544 0
vsize: 74340
[startup+430.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 18927 0 0 0 42951 55 0 0 25 0 1 0 422356115 77701120 18067 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18970 18067 603 41 0 18929 0
vsize: 75880
[startup+440.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 19290 0 0 0 43951 56 0 0 25 0 1 0 422356115 79159296 18430 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19326 18430 603 41 0 19285 0
vsize: 77304
[startup+450.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 19611 0 0 0 44949 57 0 0 25 0 1 0 422356115 80470016 18751 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19646 18751 603 41 0 19605 0
vsize: 78584
[startup+460.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 20005 0 0 0 45948 59 0 0 25 0 1 0 422356115 82665472 19145 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20182 19145 603 41 0 20141 0
vsize: 80728
[startup+470.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 20398 0 0 0 46947 60 0 0 25 0 1 0 422356115 84164608 19538 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20548 19538 603 41 0 20507 0
vsize: 82192
[startup+480.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 20703 0 0 0 47946 61 0 0 25 0 1 0 422356115 85504000 19843 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20875 19843 603 41 0 20834 0
vsize: 83500
[startup+490.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21028 0 0 0 48945 62 0 0 25 0 1 0 422356115 86822912 20168 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21197 20168 603 41 0 21156 0
vsize: 84788
[startup+500.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21334 0 0 0 49944 63 0 0 25 0 1 0 422356115 88027136 20474 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21491 20474 603 41 0 21450 0
vsize: 85964
[startup+510.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21663 0 0 0 50944 64 0 0 25 0 1 0 422356115 88682496 20664 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20664 603 41 0 21610 0
vsize: 86604
[startup+520.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21663 0 0 0 51944 64 0 0 25 0 1 0 422356115 88682496 20664 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20664 603 41 0 21610 0
vsize: 86604
[startup+530.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21663 0 0 0 52944 64 0 0 25 0 1 0 422356115 88682496 20664 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20664 603 41 0 21610 0
vsize: 86604
[startup+540.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21663 0 0 0 53944 64 0 0 25 0 1 0 422356115 88682496 20664 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20664 603 41 0 21610 0
vsize: 86604
[startup+550.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21664 0 0 0 54944 64 0 0 25 0 1 0 422356115 88682496 20665 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20665 603 41 0 21610 0
vsize: 86604
[startup+560.021 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21665 0 0 0 55944 64 0 0 25 0 1 0 422356115 88682496 20666 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20666 603 41 0 21610 0
vsize: 86604
[startup+570.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21665 0 0 0 56944 64 0 0 25 0 1 0 422356115 88682496 20666 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20666 603 41 0 21610 0
vsize: 86604
[startup+580.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21665 0 0 0 57945 64 0 0 25 0 1 0 422356115 88682496 20666 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20666 603 41 0 21610 0
vsize: 86604
[startup+590.022 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21665 0 0 0 58945 64 0 0 25 0 1 0 422356115 88682496 20666 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20666 603 41 0 21610 0
vsize: 86604
[startup+600.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21666 0 0 0 59945 64 0 0 25 0 1 0 422356115 88682496 20667 4294967295 134512640 134672761 3221224560 3221223744 134615671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20667 603 41 0 21610 0
vsize: 86604
[startup+610.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21666 0 0 0 60945 64 0 0 25 0 1 0 422356115 88682496 20667 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20667 603 41 0 21610 0
vsize: 86604
[startup+620.023 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21668 0 0 0 61945 64 0 0 25 0 1 0 422356115 88682496 20669 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20669 603 41 0 21610 0
vsize: 86604
[startup+630.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21668 0 0 0 62946 64 0 0 25 0 1 0 422356115 88682496 20669 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20669 603 41 0 21610 0
vsize: 86604
[startup+640.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21669 0 0 0 63946 64 0 0 25 0 1 0 422356115 88682496 20670 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20670 603 41 0 21610 0
vsize: 86604
[startup+650.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21670 0 0 0 64946 64 0 0 25 0 1 0 422356115 88682496 20671 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20671 603 41 0 21610 0
vsize: 86604
[startup+660.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21671 0 0 0 65946 64 0 0 25 0 1 0 422356115 88682496 20672 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20672 603 41 0 21610 0
vsize: 86604
[startup+670.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21671 0 0 0 66946 64 0 0 25 0 1 0 422356115 88682496 20672 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20672 603 41 0 21610 0
vsize: 86604
[startup+680.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21672 0 0 0 67946 64 0 0 25 0 1 0 422356115 88682496 20673 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20673 603 41 0 21610 0
vsize: 86604
[startup+690.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21672 0 0 0 68947 64 0 0 25 0 1 0 422356115 88682496 20673 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20673 603 41 0 21610 0
vsize: 86604
[startup+700.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21672 0 0 0 69947 65 0 0 25 0 1 0 422356115 88682496 20673 4294967295 134512640 134672761 3221224560 3221223744 134615673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20673 603 41 0 21610 0
vsize: 86604
[startup+710.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21675 0 0 0 70947 65 0 0 25 0 1 0 422356115 88682496 20676 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20676 603 41 0 21610 0
vsize: 86604
[startup+720.024 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21675 0 0 0 71947 65 0 0 25 0 1 0 422356115 88682496 20676 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20676 603 41 0 21610 0
vsize: 86604
[startup+730.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21675 0 0 0 72947 65 0 0 25 0 1 0 422356115 88682496 20676 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20676 603 41 0 21610 0
vsize: 86604
[startup+740.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21675 0 0 0 73947 65 0 0 25 0 1 0 422356115 88682496 20676 4294967295 134512640 134672761 3221224560 3221223744 134616020 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20676 603 41 0 21610 0
vsize: 86604
[startup+750.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21676 0 0 0 74947 65 0 0 25 0 1 0 422356115 88682496 20677 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20677 603 41 0 21610 0
vsize: 86604
[startup+760.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21676 0 0 0 75948 65 0 0 25 0 1 0 422356115 88682496 20677 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20677 603 41 0 21610 0
vsize: 86604
[startup+770.025 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21676 0 0 0 76948 65 0 0 25 0 1 0 422356115 88682496 20677 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20677 603 41 0 21610 0
vsize: 86604
[startup+780.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21677 0 0 0 77948 65 0 0 25 0 1 0 422356115 88682496 20678 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20678 603 41 0 21610 0
vsize: 86604
[startup+790.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21677 0 0 0 78948 65 0 0 25 0 1 0 422356115 88682496 20678 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20678 603 41 0 21610 0
vsize: 86604
[startup+800.026 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21678 0 0 0 79948 65 0 0 25 0 1 0 422356115 88682496 20679 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20679 603 41 0 21610 0
vsize: 86604
[startup+810.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21678 0 0 0 80948 65 0 0 25 0 1 0 422356115 88682496 20679 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21651 20679 603 41 0 21610 0
vsize: 86604
[startup+820.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21678 0 0 0 81948 65 0 0 25 0 1 0 422356115 88682496 20679 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20679 603 41 0 21610 0
vsize: 86604
[startup+830.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21679 0 0 0 82948 65 0 0 25 0 1 0 422356115 88682496 20680 4294967295 134512640 134672761 3221224560 3221223744 134615705 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20680 603 41 0 21610 0
vsize: 86604
[startup+840.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21680 0 0 0 83948 65 0 0 25 0 1 0 422356115 88682496 20681 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20681 603 41 0 21610 0
vsize: 86604
[startup+850.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21680 0 0 0 84948 65 0 0 25 0 1 0 422356115 88682496 20681 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20681 603 41 0 21610 0
vsize: 86604
[startup+860.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21680 0 0 0 85948 65 0 0 25 0 1 0 422356115 88682496 20681 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21651 20681 603 41 0 21610 0
vsize: 86604
[startup+870.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21699 0 0 0 86948 65 0 0 25 0 1 0 422356115 88813568 20700 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21683 20700 603 41 0 21642 0
vsize: 86732
[startup+880.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 21931 0 0 0 87948 66 0 0 25 0 1 0 422356115 89776128 20932 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21918 20932 603 41 0 21877 0
vsize: 87672
[startup+890.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 22149 0 0 0 88947 66 0 0 25 0 1 0 422356115 90701824 21150 4294967295 134512640 134672761 3221224560 3221223744 134615937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22144 21150 603 41 0 22103 0
vsize: 88576
[startup+900.027 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 22371 0 0 0 89947 67 0 0 25 0 1 0 422356115 91631616 21372 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22371 21372 603 41 0 22330 0
vsize: 89484
[startup+910.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 22626 0 0 0 90946 68 0 0 25 0 1 0 422356115 92712960 21627 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22635 21627 603 41 0 22594 0
vsize: 90540
[startup+920.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 22839 0 0 0 91946 69 0 0 25 0 1 0 422356115 93564928 21840 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22843 21840 603 41 0 22802 0
vsize: 91372
[startup+930.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23071 0 0 0 92945 69 0 0 25 0 1 0 422356115 94629888 22072 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23103 22072 603 41 0 23062 0
vsize: 92412
[startup+940.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23297 0 0 0 93945 70 0 0 25 0 1 0 422356115 95424512 22298 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23297 22298 603 41 0 23256 0
vsize: 93188
[startup+950.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23677 0 0 0 94944 71 0 0 25 0 1 0 422356115 97366016 22678 4294967295 134512640 134672761 3221224560 3221223616 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23771 22678 603 41 0 23730 0
vsize: 95084
[startup+960.028 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23677 0 0 0 95944 71 0 0 25 0 1 0 422356115 97366016 22678 4294967295 134512640 134672761 3221224560 3221223616 134644266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23771 22678 603 41 0 23730 0
vsize: 95084
[startup+970.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23692 0 0 0 96944 71 0 0 25 0 1 0 422356115 96841728 22540 4294967295 134512640 134672761 3221224560 3221223744 134615594 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22540 603 41 0 23602 0
vsize: 94572
[startup+980.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23692 0 0 0 97944 71 0 0 25 0 1 0 422356115 96841728 22540 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22540 603 41 0 23602 0
vsize: 94572
[startup+990.029 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23692 0 0 0 98944 71 0 0 25 0 1 0 422356115 96841728 22540 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22540 603 41 0 23602 0
vsize: 94572
[startup+1000.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23692 0 0 0 99945 71 0 0 25 0 1 0 422356115 96841728 22540 4294967295 134512640 134672761 3221224560 3221223744 134615622 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22540 603 41 0 23602 0
vsize: 94572
[startup+1010.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23692 0 0 0 100945 71 0 0 25 0 1 0 422356115 96841728 22540 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22540 603 41 0 23602 0
vsize: 94572
[startup+1020.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23692 0 0 0 101945 71 0 0 25 0 1 0 422356115 96841728 22540 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22540 603 41 0 23602 0
vsize: 94572
[startup+1030.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23692 0 0 0 102945 71 0 0 25 0 1 0 422356115 96841728 22540 4294967295 134512640 134672761 3221224560 3221223600 134614266 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22540 603 41 0 23602 0
vsize: 94572
[startup+1040.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23693 0 0 0 103945 71 0 0 25 0 1 0 422356115 96841728 22541 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22541 603 41 0 23602 0
vsize: 94572
[startup+1050.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 104946 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1060.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 105946 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1070.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 106946 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1080.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 107946 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1090.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 108946 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223600 134612628 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1100.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 109946 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1110.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 110947 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1120.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 111947 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1130.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 112947 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223600 134612739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1140.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 113947 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1150.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 114947 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1160.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 115947 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1170.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 116948 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1180.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 117948 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1190.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 118948 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
[startup+1200.03 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 18470
Raw data (stat): 18470 (minisat+) R 18469 10720 10719 0 -1 0 23694 0 0 0 119948 71 0 0 25 0 1 0 422356115 96841728 22542 4294967295 134512640 134672761 3221224560 3221223484 1075346600 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23643 22542 603 41 0 23602 0
vsize: 94572
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 18470
Raw data (stat): 18470 (minisat+) Z 18469 10720 10719 0 -1 12 23694 0 0 0 119948 75 0 0 25 0 1 0 422356115 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.08
CPU time (s): 1200.25
CPU user time (s): 1199.49
CPU system time (s): 0.758884
CPU usage (%): 100.014
Max. virtual memory (Kb): 95084
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####