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 6461

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc2 THE 2005-04-14 05:05:04 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=4876 boxname=wulflinc2 idbench=364 idsolver=13 numberseed=0
MD5SUM SOLVER: 
MD5SUM BENCH:  a788dbf2f72289ace41b812e06d88575  /oldhome/oroussel/tmp/wulflinc2/normalized-ppp:1-9,16-19.opb
REAL COMMAND:  minisat+ -w /oldhome/oroussel/tmp/wulflinc2/normalized-ppp:1-9,16-19.opb /oldhome/oroussel/tmp/wulflinc2/normalized-ppp:1-9,16-19.opb
IDLAUNCH: 4876
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
cpu MHz		: 451.191
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.191
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:        886528 kB
Buffers:         35672 kB
Cached:          91416 kB
SwapCached:          4 kB
Active:          59672 kB
Inactive:        70328 kB
HighTotal:      131008 kB
HighFree:        35812 kB
LowTotal:       903652 kB
LowFree:        850716 kB
SwapTotal:     2097136 kB
SwapFree:      2097132 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6916 kB
Slab:            12532 kB
Committed_AS:    71676 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-04-14 05:25:06 (client local time) WITH STATUS 0 IN 1200.2 SECONDS
stats: 4876 7 1200.2 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30921 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ............................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30920]---> BDD-cost:   87
c ---[30919]---> BDD-cost:   87
c ---[30918]---> BDD-cost:   87
c ---[30917]---> BDD-cost:   87
c ---[30916]---> BDD-cost:   87
c ---[30915]---> BDD-cost:   87
c ---[30914]---> BDD-cost:   87
c ---[30913]---> BDD-cost:   87
c ---[30912]---> BDD-cost:   87
c ---[30911]---> BDD-cost:   87
c ---[30910]---> BDD-cost:   87
c ---[30909]---> BDD-cost:   87
c ---[30908]---> BDD-cost:   87
c ---[30907]---> BDD-cost:   87
c ---[30906]---> BDD-cost:   87
c ---[30905]---> BDD-cost:   87
c ---[30904]---> BDD-cost:   87
c ---[30903]---> BDD-cost:   87
c ---[30902]---> BDD-cost:   58
c ---[30901]---> BDD-cost:   58
c ---[30900]---> BDD-cost:   58
c ---[30899]---> BDD-cost:   58
c ---[30898]---> BDD-cost:   58
c ---[30897]---> BDD-cost:   58
c ---[30896]---> BDD-cost:  113
c ---[30895]---> BDD-cost:  113
c ---[30894]---> BDD-cost:  113
c ---[30893]---> BDD-cost:  113
c ---[30892]---> BDD-cost:  113
c ---[30891]---> BDD-cost:  113
c ---[30890]---> BDD-cost:  124
c ---[30889]---> BDD-cost:  124
c ---[30888]---> BDD-cost:  124
c ---[30887]---> BDD-cost:  124
c ---[30886]---> BDD-cost:  124
c ---[30885]---> BDD-cost:  124
c ---[30884]---> BDD-cost:  113
c ---[30883]---> BDD-cost:  113
c ---[30882]---> BDD-cost:  113
c ---[30881]---> BDD-cost:  113
c ---[30880]---> BDD-cost:  113
c ---[30879]---> BDD-cost:  113
c ---[30878]---> BDD-cost:  113
c ---[30877]---> BDD-cost:  113
c ---[30876]---> BDD-cost:  113
c ---[30875]---> BDD-cost:  113
c ---[30874]---> BDD-cost:  113
c ---[30873]---> BDD-cost:  113
c ---[30872]---> BDD-cost:  113
c ---[30871]---> BDD-cost:  113
c ---[30870]---> BDD-cost:  113
c ---[30869]---> BDD-cost:  113
c ---[30868]---> BDD-cost:  113
c ---[30867]---> BDD-cost:  113
c ---[30866]---> Sorter-cost:  521     Base: 2 2
c ---[30865]---> Sorter-cost:  521     Base: 2 2
c ---[30864]---> Sorter-cost:  521     Base: 2 2
c ---[30863]---> Sorter-cost:  521     Base: 2 2
c ---[30862]---> Sorter-cost:  521     Base: 2 2
c ---[30861]---> Sorter-cost:  521     Base: 2 2
c ---[30860]---> Sorter-cost:  521     Base: 2 2
c ---[30859]---> Sorter-cost:  521     Base: 2 2
c ---[30858]---> Sorter-cost:  521     Base: 2 2
c ---[30857]---> Sorter-cost:  521     Base: 2 2
c ---[30856]---> Sorter-cost:  521     Base: 2 2
c ---[30855]---> Sorter-cost:  521     Base: 2 2
c ---[30854]---> BDD-cost:   87
c ---[30853]---> BDD-cost:   87
c ---[30852]---> BDD-cost:   87
c ---[30851]---> BDD-cost:   87
c ---[30850]---> BDD-cost:   87
c ---[30849]---> BDD-cost:   87
c ---[30848]---> BDD-cost:   58
c ---[30847]---> BDD-cost:   58
c ---[30846]---> BDD-cost:   58
c ---[30845]---> BDD-cost:   58
c ---[30844]---> BDD-cost:   58
c ---[30843]---> BDD-cost:   58
c ---[30841]---> BDD-cost:   23
c ---[30839]---> BDD-cost:   23
c ---[30837]---> BDD-cost:   23
c ---[30835]---> BDD-cost:   23
c ---[30833]---> BDD-cost:   23
c ---[30831]---> BDD-cost:   23
c ---[30829]---> BDD-cost:   23
c ---[30827]---> BDD-cost:   23
c ---[30825]---> BDD-cost:   23
c ---[30823]---> BDD-cost:   23
c ---[30821]---> BDD-cost:   23
c ---[30819]---> BDD-cost:   23
c ---[30817]---> BDD-cost:   23
c ---[30815]---> BDD-cost:   23
c ---[30813]---> BDD-cost:   23
c ---[30811]---> BDD-cost:   23
c ---[30809]---> BDD-cost:   23
c ---[30807]---> BDD-cost:   23
c ---[30805]---> BDD-cost:   19
c ---[30803]---> BDD-cost:   19
c ---[30801]---> BDD-cost:   19
c ---[30799]---> BDD-cost:   19
c ---[30797]---> BDD-cost:   19
c ---[30795]---> BDD-cost:   19
c ---[30793]---> BDD-cost:   23
c ---[30791]---> BDD-cost:   23
c ---[30789]---> BDD-cost:   23
c ---[30787]---> BDD-cost:   23
c ---[30785]---> BDD-cost:   23
c ---[30783]---> BDD-cost:   23
c ---[30781]---> BDD-cost:   23
c ---[30779]---> BDD-cost:   23
c ---[30777]---> BDD-cost:   23
c ---[30775]---> BDD-cost:   23
c ---[30773]---> BDD-cost:   23
c ---[30771]---> BDD-cost:   23
c ---[30769]---> BDD-cost:   19
c ---[30767]---> BDD-cost:   19
c ---[30765]---> BDD-cost:   19
c ---[30763]---> BDD-cost:   19
c ---[30761]---> BDD-cost:   19
c ---[30759]---> BDD-cost:   19
c ---[30757]---> BDD-cost:   11
c ---[30755]---> BDD-cost:   11
c ---[30753]---> BDD-cost:   11
c ---[30751]---> BDD-cost:   11
c ---[30749]---> BDD-cost:   11
c ---[30747]---> BDD-cost:   11
c ---[30745]---> BDD-cost:   23
c ---[30743]---> BDD-cost:   23
c ---[30741]---> BDD-cost:   23
c ---[30739]---> BDD-cost:   23
c ---[30737]---> BDD-cost:   23
c ---[30735]---> BDD-cost:   23
c ---[30733]---> BDD-cost:   23
c ---[30731]---> BDD-cost:   23
c ---[30729]---> BDD-cost:   23
c ---[30727]---> BDD-cost:   23
c ---[30725]---> BDD-cost:   23
c ---[30723]---> BDD-cost:   23
c ---[30721]---> BDD-cost:   23
c ---[30719]---> BDD-cost:   23
c ---[30717]---> BDD-cost:   23
c ---[30715]---> BDD-cost:   23
c ---[30713]---> BDD-cost:   23
c ---[30711]---> BDD-cost:   23
c ---[30709]---> BDD-cost:   19
c ---[30707]---> BDD-cost:   19
c ---[30705]---> BDD-cost:   19
c ---[30703]---> BDD-cost:   19
c ---[30701]---> BDD-cost:   19
c ---[30699]---> BDD-cost:   19
c ---[30697]---> BDD-cost:   23
c ---[30695]---> BDD-cost:   23
c ---[30693]---> BDD-cost:   23
c ---[30691]---> BDD-cost:   23
c ---[30689]---> BDD-cost:   23
c ---[30687]---> BDD-cost:   23
c ---[30685]---> BDD-cost:   23
c ---[30683]---> BDD-cost:   23
c ---[30681]---> BDD-cost:   23
c ---[30679]---> BDD-cost:   23
c ---[30677]---> BDD-cost:   23
c ---[30675]---> BDD-cost:   23
c ---[30673]---> BDD-cost:   23
c ---[30671]---> BDD-cost:   23
c ---[30669]---> BDD-cost:   23
c ---[30667]---> BDD-cost:   23
c ---[30665]---> BDD-cost:   23
c ---[30663]---> BDD-cost:   23
c ---[30661]---> BDD-cost:   23
c ---[30659]---> BDD-cost:   23
c ---[30657]---> BDD-cost:   23
c ---[30655]---> BDD-cost:   23
c ---[30653]---> BDD-cost:   23
c ---[30651]---> BDD-cost:   23
c ---[30649]---> BDD-cost:   23
c ---[30647]---> BDD-cost:   23
c ---[30645]---> BDD-cost:   23
c ---[30643]---> BDD-cost:   23
c ---[30641]---> BDD-cost:   23
c ---[30639]---> BDD-cost:   23
c ---[30637]---> BDD-cost:   23
c ---[30635]---> BDD-cost:   23
c ---[30633]---> BDD-cost:   23
c ---[30631]---> BDD-cost:   23
c ---[30629]---> BDD-cost:   23
c ---[30627]---> BDD-cost:   23
c ---[30625]---> BDD-cost:   23
c ---[30623]---> BDD-cost:   23
c ---[30621]---> BDD-cost:   23
c ---[30619]---> BDD-cost:   23
c ---[30617]---> BDD-cost:   23
c ---[30615]---> BDD-cost:   23
c ---[30613]---> BDD-cost:   23
c ---[30611]---> BDD-cost:   23
c ---[30609]---> BDD-cost:   23
c ---[30607]---> BDD-cost:   23
c ---[30605]---> BDD-cost:   23
c ---[30603]---> BDD-cost:   23
c ---[30601]---> BDD-cost:   23
c ---[30599]---> BDD-cost:   23
c ---[30597]---> BDD-cost:   23
c ---[30595]---> BDD-cost:   23
c ---[30593]---> BDD-cost:   23
c ---[30591]---> BDD-cost:   23
c ---[30589]---> BDD-cost:   23
c ---[30587]---> BDD-cost:   23
c ---[30585]---> BDD-cost:   23
c ---[30583]---> BDD-cost:   23
c ---[30581]---> BDD-cost:   23
c ---[30579]---> BDD-cost:   23
c ---[30577]---> BDD-cost:   23
c ---[30575]---> BDD-cost:   23
c ---[30573]---> BDD-cost:   23
c ---[30571]---> BDD-cost:   23
c ---[30569]---> BDD-cost:   23
c ---[30567]---> BDD-cost:   23
c ---[30565]---> BDD-cost:   23
c ---[30563]---> BDD-cost:   23
c ---[30561]---> BDD-cost:   23
c ---[30559]---> BDD-cost:   23
c ---[30557]---> BDD-cost:   23
c ---[30555]---> BDD-cost:   23
c ---[30553]---> BDD-cost:   23
c ---[30551]---> BDD-cost:   23
c ---[30549]---> BDD-cost:   23
c ---[30547]---> BDD-cost:   23
c ---[30545]---> BDD-cost:   23
c ---[30543]---> BDD-cost:   23
c ---[30541]---> BDD-cost:   23
c ---[30539]---> BDD-cost:   23
c ---[30537]---> BDD-cost:   23
c ---[30535]---> BDD-cost:   23
c ---[30533]---> BDD-cost:   23
c ---[30531]---> BDD-cost:   23
c ---[30529]---> BDD-cost:   23
c ---[30527]---> BDD-cost:   23
c ---[30525]---> BDD-cost:   23
c ---[30523]---> BDD-cost:   23
c ---[30521]---> BDD-cost:   23
c ---[30519]---> BDD-cost:   23
c ---[30517]---> BDD-cost:   23
c ---[30515]---> BDD-cost:   23
c ---[30513]---> BDD-cost:   23
c ---[30511]---> BDD-cost:   23
c ---[30509]---> BDD-cost:   23
c ---[30507]---> BDD-cost:   23
c ---[30505]---> BDD-cost:   23
c ---[30503]---> BDD-cost:   23
c ---[30501]---> BDD-cost:   23
c ---[30499]---> BDD-cost:   23
c ---[30497]---> BDD-cost:   23
c ---[30495]---> BDD-cost:   23
c ---[30494]---> BDD-cost:    9
c ---[30493]---> BDD-cost:    9
c ---[30492]---> BDD-cost:    9
c ---[30491]---> BDD-cost:    9
c ---[30490]---> BDD-cost:    9
c ---[30489]---> BDD-cost:    9
c ---[30488]---> BDD-cost:    9
c ---[30487]---> BDD-cost:    9
c ---[30486]---> BDD-cost:    9
c ---[30485]---> BDD-cost:    9
c ---[30484]---> BDD-cost:    9
c ---[30483]---> BDD-cost:    9
c ---[30482]---> BDD-cost:    9
c ---[30481]---> BDD-cost:    9
c ---[30480]---> BDD-cost:    9
c ---[30479]---> BDD-cost:    9
c ---[30478]---> BDD-cost:    9
c ---[30477]---> BDD-cost:    9
c ---[30476]---> BDD-cost:    9
c ---[30475]---> BDD-cost:    9
c ---[30474]---> BDD-cost:    9
c ---[30473]---> BDD-cost:    9
c ---[30472]---> BDD-cost:    9
c ---[30471]---> BDD-cost:    9
c ---[30470]---> BDD-cost:    9
c ---[30469]---> BDD-cost:    9
c ---[30468]---> BDD-cost:    9
c ---[30467]---> BDD-cost:    9
c ---[30466]---> BDD-cost:    9
c ---[30465]---> BDD-cost:    9
c ---[30464]---> BDD-cost:    9
c ---[30463]---> BDD-cost:    9
c ---[30462]---> BDD-cost:    9
c ---[30461]---> BDD-cost:    9
c ---[30460]---> BDD-cost:    9
c ---[30459]---> BDD-cost:    9
c ---[30458]---> BDD-cost:    9
c ---[30457]---> BDD-cost:    9
c ---[30456]---> BDD-cost:    9
c ---[30455]---> BDD-cost:    9
c ---[30454]---> BDD-cost:    9
c ---[30453]---> BDD-cost:    9
c ---[30452]---> BDD-cost:    9
c ---[30451]---> BDD-cost:    9
c ---[30450]---> BDD-cost:    9
c ---[30449]---> BDD-cost:    9
c ---[30448]---> BDD-cost:    9
c ---[30447]---> BDD-cost:    9
c ---[30446]---> BDD-cost:    9
c ---[30445]---> BDD-cost:    9
c ---[30444]---> BDD-cost:    9
c ---[30443]---> BDD-cost:    9
c ---[30442]---> BDD-cost:    9
c ---[30441]---> BDD-cost:    9
c ---[30440]---> BDD-cost:    9
c ---[30439]---> BDD-cost:    9
c ---[30438]---> BDD-cost:    9
c ---[30437]---> BDD-cost:    9
c ---[30436]---> BDD-cost:    9
c ---[30435]---> BDD-cost:    9
c ---[30434]---> BDD-cost:    9
c ---[30433]---> BDD-cost:    9
c ---[30432]---> BDD-cost:    9
c ---[30431]---> BDD-cost:    9
c ---[30430]---> BDD-cost:    9
c ---[30429]---> BDD-cost:    9
c ---[30428]---> BDD-cost:    9
c ---[30427]---> BDD-cost:    9
c ---[30426]---> BDD-cost:    9
c ---[30425]---> BDD-cost:    9
c ---[30424]---> BDD-cost:    9
c ---[30423]---> BDD-cost:    9
c ---[30422]---> BDD-cost:    9
c ---[30421]---> BDD-cost:    9
c ---[30420]---> BDD-cost:    9
c ---[30419]---> BDD-cost:    9
c ---[30418]---> BDD-cost:    9
c ---[30417]---> BDD-cost:    9
c ---[30416]---> BDD-cost:    9
c ---[30415]---> BDD-cost:    9
c ---[30414]---> BDD-cost:    9
c ---[30413]---> BDD-cost:    9
c ---[30412]---> BDD-cost:    9
c ---[30411]---> BDD-cost:    9
c ---[30410]---> BDD-cost:    9
c ---[30409]---> BDD-cost:    9
c ---[30408]---> BDD-cost:    9
c ---[30407]---> BDD-cost:    9
c ---[30406]---> BDD-cost:    9
c ---[30405]---> BDD-cost:    9
c ---[30404]---> BDD-cost:    9
c ---[30403]---> BDD-cost:    9
c ---[30402]---> BDD-cost:    9
c ---[30401]---> BDD-cost:    9
c ---[30400]---> BDD-cost:    9
c ---[30399]---> BDD-cost:    9
c ---[30398]---> BDD-cost:    9
c ---[30397]---> BDD-cost:    9
c ---[30396]---> BDD-cost:    9
c ---[30395]---> BDD-cost:    9
c ---[30394]---> BDD-cost:    9
c ---[30393]---> BDD-cost:    9
c ---[30392]---> BDD-cost:    9
c ---[30391]---> BDD-cost:    9
c ---[30390]---> BDD-cost:    9
c ---[30389]---> BDD-cost:    9
c ---[30388]---> BDD-cost:    9
c ---[30387]---> BDD-cost:    9
c ---[30386]---> BDD-cost:    9
c ---[30385]---> BDD-cost:    9
c ---[30384]---> BDD-cost:    9
c ---[30383]---> BDD-cost:    9
c ---[30382]---> BDD-cost:    9
c ---[30381]---> BDD-cost:    9
c ---[30380]---> BDD-cost:    9
c ---[30379]---> BDD-cost:    9
c ---[30378]---> BDD-cost:    9
c ---[30377]---> BDD-cost:    9
c ---[30376]---> BDD-cost:    9
c ---[30375]---> BDD-cost:    9
c ---[30374]---> BDD-cost:    9
c ---[30373]---> BDD-cost:    9
c ---[30372]---> BDD-cost:    9
c ---[30371]---> BDD-cost:    9
c ---[30370]---> BDD-cost:    9
c ---[30369]---> BDD-cost:    9
c ---[30368]---> BDD-cost:    9
c ---[30367]---> BDD-cost:    9
c ---[30366]---> BDD-cost:    9
c ---[30365]---> BDD-cost:    9
c ---[30364]---> BDD-cost:    9
c ---[30363]---> BDD-cost:    9
c ---[30362]---> BDD-cost:    9
c ---[30361]---> BDD-cost:    9
c ---[30360]---> BDD-cost:    9
c ---[30359]---> BDD-cost:    9
c ---[30358]---> BDD-cost:    9
c ---[30357]---> BDD-cost:    9
c ---[30356]---> BDD-cost:    9
c ---[30355]---> BDD-cost:    9
c ---[30354]---> BDD-cost:    9
c ---[30353]---> BDD-cost:    9
c ---[30352]---> BDD-cost:    9
c ---[30351]---> BDD-cost:    9
c ---[30350]---> BDD-cost:    9
c ---[30349]---> BDD-cost:    9
c ---[30348]---> BDD-cost:    9
c ---[30347]---> BDD-cost:    9
c ---[30346]---> BDD-cost:    9
c ---[30345]---> BDD-cost:    9
c ---[30344]---> BDD-cost:    9
c ---[30343]---> BDD-cost:    9
c ---[30342]---> BDD-cost:    9
c ---[30341]---> BDD-cost:    9
c ---[30340]---> BDD-cost:    9
c ---[30339]---> BDD-cost:    9
c ---[30338]---> BDD-cost:    9
c ---[30337]---> BDD-cost:    9
c ---[30336]---> BDD-cost:    9
c ---[30335]---> BDD-cost:    9
c ---[30334]---> BDD-cost:    9
c ---[30333]---> BDD-cost:    9
c ---[30332]---> BDD-cost:    9
c ---[30331]---> BDD-cost:    9
c ---[30330]---> BDD-cost:    9
c ---[30329]---> BDD-cost:    9
c ---[30328]---> BDD-cost:    9
c ---[30327]---> BDD-cost:    9
c ---[30326]---> BDD-cost:    9
c ---[30325]---> BDD-cost:    9
c ---[30324]---> BDD-cost:    9
c ---[30323]---> BDD-cost:    9
c ---[30322]---> BDD-cost:    9
c ---[30321]---> BDD-cost:    9
c ---[30320]---> BDD-cost:    9
c ---[30319]---> BDD-cost:    9
c ---[30318]---> BDD-cost:    9
c ---[30317]---> BDD-cost:    9
c ---[30316]---> BDD-cost:    9
c ---[30315]---> BDD-cost:    9
c ---[30314]---> BDD-cost:    9
c ---[30313]---> BDD-cost:    9
c ---[30312]---> BDD-cost:    9
c ---[30311]---> BDD-cost:    9
c ---[30310]---> BDD-cost:    9
c ---[30309]---> BDD-cost:    9
c ---[30308]---> BDD-cost:    9
c ---[30307]---> BDD-cost:    9
c ---[30306]---> BDD-cost:    9
c ---[30305]---> BDD-cost:    9
c ---[30304]---> BDD-cost:    9
c ---[30303]---> BDD-cost:    9
c ---[30302]---> BDD-cost:    9
c ---[30301]---> BDD-cost:    9
c ---[30300]---> BDD-cost:    9
c ---[30299]---> BDD-cost:    9
c ---[30298]---> BDD-cost:    9
c ---[30297]---> BDD-cost:    9
c ---[30296]---> BDD-cost:    9
c ---[30295]---> BDD-cost:    9
c ---[30294]---> BDD-cost:    9
c ---[30293]---> BDD-cost:    9
c ---[30292]---> BDD-cost:    9
c ---[30291]---> BDD-cost:    9
c ---[30290]---> BDD-cost:    9
c ---[30289]---> BDD-cost:    9
c ---[30288]---> BDD-cost:    9
c ---[30287]---> BDD-cost:    9
c ---[30286]---> BDD-cost:    9
c ---[30285]---> BDD-cost:    9
c ---[30284]---> BDD-cost:    9
c ---[30283]---> BDD-cost:    9
c ---[30282]---> BDD-cost:    9
c ---[30281]---> BDD-cost:    9
c ---[30280]---> BDD-cost:    9
c ---[30279]---> BDD-cost:    9
c ---[30278]---> BDD-cost:    9
c ---[30277]---> BDD-cost:    9
c ---[30276]---> BDD-cost:    9
c ---[30275]---> BDD-cost:    9
c ---[30274]---> BDD-cost:    9
c ---[30273]---> BDD-cost:    9
c ---[30272]---> BDD-cost:    9
c ---[30271]---> BDD-cost:    9
c ---[30270]---> BDD-cost:    9
c ---[30269]---> BDD-cost:    9
c ---[30268]---> BDD-cost:    9
c ---[30267]---> BDD-cost:    9
c ---[30266]---> BDD-cost:    9
c ---[30265]---> BDD-cost:    9
c ---[30264]---> BDD-cost:    9
c ---[30263]---> BDD-cost:    9
c ---[30262]---> BDD-cost:    9
c ---[30261]---> BDD-cost:    9
c ---[30260]---> BDD-cost:    9
c ---[30259]---> BDD-cost:    9
c ---[30258]---> BDD-cost:    9
c ---[30257]---> BDD-cost:    9
c ---[30256]---> BDD-cost:    9
c ---[30255]---> BDD-cost:    9
c ---[30254]---> BDD-cost:    9
c ---[30253]---> BDD-cost:    9
c ---[30252]---> BDD-cost:    9
c ---[30251]---> BDD-cost:    9
c ---[30250]---> BDD-cost:    9
c ---[30249]---> BDD-cost:    9
c ---[30248]---> BDD-cost:    9
c ---[30247]---> BDD-cost:    9
c ---[30246]---> BDD-cost:    9
c ---[30245]---> BDD-cost:    9
c ---[30244]---> BDD-cost:    9
c ---[30243]---> BDD-cost:    9
c ---[30242]---> BDD-cost:    9
c ---[30241]---> BDD-cost:    9
c ---[30240]---> BDD-cost:    9
c ---[30239]---> BDD-cost:    9
c ---[30238]---> BDD-cost:    9
c ---[30237]---> BDD-cost:    9
c ---[30236]---> BDD-cost:    9
c ---[30235]---> BDD-cost:    9
c ---[30234]---> BDD-cost:    9
c ---[30233]---> BDD-cost:    9
c ---[30232]---> BDD-cost:    9
c ---[30231]---> BDD-cost:    9
c ---[30230]---> BDD-cost:    9
c ---[30229]---> BDD-cost:    9
c ---[30228]---> BDD-cost:    9
c ---[30227]---> BDD-cost:    9
c ---[30226]---> BDD-cost:    9
c ---[30225]---> BDD-cost:    9
c ---[30224]---> BDD-cost:    9
c ---[30223]---> BDD-cost:    9
c ---[30222]---> BDD-cost:    9
c ---[30221]---> BDD-cost:    9
c ---[30220]---> BDD-cost:    9
c ---[30219]---> BDD-cost:    9
c ---[30218]---> BDD-cost:    9
c ---[30217]---> BDD-cost:    9
c ---[30216]---> BDD-cost:    9
c ---[30215]---> BDD-cost:    9
c ---[30214]---> BDD-cost:    9
c ---[30213]---> BDD-cost:    9
c ---[30212]---> BDD-cost:    9
c ---[30211]---> BDD-cost:    9
c ---[30210]---> BDD-cost:    9
c ---[30209]---> BDD-cost:    9
c ---[30208]---> BDD-cost:    9
c ---[30207]---> BDD-cost:    9
c ---[30206]---> BDD-cost:    9
c ---[30205]---> BDD-cost:    9
c ---[30204]---> BDD-cost:    9
c ---[30203]---> BDD-cost:    9
c ---[30202]---> BDD-cost:    9
c ---[30201]---> BDD-cost:    9
c ---[30200]---> BDD-cost:    9
c ---[30199]---> BDD-cost:    9
c ---[30198]---> BDD-cost:    9
c ---[30197]---> BDD-cost:    9
c ---[30196]---> BDD-cost:    9
c ---[30195]---> BDD-cost:    9
c ---[30194]---> BDD-cost:    9
c ---[30193]---> BDD-cost:    9
c ---[30192]---> BDD-cost:    9
c ---[30191]---> BDD-cost:    9
c ---[30190]---> BDD-cost:    9
c ---[30189]---> BDD-cost:    9
c ---[30188]---> BDD-cost:    9
c ---[30187]---> BDD-cost:    9
c ---[30186]---> BDD-cost:    9
c ---[30185]---> BDD-cost:    9
c ---[30184]---> BDD-cost:    9
c ---[30183]---> BDD-cost:    9
c ---[30182]---> BDD-cost:    9
c ---[30181]---> BDD-cost:    9
c ---[30180]---> BDD-cost:    9
c ---[30179]---> BDD-cost:    9
c ---[30178]---> BDD-cost:    9
c ---[30177]---> BDD-cost:    9
c ---[30176]---> BDD-cost:    9
c ---[30175]---> BDD-cost:    9
c ---[30174]---> BDD-cost:    9
c ---[30173]---> BDD-cost:    9
c ---[30172]---> BDD-cost:    9
c ---[30171]---> BDD-cost:    9
c ---[30170]---> BDD-cost:    9
c ---[30169]---> BDD-cost:    9
c ---[30168]---> BDD-cost:    9
c ---[30167]---> BDD-cost:    9
c ---[30166]---> BDD-cost:    9
c ---[30165]---> BDD-cost:    9
c ---[30164]---> BDD-cost:    9
c ---[30163]---> BDD-cost:    9
c ---[30162]---> BDD-cost:    9
c ---[30161]---> BDD-cost:    9
c ---[30160]---> BDD-cost:    9
c ---[30159]---> BDD-cost:    9
c ---[30158]---> BDD-cost:    9
c ---[30157]---> BDD-cost:    9
c ---[30156]---> BDD-cost:    9
c ---[30155]---> BDD-cost:    9
c ---[30154]---> BDD-cost:    9
c ---[30153]---> BDD-cost:    9
c ---[30152]---> BDD-cost:    9
c ---[30151]---> BDD-cost:    9
c ---[30150]---> BDD-cost:    9
c ---[30149]---> BDD-cost:    9
c ---[30148]---> BDD-cost:    9
c ---[30147]---> BDD-cost:    9
c ---[30146]---> BDD-cost:    9
c ---[30145]---> BDD-cost:    9
c ---[30144]---> BDD-cost:    9
c ---[30143]---> BDD-cost:    9
c ---[30142]---> BDD-cost:    9
c ---[30141]---> BDD-cost:    9
c ---[30140]---> BDD-cost:    9
c ---[30139]---> BDD-cost:    9
c ---[30138]---> BDD-cost:    9
c ---[30137]---> BDD-cost:    9
c ---[30136]---> BDD-cost:    9
c ---[30135]---> BDD-cost:    9
c ---[30134]---> BDD-cost:    9
c ---[30133]---> BDD-cost:    9
c ---[30132]---> BDD-cost:    9
c ---[30131]---> BDD-cost:    9
c ---[30130]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:    9
c ---[ 402]---> BDD-cost:    9
c ---[ 401]---> BDD-cost:    9
c ---[ 400]---> BDD-cost:    9
c ---[ 399]---> BDD-cost:    9
c ---[ 398]---> BDD-cost:    9
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    9
c ---[ 395]---> BDD-cost:    9
c ---[ 394]---> BDD-cost:    9
c ---[ 393]---> BDD-cost:    9
c ---[ 392]---> BDD-cost:    9
c ---[ 391]---> BDD-cost:    9
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:    9
c ---[ 386]---> BDD-cost:    9
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    9
c ---[ 383]---> BDD-cost:    9
c ---[ 382]---> BDD-cost:    9
c ---[ 381]---> BDD-cost:    9
c ---[ 380]---> BDD-cost:    9
c ---[ 379]---> BDD-cost:    9
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    9
c ---[ 375]---> BDD-cost:    9
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 372]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:    9
c ---[ 369]---> BDD-cost:    9
c ---[ 368]---> BDD-cost:    9
c ---[ 367]---> BDD-cost:    9
c ---[ 366]---> BDD-cost:    9
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:    9
c ---[ 362]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    9
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:    9
c ---[ 354]---> BDD-cost:    9
c ---[ 353]---> BDD-cost:    9
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    9
c ---[ 350]---> BDD-cost:    9
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:    9
c ---[ 347]---> BDD-cost:    9
c ---[ 346]---> BDD-cost:    9
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    9
c ---[ 343]---> BDD-cost:    9
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:    9
c ---[ 338]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    9
c ---[ 336]---> BDD-cost:    9
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:    9
c ---[ 332]---> BDD-cost:    9
c ---[ 331]---> BDD-cost:    9
c ---[ 330]---> BDD-cost:    9
c ---[ 329]---> BDD-cost:    9
c ---[ 328]---> BDD-cost:    9
c ---[ 327]---> BDD-cost:    9
c ---[ 326]---> BDD-cost:    9
c ---[ 325]---> BDD-cost:    9
c ---[ 324]---> BDD-cost:    9
c ---[ 323]---> BDD-cost:    9
c ---[ 322]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    9
c ---[ 320]---> BDD-cost:    9
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    9
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    9
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    9
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:    9
c ---[ 306]---> BDD-cost:    9
c ---[ 305]---> BDD-cost:    9
c ---[ 304]---> BDD-cost:    9
c ---[ 303]---> BDD-cost:    9
c ---[ 302]---> BDD-cost:    9
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    9
c ---[ 297]---> BDD-cost:    9
c ---[ 296]---> BDD-cost:    9
c ---[ 295]---> BDD-cost:    9
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:    9
c ---[ 290]---> BDD-cost:    9
c ---[ 289]---> BDD-cost:    9
c ---[ 288]---> BDD-cost:    9
c ---[ 287]---> BDD-cost:    9
c ---[ 286]---> BDD-cost:    9
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    9
c ---[ 281]---> BDD-cost:    9
c ---[ 280]---> BDD-cost:    9
c ---[ 279]---> BDD-cost:    9
c ---[ 278]---> BDD-cost:    9
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    9
c ---[ 273]---> BDD-cost:    9
c ---[ 272]---> BDD-cost:    9
c ---[ 271]---> BDD-cost:    9
c ---[ 270]---> BDD-cost:    9
c ---[ 269]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:    9
c ---[ 267]---> BDD-cost:    9
c ---[ 266]---> BDD-cost:    9
c ---[ 265]---> BDD-cost:    9
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    9
c ---[ 257]---> BDD-cost:    9
c ---[ 256]---> BDD-cost:    9
c ---[ 255]---> BDD-cost:    9
c ---[ 254]---> BDD-cost:    9
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:    9
c ---[ 249]---> BDD-cost:    9
c ---[ 248]---> BDD-cost:    9
c ---[ 247]---> BDD-cost:    9
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:    9
c ---[ 241]---> BDD-cost:    9
c ---[ 240]---> BDD-cost:    9
c ---[ 239]---> BDD-cost:    9
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:    9
c ---[ 236]---> BDD-cost:    9
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:    9
c ---[ 233]---> BDD-cost:    9
c ---[ 232]---> BDD-cost:    9
c ---[ 231]---> BDD-cost:    9
c ---[ 230]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:    9
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:    9
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:    9
c ---[ 222]---> BDD-cost:    9
c ---[ 221]---> BDD-cost:    9
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:    9
c ---[ 218]---> BDD-cost:    9
c ---[ 217]---> BDD-cost:    9
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:    9
c ---[ 209]---> BDD-cost:    9
c ---[ 208]---> BDD-cost:    9
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:    9
c ---[ 204]---> BDD-cost:    9
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:    9
c ---[ 201]---> BDD-cost:    9
c ---[ 200]---> BDD-cost:    9
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:    9
c ---[ 194]---> BDD-cost:    9
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:    9
c ---[ 191]---> BDD-cost:    9
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:    9
c ---[ 188]---> BDD-cost:    9
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:    9
c ---[ 185]---> BDD-cost:    9
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:    9
c ---[ 182]---> BDD-cost:    9
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:    9
c ---[ 178]---> BDD-cost:    9
c ---[ 177]---> BDD-cost:    9
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:    9
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:    9
c ---[ 170]---> BDD-cost:    9
c ---[ 169]---> BDD-cost:    9
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    9
c ---[ 159]---> BDD-cost:    9
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    9
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:    9
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:    9
c ---[ 146]---> BDD-cost:    9
c ---[ 145]---> BDD-cost:    9
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:    9
c ---[ 142]---> BDD-cost:    9
c ---[ 141]---> BDD-cost:    9
c ---[ 140]---> BDD-cost:    9
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    9
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    9
c ---[ 134]---> BDD-cost:    9
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:    9
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    9
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:    9
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:    9
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:    9
c ---[ 108]---> BDD-cost:    9
c ---[ 107]---> BDD-cost:    9
c ---[ 106]---> BDD-cost:    9
c ---[ 105]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:    9
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    9
c ---[  98]---> BDD-cost:    9
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    9
c ---[  93]---> BDD-cost:    9
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:    9
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:    9
c ---[  87]---> BDD-cost:    9
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:    9
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:    9
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:    9
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    9
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:    9
c ---[  64]---> BDD-cost:    9
c ---[  63]---> BDD-cost:    9
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:    9
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:    9
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    9
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:    9
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:    9
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:    9
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:    9
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:    9
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:    9
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:    9
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    9
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:    9
c ==================================[MINISAT+]==================================
c | Conflicts | Original         | Learnt                           | Progress |
c |           | Clauses Literals |     Max Clauses Literals     LPC |          |
c ==============================================================================
c |         0 |  117672   328254 |   39224       0        0     nan |  0.000 % |
c |       100 |  117657   328209 |   43146      89      422     4.7 |  3.968 % |
c |       253 |  117573   327976 |   47461     223     1258     5.6 |  4.041 % |
c |       478 |  117498   327751 |   52207     341     1644     4.8 |  4.099 % |
c |       815 |  117268   327092 |   57427     528     2555     4.8 |  4.289 % |
c |      1321 |  116922   326079 |   63170     872     4663     5.3 |  4.567 % |
c |      2080 |  116560   325080 |   69487    1472    13879     9.4 |  4.881 % |
c |      3219 |  116505   324915 |   76436    2474    45394    18.3 |  4.927 % |
c |      4931 |  116455   324765 |   84080    4097    99115    24.2 |  4.962 % |
c |      7493 |  116300   324300 |   92488    6512   181991    27.9 |  5.082 % |
c |     11337 |  116137   323829 |  101736   10235   351614    34.4 |  5.213 % |
c |     17106 |  115884   323122 |  111910   15893   624434    39.3 |  5.426 % |
c |     25755 |  115341   321588 |  123101   24283  1005119    41.4 |  5.886 % |
c |     38730 |  115176   321111 |  135411   37149  1653720    44.5 |  6.022 % |
c |     58193 |  114009   318019 |  148953   56129  2626493    46.8 |  7.124 % |
c |     87385 |  113797   317422 |  163848   85253  4221914    49.5 |  7.306 % |
c |    131175 |  113016   315228 |  180233  128759  6706322    52.1 |  7.998 % |
c |    196863 |  111634   311518 |  198256   30244  1342067    44.4 |  9.290 % |
c |    295390 |  109844   306687 |  218082  128128  6565206    51.2 | 11.022 % |
#### 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.93 1.00 0.95 1/54 26898
Raw data (stat): 26898 (runsolver) R 26897 20937 20936 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 423712768 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.0007 s]
Raw data (loadavg): 0.94 1.00 0.95 2/54 26898
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 3100 0 0 0 989 9 0 0 25 0 1 0 423712768 14417920 3030 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 3520 3030 603 41 0 3479 0
vsize: 14080
[startup+20.0023 s]
Raw data (loadavg): 0.95 1.00 0.95 2/54 26898
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 3622 0 0 0 1987 10 0 0 25 0 1 0 423712768 16584704 3552 4294967295 134512640 134672761 3221224560 3221223664 134560196 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4049 3552 603 41 0 4008 0
vsize: 16196
[startup+30.0028 s]
Raw data (loadavg): 0.96 1.00 0.95 2/54 26898
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 4066 0 0 0 2985 12 0 0 25 0 1 0 423712768 18427904 3996 4294967295 134512640 134672761 3221224560 3221223732 134556598 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4499 3996 603 41 0 4458 0
vsize: 17996
[startup+40.0033 s]
Raw data (loadavg): 0.96 1.00 0.95 2/54 26898
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 4390 0 0 0 3984 13 0 0 25 0 1 0 423712768 19640320 4320 4294967295 134512640 134672761 3221224560 3221223700 134565972 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 4795 4320 603 41 0 4754 0
vsize: 19180
[startup+50.0035 s]
Raw data (loadavg): 0.97 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 4982 0 0 0 4982 15 0 0 25 0 1 0 423712768 22188032 4912 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5417 4912 603 41 0 5376 0
vsize: 21668
[startup+60.0038 s]
Raw data (loadavg): 0.97 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 5318 0 0 0 5982 15 0 0 25 0 1 0 423712768 23531520 5248 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5745 5248 603 41 0 5704 0
vsize: 22980
[startup+70.0049 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 5522 0 0 0 6981 16 0 0 25 0 1 0 423712768 24350720 5452 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5945 5452 603 41 0 5904 0
vsize: 23780
[startup+80.0059 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 5717 0 0 0 7981 17 0 0 25 0 1 0 423712768 25149440 5647 4294967295 134512640 134672761 3221224560 3221223732 134556680 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6140 5647 603 41 0 6099 0
vsize: 24560
[startup+90.0059 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 5954 0 0 0 8980 17 0 0 25 0 1 0 423712768 26095616 5884 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6371 5884 603 41 0 6330 0
vsize: 25484
[startup+100.006 s]
Raw data (loadavg): 0.98 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 6249 0 0 0 9979 19 0 0 25 0 1 0 423712768 27308032 6179 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6667 6179 603 41 0 6626 0
vsize: 26668
[startup+110.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 6499 0 0 0 10979 20 0 0 25 0 1 0 423712768 28385280 6429 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 6930 6429 603 41 0 6889 0
vsize: 27720
[startup+120.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 6806 0 0 0 11979 20 0 0 25 0 1 0 423712768 29585408 6736 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7223 6736 603 41 0 7182 0
vsize: 28892
[startup+130.007 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 7177 0 0 0 12978 21 0 0 25 0 1 0 423712768 31490048 7107 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7688 7107 603 41 0 7647 0
vsize: 30752
[startup+140.008 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 7448 0 0 0 13978 21 0 0 25 0 1 0 423712768 32559104 7378 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 7949 7378 603 41 0 7908 0
vsize: 31796
[startup+150.008 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 7794 0 0 0 14977 23 0 0 25 0 1 0 423712768 33898496 7724 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8276 7724 603 41 0 8235 0
vsize: 33104
[startup+160.009 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 8080 0 0 0 15976 24 0 0 25 0 1 0 423712768 35139584 8010 4294967295 134512640 134672761 3221224560 3221223664 134560326 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8579 8010 603 41 0 8538 0
vsize: 34316
[startup+170.01 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 8318 0 0 0 16976 24 0 0 25 0 1 0 423712768 36085760 8248 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 8810 8248 603 41 0 8769 0
vsize: 35240
[startup+180.009 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 8543 0 0 0 17975 25 0 0 25 0 1 0 423712768 37011456 8473 4294967295 134512640 134672761 3221224560 3221223664 134559851 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9036 8473 603 41 0 8995 0
vsize: 36144
[startup+190.01 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 8755 0 0 0 18975 25 0 0 25 0 1 0 423712768 37838848 8685 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9238 8685 603 41 0 9197 0
vsize: 36952
[startup+200.01 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 8862 0 0 0 19974 26 0 0 25 0 1 0 423712768 38260736 8792 4294967295 134512640 134672761 3221224560 3221223728 134560937 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9341 8792 603 41 0 9300 0
vsize: 37364
[startup+210.01 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 9125 0 0 0 20974 27 0 0 25 0 1 0 423712768 39337984 9055 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9604 9055 603 41 0 9563 0
vsize: 38416
[startup+220.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 9306 0 0 0 21974 27 0 0 25 0 1 0 423712768 40173568 9236 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 9808 9236 603 41 0 9767 0
vsize: 39232
[startup+230.011 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 9558 0 0 0 22973 28 0 0 25 0 1 0 423712768 41246720 9488 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10070 9488 603 41 0 10029 0
vsize: 40280
[startup+240.011 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 9742 0 0 0 23973 28 0 0 25 0 1 0 423712768 41914368 9672 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10233 9672 603 41 0 10192 0
vsize: 40932
[startup+250.012 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 9956 0 0 0 24973 28 0 0 25 0 1 0 423712768 42864640 9886 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10465 9886 603 41 0 10424 0
vsize: 41860
[startup+260.014 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 10177 0 0 0 25973 29 0 0 25 0 1 0 423712768 43814912 10107 4294967295 134512640 134672761 3221224560 3221223728 134561008 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10697 10107 603 41 0 10656 0
vsize: 42788
[startup+270.014 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 10338 0 0 0 26972 30 0 0 25 0 1 0 423712768 44355584 10268 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 10829 10268 603 41 0 10788 0
vsize: 43316
[startup+280.014 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 10571 0 0 0 27972 30 0 0 25 0 1 0 423712768 45305856 10501 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11061 10501 603 41 0 11020 0
vsize: 44244
[startup+290.014 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 10721 0 0 0 28972 30 0 0 25 0 1 0 423712768 45973504 10651 4294967295 134512640 134672761 3221224560 3221223560 1075350517 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11224 10651 603 41 0 11183 0
vsize: 44896
[startup+300.014 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 10874 0 0 0 29972 31 0 0 25 0 1 0 423712768 46514176 10804 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11356 10804 603 41 0 11315 0
vsize: 45424
[startup+310.015 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 10959 0 0 0 30972 31 0 0 25 0 1 0 423712768 46907392 10889 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11452 10889 603 41 0 11411 0
vsize: 45808
[startup+320.016 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 11132 0 0 0 31971 31 0 0 25 0 1 0 423712768 47579136 11062 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11616 11062 603 41 0 11575 0
vsize: 46464
[startup+330.016 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 11253 0 0 0 32971 32 0 0 25 0 1 0 423712768 48123904 11183 4294967295 134512640 134672761 3221224560 3221223732 134556660 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11749 11183 603 41 0 11708 0
vsize: 46996
[startup+340.016 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 11392 0 0 0 33971 32 0 0 25 0 1 0 423712768 48689152 11322 4294967295 134512640 134672761 3221224560 3221223684 134566043 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 11887 11322 603 41 0 11846 0
vsize: 47548
[startup+350.016 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 11522 0 0 0 34970 33 0 0 25 0 1 0 423712768 49242112 11452 4294967295 134512640 134672761 3221224560 3221223732 134556685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12022 11452 603 41 0 11981 0
vsize: 48088
[startup+360.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 11621 0 0 0 35969 33 0 0 25 0 1 0 423712768 49647616 11551 4294967295 134512640 134672761 3221224560 3221223728 134561212 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12121 11551 603 41 0 12080 0
vsize: 48484
[startup+370.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 11768 0 0 0 36969 33 0 0 25 0 1 0 423712768 50712576 11698 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12381 11698 603 41 0 12340 0
vsize: 49524
[startup+380.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 11898 0 0 0 37968 34 0 0 25 0 1 0 423712768 51253248 11828 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12513 11828 603 41 0 12472 0
vsize: 50052
[startup+390.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 11994 0 0 0 38968 34 0 0 25 0 1 0 423712768 51687424 11924 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12619 11924 603 41 0 12578 0
vsize: 50476
[startup+400.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 12098 0 0 0 39968 34 0 0 25 0 1 0 423712768 52109312 12028 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12722 12028 603 41 0 12681 0
vsize: 50888
[startup+410.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 12273 0 0 0 40968 35 0 0 25 0 1 0 423712768 52781056 12203 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12886 12203 603 41 0 12845 0
vsize: 51544
[startup+420.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 12361 0 0 0 41968 35 0 0 25 0 1 0 423712768 53211136 12291 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 12991 12291 603 41 0 12950 0
vsize: 51964
[startup+430.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 12492 0 0 0 42968 35 0 0 25 0 1 0 423712768 53788672 12422 4294967295 134512640 134672761 3221224560 3221223728 134561115 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13132 12422 603 41 0 13091 0
vsize: 52528
[startup+440.018 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 12595 0 0 0 43968 35 0 0 25 0 1 0 423712768 54190080 12525 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13230 12525 603 41 0 13189 0
vsize: 52920
[startup+450.017 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 12707 0 0 0 44968 36 0 0 25 0 1 0 423712768 54595584 12637 4294967295 134512640 134672761 3221224560 3221223728 134561164 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13329 12637 603 41 0 13288 0
vsize: 53316
[startup+460.018 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 12780 0 0 0 45968 36 0 0 25 0 1 0 423712768 54992896 12710 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13426 12710 603 41 0 13385 0
vsize: 53704
[startup+470.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 12906 0 0 0 46967 37 0 0 25 0 1 0 423712768 55390208 12836 4294967295 134512640 134672761 3221224560 3221223776 134561985 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13523 12836 603 41 0 13482 0
vsize: 54092
[startup+480.018 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 13037 0 0 0 47967 37 0 0 25 0 1 0 423712768 55914496 12967 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13651 12967 603 41 0 13610 0
vsize: 54604
[startup+490.018 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 13185 0 0 0 48967 37 0 0 25 0 1 0 423712768 56582144 13115 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13814 13115 603 41 0 13773 0
vsize: 55256
[startup+500.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 13304 0 0 0 49967 38 0 0 25 0 1 0 423712768 57098240 13234 4294967295 134512640 134672761 3221224560 3221223728 134561154 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 13940 13234 603 41 0 13899 0
vsize: 55760
[startup+510.018 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 13426 0 0 0 50966 38 0 0 25 0 1 0 423712768 57552896 13356 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14051 13356 603 41 0 14010 0
vsize: 56204
[startup+520.018 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 13617 0 0 0 51966 39 0 0 25 0 1 0 423712768 58376192 13547 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14252 13547 603 41 0 14211 0
vsize: 57008
[startup+530.018 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 13783 0 0 0 52966 39 0 0 25 0 1 0 423712768 59039744 13713 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14414 13713 603 41 0 14373 0
vsize: 57656
[startup+540.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 13899 0 0 0 53966 39 0 0 25 0 1 0 423712768 59453440 13829 4294967295 134512640 134672761 3221224560 3221223728 134560874 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14515 13829 603 41 0 14474 0
vsize: 58060
[startup+550.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 13994 0 0 0 54966 40 0 0 25 0 1 0 423712768 59871232 13924 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14617 13924 603 41 0 14576 0
vsize: 58468
[startup+560.018 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14191 0 0 0 55965 41 0 0 25 0 1 0 423712768 60678144 14121 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14814 14121 603 41 0 14773 0
vsize: 59256
[startup+570.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14325 0 0 0 56965 41 0 0 25 0 1 0 423712768 61214720 14255 4294967295 134512640 134672761 3221224560 3221223732 134556667 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 14945 14255 603 41 0 14904 0
vsize: 59780
[startup+580.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14427 0 0 0 57965 41 0 0 25 0 1 0 423712768 61620224 14357 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15044 14357 603 41 0 15003 0
vsize: 60176
[startup+590.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14493 0 0 0 58965 41 0 0 25 0 1 0 423712768 61939712 14423 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15122 14423 603 41 0 15081 0
vsize: 60488
[startup+600.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14512 0 0 0 59965 41 0 0 25 0 1 0 423712768 62074880 14442 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15155 14442 603 41 0 15114 0
vsize: 60620
[startup+610.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14619 0 0 0 60965 42 0 0 25 0 1 0 423712768 62476288 14549 4294967295 134512640 134672761 3221224560 3221223728 134560929 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15253 14549 603 41 0 15212 0
vsize: 61012
[startup+620.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14731 0 0 0 61965 42 0 0 25 0 1 0 423712768 62877696 14661 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15351 14661 603 41 0 15310 0
vsize: 61404
[startup+630.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14772 0 0 0 62965 42 0 0 25 0 1 0 423712768 63152128 14702 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15418 14702 603 41 0 15377 0
vsize: 61672
[startup+640.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14895 0 0 0 63965 42 0 0 25 0 1 0 423712768 63582208 14825 4294967295 134512640 134672761 3221224560 3221223764 134561964 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15523 14825 603 41 0 15482 0
vsize: 62092
[startup+650.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 14998 0 0 0 64965 42 0 0 25 0 1 0 423712768 64122880 14928 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15655 14928 603 41 0 15614 0
vsize: 62620
[startup+660.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 65965 42 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134560852 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+670.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 66965 42 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134561005 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+680.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 67965 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223732 134556682 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+690.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 68964 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223744 134559041 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+700.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 69965 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134561205 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+710.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 70965 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+720.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 71965 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134561167 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+730.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 72965 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+740.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 73965 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+750.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 74966 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223744 134558899 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+760.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 75966 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134561151 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+770.021 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15062 0 0 0 76966 43 0 0 25 0 1 0 423712768 64421888 14992 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14992 603 41 0 15687 0
vsize: 62912
[startup+780.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15063 0 0 0 77966 43 0 0 25 0 1 0 423712768 64421888 14993 4294967295 134512640 134672761 3221224560 3221223656 1075347141 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14993 603 41 0 15687 0
vsize: 62912
[startup+790.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15063 0 0 0 78966 43 0 0 25 0 1 0 423712768 64421888 14993 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14993 603 41 0 15687 0
vsize: 62912
[startup+800.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15063 0 0 0 79966 43 0 0 25 0 1 0 423712768 64421888 14993 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14993 603 41 0 15687 0
vsize: 62912
[startup+810.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15063 0 0 0 80966 43 0 0 25 0 1 0 423712768 64421888 14993 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14993 603 41 0 15687 0
vsize: 62912
[startup+820.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15067 0 0 0 81967 43 0 0 25 0 1 0 423712768 64421888 14997 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14997 603 41 0 15687 0
vsize: 62912
[startup+830.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15067 0 0 0 82967 43 0 0 25 0 1 0 423712768 64421888 14997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14997 603 41 0 15687 0
vsize: 62912
[startup+840.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15067 0 0 0 83967 43 0 0 25 0 1 0 423712768 64421888 14997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14997 603 41 0 15687 0
vsize: 62912
[startup+850.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15067 0 0 0 84967 43 0 0 25 0 1 0 423712768 64421888 14997 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14997 603 41 0 15687 0
vsize: 62912
[startup+860.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15067 0 0 0 85967 43 0 0 25 0 1 0 423712768 64421888 14997 4294967295 134512640 134672761 3221224560 3221223728 134560956 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14997 603 41 0 15687 0
vsize: 62912
[startup+870.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15069 0 0 0 86968 43 0 0 25 0 1 0 423712768 64421888 14999 4294967295 134512640 134672761 3221224560 3221223732 134556634 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 14999 603 41 0 15687 0
vsize: 62912
[startup+880.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15070 0 0 0 87968 43 0 0 25 0 1 0 423712768 64421888 15000 4294967295 134512640 134672761 3221224560 3221223728 134561215 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 15000 603 41 0 15687 0
vsize: 62912
[startup+890.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15071 0 0 0 88968 43 0 0 25 0 1 0 423712768 64421888 15001 4294967295 134512640 134672761 3221224560 3221223664 134560264 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 15001 603 41 0 15687 0
vsize: 62912
[startup+900.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15071 0 0 0 89968 43 0 0 25 0 1 0 423712768 64421888 15001 4294967295 134512640 134672761 3221224560 3221223728 134561118 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 15001 603 41 0 15687 0
vsize: 62912
[startup+910.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15071 0 0 0 90968 43 0 0 25 0 1 0 423712768 64421888 15001 4294967295 134512640 134672761 3221224560 3221223744 134556589 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 15001 603 41 0 15687 0
vsize: 62912
[startup+920.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15074 0 0 0 91969 43 0 0 25 0 1 0 423712768 64421888 15004 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 15004 603 41 0 15687 0
vsize: 62912
[startup+930.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15074 0 0 0 92969 43 0 0 25 0 1 0 423712768 64421888 15004 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 15004 603 41 0 15687 0
vsize: 62912
[startup+940.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15092 0 0 0 93969 43 0 0 25 0 1 0 423712768 64421888 15022 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15728 15022 603 41 0 15687 0
vsize: 62912
[startup+950.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15110 0 0 0 94969 43 0 0 25 0 1 0 423712768 64684032 15040 4294967295 134512640 134672761 3221224560 3221223728 134560869 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15040 603 41 0 15751 0
vsize: 63168
[startup+960.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15112 0 0 0 95969 43 0 0 25 0 1 0 423712768 64684032 15042 4294967295 134512640 134672761 3221224560 3221223728 134560830 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15042 603 41 0 15751 0
vsize: 63168
[startup+970.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15120 0 0 0 96969 43 0 0 25 0 1 0 423712768 64684032 15050 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15792 15050 603 41 0 15751 0
vsize: 63168
[startup+980.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15121 0 0 0 97969 43 0 0 25 0 1 0 423712768 64684032 15051 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15051 603 41 0 15751 0
vsize: 63168
[startup+990.019 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15122 0 0 0 98969 43 0 0 25 0 1 0 423712768 64684032 15052 4294967295 134512640 134672761 3221224560 3221223728 134560983 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15052 603 41 0 15751 0
vsize: 63168
[startup+1000.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15132 0 0 0 99969 43 0 0 25 0 1 0 423712768 64684032 15062 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15062 603 41 0 15751 0
vsize: 63168
[startup+1010.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15132 0 0 0 100969 43 0 0 25 0 1 0 423712768 64684032 15062 4294967295 134512640 134672761 3221224560 3221223728 134561193 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15062 603 41 0 15751 0
vsize: 63168
[startup+1020.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15132 0 0 0 101969 43 0 0 25 0 1 0 423712768 64684032 15062 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15062 603 41 0 15751 0
vsize: 63168
[startup+1030.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15132 0 0 0 102969 43 0 0 25 0 1 0 423712768 64684032 15062 4294967295 134512640 134672761 3221224560 3221223728 134560980 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15062 603 41 0 15751 0
vsize: 63168
[startup+1040.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15133 0 0 0 103970 43 0 0 25 0 1 0 423712768 64684032 15063 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15063 603 41 0 15751 0
vsize: 63168
[startup+1050.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15133 0 0 0 104970 43 0 0 25 0 1 0 423712768 64684032 15063 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15063 603 41 0 15751 0
vsize: 63168
[startup+1060.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15136 0 0 0 105970 43 0 0 25 0 1 0 423712768 64684032 15066 4294967295 134512640 134672761 3221224560 3221223732 134556643 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15066 603 41 0 15751 0
vsize: 63168
[startup+1070.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15136 0 0 0 106970 43 0 0 25 0 1 0 423712768 64684032 15066 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15066 603 41 0 15751 0
vsize: 63168
[startup+1080.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15145 0 0 0 107970 43 0 0 25 0 1 0 423712768 64684032 15075 4294967295 134512640 134672761 3221224560 3221223728 134561229 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15075 603 41 0 15751 0
vsize: 63168
[startup+1090.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15154 0 0 0 108971 43 0 0 25 0 1 0 423712768 64684032 15084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15084 603 41 0 15751 0
vsize: 63168
[startup+1100.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15154 0 0 0 109971 43 0 0 25 0 1 0 423712768 64684032 15084 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15084 603 41 0 15751 0
vsize: 63168
[startup+1110.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15159 0 0 0 110971 43 0 0 25 0 1 0 423712768 64684032 15089 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15792 15089 603 41 0 15751 0
vsize: 63168
[startup+1120.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15179 0 0 0 111971 43 0 0 25 0 1 0 423712768 64880640 15109 4294967295 134512640 134672761 3221224560 3221223728 134560996 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15840 15109 603 41 0 15799 0
vsize: 63360
[startup+1130.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15181 0 0 0 112971 43 0 0 25 0 1 0 423712768 64880640 15111 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15840 15111 603 41 0 15799 0
vsize: 63360
[startup+1140.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15182 0 0 0 113972 43 0 0 25 0 1 0 423712768 64880640 15112 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15840 15112 603 41 0 15799 0
vsize: 63360
[startup+1150.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15192 0 0 0 114972 43 0 0 25 0 1 0 423712768 64880640 15122 4294967295 134512640 134672761 3221224560 3221223728 134560988 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15840 15122 603 41 0 15799 0
vsize: 63360
[startup+1160.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15196 0 0 0 115972 43 0 0 25 0 1 0 423712768 64880640 15126 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15840 15126 603 41 0 15799 0
vsize: 63360
[startup+1170.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15196 0 0 0 116972 43 0 0 25 0 1 0 423712768 64880640 15126 4294967295 134512640 134672761 3221224560 3221223728 134561001 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15840 15126 603 41 0 15799 0
vsize: 63360
[startup+1180.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15196 0 0 0 117972 43 0 0 25 0 1 0 423712768 64880640 15126 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15840 15126 603 41 0 15799 0
vsize: 63360
[startup+1190.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15215 0 0 0 118973 43 0 0 25 0 1 0 423712768 65044480 15145 4294967295 134512640 134672761 3221224560 3221223728 134560898 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 15880 15145 603 41 0 15839 0
vsize: 63520
[startup+1200.02 s]
Raw data (loadavg): 0.99 1.00 0.95 2/54 26900
Raw data (stat): 26898 (minisat+) R 26897 20937 20936 0 -1 0 15342 0 0 0 119972 43 0 0 25 0 1 0 423712768 65581056 15272 4294967295 134512640 134672761 3221224560 3221223728 134561190 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 16011 15272 603 41 0 15970 0
vsize: 64044
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.05 s]
Raw data (loadavg): 0.99 1.00 0.95 1/54 26900
Raw data (stat): 26898 (minisat+) Z 26897 20937 20936 0 -1 12 15344 0 0 0 119972 46 0 0 25 0 1 0 423712768 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 0 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.05
CPU time (s): 1200.2
CPU user time (s): 1199.73
CPU system time (s): 0.469928
CPU usage (%): 100.012
Max. virtual memory (Kb): 64044
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####