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 5092

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc26 THE 2005-04-13 21:54:33 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=3263 boxname=wulflinc26 idbench=363 idsolver=5 numberseed=0
MD5SUM SOLVER: 1d62365061f6d70b1a242542b016b2e4  /oldhome/oroussel/solvers/minisat+
MD5SUM BENCH:  4caec1e880871fcef3276cf001aca352  /oldhome/oroussel/tmp/wulflinc26/normalized-ppp:1-13.opb
REAL COMMAND:  minisat+ /oldhome/oroussel/tmp/wulflinc26/normalized-ppp:1-13.opb
IDLAUNCH: 3263
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 888.83

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.061
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	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        853492 kB
Buffers:         33812 kB
Cached:         106988 kB
SwapCached:       2476 kB
Active:          52588 kB
Inactive:        93528 kB
HighTotal:      131008 kB
HighFree:        20916 kB
LowTotal:       903652 kB
LowFree:        832576 kB
SwapTotal:     2097892 kB
SwapFree:      2095416 kB
Dirty:              52 kB
Writeback:           0 kB
Mapped:           6948 kB
Slab:            29456 kB
Committed_AS:    63616 kB
PageTables:        320 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:14:35 (client local time) WITH STATUS 0 IN 1200.24 SECONDS
stats: 3263 7 1200.24 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 |   79110   218410 |   26370       0        0     nan |  0.000 % |
c |       100 |   79110   218410 |   29007     100     1324    13.2 |  3.984 % |
c |       251 |   79110   218410 |   31907     251     6401    25.5 |  3.984 % |
c |       476 |   79110   218410 |   35098     476    18104    38.0 |  3.984 % |
c |       813 |   79110   218410 |   38608     813    30074    37.0 |  3.984 % |
c |      1321 |   79110   218410 |   42469    1321    44483    33.7 |  3.984 % |
c |      2081 |   79110   218410 |   46716    2081    71709    34.5 |  3.984 % |
c |      3226 |   79110   218410 |   51387    3226   130154    40.3 |  3.984 % |
c |      4936 |   79110   218410 |   56526    4936   206772    41.9 |  3.984 % |
c |      7499 |   79110   218410 |   62179    7499   303117    40.4 |  3.984 % |
c |     11344 |   79110   218410 |   68396   11344   509585    44.9 |  3.984 % |
c |     17113 |   79110   218410 |   75236   17113  1054449    61.6 |  3.984 % |
c |     25762 |   79110   218410 |   82760   25762  1562028    60.6 |  3.984 % |
c |     38737 |   79110   218410 |   91036   38737  2122378    54.8 |  3.984 % |
c |     58199 |   79110   218410 |  100140   58199  4146022    71.2 |  3.984 % |
c |     87391 |   79110   218410 |  110154   87391  6812247    78.0 |  3.984 % |
c |    131183 |   79110   218410 |  121169   29517  2998783   101.6 |  3.984 % |
c |    196867 |   79110   218410 |  133286   95201 10223985   107.4 |  3.984 % |
c |    295398 |   79110   218410 |  146615   64032  8332535   130.1 |  3.984 % |
c |    443194 |   79110   218410 |  161276   77800  8445018   108.5 |  3.984 % |
#### 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.84 0.94 0.90 2/54 25976
Raw data (stat): 25976 (runsolver) R 25975 22612 22611 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479353519 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0001 s]
Raw data (loadavg): 0.87 0.94 0.90 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 3917 0 0 0 986 12 0 0 25 0 1 0 479353519 17649664 3845 4294967295 134512640 134672761 3221224640 3221223808 134560830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4309 3845 603 41 0 4268 0
vsize: 17236
[startup+19.9998 s]
Raw data (loadavg): 0.89 0.94 0.90 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 4913 0 0 0 1983 15 0 0 25 0 1 0 479353519 21708800 4841 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5300 4841 603 41 0 5259 0
vsize: 21200
[startup+30.0003 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 5839 0 0 0 2981 17 0 0 25 0 1 0 479353519 25604096 5767 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6251 5767 603 41 0 6210 0
vsize: 25004
[startup+40.0002 s]
Raw data (loadavg): 0.92 0.94 0.90 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 6572 0 0 0 3979 18 0 0 25 0 1 0 479353519 28561408 6500 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6973 6500 603 41 0 6932 0
vsize: 27892
[startup+50.0008 s]
Raw data (loadavg): 0.93 0.94 0.90 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 7332 0 0 0 4976 21 0 0 25 0 1 0 479353519 31670272 7260 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7732 7260 603 41 0 7691 0
vsize: 30928
[startup+60.0003 s]
Raw data (loadavg): 0.94 0.95 0.90 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 8139 0 0 0 5973 25 0 0 25 0 1 0 479353519 35053568 8067 4294967295 134512640 134672761 3221224640 3221223776 134560677 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8558 8067 603 41 0 8517 0
vsize: 34232
[startup+70.0003 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 9148 0 0 0 6970 28 0 0 25 0 1 0 479353519 39354368 9076 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9608 9076 603 41 0 9567 0
vsize: 38432
[startup+80.0009 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 10180 0 0 0 7968 30 0 0 25 0 1 0 479353519 43524096 10108 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10626 10108 603 41 0 10585 0
vsize: 42504
[startup+90.0003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 11079 0 0 0 8966 32 0 0 25 0 1 0 479353519 47165440 11007 4294967295 134512640 134672761 3221224640 3221223776 134565092 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11515 11008 603 41 0 11474 0
vsize: 46060
[startup+100 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 11914 0 0 0 9963 35 0 0 25 0 1 0 479353519 50540544 11842 4294967295 134512640 134672761 3221224640 3221223808 134560940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12339 11842 603 41 0 12298 0
vsize: 49356
[startup+110.001 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 12642 0 0 0 10962 37 0 0 25 0 1 0 479353519 53493760 12570 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13060 12570 603 41 0 13019 0
vsize: 52240
[startup+120 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13286 0 0 0 11960 38 0 0 25 0 1 0 479353519 56193024 13214 4294967295 134512640 134672761 3221224640 3221223808 134561229 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13719 13214 603 41 0 13678 0
vsize: 54876
[startup+130 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13488 0 0 0 12960 39 0 0 25 0 1 0 479353519 56999936 13416 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13416 603 41 0 13875 0
vsize: 55664
[startup+140 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13488 0 0 0 13960 39 0 0 25 0 1 0 479353519 56999936 13416 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13416 603 41 0 13875 0
vsize: 55664
[startup+150 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 14960 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+160 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 15960 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134560892 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+170 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 16960 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223824 134559045 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+180 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 17961 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134560920 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+190 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 18961 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223744 134560344 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+200.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 19961 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 20961 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134561164 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+220.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 21961 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223744 134560051 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 22962 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+240.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 23962 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+250.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 24962 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13489 0 0 0 25962 39 0 0 25 0 1 0 479353519 56999936 13417 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13916 13417 603 41 0 13875 0
vsize: 55664
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13506 0 0 0 26962 39 0 0 25 0 1 0 479353519 57180160 13434 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13960 13434 603 41 0 13919 0
vsize: 55840
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13506 0 0 0 27962 39 0 0 25 0 1 0 479353519 57180160 13434 4294967295 134512640 134672761 3221224640 3221223744 134560148 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13960 13434 603 41 0 13919 0
vsize: 55840
[startup+290.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 13826 0 0 0 28961 41 0 0 25 0 1 0 479353519 58388480 13754 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14255 13754 603 41 0 14214 0
vsize: 57020
[startup+300.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 14168 0 0 0 29960 42 0 0 25 0 1 0 479353519 59957248 14096 4294967295 134512640 134672761 3221224640 3221223840 134557852 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14638 14096 603 41 0 14597 0
vsize: 58552
[startup+310.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 14465 0 0 0 30960 42 0 0 25 0 1 0 479353519 61157376 14393 4294967295 134512640 134672761 3221224640 3221223808 134561016 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14931 14393 603 41 0 14890 0
vsize: 59724
[startup+320.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 14782 0 0 0 31959 43 0 0 25 0 1 0 479353519 62472192 14710 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15252 14710 603 41 0 15211 0
vsize: 61008
[startup+330.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 25976
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 15042 0 0 0 32959 43 0 0 25 0 1 0 479353519 63549440 14970 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15515 14970 603 41 0 15474 0
vsize: 62060
[startup+340.004 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 26030
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 15986 0 0 0 33953 49 0 0 25 0 1 0 479353519 67452928 15914 4294967295 134512640 134672761 3221224640 3221223808 134560994 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16468 15914 603 41 0 16427 0
vsize: 65872
[startup+350.005 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 26030
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 16766 0 0 0 34951 51 0 0 25 0 1 0 479353519 70696960 16694 4294967295 134512640 134672761 3221224640 3221223808 134560888 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17260 16694 603 41 0 17219 0
vsize: 69040
[startup+360.005 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 26030
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 17441 0 0 0 35949 53 0 0 25 0 1 0 479353519 73400320 17369 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17920 17369 603 41 0 17879 0
vsize: 71680
[startup+370.005 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 26030
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 17953 0 0 0 36948 54 0 0 25 0 1 0 479353519 75554816 17881 4294967295 134512640 134672761 3221224640 3221223808 134560937 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18446 17881 603 41 0 18405 0
vsize: 73784
[startup+380.005 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 26030
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 18413 0 0 0 37947 56 0 0 25 0 1 0 479353519 77479936 18341 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18916 18341 603 41 0 18875 0
vsize: 75664
[startup+390.006 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 26030
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 18741 0 0 0 38946 57 0 0 25 0 1 0 479353519 78839808 18669 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19248 18669 603 41 0 19207 0
vsize: 76992
[startup+400.007 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 19174 0 0 0 39945 58 0 0 25 0 1 0 479353519 81166336 19102 4294967295 134512640 134672761 3221224640 3221223808 134561400 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19816 19102 603 41 0 19775 0
vsize: 79264
[startup+410.007 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 19637 0 0 0 40944 60 0 0 25 0 1 0 479353519 83050496 19565 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20276 19566 603 41 0 20235 0
vsize: 81104
[startup+420.006 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20095 0 0 0 41943 61 0 0 25 0 1 0 479353519 84811776 20023 4294967295 134512640 134672761 3221224640 3221223640 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20706 20023 603 41 0 20665 0
vsize: 82824
[startup+430.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20528 0 0 0 42942 62 0 0 25 0 1 0 479353519 86716416 20456 4294967295 134512640 134672761 3221224640 3221223744 134559872 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21171 20456 603 41 0 21130 0
vsize: 84684
[startup+440.006 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 43941 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223744 134554642 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+450.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 44941 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+460.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 45941 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134561215 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+470.007 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 46941 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223840 134557911 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+480.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 47942 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223824 134559356 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+490.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 48942 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223744 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+500.007 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 49942 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+510.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 50942 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+520.008 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 51942 63 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+530.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 52942 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+540.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 53943 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+550.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 54943 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223776 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+560.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 55943 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560980 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+570.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 56943 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+580.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 57943 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560806 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+590.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 58943 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223744 134560010 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+600.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 59942 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+610.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 60942 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223744 134560402 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+620.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 61943 64 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223856 134558181 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+630.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 62943 65 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+640.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 63943 65 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560954 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+650.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 64943 65 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+660.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 65943 65 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223824 134559503 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+670.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26032
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 66943 65 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+680.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 67944 65 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+690.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20721 0 0 0 68944 65 0 0 25 0 1 0 479353519 87388160 20649 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21335 20649 603 41 0 21294 0
vsize: 85340
[startup+700.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 69944 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223744 134554636 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+710.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 70944 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+720.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 71944 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+730.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 72944 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560912 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+740.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 73944 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223744 134560370 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+750.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 74945 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+760.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 75945 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134561151 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+770.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 76945 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+780.013 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 77945 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223744 134560246 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+790.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 78945 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223776 134565066 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+800.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 79946 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+810.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 80946 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134561218 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+820.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 81946 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134561382 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+830.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 82946 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+840.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 83946 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+850.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 84946 65 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+860.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 85946 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223744 134559927 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+870.016 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 86946 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+880.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 87946 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560983 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+890.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 88946 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134561011 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+900.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 89947 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+910.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 90947 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+920.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 91947 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+930.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 92947 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+940.017 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 93947 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+950.018 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20860 0 0 0 94947 66 0 0 25 0 1 0 479353519 87924736 20788 4294967295 134512640 134672761 3221224640 3221223744 134560289 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21466 20788 603 41 0 21425 0
vsize: 85864
[startup+960.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 20946 0 0 0 95947 66 0 0 25 0 1 0 479353519 88330240 20874 4294967295 134512640 134672761 3221224640 3221223808 134561207 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21565 20874 603 41 0 21524 0
vsize: 86260
[startup+970.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 21317 0 0 0 96946 67 0 0 25 0 1 0 479353519 89939968 21245 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21958 21245 603 41 0 21917 0
vsize: 87832
[startup+980.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 21584 0 0 0 97946 68 0 0 25 0 1 0 479353519 91017216 21512 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22221 21512 603 41 0 22180 0
vsize: 88884
[startup+990.019 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 21792 0 0 0 98945 69 0 0 25 0 1 0 479353519 91828224 21720 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22419 21720 603 41 0 22378 0
vsize: 89676
[startup+1000.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 22024 0 0 0 99944 70 0 0 25 0 1 0 479353519 92839936 21952 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22666 21952 603 41 0 22625 0
vsize: 90664
[startup+1010.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 22286 0 0 0 100943 71 0 0 25 0 1 0 479353519 93917184 22214 4294967295 134512640 134672761 3221224640 3221223808 134560903 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22929 22214 603 41 0 22888 0
vsize: 91716
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 22571 0 0 0 101943 72 0 0 25 0 1 0 479353519 95162368 22499 4294967295 134512640 134672761 3221224640 3221223808 134561139 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23233 22499 603 41 0 23192 0
vsize: 92932
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 22836 0 0 0 102942 73 0 0 25 0 1 0 479353519 96264192 22764 4294967295 134512640 134672761 3221224640 3221223744 134559887 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23502 22764 603 41 0 23461 0
vsize: 94008
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 23103 0 0 0 103941 74 0 0 25 0 1 0 479353519 97333248 23031 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23763 23031 603 41 0 23722 0
vsize: 95052
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 23396 0 0 0 104940 75 0 0 25 0 1 0 479353519 98533376 23324 4294967295 134512640 134672761 3221224640 3221223808 134560996 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24056 23324 603 41 0 24015 0
vsize: 96224
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 23673 0 0 0 105940 75 0 0 25 0 1 0 479353519 99733504 23601 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24349 23601 603 41 0 24308 0
vsize: 97396
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 23941 0 0 0 106939 76 0 0 25 0 1 0 479353519 100798464 23869 4294967295 134512640 134672761 3221224640 3221223776 134560706 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24609 23869 603 41 0 24568 0
vsize: 98436
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 24207 0 0 0 107938 77 0 0 25 0 1 0 479353519 101998592 24135 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24902 24135 603 41 0 24861 0
vsize: 99608
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 24451 0 0 0 108938 78 0 0 25 0 1 0 479353519 102944768 24379 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25133 24379 603 41 0 25092 0
vsize: 100532
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 24681 0 0 0 109938 78 0 0 25 0 1 0 479353519 103870464 24609 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25359 24609 603 41 0 25318 0
vsize: 101436
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 24943 0 0 0 110938 79 0 0 25 0 1 0 479353519 104943616 24871 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25621 24871 603 41 0 25580 0
vsize: 102484
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 25214 0 0 0 111937 79 0 0 25 0 1 0 479353519 106196992 25142 4294967295 134512640 134672761 3221224640 3221223744 134560235 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25927 25142 603 41 0 25886 0
vsize: 103708
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 25461 0 0 0 112936 80 0 0 25 0 1 0 479353519 107130880 25389 4294967295 134512640 134672761 3221224640 3221223776 134560588 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26155 25389 603 41 0 26114 0
vsize: 104620
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 25712 0 0 0 113936 81 0 0 25 0 1 0 479353519 108232704 25640 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26424 25640 603 41 0 26383 0
vsize: 105696
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 26004 0 0 0 114935 82 0 0 25 0 1 0 479353519 109436928 25932 4294967295 134512640 134672761 3221224640 3221223808 134560869 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26718 25932 603 41 0 26677 0
vsize: 106872
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 26220 0 0 0 115935 82 0 0 25 0 1 0 479353519 110493696 26148 4294967295 134512640 134672761 3221224640 3221223808 134560999 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26976 26148 603 41 0 26935 0
vsize: 107904
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 26410 0 0 0 116934 83 0 0 25 0 1 0 479353519 111161344 26338 4294967295 134512640 134672761 3221224640 3221223808 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27139 26338 603 41 0 27098 0
vsize: 108556
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 26626 0 0 0 117934 84 0 0 25 0 1 0 479353519 112099328 26554 4294967295 134512640 134672761 3221224640 3221223808 134560906 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27368 26554 603 41 0 27327 0
vsize: 109472
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 26861 0 0 0 118933 84 0 0 25 0 1 0 479353519 113037312 26789 4294967295 134512640 134672761 3221224640 3221223808 134560895 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27597 26789 603 41 0 27556 0
vsize: 110388
[startup+1200.03 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 26034
Raw data (stat): 25976 (minisat+) R 25975 22612 22611 0 -1 0 27069 0 0 0 119933 85 0 0 25 0 1 0 479353519 113844224 26997 4294967295 134512640 134672761 3221224640 3221223808 134561205 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27794 26997 603 41 0 27753 0
vsize: 111176
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.08 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 26034
Raw data (stat): 25976 (minisat+) Z 25975 22612 22611 0 -1 12 27071 0 0 0 119933 90 0 0 25 0 1 0 479353519 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.08
CPU time (s): 1200.24
CPU user time (s): 1199.33
CPU system time (s): 0.905862
CPU usage (%): 100.014
Max. virtual memory (Kb): 111176
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####