PB'05 competition: run trace

Some explanations

A solver is run under the control of another program named runsolver. runsolver is in charge of imposing the CPU time limit and the memory limit to the solver. It also monitors some information about the process. The trace of the execution of a solver is divided in four parts:
LAUNCHER DATA
These informations are related to the script which will launch the solver. The most important informations are the command line given to the solver, the md5sum of the different files and the dump of the /proc/cpuinfo and /proc/meminfo which provide some useful information on the computer.
SOLVER DATA
This is the output of the solver (stdout and stderr).
WATCHER DATA
This is the informations gathered by the runsolver program. It first prints the different limits. There's a first limit on CPU time set to 1200 seconds. After this time has ellapsed, runsolver sends a SIGTERM and 2 seconds later a SIGKILL to the solver. For safety, there's also another limit set to 1230 seconds which will send a SIGXPU to the solver. The last limit is on the virtual memory used by the process (900Mb).
Every ten seconds, the runsolver process fetches the content of /proc/loadavg, /proc/pid/stat and /proc/pid/statm (see man proc) and prints it as raw data. This is only recorded in case we need to investigate the behaviour of a solver. The memory used by the solver (vsize) is also given every ten seconds.
When the solver exits, runsolver prints some informations such as status and time. CPU usage is the ratio CPU Time/Real Time.
VERIFIER DATA
The output of the solver is piped to a verifier program which will search a value line "v " and, if found, will check that the given interpretation satisfies all constraints.
General information on the benchmark

