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-greenbea.opb
MD5SUM	44cf829c3f56aa0e06d9c19014e5de34
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	10788
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	20280599220360
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.958853
Number of variables	104437
Total number of constraints	2675
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	2675
Minimum length of a constraint	8
Maximum length of a constraint	4913
Trace number 31037

#### BEGIN LAUNCHER DATA ####
LAUNCH ON wulflinc4 THE 2005-05-25 21:31:22 (client local time)
PB2005-SCRIPT v4.0 
MARKUPS: idlaunch=22405 boxname=wulflinc4 idbench=1221 idsolver=15 numberseed=0
MD5SUM SOLVER: 34d34154b8ad81f02ee98439942e0814  /oldhome/oroussel/solvers/minisat+_script
MD5SUM BENCH:  44cf829c3f56aa0e06d9c19014e5de34  /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-greenbea.opb
REAL COMMAND:  minisat+_script /oldhome/oroussel/tmp/wulflinc4/normalized-mps-v2-13-7-greenbea.opb
IDLAUNCH: 22405
/proc/cpuinfo:
processor	: 0
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
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	: 890.88

processor	: 1
vendor_id	: GenuineIntel
cpu family	: 6
model		: 7
model name	: Pentium III (Katmai)
stepping	: 2
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:        835772 kB
Buffers:         28892 kB
Cached:         148972 kB
SwapCached:        500 kB
Active:          47508 kB
Inactive:       132784 kB
HighTotal:      131008 kB
HighFree:          252 kB
LowTotal:       903652 kB
LowFree:        835520 kB
SwapTotal:     2097136 kB
SwapFree:      2096004 kB
Dirty:              28 kB
Writeback:           0 kB
Mapped:           5784 kB
Slab:            13004 kB
Committed_AS:    71784 kB
PageTables:        316 kB
VmallocTotal:   114680 kB
VmallocUsed:      1388 kB
VmallocChunk:   113256 kB
JOB ENDED THE 2005-05-25 21:51:52 (client local time) WITH STATUS 152 IN 1229.89 SECONDS
stats: 22405 7 1229.89 152
#### END LAUNCHER DATA ####
#### BEGIN SOLVER DATA ####
c Parsing PB file...
c Converting 4200 PB-constraints to clauses...
c   -- Unit propagations: ppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp
c   -- Detecting intervals from adjacent constraints: ######################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################
c   -- Clauses(.)/Splits(s): ssssssssssssssssssssssssssssssssssssssssssssssss
c ---[4247]---> BDD-cost:   17
c ---[4242]---> BDD-cost:   15
c ---[4241]---> BDD-cost:   14
c ---[4240]---> BDD-cost:   18
c ---[4239]---> BDD-cost:   15
c ---[4237]---> BDD-cost:   14
c ---[4236]---> BDD-cost:   16
c ---[4235]---> BDD-cost:   13
c ---[4234]---> BDD-cost:   13
c ---[4233]---> BDD-cost:   11
c ---[4232]---> BDD-cost:   13
c ---[4230]---> BDD-cost:   13
c ---[4229]---> BDD-cost:   14
c ---[4227]---> BDD-cost:   12
c ---[4226]---> BDD-cost:    8
c ---[4225]---> BDD-cost:   12
c ---[4224]---> BDD-cost:   12
c ---[4223]---> BDD-cost:    9
c ---[4221]---> BDD-cost:   13
c ---[4218]---> BDD-cost:   10
c ---[4217]---> BDD-cost:   15
c ---[4214]---> BDD-cost:    9
c ---[4213]---> BDD-cost:   16
c ---[4212]---> BDD-cost:   12
c ---[4211]---> BDD-cost:   14
c ---[4210]---> BDD-cost:   14
c ---[4209]---> BDD-cost:   12
c ---[4208]---> BDD-cost:   15
c ---[4207]---> BDD-cost:   12
c ---[4206]---> BDD-cost:   13
c ---[4205]---> BDD-cost:    8
c ---[4203]---> BDD-cost:   12
c ---[4202]---> BDD-cost:   11
c ---[4201]---> BDD-cost:   10
c ---[4200]---> BDD-cost:   12
c ---[4199]---> BDD-cost:   14
c ---[4196]---> BDD-cost:   19
c ---[4195]---> BDD-cost:   13
c ---[4194]---> BDD-cost:   16
c ---[4192]---> BDD-cost:   16
c ---[4190]---> BDD-cost:   17
c ---[4189]---> BDD-cost:   15
c ---[4188]---> BDD-cost:   15
c ---[4187]---> BDD-cost:   13
c ---[4186]---> BDD-cost:   17
c ---[4185]---> BDD-cost:   16
c ---[4184]---> BDD-cost:   16
c ---[4183]---> BDD-cost:   15
c ---[4182]---> BDD-cost:   14
c ---[4181]---> BDD-cost:    7
c ---[4180]---> BDD-cost:   11
c ---[4179]---> BDD-cost:   15
c ---[4178]---> BDD-cost:    7
c ---[4177]---> BDD-cost:   12
c ---[4176]---> BDD-cost:   12
c ---[4175]---> BDD-cost:    8
c ---[4174]---> BDD-cost:   11
c ---[4173]---> BDD-cost:   14
c ---[4170]---> BDD-cost:   17
c ---[4169]---> BDD-cost:   20
c ---[4168]---> BDD-cost:   14
c ---[4167]---> BDD-cost:   13
c ---[4166]---> BDD-cost:   17
c ---[4164]---> BDD-cost:    9
c ---[4163]---> BDD-cost:   17
c ---[4162]---> BDD-cost:   11
c ---[4161]---> BDD-cost:   18
c ---[4160]---> BDD-cost:   15
c ---[4159]---> BDD-cost:   16
c ---[4158]---> BDD-cost:   16
c ---[4157]---> BDD-cost:   16
c ---[4155]---> BDD-cost:   17
c ---[4154]---> BDD-cost:   15
c ---[4153]---> BDD-cost:   15
c ---[4152]---> BDD-cost:    7
c ---[4151]---> BDD-cost:   11
c ---[4149]---> BDD-cost:    7
c ---[4148]---> BDD-cost:   14
c ---[4147]---> BDD-cost:   13
c ---[4146]---> BDD-cost:    7
c ---[4145]---> BDD-cost:   12
c ---[4142]---> BDD-cost:   14
c ---[4141]---> BDD-cost:   15
c ---[4140]---> BDD-cost:   19
c ---[4139]---> BDD-cost:   16
c ---[4138]---> BDD-cost:   16
c ---[4136]---> BDD-cost:   15
c ---[4135]---> BDD-cost:   17
c ---[4134]---> BDD-cost:   11
c ---[4133]---> BDD-cost:   16
c ---[4132]---> BDD-cost:   16
c ---[4130]---> BDD-cost:   15
c ---[4128]---> BDD-cost:   15
c ---[4127]---> BDD-cost:   15
c ---[4126]---> BDD-cost:   16
c ---[4125]---> BDD-cost:   16
c ---[4124]---> BDD-cost:   12
c ---[4123]---> BDD-cost:   16
c ---[4122]---> BDD-cost:   15
c ---[4121]---> BDD-cost:   12
c ---[4120]---> BDD-cost:   12
c ---[4119]---> BDD-cost:   11
c ---[4117]---> BDD-cost:   12
c ---[4116]---> BDD-cost:   11
c ---[4115]---> BDD-cost:   12
c ---[4114]---> BDD-cost:   11
c ---[4113]---> BDD-cost:   12
c ---[4112]---> BDD-cost:   12
c ---[4111]---> BDD-cost:   12
c ---[4110]---> BDD-cost:   13
c ---[4109]---> BDD-cost:   12
c ---[4108]---> BDD-cost:   15
c ---[4107]---> BDD-cost:   19
c ---[4104]---> BDD-cost:   15
c ---[4103]---> BDD-cost:   15
c ---[4100]---> BDD-cost:   16
c ---[4099]---> BDD-cost:   15
c ---[4098]---> BDD-cost:   16
c ---[4097]---> BDD-cost:   16
c ---[4096]---> BDD-cost:   17
c ---[4094]---> BDD-cost:   14
c ---[4093]---> BDD-cost:   13
c ---[4092]---> BDD-cost:   14
c ---[4091]---> BDD-cost:   12
c ---[4089]---> BDD-cost:   11
c ---[4087]---> BDD-cost:   12
c ---[4086]---> BDD-cost:   14
c ---[4085]---> BDD-cost:   13
c ---[4084]---> BDD-cost:   12
c ---[4083]---> BDD-cost:   15
c ---[4082]---> BDD-cost:   12
c ---[4080]---> BDD-cost:   11
c ---[4079]---> BDD-cost:   11
c ---[4077]---> BDD-cost:   10
c ---[4072]---> BDD-cost:   12
c ---[4071]---> BDD-cost:   16
c ---[4069]---> BDD-cost:   14
c ---[4067]---> BDD-cost:   13
c ---[4066]---> BDD-cost:   15
c ---[4064]---> BDD-cost:   16
c ---[4063]---> BDD-cost:   10
c ---[4061]---> BDD-cost:   16
c ---[4060]---> BDD-cost:   16
c ---[4059]---> BDD-cost:   16
c ---[4057]---> BDD-cost:   13
c ---[4056]---> BDD-cost:   18
c ---[4055]---> BDD-cost:   14
c ---[4054]---> BDD-cost:   12
c ---[4053]---> BDD-cost:   11
c ---[4052]---> BDD-cost:   13
c ---[4051]---> BDD-cost:    7
c ---[4050]---> BDD-cost:   14
c ---[4049]---> BDD-cost:   13
c ---[4048]---> BDD-cost:    9
c ---[4047]---> BDD-cost:    9
c ---[4046]---> BDD-cost:   13
c ---[4045]---> BDD-cost:   14
c ---[4044]---> BDD-cost:   17
c ---[4042]---> BDD-cost:   11
c ---[4041]---> BDD-cost:   12
c ---[4040]---> BDD-cost:   15
c ---[4039]---> BDD-cost:   19
c ---[4036]---> BDD-cost:   15
c ---[4035]---> BDD-cost:   16
c ---[4034]---> BDD-cost:   18
c ---[4032]---> BDD-cost:   18
c ---[4031]---> BDD-cost:   13
c ---[4030]---> BDD-cost:   18
c ---[4027]---> BDD-cost:   16
c ---[4026]---> BDD-cost:   15
c ---[4025]---> BDD-cost:   18
c ---[4024]---> BDD-cost:   17
c ---[4022]---> BDD-cost:   12
c ---[4021]---> BDD-cost:   15
c ---[4020]---> BDD-cost:    7
c ---[4019]---> BDD-cost:   15
c ---[4018]---> BDD-cost:   13
c ---[4017]---> BDD-cost:   12
c ---[4016]---> BDD-cost:   11
c ---[4015]---> BDD-cost:   13
c ---[4014]---> BDD-cost:   19
c ---[4013]---> BDD-cost:   16
c ---[4010]---> BDD-cost:   16
c ---[4009]---> BDD-cost:   18
c ---[4008]---> BDD-cost:   14
c ---[4007]---> BDD-cost:   15
c ---[4006]---> BDD-cost:   15
c ---[4005]---> BDD-cost:   16
c ---[4003]---> BDD-cost:   16
c ---[4002]---> BDD-cost:   10
c ---[4001]---> BDD-cost:   15
c ---[4000]---> BDD-cost:   15
c ---[3998]---> BDD-cost:   12
c ---[3997]---> BDD-cost:   13
c ---[3996]---> BDD-cost:   17
c ---[3994]---> BDD-cost:   11
c ---[3993]---> BDD-cost:   11
c ---[3992]---> BDD-cost:   10
c ---[3991]---> BDD-cost:    7
c ---[3990]---> BDD-cost:   13
c ---[3989]---> BDD-cost:   11
c ---[3988]---> BDD-cost:    8
c ---[3987]---> BDD-cost:    9
c ---[3986]---> BDD-cost:   11
c ---[3980]---> BDD-cost:   17
c ---[3979]---> BDD-cost:   13
c ---[3977]---> BDD-cost:   12
c ---[3975]---> BDD-cost:   15
c ---[3973]---> BDD-cost:   11
c ---[3972]---> BDD-cost:    7
c ---[3971]---> BDD-cost:    8
c ---[3970]---> BDD-cost:   13
c ---[3969]---> BDD-cost:   11
c ---[3968]---> BDD-cost:   14
c ---[3966]---> BDD-cost:   11
c ---[3965]---> BDD-cost:   10
c ---[3963]---> BDD-cost:    9
c ---[3961]---> BDD-cost:   13
c ---[3958]---> BDD-cost:   17
c ---[3956]---> Sorter-cost: 1853     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3954]---> Adder-cost: 593   maxlim: 310528   bits: 20/19
c ---[3952]---> Adder-cost: 926   maxlim: 1250687   bits: 22/21
c ---[3950]---> Adder-cost: 593   maxlim: 297600   bits: 20/19
c ---[3948]---> Sorter-cost: 3378     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3946]---> Adder-cost: 529   maxlim: 108800   bits: 18/17
c ---[3944]---> Sorter-cost: 3248     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3942]---> Sorter-cost: 2120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3940]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3938]---> Adder-cost: 300   maxlim: 97664   bits: 18/17
c ---[3936]---> BDD-cost:  172
c ---[3934]---> Adder-cost: 300   maxlim: 78976   bits: 18/17
c ---[3932]---> Sorter-cost:  372     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3930]---> BDD-cost:   70
c ---[3928]---> Sorter-cost: 3164     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3926]---> Adder-cost: 593   maxlim: 453888   bits: 20/19
c ---[3924]---> Adder-cost: 593   maxlim: 299136   bits: 20/19
c ---[3922]---> BDD-cost:   58
c ---[3920]---> Sorter-cost: 1562     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3918]---> Adder-cost: 561   maxlim: 248192   bits: 19/18
c ---[3916]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3914]---> Adder-cost: 593   maxlim: 321152   bits: 20/19
c ---[3912]---> BDD-cost:   85
c ---[3910]---> Sorter-cost: 2874     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3908]---> Adder-cost: 353   maxlim: 219648   bits: 19/18
c ---[3906]---> Sorter-cost: 2946     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3904]---> Sorter-cost: 3380     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3902]---> Sorter-cost:  473     Base: 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3900]---> Adder-cost: 375   maxlim: 60160   bits: 17/16
c ---[3898]---> BDD-cost:   75
c ---[3896]---> Adder-cost: 318   maxlim: 131712   bits: 19/18
c ---[3894]---> Sorter-cost: 1087     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3892]---> Sorter-cost: 1385     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3890]---> Sorter-cost: 2120     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3888]---> BDD-cost:   75
c ---[3886]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3884]---> Sorter-cost: 1844     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3882]---> BDD-cost:  170
c ---[3880]---> BDD-cost:   58
c ---[3878]---> BDD-cost:   58
c ---[3876]---> Adder-cost: 293   maxlim: 20224   bits: 16/15
c ---[3874]---> BDD-cost:   50
c ---[3872]---> BDD-cost:  314
c ---[3862]---> BDD-cost:  167
c ---[3860]---> BDD-cost:  314
c ---[3858]---> BDD-cost:  314
c ---[3856]---> BDD-cost:   90
c ---[3854]---> BDD-cost:   90
c ---[3852]---> BDD-cost:   50
c ---[3850]---> BDD-cost:   50
c ---[3840]---> Adder-cost: 404   maxlim: 2557996273   bits: 33/32
c ---[3838]---> Adder-cost: 404   maxlim: 2557996273   bits: 33/32
c ---[3836]---> Adder-cost: 404   maxlim: 2557996273   bits: 33/32
c ---[3828]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2 2
c ---[3826]---> Sorter-cost: 4718     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3824]---> Sorter-cost: 4748     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3822]---> 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 ---[3820]---> 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 ---[3816]---> 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 ---[3808]---> Sorter-cost: 3056     Base: 2 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2
c ---[3806]---> Sorter-cost: 4317     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3804]---> 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 ---[3802]---> 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 ---[3800]---> 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 ---[3796]---> Sorter-cost: 3658     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3788]---> Sorter-cost: 1577     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2
c ---[3786]---> Sorter-cost: 3148     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3784]---> Sorter-cost: 3178     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2
c ---[3782]---> Sorter-cost: 3130     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3780]---> Sorter-cost: 3130     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3776]---> Sorter-cost: 1872     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2
c ---[3768]---> Sorter-cost: 2957     Base: 2 2 2 2 5 5 2 2 2 2 2 2 5 7 2 2 2
c ---[3766]---> 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 ---[3764]---> 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 ---[3762]---> 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 ---[3760]---> 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 ---[3756]---> Sorter-cost: 3580     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 5 2 7 2 2
c ---[3748]---> Sorter-cost: 3056     Base: 2 2 2 2 2 5 5 5 2 2 2 2 7 2 2 2
c ---[3746]---> Sorter-cost: 4287     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3744]---> Sorter-cost: 4317     Base: 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3742]---> 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 ---[3740]---> 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 ---[3736]---> Sorter-cost: 3658     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 7 2 2
c ---[3726]---> BDD-cost:   53
c ---[3724]---> BDD-cost:   53
c ---[3720]---> Sorter-cost: 2016     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 11 2 2 2 2 2
c ---[3718]---> Sorter-cost: 3242     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3716]---> 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 ---[3714]---> 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 ---[3712]---> 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 ---[3708]---> Sorter-cost: 2296     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 5 5 7 2 2
c ---[3700]---> BDD-cost:  595
c ---[3698]---> 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 ---[3696]---> 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 ---[3694]---> 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 ---[3692]---> 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 ---[3688]---> 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 ---[3680]---> Sorter-cost: 2658     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3678]---> 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 ---[3676]---> 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 ---[3674]---> 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 ---[3672]---> 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 ---[3668]---> 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 ---[3660]---> Sorter-cost: 2861     Base: 2 2 2 2 2 2 2 2 2 5 2 2 3 7 2 2 2 2 2 2
c ---[3658]---> Sorter-cost: 4620     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3656]---> Sorter-cost: 4640     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3654]---> Sorter-cost: 4640     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3652]---> Sorter-cost: 4640     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 5 2 2 2
c ---[3648]---> Sorter-cost: 3187     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 ---[3640]---> BDD-cost:  596
c ---[3638]---> 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 ---[3636]---> 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 ---[3634]---> 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 ---[3632]---> 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 ---[3628]---> 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 ---[3620]---> Sorter-cost: 2658     Base: 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3618]---> 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 ---[3616]---> 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 ---[3614]---> 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 ---[3612]---> 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 ---[3608]---> 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 ---[3600]---> Sorter-cost: 2705     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[3598]---> BDD-cost:  148
c ---[3594]---> Sorter-cost: 2627     Base: 2 2 2 2 2 2 2 2 2 3 3 3 2 2 2 2 2 2 2
c ---[3592]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3590]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3588]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3586]---> Sorter-cost: 4226     Base: 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2 5 2
c ---[3582]---> Sorter-cost: 2999     Base: 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3574]---> 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 ---[3572]---> Adder-cost: 548   maxlim: 163444290   bits: 29/28
c ---[3570]---> Adder-cost: 666   maxlim: 2615146050   bits: 32/32
c ---[3568]---> Adder-cost: 666   maxlim: 2615146050   bits: 32/32
c ---[3566]---> Adder-cost: 468   maxlim: 1307573025   bits: 32/31
c ---[3564]---> 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 ---[3562]---> BDD-cost:  447
c ---[3560]---> Adder-cost: 516   maxlim: 140770970   bits: 29/28
c ---[3558]---> Adder-cost: 544   maxlim: 375389850   bits: 30/29
c ---[3556]---> Adder-cost: 516   maxlim: 140770970   bits: 29/28
c ---[3554]---> BDD-cost:  254
c ---[3552]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3550]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3548]---> Sorter-cost: 1999     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 7 2 2 2 2 2
c ---[3546]---> Adder-cost: 390   maxlim: 1301281575   bits: 32/31
c ---[3544]---> Adder-cost: 456   maxlim: 162657870   bits: 29/28
c ---[3542]---> Adder-cost: 560   maxlim: 2602563150   bits: 32/32
c ---[3540]---> Adder-cost: 560   maxlim: 2602563150   bits: 32/32
c ---[3538]---> Adder-cost: 390   maxlim: 1301281575   bits: 32/31
c ---[3536]---> Adder-cost: 370   maxlim: 650640167   bits: 31/30
c ---[3534]---> BDD-cost:  450
c ---[3532]---> Adder-cost: 358   maxlim: 161480550   bits: 28/28
c ---[3530]---> Adder-cost: 358   maxlim: 161480550   bits: 28/28
c ---[3528]---> Adder-cost: 358   maxlim: 161480550   bits: 28/28
c ---[3526]---> Adder-cost: 330   maxlim: 162659111   bits: 29/28
c ---[3524]---> 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 ---[3522]---> BDD-cost:  181
c ---[3520]---> 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 ---[3518]---> 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 ---[3516]---> BDD-cost:  615
c ---[3512]---> BDD-cost:  154
c ---[3510]---> 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 ---[3508]---> 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 ---[3506]---> 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 ---[3502]---> 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 ---[3500]---> BDD-cost:  154
c ---[3498]---> 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 ---[3496]---> 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 ---[3494]---> 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 ---[3492]---> 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 ---[3490]---> BDD-cost:  288
c ---[3488]---> 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 ---[3486]---> 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 ---[3484]---> BDD-cost:  278
c ---[3482]---> 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 ---[3480]---> 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 ---[3478]---> 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 ---[3476]---> BDD-cost:  463
c ---[3474]---> 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 ---[3472]---> 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 ---[3470]---> Sorter-cost: 3598     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2 2
c ---[3468]---> 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 ---[3466]---> Sorter-cost: 4946     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 3 3 2 2
c ---[3464]---> 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 ---[3462]---> 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 ---[3460]---> Sorter-cost: 1814     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3458]---> Sorter-cost: 1604     Base: 2 2 2 2 2 2 2 2 2 2 2 2 5 2 3 3 2
c ---[3450]---> 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 ---[3448]---> Adder-cost: 392   maxlim: 15007286   bits: 25/24
c ---[3446]---> Adder-cost: 510   maxlim: 480247350   bits: 30/29
c ---[3444]---> Adder-cost: 510   maxlim: 480247350   bits: 30/29
c ---[3442]---> 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 ---[3440]---> 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 ---[3438]---> Sorter-cost: 2793     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 3 3 2 2
c ---[3436]---> 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 ---[3434]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3432]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3430]---> Sorter-cost: 1368     Base: 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[3428]---> 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 ---[3426]---> BDD-cost:  173
c ---[3424]---> Adder-cost: 406   maxlim: 2778196813   bits: 33/32
c ---[3422]---> Adder-cost: 406   maxlim: 2778196813   bits: 33/32
c ---[3420]---> BDD-cost:  607
c ---[3416]---> BDD-cost:  172
c ---[3412]---> 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 ---[3410]---> BDD-cost:  286
c ---[3408]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3406]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3404]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3402]---> Adder-cost: 490   maxlim: 1601174025   bits: 32/31
c ---[3400]---> BDD-cost:  421
c ---[3398]---> 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 ---[3396]---> 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 ---[3394]---> BDD-cost:  451
c ---[3392]---> 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 ---[3390]---> 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 ---[3388]---> 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 ---[3386]---> 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 ---[3384]---> 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 ---[3382]---> 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 ---[3380]---> Adder-cost: 598   maxlim: 14032030650   bits: 35/34
c ---[3378]---> Adder-cost: 598   maxlim: 14032030650   bits: 35/34
c ---[3376]---> 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 ---[3374]---> Sorter-cost: 3849     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 2 2
c ---[3372]---> BDD-cost:  131
c ---[3370]---> Sorter-cost: 3210     Base: 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 ---[3368]---> 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 ---[3366]---> Sorter-cost: 3210     Base: 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 ---[3364]---> BDD-cost:  105
c ---[3356]---> Adder-cost: 384   maxlim: 7049569725   bits: 34/33
c ---[3354]---> Adder-cost: 634   maxlim: 14099139450   bits: 35/34
c ---[3352]---> Adder-cost: 634   maxlim: 14099139450   bits: 35/34
c ---[3350]---> Adder-cost: 384   maxlim: 7049569725   bits: 34/33
c ---[3348]---> Adder-cost: 364   maxlim: 3524781501   bits: 33/32
c ---[3346]---> BDD-cost:  131
c ---[3344]---> 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 ---[3342]---> 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 ---[3340]---> 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 ---[3338]---> BDD-cost:  340
c ---[3336]---> 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 ---[3334]---> 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 ---[3332]---> 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 ---[3330]---> Sorter-cost: 3456     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2
c ---[3328]---> BDD-cost:  152
c ---[3326]---> BDD-cost:  373
c ---[3324]---> 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 ---[3322]---> 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 ---[3320]---> 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 ---[3316]---> Adder-cost: 514   maxlim: 488635950   bits: 30/29
c ---[3314]---> Adder-cost: 514   maxlim: 488635950   bits: 30/29
c ---[3312]---> Adder-cost: 514   maxlim: 488635950   bits: 30/29
c ---[3310]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3308]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3306]---> Sorter-cost: 2118     Base: 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2
c ---[3304]---> BDD-cost:  758
c ---[3302]---> BDD-cost:  754
c ---[3300]---> 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 ---[3298]---> 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 ---[3296]---> 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 ---[3294]---> 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 ---[3292]---> 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 ---[3290]---> 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 ---[3288]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3286]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3284]---> Sorter-cost: 1000     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3282]---> 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 ---[3280]---> 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 ---[3278]---> 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 ---[3276]---> 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 ---[3274]---> 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 ---[3272]---> 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 ---[3270]---> BDD-cost:  595
c ---[3268]---> BDD-cost:  530
c ---[3266]---> 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 ---[3264]---> 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 ---[3262]---> 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 ---[3260]---> 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 ---[3258]---> 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 ---[3256]---> 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 ---[3254]---> Sorter-cost: 1134     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 3
c ---[3252]---> Sorter-cost: 1191     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2
c ---[3250]---> 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 ---[3248]---> 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 ---[3246]---> 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 ---[3244]---> 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 ---[3242]---> 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 ---[3240]---> 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 ---[3238]---> BDD-cost:  581
c ---[3236]---> BDD-cost:  529
c ---[3234]---> 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 ---[3232]---> 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 ---[3230]---> 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 ---[3228]---> 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 ---[3226]---> 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 ---[3224]---> 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 ---[3222]---> Sorter-cost: 1778     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 3
c ---[3220]---> Sorter-cost: 1802     Base: 2 2 2 2 2 2 2 2 2 2 2 5 5 2 2 2 2 2
c ---[3218]---> 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 ---[3216]---> 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 ---[3214]---> 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 ---[3212]---> 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 ---[3210]---> 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 ---[3208]---> 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 ---[3206]---> Sorter-cost: 2039     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[3204]---> Sorter-cost: 1871     Base: 2 2 2 2 2 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[3202]---> 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 ---[3200]---> 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 ---[3198]---> 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 ---[3196]---> 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 ---[3194]---> 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 ---[3192]---> 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 ---[3190]---> 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 ---[3188]---> 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 ---[3186]---> 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 ---[3184]---> 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 ---[3182]---> 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 ---[3180]---> 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 ---[3178]---> 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 ---[3176]---> 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 ---[3174]---> 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 ---[3172]---> Sorter-cost: 2776     Base: 2 2 2 2 2 2 5 2 2 5 2 2 2 2 2 2 2 2 2
c ---[3170]---> 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 ---[3168]---> 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 ---[3166]---> 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 ---[3164]---> 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 ---[3162]---> 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 ---[3160]---> 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 ---[3158]---> 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 ---[3156]---> 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 ---[3154]---> 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 ---[3152]---> 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 ---[3150]---> 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 ---[3148]---> 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 ---[3146]---> 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 ---[3144]---> 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 ---[3142]---> 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 ---[3140]---> 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 ---[3138]---> 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 ---[3136]---> 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 ---[3134]---> 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 ---[3132]---> 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 ---[3130]---> 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 ---[3128]---> 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 ---[3126]---> 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 ---[3124]---> 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 ---[3122]---> 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 ---[3120]---> 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 ---[3118]---> 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 ---[3116]---> 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 ---[3114]---> 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 ---[3112]---> 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 ---[3110]---> Sorter-cost: 1370     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 2 5 2 2
c ---[3108]---> 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 ---[3106]---> 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 ---[3104]---> 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 ---[3102]---> 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 ---[3100]---> 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 ---[3098]---> 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 ---[3096]---> 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 ---[3094]---> 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 ---[3092]---> 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 ---[3090]---> 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 ---[3088]---> 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 ---[3086]---> 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 ---[3084]---> 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 ---[3082]---> 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 ---[3080]---> 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 ---[3078]---> 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 ---[3076]---> 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 ---[3074]---> Adder-cost: 1048   maxlim: 22769277786   bits: 35/35
c ---[3072]---> Adder-cost: 1048   maxlim: 22769277786   bits: 35/35
c ---[3070]---> Adder-cost: 1048   maxlim: 22769277786   bits: 35/35
c ---[3068]---> Adder-cost: 1868   maxlim: 1273684285   bits: 32/31
c ---[3066]---> Adder-cost: 2325   maxlim: 1783847576   bits: 32/31
c ---[3064]---> Adder-cost: 2055   maxlim: 1724964795   bits: 32/31
c ---[3062]---> 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 ---[3060]---> 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 ---[3058]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3056]---> 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 ---[3054]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3052]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3050]---> Adder-cost: 544   maxlim: 761265450   bits: 31/30
c ---[3048]---> Adder-cost: 346   maxlim: 80740198   bits: 28/27
c ---[3046]---> 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 ---[3044]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3042]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3040]---> Adder-cost: 364   maxlim: 161480550   bits: 29/28
c ---[3038]---> 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 ---[3036]---> Adder-cost: 307   maxlim: 122158871   bits: 28/27
c ---[3034]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3032]---> Adder-cost: 307   maxlim: 122158871   bits: 28/27
c ---[3030]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3028]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3026]---> Adder-cost: 325   maxlim: 244317975   bits: 29/28
c ---[3024]---> 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 ---[3022]---> 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 ---[3020]---> 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 ---[3018]---> 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 ---[3016]---> Sorter-cost: 3584     Base: 2 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 ---[3006]---> Sorter-cost: 3810     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[3004]---> Sorter-cost: 4239     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[3002]---> Sorter-cost: 4239     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[3000]---> BDD-cost:  388
c ---[2998]---> BDD-cost:  388
c ---[2988]---> BDD-cost:  212
c ---[2986]---> BDD-cost:  212
c ---[2976]---> 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 ---[2974]---> 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 ---[2972]---> 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 ---[2970]---> Sorter-cost: 2881     Base: 2 2 2 2 2 2 2 2 2 2 2 5 2 2 2 2 2
c ---[2968]---> 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 ---[2966]---> 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 ---[2964]---> 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 ---[2962]---> Sorter-cost: 3817     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2960]---> 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 ---[2958]---> 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 ---[2956]---> Sorter-cost: 4249     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2954]---> Sorter-cost: 3817     Base: 2 2 2 2 2 2 5 5 2 2 5 2 2 2 2 2 2 2 2 2 3
c ---[2952]---> 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 ---[2950]---> 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 ---[2948]---> 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 ---[2946]---> Sorter-cost: 2693     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2944]---> Sorter-cost: 3888     Base: 2 2 5 5 2 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2942]---> 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 ---[2940]---> 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 ---[2938]---> 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 ---[2936]---> 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 ---[2934]---> BDD-cost:  389
c ---[2932]---> Sorter-cost: 4239     Base: 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2908]---> Sorter-cost: 5511     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2906]---> Sorter-cost: 5339     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2
c ---[2904]---> Sorter-cost: 5480     Base: 2 2 2 2 2 2 2 2 5 5 5 2 2 2 2 2 3 5 2
c ---[2894]---> Sorter-cost: 2986     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2892]---> Sorter-cost: 3420     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2890]---> Sorter-cost: 2929     Base: 2 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2888]---> Sorter-cost: 3817     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2886]---> Sorter-cost: 3934     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2884]---> Sorter-cost: 3365     Base: 2 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2 2 2
c ---[2882]---> 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 ---[2880]---> BDD-cost:  370
c ---[2878]---> 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 ---[2876]---> 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 ---[2874]---> Sorter-cost: 3684     Base: 2 2 2 2 5 5 5 2 2 2 2 2 5 2 2 2 2 2 2
c ---[2870]---> BDD-cost:  133
c ---[2866]---> Sorter-cost: 3117     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2 2 2
c ---[2864]---> Sorter-cost: 1880     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2862]---> Sorter-cost: 2828     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2860]---> Sorter-cost: 3165     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2858]---> Sorter-cost: 1339     Base: 2 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 2 2
c ---[2856]---> Sorter-cost: 2247     Base: 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2854]---> Sorter-cost: 2075     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2852]---> Sorter-cost: 1880     Base: 2 5 5 5 2 2 2 2 2 2 2
c ---[2850]---> Sorter-cost: 2828     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2848]---> Sorter-cost: 3165     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2846]---> Sorter-cost: 2806     Base: 2 2 2 2 5 5 5 2 2 2 2 2 2 2 2
c ---[2844]---> 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 ---[2842]---> BDD-cost:  171
c ---[2840]---> 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 ---[2838]---> 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 ---[2836]---> 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 ---[2834]---> Sorter-cost: 3129     Base: 2 2 2 2 2 2 2 2 2 2 3 13 2 2 2 2 2 2 2
c ---[2832]---> Sorter-cost: 3587     Base: 2 2 2 2 5 5 5 5 2 2 2 2 2 2 2 2 2
c ---[2830]---> BDD-cost:  171
c ---[2828]---> 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 ---[2826]---> 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 ---[2824]---> 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 ---[2822]---> 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 ---[2820]---> Sorter-cost: 2034     Base: 2 2 2 2 2 2 2 2 2 3 2 2 2 2 2 5 2
c ---[2818]---> Adder-cost: 280   maxlim: 17301471   bits: 26/25
c ---[2816]---> Adder-cost: 280   maxlim: 17301471   bits: 26/25
c ---[2814]---> Sorter-cost: 2727     Base: 2 2 2 2 2 2 2 2 2 2 2 2 2 3 2 2 2 5 2
c ---[2/oldhome/oroussel/solvers/minisat+_script: line 9:  5504 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.85 0.94 0.95 2/54 5500
Raw data (stat): 5500 (runsolver) R 5499 21152 21151 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 783908813 1052672 99 4294967295 134512640 135381576 3221224480 3221219688 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0
Raw data (statm): 257 99 215 215 0 42 0
vsize: 1028
[startup+10.0008 s]
Raw data (loadavg): 0.88 0.94 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.0015 s]
Raw data (loadavg): 0.89 0.94 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.0023 s]
Raw data (loadavg): 0.91 0.94 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.0032 s]
Raw data (loadavg): 0.92 0.94 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.93 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.94 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.0038 s]
Raw data (loadavg): 0.95 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.0047 s]
Raw data (loadavg): 0.96 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.0045 s]
Raw data (loadavg): 0.96 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.004 s]
Raw data (loadavg): 0.97 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.005 s]
Raw data (loadavg): 0.97 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.006 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.007 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.98 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.007 s]
Raw data (loadavg): 0.98 0.95 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.008 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.009 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.013 s]
Raw data (loadavg): 0.99 0.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.96 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.014 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.015 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.016 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.017 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.019 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.02 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.021 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.022 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.023 s]
Raw data (loadavg): 0.99 0.97 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.023 s]
Raw data (loadavg): 1.07 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.023 s]
Raw data (loadavg): 1.06 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.024 s]
Raw data (loadavg): 1.05 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.024 s]
Raw data (loadavg): 1.04 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.025 s]
Raw data (loadavg): 1.04 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.026 s]
Raw data (loadavg): 1.03 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.026 s]
Raw data (loadavg): 1.03 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.027 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.027 s]
Raw data (loadavg): 1.02 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.028 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.028 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.028 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.029 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.03 s]
Raw data (loadavg): 1.01 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.031 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.032 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.035 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.036 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.037 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.038 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.039 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.04 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.042 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.046 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.052 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.052 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.051 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.052 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.053 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.054 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.054 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.054 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.054 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.054 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.055 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.056 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.056 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.057 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.058 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.059 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.058 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.058 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.059 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.06 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.07 s]
Raw data (loadavg): 1.00 0.99 0.95 2/55 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.72 s]
Raw data (loadavg): 1.00 0.99 0.95 1/53 5504
Raw data (stat): 5500 (minisat+_script) S 5499 21152 21151 0 -1 0 274 239 0 0 0 0 0 0 19 0 1 0 783908813 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.72
CPU time (s): 1229.89
CPU user time (s): 1227.69
CPU system time (s): 2.19267
CPU usage (%): 100.013
Max. virtual memory (Kb): 2124
#### END WATCHER DATA ####
#### BEGIN VERIFIER DATA ####
ERROR: no interpretation found !
#### END VERIFIER DATA ####