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 wulflinc19 THE 2005-05-27 09:07:34 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23702 boxname=wulflinc19 idbench=1346 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: b6a39917c8daf46435ad718b26e9c6f0 /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-dano3mip.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc19/normalized-mps-v2-13-7-dano3mip.opb IDLAUNCH: 23702 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.037 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 : 3 cpu MHz : 451.037 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: 839000 kB Buffers: 3684 kB Cached: 170748 kB SwapCached: 736 kB Active: 41344 kB Inactive: 135352 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 838748 kB SwapTotal: 2097892 kB SwapFree: 2096432 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5400 kB Slab: 13356 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-27 09:10:23 (client local time) WITH STATUS 139 IN 166.46 SECONDS stats: 23702 7 166.46 139 #### 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 --/oldhome/oroussel/solvers/minisat+_script: line 9: 3809 Segmentation fault $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): 1.13 1.02 0.93 2/54 3805 Raw data (stat): 3805 (runsolver) R 3804 10795 10794 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 854950102 1052672 99 4294967295 134512640 135381576 3221224464 3221219672 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.0014 s] Raw data (loadavg): 1.11 1.02 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0021 s] Raw data (loadavg): 1.09 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0016 s] Raw data (loadavg): 1.08 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0027 s] Raw data (loadavg): 1.06 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0035 s] Raw data (loadavg): 1.05 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 1.04 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0045 s] Raw data (loadavg): 1.04 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0049 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.0058 s] Raw data (loadavg): 1.03 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.006 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+110.006 s] Raw data (loadavg): 1.02 1.01 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+120.007 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 1.01 1.00 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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.008 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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): 1.01 1.00 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 1074634510 0 65536 5 65538 3222414538 0 0 17 1 0 0 Raw data (statm): 531 226 485 147 0 384 0 vsize: 2124 [startup+160.009 s] Raw data (loadavg): 1.01 1.00 0.93 2/55 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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+168.05 s] Raw data (loadavg): 1.00 1.00 0.93 1/53 3809 Raw data (stat): 3805 (minisat+_script) S 3804 10795 10794 0 -1 0 275 239 0 0 0 0 0 1 19 0 1 0 854950102 2174976 226 4294967295 134512640 135087896 3221224528 3221223800 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: 139 Real time (s): 168.05 CPU time (s): 166.46 CPU user time (s): 157.347 CPU system time (s): 9.11261 CPU usage (%): 99.0539 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####