Name | normalized-opb/mps-v2-13-7/MIPLIB/miplib2003/normalized-mps-v2-13-7-dano3mip.opb |
MD5SUM | b6a39917c8daf46435ad718b26e9c6f0 |
Bench Category | optimization, medium integers (OPTMEDINT) |
Has Objective Function | YES |
Satisfiable | |
(Un)Satisfiability was proved | |
Best value of the objective function | |
Optimality of the best value was proved | |
Number of terms in the objective function | 20 |
Biggest coefficient in the objective function | 524288 |
Number of bits for the biggest coefficient in the objective function | 20 |
Sum of the numbers in the objective function | 1048575 |
Number of bits of the sum of numbers in the objective function | 20 |
Biggest number in a constraint | 65536000 |
Number of bits of the biggest number in a constraint | 26 |
Biggest sum of numbers in a constraint | 555744750 |
Number of bits of the biggest sum of numbers | 30 |
Best result obtained on this benchmark | |
Best CPU time to get the best result obtained on this benchmark | |
Number of variables | 266924 |
Total number of constraints | 3778 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 600 |
Number of constraints which are nor clauses,nor cardinality constraints | 3178 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 10600 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc27 THE 2005-04-21 16:36:15 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=17497 boxname=wulflinc27 idbench=1346 idsolver=12 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b6a39917c8daf46435ad718b26e9c6f0 /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-dano3mip.opb REAL COMMAND: minisat+ -cb -gs /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-dano3mip.opb /oldhome/oroussel/tmp/wulflinc27/normalized-mps-v2-13-7-dano3mip.opb IDLAUNCH: 17497 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 888.83 processor : 1 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.169 cache size : 512 KB fdiv_bug : no hlt_bug : no f00f_bug : no coma_bug : no fpu : yes fpu_exception : yes cpuid level : 2 wp : yes flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 mmx fxsr sse bogomips : 899.07 /proc/meminfo: MemTotal: 1034660 kB MemFree: 628212 kB Buffers: 22808 kB Cached: 359520 kB SwapCached: 512 kB Active: 57772 kB Inactive: 326500 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 627960 kB SwapTotal: 2097892 kB SwapFree: 2096472 kB Dirty: 24 kB Writeback: 0 kB Mapped: 5096 kB Slab: 16428 kB Committed_AS: 63592 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-04-21 16:38:23 (client local time) WITH STATUS 0 IN 128.012 SECONDS stats: 17497 7 128.012 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 4450 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: #####################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################=====#=====#=====################################################################################################################################################################################################################################################################################################################################################################################################################################################################################# c -- Clauses(.)/Splits(s): sssssssssssssssssssssssssssssssssssssssssssssssss c ---[4498]---> BDD-cost: 17 c ---[4497]---> BDD-cost: 17 c ---[4496]---> BDD-cost: 17 c ---[4495]---> BDD-cost: 17 c ---[4494]---> BDD-cost: 17 c ---[4493]---> BDD-cost: 17 c ---[4492]---> BDD-cost: 17 c ---[4491]---> BDD-cost: 17 c ---[4490]---> BDD-cost: 17 c ---[4489]---> BDD-cost: 17 c ---[4488]---> BDD-cost: 17 c ---[4487]---> BDD-cost: 17 c ---[4486]---> BDD-cost: 17 c ---[4485]---> BDD-cost: 17 c ---[4484]---> BDD-cost: 17 c ---[4483]---> BDD-cost: 17 c ---[4482]---> BDD-cost: 17 c ---[4481]---> BDD-cost: 17 c ---[4480]---> BDD-cost: 17 c ---[4479]---> BDD-cost: 17 c ---[4478]---> BDD-cost: 17 c ---[4477]---> BDD-cost: 17 c ---[4476]---> BDD-cost: 17 c ---[4475]---> BDD-cost: 17 c ---[4473]---> BDD-cost: 63 c ---[4471]---> BDD-cost: 63 c ---[4469]---> BDD-cost:10393 c ---[4468]---> BDD-cost: 9614 c ---[4467]---> BDD-cost:12191 c ---[4466]---> BDD-cost:11960 c ---[4465]---> BDD-cost:12742 c ---[4464]---> BDD-cost:12742 c ---[4463]---> BDD-cost: 9614 c ---[4462]---> BDD-cost:12742 c ---[4461]---> BDD-cost:12742 c ---[4460]---> BDD-cost:12742 c ---[4459]---> BDD-cost:12742 c ---[4457]---> BDD-cost:10393 c ---[4456]---> BDD-cost:11178 c ---[4455]---> BDD-cost:12742 c ---[4454]---> BDD-cost:12614 c ---[4453]---> BDD-cost:12742 c ---[4452]---> BDD-cost:11178 c ---[4451]---> BDD-cost:12742 c ---[4450]---> BDD-cost:10396 c ---[4449]---> BDD-cost:12742 c ---[4448]---> BDD-cost:11409 c ---[4447]---> BDD-cost:12614 c ---[4445]---> BDD-cost:10393 c ---[4444]---> BDD-cost:12742 c ---[4443]---> BDD-cost:11960 c ---[4442]---> BDD-cost:10396 c ---[4441]---> BDD-cost:12614 c ---[4440]---> BDD-cost: 9614 c ---[4439]---> BDD-cost:13396 c ---[4438]---> BDD-cost:10396 c ---[4437]---> BDD-cost:11832 c ---[4436]---> BDD-cost: 9614 c ---[4435]---> BDD-cost:10396 c ---[4433]---> BDD-cost:10393 c ---[4432]---> BDD-cost:13396 c ---[4431]---> BDD-cost:13396 c ---[4430]---> BDD-cost:10396 c ---[4429]---> BDD-cost:11048 c ---[4428]---> BDD-cost:12614 c ---[4427]---> BDD-cost:13396 c ---[4426]---> BDD-cost:12742 c ---[4425]---> BDD-cost:13396 c ---[4424]---> BDD-cost:12742 c ---[4423]---> BDD-cost:12742 c ---[4421]---> BDD-cost:10393 c ---[4420]---> BDD-cost:12614 c ---[4419]---> BDD-cost: 9614 c ---[4418]---> BDD-cost:12742 c ---[4417]---> BDD-cost:12146 c ---[4416]---> BDD-cost:12742 c ---[4415]---> BDD-cost:10396 c ---[4414]---> BDD-cost:11178 c ---[4413]---> BDD-cost:13396 c ---[4412]---> BDD-cost:11178 c ---[4411]---> BDD-cost:10396 c ---[4409]---> BDD-cost:10393 c ---[4408]---> BDD-cost:11050 c ---[4407]---> BDD-cost:12742 c ---[4406]---> BDD-cost:13396 c ---[4405]---> BDD-cost:11178 c ---[4404]---> BDD-cost:13396 c ---[4403]---> BDD-cost:11178 c ---[4402]---> BDD-cost:12742 c ---[4401]---> BDD-cost:12742 c ---[4400]---> BDD-cost:11178 c ---[4399]---> BDD-cost:12742 c ---[4397]---> BDD-cost:10393 c ---[4396]---> BDD-cost:10582 c ---[4395]---> BDD-cost:11050 c ---[4394]---> BDD-cost:11050 c ---[4393]---> BDD-cost: 9614 c ---[4392]---> BDD-cost:12742 c ---[4391]---> BDD-cost:11960 c ---[4390]---> BDD-cost:12742 c ---[4389]---> BDD-cost:11960 c ---[4388]---> BDD-cost:11178 c ---[4387]---> BDD-cost:11832 c ---[4385]---> BDD-cost:10393 c ---[4384]---> BDD-cost: 9845 c ---[4383]---> BDD-cost:12742 c ---[4382]---> BDD-cost:11960 c ---[4381]---> BDD-cost:11178 c ---[4380]---> BDD-cost: 9614 c ---[4379]---> BDD-cost:10396 c ---[4378]---> BDD-cost:12742 c ---[4377]---> BDD-cost:11960 c ---[4376]---> BDD-cost:12742 c ---[4375]---> BDD-cost:12742 c ---[4373]---> BDD-cost:10393 c ---[4372]---> BDD-cost:12742 c ---[4371]---> BDD-cost:11832 c ---[4370]---> BDD-cost:12614 c ---[4369]---> BDD-cost:11832 c ---[4368]---> BDD-cost:12614 c ---[4367]---> BDD-cost:12742 c ---[4366]---> BDD-cost:13396 c ---[4365]---> BDD-cost:12175 c ---[4364]---> BDD-cost:13396 c ---[4363]---> BDD-cost:11960 c ---[4361]---> BDD-cost:10393 c ---[4360]---> BDD-cost:11178 c ---[4359]---> BDD-cost:12742 c ---[4358]---> BDD-cost:13394 c ---[4357]---> BDD-cost:11960 c ---[4356]---> BDD-cost:12614 c ---[4354]---> BDD-cost:45222 c ---[4352]---> BDD-cost:45357 c ---[4350]---> BDD-cost:45357 c ---[4348]---> BDD-cost:45357 c ---[4346]---> BDD-cost:45357 c ---[4344]---> BDD-cost: 63 c ---[4342]---> BDD-cost:10393 c ---[4340]---> BDD-cost:45357 c ---[4338]---> BDD-cost:45357 c ---[4336]---> BDD-cost:45267 c ---[4334]---> BDD-cost:44995 c ---[4332]---> BDD-cost:44995 c ---[4330]---> BDD-cost:44995 c ---[4328]---> BDD-cost:44995 c ---[4326]---> BDD-cost:44995 c ---[4324]---> BDD-cost:45177 c ---[4322]---> BDD-cost:44995 c ---[4320]---> BDD-cost:10393 c ---[4318]---> BDD-cost:44995 c ---[4316]---> BDD-cost:44995 c ---[4314]---> BDD-cost:44995 c ---[4312]---> BDD-cost:44995 c ---[4310]---> BDD-cost:45222 c ---[4308]---> BDD-cost:45357 c ---[4306]---> BDD-cost:45357 c ---[4304]---> BDD-cost:44995 c ---[4302]---> BDD-cost:44995 c ---[4300]---> BDD-cost:44995 c ---[4298]---> BDD-cost:10393 c ---[4296]---> BDD-cost:44995 c ---[4294]---> BDD-cost:45357 c ---[4292]---> BDD-cost:45312 c ---[4290]---> BDD-cost:45357 c ---[4288]---> BDD-cost:45357 c ---[4286]---> BDD-cost:44995 c ---[4284]---> BDD-cost:44995 c ---[4282]---> BDD-cost:45222 c ---[4280]---> BDD-cost:45357 c ---[4278]---> BDD-cost:45087 c ---[4276]---> BDD-cost:10393 c ---[4274]---> BDD-cost:45357 c ---[4272]---> BDD-cost:45357 c ---[4270]---> BDD-cost:45042 c ---[4268]---> BDD-cost:45128 c ---[4266]---> BDD-cost:44995 c ---[4264]---> BDD-cost:44995 c ---[4262]---> BDD-cost:45312 c ---[4260]---> BDD-cost:45177 c ---[4258]---> BDD-cost:45312 c ---[4256]---> BDD-cost:45357 c ---[4254]---> BDD-cost:10393 c ---[4252]---> BDD-cost:44995 c ---[4250]---> BDD-cost:45177 c ---[4248]---> BDD-cost:44995 c ---[4246]---> BDD-cost:45267 c ---[4244]---> BDD-cost:45267 c ---[4242]---> BDD-cost:44995 c ---[4240]---> BDD-cost:45312 c ---[4238]---> BDD-cost:45312 c ---[4236]---> BDD-cost:45267 c ---[4234]---> BDD-cost:44995 c ---[4232]---> BDD-cost:10393 c ---[4230]---> BDD-cost:44995 c ---[4228]---> BDD-cost:45357 c ---[4226]---> BDD-cost:45357 c ---[4224]---> BDD-cost:44995 c ---[4222]---> BDD-cost:45222 c ---[4220]---> BDD-cost:45357 c ---[4218]---> BDD-cost:45312 c ---[4216]---> BDD-cost:45357 c ---[4214]---> BDD-cost:45312 c ---[4212]---> BDD-cost:45357 c ---[4210]---> BDD-cost:10393 c ---[4208]---> BDD-cost:45267 c ---[4206]---> BDD-cost:45357 c ---[4204]---> BDD-cost:45357 c ---[4202]---> BDD-cost:45267 c ---[4200]---> BDD-cost:45312 c ---[4198]---> BDD-cost:45267 c ---[4196]---> BDD-cost:45312 c ---[4194]---> BDD-cost:45222 c ---[4192]---> BDD-cost:45308 c ---[4190]---> BDD-cost:45357 c ---[4188]---> BDD-cost:10393 c ---[4186]---> BDD-cost:45312 c ---[4184]---> BDD-cost:44995 c ---[4182]---> BDD-cost:44951 c ---[4180]---> BDD-cost:45357 c ---[4178]---> BDD-cost:45357 c ---[4176]---> BDD-cost:44995 c ---[4174]---> BDD-cost:45357 c ---[4172]---> BDD-cost:44995 c ---[4170]---> BDD-cost:44995 c ---[4168]---> BDD-cost:45312 c ---[4166]---> BDD-cost:10393 c ---[4164]---> BDD-cost:45357 c ---[4162]---> BDD-cost:44995 c ---[4160]---> BDD-cost:44995 c ---[4158]---> BDD-cost:45357 c ---[4156]---> BDD-cost:45312 c ---[4154]---> BDD-cost:45177 c ---[4152]---> BDD-cost:45308 c ---[4150]---> BDD-cost:44995 c ---[4148]---> BDD-cost:44995 c ---[4146]---> BDD-cost:44995 c ---[4144]---> BDD-cost:10393 c ---[4142]---> BDD-cost:45177 c ---[4140]---> BDD-cost:45256 c ---[4138]---> BDD-cost:45267 c ---[4136]---> BDD-cost:44995 c ---[4134]---> BDD-cost:45267 c ---[4132]---> BDD-cost:44995 c ---[4130]---> BDD-cost:45357 c ---[4128]---> BDD-cost:45267 c ---[4126]---> BDD-cost:44995 c ---[4124]---> BDD-cost:45177 c ---[4122]---> BDD-cost: 63 c ---[4120]---> BDD-cost:10393 c ---[4118]---> BDD-cost:44995 c ---[4116]---> BDD-cost:44995 c ---[4114]---> BDD-cost:45222 c ---[4112]---> BDD-cost:45357 c ---[4110]---> BDD-cost:44995 c ---[4108]---> BDD-cost:45357 c ---[4106]---> BDD-cost:45357 c ---[4104]---> BDD-cost:45357 c ---[4102]---> BDD-cost:44995 c ---[4100]---> BDD-cost:44995 c ---[4098]---> BDD-cost:10393 c ---[4096]---> BDD-cost:45267 c ---[4094]---> BDD-cost:45312 c ---[4092]---> BDD-cost:44995 c ---[4090]---> BDD-cost:45357 c ---[4088]---> BDD-cost:45312 c ---[4086]---> BDD-cost:45357 c ---[4084]---> BDD-cost:45357 c ---[4082]---> BDD-cost:45357 c ---[4080]---> BDD-cost:45357 c ---[4078]---> BDD-cost:44995 c ---[4076]---> BDD-cost:10393 c ---[4074]---> BDD-cost:45357 c ---[4072]---> BDD-cost:45267 c ---[4070]---> BDD-cost:45357 c ---[4068]---> BDD-cost:44995 c ---[4066]---> BDD-cost:45357 c ---[4064]---> BDD-cost:44995 c ---[4062]---> BDD-cost:45177 c ---[4060]---> BDD-cost:45177 c ---[4058]---> BDD-cost:44995 c ---[4056]---> BDD-cost:44995 c ---[4054]---> BDD-cost:10393 c ---[4052]---> BDD-cost:45222 c ---[4050]---> BDD-cost:44995 c ---[4048]---> BDD-cost:45177 c ---[4046]---> BDD-cost:45312 c ---[4044]---> BDD-cost:44995 c ---[4042]---> BDD-cost:44995 c ---[4040]---> BDD-cost:44951 c ---[4038]---> BDD-cost:44995 c ---[4036]---> BDD-cost:44995 c ---[4034]---> BDD-cost:45312 c ---[4032]---> BDD-cost:10393 c ---[4030]---> BDD-cost:45267 c ---[4028]---> BDD-cost:44963 c ---[4026]---> BDD-cost:45132 c ---[4024]---> BDD-cost:45357 c ---[4022]---> BDD-cost:45357 c ---[4020]---> BDD-cost:45357 c ---[4018]---> BDD-cost:45177 c ---[4016]---> BDD-cost:44995 c ---[4014]---> BDD-cost:44995 c ---[4012]---> BDD-cost:44995 c ---[4010]---> BDD-cost:10393 c ---[4008]---> BDD-cost:45267 c ---[4006]---> BDD-cost:44995 c ---[4004]---> BDD-cost:45357 c ---[4002]---> BDD-cost:44995 c ---[4000]---> BDD-cost:45222 c ---[3998]---> BDD-cost:45312 c ---[3996]---> BDD-cost:44995 c ---[3994]---> BDD-cost:44995 c ---[3992]---> BDD-cost:45267 c ---[3990]---> BDD-cost:45357 c ---[3988]---> BDD-cost:10393 c ---[3986]---> BDD-cost:45357 c ---[3984]---> BDD-cost:45267 c ---[3982]---> BDD-cost:45222 c ---[3980]---> BDD-cost:44995 c ---[3978]---> BDD-cost:45267 c ---[3976]---> BDD-cost:45357 c ---[3974]---> BDD-cost:44995 c ---[3972]---> BDD-cost:45267 c ---[3970]---> BDD-cost:45312 c ---[3968]---> BDD-cost:45267 c ---[3966]---> BDD-cost:10393 c ---[3964]---> BDD-cost:44995 c ---[3962]---> BDD-cost:44995 c ---[3960]---> BDD-cost:45312 c ---[3958]---> BDD-cost:44995 c ---[3956]---> BDD-cost:44995 c ---[3954]---> BDD-cost:44995 c ---[3952]---> BDD-cost:44995 c ---[3950]---> BDD-cost:45222 c ---[3948]---> BDD-cost:45312 c ---[3946]---> BDD-cost:45357 c ---[3944]---> BDD-cost:10393 c ---[3942]---> BDD-cost:45312 c ---[3940]---> BDD-cost:45312 c ---[3938]---> BDD-cost:44995 c ---[3936]---> BDD-cost:45267 c ---[3934]---> BDD-cost:45267 c ---[3932]---> BDD-cost:45222 c ---[3930]---> BDD-cost:45357 c ---[3928]---> BDD-cost:45267 c ---[3926]---> BDD-cost:45312 c ---[3924]---> BDD-cost:45357 c ---[3922]---> BDD-cost:10393 c ---[3920]---> BDD-cost:45357 c ---[3918]---> BDD-cost:45357 c ---[3916]---> BDD-cost:45357 c ---[3914]---> BDD-cost:44995 c ---[3912]---> BDD-cost:44995 c ---[3910]---> BDD-cost:45357 c ---[3908]---> BDD-cost:45222 c ---[3906]---> BDD-cost:45177 c ---[3904]---> BDD-cost:45357 c ---[3902]---> BDD-cost:45357 c ---[3900]---> BDD-cost: 63 c ---[3898]---> BDD-cost:10393 c ---[3896]---> BDD-cost:45357 c ---[3894]---> BDD-cost:44995 c ---[3892]---> BDD-cost:44995 c ---[3890]---> BDD-cost:45222 c ---[3888]---> BDD-cost:45312 c ---[3886]---> BDD-cost:45357 c ---[3884]---> BDD-cost:45267 c ---[3882]---> BDD-cost:44995 c ---[3880]---> BDD-cost:44995 c ---[3878]---> BDD-cost:45357 c ---[3876]---> BDD-cost:10393 c ---[3874]---> BDD-cost:44995 c ---[3872]---> BDD-cost:44951 c ---[3870]---> BDD-cost:45312 c ---[3868]---> BDD-cost:44995 c ---[3866]---> BDD-cost:44995 c ---[3864]---> BDD-cost:45218 c ---[3862]---> BDD-cost:45312 c ---[3860]---> BDD-cost:45312 c ---[3858]---> BDD-cost:45211 c ---[3856]---> BDD-cost:45267 c ---[3854]---> BDD-cost:10393 c ---[3852]---> BDD-cost:45357 c ---[3850]---> BDD-cost:45267 c ---[3848]---> BDD-cost:45312 c ---[3846]---> BDD-cost:45312 c ---[3844]---> BDD-cost:44995 c ---[3842]---> BDD-cost:45166 c ---[3840]---> BDD-cost:45312 c ---[3838]---> BDD-cost:44995 c ---[3836]---> BDD-cost:44995 c ---[3834]---> BDD-cost:45177 c ---[3832]---> BDD-cost:10393 c ---[3830]---> BDD-cost:44995 c ---[3828]---> BDD-cost:45177 c ---[3826]---> BDD-cost:45312 c ---[3824]---> BDD-cost:44946 c ---[3822]---> BDD-cost:44995 c ---[3820]---> BDD-cost:45267 c ---[3818]---> BDD-cost:45312 c ---[3816]---> BDD-cost:44995 c ---[3814]---> BDD-cost:45312 c ---[3812]---> BDD-cost:44995 c ---[3810]---> BDD-cost:10393 c ---[3808]---> BDD-cost:45357 c ---[3806]---> BDD-cost:45312 c ---[3804]---> BDD-cost:44995 c ---[3802]---> BDD-cost:44995 c ---[3800]---> BDD-cost:44995 c ---[3798]---> BDD-cost:45267 c ---[3796]---> BDD-cost:45177 c ---[3794]---> BDD-cost:45357 c ---[3792]---> BDD-cost:44995 c ---[3790]---> BDD-cost:45267 c ---[3788]---> BDD-cost:10393 c ---[3786]---> BDD-cost:45267 c ---[3784]---> BDD-cost:44995 c ---[3782]---> BDD-cost:45357 c ---[3780]---> BDD-cost:45357 c ---[3778]---> BDD-cost:45357 c ---[3776]---> BDD-cost:45357 c ---[3774]---> BDD-cost:44995 c ---[3772]---> BDD-cost:45357 c ---[3770]---> BDD-cost:45177 c ---[3768]---> BDD-cost:45222 c ---[3766]---> BDD-cost:10393 c ---[3764]---> BDD-cost:45312 c ---[3762]---> BDD-cost:45357 c ---[3760]---> BDD-cost:45173 c ---[3758]---> BDD-cost:45267 c ---[3756]---> BDD-cost:45312 c ---[3754]---> BDD-cost:44995 c ---[3752]---> BDD-cost:45222 c ---[3750]---> BDD-cost:45222 c ---[3748]---> BDD-cost:44995 c ---[3746]---> BDD-cost:45267 c ---[3744]---> BDD-cost:10393 c ---[3742]---> BDD-cost:44995 c ---[3740]---> BDD-cost:45357 c ---[3738]---> BDD-cost:45177 c ---[3736]---> BDD-cost:44995 c ---[3734]---> BDD-cost:44995 c ---[3732]---> BDD-cost:44995 c ---[3730]---> BDD-cost:45312 c ---[3728]---> BDD-cost:44995 c ---[3726]---> BDD-cost:44995 c ---[3724]---> BDD-cost:44995 c ---[3722]---> BDD-cost:10393 c ---[3720]---> BDD-cost:44995 c ---[3718]---> BDD-cost:45177 c ---[3716]---> BDD-cost:45129 c ---[3714]---> BDD-cost:44863 c ---[3712]---> BDD-cost:45222 c ---[3710]---> BDD-cost:44842 c ---[3708]---> BDD-cost:44995 c ---[3706]---> BDD-cost:44995 c ---[3704]---> BDD-cost:45223 c ---[3702]---> BDD-cost:44995 c ---[3700]---> BDD-cost:10393 c ---[3698]---> BDD-cost:45223 c ---[3696]---> BDD-cost:44995 c ---[3694]---> BDD-cost:45267 c ---[3692]---> BDD-cost:44995 c ---[3690]---> BDD-cost:45222 c ---[3688]---> BDD-cost:45267 c ---[3686]---> BDD-cost:44995 c ---[3684]---> BDD-cost:45357 c ---[3682]---> BDD-cost:45357 c ---[3680]---> BDD-cost:44995 c ---[3678]---> BDD-cost: 63 c ---[3676]---> BDD-cost:10393 c ---[3674]---> BDD-cost:45357 c ---[3672]---> BDD-cost:45357 c ---[3670]---> BDD-cost:44995 c ---[3668]---> BDD-cost:44995 c ---[3666]---> BDD-cost:44995 c ---[3664]---> BDD-cost:45312 c ---[3662]---> BDD-cost:45312 c --#### END SOLVER DATA #### #### BEGIN WATCHER DATA #### Enforcing CPU limit (will send SIGTERM then SIGKILL): 1200 seconds Enforcing CPUTime (will send SIGXCPU) limit: 1230 seconds Enforcing VSIZE limit: 943718400 bytes Raw data (loadavg): 0.88 0.94 0.92 2/54 21845 Raw data (stat): 21845 (runsolver) R 21844 18865 18864 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 546565338 1052672 99 4294967295 134512640 135381576 3221224432 3221219676 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.0015 s] Raw data (loadavg): 0.89 0.94 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 26824 0 0 0 924 74 0 0 25 0 1 0 546565338 124067840 22418 4294967295 134512640 134672761 3221224528 3221223836 1075372042 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 30290 22418 603 41 0 30249 0 vsize: 121160 [startup+20.0087 s] Raw data (loadavg): 0.91 0.94 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 32069 0 0 0 1912 87 0 0 25 0 1 0 546565338 145498112 27663 4294967295 134512640 134672761 3221224528 3221223920 134580834 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35522 27663 603 41 0 35481 0 vsize: 142088 [startup+30.0145 s] Raw data (loadavg): 0.92 0.94 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 32069 0 0 0 2912 87 0 0 25 0 1 0 546565338 145498112 27663 4294967295 134512640 134672761 3221224528 3221223920 134580756 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35522 27663 603 41 0 35481 0 vsize: 142088 [startup+40.0241 s] Raw data (loadavg): 0.93 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 32069 0 0 0 3913 88 0 0 25 0 1 0 546565338 145498112 27663 4294967295 134512640 134672761 3221224528 3221223920 134581436 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 35522 27663 603 41 0 35481 0 vsize: 142088 [startup+50.0248 s] Raw data (loadavg): 0.94 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 52231 0 0 0 4870 131 0 0 25 0 1 0 546565338 202616832 39503 4294967295 134512640 134672761 3221224528 3221155000 134594161 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 49467 39503 603 41 0 49426 0 vsize: 197868 [startup+60.0257 s] Raw data (loadavg): 0.95 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 91424 0 0 0 5786 215 0 0 25 0 1 0 546565338 291106816 60911 4294967295 134512640 134672761 3221224528 3221212224 134592425 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 71071 60911 603 41 0 71030 0 vsize: 284284 [startup+70.0266 s] Raw data (loadavg): 0.96 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 140931 0 0 0 6676 324 0 0 25 0 1 0 546565338 468877312 97865 4294967295 134512640 134672761 3221224528 3221216400 134523717 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 114472 97865 603 41 0 114431 0 vsize: 457888 [startup+80.0274 s] Raw data (loadavg): 0.96 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 168781 0 0 0 7617 383 0 0 25 0 1 0 546565338 465678336 102824 4294967295 134512640 134672761 3221224528 3221181040 134594592 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 113691 102824 603 41 0 113650 0 vsize: 454764 [startup+90.0282 s] Raw data (loadavg): 0.97 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 204145 0 0 0 8542 459 0 0 25 0 1 0 546565338 617099264 122528 4294967295 134512640 134672761 3221224528 3221184480 134522994 0 0 5 16386 0 0 0 17 1 0 0 Raw data (statm): 150659 122528 603 41 0 150618 0 vsize: 602636 [startup+100.029 s] Raw data (loadavg): 0.97 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 259635 0 0 0 9412 588 0 0 25 0 1 0 546565338 809103360 172176 4294967295 134512640 134672761 3221224528 3221196720 134523741 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 197535 172176 603 41 0 197494 0 vsize: 790140 [startup+110.03 s] Raw data (loadavg): 0.98 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 286559 0 0 0 10348 652 0 0 25 0 1 0 546565338 761565184 166119 4294967295 134512640 134672761 3221224528 3221208088 1075350517 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 185929 166120 603 41 0 185888 0 vsize: 743716 [startup+120.029 s] Raw data (loadavg): 0.98 0.95 0.92 2/54 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 321610 0 0 0 11269 731 0 0 25 0 1 0 546565338 811659264 185552 4294967295 134512640 134672761 3221224528 3221164560 134594086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 198159 185552 603 41 0 198118 0 vsize: 792636 [startup+128.032 s] Raw data (loadavg): 0.98 0.95 0.92 1/53 21845 Raw data (stat): 21845 (minisat+) R 21844 18865 18864 0 -1 0 321610 0 0 0 11269 731 0 0 25 0 1 0 546565338 811659264 185552 4294967295 134512640 134672761 3221224528 3221164560 134594086 0 0 5 16386 0 0 0 17 0 0 0 Raw data (statm): 198159 185552 603 41 0 198118 0 vsize: 0 Child ended because it received signal 11 (SIGSEGV) Real time (s): 128.032 CPU time (s): 128.012 CPU user time (s): 119.726 CPU system time (s): 8.28574 CPU usage (%): 99.9843 Max. virtual memory (Kb): 792636 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####