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 5659

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        822304 kB
Buffers:         35856 kB
Cached:         141288 kB
SwapCached:       2376 kB
Active:          59628 kB
Inactive:       122844 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        822052 kB
SwapTotal:     2097892 kB
SwapFree:      2095516 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           7036 kB
Slab:            24084 kB
Committed_AS:    63672 kB
PageTables:        328 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:41:28 (client local time) WITH STATUS 0 IN 1200.23 SECONDS
stats: 4123 7 1200.23 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   79110   218410 |   23732       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24680          
c   -- var.elim.:  2000/24680          
c   -- var.elim.:  3000/24680          
c   -- var.elim.:  4000/24680          
c   -- var.elim.:  5000/24680          
c   -- var.elim.:  6000/24680          
c   -- var.elim.:  7000/24680          
c   -- var.elim.:  8000/24680          
c   -- var.elim.:  9000/24680          
c   -- var.elim.:  10000/24680          
c   -- var.elim.:  11000/24680          
c   -- var.elim.:  12000/24680          
c   -- var.elim.:  13000/24680          
c   -- var.elim.:  14000/24680          
c   -- var.elim.:  15000/24680          
c   -- var.elim.:  16000/24680          
c   -- var.elim.:  17000/24680          
c   -- var.elim.:  18000/24680          
c   -- var.elim.:  19000/24680          
c   -- var.elim.:  20000/24680          
c   -- var.elim.:  21000/24680          
c   -- var.elim.:  22000/24680          
c   -- var.elim.:  23000/24680          
c   -- var.elim.:  24000/24680          
c   -- var.elim.:  24680/24680          
c   -- var.elim.:  1000/10782          
c   -- var.elim.:  2000/10782          
c   -- var.elim.:  3000/10782          
c   -- var.elim.:  4000/10782          
c   -- var.elim.:  5000/10782          
c   -- var.elim.:  6000/10782          
c   -- var.elim.:  7000/10782          
c   -- var.elim.:  8000/10782          
c   -- var.elim.:  9000/10782          
c   -- var.elim.:  10000/10782          
c   -- var.elim.:  10782/10782          
c   -- var.elim.:  816/816          
c   -- subsuming                       
c   -- var.elim.:  1000/9792          
c   -- var.elim.:  2000/9792          
c   -- var.elim.:  3000/9792          
c   -- var.elim.:  4000/9792          
c   -- var.elim.:  5000/9792          
c   -- var.elim.:  6000/9792          
c   -- var.elim.:  7000/9792          
c   -- var.elim.:  8000/9792          
c   -- var.elim.:  9000/9792          
c   -- var.elim.:  9792/9792          
c   -- var.elim.:  1000/9374          
c   -- var.elim.:  2000/9374          
c   -- var.elim.:  3000/9374          
c   -- var.elim.:  4000/9374          
c   -- var.elim.:  5000/9374          
c   -- var.elim.:  6000/9374          
c   -- var.elim.:  7000/9374          
c   -- var.elim.:  8000/93#### 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.97 0.91 2/55 27453
Raw data (stat): 27453 (runsolver) R 27452 20838 20837 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480597574 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 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+9.99981 s]
Raw data (loadavg): 0.87 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 5448 0 0 0 983 14 0 0 25 0 1 0 480597574 22384640 4707 4294967295 134512640 134672761 3221224560 3221223516 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5465 4707 603 41 0 5424 0
vsize: 21860
[startup+19.9998 s]
Raw data (loadavg): 0.89 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 6743 0 0 0 1981 17 0 0 25 0 1 0 480597574 27693056 6002 4294967295 134512640 134672761 3221224560 3221223744 134615673 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6761 6002 603 41 0 6720 0
vsize: 27044
[startup+29.9997 s]
Raw data (loadavg): 0.90 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 8029 0 0 0 2978 20 0 0 25 0 1 0 480597574 33005568 7288 4294967295 134512640 134672761 3221224560 3221223372 1075350517 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 8058 7288 603 41 0 8017 0
vsize: 32232
[startup+39.9993 s]
Raw data (loadavg): 0.92 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 9125 0 0 0 3975 23 0 0 25 0 1 0 480597574 37498880 8384 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9155 8384 603 41 0 9114 0
vsize: 36620
[startup+49.9996 s]
Raw data (loadavg): 0.93 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 9960 0 0 0 4974 25 0 0 25 0 1 0 480597574 40947712 9219 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9997 9219 603 41 0 9956 0
vsize: 39988
[startup+59.9995 s]
Raw data (loadavg): 0.94 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 11116 0 0 0 5972 27 0 0 25 0 1 0 480597574 45834240 10375 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11190 10375 603 41 0 11149 0
vsize: 44760
[startup+70.0004 s]
Raw data (loadavg): 0.95 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 12270 0 0 0 6969 29 0 0 25 0 1 0 480597574 50577408 11529 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12348 11529 603 41 0 12307 0
vsize: 49392
[startup+80.0004 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 13238 0 0 0 7967 32 0 0 25 0 1 0 480597574 54546432 12497 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13317 12497 603 41 0 13276 0
vsize: 53268
[startup+90.0003 s]
Raw data (loadavg): 0.96 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 13981 0 0 0 8965 34 0 0 25 0 1 0 480597574 57593856 13240 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14061 13240 603 41 0 14020 0
vsize: 56244
[startup+99.9999 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 15019 0 0 0 9963 36 0 0 25 0 1 0 480597574 61841408 14278 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15098 14278 603 41 0 15057 0
vsize: 60392
[startup+109.999 s]
Raw data (loadavg): 0.97 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 15916 0 0 0 10961 38 0 0 25 0 1 0 480597574 65404928 15175 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15968 15175 603 41 0 15927 0
vsize: 63872
[startup+120 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 16663 0 0 0 11958 41 0 0 25 0 1 0 480597574 68472832 15922 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16717 15922 603 41 0 16676 0
vsize: 66868
[startup+130 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 17289 0 0 0 12958 42 0 0 25 0 1 0 480597574 70991872 16548 4294967295 134512640 134672761 3221224560 3221223600 134613818 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17332 16548 603 41 0 17291 0
vsize: 69328
[startup+139.999 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 17932 0 0 0 13956 44 0 0 25 0 1 0 480597574 73633792 17191 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17977 17191 603 41 0 17936 0
vsize: 71908
[startup+150 s]
Raw data (loadavg): 0.98 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 14955 45 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 15955 45 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 16955 45 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 17955 45 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223552 134565056 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 18955 46 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 19955 46 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+210 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 20956 46 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+220 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 21956 46 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+230 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 22956 46 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+239.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27453
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 23956 46 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+249.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 24956 46 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223600 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+259.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18245 0 0 0 25956 46 0 0 25 0 1 0 480597574 74326016 17354 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18146 17354 603 41 0 18105 0
vsize: 72584
[startup+269.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18267 0 0 0 26957 46 0 0 25 0 1 0 480597574 74457088 17376 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18178 17376 603 41 0 18137 0
vsize: 72712
[startup+279.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 18806 0 0 0 27955 47 0 0 25 0 1 0 480597574 76697600 17915 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18725 17915 603 41 0 18684 0
vsize: 74900
[startup+289.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 19304 0 0 0 28953 49 0 0 25 0 1 0 480597574 78721024 18413 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19219 18413 603 41 0 19178 0
vsize: 76876
[startup+299.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 19910 0 0 0 29952 51 0 0 25 0 1 0 480597574 81235968 19019 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19833 19019 603 41 0 19792 0
vsize: 79332
[startup+309.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 20903 0 0 0 30948 55 0 0 25 0 1 0 480597574 85336064 20012 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20834 20012 603 41 0 20793 0
vsize: 83336
[startup+319.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 21476 0 0 0 31947 56 0 0 25 0 1 0 480597574 87719936 20585 4294967295 134512640 134672761 3221224560 3221223760 134610661 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21416 20585 603 41 0 21375 0
vsize: 85664
[startup+329.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 22075 0 0 0 32946 57 0 0 25 0 1 0 480597574 90103808 21184 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21998 21184 603 41 0 21957 0
vsize: 87992
[startup+339.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 22611 0 0 0 33945 59 0 0 25 0 1 0 480597574 92364800 21720 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22550 21720 603 41 0 22509 0
vsize: 90200
[startup+349.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 23109 0 0 0 34944 60 0 0 25 0 1 0 480597574 94355456 22218 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23036 22218 603 41 0 22995 0
vsize: 92144
[startup+359.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 24148 0 0 0 35942 62 0 0 25 0 1 0 480597574 98590720 23257 4294967295 134512640 134672761 3221224560 3221223568 134522555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24070 23257 603 41 0 24029 0
vsize: 96280
[startup+369.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 25316 0 0 0 36939 65 0 0 25 0 1 0 480597574 103886848 24425 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25363 24425 603 41 0 25322 0
vsize: 101452
[startup+379.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26005 0 0 0 37938 67 0 0 25 0 1 0 480597574 106336256 24940 4294967295 134512640 134672761 3221224560 3221223600 134612987 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24940 603 41 0 25920 0
vsize: 103844
[startup+389.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26006 0 0 0 38938 67 0 0 25 0 1 0 480597574 106336256 24941 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24941 603 41 0 25920 0
vsize: 103844
[startup+399.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 39938 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+409.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 40938 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+419.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 41938 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+429.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 42938 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223600 134614340 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+439.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 43938 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+449.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 44939 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+459.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 45939 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+469.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 46939 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+479.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 47939 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+489.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 48939 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+499.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 49939 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+509.997 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 50939 67 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+519.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 51939 68 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+529.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 52939 68 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+539.998 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27455
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 53939 68 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+549.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 54940 68 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+559.999 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 55938 68 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+570 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 56938 69 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223760 134610675 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+580.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26008 0 0 0 57938 69 0 0 25 0 1 0 480597574 106336256 24943 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 24943 603 41 0 25920 0
vsize: 103844
[startup+590 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26009 0 0 0 58938 69 0 0 25 0 1 0 480597574 106336256 24944 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 24944 603 41 0 25920 0
vsize: 103844
[startup+600.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26012 0 0 0 59937 70 0 0 25 0 1 0 480597574 106336256 24947 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 24947 603 41 0 25920 0
vsize: 103844
[startup+610.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26014 0 0 0 60937 70 0 0 25 0 1 0 480597574 106336256 24949 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 24949 603 41 0 25920 0
vsize: 103844
[startup+620.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26017 0 0 0 61937 70 0 0 25 0 1 0 480597574 106336256 24952 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25961 24952 603 41 0 25920 0
vsize: 103844
[startup+630.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26043 0 0 0 62937 70 0 0 25 0 1 0 480597574 106467328 24978 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25993 24978 603 41 0 25952 0
vsize: 103972
[startup+640.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26373 0 0 0 63936 72 0 0 25 0 1 0 480597574 107991040 25308 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26365 25308 603 41 0 26324 0
vsize: 105460
[startup+650.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26615 0 0 0 64935 73 0 0 25 0 1 0 480597574 108949504 25550 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26599 25550 603 41 0 26558 0
vsize: 106396
[startup+660.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26968 0 0 0 65934 74 0 0 25 0 1 0 480597574 110784512 25903 4294967295 134512640 134672761 3221224560 3221223616 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27047 25903 603 41 0 27006 0
vsize: 108188
[startup+670.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 66933 74 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+680.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 67933 74 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615676 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+690 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 68933 74 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223760 134610618 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+700.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 69933 74 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+710 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 70933 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+720.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 71934 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+730.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 72934 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+740 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 73934 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+750.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 74934 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+760 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 75934 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+770.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 76934 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+780.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 77934 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+790 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 78934 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+800.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 79935 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+810.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 80935 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+820.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 81935 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+830.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 82935 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+840 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27457
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 83935 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+850.001 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 84935 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615788 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+860.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 85936 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+870.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 86936 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+880.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 87936 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+890.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 88936 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+900.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26979 0 0 0 89936 75 0 0 25 0 1 0 480597574 109735936 25756 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26791 25756 603 41 0 26750 0
vsize: 107164
[startup+910.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26989 0 0 0 90936 75 0 0 25 0 1 0 480597574 109932544 25766 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26839 25766 603 41 0 26798 0
vsize: 107356
[startup+920.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 26989 0 0 0 91937 75 0 0 25 0 1 0 480597574 109932544 25766 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26839 25766 603 41 0 26798 0
vsize: 107356
[startup+930.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27012 0 0 0 92937 75 0 0 25 0 1 0 480597574 109932544 25789 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26839 25789 603 41 0 26798 0
vsize: 107356
[startup+940.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27012 0 0 0 93937 75 0 0 25 0 1 0 480597574 109932544 25789 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26839 25789 603 41 0 26798 0
vsize: 107356
[startup+950.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27012 0 0 0 94937 75 0 0 25 0 1 0 480597574 109932544 25789 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26839 25789 603 41 0 26798 0
vsize: 107356
[startup+960.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27036 0 0 0 95937 75 0 0 25 0 1 0 480597574 110129152 25813 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26887 25813 603 41 0 26846 0
vsize: 107548
[startup+970.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27037 0 0 0 96938 75 0 0 25 0 1 0 480597574 110129152 25814 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26887 25814 603 41 0 26846 0
vsize: 107548
[startup+980.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27046 0 0 0 97938 76 0 0 25 0 1 0 480597574 110129152 25823 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26887 25823 603 41 0 26846 0
vsize: 107548
[startup+990.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27058 0 0 0 98938 76 0 0 25 0 1 0 480597574 110325760 25835 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26935 25835 603 41 0 26894 0
vsize: 107740
[startup+1000 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27060 0 0 0 99938 76 0 0 25 0 1 0 480597574 110325760 25837 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26935 25837 603 41 0 26894 0
vsize: 107740
[startup+1010 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27071 0 0 0 100938 76 0 0 25 0 1 0 480597574 110325760 25848 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26935 25848 603 41 0 26894 0
vsize: 107740
[startup+1020 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27099 0 0 0 101938 76 0 0 25 0 1 0 480597574 110587904 25876 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26999 25876 603 41 0 26958 0
vsize: 107996
[startup+1030 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27101 0 0 0 102938 76 0 0 25 0 1 0 480597574 110587904 25878 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26999 25878 603 41 0 26958 0
vsize: 107996
[startup+1040 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27115 0 0 0 103938 76 0 0 25 0 1 0 480597574 110587904 25892 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26999 25892 603 41 0 26958 0
vsize: 107996
[startup+1050 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27125 0 0 0 104939 76 0 0 25 0 1 0 480597574 110587904 25902 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26999 25902 603 41 0 26958 0
vsize: 107996
[startup+1060 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27125 0 0 0 105938 76 0 0 25 0 1 0 480597574 110587904 25902 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26999 25902 603 41 0 26958 0
vsize: 107996
[startup+1070 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27125 0 0 0 106938 76 0 0 25 0 1 0 480597574 110587904 25902 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26999 25902 603 41 0 26958 0
vsize: 107996
[startup+1080 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27144 0 0 0 107938 76 0 0 25 0 1 0 480597574 110850048 25921 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27063 25921 603 41 0 27022 0
vsize: 108252
[startup+1090 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27149 0 0 0 108938 76 0 0 25 0 1 0 480597574 110850048 25926 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27063 25926 603 41 0 27022 0
vsize: 108252
[startup+1100 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27149 0 0 0 109939 76 0 0 25 0 1 0 480597574 110850048 25926 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27063 25926 603 41 0 27022 0
vsize: 108252
[startup+1110 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27149 0 0 0 110939 76 0 0 25 0 1 0 480597574 110850048 25926 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27063 25926 603 41 0 27022 0
vsize: 108252
[startup+1120 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27173 0 0 0 111939 76 0 0 25 0 1 0 480597574 110850048 25950 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27063 25950 603 41 0 27022 0
vsize: 108252
[startup+1130 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27197 0 0 0 112939 76 0 0 25 0 1 0 480597574 111112192 25974 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27127 25974 603 41 0 27086 0
vsize: 108508
[startup+1140 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27459
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27234 0 0 0 113939 76 0 0 25 0 1 0 480597574 111374336 26011 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27191 26011 603 41 0 27150 0
vsize: 108764
[startup+1150 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27461
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27261 0 0 0 114939 77 0 0 25 0 1 0 480597574 111374336 26038 4294967295 134512640 134672761 3221224560 3221223744 134615549 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27191 26038 603 41 0 27150 0
vsize: 108764
[startup+1160 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27461
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27284 0 0 0 115939 77 0 0 25 0 1 0 480597574 111636480 26061 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27255 26061 603 41 0 27214 0
vsize: 109020
[startup+1170 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27461
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27286 0 0 0 116940 77 0 0 25 0 1 0 480597574 111636480 26063 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27255 26063 603 41 0 27214 0
vsize: 109020
[startup+1180 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27461
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27287 0 0 0 117940 77 0 0 25 0 1 0 480597574 111636480 26064 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27255 26064 603 41 0 27214 0
vsize: 109020
[startup+1190 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27461
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27288 0 0 0 118940 77 0 0 25 0 1 0 480597574 111636480 26065 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27255 26065 603 41 0 27214 0
vsize: 109020
[startup+1200 s]
Raw data (loadavg): 0.99 0.97 0.91 2/55 27461
Raw data (stat): 27453 (minisat+) R 27452 20838 20837 0 -1 0 27290 0 0 0 119940 77 0 0 25 0 1 0 480597574 111636480 26067 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27255 26067 603 41 0 27214 0
vsize: 109020
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 0.99 0.97 0.91 1/55 27461
Raw data (stat): 27453 (minisat+) Z 27452 20838 20837 0 -1 12 27290 0 0 0 119940 82 0 0 25 0 1 0 480597574 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.06
CPU time (s): 1200.23
CPU user time (s): 1199.41
CPU system time (s): 0.822874
CPU usage (%): 100.014
Max. virtual memory (Kb): 109020
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####