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,3-13,19.opb
MD5SUM	fa67033d6a242cf79309b3804f79a4fe
Bench Category	no optimization function (SAT)
Has Objective Function	NO
Satisfiable	YES
(Un)Satisfiability was proved	YES
Best value of the objective function	0
Optimality of the best value was proved	NO
Number of terms in the objective function	0
Biggest coefficient in the objective function	0
Number of bits for the biggest coefficient in the objective function	0
Sum of the numbers in the objective function	0
Number of bits of the sum of numbers in the objective function	0
Biggest number in a constraint	10
Number of bits of the biggest number in a constraint	4
Biggest sum of numbers in a constraint	102
Number of bits of the biggest sum of numbers	7
Best result obtained on this benchmark	SAT
Best CPU time to get the best result obtained on this benchmark	15.8556
Number of variables	4608
Total number of constraints	34956
Number of constraints which are clauses	29328
Number of constraints which are cardinality constraints (but not clauses)	5550
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 5657

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

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

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        731336 kB
Buffers:         38000 kB
Cached:         224208 kB
SwapCached:          0 kB
Active:          83208 kB
Inactive:       181896 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        731084 kB
SwapTotal:     2097892 kB
SwapFree:      2097892 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           6928 kB
Slab:            32536 kB
Committed_AS:    63492 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-04-14 01:38:13 (client local time) WITH STATUS 0 IN 1200.28 SECONDS
stats: 4120 7 1200.28 0
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 30522 PB-constraints to clauses...
c   -- Unit propagations: (none)
c   -- Detecting intervals from adjacent constraints: ##############################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................................
c ---[30521]---> BDD-cost:   57
c ---[30520]---> BDD-cost:   57
c ---[30519]---> BDD-cost:   57
c ---[30518]---> BDD-cost:   57
c ---[30517]---> BDD-cost:   57
c ---[30516]---> BDD-cost:   57
c ---[30515]---> BDD-cost:  100
c ---[30514]---> BDD-cost:  100
c ---[30513]---> BDD-cost:  100
c ---[30512]---> BDD-cost:  100
c ---[30511]---> BDD-cost:  100
c ---[30510]---> BDD-cost:  100
c ---[30509]---> BDD-cost:  122
c ---[30508]---> BDD-cost:  122
c ---[30507]---> BDD-cost:  122
c ---[30506]---> BDD-cost:  122
c ---[30505]---> BDD-cost:  122
c ---[30504]---> BDD-cost:  122
c ---[30503]---> BDD-cost:  122
c ---[30502]---> BDD-cost:  122
c ---[30501]---> BDD-cost:  122
c ---[30500]---> BDD-cost:  122
c ---[30499]---> BDD-cost:  122
c ---[30498]---> BDD-cost:  122
c ---[30497]---> BDD-cost:  122
c ---[30496]---> BDD-cost:  122
c ---[30495]---> BDD-cost:  122
c ---[30494]---> BDD-cost:  122
c ---[30493]---> BDD-cost:  122
c ---[30492]---> BDD-cost:  122
c ---[30491]---> BDD-cost:  131
c ---[30490]---> BDD-cost:  131
c ---[30489]---> BDD-cost:  131
c ---[30488]---> BDD-cost:  131
c ---[30487]---> BDD-cost:  131
c ---[30486]---> BDD-cost:  131
c ---[30485]---> BDD-cost:  122
c ---[30484]---> BDD-cost:  122
c ---[30483]---> BDD-cost:  122
c ---[30482]---> BDD-cost:  122
c ---[30481]---> BDD-cost:  122
c ---[30480]---> BDD-cost:  122
c ---[30479]---> BDD-cost:  122
c ---[30478]---> BDD-cost:  122
c ---[30477]---> BDD-cost:  122
c ---[30476]---> BDD-cost:  122
c ---[30475]---> BDD-cost:  122
c ---[30474]---> BDD-cost:  122
c ---[30473]---> BDD-cost:  122
c ---[30472]---> BDD-cost:  122
c ---[30471]---> BDD-cost:  122
c ---[30470]---> BDD-cost:  122
c ---[30469]---> BDD-cost:  122
c ---[30468]---> BDD-cost:  122
c ---[30467]---> Sorter-cost:  544     Base: 2 2
c ---[30466]---> Sorter-cost:  544     Base: 2 2
c ---[30465]---> Sorter-cost:  544     Base: 2 2
c ---[30464]---> Sorter-cost:  544     Base: 2 2
c ---[30463]---> Sorter-cost:  544     Base: 2 2
c ---[30462]---> Sorter-cost:  544     Base: 2 2
c ---[30461]---> Sorter-cost:  544     Base: 2 2
c ---[30460]---> Sorter-cost:  544     Base: 2 2
c ---[30459]---> Sorter-cost:  544     Base: 2 2
c ---[30458]---> Sorter-cost:  544     Base: 2 2
c ---[30457]---> Sorter-cost:  544     Base: 2 2
c ---[30456]---> Sorter-cost:  544     Base: 2 2
c ---[30455]---> BDD-cost:   57
c ---[30454]---> BDD-cost:   57
c ---[30453]---> BDD-cost:   57
c ---[30452]---> BDD-cost:   57
c ---[30451]---> BDD-cost:   57
c ---[30450]---> BDD-cost:   57
c ---[30449]---> BDD-cost:   57
c ---[30448]---> BDD-cost:   57
c ---[30447]---> BDD-cost:   57
c ---[30446]---> BDD-cost:   57
c ---[30445]---> BDD-cost:   57
c ---[30444]---> BDD-cost:   57
c ---[30442]---> BDD-cost:   23
c ---[30440]---> BDD-cost:   23
c ---[30438]---> BDD-cost:   23
c ---[30436]---> BDD-cost:   23
c ---[30434]---> BDD-cost:   23
c ---[30432]---> BDD-cost:   23
c ---[30430]---> BDD-cost:   23
c ---[30428]---> BDD-cost:   23
c ---[30426]---> BDD-cost:   23
c ---[30424]---> BDD-cost:   23
c ---[30422]---> BDD-cost:   23
c ---[30420]---> BDD-cost:   23
c ---[30418]---> BDD-cost:   23
c ---[30416]---> BDD-cost:   23
c ---[30414]---> BDD-cost:   23
c ---[30412]---> BDD-cost:   23
c ---[30410]---> BDD-cost:   23
c ---[30408]---> BDD-cost:   23
c ---[30406]---> BDD-cost:   17
c ---[30404]---> BDD-cost:   17
c ---[30402]---> BDD-cost:   17
c ---[30400]---> BDD-cost:   17
c ---[30398]---> BDD-cost:   17
c ---[30396]---> BDD-cost:   17
c ---[30394]---> BDD-cost:   23
c ---[30392]---> BDD-cost:   23
c ---[30390]---> BDD-cost:   23
c ---[30388]---> BDD-cost:   23
c ---[30386]---> BDD-cost:   23
c ---[30384]---> BDD-cost:   23
c ---[30382]---> BDD-cost:   23
c ---[30380]---> BDD-cost:   23
c ---[30378]---> BDD-cost:   23
c ---[30376]---> BDD-cost:   23
c ---[30374]---> BDD-cost:   23
c ---[30372]---> BDD-cost:   23
c ---[30370]---> BDD-cost:   17
c ---[30368]---> BDD-cost:   17
c ---[30366]---> BDD-cost:   17
c ---[30364]---> BDD-cost:   17
c ---[30362]---> BDD-cost:   17
c ---[30360]---> BDD-cost:   17
c ---[30358]---> BDD-cost:   17
c ---[30356]---> BDD-cost:   17
c ---[30354]---> BDD-cost:   17
c ---[30352]---> BDD-cost:   17
c ---[30350]---> BDD-cost:   17
c ---[30348]---> BDD-cost:   17
c ---[30346]---> BDD-cost:   23
c ---[30344]---> BDD-cost:   23
c ---[30342]---> BDD-cost:   23
c ---[30340]---> BDD-cost:   23
c ---[30338]---> BDD-cost:   23
c ---[30336]---> BDD-cost:   23
c ---[30334]---> BDD-cost:   23
c ---[30332]---> BDD-cost:   23
c ---[30330]---> BDD-cost:   23
c ---[30328]---> BDD-cost:   23
c ---[30326]---> BDD-cost:   23
c ---[30324]---> BDD-cost:   23
c ---[30322]---> BDD-cost:   23
c ---[30320]---> BDD-cost:   23
c ---[30318]---> BDD-cost:   23
c ---[30316]---> BDD-cost:   23
c ---[30314]---> BDD-cost:   23
c ---[30312]---> BDD-cost:   23
c ---[30310]---> BDD-cost:   17
c ---[30308]---> BDD-cost:   17
c ---[30306]---> BDD-cost:   17
c ---[30304]---> BDD-cost:   17
c ---[30302]---> BDD-cost:   17
c ---[30300]---> BDD-cost:   17
c ---[30298]---> BDD-cost:   23
c ---[30296]---> BDD-cost:   23
c ---[30294]---> BDD-cost:   23
c ---[30292]---> BDD-cost:   23
c ---[30290]---> BDD-cost:   23
c ---[30288]---> BDD-cost:   23
c ---[30286]---> BDD-cost:   23
c ---[30284]---> BDD-cost:   23
c ---[30282]---> BDD-cost:   23
c ---[30280]---> BDD-cost:   23
c ---[30278]---> BDD-cost:   23
c ---[30276]---> BDD-cost:   23
c ---[30274]---> BDD-cost:   23
c ---[30272]---> BDD-cost:   23
c ---[30270]---> BDD-cost:   23
c ---[30268]---> BDD-cost:   23
c ---[30266]---> BDD-cost:   23
c ---[30264]---> BDD-cost:   23
c ---[30262]---> BDD-cost:   23
c ---[30260]---> BDD-cost:   23
c ---[30258]---> BDD-cost:   23
c ---[30256]---> BDD-cost:   23
c ---[30254]---> BDD-cost:   23
c ---[30252]---> BDD-cost:   23
c ---[30250]---> BDD-cost:   23
c ---[30248]---> BDD-cost:   23
c ---[30246]---> BDD-cost:   23
c ---[30244]---> BDD-cost:   23
c ---[30242]---> BDD-cost:   23
c ---[30240]---> BDD-cost:   23
c ---[30238]---> BDD-cost:   23
c ---[30236]---> BDD-cost:   23
c ---[30234]---> BDD-cost:   23
c ---[30232]---> BDD-cost:   23
c ---[30230]---> BDD-cost:   23
c ---[30228]---> BDD-cost:   23
c ---[30226]---> BDD-cost:   23
c ---[30224]---> BDD-cost:   23
c ---[30222]---> BDD-cost:   23
c ---[30220]---> BDD-cost:   23
c ---[30218]---> BDD-cost:   23
c ---[30216]---> BDD-cost:   23
c ---[30214]---> BDD-cost:   23
c ---[30212]---> BDD-cost:   23
c ---[30210]---> BDD-cost:   23
c ---[30208]---> BDD-cost:   23
c ---[30206]---> BDD-cost:   23
c ---[30204]---> BDD-cost:   23
c ---[30202]---> BDD-cost:   23
c ---[30200]---> BDD-cost:   23
c ---[30198]---> BDD-cost:   23
c ---[30196]---> BDD-cost:   23
c ---[30194]---> BDD-cost:   23
c ---[30192]---> BDD-cost:   23
c ---[30190]---> BDD-cost:   23
c ---[30188]---> BDD-cost:   23
c ---[30186]---> BDD-cost:   23
c ---[30184]---> BDD-cost:   23
c ---[30182]---> BDD-cost:   23
c ---[30180]---> BDD-cost:   23
c ---[30178]---> BDD-cost:   23
c ---[30176]---> BDD-cost:   23
c ---[30174]---> BDD-cost:   23
c ---[30172]---> BDD-cost:   23
c ---[30170]---> BDD-cost:   23
c ---[30168]---> BDD-cost:   23
c ---[30166]---> BDD-cost:   23
c ---[30164]---> BDD-cost:   23
c ---[30162]---> BDD-cost:   23
c ---[30160]---> BDD-cost:   23
c ---[30158]---> BDD-cost:   23
c ---[30156]---> BDD-cost:   23
c ---[30154]---> BDD-cost:   23
c ---[30152]---> BDD-cost:   23
c ---[30150]---> BDD-cost:   23
c ---[30148]---> BDD-cost:   23
c ---[30146]---> BDD-cost:   23
c ---[30144]---> BDD-cost:   23
c ---[30142]---> BDD-cost:   23
c ---[30140]---> BDD-cost:   23
c ---[30138]---> BDD-cost:   23
c ---[30136]---> BDD-cost:   23
c ---[30134]---> BDD-cost:   23
c ---[30132]---> BDD-cost:   23
c ---[30130]---> BDD-cost:   23
c ---[30128]---> BDD-cost:   23
c ---[30126]---> BDD-cost:   23
c ---[30124]---> BDD-cost:   23
c ---[30122]---> BDD-cost:   23
c ---[30120]---> BDD-cost:   23
c ---[30118]---> BDD-cost:   17
c ---[30116]---> BDD-cost:   17
c ---[30114]---> BDD-cost:   17
c ---[30112]---> BDD-cost:   17
c ---[30110]---> BDD-cost:   17
c ---[30108]---> BDD-cost:   17
c ---[30106]---> BDD-cost:   23
c ---[30104]---> BDD-cost:   23
c ---[30102]---> BDD-cost:   23
c ---[30100]---> BDD-cost:   23
c ---[30098]---> BDD-cost:   23
c ---[30096]---> BDD-cost:   23
c ---[30095]---> BDD-cost:    9
c ---[30094]---> BDD-cost:    9
c ---[30093]---> BDD-cost:    9
c ---[30092]---> BDD-cost:    9
c ---[30091]---> BDD-cost:    9
c ---[30090]---> BDD-cost:    9
c ---[30089]---> BDD-cost:    9
c ---[30088]---> BDD-cost:    9
c ---[30087]---> BDD-cost:    9
c ---[30086]---> BDD-cost:    9
c ---[30085]---> BDD-cost:    9
c ---[30084]---> BDD-cost:    9
c ---[30083]---> BDD-cost:    9
c ---[30082]---> BDD-cost:    9
c ---[30081]---> BDD-cost:    9
c ---[30080]---> BDD-cost:    9
c ---[30079]---> BDD-cost:    9
c ---[30078]---> BDD-cost:    9
c ---[30077]---> BDD-cost:    9
c ---[30076]---> BDD-cost:    9
c ---[30075]---> BDD-cost:    9
c ---[30074]---> BDD-cost:    9
c ---[30073]---> BDD-cost:    9
c ---[30072]---> BDD-cost:    9
c ---[30071]---> BDD-cost:    9
c ---[30070]---> BDD-cost:    9
c ---[30069]---> BDD-cost:    9
c ---[30068]---> BDD-cost:    9
c ---[30067]---> BDD-cost:    9
c ---[30066]---> BDD-cost:    9
c ---[30065]---> BDD-cost:    9
c ---[30064]---> BDD-cost:    9
c ---[30063]---> BDD-cost:    9
c ---[30062]---> BDD-cost:    9
c ---[30061]---> BDD-cost:    9
c ---[30060]---> BDD-cost:    9
c ---[30059]---> BDD-cost:    9
c ---[30058]---> BDD-cost:    9
c ---[30057]---> BDD-cost:    9
c ---[30056]---> BDD-cost:    9
c ---[30055]---> BDD-cost:    9
c ---[30054]---> BDD-cost:    9
c ---[30053]---> BDD-cost:    9
c ---[30052]---> BDD-cost:    9
c ---[30051]---> BDD-cost:    9
c ---[30050]---> BDD-cost:    9
c ---[30049]---> BDD-cost:    9
c ---[30048]---> BDD-cost:    9
c ---[30047]---> BDD-cost:    9
c ---[30046]---> BDD-cost:    9
c ---[30045]---> BDD-cost:    9
c ---[30044]---> BDD-cost:    9
c ---[30043]---> BDD-cost:    9
c ---[30042]---> BDD-cost:    9
c ---[30041]---> BDD-cost:    9
c ---[30040]---> BDD-cost:    9
c ---[30039]---> BDD-cost:    9
c ---[30038]---> BDD-cost:    9
c ---[30037]---> BDD-cost:    9
c ---[30036]---> BDD-cost:    9
c ---[30035]---> BDD-cost:    9
c ---[30034]---> BDD-cost:    9
c ---[30033]---> BDD-cost:    9
c ---[30032]---> BDD-cost:    9
c ---[30031]---> BDD-cost:    9
c ---[30030]---> BDD-cost:    9
c ---[30029]---> BDD-cost:    9
c ---[30028]---> BDD-cost:    9
c ---[30027]---> BDD-cost:    9
c ---[30026]---> BDD-cost:    9
c ---[30025]---> BDD-cost:    9
c ---[30024]---> BDD-cost:    9
c ---[30023]---> BDD-cost:    9
c ---[30022]---> BDD-cost:    9
c ---[30021]---> BDD-cost:    9
c ---[30020]---> BDD-cost:    9
c ---[30019]---> BDD-cost:    9
c ---[30018]---> BDD-cost:    9
c ---[30017]---> BDD-cost:    9
c ---[30016]---> BDD-cost:    9
c ---[30015]---> BDD-cost:    9
c ---[30014]---> BDD-cost:    9
c ---[30013]---> BDD-cost:    9
c ---[30012]---> BDD-cost:    9
c ---[30011]---> BDD-cost:    9
c ---[30010]---> BDD-cost:    9
c ---[30009]---> BDD-cost:    9
c ---[30008]---> BDD-cost:    9
c ---[30007]---> BDD-cost:    9
c ---[30006]---> BDD-cost:    9
c ---[30005]---> BDD-cost:    9
c ---[30004]---> BDD-cost:    9
c ---[30003]---> BDD-cost:    9
c ---[30002]---> BDD-cost:    9
c ---[30001]---> BDD-cost:    9
c ---[30000]---> BDD-cost:    9
c ---[29999]---> BDD-cost:    9
c ---[29998]---> BDD-cost:    9
c ---[29997]---> BDD-cost:    9
c ---[29996]---> BDD-cost:    9
c ---[29995]---> BDD-cost:    9
c ---[29994]---> BDD-cost:    9
c ---[29993]---> BDD-cost:    9
c ---[29992]---> BDD-cost:    9
c ---[29991]---> BDD-cost:    9
c ---[29990]---> BDD-cost:    9
c ---[29989]---> BDD-cost:    9
c ---[29988]---> BDD-cost:    9
c ---[29987]---> BDD-cost:    9
c ---[29986]---> BDD-cost:    9
c ---[29985]---> BDD-cost:    9
c ---[29984]---> BDD-cost:    9
c ---[29983]---> BDD-cost:    9
c ---[29982]---> BDD-cost:    9
c ---[29981]---> BDD-cost:    9
c ---[29980]---> BDD-cost:    9
c ---[29979]---> BDD-cost:    9
c ---[29978]---> BDD-cost:    9
c ---[29977]---> BDD-cost:    9
c ---[29976]---> BDD-cost:    9
c ---[29975]---> BDD-cost:    9
c ---[29974]---> BDD-cost:    9
c ---[29973]---> BDD-cost:    9
c ---[29972]---> BDD-cost:    9
c ---[29971]---> BDD-cost:    9
c ---[29970]---> BDD-cost:    9
c ---[29969]---> BDD-cost:    9
c ---[29968]---> BDD-cost:    9
c ---[29967]---> BDD-cost:    9
c ---[29966]---> BDD-cost:    9
c ---[29965]---> BDD-cost:    9
c ---[29964]---> BDD-cost:    9
c ---[29963]---> BDD-cost:    9
c ---[29962]---> BDD-cost:    9
c ---[29961]---> BDD-cost:    9
c ---[29960]---> BDD-cost:    9
c ---[29959]---> BDD-cost:    9
c ---[29958]---> BDD-cost:    9
c ---[29957]---> BDD-cost:    9
c ---[29956]---> BDD-cost:    9
c ---[29955]---> BDD-cost:    9
c ---[29954]---> BDD-cost:    9
c ---[29953]---> BDD-cost:    9
c ---[29952]---> BDD-cost:    9
c ---[29951]---> BDD-cost:    9
c ---[29950]---> BDD-cost:    9
c ---[29949]---> BDD-cost:    9
c ---[29948]---> BDD-cost:    9
c ---[29947]---> BDD-cost:    9
c ---[29946]---> BDD-cost:    9
c ---[29945]---> BDD-cost:    9
c ---[29944]---> BDD-cost:    9
c ---[29943]---> BDD-cost:    9
c ---[29942]---> BDD-cost:    9
c ---[29941]---> BDD-cost:    9
c ---[29940]---> BDD-cost:    9
c ---[29939]---> BDD-cost:    9
c ---[29938]---> BDD-cost:    9
c ---[29937]---> BDD-cost:    9
c ---[29936]---> BDD-cost:    9
c ---[29935]---> BDD-cost:    9
c ---[29934]---> BDD-cost:    9
c ---[29933]---> BDD-cost:    9
c ---[29932]---> BDD-cost:    9
c ---[29931]---> BDD-cost:    9
c ---[29930]---> BDD-cost:    9
c ---[29929]---> BDD-cost:    9
c ---[29928]---> BDD-cost:    9
c ---[29927]---> BDD-cost:    9
c ---[29926]---> BDD-cost:    9
c ---[29925]---> BDD-cost:    9
c ---[29924]---> BDD-cost:    9
c ---[29923]---> BDD-cost:    9
c ---[29922]---> BDD-cost:    9
c ---[29921]---> BDD-cost:    9
c ---[29920]---> BDD-cost:    9
c ---[29919]---> BDD-cost:    9
c ---[29918]---> BDD-cost:    9
c ---[29917]---> BDD-cost:    9
c ---[29916]---> BDD-cost:    9
c ---[29915]---> BDD-cost:    9
c ---[29914]---> BDD-cost:    9
c ---[29913]---> BDD-cost:    9
c ---[29912]---> BDD-cost:    9
c ---[29911]---> BDD-cost:    9
c ---[29910]---> BDD-cost:    9
c ---[29909]---> BDD-cost:    9
c ---[29908]---> BDD-cost:    9
c ---[29907]---> BDD-cost:    9
c ---[29906]---> BDD-cost:    9
c ---[29905]---> BDD-cost:    9
c ---[29904]---> BDD-cost:    9
c ---[29903]---> BDD-cost:    9
c ---[29902]---> BDD-cost:    9
c ---[29901]---> BDD-cost:    9
c ---[29900]---> BDD-cost:    9
c ---[29899]---> BDD-cost:    9
c ---[29898]---> BDD-cost:    9
c ---[29897]---> BDD-cost:    9
c ---[29896]---> BDD-cost:    9
c ---[29895]---> BDD-cost:    9
c ---[29894]---> BDD-cost:    9
c ---[29893]---> BDD-cost:    9
c ---[29892]---> BDD-cost:    9
c ---[29891]---> BDD-cost:    9
c ---[29890]---> BDD-cost:    9
c ---[29889]---> BDD-cost:    9
c ---[29888]---> BDD-cost:    9
c ---[29887]---> BDD-cost:    9
c ---[29886]---> BDD-cost:    9
c ---[29885]---> BDD-cost:    9
c ---[29884]---> BDD-cost:    9
c ---[29883]---> BDD-cost:    9
c ---[29882]---> BDD-cost:    9
c ---[29881]---> BDD-cost:    9
c ---[29880]---> BDD-cost:    9
c ---[29879]---> BDD-cost:    9
c ---[29878]---> BDD-cost:    9
c ---[29877]---> BDD-cost:    9
c ---[29876]---> BDD-cost:    9
c ---[29875]---> BDD-cost:    9
c ---[29874]---> BDD-cost:    9
c ---[29873]---> BDD-cost:    9
c ---[29872]---> BDD-cost:    9
c ---[29871]---> BDD-cost:    9
c ---[29870]---> BDD-cost:    9
c ---[29869]---> BDD-cost:    9
c ---[29868]---> BDD-cost:    9
c ---[29867]---> BDD-cost:    9
c ---[29866]---> BDD-cost:    9
c ---[29865]---> BDD-cost:    9
c ---[29864]---> BDD-cost:    9
c ---[29863]---> BDD-cost:    9
c ---[29862]---> BDD-cost:    9
c ---[29861]---> BDD-cost:    9
c ---[29860]---> BDD-cost:    9
c ---[29859]---> BDD-cost:    9
c ---[29858]---> BDD-cost:    9
c ---[29857]---> BDD-cost:    9
c ---[29856]---> BDD-cost:    9
c ---[29855]---> BDD-cost:    9
c ---[29854]---> BDD-cost:    9
c ---[29853]---> BDD-cost:    9
c ---[29852]---> BDD-cost:    9
c ---[29851]---> BDD-cost:    9
c ---[29850]---> BDD-cost:    9
c ---[29849]---> BDD-cost:    9
c ---[29848]---> BDD-cost:    9
c ---[29847]---> BDD-cost:    9
c ---[29846]---> BDD-cost:    9
c ---[29845]---> BDD-cost:    9
c ---[29844]---> BDD-cost:    9
c ---[29843]---> BDD-cost:    9
c ---[29842]---> BDD-cost:    9
c ---[29841]---> BDD-cost:    9
c ---[29840]---> BDD-cost:    9
c ---[29839]---> BDD-cost:    9
c ---[29838]---> BDD-cost:    9
c ---[29837]---> BDD-cost:    9
c ---[29836]---> BDD-cost:    9
c ---[29835]---> BDD-cost:    9
c ---[29834]---> BDD-cost:    9
c ---[29833]---> BDD-cost:    9
c ---[29832]---> BDD-cost:    9
c ---[29831]---> BDD-cost:    9
c ---[29830]---> BDD-cost:    9
c ---[29829]---> BDD-cost:    9
c ---[29828]---> BDD-cost:    9
c ---[29827]---> BDD-cost:    9
c ---[29826]---> BDD-cost:    9
c ---[29825]---> BDD-cost:    9
c ---[29824]---> BDD-cost:    9
c ---[29823]---> BDD-cost:    9
c ---[29822]---> BDD-cost:    9
c ---[29821]---> BDD-cost:    9
c ---[29820]---> BDD-cost:    9
c ---[29819]---> BDD-cost:    9
c ---[29818]---> BDD-cost:    9
c ---[29817]---> BDD-cost:    9
c ---[29816]---> BDD-cost:    9
c ---[29815]---> BDD-cost:    9
c ---[29814]---> BDD-cost:    9
c ---[29813]---> BDD-cost:    9
c ---[29812]---> BDD-cost:    9
c ---[29811]---> BDD-cost:    9
c ---[29810]---> BDD-cost:    9
c ---[29809]---> BDD-cost:    9
c ---[29808]---> BDD-cost:    9
c ---[29807]---> BDD-cost:    9
c ---[29806]---> BDD-cost:    9
c ---[29805]---> BDD-cost:    9
c ---[29804]---> BDD-cost:    9
c ---[29803]---> BDD-cost:    9
c ---[29802]---> BDD-cost:    9
c ---[29801]---> BDD-cost:    9
c ---[29800]---> BDD-cost:    9
c ---[29799]---> BDD-cost:    9
c ---[29798]---> BDD-cost:    9
c ---[29797]---> BDD-cost:    9
c ---[29796]---> BDD-cost:    9
c ---[29795]---> BDD-cost:    9
c ---[29794]---> BDD-cost:    9
c ---[29793]---> BDD-cost:    9
c ---[29792]---> BDD-cost:    9
c ---[29791]---> BDD-cost:    9
c ---[29790]---> BDD-cost:    9
c ---[29789]---> BDD-cost:    9
c ---[29788]---> BDD-cost:    9
c ---[29787]---> BDD-cost:    9
c ---[29786]---> BDD-cost:    9
c ---[29785]---> BDD-cost:    9
c ---[29784]---> BDD-cost:    9
c ---[29783]---> BDD-cost:    9
c ---[29782]---> BDD-cost:    9
c ---[29781]---> BDD-cost:    9
c ---[29780]---> BDD-cost:    9
c ---[29779]---> BDD-cost:    9
c ---[29778]---> BDD-cost:    9
c ---[29777]---> BDD-cost:    9
c ---[29776]---> BDD-cost:    9
c ---[29775]---> BDD-cost:    9
c ---[29774]---> BDD-cost:    9
c ---[29773]---> BDD-cost:    9
c ---[29772]---> BDD-cost:    9
c ---[29771]---> BDD-cost:    9
c ---[29770]---> BDD-cost:    9
c ---[29769]---> BDD-cost:    9
c ---[29768]---> BDD-cost:    9
c ---[29767]---> BDD-cost:    9
c ---[29766]---> BDD-cost:    9
c ---[29765]---> BDD-cost:    9
c ---[29764]---> BDD-cost:    9
c ---[29763]---> BDD-cost:    9
c ---[29762]---> BDD-cost:    9
c ---[29761]---> BDD-cost:    9
c ---[29760]---> BDD-cost:    9
c ---[29759]---> BDD-cost:    9
c ---[29758]---> BDD-cost:    9
c ---[29757]---> BDD-cost:    9
c ---[29756]---> BDD-cost:    9
c ---[29755]---> BDD-cost:    9
c ---[29754]---> BDD-cost:    9
c ---[29753]---> BDD-cost:    9
c ---[29752]---> BDD-cost:    9
c ---[29751]---> BDD-cost:    9
c ---[29750]---> BDD-cost:    9
c ---[29749]---> BDD-cost:    9
c ---[29748]---> BDD-cost:    9
c ---[29747]---> BDD-cost:    9
c ---[29746]---> BDD-cost:    9
c ---[29745]---> BDD-cost:    9
c ---[29744]---> BDD-cost:    9
c ---[29743]---> BDD-cost:    9
c ---[29742]---> BDD-cost:    9
c ---[29741]---> BDD-cost:    9
c ---[29740]---> BDD-cost:    9
c ---[29739]---> BDD-cost:    9
c ---[29738]---> BDD-cost:    9
c ---[29737]---> BDD-cost:    9
c ---[29736]---> BDD-cost:    9
c ---[29735]---> BDD-cost:    9
c ---[29734]---> BDD-cost:    9
c ---[ 405]---> BDD-cost:    9
c ---[ 404]---> BDD-cost:    9
c ---[ 403]---> BDD-cost:    9
c ---[ 402]---> BDD-cost:    9
c ---[ 401]---> BDD-cost:    9
c ---[ 400]---> BDD-cost:    9
c ---[ 399]---> BDD-cost:    9
c ---[ 398]---> BDD-cost:    9
c ---[ 397]---> BDD-cost:    9
c ---[ 396]---> BDD-cost:    9
c ---[ 395]---> BDD-cost:    9
c ---[ 394]---> BDD-cost:    9
c ---[ 393]---> BDD-cost:    9
c ---[ 392]---> BDD-cost:    9
c ---[ 391]---> BDD-cost:    9
c ---[ 390]---> BDD-cost:    9
c ---[ 389]---> BDD-cost:    9
c ---[ 388]---> BDD-cost:    9
c ---[ 387]---> BDD-cost:    9
c ---[ 386]---> BDD-cost:    9
c ---[ 385]---> BDD-cost:    9
c ---[ 384]---> BDD-cost:    9
c ---[ 383]---> BDD-cost:    9
c ---[ 382]---> BDD-cost:    9
c ---[ 381]---> BDD-cost:    9
c ---[ 380]---> BDD-cost:    9
c ---[ 379]---> BDD-cost:    9
c ---[ 378]---> BDD-cost:    9
c ---[ 377]---> BDD-cost:    9
c ---[ 376]---> BDD-cost:    9
c ---[ 375]---> BDD-cost:    9
c ---[ 374]---> BDD-cost:    9
c ---[ 373]---> BDD-cost:    9
c ---[ 372]---> BDD-cost:    9
c ---[ 371]---> BDD-cost:    9
c ---[ 370]---> BDD-cost:    9
c ---[ 369]---> BDD-cost:    9
c ---[ 368]---> BDD-cost:    9
c ---[ 367]---> BDD-cost:    9
c ---[ 366]---> BDD-cost:    9
c ---[ 365]---> BDD-cost:    9
c ---[ 364]---> BDD-cost:    9
c ---[ 363]---> BDD-cost:    9
c ---[ 362]---> BDD-cost:    9
c ---[ 361]---> BDD-cost:    9
c ---[ 360]---> BDD-cost:    9
c ---[ 359]---> BDD-cost:    9
c ---[ 358]---> BDD-cost:    9
c ---[ 357]---> BDD-cost:    9
c ---[ 356]---> BDD-cost:    9
c ---[ 355]---> BDD-cost:    9
c ---[ 354]---> BDD-cost:    9
c ---[ 353]---> BDD-cost:    9
c ---[ 352]---> BDD-cost:    9
c ---[ 351]---> BDD-cost:    9
c ---[ 350]---> BDD-cost:    9
c ---[ 349]---> BDD-cost:    9
c ---[ 348]---> BDD-cost:    9
c ---[ 347]---> BDD-cost:    9
c ---[ 346]---> BDD-cost:    9
c ---[ 345]---> BDD-cost:    9
c ---[ 344]---> BDD-cost:    9
c ---[ 343]---> BDD-cost:    9
c ---[ 342]---> BDD-cost:    9
c ---[ 341]---> BDD-cost:    9
c ---[ 340]---> BDD-cost:    9
c ---[ 339]---> BDD-cost:    9
c ---[ 338]---> BDD-cost:    9
c ---[ 337]---> BDD-cost:    9
c ---[ 336]---> BDD-cost:    9
c ---[ 335]---> BDD-cost:    9
c ---[ 334]---> BDD-cost:    9
c ---[ 333]---> BDD-cost:    9
c ---[ 332]---> BDD-cost:    9
c ---[ 331]---> BDD-cost:    9
c ---[ 330]---> BDD-cost:    9
c ---[ 329]---> BDD-cost:    9
c ---[ 328]---> BDD-cost:    9
c ---[ 327]---> BDD-cost:    9
c ---[ 326]---> BDD-cost:    9
c ---[ 325]---> BDD-cost:    9
c ---[ 324]---> BDD-cost:    9
c ---[ 323]---> BDD-cost:    9
c ---[ 322]---> BDD-cost:    9
c ---[ 321]---> BDD-cost:    9
c ---[ 320]---> BDD-cost:    9
c ---[ 319]---> BDD-cost:    9
c ---[ 318]---> BDD-cost:    9
c ---[ 317]---> BDD-cost:    9
c ---[ 316]---> BDD-cost:    9
c ---[ 315]---> BDD-cost:    9
c ---[ 314]---> BDD-cost:    9
c ---[ 313]---> BDD-cost:    9
c ---[ 312]---> BDD-cost:    9
c ---[ 311]---> BDD-cost:    9
c ---[ 310]---> BDD-cost:    9
c ---[ 309]---> BDD-cost:    9
c ---[ 308]---> BDD-cost:    9
c ---[ 307]---> BDD-cost:    9
c ---[ 306]---> BDD-cost:    9
c ---[ 305]---> BDD-cost:    9
c ---[ 304]---> BDD-cost:    9
c ---[ 303]---> BDD-cost:    9
c ---[ 302]---> BDD-cost:    9
c ---[ 301]---> BDD-cost:    9
c ---[ 300]---> BDD-cost:    9
c ---[ 299]---> BDD-cost:    9
c ---[ 298]---> BDD-cost:    9
c ---[ 297]---> BDD-cost:    9
c ---[ 296]---> BDD-cost:    9
c ---[ 295]---> BDD-cost:    9
c ---[ 294]---> BDD-cost:    9
c ---[ 293]---> BDD-cost:    9
c ---[ 292]---> BDD-cost:    9
c ---[ 291]---> BDD-cost:    9
c ---[ 290]---> BDD-cost:    9
c ---[ 289]---> BDD-cost:    9
c ---[ 288]---> BDD-cost:    9
c ---[ 287]---> BDD-cost:    9
c ---[ 286]---> BDD-cost:    9
c ---[ 285]---> BDD-cost:    9
c ---[ 284]---> BDD-cost:    9
c ---[ 283]---> BDD-cost:    9
c ---[ 282]---> BDD-cost:    9
c ---[ 281]---> BDD-cost:    9
c ---[ 280]---> BDD-cost:    9
c ---[ 279]---> BDD-cost:    9
c ---[ 278]---> BDD-cost:    9
c ---[ 277]---> BDD-cost:    9
c ---[ 276]---> BDD-cost:    9
c ---[ 275]---> BDD-cost:    9
c ---[ 274]---> BDD-cost:    9
c ---[ 273]---> BDD-cost:    9
c ---[ 272]---> BDD-cost:    9
c ---[ 271]---> BDD-cost:    9
c ---[ 270]---> BDD-cost:    9
c ---[ 269]---> BDD-cost:    9
c ---[ 268]---> BDD-cost:    9
c ---[ 267]---> BDD-cost:    9
c ---[ 266]---> BDD-cost:    9
c ---[ 265]---> BDD-cost:    9
c ---[ 264]---> BDD-cost:    9
c ---[ 263]---> BDD-cost:    9
c ---[ 262]---> BDD-cost:    9
c ---[ 261]---> BDD-cost:    9
c ---[ 260]---> BDD-cost:    9
c ---[ 259]---> BDD-cost:    9
c ---[ 258]---> BDD-cost:    9
c ---[ 257]---> BDD-cost:    9
c ---[ 256]---> BDD-cost:    9
c ---[ 255]---> BDD-cost:    9
c ---[ 254]---> BDD-cost:    9
c ---[ 253]---> BDD-cost:    9
c ---[ 252]---> BDD-cost:    9
c ---[ 251]---> BDD-cost:    9
c ---[ 250]---> BDD-cost:    9
c ---[ 249]---> BDD-cost:    9
c ---[ 248]---> BDD-cost:    9
c ---[ 247]---> BDD-cost:    9
c ---[ 246]---> BDD-cost:    9
c ---[ 245]---> BDD-cost:    9
c ---[ 244]---> BDD-cost:    9
c ---[ 243]---> BDD-cost:    9
c ---[ 242]---> BDD-cost:    9
c ---[ 241]---> BDD-cost:    9
c ---[ 240]---> BDD-cost:    9
c ---[ 239]---> BDD-cost:    9
c ---[ 238]---> BDD-cost:    9
c ---[ 237]---> BDD-cost:    9
c ---[ 236]---> BDD-cost:    9
c ---[ 235]---> BDD-cost:    9
c ---[ 234]---> BDD-cost:    9
c ---[ 233]---> BDD-cost:    9
c ---[ 232]---> BDD-cost:    9
c ---[ 231]---> BDD-cost:    9
c ---[ 230]---> BDD-cost:    9
c ---[ 229]---> BDD-cost:    9
c ---[ 228]---> BDD-cost:    9
c ---[ 227]---> BDD-cost:    9
c ---[ 226]---> BDD-cost:    9
c ---[ 225]---> BDD-cost:    9
c ---[ 224]---> BDD-cost:    9
c ---[ 223]---> BDD-cost:    9
c ---[ 222]---> BDD-cost:    9
c ---[ 221]---> BDD-cost:    9
c ---[ 220]---> BDD-cost:    9
c ---[ 219]---> BDD-cost:    9
c ---[ 218]---> BDD-cost:    9
c ---[ 217]---> BDD-cost:    9
c ---[ 216]---> BDD-cost:    9
c ---[ 215]---> BDD-cost:    9
c ---[ 214]---> BDD-cost:    9
c ---[ 213]---> BDD-cost:    9
c ---[ 212]---> BDD-cost:    9
c ---[ 211]---> BDD-cost:    9
c ---[ 210]---> BDD-cost:    9
c ---[ 209]---> BDD-cost:    9
c ---[ 208]---> BDD-cost:    9
c ---[ 207]---> BDD-cost:    9
c ---[ 206]---> BDD-cost:    9
c ---[ 205]---> BDD-cost:    9
c ---[ 204]---> BDD-cost:    9
c ---[ 203]---> BDD-cost:    9
c ---[ 202]---> BDD-cost:    9
c ---[ 201]---> BDD-cost:    9
c ---[ 200]---> BDD-cost:    9
c ---[ 199]---> BDD-cost:    9
c ---[ 198]---> BDD-cost:    9
c ---[ 197]---> BDD-cost:    9
c ---[ 196]---> BDD-cost:    9
c ---[ 195]---> BDD-cost:    9
c ---[ 194]---> BDD-cost:    9
c ---[ 193]---> BDD-cost:    9
c ---[ 192]---> BDD-cost:    9
c ---[ 191]---> BDD-cost:    9
c ---[ 190]---> BDD-cost:    9
c ---[ 189]---> BDD-cost:    9
c ---[ 188]---> BDD-cost:    9
c ---[ 187]---> BDD-cost:    9
c ---[ 186]---> BDD-cost:    9
c ---[ 185]---> BDD-cost:    9
c ---[ 184]---> BDD-cost:    9
c ---[ 183]---> BDD-cost:    9
c ---[ 182]---> BDD-cost:    9
c ---[ 181]---> BDD-cost:    9
c ---[ 180]---> BDD-cost:    9
c ---[ 179]---> BDD-cost:    9
c ---[ 178]---> BDD-cost:    9
c ---[ 177]---> BDD-cost:    9
c ---[ 176]---> BDD-cost:    9
c ---[ 175]---> BDD-cost:    9
c ---[ 174]---> BDD-cost:    9
c ---[ 173]---> BDD-cost:    9
c ---[ 172]---> BDD-cost:    9
c ---[ 171]---> BDD-cost:    9
c ---[ 170]---> BDD-cost:    9
c ---[ 169]---> BDD-cost:    9
c ---[ 168]---> BDD-cost:    9
c ---[ 167]---> BDD-cost:    9
c ---[ 166]---> BDD-cost:    9
c ---[ 165]---> BDD-cost:    9
c ---[ 164]---> BDD-cost:    9
c ---[ 163]---> BDD-cost:    9
c ---[ 162]---> BDD-cost:    9
c ---[ 161]---> BDD-cost:    9
c ---[ 160]---> BDD-cost:    9
c ---[ 159]---> BDD-cost:    9
c ---[ 158]---> BDD-cost:    9
c ---[ 157]---> BDD-cost:    9
c ---[ 156]---> BDD-cost:    9
c ---[ 155]---> BDD-cost:    9
c ---[ 154]---> BDD-cost:    9
c ---[ 153]---> BDD-cost:    9
c ---[ 152]---> BDD-cost:    9
c ---[ 151]---> BDD-cost:    9
c ---[ 150]---> BDD-cost:    9
c ---[ 149]---> BDD-cost:    9
c ---[ 148]---> BDD-cost:    9
c ---[ 147]---> BDD-cost:    9
c ---[ 146]---> BDD-cost:    9
c ---[ 145]---> BDD-cost:    9
c ---[ 144]---> BDD-cost:    9
c ---[ 143]---> BDD-cost:    9
c ---[ 142]---> BDD-cost:    9
c ---[ 141]---> BDD-cost:    9
c ---[ 140]---> BDD-cost:    9
c ---[ 139]---> BDD-cost:    9
c ---[ 138]---> BDD-cost:    9
c ---[ 137]---> BDD-cost:    9
c ---[ 136]---> BDD-cost:    9
c ---[ 135]---> BDD-cost:    9
c ---[ 134]---> BDD-cost:    9
c ---[ 133]---> BDD-cost:    9
c ---[ 132]---> BDD-cost:    9
c ---[ 131]---> BDD-cost:    9
c ---[ 130]---> BDD-cost:    9
c ---[ 129]---> BDD-cost:    9
c ---[ 128]---> BDD-cost:    9
c ---[ 127]---> BDD-cost:    9
c ---[ 126]---> BDD-cost:    9
c ---[ 125]---> BDD-cost:    9
c ---[ 124]---> BDD-cost:    9
c ---[ 123]---> BDD-cost:    9
c ---[ 122]---> BDD-cost:    9
c ---[ 121]---> BDD-cost:    9
c ---[ 120]---> BDD-cost:    9
c ---[ 119]---> BDD-cost:    9
c ---[ 118]---> BDD-cost:    9
c ---[ 117]---> BDD-cost:    9
c ---[ 116]---> BDD-cost:    9
c ---[ 115]---> BDD-cost:    9
c ---[ 114]---> BDD-cost:    9
c ---[ 113]---> BDD-cost:    9
c ---[ 112]---> BDD-cost:    9
c ---[ 111]---> BDD-cost:    9
c ---[ 110]---> BDD-cost:    9
c ---[ 109]---> BDD-cost:    9
c ---[ 108]---> BDD-cost:    9
c ---[ 107]---> BDD-cost:    9
c ---[ 106]---> BDD-cost:    9
c ---[ 105]---> BDD-cost:    9
c ---[ 104]---> BDD-cost:    9
c ---[ 103]---> BDD-cost:    9
c ---[ 102]---> BDD-cost:    9
c ---[ 101]---> BDD-cost:    9
c ---[ 100]---> BDD-cost:    9
c ---[  99]---> BDD-cost:    9
c ---[  98]---> BDD-cost:    9
c ---[  97]---> BDD-cost:    9
c ---[  96]---> BDD-cost:    9
c ---[  95]---> BDD-cost:    9
c ---[  94]---> BDD-cost:    9
c ---[  93]---> BDD-cost:    9
c ---[  92]---> BDD-cost:    9
c ---[  91]---> BDD-cost:    9
c ---[  90]---> BDD-cost:    9
c ---[  89]---> BDD-cost:    9
c ---[  88]---> BDD-cost:    9
c ---[  87]---> BDD-cost:    9
c ---[  86]---> BDD-cost:    9
c ---[  85]---> BDD-cost:    9
c ---[  84]---> BDD-cost:    9
c ---[  83]---> BDD-cost:    9
c ---[  82]---> BDD-cost:    9
c ---[  81]---> BDD-cost:    9
c ---[  80]---> BDD-cost:    9
c ---[  79]---> BDD-cost:    9
c ---[  78]---> BDD-cost:    9
c ---[  77]---> BDD-cost:    9
c ---[  76]---> BDD-cost:    9
c ---[  75]---> BDD-cost:    9
c ---[  74]---> BDD-cost:    9
c ---[  73]---> BDD-cost:    9
c ---[  72]---> BDD-cost:    9
c ---[  71]---> BDD-cost:    9
c ---[  70]---> BDD-cost:    9
c ---[  69]---> BDD-cost:    9
c ---[  68]---> BDD-cost:    9
c ---[  67]---> BDD-cost:    9
c ---[  66]---> BDD-cost:    9
c ---[  65]---> BDD-cost:    9
c ---[  64]---> BDD-cost:    9
c ---[  63]---> BDD-cost:    9
c ---[  62]---> BDD-cost:    9
c ---[  61]---> BDD-cost:    9
c ---[  60]---> BDD-cost:    9
c ---[  59]---> BDD-cost:    9
c ---[  58]---> BDD-cost:    9
c ---[  57]---> BDD-cost:    9
c ---[  56]---> BDD-cost:    9
c ---[  55]---> BDD-cost:    9
c ---[  54]---> BDD-cost:    9
c ---[  53]---> BDD-cost:    9
c ---[  52]---> BDD-cost:    9
c ---[  51]---> BDD-cost:    9
c ---[  50]---> BDD-cost:    9
c ---[  49]---> BDD-cost:    9
c ---[  48]---> BDD-cost:    9
c ---[  47]---> BDD-cost:    9
c ---[  46]---> BDD-cost:    9
c ---[  45]---> BDD-cost:    9
c ---[  44]---> BDD-cost:    9
c ---[  43]---> BDD-cost:    9
c ---[  42]---> BDD-cost:    9
c ---[  41]---> BDD-cost:    9
c ---[  40]---> BDD-cost:    9
c ---[  39]---> BDD-cost:    9
c ---[  38]---> BDD-cost:    9
c ---[  37]---> BDD-cost:    9
c ---[  36]---> BDD-cost:    9
c ---[  35]---> BDD-cost:    9
c ---[  34]---> BDD-cost:    9
c ---[  33]---> BDD-cost:    9
c ---[  32]---> BDD-cost:    9
c ---[  31]---> BDD-cost:    9
c ---[  30]---> BDD-cost:    9
c ---[  29]---> BDD-cost:    9
c ---[  28]---> BDD-cost:    9
c ---[  27]---> BDD-cost:    9
c ---[  26]---> BDD-cost:    9
c ---[  25]---> BDD-cost:    9
c ---[  24]---> BDD-cost:    9
c ---[  23]---> BDD-cost:    9
c ---[  22]---> BDD-cost:    9
c ---[  21]---> BDD-cost:    9
c ---[  20]---> BDD-cost:    9
c ---[  19]---> BDD-cost:    9
c ---[  18]---> BDD-cost:    9
c ---[  17]---> BDD-cost:    9
c ---[  16]---> BDD-cost:    9
c ---[  15]---> BDD-cost:    9
c ---[  14]---> BDD-cost:    9
c ---[  13]---> BDD-cost:    9
c ---[  12]---> BDD-cost:    9
c ---[  11]---> BDD-cost:    9
c ---[  10]---> BDD-cost:    9
c ---[   9]---> BDD-cost:    9
c ---[   8]---> BDD-cost:    9
c ---[   7]---> BDD-cost:    9
c ---[   6]---> BDD-cost:    9
c ---[   5]---> BDD-cost:    9
c ---[   4]---> BDD-cost:    9
c ---[   3]---> BDD-cost:    9
c ---[   2]---> BDD-cost:    9
c ---[   1]---> BDD-cost:    9
c ---[   0]---> BDD-cost:    9
c =================================[SATELITE+]==================================
c |           |     ORIGINAL     |              LEARNT              |          |
c | Conflicts | Clauses Literals |   Limit Clauses Literals  Lit/Cl | Progress |
c ==============================================================================
c |         0 |   83484   228138 |   25045       0        0     nan |  0.000 % |
c   -- subsuming                       
c   -- var.elim.:  1000/25068          
c   -- var.elim.:  2000/25068          
c   -- var.elim.:  3000/25068          
c   -- var.elim.:  4000/25068          
c   -- var.elim.:  5000/25068          
c   -- var.elim.:  6000/25068          
c   -- var.elim.:  7000/25068          
c   -- var.elim.:  8000/25068          
c   -- var.elim.:  9000/25068          
c   -- var.elim.:  10000/25068          
c   -- var.elim.:  11000/25068          
c   -- var.elim.:  12000/25068          
c   -- var.elim.:  13000/25068          
c   -- var.elim.:  14000/25068          
c   -- var.elim.:  15000/25068          
c   -- var.elim.:  16000/25068          
c   -- var.elim.:  17000/25068          
c   -- var.elim.:  18000/25068          
c   -- var.elim.:  19000/25068          
c   -- var.elim.:  20000/25068          
c   -- var.elim.:  21000/25068          
c   -- var.elim.:  22000/25068          
c   -- var.elim.:  23000/25068          
c   -- var.elim.:  24000/25068          
c   -- var.elim.:  25000/25068          
c   -- var.elim.:  25068/25068          
c   -- var.elim.:  1000/10949          
c   -- var.elim.:  2000/10949          
c   -- var.elim.:  3000/10949          
c   -- var.elim.:  4000/10949          
c   -- var.elim.:  5000/10949          
c   -- var.elim.:  6000/10949          
c   -- var.elim.:  7000/10949          
c   -- var.elim.:  8000/10949          
c   -- var.elim.:  9000/10949          
c   -- var.elim.:  10000/10949          
c   -- var.elim.:  10949/10949          
c   -- var.elim.:  148/148          
c   -- subsuming                       
c   -- var.elim.:  1000/9020          
c   -- var.elim.:  2000/9020          
c   -- var.elim.:  3000/9020          
c   -- var.elim.:  4000/9020          
c   -- var.elim.:  5000/9020          
c   -- var.elim.:  6000/9020          
c   -- var.elim.:  7000/9020          
c   -- var.elim.:  8000/9020          
c   -- var.elim.:  9000/9020          
c   -- var.elim.:  9020/9020          
c   -- var.elim.:  1000/8546          
c   -- var.elim.:  2000/8546          
c   -- var.elim.:  3000/8546          
c   -- var.elim.:  4000/8546          
c   -- var.elim.:  5000/8546          
c   -- var.elim.:  6000/8546          
c   -- var.elim.:  7000/8546          
c   -- var.elim.:  8000/8546          
c   -- var.elim.:  8546/8546          
c   -- var.elim.:  116/116          
c   -- subsuming                       
c   -- var.elim.:  1000/5878          
c   -- var.elim.:  2000/5878          
c   -- var.elim.:  3000/5878          
c   -- var.elim.:  4000/5878          
c   -- var.elim.:  5000/5878          
c   -- var.elim.:  5878/5878          
c   -- var.elim.:  1000/3866          
c   -- var.elim.:  2000/3866          
c   -- var.elim.:  3000/3866          
c   -- var.elim.:  3866/3866          
c   -- subsuming                       
c   -- var.elim.:  1000/3870          
c   -- var.elim.:  2000/3870          
c   -- var.elim.:  3000/3870          
c   -- var.elim.:  3870#### 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.96 1.00 0.92 2/54 16830
Raw data (stat): 16830 (runsolver) R 16829 11931 11930 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 480568165 1052672 99 4294967295 134512640 135381576 3221224448 3221219692 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0016 s]
Raw data (loadavg): 0.97 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 5698 0 0 0 982 17 0 0 25 0 1 0 480568165 22941696 4858 4294967295 134512640 134672761 3221224560 3221223744 134615581 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 5601 4858 603 41 0 5560 0
vsize: 22404
[startup+20.0022 s]
Raw data (loadavg): 0.97 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 6946 0 0 0 1978 20 0 0 25 0 1 0 480568165 27979776 6106 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 6831 6106 603 41 0 6790 0
vsize: 27324
[startup+30.0016 s]
Raw data (loadavg): 0.98 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 7915 0 0 0 2975 23 0 0 25 0 1 0 480568165 32079872 7075 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 7832 7075 603 41 0 7791 0
vsize: 31328
[startup+40.0017 s]
Raw data (loadavg): 0.98 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 9130 0 0 0 3972 26 0 0 25 0 1 0 480568165 36978688 8290 4294967295 134512640 134672761 3221224560 3221223744 134615747 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9028 8290 603 41 0 8987 0
vsize: 36112
[startup+50.0025 s]
Raw data (loadavg): 0.98 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 10083 0 0 0 4970 29 0 0 25 0 1 0 480568165 40837120 9243 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 9970 9243 603 41 0 9929 0
vsize: 39880
[startup+60.003 s]
Raw data (loadavg): 0.98 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 10918 0 0 0 5968 31 0 0 25 0 1 0 480568165 44552192 10078 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 10877 10078 603 41 0 10836 0
vsize: 43508
[startup+70.0032 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 11715 0 0 0 6966 33 0 0 25 0 1 0 480568165 47865856 10875 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 11686 10876 603 41 0 11645 0
vsize: 46744
[startup+80.0029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 12342 0 0 0 7964 35 0 0 25 0 1 0 480568165 50372608 11502 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12298 11502 603 41 0 12257 0
vsize: 49192
[startup+90.0034 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 12947 0 0 0 8962 38 0 0 25 0 1 0 480568165 52752384 12107 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 12879 12107 603 41 0 12838 0
vsize: 51516
[startup+100.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 13516 0 0 0 9961 39 0 0 25 0 1 0 480568165 55136256 12676 4294967295 134512640 134672761 3221224560 3221223600 134612478 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 13461 12676 603 41 0 13420 0
vsize: 53844
[startup+110.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 14158 0 0 0 10959 40 0 0 25 0 1 0 480568165 57786368 13318 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14108 13318 603 41 0 14067 0
vsize: 56432
[startup+120.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 14757 0 0 0 11958 42 0 0 25 0 1 0 480568165 60174336 13917 4294967295 134512640 134672761 3221224560 3221223600 134614228 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 14691 13917 603 41 0 14650 0
vsize: 58764
[startup+130.004 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 15274 0 0 0 12957 43 0 0 25 0 1 0 480568165 62304256 14434 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15211 14434 603 41 0 15170 0
vsize: 60844
[startup+140.005 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 15724 0 0 0 13956 45 0 0 25 0 1 0 480568165 64151552 14884 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 15662 14884 603 41 0 15621 0
vsize: 62648
[startup+150.005 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 16165 0 0 0 14955 46 0 0 25 0 1 0 480568165 66007040 15325 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16115 15325 603 41 0 16074 0
vsize: 64460
[startup+160.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 16587 0 0 0 15954 47 0 0 25 0 1 0 480568165 67723264 15747 4294967295 134512640 134672761 3221224560 3221223744 134615741 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16534 15747 603 41 0 16493 0
vsize: 66136
[startup+170.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 17006 0 0 0 16954 47 0 0 25 0 1 0 480568165 69464064 16166 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 16959 16166 603 41 0 16918 0
vsize: 67836
[startup+180.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 17388 0 0 0 17953 48 0 0 25 0 1 0 480568165 70991872 16548 4294967295 134512640 134672761 3221224560 3221223744 134615807 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17332 16548 603 41 0 17291 0
vsize: 69328
[startup+190.005 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 17764 0 0 0 18952 49 0 0 25 0 1 0 480568165 72503296 16924 4294967295 134512640 134672761 3221224560 3221223744 134615681 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 17701 16924 603 41 0 17660 0
vsize: 70804
[startup+200.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 18111 0 0 0 19951 50 0 0 25 0 1 0 480568165 73969664 17271 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18059 17271 603 41 0 18018 0
vsize: 72236
[startup+210.006 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 18436 0 0 0 20951 51 0 0 25 0 1 0 480568165 75329536 17596 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 18391 17596 603 41 0 18350 0
vsize: 73564
[startup+220.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 19447 0 0 0 21949 53 0 0 25 0 1 0 480568165 79958016 18607 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 19521 18607 603 41 0 19480 0
vsize: 78084
[startup+230.007 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 19940 0 0 0 22948 54 0 0 25 0 1 0 480568165 81952768 19100 4294967295 134512640 134672761 3221224560 3221223696 134614701 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20008 19100 603 41 0 19967 0
vsize: 80032
[startup+240.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20415 0 0 0 23946 56 0 0 25 0 1 0 480568165 83927040 19575 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20490 19575 603 41 0 20449 0
vsize: 81960
[startup+250.008 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20966 0 0 0 24944 58 0 0 25 0 1 0 480568165 86646784 20126 4294967295 134512640 134672761 3221224560 3221223616 134644281 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21154 20126 603 41 0 21113 0
vsize: 84616
[startup+260.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 25944 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+270.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 26944 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223664 134604560 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+280.009 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 27944 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+290.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 28945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+300.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 29945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134616017 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+310.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 30945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+320.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 31945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+330.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 32945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615830 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+340.01 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 33945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+350.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 34945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615579 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+360.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 35945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615585 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+370.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 36945 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+380.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 37946 59 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+390.012 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 38946 60 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+400.011 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 39946 60 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+410.012 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 40946 60 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223712 134614555 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+420.013 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 20994 0 0 0 41946 60 0 0 25 0 1 0 480568165 85598208 20013 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20898 20013 603 41 0 20857 0
vsize: 83592
[startup+430.013 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 21048 0 0 0 42946 60 0 0 25 0 1 0 480568165 85860352 20067 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 20962 20067 603 41 0 20921 0
vsize: 83848
[startup+440.013 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 21463 0 0 0 43946 61 0 0 25 0 1 0 480568165 87588864 20482 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21384 20482 603 41 0 21343 0
vsize: 85536
[startup+450.013 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 21856 0 0 0 44945 62 0 0 25 0 1 0 480568165 89321472 20875 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 21807 20875 603 41 0 21766 0
vsize: 87228
[startup+460.014 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 22242 0 0 0 45944 63 0 0 25 0 1 0 480568165 90808320 21261 4294967295 134512640 134672761 3221224560 3221223744 134615693 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22170 21261 603 41 0 22129 0
vsize: 88680
[startup+470.014 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 22601 0 0 0 46942 65 0 0 25 0 1 0 480568165 92389376 21620 4294967295 134512640 134672761 3221224560 3221223744 134615727 0 0 5 16386 0 0 0 17 1 0 0
Raw data (statm): 22556 21620 603 41 0 22515 0
vsize: 90224
[startup+480.014 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 22965 0 0 0 47940 66 0 0 25 0 1 0 480568165 93843456 21984 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 22911 21984 603 41 0 22870 0
vsize: 91644
[startup+490.015 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 23252 0 0 0 48940 67 0 0 25 0 1 0 480568165 95035392 22271 4294967295 134512640 134672761 3221224560 3221223744 134615732 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23202 22271 603 41 0 23161 0
vsize: 92808
[startup+500.015 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 23560 0 0 0 49939 68 0 0 25 0 1 0 480568165 96387072 22579 4294967295 134512640 134672761 3221224560 3221223744 134615608 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23532 22579 603 41 0 23491 0
vsize: 94128
[startup+510.015 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 23888 0 0 0 50938 69 0 0 25 0 1 0 480568165 97705984 22907 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 23854 22907 603 41 0 23813 0
vsize: 95416
[startup+520.016 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 24195 0 0 0 51937 70 0 0 25 0 1 0 480568165 98889728 23214 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24143 23214 603 41 0 24102 0
vsize: 96572
[startup+530.016 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 24530 0 0 0 52936 72 0 0 25 0 1 0 480568165 100352000 23549 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24500 23549 603 41 0 24459 0
vsize: 98000
[startup+540.017 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 24823 0 0 0 53935 73 0 0 25 0 1 0 480568165 101531648 23842 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 24788 23842 603 41 0 24747 0
vsize: 99152
[startup+550.016 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 25104 0 0 0 54934 74 0 0 25 0 1 0 480568165 102711296 24123 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25076 24123 603 41 0 25035 0
vsize: 100304
[startup+560.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 25380 0 0 0 55934 74 0 0 25 0 1 0 480568165 103895040 24399 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25365 24399 603 41 0 25324 0
vsize: 101460
[startup+570.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 25675 0 0 0 56933 75 0 0 25 0 1 0 480568165 105091072 24694 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25657 24694 603 41 0 25616 0
vsize: 102628
[startup+580.018 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 25941 0 0 0 57933 76 0 0 25 0 1 0 480568165 106209280 24960 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 25930 24960 603 41 0 25889 0
vsize: 103720
[startup+590.022 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 26178 0 0 0 58933 76 0 0 25 0 1 0 480568165 107163648 25197 4294967295 134512640 134672761 3221224560 3221223600 134603565 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26163 25197 603 41 0 26122 0
vsize: 104652
[startup+600.022 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 26410 0 0 0 59932 77 0 0 25 0 1 0 480568165 108113920 25429 4294967295 134512640 134672761 3221224560 3221223744 134615804 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26395 25429 603 41 0 26354 0
vsize: 105580
[startup+610.022 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 26663 0 0 0 60932 77 0 0 25 0 1 0 480568165 109178880 25682 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26655 25682 603 41 0 26614 0
vsize: 106620
[startup+620.022 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 26905 0 0 0 61931 78 0 0 25 0 1 0 480568165 110284800 25924 4294967295 134512640 134672761 3221224560 3221223600 134612885 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 26925 25924 603 41 0 26884 0
vsize: 107700
[startup+630.023 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27164 0 0 0 62931 79 0 0 25 0 1 0 480568165 111386624 26183 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27194 26183 603 41 0 27153 0
vsize: 108776
[startup+640.023 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27456 0 0 0 63930 80 0 0 25 0 1 0 480568165 112898048 26475 4294967295 134512640 134672761 3221224560 3221223616 134644266 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27563 26475 603 41 0 27522 0
vsize: 110252
[startup+650.023 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 64930 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223696 134614685 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+660.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 65931 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+670.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 66931 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+680.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 67931 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+690.025 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 68931 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223748 1075346941 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+700.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 69931 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+710.025 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 70931 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+720.025 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 71931 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615940 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+730.025 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 72932 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+740.025 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 73932 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615828 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+750.024 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 74932 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223732 134615856 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+760.025 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 75932 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+770.026 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 76932 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615724 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+780.026 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 77932 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+790.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 78932 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615916 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+800.028 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 79933 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+810.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 80933 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+820.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 81933 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+830.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 82933 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+840.028 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 83933 80 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+850.028 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 84933 81 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615583 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+860.027 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 85933 81 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+870.028 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 86934 81 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+880.028 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 87934 81 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+890.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 88934 81 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615665 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+900.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27458 0 0 0 89934 81 0 0 25 0 1 0 480568165 112373760 26328 4294967295 134512640 134672761 3221224560 3221223744 134615921 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27435 26328 603 41 0 27394 0
vsize: 109740
[startup+910.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27599 0 0 0 90934 81 0 0 25 0 1 0 480568165 113029120 26469 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27595 26469 603 41 0 27554 0
vsize: 110380
[startup+920.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 27960 0 0 0 91933 82 0 0 25 0 1 0 480568165 114507776 26830 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 27956 26830 603 41 0 27915 0
vsize: 111824
[startup+930.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 28338 0 0 0 92932 84 0 0 25 0 1 0 480568165 116084736 27208 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28341 27208 603 41 0 28300 0
vsize: 113364
[startup+940.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 28661 0 0 0 93931 85 0 0 25 0 1 0 480568165 117411840 27531 4294967295 134512640 134672761 3221224560 3221223744 134615791 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 28665 27531 603 41 0 28624 0
vsize: 114660
[startup+950.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 29014 0 0 0 94930 86 0 0 25 0 1 0 480568165 118861824 27884 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29019 27884 603 41 0 28978 0
vsize: 116076
[startup+960.029 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 29381 0 0 0 95929 87 0 0 25 0 1 0 480568165 120442880 28251 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29405 28251 603 41 0 29364 0
vsize: 117620
[startup+970.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 29736 0 0 0 96928 88 0 0 25 0 1 0 480568165 121901056 28606 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 29761 28606 603 41 0 29720 0
vsize: 119044
[startup+980.031 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 30056 0 0 0 97928 88 0 0 25 0 1 0 480568165 123232256 28926 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30086 28926 603 41 0 30045 0
vsize: 120344
[startup+990.032 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 30429 0 0 0 98927 90 0 0 25 0 1 0 480568165 124678144 29299 4294967295 134512640 134672761 3221224560 3221223744 134615564 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30439 29299 603 41 0 30398 0
vsize: 121756
[startup+1000.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 30805 0 0 0 99926 91 0 0 25 0 1 0 480568165 126308352 29675 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 30837 29675 603 41 0 30796 0
vsize: 123348
[startup+1010.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 31210 0 0 0 100925 92 0 0 25 0 1 0 480568165 127893504 30080 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31224 30080 603 41 0 31183 0
vsize: 124896
[startup+1020.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 31563 0 0 0 101924 93 0 0 25 0 1 0 480568165 129351680 30433 4294967295 134512640 134672761 3221224560 3221223552 134565073 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31580 30433 603 41 0 31539 0
vsize: 126320
[startup+1030.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 31875 0 0 0 102923 94 0 0 25 0 1 0 480568165 130674688 30745 4294967295 134512640 134672761 3221224560 3221223744 134615627 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 31903 30745 603 41 0 31862 0
vsize: 127612
[startup+1040.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 32216 0 0 0 103923 95 0 0 25 0 1 0 480568165 131993600 31086 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32225 31086 603 41 0 32184 0
vsize: 128900
[startup+1050.03 s]
Raw data (loadavg): 0.99 1.00 0.92 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 32547 0 0 0 104922 96 0 0 25 0 1 0 480568165 133320704 31417 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32549 31417 603 41 0 32508 0
vsize: 130196
[startup+1060.03 s]
Raw data (loadavg): 1.07 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 32861 0 0 0 105921 97 0 0 25 0 1 0 480568165 134635520 31731 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 32870 31731 603 41 0 32829 0
vsize: 131480
[startup+1070.03 s]
Raw data (loadavg): 1.06 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33213 0 0 0 106920 98 0 0 25 0 1 0 480568165 136089600 32083 4294967295 134512640 134672761 3221224560 3221223744 134615619 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33225 32083 603 41 0 33184 0
vsize: 132900
[startup+1080.03 s]
Raw data (loadavg): 1.05 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 107920 98 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1090.04 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 108920 98 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615833 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1100.03 s]
Raw data (loadavg): 1.04 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 109920 98 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1110.03 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 110920 98 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1120.04 s]
Raw data (loadavg): 1.03 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 111921 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615663 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1130.04 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 112921 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1140.04 s]
Raw data (loadavg): 1.02 1.01 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 113921 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615708 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1150.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 114921 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615794 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1160.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 115921 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223600 134614333 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1170.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 116921 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615736 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1180.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 117921 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1190.04 s]
Raw data (loadavg): 1.01 1.00 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 118922 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223600 134612978 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
[startup+1200.04 s]
Raw data (loadavg): 1.00 1.00 0.93 2/54 16830
Raw data (stat): 16830 (minisat+) R 16829 11931 11930 0 -1 0 33586 0 0 0 119922 99 0 0 25 0 1 0 480568165 136638464 32254 4294967295 134512640 134672761 3221224560 3221223744 134615625 0 0 5 16386 0 0 0 17 0 0 0
Raw data (statm): 33359 32254 603 41 0 33318 0
vsize: 133436
Maximum CPU time exceeded: sending SIGTERM and SIGKILL
[startup+1200.1 s]
Raw data (loadavg): 1.00 1.00 0.93 1/54 16830
Raw data (stat): 16830 (minisat+) Z 16829 11931 11930 0 -1 12 33586 0 0 0 119922 105 0 0 25 0 1 0 480568165 0 0 4294967295 0 0 0 0 0 0 16384 5 16386 3222412051 0 0 17 1 0 0
Raw data (statm): 0 0 0 0 0 0 0
vsize: 0
Maximum CPU time exceeded: sending SIGTERM and SIGKILL

Child status: 0
Real time (s): 1200.1
CPU time (s): 1200.28
CPU user time (s): 1199.22
CPU system time (s): 1.05684
CPU usage (%): 100.015
Max. virtual memory (Kb): 133436
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####