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-9,16-19.opb
MD5SUM	a788dbf2f72289ace41b812e06d88575
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	101
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	362.64
Number of variables	4626
Total number of constraints	35373
Number of constraints which are clauses	29724
Number of constraints which are cardinality constraints (but not clauses)	5571
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 5093

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

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.072
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 901.12

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        737360 kB
Buffers:         37240 kB
Cached:         219120 kB
SwapCached:          0 kB
Active:          80384 kB
Inactive:       178800 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        737108 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32548 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-13 22:14:45 (client local time) WITH STATUS 0 IN 1200.21 SECONDS
stats: 3272 7 1200.21 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30921 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30920]---> BDD-cost:   87
c ---[30919]---> BDD-cost:   87
c ---[30918]---> BDD-cost:   87
c ---[30917]---> BDD-cost:   87
c ---[30916]---> BDD-cost:   87
c ---[30915]---> BDD-cost:   87
c ---[30914]---> BDD-cost:   87
c ---[30913]---> BDD-cost:   87
c ---[30912]---> BDD-cost:   87
c ---[30911]---> BDD-cost:   87
c ---[30910]---> BDD-cost:   87
c ---[30909]---> BDD-cost:   87
c ---[30908]---> BDD-cost:   87
c ---[30907]---> BDD-cost:   87
c ---[30906]---> BDD-cost:   87
c ---[30905]---> BDD-cost:   87
c ---[30904]---> BDD-cost:   87
c ---[30903]---> BDD-cost:   87
c ---[30902]---> BDD-cost:   58
c ---[30901]---> BDD-cost:   58
c ---[30900]---> BDD-cost:   58
c ---[30899]---> BDD-cost:   58
c ---[30898]---> BDD-cost:   58
c ---[30897]---> BDD-cost:   58
c ---[30896]---> BDD-cost:  113
c ---[30895]---> BDD-cost:  113
c ---[30894]---> BDD-cost:  113
c ---[30893]---> BDD-cost:  113
c ---[30892]---> BDD-cost:  113
c ---[30891]---> BDD-cost:  113
c ---[30890]---> BDD-cost:  124
c ---[30889]---> BDD-cost:  124
c ---[30888]---> BDD-cost:  124
c ---[30887]---> BDD-cost:  124
c ---[30886]---> BDD-cost:  124
c ---[30885]---> BDD-cost:  124
c ---[30884]---> BDD-cost:  113
c ---[30883]---> BDD-cost:  113
c ---[30882]---> BDD-cost:  113
c ---[30881]---> BDD-cost:  113
c ---[30880]---> BDD-cost:  113
c ---[30879]---> BDD-cost:  113
c ---[30878]---> BDD-cost:  113
c ---[30877]---> BDD-cost:  113
c ---[30876]---> BDD-cost:  113
c ---[30875]---> BDD-cost:  113
c ---[30874]---> BDD-cost:  113
c ---[30873]---> BDD-cost:  113
c ---[30872]---> BDD-cost:  113
c ---[30871]---> BDD-cost:  113
c ---[30870]---> BDD-cost:  113
c ---[30869]---> BDD-cost:  113
c ---[30868]---> BDD-cost:  113
c ---[30867]---> BDD-cost:  113
c ---[30866]---> Sorter-cost:  521     Base: 2 2
c ---[30865]---> Sorter-cost:  521     Base: 2 2
c ---[30864]---> Sorter-cost:  521     Base: 2 2
c ---[30863]---> Sorter-cost:  521     Base: 2 2
c ---[30862]---> Sorter-cost:  521     Base: 2 2
c ---[30861]---> Sorter-cost:  521     Base: 2 2
c ---[30860]---> Sorter-cost:  521     Base: 2 2
c ---[30859]---> Sorter-cost:  521     Base: 2 2
c ---[30858]---> Sorter-cost:  521     Base: 2 2
c ---[30857]---> Sorter-cost:  521     Base: 2 2
c ---[30856]---> Sorter-cost:  521     Base: 2 2
c ---[30855]---> Sorter-cost:  521     Base: 2 2
c ---[30854]---> BDD-cost:   87
c ---[30853]---> BDD-cost:   87
c ---[30852]---> BDD-cost:   87
c ---[30851]---> BDD-cost:   87
c ---[30850]---> BDD-cost:   87
c ---[30849]---> BDD-cost:   87
c ---[30848]---> BDD-cost:   58
c ---[30847]---> BDD-cost:   58
c ---[30846]---> BDD-cost:   58
c ---[30845]---> BDD-cost:   58
c ---[30844]---> BDD-cost:   58
c ---[30843]---> BDD-cost:   58
c ---[30841]---> BDD-cost:   23
c ---[30839]---> BDD-cost:   23
c ---[30837]---> BDD-cost:   23
c ---[30835]---> BDD-cost:   23
c ---[30833]---> BDD-cost:   23
c ---[30831]---> BDD-cost:   23
c ---[30829]---> BDD-cost:   23
c ---[30827]---> BDD-cost:   23
c ---[30825]---> BDD-cost:   23
c ---[30823]---> BDD-cost:   23
c ---[30821]---> BDD-cost:   23
c ---[30819]---> BDD-cost:   23
c ---[30817]---> BDD-cost:   23
c ---[30815]---> BDD-cost:   23
c ---[30813]---> BDD-cost:   23
c ---[30811]---> BDD-cost:   23
c ---[30809]---> BDD-cost:   23
c ---[30807]---> BDD-cost:   23
c ---[30805]---> BDD-cost:   19
c ---[30803]---> BDD-cost:   19
c ---[30801]---> BDD-cost:   19
c ---[30799]---> BDD-cost:   19
c ---[30797]---> BDD-cost:   19
c ---[30795]---> BDD-cost:   19
c ---[30793]---> BDD-cost:   23
c ---[30791]---> BDD-cost:   23
c ---[30789]---> BDD-cost:   23
c ---[30787]---> BDD-cost:   23
c ---[30785]---> BDD-cost:   23
c ---[30783]---> BDD-cost:   23
c ---[30781]---> BDD-cost:   23
c ---[30779]---> BDD-cost:   23
c ---[30777]---> BDD-cost:   23
c ---[30775]---> BDD-cost:   23
c ---[30773]---> BDD-cost:   23
c ---[30771]---> BDD-cost:   23
c ---[30769]---> BDD-cost:   19
c ---[30767]---> BDD-cost:   19
c ---[30765]---> BDD-cost:   19
c ---[30763]---> BDD-cost:   19
c ---[30761]---> BDD-cost:   19
c ---[30759]---> BDD-cost:   19
c ---[30757]---> BDD-cost:   11
c ---[30755]---> BDD-cost:   11
c ---[30753]---> BDD-cost:   11
c ---[30751]---> BDD-cost:   11
c ---[30749]---> BDD-cost:   11
c ---[30747]---> BDD-cost:   11
c ---[30745]---> BDD-cost:   23
c ---[30743]---> BDD-cost:   23
c ---[30741]---> BDD-cost:   23
c ---[30739]---> BDD-cost:   23
c ---[30737]---> BDD-cost:   23
c ---[30735]---> BDD-cost:   23
c ---[30733]---> BDD-cost:   23
c ---[30731]---> BDD-cost:   23
c ---[30729]---> BDD-cost:   23
c ---[30727]---> BDD-cost:   23
c ---[30725]---> BDD-cost:   23
c ---[30723]---> BDD-cost:   23
c ---[30721]---> BDD-cost:   23
c ---[30719]---> BDD-cost:   23
c ---[30717]---> BDD-cost:   23
c ---[30715]---> BDD-cost:   23
c ---[30713]---> BDD-cost:   23
c ---[30711]---> BDD-cost:   23
c ---[30709]---> BDD-cost:   19
c ---[30707]---> BDD-cost:   19
c ---[30705]---> BDD-cost:   19
c ---[30703]---> BDD-cost:   19
c ---[30701]---> BDD-cost:   19
c ---[30699]---> BDD-cost:   19
c ---[30697]---> BDD-cost:   23
c ---[30695]---> BDD-cost:   23
c ---[30693]---> BDD-cost:   23
c ---[30691]---> BDD-cost:   23
c ---[30689]---> BDD-cost:   23
c ---[30687]---> BDD-cost:   23
c ---[30685]---> BDD-cost:   23
c ---[30683]---> BDD-cost:   23
c ---[30681]---> BDD-cost:   23
c ---[30679]---> BDD-cost:   23
c ---[30677]---> BDD-cost:   23
c ---[30675]---> BDD-cost:   23
c ---[30673]---> BDD-cost:   23
c ---[30671]---> BDD-cost:   23
c ---[30669]---> BDD-cost:   23
c ---[30667]---> BDD-cost:   23
c ---[30665]---> BDD-cost:   23
c ---[30663]---> BDD-cost:   23
c ---[30661]---> BDD-cost:   23
c ---[30659]---> BDD-cost:   23
c ---[30657]---> BDD-cost:   23
c ---[30655]---> BDD-cost:   23
c ---[30653]---> BDD-cost:   23
c ---[30651]---> BDD-cost:   23
c ---[30649]---> BDD-cost:   23
c ---[30647]---> BDD-cost:   23
c ---[30645]---> BDD-cost:   23
c ---[30643]---> BDD-cost:   23
c ---[30641]---> BDD-cost:   23
c ---[30639]---> BDD-cost:   23
c ---[30637]---> BDD-cost:   23
c ---[30635]---> BDD-cost:   23
c ---[30633]---> BDD-cost:   23
c ---[30631]---> BDD-cost:   23
c ---[30629]---> BDD-cost:   23
c ---[30627]---> BDD-cost:   23
c ---[30625]---> BDD-cost:   23
c ---[30623]---> BDD-cost:   23
c ---[30621]---> BDD-cost:   23
c ---[30619]---> BDD-cost:   23
c ---[30617]---> BDD-cost:   23
c ---[30615]---> BDD-cost:   23
c ---[30613]---> BDD-cost:   23
c ---[30611]---> BDD-cost:   23
c ---[30609]---> BDD-cost:   23
c ---[30607]---> BDD-cost:   23
c ---[30605]---> BDD-cost:   23
c ---[30603]---> BDD-cost:   23
c ---[30601]---> BDD-cost:   23
c ---[30599]---> BDD-cost:   23
c ---[30597]---> BDD-cost:   23
c ---[30595]---> BDD-cost:   23
c ---[30593]---> BDD-cost:   23
c ---[30591]---> BDD-cost:   23
c ---[30589]---> BDD-cost:   23
c ---[30587]---> BDD-cost:   23
c ---[30585]---> BDD-cost:   23
c ---[30583]---> BDD-cost:   23
c ---[30581]---> BDD-cost:   23
c ---[30579]---> BDD-cost:   23
c ---[30577]---> BDD-cost:   23
c ---[30575]---> BDD-cost:   23
c ---[30573]---> BDD-cost:   23
c ---[30571]---> BDD-cost:   23
c ---[30569]---> BDD-cost:   23
c ---[30567]---> BDD-cost:   23
c ---[30565]---> BDD-cost:   23
c ---[30563]---> BDD-cost:   23
c ---[30561]---> BDD-cost:   23
c ---[30559]---> BDD-cost:   23
c ---[30557]---> BDD-cost:   23
c ---[30555]---> BDD-cost:   23
c ---[30553]---> BDD-cost:   23
c ---[30551]---> BDD-cost:   23
c ---[30549]---> BDD-cost:   23
c ---[30547]---> BDD-cost:   23
c ---[30545]---> BDD-cost:   23
c ---[30543]---> BDD-cost:   23
c ---[30541]---> BDD-cost:   23
c ---[30539]---> BDD-cost:   23
c ---[30537]---> BDD-cost:   23
c ---[30535]---> BDD-cost:   23
c ---[30533]---> BDD-cost:   23
c ---[30531]---> BDD-cost:   23
c ---[30529]---> BDD-cost:   23
c ---[30527]---> BDD-cost:   23
c ---[30525]---> BDD-cost:   23
c ---[30523]---> BDD-cost:   23
c ---[30521]---> BDD-cost:   23
c ---[30519]---> BDD-cost:   23
c ---[30517]---> BDD-cost:   23
c ---[30515]---> BDD-cost:   23
c ---[30513]---> BDD-cost:   23
c ---[30511]---> BDD-cost:   23
c ---[30509]---> BDD-cost:   23
c ---[30507]---> BDD-cost:   23
c ---[30505]---> BDD-cost:   23
c ---[30503]---> BDD-cost:   23
c ---[30501]---> BDD-cost:   23
c ---[30499]---> BDD-cost:   23
c ---[30497]---> BDD-cost:   23
c ---[30495]---> BDD-cost:   23
c ---[30494]---> BDD-cost:    9
c ---[30493]---> BDD-cost:    9
c ---[30492]---> BDD-cost:    9
c ---[30491]---> BDD-cost:    9
c ---[30490]---> BDD-cost:    9
c ---[30489]---> BDD-cost:    9
c ---[30488]---> BDD-cost:    9
c ---[30487]---> BDD-cost:    9
c ---[30486]---> BDD-cost:    9
c ---[30485]---> BDD-cost:    9
c ---[30484]---> BDD-cost:    9
c ---[30483]---> BDD-cost:    9
c ---[30482]---> BDD-cost:    9
c ---[30481]---> BDD-cost:    9
c ---[30480]---> BDD-cost:    9
c ---[30479]---> BDD-cost:    9
c ---[30478]---> BDD-cost:    9
c ---[30477]---> BDD-cost:    9
c ---[30476]---> BDD-cost:    9
c ---[30475]---> BDD-cost:    9
c ---[30474]---> BDD-cost:    9
c ---[30473]---> BDD-cost:    9
c ---[30472]---> BDD-cost:    9
c ---[30471]---> BDD-cost:    9
c ---[30470]---> BDD-cost:    9
c ---[30469]---> BDD-cost:    9
c ---[30468]---> BDD-cost:    9
c ---[30467]---> BDD-cost:    9
c ---[30466]---> BDD-cost:    9
c ---[30465]---> BDD-cost:    9
c ---[30464]---> BDD-cost:    9
c ---[30463]---> BDD-cost:    9
c ---[30462]---> BDD-cost:    9
c ---[30461]---> BDD-cost:    9
c ---[30460]---> BDD-cost:    9
c ---[30459]---> BDD-cost:    9
c ---[30458]---> BDD-cost:    9
c ---[30457]---> BDD-cost:    9
c ---[30456]---> BDD-cost:    9
c ---[30455]---> BDD-cost:    9
c ---[30454]---> BDD-cost:    9
c ---[30453]---> BDD-cost:    9
c ---[30452]---> BDD-cost:    9
c ---[30451]---> BDD-cost:    9
c ---[30450]---> BDD-cost:    9
c ---[30449]---> BDD-cost:    9
c ---[30448]---> BDD-cost:    9
c ---[30447]---> BDD-cost:    9
c ---[30446]---> BDD-cost:    9
c ---[30445]---> BDD-cost:    9
c ---[30444]---> BDD-cost:    9
c ---[30443]---> BDD-cost:    9
c ---[30442]---> BDD-cost:    9
c ---[30441]---> BDD-cost:    9
c ---[30440]---> BDD-cost:    9
c ---[30439]---> BDD-cost:    9
c ---[30438]---> BDD-cost:    9
c ---[30437]---> BDD-cost:    9
c ---[30436]---> BDD-cost:    9
c ---[30435]---> BDD-cost:    9
c ---[30434]---> BDD-cost:    9
c ---[30433]---> BDD-cost:    9
c ---[30432]---> BDD-cost:    9
c ---[30431]---> BDD-cost:    9
c ---[30430]---> BDD-cost:    9
c ---[30429]---> BDD-cost:    9
c ---[30428]---> BDD-cost:    9
c ---[30427]---> BDD-cost:    9
c ---[30426]---> BDD-cost:    9
c ---[30425]---> BDD-cost:    9
c ---[30424]---> BDD-cost:    9
c ---[30423]---> BDD-cost:    9
c ---[30422]---> BDD-cost:    9
c ---[30421]---> BDD-cost:    9
c ---[30420]---> BDD-cost:    9
c ---[30419]---> BDD-cost:    9
c ---[30418]---> BDD-cost:    9
c ---[30417]---> BDD-cost:    9
c ---[30416]---> BDD-cost:    9
c ---[30415]---> BDD-cost:    9
c ---[30414]---> BDD-cost:    9
c ---[30413]---> BDD-cost:    9
c ---[30412]---> BDD-cost:    9
c ---[30411]---> BDD-cost:    9
c ---[30410]---> BDD-cost:    9
c ---[30409]---> BDD-cost:    9
c ---[30408]---> BDD-cost:    9
c ---[30407]---> BDD-cost:    9
c ---[30406]---> BDD-cost:    9
c ---[30405]---> BDD-cost:    9
c ---[30404]---> BDD-cost:    9
c ---[30403]---> BDD-cost:    9
c ---[30402]---> BDD-cost:    9
c ---[30401]---> BDD-cost:    9
c ---[30400]---> BDD-cost:    9
c ---[30399]---> BDD-cost:    9
c ---[30398]---> BDD-cost:    9
c ---[30397]---> BDD-cost:    9
c ---[30396]---> BDD-cost:    9
c ---[30395]---> BDD-cost:    9
c ---[30394]---> BDD-cost:    9
c ---[30393]---> BDD-cost:    9
c ---[30392]---> BDD-cost:    9
c ---[30391]---> BDD-cost:    9
c ---[30390]---> BDD-cost:    9
c ---[30389]---> BDD-cost:    9
c ---[30388]---> BDD-cost:    9
c ---[30387]---> BDD-cost:    9
c ---[30386]---> BDD-cost:    9
c ---[30385]---> BDD-cost:    9
c ---[30384]---> BDD-cost:    9
c ---[30383]---> BDD-cost:    9
c ---[30382]---> BDD-cost:    9
c ---[30381]---> BDD-cost:    9
c ---[30380]---> BDD-cost:    9
c ---[30379]---> BDD-cost:    9
c ---[30378]---> BDD-cost:    9
c ---[30377]---> BDD-cost:    9
c ---[30376]---> BDD-cost:    9
c ---[30375]---> BDD-cost:    9
c ---[30374]---> BDD-cost:    9
c ---[30373]---> BDD-cost:    9
c ---[30372]---> BDD-cost:    9
c ---[30371]---> BDD-cost:    9
c ---[30370]---> BDD-cost:    9
c ---[30369]---> BDD-cost:    9
c ---[30368]---> BDD-cost:    9
c ---[30367]---> BDD-cost:    9
c ---[30366]---> BDD-cost:    9
c ---[30365]---> BDD-cost:    9
c ---[30364]---> BDD-cost:    9
c ---[30363]---> BDD-cost:    9
c ---[30362]---> BDD-cost:    9
c ---[30361]---> BDD-cost:    9
c ---[30360]---> BDD-cost:    9
c ---[30359]---> BDD-cost:    9
c ---[30358]---> BDD-cost:    9
c ---[30357]---> BDD-cost:    9
c ---[30356]---> BDD-cost:    9
c ---[30355]---> BDD-cost:    9
c ---[30354]---> BDD-cost:    9
c ---[30353]---> BDD-cost:    9
c ---[30352]---> BDD-cost:    9
c ---[30351]---> BDD-cost:    9
c ---[30350]---> BDD-cost:    9
c ---[30349]---> BDD-cost:    9
c ---[30348]---> BDD-cost:    9
c ---[30347]---> BDD-cost:    9
c ---[30346]---> BDD-cost:    9
c ---[30345]---> BDD-cost:    9
c ---[30344]---> BDD-cost:    9
c ---[30343]---> BDD-cost:    9
c ---[30342]---> BDD-cost:    9
c ---[30341]---> BDD-cost:    9
c ---[30340]---> BDD-cost:    9
c ---[30339]---> BDD-cost:    9
c ---[30338]---> BDD-cost:    9
c ---[30337]---> BDD-cost:    9
c ---[30336]---> BDD-cost:    9
c ---[30335]---> BDD-cost:    9
c ---[30334]---> BDD-cost:    9
c ---[30333]---> BDD-cost:    9
c ---[30332]---> BDD-cost:    9
c ---[30331]---> BDD-cost:    9
c ---[30330]---> BDD-cost:    9
c ---[30329]---> BDD-cost:    9
c ---[30328]---> BDD-cost:    9
c ---[30327]---> BDD-cost:    9
c ---[30326]---> BDD-cost:    9
c ---[30325]---> BDD-cost:    9
c ---[30324]---> BDD-cost:    9
c ---[30323]---> BDD-cost:    9
c ---[30322]---> BDD-cost:    9
c ---[30321]---> BDD-cost:    9
c ---[30320]---> BDD-cost:    9
c ---[30319]---> BDD-cost:    9
c ---[30318]---> BDD-cost:    9
c ---[30317]---> BDD-cost:    9
c ---[30316]---> BDD-cost:    9
c ---[30315]---> BDD-cost:    9
c ---[30314]---> BDD-cost:    9
c ---[30313]---> BDD-cost:    9
c ---[30312]---> BDD-cost:    9
c ---[30311]---> BDD-cost:    9
c ---[30310]---> BDD-cost:    9
c ---[30309]---> BDD-cost:    9
c ---[30308]---> BDD-cost:    9
c ---[30307]---> BDD-cost:    9
c ---[30306]---> BDD-cost:    9
c ---[30305]---> BDD-cost:    9
c ---[30304]---> BDD-cost:    9
c ---[30303]---> BDD-cost:    9
c ---[30302]---> BDD-cost:    9
c ---[30301]---> BDD-cost:    9
c ---[30300]---> BDD-cost:    9
c ---[30299]---> BDD-cost:    9
c ---[30298]---> BDD-cost:    9
c ---[30297]---> BDD-cost:    9
c ---[30296]---> BDD-cost:    9
c ---[30295]---> BDD-cost:    9
c ---[30294]---> BDD-cost:    9
c ---[30293]---> BDD-cost:    9
c ---[30292]---> BDD-cost:    9
c ---[30291]---> BDD-cost:    9
c ---[30290]---> BDD-cost:    9
c ---[30289]---> BDD-cost:    9
c ---[30288]---> BDD-cost:    9
c ---[30287]---> BDD-cost:    9
c ---[30286]---> BDD-cost:    9
c ---[30285]---> BDD-cost:    9
c ---[30284]---> BDD-cost:    9
c ---[30283]---> BDD-cost:    9
c ---[30282]---> BDD-cost:    9
c ---[30281]---> BDD-cost:    9
c ---[30280]---> BDD-cost:    9
c ---[30279]---> BDD-cost:    9
c ---[30278]---> BDD-cost:    9
c ---[30277]---> BDD-cost:    9
c ---[30276]---> BDD-cost:    9
c ---[30275]---> BDD-cost:    9
c ---[30274]---> BDD-cost:    9
c ---[30273]---> BDD-cost:    9
c ---[30272]---> BDD-cost:    9
c ---[30271]---> BDD-cost:    9
c ---[30270]---> BDD-cost:    9
c ---[30269]---> BDD-cost:    9
c ---[30268]---> BDD-cost:    9
c ---[30267]---> BDD-cost:    9
c ---[30266]---> BDD-cost:    9
c ---[30265]---> BDD-cost:    9
c ---[30264]---> BDD-cost:    9
c ---[30263]---> BDD-cost:    9
c ---[30262]---> BDD-cost:    9
c ---[30261]---> BDD-cost:    9
c ---[30260]---> BDD-cost:    9
c ---[30259]---> BDD-cost:    9
c ---[30258]---> BDD-cost:    9
c ---[30257]---> BDD-cost:    9
c ---[30256]---> BDD-cost:    9
c ---[30255]---> BDD-cost:    9
c ---[30254]---> BDD-cost:    9
c ---[30253]---> BDD-cost:    9
c ---[30252]---> BDD-cost:    9
c ---[30251]---> BDD-cost:    9
c ---[30250]---> BDD-cost:    9
c ---[30249]---> BDD-cost:    9
c ---[30248]---> BDD-cost:    9
c ---[30247]---> BDD-cost:    9
c ---[30246]---> BDD-cost:    9
c ---[30245]---> BDD-cost:    9
c ---[30244]---> BDD-cost:    9
c ---[30243]---> BDD-cost:    9
c ---[30242]---> BDD-cost:    9
c ---[30241]---> BDD-cost:    9
c ---[30240]---> BDD-cost:    9
c ---[30239]---> BDD-cost:    9
c ---[30238]---> BDD-cost:    9
c ---[30237]---> BDD-cost:    9
c ---[30236]---> BDD-cost:    9
c ---[30235]---> BDD-cost:    9
c ---[30234]---> BDD-cost:    9
c ---[30233]---> BDD-cost:    9
c ---[30232]---> BDD-cost:    9
c ---[30231]---> BDD-cost:    9
c ---[30230]---> BDD-cost:    9
c ---[30229]---> BDD-cost:    9
c ---[30228]---> BDD-cost:    9
c ---[30227]---> BDD-cost:    9
c ---[30226]---> BDD-cost:    9
c ---[30225]---> BDD-cost:    9
c ---[30224]---> BDD-cost:    9
c ---[30223]---> BDD-cost:    9
c ---[30222]---> BDD-cost:    9
c ---[30221]---> BDD-cost:    9
c ---[30220]---> BDD-cost:    9
c ---[30219]---> BDD-cost:    9
c ---[30218]---> BDD-cost:    9
c ---[30217]---> BDD-cost:    9
c ---[30216]---> BDD-cost:    9
c ---[30215]---> BDD-cost:    9
c ---[30214]---> BDD-cost:    9
c ---[30213]---> BDD-cost:    9
c ---[30212]---> BDD-cost:    9
c ---[30211]---> BDD-cost:    9
c ---[30210]---> BDD-cost:    9
c ---[30209]---> BDD-cost:    9
c ---[30208]---> BDD-cost:    9
c ---[30207]---> BDD-cost:    9
c ---[30206]---> BDD-cost:    9
c ---[30205]---> BDD-cost:    9
c ---[30204]---> BDD-cost:    9
c ---[30203]---> BDD-cost:    9
c ---[30202]---> BDD-cost:    9
c ---[30201]---> BDD-cost:    9
c ---[30200]---> BDD-cost:    9
c ---[30199]---> BDD-cost:    9
c ---[30198]---> BDD-cost:    9
c ---[30197]---> BDD-cost:    9
c ---[30196]---> BDD-cost:    9
c ---[30195]---> BDD-cost:    9
c ---[30194]---> BDD-cost:    9
c ---[30193]---> BDD-cost:    9
c ---[30192]---> BDD-cost:    9
c ---[30191]---> BDD-cost:    9
c ---[30190]---> BDD-cost:    9
c ---[30189]---> BDD-cost:    9
c ---[30188]---> BDD-cost:    9
c ---[30187]---> BDD-cost:    9
c ---[30186]---> BDD-cost:    9
c ---[30185]---> BDD-cost:    9
c ---[30184]---> BDD-cost:    9
c ---[30183]---> BDD-cost:    9
c ---[30182]---> BDD-cost:    9
c ---[30181]---> BDD-cost:    9
c ---[30180]---> BDD-cost:    9
c ---[30179]---> BDD-cost:    9
c ---[30178]---> BDD-cost:    9
c ---[30177]---> BDD-cost:    9
c ---[30176]---> BDD-cost:    9
c ---[30175]---> BDD-cost:    9
c ---[30174]---> BDD-cost:    9
c ---[30173]---> BDD-cost:    9
c ---[30172]---> BDD-cost:    9
c ---[30171]---> BDD-cost:    9
c ---[30170]---> BDD-cost:    9
c ---[30169]---> BDD-cost:    9
c ---[30168]---> BDD-cost:    9
c ---[30167]---> BDD-cost:    9
c ---[30166]---> BDD-cost:    9
c ---[30165]---> BDD-cost:    9
c ---[30164]---> BDD-cost:    9
c ---[30163]---> BDD-cost:    9
c ---[30162]---> BDD-cost:    9
c ---[30161]---> BDD-cost:    9
c ---[30160]---> BDD-cost:    9
c ---[30159]---> BDD-cost:    9
c ---[30158]---> BDD-cost:    9
c ---[30157]---> BDD-cost:    9
c ---[30156]---> BDD-cost:    9
c ---[30155]---> BDD-cost:    9
c ---[30154]---> BDD-cost:    9
c ---[30153]---> BDD-cost:    9
c ---[30152]---> BDD-cost:    9
c ---[30151]---> BDD-cost:    9
c ---[30150]---> BDD-cost:    9
c ---[30149]---> BDD-cost:    9
c ---[30148]---> BDD-cost:    9
c ---[30147]---> BDD-cost:    9
c ---[30146]---> BDD-cost:    9
c ---[30145]---> BDD-cost:    9
c ---[30144]---> BDD-cost:    9
c ---[30143]---> BDD-cost:    9
c ---[30142]---> BDD-cost:    9
c ---[30141]---> BDD-cost:    9
c ---[30140]---> BDD-cost:    9
c ---[30139]---> BDD-cost:    9
c ---[30138]---> BDD-cost:    9
c ---[30137]---> BDD-cost:    9
c ---[30136]---> BDD-cost:    9
c ---[30135]---> BDD-cost:    9
c ---[30134]---> BDD-cost:    9
c ---[30133]---> BDD-cost:    9
c ---[30132]---> BDD-cost:    9
c ---[30131]---> BDD-cost:    9
c ---[30130]---> 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 |   82785   226581 |   27595       0        0     nan |  0.000 % |
c |       102 |   82785   226581 |   30354     102     1414    13.9 |  3.956 % |
c |       253 |   82781   226572 |   33389     252     5153    20.4 |  3.960 % |
c |       479 |   82781   226572 |   36728     478    11639    24.3 |  3.960 % |
c |       816 |   82781   226572 |   40401     815    18415    22.6 |  3.960 % |
c |      1322 |   82781   226572 |   44442    1321    34949    26.5 |  3.960 % |
c |      2081 |   82677   226339 |   48886    2057    58093    28.2 |  4.076 % |
c |      3220 |   82677   226339 |   53774    3196   111287    34.8 |  4.076 % |
c |      4929 |   82677   226339 |   59152    4905   186050    37.9 |  4.076 % |
c |      7494 |   82677   226339 |   65067    7470   365268    48.9 |  4.076 % |
c |     11338 |   82677   226339 |   71574   11314   684871    60.5 |  4.076 % |
c |     17104 |   82677   226339 |   78731   17080   936279    54.8 |  4.076 % |
c |     25753 |   82677   226339 |   86604   25729  1532830    59.6 |  4.076 % |
c |     38729 |   82612   226194 |   95265   38697  2370850    61.3 |  4.150 % |
c |     58190 |   82586   226136 |  104791   58155  3732456    64.2 |  4.181 % |
c |     87384 |   82586   226136 |  115271   87349  5542412    63.5 |  4.181 % |
c |    131173 |   82586   226136 |  126798   27597  2915213   105.6 |  4.181 % |
c |    196858 |   82533   226017 |  139478   93275  7132345    76.5 |  4.239 % |
c |    295384 |   82465   225861 |  153425   57831  3447659    59.6 |  4.335 % |
c |    443173 |   82397   225710 |  168768   67140  4725984    70.4 |  4.409 % |
#### 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.89 0.94 0.90 2/54 14701
Raw data (stat): 14701 (runsolver) R 14700 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 479347167 1052672 99 4294967295 134512640 135381576 3221224528 3221219772 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.0002 s]
Raw data (loadavg): 0.90 0.94 0.90 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 3888 0 0 0 987 11 0 0 25 0 1 0 479347167 17473536 3818 4294967295 134512640 134672761 3221224624 3221223748 134566049 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 4266 3818 603 41 0 4225 0
vsize: 17064
[startup+20.0007 s]
Raw data (loadavg): 0.92 0.94 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 4690 0 0 0 1985 12 0 0 25 0 1 0 479347167 20840448 4620 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5088 4620 603 41 0 5047 0
vsize: 20352
[startup+30.0018 s]
Raw data (loadavg): 0.93 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 5563 0 0 0 2983 15 0 0 25 0 1 0 479347167 24592384 5493 4294967295 134512640 134672761 3221224624 3221223792 134561188 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6004 5493 603 41 0 5963 0
vsize: 24016
[startup+40.0019 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 6611 0 0 0 3978 19 0 0 25 0 1 0 479347167 28762112 6541 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7022 6541 603 41 0 6981 0
vsize: 28088
[startup+50.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 7342 0 0 0 4977 20 0 0 25 0 1 0 479347167 31715328 7272 4294967295 134512640 134672761 3221224624 3221223796 134559669 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7743 7272 603 41 0 7702 0
vsize: 30972
[startup+60.0024 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 8026 0 0 0 5975 22 0 0 25 0 1 0 479347167 34783232 7956 4294967295 134512640 134672761 3221224624 3221223728 134559824 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8492 7956 603 41 0 8451 0
vsize: 33968
[startup+70.003 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 8618 0 0 0 6973 24 0 0 25 0 1 0 479347167 37195776 8548 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9081 8548 603 41 0 9040 0
vsize: 36324
[startup+80.0035 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 9190 0 0 0 7972 26 0 0 25 0 1 0 479347167 39477248 9120 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9638 9120 603 41 0 9597 0
vsize: 38552
[startup+90.0036 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 9808 0 0 0 8969 28 0 0 25 0 1 0 479347167 42057728 9738 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10268 9738 603 41 0 10227 0
vsize: 41072
[startup+100.004 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 10388 0 0 0 9968 30 0 0 25 0 1 0 479347167 44359680 10318 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10830 10318 603 41 0 10789 0
vsize: 43320
[startup+110.005 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 10833 0 0 0 10966 32 0 0 25 0 1 0 479347167 46243840 10763 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11290 10763 603 41 0 11249 0
vsize: 45160
[startup+120.006 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 11209 0 0 0 11965 33 0 0 25 0 1 0 479347167 47734784 11139 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11654 11139 603 41 0 11613 0
vsize: 46616
[startup+130.007 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 11631 0 0 0 12964 34 0 0 25 0 1 0 479347167 49491968 11561 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12083 11561 603 41 0 12042 0
vsize: 48332
[startup+140.006 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 11968 0 0 0 13963 36 0 0 25 0 1 0 479347167 50835456 11898 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12411 11898 603 41 0 12370 0
vsize: 49644
[startup+150.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12323 0 0 0 14962 37 0 0 25 0 1 0 479347167 52322304 12253 4294967295 134512640 134672761 3221224624 3221223792 134561218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12774 12253 603 41 0 12733 0
vsize: 51096
[startup+160.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12680 0 0 0 15961 38 0 0 25 0 1 0 479347167 53673984 12610 4294967295 134512640 134672761 3221224624 3221223792 134560864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13104 12610 603 41 0 13063 0
vsize: 52416
[startup+170.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12800 0 0 0 16961 38 0 0 25 0 1 0 479347167 54214656 12730 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12730 603 41 0 13195 0
vsize: 52944
[startup+180.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12801 0 0 0 17961 38 0 0 25 0 1 0 479347167 54214656 12731 4294967295 134512640 134672761 3221224624 3221223792 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12731 603 41 0 13195 0
vsize: 52944
[startup+190.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12802 0 0 0 18961 38 0 0 25 0 1 0 479347167 54214656 12732 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13236 12732 603 41 0 13195 0
vsize: 52944
[startup+200.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12802 0 0 0 19961 39 0 0 25 0 1 0 479347167 54214656 12732 4294967295 134512640 134672761 3221224624 3221223808 134558875 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12732 603 41 0 13195 0
vsize: 52944
[startup+210.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12803 0 0 0 20961 39 0 0 25 0 1 0 479347167 54214656 12733 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12733 603 41 0 13195 0
vsize: 52944
[startup+220.008 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12803 0 0 0 21961 39 0 0 25 0 1 0 479347167 54214656 12733 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12733 603 41 0 13195 0
vsize: 52944
[startup+230.007 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12803 0 0 0 22961 39 0 0 25 0 1 0 479347167 54214656 12733 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12733 603 41 0 13195 0
vsize: 52944
[startup+240.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12803 0 0 0 23961 39 0 0 25 0 1 0 479347167 54214656 12733 4294967295 134512640 134672761 3221224624 3221223792 134560909 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12733 603 41 0 13195 0
vsize: 52944
[startup+250.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12803 0 0 0 24962 39 0 0 25 0 1 0 479347167 54214656 12733 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12733 603 41 0 13195 0
vsize: 52944
[startup+260.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12803 0 0 0 25962 39 0 0 25 0 1 0 479347167 54214656 12733 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12733 603 41 0 13195 0
vsize: 52944
[startup+270.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12803 0 0 0 26962 39 0 0 25 0 1 0 479347167 54214656 12733 4294967295 134512640 134672761 3221224624 3221223792 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12733 603 41 0 13195 0
vsize: 52944
[startup+280.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12803 0 0 0 27962 39 0 0 25 0 1 0 479347167 54214656 12733 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12733 603 41 0 13195 0
vsize: 52944
[startup+290.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12804 0 0 0 28962 39 0 0 25 0 1 0 479347167 54214656 12734 4294967295 134512640 134672761 3221224624 3221223792 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13236 12734 603 41 0 13195 0
vsize: 52944
[startup+300.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12823 0 0 0 29962 39 0 0 25 0 1 0 479347167 54390784 12753 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13279 12753 603 41 0 13238 0
vsize: 53116
[startup+310.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12823 0 0 0 30962 39 0 0 25 0 1 0 479347167 54390784 12753 4294967295 134512640 134672761 3221224624 3221223792 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13279 12753 603 41 0 13238 0
vsize: 53116
[startup+320.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 14701
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12823 0 0 0 31963 39 0 0 25 0 1 0 479347167 54390784 12753 4294967295 134512640 134672761 3221224624 3221223728 134560057 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13279 12753 603 41 0 13238 0
vsize: 53116
[startup+330.009 s]
Raw data (loadavg): 1.07 0.99 0.91 2/54 14754
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 12979 0 0 0 32962 39 0 0 25 0 1 0 479347167 54931456 12909 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13411 12909 603 41 0 13370 0
vsize: 53644
[startup+340.009 s]
Raw data (loadavg): 1.06 0.99 0.91 2/54 14754
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 13279 0 0 0 33961 40 0 0 25 0 1 0 479347167 56266752 13209 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13737 13209 603 41 0 13696 0
vsize: 54948
[startup+350.009 s]
Raw data (loadavg): 1.05 0.99 0.91 2/54 14754
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 13568 0 0 0 34961 41 0 0 25 0 1 0 479347167 57352192 13498 4294967295 134512640 134672761 3221224624 3221223748 134566034 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14002 13498 603 41 0 13961 0
vsize: 56008
[startup+360.009 s]
Raw data (loadavg): 1.04 0.99 0.91 2/54 14754
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 13809 0 0 0 35961 41 0 0 25 0 1 0 479347167 58454016 13739 4294967295 134512640 134672761 3221224624 3221223792 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14271 13740 603 41 0 14230 0
vsize: 57084
[startup+370.009 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 14754
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 14800 0 0 0 36958 44 0 0 25 0 1 0 479347167 62476288 14730 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15253 14730 603 41 0 15212 0
vsize: 61012
[startup+380.008 s]
Raw data (loadavg): 1.03 0.99 0.91 2/54 14754
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 15759 0 0 0 37955 48 0 0 25 0 1 0 479347167 66895872 15689 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16332 15689 603 41 0 16291 0
vsize: 65328
[startup+390.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14754
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16387 0 0 0 38953 49 0 0 25 0 1 0 479347167 69464064 16317 4294967295 134512640 134672761 3221224624 3221223728 134555126 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16317 603 41 0 16918 0
vsize: 67836
[startup+400.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 39954 49 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+410.009 s]
Raw data (loadavg): 1.02 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 40954 49 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223728 134560218 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+420.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 41954 49 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+430.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 42954 49 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223808 134558851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+440.009 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 43954 49 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+450.01 s]
Raw data (loadavg): 1.01 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 44954 49 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+460.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 45953 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+470.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 46954 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+480.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 47954 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134561375 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+490.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 48954 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+500.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 49954 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+510.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 50954 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+520.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 51954 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+530.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 52955 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+540.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 53955 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+550.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 54955 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+560.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 55955 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+570.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 56955 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+580.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 57955 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+590.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16409 0 0 0 58956 50 0 0 25 0 1 0 479347167 69464064 16339 4294967295 134512640 134672761 3221224624 3221223792 134560999 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16339 603 41 0 16918 0
vsize: 67836
[startup+600.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16410 0 0 0 59956 50 0 0 25 0 1 0 479347167 69464064 16340 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16959 16340 603 41 0 16918 0
vsize: 67836
[startup+610.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16543 0 0 0 60956 50 0 0 25 0 1 0 479347167 70012928 16473 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17093 16473 603 41 0 17052 0
vsize: 68372
[startup+620.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16781 0 0 0 61955 51 0 0 25 0 1 0 479347167 71102464 16711 4294967295 134512640 134672761 3221224624 3221223728 134560405 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17359 16711 603 41 0 17318 0
vsize: 69436
[startup+630.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 62955 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223728 134554642 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+640.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 63955 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+650.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 64955 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+660.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 65956 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+670.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14756
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 66956 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223728 134560031 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+680.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 67956 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+690.009 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 68956 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+700.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 69956 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+710.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 70956 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223824 134557822 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+720.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 71956 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+730.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 72956 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+740.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 73957 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+750.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 74957 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223824 134557911 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+760.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 75957 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+770.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 76957 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+780.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 77957 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+790.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 78957 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560903 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+800.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 79958 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+810.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16841 0 0 0 80958 51 0 0 25 0 1 0 479347167 71237632 16771 4294967295 134512640 134672761 3221224624 3221223808 134559166 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17392 16771 603 41 0 17351 0
vsize: 69568
[startup+820.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16851 0 0 0 81958 51 0 0 25 0 1 0 479347167 71430144 16781 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17439 16781 603 41 0 17398 0
vsize: 69756
[startup+830.011 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16855 0 0 0 82958 51 0 0 25 0 1 0 479347167 71430144 16785 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17439 16785 603 41 0 17398 0
vsize: 69756
[startup+840.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16855 0 0 0 83958 51 0 0 25 0 1 0 479347167 71430144 16785 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17439 16785 603 41 0 17398 0
vsize: 69756
[startup+850.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16879 0 0 0 84959 51 0 0 25 0 1 0 479347167 71430144 16809 4294967295 134512640 134672761 3221224624 3221223728 134554988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17439 16809 603 41 0 17398 0
vsize: 69756
[startup+860.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16882 0 0 0 85959 51 0 0 25 0 1 0 479347167 71430144 16812 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17439 16812 603 41 0 17398 0
vsize: 69756
[startup+870.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16886 0 0 0 86959 51 0 0 25 0 1 0 479347167 71626752 16816 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17487 16816 603 41 0 17446 0
vsize: 69948
[startup+880.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 16922 0 0 0 87959 51 0 0 25 0 1 0 479347167 71757824 16852 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17519 16852 603 41 0 17478 0
vsize: 70076
[startup+890.012 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 17139 0 0 0 88958 52 0 0 25 0 1 0 479347167 72568832 17069 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17717 17069 603 41 0 17676 0
vsize: 70868
[startup+900.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 17350 0 0 0 89958 53 0 0 25 0 1 0 479347167 73498624 17280 4294967295 134512640 134672761 3221224624 3221223792 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17944 17280 603 41 0 17903 0
vsize: 71776
[startup+910.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 17571 0 0 0 90957 54 0 0 25 0 1 0 479347167 74440704 17501 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18174 17501 603 41 0 18133 0
vsize: 72696
[startup+920.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 17792 0 0 0 91956 55 0 0 25 0 1 0 479347167 75276288 17722 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18378 17722 603 41 0 18337 0
vsize: 73512
[startup+930.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18001 0 0 0 92955 56 0 0 25 0 1 0 479347167 76275712 17931 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18622 17931 603 41 0 18581 0
vsize: 74488
[startup+940.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18207 0 0 0 93954 57 0 0 25 0 1 0 479347167 77086720 18137 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18820 18137 603 41 0 18779 0
vsize: 75280
[startup+950.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18407 0 0 0 94954 57 0 0 25 0 1 0 479347167 77885440 18337 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19015 18337 603 41 0 18974 0
vsize: 76060
[startup+960.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 95954 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223728 134554636 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+970.015 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 96954 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223760 134560729 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+980.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 97954 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+990.014 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 98954 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1000.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 99955 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1010.01 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 100955 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223728 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1020.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 101955 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1030.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 102955 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1040.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 103955 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1050.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 104956 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1060.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 105956 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223760 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1070.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 106956 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1080.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 107956 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223808 134559616 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1090.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 108956 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1100.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 109956 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560892 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1110.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 110957 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560858 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1120.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 111957 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223728 134560514 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1130.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18512 0 0 0 112957 58 0 0 25 0 1 0 479347167 78286848 18442 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19113 18442 603 41 0 19072 0
vsize: 76452
[startup+1140.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18534 0 0 0 113957 58 0 0 25 0 1 0 479347167 78458880 18464 4294967295 134512640 134672761 3221224624 3221223776 134565086 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18464 603 41 0 19114 0
vsize: 76620
[startup+1150.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18535 0 0 0 114957 58 0 0 25 0 1 0 479347167 78458880 18465 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18465 603 41 0 19114 0
vsize: 76620
[startup+1160.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18537 0 0 0 115958 58 0 0 25 0 1 0 479347167 78458880 18467 4294967295 134512640 134672761 3221224624 3221223792 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18467 603 41 0 19114 0
vsize: 76620
[startup+1170.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18538 0 0 0 116958 58 0 0 25 0 1 0 479347167 78458880 18468 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18468 603 41 0 19114 0
vsize: 76620
[startup+1180.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18539 0 0 0 117958 58 0 0 25 0 1 0 479347167 78458880 18469 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18469 603 41 0 19114 0
vsize: 76620
[startup+1190.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18546 0 0 0 118958 58 0 0 25 0 1 0 479347167 78458880 18476 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18476 603 41 0 19114 0
vsize: 76620
[startup+1200.02 s]
Raw data (loadavg): 1.00 0.99 0.91 2/54 14758
Raw data (stat): 14701 (minisat+) R 14700 11931 11930 0 -1 0 18548 0 0 0 119958 58 0 0 25 0 1 0 479347167 78458880 18478 4294967295 134512640 134672761 3221224624 3221223792 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19155 18478 603 41 0 19114 0
vsize: 76620
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.06 s]
Raw data (loadavg): 1.00 0.99 0.91 1/54 14758
Raw data (stat): 14701 (minisat+) Z 14700 11931 11930 0 -1 12 18550 0 0 0 119958 61 0 0 25 0 1 0 479347167 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.21
CPU user time (s): 1199.59
CPU system time (s): 0.615906
CPU usage (%): 100.013
Max. virtual memory (Kb): 76620
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####