Name | normalized-opb/mps-v2-20-10/www.csit.fsu.edu/~burkardt/datasets/mps/normalized-mps-v2-20-10-adlittle.opb |
MD5SUM | 2833b37c31c7399c7b1bcb72ed443385 |
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 | 2460 |
Biggest coefficient in the objective function | 88852135936000 |
Number of bits for the biggest coefficient in the objective function | 47 |
Sum of the numbers in the objective function | 3689448844530141 |
Number of bits of the sum of numbers in the objective function | 52 |
Biggest number in a constraint | 359703511040000 |
Number of bits of the biggest number in a constraint | 49 |
Biggest sum of numbers in a constraint | 6054438712178314 |
Number of bits of the biggest sum of numbers | 53 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.028995 |
Number of variables | 2910 |
Total number of constraints | 56 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 0 |
Number of constraints which are nor clauses,nor cardinality constraints | 56 |
Minimum length of a constraint | 30 |
Maximum length of a constraint | 810 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc31 THE 2005-05-24 02:56:17 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=15342 boxname=wulflinc31 idbench=1181 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: 2833b37c31c7399c7b1bcb72ed443385 /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-adlittle.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-adlittle.opb IDLAUNCH: 15342 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 3 cpu MHz : 451.153 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.153 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 : 901.12 /proc/meminfo: MemTotal: 1034660 kB MemFree: 583808 kB Buffers: 28164 kB Cached: 401672 kB SwapCached: 1352 kB Active: 298444 kB Inactive: 133920 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 583556 kB SwapTotal: 2097892 kB SwapFree: 2095532 kB Dirty: 4 kB Writeback: 0 kB Mapped: 5104 kB Slab: 12792 kB Committed_AS: 63840 kB PageTables: 328 kB VmallocTotal: 114680 kB VmallocUsed: 1368 kB VmallocChunk: 113252 kB JOB ENDED THE 2005-05-24 02:56:19 (client local time) WITH STATUS 0 IN 1.51377 SECONDS stats: 15342 7 1.51377 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c ERROR Parsing file!!! c ERROR parsing line: -506*V_0x2e__0x2e__0x2e_100_bit_10 -1012*V_0x2e__0x2e__0x2e_100_bit_9 -2024*V_0x2e__0x2e__0x2e_100_bit_8 -4048*V_0x2e__0x2e__0x2e_100_bit_7 -8096*V_0x2e__0x2e__0x2e_100_bit_6 -16192*V_0x2e__0x2e__0x2e_100_bit_5 -32384*V_0x2e__0x2e__0x2e_100_bit_4 -64768*V_0x2e__0x2e__0x2e_100_bit_3 -129536*V_0x2e__0x2e__0x2e_100_bit_2 -259072*V_0x2e__0x2e__0x2e_100_bit_1 -518144*V_0x2e__0x2e__0x2e_100_bit0 -1036288*V_0x2e__0x2e__0x2e_100_bit1 -2072576*V_0x2e__0x2e__0x2e_100_bit2 -4145152*V_0x2e__0x2e__0x2e_100_bit3 -8290304*V_0x2e__0x2e__0x2e_100_bit4 -16580608*V_0x2e__0x2e__0x2e_100_bit5 -33161216*V_0x2e__0x2e__0x2e_100_bit6 -66322432*V_0x2e__0x2e__0x2e_100_bit7 -132644864*V_0x2e__0x2e__0x2e_100_bit8 -265289728*V_0x2e__0x2e__0x2e_100_bit9 -530579456*V_0x2e__0x2e__0x2e_100_bit10 -1061158912*V_0x2e__0x2e__0x2e_100_bit11 -2122317824*V_0x2e__0x2e__0x2e_100_bit12 -4244635648*V_0x2e__0x2e__0x2e_100_bit13 -8489271296*V_0x2e__0x2e__0x2e_100_bit14 -16978542592*V_0x2e__0x2e__0x2e_100_bit15 -33957085184*V_0x2e__0x2e__0x2e_100_bit16 -67914170368*V_0x2e__0x2e__0x2e_100_bit17 -135828340736*V_0x2e__0x2e__0x2e_100_bit18 -271656681472*V_0x2e__0x2e__0x2e_100_bit19 -638*V_0x2e__0x2e__0x2e_101_bit_10 -1276*V_0x2e__0x2e__0x2e_101_bit_9 -2552*V_0x2e__0x2e__0x2e_101_bit_8 -5104*V_0x2e__0x2e__0x2e_101_bit_7 -10208*V_0x2e__0x2e__0x2e_101_bit_6 -20416*V_0x2e__0x2e__0x2e_101_bit_5 -40832*V_0x2e__0x2e__0x2e_101_bit_4 -81664*V_0x2e__0x2e__0x2e_101_bit_3 -163328*V_0x2e__0x2e__0x2e_101_bit_2 -326656*V_0x2e__0x2e__0x2e_101_bit_1 -653312*V_0x2e__0x2e__0x2e_101_bit0 -1306624*V_0x2e__0x2e__0x2e_101_bit1 -2613248*V_0x2e__0x2e__0x2e_101_bit2 -5226496*V_0x2e__0x2e__0x2e_101_bit3 -10452992*V_0x2e__0x2e__0x2e_101_bit4 -20905984*V_0x2e__0x2e__0x2e_101_bit5 -41811968*V_0x2e__0x2e__0x2e_101_bit6 -83623936*V_0x2e__0x2e__0x2e_101_bit7 -167247872*V_0x2e__0x2e__0x2e_101_bit8 -334495744*V_0x2e__0x2e__0x2e_101_bit9 -668991488*V_0x2e__0x2e__0x2e_101_bit10 -1337982976*V_0x2e__0x2e__0x2e_101_bit11 -2675965952*V_0x2e__0x2e__0x2e_101_bit12 -5351931904*V_0x2e__0x2e__0x2e_101_bit13 -10703863808*V_0x2e__0x2e__0x2e_101_bit14 -21407727616*V_0x2e__0x2e__0x2e_101_bit15 -42815455232*V_0x2e__0x2e__0x2e_101_bit16 -85630910464*V_0x2e__0x2e__0x2e_101_bit17 -171261820928*V_0x2e__0x2e__0x2e_101_bit18 -342523641856*V_0x2e__0x2e__0x2e_101_bit19 +1000*V_0x2e__0x2e__0x2e_102_bit_10 +2000*V_0x2e__0x2e__0x2e_102_bit_9 +4000*V_0x2e__0x2e__0x2e_102_bit_8 +8000*V_0x2e__0x2e__0x2e_102_bit_7 +16000*V_0x2e__0x2e__0x2e_102_bit_6 +32000*V_0x2e__0x2e__0x2e_102_bit_5 +64000*V_0x2e__0x2e__0x2e_102_bit_4 +128000*V_0x2e__0x2e__0x2e_102_bit_3 +256000*V_0x2e__0x2e__0x2e_102_bit_2 +512000*V_0x2e__0x2e__0x2e_102_bit_1 +1024000*V_0x2e__0x2e__0x2e_102_bit0 +2048000*V_0x2e__0x2e__0x2e_102_bit1 +4096000*V_0x2e__0x2e__0x2e_102_bit2 +8192000*V_0x2e__0x2e__0x2e_102_bit3 +16384000*V_0x2e__0x2e__0x2e_102_bit4 +32768000*V_0x2e__0x2e__0x2e_102_bit5 +65536000*V_0x2e__0x2e__0x2e_102_bit6 +131072000*V_0x2e__0x2e__0x2e_102_bit7 +262144000*V_0x2e__0x2e__0x2e_102_bit8 +524288000*V_0x2e__0x2e__0x2e_102_bit9 +1048576000*V_0x2e__0x2e__0x2e_102_bit10 +2097152000*V_0x2e__0x2e__0x2e_102_bit11 +4194304000*V_0x2e__0x2e__0x2e_102_bit12 +8388608000*V_0x2e__0x2e__0x2e_102_bit13 +16777216000*V_0x2e__0x2e__0x2e_102_bit14 +33554432000*V_0x2e__0x2e__0x2e_102_bit15 +67108864000*V_0x2e__0x2e__0x2e_102_bit16 +134217728000*V_0x2e__0x2e__0x2e_102_bit17 +268435456000*V_0x2e__0x2e__0x2e_102_bit18 +536870912000*V_0x2e__0x2e__0x2e_102_bit19 +247*V_0x2e__0x2e__0x2e_148_bit_10 +494*V_0x2e__0x2e__0x2e_148_bit_9 +988*V_0x2e__0x2e__0x2e_148_bit_8 +1976*V_0x2e__0x2e__0x2e_148_bit_7 +3952*V_0x2e__0x2e__0x2e_148_bit_6 +7904*V_0x2e__0x2e__0x2e_148_bit_5 +15808*V_0x2e__0x2e__0x2e_148_bit_4 +31616*V_0x2e__0x2e__0x2e_148_bit_3 +63232*V_0x2e__0x2e__0x2e_148_bit_2 +126464*V_0x2e__0x2e__0x2e_148_bit_1 +252928*V_0x2e__0x2e__0x2e_148_bit0 +505856*V_0x2e__0x2e__0x2e_148_bit1 +1011712*V_0x2e__0x2e__0x2e_148_bit2 +2023424*V_0x2e__0x2e__0x2e_148_bit3 +4046848*V_0x2e__0x2e__0x2e_148_bit4 +8093696*V_0x2e__0x2e__0x2e_148_bit5 +16187392*V_0x2e__0x2e__0x2e_148_bit6 +32374784*V_0x2e__0x2e__0x2e_148_bit7 +64749568*V_0x2e__0x2e__0x2e_148_bit8 +129499136*V_0x2e__0x2e__0x2e_148_bit9 +258998272*V_0x2e__0x2e__0x2e_148_bit10 +517996544*V_0x2e__0x2e__0x2e_148_bit11 +1035993088*V_0x2e__0x2e__0x2e_148_bit12 +2071986176*V_0x2e__0x2e__0x2e_148_bit13 +4143972352*V_0x2e__0x2e__0x2e_148_bit14 +8287944704*V_0x2e__0x2e__0x2e_148_bit15 +16575889408*V_0x2e__0x2e__0x2e_148_bit16 +33151778816*V_0x2e__0x2e__0x2e_148_bit17 +66303557632*V_0x2e__0x2e__0x2e_148_bit18 +132607115264*V_0x2e__0x2e__0x2e_148_bit19 +157*V_0x2e__0x2e__0x2e_149_bit_10 +314*V_0x2e__0x2e__0x2e_149_bit_9 +628*V_0x2e__0x2e__0x2e_149_bit_8 +1256*V_0x2e__0x2e__0x2e_149_bit_7 +2512*V_0x2e__0x2e__0x2e_149_bit_6 +5024*V_0x2e__0x2e__0x2e_149_bit_5 +10048*V_0x2e__0x2e__0x2e_149_bit_4 +20096*V_0x2e__0x2e__0x2e_149_bit_3 +40192*V_0x2e__0x2e__0x2e_149_bit_2 +80384*V_0x2e__0x2e__0x2e_149_bit_1 +160768*V_0x2e__0x2e__0x2e_149_bit0 +321536*V_0x2e__0x2e__0x2e_149_bit1 +643072*V_0x2e__0x2e__0x2e_149_bit2 +1286144*V_0x2e__0x2e__0x2e_149_bit3 +2572288*V_0x2e__0x2e__0x2e_149_bit4 +5144576*V_0x2e__0x2e__0x2e_149_bit5 +10289152*V_0x2e__0x2e__0x2e_149_bit6 +20578304*V_0x2e__0x2e__0x2e_149_bit7 +41156608*V_0x2e__0x2e__0x2e_149_bit8 +82313216*V_0x2e__0x2e__0x2e_149_bit9 +164626432*V_0x2e__0x2e__0x2e_149_bit10 +329252864*V_0x2e__0x2e__0x2e_149_bit11 +658505728*V_0x2e__0x2e__0x2e_149_bit12 +1317011456*V_0x2e__0x2e__0x2e_149_bit13 +2634022912*V_0x2e__0x2e__0x2e_149_bit14 +5268045824*V_0x2e__0x2e__0x2e_149_bit15 +10536091648*V_0x2e__0x2e__0x2e_149_bit16 +21072183296*V_0x2e__0x2e__0x2e_149_bit17 +42144366592*V_0x2e__0x2e__0x2e_149_bit18 +84288733184*V_0x2e__0x2e__0x2e_149_bit19 +157*V_0x2e__0x2e__0x2e_150_bit_10 +314*V_0x2e__0x2e__0x2e_150_bit_9 +628*V_0x2e__0x2e__0x2e_150_bit_8 +1256*V_0x2e__0x2e__0x2e_150_bit_7 +2512*V_0x2e__0x2e__0x2e_150_bit_6 +5024*V_0x2e__0x2e__0x2e_150_bit_5 +10048*V_0x2e__0x2e__0x2e_150_bit_4 +20096*V_0x2e__0x2e__0x2e_150_bit_3 +40192*V_0x2e__0x2e__0x2e_150_bit_2 +80384*V_0x2e__0x2e__0x2e_150_bit_1 +160768*V_0x2e__0x2e__0x2e_150_bit0 +321536*V_0x2e__0x2e__0x2e_150_bit1 +643072*V_0x2e__0x2e__0x2e_150_bit2 +1286144*V_0x2e__0x2e__0x2e_150_bit3 +2572288*V_0x2e__0x2e__0x2e_150_bit4 +5144576*V_0x2e__0x2e__0x2e_150_bit5 +10289152*V_0x2e__0x2e__0x2e_150_bit6 +20578304*V_0x2e__0x2e__0x2e_150_bit7 +41156608*V_0x2e__0x2e__0x2e_150_bit8 +82313216*V_0x2e__0x2e__0x2e_150_bit9 +164626432*V_0x2e__0x2e__0x2e_150_bit10 +329252864*V_0x2e__0x2e__0x2e_150_bit11 +658505728*V_0x2e__0x2e__0x2e_150_bit12 +1317011456*V_0x2e__0x2e__0x2e_150_bit13 +2634022912*V_0x2e__0x2e__0x2e_150_bit14 +5268045824*V_0x2e__0x2e__0x2e_150_bit15 +10536091648*V_0x2e__0x2e__0x2e_150_bit16 +21072183296*V_0x2e__0x2e__0x2e_150_bit17 +42144366592*V_0x2e__0x2e__0x2e_150_bit18 +84288733184*V_0x2e__0x2e__0x2e_150_bit19 -200*V_0x2e__0x2e__0x2e_155_bit_10 -400*V_0x2e__0x2e__0x2e_155_bit_9 -800*V_0x2e__0x2e__0x2e_155_bit_8 -1600*V_0x2e__0x2e__0x2e_155_bit_7 -3200*V_0x2e__0x2e__0x2e_155_bit_6 -6400*V_0x2e__0x2e__0x2e_155_bit_5 -12800*V_0x2e__0x2e__0x2e_155_bit_4 -25600*V_0x2e__0x2e__0x2e_155_bit_3 -51200*V_0x2e__0x2e__0x2e_155_bit_2 -102400*V_0x2e__0x2e__0x2e_155_bit_1 -204800*V_0x2e__0x2e__0x2e_155_bit0 -409600*V_0x2e__0x2e__0x2e_155_bit1 -819200*V_0x2e__0x2e__0x2e_155_bit2 -1638400*V_0x2e__0x2e__0x2e_155_bit3 -3276800*V_0x2e__0x2e__0x2e_155_bit4 -6553600*V_0x2e__0x2e__0x2e_155_bit5 -13107200*V_0x2e__0x2e__0x2e_155_bit6 -26214400*V_0x2e__0x2e__0x2e_155_bit7 -52428800*V_0x2e__0x2e__0x2e_155_bit8 -104857600*V_0x2e__0x2e__0x2e_155_bit9 -209715200*V_0x2e__0x2e__0x2e_155_bit10 -419430400*V_0x2e__0x2e__0x2e_155_bit11 -838860800*V_0x2e__0x2e__0x2e_155_bit12 -1677721600*V_0x2e__0x2e__0x2e_155_bit13 -3355443200*V_0x2e__0x2e__0x2e_155_bit14 -6710886400*V_0x2e__0x2e__0x2e_155_bit15 -13421772800*V_0x2e__0x2e__0x2e_155_bit16 -26843545600*V_0x2e__0x2e__0x2e_155_bit17 -53687091200*V_0x2e__0x2e__0x2e_155_bit18 -107374182400*V_0x2e__0x2e__0x2e_155_bit19 +18*V_0x2e__0x2e__0x2e_160_bit_10 +36*V_0x2e__0x2e__0x2e_160_bit_9 +72*V_0x2e__0x2e__0x2e_160_bit_8 +144*V_0x2e__0x2e__0x2e_160_bit_7 +288*V_0x2e__0x2e__0x2e_160_bit_6 +576*V_0x2e__0x2e__0x2e_160_bit_5 +1152*V_0x2e__0x2e__0x2e_160_bit_4 +2304*V_0x2e__0x2e__0x2e_160_bit_3 +4608*V_0x2e__0x2e__0x2e_160_bit_2 +9216*V_0x2e__0x2e__0x2e_160_bit_1 +18432*V_0x2e__0x2e__0x2e_160_bit0 +36864*V_0x2e__0x2e__0x2e_160_bit1 +73728*V_0x2e__0x2e__0x2e_160_bit2 +147456*V_0x2e__0x2e__0x2e_160_bit3 +294912*V_0x2e__0x2e__0x2e_160_bit4 +589824*V_0x2e__0x2e__0x2e_160_bit5 +1179648*V_0x2e__0x2e__0x2e_160_bit6 +2359296*V_0x2e__0x2e__0x2e_160_bit7 +4718592*V_0x2e__0x2e__0x2e_160_bit8 +9437184*V_0x2e__0x2e__0x2e_160_bit9 +18874368*V_0x2e__0x2e__0x2e_160_bit10 +37748736*V_0x2e__0x2e__0x2e_160_bit11 +75497472*V_0x2e__0x2e__0x2e_160_bit12 +150994944*V_0x2e__0x2e__0x2e_160_bit13 +301989888*V_0x2e__0x2e__0x2e_160_bit14 +603979776*V_0x2e__0x2e__0x2e_160_bit15 +1207959552*V_0x2e__0x2e__0x2e_160_bit16 +2415919104*V_0x2e__0x2e__0x2e_160_bit17 +4831838208*V_0x2e__0x2e__0x2e_160_bit18 +9663676416*V_0x2e__0x2e__0x2e_160_bit19 +18*V_0x2e__0x2e__0x2e_161_bit_10 +36*V_0x2e__0x2e__0x2e_161_bit_9 +72*V_0x2e__0x2e__0x2e_161_bit_8 +144*V_0x2e__0x2e__0x2e_161_bit_7 +288*V_0x2e__0x2e__0x2e_161_bit_6 +576*V_0x2e__0x2e__0x2e_161_bit_5 +1152*V_0x2e__0x2e__0x2e_161_bit_4 +2304*V_0x2e__0x2e__0x2e_161_bit_3 +4608*V_0x2e__0x2e__0x2e_161_bit_2 +9216*V_0x2e__0x2e__0x2e_161_bit_1 +18432*V_0x2e__0x2e__0x2e_161_bit0 +36864*V_0x2e__0x2e__0x2e_161_bit1 +73728*V_0x2e__0x2e__0x2e_161_bit2 +147456*V_0x2e__0x2e__0x2e_161_bit3 +294912*V_0x2e__0x2e__0x2e_161_bit4 +589824*V_0x2e__0x2e__0x2e_161_bit5 +1179648*V_0x2e__0x2e__0x2e_161_bit6 +2359296*V_0x2e__0x2e__0x2e_161_bit7 +4718592*V_0x2e__0x2e__0x2e_161_bit8 +9437184*V_0x2e__0x2e__0x2e_161_bit9 +18874368*V_0x2e__0x2e__0x2e_161_bit10 +37748736*V_0x2e__0x2e__0x2e_161_bit11 +75497472*V_0x2e__0x2e__0x2e_161_bit12 +150994944*V_0x2e__0x2e__0x2e_161_bit13 +301989888*V_0x2e__0x2e__0x2e_161_bit14 +603979776*V_0x2e__0x2e__0x2e_161_bit15 +1207959552*V_0x2e__0x2e__0x2e_161_bit16 +2415919104*V_0x2e__0x2e__0x2e_161_bit17 +4831838208*V_0x2e__0x2e__0x2e_161_bit18 +9663676416*V_0x2e__0x2e__0x2e_161_bit19 +10*V_0x2e__0x2e__0x2e_176_bit_10 +20*V_0x2e__0x2e__0x2e_176_bit_9 +40*V_0x2e__0x2e__0x2e_176_bit_8 +80*V_0x2e__0x2e__0x2e_176_bit_7 +160*V_0x2e__0x2e__0x2e_176_bit_6 +320*V_0x2e__0x2e__0x2e_176_bit_5 +640*V_0x2e__0x2e__0x2e_176_bit_4 +1280*V_0x2e__0x2e__0x2e_176_bit_3 +2560*V_0x2e__0x2e__0x2e_176_bit_2 +5120*V_0x2e__0x2e__0x2e_176_bit_1 +10240*V_0x2e__0x2e__0x2e_176_bit0 +20480*V_0x2e__0x2e__0x2e_176_bit1 +40960*V_0x2e__0x2e__0x2e_176_bit2 +81920*V_0x2e__0x2e__0x2e_176_bit3 +163840*V_0x2e__0x2e__0x2e_176_bit4 +327680*V_0x2e__0x2e__0x2e_176_bit5 +655360*V_0x2e__0x2e__0x2e_176_bit6 +1310720*V_0x2e__0x2e__0x2e_176_bit7 +2621440*V_0x2e__0x2e__0x2e_176_bit8 +5242880*V_0x2e__0x2e__0x2e_176_bit9 +10485760*V_0x2e__0x2e__0x2e_176_bit10 +20971520*V_0x2e__0x2e__0x2e_176_bit11 +41943040*V_0x2e__0x2e__0x2e_176_bit12 +83886080*V_0x2e__0x2e__0x2e_176_bit13 +167772160*V_0x2e__0x2e__0x2e_176_bit14 +335544320*V_0x2e__0x2e__0x2e_176_bit15 +671088640*V_0x2e__0x2e__0x2e_176_bit16 +1342177280*V_0x2e__0x2e__0x2e_176_bit17 +2684354560*V_0x2e__0x2e__0x2e_176_bit18 +5368709120*V_0x2e__0x2e__0x2e_176_bit19 +10*V_0x2e__0x2e__0x2e_177_bit_10 +20*V_0x2e__0x2e__0x2e_177_bit_9 +40*V_0x2e__0x2e__0x2e_177_bit_8 +80*V_0x2e__0x2e__0x2e_177_bit_7 +160*V_0x2e__0x2e__0x2e_177_bit_6 +320*V_0x2e__0x2e__0x2e_177_bit_5 +640*V_0x2e__0x2e__0x2e_177_bit_4 +1280*V_0x2e__0x2e__0x2e_177_bit_3 +2560*V_0x2e__0x2e__0x2e_177_bit_2 +5120*V_0x2e__0x2e__0x2e_177_bit_1 +10240*V_0x2e__0x2e__0x2e_177_bit0 +20480*V_0x2e__0x2e__0x2e_177_bit1 +40960*V_0x2e__0x2e__0x2e_177_bit2 +81920*V_0x2e__0x2e__0x2e_177_bit3 +163840*V_0x2e__0x2e__0x2e_177_bit4 +327680*V_0x2e__0x2e__0x2e_177_bit5 +655360*V_0x2e__0x2e__0x2e_177_bit6 +1310720*V_0x2e__0x2e__0x2e_177_bit7 +2621440*V_0x2e__0x2e__0x2e_177_bit8 +5242880*V_0x2e__0x2e__0x2e_177_bit9 +10485760*V_0x2e__0x2e__0x2e_177_bit10 +20971520*V_0x2e__0x2e__0x2e_177_bit11 +41943040*V_0x2e__0x2e__0x2e_177_bit12 +83886080*V_0x2e__0x2e__0x2e_177_bit13 +167772160*V_0x2e__0x2e__0x2e_177_bit14 +335544320*V_0x2e__0x2e__0x2e_177_bit15 +671088640*V_0x2e__0x2e__0x2e_177_bit16 +1342177280*V_0x2e__0x2e__0x2e_177_bit17 +2684354560*V_0x2e__0x2e__0x2e_177_bit18 +5368709120*V_0x2e__0x2e__0x2e_177_bit19 >= +0; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc31/normalized-mps-v2-20-10-adlittle.opb s UNKNOWN c Exit Code: 0 c Total time: 1.49 s #### 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.70 0.88 0.88 2/55 24550 Raw data (stat): 24550 (runsolver) R 24549 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 826786481 1056768 100 4294967295 134512640 135381576 3221221664 3221216880 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 1032 [startup+1.56393 s] Raw data (loadavg): 0.70 0.88 0.88 1/54 24550 Raw data (stat): 24550 (runsolver) R 24549 7876 7672 0 -1 64 5 0 0 0 0 0 0 0 19 0 1 0 826786481 1056768 100 4294967295 134512640 135381576 3221221664 3221216880 135158418 0 2147483391 1 90112 0 0 0 17 0 0 0 Raw data (statm): 258 100 215 215 0 43 0 vsize: 0 Child status: 0 Real time (s): 1.56364 CPU time (s): 1.51377 CPU user time (s): 1.44478 CPU system time (s): 0.068989 CPU usage (%): 96.8107 Max. virtual memory (Kb): 1032 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####