Name | normalized-opb/mps-v2-20-10/ftp.netlib.org/lp/data/normalized-mps-v2-20-10-adlittle.opb |
MD5SUM | 1bb3cde4ae28db77cb8e051d278e83a5 |
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.030994 |
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 wulflinc5 THE 2005-05-25 04:34:04 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=10442 boxname=wulflinc5 idbench=804 idsolver=3 numberseed=0 MD5SUM SOLVER: 03a6a792daea978e4202f78851741568 /oldhome/oroussel/solvers/bsolo_mis MD5SUM BENCH: 1bb3cde4ae28db77cb8e051d278e83a5 /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-adlittle.opb REAL COMMAND: bsolo_mis /oldhome/oroussel/tmp/wulflinc5/normalized-mps-v2-20-10-adlittle.opb IDLAUNCH: 10442 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.007 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.007 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: 855084 kB Buffers: 10632 kB Cached: 147336 kB SwapCached: 472 kB Active: 23416 kB Inactive: 136588 kB HighTotal: 131008 kB HighFree: 26740 kB LowTotal: 903652 kB LowFree: 828344 kB SwapTotal: 2097136 kB SwapFree: 2095792 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5220 kB Slab: 13676 kB Committed_AS: 63600 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1364 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-05-25 04:34:06 (client local time) WITH STATUS 0 IN 1.50177 SECONDS stats: 10442 7 1.50177 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c ERROR Parsing file!!! c ERROR parsing line: -2530*V_0x2e__0x2e__0x2e_100_bit_10 -5060*V_0x2e__0x2e__0x2e_100_bit_9 -10120*V_0x2e__0x2e__0x2e_100_bit_8 -20240*V_0x2e__0x2e__0x2e_100_bit_7 -40480*V_0x2e__0x2e__0x2e_100_bit_6 -80960*V_0x2e__0x2e__0x2e_100_bit_5 -161920*V_0x2e__0x2e__0x2e_100_bit_4 -323840*V_0x2e__0x2e__0x2e_100_bit_3 -647680*V_0x2e__0x2e__0x2e_100_bit_2 -1295360*V_0x2e__0x2e__0x2e_100_bit_1 -2590720*V_0x2e__0x2e__0x2e_100_bit0 -5181440*V_0x2e__0x2e__0x2e_100_bit1 -10362880*V_0x2e__0x2e__0x2e_100_bit2 -20725760*V_0x2e__0x2e__0x2e_100_bit3 -41451520*V_0x2e__0x2e__0x2e_100_bit4 -82903040*V_0x2e__0x2e__0x2e_100_bit5 -165806080*V_0x2e__0x2e__0x2e_100_bit6 -331612160*V_0x2e__0x2e__0x2e_100_bit7 -663224320*V_0x2e__0x2e__0x2e_100_bit8 -1326448640*V_0x2e__0x2e__0x2e_100_bit9 -2652897280*V_0x2e__0x2e__0x2e_100_bit10 -5305794560*V_0x2e__0x2e__0x2e_100_bit11 -10611589120*V_0x2e__0x2e__0x2e_100_bit12 -21223178240*V_0x2e__0x2e__0x2e_100_bit13 -42446356480*V_0x2e__0x2e__0x2e_100_bit14 -84892712960*V_0x2e__0x2e__0x2e_100_bit15 -169785425920*V_0x2e__0x2e__0x2e_100_bit16 -339570851840*V_0x2e__0x2e__0x2e_100_bit17 -679141703680*V_0x2e__0x2e__0x2e_100_bit18 -1358283407360*V_0x2e__0x2e__0x2e_100_bit19 -3190*V_0x2e__0x2e__0x2e_101_bit_10 -6380*V_0x2e__0x2e__0x2e_101_bit_9 -12760*V_0x2e__0x2e__0x2e_101_bit_8 -25520*V_0x2e__0x2e__0x2e_101_bit_7 -51040*V_0x2e__0x2e__0x2e_101_bit_6 -102080*V_0x2e__0x2e__0x2e_101_bit_5 -204160*V_0x2e__0x2e__0x2e_101_bit_4 -408320*V_0x2e__0x2e__0x2e_101_bit_3 -816640*V_0x2e__0x2e__0x2e_101_bit_2 -1633280*V_0x2e__0x2e__0x2e_101_bit_1 -3266560*V_0x2e__0x2e__0x2e_101_bit0 -6533120*V_0x2e__0x2e__0x2e_101_bit1 -13066240*V_0x2e__0x2e__0x2e_101_bit2 -26132480*V_0x2e__0x2e__0x2e_101_bit3 -52264960*V_0x2e__0x2e__0x2e_101_bit4 -104529920*V_0x2e__0x2e__0x2e_101_bit5 -209059840*V_0x2e__0x2e__0x2e_101_bit6 -418119680*V_0x2e__0x2e__0x2e_101_bit7 -836239360*V_0x2e__0x2e__0x2e_101_bit8 -1672478720*V_0x2e__0x2e__0x2e_101_bit9 -3344957440*V_0x2e__0x2e__0x2e_101_bit10 -6689914880*V_0x2e__0x2e__0x2e_101_bit11 -13379829760*V_0x2e__0x2e__0x2e_101_bit12 -26759659520*V_0x2e__0x2e__0x2e_101_bit13 -53519319040*V_0x2e__0x2e__0x2e_101_bit14 -107038638080*V_0x2e__0x2e__0x2e_101_bit15 -214077276160*V_0x2e__0x2e__0x2e_101_bit16 -428154552320*V_0x2e__0x2e__0x2e_101_bit17 -856309104640*V_0x2e__0x2e__0x2e_101_bit18 -1712618209280*V_0x2e__0x2e__0x2e_101_bit19 +5000*V_0x2e__0x2e__0x2e_102_bit_10 +10000*V_0x2e__0x2e__0x2e_102_bit_9 +20000*V_0x2e__0x2e__0x2e_102_bit_8 +40000*V_0x2e__0x2e__0x2e_102_bit_7 +80000*V_0x2e__0x2e__0x2e_102_bit_6 +160000*V_0x2e__0x2e__0x2e_102_bit_5 +320000*V_0x2e__0x2e__0x2e_102_bit_4 +640000*V_0x2e__0x2e__0x2e_102_bit_3 +1280000*V_0x2e__0x2e__0x2e_102_bit_2 +2560000*V_0x2e__0x2e__0x2e_102_bit_1 +5120000*V_0x2e__0x2e__0x2e_102_bit0 +10240000*V_0x2e__0x2e__0x2e_102_bit1 +20480000*V_0x2e__0x2e__0x2e_102_bit2 +40960000*V_0x2e__0x2e__0x2e_102_bit3 +81920000*V_0x2e__0x2e__0x2e_102_bit4 +163840000*V_0x2e__0x2e__0x2e_102_bit5 +327680000*V_0x2e__0x2e__0x2e_102_bit6 +655360000*V_0x2e__0x2e__0x2e_102_bit7 +1310720000*V_0x2e__0x2e__0x2e_102_bit8 +2621440000*V_0x2e__0x2e__0x2e_102_bit9 +5242880000*V_0x2e__0x2e__0x2e_102_bit10 +10485760000*V_0x2e__0x2e__0x2e_102_bit11 +20971520000*V_0x2e__0x2e__0x2e_102_bit12 +41943040000*V_0x2e__0x2e__0x2e_102_bit13 +83886080000*V_0x2e__0x2e__0x2e_102_bit14 +167772160000*V_0x2e__0x2e__0x2e_102_bit15 +335544320000*V_0x2e__0x2e__0x2e_102_bit16 +671088640000*V_0x2e__0x2e__0x2e_102_bit17 +1342177280000*V_0x2e__0x2e__0x2e_102_bit18 +2684354560000*V_0x2e__0x2e__0x2e_102_bit19 +1235*V_0x2e__0x2e__0x2e_148_bit_10 +2470*V_0x2e__0x2e__0x2e_148_bit_9 +4940*V_0x2e__0x2e__0x2e_148_bit_8 +9880*V_0x2e__0x2e__0x2e_148_bit_7 +19760*V_0x2e__0x2e__0x2e_148_bit_6 +39520*V_0x2e__0x2e__0x2e_148_bit_5 +79040*V_0x2e__0x2e__0x2e_148_bit_4 +158080*V_0x2e__0x2e__0x2e_148_bit_3 +316160*V_0x2e__0x2e__0x2e_148_bit_2 +632320*V_0x2e__0x2e__0x2e_148_bit_1 +1264640*V_0x2e__0x2e__0x2e_148_bit0 +2529280*V_0x2e__0x2e__0x2e_148_bit1 +5058560*V_0x2e__0x2e__0x2e_148_bit2 +10117120*V_0x2e__0x2e__0x2e_148_bit3 +20234240*V_0x2e__0x2e__0x2e_148_bit4 +40468480*V_0x2e__0x2e__0x2e_148_bit5 +80936960*V_0x2e__0x2e__0x2e_148_bit6 +161873920*V_0x2e__0x2e__0x2e_148_bit7 +323747840*V_0x2e__0x2e__0x2e_148_bit8 +647495680*V_0x2e__0x2e__0x2e_148_bit9 +1294991360*V_0x2e__0x2e__0x2e_148_bit10 +2589982720*V_0x2e__0x2e__0x2e_148_bit11 +5179965440*V_0x2e__0x2e__0x2e_148_bit12 +10359930880*V_0x2e__0x2e__0x2e_148_bit13 +20719861760*V_0x2e__0x2e__0x2e_148_bit14 +41439723520*V_0x2e__0x2e__0x2e_148_bit15 +82879447040*V_0x2e__0x2e__0x2e_148_bit16 +165758894080*V_0x2e__0x2e__0x2e_148_bit17 +331517788160*V_0x2e__0x2e__0x2e_148_bit18 +663035576320*V_0x2e__0x2e__0x2e_148_bit19 +785*V_0x2e__0x2e__0x2e_149_bit_10 +1570*V_0x2e__0x2e__0x2e_149_bit_9 +3140*V_0x2e__0x2e__0x2e_149_bit_8 +6280*V_0x2e__0x2e__0x2e_149_bit_7 +12560*V_0x2e__0x2e__0x2e_149_bit_6 +25120*V_0x2e__0x2e__0x2e_149_bit_5 +50240*V_0x2e__0x2e__0x2e_149_bit_4 +100480*V_0x2e__0x2e__0x2e_149_bit_3 +200960*V_0x2e__0x2e__0x2e_149_bit_2 +401920*V_0x2e__0x2e__0x2e_149_bit_1 +803840*V_0x2e__0x2e__0x2e_149_bit0 +1607680*V_0x2e__0x2e__0x2e_149_bit1 +3215360*V_0x2e__0x2e__0x2e_149_bit2 +6430720*V_0x2e__0x2e__0x2e_149_bit3 +12861440*V_0x2e__0x2e__0x2e_149_bit4 +25722880*V_0x2e__0x2e__0x2e_149_bit5 +51445760*V_0x2e__0x2e__0x2e_149_bit6 +102891520*V_0x2e__0x2e__0x2e_149_bit7 +205783040*V_0x2e__0x2e__0x2e_149_bit8 +411566080*V_0x2e__0x2e__0x2e_149_bit9 +823132160*V_0x2e__0x2e__0x2e_149_bit10 +1646264320*V_0x2e__0x2e__0x2e_149_bit11 +3292528640*V_0x2e__0x2e__0x2e_149_bit12 +6585057280*V_0x2e__0x2e__0x2e_149_bit13 +13170114560*V_0x2e__0x2e__0x2e_149_bit14 +26340229120*V_0x2e__0x2e__0x2e_149_bit15 +52680458240*V_0x2e__0x2e__0x2e_149_bit16 +105360916480*V_0x2e__0x2e__0x2e_149_bit17 +210721832960*V_0x2e__0x2e__0x2e_149_bit18 +421443665920*V_0x2e__0x2e__0x2e_149_bit19 +785*V_0x2e__0x2e__0x2e_150_bit_10 +1570*V_0x2e__0x2e__0x2e_150_bit_9 +3140*V_0x2e__0x2e__0x2e_150_bit_8 +6280*V_0x2e__0x2e__0x2e_150_bit_7 +12560*V_0x2e__0x2e__0x2e_150_bit_6 +25120*V_0x2e__0x2e__0x2e_150_bit_5 +50240*V_0x2e__0x2e__0x2e_150_bit_4 +100480*V_0x2e__0x2e__0x2e_150_bit_3 +200960*V_0x2e__0x2e__0x2e_150_bit_2 +401920*V_0x2e__0x2e__0x2e_150_bit_1 +803840*V_0x2e__0x2e__0x2e_150_bit0 +1607680*V_0x2e__0x2e__0x2e_150_bit1 +3215360*V_0x2e__0x2e__0x2e_150_bit2 +6430720*V_0x2e__0x2e__0x2e_150_bit3 +12861440*V_0x2e__0x2e__0x2e_150_bit4 +25722880*V_0x2e__0x2e__0x2e_150_bit5 +51445760*V_0x2e__0x2e__0x2e_150_bit6 +102891520*V_0x2e__0x2e__0x2e_150_bit7 +205783040*V_0x2e__0x2e__0x2e_150_bit8 +411566080*V_0x2e__0x2e__0x2e_150_bit9 +823132160*V_0x2e__0x2e__0x2e_150_bit10 +1646264320*V_0x2e__0x2e__0x2e_150_bit11 +3292528640*V_0x2e__0x2e__0x2e_150_bit12 +6585057280*V_0x2e__0x2e__0x2e_150_bit13 +13170114560*V_0x2e__0x2e__0x2e_150_bit14 +26340229120*V_0x2e__0x2e__0x2e_150_bit15 +52680458240*V_0x2e__0x2e__0x2e_150_bit16 +105360916480*V_0x2e__0x2e__0x2e_150_bit17 +210721832960*V_0x2e__0x2e__0x2e_150_bit18 +421443665920*V_0x2e__0x2e__0x2e_150_bit19 -1000*V_0x2e__0x2e__0x2e_155_bit_10 -2000*V_0x2e__0x2e__0x2e_155_bit_9 -4000*V_0x2e__0x2e__0x2e_155_bit_8 -8000*V_0x2e__0x2e__0x2e_155_bit_7 -16000*V_0x2e__0x2e__0x2e_155_bit_6 -32000*V_0x2e__0x2e__0x2e_155_bit_5 -64000*V_0x2e__0x2e__0x2e_155_bit_4 -128000*V_0x2e__0x2e__0x2e_155_bit_3 -256000*V_0x2e__0x2e__0x2e_155_bit_2 -512000*V_0x2e__0x2e__0x2e_155_bit_1 -1024000*V_0x2e__0x2e__0x2e_155_bit0 -2048000*V_0x2e__0x2e__0x2e_155_bit1 -4096000*V_0x2e__0x2e__0x2e_155_bit2 -8192000*V_0x2e__0x2e__0x2e_155_bit3 -16384000*V_0x2e__0x2e__0x2e_155_bit4 -32768000*V_0x2e__0x2e__0x2e_155_bit5 -65536000*V_0x2e__0x2e__0x2e_155_bit6 -131072000*V_0x2e__0x2e__0x2e_155_bit7 -262144000*V_0x2e__0x2e__0x2e_155_bit8 -524288000*V_0x2e__0x2e__0x2e_155_bit9 -1048576000*V_0x2e__0x2e__0x2e_155_bit10 -2097152000*V_0x2e__0x2e__0x2e_155_bit11 -4194304000*V_0x2e__0x2e__0x2e_155_bit12 -8388608000*V_0x2e__0x2e__0x2e_155_bit13 -16777216000*V_0x2e__0x2e__0x2e_155_bit14 -33554432000*V_0x2e__0x2e__0x2e_155_bit15 -67108864000*V_0x2e__0x2e__0x2e_155_bit16 -134217728000*V_0x2e__0x2e__0x2e_155_bit17 -268435456000*V_0x2e__0x2e__0x2e_155_bit18 -536870912000*V_0x2e__0x2e__0x2e_155_bit19 +9*V_0x2e__0x2e__0x2e_160_bit_10 +18*V_0x2e__0x2e__0x2e_160_bit_9 +36*V_0x2e__0x2e__0x2e_160_bit_8 +72*V_0x2e__0x2e__0x2e_160_bit_7 +144*V_0x2e__0x2e__0x2e_160_bit_6 +288*V_0x2e__0x2e__0x2e_160_bit_5 +576*V_0x2e__0x2e__0x2e_160_bit_4 +1152*V_0x2e__0x2e__0x2e_160_bit_3 +2304*V_0x2e__0x2e__0x2e_160_bit_2 +4608*V_0x2e__0x2e__0x2e_160_bit_1 +9216*V_0x2e__0x2e__0x2e_160_bit0 +18432*V_0x2e__0x2e__0x2e_160_bit1 +36864*V_0x2e__0x2e__0x2e_160_bit2 +73728*V_0x2e__0x2e__0x2e_160_bit3 +147456*V_0x2e__0x2e__0x2e_160_bit4 +294912*V_0x2e__0x2e__0x2e_160_bit5 +589824*V_0x2e__0x2e__0x2e_160_bit6 +1179648*V_0x2e__0x2e__0x2e_160_bit7 +2359296*V_0x2e__0x2e__0x2e_160_bit8 +4718592*V_0x2e__0x2e__0x2e_160_bit9 +9437184*V_0x2e__0x2e__0x2e_160_bit10 +18874368*V_0x2e__0x2e__0x2e_160_bit11 +37748736*V_0x2e__0x2e__0x2e_160_bit12 +75497472*V_0x2e__0x2e__0x2e_160_bit13 +150994944*V_0x2e__0x2e__0x2e_160_bit14 +301989888*V_0x2e__0x2e__0x2e_160_bit15 +603979776*V_0x2e__0x2e__0x2e_160_bit16 +1207959552*V_0x2e__0x2e__0x2e_160_bit17 +2415919104*V_0x2e__0x2e__0x2e_160_bit18 +4831838208*V_0x2e__0x2e__0x2e_160_bit19 +9*V_0x2e__0x2e__0x2e_161_bit_10 +18*V_0x2e__0x2e__0x2e_161_bit_9 +36*V_0x2e__0x2e__0x2e_161_bit_8 +72*V_0x2e__0x2e__0x2e_161_bit_7 +144*V_0x2e__0x2e__0x2e_161_bit_6 +288*V_0x2e__0x2e__0x2e_161_bit_5 +576*V_0x2e__0x2e__0x2e_161_bit_4 +1152*V_0x2e__0x2e__0x2e_161_bit_3 +2304*V_0x2e__0x2e__0x2e_161_bit_2 +4608*V_0x2e__0x2e__0x2e_161_bit_1 +9216*V_0x2e__0x2e__0x2e_161_bit0 +18432*V_0x2e__0x2e__0x2e_161_bit1 +36864*V_0x2e__0x2e__0x2e_161_bit2 +73728*V_0x2e__0x2e__0x2e_161_bit3 +147456*V_0x2e__0x2e__0x2e_161_bit4 +294912*V_0x2e__0x2e__0x2e_161_bit5 +589824*V_0x2e__0x2e__0x2e_161_bit6 +1179648*V_0x2e__0x2e__0x2e_161_bit7 +2359296*V_0x2e__0x2e__0x2e_161_bit8 +4718592*V_0x2e__0x2e__0x2e_161_bit9 +9437184*V_0x2e__0x2e__0x2e_161_bit10 +18874368*V_0x2e__0x2e__0x2e_161_bit11 +37748736*V_0x2e__0x2e__0x2e_161_bit12 +75497472*V_0x2e__0x2e__0x2e_161_bit13 +150994944*V_0x2e__0x2e__0x2e_161_bit14 +301989888*V_0x2e__0x2e__0x2e_161_bit15 +603979776*V_0x2e__0x2e__0x2e_161_bit16 +1207959552*V_0x2e__0x2e__0x2e_161_bit17 +2415919104*V_0x2e__0x2e__0x2e_161_bit18 +4831838208*V_0x2e__0x2e__0x2e_161_bit19 +5*V_0x2e__0x2e__0x2e_176_bit_10 +10*V_0x2e__0x2e__0x2e_176_bit_9 +20*V_0x2e__0x2e__0x2e_176_bit_8 +40*V_0x2e__0x2e__0x2e_176_bit_7 +80*V_0x2e__0x2e__0x2e_176_bit_6 +160*V_0x2e__0x2e__0x2e_176_bit_5 +320*V_0x2e__0x2e__0x2e_176_bit_4 +640*V_0x2e__0x2e__0x2e_176_bit_3 +1280*V_0x2e__0x2e__0x2e_176_bit_2 +2560*V_0x2e__0x2e__0x2e_176_bit_1 +5120*V_0x2e__0x2e__0x2e_176_bit0 +10240*V_0x2e__0x2e__0x2e_176_bit1 +20480*V_0x2e__0x2e__0x2e_176_bit2 +40960*V_0x2e__0x2e__0x2e_176_bit3 +81920*V_0x2e__0x2e__0x2e_176_bit4 +163840*V_0x2e__0x2e__0x2e_176_bit5 +327680*V_0x2e__0x2e__0x2e_176_bit6 +655360*V_0x2e__0x2e__0x2e_176_bit7 +1310720*V_0x2e__0x2e__0x2e_176_bit8 +2621440*V_0x2e__0x2e__0x2e_176_bit9 +5242880*V_0x2e__0x2e__0x2e_176_bit10 +10485760*V_0x2e__0x2e__0x2e_176_bit11 +20971520*V_0x2e__0x2e__0x2e_176_bit12 +41943040*V_0x2e__0x2e__0x2e_176_bit13 +83886080*V_0x2e__0x2e__0x2e_176_bit14 +167772160*V_0x2e__0x2e__0x2e_176_bit15 +335544320*V_0x2e__0x2e__0x2e_176_bit16 +671088640*V_0x2e__0x2e__0x2e_176_bit17 +1342177280*V_0x2e__0x2e__0x2e_176_bit18 +2684354560*V_0x2e__0x2e__0x2e_176_bit19 +5*V_0x2e__0x2e__0x2e_177_bit_10 +10*V_0x2e__0x2e__0x2e_177_bit_9 +20*V_0x2e__0x2e__0x2e_177_bit_8 +40*V_0x2e__0x2e__0x2e_177_bit_7 +80*V_0x2e__0x2e__0x2e_177_bit_6 +160*V_0x2e__0x2e__0x2e_177_bit_5 +320*V_0x2e__0x2e__0x2e_177_bit_4 +640*V_0x2e__0x2e__0x2e_177_bit_3 +1280*V_0x2e__0x2e__0x2e_177_bit_2 +2560*V_0x2e__0x2e__0x2e_177_bit_1 +5120*V_0x2e__0x2e__0x2e_177_bit0 +10240*V_0x2e__0x2e__0x2e_177_bit1 +20480*V_0x2e__0x2e__0x2e_177_bit2 +40960*V_0x2e__0x2e__0x2e_177_bit3 +81920*V_0x2e__0x2e__0x2e_177_bit4 +163840*V_0x2e__0x2e__0x2e_177_bit5 +327680*V_0x2e__0x2e__0x2e_177_bit6 +655360*V_0x2e__0x2e__0x2e_177_bit7 +1310720*V_0x2e__0x2e__0x2e_177_bit8 +2621440*V_0x2e__0x2e__0x2e_177_bit9 +5242880*V_0x2e__0x2e__0x2e_177_bit10 +10485760*V_0x2e__0x2e__0x2e_177_bit11 +20971520*V_0x2e__0x2e__0x2e_177_bit12 +41943040*V_0x2e__0x2e__0x2e_177_bit13 +83886080*V_0x2e__0x2e__0x2e_177_bit14 +167772160*V_0x2e__0x2e__0x2e_177_bit15 +335544320*V_0x2e__0x2e__0x2e_177_bit16 +671088640*V_0x2e__0x2e__0x2e_177_bit17 +1342177280*V_0x2e__0x2e__0x2e_177_bit18 +2684354560*V_0x2e__0x2e__0x2e_177_bit19 >= +0; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc5/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.58 0.82 0.86 2/54 19422 Raw data (stat): 19422 (runsolver) R 19421 7266 7265 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 777812491 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 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+1.51213 s] Raw data (loadavg): 0.58 0.82 0.86 1/53 19422 Raw data (stat): 19422 (runsolver) R 19421 7266 7265 0 -1 64 4 0 0 0 0 0 0 0 19 0 1 0 777812491 1052672 99 4294967295 134512640 135381576 3221224496 3221219712 135158418 0 2147483391 7 90112 0 0 0 17 1 0 0 Raw data (statm): 257 99 215 215 0 42 0 vsize: 0 Child status: 0 Real time (s): 1.51182 CPU time (s): 1.50177 CPU user time (s): 1.45878 CPU system time (s): 0.042993 CPU usage (%): 99.335 Max. virtual memory (Kb): 1028 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####