Name | normalized-opb/mps-v2-20-10/MIPLIB/miplib2003/normalized-mps-v2-20-10-atlanta-ip.opb |
MD5SUM | 0a1ff370c051d88127ca8cdb722ca490 |
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 | 31296 |
Biggest coefficient in the objective function | 1700000000000 |
Number of bits for the biggest coefficient in the objective function | 41 |
Sum of the numbers in the objective function | 81421012358779 |
Number of bits of the sum of numbers in the objective function | 47 |
Biggest number in a constraint | 1700000000000 |
Number of bits of the biggest number in a constraint | 41 |
Biggest sum of numbers in a constraint | 81421012358779 |
Number of bits of the biggest sum of numbers | 47 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.893863 |
Number of variables | 77286 |
Total number of constraints | 70354 |
Number of constraints which are clauses | 2311 |
Number of constraints which are cardinality constraints (but not clauses) | 47534 |
Number of constraints which are nor clauses,nor cardinality constraints | 20509 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 2790 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc7 THE 2005-05-27 06:58:33 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=23316 boxname=wulflinc7 idbench=960 idsolver=16 numberseed=0 MD5SUM SOLVER: MD5SUM BENCH: 0a1ff370c051d88127ca8cdb722ca490 /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-atlanta-ip.opb REAL COMMAND: minisat+_script -cb -gs /oldhome/oroussel/tmp/wulflinc7/normalized-mps-v2-20-10-atlanta-ip.opb IDLAUNCH: 23316 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.050 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.050 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: 840192 kB Buffers: 33664 kB Cached: 139860 kB SwapCached: 692 kB Active: 62712 kB Inactive: 112936 kB HighTotal: 131008 kB HighFree: 29232 kB LowTotal: 903652 kB LowFree: 810960 kB SwapTotal: 2097136 kB SwapFree: 2095524 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5084 kB Slab: 13212 kB Committed_AS: 63604 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-27 06:59:59 (client local time) WITH STATUS 139 IN 85.819 SECONDS stats: 23316 7 85.819 139 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c Parsing PB file... c Converting 30320 PB-constraints to clauses... c -- Unit propagations: pppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppppp c -- Detecting intervals from adjacent constraints: ###########################################################################################################################################################################################################################################################################################################################################################################################=#============#=====#===#=====#=======#====#===============#=#===============##===#===############################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################################## c -- Clauses(.)/Splits(s): .....................................................ssssss...............................................ssssssssssss.............................ssss.s.ss.s................................ssssssss..ss.ssss.............................ssssssssss..............................ssssss..............................ss...................................s..sssssssssssss.........................ss.......s.s..................................ssssssssssssssss.....................ssssssssssssss.ssssssss.s........................ss.s.ssssssssssss.................................ssssss......................................sssssss...sssssssss...............................s.s.ss.ssssssss...............sssss.....................................s.sss...............................sssssssssssssss.............................sssssssssss..............................sssssssssssssssss................................ssssss.s.ss......................................sssssssssssss.................................ssssssss...............................ssssssssss.......................................ssssssssssssssssss........................ssssssssssss.......................sssssssssss.............................sssssssssssssssssssss...................ssssssssssssssss................................ssssssssssss...................sssssss..............ssssssssssssssssssssssssss.......................ssssssssssssssssssssssssssss.............sssssssssssssssssssssssssss...................sssssssssssssssssssssssss......................sssssssssssssssssssss....................sssssssssssssssssssssssssssss....................sssssssssssssssssssssssss..................ssssssssssssssssssssssss....................ssssss...................sssssssssssssss........................ssssssss............................ssss..ssss................ssssssssssssssssss................................ssssssssssssssssss...............sssssssssssss...........sssssssssssssssssssssssssss.......ssssssssssssssss..........sssssssssssssssss....ssssssssssssssssssssss........sssssssss..................ssssssssssss..............sss........sssssssssssss......................ssssssssssssss..............ssss..sssssssss.ssssss.sss..............ssssssssssssss...................ssssssssss...........ssssssssss..............ssssssssssssssssssssssss........................sssssssssssssssss..............ssss............................sssssssssssssssss...........sssssssssssssss...........ssssssss.............ssssssssssss......sssssssssssssss..........ssssssss........sssssssssssssss........sssss.......sssssssssss.....ssssss...........sssss.................sss.......s...ss...........ssssssssssssssssssssss.......................ssssss.........sssssssssssssssssssss..................ssssss.s..ssss..........................sssssssssss.s.......................sssss...........sss....ssssssss.........ssss.ssssssssss.........................sssssssss....................ssssss.ssssssssss.s................sssssssssss.sssssssssss..........ssssssssss.......ssssssssssss....sssssssss.......sss....s........ssssssssssssssssssssssssss......ssssssssssssss.........ssssssss.s.s.s.s.....ssssssssss......ssssssssssssss......sssssssssssss..sssssssssssssss....sssssssssss...sssss......ssssss..s.sss.ssss.......ssssssssssssssssssssssss.sssssssssssssssss...sssss.......sss.........sssss.............sssssssssssssssssssss.......ssssssssssssssssssssssssssss......................ss.ss............sssssssssssssssssssssssss.....sss....ssssssssssssssssssssss.........sssssssssssssssssssssss........sssssssssss....ssssssssssssssssss.......ssssssssssssssssssssssssss............ssssssssssssssssss..........ssssssss..ssssssssssssssssssssssss........ssssssssssssssssssss..........ssss...sss...s............sssssssssssssssssssssssssss.........sssssssssssssssssss.............ssssssss.....ssssssssss........sssss....ssss..sssssssssssssssss............sss....ssssssssssss.......sssssssssss........sssssssssss...sssssssssssssssss............ss.....s..s.sss........ssssssssssssssssss.......sssssssssssssss.......ssssssss....sssssssss.........sssssssssssssssssssss....ssssssssssssssss...ssssssssss.............ssssssssss....ssssssssssssss.ssssssssss....sssss...ssssssssssssssssssssss..........ssssssssss....sssssss...ssssssssssssssssssssss...ssssssssssssssssssss......ss......ssssssssssssssssssssssssss.......ssssssssssss.......ssss.sss..sssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssssss................................................................................................................................................................................ c ---[32480]---> BDD-cost: 10 c ---[32479]---> BDD-cost: 10 c ---[32477]---> BDD-cost: 12 c ---[32476]---> BDD-cost: 13 c ---[32475]---> BDD-cost: 14 c ---[32473]---> BDD-cost: 10 c ---[32471]---> BDD-cost: 12 c ---[32470]---> BDD-cost: 13 c ---[32469]---> BDD-cost: 14 c ---[32467]---> BDD-cost: 10 c ---[32465]---> BDD-cost: 12 c ---[32464]---> BDD-cost: 13 c ---[32463]---> BDD-cost: 14 c ---[32461]---> BDD-cost: 10 c ---[32459]---> BDD-cost: 12 c ---[32458]---> BDD-cost: 13 c ---[32457]---> BDD-cost: 14 c ---[32455]---> BDD-cost: 10 c ---[32453]---> BDD-cost: 12 c ---[32452]---> BDD-cost: 13 c ---[32451]---> BDD-cost: 14 c ---[32449]---> BDD-cost: 10 c ---[32447]---> BDD-cost: 12 c ---[32446]---> BDD-cost: 13 c ---[32445]---> BDD-cost: 14 c ---[32443]---> BDD-cost: 10 c ---[32441]---> BDD-cost: 12 c ---[32440]---> BDD-cost: 13 c ---[32439]---> BDD-cost: 14 c ---[32437]---> BDD-cost: 10 c ---[32435]---> BDD-cost: 12 c ---[32434]---> BDD-cost: 13 c ---[32433]---> BDD-cost: 14 c ---[32431]---> BDD-cost: 10 c ---[32429]---> BDD-cost: 12 c ---[32428]---> BDD-cost: 13 c ---[32427]---> BDD-cost: 14 c ---[32425]---> BDD-cost: 10 c ---[32423]---> BDD-cost: 12 c ---[32422]---> BDD-cost: 13 c ---[32421]---> BDD-cost: 14 c ---[32419]---> BDD-cost: 10 c ---[32417]---> BDD-cost: 12 c ---[32416]---> BDD-cost: 13 c ---[32415]---> BDD-cost: 14 c ---[32413]---> BDD-cost: 10 c ---[32411]---> BDD-cost: 12 c ---[32410]---> BDD-cost: 13 c ---[32409]---> BDD-cost: 14 c ---[32407]---> BDD-cost: 10 c ---[32405]---> BDD-cost: 12 c ---[32404]---> BDD-cost: 13 c ---[32403]---> BDD-cost: 14 c ---[32401]---> BDD-cost: 10 c ---[32399]---> BDD-cost: 12 c ---[32398]---> BDD-cost: 13 c ---[32397]---> BDD-cost: 14 c ---[32395]---> BDD-cost: 10 c ---[32393]---> BDD-cost: 12 c ---[32392]---> BDD-cost: 13 c ---[32391]---> BDD-cost: 14 c ---[32389]---> BDD-cost: 10 c ---[32387]---> BDD-cost: 12 c ---[32386]---> BDD-cost: 13 c ---[32385]---> BDD-cost: 14 c ---[32383]---> BDD-cost: 10 c ---[32381]---> BDD-cost: 12 c ---[32380]---> BDD-cost: 13 c ---[32379]---> BDD-cost: 14 c ---[32377]---> BDD-cost: 10 c ---[32375]---> BDD-cost: 12 c ---[32374]---> BDD-cost: 13 c ---[32373]---> BDD-cost: 14 c ---[32371]---> BDD-cost: 10 c ---[32369]---> BDD-cost: 12 c ---[32368]---> BDD-cost: 13 c ---[32367]---> BDD-cost: 14 c ---[32365]---> BDD-cost: 10 c ---[32363]---> BDD-cost: 12 c ---[32362]---> BDD-cost: 13 c ---[32361]---> BDD-cost: 14 c ---[32359]---> BDD-cost: 10 c ---[32357]---> BDD-cost: 12 c ---[32356]---> BDD-cost: 13 c ---[32355]---> BDD-cost: 14 c ---[32353]---> BDD-cost: 10 c ---[32351]---> BDD-cost: 12 c ---[32350]---> BDD-cost: 13 c ---[32349]---> BDD-cost: 14 c ---[32347]---> BDD-cost: 11 c ---[32346]---> BDD-cost: 11 c ---[32344]---> BDD-cost: 13 c ---[32343]---> BDD-cost: 14 c ---[32342]---> BDD-cost: 15 c ---[32340]---> BDD-cost: 11 c ---[32338]---> BDD-cost: 13 c ---[32337]---> BDD-cost: 14 c ---[32336]---> BDD-cost: 15 c ---[32334]---> BDD-cost: 11 c ---[32332]---> BDD-cost: 13 c ---[32331]---> BDD-cost: 14 c ---[32330]---> BDD-cost: 15 c ---[32328]---> BDD-cost: 11 c ---[32326]---> BDD-cost: 13 c ---[32325]---> BDD-cost: 14 c ---[32324]---> BDD-cost: 15 c ---[32322]---> BDD-cost: 11 c ---[32320]---> BDD-cost: 13 c ---[32319]---> BDD-cost: 14 c ---[32318]---> BDD-cost: 15 c ---[32316]---> BDD-cost: 11 c ---[32314]---> BDD-cost: 13 c ---[32313]---> BDD-cost: 14 c ---[32312]---> BDD-cost: 15 c ---[32310]---> BDD-cost: 11 c ---[32308]---> BDD-cost: 13 c ---[32307]---> BDD-cost: 14 c ---[32306]---> BDD-cost: 15 c ---[32304]---> BDD-cost: 11 c ---[32302]---> BDD-cost: 13 c ---[32301]---> BDD-cost: 14 c ---[32300]---> BDD-cost: 15 c ---[32298]---> BDD-cost: 11 c ---[32296]---> BDD-cost: 13 c ---[32295]---> BDD-cost: 14 c ---[32294]---> BDD-cost: 15 c ---[32292]---> BDD-cost: 11 c ---[32290]---> BDD-cost: 13 c ---[32289]---> BDD-cost: 14 c ---[32288]---> BDD-cost: 15 c ---[32286]---> BDD-cost: 11 c ---[32284]---> BDD-cost: 13 c ---[32283]---> BDD-cost: 14 c ---[32282]---> BDD-cost: 15 c ---[32280]---> BDD-cost: 11 c ---[32278]---> BDD-cost: 13 c ---[32277]---> BDD-cost: 14 c ---[32276]---> BDD-cost: 15 c ---[32274]---> BDD-cost: 11 c ---[32272]---> BDD-cost: 13 c ---[32271]---> BDD-cost: 14 c ---[32270]---> BDD-cost: 15 c ---[32268]---> BDD-cost: 11 c ---[32266]---> BDD-cost: 13 c ---[32265]---> BDD-cost: 14 c ---[32264]---> BDD-cost: 15 c ---[32262]---> BDD-cost: 11 c ---[32260]---> BDD-cost: 13 c ---[32259]---> BDD-cost: 14 c ---[32258]---> BDD-cost: 15 c ---[32256]---> BDD-cost: 11 c ---[32254]---> BDD-cost: 13 c ---[32253]---> BDD-cost: 14 c ---[32252]---> BDD-cost: 15 c ---[32250]---> BDD-cost: 11 c ---[32248]---> BDD-cost: 13 c ---[32247]---> BDD-cost: 14 c ---[32246]---> BDD-cost: 15 c ---[32244]---> BDD-cost: 11 c ---[32242]---> BDD-cost: 13 c ---[32241]---> BDD-cost: 14 c ---[32240]---> BDD-cost: 15 c ---[32238]---> BDD-cost: 11 c ---[32236]---> BDD-cost: 13 c ---[32235]---> BDD-cost: 14 c ---[32234]---> BDD-cost: 15 c ---[32232]---> BDD-cost: 11 c ---[32230]---> BDD-cost: 13 c ---[32229]---> BDD-cost: 14 c ---[32228]---> BDD-cost: 15 c ---[32226]---> BDD-cost: 11 c ---[32224]---> BDD-cost: 13 c ---[32223]---> BDD-cost: 14 c ---[32222]---> BDD-cost: 15 c ---[32220]---> BDD-cost: 11 c ---[32218]---> BDD-cost: 13 c ---[32217]---> BDD-cost: 14 c ---[32216]---> BDD-cost: 15 c ---[32214]---> BDD-cost: 11 c ---[32212]---> BDD-cost: 13 c ---[32211]---> BDD-cost: 14 c ---[32210]---> BDD-cost: 15 c ---[32208]---> BDD-cost: 11 c ---[32206]---> BDD-cost: 13 c ---[32205]---> BDD-cost: 14 c ---[32204]---> BDD-cost: 15 c ---[32202]---> BDD-cost: 11 c ---[32200]---> BDD-cost: 13 c ---[32199]---> BDD-cost: 14 c ---[32198]---> BDD-cost: 15 c ---[32196]---> BDD-cost: 11 c ---[32194]---> BDD-cost: 13 c ---[32193]---> BDD-cost: 14 c ---[32192]---> BDD-cost: 15 c ---[32190]---> BDD-cost: 11 c ---[32188]---> BDD-cost: 13 c ---[32187]---> BDD-cost: 14 c ---[32186]---> BDD-cost: 15 c ---[32184]---> BDD-cost: 11 c ---[32182]---> BDD-cost: 13 c ---[32181]---> BDD-cost: 14 c ---[32180]---> BDD-cost: 15 c ---[32178]---> BDD-cost: 11 c ---[32176]---> BDD-cost: 13 c ---[32175]---> BDD-cost: 14 c ---[32174]---> BDD-cost: 15 c ---[32172]---> BDD-cost: 11 c ---[32170]---> BDD-cost: 13 c ---[32169]---> BDD-cost: 14 c ---[32168]---> BDD-cost: 15 c ---[32166]---> BDD-cost: 11 c ---[32164]---> BDD-cost: 13 c ---[32163]---> BDD-cost: 14 c ---[32162]---> BDD-cost: 15 c ---[32160]---> BDD-cost: 11 c ---[32158]---> BDD-cost: 13 c ---[32157]---> BDD-cost: 14 c ---[32156]---> BDD-cost: 15 c ---[32154]---> BDD-cost: 11 c ---[32152]---> BDD-cost: 13 c ---[32151]---> BDD-cost: 14 c ---[32150]---> BDD-cost: 15 c ---[32148]---> BDD-cost: 11 c ---[32146]---> BDD-cost: 13 c ---[32145]---> BDD-cost: 14 c ---[32144]---> BDD-cost: 15 c ---[32142]---> BDD-cost: 11 c ---[32140]---> BDD-cost: 13 c ---[32139]---> BDD-cost: 14 c ---[32138]---> BDD-cost: 15 c ---[32136]---> BDD-cost: 11 c ---[32134]---> BDD-cost: 13 c ---[32133]---> BDD-cost: 14 c ---[32132]---> BDD-cost: 15 c ---[32130]---> BDD-cost: 11 c ---[32128]---> BDD-cost: 13 c ---[32127]---> BDD-cost: 14 c ---[32126]---> BDD-cost: 15 c ---[32124]---> BDD-cost: 11 c ---[32122]---> BDD-cost: 13 c ---[32121]---> BDD-cost: 14 c ---[32120]---> BDD-cost: 15 c ---[32118]---> BDD-cost: 11 c ---[32116]---> BDD-cost: 13 c ---[32115]---> BDD-cost: 14 c ---[32114]---> BDD-cost: 15 c ---[32112]---> BDD-cost: 11 c ---[32110]---> BDD-cost: 13 c ---[32109]---> BDD-cost: 14 c ---[32108]---> BDD-cost: 15 c ---[32106]---> BDD-cost: 11 c ---[32104]---> BDD-cost: 13 c ---[32103]---> BDD-cost: 14 c ---[32102]---> BDD-cost: 15 c ---[32100]---> BDD-cost: 11 c ---[32098]---> BDD-cost: 13 c ---[32097]---> BDD-cost: 14 c ---[32096]---> BDD-cost: 15 c ---[32094]---> BDD-cost: 11 c ---[32092]---> BDD-cost: 13 c ---[32091]---> BDD-cost: 14 c ---[32090]---> BDD-cost: 15 c ---[32088]---> BDD-cost: 11 c ---[32086]---> BDD-cost: 13 c ---[32085]---> BDD-cost: 14 c ---[32084]---> BDD-cost: 15 c ---[32082]---> BDD-cost: 11 c ---[32080]---> BDD-cost: 13 c ---[32079]---> BDD-cost: 14 c ---[32078]---> BDD-cost: 15 c ---[32076]---> BDD-cost: 11 c ---[32074]---> BDD-cost: 13 c ---[32073]---> BDD-cost: 14 c ---[32072]---> BDD-cost: 15 c ---[32070]---> BDD-cost: 11 c ---[32068]---> BDD-cost: 13 c ---[32067]---> BDD-cost: 14 c ---[32066]---> BDD-cost: 15 c ---[32064]---> BDD-cost: 11 c ---[32062]---> BDD-cost: 13 c ---[32061]---> BDD-cost: 14 c ---[32060]---> BDD-cost: 15 c ---[32058]---> BDD-cost: 11 c ---[32056]---> BDD-cost: 13 c ---[32055]---> BDD-cost: 14 c ---[32054]---> BDD-cost: 15 c ---[32052]---> BDD-cost: 11 c ---[32050]---> BDD-cost: 13 c ---[32049]---> BDD-cost: 14 c ---[32048]---> BDD-cost: 15 c ---[32046]---> BDD-cost: 11 c ---[32044]---> BDD-cost: 13 c ---[32043]---> BDD-cost: 14 c ---[32042]---> BDD-cost: 15 c ---[32040]---> BDD-cost: 11 c ---[32038]---> BDD-cost: 13 c ---[32037]---> BDD-cost: 14 c ---[32036]---> BDD-cost: 15 c ---[32034]---> BDD-cost: 11 c ---[32032]---> BDD-cost: 13 c ---[32031]---> BDD-cost: 14 c ---[32030]---> BDD-cost: 15 c ---[32028]---> BDD-cost: 11 c ---[32026]---> BDD-cost: 13 c ---[32025]---> BDD-cost: 14 c ---[32024]---> BDD-cost: 15 c ---[32022]---> BDD-cost: 11 c ---[32020]---> BDD-cost: 13 c ---[32019]---> BDD-cost: 14 c ---[32018]---> BDD-cost: 15 c ---[32016]---> BDD-cost: 11 c ---[32014]---> BDD-cost: 13 c ---[32013]---> BDD-cost: 14 c ---[32012]---> BDD-cost: 15 c ---[32010]---> BDD-cost: 11 c ---[32008]---> BDD-cost: 13 c ---[32007]---> BDD-cost: 14 c ---[32006]---> BDD-cost: 15 c ---[32004]---> BDD-cost: 11 c ---[32002]---> BDD-cost: 13 c ---[32001]---> BDD-cost: 14 c ---[32000]---> BDD-cost: 15 c ---[31998]---> BDD-cost: 11 c ---[31996]---> BDD-cost: 13 c ---[31995]---> BDD-cost: 14 c ---[31994]---> BDD-cost: 15 c ---[31992]---> BDD-cost: 11 c ---[31990]---> BDD-cost: 13 c ---[31989]---> BDD-cost: 14 c ---[31988]---> BDD-cost: 15 c ---[31986]---> BDD-cost: 11 c ---[31984]---> BDD-cost: 13 c ---[31983]---> BDD-cost: 14 c ---[31982]---> BDD-cost: 15 c ---[31980]---> BDD-cost: 11 c ---[31978]---> BDD-cost: 13 c ---[31977]---> BDD-cost: 14 c ---[31976]---> BDD-cost: 15 c ---[31974]---> BDD-cost: 11 c ---[31972]---> BDD-cost: 13 c ---[31971]---> BDD-cost: 14 c ---[31970]---> BDD-cost: 15 c ---[31968]---> BDD-cost: 11 c ---[31966]---> BDD-cost: 13 c ---[31965]---> BDD-cost: 14 c ---[31964]---> BDD-cost: 15 c ---[31962]---> BDD-cost: 11 c ---[31960]---> BDD-cost: 13 c ---[31959]---> BDD-cost: 14 c ---[31958]---> BDD-cost: 15 c ---[31956]---> BDD-cost: 11 c ---[31954]---> BDD-cost: 13 c ---[31953]---> BDD-cost: 14 c ---[31952]---> BDD-cost: 15 c ---[31950]---> BDD-cost: 11 c ---[31948]---> BDD-cost: 13 c ---[31947]---> BDD-cost: 14 c ---[31946]---> BDD-cost: 15 c ---[31944]---> BDD-cost: 11 c ---[31942]---> BDD-cost: 13 c ---[31941]---> BDD-cost: 14 c ---[31940]---> BDD-cost: 15 c ---[31938]---> BDD-cost: 11 c ---[31936]---> BDD-cost: 13 c ---[31935]---> BDD-cost: 14 c ---[31934]---> BDD-cost: 15 c ---[31932]---> BDD-cost: 11 c ---[31930]---> BDD-cost: 13 c ---[31929]---> BDD-cost: 14 c ---[31928]---> BDD-cost: 15 c ---[31926]---> BDD-cost: 11 c ---[31924]---> BDD-cost: 13 c ---[31923]---> BDD-cost: 14 c ---[31922]---> BDD-cost: 15 c ---[31920]---> BDD-cost: 11 c ---[31918]---> BDD-cost: 13 c ---[31917]---> BDD-cost: 14 c ---[31916]---> BDD-cost: 15 c ---[31914]---> BDD-cost: 11 c ---[31912]---> BDD-cost: 13 c ---[31911]---> BDD-cost: 14 c ---[31910]---> BDD-cost: 15 c ---[31908]---> BDD-cost: 11 c ---[31906]---> BDD-cost: 13 c ---[31905]---> BDD-cost: 14 c ---[31904]---> BDD-cost: 15 c ---[31902]---> BDD-cost: 11 c ---[31900]---> BDD-cost: 13 c ---[31899]---> BDD-cost: 14 c ---[31898]---> BDD-cost: 15 c ---[31896]---> BDD-cost: 11 c ---[31894]---> BDD-cost: 13 c ---[31893]---> BDD-cost: 14 c ---[31892]---> BDD-cost: 15 c ---[31890]---> BDD-cost: 11 c ---[31888]---> BDD-cost: 13 c ---[31887]---> BDD-cost: 14 c ---[31886]---> BDD-cost: 15 c ---[31884]---> BDD-cost: 11 c ---[31882]---> BDD-cost: 13 c ---[31881]---> BDD-cost: 14 c ---[31880]---> BDD-cost: 15 c ---[31878]---> BDD-cost: 11 c ---[31876]---> BDD-cost: 13 c ---[31875]---> BDD-cost: 14 c ---[31874]---> BDD-cost: 15 c ---[31872]---> BDD-cost: 11 c ---[31870]---> BDD-cost: 13 c ---[31869]---> BDD-cost: 14 c ---[31868]---> BDD-cost: 15 c ---[31866]---> BDD-cost: 11 c ---[31864]---> BDD-cost: 13 c ---[31863]---> BDD-cost: 14 c ---[31862]---> BDD-cost: 15 c ---[31860]---> BDD-cost: 11 c ---[31858]---> BDD-cost: 13 c ---[31857]---> BDD-cost: 14 c ---[31856]---> BDD-cost: 15 c ---[31854]---> BDD-cost: 11 c ---[31852]---> BDD-cost: 13 c ---[31851]---> BDD-cost: 14 c ---[31850]---> BDD-cost: 15 c ---[31848]---> BDD-cost: 11 c ---[31846]---> BDD-cost: 13 c ---[31845]---> BDD-cost: 14 c ---[31844]---> BDD-cost: 15 c ---[31842]---> BDD-cost: 11 c ---[31840]---> BDD-cost: 13 c ---[31839]---> BDD-cost: 14 c ---[31838]---> BDD-cost: 15 c ---[31836]---> BDD-cost: 11 c ---[31834]---> BDD-cost: 13 c ---[31833]---> BDD-cost: 14 c ---[31832]---> BDD-cost: 15 c ---[31830]---> BDD-cost: 11 c ---[31828]---> BDD-cost: 13 c ---[31827]---> BDD-cost: 14 c ---[31826]---> BDD-cost: 15 c ---[31824]---> BDD-cost: 11 c ---[31822]---> BDD-cost: 13 c ---[31821]---> BDD-cost: 14 c ---[31820]---> BDD-cost: 15 c ---[31818]---> BDD-cost: 11 c ---[31816]---> BDD-cost: 13 c ---[31815]---> BDD-cost: 14 c ---[31814]---> BDD-cost: 15 c ---[31812]---> BDD-cost: 11 c ---[31810]---> BDD-cost: 13 c ---[31809]---> BDD-cost: 14 c ---[31808]---> BDD-cost: 15 c ---[31806]---> BDD-cost: 11 c ---[31804]---> BDD-cost: 13 c ---[31803]---> BDD-cost: 14 c ---[31802]---> BDD-cost: 15 c ---[31800]---> BDD-cost: 11 c ---[31798]---> BDD-cost: 13 c ---[31797]---> BDD-cost: 14 c ---[31796]---> BDD-cost: 15 c ---[31794]---> BDD-cost: 11 c ---[31792]---> BDD-cost: 13 c ---[31791]---> BDD-cost: 14 c ---[31790]---> BDD-cost: 15 c ---[31788]---> BDD-cost: 11 c ---[31786]---> BDD-cost: 13 c ---[31785]---> BDD-cost: 14 c ---[31784]---> BDD-cost: 15 c ---[31782]---> BDD-cost: 11 c ---[31780]---> BDD-cost: 13 c ---[31779]---> BDD-cost: 14 c ---[31778]---> BDD-cost: 15 c ---[31776]---> BDD-cost: 11 c ---[31774]---> BDD-cost: 13 c ---[31773]---> BDD-cost: 14 c ---[31772]---> BDD-cost: 15 c ---[31770]---> BDD-cost: 11 c ---[31768]---> BDD-cost: 13 c ---[31767]---> BDD-cost: 14 c ---[31766]---> BDD-cost: 15 c ---[31764]---> BDD-cost: 11 c ---[31762]---> BDD-cost: 13 c ---[31761]---> BDD-cost: 14 c ---[31760]---> BDD-cost: 15 c ---[31758]---> BDD-cost: 11 c ---[31756]---> BDD-cost: 13 c ---[31755]---> BDD-cost: 14 c ---[31754]---> BDD-cost: 15 c ---[31752]---> BDD-cost: 11 c ---[31750]---> BDD-cost: 13 c ---[31749]---> BDD-cost: 14 c ---[31748]---> BDD-cost: 15 c ---[31746]---> BDD-cost: 11 c ---[31744]---> BDD-cost: 13 c ---[31743]---> BDD-cost: 14 c ---[31742]---> BDD-cost: 15 c ---[31740]---> BDD-cost: 11 c ---[31738]---> BDD-cost: 13 c ---[31737]---> BDD-cost: 14 c ---[31736]---> BDD-cost: 15 c ---[31734]---> BDD-cost: 11 c ---[31732]---> BDD-cost: 13 c ---[31731]---> BDD-cost: 14 c ---[31730]---> BDD-cost: 15 c ---[31728]---> BDD-cost: 11 c ---[31726]---> BDD-cost: 13 c ---[31725]---> BDD-cost: 14 c ---[31724]---> BDD-cost: 15 c ---[31722]---> BDD-cost: 11 c ---[31720]---> BDD-cost: 13 c ---[31719]---> BDD-cost: 14 c ---[31718]---> BDD-cost: 15 c ---[31716]---> BDD-cost: 11 c ---[31714]---> BDD-cost: 13 c ---[31713]---> BDD-cost: 14 c ---[31712]---> BDD-cost: 15 c ---[31710]---> BDD-cost: 11 c ---[31708]---> BDD-cost: 13 c ---[31707]---> BDD-cost: 14 c ---[31706]---> BDD-cost: 15 c ---[31704]---> BDD-cost: 11 c ---[31702]---> BDD-cost: 13 c ---[31701]---> BDD-cost: 14 c ---[31700]---> BDD-cost: 15 c ---[31698]---> BDD-cost: 11 c ---[31696]---> BDD-cost: 13 c ---[31695]---> BDD-cost: 14 c ---[31694]---> BDD-cost: 15 c ---[31692]---> BDD-cost: 11 c ---[31690]---> BDD-cost: 13 c ---[31689]---> BDD-cost: 14 c ---[31688]---> BDD-cost: 15 c ---[31686]---> BDD-cost: 11 c ---[31684]---> BDD-cost: 13 c ---[31683]---> BDD-cost: 14 c ---[31682]---> BDD-cost: 15 c ---[31680]---> BDD-cost: 11 c ---[31678]---> BDD-cost: 13 c ---[31677]---> BDD-cost: 14 c ---[31676]---> BDD-cost: 15 c ---[31674]---> BDD-cost: 11 c ---[31672]---> BDD-cost: 13 c ---[31671]---> BDD-cost: 14 c ---[31670]---> BDD-cost: 15 c ---[31668]---> BDD-cost: 11 c ---[31666]---> BDD-cost: 13 c ---[31665]---> BDD-cost: 14 c ---[31664]---> BDD-cost: 15 c ---[31662]---> BDD-cost: 11 c ---[31660]---> BDD-cost: 13 c ---[31659]---> BDD-cost: 14 c ---[31658]---> BDD-cost: 15 c ---[31656]---> BDD-cost: 11 c ---[31654]---> BDD-cost: 13 c ---[31653]---> BDD-cost: 14 c ---[31652]---> BDD-cost: 15 c ---[31650]---> BDD-cost: 11 c ---[31648]---> BDD-cost: 13 c ---[31647]---> BDD-cost: 14 c ---[31646]---> BDD-cost: 15 c ---[31644]---> BDD-cost: 11 c ---[31642]---> BDD-cost: 13 c ---[31641]---> BDD-cost: 14 c ---[31640]---> BDD-cost: 15 c ---[31638]---> BDD-cost: 11 c ---[31636]---> BDD-cost: 13 c ---[31635]---> BDD-cost: 14 c ---[31634]---> BDD-cost: 15 c ---[31632]---> BDD-cost: 11 c ---[31630]---> BDD-cost: 13 c ---[31629]---> BDD-cost: 14 c ---[31628]---> BDD-cost: 15 c ---[31626]---> BDD-cost: 11 c ---[31624]---> BDD-cost: 13 c ---[31623]---> BDD-cost: 14 c ---[31622]---> BDD-cost: 15 c ---[31620]---> BDD-cost: 11 c ---[31618]---> BDD-cost: 13 c ---[31617]---> BDD-cost: 14 c ---[31616]---> BDD-cost: 15 c ---[31614]---> BDD-cost: 11 c ---[31612]---> BDD-cost: 13 c ---[31611]---> BDD-cost: 14 c ---[31610]---> BDD-cost: 15 c ---[31608]---> BDD-cost: 11 c ---[31606]---> BDD-cost: 13 c ---[31605]---> BDD-cost: 14 c ---[31604]---> BDD-cost: 15 c ---[31602]---> BDD-cost: 11 c ---[31600]---> BDD-cost: 13 c ---[31599]---> BDD-cost: 14 c ---[31598]---> BDD-cost: 15 c ---[31596]---> BDD-cost: 11 c ---[31594]---> BDD-cost: 13 c ---[31593]---> BDD-cost: 14 c ---[31592]---> BDD-cost: 15 c ---[31590]---> BDD-cost: 11 c ---[31588]---> BDD-cost: 13 c ---[31587]---> BDD-cost: 14 c ---[31586]---> BDD-cost: 15 c ---[31584]---> BDD-cost: 11 c ---[31582]---> BDD-cost: 13 c ---[31581]---> BDD-cost: 14 c ---[31580]---> BDD-cost: 15 c ---[31578]---> BDD-cost: 11 c ---[31576]---> BDD-cost: 13 c ---[31575]---> BDD-cost: 14 c ---[31574]---> BDD-cost: 15 c ---[31572]---> BDD-cost: 11 c ---[31570]---> BDD-cost: 13 c ---[31569]---> BDD-cost: 14 c ---[31568]---> BDD-cost: 15 c ---[31566]---> BDD-cost: 11 c ---[31564]---> BDD-cost: 13 c ---[31563]---> BDD-cost: 14 c ---[31562]---> BDD-cost: 15 c ---[31560]---> BDD-cost: 11 c ---[31558]---> BDD-cost: 13 c ---[31557]---> BDD-cost: 14 c ---[31556]---> BDD-cost: 15 c ---[31554]---> BDD-cost: 11 c ---[31552]---> BDD-cost: 13 c ---[31551]---> BDD-cost: 14 c ---[31550]---> BDD-cost: 15 c ---[31548]---> BDD-cost: 11 c ---[31546]---> BDD-cost: 13 c ---[31545]---> BDD-cost: 14 c ---[31544]---> BDD-cost: 15 c ---[31542]---> BDD-cost: 11 c ---[31540]---> BDD-cost: 13 c ---[31539]---> BDD-cost: 14 c ---[31538]---> BDD-cost: 15 c ---[31536]---> BDD-cost: 11 c ---[31534]---> BDD-cost: 13 c ---[31533]---> BDD-cost: 14 c ---[31532]---> BDD-cost: 15 c ---[31530]---> BDD-cost: 11 c ---[31528]---> BDD-cost: 13 c ---[31527]---> BDD-cost: 14 c ---[31526]---> BDD-cost: 15 c ---[31524]---> BDD-cost: 11 c ---[31522]---> BDD-cost: 13 c ---[31521]---> BDD-cost: 14 c ---[31520]---> BDD-cost: 15 c ---[31518]---> BDD-cost: 11 c ---[31516]---> BDD-cost: 13 c ---[31515]---> BDD-cost: 14 c ---[31514]---> BDD-cost: 15 c ---[31512]---> BDD-cost: 11 c ---[31510]---> BDD-cost: 13 c ---[31509]---> BDD-cost: 14 c ---[31508]---> BDD-cost: 15 c ---[31506]---> BDD-cost: 11 c ---[31504]---> BDD-cost: 13 c ---[31503]---> BDD-cost: 14 c ---[31502]---> BDD-cost: 15 c ---[31500]---> BDD-cost: 11 c ---[31498]---> BDD-cost: 13 c ---[31497]---> BDD-cost: 14 c ---[31496]---> BDD-cost: 15 c ---[31494]---> BDD-cost: 11 c ---[31492]---> BDD-cost: 13 c ---[31491]---> BDD-cost: 14 c ---[31490]---> BDD-cost: 15 c ---[31488]---> BDD-cost: 11 c ---[31486]---> BDD-cost: 13 c ---[31485]---> BDD-cost: 14 c ---[31484]---> BDD-cost: 15 c ---[31482]---> BDD-cost: 11 c ---[31480]---> BDD-cost: 13 c ---[31479]---> BDD-cost: 14 c ---[31478]---> BDD-cost: 15 c ---[31476]---> BDD-cost: 11 c ---[31474]---> BDD-cost: 13 c ---[31473]---> BDD-cost: 14 c ---[31472]---> BDD-cost: 15 c ---[31470]---> BDD-cost: 11 c ---[31468]---> BDD-cost: 13 c ---[31467]---> BDD-cost: 14 c ---[31466]---> BDD-cost: 15 c ---[31464]---> BDD-cost: 11 c ---[31462]---> BDD-cost: 13 c ---[31461]---> BDD-cost: 14 c ---[31460]---> BDD-cost: 15 c ---[31458]---> BDD-cost: 11 c ---[31456]---> BDD-cost: 13 c ---[31455]---> BDD-cost: 14 c ---[31454]---> BDD-cost: 15 c ---[31452]---> BDD-cost: 11 c ---[31450]---> BDD-cost: 13 c ---[31449]---> BDD-cost: 14 c ---[31448]---> BDD-cost: 15 c ---[31446]---> BDD-cost: 11 c ---[31444]---> BDD-cost: 13 c ---[31443]---> BDD-cost: 14 c ---[31442]---> BDD-cost: 15 c ---[31440]---> BDD-cost: 11 c ---[31438]---> BDD-cost: 13 c ---[31437]---> BDD-cost: 14 c ---[31436]---> BDD-cost: 15 c ---[31434]---> BDD-cost: 11 c ---[31432]---> BDD-cost: 13 c ---[31431]---> BDD-cost: 14 c ---[31430]---> BDD-cost: 15 c ---[31428]---> BDD-cost: 11 c ---[31426]---> BDD-cost: 13 c ---[31425]---> BDD-cost: 14 c ---[31424]---> BDD-cost: 15 c ---[31422]---> BDD-cost: 11 c ---[31420]---> BDD-cost: 13 c ---[31419]---> BDD-cost: 14 c ---[31418]---> BDD-cost: 15 c ---[31416]---> BDD-cost: 11 c ---[31414]---> BDD-cost: 13 c ---[31413]---> BDD-cost: 14 c ---[31412]---> BDD-cost: 15 c ---[31410]---> BDD-cost: 11 c ---[31408]---> BDD-cost: 13 c ---[31407]---> BDD-cost: 14 c ---[31406]---> BDD-cost: 15 c ---[31404]---> BDD-cost: 11 c ---[31402]---> BDD-cost: 13 c ---[31401]---> BDD-cost: 14 c ---[31400]---> BDD-cost: 15 c ---[31398]---> BDD-cost: 11 c ---[31396]---> BDD-cost: 13 c ---[31395]---> BDD-cost: 14 c ---[31394]---> BDD-cost: 15 c ---[31392]---> BDD-cost: 11 c ---[31390]---> BDD-cost: 13 c ---[31389]---> BDD-cost: 14 c ---[31388]---> BDD-cost: 15 c ---[31386]---> BDD-cost: 11 c ---[31384]---> BDD-cost: 13 c ---[31383]---> BDD-cost: 14 c ---[31382]---> BDD-cost: 15 c ---[31380]---> BDD-cost: 11 c ---[31378]---> BDD-cost: 13 c ---[31377]---> BDD-cost: 14 c ---[31376]---> BDD-cost: 15 c ---[31374]---> BDD-cost: 11 c ---[31372]---> BDD-cost: 13 c ---[31371]---> BDD-cost: 14 c ---[31370]---> BDD-cost: 15 c ---[31368]---> BDD-cost: 11 c ---[31366]---> BDD-cost: 13 c ---[31365]---> BDD-cost: 14 c ---[31364]---> BDD-cost: 15 c ---[31362]---> BDD-cost: 11 c ---[31360]---> BDD-cost: 13 c ---[31359]---> BDD-cost: 14 c ---[31358]---> BDD-cost: 15 c ---[31356]---> BDD-cost: 11 c ---[31354]---> BDD-cost: 13 c ---[31353]---> BDD-cost: 14 c ---[31352]---> BDD-cost: 15 c ---[31350]---> BDD-cost: 11 c ---[31348]---> BDD-cost: 13 c ---[31347]---> BDD-cost: 14 c ---[31346]---> BDD-cost: 15 c ---[31344]---> BDD-cost: 11 c ---[31342]---> BDD-cost: 13 c ---[31341]---> BDD-cost: 14 c ---[31340]---> BDD-cost: 15 c ---[31338]---> BDD-cost: 11 c ---[31336]---> BDD-cost: 13 c ---[31335]---> BDD-cost: 14 c ---[31334]---> BDD-cost: 15 c ---[31332]---> BDD-cost: 11 c ---[31330]---> BDD-cost: 13 c ---[31329]---> BDD-cost: 14 c ---[31328]---> BDD-cost: 15 c ---[31326]---> BDD-cost: 11 c ---[31324]---> BDD-cost: 13 c ---[31323]---> BDD-cost: 14 c ---[31322]---> BDD-cost: 15 c ---[31320]---> BDD-cost: 11 c ---[31318]---> BDD-cost: 13 c ---[31317]---> BDD-cost: 14 c ---[31316]---> BDD-cost: 15 c ---[31314]---> BDD-cost: 11 c ---[31312]---> BDD-cost: 13 c ---[31311]---> BDD-cost: 14 c ---[31310]---> BDD-cost: 15 c ---[31308]---> BDD-cost: 11 c ---[31306]---> BDD-cost: 13 c ---[31305]---> BDD-cost: 14 c ---[31304]---> BDD-cost: 15 c ---[31302]---> BDD-cost: 11 c ---[31300]---> BDD-cost: 13 c ---[31299]---> BDD-cost: 14 c ---[31298]---> BDD-cost: 15 c ---[31296]---> BDD-cost: 11 c ---[31294]---> BDD-cost: 13 c ---[31293]---> BDD-cost: 14 c ---[31292]---> BDD-cost: 15 c ---[31290]---> BDD-cost: 11 c ---[31288]---> BDD-cost: 13 c ---[31287]---> BDD-cost: 14 c ---[31286]---> BDD-cost: 15 c ---[31284]---> BDD-cost: 11 c ---[31282]---> BDD-cost: 13 c ---[31281]---> BDD-cost: 14 c ---[31280]---> BDD-cost: 15 c ---[31278]---> BDD-cost: 11 c ---[31276]---> BDD-cost: 13 c ---[31275]---> BDD-cost: 14 c ---[31274]---> BDD-cost: 15 c ---[31272]---> BDD-cost: 11 c ---[31270]---> BDD-cost: 13 c ---[31269]---> BDD-cost: 14 c ---[31268]---> BDD-cost: 15 c ---[31266]---> BDD-cost: 11 c ---[31264]---> BDD-cost: 13 c ---[31263]---> BDD-cost: 14 c ---[31262]---> BDD-cost: 15 c ---[31260]---> BDD-cost: 11 c ---[31258]---> BDD-cost: 13 c ---[31257]---> BDD-cost: 14 c ---[31256]---> BDD-cost: 15 c ---[31254]---> BDD-cost: 11 c ---[31252]---> BDD-cost: 13 c ---[31251]---> BDD-cost: 14 c ---[31250]---> BDD-cost: 15 c ---[31248]---> BDD-cost: 11 c ---[31246]---> BDD-cost: 13 c ---[31245]---> BDD-cost: 14 c ---[31244]---> BDD-cost: 15 c ---[31242]---> BDD-cost: 11 c ---[31240]---> BDD-cost: 13 c ---[31239]---> BDD-cost: 14 c ---[31238]---> BDD-cost: 15 c ---[31236]---> BDD-cost: 11 c ---[31234]---> BDD-cost: 13 c ---[31233]---> BDD-cost: 14 c ---[31232]---> BDD-cost: 15 c ---[31230]---> BDD-cost: 11 c ---[31228]---> BDD-cost: 13 c ---[31227]---> BDD-cost: 14 c ---[31226]---> BDD-cost: 15 c ---[31224]---> BDD-cost: 11 c ---[31222]---> BDD-cost: 13 c ---[31221]---> BDD-cost: 14 c ---[31220]---> BDD-cost: 15 c ---[31218]---> BDD-cost: 11 c ---[31216]---> BDD-cost: 13 c ---[31215]---> BDD-cost: 14 c ---[31214]---> BDD-cost: 15 c ---[31212]---> BDD-cost: 11 c ---[31210]---> BDD-cost: 13 c ---[31209]---> BDD-cost: 14 c ---[31208]---> BDD-cost: 15 c ---[31206]---> BDD-cost: 11 c ---[31204]---> BDD-cost: 13 c ---[31203]---> BDD-cost: 14 c ---[31202]---> BDD-cost: 15 c ---[31200]---> BDD-cost: 11 c ---[31198]---> BDD-cost: 13 c ---[31197]---> BDD-cost: 14 c ---[31196]---> BDD-cost: 15 c ---[31194]---> BDD-cost: 11 c ---[31192]---> BDD-cost: 13 c ---[31191]---> BDD-cost: 14 c ---[31190]---> BDD-cost: 15 c ---[31188]---> BDD-cost: 11 c ---[31186]---> BDD-cost: 13 c ---[31185]---> BDD-cost: 14 c ---[31184]---> BDD-cost: 15 c ---[31182]---> BDD-cost: 11 c ---[31180]---> BDD-cost: 13 c ---[31179]---> BDD-cost: 14 c ---[31178]---> BDD-cost: 15 c ---[31176]---> BDD-cost: 11 c ---[31174]---> BDD-cost: 13 c ---[31173]---> BDD-cost: 14 c ---[31172]---> BDD-cost: 15 c ---[31170]---> BDD-cost: 11 c ---[31168]---> BDD-cost: 13 c ---[31167]---> BDD-cost: 14 c ---[31166]---> BDD-cost: 15 c ---[31164]---> BDD-cost: 11 c ---[31162]---> BDD-cost: 13 c ---[31161]---> BDD-cost: 14 c ---[31160]---> BDD-cost: 15 c ---[31158]---> BDD-cost: 11 c ---[31156]---> BDD-cost: 13 c ---[31155]---> BDD-cost: 14 c ---[31154]---> BDD-cost: 15 c ---[31152]---> BDD-cost: 11 c ---[31150]---> BDD-cost: 13 c ---[31149]---> BDD-cost: 14 c ---[31148]---> BDD-cost: 15 c ---[31146]---> BDD-cost: 11 c ---[31144]---> BDD-cost: 13 c ---[31143]---> BDD-cost: 14 c ---[31142]---> BDD-cost: 15 c ---[31140]---> BDD-cost: 11 c ---[31138]---> BDD-cost: 13 c ---[31137]---> BDD-cost: 14 c ---[31136]---> BDD-cost: 15 c ---[31134]---> BDD-cost: 11 c ---[31132]---> BDD-cost: 13 c ---[31131]---> BDD-cost: 14 c ---[31130]---> BDD-cost: 15 c ---[31128]---> BDD-cost: 11 c ---[31126]---> BDD-cost: 13 c ---[31125]---> BDD-cost: 14 c ---[31124]---> BDD-cost: 15 c ---[31122]---> BDD-cost: 11 c ---[31120]---> BDD-cost: 13 c ---[31119]---> BDD-cost: 14 c ---[31118]---> BDD-cost: 15 c ---[31116]---> BDD-cost: 11 c ---[31114]---> BDD-cost: 13 c ---[31113]---> BDD-cost: 14 c ---[31112]---> BDD-cost: 15 c ---[31110]---> BDD-cost: 11 c ---[31108]---> BDD-cost: 13 c ---[31107]---> BDD-cost: 14 c ---[31106]---> BDD-cost: 15 c ---[31104]---> BDD-cost: 11 c ---[31102]---> BDD-cost: 13 c ---[31101]---> BDD-cost: 14 c ---[31100]---> BDD-cost: 15 c ---[31098]---> BDD-cost: 11 c ---[31096]---> BDD-cost: 13 c ---[31095]---> BDD-cost: 14 c ---[31094]---> BDD-cost: 15 c ---[31092]---> BDD-cost: 11 c ---[31090]---> BDD-cost: 13 c ---[31089]---> BDD-cost: 14 c ---[31088]---> BDD-cost: 15 c ---[31086]---> BDD-cost: 11 c ---[31084]---> BDD-cost: 13 c ---[31083]---> BDD-cost: 14 c ---[31082]---> BDD-cost: 15 c ---[31080]---> BDD-cost: 11 c ---[31078]---> BDD-cost: 13 c ---[31077]---> BDD-cost: 14 c ---[31076]---> BDD-cost: 15 c ---[31074]---> BDD-cost: 11 c ---[31072]---> BDD-cost: 13 c ---[31071]---> BDD-cost: 14 c ---[31070]---> BDD-cost: 15 c ---[31068]---> BDD-cost: 11 c ---[31066]---> BDD-cost: 13 c ---[31065]---> BDD-cost: 14 c ---[31064]---> BDD-cost: 15 c ---[31062]---> BDD-cost: 11 c ---[31060]---> BDD-cost: 13 c ---[31059]---> BDD-cost: 14 c ---[31058]---> BDD-cost: 15 c ---[31056]---> BDD-cost: 11 c ---[31054]---> BDD-cost: 13 c ---[31053]---> BDD-cost: 14 c ---[31052]---> BDD-cost: 15 c ---[31050]---> BDD-cost: 11 c ---[31048]---> BDD-cost: 13 c ---[31047]---> BDD-cost: 14 c ---[31046]---> BDD-cost: 15 c ---[31044]---> BDD-cost: 11 c ---[31042]---> BDD-cost: 13 c ---[31041]---> BDD-cost: 14 c ---[31040]---> BDD-cost: 15 c ---[31038]---> BDD-cost: 11 c ---[31036]---> BDD-cost: 13 c ---[31035]---> BDD-cost: 14 c ---[31034]---> BDD-cost: 15 c ---[31032]---> BDD-cost: 11 c ---[31030]---> BDD-cost: 13 c ---[31029]---> BDD-cost: 14 c ---[31028]---> BDD-cost: 15 c ---[31026]---> BDD-cost: 11 c ---[31024]---> BDD-cost: 13 c ---[31023]---> BDD-cost: 14 c ---[31022]---> BDD-cost: 15 c ---[31020]---> BDD-cost: 11 c ---[31018]---> BDD-cost: 13 c ---[31017]---> BDD-cost: 14 c ---[31016]---> BDD-cost: 15 c ---[31014]---> BDD-cost: 11 c ---[31012]---> BDD-cost: 13 c ---[31011]---> BDD-cost: 14 c ---[31010]---> BDD-cost: 15 c ---[31008]---> BDD-cost: 11 c ---[31006]---> BDD-cost: 13 c ---[31005]---> BDD-cost: 14 c ---[31004]---> BDD-cost: 15 c ---[31002]---> BDD-cost: 11 c ---[31000]---> BDD-cost: 13 c ---[30999]---> BDD-cost: 14 c ---[30998]---> BDD-cost: 15 c ---[30996]---> BDD-cost: 11 c ---[30994]---> BDD-cost: 13 c ---[30993]---> BDD-cost: 14 c ---[30992]---> BDD-cost: 15 c ---[30990]---> BDD-cost: 11 c ---[30988]---> BDD-cost: 13 c ---[30987]---> BDD-cost: 14 c ---[30986]---> BDD-cost: 15 c ---[30984]---> BDD-cost: 11 c ---[30982]---> BDD-cost: 13 c ---[30981]---> BDD-cost: 14 c ---[30980]---> BDD-cost: 15 c ---[30978]---> BDD-cost: 11 c ---[30976]---> BDD-cost: 13 c ---[30975]---> BDD-cost: 14 c ---[30974]---> BDD-cost: 15 c ---[30972]---> BDD-cost: 11 c ---[30970]---> BDD-cost: 13 c ---[30969]---> BDD-cost: 14 c ---[30968]---> BDD-cost: 15 c ---[30966]---> BDD-cost: 11 c ---[30964]---> BDD-cost: 13 c ---[30963]---> BDD-cost: 14 c ---[30962]---> BDD-cost: 15 c ---[30960]---> BDD-cost: 11 c ---[30958]---> BDD-cost: 13 c ---[30957]---> BDD-cost: 14 c ---[30956]---> BDD-cost: 15 c ---[30954]---> BDD-cost: 11 c ---[30952]---> BDD-cost: 13 c ---[30951]---> BDD-cost: 14 c ---[30950]---> BDD-cost: 15 c ---[30948]---> BDD-cost: 11 c ---[30946]---> BDD-cost: 13 c ---[30945]---> BDD-cost: 14 c ---[30944]---> BDD-cost: 15 c ---[30942]---> BDD-cost: 11 c ---[30940]---> BDD-cost: 13 c ---[30939]---> BDD-cost: 14 c ---[30938]---> BDD-cost: 15 c ---[30936]---> BDD-cost: 11 c ---[30934]---> BDD-cost: 13 c ---[30933]---> BDD-cost: 14 c ---[30932]---> BDD-cost: 15 c ---[30930]---> BDD-cost: 11 c ---[30928]---> BDD-cost: 13 c ---[30927]---> BDD-cost: 14 c ---[30926]---> BDD-cost: 15 c ---[30924]---> BDD-cost: 11 c ---[30922]---> BDD-cost: 13 c ---[30921]---> BDD-cost: 14 c ---[30920]---> BDD-cost: 15 c ---[30918]---> BDD-cost: 11 c ---[30916]---> BDD-cost: 13 c ---[30915]---> BDD-cost: 14 c ---[30914]---> BDD-cost: 15 c ---[30912]---> BDD-cost: 11 c ---[30910]---> BDD-cost: 13 c ---[30909]---> BDD-cost: 14 c ---[30908]---> BDD-cost: 15 c ---[30906]---> BDD-cost: 11 c ---[30904]---> BDD-cost: 13 c ---[30903]---> BDD-cost: 14 c ---[30902]---> BDD-cost: 15 c ---[30900]---> BDD-cost: 11 c ---[30898]---> BDD-cost: 13 c ---[30897]---> BDD-cost: 14 c ---[30896]---> BDD-cost: 15 c ---[30894]---> BDD-cost: 11 c ---[30892]---> BDD-cost: 13 c ---[30891]---> BDD-cost: 14 c ---[30890]---> BDD-cost: 15 c ---[30888]---> BDD-cost: 11 c ---[30886]---> BDD-cost: 13 c ---[30885]---> BDD-cost: 14 c ---[30884]---> BDD-cost: 15 c ---[30882]---> BDD-cost: 11 c ---[30880]---> BDD-cost: 13 c ---[30879]---> BDD-cost: 14 c ---[30878]---> BDD-cost: 15 c ---[30876]---> BDD-cost: 11 c ---[30874]---> BDD-cost: 13 c ---[30873]---> BDD-cost: 14 c ---[30872]---> BDD-cost: 15 c ---[30870]---> BDD-cost: 11 c ---[30868]---> BDD-cost: 13 c ---[30867]---> BDD-cost: 14 c ---[30866]---> BDD-cost: 15 c ---[30864]---> BDD-cost: 11 c ---[30862]---> BDD-cost: 13 c ---[30861]---> BDD-cost: 14 c ---[30860]---> BDD-cost: 15 c ---[30858]---> BDD-cost: 11 c ---[30856]---> BDD-cost: 13 c ---[30855]---> BDD-cost: 14 c ---[30854]---> BDD-cost: 15 c ---[30852]---> BDD-cost: 11 c ---[30850]---> BDD-cost: 13 c ---[30849]---> BDD-cost: 14 c ---[30848]---> BDD-cost: 15 c ---[30846]---> BDD-cost: 11 c ---[30844]---> BDD-cost: 13 c ---[30843]---> BDD-cost: 14 c ---[30842]---> BDD-cost: 15 c ---[30840]---> BDD-cost: 11 c ---[30838]---> BDD-cost: 13 c ---[30837]---> BDD-cost: 14 c ---[30836]---> BDD-cost: 15 c ---[30834]---> BDD-cost: 11 c ---[30832]---> BDD-cost: 13 c ---[30831]---> BDD-cost: 14 c ---[30830]---> BDD-cost: 15 c ---[30828]---> BDD-cost: 11 c ---[30826]---> BDD-cost: 13 c ---[30825]---> BDD-cost: 14 c ---[30824]---> BDD-cost: 15 c ---[30822]---> BDD-cost: 11 c ---[30820]---> BDD-cost: 13 c ---[30819]---> BDD-cost: 14 c ---[30818]---> BDD-cost: 15 c ---[30816]---> BDD-cost: 11 c ---[30814]---> BDD-cost: 13 c ---[30813]---> BDD-cost: 14 c ---[30812]---> BDD-cost: 15 c ---[30810]---> BDD-cost: 11 c ---[30808]---> BDD-cost: 13 c ---[30807]---> BDD-cost: 14 c ---[30806]---> BDD-cost: 15 c ---[30804]---> BDD-cost: 11 c ---[30802]---> BDD-cost: 13 c ---[30801]---> BDD-cost: 14 c ---[30800]---> BDD-cost: 15 c ---[30798]---> BDD-cost: 11 c ---[30796]---> BDD-cost: 13 c ---[30795]---> BDD-cost: 14 c ---[30794]---> BDD-cost: 15 c ---[30792]---> BDD-cost: 11 c ---[30790]---> BDD-cost: 13 c ---[30789]---> BDD-cost: 14 c ---[30788]---> BDD-cost: 15 c ---[30786]---> BDD-cost: 11 c ---[30784]---> BDD-cost: 13 c ---[30783]---> BDD-cost: 14 c ---[30782]---> BDD-cost: 15 c ---[30780]---> BDD-cost: 11 c ---[30778]---> BDD-cost: 13 c ---[30777]---> BDD-cost: 14 c ---[30776]---> BDD-cost: 15 c ---[30774]---> BDD-cost: 11 c ---[30772]---> BDD-cost: 13 c ---[30771]---> BDD-cost: 14 c ---[30770]---> BDD-cost: 15 c ---[30768]---> BDD-cost: 11 c ---[30766]---> BDD-cost: 13 c ---[30765]---> BDD-cost: 14 c ---[30764]---> BDD-cost: 15 c ---[30762]---> BDD-cost: 11 c ---[30760]---> BDD-cost: 1/oldhome/oroussel/solvers/minisat+_script: line 9: 23626 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): 0.90 0.94 0.90 2/54 23622 Raw data (stat): 23622 (runsolver) R 23621 24300 24299 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 795970243 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.001 s] Raw data (loadavg): 0.91 0.94 0.91 2/55 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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.0011 s] Raw data (loadavg): 0.92 0.95 0.91 2/55 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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.0009 s] Raw data (loadavg): 0.94 0.95 0.91 2/55 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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.0016 s] Raw data (loadavg): 0.94 0.95 0.91 2/55 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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.0022 s] Raw data (loadavg): 0.95 0.95 0.91 2/55 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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.0015 s] Raw data (loadavg): 0.96 0.95 0.91 2/55 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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.0015 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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.0018 s] Raw data (loadavg): 0.97 0.95 0.91 2/55 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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+85.8171 s] Raw data (loadavg): 0.97 0.95 0.91 1/53 23626 Raw data (stat): 23622 (minisat+_script) S 23621 24300 24299 0 -1 0 275 239 0 0 0 0 0 0 19 0 1 0 795970243 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): 85.8165 CPU time (s): 85.819 CPU user time (s): 78.1281 CPU system time (s): 7.69083 CPU usage (%): 100.003 Max. virtual memory (Kb): 2124 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####