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/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-greenbeb.opb
MD5SUM	32c6aa90779c7f105af21c4a840e4d92
Bench Category	optimization, big integers (OPTBIGINT)
Has Objective Function	YES
Satisfiable	NO
(Un)Satisfiability was proved
Best value of the objective function
Optimality of the best value was proved
Number of terms in the objective function	10569
Biggest coefficient in the objective function	524288000000
Number of bits for the biggest coefficient in the objective function	39
Sum of the numbers in the objective function	20687385806400
Number of bits of the sum of numbers in the objective function	45
Biggest number in a constraint	524288000000
Number of bits of the biggest number in a constraint	39
Biggest sum of numbers in a constraint	23881563011625
Number of bits of the biggest sum of numbers	45
Best result obtained on this benchmark	UNSAT
Best CPU time to get the best result obtained on this benchmark	0.949854
Number of variables	104157
Total number of constraints	2676
Number of constraints which are clauses	0
Number of constraints which are cardinality constraints (but not clauses)	0
Number of constraints which are nor clauses,nor cardinality constraints	2676
Minimum length of a constraint	8
Maximum length of a constraint	4848
Trace number 31038

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc27 THE 2005-05-25 21:31:30 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22406 boxname=wulflinc27 idbench=1222 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  32c6aa90779c7f105af21c4a840e4d92  /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-greenbeb.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-greenbeb.opb
IDLAUNCH: 22406
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 3
cpu MHz		: 451.169
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.169
cache size	: 512 KB
fdiv_bug	: no
hlt_bug		: no
f00f_bug	: no
coma_bug	: no
fpu		: yes
fpu_exception	: yes
cpuid level	: 2
wp		: yes
flags		: fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse
bogomips	: 899.07

