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-12,16.opb
MD5SUM	41edd2db35f2c8eb6d4b1f0a68a60338
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	102
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	6.63699
Number of variables	4662
Total number of constraints	36387
Number of constraints which are clauses	30696
Number of constraints which are cardinality constraints (but not clauses)	5613
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 6450

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc29 THE 2005-04-14 05:03:55 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4874 boxname=wulflinc29 idbench=362 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  41edd2db35f2c8eb6d4b1f0a68a60338  /oldhome/oroussel/tmp/wulflinc29/normalized-ppp:1-12,16.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc29/normalized-ppp:1-12,16.opb /oldhome/oroussel/tmp/wulflinc29/normalized-ppp:1-12,16.opb
IDLAUNCH: 4874
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.020
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.020
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:        810992 kB
Buffers:         36880 kB
Cached:         148884 kB
SwapCached:         12 kB
Active:          66632 kB
Inactive:       121988 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        810740 kB
SwapTotal:     2097892 kB
SwapFree:      2097880 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            29404 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 05:19:23 (client local time) WITH STATUS 30 IN 927.159 SECONDS
stats: 4874 7 927.159 30
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 31899 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ........................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[31898]---> BDD-cost:   86
c ---[31897]---> BDD-cost:   86
c ---[31896]---> BDD-cost:   86
c ---[31895]---> BDD-cost:   86
c ---[31894]---> BDD-cost:   86
c ---[31893]---> BDD-cost:   86
c ---[31892]---> BDD-cost:  102
c ---[31891]---> BDD-cost:  102
c ---[31890]---> BDD-cost:  102
c ---[31889]---> BDD-cost:  102
c ---[31888]---> BDD-cost:  102
c ---[31887]---> BDD-cost:  102
c ---[31886]---> BDD-cost:  111
c ---[31885]---> BDD-cost:  111
c ---[31884]---> BDD-cost:  111
c ---[31883]---> BDD-cost:  111
c ---[31882]---> BDD-cost:  111
c ---[31881]---> BDD-cost:  111
c ---[31880]---> BDD-cost:  111
c ---[31879]---> BDD-cost:  111
c ---[31878]---> BDD-cost:  111
c ---[31877]---> BDD-cost:  111
c ---[31876]---> BDD-cost:  111
c ---[31875]---> BDD-cost:  111
c ---[31874]---> BDD-cost:  111
c ---[31873]---> BDD-cost:  111
c ---[31872]---> BDD-cost:  111
c ---[31871]---> BDD-cost:  111
c ---[31870]---> BDD-cost:  111
c ---[31869]---> BDD-cost:  111
c ---[31868]---> BDD-cost:  122
c ---[31867]---> BDD-cost:  122
c ---[31866]---> BDD-cost:  122
c ---[31865]---> BDD-cost:  122
c ---[31864]---> BDD-cost:  122
c ---[31863]---> BDD-cost:  122
c ---[31862]---> BDD-cost:  111
c ---[31861]---> BDD-cost:  111
c ---[31860]---> BDD-cost:  111
c ---[31859]---> BDD-cost:  111
c ---[31858]---> BDD-cost:  111
c ---[31857]---> BDD-cost:  111
c ---[31856]---> BDD-cost:  111
c ---[31855]---> BDD-cost:  111
c ---[31854]---> BDD-cost:  111
c ---[31853]---> BDD-cost:  111
c ---[31852]---> BDD-cost:  111
c ---[31851]---> BDD-cost:  111
c ---[31850]---> BDD-cost:  111
c ---[31849]---> BDD-cost:  111
c ---[31848]---> BDD-cost:  111
c ---[31847]---> BDD-cost:  111
c ---[31846]---> BDD-cost:  111
c ---[31845]---> BDD-cost:  111
c ---[31844]---> Sorter-cost:  508     Base: 2 2
c ---[31843]---> Sorter-cost:  508     Base: 2 2
c ---[31842]---> Sorter-cost:  508     Base: 2 2
c ---[31841]---> Sorter-cost:  508     Base: 2 2
c ---[31840]---> Sorter-cost:  508     Base: 2 2
c ---[31839]---> Sorter-cost:  508     Base: 2 2
c ---[31838]---> Sorter-cost:  508     Base: 2 2
c ---[31837]---> Sorter-cost:  508     Base: 2 2
c ---[31836]---> Sorter-cost:  508     Base: 2 2
c ---[31835]---> Sorter-cost:  508     Base: 2 2
c ---[31834]---> Sorter-cost:  508     Base: 2 2
c ---[31833]---> Sorter-cost:  508     Base: 2 2
c ---[31832]---> BDD-cost:   86
c ---[31831]---> BDD-cost:   86
c ---[31830]---> BDD-cost:   86
c ---[31829]---> BDD-cost:   86
c ---[31828]---> BDD-cost:   86
c ---[31827]---> BDD-cost:   86
c ---[31826]---> BDD-cost:   58
c ---[31825]---> BDD-cost:   58
c ---[31824]---> BDD-cost:   58
c ---[31823]---> BDD-cost:   58
c ---[31822]---> BDD-cost:   58
c ---[31821]---> BDD-cost:   58
c ---[31819]---> BDD-cost:   23
c ---[31817]---> BDD-cost:   23
c ---[31815]---> BDD-cost:   23
c ---[31813]---> BDD-cost:   23
c ---[31811]---> BDD-cost:   23
c ---[31809]---> BDD-cost:   23
c ---[31807]---> BDD-cost:   23
c ---[31805]---> BDD-cost:   23
c ---[31803]---> BDD-cost:   23
c ---[31801]---> BDD-cost:   23
c ---[31799]---> BDD-cost:   23
c ---[31797]---> BDD-cost:   23
c ---[31795]---> BDD-cost:   23
c ---[31793]---> BDD-cost:   23
c ---[31791]---> BDD-cost:   23
c ---[31789]---> BDD-cost:   23
c ---[31787]---> BDD-cost:   23
c ---[31785]---> BDD-cost:   23
c ---[31783]---> BDD-cost:   21
c ---[31781]---> BDD-cost:   21
c ---[31779]---> BDD-cost:   21
c ---[31777]---> BDD-cost:   21
c ---[31775]---> BDD-cost:   21
c ---[31773]---> BDD-cost:   21
c ---[31771]---> BDD-cost:   23
c ---[31769]---> BDD-cost:   23
c ---[31767]---> BDD-cost:   23
c ---[31765]---> BDD-cost:   23
c ---[31763]---> BDD-cost:   23
c ---[31761]---> BDD-cost:   23
c ---[31759]---> BDD-cost:   23
c ---[31757]---> BDD-cost:   23
c ---[31755]---> BDD-cost:   23
c ---[31753]---> BDD-cost:   23
c ---[31751]---> BDD-cost:   23
c ---[31749]---> BDD-cost:   23
c ---[31747]---> BDD-cost:   21
c ---[31745]---> BDD-cost:   21
c ---[31743]---> BDD-cost:   21
c ---[31741]---> BDD-cost:   21
c ---[31739]---> BDD-cost:   21
c ---[31737]---> BDD-cost:   21
c ---[31735]---> BDD-cost:   17
c ---[31733]---> BDD-cost:   17
c ---[31731]---> BDD-cost:   17
c ---[31729]---> BDD-cost:   17
c ---[31727]---> BDD-cost:   17
c ---[31725]---> BDD-cost:   17
c ---[31723]---> BDD-cost:   23
c ---[31721]---> BDD-cost:   23
c ---[31719]---> BDD-cost:   23
c ---[31717]---> BDD-cost:   23
c ---[31715]---> BDD-cost:   23
c ---[31713]---> BDD-cost:   23
c ---[31711]---> BDD-cost:   23
c ---[31709]---> BDD-cost:   23
c ---[31707]---> BDD-cost:   23
c ---[31705]---> BDD-cost:   23
c ---[31703]---> BDD-cost:   23
c ---[31701]---> BDD-cost:   23
c ---[31699]---> BDD-cost:   23
c ---[31697]---> BDD-cost:   23
c ---[31695]---> BDD-cost:   23
c ---[31693]---> BDD-cost:   23
c ---[31691]---> BDD-cost:   23
c ---[31689]---> BDD-cost:   23
c ---[31687]---> BDD-cost:   21
c ---[31685]---> BDD-cost:   21
c ---[31683]---> BDD-cost:   21
c ---[31681]---> BDD-cost:   21
c ---[31679]---> BDD-cost:   21
c ---[31677]---> BDD-cost:   21
c ---[31675]---> BDD-cost:   23
c ---[31673]---> BDD-cost:   23
c ---[31671]---> BDD-cost:   23
c ---[31669]---> BDD-cost:   23
c ---[31667]---> BDD-cost:   23
c ---[31665]---> BDD-cost:   23
c ---[31663]---> BDD-cost:   23
c ---[31661]---> BDD-cost:   23
c ---[31659]---> BDD-cost:   23
c ---[31657]---> BDD-cost:   23
c ---[31655]---> BDD-cost:   23
c ---[31653]---> BDD-cost:   23
c ---[31651]---> BDD-cost:   23
c ---[31649]---> BDD-cost:   23
c ---[31647]---> BDD-cost:   23
c ---[31645]---> BDD-cost:   23
c ---[31643]---> BDD-cost:   23
c ---[31641]---> BDD-cost:   23
c ---[31639]---> BDD-cost:   23
c ---[31637]---> BDD-cost:   23
c ---[31635]---> BDD-cost:   23
c ---[31633]---> BDD-cost:   23
c ---[31631]---> BDD-cost:   23
c ---[31629]---> BDD-cost:   23
c ---[31627]---> BDD-cost:   23
c ---[31625]---> BDD-cost:   23
c ---[31623]---> BDD-cost:   23
c ---[31621]---> BDD-cost:   23
c ---[31619]---> BDD-cost:   23
c ---[31617]---> BDD-cost:   23
c ---[31615]---> BDD-cost:   23
c ---[31613]---> BDD-cost:   23
c ---[31611]---> BDD-cost:   23
c ---[31609]---> BDD-cost:   23
c ---[31607]---> BDD-cost:   23
c ---[31605]---> BDD-cost:   23
c ---[31603]---> BDD-cost:   23
c ---[31601]---> BDD-cost:   23
c ---[31599]---> BDD-cost:   23
c ---[31597]---> BDD-cost:   23
c ---[31595]---> BDD-cost:   23
c ---[31593]---> BDD-cost:   23
c ---[31591]---> BDD-cost:   23
c ---[31589]---> BDD-cost:   23
c ---[31587]---> BDD-cost:   23
c ---[31585]---> BDD-cost:   23
c ---[31583]---> BDD-cost:   23
c ---[31581]---> BDD-cost:   23
c ---[31579]---> BDD-cost:   23
c ---[31577]---> BDD-cost:   23
c ---[31575]---> BDD-cost:   23
c ---[31573]---> BDD-cost:   23
c ---[31571]---> BDD-cost:   23
c ---[31569]---> BDD-cost:   23
c ---[31567]---> BDD-cost:   23
c ---[31565]---> BDD-cost:   23
c ---[31563]---> BDD-cost:   23
c ---[31561]---> BDD-cost:   23
c ---[31559]---> BDD-cost:   23
c ---[31557]---> BDD-cost:   23
c ---[31555]---> BDD-cost:   23
c ---[31553]---> BDD-cost:   23
c ---[31551]---> BDD-cost:   23
c ---[31549]---> BDD-cost:   23
c ---[31547]---> BDD-cost:   23
c ---[31545]---> BDD-cost:   23
c ---[31543]---> BDD-cost:   23
c ---[31541]---> BDD-cost:   23
c ---[31539]---> BDD-cost:   23
c ---[31537]---> BDD-cost:   23
c ---[31535]---> BDD-cost:   23
c ---[31533]---> BDD-cost:   23
c ---[31531]---> BDD-cost:   23
c ---[31529]---> BDD-cost:   23
c ---[31527]---> BDD-cost:   23
c ---[31525]---> BDD-cost:   23
c ---[31523]---> BDD-cost:   23
c ---[31521]---> BDD-cost:   23
c ---[31519]---> BDD-cost:   23
c ---[31517]---> BDD-cost:   23
c ---[31515]---> BDD-cost:   23
c ---[31513]---> BDD-cost:   23
c ---[31511]---> BDD-cost:   23
c ---[31509]---> BDD-cost:   23
c ---[31507]---> BDD-cost:   23
c ---[31505]---> BDD-cost:   23
c ---[31503]---> BDD-cost:   23
c ---[31501]---> BDD-cost:   23
c ---[31499]---> BDD-cost:   23
c ---[31497]---> BDD-cost:   23
c ---[31495]---> BDD-cost:   23
c ---[31493]---> BDD-cost:   23
c ---[31491]---> BDD-cost:   23
c ---[31489]---> BDD-cost:   23
c ---[31487]---> BDD-cost:   23
c ---[31485]---> BDD-cost:   23
c ---[31483]---> BDD-cost:   23
c ---[31481]---> BDD-cost:   23
c ---[31479]---> BDD-cost:   23
c ---[31477]---> BDD-cost:   23
c ---[31475]---> BDD-cost:   23
c ---[31473]---> BDD-cost:   23
c ---[31472]---> BDD-cost:    9
c ---[31471]---> BDD-cost:    9
c ---[31470]---> BDD-cost:    9
c ---[31469]---> BDD-cost:    9
c ---[31468]---> BDD-cost:    9
c ---[31467]---> BDD-cost:    9
c ---[31466]---> BDD-cost:    9
c ---[31465]---> BDD-cost:    9
c ---[31464]---> BDD-cost:    9
c ---[31463]---> BDD-cost:    9
c ---[31462]---> BDD-cost:    9
c ---[31461]---> BDD-cost:    9
c ---[31460]---> BDD-cost:    9
c ---[31459]---> BDD-cost:    9
c ---[31458]---> BDD-cost:    9
c ---[31457]---> BDD-cost:    9
c ---[31456]---> BDD-cost:    9
c ---[31455]---> BDD-cost:    9
c ---[31454]---> BDD-cost:    9
c ---[31453]---> BDD-cost:    9
c ---[31452]---> BDD-cost:    9
c ---[31451]---> BDD-cost:    9
c ---[31450]---> BDD-cost:    9
c ---[31449]---> BDD-cost:    9
c ---[31448]---> BDD-cost:    9
c ---[31447]---> BDD-cost:    9
c ---[31446]---> BDD-cost:    9
c ---[31445]---> BDD-cost:    9
c ---[31444]---> BDD-cost:    9
c ---[31443]---> BDD-cost:    9
c ---[31442]---> BDD-cost:    9
c ---[31441]---> BDD-cost:    9
c ---[31440]---> BDD-cost:    9
c ---[31439]---> BDD-cost:    9
c ---[31438]---> BDD-cost:    9
c ---[31437]---> BDD-cost:    9
c ---[31436]---> BDD-cost:    9
c ---[31435]---> BDD-cost:    9
c ---[31434]---> BDD-cost:    9
c ---[31433]---> BDD-cost:    9
c ---[31432]---> BDD-cost:    9
c ---[31431]---> BDD-cost:    9
c ---[31430]---> BDD-cost:    9
c ---[31429]---> BDD-cost:    9
c ---[31428]---> BDD-cost:    9
c ---[31427]---> BDD-cost:    9
c ---[31426]---> BDD-cost:    9
c ---[31425]---> BDD-cost:    9
c ---[31424]---> BDD-cost:    9
c ---[31423]---> BDD-cost:    9
c ---[31422]---> BDD-cost:    9
c ---[31421]---> BDD-cost:    9
c ---[31420]---> BDD-cost:    9
c ---[31419]---> BDD-cost:    9
c ---[31418]---> BDD-cost:    9
c ---[31417]---> BDD-cost:    9
c ---[31416]---> BDD-cost:    9
c ---[31415]---> BDD-cost:    9
c ---[31414]---> BDD-cost:    9
c ---[31413]---> BDD-cost:    9
c ---[31412]---> BDD-cost:    9
c ---[31411]---> BDD-cost:    9
c ---[31410]---> BDD-cost:    9
c ---[31409]---> BDD-cost:    9
c ---[31408]---> BDD-cost:    9
c ---[31407]---> BDD-cost:    9
c ---[31406]---> BDD-cost:    9
c ---[31405]---> BDD-cost:    9
c ---[31404]---> BDD-cost:    9
c ---[31403]---> BDD-cost:    9
c ---[31402]---> BDD-cost:    9
c ---[31401]---> BDD-cost:    9
c ---[31400]---> BDD-cost:    9
c ---[31399]---> BDD-cost:    9
c ---[31398]---> BDD-cost:    9
c ---[31397]---> BDD-cost:    9
c ---[31396]---> BDD-cost:    9
c ---[31395]---> BDD-cost:    9
c ---[31394]---> BDD-cost:    9
c ---[31393]---> BDD-cost:    9
c ---[31392]---> BDD-cost:    9
c ---[31391]---> BDD-cost:    9
c ---[31390]---> BDD-cost:    9
c ---[31389]---> BDD-cost:    9
c ---[31388]---> BDD-cost:    9
c ---[31387]---> BDD-cost:    9
c ---[31386]---> BDD-cost:    9
c ---[31385]---> BDD-cost:    9
c ---[31384]---> BDD-cost:    9
c ---[31383]---> BDD-cost:    9
c ---[31382]---> BDD-cost:    9
c ---[31381]---> BDD-cost:    9
c ---[31380]---> BDD-cost:    9
c ---[31379]---> BDD-cost:    9
c ---[31378]---> BDD-cost:    9
c ---[31377]---> BDD-cost:    9
c ---[31376]---> BDD-cost:    9
c ---[31375]---> BDD-cost:    9
c ---[31374]---> BDD-cost:    9
c ---[31373]---> BDD-cost:    9
c ---[31372]---> BDD-cost:    9
c ---[31371]---> BDD-cost:    9
c ---[31370]---> BDD-cost:    9
c ---[31369]---> BDD-cost:    9
c ---[31368]---> BDD-cost:    9
c ---[31367]---> BDD-cost:    9
c ---[31366]---> BDD-cost:    9
c ---[31365]---> BDD-cost:    9
c ---[31364]---> BDD-cost:    9
c ---[31363]---> BDD-cost:    9
c ---[31362]---> BDD-cost:    9
c ---[31361]---> BDD-cost:    9
c ---[31360]---> BDD-cost:    9
c ---[31359]---> BDD-cost:    9
c ---[31358]---> BDD-cost:    9
c ---[31357]---> BDD-cost:    9
c ---[31356]---> BDD-cost:    9
c ---[31355]---> BDD-cost:    9
c ---[31354]---> BDD-cost:    9
c ---[31353]---> BDD-cost:    9
c ---[31352]---> BDD-cost:    9
c ---[31351]---> BDD-cost:    9
c ---[31350]---> BDD-cost:    9
c ---[31349]---> BDD-cost:    9
c ---[31348]---> BDD-cost:    9
c ---[31347]---> BDD-cost:    9
c ---[31346]---> BDD-cost:    9
c ---[31345]---> BDD-cost:    9
c ---[31344]---> BDD-cost:    9
c ---[31343]---> BDD-cost:    9
c ---[31342]---> BDD-cost:    9
c ---[31341]---> BDD-cost:    9
c ---[31340]---> BDD-cost:    9
c ---[31339]---> BDD-cost:    9
c ---[31338]---> BDD-cost:    9
c ---[31337]---> BDD-cost:    9
c ---[31336]---> BDD-cost:    9
c ---[31335]---> BDD-cost:    9
c ---[31334]---> BDD-cost:    9
c ---[31333]---> BDD-cost:    9
c ---[31332]---> BDD-cost:    9
c ---[31331]---> BDD-cost:    9
c ---[31330]---> BDD-cost:    9
c ---[31329]---> BDD-cost:    9
c ---[31328]---> BDD-cost:    9
c ---[31327]---> BDD-cost:    9
c ---[31326]---> BDD-cost:    9
c ---[31325]---> BDD-cost:    9
c ---[31324]---> BDD-cost:    9
c ---[31323]---> BDD-cost:    9
c ---[31322]---> BDD-cost:    9
c ---[31321]---> BDD-cost:    9
c ---[31320]---> BDD-cost:    9
c ---[31319]---> BDD-cost:    9
c ---[31318]---> BDD-cost:    9
c ---[31317]---> BDD-cost:    9
c ---[31316]---> BDD-cost:    9
c ---[31315]---> BDD-cost:    9
c ---[31314]---> BDD-cost:    9
c ---[31313]---> BDD-cost:    9
c ---[31312]---> BDD-cost:    9
c ---[31311]---> BDD-cost:    9
c ---[31310]---> BDD-cost:    9
c ---[31309]---> BDD-cost:    9
c ---[31308]---> BDD-cost:    9
c ---[31307]---> BDD-cost:    9
c ---[31306]---> BDD-cost:    9
c ---[31305]---> BDD-cost:    9
c ---[31304]---> BDD-cost:    9
c ---[31303]---> BDD-cost:    9
c ---[31302]---> BDD-cost:    9
c ---[31301]---> BDD-cost:    9
c ---[31300]---> BDD-cost:    9
c ---[31299]---> BDD-cost:    9
c ---[31298]---> BDD-cost:    9
c ---[31297]---> BDD-cost:    9
c ---[31296]---> BDD-cost:    9
c ---[31295]---> BDD-cost:    9
c ---[31294]---> BDD-cost:    9
c ---[31293]---> BDD-cost:    9
c ---[31292]---> BDD-cost:    9
c ---[31291]---> BDD-cost:    9
c ---[31290]---> BDD-cost:    9
c ---[31289]---> BDD-cost:    9
c ---[31288]---> BDD-cost:    9
c ---[31287]---> BDD-cost:    9
c ---[31286]---> BDD-cost:    9
c ---[31285]---> BDD-cost:    9
c ---[31284]---> BDD-cost:    9
c ---[31283]---> BDD-cost:    9
c ---[31282]---> BDD-cost:    9
c ---[31281]---> BDD-cost:    9
c ---[31280]---> BDD-cost:    9
c ---[31279]---> BDD-cost:    9
c ---[31278]---> BDD-cost:    9
c ---[31277]---> BDD-cost:    9
c ---[31276]---> BDD-cost:    9
c ---[31275]---> BDD-cost:    9
c ---[31274]---> BDD-cost:    9
c ---[31273]---> BDD-cost:    9
c ---[31272]---> BDD-cost:    9
c ---[31271]---> BDD-cost:    9
c ---[31270]---> BDD-cost:    9
c ---[31269]---> BDD-cost:    9
c ---[31268]---> BDD-cost:    9
c ---[31267]---> BDD-cost:    9
c ---[31266]---> BDD-cost:    9
c ---[31265]---> BDD-cost:    9
c ---[31264]---> BDD-cost:    9
c ---[31263]---> BDD-cost:    9
c ---[31262]---> BDD-cost:    9
c ---[31261]---> BDD-cost:    9
c ---[31260]---> BDD-cost:    9
c ---[31259]---> BDD-cost:    9
c ---[31258]---> BDD-cost:    9
c ---[31257]---> BDD-cost:    9
c ---[31256]---> BDD-cost:    9
c ---[31255]---> BDD-cost:    9
c ---[31254]---> BDD-cost:    9
c ---[31253]---> BDD-cost:    9
c ---[31252]---> BDD-cost:    9
c ---[31251]---> BDD-cost:    9
c ---[31250]---> BDD-cost:    9
c ---[31249]---> BDD-cost:    9
c ---[31248]---> BDD-cost:    9
c ---[31247]---> BDD-cost:    9
c ---[31246]---> BDD-cost:    9
c ---[31245]---> BDD-cost:    9
c ---[31244]---> BDD-cost:    9
c ---[31243]---> BDD-cost:    9
c ---[31242]---> BDD-cost:    9
c ---[31241]---> BDD-cost:    9
c ---[31240]---> BDD-cost:    9
c ---[31239]---> BDD-cost:    9
c ---[31238]---> BDD-cost:    9
c ---[31237]---> BDD-cost:    9
c ---[31236]---> BDD-cost:    9
c ---[31235]---> BDD-cost:    9
c ---[31234]---> BDD-cost:    9
c ---[31233]---> BDD-cost:    9
c ---[31232]---> BDD-cost:    9
c ---[31231]---> BDD-cost:    9
c ---[31230]---> BDD-cost:    9
c ---[31229]---> BDD-cost:    9
c ---[31228]---> BDD-cost:    9
c ---[31227]---> BDD-cost:    9
c ---[31226]---> BDD-cost:    9
c ---[31225]---> BDD-cost:    9
c ---[31224]---> BDD-cost:    9
c ---[31223]---> BDD-cost:    9
c ---[31222]---> BDD-cost:    9
c ---[31221]---> BDD-cost:    9
c ---[31220]---> BDD-cost:    9
c ---[31219]---> BDD-cost:    9
c ---[31218]---> BDD-cost:    9
c ---[31217]---> BDD-cost:    9
c ---[31216]---> BDD-cost:    9
c ---[31215]---> BDD-cost:    9
c ---[31214]---> BDD-cost:    9
c ---[31213]---> BDD-cost:    9
c ---[31212]---> BDD-cost:    9
c ---[31211]---> BDD-cost:    9
c ---[31210]---> BDD-cost:    9
c ---[31209]---> BDD-cost:    9
c ---[31208]---> BDD-cost:    9
c ---[31207]---> BDD-cost:    9
c ---[31206]---> BDD-cost:    9
c ---[31205]---> BDD-cost:    9
c ---[31204]---> BDD-cost:    9
c ---[31203]---> BDD-cost:    9
c ---[31202]---> BDD-cost:    9
c ---[31201]---> BDD-cost:    9
c ---[31200]---> BDD-cost:    9
c ---[31199]---> BDD-cost:    9
c ---[31198]---> BDD-cost:    9
c ---[31197]---> BDD-cost:    9
c ---[31196]---> BDD-cost:    9
c ---[31195]---> BDD-cost:    9
c ---[31194]---> BDD-cost:    9
c ---[31193]---> BDD-cost:    9
c ---[31192]---> BDD-cost:    9
c ---[31191]---> BDD-cost:    9
c ---[31190]---> BDD-cost:    9
c ---[31189]---> BDD-cost:    9
c ---[31188]---> BDD-cost:    9
c ---[31187]---> BDD-cost:    9
c ---[31186]---> BDD-cost:    9
c ---[31185]---> BDD-cost:    9
c ---[31184]---> BDD-cost:    9
c ---[31183]---> BDD-cost:    9
c ---[31182]---> BDD-cost:    9
c ---[31181]---> BDD-cost:    9
c ---[31180]---> BDD-cost:    9
c ---[31179]---> BDD-cost:    9
c ---[31178]---> BDD-cost:    9
c ---[31177]---> BDD-cost:    9
c ---[31176]---> BDD-cost:    9
c ---[31175]---> BDD-cost:    9
c ---[31174]---> BDD-cost:    9
c ---[31173]---> BDD-cost:    9
c ---[31172]---> BDD-cost:    9
c ---[31171]---> BDD-cost:    9
c ---[31170]---> BDD-cost:    9
c ---[31169]---> BDD-cost:    9
c ---[31168]---> BDD-cost:    9
c ---[31167]---> BDD-cost:    9
c ---[31166]---> BDD-cost:    9
c ---[31165]---> BDD-cost:    9
c ---[31164]---> BDD-cost:    9
c ---[31163]---> BDD-cost:    9
c ---[31162]---> BDD-cost:    9
c ---[31161]---> BDD-cost:    9
c ---[31160]---> BDD-cost:    9
c ---[31159]---> BDD-cost:    9
c ---[31158]---> BDD-cost:    9
c ---[31157]---> BDD-cost:    9
c ---[31156]---> BDD-cost:    9
c ---[31155]---> BDD-cost:    9
c ---[31154]---> BDD-cost:    9
c ---[31153]---> BDD-cost:    9
c ---[31152]---> BDD-cost:    9
c ---[31151]---> BDD-cost:    9
c ---[31150]---> BDD-cost:    9
c ---[31149]---> BDD-cost:    9
c ---[31148]---> BDD-cost:    9
c ---[31147]---> BDD-cost:    9
c ---[31146]---> BDD-cost:    9
c ---[31145]---> BDD-cost:    9
c ---[31144]---> BDD-cost:    9
c ---[31143]---> BDD-cost:    9
c ---[31142]---> BDD-cost:    9
c ---[31141]---> BDD-cost:    9
c ---[31140]---> BDD-cost:    9
c ---[31139]---> BDD-cost:    9
c ---[31138]---> BDD-cost:    9
c ---[31137]---> BDD-cost:    9
c ---[31136]---> BDD-cost:    9
c ---[31135]---> BDD-cost:    9
c ---[31134]---> BDD-cost:    9
c ---[31133]---> BDD-cost:    9
c ---[31132]---> BDD-cost:    9
c ---[31131]---> BDD-cost:    9
c ---[31130]---> BDD-cost:    9
c ---[31129]---> BDD-cost:    9
c ---[31128]---> BDD-cost:    9
c ---[31127]---> BDD-cost:    9
c ---[31126]---> BDD-cost:    9
c ---[31125]---> BDD-cost:    9
c ---[31124]---> BDD-cost:    9
c ---[31123]---> BDD-cost:    9
c ---[31122]---> BDD-cost:    9
c ---[31121]---> BDD-cost:    9
c ---[31120]---> BDD-cost:    9
c ---[31119]---> BDD-cost:    9
c ---[31118]---> BDD-cost:    9
c ---[31117]---> BDD-cost:    9
c ---[31116]---> BDD-cost:    9
c ---[31115]---> BDD-cost:    9
c ---[31114]---> BDD-cost:    9
c ---[31113]---> BDD-cost:    9
c ---[31112]---> BDD-cost:    9
c ---[31111]---> BDD-cost:    9
c ---[31110]---> BDD-cost:    9
c ---[31109]---> BDD-cost:    9
c ---[31108]---> BDD-cost:    9
c ---[31107]---> BDD-cost:    9
c ---[31106]---> BDD-cost:    9
c ---[31105]---> BDD-cost:    9
c ---[31104]---> BDD-cost:    9
c ---[31103]---> BDD-cost:    9
c ---[31102]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:    9
c ---[ 402]---> BDD-cost:    9
c ---[ 401]---> BDD-cost:    9
c ---[ 400]---> BDD-cost:    9
c ---[ 399]---> BDD-cost:    9
c ---[ 398]---> BDD-cost:    9
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    9
c ---[ 395]---> BDD-cost:    9
c ---[ 394]---> BDD-cost:    9
c ---[ 393]---> BDD-cost:    9
c ---[ 392]---> BDD-cost:    9
c ---[ 391]---> BDD-cost:    9
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:    9
c ---[ 386]---> BDD-cost:    9
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    9
c ---[ 383]---> BDD-cost:    9
c ---[ 382]---> BDD-cost:    9
c ---[ 381]---> BDD-cost:    9
c ---[ 380]---> BDD-cost:    9
c ---[ 379]---> BDD-cost:    9
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    9
c ---[ 375]---> BDD-cost:    9
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 372]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:    9
c ---[ 369]---> BDD-cost:    9
c ---[ 368]---> BDD-cost:    9
c ---[ 367]---> BDD-cost:    9
c ---[ 366]---> BDD-cost:    9
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:    9
c ---[ 362]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    9
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:    9
c ---[ 354]---> BDD-cost:    9
c ---[ 353]---> BDD-cost:    9
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    9
c ---[ 350]---> BDD-cost:    9
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:    9
c ---[ 347]---> BDD-cost:    9
c ---[ 346]---> BDD-cost:    9
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    9
c ---[ 343]---> BDD-cost:    9
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:    9
c ---[ 338]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    9
c ---[ 336]---> BDD-cost:    9
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:    9
c ---[ 332]---> BDD-cost:    9
c ---[ 331]---> BDD-cost:    9
c ---[ 330]---> BDD-cost:    9
c ---[ 329]---> BDD-cost:    9
c ---[ 328]---> BDD-cost:    9
c ---[ 327]---> BDD-cost:    9
c ---[ 326]---> BDD-cost:    9
c ---[ 325]---> BDD-cost:    9
c ---[ 324]---> BDD-cost:    9
c ---[ 323]---> BDD-cost:    9
c ---[ 322]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    9
c ---[ 320]---> BDD-cost:    9
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    9
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    9
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    9
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:    9
c ---[ 306]---> BDD-cost:    9
c ---[ 305]---> BDD-cost:    9
c ---[ 304]---> BDD-cost:    9
c ---[ 303]---> BDD-cost:    9
c ---[ 302]---> BDD-cost:    9
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    9
c ---[ 297]---> BDD-cost:    9
c ---[ 296]---> BDD-cost:    9
c ---[ 295]---> BDD-cost:    9
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:    9
c ---[ 290]---> BDD-cost:    9
c ---[ 289]---> BDD-cost:    9
c ---[ 288]---> BDD-cost:    9
c ---[ 287]---> BDD-cost:    9
c ---[ 286]---> BDD-cost:    9
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    9
c ---[ 281]---> BDD-cost:    9
c ---[ 280]---> BDD-cost:    9
c ---[ 279]---> BDD-cost:    9
c ---[ 278]---> BDD-cost:    9
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    9
c ---[ 273]---> BDD-cost:    9
c ---[ 272]---> BDD-cost:    9
c ---[ 271]---> BDD-cost:    9
c ---[ 270]---> BDD-cost:    9
c ---[ 269]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:    9
c ---[ 267]---> BDD-cost:    9
c ---[ 266]---> BDD-cost:    9
c ---[ 265]---> BDD-cost:    9
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    9
c ---[ 257]---> BDD-cost:    9
c ---[ 256]---> BDD-cost:    9
c ---[ 255]---> BDD-cost:    9
c ---[ 254]---> BDD-cost:    9
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:    9
c ---[ 249]---> BDD-cost:    9
c ---[ 248]---> BDD-cost:    9
c ---[ 247]---> BDD-cost:    9
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:    9
c ---[ 241]---> BDD-cost:    9
c ---[ 240]---> BDD-cost:    9
c ---[ 239]---> BDD-cost:    9
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:    9
c ---[ 236]---> BDD-cost:    9
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:    9
c ---[ 233]---> BDD-cost:    9
c ---[ 232]---> BDD-cost:    9
c ---[ 231]---> BDD-cost:    9
c ---[ 230]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:    9
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:    9
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:    9
c ---[ 222]---> BDD-cost:    9
c ---[ 221]---> BDD-cost:    9
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:    9
c ---[ 218]---> BDD-cost:    9
c ---[ 217]---> BDD-cost:    9
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:    9
c ---[ 209]---> BDD-cost:    9
c ---[ 208]---> BDD-cost:    9
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:    9
c ---[ 204]---> BDD-cost:    9
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:    9
c ---[ 201]---> BDD-cost:    9
c ---[ 200]---> BDD-cost:    9
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:    9
c ---[ 194]---> BDD-cost:    9
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:    9
c ---[ 191]---> BDD-cost:    9
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:    9
c ---[ 188]---> BDD-cost:    9
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:    9
c ---[ 185]---> BDD-cost:    9
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:    9
c ---[ 182]---> BDD-cost:    9
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:    9
c ---[ 178]---> BDD-cost:    9
c ---[ 177]---> BDD-cost:    9
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:    9
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:    9
c ---[ 170]---> BDD-cost:    9
c ---[ 169]---> BDD-cost:    9
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    9
c ---[ 159]---> BDD-cost:    9
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    9
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:    9
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:    9
c ---[ 146]---> BDD-cost:    9
c ---[ 145]---> BDD-cost:    9
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:    9
c ---[ 142]---> BDD-cost:    9
c ---[ 141]---> BDD-cost:    9
c ---[ 140]---> BDD-cost:    9
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    9
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    9
c ---[ 134]---> BDD-cost:    9
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:    9
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    9
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:    9
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:    9
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:    9
c ---[ 108]---> BDD-cost:    9
c ---[ 107]---> BDD-cost:    9
c ---[ 106]---> BDD-cost:    9
c ---[ 105]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:    9
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    9
c ---[  98]---> BDD-cost:    9
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    9
c ---[  93]---> BDD-cost:    9
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:    9
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:    9
c ---[  87]---> BDD-cost:    9
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:    9
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:    9
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:    9
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    9
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:    9
c ---[  64]---> BDD-cost:    9
c ---[  63]---> BDD-cost:    9
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:    9
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:    9
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    9
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:    9
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:    9
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:    9
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:    9
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:    9
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:    9
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:    9
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    9
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  120408   336738 |   40136       0        0     nan |  0.000 % |
c |       100 |  120238   336300 |   44149      52      201     3.9 |  4.107 % |
c |       250 |  120018   335640 |   48564     122      482     4.0 |  4.275 % |
c |       475 |  119826   335095 |   53421     287     1241     4.3 |  4.429 % |
c |       812 |  119271   333740 |   58763     546     2706     5.0 |  4.980 % |
c |      1319 |  119236   333635 |   64639    1001    11932    11.9 |  5.007 % |
c |      2078 |  119221   333590 |   71103    1739    37128    21.4 |  5.019 % |
c |      3217 |  119086   333185 |   78213    2649    51245    19.3 |  5.122 % |
c |      4925 |  118760   332233 |   86035    4007    75530    18.8 |  5.379 % |
c |      7488 |  118200   330653 |   94638    6139   117020    19.1 |  5.854 % |
c |     11332 |  117399   328386 |  104102    9666   187545    19.4 |  6.528 % |
c |     17098 |  116474   325835 |  114512   14659   279027    19.0 |  7.344 % |
c |     25747 |  115232   322406 |  125963   22340   482182    21.6 |  8.451 % |
c |     38721 |  114200   319431 |  138560   34266   778576    22.7 |  9.313 % |
c |     58185 |  112274   314025 |  152416   52205  1384674    26.5 | 10.968 % |
c |     87377 |  109872   307329 |  167658   79844  2357288    29.5 | 13.071 % |
c |    131169 |  107727   301200 |  184423  122195  4141092    33.9 | 14.899 % |
c |    196853 |  105664   295505 |  202866  186447  7282954    39.1 | 16.730 % |
c |    295379 |  103087   288278 |  223152   98077  4072563    41.5 | 19.002 % |
c ==============================================================================
c [1mSATISFIABLE: No goal function specified.[0m
s SATISFIABLE
v
c _______________________________________________________________________________
c 
c restarts              : 19
c conflicts             : 378539         (408 /sec)
c decisions             : 1497744        (1616 /sec)
c propagations          : 0              (0 /sec)
c inspects              : 0              (0 /sec)
c CPU time              : 926.675 s
c _______________________________________________________________________________
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.85 0.97 0.91 2/54 2233
Raw data (stat): 2233 (runsolver) R 2232 27222 27221 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 481922658 1052672 99 4294967295 134512640 135381576 3221224464 3221219708 135158418 0 2147483391 7 90112 0 0 0 17 0 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.001 s]
Raw data (loadavg): 0.87 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 3168 0 0 0 989 9 0 0 25 0 1 0 481922658 14614528 3097 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3568 3097 603 41 0 3527 0
vsize: 14272
[startup+20.0012 s]
Raw data (loadavg): 0.89 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 3267 0 0 0 1988 10 0 0 25 0 1 0 481922658 15020032 3196 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3667 3196 603 41 0 3626 0
vsize: 14668
[startup+30.001 s]
Raw data (loadavg): 0.91 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 3419 0 0 0 2987 10 0 0 25 0 1 0 481922658 15720448 3348 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 3838 3348 603 41 0 3797 0
vsize: 15352
[startup+40.0011 s]
Raw data (loadavg): 0.92 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 3548 0 0 0 3987 11 0 0 25 0 1 0 481922658 16330752 3477 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3987 3477 603 41 0 3946 0
vsize: 15948
[startup+50.0015 s]
Raw data (loadavg): 0.93 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 3768 0 0 0 4986 12 0 0 25 0 1 0 481922658 17141760 3697 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4185 3697 603 41 0 4144 0
vsize: 16740
[startup+60.0013 s]
Raw data (loadavg): 0.94 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 3961 0 0 0 5985 12 0 0 25 0 1 0 481922658 17952768 3890 4294967295 134512640 134672761 3221224560 3221223728 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4383 3890 603 41 0 4342 0
vsize: 17532
[startup+70.0014 s]
Raw data (loadavg): 0.95 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 4188 0 0 0 6985 13 0 0 25 0 1 0 481922658 18886656 4117 4294967295 134512640 134672761 3221224560 3221223696 134560577 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4611 4117 603 41 0 4570 0
vsize: 18444
[startup+80.0008 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 4287 0 0 0 7985 13 0 0 25 0 1 0 481922658 19292160 4216 4294967295 134512640 134672761 3221224560 3221223760 134557849 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4710 4216 603 41 0 4669 0
vsize: 18840
[startup+90.0006 s]
Raw data (loadavg): 0.96 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 4569 0 0 0 8984 14 0 0 25 0 1 0 481922658 20504576 4498 4294967295 134512640 134672761 3221224560 3221223732 134556651 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5006 4498 603 41 0 4965 0
vsize: 20024
[startup+100.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 4737 0 0 0 9983 15 0 0 25 0 1 0 481922658 21180416 4666 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5171 4666 603 41 0 5130 0
vsize: 20684
[startup+110.001 s]
Raw data (loadavg): 0.97 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 4940 0 0 0 10983 16 0 0 25 0 1 0 481922658 21987328 4869 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5368 4869 603 41 0 5327 0
vsize: 21472
[startup+120.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2233
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 5181 0 0 0 11983 16 0 0 25 0 1 0 481922658 22929408 5110 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5598 5110 603 41 0 5557 0
vsize: 22392
[startup+130.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 5400 0 0 0 12982 17 0 0 25 0 1 0 481922658 23867392 5329 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5827 5329 603 41 0 5786 0
vsize: 23308
[startup+140.003 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 5551 0 0 0 13982 17 0 0 25 0 1 0 481922658 24408064 5480 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5959 5480 603 41 0 5918 0
vsize: 23836
[startup+150.002 s]
Raw data (loadavg): 0.98 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 5699 0 0 0 14982 17 0 0 25 0 1 0 481922658 25206784 5628 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6154 5628 603 41 0 6113 0
vsize: 24616
[startup+160.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 5788 0 0 0 15982 18 0 0 25 0 1 0 481922658 25612288 5717 4294967295 134512640 134672761 3221224560 3221223684 134566057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6253 5717 603 41 0 6212 0
vsize: 25012
[startup+170.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 5906 0 0 0 16982 18 0 0 25 0 1 0 481922658 26148864 5835 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6384 5835 603 41 0 6343 0
vsize: 25536
[startup+180.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 6067 0 0 0 17982 18 0 0 25 0 1 0 481922658 26689536 5996 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6516 5996 603 41 0 6475 0
vsize: 26064
[startup+190.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 6227 0 0 0 18981 19 0 0 25 0 1 0 481922658 27361280 6156 4294967295 134512640 134672761 3221224560 3221223728 134564748 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6680 6156 603 41 0 6639 0
vsize: 26720
[startup+200.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 6399 0 0 0 19981 19 0 0 25 0 1 0 481922658 28037120 6328 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6845 6328 603 41 0 6804 0
vsize: 27380
[startup+210.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 6675 0 0 0 20980 20 0 0 25 0 1 0 481922658 29249536 6604 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7141 6604 603 41 0 7100 0
vsize: 28564
[startup+220.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 6867 0 0 0 21980 21 0 0 25 0 1 0 481922658 29925376 6796 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7306 6796 603 41 0 7265 0
vsize: 29224
[startup+230.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 7037 0 0 0 22979 21 0 0 25 0 1 0 481922658 30597120 6966 4294967295 134512640 134672761 3221224560 3221223712 134565098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7470 6966 603 41 0 7429 0
vsize: 29880
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 7284 0 0 0 23979 22 0 0 25 0 1 0 481922658 31674368 7213 4294967295 134512640 134672761 3221224560 3221223728 134561014 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7733 7213 603 41 0 7692 0
vsize: 30932
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 7407 0 0 0 24979 22 0 0 25 0 1 0 481922658 32079872 7336 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7832 7336 603 41 0 7791 0
vsize: 31328
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 7549 0 0 0 25978 23 0 0 25 0 1 0 481922658 32751616 7478 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7996 7478 603 41 0 7955 0
vsize: 31984
[startup+270.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 7747 0 0 0 26978 23 0 0 25 0 1 0 481922658 33562624 7676 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8194 7676 603 41 0 8153 0
vsize: 32776
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 7848 0 0 0 27978 23 0 0 25 0 1 0 481922658 33964032 7777 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8292 7777 603 41 0 8251 0
vsize: 33168
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 7944 0 0 0 28978 24 0 0 25 0 1 0 481922658 34230272 7873 4294967295 134512640 134672761 3221224560 3221223732 134556671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8357 7873 603 41 0 8316 0
vsize: 33428
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 8375 0 0 0 29978 24 0 0 25 0 1 0 481922658 36085760 8304 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8810 8304 603 41 0 8769 0
vsize: 35240
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 8466 0 0 0 30977 25 0 0 25 0 1 0 481922658 36356096 8395 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8876 8395 603 41 0 8835 0
vsize: 35504
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 8598 0 0 0 31977 25 0 0 25 0 1 0 481922658 36896768 8527 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9008 8527 603 41 0 8967 0
vsize: 36032
[startup+330.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 8693 0 0 0 32976 26 0 0 25 0 1 0 481922658 37302272 8622 4294967295 134512640 134672761 3221224560 3221223728 134560942 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9107 8622 603 41 0 9066 0
vsize: 36428
[startup+340.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 8983 0 0 0 33975 26 0 0 25 0 1 0 481922658 38506496 8912 4294967295 134512640 134672761 3221224560 3221223732 134556688 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9401 8912 603 41 0 9360 0
vsize: 37604
[startup+350.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 9177 0 0 0 34974 27 0 0 25 0 1 0 481922658 39829504 9106 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9724 9106 603 41 0 9683 0
vsize: 38896
[startup+360.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 9235 0 0 0 35974 27 0 0 25 0 1 0 481922658 39964672 9164 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9757 9164 603 41 0 9716 0
vsize: 39028
[startup+370.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 9472 0 0 0 36974 28 0 0 25 0 1 0 481922658 40902656 9401 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9986 9401 603 41 0 9945 0
vsize: 39944
[startup+380.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 9864 0 0 0 37973 29 0 0 25 0 1 0 481922658 42512384 9793 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10379 9793 603 41 0 10338 0
vsize: 41516
[startup+390.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 10046 0 0 0 38973 29 0 0 25 0 1 0 481922658 43307008 9975 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10573 9975 603 41 0 10532 0
vsize: 42292
[startup+400.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 10334 0 0 0 39972 30 0 0 25 0 1 0 481922658 44376064 10263 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10834 10263 603 41 0 10793 0
vsize: 43336
[startup+410.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 10470 0 0 0 40972 31 0 0 25 0 1 0 481922658 45043712 10399 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10997 10399 603 41 0 10956 0
vsize: 43988
[startup+420.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 10568 0 0 0 41972 31 0 0 25 0 1 0 481922658 45449216 10497 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11096 10497 603 41 0 11055 0
vsize: 44384
[startup+430.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 10711 0 0 0 42972 31 0 0 25 0 1 0 481922658 45989888 10640 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11228 10640 603 41 0 11187 0
vsize: 44912
[startup+440.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 10843 0 0 0 43972 31 0 0 25 0 1 0 481922658 46526464 10772 4294967295 134512640 134672761 3221224560 3221223664 134559910 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11359 10772 603 41 0 11318 0
vsize: 45436
[startup+450.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 11179 0 0 0 44970 33 0 0 25 0 1 0 481922658 47869952 11108 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11687 11108 603 41 0 11646 0
vsize: 46748
[startup+460.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 11270 0 0 0 45970 33 0 0 25 0 1 0 481922658 48275456 11199 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11786 11199 603 41 0 11745 0
vsize: 47144
[startup+470.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 11522 0 0 0 46970 34 0 0 25 0 1 0 481922658 49217536 11451 4294967295 134512640 134672761 3221224560 3221223760 134561972 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12016 11451 603 41 0 11975 0
vsize: 48064
[startup+480.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 11727 0 0 0 47969 35 0 0 25 0 1 0 481922658 50032640 11656 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12215 11656 603 41 0 12174 0
vsize: 48860
[startup+490.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 11993 0 0 0 48968 36 0 0 25 0 1 0 481922658 51113984 11922 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12479 11922 603 41 0 12438 0
vsize: 49916
[startup+500.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 12284 0 0 0 49967 37 0 0 25 0 1 0 481922658 52322304 12213 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12774 12213 603 41 0 12733 0
vsize: 51096
[startup+510.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 12527 0 0 0 50966 38 0 0 25 0 1 0 481922658 53256192 12456 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13002 12456 603 41 0 12961 0
vsize: 52008
[startup+520.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 12638 0 0 0 51966 38 0 0 25 0 1 0 481922658 53661696 12567 4294967295 134512640 134672761 3221224560 3221223664 134560529 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13101 12567 603 41 0 13060 0
vsize: 52404
[startup+530.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 12766 0 0 0 52965 39 0 0 25 0 1 0 481922658 54206464 12695 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13234 12695 603 41 0 13193 0
vsize: 52936
[startup+540.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 12889 0 0 0 53965 39 0 0 25 0 1 0 481922658 54747136 12818 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13366 12818 603 41 0 13325 0
vsize: 53464
[startup+550.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 12930 0 0 0 54965 39 0 0 25 0 1 0 481922658 54878208 12859 4294967295 134512640 134672761 3221224560 3221223744 134558671 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13398 12859 603 41 0 13357 0
vsize: 53592
[startup+560.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13200 0 0 0 55965 40 0 0 25 0 1 0 481922658 55947264 13129 4294967295 134512640 134672761 3221224560 3221223664 134559933 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13659 13129 603 41 0 13618 0
vsize: 54636
[startup+570.006 s]
Raw data (loadavg): 0.99 0.97 0.91 3/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13335 0 0 0 56965 40 0 0 25 0 1 0 481922658 56479744 13264 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13789 13264 603 41 0 13748 0
vsize: 55156
[startup+580.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13603 0 0 0 57964 41 0 0 25 0 1 0 481922658 57556992 13532 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14052 13532 603 41 0 14011 0
vsize: 56208
[startup+590.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13641 0 0 0 58965 41 0 0 25 0 1 0 481922658 57827328 13570 4294967295 134512640 134672761 3221224560 3221223768 134561960 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14118 13570 603 41 0 14077 0
vsize: 56472
[startup+600.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13743 0 0 0 59965 41 0 0 25 0 1 0 481922658 58228736 13672 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14216 13672 603 41 0 14175 0
vsize: 56864
[startup+610.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 60965 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+620.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 61965 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223664 134559914 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+630.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 62965 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223744 134559376 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+640.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 63965 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+650.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 64965 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+660.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 65966 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223664 134560246 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+670.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 66966 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134561148 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+680.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 67966 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+690.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 68966 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+700.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 69966 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+710.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 70967 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+720.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 71967 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223732 134556646 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+730.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 72967 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+740.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 73966 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+750.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 74967 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223684 134566031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+760.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 75967 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560806 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+770.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 76967 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+780.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 77967 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223664 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+790.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 78967 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134561382 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+800.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 79968 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+810.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 80968 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223732 134556649 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+820.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 81968 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+830.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 82969 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+840.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 83979 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223684 134566068 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+850.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 84979 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223664 134559887 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+860.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 85980 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+870.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 86980 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+880.119 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13784 0 0 0 87980 41 0 0 25 0 1 0 481922658 58363904 13713 4294967295 134512640 134672761 3221224560 3221223656 1075347133 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14249 13713 603 41 0 14208 0
vsize: 56996
[startup+890.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 13986 0 0 0 88980 42 0 0 25 0 1 0 481922658 59183104 13915 4294967295 134512640 134672761 3221224560 3221223684 134566098 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14449 13915 603 41 0 14408 0
vsize: 57796
[startup+900.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 14271 0 0 0 89979 43 0 0 25 0 1 0 481922658 60395520 14200 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14745 14200 603 41 0 14704 0
vsize: 58980
[startup+910.12 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 14452 0 0 0 90978 43 0 0 25 0 1 0 481922658 61063168 14381 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14908 14381 603 41 0 14867 0
vsize: 59632
[startup+920.121 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 14595 0 0 0 91978 44 0 0 25 0 1 0 481922658 61739008 14524 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15073 14524 603 41 0 15032 0
vsize: 60292
[startup+927.052 s]
Raw data (loadavg): 0.99 0.97 0.91 1/53 2235
Raw data (stat): 2233 (minisat+) R 2232 27222 27221 0 -1 0 14595 0 0 0 91978 44 0 0 25 0 1 0 481922658 61739008 14524 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15073 14524 603 41 0 15032 0
vsize: 0

Child status: 30
Real time (s): 927.052
CPU time (s): 927.159
CPU user time (s): 926.684
CPU system time (s): 0.474927
CPU usage (%): 100.012
Max. virtual memory (Kb): 60292
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####