Name | normalized-opb/mps-v2-13-7/ftp.netlib.org/lp/data/normalized-mps-v2-13-7-standata.opb |
MD5SUM | d5b771efe8f3bc863eeca85beb6d9cd6 |
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 | 140 |
Biggest coefficient in the objective function | 52428800 |
Number of bits for the biggest coefficient in the objective function | 26 |
Sum of the numbers in the objective function | 318766800 |
Number of bits of the sum of numbers in the objective function | 29 |
Biggest number in a constraint | 75573493760 |
Number of bits of the biggest number in a constraint | 37 |
Biggest sum of numbers in a constraint | 2374370081400 |
Number of bits of the biggest sum of numbers | 42 |
Best result obtained on this benchmark | UNSAT |
Best CPU time to get the best result obtained on this benchmark | 1.05684 |
Number of variables | 20142 |
Total number of constraints | 462 |
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 | 462 |
Minimum length of a constraint | 8 |
Maximum length of a constraint | 14900 |
#### BEGIN LAUNCHER DATA #### LAUNCH ON wulflinc3 THE 2005-06-09 12:13:35 (client local time) PB2005-SCRIPT v4.0 MARKUPS: idlaunch=29486 boxname=wulflinc3 idbench=1270 idsolver=21 numberseed=0 MD5SUM SOLVER: 174a32271cb3bba0a277d6d7724e60fb /oldhome/oroussel/solvers/bsolo_lpr_cuts-v2 MD5SUM BENCH: d5b771efe8f3bc863eeca85beb6d9cd6 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-standata.opb REAL COMMAND: bsolo_lpr_cuts-v2 /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-standata.opb IDLAUNCH: 29486 /proc/cpuinfo: processor : 0 vendor_id : GenuineIntel cpu family : 6 model : 7 model name : Pentium III (Katmai) stepping : 2 cpu MHz : 451.190 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.190 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: 714168 kB Buffers: 21808 kB Cached: 278248 kB SwapCached: 708 kB Active: 34220 kB Inactive: 267864 kB HighTotal: 131008 kB HighFree: 252 kB LowTotal: 903652 kB LowFree: 713916 kB SwapTotal: 2097136 kB SwapFree: 2095380 kB Dirty: 28 kB Writeback: 0 kB Mapped: 5036 kB Slab: 12704 kB Committed_AS: 71792 kB PageTables: 316 kB VmallocTotal: 114680 kB VmallocUsed: 1388 kB VmallocChunk: 113256 kB JOB ENDED THE 2005-06-09 12:13:39 (client local time) WITH STATUS 0 IN 3.86041 SECONDS stats: 29486 7 3.86041 0 #### END LAUNCHER DATA #### #### BEGIN SOLVER DATA #### c INFO: OSL Context initialized. c ERROR Parsing file!!! c ERROR parsing line: +144145*CIN1_0x2e__0x2e_T1_bit_7 +288290*CIN1_0x2e__0x2e_T1_bit_6 +576580*CIN1_0x2e__0x2e_T1_bit_5 +1153160*CIN1_0x2e__0x2e_T1_bit_4 +2306320*CIN1_0x2e__0x2e_T1_bit_3 +4612640*CIN1_0x2e__0x2e_T1_bit_2 +9225280*CIN1_0x2e__0x2e_T1_bit_1 +18450560*CIN1_0x2e__0x2e_T1_bit0 +36901120*CIN1_0x2e__0x2e_T1_bit1 +73802240*CIN1_0x2e__0x2e_T1_bit2 +147604480*CIN1_0x2e__0x2e_T1_bit3 +295208960*CIN1_0x2e__0x2e_T1_bit4 +590417920*CIN1_0x2e__0x2e_T1_bit5 +1180835840*CIN1_0x2e__0x2e_T1_bit6 +2361671680*CIN1_0x2e__0x2e_T1_bit7 +4723343360*CIN1_0x2e__0x2e_T1_bit8 +9446686720*CIN1_0x2e__0x2e_T1_bit9 +18893373440*CIN1_0x2e__0x2e_T1_bit10 +37786746880*CIN1_0x2e__0x2e_T1_bit11 +75573493760*CIN1_0x2e__0x2e_T1_bit12 +125304*CVA1_0x2e__0x2e_T1_bit_7 +250608*CVA1_0x2e__0x2e_T1_bit_6 +501216*CVA1_0x2e__0x2e_T1_bit_5 +1002432*CVA1_0x2e__0x2e_T1_bit_4 +2004864*CVA1_0x2e__0x2e_T1_bit_3 +4009728*CVA1_0x2e__0x2e_T1_bit_2 +8019456*CVA1_0x2e__0x2e_T1_bit_1 +16038912*CVA1_0x2e__0x2e_T1_bit0 +32077824*CVA1_0x2e__0x2e_T1_bit1 +64155648*CVA1_0x2e__0x2e_T1_bit2 +128311296*CVA1_0x2e__0x2e_T1_bit3 +256622592*CVA1_0x2e__0x2e_T1_bit4 +513245184*CVA1_0x2e__0x2e_T1_bit5 +1026490368*CVA1_0x2e__0x2e_T1_bit6 +2052980736*CVA1_0x2e__0x2e_T1_bit7 +4105961472*CVA1_0x2e__0x2e_T1_bit8 +8211922944*CVA1_0x2e__0x2e_T1_bit9 +16423845888*CVA1_0x2e__0x2e_T1_bit10 +32847691776*CVA1_0x2e__0x2e_T1_bit11 +65695383552*CVA1_0x2e__0x2e_T1_bit12 +101600*CIN3_0x2e__0x2e_T1_bit_7 +203200*CIN3_0x2e__0x2e_T1_bit_6 +406400*CIN3_0x2e__0x2e_T1_bit_5 +812800*CIN3_0x2e__0x2e_T1_bit_4 +1625600*CIN3_0x2e__0x2e_T1_bit_3 +3251200*CIN3_0x2e__0x2e_T1_bit_2 +6502400*CIN3_0x2e__0x2e_T1_bit_1 +13004800*CIN3_0x2e__0x2e_T1_bit0 +26009600*CIN3_0x2e__0x2e_T1_bit1 +52019200*CIN3_0x2e__0x2e_T1_bit2 +104038400*CIN3_0x2e__0x2e_T1_bit3 +208076800*CIN3_0x2e__0x2e_T1_bit4 +416153600*CIN3_0x2e__0x2e_T1_bit5 +832307200*CIN3_0x2e__0x2e_T1_bit6 +1664614400*CIN3_0x2e__0x2e_T1_bit7 +3329228800*CIN3_0x2e__0x2e_T1_bit8 +6658457600*CIN3_0x2e__0x2e_T1_bit9 +13316915200*CIN3_0x2e__0x2e_T1_bit10 +26633830400*CIN3_0x2e__0x2e_T1_bit11 +53267660800*CIN3_0x2e__0x2e_T1_bit12 +88320*CVA3_0x2e__0x2e_T1_bit_7 +176640*CVA3_0x2e__0x2e_T1_bit_6 +353280*CVA3_0x2e__0x2e_T1_bit_5 +706560*CVA3_0x2e__0x2e_T1_bit_4 +1413120*CVA3_0x2e__0x2e_T1_bit_3 +2826240*CVA3_0x2e__0x2e_T1_bit_2 +5652480*CVA3_0x2e__0x2e_T1_bit_1 +11304960*CVA3_0x2e__0x2e_T1_bit0 +22609920*CVA3_0x2e__0x2e_T1_bit1 +45219840*CVA3_0x2e__0x2e_T1_bit2 +90439680*CVA3_0x2e__0x2e_T1_bit3 +180879360*CVA3_0x2e__0x2e_T1_bit4 +361758720*CVA3_0x2e__0x2e_T1_bit5 +723517440*CVA3_0x2e__0x2e_T1_bit6 +1447034880*CVA3_0x2e__0x2e_T1_bit7 +2894069760*CVA3_0x2e__0x2e_T1_bit8 +5788139520*CVA3_0x2e__0x2e_T1_bit9 +11576279040*CVA3_0x2e__0x2e_T1_bit10 +23152558080*CVA3_0x2e__0x2e_T1_bit11 +46305116160*CVA3_0x2e__0x2e_T1_bit12 +53975*CIN5_0x2e__0x2e_T1_bit_7 +107950*CIN5_0x2e__0x2e_T1_bit_6 +215900*CIN5_0x2e__0x2e_T1_bit_5 +431800*CIN5_0x2e__0x2e_T1_bit_4 +863600*CIN5_0x2e__0x2e_T1_bit_3 +1727200*CIN5_0x2e__0x2e_T1_bit_2 +3454400*CIN5_0x2e__0x2e_T1_bit_1 +6908800*CIN5_0x2e__0x2e_T1_bit0 +13817600*CIN5_0x2e__0x2e_T1_bit1 +27635200*CIN5_0x2e__0x2e_T1_bit2 +55270400*CIN5_0x2e__0x2e_T1_bit3 +110540800*CIN5_0x2e__0x2e_T1_bit4 +221081600*CIN5_0x2e__0x2e_T1_bit5 +442163200*CIN5_0x2e__0x2e_T1_bit6 +884326400*CIN5_0x2e__0x2e_T1_bit7 +1768652800*CIN5_0x2e__0x2e_T1_bit8 +3537305600*CIN5_0x2e__0x2e_T1_bit9 +7074611200*CIN5_0x2e__0x2e_T1_bit10 +14149222400*CIN5_0x2e__0x2e_T1_bit11 +28298444800*CIN5_0x2e__0x2e_T1_bit12 +46920*CVA5_0x2e__0x2e_T1_bit_7 +93840*CVA5_0x2e__0x2e_T1_bit_6 +187680*CVA5_0x2e__0x2e_T1_bit_5 +375360*CVA5_0x2e__0x2e_T1_bit_4 +750720*CVA5_0x2e__0x2e_T1_bit_3 +1501440*CVA5_0x2e__0x2e_T1_bit_2 +3002880*CVA5_0x2e__0x2e_T1_bit_1 +6005760*CVA5_0x2e__0x2e_T1_bit0 +12011520*CVA5_0x2e__0x2e_T1_bit1 +24023040*CVA5_0x2e__0x2e_T1_bit2 +48046080*CVA5_0x2e__0x2e_T1_bit3 +96092160*CVA5_0x2e__0x2e_T1_bit4 +192184320*CVA5_0x2e__0x2e_T1_bit5 +384368640*CVA5_0x2e__0x2e_T1_bit6 +768737280*CVA5_0x2e__0x2e_T1_bit7 +1537474560*CVA5_0x2e__0x2e_T1_bit8 +3074949120*CVA5_0x2e__0x2e_T1_bit9 +6149898240*CVA5_0x2e__0x2e_T1_bit10 +12299796480*CVA5_0x2e__0x2e_T1_bit11 +24599592960*CVA5_0x2e__0x2e_T1_bit12 +144145*CIN1_0x2e__0x2e_T2_bit_7 +288290*CIN1_0x2e__0x2e_T2_bit_6 +576580*CIN1_0x2e__0x2e_T2_bit_5 +1153160*CIN1_0x2e__0x2e_T2_bit_4 +2306320*CIN1_0x2e__0x2e_T2_bit_3 +4612640*CIN1_0x2e__0x2e_T2_bit_2 +9225280*CIN1_0x2e__0x2e_T2_bit_1 +18450560*CIN1_0x2e__0x2e_T2_bit0 +36901120*CIN1_0x2e__0x2e_T2_bit1 +73802240*CIN1_0x2e__0x2e_T2_bit2 +147604480*CIN1_0x2e__0x2e_T2_bit3 +295208960*CIN1_0x2e__0x2e_T2_bit4 +590417920*CIN1_0x2e__0x2e_T2_bit5 +1180835840*CIN1_0x2e__0x2e_T2_bit6 +2361671680*CIN1_0x2e__0x2e_T2_bit7 +4723343360*CIN1_0x2e__0x2e_T2_bit8 +9446686720*CIN1_0x2e__0x2e_T2_bit9 +18893373440*CIN1_0x2e__0x2e_T2_bit10 +37786746880*CIN1_0x2e__0x2e_T2_bit11 +75573493760*CIN1_0x2e__0x2e_T2_bit12 +125304*CVA1_0x2e__0x2e_T2_bit_7 +250608*CVA1_0x2e__0x2e_T2_bit_6 +501216*CVA1_0x2e__0x2e_T2_bit_5 +1002432*CVA1_0x2e__0x2e_T2_bit_4 +2004864*CVA1_0x2e__0x2e_T2_bit_3 +4009728*CVA1_0x2e__0x2e_T2_bit_2 +8019456*CVA1_0x2e__0x2e_T2_bit_1 +16038912*CVA1_0x2e__0x2e_T2_bit0 +32077824*CVA1_0x2e__0x2e_T2_bit1 +64155648*CVA1_0x2e__0x2e_T2_bit2 +128311296*CVA1_0x2e__0x2e_T2_bit3 +256622592*CVA1_0x2e__0x2e_T2_bit4 +513245184*CVA1_0x2e__0x2e_T2_bit5 +1026490368*CVA1_0x2e__0x2e_T2_bit6 +2052980736*CVA1_0x2e__0x2e_T2_bit7 +4105961472*CVA1_0x2e__0x2e_T2_bit8 +8211922944*CVA1_0x2e__0x2e_T2_bit9 +16423845888*CVA1_0x2e__0x2e_T2_bit10 +32847691776*CVA1_0x2e__0x2e_T2_bit11 +65695383552*CVA1_0x2e__0x2e_T2_bit12 +101600*CIN3_0x2e__0x2e_T2_bit_7 +203200*CIN3_0x2e__0x2e_T2_bit_6 +406400*CIN3_0x2e__0x2e_T2_bit_5 +812800*CIN3_0x2e__0x2e_T2_bit_4 +1625600*CIN3_0x2e__0x2e_T2_bit_3 +3251200*CIN3_0x2e__0x2e_T2_bit_2 +6502400*CIN3_0x2e__0x2e_T2_bit_1 +13004800*CIN3_0x2e__0x2e_T2_bit0 +26009600*CIN3_0x2e__0x2e_T2_bit1 +52019200*CIN3_0x2e__0x2e_T2_bit2 +104038400*CIN3_0x2e__0x2e_T2_bit3 +208076800*CIN3_0x2e__0x2e_T2_bit4 +416153600*CIN3_0x2e__0x2e_T2_bit5 +832307200*CIN3_0x2e__0x2e_T2_bit6 +1664614400*CIN3_0x2e__0x2e_T2_bit7 +3329228800*CIN3_0x2e__0x2e_T2_bit8 +6658457600*CIN3_0x2e__0x2e_T2_bit9 +13316915200*CIN3_0x2e__0x2e_T2_bit10 +26633830400*CIN3_0x2e__0x2e_T2_bit11 +53267660800*CIN3_0x2e__0x2e_T2_bit12 +88320*CVA3_0x2e__0x2e_T2_bit_7 +176640*CVA3_0x2e__0x2e_T2_bit_6 +353280*CVA3_0x2e__0x2e_T2_bit_5 +706560*CVA3_0x2e__0x2e_T2_bit_4 +1413120*CVA3_0x2e__0x2e_T2_bit_3 +2826240*CVA3_0x2e__0x2e_T2_bit_2 +5652480*CVA3_0x2e__0x2e_T2_bit_1 +11304960*CVA3_0x2e__0x2e_T2_bit0 +22609920*CVA3_0x2e__0x2e_T2_bit1 +45219840*CVA3_0x2e__0x2e_T2_bit2 +90439680*CVA3_0x2e__0x2e_T2_bit3 +180879360*CVA3_0x2e__0x2e_T2_bit4 +361758720*CVA3_0x2e__0x2e_T2_bit5 +723517440*CVA3_0x2e__0x2e_T2_bit6 +1447034880*CVA3_0x2e__0x2e_T2_bit7 +2894069760*CVA3_0x2e__0x2e_T2_bit8 +5788139520*CVA3_0x2e__0x2e_T2_bit9 +11576279040*CVA3_0x2e__0x2e_T2_bit10 +23152558080*CVA3_0x2e__0x2e_T2_bit11 +46305116160*CVA3_0x2e__0x2e_T2_bit12 +53975*CIN5_0x2e__0x2e_T2_bit_7 +107950*CIN5_0x2e__0x2e_T2_bit_6 +215900*CIN5_0x2e__0x2e_T2_bit_5 +431800*CIN5_0x2e__0x2e_T2_bit_4 +863600*CIN5_0x2e__0x2e_T2_bit_3 +1727200*CIN5_0x2e__0x2e_T2_bit_2 +3454400*CIN5_0x2e__0x2e_T2_bit_1 +6908800*CIN5_0x2e__0x2e_T2_bit0 +13817600*CIN5_0x2e__0x2e_T2_bit1 +27635200*CIN5_0x2e__0x2e_T2_bit2 +55270400*CIN5_0x2e__0x2e_T2_bit3 +110540800*CIN5_0x2e__0x2e_T2_bit4 +221081600*CIN5_0x2e__0x2e_T2_bit5 +442163200*CIN5_0x2e__0x2e_T2_bit6 +884326400*CIN5_0x2e__0x2e_T2_bit7 +1768652800*CIN5_0x2e__0x2e_T2_bit8 +3537305600*CIN5_0x2e__0x2e_T2_bit9 +7074611200*CIN5_0x2e__0x2e_T2_bit10 +14149222400*CIN5_0x2e__0x2e_T2_bit11 +28298444800*CIN5_0x2e__0x2e_T2_bit12 +46920*CVA5_0x2e__0x2e_T2_bit_7 +93840*CVA5_0x2e__0x2e_T2_bit_6 +187680*CVA5_0x2e__0x2e_T2_bit_5 +375360*CVA5_0x2e__0x2e_T2_bit_4 +750720*CVA5_0x2e__0x2e_T2_bit_3 +1501440*CVA5_0x2e__0x2e_T2_bit_2 +3002880*CVA5_0x2e__0x2e_T2_bit_1 +6005760*CVA5_0x2e__0x2e_T2_bit0 +12011520*CVA5_0x2e__0x2e_T2_bit1 +24023040*CVA5_0x2e__0x2e_T2_bit2 +48046080*CVA5_0x2e__0x2e_T2_bit3 +96092160*CVA5_0x2e__0x2e_T2_bit4 +192184320*CVA5_0x2e__0x2e_T2_bit5 +384368640*CVA5_0x2e__0x2e_T2_bit6 +768737280*CVA5_0x2e__0x2e_T2_bit7 +1537474560*CVA5_0x2e__0x2e_T2_bit8 +3074949120*CVA5_0x2e__0x2e_T2_bit9 +6149898240*CVA5_0x2e__0x2e_T2_bit10 +12299796480*CVA5_0x2e__0x2e_T2_bit11 +24599592960*CVA5_0x2e__0x2e_T2_bit12 +144145*CIN1_0x2e__0x2e_T3_bit_7 +288290*CIN1_0x2e__0x2e_T3_bit_6 +576580*CIN1_0x2e__0x2e_T3_bit_5 +1153160*CIN1_0x2e__0x2e_T3_bit_4 +2306320*CIN1_0x2e__0x2e_T3_bit_3 +4612640*CIN1_0x2e__0x2e_T3_bit_2 +9225280*CIN1_0x2e__0x2e_T3_bit_1 +18450560*CIN1_0x2e__0x2e_T3_bit0 +36901120*CIN1_0x2e__0x2e_T3_bit1 +73802240*CIN1_0x2e__0x2e_T3_bit2 +147604480*CIN1_0x2e__0x2e_T3_bit3 +295208960*CIN1_0x2e__0x2e_T3_bit4 +590417920*CIN1_0x2e__0x2e_T3_bit5 +1180835840*CIN1_0x2e__0x2e_T3_bit6 +2361671680*CIN1_0x2e__0x2e_T3_bit7 +4723343360*CIN1_0x2e__0x2e_T3_bit8 +9446686720*CIN1_0x2e__0x2e_T3_bit9 +18893373440*CIN1_0x2e__0x2e_T3_bit10 +37786746880*CIN1_0x2e__0x2e_T3_bit11 +75573493760*CIN1_0x2e__0x2e_T3_bit12 +125304*CVA1_0x2e__0x2e_T3_bit_7 +250608*CVA1_0x2e__0x2e_T3_bit_6 +501216*CVA1_0x2e__0x2e_T3_bit_5 +1002432*CVA1_0x2e__0x2e_T3_bit_4 +2004864*CVA1_0x2e__0x2e_T3_bit_3 +4009728*CVA1_0x2e__0x2e_T3_bit_2 +8019456*CVA1_0x2e__0x2e_T3_bit_1 +16038912*CVA1_0x2e__0x2e_T3_bit0 +32077824*CVA1_0x2e__0x2e_T3_bit1 +64155648*CVA1_0x2e__0x2e_T3_bit2 +128311296*CVA1_0x2e__0x2e_T3_bit3 +256622592*CVA1_0x2e__0x2e_T3_bit4 +513245184*CVA1_0x2e__0x2e_T3_bit5 +1026490368*CVA1_0x2e__0x2e_T3_bit6 +2052980736*CVA1_0x2e__0x2e_T3_bit7 +4105961472*CVA1_0x2e__0x2e_T3_bit8 +8211922944*CVA1_0x2e__0x2e_T3_bit9 +16423845888*CVA1_0x2e__0x2e_T3_bit10 +32847691776*CVA1_0x2e__0x2e_T3_bit11 +65695383552*CVA1_0x2e__0x2e_T3_bit12 +101600*CIN3_0x2e__0x2e_T3_bit_7 +203200*CIN3_0x2e__0x2e_T3_bit_6 +406400*CIN3_0x2e__0x2e_T3_bit_5 +812800*CIN3_0x2e__0x2e_T3_bit_4 +1625600*CIN3_0x2e__0x2e_T3_bit_3 +3251200*CIN3_0x2e__0x2e_T3_bit_2 +6502400*CIN3_0x2e__0x2e_T3_bit_1 +13004800*CIN3_0x2e__0x2e_T3_bit0 +26009600*CIN3_0x2e__0x2e_T3_bit1 +52019200*CIN3_0x2e__0x2e_T3_bit2 +104038400*CIN3_0x2e__0x2e_T3_bit3 +208076800*CIN3_0x2e__0x2e_T3_bit4 +416153600*CIN3_0x2e__0x2e_T3_bit5 +832307200*CIN3_0x2e__0x2e_T3_bit6 +1664614400*CIN3_0x2e__0x2e_T3_bit7 +3329228800*CIN3_0x2e__0x2e_T3_bit8 +6658457600*CIN3_0x2e__0x2e_T3_bit9 +13316915200*CIN3_0x2e__0x2e_T3_bit10 +26633830400*CIN3_0x2e__0x2e_T3_bit11 +53267660800*CIN3_0x2e__0x2e_T3_bit12 +88320*CVA3_0x2e__0x2e_T3_bit_7 +176640*CVA3_0x2e__0x2e_T3_bit_6 +353280*CVA3_0x2e__0x2e_T3_bit_5 +706560*CVA3_0x2e__0x2e_T3_bit_4 +1413120*CVA3_0x2e__0x2e_T3_bit_3 +2826240*CVA3_0x2e__0x2e_T3_bit_2 +5652480*CVA3_0x2e__0x2e_T3_bit_1 +11304960*CVA3_0x2e__0x2e_T3_bit0 +22609920*CVA3_0x2e__0x2e_T3_bit1 +45219840*CVA3_0x2e__0x2e_T3_bit2 +90439680*CVA3_0x2e__0x2e_T3_bit3 +180879360*CVA3_0x2e__0x2e_T3_bit4 +361758720*CVA3_0x2e__0x2e_T3_bit5 +723517440*CVA3_0x2e__0x2e_T3_bit6 +1447034880*CVA3_0x2e__0x2e_T3_bit7 +2894069760*CVA3_0x2e__0x2e_T3_bit8 +5788139520*CVA3_0x2e__0x2e_T3_bit9 +11576279040*CVA3_0x2e__0x2e_T3_bit10 +23152558080*CVA3_0x2e__0x2e_T3_bit11 +46305116160*CVA3_0x2e__0x2e_T3_bit12 +53975*CIN5_0x2e__0x2e_T3_bit_7 +107950*CIN5_0x2e__0x2e_T3_bit_6 +215900*CIN5_0x2e__0x2e_T3_bit_5 +431800*CIN5_0x2e__0x2e_T3_bit_4 +863600*CIN5_0x2e__0x2e_T3_bit_3 +1727200*CIN5_0x2e__0x2e_T3_bit_2 +3454400*CIN5_0x2e__0x2e_T3_bit_1 +6908800*CIN5_0x2e__0x2e_T3_bit0 +13817600*CIN5_0x2e__0x2e_T3_bit1 +27635200*CIN5_0x2e__0x2e_T3_bit2 +55270400*CIN5_0x2e__0x2e_T3_bit3 +110540800*CIN5_0x2e__0x2e_T3_bit4 +221081600*CIN5_0x2e__0x2e_T3_bit5 +442163200*CIN5_0x2e__0x2e_T3_bit6 +884326400*CIN5_0x2e__0x2e_T3_bit7 +1768652800*CIN5_0x2e__0x2e_T3_bit8 +3537305600*CIN5_0x2e__0x2e_T3_bit9 +7074611200*CIN5_0x2e__0x2e_T3_bit10 +14149222400*CIN5_0x2e__0x2e_T3_bit11 +28298444800*CIN5_0x2e__0x2e_T3_bit12 +46920*CVA5_0x2e__0x2e_T3_bit_7 +93840*CVA5_0x2e__0x2e_T3_bit_6 +187680*CVA5_0x2e__0x2e_T3_bit_5 +375360*CVA5_0x2e__0x2e_T3_bit_4 +750720*CVA5_0x2e__0x2e_T3_bit_3 +1501440*CVA5_0x2e__0x2e_T3_bit_2 +3002880*CVA5_0x2e__0x2e_T3_bit_1 +6005760*CVA5_0x2e__0x2e_T3_bit0 +12011520*CVA5_0x2e__0x2e_T3_bit1 +24023040*CVA5_0x2e__0x2e_T3_bit2 +48046080*CVA5_0x2e__0x2e_T3_bit3 +96092160*CVA5_0x2e__0x2e_T3_bit4 +192184320*CVA5_0x2e__0x2e_T3_bit5 +384368640*CVA5_0x2e__0x2e_T3_bit6 +768737280*CVA5_0x2e__0x2e_T3_bit7 +1537474560*CVA5_0x2e__0x2e_T3_bit8 +3074949120*CVA5_0x2e__0x2e_T3_bit9 +6149898240*CVA5_0x2e__0x2e_T3_bit10 +12299796480*CVA5_0x2e__0x2e_T3_bit11 +24599592960*CVA5_0x2e__0x2e_T3_bit12 +144145*CIN1_0x2e__0x2e_T4_bit_7 +288290*CIN1_0x2e__0x2e_T4_bit_6 +576580*CIN1_0x2e__0x2e_T4_bit_5 +1153160*CIN1_0x2e__0x2e_T4_bit_4 +2306320*CIN1_0x2e__0x2e_T4_bit_3 +4612640*CIN1_0x2e__0x2e_T4_bit_2 +9225280*CIN1_0x2e__0x2e_T4_bit_1 +18450560*CIN1_0x2e__0x2e_T4_bit0 +36901120*CIN1_0x2e__0x2e_T4_bit1 +73802240*CIN1_0x2e__0x2e_T4_bit2 +147604480*CIN1_0x2e__0x2e_T4_bit3 +295208960*CIN1_0x2e__0x2e_T4_bit4 +590417920*CIN1_0x2e__0x2e_T4_bit5 +1180835840*CIN1_0x2e__0x2e_T4_bit6 +2361671680*CIN1_0x2e__0x2e_T4_bit7 +4723343360*CIN1_0x2e__0x2e_T4_bit8 +9446686720*CIN1_0x2e__0x2e_T4_bit9 +18893373440*CIN1_0x2e__0x2e_T4_bit10 +37786746880*CIN1_0x2e__0x2e_T4_bit11 +75573493760*CIN1_0x2e__0x2e_T4_bit12 +125304*CVA1_0x2e__0x2e_T4_bit_7 +250608*CVA1_0x2e__0x2e_T4_bit_6 +501216*CVA1_0x2e__0x2e_T4_bit_5 +1002432*CVA1_0x2e__0x2e_T4_bit_4 +2004864*CVA1_0x2e__0x2e_T4_bit_3 +4009728*CVA1_0x2e__0x2e_T4_bit_2 +8019456*CVA1_0x2e__0x2e_T4_bit_1 +16038912*CVA1_0x2e__0x2e_T4_bit0 +32077824*CVA1_0x2e__0x2e_T4_bit1 +64155648*CVA1_0x2e__0x2e_T4_bit2 +128311296*CVA1_0x2e__0x2e_T4_bit3 +256622592*CVA1_0x2e__0x2e_T4_bit4 +513245184*CVA1_0x2e__0x2e_T4_bit5 +1026490368*CVA1_0x2e__0x2e_T4_bit6 +2052980736*CVA1_0x2e__0x2e_T4_bit7 +4105961472*CVA1_0x2e__0x2e_T4_bit8 +8211922944*CVA1_0x2e__0x2e_T4_bit9 +16423845888*CVA1_0x2e__0x2e_T4_bit10 +32847691776*CVA1_0x2e__0x2e_T4_bit11 +65695383552*CVA1_0x2e__0x2e_T4_bit12 +101600*CIN3_0x2e__0x2e_T4_bit_7 +203200*CIN3_0x2e__0x2e_T4_bit_6 +406400*CIN3_0x2e__0x2e_T4_bit_5 +812800*CIN3_0x2e__0x2e_T4_bit_4 +1625600*CIN3_0x2e__0x2e_T4_bit_3 +3251200*CIN3_0x2e__0x2e_T4_bit_2 +6502400*CIN3_0x2e__0x2e_T4_bit_1 +13004800*CIN3_0x2e__0x2e_T4_bit0 +26009600*CIN3_0x2e__0x2e_T4_bit1 +52019200*CIN3_0x2e__0x2e_T4_bit2 +104038400*CIN3_0x2e__0x2e_T4_bit3 +208076800*CIN3_0x2e__0x2e_T4_bit4 +416153600*CIN3_0x2e__0x2e_T4_bit5 +832307200*CIN3_0x2e__0x2e_T4_bit6 +1664614400*CIN3_0x2e__0x2e_T4_bit7 +3329228800*CIN3_0x2e__0x2e_T4_bit8 +6658457600*CIN3_0x2e__0x2e_T4_bit9 +13316915200*CIN3_0x2e__0x2e_T4_bit10 +26633830400*CIN3_0x2e__0x2e_T4_bit11 +53267660800*CIN3_0x2e__0x2e_T4_bit12 +88320*CVA3_0x2e__0x2e_T4_bit_7 +176640*CVA3_0x2e__0x2e_T4_bit_6 +353280*CVA3_0x2e__0x2e_T4_bit_5 +706560*CVA3_0x2e__0x2e_T4_bit_4 +1413120*CVA3_0x2e__0x2e_T4_bit_3 +2826240*CVA3_0x2e__0x2e_T4_bit_2 +5652480*CVA3_0x2e__0x2e_T4_bit_1 +11304960*CVA3_0x2e__0x2e_T4_bit0 +22609920*CVA3_0x2e__0x2e_T4_bit1 +45219840*CVA3_0x2e__0x2e_T4_bit2 +90439680*CVA3_0x2e__0x2e_T4_bit3 +180879360*CVA3_0x2e__0x2e_T4_bit4 +361758720*CVA3_0x2e__0x2e_T4_bit5 +723517440*CVA3_0x2e__0x2e_T4_bit6 +1447034880*CVA3_0x2e__0x2e_T4_bit7 +2894069760*CVA3_0x2e__0x2e_T4_bit8 +5788139520*CVA3_0x2e__0x2e_T4_bit9 +11576279040*CVA3_0x2e__0x2e_T4_bit10 +23152558080*CVA3_0x2e__0x2e_T4_bit11 +46305116160*CVA3_0x2e__0x2e_T4_bit12 +53975*CIN5_0x2e__0x2e_T4_bit_7 +107950*CIN5_0x2e__0x2e_T4_bit_6 +215900*CIN5_0x2e__0x2e_T4_bit_5 +431800*CIN5_0x2e__0x2e_T4_bit_4 +863600*CIN5_0x2e__0x2e_T4_bit_3 +1727200*CIN5_0x2e__0x2e_T4_bit_2 +3454400*CIN5_0x2e__0x2e_T4_bit_1 +6908800*CIN5_0x2e__0x2e_T4_bit0 +13817600*CIN5_0x2e__0x2e_T4_bit1 +27635200*CIN5_0x2e__0x2e_T4_bit2 +55270400*CIN5_0x2e__0x2e_T4_bit3 +110540800*CIN5_0x2e__0x2e_T4_bit4 +221081600*CIN5_0x2e__0x2e_T4_bit5 +442163200*CIN5_0x2e__0x2e_T4_bit6 +884326400*CIN5_0x2e__0x2e_T4_bit7 +1768652800*CIN5_0x2e__0x2e_T4_bit8 +3537305600*CIN5_0x2e__0x2e_T4_bit9 +7074611200*CIN5_0x2e__0x2e_T4_bit10 +14149222400*CIN5_0x2e__0x2e_T4_bit11 +28298444800*CIN5_0x2e__0x2e_T4_bit12 +46920*CVA5_0x2e__0x2e_T4_bit_7 +93840*CVA5_0x2e__0x2e_T4_bit_6 +187680*CVA5_0x2e__0x2e_T4_bit_5 +375360*CVA5_0x2e__0x2e_T4_bit_4 +750720*CVA5_0x2e__0x2e_T4_bit_3 +1501440*CVA5_0x2e__0x2e_T4_bit_2 +3002880*CVA5_0x2e__0x2e_T4_bit_1 +6005760*CVA5_0x2e__0x2e_T4_bit0 +12011520*CVA5_0x2e__0x2e_T4_bit1 +24023040*CVA5_0x2e__0x2e_T4_bit2 +48046080*CVA5_0x2e__0x2e_T4_bit3 +96092160*CVA5_0x2e__0x2e_T4_bit4 +192184320*CVA5_0x2e__0x2e_T4_bit5 +384368640*CVA5_0x2e__0x2e_T4_bit6 +768737280*CVA5_0x2e__0x2e_T4_bit7 +1537474560*CVA5_0x2e__0x2e_T4_bit8 +3074949120*CVA5_0x2e__0x2e_T4_bit9 +6149898240*CVA5_0x2e__0x2e_T4_bit10 +12299796480*CVA5_0x2e__0x2e_T4_bit11 +24599592960*CVA5_0x2e__0x2e_T4_bit12 -20000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit_7 -40000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit_6 -80000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit_5 -160000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit_4 -320000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit_3 -640000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit_2 -1280000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit_1 -2560000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit0 -5120000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit1 -10240000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit2 -20480000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit3 -40960000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit4 -81920000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit5 -163840000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit6 -327680000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit7 -655360000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit8 -1310720000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit9 -2621440000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit10 -5242880000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit11 -10485760000*FCC_0x2e__0x2e__0x2e__0x2e__0x2e__bit12 +485780*KVA1_0x2e__0x2e_T1_bit_7 +971560*KVA1_0x2e__0x2e_T1_bit_6 +1943120*KVA1_0x2e__0x2e_T1_bit_5 +3886240*KVA1_0x2e__0x2e_T1_bit_4 +7772480*KVA1_0x2e__0x2e_T1_bit_3 +15544960*KVA1_0x2e__0x2e_T1_bit_2 +31089920*KVA1_0x2e__0x2e_T1_bit_1 +62179840*KVA1_0x2e__0x2e_T1_bit0 +960000*KIN3_0x2e__0x2e_T1_bit_7 +1920000*KIN3_0x2e__0x2e_T1_bit_6 +3840000*KIN3_0x2e__0x2e_T1_bit_5 +7680000*KIN3_0x2e__0x2e_T1_bit_4 +15360000*KIN3_0x2e__0x2e_T1_bit_3 +30720000*KIN3_0x2e__0x2e_T1_bit_2 +61440000*KIN3_0x2e__0x2e_T1_bit_1 +122880000*KIN3_0x2e__0x2e_T1_bit0 +342400*KVA3_0x2e__0x2e_T1_bit_7 +684800*KVA3_0x2e__0x2e_T1_bit_6 +1369600*KVA3_0x2e__0x2e_T1_bit_5 +2739200*KVA3_0x2e__0x2e_T1_bit_4 +5478400*KVA3_0x2e__0x2e_T1_bit_3 +10956800*KVA3_0x2e__0x2e_T1_bit_2 +21913600*KVA3_0x2e__0x2e_T1_bit_1 +43827200*KVA3_0x2e__0x2e_T1_bit0 +510000*KIN5_0x2e__0x2e_T1_bit_7 +1020000*KIN5_0x2e__0x2e_T1_bit_6 +2040000*KIN5_0x2e__0x2e_T1_bit_5 +4080000*KIN5_0x2e__0x2e_T1_bit_4 +8160000*KIN5_0x2e__0x2e_T1_bit_3 +16320000*KIN5_0x2e__0x2e_T1_bit_2 +32640000*KIN5_0x2e__0x2e_T1_bit_1 +65280000*KIN5_0x2e__0x2e_T1_bit0 +1362000*KIN1_0x2e__0x2e_T2_bit_7 +2724000*KIN1_0x2e__0x2e_T2_bit_6 +5448000*KIN1_0x2e__0x2e_T2_bit_5 +10896000*KIN1_0x2e__0x2e_T2_bit_4 +21792000*KIN1_0x2e__0x2e_T2_bit_3 +43584000*KIN1_0x2e__0x2e_T2_bit_2 +87168000*KIN1_0x2e__0x2e_T2_bit_1 +174336000*KIN1_0x2e__0x2e_T2_bit0 +485780*KVA1_0x2e__0x2e_T2_bit_7 +971560*KVA1_0x2e__0x2e_T2_bit_6 +1943120*KVA1_0x2e__0x2e_T2_bit_5 +3886240*KVA1_0x2e__0x2e_T2_bit_4 +7772480*KVA1_0x2e__0x2e_T2_bit_3 +15544960*KVA1_0x2e__0x2e_T2_bit_2 +31089920*KVA1_0x2e__0x2e_T2_bit_1 +62179840*KVA1_0x2e__0x2e_T2_bit0 +960000*KIN3_0x2e__0x2e_T2_bit_7 +1920000*KIN3_0x2e__0x2e_T2_bit_6 +3840000*KIN3_0x2e__0x2e_T2_bit_5 +7680000*KIN3_0x2e__0x2e_T2_bit_4 +15360000*KIN3_0x2e__0x2e_T2_bit_3 +30720000*KIN3_0x2e__0x2e_T2_bit_2 +61440000*KIN3_0x2e__0x2e_T2_bit_1 +122880000*KIN3_0x2e__0x2e_T2_bit0 +342400*KVA3_0x2e__0x2e_T2_bit_7 +684800*KVA3_0x2e__0x2e_T2_bit_6 +1369600*KVA3_0x2e__0x2e_T2_bit_5 +2739200*KVA3_0x2e__0x2e_T2_bit_4 +5478400*KVA3_0x2e__0x2e_T2_bit_3 +10956800*KVA3_0x2e__0x2e_T2_bit_2 +21913600*KVA3_0x2e__0x2e_T2_bit_1 +43827200*KVA3_0x2e__0x2e_T2_bit0 +510000*KIN5_0x2e__0x2e_T2_bit_7 +1020000*KIN5_0x2e__0x2e_T2_bit_6 +2040000*KIN5_0x2e__0x2e_T2_bit_5 +4080000*KIN5_0x2e__0x2e_T2_bit_4 +8160000*KIN5_0x2e__0x2e_T2_bit_3 +16320000*KIN5_0x2e__0x2e_T2_bit_2 +32640000*KIN5_0x2e__0x2e_T2_bit_1 +65280000*KIN5_0x2e__0x2e_T2_bit0 +181900*KVA5_0x2e__0x2e_T2_bit_7 +363800*KVA5_0x2e__0x2e_T2_bit_6 +727600*KVA5_0x2e__0x2e_T2_bit_5 +1455200*KVA5_0x2e__0x2e_T2_bit_4 +2910400*KVA5_0x2e__0x2e_T2_bit_3 +5820800*KVA5_0x2e__0x2e_T2_bit_2 +11641600*KVA5_0x2e__0x2e_T2_bit_1 +23283200*KVA5_0x2e__0x2e_T2_bit0 +485780*KVA1_0x2e__0x2e_T3_bit_7 +971560*KVA1_0x2e__0x2e_T3_bit_6 +1943120*KVA1_0x2e__0x2e_T3_bit_5 +3886240*KVA1_0x2e__0x2e_T3_bit_4 +7772480*KVA1_0x2e__0x2e_T3_bit_3 +15544960*KVA1_0x2e__0x2e_T3_bit_2 +31089920*KVA1_0x2e__0x2e_T3_bit_1 +62179840*KVA1_0x2e__0x2e_T3_bit0 +960000*KIN3_0x2e__0x2e_T3_bit_7 +1920000*KIN3_0x2e__0x2e_T3_bit_6 +3840000*KIN3_0x2e__0x2e_T3_bit_5 +7680000*KIN3_0x2e__0x2e_T3_bit_4 +15360000*KIN3_0x2e__0x2e_T3_bit_3 +30720000*KIN3_0x2e__0x2e_T3_bit_2 +61440000*KIN3_0x2e__0x2e_T3_bit_1 +122880000*KIN3_0x2e__0x2e_T3_bit0 +510000*KIN5_0x2e__0x2e_T3_bit_7 +1020000*KIN5_0x2e__0x2e_T3_bit_6 +2040000*KIN5_0x2e__0x2e_T3_bit_5 +4080000*KIN5_0x2e__0x2e_T3_bit_4 +8160000*KIN5_0x2e__0x2e_T3_bit_3 +16320000*KIN5_0x2e__0x2e_T3_bit_2 +32640000*KIN5_0x2e__0x2e_T3_bit_1 +65280000*KIN5_0x2e__0x2e_T3_bit0 +1362000*KIN1_0x2e__0x2e_T4_bit_7 +2724000*KIN1_0x2e__0x2e_T4_bit_6 +5448000*KIN1_0x2e__0x2e_T4_bit_5 +10896000*KIN1_0x2e__0x2e_T4_bit_4 +21792000*KIN1_0x2e__0x2e_T4_bit_3 +43584000*KIN1_0x2e__0x2e_T4_bit_2 +87168000*KIN1_0x2e__0x2e_T4_bit_1 +174336000*KIN1_0x2e__0x2e_T4_bit0 +485780*KVA1_0x2e__0x2e_T4_bit_7 +971560*KVA1_0x2e__0x2e_T4_bit_6 +1943120*KVA1_0x2e__0x2e_T4_bit_5 +3886240*KVA1_0x2e__0x2e_T4_bit_4 +7772480*KVA1_0x2e__0x2e_T4_bit_3 +15544960*KVA1_0x2e__0x2e_T4_bit_2 +31089920*KVA1_0x2e__0x2e_T4_bit_1 +62179840*KVA1_0x2e__0x2e_T4_bit0 +960000*KIN3_0x2e__0x2e_T4_bit_7 +1920000*KIN3_0x2e__0x2e_T4_bit_6 +3840000*KIN3_0x2e__0x2e_T4_bit_5 +7680000*KIN3_0x2e__0x2e_T4_bit_4 +15360000*KIN3_0x2e__0x2e_T4_bit_3 +30720000*KIN3_0x2e__0x2e_T4_bit_2 +61440000*KIN3_0x2e__0x2e_T4_bit_1 +122880000*KIN3_0x2e__0x2e_T4_bit0 +342400*KVA3_0x2e__0x2e_T4_bit_7 +684800*KVA3_0x2e__0x2e_T4_bit_6 +1369600*KVA3_0x2e__0x2e_T4_bit_5 +2739200*KVA3_0x2e__0x2e_T4_bit_4 +5478400*KVA3_0x2e__0x2e_T4_bit_3 +10956800*KVA3_0x2e__0x2e_T4_bit_2 +21913600*KVA3_0x2e__0x2e_T4_bit_1 +43827200*KVA3_0x2e__0x2e_T4_bit0 +510000*KIN5_0x2e__0x2e_T4_bit_7 +1020000*KIN5_0x2e__0x2e_T4_bit_6 +2040000*KIN5_0x2e__0x2e_T4_bit_5 +4080000*KIN5_0x2e__0x2e_T4_bit_4 +8160000*KIN5_0x2e__0x2e_T4_bit_3 +16320000*KIN5_0x2e__0x2e_T4_bit_2 +32640000*KIN5_0x2e__0x2e_T4_bit_1 +65280000*KIN5_0x2e__0x2e_T4_bit0 +181900*KVA5_0x2e__0x2e_T4_bit_7 +363800*KVA5_0x2e__0x2e_T4_bit_6 +727600*KVA5_0x2e__0x2e_T4_bit_5 +1455200*KVA5_0x2e__0x2e_T4_bit_4 +2910400*KVA5_0x2e__0x2e_T4_bit_3 +5820800*KVA5_0x2e__0x2e_T4_bit_2 +11641600*KVA5_0x2e__0x2e_T4_bit_1 +23283200*KVA5_0x2e__0x2e_T4_bit0 = -439065600; c Cannot parse input file name: /oldhome/oroussel/tmp/wulflinc3/normalized-mps-v2-13-7-standata.opb s UNKNOWN c Exit Code: 0 c Total time: 3.826 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 Enforcing Stack size limit: 67108864 bytes Current StackSize limit: 67108864 bytes Raw data (loadavg): 0.91 0.98 0.91 2/54 9192 Raw data (stat): 9192 (runsolver) R 9191 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 910178748 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 864 [startup+3.88077 s] Raw data (loadavg): 0.91 0.98 0.91 1/53 9192 Raw data (stat): 9192 (runsolver) R 9191 20224 20223 0 -1 64 8 0 0 0 0 0 0 0 19 0 1 0 910178748 884736 94 4294967295 134512640 135332820 3221224448 3221219628 135092226 0 2147483391 7 90112 0 0 0 17 0 0 0 Raw data (statm): 216 94 205 205 0 11 0 vsize: 0 Child status: 0 Real time (s): 3.88014 CPU time (s): 3.86041 CPU user time (s): 3.51247 CPU system time (s): 0.347947 CPU usage (%): 99.4916 Max. virtual memory (Kb): 864 #### END WATCHER DATA #### #### BEGIN VERIFIER DATA #### ERROR: no interpretation found ! #### END VERIFIER DATA ####