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 5660

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        906344 kB
Buffers:         35724 kB
Cached:          72924 kB
SwapCached:         16 kB
Active:          62336 kB
Inactive:        49176 kB
HighTotal:      131008 kB
HighFree:        54152 kB
LowTotal:       903652 kB
LowFree:        852192 kB
SwapTotal:     2097136 kB
SwapFree:      2097120 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6920 kB
Slab:            11332 kB
Committed_AS:    63484 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1364 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 01:41:29 (client local time) WITH STATUS 0 IN 1200.26 SECONDS
stats: 4124 7 1200.26 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 =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   82785   226581 |   24835       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/24834          
c   -- var.elim.:  2000/24834          
c   -- var.elim.:  3000/24834          
c   -- var.elim.:  4000/24834          
c   -- var.elim.:  5000/24834          
c   -- var.elim.:  6000/24834          
c   -- var.elim.:  7000/24834          
c   -- var.elim.:  8000/24834          
c   -- var.elim.:  9000/24834          
c   -- var.elim.:  10000/24834          
c   -- var.elim.:  11000/24834          
c   -- var.elim.:  12000/24834          
c   -- var.elim.:  13000/24834          
c   -- var.elim.:  14000/24834          
c   -- var.elim.:  15000/24834          
c   -- var.elim.:  16000/24834          
c   -- var.elim.:  17000/24834          
c   -- var.elim.:  18000/24834          
c   -- var.elim.:  19000/24834          
c   -- var.elim.:  20000/24834          
c   -- var.elim.:  21000/24834          
c   -- var.elim.:  22000/24834          
c   -- var.elim.:  23000/24834          
c   -- var.elim.:  24000/24834          
c   -- var.elim.:  24834/24834          
c   -- var.elim.:  1000/10993          
c   -- var.elim.:  2000/10993          
c   -- var.elim.:  3000/10993          
c   -- var.elim.:  4000/10993          
c   -- var.elim.:  5000/10993          
c   -- var.elim.:  6000/10993          
c   -- var.elim.:  7000/10993          
c   -- var.elim.:  8000/10993          
c   -- var.elim.:  9000/10993          
c   -- var.elim.:  10000/10993          
c   -- var.elim.:  10993/10993          
c   -- var.elim.:  232/232          
c   -- subsuming                       
c   -- var.elim.:  1000/9175          
c   -- var.elim.:  2000/9175          
c   -- var.elim.:  3000/9175          
c   -- var.elim.:  4000/9175          
c   -- var.elim.:  5000/9175          
c   -- var.elim.:  6000/9175          
c   -- var.elim.:  7000/9175          
c   -- var.elim.:  8000/9175          
c   -- var.elim.:  9000/9175          
c   -- var.elim.:  9175/9175          
c   -- var.elim.:  1000/9023          
c   -- var.elim.:  2000/9023          
c   -- var.elim.:  3000/9023          
c   -- var.elim.:  4000/9023          
c   -- var.elim.:  5000/9023          
c   -- var.elim.:  6000/9023          
c   -- var.elim.:  7000/9023          
c   -- var.elim.:  8000/9023          
c   -- var.elim.:  9000/9023          
c   -- var.elim.:  9023/9023          
c   -- var.elim.:  124/124          
c   -- subsuming                       
c   -- var.elim.:  1000/6439          
c   -- var.elim.:  2000/6439          
c #### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.88 0.94 0.90 2/54 30110
Raw data (stat): 30110 (runsolver) R 30109 25285 25284 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 422365970 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 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.0013 s]
Raw data (loadavg): 0.90 0.94 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 5561 0 0 0 981 17 0 0 25 0 1 0 422365970 22515712 4746 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 5497 4746 603 41 0 5456 0
vsize: 21988
[startup+20.0016 s]
Raw data (loadavg): 0.91 0.94 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 6680 0 0 0 1977 21 0 0 25 0 1 0 422365970 27099136 5865 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6616 5865 603 41 0 6575 0
vsize: 26464
[startup+30.0024 s]
Raw data (loadavg): 0.93 0.94 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 7572 0 0 0 2975 23 0 0 25 0 1 0 422365970 30806016 6757 4294967295 134512640 134672761 3221224560 3221223744 134615632 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7521 6757 603 41 0 7480 0
vsize: 30084
[startup+40.0025 s]
Raw data (loadavg): 0.94 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 8219 0 0 0 3974 24 0 0 25 0 1 0 422365970 33484800 7404 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8175 7404 603 41 0 8134 0
vsize: 32700
[startup+50.0021 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 8770 0 0 0 4973 26 0 0 25 0 1 0 422365970 35758080 7955 4294967295 134512640 134672761 3221224560 3221223744 134615749 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8730 7955 603 41 0 8689 0
vsize: 34920
[startup+60.0019 s]
Raw data (loadavg): 0.95 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 9255 0 0 0 5971 27 0 0 25 0 1 0 422365970 37740544 8440 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9214 8440 603 41 0 9173 0
vsize: 36856
[startup+70.002 s]
Raw data (loadavg): 0.96 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 9804 0 0 0 6969 30 0 0 25 0 1 0 422365970 40009728 8989 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9768 8989 603 41 0 9727 0
vsize: 39072
[startup+80.0026 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 10523 0 0 0 7968 31 0 0 25 0 1 0 422365970 43094016 9708 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10521 9708 603 41 0 10480 0
vsize: 42084
[startup+90.0024 s]
Raw data (loadavg): 0.97 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 11221 0 0 0 8966 33 0 0 25 0 1 0 422365970 46018560 10406 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11235 10406 603 41 0 11194 0
vsize: 44940
[startup+100.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 11810 0 0 0 9964 36 0 0 25 0 1 0 422365970 48402432 10995 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11817 10995 603 41 0 11776 0
vsize: 47268
[startup+110.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 12855 0 0 0 10961 39 0 0 25 0 1 0 422365970 52654080 12040 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12855 12040 603 41 0 12814 0
vsize: 51420
[startup+120.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 13790 0 0 0 11958 41 0 0 25 0 1 0 422365970 56352768 12975 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13758 12975 603 41 0 13717 0
vsize: 55032
[startup+130.003 s]
Raw data (loadavg): 0.98 0.95 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 14598 0 0 0 12957 43 0 0 25 0 1 0 422365970 59670528 13783 4294967295 134512640 134672761 3221224560 3221223600 134612885 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14568 13783 603 41 0 14527 0
vsize: 58272
[startup+140.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 15520 0 0 0 13954 46 0 0 25 0 1 0 422365970 63508480 14705 4294967295 134512640 134672761 3221224560 3221223600 134612653 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15505 14705 603 41 0 15464 0
vsize: 62020
[startup+150.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 16285 0 0 0 14951 49 0 0 25 0 1 0 422365970 66551808 15470 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16248 15470 603 41 0 16207 0
vsize: 64992
[startup+160.003 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17262 0 0 0 15949 51 0 0 25 0 1 0 422365970 70598656 16447 4294967295 134512640 134672761 3221224560 3221223616 134644275 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17236 16447 603 41 0 17195 0
vsize: 68944
[startup+170.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17264 0 0 0 16949 51 0 0 25 0 1 0 422365970 70074368 16324 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16324 603 41 0 17067 0
vsize: 68432
[startup+180.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17264 0 0 0 17949 51 0 0 25 0 1 0 422365970 70074368 16324 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16324 603 41 0 17067 0
vsize: 68432
[startup+190.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17264 0 0 0 18949 51 0 0 25 0 1 0 422365970 70074368 16324 4294967295 134512640 134672761 3221224560 3221223744 134615767 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16324 603 41 0 17067 0
vsize: 68432
[startup+200.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17264 0 0 0 19950 51 0 0 25 0 1 0 422365970 70074368 16324 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16324 603 41 0 17067 0
vsize: 68432
[startup+210.001 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17264 0 0 0 20950 51 0 0 25 0 1 0 422365970 70074368 16324 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16324 603 41 0 17067 0
vsize: 68432
[startup+220.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17264 0 0 0 21950 51 0 0 25 0 1 0 422365970 70074368 16324 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16324 603 41 0 17067 0
vsize: 68432
[startup+230.002 s]
Raw data (loadavg): 0.99 0.96 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17266 0 0 0 22950 51 0 0 25 0 1 0 422365970 70074368 16326 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16326 603 41 0 17067 0
vsize: 68432
[startup+240.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17266 0 0 0 23950 51 0 0 25 0 1 0 422365970 70074368 16326 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16326 603 41 0 17067 0
vsize: 68432
[startup+250.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17266 0 0 0 24950 51 0 0 25 0 1 0 422365970 70074368 16326 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16326 603 41 0 17067 0
vsize: 68432
[startup+260.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17266 0 0 0 25951 51 0 0 25 0 1 0 422365970 70074368 16326 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16326 603 41 0 17067 0
vsize: 68432
[startup+270.002 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17266 0 0 0 26951 51 0 0 25 0 1 0 422365970 70074368 16326 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16326 603 41 0 17067 0
vsize: 68432
[startup+280.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17266 0 0 0 27951 51 0 0 25 0 1 0 422365970 70074368 16326 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16326 603 41 0 17067 0
vsize: 68432
[startup+290.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17266 0 0 0 28951 51 0 0 25 0 1 0 422365970 70074368 16326 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16326 603 41 0 17067 0
vsize: 68432
[startup+300.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17266 0 0 0 29951 51 0 0 25 0 1 0 422365970 70074368 16326 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17108 16326 603 41 0 17067 0
vsize: 68432
[startup+310.003 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 17640 0 0 0 30950 53 0 0 25 0 1 0 422365970 71667712 16700 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17497 16700 603 41 0 17456 0
vsize: 69988
[startup+320.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 18066 0 0 0 31949 55 0 0 25 0 1 0 422365970 73379840 17126 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 17915 17126 603 41 0 17874 0
vsize: 71660
[startup+330.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 18518 0 0 0 32948 56 0 0 25 0 1 0 422365970 75366400 17578 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18400 17578 603 41 0 18359 0
vsize: 73600
[startup+340.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 18945 0 0 0 33947 57 0 0 25 0 1 0 422365970 77107200 18005 4294967295 134512640 134672761 3221224560 3221223744 134615652 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 18825 18005 603 41 0 18784 0
vsize: 75300
[startup+350.004 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 19376 0 0 0 34945 58 0 0 25 0 1 0 422365970 78827520 18436 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19245 18436 603 41 0 19204 0
vsize: 76980
[startup+360.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 19803 0 0 0 35945 59 0 0 25 0 1 0 422365970 80551936 18863 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 19666 18863 603 41 0 19625 0
vsize: 78664
[startup+370.005 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 20216 0 0 0 36944 60 0 0 25 0 1 0 422365970 82800640 19276 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20215 19276 603 41 0 20174 0
vsize: 80860
[startup+380.006 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 20569 0 0 0 37943 62 0 0 25 0 1 0 422365970 84254720 19629 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20570 19629 603 41 0 20529 0
vsize: 82280
[startup+390.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 20906 0 0 0 38941 63 0 0 25 0 1 0 422365970 85704704 19966 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 20924 19966 603 41 0 20883 0
vsize: 83696
[startup+400.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 21257 0 0 0 39941 64 0 0 25 0 1 0 422365970 87154688 20317 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21278 20317 603 41 0 21237 0
vsize: 85112
[startup+410.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 21588 0 0 0 40940 65 0 0 25 0 1 0 422365970 88539136 20648 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21616 20648 603 41 0 21575 0
vsize: 86464
[startup+420.007 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 21892 0 0 0 41939 66 0 0 25 0 1 0 422365970 89739264 20952 4294967295 134512640 134672761 3221224560 3221223728 134615864 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 21909 20952 603 41 0 21868 0
vsize: 87636
[startup+430.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22237 0 0 0 42938 67 0 0 25 0 1 0 422365970 91197440 21297 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22265 21297 603 41 0 22224 0
vsize: 89060
[startup+440.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22503 0 0 0 43937 69 0 0 25 0 1 0 422365970 92262400 21563 4294967295 134512640 134672761 3221224560 3221223744 134615773 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22525 21563 603 41 0 22484 0
vsize: 90100
[startup+450.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22816 0 0 0 44936 70 0 0 25 0 1 0 422365970 93302784 21727 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21727 603 41 0 22738 0
vsize: 91116
[startup+460.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22816 0 0 0 45936 70 0 0 25 0 1 0 422365970 93302784 21727 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21727 603 41 0 22738 0
vsize: 91116
[startup+470.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22816 0 0 0 46936 70 0 0 25 0 1 0 422365970 93302784 21727 4294967295 134512640 134672761 3221224560 3221223760 134610707 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21727 603 41 0 22738 0
vsize: 91116
[startup+480.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22817 0 0 0 47937 70 0 0 25 0 1 0 422365970 93302784 21728 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21728 603 41 0 22738 0
vsize: 91116
[startup+490.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22817 0 0 0 48937 70 0 0 25 0 1 0 422365970 93302784 21728 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21728 603 41 0 22738 0
vsize: 91116
[startup+500.008 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22817 0 0 0 49937 70 0 0 25 0 1 0 422365970 93302784 21728 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21728 603 41 0 22738 0
vsize: 91116
[startup+510.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22817 0 0 0 50937 70 0 0 25 0 1 0 422365970 93302784 21728 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21728 603 41 0 22738 0
vsize: 91116
[startup+520.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22817 0 0 0 51937 70 0 0 25 0 1 0 422365970 93302784 21728 4294967295 134512640 134672761 3221224560 3221223552 134565092 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21728 603 41 0 22738 0
vsize: 91116
[startup+530.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22817 0 0 0 52937 70 0 0 25 0 1 0 422365970 93302784 21728 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21728 603 41 0 22738 0
vsize: 91116
[startup+540.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22818 0 0 0 53938 70 0 0 25 0 1 0 422365970 93302784 21729 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21729 603 41 0 22738 0
vsize: 91116
[startup+550.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22818 0 0 0 54938 70 0 0 25 0 1 0 422365970 93302784 21729 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21729 603 41 0 22738 0
vsize: 91116
[startup+560.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22818 0 0 0 55938 70 0 0 25 0 1 0 422365970 93302784 21729 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21729 603 41 0 22738 0
vsize: 91116
[startup+570.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22818 0 0 0 56938 70 0 0 25 0 1 0 422365970 93302784 21729 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21729 603 41 0 22738 0
vsize: 91116
[startup+580.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22818 0 0 0 57938 70 0 0 25 0 1 0 422365970 93302784 21729 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21729 603 41 0 22738 0
vsize: 91116
[startup+590.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22818 0 0 0 58938 70 0 0 25 0 1 0 422365970 93302784 21729 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21729 603 41 0 22738 0
vsize: 91116
[startup+600.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22818 0 0 0 59939 70 0 0 25 0 1 0 422365970 93302784 21729 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21729 603 41 0 22738 0
vsize: 91116
[startup+610.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22818 0 0 0 60939 70 0 0 25 0 1 0 422365970 93302784 21729 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21729 603 41 0 22738 0
vsize: 91116
[startup+620.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22819 0 0 0 61939 70 0 0 25 0 1 0 422365970 93302784 21730 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21730 603 41 0 22738 0
vsize: 91116
[startup+630.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22819 0 0 0 62939 70 0 0 25 0 1 0 422365970 93302784 21730 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21730 603 41 0 22738 0
vsize: 91116
[startup+640.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22819 0 0 0 63939 70 0 0 25 0 1 0 422365970 93302784 21730 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21730 603 41 0 22738 0
vsize: 91116
[startup+650.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22820 0 0 0 64939 70 0 0 25 0 1 0 422365970 93302784 21731 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21731 603 41 0 22738 0
vsize: 91116
[startup+660.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22820 0 0 0 65939 70 0 0 25 0 1 0 422365970 93302784 21731 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21731 603 41 0 22738 0
vsize: 91116
[startup+670.009 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 66940 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+680.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 67940 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+690.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 68940 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+700.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 69940 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+710.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 70940 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+720.01 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 71941 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+730.011 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 72941 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+740.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 73941 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+750.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 22821 0 0 0 74941 70 0 0 25 0 1 0 422365970 93302784 21732 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22779 21732 603 41 0 22738 0
vsize: 91116
[startup+760.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 23049 0 0 0 75941 71 0 0 25 0 1 0 422365970 94359552 21960 4294967295 134512640 134672761 3221224560 3221223744 134615571 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23037 21960 603 41 0 22996 0
vsize: 92148
[startup+770.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 23326 0 0 0 76940 72 0 0 25 0 1 0 422365970 95424512 22237 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23297 22237 603 41 0 23256 0
vsize: 93188
[startup+780.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 23609 0 0 0 77939 73 0 0 25 0 1 0 422365970 96628736 22520 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23591 22520 603 41 0 23550 0
vsize: 94364
[startup+790.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 23930 0 0 0 78938 74 0 0 25 0 1 0 422365970 97964032 22841 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 23917 22841 603 41 0 23876 0
vsize: 95668
[startup+800.012 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 24147 0 0 0 79938 74 0 0 25 0 1 0 422365970 98910208 23058 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24148 23058 603 41 0 24107 0
vsize: 96592
[startup+810.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 24412 0 0 0 80938 74 0 0 25 0 1 0 422365970 99962880 23323 4294967295 134512640 134672761 3221224560 3221223744 134615720 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24405 23323 603 41 0 24364 0
vsize: 97620
[startup+820.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 24676 0 0 0 81937 75 0 0 25 0 1 0 422365970 101023744 23587 4294967295 134512640 134672761 3221224560 3221223744 134615601 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24664 23587 603 41 0 24623 0
vsize: 98656
[startup+830.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 24913 0 0 0 82937 76 0 0 25 0 1 0 422365970 102084608 23824 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 24923 23824 603 41 0 24882 0
vsize: 99692
[startup+840.013 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 25118 0 0 0 83936 76 0 0 25 0 1 0 422365970 102875136 24029 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25116 24029 603 41 0 25075 0
vsize: 100464
[startup+850.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 25320 0 0 0 84935 77 0 0 25 0 1 0 422365970 103706624 24231 4294967295 134512640 134672761 3221224560 3221223664 134604546 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25319 24231 603 41 0 25278 0
vsize: 101276
[startup+860.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 25518 0 0 0 85935 78 0 0 25 0 1 0 422365970 104660992 24429 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25552 24429 603 41 0 25511 0
vsize: 102208
[startup+870.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 25757 0 0 0 86935 78 0 0 25 0 1 0 422365970 105578496 24668 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25776 24668 603 41 0 25735 0
vsize: 103104
[startup+880.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 25956 0 0 0 87934 79 0 0 25 0 1 0 422365970 106397696 24867 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 25976 24867 603 41 0 25935 0
vsize: 103904
[startup+890.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 26167 0 0 0 88934 80 0 0 25 0 1 0 422365970 107204608 25078 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26173 25078 603 41 0 26132 0
vsize: 104692
[startup+900.014 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 26359 0 0 0 89933 80 0 0 25 0 1 0 422365970 108068864 25270 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26384 25270 603 41 0 26343 0
vsize: 105536
[startup+910.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 26547 0 0 0 90933 81 0 0 25 0 1 0 422365970 108863488 25458 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26578 25458 603 41 0 26537 0
vsize: 106312
[startup+920.015 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 26721 0 0 0 91933 81 0 0 25 0 1 0 422365970 109522944 25632 4294967295 134512640 134672761 3221224560 3221223760 134610686 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26739 25632 603 41 0 26698 0
vsize: 106956
[startup+930.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 26900 0 0 0 92932 82 0 0 25 0 1 0 422365970 110325760 25811 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 26935 25811 603 41 0 26894 0
vsize: 107740
[startup+940.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27065 0 0 0 93932 82 0 0 25 0 1 0 422365970 111013888 25976 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27103 25976 603 41 0 27062 0
vsize: 108412
[startup+950.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27178 0 0 0 94932 83 0 0 25 0 1 0 422365970 111419392 26089 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27202 26089 603 41 0 27161 0
vsize: 108808
[startup+960.016 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27295 0 0 0 95932 83 0 0 25 0 1 0 422365970 112005120 26206 4294967295 134512640 134672761 3221224560 3221223744 134615758 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27345 26206 603 41 0 27304 0
vsize: 109380
[startup+970.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27472 0 0 0 96932 83 0 0 25 0 1 0 422365970 112689152 26383 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27512 26383 603 41 0 27471 0
vsize: 110048
[startup+980.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27674 0 0 0 97932 84 0 0 25 0 1 0 422365970 113479680 26585 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27705 26585 603 41 0 27664 0
vsize: 110820
[startup+990.017 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27952 0 0 0 98931 84 0 0 25 0 1 0 422365970 114814976 26831 4294967295 134512640 134672761 3221224560 3221223656 134616350 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 28031 26831 603 41 0 27990 0
vsize: 112124
[startup+1000.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27952 0 0 0 99931 84 0 0 25 0 1 0 422365970 113766400 26669 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26669 603 41 0 27734 0
vsize: 111100
[startup+1010.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27952 0 0 0 100932 84 0 0 25 0 1 0 422365970 113766400 26669 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26669 603 41 0 27734 0
vsize: 111100
[startup+1020.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27952 0 0 0 101932 84 0 0 25 0 1 0 422365970 113766400 26669 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26669 603 41 0 27734 0
vsize: 111100
[startup+1030.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27952 0 0 0 102932 84 0 0 25 0 1 0 422365970 113766400 26669 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26669 603 41 0 27734 0
vsize: 111100
[startup+1040.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27952 0 0 0 103932 84 0 0 25 0 1 0 422365970 113766400 26669 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26669 603 41 0 27734 0
vsize: 111100
[startup+1050.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 104932 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1060.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 105932 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1070.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 106933 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1080.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 107933 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1090.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 108933 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1100.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 109933 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1110.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 110933 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1120.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 111933 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1130.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 112934 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1140.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 113934 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615919 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1150.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 114934 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223716 134614480 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1160.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 115934 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1170.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 116934 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1180.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 117935 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615739 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1190.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 118935 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
[startup+1200.02 s]
Raw data (loadavg): 0.99 0.97 0.91 2/54 30110
Raw data (stat): 30110 (minisat+) R 30109 25285 25284 0 -1 0 27953 0 0 0 119935 84 0 0 25 0 1 0 422365970 113766400 26670 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 27775 26670 603 41 0 27734 0
vsize: 111100
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.07 s]
Raw data (loadavg): 0.99 0.97 0.91 1/54 30110
Raw data (stat): 30110 (minisat+) Z 30109 25285 25284 0 -1 12 27953 0 0 0 119935 89 0 0 25 0 1 0 422365970 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.07
CPU time (s): 1200.26
CPU user time (s): 1199.36
CPU system time (s): 0.899863
CPU usage (%): 100.015
Max. virtual memory (Kb): 112124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####