Name	normalized-opb/web/www.ps.uni-sb.de/~walser/benchmarks/ppp-problems/normalized-ppp:1-13.opb
MD5SUM	4caec1e880871fcef3276cf001aca352
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	7.63384
Number of variables	4632
Total number of constraints	35596
Number of constraints which are clauses	29940
Number of constraints which are cardinality constraints (but not clauses)	5578
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 6459

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc15 THE 2005-04-14 05:04:17 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4875 boxname=wulflinc15 idbench=363 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  4caec1e880871fcef3276cf001aca352  /oldhome/oroussel/tmp/wulflinc15/normalized-ppp:1-13.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc15/normalized-ppp:1-13.opb /oldhome/oroussel/tmp/wulflinc15/normalized-ppp:1-13.opb
IDLAUNCH: 4875
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 450.999
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		: 450.999
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:        890140 kB
Buffers:         36768 kB
Cached:          85732 kB
SwapCached:       2144 kB
Active:          66892 kB
Inactive:        60604 kB
HighTotal:      131008 kB
HighFree:        41384 kB
LowTotal:       903652 kB
LowFree:        848756 kB
SwapTotal:     2097136 kB
SwapFree:      2094992 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            11404 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:24:19 (client local time) WITH STATUS 0 IN 1200.16 SECONDS
stats: 4875 7 1200.16 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 31138 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ....................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[31137]---> BDD-cost:   56
c ---[31136]---> BDD-cost:   56
c ---[31135]---> BDD-cost:   56
c ---[31134]---> BDD-cost:   56
c ---[31133]---> BDD-cost:   56
c ---[31132]---> BDD-cost:   56
c ---[31131]---> BDD-cost:  100
c ---[31130]---> BDD-cost:  100
c ---[31129]---> BDD-cost:  100
c ---[31128]---> BDD-cost:  100
c ---[31127]---> BDD-cost:  100
c ---[31126]---> BDD-cost:  100
c ---[31125]---> BDD-cost:  122
c ---[31124]---> BDD-cost:  122
c ---[31123]---> BDD-cost:  122
c ---[31122]---> BDD-cost:  122
c ---[31121]---> BDD-cost:  122
c ---[31120]---> BDD-cost:  122
c ---[31119]---> BDD-cost:  122
c ---[31118]---> BDD-cost:  122
c ---[31117]---> BDD-cost:  122
c ---[31116]---> BDD-cost:  122
c ---[31115]---> BDD-cost:  122
c ---[31114]---> BDD-cost:  122
c ---[31113]---> BDD-cost:  122
c ---[31112]---> BDD-cost:  122
c ---[31111]---> BDD-cost:  122
c ---[31110]---> BDD-cost:  122
c ---[31109]---> BDD-cost:  122
c ---[31108]---> BDD-cost:  122
c ---[31107]---> BDD-cost:  132
c ---[31106]---> BDD-cost:  132
c ---[31105]---> BDD-cost:  132
c ---[31104]---> BDD-cost:  132
c ---[31103]---> BDD-cost:  132
c ---[31102]---> BDD-cost:  132
c ---[31101]---> BDD-cost:  122
c ---[31100]---> BDD-cost:  122
c ---[31099]---> BDD-cost:  122
c ---[31098]---> BDD-cost:  122
c ---[31097]---> BDD-cost:  122
c ---[31096]---> BDD-cost:  122
c ---[31095]---> BDD-cost:  122
c ---[31094]---> BDD-cost:  122
c ---[31093]---> BDD-cost:  122
c ---[31092]---> BDD-cost:  122
c ---[31091]---> BDD-cost:  122
c ---[31090]---> BDD-cost:  122
c ---[31089]---> BDD-cost:  122
c ---[31088]---> BDD-cost:  122
c ---[31087]---> BDD-cost:  122
c ---[31086]---> BDD-cost:  122
c ---[31085]---> BDD-cost:  122
c ---[31084]---> BDD-cost:  122
c ---[31083]---> Sorter-cost:  524     Base: 2 2
c ---[31082]---> Sorter-cost:  524     Base: 2 2
c ---[31081]---> Sorter-cost:  524     Base: 2 2
c ---[31080]---> Sorter-cost:  524     Base: 2 2
c ---[31079]---> Sorter-cost:  524     Base: 2 2
c ---[31078]---> Sorter-cost:  524     Base: 2 2
c ---[31077]---> Sorter-cost:  524     Base: 2 2
c ---[31076]---> Sorter-cost:  524     Base: 2 2
c ---[31075]---> Sorter-cost:  524     Base: 2 2
c ---[31074]---> Sorter-cost:  524     Base: 2 2
c ---[31073]---> Sorter-cost:  524     Base: 2 2
c ---[31072]---> Sorter-cost:  524     Base: 2 2
c ---[31071]---> BDD-cost:   85
c ---[31070]---> BDD-cost:   85
c ---[31069]---> BDD-cost:   85
c ---[31068]---> BDD-cost:   85
c ---[31067]---> BDD-cost:   85
c ---[31066]---> BDD-cost:   85
c ---[31065]---> BDD-cost:   56
c ---[31064]---> BDD-cost:   56
c ---[31063]---> BDD-cost:   56
c ---[31062]---> BDD-cost:   56
c ---[31061]---> BDD-cost:   56
c ---[31060]---> BDD-cost:   56
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:   23
c ---[31046]---> BDD-cost:   23
c ---[31044]---> BDD-cost:   23
c ---[31042]---> BDD-cost:   23
c ---[31040]---> BDD-cost:   23
c ---[31038]---> BDD-cost:   23
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:   19
c ---[31020]---> BDD-cost:   19
c ---[31018]---> BDD-cost:   19
c ---[31016]---> BDD-cost:   19
c ---[31014]---> BDD-cost:   19
c ---[31012]---> BDD-cost:   19
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 ---[31000]---> BDD-cost:   23
c ---[30998]---> BDD-cost:   23
c ---[30996]---> BDD-cost:   23
c ---[30994]---> BDD-cost:   23
c ---[30992]---> BDD-cost:   23
c ---[30990]---> BDD-cost:   23
c ---[30988]---> BDD-cost:   23
c ---[30986]---> BDD-cost:   19
c ---[30984]---> BDD-cost:   19
c ---[30982]---> BDD-cost:   19
c ---[30980]---> BDD-cost:   19
c ---[30978]---> BDD-cost:   19
c ---[30976]---> BDD-cost:   19
c ---[30974]---> BDD-cost:   17
c ---[30972]---> BDD-cost:   17
c ---[30970]---> BDD-cost:   17
c ---[30968]---> BDD-cost:   17
c ---[30966]---> BDD-cost:   17
c ---[30964]---> BDD-cost:   17
c ---[30962]---> BDD-cost:   23
c ---[30960]---> BDD-cost:   23
c ---[30958]---> BDD-cost:   23
c ---[30956]---> BDD-cost:   23
c ---[30954]---> BDD-cost:   23
c ---[30952]---> BDD-cost:   23
c ---[30950]---> BDD-cost:   23
c ---[30948]---> BDD-cost:   23
c ---[30946]---> BDD-cost:   23
c ---[30944]---> BDD-cost:   23
c ---[30942]---> BDD-cost:   23
c ---[30940]---> BDD-cost:   23
c ---[30938]---> BDD-cost:   23
c ---[30936]---> BDD-cost:   23
c ---[30934]---> BDD-cost:   23
c ---[30932]---> BDD-cost:   23
c ---[30930]---> BDD-cost:   23
c ---[30928]---> BDD-cost:   23
c ---[30926]---> BDD-cost:   19
c ---[30924]---> BDD-cost:   19
c ---[30922]---> BDD-cost:   19
c ---[30920]---> BDD-cost:   19
c ---[30918]---> BDD-cost:   19
c ---[30916]---> BDD-cost:   19
c ---[30914]---> BDD-cost:   23
c ---[30912]---> BDD-cost:   23
c ---[30910]---> BDD-cost:   23
c ---[30908]---> BDD-cost:   23
c ---[30906]---> BDD-cost:   23
c ---[30904]---> BDD-cost:   23
c ---[30902]---> BDD-cost:   23
c ---[30900]---> BDD-cost:   23
c ---[30898]---> BDD-cost:   23
c ---[30896]---> BDD-cost:   23
c ---[30894]---> BDD-cost:   23
c ---[30892]---> BDD-cost:   23
c ---[30890]---> BDD-cost:   23
c ---[30888]---> BDD-cost:   23
c ---[30886]---> BDD-cost:   23
c ---[30884]---> BDD-cost:   23
c ---[30882]---> BDD-cost:   23
c ---[30880]---> BDD-cost:   23
c ---[30878]---> BDD-cost:   23
c ---[30876]---> BDD-cost:   23
c ---[30874]---> BDD-cost:   23
c ---[30872]---> BDD-cost:   23
c ---[30870]---> BDD-cost:   23
c ---[30868]---> BDD-cost:   23
c ---[30866]---> BDD-cost:   23
c ---[30864]---> BDD-cost:   23
c ---[30862]---> BDD-cost:   23
c ---[30860]---> BDD-cost:   23
c ---[30858]---> BDD-cost:   23
c ---[30856]---> BDD-cost:   23
c ---[30854]---> BDD-cost:   23
c ---[30852]---> BDD-cost:   23
c ---[30850]---> BDD-cost:   23
c ---[30848]---> BDD-cost:   23
c ---[30846]---> BDD-cost:   23
c ---[30844]---> BDD-cost:   23
c ---[30842]---> BDD-cost:   23
c ---[30840]---> BDD-cost:   23
c ---[30838]---> BDD-cost:   23
c ---[30836]---> BDD-cost:   23
c ---[30834]---> BDD-cost:   23
c ---[30832]---> BDD-cost:   23
c ---[30830]---> BDD-cost:   23
c ---[30828]---> BDD-cost:   23
c ---[30826]---> BDD-cost:   23
c ---[30824]---> BDD-cost:   23
c ---[30822]---> BDD-cost:   23
c ---[30820]---> BDD-cost:   23
c ---[30818]---> BDD-cost:   23
c ---[30816]---> BDD-cost:   23
c ---[30814]---> BDD-cost:   23
c ---[30812]---> BDD-cost:   23
c ---[30810]---> BDD-cost:   23
c ---[30808]---> BDD-cost:   23
c ---[30806]---> BDD-cost:   23
c ---[30804]---> BDD-cost:   23
c ---[30802]---> BDD-cost:   23
c ---[30800]---> BDD-cost:   23
c ---[30798]---> BDD-cost:   23
c ---[30796]---> BDD-cost:   23
c ---[30794]---> BDD-cost:   23
c ---[30792]---> BDD-cost:   23
c ---[30790]---> BDD-cost:   23
c ---[30788]---> BDD-cost:   23
c ---[30786]---> BDD-cost:   23
c ---[30784]---> BDD-cost:   23
c ---[30782]---> BDD-cost:   23
c ---[30780]---> BDD-cost:   23
c ---[30778]---> BDD-cost:   23
c ---[30776]---> BDD-cost:   23
c ---[30774]---> BDD-cost:   23
c ---[30772]---> BDD-cost:   23
c ---[30770]---> BDD-cost:   23
c ---[30768]---> BDD-cost:   23
c ---[30766]---> BDD-cost:   23
c ---[30764]---> BDD-cost:   23
c ---[30762]---> BDD-cost:   23
c ---[30760]---> BDD-cost:   23
c ---[30758]---> BDD-cost:   23
c ---[30756]---> BDD-cost:   23
c ---[30754]---> BDD-cost:   23
c ---[30752]---> BDD-cost:   23
c ---[30750]---> BDD-cost:   23
c ---[30748]---> BDD-cost:   23
c ---[30746]---> BDD-cost:   23
c ---[30744]---> BDD-cost:   23
c ---[30742]---> BDD-cost:   23
c ---[30740]---> BDD-cost:   23
c ---[30738]---> BDD-cost:   23
c ---[30736]---> BDD-cost:   23
c ---[30734]---> BDD-cost:   23
c ---[30732]---> BDD-cost:   23
c ---[30730]---> BDD-cost:   23
c ---[30728]---> BDD-cost:   23
c ---[30726]---> BDD-cost:   23
c ---[30724]---> BDD-cost:   23
c ---[30722]---> BDD-cost:   19
c ---[30720]---> BDD-cost:   19
c ---[30718]---> BDD-cost:   19
c ---[30716]---> BDD-cost:   19
c ---[30714]---> BDD-cost:   19
c ---[30712]---> BDD-cost:   19
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 ---[30633]---> BDD-cost:    9
c ---[30632]---> BDD-cost:    9
c ---[30631]---> BDD-cost:    9
c ---[30630]---> BDD-cost:    9
c ---[30629]---> BDD-cost:    9
c ---[30628]---> BDD-cost:    9
c ---[30627]---> BDD-cost:    9
c ---[30626]---> BDD-cost:    9
c ---[30625]---> BDD-cost:    9
c ---[30624]---> BDD-cost:    9
c ---[30623]---> BDD-cost:    9
c ---[30622]---> BDD-cost:    9
c ---[30621]---> BDD-cost:    9
c ---[30620]---> BDD-cost:    9
c ---[30619]---> BDD-cost:    9
c ---[30618]---> BDD-cost:    9
c ---[30617]---> BDD-cost:    9
c ---[30616]---> BDD-cost:    9
c ---[30615]---> BDD-cost:    9
c ---[30614]---> BDD-cost:    9
c ---[30613]---> BDD-cost:    9
c ---[30612]---> BDD-cost:    9
c ---[30611]---> BDD-cost:    9
c ---[30610]---> BDD-cost:    9
c ---[30609]---> BDD-cost:    9
c ---[30608]---> BDD-cost:    9
c ---[30607]---> BDD-cost:    9
c ---[30606]---> BDD-cost:    9
c ---[30605]---> BDD-cost:    9
c ---[30604]---> BDD-cost:    9
c ---[30603]---> BDD-cost:    9
c ---[30602]---> BDD-cost:    9
c ---[30601]---> BDD-cost:    9
c ---[30600]---> BDD-cost:    9
c ---[30599]---> BDD-cost:    9
c ---[30598]---> BDD-cost:    9
c ---[30597]---> BDD-cost:    9
c ---[30596]---> BDD-cost:    9
c ---[30595]---> BDD-cost:    9
c ---[30594]---> BDD-cost:    9
c ---[30593]---> BDD-cost:    9
c ---[30592]---> BDD-cost:    9
c ---[30591]---> BDD-cost:    9
c ---[30590]---> BDD-cost:    9
c ---[30589]---> BDD-cost:    9
c ---[30588]---> BDD-cost:    9
c ---[30587]---> BDD-cost:    9
c ---[30586]---> BDD-cost:    9
c ---[30585]---> BDD-cost:    9
c ---[30584]---> BDD-cost:    9
c ---[30583]---> BDD-cost:    9
c ---[30582]---> BDD-cost:    9
c ---[30581]---> BDD-cost:    9
c ---[30580]---> BDD-cost:    9
c ---[30579]---> BDD-cost:    9
c ---[30578]---> BDD-cost:    9
c ---[30577]---> BDD-cost:    9
c ---[30576]---> BDD-cost:    9
c ---[30575]---> BDD-cost:    9
c ---[30574]---> BDD-cost:    9
c ---[30573]---> BDD-cost:    9
c ---[30572]---> BDD-cost:    9
c ---[30571]---> BDD-cost:    9
c ---[30570]---> BDD-cost:    9
c ---[30569]---> BDD-cost:    9
c ---[30568]---> BDD-cost:    9
c ---[30567]---> BDD-cost:    9
c ---[30566]---> BDD-cost:    9
c ---[30565]---> BDD-cost:    9
c ---[30564]---> BDD-cost:    9
c ---[30563]---> BDD-cost:    9
c ---[30562]---> BDD-cost:    9
c ---[30561]---> BDD-cost:    9
c ---[30560]---> BDD-cost:    9
c ---[30559]---> BDD-cost:    9
c ---[30558]---> BDD-cost:    9
c ---[30557]---> BDD-cost:    9
c ---[30556]---> BDD-cost:    9
c ---[30555]---> BDD-cost:    9
c ---[30554]---> BDD-cost:    9
c ---[30553]---> BDD-cost:    9
c ---[30552]---> BDD-cost:    9
c ---[30551]---> BDD-cost:    9
c ---[30550]---> BDD-cost:    9
c ---[30549]---> BDD-cost:    9
c ---[30548]---> BDD-cost:    9
c ---[30547]---> BDD-cost:    9
c ---[30546]---> BDD-cost:    9
c ---[30545]---> BDD-cost:    9
c ---[30544]---> BDD-cost:    9
c ---[30543]---> BDD-cost:    9
c ---[30542]---> BDD-cost:    9
c ---[30541]---> BDD-cost:    9
c ---[30540]---> BDD-cost:    9
c ---[30539]---> BDD-cost:    9
c ---[30538]---> BDD-cost:    9
c ---[30537]---> BDD-cost:    9
c ---[30536]---> BDD-cost:    9
c ---[30535]---> BDD-cost:    9
c ---[30534]---> BDD-cost:    9
c ---[30533]---> BDD-cost:    9
c ---[30532]---> BDD-cost:    9
c ---[30531]---> BDD-cost:    9
c ---[30530]---> BDD-cost:    9
c ---[30529]---> BDD-cost:    9
c ---[30528]---> BDD-cost:    9
c ---[30527]---> BDD-cost:    9
c ---[30526]---> BDD-cost:    9
c ---[30525]---> BDD-cost:    9
c ---[30524]---> BDD-cost:    9
c ---[30523]---> BDD-cost:    9
c ---[30522]---> BDD-cost:    9
c ---[30521]---> BDD-cost:    9
c ---[30520]---> BDD-cost:    9
c ---[30519]---> BDD-cost:    9
c ---[30518]---> BDD-cost:    9
c ---[30517]---> BDD-cost:    9
c ---[30516]---> BDD-cost:    9
c ---[30515]---> BDD-cost:    9
c ---[30514]---> BDD-cost:    9
c ---[30513]---> BDD-cost:    9
c ---[30512]---> BDD-cost:    9
c ---[30511]---> BDD-cost:    9
c ---[30510]---> BDD-cost:    9
c ---[30509]---> BDD-cost:    9
c ---[30508]---> BDD-cost:    9
c ---[30507]---> BDD-cost:    9
c ---[30506]---> BDD-cost:    9
c ---[30505]---> BDD-cost:    9
c ---[30504]---> BDD-cost:    9
c ---[30503]---> BDD-cost:    9
c ---[30502]---> BDD-cost:    9
c ---[30501]---> BDD-cost:    9
c ---[30500]---> BDD-cost:    9
c ---[30499]---> BDD-cost:    9
c ---[30498]---> BDD-cost:    9
c ---[30497]---> BDD-cost:    9
c ---[30496]---> BDD-cost:    9
c ---[30495]---> BDD-cost:    9
c ---[30494]---> BDD-cost:    9
c ---[30493]---> BDD-cost:    9
c ---[30492]---> BDD-cost:    9
c ---[30491]---> BDD-cost:    9
c ---[30490]---> BDD-cost:    9
c ---[30489]---> BDD-cost:    9
c ---[30488]---> BDD-cost:    9
c ---[30487]---> BDD-cost:    9
c ---[30486]---> BDD-cost:    9
c ---[30485]---> BDD-cost:    9
c ---[30484]---> BDD-cost:    9
c ---[30483]---> BDD-cost:    9
c ---[30482]---> BDD-cost:    9
c ---[30481]---> BDD-cost:    9
c ---[30480]---> BDD-cost:    9
c ---[30479]---> BDD-cost:    9
c ---[30478]---> BDD-cost:    9
c ---[30477]---> BDD-cost:    9
c ---[30476]---> BDD-cost:    9
c ---[30475]---> BDD-cost:    9
c ---[30474]---> BDD-cost:    9
c ---[30473]---> BDD-cost:    9
c ---[30472]---> BDD-cost:    9
c ---[30471]---> BDD-cost:    9
c ---[30470]---> BDD-cost:    9
c ---[30469]---> BDD-cost:    9
c ---[30468]---> BDD-cost:    9
c ---[30467]---> BDD-cost:    9
c ---[30466]---> BDD-cost:    9
c ---[30465]---> BDD-cost:    9
c ---[30464]---> BDD-cost:    9
c ---[30463]---> BDD-cost:    9
c ---[30462]---> BDD-cost:    9
c ---[30461]---> BDD-cost:    9
c ---[30460]---> BDD-cost:    9
c ---[30459]---> BDD-cost:    9
c ---[30458]---> BDD-cost:    9
c ---[30457]---> BDD-cost:    9
c ---[30456]---> BDD-cost:    9
c ---[30455]---> BDD-cost:    9
c ---[30454]---> BDD-cost:    9
c ---[30453]---> BDD-cost:    9
c ---[30452]---> BDD-cost:    9
c ---[30451]---> BDD-cost:    9
c ---[30450]---> BDD-cost:    9
c ---[30449]---> BDD-cost:    9
c ---[30448]---> BDD-cost:    9
c ---[30447]---> BDD-cost:    9
c ---[30446]---> BDD-cost:    9
c ---[30445]---> BDD-cost:    9
c ---[30444]---> BDD-cost:    9
c ---[30443]---> BDD-cost:    9
c ---[30442]---> BDD-cost:    9
c ---[30441]---> BDD-cost:    9
c ---[30440]---> BDD-cost:    9
c ---[30439]---> BDD-cost:    9
c ---[30438]---> BDD-cost:    9
c ---[30437]---> BDD-cost:    9
c ---[30436]---> BDD-cost:    9
c ---[30435]---> BDD-cost:    9
c ---[30434]---> BDD-cost:    9
c ---[30433]---> BDD-cost:    9
c ---[30432]---> BDD-cost:    9
c ---[30431]---> BDD-cost:    9
c ---[30430]---> BDD-cost:    9
c ---[30429]---> BDD-cost:    9
c ---[30428]---> BDD-cost:    9
c ---[30427]---> BDD-cost:    9
c ---[30426]---> BDD-cost:    9
c ---[30425]---> BDD-cost:    9
c ---[30424]---> BDD-cost:    9
c ---[30423]---> BDD-cost:    9
c ---[30422]---> BDD-cost:    9
c ---[30421]---> BDD-cost:    9
c ---[30420]---> BDD-cost:    9
c ---[30419]---> BDD-cost:    9
c ---[30418]---> BDD-cost:    9
c ---[30417]---> BDD-cost:    9
c ---[30416]---> BDD-cost:    9
c ---[30415]---> BDD-cost:    9
c ---[30414]---> BDD-cost:    9
c ---[30413]---> BDD-cost:    9
c ---[30412]---> BDD-cost:    9
c ---[30411]---> BDD-cost:    9
c ---[30410]---> BDD-cost:    9
c ---[30409]---> BDD-cost:    9
c ---[30408]---> BDD-cost:    9
c ---[30407]---> BDD-cost:    9
c ---[30406]---> BDD-cost:    9
c ---[30405]---> BDD-cost:    9
c ---[30404]---> BDD-cost:    9
c ---[30403]---> BDD-cost:    9
c ---[30402]---> BDD-cost:    9
c ---[30401]---> BDD-cost:    9
c ---[30400]---> BDD-cost:    9
c ---[30399]---> BDD-cost:    9
c ---[30398]---> BDD-cost:    9
c ---[30397]---> BDD-cost:    9
c ---[30396]---> BDD-cost:    9
c ---[30395]---> BDD-cost:    9
c ---[30394]---> BDD-cost:    9
c ---[30393]---> BDD-cost:    9
c ---[30392]---> BDD-cost:    9
c ---[30391]---> BDD-cost:    9
c ---[30390]---> BDD-cost:    9
c ---[30389]---> BDD-cost:    9
c ---[30388]---> BDD-cost:    9
c ---[30387]---> BDD-cost:    9
c ---[30386]---> BDD-cost:    9
c ---[30385]---> BDD-cost:    9
c ---[30384]---> BDD-cost:    9
c ---[30383]---> BDD-cost:    9
c ---[30382]---> BDD-cost:    9
c ---[30381]---> BDD-cost:    9
c ---[30380]---> BDD-cost:    9
c ---[30379]---> BDD-cost:    9
c ---[30378]---> BDD-cost:    9
c ---[30377]---> BDD-cost:    9
c ---[30376]---> BDD-cost:    9
c ---[30375]---> BDD-cost:    9
c ---[30374]---> BDD-cost:    9
c ---[30373]---> BDD-cost:    9
c ---[30372]---> BDD-cost:    9
c ---[30371]---> BDD-cost:    9
c ---[30370]---> BDD-cost:    9
c ---[30369]---> BDD-cost:    9
c ---[30368]---> BDD-cost:    9
c ---[30367]---> BDD-cost:    9
c ---[30366]---> BDD-cost:    9
c ---[30365]---> BDD-cost:    9
c ---[30364]---> BDD-cost:    9
c ---[30363]---> BDD-cost:    9
c ---[30362]---> BDD-cost:    9
c ---[30361]---> BDD-cost:    9
c ---[30360]---> BDD-cost:    9
c ---[30359]---> BDD-cost:    9
c ---[30358]---> BDD-cost:    9
c ---[30357]---> BDD-cost:    9
c ---[30356]---> BDD-cost:    9
c ---[30355]---> BDD-cost:    9
c ---[30354]---> BDD-cost:    9
c ---[30353]---> BDD-cost:    9
c ---[30352]---> BDD-cost:    9
c ---[30351]---> BDD-cost:    9
c ---[30350]---> BDD-cost:    9
c ---[30349]---> BDD-cost:    9
c ---[30348]---> BDD-cost:    9
c ---[30347]---> BDD-cost:    9
c ---[30346]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:    9
c ---[ 402]---> BDD-cost:    9
c ---[ 401]---> BDD-cost:    9
c ---[ 400]---> BDD-cost:    9
c ---[ 399]---> BDD-cost:    9
c ---[ 398]---> BDD-cost:    9
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    9
c ---[ 395]---> BDD-cost:    9
c ---[ 394]---> BDD-cost:    9
c ---[ 393]---> BDD-cost:    9
c ---[ 392]---> BDD-cost:    9
c ---[ 391]---> BDD-cost:    9
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:    9
c ---[ 386]---> BDD-cost:    9
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    9
c ---[ 383]---> BDD-cost:    9
c ---[ 382]---> BDD-cost:    9
c ---[ 381]---> BDD-cost:    9
c ---[ 380]---> BDD-cost:    9
c ---[ 379]---> BDD-cost:    9
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    9
c ---[ 375]---> BDD-cost:    9
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 372]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:    9
c ---[ 369]---> BDD-cost:    9
c ---[ 368]---> BDD-cost:    9
c ---[ 367]---> BDD-cost:    9
c ---[ 366]---> BDD-cost:    9
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:    9
c ---[ 362]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    9
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:    9
c ---[ 354]---> BDD-cost:    9
c ---[ 353]---> BDD-cost:    9
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    9
c ---[ 350]---> BDD-cost:    9
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:    9
c ---[ 347]---> BDD-cost:    9
c ---[ 346]---> BDD-cost:    9
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    9
c ---[ 343]---> BDD-cost:    9
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:    9
c ---[ 338]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    9
c ---[ 336]---> BDD-cost:    9
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:    9
c ---[ 332]---> BDD-cost:    9
c ---[ 331]---> BDD-cost:    9
c ---[ 330]---> BDD-cost:    9
c ---[ 329]---> BDD-cost:    9
c ---[ 328]---> BDD-cost:    9
c ---[ 327]---> BDD-cost:    9
c ---[ 326]---> BDD-cost:    9
c ---[ 325]---> BDD-cost:    9
c ---[ 324]---> BDD-cost:    9
c ---[ 323]---> BDD-cost:    9
c ---[ 322]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    9
c ---[ 320]---> BDD-cost:    9
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    9
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    9
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    9
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:    9
c ---[ 306]---> BDD-cost:    9
c ---[ 305]---> BDD-cost:    9
c ---[ 304]---> BDD-cost:    9
c ---[ 303]---> BDD-cost:    9
c ---[ 302]---> BDD-cost:    9
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    9
c ---[ 297]---> BDD-cost:    9
c ---[ 296]---> BDD-cost:    9
c ---[ 295]---> BDD-cost:    9
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:    9
c ---[ 290]---> BDD-cost:    9
c ---[ 289]---> BDD-cost:    9
c ---[ 288]---> BDD-cost:    9
c ---[ 287]---> BDD-cost:    9
c ---[ 286]---> BDD-cost:    9
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    9
c ---[ 281]---> BDD-cost:    9
c ---[ 280]---> BDD-cost:    9
c ---[ 279]---> BDD-cost:    9
c ---[ 278]---> BDD-cost:    9
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    9
c ---[ 273]---> BDD-cost:    9
c ---[ 272]---> BDD-cost:    9
c ---[ 271]---> BDD-cost:    9
c ---[ 270]---> BDD-cost:    9
c ---[ 269]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:    9
c ---[ 267]---> BDD-cost:    9
c ---[ 266]---> BDD-cost:    9
c ---[ 265]---> BDD-cost:    9
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    9
c ---[ 257]---> BDD-cost:    9
c ---[ 256]---> BDD-cost:    9
c ---[ 255]---> BDD-cost:    9
c ---[ 254]---> BDD-cost:    9
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:    9
c ---[ 249]---> BDD-cost:    9
c ---[ 248]---> BDD-cost:    9
c ---[ 247]---> BDD-cost:    9
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:    9
c ---[ 241]---> BDD-cost:    9
c ---[ 240]---> BDD-cost:    9
c ---[ 239]---> BDD-cost:    9
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:    9
c ---[ 236]---> BDD-cost:    9
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:    9
c ---[ 233]---> BDD-cost:    9
c ---[ 232]---> BDD-cost:    9
c ---[ 231]---> BDD-cost:    9
c ---[ 230]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:    9
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:    9
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:    9
c ---[ 222]---> BDD-cost:    9
c ---[ 221]---> BDD-cost:    9
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:    9
c ---[ 218]---> BDD-cost:    9
c ---[ 217]---> BDD-cost:    9
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:    9
c ---[ 209]---> BDD-cost:    9
c ---[ 208]---> BDD-cost:    9
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:    9
c ---[ 204]---> BDD-cost:    9
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:    9
c ---[ 201]---> BDD-cost:    9
c ---[ 200]---> BDD-cost:    9
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:    9
c ---[ 194]---> BDD-cost:    9
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:    9
c ---[ 191]---> BDD-cost:    9
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:    9
c ---[ 188]---> BDD-cost:    9
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:    9
c ---[ 185]---> BDD-cost:    9
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:    9
c ---[ 182]---> BDD-cost:    9
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:    9
c ---[ 178]---> BDD-cost:    9
c ---[ 177]---> BDD-cost:    9
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:    9
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:    9
c ---[ 170]---> BDD-cost:    9
c ---[ 169]---> BDD-cost:    9
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    9
c ---[ 159]---> BDD-cost:    9
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    9
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:    9
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:    9
c ---[ 146]---> BDD-cost:    9
c ---[ 145]---> BDD-cost:    9
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:    9
c ---[ 142]---> BDD-cost:    9
c ---[ 141]---> BDD-cost:    9
c ---[ 140]---> BDD-cost:    9
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    9
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    9
c ---[ 134]---> BDD-cost:    9
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:    9
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    9
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:    9
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:    9
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:    9
c ---[ 108]---> BDD-cost:    9
c ---[ 107]---> BDD-cost:    9
c ---[ 106]---> BDD-cost:    9
c ---[ 105]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:    9
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    9
c ---[  98]---> BDD-cost:    9
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    9
c ---[  93]---> BDD-cost:    9
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:    9
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:    9
c ---[  87]---> BDD-cost:    9
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:    9
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:    9
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:    9
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    9
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:    9
c ---[  64]---> BDD-cost:    9
c ---[  63]---> BDD-cost:    9
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:    9
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:    9
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    9
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:    9
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:    9
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:    9
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:    9
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:    9
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:    9
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:    9
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    9
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  118356   330968 |   39452       0        0     nan |  0.000 % |
c |       100 |  118102   330208 |   43397      17       58     3.4 |  4.182 % |
c |       250 |  117895   329665 |   47736     116      718     6.2 |  4.373 % |
c |       476 |  117825   329455 |   52510     198      986     5.0 |  4.427 % |
c |       813 |  117367   328353 |   57761     406     1916     4.7 |  4.991 % |
c |      1319 |  116985   327268 |   63537     760     3885     5.1 |  5.310 % |
c |      2078 |  116816   326816 |   69891    1480     8112     5.5 |  5.466 % |
c |      3217 |  116351   325660 |   76880    2452    36035    14.7 |  5.921 % |
c |      4927 |  116206   325225 |   84568    3961    90825    22.9 |  6.034 % |
c |      7489 |  115578   323542 |   93025    6014   121348    20.2 |  6.657 % |
c |     11333 |  115099   322180 |  102328    9457   196337    20.8 |  7.061 % |
c |     17099 |  114379   320149 |  112561   14517   323642    22.3 |  7.680 % |
c |     25748 |  113673   318137 |  123817   22384   610242    27.3 |  8.279 % |
c |     38722 |  112558   315033 |  136199   34652  1058260    30.5 |  9.302 % |
c |     58183 |  111207   311282 |  149818   53612  1760332    32.8 | 10.570 % |
c |     87375 |  109739   307213 |  164800   82059  2866738    34.9 | 11.920 % |
c |    131165 |  108435   303580 |  181280  125245  4705759    37.6 | 13.091 % |
c |    196850 |  106859   299070 |  199408   24525   697160    28.4 | 14.441 % |
c |    295377 |  104691   293030 |  219349  121746  5318309    43.7 | 16.468 % |
c |    443166 |  102633   287277 |  241284   65118  2728193    41.9 | 18.351 % |
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.93 0.98 0.95 2/54 5190
Raw data (stat): 5190 (runsolver) R 5189 29151 29150 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423703193 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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.0008 s]
Raw data (loadavg): 0.94 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 3084 0 0 0 989 9 0 0 25 0 1 0 423703193 14303232 3012 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3492 3012 603 41 0 3451 0
vsize: 13968
[startup+20.0015 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 3272 0 0 0 1989 9 0 0 25 0 1 0 423703193 15114240 3200 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3690 3200 603 41 0 3649 0
vsize: 14760
[startup+30.0029 s]
Raw data (loadavg): 0.95 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 3499 0 0 0 2988 10 0 0 25 0 1 0 423703193 16056320 3427 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3920 3427 603 41 0 3879 0
vsize: 15680
[startup+40.0032 s]
Raw data (loadavg): 0.96 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 3786 0 0 0 3987 11 0 0 25 0 1 0 423703193 17207296 3714 4294967295 134512640 134672761 3221224560 3221223732 134556627 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4201 3714 603 41 0 4160 0
vsize: 16804
[startup+50.003 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 4044 0 0 0 4987 11 0 0 25 0 1 0 423703193 18284544 3972 4294967295 134512640 134672761 3221224560 3221223744 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4464 3972 603 41 0 4423 0
vsize: 17856
[startup+60.0031 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 4390 0 0 0 5986 12 0 0 25 0 1 0 423703193 19632128 4318 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4793 4318 603 41 0 4752 0
vsize: 19172
[startup+70.0036 s]
Raw data (loadavg): 0.97 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 4632 0 0 0 6986 13 0 0 25 0 1 0 423703193 20701184 4560 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5054 4560 603 41 0 5013 0
vsize: 20216
[startup+80.0045 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 4979 0 0 0 7985 14 0 0 25 0 1 0 423703193 22175744 4907 4294967295 134512640 134672761 3221224560 3221223664 134560235 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5414 4907 603 41 0 5373 0
vsize: 21656
[startup+90.0043 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 5159 0 0 0 8985 15 0 0 25 0 1 0 423703193 22851584 5087 4294967295 134512640 134672761 3221224560 3221223728 134560906 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5579 5087 603 41 0 5538 0
vsize: 22316
[startup+100.004 s]
Raw data (loadavg): 0.98 0.98 0.95 2/54 5190
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 5397 0 0 0 9984 15 0 0 25 0 1 0 423703193 23797760 5325 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5810 5325 603 41 0 5769 0
vsize: 23240
[startup+110.005 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 5685 0 0 0 10983 16 0 0 25 0 1 0 423703193 25010176 5613 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6106 5613 603 41 0 6065 0
vsize: 24424
[startup+120.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 6015 0 0 0 11981 18 0 0 25 0 1 0 423703193 26353664 5943 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6434 5943 603 41 0 6393 0
vsize: 25736
[startup+130.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 6171 0 0 0 12980 19 0 0 25 0 1 0 423703193 27156480 6099 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6630 6099 603 41 0 6589 0
vsize: 26520
[startup+140.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 6385 0 0 0 13978 21 0 0 25 0 1 0 423703193 28094464 6313 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6859 6313 603 41 0 6818 0
vsize: 27436
[startup+150.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 6603 0 0 0 14977 22 0 0 25 0 1 0 423703193 28901376 6531 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7056 6531 603 41 0 7015 0
vsize: 28224
[startup+160.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 6831 0 0 0 15977 23 0 0 25 0 1 0 423703193 29839360 6759 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7285 6759 603 41 0 7244 0
vsize: 29140
[startup+170.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 7098 0 0 0 16976 24 0 0 25 0 1 0 423703193 30908416 7026 4294967295 134512640 134672761 3221224560 3221223740 134556590 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7546 7026 603 41 0 7505 0
vsize: 30184
[startup+180.006 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 7382 0 0 0 17974 25 0 0 25 0 1 0 423703193 32112640 7310 4294967295 134512640 134672761 3221224560 3221223728 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7840 7310 603 41 0 7799 0
vsize: 31360
[startup+190.007 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 7617 0 0 0 18973 27 0 0 25 0 1 0 423703193 33046528 7545 4294967295 134512640 134672761 3221224560 3221223728 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8068 7545 603 41 0 8027 0
vsize: 32272
[startup+200.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 7942 0 0 0 19971 28 0 0 25 0 1 0 423703193 34250752 7870 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8362 7870 603 41 0 8321 0
vsize: 33448
[startup+210.008 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 8134 0 0 0 20971 29 0 0 25 0 1 0 423703193 35069952 8062 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8562 8062 603 41 0 8521 0
vsize: 34248
[startup+220.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 8323 0 0 0 21970 30 0 0 25 0 1 0 423703193 35876864 8251 4294967295 134512640 134672761 3221224560 3221223760 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8759 8251 603 41 0 8718 0
vsize: 35036
[startup+230.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 8538 0 0 0 22969 31 0 0 25 0 1 0 423703193 36687872 8466 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8957 8466 603 41 0 8916 0
vsize: 35828
[startup+240.009 s]
Raw data (loadavg): 0.99 0.98 0.95 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 8772 0 0 0 23968 32 0 0 25 0 1 0 423703193 37634048 8700 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9188 8700 603 41 0 9147 0
vsize: 36752
[startup+250.009 s]
Raw data (loadavg): 1.07 1.00 0.96 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 9013 0 0 0 24967 33 0 0 25 0 1 0 423703193 38580224 8941 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9419 8941 603 41 0 9378 0
vsize: 37676
[startup+260.01 s]
Raw data (loadavg): 1.06 1.00 0.96 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 9227 0 0 0 25966 34 0 0 25 0 1 0 423703193 39530496 9155 4294967295 134512640 134672761 3221224560 3221223760 134557809 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9651 9155 603 41 0 9610 0
vsize: 38604
[startup+270.011 s]
Raw data (loadavg): 1.05 1.00 0.96 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 9401 0 0 0 26965 35 0 0 25 0 1 0 423703193 40202240 9329 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9815 9329 603 41 0 9774 0
vsize: 39260
[startup+280.01 s]
Raw data (loadavg): 1.11 1.02 0.96 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 9714 0 0 0 27963 37 0 0 25 0 1 0 423703193 41934848 9642 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10238 9642 603 41 0 10197 0
vsize: 40952
[startup+290.011 s]
Raw data (loadavg): 1.10 1.02 0.96 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 9908 0 0 0 28962 38 0 0 25 0 1 0 423703193 42733568 9836 4294967295 134512640 134672761 3221224560 3221223756 134556584 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10433 9836 603 41 0 10392 0
vsize: 41732
[startup+300.011 s]
Raw data (loadavg): 1.08 1.01 0.96 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 10111 0 0 0 29961 38 0 0 25 0 1 0 423703193 43540480 10039 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10630 10039 603 41 0 10589 0
vsize: 42520
[startup+310.012 s]
Raw data (loadavg): 1.29 1.06 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 10433 0 0 0 30961 39 0 0 25 0 1 0 423703193 44879872 10361 4294967295 134512640 134672761 3221224560 3221223760 134557828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10957 10361 603 41 0 10916 0
vsize: 43828
[startup+320.012 s]
Raw data (loadavg): 1.25 1.06 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 10606 0 0 0 31960 40 0 0 25 0 1 0 423703193 45568000 10534 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11125 10534 603 41 0 11084 0
vsize: 44500
[startup+330.013 s]
Raw data (loadavg): 1.21 1.06 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 10790 0 0 0 32958 42 0 0 25 0 1 0 423703193 46366720 10718 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11320 10718 603 41 0 11279 0
vsize: 45280
[startup+340.013 s]
Raw data (loadavg): 1.18 1.06 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 11003 0 0 0 33957 43 0 0 25 0 1 0 423703193 47169536 10931 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11516 10931 603 41 0 11475 0
vsize: 46064
[startup+350.013 s]
Raw data (loadavg): 1.15 1.05 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 11305 0 0 0 34955 45 0 0 25 0 1 0 423703193 48373760 11233 4294967295 134512640 134672761 3221224560 3221223744 134556589 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11810 11233 603 41 0 11769 0
vsize: 47240
[startup+360.014 s]
Raw data (loadavg): 1.13 1.05 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 11451 0 0 0 35955 45 0 0 25 0 1 0 423703193 49049600 11379 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11975 11379 603 41 0 11934 0
vsize: 47900
[startup+370.015 s]
Raw data (loadavg): 1.11 1.05 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 11683 0 0 0 36954 46 0 0 25 0 1 0 423703193 49991680 11611 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12205 11611 603 41 0 12164 0
vsize: 48820
[startup+380.014 s]
Raw data (loadavg): 1.09 1.05 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 11832 0 0 0 37953 47 0 0 25 0 1 0 423703193 50532352 11760 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12337 11760 603 41 0 12296 0
vsize: 49348
[startup+390.015 s]
Raw data (loadavg): 1.08 1.05 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12030 0 0 0 38953 47 0 0 25 0 1 0 423703193 51351552 11958 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12537 11958 603 41 0 12496 0
vsize: 50148
[startup+400.015 s]
Raw data (loadavg): 1.06 1.04 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12158 0 0 0 39952 48 0 0 25 0 1 0 423703193 51904512 12086 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12672 12086 603 41 0 12631 0
vsize: 50688
[startup+410.016 s]
Raw data (loadavg): 1.05 1.04 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12237 0 0 0 40951 49 0 0 25 0 1 0 423703193 52174848 12165 4294967295 134512640 134672761 3221224560 3221223728 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12738 12165 603 41 0 12697 0
vsize: 50952
[startup+420.016 s]
Raw data (loadavg): 1.04 1.04 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12464 0 0 0 41951 50 0 0 25 0 1 0 423703193 53112832 12392 4294967295 134512640 134672761 3221224560 3221223728 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12967 12392 603 41 0 12926 0
vsize: 51868
[startup+430.016 s]
Raw data (loadavg): 1.04 1.04 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12660 0 0 0 42950 51 0 0 25 0 1 0 423703193 53927936 12588 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13166 12588 603 41 0 13125 0
vsize: 52664
[startup+440.016 s]
Raw data (loadavg): 1.03 1.04 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 43950 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+450.016 s]
Raw data (loadavg): 1.03 1.03 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 44949 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223696 134560604 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+460.016 s]
Raw data (loadavg): 1.02 1.03 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 45949 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+470.017 s]
Raw data (loadavg): 1.02 1.03 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 46950 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+480.016 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 47950 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+490.017 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 48950 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+500.017 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 49950 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+510.017 s]
Raw data (loadavg): 1.01 1.03 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 50950 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223664 134560393 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+520.017 s]
Raw data (loadavg): 1.01 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 51950 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223760 134557959 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+530.017 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 52951 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+540.017 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 53951 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+550.018 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 54951 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+560.018 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 55951 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+570.018 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 56951 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+580.018 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 57951 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134560920 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+590.019 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 58952 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+600.018 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 59952 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223744 134559538 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+610.02 s]
Raw data (loadavg): 1.00 1.02 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12723 0 0 0 60952 51 0 0 25 0 1 0 423703193 54198272 12651 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12651 603 41 0 13191 0
vsize: 52928
[startup+620.02 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 61952 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+630.02 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 62951 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+640.021 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 63951 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+650.02 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 64951 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+660.02 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 65951 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+670.021 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 66952 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+680.021 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 67952 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+690.021 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 68952 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+700.021 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12724 0 0 0 69952 51 0 0 25 0 1 0 423703193 54198272 12652 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13232 12652 603 41 0 13191 0
vsize: 52928
[startup+710.021 s]
Raw data (loadavg): 1.00 1.01 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 12900 0 0 0 70952 52 0 0 25 0 1 0 423703193 54874112 12828 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13397 12828 603 41 0 13356 0
vsize: 53588
[startup+720.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 13211 0 0 0 71951 53 0 0 25 0 1 0 423703193 56213504 13139 4294967295 134512640 134672761 3221224560 3221223728 134561207 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13724 13139 603 41 0 13683 0
vsize: 54896
[startup+730.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 13365 0 0 0 72951 53 0 0 25 0 1 0 423703193 56750080 13293 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13855 13293 603 41 0 13814 0
vsize: 55420
[startup+740.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 13565 0 0 0 73951 53 0 0 25 0 1 0 423703193 57556992 13493 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14052 13493 603 41 0 14011 0
vsize: 56208
[startup+750.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 13747 0 0 0 74950 54 0 0 25 0 1 0 423703193 58359808 13675 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14248 13675 603 41 0 14207 0
vsize: 56992
[startup+760.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 13936 0 0 0 75950 55 0 0 25 0 1 0 423703193 59150336 13864 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14441 13864 603 41 0 14400 0
vsize: 57764
[startup+770.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 14027 0 0 0 76950 55 0 0 25 0 1 0 423703193 59551744 13955 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14539 13955 603 41 0 14498 0
vsize: 58156
[startup+780.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 14318 0 0 0 77950 55 0 0 25 0 1 0 423703193 60768256 14246 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14836 14246 603 41 0 14795 0
vsize: 59344
[startup+790.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 14594 0 0 0 78949 56 0 0 25 0 1 0 423703193 61845504 14522 4294967295 134512640 134672761 3221224560 3221223728 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15099 14522 603 41 0 15058 0
vsize: 60396
[startup+800.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 14848 0 0 0 79948 57 0 0 25 0 1 0 423703193 62918656 14776 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15361 14776 603 41 0 15320 0
vsize: 61444
[startup+810.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 15137 0 0 0 80948 58 0 0 25 0 1 0 423703193 63995904 15065 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15624 15065 603 41 0 15583 0
vsize: 62496
[startup+820.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 15325 0 0 0 81947 58 0 0 25 0 1 0 423703193 64798720 15253 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15820 15253 603 41 0 15779 0
vsize: 63280
[startup+830.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 15560 0 0 0 82947 59 0 0 25 0 1 0 423703193 65761280 15488 4294967295 134512640 134672761 3221224560 3221223728 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16055 15488 603 41 0 16014 0
vsize: 64220
[startup+840.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 15783 0 0 0 83946 60 0 0 25 0 1 0 423703193 66707456 15711 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16286 15711 603 41 0 16245 0
vsize: 65144
[startup+850.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 15886 0 0 0 84946 60 0 0 25 0 1 0 423703193 67117056 15814 4294967295 134512640 134672761 3221224560 3221223728 134560888 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16386 15814 603 41 0 16345 0
vsize: 65544
[startup+860.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 16079 0 0 0 85946 60 0 0 25 0 1 0 423703193 67919872 16007 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16582 16007 603 41 0 16541 0
vsize: 66328
[startup+870.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 16297 0 0 0 86945 61 0 0 25 0 1 0 423703193 68730880 16225 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16780 16225 603 41 0 16739 0
vsize: 67120
[startup+880.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 16587 0 0 0 87944 62 0 0 25 0 1 0 423703193 69943296 16515 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17076 16515 603 41 0 17035 0
vsize: 68304
[startup+890.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 16752 0 0 0 88944 62 0 0 25 0 1 0 423703193 70619136 16680 4294967295 134512640 134672761 3221224560 3221223664 134560289 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17241 16680 603 41 0 17200 0
vsize: 68964
[startup+900.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 16970 0 0 0 89944 62 0 0 25 0 1 0 423703193 71426048 16898 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17438 16898 603 41 0 17397 0
vsize: 69752
[startup+910.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 90944 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+920.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 91945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+930.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 92945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223664 134560048 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+940.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 93945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+950.021 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 94945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+960.022 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 95945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223744 134558662 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+970.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 96945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+980.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 97945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223696 134560588 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+990.023 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 98945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223744 134559342 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1000.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 99945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1010.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 100945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1020.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 101945 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1030.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 102946 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223696 134560673 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1040.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 103946 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223664 134560291 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1050.02 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 104946 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134561198 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1060.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 105946 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223732 134556653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1070.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 106946 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1080.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 107946 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1090.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 108947 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1100.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 109947 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1110.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 110947 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1120.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 111947 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1130.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 112947 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1140.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 113948 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1150.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17009 0 0 0 114948 63 0 0 25 0 1 0 423703193 71696384 16937 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16937 603 41 0 17463 0
vsize: 70016
[startup+1160.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17010 0 0 0 115948 63 0 0 25 0 1 0 423703193 71696384 16938 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16938 603 41 0 17463 0
vsize: 70016
[startup+1170.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17011 0 0 0 116948 63 0 0 25 0 1 0 423703193 71696384 16939 4294967295 134512640 134672761 3221224560 3221223728 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16939 603 41 0 17463 0
vsize: 70016
[startup+1180.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17011 0 0 0 117948 63 0 0 25 0 1 0 423703193 71696384 16939 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16939 603 41 0 17463 0
vsize: 70016
[startup+1190.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17011 0 0 0 118949 63 0 0 25 0 1 0 423703193 71696384 16939 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16939 603 41 0 17463 0
vsize: 70016
[startup+1200.03 s]
Raw data (loadavg): 1.00 1.00 0.98 2/54 5192
Raw data (stat): 5190 (minisat+) R 5189 29151 29150 0 -1 0 17011 0 0 0 119949 63 0 0 25 0 1 0 423703193 71696384 16939 4294967295 134512640 134672761 3221224560 3221223732 134556639 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17504 16939 603 41 0 17463 0
vsize: 70016
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 0.98 1/54 5192
Raw data (stat): 5190 (minisat+) Z 5189 29151 29150 0 -1 12 17013 0 0 0 119949 66 0 0 25 0 1 0 423703193 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.06
CPU time (s): 1200.16
CPU user time (s): 1199.49
CPU system time (s): 0.663899
CPU usage (%): 100.008
Max. virtual memory (Kb): 70016
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####