Name | normalized-opb/mps-v2-20-10/plato.asu.edu/pub/unibo/normalized-mps-v2-20-10-B2C1S1.opb |
MD5SUM | b0cb3e99053428809f85a5c10e91266f |
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 | 38688 |
Biggest coefficient in the objective function | 348966092800 |
Number of bits for the biggest coefficient in the objective function | 39 |
Sum of the numbers in the objective function | 299074813804544 |
Number of bits of the sum of numbers in the objective function | 49 |
Biggest number in a constraint | 348966092800 |
Number of bits of the biggest number in a constraint | 39 |
Biggest sum of numbers in a constraint | 299074813804544 |
Number of bits of the biggest sum of numbers | 49 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 0.959853 |
Number of variables | 107808 |
Total number of constraints | 4192 |
Number of constraints which are clauses | 0 |
Number of constraints which are cardinality constraints (but not clauses) | 288 |
Number of constraints which are nor clauses,nor cardinality constraints | 3904 |
Minimum length of a constraint | 1 |
Maximum length of a constraint | 1440 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc9 THE 2005-05-24 14:36:12 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=14900 boxname=wulflinc9 idbench=1147 idsolver=2 numberseed=0 MD5SUM SOLVER: 754786be69defe53c030aa54f111e0a7 /oldhome/oroussel/solvers/bsolo_lpr_cuts MD5SUM BENCH: b0cb3e99053428809f85a5c10e91266f /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-B2C1S1.opb REAL COMMAND: bsolo_lpr_cuts /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-B2C1S1.opb IDLAUNCH: 14900 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.242 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 : 2 cpu MHz : 451.242 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: 947008 kB Buffers: 34012 kB Cached: 30772 kB SwapCached: 88 kB Active: 56264 kB Inactive: 11516 kB HighTotal: 131008 kB HighFree: 95956 kB LowTotal: 903652 kB LowFree: 851052 kB SwapTotal: 2097136 kB SwapFree: 2097048 kB Dirty: 0 kB Writeback: 0 kB Mapped: 6888 kB Slab: 14300 kB Committed_AS: 63596 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-24 14:41:55 (client local time) WITH STATUS 0 IN 336.574 SECONDS stats: 14900 7 336.574 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c ERROR Parsing file!!! c ERROR parsing line: -500*x__17101_bit_10 -1000*x__17101_bit_9 -2000*x__17101_bit_8 -4000*x__17101_bit_7 -8000*x__17101_bit_6 -16000*x__17101_bit_5 -32000*x__17101_bit_4 -64000*x__17101_bit_3 -128000*x__17101_bit_2 -256000*x__17101_bit_1 -512000*x__17101_bit0 -1024000*x__17101_bit1 -2048000*x__17101_bit2 -4096000*x__17101_bit3 -8192000*x__17101_bit4 -16384000*x__17101_bit5 -32768000*x__17101_bit6 -65536000*x__17101_bit7 -131072000*x__17101_bit8 -262144000*x__17101_bit9 -524288000*x__17101_bit10 -1048576000*x__17101_bit11 -2097152000*x__17101_bit12 -4194304000*x__17101_bit13 -8388608000*x__17101_bit14 -16777216000*x__17101_bit15 -33554432000*x__17101_bit16 -67108864000*x__17101_bit17 -134217728000*x__17101_bit18 -268435456000*x__17101_bit19 -100*x__19101_bit_10 -200*x__19101_bit_9 -400*x__19101_bit_8 -800*x__19101_bit_7 -1600*x__19101_bit_6 -3200*x__19101_bit_5 -6400*x__19101_bit_4 -12800*x__19101_bit_3 -25600*x__19101_bit_2 -51200*x__19101_bit_1 -102400*x__19101_bit0 -204800*x__19101_bit1 -409600*x__19101_bit2 -819200*x__19101_bit3 -1638400*x__19101_bit4 -3276800*x__19101_bit5 -6553600*x__19101_bit6 -13107200*x__19101_bit7 -26214400*x__19101_bit8 -52428800*x__19101_bit9 -104857600*x__19101_bit10 -209715200*x__19101_bit11 -419430400*x__19101_bit12 -838860800*x__19101_bit13 -1677721600*x__19101_bit14 -3355443200*x__19101_bit15 -6710886400*x__19101_bit16 -13421772800*x__19101_bit17 -26843545600*x__19101_bit18 -53687091200*x__19101_bit19 -500*x__21101_bit_10 -1000*x__21101_bit_9 -2000*x__21101_bit_8 -4000*x__21101_bit_7 -8000*x__21101_bit_6 -16000*x__21101_bit_5 -32000*x__21101_bit_4 -64000*x__21101_bit_3 -128000*x__21101_bit_2 -256000*x__21101_bit_1 -512000*x__21101_bit0 -1024000*x__21101_bit1 -2048000*x__21101_bit2 -4096000*x__21101_bit3 -8192000*x__21101_bit4 -16384000*x__21101_bit5 -32768000*x__21101_bit6 -65536000*x__21101_bit7 -131072000*x__21101_bit8 -262144000*x__21101_bit9 -524288000*x__21101_bit10 -1048576000*x__21101_bit11 -2097152000*x__21101_bit12 -4194304000*x__21101_bit13 -8388608000*x__21101_bit14 -16777216000*x__21101_bit15 -33554432000*x__21101_bit16 -67108864000*x__21101_bit17 -134217728000*x__21101_bit18 -268435456000*x__21101_bit19 -300*x__23101_bit_10 -600*x__23101_bit_9 -1200*x__23101_bit_8 -2400*x__23101_bit_7 -4800*x__23101_bit_6 -9600*x__23101_bit_5 -19200*x__23101_bit_4 -38400*x__23101_bit_3 -76800*x__23101_bit_2 -153600*x__23101_bit_1 -307200*x__23101_bit0 -614400*x__23101_bit1 -1228800*x__23101_bit2 -2457600*x__23101_bit3 -4915200*x__23101_bit4 -9830400*x__23101_bit5 -19660800*x__23101_bit6 -39321600*x__23101_bit7 -78643200*x__23101_bit8 -157286400*x__23101_bit9 -314572800*x__23101_bit10 -629145600*x__23101_bit11 -1258291200*x__23101_bit12 -2516582400*x__23101_bit13 -5033164800*x__23101_bit14 -10066329600*x__23101_bit15 -20132659200*x__23101_bit16 -40265318400*x__23101_bit17 -80530636800*x__23101_bit18 -161061273600*x__23101_bit19 -500*x__25101_bit_10 -1000*x__25101_bit_9 -2000*x__25101_bit_8 -4000*x__25101_bit_7 -8000*x__25101_bit_6 -16000*x__25101_bit_5 -32000*x__25101_bit_4 -64000*x__25101_bit_3 -128000*x__25101_bit_2 -256000*x__25101_bit_1 -512000*x__25101_bit0 -1024000*x__25101_bit1 -2048000*x__25101_bit2 -4096000*x__25101_bit3 -8192000*x__25101_bit4 -16384000*x__25101_bit5 -32768000*x__25101_bit6 -65536000*x__25101_bit7 -131072000*x__25101_bit8 -262144000*x__25101_bit9 -524288000*x__25101_bit10 -1048576000*x__25101_bit11 -2097152000*x__25101_bit12 -4194304000*x__25101_bit13 -8388608000*x__25101_bit14 -16777216000*x__25101_bit15 -33554432000*x__25101_bit16 -67108864000*x__25101_bit17 -134217728000*x__25101_bit18 -268435456000*x__25101_bit19 -100*x__27101_bit_10 -200*x__27101_bit_9 -400*x__27101_bit_8 -800*x__27101_bit_7 -1600*x__27101_bit_6 -3200*x__27101_bit_5 -6400*x__27101_bit_4 -12800*x__27101_bit_3 -25600*x__27101_bit_2 -51200*x__27101_bit_1 -102400*x__27101_bit0 -204800*x__27101_bit1 -409600*x__27101_bit2 -819200*x__27101_bit3 -1638400*x__27101_bit4 -3276800*x__27101_bit5 -6553600*x__27101_bit6 -13107200*x__27101_bit7 -26214400*x__27101_bit8 -52428800*x__27101_bit9 -104857600*x__27101_bit10 -209715200*x__27101_bit11 -419430400*x__27101_bit12 -838860800*x__27101_bit13 -1677721600*x__27101_bit14 -3355443200*x__27101_bit15 -6710886400*x__27101_bit16 -13421772800*x__27101_bit17 -26843545600*x__27101_bit18 -53687091200*x__27101_bit19 -500*x__29101_bit_10 -1000*x__29101_bit_9 -2000*x__29101_bit_8 -4000*x__29101_bit_7 -8000*x__29101_bit_6 -16000*x__29101_bit_5 -32000*x__29101_bit_4 -64000*x__29101_bit_3 -128000*x__29101_bit_2 -256000*x__29101_bit_1 -512000*x__29101_bit0 -1024000*x__29101_bit1 -2048000*x__29101_bit2 -4096000*x__29101_bit3 -8192000*x__29101_bit4 -16384000*x__29101_bit5 -32768000*x__29101_bit6 -65536000*x__29101_bit7 -131072000*x__29101_bit8 -262144000*x__29101_bit9 -524288000*x__29101_bit10 -1048576000*x__29101_bit11 -2097152000*x__29101_bit12 -4194304000*x__29101_bit13 -8388608000*x__29101_bit14 -16777216000*x__29101_bit15 -33554432000*x__29101_bit16 -67108864000*x__29101_bit17 -134217728000*x__29101_bit18 -268435456000*x__29101_bit19 -300*x__31101_bit_10 -600*x__31101_bit_9 -1200*x__31101_bit_8 -2400*x__31101_bit_7 -4800*x__31101_bit_6 -9600*x__31101_bit_5 -19200*x__31101_bit_4 -38400*x__31101_bit_3 -76800*x__31101_bit_2 -153600*x__31101_bit_1 -307200*x__31101_bit0 -614400*x__31101_bit1 -1228800*x__31101_bit2 -2457600*x__31101_bit3 -4915200*x__31101_bit4 -9830400*x__31101_bit5 -19660800*x__31101_bit6 -39321600*x__31101_bit7 -78643200*x__31101_bit8 -157286400*x__31101_bit9 -314572800*x__31101_bit10 -629145600*x__31101_bit11 -1258291200*x__31101_bit12 -2516582400*x__31101_bit13 -5033164800*x__31101_bit14 -10066329600*x__31101_bit15 -20132659200*x__31101_bit16 -40265318400*x__31101_bit17 -80530636800*x__31101_bit18 -161061273600*x__31101_bit19 -500*x__33101_bit_10 -1000*x__33101_bit_9 -2000*x__33101_bit_8 -4000*x__33101_bit_7 -8000*x__33101_bit_6 -16000*x__33101_bit_5 -32000*x__33101_bit_4 -64000*x__33101_bit_3 -128000*x__33101_bit_2 -256000*x__33101_bit_1 -512000*x__33101_bit0 -1024000*x__33101_bit1 -2048000*x__33101_bit2 -4096000*x__33101_bit3 -8192000*x__33101_bit4 -16384000*x__33101_bit5 -32768000*x__33101_bit6 -65536000*x__33101_bit7 -131072000*x__33101_bit8 -262144000*x__33101_bit9 -524288000*x__33101_bit10 -1048576000*x__33101_bit11 -2097152000*x__33101_bit12 -4194304000*x__33101_bit13 -8388608000*x__33101_bit14 -16777216000*x__33101_bit15 -33554432000*x__33101_bit16 -67108864000*x__33101_bit17 -134217728000*x__33101_bit18 -268435456000*x__33101_bit19 -100*x__35101_bit_10 -200*x__35101_bit_9 -400*x__35101_bit_8 -800*x__35101_bit_7 -1600*x__35101_bit_6 -3200*x__35101_bit_5 -6400*x__35101_bit_4 -12800*x__35101_bit_3 -25600*x__35101_bit_2 -51200*x__35101_bit_1 -102400*x__35101_bit0 -204800*x__35101_bit1 -409600*x__35101_bit2 -819200*x__35101_bit3 -1638400*x__35101_bit4 -3276800*x__35101_bit5 -6553600*x__35101_bit6 -13107200*x__35101_bit7 -26214400*x__35101_bit8 -52428800*x__35101_bit9 -104857600*x__35101_bit10 -209715200*x__35101_bit11 -419430400*x__35101_bit12 -838860800*x__35101_bit13 -1677721600*x__35101_bit14 -3355443200*x__35101_bit15 -6710886400*x__35101_bit16 -13421772800*x__35101_bit17 -26843545600*x__35101_bit18 -53687091200*x__35101_bit19 -500*x__37101_bit_10 -1000*x__37101_bit_9 -2000*x__37101_bit_8 -4000*x__37101_bit_7 -8000*x__37101_bit_6 -16000*x__37101_bit_5 -32000*x__37101_bit_4 -64000*x__37101_bit_3 -128000*x__37101_bit_2 -256000*x__37101_bit_1 -512000*x__37101_bit0 -1024000*x__37101_bit1 -2048000*x__37101_bit2 -4096000*x__37101_bit3 -8192000*x__37101_bit4 -16384000*x__37101_bit5 -32768000*x__37101_bit6 -65536000*x__37101_bit7 -131072000*x__37101_bit8 -262144000*x__37101_bit9 -524288000*x__37101_bit10 -1048576000*x__37101_bit11 -2097152000*x__37101_bit12 -4194304000*x__37101_bit13 -8388608000*x__37101_bit14 -16777216000*x__37101_bit15 -33554432000*x__37101_bit16 -67108864000*x__37101_bit17 -134217728000*x__37101_bit18 -268435456000*x__37101_bit19 -300*x__39101_bit_10 -600*x__39101_bit_9 -1200*x__39101_bit_8 -2400*x__39101_bit_7 -4800*x__39101_bit_6 -9600*x__39101_bit_5 -19200*x__39101_bit_4 -38400*x__39101_bit_3 -76800*x__39101_bit_2 -153600*x__39101_bit_1 -307200*x__39101_bit0 -614400*x__39101_bit1 -1228800*x__39101_bit2 -2457600*x__39101_bit3 -4915200*x__39101_bit4 -9830400*x__39101_bit5 -19660800*x__39101_bit6 -39321600*x__39101_bit7 -78643200*x__39101_bit8 -157286400*x__39101_bit9 -314572800*x__39101_bit10 -629145600*x__39101_bit11 -1258291200*x__39101_bit12 -2516582400*x__39101_bit13 -5033164800*x__39101_bit14 -10066329600*x__39101_bit15 -20132659200*x__39101_bit16 -40265318400*x__39101_bit17 -80530636800*x__39101_bit18 -161061273600*x__39101_bit19 -500*x__41101_bit_10 -1000*x__41101_bit_9 -2000*x__41101_bit_8 -4000*x__41101_bit_7 -8000*x__41101_bit_6 -16000*x__41101_bit_5 -32000*x__41101_bit_4 -64000*x__41101_bit_3 -128000*x__41101_bit_2 -256000*x__41101_bit_1 -512000*x__41101_bit0 -1024000*x__41101_bit1 -2048000*x__41101_bit2 -4096000*x__41101_bit3 -8192000*x__41101_bit4 -16384000*x__41101_bit5 -32768000*x__41101_bit6 -65536000*x__41101_bit7 -131072000*x__41101_bit8 -262144000*x__41101_bit9 -524288000*x__41101_bit10 -1048576000*x__41101_bit11 -2097152000*x__41101_bit12 -4194304000*x__41101_bit13 -8388608000*x__41101_bit14 -16777216000*x__41101_bit15 -33554432000*x__41101_bit16 -67108864000*x__41101_bit17 -134217728000*x__41101_bit18 -268435456000*x__41101_bit19 -100*x__43101_bit_10 -200*x__43101_bit_9 -400*x__43101_bit_8 -800*x__43101_bit_7 -1600*x__43101_bit_6 -3200*x__43101_bit_5 -6400*x__43101_bit_4 -12800*x__43101_bit_3 -25600*x__43101_bit_2 -51200*x__43101_bit_1 -102400*x__43101_bit0 -204800*x__43101_bit1 -409600*x__43101_bit2 -819200*x__43101_bit3 -1638400*x__43101_bit4 -3276800*x__43101_bit5 -6553600*x__43101_bit6 -13107200*x__43101_bit7 -26214400*x__43101_bit8 -52428800*x__43101_bit9 -104857600*x__43101_bit10 -209715200*x__43101_bit11 -419430400*x__43101_bit12 -838860800*x__43101_bit13 -1677721600*x__43101_bit14 -3355443200*x__43101_bit15 -6710886400*x__43101_bit16 -13421772800*x__43101_bit17 -26843545600*x__43101_bit18 -53687091200*x__43101_bit19 -500*x__45101_bit_10 -1000*x__45101_bit_9 -2000*x__45101_bit_8 -4000*x__45101_bit_7 -8000*x__45101_bit_6 -16000*x__45101_bit_5 -32000*x__45101_bit_4 -64000*x__45101_bit_3 -128000*x__45101_bit_2 -256000*x__45101_bit_1 -512000*x__45101_bit0 -1024000*x__45101_bit1 -2048000*x__45101_bit2 -4096000*x__45101_bit3 -8192000*x__45101_bit4 -16384000*x__45101_bit5 -32768000*x__45101_bit6 -65536000*x__45101_bit7 -131072000*x__45101_bit8 -262144000*x__45101_bit9 -524288000*x__45101_bit10 -1048576000*x__45101_bit11 -2097152000*x__45101_bit12 -4194304000*x__45101_bit13 -8388608000*x__45101_bit14 -16777216000*x__45101_bit15 -33554432000*x__45101_bit16 -67108864000*x__45101_bit17 -134217728000*x__45101_bit18 -268435456000*x__45101_bit19 -300*x__47101_bit_10 -600*x__47101_bit_9 -1200*x__47101_bit_8 -2400*x__47101_bit_7 -4800*x__47101_bit_6 -9600*x__47101_bit_5 -19200*x__47101_bit_4 -38400*x__47101_bit_3 -76800*x__47101_bit_2 -153600*x__47101_bit_1 -307200*x__47101_bit0 -614400*x__47101_bit1 -1228800*x__47101_bit2 -2457600*x__47101_bit3 -4915200*x__47101_bit4 -9830400*x__47101_bit5 -19660800*x__47101_bit6 -39321600*x__47101_bit7 -78643200*x__47101_bit8 -157286400*x__47101_bit9 -314572800*x__47101_bit10 -629145600*x__47101_bit11 -1258291200*x__47101_bit12 -2516582400*x__47101_bit13 -5033164800*x__47101_bit14 -10066329600*x__47101_bit15 -20132659200*x__47101_bit16 -40265318400*x__47101_bit17 -80530636800*x__47101_bit18 -161061273600*x__47101_bit19 -10*x__49101_bit_10 -20*x__49101_bit_9 -40*x__49101_bit_8 -80*x__49101_bit_7 -160*x__49101_bit_6 -320*x__49101_bit_5 -640*x__49101_bit_4 -1280*x__49101_bit_3 -2560*x__49101_bit_2 -5120*x__49101_bit_1 -10240*x__49101_bit0 -20480*x__49101_bit1 -40960*x__49101_bit2 -81920*x__49101_bit3 -163840*x__49101_bit4 -327680*x__49101_bit5 -655360*x__49101_bit6 -1310720*x__49101_bit7 -2621440*x__49101_bit8 -5242880*x__49101_bit9 -10485760*x__49101_bit10 -20971520*x__49101_bit11 -41943040*x__49101_bit12 -83886080*x__49101_bit13 -167772160*x__49101_bit14 -335544320*x__49101_bit15 -671088640*x__49101_bit16 -1342177280*x__49101_bit17 -2684354560*x__49101_bit18 -5368709120*x__49101_bit19 -15*x__50101_bit_10 -30*x__50101_bit_9 -60*x__50101_bit_8 -120*x__50101_bit_7 -240*x__50101_bit_6 -480*x__50101_bit_5 -960*x__50101_bit_4 -1920*x__50101_bit_3 -3840*x__50101_bit_2 -7680*x__50101_bit_1 -15360*x__50101_bit0 -30720*x__50101_bit1 -61440*x__50101_bit2 -122880*x__50101_bit3 -245760*x__50101_bit4 -491520*x__50101_bit5 -983040*x__50101_bit6 -1966080*x__50101_bit7 -3932160*x__50101_bit8 -7864320*x__50101_bit9 -15728640*x__50101_bit10 -31457280*x__50101_bit11 -62914560*x__50101_bit12 -125829120*x__50101_bit13 -251658240*x__50101_bit14 -503316480*x__50101_bit15 -1006632960*x__50101_bit16 -2013265920*x__50101_bit17 -4026531840*x__50101_bit18 -8053063680*x__50101_bit19 -10*x__51101_bit_10 -20*x__51101_bit_9 -40*x__51101_bit_8 -80*x__51101_bit_7 -160*x__51101_bit_6 -320*x__51101_bit_5 -640*x__51101_bit_4 -1280*x__51101_bit_3 -2560*x__51101_bit_2 -5120*x__51101_bit_1 -10240*x__51101_bit0 -20480*x__51101_bit1 -40960*x__51101_bit2 -81920*x__51101_bit3 -163840*x__51101_bit4 -327680*x__51101_bit5 -655360*x__51101_bit6 -1310720*x__51101_bit7 -2621440*x__51101_bit8 -5242880*x__51101_bit9 -10485760*x__51101_bit10 -20971520*x__51101_bit11 -41943040*x__51101_bit12 -83886080*x__51101_bit13 -167772160*x__51101_bit14 -335544320*x__51101_bit15 -671088640*x__51101_bit16 -1342177280*x__51101_bit17 -2684354560*x__51101_bit18 -5368709120*x__51101_bit19 -15*x__52101_bit_10 -30*x__52101_bit_9 -60*x__52101_bit_8 -120*x__52101_bit_7 -240*x__52101_bit_6 -480*x__52101_bit_5 -960*x__52101_bit_4 -1920*x__52101_bit_3 -3840*x__52101_bit_2 -7680*x__52101_bit_1 -15360*x__52101_bit0 -30720*x__52101_bit1 -61440*x__52101_bit2 -122880*x__52101_bit3 -245760*x__52101_bit4 -491520*x__52101_bit5 -983040*x__52101_bit6 -1966080*x__52101_bit7 -3932160*x__52101_bit8 -7864320*x__52101_bit9 -15728640*x__52101_bit10 -31457280*x__52101_bit11 -62914560*x__52101_bit12 -125829120*x__52101_bit13 -251658240*x__52101_bit14 -503316480*x__52101_bit15 -1006632960*x__52101_bit16 -2013265920*x__52101_bit17 -4026531840*x__52101_bit18 -8053063680*x__52101_bit19 -2*x__53101_bit_10 -4*x__53101_bit_9 -8*x__53101_bit_8 -16*x__53101_bit_7 -32*x__53101_bit_6 -64*x__53101_bit_5 -128*x__53101_bit_4 -256*x__53101_bit_3 -512*x__53101_bit_2 -1024*x__53101_bit_1 -2048*x__53101_bit0 -4096*x__53101_bit1 -8192*x__53101_bit2 -16384*x__53101_bit3 -32768*x__53101_bit4 -65536*x__53101_bit5 -131072*x__53101_bit6 -262144*x__53101_bit7 -524288*x__53101_bit8 -1048576*x__53101_bit9 -2097152*x__53101_bit10 -4194304*x__53101_bit11 -8388608*x__53101_bit12 -16777216*x__53101_bit13 -33554432*x__53101_bit14 -67108864*x__53101_bit15 -134217728*x__53101_bit16 -268435456*x__53101_bit17 -536870912*x__53101_bit18 -1073741824*x__53101_bit19 -10*x__54101_bit_10 -20*x__54101_bit_9 -40*x__54101_bit_8 -80*x__54101_bit_7 -160*x__54101_bit_6 -320*x__54101_bit_5 -640*x__54101_bit_4 -1280*x__54101_bit_3 -2560*x__54101_bit_2 -5120*x__54101_bit_1 -10240*x__54101_bit0 -20480*x__54101_bit1 -40960*x__54101_bit2 -81920*x__54101_bit3 -163840*x__54101_bit4 -327680*x__54101_bit5 -655360*x__54101_bit6 -1310720*x__54101_bit7 -2621440*x__54101_bit8 -5242880*x__54101_bit9 -10485760*x__54101_bit10 -20971520*x__54101_bit11 -41943040*x__54101_bit12 -83886080*x__54101_bit13 -167772160*x__54101_bit14 -335544320*x__54101_bit15 -671088640*x__54101_bit16 -1342177280*x__54101_bit17 -2684354560*x__54101_bit18 -5368709120*x__54101_bit19 -2*x__55101_bit_10 -4*x__55101_bit_9 -8*x__55101_bit_8 -16*x__55101_bit_7 -32*x__55101_bit_6 -64*x__55101_bit_5 -128*x__55101_bit_4 -256*x__55101_bit_3 -512*x__55101_bit_2 -1024*x__55101_bit_1 -2048*x__55101_bit0 -4096*x__55101_bit1 -8192*x__55101_bit2 -16384*x__55101_bit3 -32768*x__55101_bit4 -65536*x__55101_bit5 -131072*x__55101_bit6 -262144*x__55101_bit7 -524288*x__55101_bit8 -1048576*x__55101_bit9 -2097152*x__55101_bit10 -4194304*x__55101_bit11 -8388608*x__55101_bit12 -16777216*x__55101_bit13 -33554432*x__55101_bit14 -67108864*x__55101_bit15 -134217728*x__55101_bit16 -268435456*x__55101_bit17 -536870912*x__55101_bit18 -1073741824*x__55101_bit19 -10*x__56101_bit_10 -20*x__56101_bit_9 -40*x__56101_bit_8 -80*x__56101_bit_7 -160*x__56101_bit_6 -320*x__56101_bit_5 -640*x__56101_bit_4 -1280*x__56101_bit_3 -2560*x__56101_bit_2 -5120*x__56101_bit_1 -10240*x__56101_bit0 -20480*x__56101_bit1 -40960*x__56101_bit2 -81920*x__56101_bit3 -163840*x__56101_bit4 -327680*x__56101_bit5 -655360*x__56101_bit6 -1310720*x__56101_bit7 -2621440*x__56101_bit8 -5242880*x__56101_bit9 -10485760*x__56101_bit10 -20971520*x__56101_bit11 -41943040*x__56101_bit12 -83886080*x__56101_bit13 -167772160*x__56101_bit14 -335544320*x__56101_bit15 -671088640*x__56101_bit16 -1342177280*x__56101_bit17 -2684354560*x__56101_bit18 -5368709120*x__56101_bit19 -5*x__57101_bit_10 -10*x__57101_bit_9 -20*x__57101_bit_8 -40*x__57101_bit_7 -80*x__57101_bit_6 -160*x__57101_bit_5 -320*x__57101_bit_4 -640*x__57101_bit_3 -1280*x__57101_bit_2 -2560*x__57101_bit_1 -5120*x__57101_bit0 -10240*x__57101_bit1 -20480*x__57101_bit2 -40960*x__57101_bit3 -81920*x__57101_bit4 -163840*x__57101_bit5 -327680*x__57101_bit6 -655360*x__57101_bit7 -1310720*x__57101_bit8 -2621440*x__57101_bit9 -5242880*x__57101_bit10 -10485760*x__57101_bit11 -20971520*x__57101_bit12 -41943040*x__57101_bit13 -83886080*x__57101_bit14 -167772160*x__57101_bit15 -335544320*x__57101_bit16 -671088640*x__57101_bit17 -1342177280*x__57101_bit18 -2684354560*x__57101_bit19 -30*x__58101_bit_10 -60*x__58101_bit_9 -120*x__58101_bit_8 -240*x__58101_bit_7 -480*x__58101_bit_6 -960*x__58101_bit_5 -1920*x__58101_bit_4 -3840*x__58101_bit_3 -7680*x__58101_bit_2 -15360*x__58101_bit_1 -30720*x__58101_bit0 -61440*x__58101_bit1 -122880*x__58101_bit2 -245760*x__58101_bit3 -491520*x__58101_bit4 -983040*x__58101_bit5 -1966080*x__58101_bit6 -3932160*x__58101_bit7 -7864320*x__58101_bit8 -15728640*x__58101_bit9 -31457280*x__58101_bit10 -62914560*x__58101_bit11 -125829120*x__58101_bit12 -251658240*x__58101_bit13 -503316480*x__58101_bit14 -1006632960*x__58101_bit15 -2013265920*x__58101_bit16 -4026531840*x__58101_bit17 -8053063680*x__58101_bit18 -16106127360*x__58101_bit19 -5*x__59101_bit_10 -10*x__59101_bit_9 -20*x__59101_bit_8 -40*x__59101_bit_7 -80*x__59101_bit_6 -160*x__59101_bit_5 -320*x__59101_bit_4 -640*x__59101_bit_3 -1280*x__59101_bit_2 -2560*x__59101_bit_1 -5120*x__59101_bit0 -10240*x__59101_bit1 -20480*x__59101_bit2 -40960*x__59101_bit3 -81920*x__59101_bit4 -163840*x__59101_bit5 -327680*x__59101_bit6 -655360*x__59101_bit7 -1310720*x__59101_bit8 -2621440*x__59101_bit9 -5242880*x__59101_bit10 -10485760*x__59101_bit11 -20971520*x__59101_bit12 -41943040*x__59101_bit13 -83886080*x__59101_bit14 -167772160*x__59101_bit15 -335544320*x__59101_bit16 -671088640*x__59101_bit17 -1342177280*x__59101_bit18 -2684354560*x__59101_bit19 -30*x__60101_bit_10 -60*x__60101_bit_9 -120*x__60101_bit_8 -240*x__60101_bit_7 -480*x__60101_bit_6 -960*x__60101_bit_5 -1920*x__60101_bit_4 -3840*x__60101_bit_3 -7680*x__60101_bit_2 -15360*x__60101_bit_1 -30720*x__60101_bit0 -61440*x__60101_bit1 -122880*x__60101_bit2 -245760*x__60101_bit3 -491520*x__60101_bit4 -983040*x__60101_bit5 -1966080*x__60101_bit6 -3932160*x__60101_bit7 -7864320*x__60101_bit8 -15728640*x__60101_bit9 -31457280*x__60101_bit10 -62914560*x__60101_bit11 -125829120*x__60101_bit12 -251658240*x__60101_bit13 -503316480*x__60101_bit14 -1006632960*x__60101_bit15 -2013265920*x__60101_bit16 -4026531840*x__60101_bit17 -8053063680*x__60101_bit18 -16106127360*x__60101_bit19 -2*x__61101_bit_10 -4*x__61101_bit_9 -8*x__61101_bit_8 -16*x__61101_bit_7 -32*x__61101_bit_6 -64*x__61101_bit_5 -128*x__61101_bit_4 -256*x__61101_bit_3 -512*x__61101_bit_2 -1024*x__61101_bit_1 -2048*x__61101_bit0 -4096*x__61101_bit1 -8192*x__61101_bit2 -16384*x__61101_bit3 -32768*x__61101_bit4 -65536*x__61101_bit5 -131072*x__61101_bit6 -262144*x__61101_bit7 -524288*x__61101_bit8 -1048576*x__61101_bit9 -2097152*x__61101_bit10 -4194304*x__61101_bit11 -8388608*x__61101_bit12 -16777216*x__61101_bit13 -33554432*x__61101_bit14 -67108864*x__61101_bit15 -134217728*x__61101_bit16 -268435456*x__61101_bit17 -536870912*x__61101_bit18 -1073741824*x__61101_bit19 -15*x__62101_bit_10 -30*x__62101_bit_9 -60*x__62101_bit_8 -120*x__62101_bit_7 -240*x__62101_bit_6 -480*x__62101_bit_5 -960*x__62101_bit_4 -1920*x__62101_bit_3 -3840*x__62101_bit_2 -7680*x__62101_bit_1 -15360*x__62101_bit0 -30720*x__62101_bit1 -61440*x__62101_bit2 -122880*x__62101_bit3 -245760*x__62101_bit4 -491520*x__62101_bit5 -983040*x__62101_bit6 -1966080*x__62101_bit7 -3932160*x__62101_bit8 -7864320*x__62101_bit9 -15728640*x__62101_bit10 -31457280*x__62101_bit11 -62914560*x__62101_bit12 -125829120*x__62101_bit13 -251658240*x__62101_bit14 -503316480*x__62101_bit15 -1006632960*x__62101_bit16 -2013265920*x__62101_bit17 -4026531840*x__62101_bit18 -8053063680*x__62101_bit19 -2*x__63101_bit_10 -4*x__63101_bit_9 -8*x__63101_bit_8 -16*x__63101_bit_7 -32*x__63101_bit_6 -64*x__63101_bit_5 -128*x__63101_bit_4 -256*x__63101_bit_3 -512*x__63101_bit_2 -1024*x__63101_bit_1 -2048*x__63101_bit0 -4096*x__63101_bit1 -8192*x__63101_bit2 -16384*x__63101_bit3 -32768*x__63101_bit4 -65536*x__63101_bit5 -131072*x__63101_bit6 -262144*x__63101_bit7 -524288*x__63101_bit8 -1048576*x__63101_bit9 -2097152*x__63101_bit10 -4194304*x__63101_bit11 -8388608*x__63101_bit12 -16777216*x__63101_bit13 -33554432*x__63101_bit14 -67108864*x__63101_bit15 -134217728*x__63101_bit16 -268435456*x__63101_bit17 -536870912*x__63101_bit18 -1073741824*x__63101_bit19 -15*x__64101_bit_10 -30*x__64101_bit_9 -60*x__64101_bit_8 -120*x__64101_bit_7 -240*x__64101_bit_6 -480*x__64101_bit_5 -960*x__64101_bit_4 -1920*x__64101_bit_3 -3840*x__64101_bit_2 -7680*x__64101_bit_1 -15360*x__64101_bit0 -30720*x__64101_bit1 -61440*x__64101_bit2 -122880*x__64101_bit3 -245760*x__64101_bit4 -491520*x__64101_bit5 -983040*x__64101_bit6 -1966080*x__64101_bit7 -3932160*x__64101_bit8 -7864320*x__64101_bit9 -15728640*x__64101_bit10 -31457280*x__64101_bit11 -62914560*x__64101_bit12 -125829120*x__64101_bit13 -251658240*x__64101_bit14 -503316480*x__64101_bit15 -1006632960*x__64101_bit16 -2013265920*x__64101_bit17 -4026531840*x__64101_bit18 -8053063680*x__64101_bit19 -5*x__65101_bit_10 -10*x__65101_bit_9 -20*x__65101_bit_8 -40*x__65101_bit_7 -80*x__65101_bit_6 -160*x__65101_bit_5 -320*x__65101_bit_4 -640*x__65101_bit_3 -1280*x__65101_bit_2 -2560*x__65101_bit_1 -5120*x__65101_bit0 -10240*x__65101_bit1 -20480*x__65101_bit2 -40960*x__65101_bit3 -81920*x__65101_bit4 -163840*x__65101_bit5 -327680*x__65101_bit6 -655360*x__65101_bit7 -1310720*x__65101_bit8 -2621440*x__65101_bit9 -5242880*x__65101_bit10 -10485760*x__65101_bit11 -20971520*x__65101_bit12 -41943040*x__65101_bit13 -83886080*x__65101_bit14 -167772160*x__65101_bit15 -335544320*x__65101_bit16 -671088640*x__65101_bit17 -1342177280*x__65101_bit18 -2684354560*x__65101_bit19 -25*x__66101_bit_10 -50*x__66101_bit_9 -100*x__66101_bit_8 -200*x__66101_bit_7 -400*x__66101_bit_6 -800*x__66101_bit_5 -1600*x__66101_bit_4 -3200*x__66101_bit_3 -6400*x__66101_bit_2 -12800*x__66101_bit_1 -25600*x__66101_bit0 -51200*x__66101_bit1 -102400*x__66101_bit2 -204800*x__66101_bit3 -409600*x__66101_bit4 -819200*x__66101_bit5 -1638400*x__66101_bit6 -3276800*x__66101_bit7 -6553600*x__66101_bit8 -13107200*x__66101_bit9 -26214400*x__66101_bit10 -52428800*x__66101_bit11 -104857600*x__66101_bit12 -209715200*x__66101_bit13 -419430400*x__66101_bit14 -838860800*x__66101_bit15 -1677721600*x__66101_bit16 -3355443200*x__66101_bit17 -6710886400*x__66101_bit18 -13421772800*x__66101_bit19 -5*x__67101_bit_10 -10*x__67101_bit_9 -20*x__67101_bit_8 -40*x__67101_bit_7 -80*x__67101_bit_6 -160*x__67101_bit_5 -320*x__67101_bit_4 -640*x__67101_bit_3 -1280*x__67101_bit_2 -2560*x__67101_bit_1 -5120*x__67101_bit0 -10240*x__67101_bit1 -20480*x__67101_bit2 -40960*x__67101_bit3 -81920*x__67101_bit4 -163840*x__67101_bit5 -327680*x__67101_bit6 -655360*x__67101_bit7 -1310720*x__67101_bit8 -2621440*x__67101_bit9 -5242880*x__67101_bit10 -10485760*x__67101_bit11 -20971520*x__67101_bit12 -41943040*x__67101_bit13 -83886080*x__67101_bit14 -167772160*x__67101_bit15 -335544320*x__67101_bit16 -671088640*x__67101_bit17 -1342177280*x__67101_bit18 -2684354560*x__67101_bit19 -25*x__68101_bit_10 -50*x__68101_bit_9 -100*x__68101_bit_8 -200*x__68101_bit_7 -400*x__68101_bit_6 -800*x__68101_bit_5 -1600*x__68101_bit_4 -3200*x__68101_bit_3 -6400*x__68101_bit_2 -12800*x__68101_bit_1 -25600*x__68101_bit0 -51200*x__68101_bit1 -102400*x__68101_bit2 -204800*x__68101_bit3 -409600*x__68101_bit4 -819200*x__68101_bit5 -1638400*x__68101_bit6 -3276800*x__68101_bit7 -6553600*x__68101_bit8 -13107200*x__68101_bit9 -26214400*x__68101_bit10 -52428800*x__68101_bit11 -104857600*x__68101_bit12 -209715200*x__68101_bit13 -419430400*x__68101_bit14 -838860800*x__68101_bit15 -1677721600*x__68101_bit16 -3355443200*x__68101_bit17 -6710886400*x__68101_bit18 -13421772800*x__68101_bit19 -2*x__69101_bit_10 -4*x__69101_bit_9 -8*x__69101_bit_8 -16*x__69101_bit_7 -32*x__69101_bit_6 -64*x__69101_bit_5 -128*x__69101_bit_4 -256*x__69101_bit_3 -512*x__69101_bit_2 -1024*x__69101_bit_1 -2048*x__69101_bit0 -4096*x__69101_bit1 -8192*x__69101_bit2 -16384*x__69101_bit3 -32768*x__69101_bit4 -65536*x__69101_bit5 -131072*x__69101_bit6 -262144*x__69101_bit7 -524288*x__69101_bit8 -1048576*x__69101_bit9 -2097152*x__69101_bit10 -4194304*x__69101_bit11 -8388608*x__69101_bit12 -16777216*x__69101_bit13 -33554432*x__69101_bit14 -67108864*x__69101_bit15 -134217728*x__69101_bit16 -268435456*x__69101_bit17 -536870912*x__69101_bit18 -1073741824*x__69101_bit19 -20*x__70101_bit_10 -40*x__70101_bit_9 -80*x__70101_bit_8 -160*x__70101_bit_7 -320*x__70101_bit_6 -640*x__70101_bit_5 -1280*x__70101_bit_4 -2560*x__70101_bit_3 -5120*x__70101_bit_2 -10240*x__70101_bit_1 -20480*x__70101_bit0 -40960*x__70101_bit1 -81920*x__70101_bit2 -163840*x__70101_bit3 -327680*x__70101_bit4 -655360*x__70101_bit5 -1310720*x__70101_bit6 -2621440*x__70101_bit7 -5242880*x__70101_bit8 -10485760*x__70101_bit9 -20971520*x__70101_bit10 -41943040*x__70101_bit11 -83886080*x__70101_bit12 -167772160*x__70101_bit13 -335544320*x__70101_bit14 -671088640*x__70101_bit15 -1342177280*x__70101_bit16 -2684354560*x__70101_bit17 -5368709120*x__70101_bit18 -10737418240*x__70101_bit19 -2*x__71101_bit_10 -4*x__71101_bit_9 -8*x__71101_bit_8 -16*x__71101_bit_7 -32*x__71101_bit_6 -64*x__71101_bit_5 -128*x__71101_bit_4 -256*x__71101_bit_3 -512*x__71101_bit_2 -1024*x__71101_bit_1 -2048*x__71101_bit0 -4096*x__71101_bit1 -8192*x__71101_bit2 -16384*x__71101_bit3 -32768*x__71101_bit4 -65536*x__71101_bit5 -131072*x__71101_bit6 -262144*x__71101_bit7 -524288*x__71101_bit8 -1048576*x__71101_bit9 -2097152*x__71101_bit10 -4194304*x__71101_bit11 -8388608*x__71101_bit12 -16777216*x__71101_bit13 -33554432*x__71101_bit14 -67108864*x__71101_bit15 -134217728*x__71101_bit16 -268435456*x__71101_bit17 -536870912*x__71101_bit18 -1073741824*x__71101_bit19 -20*x__72101_bit_10 -40*x__72101_bit_9 -80*x__72101_bit_8 -160*x__72101_bit_7 -320*x__72101_bit_6 -640*x__72101_bit_5 -1280*x__72101_bit_4 -2560*x__72101_bit_3 -5120*x__72101_bit_2 -10240*x__72101_bit_1 -20480*x__72101_bit0 -40960*x__72101_bit1 -81920*x__72101_bit2 -163840*x__72101_bit3 -327680*x__72101_bit4 -655360*x__72101_bit5 -1310720*x__72101_bit6 -2621440*x__72101_bit7 -5242880*x__72101_bit8 -10485760*x__72101_bit9 -20971520*x__72101_bit10 -41943040*x__72101_bit11 -83886080*x__72101_bit12 -167772160*x__72101_bit13 -335544320*x__72101_bit14 -671088640*x__72101_bit15 -1342177280*x__72101_bit16 -2684354560*x__72101_bit17 -5368709120*x__72101_bit18 -10737418240*x__72101_bit19 -5*x__73101_bit_10 -10*x__73101_bit_9 -20*x__73101_bit_8 -40*x__73101_bit_7 -80*x__73101_bit_6 -160*x__73101_bit_5 -320*x__73101_bit_4 -640*x__73101_bit_3 -1280*x__73101_bit_2 -2560*x__73101_bit_1 -5120*x__73101_bit0 -10240*x__73101_bit1 -20480*x__73101_bit2 -40960*x__73101_bit3 -81920*x__73101_bit4 -163840*x__73101_bit5 -327680*x__73101_bit6 -655360*x__73101_bit7 -1310720*x__73101_bit8 -2621440*x__73101_bit9 -5242880*x__73101_bit10 -10485760*x__73101_bit11 -20971520*x__73101_bit12 -41943040*x__73101_bit13 -83886080*x__73101_bit14 -167772160*x__73101_bit15 -335544320*x__73101_bit16 -671088640*x__73101_bit17 -1342177280*x__73101_bit18 -2684354560*x__73101_bit19 -35*x__74101_bit_10 -70*x__74101_bit_9 -140*x__74101_bit_8 -280*x__74101_bit_7 -560*x__74101_bit_6 -1120*x__74101_bit_5 -2240*x__74101_bit_4 -4480*x__74101_bit_3 -8960*x__74101_bit_2 -17920*x__74101_bit_1 -35840*x__74101_bit0 -71680*x__74101_bit1 -143360*x__74101_bit2 -286720*x__74101_bit3 -573440*x__74101_bit4 -1146880*x__74101_bit5 -2293760*x__74101_bit6 -4587520*x__74101_bit7 -9175040*x__74101_bit8 -18350080*x__74101_bit9 -36700160*x__74101_bit10 -73400320*x__74101_bit11 -146800640*x__74101_bit12 -293601280*x__74101_bit13 -587202560*x__74101_bit14 -1174405120*x__74101_bit15 -2348810240*x__74101_bit16 -4697620480*x__74101_bit17 -9395240960*x__74101_bit18 -18790481920*x__74101_bit19 -5*x__75101_bit_10 -10*x__75101_bit_9 -20*x__75101_bit_8 -40*x__75101_bit_7 -80*x__75101_bit_6 -160*x__75101_bit_5 -320*x__75101_bit_4 -640*x__75101_bit_3 -1280*x__75101_bit_2 -2560*x__75101_bit_1 -5120*x__75101_bit0 -10240*x__75101_bit1 -20480*x__75101_bit2 -40960*x__75101_bit3 -81920*x__75101_bit4 -163840*x__75101_bit5 -327680*x__75101_bit6 -655360*x__75101_bit7 -1310720*x__75101_bit8 -2621440*x__75101_bit9 -5242880*x__75101_bit10 -10485760*x__75101_bit11 -20971520*x__75101_bit12 -41943040*x__75101_bit13 -83886080*x__75101_bit14 -167772160*x__75101_bit15 -335544320*x__75101_bit16 -671088640*x__75101_bit17 -1342177280*x__75101_bit18 -2684354560*x__75101_bit19 -35*x__76101_bit_10 -70*x__76101_bit_9 -140*x__76101_bit_8 -280*x__76101_bit_7 -560*x__76101_bit_6 -1120*x__76101_bit_5 -2240*x__76101_bit_4 -4480*x__76101_bit_3 -8960*x__76101_bit_2 -17920*x__76101_bit_1 -35840*x__76101_bit0 -71680*x__76101_bit1 -143360*x__76101_bit2 -286720*x__76101_bit3 -573440*x__76101_bit4 -1146880*x__76101_bit5 -2293760*x__76101_bit6 -4587520*x__76101_bit7 -9175040*x__76101_bit8 -18350080*x__76101_bit9 -36700160*x__76101_bit10 -73400320*x__76101_bit11 -146800640*x__76101_bit12 -293601280*x__76101_bit13 -587202560*x__76101_bit14 -1174405120*x__76101_bit15 -2348810240*x__76101_bit16 -4697620480*x__76101_bit17 -9395240960*x__76101_bit18 -18790481920*x__76101_bit19 -2*x__77101_bit_10 -4*x__77101_bit_9 -8*x__77101_bit_8 -16*x__77101_bit_7 -32*x__77101_bit_6 -64*x__77101_bit_5 -128*x__77101_bit_4 -256*x__77101_bit_3 -512*x__77101_bit_2 -1024*x__77101_bit_1 -2048*x__77101_bit0 -4096*x__77101_bit1 -8192*x__77101_bit2 -16384*x__77101_bit3 -32768*x__77101_bit4 -65536*x__77101_bit5 -131072*x__77101_bit6 -262144*x__77101_bit7 -524288*x__77101_bit8 -1048576*x__77101_bit9 -2097152*x__77101_bit10 -4194304*x__77101_bit11 -8388608*x__77101_bit12 -16777216*x__77101_bit13 -33554432*x__77101_bit14 -67108864*x__77101_bit15 -134217728*x__77101_bit16 -268435456*x__77101_bit17 -536870912*x__77101_bit18 -1073741824*x__77101_bit19 -25*x__78101_bit_10 -50*x__78101_bit_9 -100*x__78101_bit_8 -200*x__78101_bit_7 -400*x__78101_bit_6 -800*x__78101_bit_5 -1600*x__78101_bit_4 -3200*x__78101_bit_3 -6400*x__78101_bit_2 -12800*x__78101_bit_1 -25600*x__78101_bit0 -51200*x__78101_bit1 -102400*x__78101_bit2 -204800*x__78101_bit3 -409600*x__78101_bit4 -819200*x__78101_bit5 -1638400*x__78101_bit6 -3276800*x__78101_bit7 -6553600*x__78101_bit8 -13107200*x__78101_bit9 -26214400*x__78101_bit10 -52428800*x__78101_bit11 -104857600*x__78101_bit12 -209715200*x__78101_bit13 -419430400*x__78101_bit14 -838860800*x__78101_bit15 -1677721600*x__78101_bit16 -3355443200*x__78101_bit17 -6710886400*x__78101_bit18 -13421772800*x__78101_bit19 -2*x__79101_bit_10 -4*x__79101_bit_9 -8*x__79101_bit_8 -16*x__79101_bit_7 -32*x__79101_bit_6 -64*x__79101_bit_5 -128*x__79101_bit_4 -256*x__79101_bit_3 -512*x__79101_bit_2 -1024*x__79101_bit_1 -2048*x__79101_bit0 -4096*x__79101_bit1 -8192*x__79101_bit2 -16384*x__79101_bit3 -32768*x__79101_bit4 -65536*x__79101_bit5 -131072*x__79101_bit6 -262144*x__79101_bit7 -524288*x__79101_bit8 -1048576*x__79101_bit9 -2097152*x__79101_bit10 -4194304*x__79101_bit11 -8388608*x__79101_bit12 -16777216*x__79101_bit13 -33554432*x__79101_bit14 -67108864*x__79101_bit15 -134217728*x__79101_bit16 -268435456*x__79101_bit17 -536870912*x__79101_bit18 -1073741824*x__79101_bit19 -25*x__80101_bit_10 -50*x__80101_bit_9 -100*x__80101_bit_8 -200*x__80101_bit_7 -400*x__80101_bit_6 -800*x__80101_bit_5 -1600*x__80101_bit_4 -3200*x__80101_bit_3 -6400*x__80101_bit_2 -12800*x__80101_bit_1 -25600*x__80101_bit0 -51200*x__80101_bit1 -102400*x__80101_bit2 -204800*x__80101_bit3 -409600*x__80101_bit4 -819200*x__80101_bit5 -1638400*x__80101_bit6 -3276800*x__80101_bit7 -6553600*x__80101_bit8 -13107200*x__80101_bit9 -26214400*x__80101_bit10 -52428800*x__80101_bit11 -104857600*x__80101_bit12 -209715200*x__80101_bit13 -419430400*x__80101_bit14 -838860800*x__80101_bit15 -1677721600*x__80101_bit16 -3355443200*x__80101_bit17 -6710886400*x__80101_bit18 -13421772800*x__80101_bit19 >= -76800000; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc9/normalized-mps-v2-20-10-B2C1S1.opb s UNKNOWN c Exit Code: 0 c Total time: 336.52 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.69 1.32 1.82 1/54 3986 Raw data (stat): 3986 (runsolver) D 3985 3944 3943 0 -1 64 4 0 0 0 0 0 0 0 18 0 1 0 772783885 1052672 99 4294967295 134512640 135381576 3221224496 3221219708 135158418 0 2147483391 7 90112 3225161850 0 0 17 0 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 1028 [startup+10.0471 s] Raw data (loadavg): 0.74 1.31 1.81 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 899 0 6 0 643 4 0 0 25 0 1 0 772783885 15945728 829 4294967295 134512640 134714508 3221224592 3221222820 1077414420 0 0 7 0 0 0 0 17 0 0 0 Raw data (statm): 3893 829 1111 63 0 3830 0 vsize: 15572 [startup+20.0599 s] Raw data (loadavg): 0.78 1.29 1.81 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 1246 0 6 0 1642 6 0 0 25 0 1 0 772783885 17420288 1176 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4253 1176 1111 63 0 4190 0 vsize: 17012 [startup+30.0605 s] Raw data (loadavg): 0.81 1.28 1.80 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 1606 0 6 0 2642 7 0 0 25 0 1 0 772783885 18894848 1536 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4613 1536 1111 63 0 4550 0 vsize: 18452 [startup+40.0715 s] Raw data (loadavg): 0.84 1.27 1.79 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 1974 0 6 0 3642 7 0 0 25 0 1 0 772783885 20393984 1904 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 4979 1904 1111 63 0 4916 0 vsize: 19916 [startup+51.3332 s] Raw data (loadavg): 0.94 1.28 1.78 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 2369 0 6 0 4768 8 0 0 25 0 1 0 772783885 22048768 2299 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5383 2299 1111 63 0 5320 0 vsize: 21532 [startup+61.3325 s] Raw data (loadavg): 0.95 1.27 1.77 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 2750 0 6 0 5767 9 0 0 25 0 1 0 772783885 23543808 2680 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 5748 2680 1111 63 0 5685 0 vsize: 22992 [startup+71.3506 s] Raw data (loadavg): 0.96 1.26 1.76 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 3142 0 6 0 6769 9 0 0 25 0 1 0 772783885 25202688 3072 4294967295 134512640 134714508 3221224592 3221222820 1077414433 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6153 3072 1111 63 0 6090 0 vsize: 24612 [startup+81.3602 s] Raw data (loadavg): 0.96 1.25 1.75 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 3524 0 6 0 7769 10 0 0 25 0 1 0 772783885 26701824 3454 4294967295 134512640 134714508 3221224592 3221222820 1077414360 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6519 3454 1111 63 0 6456 0 vsize: 26076 [startup+91.3609 s] Raw data (loadavg): 0.97 1.24 1.75 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 3938 0 6 0 8769 10 0 0 25 0 1 0 772783885 28475392 3868 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 6952 3868 1111 63 0 6889 0 vsize: 27808 [startup+101.367 s] Raw data (loadavg): 0.97 1.23 1.74 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 4373 0 6 0 9769 11 0 0 25 0 1 0 772783885 30281728 4303 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7393 4303 1111 63 0 7330 0 vsize: 29572 [startup+111.367 s] Raw data (loadavg): 0.98 1.22 1.73 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 4810 0 6 0 10768 12 0 0 25 0 1 0 772783885 32124928 4740 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 7843 4740 1111 63 0 7780 0 vsize: 31372 [startup+121.367 s] Raw data (loadavg): 0.98 1.22 1.72 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 5260 0 6 0 11767 13 0 0 25 0 1 0 772783885 33931264 5190 4294967295 134512640 134714508 3221224592 3221222820 1077414345 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 8284 5190 1111 63 0 8221 0 vsize: 33136 [startup+131.367 s] Raw data (loadavg): 0.98 1.21 1.71 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 5710 0 6 0 12767 14 0 0 25 0 1 0 772783885 35737600 5640 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 8725 5640 1111 63 0 8662 0 vsize: 34900 [startup+141.368 s] Raw data (loadavg): 0.98 1.20 1.70 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 6154 0 6 0 13766 15 0 0 25 0 1 0 772783885 37543936 6084 4294967295 134512640 134714508 3221224592 3221222820 1077414338 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 9166 6084 1111 63 0 9103 0 vsize: 36664 [startup+151.369 s] Raw data (loadavg): 0.99 1.19 1.70 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 6640 0 6 0 14765 16 0 0 25 0 1 0 772783885 39501824 6570 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 9644 6570 1111 63 0 9581 0 vsize: 38576 [startup+161.369 s] Raw data (loadavg): 0.99 1.19 1.69 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 7100 0 6 0 15765 17 0 0 25 0 1 0 772783885 41459712 7030 4294967295 134512640 134714508 3221224592 3221222820 1077414363 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 10122 7030 1111 63 0 10059 0 vsize: 40488 [startup+171.369 s] Raw data (loadavg): 0.99 1.18 1.68 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 7594 0 6 0 16764 18 0 0 25 0 1 0 772783885 43384832 7524 4294967295 134512640 134714508 3221224592 3221222820 1077414383 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 10592 7524 1111 63 0 10529 0 vsize: 42368 [startup+181.37 s] Raw data (loadavg): 0.99 1.17 1.67 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 8086 0 6 0 17763 18 0 0 25 0 1 0 772783885 45490176 8016 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 11106 8016 1111 63 0 11043 0 vsize: 44424 [startup+191.371 s] Raw data (loadavg): 0.99 1.17 1.66 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 8604 0 6 0 18763 19 0 0 25 0 1 0 772783885 47710208 8534 4294967295 134512640 134714508 3221224592 3221222820 1077414358 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 11648 8534 1111 63 0 11585 0 vsize: 46592 [startup+201.372 s] Raw data (loadavg): 0.99 1.16 1.66 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 9136 0 6 0 19762 20 0 0 25 0 1 0 772783885 49774592 9066 4294967295 134512640 134714508 3221224592 3221222820 1077414413 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 12152 9066 1111 63 0 12089 0 vsize: 48608 [startup+211.375 s] Raw data (loadavg): 0.99 1.16 1.65 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 9680 0 6 0 20762 21 0 0 25 0 1 0 772783885 52006912 9610 4294967295 134512640 134714508 3221224592 3221222820 1077414385 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 12697 9610 1111 63 0 12634 0 vsize: 50788 [startup+221.375 s] Raw data (loadavg): 0.99 1.15 1.64 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 10257 0 6 0 21761 22 0 0 25 0 1 0 772783885 54415360 10187 4294967295 134512640 134714508 3221224592 3221222820 1077414435 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 13285 10187 1111 63 0 13222 0 vsize: 53140 [startup+231.375 s] Raw data (loadavg): 0.99 1.14 1.63 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 10831 0 6 0 22760 23 0 0 25 0 1 0 772783885 56819712 10761 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 13872 10761 1111 63 0 13809 0 vsize: 55488 [startup+241.391 s] Raw data (loadavg): 0.99 1.14 1.63 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 11466 0 6 0 23760 25 0 0 25 0 1 0 772783885 59379712 11396 4294967295 134512640 134714508 3221224592 3221222820 1077414388 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 14497 11396 1111 63 0 14434 0 vsize: 57988 [startup+251.391 s] Raw data (loadavg): 0.99 1.13 1.62 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 12130 0 6 0 24759 26 0 0 25 0 1 0 772783885 62091264 12060 4294967295 134512640 134714508 3221224592 3221222820 1077414401 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 15159 12060 1111 63 0 15096 0 vsize: 60636 [startup+261.391 s] Raw data (loadavg): 0.99 1.13 1.61 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 12852 0 6 0 25757 28 0 0 25 0 1 0 772783885 64946176 12782 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 15856 12782 1111 63 0 15793 0 vsize: 63424 [startup+271.392 s] Raw data (loadavg): 0.99 1.12 1.61 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 13607 0 6 0 26756 30 0 0 25 0 1 0 772783885 68112384 13537 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 16629 13537 1111 63 0 16566 0 vsize: 66516 [startup+281.392 s] Raw data (loadavg): 0.99 1.12 1.60 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 14386 0 6 0 27755 31 0 0 25 0 1 0 772783885 71266304 14316 4294967295 134512640 134714508 3221224592 3221222820 1077414385 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 17399 14316 1111 63 0 17336 0 vsize: 69596 [startup+291.393 s] Raw data (loadavg): 0.99 1.12 1.59 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 15214 0 6 0 28754 32 0 0 25 0 1 0 772783885 74698752 15144 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 18237 15144 1111 63 0 18174 0 vsize: 72948 [startup+301.393 s] Raw data (loadavg): 0.99 1.11 1.59 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 16069 0 6 0 29752 34 0 0 25 0 1 0 772783885 78163968 15999 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 19083 15999 1111 63 0 19020 0 vsize: 76332 [startup+311.393 s] Raw data (loadavg): 0.99 1.11 1.58 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 16987 0 6 0 30751 36 0 0 25 0 1 0 772783885 82104320 16917 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 20045 16917 1111 63 0 19982 0 vsize: 80180 [startup+321.393 s] Raw data (loadavg): 0.99 1.10 1.57 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 17929 0 6 0 31748 38 0 0 25 0 1 0 772783885 86016000 17859 4294967295 134512640 134714508 3221224592 3221223248 134527932 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 21000 17859 1111 63 0 20937 0 vsize: 84000 [startup+331.393 s] Raw data (loadavg): 0.99 1.10 1.56 2/54 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 18920 0 6 0 32747 40 0 0 25 0 1 0 772783885 90075136 18850 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 21991 18850 1111 63 0 21928 0 vsize: 87964 [startup+340.095 s] Raw data (loadavg): 0.99 1.10 1.56 1/53 3988 Raw data (stat): 3986 (bsolo_lpr_cuts) R 3985 3944 3943 0 -1 0 18920 0 6 0 32747 40 0 0 25 0 1 0 772783885 90075136 18850 4294967295 134512640 134714508 3221224592 3221223248 134527946 0 0 7 0 0 0 0 17 1 0 0 Raw data (statm): 21991 18850 1111 63 0 21928 0 vsize: 0 Child status: 0 Real time (s): 340.094 CPU time (s): 336.574 CPU user time (s): 336.086 CPU system time (s): 0.487925 CPU usage (%): 98.9649 Max. virtual memory (Kb): 87964 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####