/proc/meminfo:
MemTotal:      1034660 kB
MemFree:        881720 kB
Buffers:         12616 kB
Cached:         118556 kB
SwapCached:        612 kB
Active:          29448 kB
Inactive:       103788 kB
HighTotal:      131008 kB
HighFree:        17164 kB
LowTotal:       903652 kB
LowFree:        864556 kB
SwapTotal:     2097892 kB
SwapFree:      2096360 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5072 kB
Slab:            13976 kB
Committed_AS:    63600 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1368 kB
VmallocChunk:   113252 kB
JOB ENDED THE 2005-05-25 21:52:00 (client local time) WITH STATUS 152 IN 1229.91 SECONDS
stats: 22406 7 1229.91 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4201 PB-constraints to clauses...
c   -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssssssssss
c ---[4255]---> BDD-cost:   17
c ---[4250]---> BDD-cost:   15
c ---[4249]---> BDD-cost:   14
c ---[4248]---> BDD-cost:   18
c ---[4247]---> BDD-cost:   15
c ---[4245]---> BDD-cost:   14
c ---[4244]---> BDD-cost:   16
c ---[4243]---> BDD-cost:   13
c ---[4242]---> BDD-cost:   13
c ---[4238]---> BDD-cost:   13
c ---[4236]---> BDD-cost:   10
c ---[4235]---> BDD-cost:   12
c ---[4234]---> BDD-cost:    8
c ---[4233]---> BDD-cost:   12
c ---[4232]---> BDD-cost:   12
c ---[4231]---> BDD-cost:    9
c ---[4229]---> BDD-cost:   13
c ---[4226]---> BDD-cost:   15
c ---[4223]---> BDD-cost:    9
c ---[4222]---> BDD-cost:   16
c ---[4221]---> BDD-cost:   12
c ---[4220]---> BDD-cost:   13
c ---[4219]---> BDD-cost:   14
c ---[4218]---> BDD-cost:   12
c ---[4217]---> BDD-cost:   15
c ---[4216]---> BDD-cost:   12
c ---[4214]---> BDD-cost:    9
c ---[4212]---> BDD-cost:   12
c ---[4211]---> BDD-cost:   11
c ---[4210]---> BDD-cost:   11
c ---[4209]---> BDD-cost:   12
c ---[4208]---> BDD-cost:   14
c ---[4205]---> BDD-cost:   19
c ---[4204]---> BDD-cost:   12
c ---[4203]---> BDD-cost:   16
c ---[4201]---> BDD-cost:   16
c ---[4200]---> BDD-cost:   10
c ---[4199]---> BDD-cost:   17
c ---[4198]---> BDD-cost:   14
c ---[4197]---> BDD-cost:   14
c ---[4195]---> BDD-cost:   17
c ---[4194]---> BDD-cost:   15
c ---[4193]---> BDD-cost:   16
c ---[4192]---> BDD-cost:   14
c ---[4191]---> BDD-cost:   13
c ---[4190]---> BDD-cost:    7
c ---[4189]---> BDD-cost:   11
c ---[4187]---> BDD-cost:    7
c ---[4186]---> BDD-cost:   13
c ---[4185]---> BDD-cost:   12
c ---[4184]---> BDD-cost:    9
c ---[4182]---> BDD-cost:   13
c ---[4181]---> BDD-cost:   12
c ---[4180]---> BDD-cost:   15
c ---[4179]---> BDD-cost:   17
c ---[4178]---> BDD-cost:   20
c ---[4177]---> BDD-cost:   14
c ---[4176]---> BDD-cost:   13
c ---[4175]---> BDD-cost:   17
c ---[4173]---> BDD-cost:    9
c ---[4172]---> BDD-cost:   17
c ---[4171]---> BDD-cost:   11
c ---[4170]---> BDD-cost:   18
c ---[4169]---> BDD-cost:   15
c ---[4167]---> BDD-cost:   16
c ---[4166]---> BDD-cost:   16
c ---[4165]---> BDD-cost:   15
c ---[4164]---> BDD-cost:   17
c ---[4161]---> BDD-cost:    7
c ---[4160]---> BDD-cost:   11
c ---[4158]---> BDD-cost:    7
c ---[4157]---> BDD-cost:   14
c ---[4156]---> BDD-cost:   13
c ---[4155]---> BDD-cost:    8
c ---[4154]---> BDD-cost:   13
c ---[4153]---> BDD-cost:   14
c ---[4152]---> BDD-cost:   13
c ---[4151]---> BDD-cost:   14
c ---[4150]---> BDD-cost:   13
c ---[4149]---> BDD-cost:   14
c ---[4148]---> BDD-cost:   15
c ---[4147]---> BDD-cost:   19
c ---[4146]---> BDD-cost:   16
c ---[4145]---> BDD-cost:   16
c ---[4143]---> BDD-cost:   15
c ---[4142]---> BDD-cost:   17
c ---[4141]---> BDD-cost:   13
c ---[4140]---> BDD-cost:   16
c ---[4139]---> BDD-cost:   16
c ---[4138]---> BDD-cost:   16
c ---[4137]---> BDD-cost:   15
c ---[4136]---> BDD-cost:   16
c ---[4134]---> BDD-cost:   15
c ---[4133]---> BDD-cost:   16
c ---[4131]---> BDD-cost:   12
c ---[4130]---> BDD-cost:   16
c ---[4129]---> BDD-cost:   15
c ---[4128]---> BDD-cost:   13
c ---[4127]---> BDD-cost:   12
c ---[4126]---> BDD-cost:   11
c ---[4125]---> BDD-cost:   11
c ---[4124]---> BDD-cost:   12
c ---[4123]---> BDD-cost:   11
c ---[4122]---> BDD-cost:   12
c ---[4121]---> BDD-cost:   11
c ---[4120]---> BDD-cost:   12
c ---[4119]---> BDD-cost:   11
c ---[4118]---> BDD-cost:   11
c ---[4117]---> BDD-cost:   12
c ---[4116]---> BDD-cost:   12
c ---[4114]---> BDD-cost:   18
c ---[4111]---> BDD-cost:   14
c ---[4110]---> BDD-cost:   15
c ---[4107]---> BDD-cost:   16
c ---[4106]---> BDD-cost:   13
c ---[4105]---> BDD-cost:   15
c ---[4104]---> BDD-cost:   16
c ---[4103]---> BDD-cost:   17
c ---[4101]---> BDD-cost:   13
c ---[4100]---> BDD-cost:   12
c ---[4098]---> BDD-cost:   10
c ---[4097]---> BDD-cost:   12
c ---[4095]---> BDD-cost:   11
c ---[4093]---> BDD-cost:   12
c ---[4092]---> BDD-cost:   14
c ---[4091]---> BDD-cost:   13
c ---[4088]---> BDD-cost:   12
c ---[4087]---> BDD-cost:    9
c ---[4083]---> BDD-cost:   10
c ---[4078]---> BDD-cost:   12
c ---[4077]---> BDD-cost:   16
c ---[4076]---> BDD-cost:   17
c ---[4075]---> BDD-cost:   14
c ---[4073]---> BDD-cost:   13
c ---[4072]---> BDD-cost:   15
c ---[4071]---> BDD-cost:   16
c ---[4070]---> BDD-cost:   10
c ---[4069]---> BDD-cost:   17
c ---[4067]---> BDD-cost:   16
c ---[4066]---> BDD-cost:   16
c ---[4064]---> BDD-cost:   13
c ---[4063]---> BDD-cost:   18
c ---[4062]---> BDD-cost:   14
c ---[4061]---> BDD-cost:   12
c ---[4060]---> BDD-cost:   12
c ---[4059]---> BDD-cost:   13
c ---[4058]---> BDD-cost:    7
c ---[4056]---> BDD-cost:   13
c ---[4055]---> BDD-cost:    9
c ---[4054]---> BDD-cost:    9
c ---[4053]---> BDD-cost:   13
c ---[4052]---> BDD-cost:   12
c ---[4051]---> BDD-cost:   17
c ---[4050]---> BDD-cost:   14
c ---[4049]---> BDD-cost:   11
c ---[4047]---> BDD-cost:   15
c ---[4046]---> BDD-cost:   19
c ---[4045]---> BDD-cost:   20
c ---[4043]---> BDD-cost:   15
c ---[4042]---> BDD-cost:   16
c ---[4041]---> BDD-cost:   18
c ---[4039]---> BDD-cost:   18
c ---[4038]---> BDD-cost:   13
c ---[4036]---> BDD-cost:   18
c ---[4035]---> BDD-cost:   15
c ---[4033]---> BDD-cost:   15
c ---[4032]---> BDD-cost:   15
c ---[4030]---> BDD-cost:   17
c ---[4029]---> BDD-cost:   14
c ---[4028]---> BDD-cost:   13
c ---[4026]---> BDD-cost:    7
c ---[4025]---> BDD-cost:   15
c ---[4024]---> BDD-cost:   13
c ---[4023]---> BDD-cost:   12
c ---[4022]---> BDD-cost:   12
c ---[4021]---> BDD-cost:   14
c ---[4020]---> BDD-cost:   12
c ---[4019]---> BDD-cost:   19
c ---[4018]---> BDD-cost:   17
c ---[4015]---> BDD-cost:   16
c ---[4014]---> BDD-cost:   18
c ---[4013]---> BDD-cost:   14
c ---[4012]---> BDD-cost:   15
c ---[4011]---> BDD-cost:   15
c ---[4010]---> BDD-cost:   16
c ---[4008]---> BDD-cost:   16
c ---[4006]---> BDD-cost:   15
c ---[4005]---> BDD-cost:   15
c ---[4002]---> BDD-cost:   13
c ---[4001]---> BDD-cost:   17
c ---[3999]---> BDD-cost:   11
c ---[3998]---> BDD-cost:   12
c ---[3997]---> BDD-cost:   10
c ---[3996]---> BDD-cost:    7
c ---[3995]---> BDD-cost:   13
c ---[3994]---> BDD-cost:   11
c ---[3993]---> BDD-cost:    7
c ---[3992]---> BDD-cost:    9
c ---[3991]---> BDD-cost:   12
c ---[3990]---> BDD-cost:   12
c ---[3987]---> BDD-cost:   11
c ---[3985]---> BDD-cost:   13
c ---[3984]---> BDD-cost:   17
c ---[3983]---> BDD-cost:   13
c ---[3981]---> BDD-cost:   11
c ---[3980]---> BDD-cost:   15
c ---[3979]---> BDD-cost:   13
c ---[3978]---> BDD-cost:   11
c ---[3977]---> BDD-cost:    7
c ---[3976]---> BDD-cost:    8
c ---[3975]---> BDD-cost:   13
c ---[3974]---> BDD-cost:   14
c ---[3973]---> BDD-cost:   11
c ---[3970]---> BDD-cost:   10
c ---[3969]---> BDD-cost:    8
c ---[3967]---> BDD-cost:   13
c ---[3965]---> BDD-cost:   16
c ---[3963]---> Sorter-cost: 1986     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3961]---> Adder-cost: 561   maxlim: 185088   bits: 19/18
c ---[3959]---> Adder-cost: 902   maxlim: 1253375   bits: 22/21
c ---[3957]---> Adder-cost: 561   maxlim: 144640   bits: 19/18
c ---[3955]---> Sorter-cost: 3380     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3953]---> Adder-cost: 529   maxlim: 83200   bits: 18/17
c ---[3951]---> Sorter-cost: 3060     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3949]---> Sorter-cost: 2120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3947]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3945]---> Adder-cost: 300   maxlim: 70784   bits: 18/17
c ---[3943]---> BDD-cost:  170
c ---[3941]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3939]---> Sorter-cost:  350     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3937]---> BDD-cost:   65
c ---[3935]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3933]---> Adder-cost: 593   maxlim: 438656   bits: 20/19
c ---[3931]---> Adder-cost: 593   maxlim: 316416   bits: 20/19
c ---[3929]---> BDD-cost:   58
c ---[3927]---> Sorter-cost: 1562     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3925]---> Adder-cost: 561   maxlim: 176000   bits: 19/18
c ---[3923]---> Sorter-cost: 1020     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3921]---> Adder-cost: 561   maxlim: 220032   bits: 19/18
c ---[3917]---> Sorter-cost: 3009     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3915]---> Adder-cost: 318   maxlim: 164992   bits: 19/18
c ---[3913]---> Sorter-cost: 2948     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3911]---> Sorter-cost: 3379     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3909]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3907]---> Adder-cost: 375   maxlim: 60160   bits: 17/16
c ---[3905]---> BDD-cost:   75
c ---[3903]---> Adder-cost: 300   maxlim: 125440   bits: 18/17
c ---[3901]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3899]---> Sorter-cost: 1388     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3897]---> Sorter-cost: 2121     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3895]---> BDD-cost:   75
c ---[3893]---> Sorter-cost: 1843     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3891]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3889]---> BDD-cost:  166
c ---[3887]---> BDD-cost:   58
c ---[3885]---> BDD-cost:   58
c ---[3883]---> Adder-cost: 293   maxlim: 27776   bits: 16/15
c ---[3881]---> BDD-cost:   24
c ---[3879]---> BDD-cost:   50
c ---[3869]---> BDD-cost:   24
c ---[3867]---> BDD-cost:   98
c ---[3865]---> BDD-cost:   50
c ---[3863]---> BDD-cost:   20
c ---[3861]---> BDD-cost:   20
c ---[3859]---> BDD-cost:   20
c ---[3857]---> BDD-cost:   20
c ---[3847]---> BDD-cost:   24
c ---[3845]---> BDD-cost:   98
c ---[3843]---> BDD-cost:   50
c ---[3835]---> Sorter-cost: 1815     Base: 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 2
c ---[3833]---> Sorter-cost: 4725     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[3831]---> Sorter-cost: 4718     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3829]---> Sorter-cost: 4748     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3827]---> Sorter-cost: 4702     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3823]---> Sorter-cost: 2732     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3815]---> Sorter-cost: 2782     Base: 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2
c ---[3813]---> Sorter-cost: 4287     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3811]---> Sorter-cost: 4317     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3809]---> Sorter-cost: 4269     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3807]---> Sorter-cost: 4269     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3803]---> Sorter-cost: 3658     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3795]---> Sorter-cost: 1467     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2
c ---[3793]---> Sorter-cost: 2951     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3791]---> Sorter-cost: 2981     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3789]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3787]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3783]---> Sorter-cost: 1762     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2
c ---[3775]---> BDD-cost:  507
c ---[3773]---> Sorter-cost: 4615     Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2
c ---[3771]---> Sorter-cost: 4645     Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2
c ---[3769]---> Sorter-cost: 4597     Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3767]---> Sorter-cost: 4597     Base: 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3763]---> Sorter-cost: 3580     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 5 2 7 2 2
c ---[3755]---> Sorter-cost: 2782     Base: 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2
c ---[3753]---> Sorter-cost: 4018     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3751]---> Sorter-cost: 4048     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3749]---> Sorter-cost: 4000     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3747]---> Sorter-cost: 4000     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3743]---> Sorter-cost: 3370     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 7 2 2
c ---[3733]---> BDD-cost:   53
c ---[3731]---> BDD-cost:   53
c ---[3727]---> Sorter-cost: 1882     Base: 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2 2
c ---[3725]---> Sorter-cost: 3212     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3723]---> Sorter-cost: 3242     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3721]---> Sorter-cost: 3196     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3719]---> Sorter-cost: 3196     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3715]---> Sorter-cost: 2296     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 7 2 2
c ---[3707]---> BDD-cost:  330
c ---[3705]---> Sorter-cost: 3910     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[3703]---> Sorter-cost: 3899     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3701]---> Sorter-cost: 3929     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3699]---> Sorter-cost: 3881     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3695]---> Sorter-cost: 3755     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 7
c ---[3687]---> BDD-cost:  330
c ---[3685]---> Sorter-cost: 4355     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5
c ---[3683]---> Sorter-cost: 4342     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3681]---> Sorter-cost: 4362     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3679]---> Sorter-cost: 4362     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3675]---> Sorter-cost: 3084     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3667]---> BDD-cost:  342
c ---[3665]---> Sorter-cost: 4200     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3663]---> Sorter-cost: 4220     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3661]---> Sorter-cost: 4220     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3659]---> Sorter-cost: 4220     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3655]---> Sorter-cost: 2940     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3647]---> BDD-cost:  330
c ---[3645]---> Sorter-cost: 3476     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3643]---> Sorter-cost: 3506     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3641]---> Sorter-cost: 3458     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3639]---> Sorter-cost: 3458     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3635]---> Sorter-cost: 3165     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 7
c ---[3627]---> BDD-cost:  330
c ---[3625]---> Sorter-cost: 3946     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3623]---> Sorter-cost: 3966     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3621]---> Sorter-cost: 3966     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3619]---> Sorter-cost: 3966     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3615]---> Sorter-cost: 2863     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3607]---> Sorter-cost: 2717     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[3605]---> BDD-cost:  129
c ---[3601]---> Sorter-cost: 2385     Base: 2 2 2 2 2 2 2 2 3 3 3 2 2 2 2 2 2 2
c ---[3599]---> Sorter-cost: 4206     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3597]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3595]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3593]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3589]---> Sorter-cost: 2999     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3581]---> Sorter-cost: 4674     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 3 2 3 11 2 2 2
c ---[3579]---> Adder-cost: 548   maxlim: 163444290   bits: 29/28
c ---[3577]---> Adder-cost: 668   maxlim: 1961358914   bits: 32/31
c ---[3575]---> Adder-cost: 616   maxlim: 653784642   bits: 31/30
c ---[3573]---> Adder-cost: 468   maxlim: 1307573025   bits: 32/31
c ---[3571]---> Sorter-cost: 4211     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 3 2 3 11 2 2 2
c ---[3569]---> BDD-cost:  447
c ---[3567]---> Adder-cost: 460   maxlim: 46923418   bits: 27/26
c ---[3565]---> Adder-cost: 544   maxlim: 375389850   bits: 30/29
c ---[3563]---> Adder-cost: 488   maxlim: 70385306   bits: 28/27
c ---[3561]---> BDD-cost:  254
c ---[3559]---> Sorter-cost: 1815     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3557]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3555]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3553]---> Adder-cost: 390   maxlim: 1301281575   bits: 32/31
c ---[3551]---> Adder-cost: 456   maxlim: 162657870   bits: 29/28
c ---[3549]---> Adder-cost: 560   maxlim: 2602563150   bits: 32/32
c ---[3547]---> Adder-cost: 512   maxlim: 650638926   bits: 31/30
c ---[3545]---> Adder-cost: 390   maxlim: 1301281575   bits: 32/31
c ---[3543]---> Adder-cost: 370   maxlim: 650640167   bits: 31/30
c ---[3541]---> BDD-cost:  450
c ---[3539]---> Adder-cost: 334   maxlim: 40370022   bits: 27/26
c ---[3537]---> Adder-cost: 358   maxlim: 161480550   bits: 28/28
c ---[3535]---> Adder-cost: 358   maxlim: 161480550   bits: 28/28
c ---[3533]---> Adder-cost: 330   maxlim: 162659111   bits: 29/28
c ---[3531]---> Sorter-cost: 5540     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2
c ---[3529]---> BDD-cost:  181
c ---[3527]---> Sorter-cost: 3779     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2
c ---[3525]---> BDD-cost:  615
c ---[3523]---> BDD-cost:  340
c ---[3519]---> BDD-cost:  154
c ---[3517]---> Sorter-cost: 2847     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3515]---> Sorter-cost: 3405     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3513]---> Sorter-cost: 3114     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3509]---> Sorter-cost: 5380     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3507]---> BDD-cost:  154
c ---[3505]---> Sorter-cost: 3650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3503]---> BDD-cost:  517
c ---[3501]---> Sorter-cost: 3650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3499]---> Sorter-cost: 3650     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3497]---> BDD-cost:  288
c ---[3495]---> Sorter-cost: 3502     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 5 2 2 2 2 2 2
c ---[3493]---> Sorter-cost: 4188     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3491]---> BDD-cost:  278
c ---[3489]---> Sorter-cost: 4188     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3487]---> Sorter-cost: 3638     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3485]---> Sorter-cost: 4022     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3483]---> BDD-cost:  463
c ---[3481]---> Sorter-cost: 3748     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[3479]---> Sorter-cost: 2140     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3477]---> Sorter-cost: 3598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 2
c ---[3475]---> Sorter-cost: 4750     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3473]---> Sorter-cost: 4498     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 2
c ---[3471]---> Sorter-cost: 2140     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3469]---> Sorter-cost: 2006     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3467]---> Sorter-cost: 1814     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3465]---> Sorter-cost: 1604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3457]---> Sorter-cost: 3521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2
c ---[3455]---> Adder-cost: 392   maxlim: 15007286   bits: 25/24
c ---[3453]---> Adder-cost: 510   maxlim: 480247350   bits: 30/29
c ---[3451]---> Adder-cost: 470   maxlim: 120061494   bits: 28/27
c ---[3449]---> Sorter-cost: 3521     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2
c ---[3447]---> Sorter-cost: 3264     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3445]---> Sorter-cost: 2793     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2
c ---[3443]---> Sorter-cost: 2778     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3441]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3439]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3437]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3435]---> Sorter-cost: 5758     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2
c ---[3433]---> BDD-cost:  173
c ---[3431]---> Adder-cost: 406   maxlim: 2778196813   bits: 33/32
c ---[3429]---> BDD-cost:  607
c ---[3427]---> BDD-cost:  333
c ---[3423]---> BDD-cost:  172
c ---[3419]---> Sorter-cost: 6191     Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3417]---> BDD-cost:  286
c ---[3415]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3413]---> Sorter-cost: 4380     Base: 2 2 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3411]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3409]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3407]---> BDD-cost:  421
c ---[3405]---> Sorter-cost: 5086     Base: 2 2 2 2 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2
c ---[3403]---> Sorter-cost: 3252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3401]---> BDD-cost:  451
c ---[3399]---> Sorter-cost: 3252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3397]---> Sorter-cost: 2893     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 3
c ---[3395]---> Sorter-cost: 3252     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3393]---> Sorter-cost: 2610     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3391]---> Sorter-cost: 3036     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2
c ---[3389]---> Sorter-cost: 3602     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 3
c ---[3387]---> Adder-cost: 590   maxlim: 10524019642   bits: 34/34
c ---[3385]---> BDD-cost:  540
c ---[3383]---> Sorter-cost: 4093     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 13 2 2 2 2 2 2 2
c ---[3381]---> BDD-cost:  612
c ---[3379]---> BDD-cost:  131
c ---[3377]---> Sorter-cost: 2923     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 3
c ---[3375]---> Sorter-cost: 3524     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2
c ---[3373]---> Sorter-cost: 2962     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2
c ---[3371]---> BDD-cost:  105
c ---[3363]---> Adder-cost: 384   maxlim: 7049569725   bits: 34/33
c ---[3361]---> Adder-cost: 634   maxlim: 14099139450   bits: 35/34
c ---[3359]---> BDD-cost:  540
c ---[3357]---> Adder-cost: 384   maxlim: 7049569725   bits: 34/33
c ---[3355]---> Adder-cost: 364   maxlim: 3524781501   bits: 33/32
c ---[3353]---> BDD-cost:  131
c ---[3351]---> Sorter-cost: 5168     Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3
c ---[3349]---> Sorter-cost: 5682     Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3347]---> Sorter-cost: 5682     Base: 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3345]---> BDD-cost:  340
c ---[3343]---> Sorter-cost: 6568     Base: 2 2 2 2 2 5 5 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3341]---> Sorter-cost: 3886     Base: 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[3339]---> BDD-cost:  510
c ---[3337]---> Sorter-cost: 3176     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[3335]---> BDD-cost:   89
c ---[3333]---> BDD-cost:  373
c ---[3331]---> Sorter-cost: 3678     Base: 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2
c ---[3329]---> Sorter-cost: 4232     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2
c ---[3327]---> Sorter-cost: 3956     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 5 2 2 2 2 2
c ---[3323]---> Adder-cost: 462   maxlim: 122158638   bits: 28/27
c ---[3321]---> Adder-cost: 514   maxlim: 488635950   bits: 30/29
c ---[3319]---> Adder-cost: 514   maxlim: 488635950   bits: 30/29
c ---[3317]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3315]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3313]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3311]---> BDD-cost:   65
c ---[3309]---> BDD-cost:   75
c ---[3307]---> Sorter-cost: 2001     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[3305]---> Sorter-cost: 2265     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[3303]---> Sorter-cost: 2133     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2
c ---[3301]---> Sorter-cost: 2223     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2
c ---[3299]---> Sorter-cost: 2491     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2
c ---[3297]---> Sorter-cost: 2357     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 7 2 2
c ---[3295]---> Sorter-cost:  868     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3293]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3291]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3289]---> Sorter-cost: 4366     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3287]---> Sorter-cost: 3277     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2
c ---[3285]---> Sorter-cost: 3277     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2
c ---[3283]---> Sorter-cost: 3501     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2
c ---[3281]---> Sorter-cost: 3277     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2
c ---[3279]---> Sorter-cost: 3004     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2 2
c ---[3277]---> BDD-cost:  595
c ---[3275]---> BDD-cost:  530
c ---[3273]---> Sorter-cost: 3151     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3271]---> Sorter-cost: 1392     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3269]---> Sorter-cost: 1478     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3267]---> Sorter-cost: 1535     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[3265]---> Sorter-cost: 1478     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3263]---> Sorter-cost: 1535     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[3261]---> Sorter-cost: 1134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3259]---> Sorter-cost: 1191     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[3257]---> Sorter-cost: 5317     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3255]---> Sorter-cost: 4100     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 7 2 2 2
c ---[3253]---> Sorter-cost: 4142     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3251]---> Sorter-cost: 4142     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3249]---> Sorter-cost: 3745     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3247]---> Sorter-cost: 3745     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3245]---> BDD-cost:  581
c ---[3243]---> BDD-cost:  529
c ---[3241]---> Sorter-cost: 3523     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3239]---> Sorter-cost: 2102     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3237]---> Sorter-cost: 2210     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3235]---> Sorter-cost: 2234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3233]---> Sorter-cost: 2210     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3231]---> Sorter-cost: 2234     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3229]---> Sorter-cost: 1778     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3227]---> Sorter-cost: 1802     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3225]---> Sorter-cost: 4684     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3223]---> Sorter-cost: 2644     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3221]---> Sorter-cost: 2644     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3219]---> Sorter-cost: 2879     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3217]---> Sorter-cost: 2644     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3215]---> Sorter-cost: 2427     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3213]---> Sorter-cost: 2039     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3211]---> Sorter-cost: 1871     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3209]---> Sorter-cost: 6062     Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3207]---> Sorter-cost: 3284     Base: 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3
c ---[3205]---> Sorter-cost: 3561     Base: 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3
c ---[3203]---> Sorter-cost: 3832     Base: 2 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2
c ---[3201]---> Sorter-cost: 3561     Base: 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3
c ---[3199]---> Sorter-cost: 3832     Base: 2 2 2 2 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2
c ---[3197]---> Sorter-cost: 2300     Base: 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 3
c ---[3195]---> Sorter-cost: 2756     Base: 2 2 2 2 2 2 2 3 3 3 3 2 2 3 2 2 2 2 2 2 2
c ---[3193]---> Sorter-cost: 5559     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3191]---> Sorter-cost: 3987     Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3189]---> Sorter-cost: 4024     Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3187]---> Sorter-cost: 4024     Base: 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3185]---> Sorter-cost: 3727     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3183]---> Sorter-cost: 3727     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3181]---> Sorter-cost: 3052     Base: 2 2 2 2 2 2 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3179]---> Sorter-cost: 2776     Base: 2 2 2 2 2 2 5 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3177]---> Sorter-cost: 6731     Base: 2 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3175]---> Sorter-cost: 3761     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3
c ---[3173]---> Sorter-cost: 4035     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3
c ---[3171]---> Sorter-cost: 4126     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2
c ---[3169]---> Sorter-cost: 4035     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3
c ---[3167]---> Sorter-cost: 4126     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2
c ---[3165]---> Sorter-cost: 2939     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 3
c ---[3163]---> Sorter-cost: 3030     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 3 2 2 2 2 2 2 2 2
c ---[3161]---> Sorter-cost: 3706     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3159]---> Sorter-cost: 3706     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3157]---> Sorter-cost: 3706     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3155]---> Sorter-cost: 3580     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3153]---> Sorter-cost: 3580     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3151]---> Sorter-cost: 3580     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3149]---> Sorter-cost: 3798     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2
c ---[3147]---> Sorter-cost: 3798     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2
c ---[3145]---> Sorter-cost: 3798     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 7 2 2 2
c ---[3143]---> Sorter-cost: 4211     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3141]---> Sorter-cost: 4211     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3139]---> Sorter-cost: 4211     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3137]---> Sorter-cost: 5069     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3135]---> Sorter-cost: 3088     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3133]---> Sorter-cost: 3389     Base: 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3131]---> Sorter-cost: 3088     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3129]---> Sorter-cost: 3696     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3127]---> Sorter-cost: 3696     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3125]---> Sorter-cost: 3696     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3123]---> Sorter-cost: 3172     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2 2 2
c ---[3121]---> Sorter-cost: 1456     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3119]---> Sorter-cost: 1456     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3117]---> Sorter-cost: 1370     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3115]---> Sorter-cost: 2101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2
c ---[3113]---> Sorter-cost: 2101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2
c ---[3111]---> Sorter-cost: 2101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2
c ---[3109]---> Sorter-cost: 3791     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3107]---> Sorter-cost: 2107     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5
c ---[3105]---> Sorter-cost: 2101     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5 2
c ---[3103]---> Sorter-cost: 2107     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 5
c ---[3101]---> Sorter-cost: 1542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3099]---> Sorter-cost: 1542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3097]---> Sorter-cost: 1542     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3095]---> Sorter-cost: 5054     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3093]---> Sorter-cost: 2867     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 3 2 2 2 3
c ---[3091]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3089]---> Sorter-cost: 2867     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 3 2 2 2 3
c ---[3087]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3085]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3083]---> Sorter-cost: 2935     Base: 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2
c ---[3081]---> Adder-cost: 994   maxlim: 13873748826   bits: 35/34
c ---[3079]---> Adder-cost: 1010   maxlim: 14466784090   bits: 35/34
c ---[3077]---> Adder-cost: 1010   maxlim: 14466784090   bits: 35/34
c ---[3075]---> Adder-cost: 1568   maxlim: 93995325   bits: 28/27
c ---[3073]---> Adder-cost: 2013   maxlim: 485866136   bits: 30/29
c ---[3071]---> Adder-cost: 1752   maxlim: 328064955   bits: 30/29
c ---[3069]---> Sorter-cost: 2144     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3067]---> Sorter-cost: 6043     Base: 11 11 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3
c ---[3065]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3063]---> Sorter-cost: 6043     Base: 11 11 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 3
c ---[3061]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3059]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3057]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3055]---> Adder-cost: 346   maxlim: 80740198   bits: 28/27
c ---[3053]---> Sorter-cost: 4195     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 3 2
c ---[3051]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3049]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3047]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3045]---> Sorter-cost: 3199     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 7 11 2 2 2 2
c ---[3043]---> Adder-cost: 307   maxlim: 122158871   bits: 28/27
c ---[3041]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3039]---> Adder-cost: 307   maxlim: 122158871   bits: 28/27
c ---[3037]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3035]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3033]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3031]---> Sorter-cost: 2623     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3029]---> Sorter-cost: 2602     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3027]---> Sorter-cost: 2602     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3025]---> Sorter-cost: 3051     Base: 2 2 2 3 13 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3023]---> Sorter-cost: 3342     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 3 2 2 2
c ---[3013]---> BDD-cost:  212
c ---[3011]---> BDD-cost:  692
c ---[3009]---> BDD-cost:  389
c ---[3007]---> BDD-cost:   27
c ---[3005]---> BDD-cost:   27
c ---[2995]---> BDD-cost:   27
c ---[2993]---> BDD-cost:   27
c ---[2983]---> Sorter-cost: 4072     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2981]---> Sorter-cost: 4163     Base: 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2979]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2977]---> Sorter-cost: 2829     Base: 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2
c ---[2975]---> Sorter-cost: 3830     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2973]---> Sorter-cost: 3844     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2971]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2969]---> Sorter-cost: 3461     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2967]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2965]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2963]---> Sorter-cost: 4197     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2961]---> Sorter-cost: 3461     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2959]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2957]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2955]---> Sorter-cost: 6254     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2953]---> Sorter-cost: 2691     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2951]---> Sorter-cost: 3868     Base: 2 2 5 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2949]---> Sorter-cost: 6234     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2947]---> Sorter-cost: 3461     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2945]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2943]---> Sorter-cost: 3473     Base: 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2941]---> BDD-cost:  212
c ---[2939]---> BDD-cost:  389
c ---[2915]---> BDD-cost:  406
c ---[2913]---> BDD-cost:  692
c ---[2911]---> BDD-cost:  389
c ---[2901]---> Sorter-cost: 2790     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2899]---> Sorter-cost: 3420     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2897]---> Sorter-cost: 2677     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2895]---> Sorter-cost: 3143     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2893]---> Sorter-cost: 3934     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2891]---> Sorter-cost: 2986     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2889]---> Sorter-cost: 3263     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 5 2
c ---[2887]---> BDD-cost:  370
c ---[2885]---> Sorter-cost: 3866     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 5 2 2 2 2 2 2
c ---[2883]---> Sorter-cost: 3684     Base: 2 2 2 2 5 5 5 2 2 2 2 2 5 2 2 2 2 2 2
c ---[2881]---> Sorter-cost: 3437     Base: 2 2 2 2 5 5 5 2 2 2 2 5 2 2 2 2 2 2
c ---[2877]---> BDD-cost:  133
c ---[2873]---> Sorter-cost: 3117     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2871]---> Sorter-cost: 1880     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2869]---> Sorter-cost: 2828     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2867]---> Sorter-cost: 2566     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2865]---> Sorter-cost: 1207     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[2863]---> Sorter-cost: 2247     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2861]---> Sorter-cost: 2075     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2859]---> Sorter-cost: 1880     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2857]---> Sorter-cost: 2828     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2855]---> Sorter-cost: 2566     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2853]---> Sorter-cost: 2806     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2851]---> Sorter-cost: 5284     Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[2849]---> BDD-cost:  171
c ---[2847]---> Sorter-cost: 3874     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2845]---> Sorter-cost: 3538     Base: 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[2843]---> Sorter-cost: 2253     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2841]---> Sorter-cost: 3129     Base: 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[2839]---> Sorter-cost: 3587     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2837]---> BDD-cost:  171
c ---[2835]---> Sorter-cost: 3874     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2833]---> Sorter-cost: 3538     Base: 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[2831]---> Sorter-cost: 3864     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2
c ---[2829]---> Sorter-cost: 1420     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 5 2
c ---[2827]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 5 2
c ---[2825]---> Adder-cost: 280   maxlim: 17301471   bits: 26/25
c ---[2823]---> Sorter-cost: 2727     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 5 2
c ---[2821]---> Adder-cost: 236   maxlim: 4325343   bits: 24/23
c ---[2817]---> BDD-cost:  219
c ---[2813]---> Sorter-cost: 5746     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2811]---> Adder-cost: 454   maxlim: 237502011   bits: 29/28
c ---[2809]---> BDD-cost:  205
c ---[2807]---> BDD-cost:  426
c ---[2805]---> BDD-cost:  385
c ---[2803]---> Sorter-cost: 4159     Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2801]---> Sorter-cost: 5594     Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2799]---> Sorter-cost: 3844     Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2797]---> BDD-cost:  394
c ---[2795]---> Adder-cost: 482   maxlim: 475004475   bits: 30/29
c ---[2793]---> BDD-cost:  205
c ---[2791]---> Adder-cost: 482   maxlim: 475004475   bits: 30/29
c ---[2789]---> Sorter-cost: 4552     Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2787]---> Sorter-cost: 5683     Base: 2 2 2 5 5 5 2 2 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2785]---> Sorter-cost: 4751     Base: 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2783]---> Sorter-cost: 4996     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2781]---> Sorter-cost: 4632     Base: 2 2 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2779]---> BDD-cost:  20/oldhome/oroussel/solvers/minisat+_script: line 9: 21940 CPU time limit exceeded $XDIR/minisat+_64-bit_static -try "$@"
#### END SOLVER DATA ####
#### BEGIN WATCHER DATA ####
Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds
Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds
Enforcing VSIZE limit: 943718400 bytes
Raw data (loadavg): 0.88 0.97 0.99 2/54 21936
Raw data (stat): 21936 (runsolver) D 21935 3394 3393 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 842133832 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 3225161850 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0004 s]
Raw data (loadavg): 0.90 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+20.0016 s]
Raw data (loadavg): 0.91 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+30.001 s]
Raw data (loadavg): 0.92 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+40.0018 s]
Raw data (loadavg): 0.94 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+50.0031 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+60.004 s]
Raw data (loadavg): 0.95 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+70.0043 s]
Raw data (loadavg): 0.96 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+80.0046 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+90.0049 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+100.005 s]
Raw data (loadavg): 0.97 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+110.006 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+120.007 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+130.006 s]
Raw data (loadavg): 0.98 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+140.007 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+150.008 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+160.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+170.009 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+180.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+190.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+200.01 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+210.011 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+220.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+230.012 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+240.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+250.013 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+260.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+270.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+280.022 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+290.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+300.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+310.023 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+320.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+330.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+340.024 s]
Raw data (loadavg): 0.99 0.97 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+350.024 s]
Raw data (loadavg): 1.07 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+360.025 s]
Raw data (loadavg): 1.06 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+370.026 s]
Raw data (loadavg): 1.05 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+380.026 s]
Raw data (loadavg): 1.04 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+390.027 s]
Raw data (loadavg): 1.03 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+400.026 s]
Raw data (loadavg): 1.03 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+410.027 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+420.028 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+430.031 s]
Raw data (loadavg): 1.02 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+440.031 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+450.03 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+460.031 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+470.031 s]
Raw data (loadavg): 1.01 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+480.031 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+490.032 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+500.034 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+510.034 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+520.034 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+530.034 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+540.035 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+550.035 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+560.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+570.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+580.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+590.036 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+600.037 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+610.038 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+620.038 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+630.037 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+640.038 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+650.038 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+660.039 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+670.04 s]
Raw data (loadavg): 1.00 0.99 0.99 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+680.039 s]
Raw data (loadavg): 1.08 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+690.04 s]
Raw data (loadavg): 1.14 1.02 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+700.04 s]
Raw data (loadavg): 1.12 1.02 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+710.041 s]
Raw data (loadavg): 1.10 1.02 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+720.041 s]
Raw data (loadavg): 1.08 1.02 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+730.041 s]
Raw data (loadavg): 1.07 1.02 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+740.041 s]
Raw data (loadavg): 1.06 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+750.041 s]
Raw data (loadavg): 1.05 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+760.042 s]
Raw data (loadavg): 1.04 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+770.043 s]
Raw data (loadavg): 1.04 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+780.043 s]
Raw data (loadavg): 1.03 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+790.044 s]
Raw data (loadavg): 1.02 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+800.044 s]
Raw data (loadavg): 1.02 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+810.045 s]
Raw data (loadavg): 1.02 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+820.045 s]
Raw data (loadavg): 1.01 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+830.045 s]
Raw data (loadavg): 1.01 1.01 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+840.046 s]
Raw data (loadavg): 1.01 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+850.045 s]
Raw data (loadavg): 1.01 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+860.046 s]
Raw data (loadavg): 1.01 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+870.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+880.047 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+890.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+900.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+910.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+920.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+930.048 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+940.049 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+950.049 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+960.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+970.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+980.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+990.051 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1000.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1010.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1020.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1030.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1040.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1050.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1060.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1070.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1080.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1090.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1100.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1110.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1120.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1130.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1140.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1150.05 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1160.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1170.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1180.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1190.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1200.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1210.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1220.06 s]
Raw data (loadavg): 1.00 1.00 1.00 2/55 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 2124
[startup+1229.78 s]
Raw data (loadavg): 1.00 1.00 1.00 1/53 21940
Raw data (stat): 21936 (minisat+_script) S 21935 3394 3393 0 -1 0 274 239 0 0 0 0 0 1 19 0 1 0 842133832 2174976 226 4294967295 134512640 135087896 3221224544 3221223816 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0
Raw data (statm): 531 226 485 147 0 384 0
vsize: 0

Child status: 152
Real time (s): 1229.78
CPU time (s): 1229.91
CPU user time (s): 1226.06
CPU system time (s): 3.85041
CPU usage (%): 100.011
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####