SUCCESS(2) SUCCESS f1(x0,x1) = 1 + x0; f10(x0,x1,x2) = 0; f11(x0,x1,x2) = x0*x2 + x1; f12(x0,x1,x2) = 1 + 2*x0*x2 + x2; f13(x0,x1,x2,x3) = 0; f14(x0,x1,x2,x3,x4) = 0; f15(x0) = 1 + x0; f16(x0) = 1; f17(x0,x1) = 0; f18(x0,x1,x2) = 0; f19(x0,x1) = x0 + x1; f2(x0,x1) = 1; f20(x0,x1) = 2 + 2*x0; f21(x0,x1,x2) = 0; f22(x0,x1,x2,x3) = 0; f23(x0,x1) = x0 + x0*x1; f24(x0,x1) = 2 + 3*x0 + 2*x0*x1; f3(x0,x1,x2) = 0; f4(x0,x1,x2) = x1 + x2; f416(x0) = x0; f417(x0) = x0; f418(x0) = x0; f419(x0) = x0; f420(x0) = x0; f421(x0) = x0; f422(x0) = x0; f423(x0) = 1 + x0; f424(x0,x1,x2,x3,x4) = x1; f425(x0,x1,x2,x3,x4,x5) = x2; f426() = 0; f427(x0) = x0; f428(x0,x1,x2,x3,x4,x5) = x2; f429(x0,x1,x2,x3,x4,x5) = x2; f430(x0,x1,x2,x3,x4,x5) = 1 + 3*x0 + 2*x0*x1 + x2; f431(x0) = x0; f432(x0) = x0; f433(x0) = x0; f434(x0) = x0; f435(x0) = x0; f436(x0) = x0; f437() = 0; f438(x0,x1,x2,x3) = x0; f439(x0) = x0; f440(x0,x1,x2,x3,x4,x5) = x2; f441(x0) = x0; f442(x0,x1,x2,x3,x4,x5) = x2; f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2; f444(x0) = x0; f445(x0) = x0; f446(x0) = x0; f447(x0) = x0; f448(x0) = x0; f449(x0) = x0; f450(x0,x1,x2,x3,x4,x5,x6) = x2; f451(x0,x1,x2,x3,x4,x5) = x1 + x2; f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 + 2*x3; f453(x0) = x0; f454(x0) = x0; f455(x0) = x0; f456(x0) = 0; f457(x0,x1,x2,x3,x4,x5,x6) = x2; f458(x0) = x0; f459(x0,x1,x2,x3,x4,x5,x6) = x2; f460(x0) = x0; f461(x0,x1,x2,x3,x4,x5,x6) = x2; f462(x0,x1,x2,x3,x4,x5,x6) = 2 + x2 + 2*x3; f463(x0) = x0; f464(x0) = x0; f465(x0,x1,x2,x3,x4,x5,x6) = x2; f466(x0,x1,x2,x3,x4,x5) = x0*x2 + x1; f467(x0,x1,x2,x3,x4,x5,x6) = 1 + 2*x0*x3 + x2 + x3; f468(x0) = x0; f469(x0) = x0; f470(x0) = x0; f471(x0) = x0; f472(x0,x1,x2,x3,x4,x5,x6) = x2; f473(x0) = x0; f474(x0,x1,x2,x3,x4,x5,x6) = x2; f475(x0) = x0; f476(x0,x1,x2,x3,x4,x5,x6) = x2; f477(x0,x1,x2,x3,x4,x5,x6) = 1 + 2*x0 + 2*x0*x3 + x2 + x3; f478(x0) = x0; f5(x0,x1,x2) = 1 + 2*x2; f6(x0,x1,x2,x3) = 0; f7(x0,x1,x2,x3,x4) = 0; f8(x0,x1) = x0 + x1; f9(x0,x1) = 2*x1; ExecutionLog | +- Staring timer: 2017-03-30 07:40:39.597236 UTC | +- Open Constraints | | | +- f416(x5) = f416(x5) >= x5 = x5 | | | +- f417(x5) = f417(x5) >= f416(x5) = f416(x5) | | | +- f418(x4) = f418(x4) >= x4 = x4 | | | +- f419(x5) = f419(x5) >= f417(x5) = f417(x5) | | | +- f420(x101) = f420(x101) >= x101 = x101 | | | +- f421(x99) = f421(x99) >= x99 = x99 | | | +- f422(x100) = f422(x100) >= x100 = x100 | | | +- f8(x99,f423(x4)) = f8(x99,f423(x4)) >= f19(f418(x4),f421(x99)) = f19(f418(x4),f421(x99)) | | | +- f9(x99,f423(x4)) + x100 = f9(x99,f423(x4)) + x100 >= f20(f418(x4),f421(x99)) + f422(x100) = f20(f418(x4),f421(x99)) + f422(x100) | | | +- f10(x99,f423(x4),x100) + x101 = f10(x99,f423(x4),x100) + x101 >= f21(f418(x4),f421(x99),f422(x100)) + f420(x101) = f21(f418(x4),f421(x99),f422(x100)) + f420(x101) | | | +- f424(x4,x5,x99,x100,x101) = f424(x4,x5,x99,x100,x101) >= f22(f418(x4),f421(x99),f422(x100),f420(x101)) + f419(x5) = f22(f418(x4),f421(x99),f422(x100),f420(x101)) + f419(x5) | | | +- f425(x3,x4,x5,x99,x100,x101) = f425(x3,x4,x5,x99,x100,x101) >= f14(f423(x4),f426(),f427(x3),f428(x3,x4,x5,x99,x100,x101),f429(x3,x4,x5,x99,x100,x101)) + f424(x4,x5,x99,x100,x101) = f14(f423(x4) ,f426() ,f427(x3) ,f428(x3 ,x4 ,x5 ,x99 ,x100 ,x101) ,f429(x3 ,x4 ,x5 ,x99 ,x100 ,x101)) + f424(x4,x5,x99,x100,x101) | | | +- f426() = f426() >= 0 = 0 | | | +- f429(x3,x4,x5,x99,x100,x101) = f429(x3,x4,x5,x99,x100,x101) >= f425(x3,x4,x5,x99,x100,x101) = f425(x3,x4,x5,x99,x100,x101) | | | +- f427(x3) = f427(x3) >= x3 = x3 | | | +- f428(x3,x4,x5,x99,x100,x101) = f428(x3,x4,x5,x99,x100,x101) >= f13(f423(x4),f426(),f427(x3),f428(x3,x4,x5,x99,x100,x101)) + f429(x3,x4,x5,x99,x100,x101) = f13(f423(x4) ,f426() ,f427(x3) ,f428(x3,x4,x5,x99,x100,x101)) + f429(x3,x4,x5,x99,x100,x101) | | | +- f430(x3,x4,x5,x99,x100,x101) = f430(x3,x4,x5,x99,x100,x101) >= f12(f423(x4),f426(),f427(x3)) + f428(x3,x4,x5,x99,x100,x101) = f12(f423(x4),f426(),f427(x3)) + f428(x3,x4,x5,x99,x100,x101) | | | +- f23(x3,x4) = f23(x3,x4) >= f11(f423(x4),f426(),f427(x3)) = f11(f423(x4),f426(),f427(x3)) | | | +- f24(x3,x4) + x5 = f24(x3,x4) + x5 >= f430(x3,x4,x5,x99,x100,x101) + 1 = f430(x3,x4,x5,x99,x100,x101) + 1 | | | +- f431(x10) = f431(x10) >= x10 = x10 | | | +- f432(x10) = f432(x10) >= f431(x10) = f431(x10) | | | +- f433(x10) = f433(x10) >= f432(x10) = f432(x10) | | | +- f434(x173) = f434(x173) >= x173 = x173 | | | +- f435(x171) = f435(x171) >= x171 = x171 | | | +- f436(x172) = f436(x172) >= x172 = x172 | | | +- f1(x171,f437()) = f1(x171,f437()) >= f15(f435(x171)) = f15(f435(x171)) | | | +- f2(x171,f437()) + x172 = f2(x171,f437()) + x172 >= f16(f435(x171)) + f436(x172) = f16(f435(x171)) + f436(x172) | | | +- f3(x171,f437(),x172) + x173 = f3(x171,f437(),x172) + x173 >= f17(f435(x171),f436(x172)) + f434(x173) = f17(f435(x171),f436(x172)) + f434(x173) | | | +- f438(x10,x171,x172,x173) = f438(x10,x171,x172,x173) >= f18(f435(x171),f436(x172),f434(x173)) + f433(x10) = f18(f435(x171),f436(x172),f434(x173)) + f433(x10) | | | +- f439(x9) = f439(x9) >= x9 = x9 | | | +- f440(x8,x9,x10,x171,x172,x173) = f440(x8,x9,x10,x171,x172,x173) >= f7(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173),f440(x8,x9,x10,x171,x172,x173)) + f438(x10,x171,x172,x173) = f7(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173),f440(x8,x9,x10,x171,x172,x173)) + f438(x10,x171,x172,x173) | | | +- f441(x8) = f441(x8) >= x8 = x8 | | | +- f442(x8,x9,x10,x171,x172,x173) = f442(x8,x9,x10,x171,x172,x173) >= f6(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173)) + f440(x8,x9,x10,x171,x172,x173) = f6(f437() ,f439(x9) ,f441(x8) ,f442(x8,x9,x10,x171,x172,x173)) + f440(x8,x9,x10,x171,x172,x173) | | | +- f443(x8,x9,x10,x171,x172,x173) = f443(x8,x9,x10,x171,x172,x173) >= f5(f437(),f439(x9),f441(x8)) + f442(x8,x9,x10,x171,x172,x173) = f5(f437(),f439(x9),f441(x8)) + f442(x8,x9,x10,x171,x172,x173) | | | +- f19(x8,x9) = f19(x8,x9) >= f4(f437(),f439(x9),f441(x8)) = f4(f437(),f439(x9),f441(x8)) | | | +- f20(x8,x9) + x10 = f20(x8,x9) + x10 >= f443(x8,x9,x10,x171,x172,x173) + 1 = f443(x8,x9,x10,x171,x172,x173) + 1 | | | +- f444(x14) = f444(x14) >= x14 = x14 | | | +- f445(x14) = f445(x14) >= f444(x14) = f444(x14) | | | +- f446(x13) = f446(x13) >= x13 = x13 | | | +- f447(x14) = f447(x14) >= f445(x14) = f445(x14) | | | +- f448(x14) = f448(x14) >= f447(x14) = f447(x14) | | | +- f15(x13) = f15(x13) >= f446(x13) + 1 = f446(x13) + 1 | | | +- f16(x13) + x14 = f16(x13) + x14 >= f448(x14) + 1 = f448(x14) + 1 | | | +- f449(x20) = f449(x20) >= x20 = x20 | | | +- f450(x17,x18,x20,x22,x242,x243,x244) = f450(x17,x18,x20,x22,x242,x243,x244) >= f3(f451(x17,x18,x22,x242,x243,x244),x17,f452(x17,x18,x20,x22,x242,x243,x244)) + f449(x20) = f3(f451(x17 ,x18 ,x22 ,x242 ,x243 ,x244) ,x17 ,f452(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244)) + f449(x20) | | | +- f453(x244) = f453(x244) >= x244 = x244 | | | +- f454(x242) = f454(x242) >= x242 = x242 | | | +- f455(x243) = f455(x243) >= x243 = x243 | | | +- f1(x242,f456(x17)) = f1(x242,f456(x17)) >= f1(f454(x242),x17) = f1(f454(x242),x17) | | | +- f2(x242,f456(x17)) + x243 = f2(x242,f456(x17)) + x243 >= f2(f454(x242),x17) + f455(x243) = f2(f454(x242),x17) + f455(x243) | | | +- f3(x242,f456(x17),x243) + x244 = f3(x242,f456(x17),x243) + x244 >= f3(f454(x242),x17,f455(x243)) + f453(x244) = f3(f454(x242),x17,f455(x243)) + f453(x244) | | | +- f457(x17,x18,x20,x22,x242,x243,x244) = f457(x17,x18,x20,x22,x242,x243,x244) >= f450(x17,x18,x20,x22,x242,x243,x244) = f450(x17,x18,x20,x22,x242,x243,x244) | | | +- f458(x18) = f458(x18) >= x18 = x18 | | | +- f459(x17,x18,x20,x22,x242,x243,x244) = f459(x17,x18,x20,x22,x242,x243,x244) >= f7(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244),f459(x17,x18,x20,x22,x242,x243,x244)) + f457(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) = f7(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244),f459(x17,x18,x20,x22,x242,x243,x244)) + f457(x17,x18,x20,x22,x242,x243,x244) | | | +- f460(x22) = f460(x22) >= x22 = x22 | | | +- f461(x17,x18,x20,x22,x242,x243,x244) = f461(x17,x18,x20,x22,x242,x243,x244) >= f6(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244)) + f459(x17,x18,x20,x22,x242,x243,x244) = f6(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244)) + f459(x17,x18,x20,x22,x242,x243,x244) | | | +- f451(x17,x18,x22,x242,x243,x244) = f451(x17,x18,x22,x242,x243,x244) >= f4(f456(x17),f458(x18),f460(x22)) = f4(f456(x17),f458(x18),f460(x22)) | | | +- f452(x17,x18,x20,x22,x242,x243,x244) = f452(x17,x18,x20,x22,x242,x243,x244) >= f5(f456(x17),f458(x18),f460(x22)) + f461(x17,x18,x20,x22,x242,x243,x244) = f5(f456(x17),f458(x18),f460(x22)) + f461(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) | | | +- f462(x17,x18,x20,x22,x242,x243,x244) = f462(x17,x18,x20,x22,x242,x243,x244) >= f2(f451(x17,x18,x22,x242,x243,x244),x17) + f452(x17,x18,x20,x22,x242,x243,x244) = f2(f451(x17,x18,x22,x242,x243,x244) ,x17) + f452(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) | | | +- f4(x17,x18,x22 + 1) = f4(x17,x18,x22 + 1) >= f1(f451(x17,x18,x22,x242,x243,x244),x17) = f1(f451(x17,x18,x22,x242,x243,x244),x17) | | | +- f5(x17,x18,x22 + 1) + x20 = f5(x17,x18,x22 + 1) + x20 >= f462(x17,x18,x20,x22,x242,x243,x244) + 1 = f462(x17,x18,x20,x22,x242,x243,x244) + 1 | | | +- f463(x31) = f463(x31) >= x31 = x31 | | | +- f4(x28,x29,0) = f4(x28,x29,0) >= x29 = x29 | | | +- f5(x28,x29,0) + x31 = f5(x28,x29,0) + x31 >= f463(x31) + 1 = f463(x31) + 1 | | | +- f464(x41) = f464(x41) >= x41 = x41 | | | +- f465(x38,x39,x41,x43,x346,x347,x348) = f465(x38,x39,x41,x43,x346,x347,x348) >= f10(f466(x38,x39,x43,x346,x347,x348),x38,f467(x38,x39,x41,x43,x346,x347,x348)) + f464(x41) = f10(f466(x38 ,x39 ,x43 ,x346 ,x347 ,x348) ,x38 ,f467(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348)) + f464(x41) | | | +- f468(x348) = f468(x348) >= x348 = x348 | | | +- f469(x346) = f469(x346) >= x346 = x346 | | | +- f470(x347) = f470(x347) >= x347 = x347 | | | +- f8(x346,f471(x38)) = f8(x346,f471(x38)) >= f8(f469(x346),x38) = f8(f469(x346),x38) | | | +- f9(x346,f471(x38)) + x347 = f9(x346,f471(x38)) + x347 >= f9(f469(x346),x38) + f470(x347) = f9(f469(x346),x38) + f470(x347) | | | +- f10(x346,f471(x38),x347) + x348 = f10(x346,f471(x38),x347) + x348 >= f10(f469(x346),x38,f470(x347)) + f468(x348) = f10(f469(x346),x38,f470(x347)) + f468(x348) | | | +- f472(x38,x39,x41,x43,x346,x347,x348) = f472(x38,x39,x41,x43,x346,x347,x348) >= f465(x38,x39,x41,x43,x346,x347,x348) = f465(x38,x39,x41,x43,x346,x347,x348) | | | +- f473(x39) = f473(x39) >= x39 = x39 | | | +- f474(x38,x39,x41,x43,x346,x347,x348) = f474(x38,x39,x41,x43,x346,x347,x348) >= f14(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348),f474(x38,x39,x41,x43,x346,x347,x348)) + f472(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348) = f14(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348),f474(x38,x39,x41,x43,x346,x347,x348)) + f472(x38,x39,x41,x43,x346,x347,x348) | | | +- f475(x43) = f475(x43) >= x43 = x43 | | | +- f476(x38,x39,x41,x43,x346,x347,x348) = f476(x38,x39,x41,x43,x346,x347,x348) >= f13(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348)) + f474(x38,x39,x41,x43,x346,x347,x348) = f13(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348)) + f474(x38,x39,x41,x43,x346,x347,x348) | | | +- f466(x38,x39,x43,x346,x347,x348) = f466(x38,x39,x43,x346,x347,x348) >= f11(f471(x38),f473(x39),f475(x43)) = f11(f471(x38),f473(x39),f475(x43)) | | | +- f467(x38,x39,x41,x43,x346,x347,x348) = f467(x38,x39,x41,x43,x346,x347,x348) >= f12(f471(x38),f473(x39),f475(x43)) + f476(x38,x39,x41,x43,x346,x347,x348) = f12(f471(x38),f473(x39),f475(x43)) + f476(x38,x39,x41,x43,x346,x347,x348) | | | +- f477(x38,x39,x41,x43,x346,x347,x348) = f477(x38,x39,x41,x43,x346,x347,x348) >= f9(f466(x38,x39,x43,x346,x347,x348),x38) + f467(x38,x39,x41,x43,x346,x347,x348) = f9(f466(x38,x39,x43,x346,x347,x348) ,x38) + f467(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348) | | | +- f11(x38,x39,x43 + 1) = f11(x38,x39,x43 + 1) >= f8(f466(x38,x39,x43,x346,x347,x348),x38) = f8(f466(x38,x39,x43,x346,x347,x348),x38) | | | +- f12(x38,x39,x43 + 1) + x41 = f12(x38,x39,x43 + 1) + x41 >= f477(x38,x39,x41,x43,x346,x347,x348) + 1 = f477(x38,x39,x41,x43,x346,x347,x348) + 1 | | | +- f478(x52) = f478(x52) >= x52 = x52 | | | +- f11(x49,x50,0) = f11(x49,x50,0) >= x50 = x50 | | | `- f12(x49,x50,0) + x52 = f12(x49,x50,0) + x52 >= f478(x52) + 1 = f478(x52) + 1 | +- Open Constraints | | | +- f416(x5) = f416(x5) >= x5 = x5 | | | +- f417(x5) = f417(x5) >= f416(x5) = f416(x5) | | | +- f418(x4) = f418(x4) >= x4 = x4 | | | +- f419(x5) = f419(x5) >= f417(x5) = f417(x5) | | | +- f420(x101) = f420(x101) >= x101 = x101 | | | +- f421(x99) = f421(x99) >= x99 = x99 | | | +- f422(x100) = f422(x100) >= x100 = x100 | | | +- f8(x99,f423(x4)) = f8(x99,f423(x4)) >= f19(f418(x4),f421(x99)) = f19(f418(x4),f421(x99)) | | | +- f9(x99,f423(x4)) + x100 = f9(x99,f423(x4)) + x100 >= f20(f418(x4),f421(x99)) + f422(x100) = f20(f418(x4),f421(x99)) + f422(x100) | | | +- f10(x99,f423(x4),x100) + x101 = f10(x99,f423(x4),x100) + x101 >= f21(f418(x4),f421(x99),f422(x100)) + f420(x101) = f21(f418(x4),f421(x99),f422(x100)) + f420(x101) | | | +- f424(x4,x5,x99,x100,x101) = f424(x4,x5,x99,x100,x101) >= f22(f418(x4),f421(x99),f422(x100),f420(x101)) + f419(x5) = f22(f418(x4),f421(x99),f422(x100),f420(x101)) + f419(x5) | | | +- f425(x3,x4,x5,x99,x100,x101) = f425(x3,x4,x5,x99,x100,x101) >= f14(f423(x4),f426(),f427(x3),f428(x3,x4,x5,x99,x100,x101),f429(x3,x4,x5,x99,x100,x101)) + f424(x4,x5,x99,x100,x101) = f14(f423(x4) ,f426() ,f427(x3) ,f428(x3 ,x4 ,x5 ,x99 ,x100 ,x101) ,f429(x3 ,x4 ,x5 ,x99 ,x100 ,x101)) + f424(x4,x5,x99,x100,x101) | | | +- f426() = f426() >= 0 = 0 | | | +- f429(x3,x4,x5,x99,x100,x101) = f429(x3,x4,x5,x99,x100,x101) >= f425(x3,x4,x5,x99,x100,x101) = f425(x3,x4,x5,x99,x100,x101) | | | +- f427(x3) = f427(x3) >= x3 = x3 | | | +- f428(x3,x4,x5,x99,x100,x101) = f428(x3,x4,x5,x99,x100,x101) >= f13(f423(x4),f426(),f427(x3),f428(x3,x4,x5,x99,x100,x101)) + f429(x3,x4,x5,x99,x100,x101) = f13(f423(x4) ,f426() ,f427(x3) ,f428(x3,x4,x5,x99,x100,x101)) + f429(x3,x4,x5,x99,x100,x101) | | | +- f430(x3,x4,x5,x99,x100,x101) = f430(x3,x4,x5,x99,x100,x101) >= f12(f423(x4),f426(),f427(x3)) + f428(x3,x4,x5,x99,x100,x101) = f12(f423(x4),f426(),f427(x3)) + f428(x3,x4,x5,x99,x100,x101) | | | +- f23(x3,x4) = f23(x3,x4) >= f11(f423(x4),f426(),f427(x3)) = f11(f423(x4),f426(),f427(x3)) | | | +- f24(x3,x4) + x5 = f24(x3,x4) + x5 >= f430(x3,x4,x5,x99,x100,x101) + 1 = f430(x3,x4,x5,x99,x100,x101) + 1 | | | +- f431(x10) = f431(x10) >= x10 = x10 | | | +- f432(x10) = f432(x10) >= f431(x10) = f431(x10) | | | +- f433(x10) = f433(x10) >= f432(x10) = f432(x10) | | | +- f434(x173) = f434(x173) >= x173 = x173 | | | +- f435(x171) = f435(x171) >= x171 = x171 | | | +- f436(x172) = f436(x172) >= x172 = x172 | | | +- f1(x171,f437()) = f1(x171,f437()) >= f15(f435(x171)) = f15(f435(x171)) | | | +- f2(x171,f437()) + x172 = f2(x171,f437()) + x172 >= f16(f435(x171)) + f436(x172) = f16(f435(x171)) + f436(x172) | | | +- f3(x171,f437(),x172) + x173 = f3(x171,f437(),x172) + x173 >= f17(f435(x171),f436(x172)) + f434(x173) = f17(f435(x171),f436(x172)) + f434(x173) | | | +- f438(x10,x171,x172,x173) = f438(x10,x171,x172,x173) >= f18(f435(x171),f436(x172),f434(x173)) + f433(x10) = f18(f435(x171),f436(x172),f434(x173)) + f433(x10) | | | +- f439(x9) = f439(x9) >= x9 = x9 | | | +- f440(x8,x9,x10,x171,x172,x173) = f440(x8,x9,x10,x171,x172,x173) >= f7(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173),f440(x8,x9,x10,x171,x172,x173)) + f438(x10,x171,x172,x173) = f7(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173),f440(x8,x9,x10,x171,x172,x173)) + f438(x10,x171,x172,x173) | | | +- f441(x8) = f441(x8) >= x8 = x8 | | | +- f442(x8,x9,x10,x171,x172,x173) = f442(x8,x9,x10,x171,x172,x173) >= f6(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173)) + f440(x8,x9,x10,x171,x172,x173) = f6(f437() ,f439(x9) ,f441(x8) ,f442(x8,x9,x10,x171,x172,x173)) + f440(x8,x9,x10,x171,x172,x173) | | | +- f443(x8,x9,x10,x171,x172,x173) = f443(x8,x9,x10,x171,x172,x173) >= f5(f437(),f439(x9),f441(x8)) + f442(x8,x9,x10,x171,x172,x173) = f5(f437(),f439(x9),f441(x8)) + f442(x8,x9,x10,x171,x172,x173) | | | +- f19(x8,x9) = f19(x8,x9) >= f4(f437(),f439(x9),f441(x8)) = f4(f437(),f439(x9),f441(x8)) | | | +- f20(x8,x9) + x10 = f20(x8,x9) + x10 >= f443(x8,x9,x10,x171,x172,x173) + 1 = f443(x8,x9,x10,x171,x172,x173) + 1 | | | +- f444(x14) = f444(x14) >= x14 = x14 | | | +- f445(x14) = f445(x14) >= f444(x14) = f444(x14) | | | +- f446(x13) = f446(x13) >= x13 = x13 | | | +- f447(x14) = f447(x14) >= f445(x14) = f445(x14) | | | +- f448(x14) = f448(x14) >= f447(x14) = f447(x14) | | | +- f15(x13) = f15(x13) >= f446(x13) + 1 = f446(x13) + 1 | | | +- f16(x13) + x14 = f16(x13) + x14 >= f448(x14) + 1 = f448(x14) + 1 | | | +- f449(x20) = f449(x20) >= x20 = x20 | | | +- f450(x17,x18,x20,x22,x242,x243,x244) = f450(x17,x18,x20,x22,x242,x243,x244) >= f3(f451(x17,x18,x22,x242,x243,x244),x17,f452(x17,x18,x20,x22,x242,x243,x244)) + f449(x20) = f3(f451(x17 ,x18 ,x22 ,x242 ,x243 ,x244) ,x17 ,f452(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244)) + f449(x20) | | | +- f453(x244) = f453(x244) >= x244 = x244 | | | +- f454(x242) = f454(x242) >= x242 = x242 | | | +- f455(x243) = f455(x243) >= x243 = x243 | | | +- f1(x242,f456(x17)) = f1(x242,f456(x17)) >= f1(f454(x242),x17) = f1(f454(x242),x17) | | | +- f2(x242,f456(x17)) + x243 = f2(x242,f456(x17)) + x243 >= f2(f454(x242),x17) + f455(x243) = f2(f454(x242),x17) + f455(x243) | | | +- f3(x242,f456(x17),x243) + x244 = f3(x242,f456(x17),x243) + x244 >= f3(f454(x242),x17,f455(x243)) + f453(x244) = f3(f454(x242),x17,f455(x243)) + f453(x244) | | | +- f457(x17,x18,x20,x22,x242,x243,x244) = f457(x17,x18,x20,x22,x242,x243,x244) >= f450(x17,x18,x20,x22,x242,x243,x244) = f450(x17,x18,x20,x22,x242,x243,x244) | | | +- f458(x18) = f458(x18) >= x18 = x18 | | | +- f459(x17,x18,x20,x22,x242,x243,x244) = f459(x17,x18,x20,x22,x242,x243,x244) >= f7(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244),f459(x17,x18,x20,x22,x242,x243,x244)) + f457(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) = f7(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244),f459(x17,x18,x20,x22,x242,x243,x244)) + f457(x17,x18,x20,x22,x242,x243,x244) | | | +- f460(x22) = f460(x22) >= x22 = x22 | | | +- f461(x17,x18,x20,x22,x242,x243,x244) = f461(x17,x18,x20,x22,x242,x243,x244) >= f6(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244)) + f459(x17,x18,x20,x22,x242,x243,x244) = f6(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244)) + f459(x17,x18,x20,x22,x242,x243,x244) | | | +- f451(x17,x18,x22,x242,x243,x244) = f451(x17,x18,x22,x242,x243,x244) >= f4(f456(x17),f458(x18),f460(x22)) = f4(f456(x17),f458(x18),f460(x22)) | | | +- f452(x17,x18,x20,x22,x242,x243,x244) = f452(x17,x18,x20,x22,x242,x243,x244) >= f5(f456(x17),f458(x18),f460(x22)) + f461(x17,x18,x20,x22,x242,x243,x244) = f5(f456(x17),f458(x18),f460(x22)) + f461(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) | | | +- f462(x17,x18,x20,x22,x242,x243,x244) = f462(x17,x18,x20,x22,x242,x243,x244) >= f2(f451(x17,x18,x22,x242,x243,x244),x17) + f452(x17,x18,x20,x22,x242,x243,x244) = f2(f451(x17,x18,x22,x242,x243,x244) ,x17) + f452(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) | | | +- f4(x17,x18,x22 + 1) = f4(x17,x18,x22 + 1) >= f1(f451(x17,x18,x22,x242,x243,x244),x17) = f1(f451(x17,x18,x22,x242,x243,x244),x17) | | | +- f5(x17,x18,x22 + 1) + x20 = f5(x17,x18,x22 + 1) + x20 >= f462(x17,x18,x20,x22,x242,x243,x244) + 1 = f462(x17,x18,x20,x22,x242,x243,x244) + 1 | | | +- f463(x31) = f463(x31) >= x31 = x31 | | | +- f4(x28,x29,0) = f4(x28,x29,0) >= x29 = x29 | | | +- f5(x28,x29,0) + x31 = f5(x28,x29,0) + x31 >= f463(x31) + 1 = f463(x31) + 1 | | | +- f464(x41) = f464(x41) >= x41 = x41 | | | +- f465(x38,x39,x41,x43,x346,x347,x348) = f465(x38,x39,x41,x43,x346,x347,x348) >= f10(f466(x38,x39,x43,x346,x347,x348),x38,f467(x38,x39,x41,x43,x346,x347,x348)) + f464(x41) = f10(f466(x38 ,x39 ,x43 ,x346 ,x347 ,x348) ,x38 ,f467(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348)) + f464(x41) | | | +- f468(x348) = f468(x348) >= x348 = x348 | | | +- f469(x346) = f469(x346) >= x346 = x346 | | | +- f470(x347) = f470(x347) >= x347 = x347 | | | +- f8(x346,f471(x38)) = f8(x346,f471(x38)) >= f8(f469(x346),x38) = f8(f469(x346),x38) | | | +- f9(x346,f471(x38)) + x347 = f9(x346,f471(x38)) + x347 >= f9(f469(x346),x38) + f470(x347) = f9(f469(x346),x38) + f470(x347) | | | +- f10(x346,f471(x38),x347) + x348 = f10(x346,f471(x38),x347) + x348 >= f10(f469(x346),x38,f470(x347)) + f468(x348) = f10(f469(x346),x38,f470(x347)) + f468(x348) | | | +- f472(x38,x39,x41,x43,x346,x347,x348) = f472(x38,x39,x41,x43,x346,x347,x348) >= f465(x38,x39,x41,x43,x346,x347,x348) = f465(x38,x39,x41,x43,x346,x347,x348) | | | +- f473(x39) = f473(x39) >= x39 = x39 | | | +- f474(x38,x39,x41,x43,x346,x347,x348) = f474(x38,x39,x41,x43,x346,x347,x348) >= f14(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348),f474(x38,x39,x41,x43,x346,x347,x348)) + f472(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348) = f14(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348),f474(x38,x39,x41,x43,x346,x347,x348)) + f472(x38,x39,x41,x43,x346,x347,x348) | | | +- f475(x43) = f475(x43) >= x43 = x43 | | | +- f476(x38,x39,x41,x43,x346,x347,x348) = f476(x38,x39,x41,x43,x346,x347,x348) >= f13(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348)) + f474(x38,x39,x41,x43,x346,x347,x348) = f13(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348)) + f474(x38,x39,x41,x43,x346,x347,x348) | | | +- f466(x38,x39,x43,x346,x347,x348) = f466(x38,x39,x43,x346,x347,x348) >= f11(f471(x38),f473(x39),f475(x43)) = f11(f471(x38),f473(x39),f475(x43)) | | | +- f467(x38,x39,x41,x43,x346,x347,x348) = f467(x38,x39,x41,x43,x346,x347,x348) >= f12(f471(x38),f473(x39),f475(x43)) + f476(x38,x39,x41,x43,x346,x347,x348) = f12(f471(x38),f473(x39),f475(x43)) + f476(x38,x39,x41,x43,x346,x347,x348) | | | +- f477(x38,x39,x41,x43,x346,x347,x348) = f477(x38,x39,x41,x43,x346,x347,x348) >= f9(f466(x38,x39,x43,x346,x347,x348),x38) + f467(x38,x39,x41,x43,x346,x347,x348) = f9(f466(x38,x39,x43,x346,x347,x348) ,x38) + f467(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348) | | | +- f11(x38,x39,x43 + 1) = f11(x38,x39,x43 + 1) >= f8(f466(x38,x39,x43,x346,x347,x348),x38) = f8(f466(x38,x39,x43,x346,x347,x348),x38) | | | +- f12(x38,x39,x43 + 1) + x41 = f12(x38,x39,x43 + 1) + x41 >= f477(x38,x39,x41,x43,x346,x347,x348) + 1 = f477(x38,x39,x41,x43,x346,x347,x348) + 1 | | | +- f478(x52) = f478(x52) >= x52 = x52 | | | +- f11(x49,x50,0) = f11(x49,x50,0) >= x50 = x50 | | | `- f12(x49,x50,0) + x52 = f12(x49,x50,0) + x52 >= f478(x52) + 1 = f478(x52) + 1 | +- Simplification ... | | | +- Substituted: f16(x13) + x14 ≥ f448(x14) + 1 ↦ f16(0) + x14 ≥ f448(x14) + 1 | | | +- Substituted: f451(x17,x18,x22,x242,x243,x244) ≥ f4(f456(x17),f458(x18),f460(x22)) ↦ f451(x17,x18,x22,0,0,0) ≥ f4(f456(x17),f458(x18),f460(x22)) | | | +- Substituted: f4(x28,x29,0) ≥ x29 ↦ f4(0,x29,0) ≥ x29 | | | +- Substituted: f5(x28,x29,0) + x31 ≥ f463(x31) + 1 ↦ f5(0,0,0) + x31 ≥ f463(x31) + 1 | | | +- Substituted: f466(x38,x39,x43,x346,x347,x348) ≥ f11(f471(x38),f473(x39),f475(x43)) ↦ f466(x38,x39,x43,0,0,0) ≥ f11(f471(x38),f473(x39),f475(x43)) | | | +- Substituted: f11(x49,x50,0) ≥ x50 ↦ f11(0,x50,0) ≥ x50 | | | +- Substituted: f12(x49,x50,0) + x52 ≥ f478(x52) + 1 ↦ f12(0,0,0) + x52 ≥ f478(x52) + 1 | | | +- Eliminated: f13/4 | | | +- Eliminated: f14/5 | | | +- Eliminated: f17/2 | | | +- Eliminated: f18/3 | | | +- Eliminated: f21/3 | | | +- Eliminated: f22/4 | | | +- Eliminated: f6/4 | | | +- Eliminated: f7/5 | | | +- Propagated: f416(x0) ↦ x0 | | | +- Propagated: f418(x0) ↦ x0 | | | +- Propagated: f420(x0) ↦ x0 | | | +- Propagated: f421(x0) ↦ x0 | | | +- Propagated: f422(x0) ↦ x0 | | | +- Propagated: f426() ↦ 0 | | | +- Propagated: f427(x0) ↦ x0 | | | +- Propagated: f431(x0) ↦ x0 | | | +- Propagated: f434(x0) ↦ x0 | | | +- Propagated: f435(x0) ↦ x0 | | | +- Propagated: f436(x0) ↦ x0 | | | +- Propagated: f439(x0) ↦ x0 | | | +- Propagated: f441(x0) ↦ x0 | | | +- Propagated: f444(x0) ↦ x0 | | | +- Propagated: f446(x0) ↦ x0 | | | +- Propagated: f449(x0) ↦ x0 | | | +- Propagated: f453(x0) ↦ x0 | | | +- Propagated: f454(x0) ↦ x0 | | | +- Propagated: f455(x0) ↦ x0 | | | +- Propagated: f458(x0) ↦ x0 | | | +- Propagated: f460(x0) ↦ x0 | | | +- Propagated: f463(x0) ↦ x0 | | | +- Propagated: f464(x0) ↦ x0 | | | +- Propagated: f468(x0) ↦ x0 | | | +- Propagated: f469(x0) ↦ x0 | | | +- Propagated: f470(x0) ↦ x0 | | | +- Propagated: f473(x0) ↦ x0 | | | +- Propagated: f475(x0) ↦ x0 | | | +- Propagated: f478(x0) ↦ x0 | | | +- Propagated: f15(x0) ↦ 1 + x0 | | | +- Propagated: f417(x0) ↦ x0 | | | +- Propagated: f432(x0) ↦ x0 | | | +- Propagated: f445(x0) ↦ x0 | | | +- Propagated: f419(x0) ↦ x0 | | | +- Propagated: f433(x0) ↦ x0 | | | +- Propagated: f447(x0) ↦ x0 | | | +- Propagated: f424(x0,x1,x2,x3,x4) ↦ x1 | | | +- Propagated: f438(x0,x1,x2,x3) ↦ x0 | | | +- Propagated: f448(x0) ↦ x0 | | | +- Propagated: f425(x0,x1,x2,x3,x4,x5) ↦ x2 | | | +- Propagated: f440(x0,x1,x2,x3,x4,x5) ↦ x2 | | | +- Propagated: f429(x0,x1,x2,x3,x4,x5) ↦ x2 | | | +- Propagated: f442(x0,x1,x2,x3,x4,x5) ↦ x2 | | | `- Propagated: f428(x0,x1,x2,x3,x4,x5) ↦ x2 | +- Interpretation | | | +- f13(x0,x1,x2,x3) = 0 | | | +- f14(x0,x1,x2,x3,x4) = 0 | | | +- f15(x0) = 1 + x0 | | | +- f17(x0,x1) = 0 | | | +- f18(x0,x1,x2) = 0 | | | +- f21(x0,x1,x2) = 0 | | | +- f22(x0,x1,x2,x3) = 0 | | | +- f416(x0) = x0 | | | +- f417(x0) = x0 | | | +- f418(x0) = x0 | | | +- f419(x0) = x0 | | | +- f420(x0) = x0 | | | +- f421(x0) = x0 | | | +- f422(x0) = x0 | | | +- f424(x0,x1,x2,x3,x4) = x1 | | | +- f425(x0,x1,x2,x3,x4,x5) = x2 | | | +- f426() = 0 | | | +- f427(x0) = x0 | | | +- f428(x0,x1,x2,x3,x4,x5) = x2 | | | +- f429(x0,x1,x2,x3,x4,x5) = x2 | | | +- f431(x0) = x0 | | | +- f432(x0) = x0 | | | +- f433(x0) = x0 | | | +- f434(x0) = x0 | | | +- f435(x0) = x0 | | | +- f436(x0) = x0 | | | +- f438(x0,x1,x2,x3) = x0 | | | +- f439(x0) = x0 | | | +- f440(x0,x1,x2,x3,x4,x5) = x2 | | | +- f441(x0) = x0 | | | +- f442(x0,x1,x2,x3,x4,x5) = x2 | | | +- f444(x0) = x0 | | | +- f445(x0) = x0 | | | +- f446(x0) = x0 | | | +- f447(x0) = x0 | | | +- f448(x0) = x0 | | | +- f449(x0) = x0 | | | +- f453(x0) = x0 | | | +- f454(x0) = x0 | | | +- f455(x0) = x0 | | | +- f458(x0) = x0 | | | +- f460(x0) = x0 | | | +- f463(x0) = x0 | | | +- f464(x0) = x0 | | | +- f468(x0) = x0 | | | +- f469(x0) = x0 | | | +- f470(x0) = x0 | | | +- f473(x0) = x0 | | | +- f475(x0) = x0 | | | +- f478(x0) = x0 | | | +- f6(x0,x1,x2,x3) = 0 | | | `- f7(x0,x1,x2,x3,x4) = 0 | +- Constraints | | | +- f416(x5) = x5 >= x5 = x5 | | | +- f417(x5) = x5 >= x5 = f416(x5) | | | +- f418(x4) = x4 >= x4 = x4 | | | +- f419(x5) = x5 >= x5 = f417(x5) | | | +- f420(x101) = x101 >= x101 = x101 | | | +- f421(x99) = x99 >= x99 = x99 | | | +- f422(x100) = x100 >= x100 = x100 | | | +- f8(x99,f423(x4)) = f8(x99,f423(x4)) >= f19(x4,x99) = f19(f418(x4),f421(x99)) | | | +- f9(x99,f423(x4)) + x100 = f9(x99,f423(x4)) + x100 >= f20(x4,x99) + x100 = f20(f418(x4),f421(x99)) + f422(x100) | | | +- f10(x99,f423(x4),x100) + x101 = f10(x99,f423(x4),x100) + x101 >= x101 = f21(f418(x4),f421(x99),f422(x100)) + f420(x101) | | | +- f424(x4,x5,x99,x100,x101) = x5 >= x5 = f22(f418(x4),f421(x99),f422(x100),f420(x101)) + f419(x5) | | | +- f425(x3,x4,x5,x99,x100,x101) = x5 >= x5 = f14(f423(x4),f426(),f427(x3),f428(x3,x4,x5,x99,x100,x101),f429(x3,x4,x5,x99,x100,x101)) + f424(x4,x5,x99,x100,x101) | | | +- f426() = 0 >= 0 = 0 | | | +- f429(x3,x4,x5,x99,x100,x101) = x5 >= x5 = f425(x3,x4,x5,x99,x100,x101) | | | +- f427(x3) = x3 >= x3 = x3 | | | +- f428(x3,x4,x5,x99,x100,x101) = x5 >= x5 = f13(f423(x4),f426(),f427(x3),f428(x3,x4,x5,x99,x100,x101)) + f429(x3,x4,x5,x99,x100,x101) | | | +- f430(x3,x4,x5,x99,x100,x101) = f430(x3,x4,x5,x99,x100,x101) >= f12(f423(x4),0,x3) + x5 = f12(f423(x4),f426(),f427(x3)) + f428(x3,x4,x5,x99,x100,x101) | | | +- f23(x3,x4) = f23(x3,x4) >= f11(f423(x4),0,x3) = f11(f423(x4),f426(),f427(x3)) | | | +- f24(x3,x4) + x5 = f24(x3,x4) + x5 >= f430(x3,x4,x5,x99,x100,x101) + 1 = f430(x3,x4,x5,x99,x100,x101) + 1 | | | +- f431(x10) = x10 >= x10 = x10 | | | +- f432(x10) = x10 >= x10 = f431(x10) | | | +- f433(x10) = x10 >= x10 = f432(x10) | | | +- f434(x173) = x173 >= x173 = x173 | | | +- f435(x171) = x171 >= x171 = x171 | | | +- f436(x172) = x172 >= x172 = x172 | | | +- f1(x171,f437()) = f1(x171,f437()) >= x171 + 1 = f15(f435(x171)) | | | +- f2(x171,f437()) + x172 = f2(x171,f437()) + x172 >= f16(x171) + x172 = f16(f435(x171)) + f436(x172) | | | +- f3(x171,f437(),x172) + x173 = f3(x171,f437(),x172) + x173 >= x173 = f17(f435(x171),f436(x172)) + f434(x173) | | | +- f438(x10,x171,x172,x173) = x10 >= x10 = f18(f435(x171),f436(x172),f434(x173)) + f433(x10) | | | +- f439(x9) = x9 >= x9 = x9 | | | +- f440(x8,x9,x10,x171,x172,x173) = x10 >= x10 = f7(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173),f440(x8,x9,x10,x171,x172,x173)) + f438(x10,x171,x172,x173) | | | +- f441(x8) = x8 >= x8 = x8 | | | +- f442(x8,x9,x10,x171,x172,x173) = x10 >= x10 = f6(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173)) + f440(x8,x9,x10,x171,x172,x173) | | | +- f443(x8,x9,x10,x171,x172,x173) = f443(x8,x9,x10,x171,x172,x173) >= f5(f437(),x9,x8) + x10 = f5(f437(),f439(x9),f441(x8)) + f442(x8,x9,x10,x171,x172,x173) | | | +- f19(x8,x9) = f19(x8,x9) >= f4(f437(),x9,x8) = f4(f437(),f439(x9),f441(x8)) | | | +- f20(x8,x9) + x10 = f20(x8,x9) + x10 >= f443(x8,x9,x10,x171,x172,x173) + 1 = f443(x8,x9,x10,x171,x172,x173) + 1 | | | +- f444(x14) = x14 >= x14 = x14 | | | +- f445(x14) = x14 >= x14 = f444(x14) | | | +- f446(x13) = x13 >= x13 = x13 | | | +- f447(x14) = x14 >= x14 = f445(x14) | | | +- f448(x14) = x14 >= x14 = f447(x14) | | | +- f15(x13) = x13 + 1 >= x13 + 1 = f446(x13) + 1 | | | +- f16(x13) + x14 = f16(x13) + x14 >= x14 + 1 = f448(x14) + 1 | | | +- f449(x20) = x20 >= x20 = x20 | | | +- f450(x17,x18,x20,x22,x242,x243,x244) = f450(x17,x18,x20,x22,x242,x243,x244) >= f3(f451(x17,x18,x22,x242,x243,x244),x17,f452(x17,x18,x20,x22,x242,x243,x244)) + x20 = f3(f451(x17,x18,x22,x242,x243,x244) ,x17 ,f452(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244)) + f449(x20) | | | +- f453(x244) = x244 >= x244 = x244 | | | +- f454(x242) = x242 >= x242 = x242 | | | +- f455(x243) = x243 >= x243 = x243 | | | +- f1(x242,f456(x17)) = f1(x242,f456(x17)) >= f1(x242,x17) = f1(f454(x242),x17) | | | +- f2(x242,f456(x17)) + x243 = f2(x242,f456(x17)) + x243 >= f2(x242,x17) + x243 = f2(f454(x242),x17) + f455(x243) | | | +- f3(x242,f456(x17),x243) + x244 = f3(x242,f456(x17),x243) + x244 >= f3(x242,x17,x243) + x244 = f3(f454(x242),x17,f455(x243)) + f453(x244) | | | +- f457(x17,x18,x20,x22,x242,x243,x244) = f457(x17,x18,x20,x22,x242,x243,x244) >= f450(x17,x18,x20,x22,x242,x243,x244) = f450(x17,x18,x20,x22,x242,x243,x244) | | | +- f458(x18) = x18 >= x18 = x18 | | | +- f459(x17,x18,x20,x22,x242,x243,x244) = f459(x17,x18,x20,x22,x242,x243,x244) >= f457(x17,x18,x20,x22,x242,x243,x244) = f7(f456(x17) ,f458(x18) ,f460(x22) ,f461(x17,x18,x20,x22,x242,x243,x244) ,f459(x17,x18,x20,x22,x242,x243,x244)) + f457(x17,x18,x20,x22,x242,x243,x244) | | | +- f460(x22) = x22 >= x22 = x22 | | | +- f461(x17,x18,x20,x22,x242,x243,x244) = f461(x17,x18,x20,x22,x242,x243,x244) >= f459(x17,x18,x20,x22,x242,x243,x244) = f6(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244)) + f459(x17,x18,x20,x22,x242,x243,x244) | | | +- f451(x17,x18,x22,x242,x243,x244) = f451(x17,x18,x22,x242,x243,x244) >= f4(f456(x17),x18,x22) = f4(f456(x17),f458(x18),f460(x22)) | | | +- f452(x17,x18,x20,x22,x242,x243,x244) = f452(x17,x18,x20,x22,x242,x243,x244) >= f5(f456(x17),x18,x22) + f461(x17,x18,x20,x22,x242,x243,x244) = f5(f456(x17),f458(x18),f460(x22)) + f461(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) | | | +- f462(x17,x18,x20,x22,x242,x243,x244) = f462(x17,x18,x20,x22,x242,x243,x244) >= f2(f451(x17,x18,x22,x242,x243,x244),x17) + f452(x17,x18,x20,x22,x242,x243,x244) = f2(f451(x17,x18,x22,x242,x243,x244) ,x17) + f452(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) | | | +- f4(x17,x18,x22 + 1) = f4(x17,x18,x22 + 1) >= f1(f451(x17,x18,x22,x242,x243,x244),x17) = f1(f451(x17,x18,x22,x242,x243,x244),x17) | | | +- f5(x17,x18,x22 + 1) + x20 = f5(x17,x18,x22 + 1) + x20 >= f462(x17,x18,x20,x22,x242,x243,x244) + 1 = f462(x17,x18,x20,x22,x242,x243,x244) + 1 | | | +- f463(x31) = x31 >= x31 = x31 | | | +- f4(x28,x29,0) = f4(x28,x29,0) >= x29 = x29 | | | +- f5(x28,x29,0) + x31 = f5(x28,x29,0) + x31 >= x31 + 1 = f463(x31) + 1 | | | +- f464(x41) = x41 >= x41 = x41 | | | +- f465(x38,x39,x41,x43,x346,x347,x348) = f465(x38,x39,x41,x43,x346,x347,x348) >= f10(f466(x38,x39,x43,x346,x347,x348),x38,f467(x38,x39,x41,x43,x346,x347,x348)) + x41 = f10(f466(x38 ,x39 ,x43 ,x346 ,x347 ,x348) ,x38 ,f467(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348)) + f464(x41) | | | +- f468(x348) = x348 >= x348 = x348 | | | +- f469(x346) = x346 >= x346 = x346 | | | +- f470(x347) = x347 >= x347 = x347 | | | +- f8(x346,f471(x38)) = f8(x346,f471(x38)) >= f8(x346,x38) = f8(f469(x346),x38) | | | +- f9(x346,f471(x38)) + x347 = f9(x346,f471(x38)) + x347 >= f9(x346,x38) + x347 = f9(f469(x346),x38) + f470(x347) | | | +- f10(x346,f471(x38),x347) + x348 = f10(x346,f471(x38),x347) + x348 >= f10(x346,x38,x347) + x348 = f10(f469(x346),x38,f470(x347)) + f468(x348) | | | +- f472(x38,x39,x41,x43,x346,x347,x348) = f472(x38,x39,x41,x43,x346,x347,x348) >= f465(x38,x39,x41,x43,x346,x347,x348) = f465(x38,x39,x41,x43,x346,x347,x348) | | | +- f473(x39) = x39 >= x39 = x39 | | | +- f474(x38,x39,x41,x43,x346,x347,x348) = f474(x38,x39,x41,x43,x346,x347,x348) >= f472(x38,x39,x41,x43,x346,x347,x348) = f14(f471(x38) ,f473(x39) ,f475(x43) ,f476(x38,x39,x41,x43,x346,x347,x348) ,f474(x38,x39,x41,x43,x346,x347,x348)) + f472(x38,x39,x41,x43,x346,x347,x348) | | | +- f475(x43) = x43 >= x43 = x43 | | | +- f476(x38,x39,x41,x43,x346,x347,x348) = f476(x38,x39,x41,x43,x346,x347,x348) >= f474(x38,x39,x41,x43,x346,x347,x348) = f13(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348)) + f474(x38,x39,x41,x43,x346,x347,x348) | | | +- f466(x38,x39,x43,x346,x347,x348) = f466(x38,x39,x43,x346,x347,x348) >= f11(f471(x38),x39,x43) = f11(f471(x38),f473(x39),f475(x43)) | | | +- f467(x38,x39,x41,x43,x346,x347,x348) = f467(x38,x39,x41,x43,x346,x347,x348) >= f12(f471(x38),x39,x43) + f476(x38,x39,x41,x43,x346,x347,x348) = f12(f471(x38),f473(x39),f475(x43)) + f476(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348) | | | +- f477(x38,x39,x41,x43,x346,x347,x348) = f477(x38,x39,x41,x43,x346,x347,x348) >= f9(f466(x38,x39,x43,x346,x347,x348),x38) + f467(x38,x39,x41,x43,x346,x347,x348) = f9(f466(x38,x39,x43,x346,x347,x348) ,x38) + f467(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348) | | | +- f11(x38,x39,x43 + 1) = f11(x38,x39,x43 + 1) >= f8(f466(x38,x39,x43,x346,x347,x348),x38) = f8(f466(x38,x39,x43,x346,x347,x348),x38) | | | +- f12(x38,x39,x43 + 1) + x41 = f12(x38,x39,x43 + 1) + x41 >= f477(x38,x39,x41,x43,x346,x347,x348) + 1 = f477(x38,x39,x41,x43,x346,x347,x348) + 1 | | | +- f478(x52) = x52 >= x52 = x52 | | | +- f11(x49,x50,0) = f11(x49,x50,0) >= x50 = x50 | | | `- f12(x49,x50,0) + x52 = f12(x49,x50,0) + x52 >= x52 + 1 = f478(x52) + 1 | +- SCC-DECOMPOSE ... | | | +- SCC: 13 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:39.606162 UTC | | | +- Open Constraints | | | | | `- f16(0) + x14 = f16(0) + x14 >= x14 + 1 = x14 + 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.606212 UTC | | | | | +- Interpretation | | | | | | | `- f16(x0) = 16 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f16(x0) = 1 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:39.612358 UTC(+0.006146s) | | | +- Interpretation | | | | | `- f16(x0) = 1 | | | +- Constraints | | | | | `- f16(0) + x14 = 1 + x14 >= x14 + 1 = x14 + 1 | | | `- Stopping timer: 2017-03-30 07:40:39.612436 UTC(+0.006274s) | +- SCC-DECOMPOSE ... | | | +- SCC: 12 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:39.616706 UTC | | | +- Open Constraints | | | | | +- f2(x171,f437()) + x172 = f2(x171,f437()) + x172 >= 1 + x172 = f16(x171) + x172 | | | | | +- f3(x171,f437(),x172) + x173 = f3(x171,f437(),x172) + x173 >= x173 = x173 | | | | | +- f3(x242,f456(x17),x243) + x244 = f3(x242,f456(x17),x243) + x244 >= f3(x242,x17,x243) + x244 = f3(x242,x17,x243) + x244 | | | | | +- f2(x242,f456(x17)) + x243 = f2(x242,f456(x17)) + x243 >= f2(x242,x17) + x243 = f2(x242,x17) + x243 | | | | | +- f1(x242,f456(x17)) = f1(x242,f456(x17)) >= f1(x242,x17) = f1(x242,x17) | | | | | `- f1(x171,f437()) = f1(x171,f437()) >= x171 + 1 = x171 + 1 | | | +- Simplification ... | | | | | `- Substituted: f3(x171,f437(),x172) + x173 ≥ x173 ↦ f3(0,f437(),0) + x173 ≥ x173 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.616826 UTC | | | | | +- Interpretation | | | | | | | +- f1(x0,x1) = max(14 + x0,15 + x1) | | | | | | | +- f2(x0,x1) = max(7 + x1,7 + x0) | | | | | | | +- f3(x0,x1,x2) = max(12 + x1,10 + x1 + x2,x0) | | | | | | | +- f437() = 0 | | | | | | | `- f456(x0) = 15 + x0 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f1(x0,x1) = 1 + x0 | | | | | | | +- f2(x0,x1) = 1 | | | | | | | +- f3(x0,x1,x2) = 0 | | | | | | | +- f437() = 0 | | | | | | | `- f456(x0) = 1 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f1(x0,x1) = 1 + x0 | | | | | | | +- f2(x0,x1) = 1 | | | | | | | +- f3(x0,x1,x2) = 0 | | | | | | | +- f437() = 0 | | | | | | | `- f456(x0) = 0 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:39.645489 UTC(+0.028663s) | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f16(x0) = 1 | | | | | +- f2(x0,x1) = 1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f437() = 0 | | | | | `- f456(x0) = 0 | | | +- Constraints | | | | | +- f2(x171,f437()) + x172 = 1 + x172 >= 1 + x172 = f16(x171) + x172 | | | | | +- f3(x171,f437(),x172) + x173 = x173 >= x173 = x173 | | | | | +- f3(x242,f456(x17),x243) + x244 = x244 >= x244 = f3(x242,x17,x243) + x244 | | | | | +- f2(x242,f456(x17)) + x243 = 1 + x243 >= 1 + x243 = f2(x242,x17) + x243 | | | | | +- f1(x242,f456(x17)) = 1 + x242 >= 1 + x242 = f1(x242,x17) | | | | | `- f1(x171,f437()) = 1 + x171 >= x171 + 1 = x171 + 1 | | | `- Stopping timer: 2017-03-30 07:40:39.645586 UTC(+0.02888s) | +- SCC-DECOMPOSE ... | | | +- SCC: 11 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:39.647095 UTC | | | +- Open Constraints | | | | | +- f4(x17,x18,x22 + 1) = f4(x17,x18,x22 + 1) >= 1 + f451(x17,x18,x22,x242,x243,x244) = f1(f451(x17,x18,x22,x242,x243,x244),x17) | | | | | +- f4(0,x29,0) = f4(0,x29,0) >= x29 = x29 | | | | | `- f451(x17,x18,x22,0,0,0) = f451(x17,x18,x22,0,0,0) >= f4(0,x18,x22) = f4(f456(x17),x18,x22) | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.647213 UTC | | | | | +- Interpretation | | | | | | | +- f4(x0,x1,x2) = max(10 + x2,4 + x0,7 + x1 + x2) | | | | | | | `- f451(x0,x1,x2,x3,x4,x5) = max(10 + x2,7 + x1 + x2) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f4(x0,x1,x2) = x1 + x2 | | | | | | | `- f451(x0,x1,x2,x3,x4,x5) = x1 + x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:39.676999 UTC(+0.029786s) | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f4(x0,x1,x2) = x1 + x2 | | | | | +- f451(x0,x1,x2,x3,x4,x5) = x1 + x2 | | | | | `- f456(x0) = 0 | | | +- Constraints | | | | | +- f4(x17,x18,x22 + 1) = x18 + (x22 + 1) >= 1 + (x18 + x22) = f1(f451(x17,x18,x22,x242,x243,x244),x17) | | | | | +- f4(0,x29,0) = x29 >= x29 = x29 | | | | | `- f451(x17,x18,x22,0,0,0) = x18 + x22 >= x18 + x22 = f4(f456(x17),x18,x22) | | | `- Stopping timer: 2017-03-30 07:40:39.677058 UTC(+0.029963s) | +- SCC-DECOMPOSE ... | | | +- SCC: 10 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:39.678273 UTC | | | +- Open Constraints | | | | | `- f19(x8,x9) = f19(x8,x9) >= x9 + x8 = f4(f437(),x9,x8) | | | +- Simplification ... | | | | | `- Propagated: f19(x0,x1) ↦ x0 + x1 | | | +- Interpretation | | | | | +- f19(x0,x1) = x0 + x1 | | | | | +- f4(x0,x1,x2) = x1 + x2 | | | | | `- f437() = 0 | | | +- Constraints | | | | | `- f19(x8,x9) = x9 + x8 >= x9 + x8 = f4(f437(),x9,x8) | | | `- Stopping timer: 2017-03-30 07:40:39.678347 UTC(+0.000074s) | +- SCC-DECOMPOSE ... | | | +- SCC: 9 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:39.679413 UTC | | | +- Open Constraints | | | | | +- f450(x17,x18,x20,x22,x242,x243,x244) = f450(x17,x18,x20,x22,x242,x243,x244) >= x20 = f3(f451(x17,x18,x22,x242,x243,x244),x17,f452(x17,x18,x20,x22,x242,x243,x244)) + x20 | | | | | +- f452(x17,x18,x20,x22,x242,x243,x244) = f452(x17,x18,x20,x22,x242,x243,x244) >= f5(0,x18,x22) + f461(x17,x18,x20,x22,x242,x243,x244) = f5(f456(x17),x18,x22) + f461(x17,x18,x20,x22,x242,x243,x244) | | | | | +- f5(x17,x18,x22 + 1) + x20 = f5(x17,x18,x22 + 1) + x20 >= f462(x17,x18,x20,x22,x242,x243,x244) + 1 = f462(x17,x18,x20,x22,x242,x243,x244) + 1 | | | | | +- f462(x17,x18,x20,x22,x242,x243,x244) = f462(x17,x18,x20,x22,x242,x243,x244) >= 1 + f452(x17,x18,x20,x22,x242,x243,x244) = f2(f451(x17,x18,x22,x242,x243,x244),x17) + f452(x17 ,x18 ,x20 ,x22 ,x242 ,x243 ,x244) | | | | | +- f5(0,0,0) + x31 = f5(0,0,0) + x31 >= x31 + 1 = x31 + 1 | | | | | +- f461(x17,x18,x20,x22,x242,x243,x244) = f461(x17,x18,x20,x22,x242,x243,x244) >= f459(x17,x18,x20,x22,x242,x243,x244) = f459(x17,x18,x20,x22,x242,x243,x244) | | | | | +- f459(x17,x18,x20,x22,x242,x243,x244) = f459(x17,x18,x20,x22,x242,x243,x244) >= f457(x17,x18,x20,x22,x242,x243,x244) = f457(x17,x18,x20,x22,x242,x243,x244) | | | | | `- f457(x17,x18,x20,x22,x242,x243,x244) = f457(x17,x18,x20,x22,x242,x243,x244) >= f450(x17,x18,x20,x22,x242,x243,x244) = f450(x17,x18,x20,x22,x242,x243,x244) | | | +- Simplification ... | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.880138 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:39.891682 UTC(+0.011544s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.891691 UTC | | | | | +- Interpretation | | | | | | | +- f450(x0,x1,x2,x3,x4,x5,x6) = x0 + x2 | | | | | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 7 + 14*x0 + 5*x1 + x2 + 11*x3 | | | | | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = 12*x0 + x2 | | | | | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = 14*x0 + x2 | | | | | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = 14*x0 + x2 | | | | | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 8 + 14*x0 + 5*x1 + x2 + 11*x3 | | | | | | | `- f5(x0,x1,x2) = 1 + 14*x0 + 5*x1 + 11*x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f450(x0,x1,x2,x3,x4,x5,x6) = x0 + x2 | | | | | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x0 + x2 + 2*x3 | | | | | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = x0 + x2 | | | | | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = x0 + x2 | | | | | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = x0 + x2 | | | | | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 2 + x0 + x2 + 2*x3 | | | | | | | `- f5(x0,x1,x2) = 1 + x0 + 2*x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f450(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x0 + x2 + 2*x3 | | | | | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = x0 + x2 | | | | | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = x0 + x2 | | | | | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = x0 + x2 | | | | | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 2 + x0 + x2 + 2*x3 | | | | | | | `- f5(x0,x1,x2) = 1 + x0 + 2*x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f450(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 + 2*x3 | | | | | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 2 + x2 + 2*x3 | | | | | | | `- f5(x0,x1,x2) = 1 + 2*x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:39.95277 UTC(+0.061079s) | | | +- Interpretation | | | | | +- f2(x0,x1) = 1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f450(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f451(x0,x1,x2,x3,x4,x5) = x1 + x2 | | | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 + 2*x3 | | | | | +- f456(x0) = 0 | | | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 2 + x2 + 2*x3 | | | | | `- f5(x0,x1,x2) = 1 + 2*x2 | | | +- Constraints | | | | | +- f450(x17,x18,x20,x22,x242,x243,x244) = x20 >= x20 = f3(f451(x17,x18,x22,x242,x243,x244),x17,f452(x17,x18,x20,x22,x242,x243,x244)) + x20 | | | | | +- f452(x17,x18,x20,x22,x242,x243,x244) = 1 + (x20 + (2 * x22)) >= (1 + (2 * x22)) + x20 = f5(f456(x17),x18,x22) + f461(x17,x18,x20,x22,x242,x243,x244) | | | | | +- f5(x17,x18,x22 + 1) + x20 = (1 + (2 * (x22 + 1))) + x20 >= (2 + (x20 + (2 * x22))) + 1 = f462(x17,x18,x20,x22,x242,x243,x244) + 1 | | | | | +- f462(x17,x18,x20,x22,x242,x243,x244) = 2 + (x20 + (2 * x22)) >= 1 + (1 + (x20 + (2 * x22))) = f2(f451(x17,x18,x22,x242,x243,x244),x17) + f452(x17,x18,x20,x22,x242,x243,x244) | | | | | +- f5(0,0,0) + x31 = 1 + x31 >= x31 + 1 = x31 + 1 | | | | | +- f461(x17,x18,x20,x22,x242,x243,x244) = x20 >= x20 = f459(x17,x18,x20,x22,x242,x243,x244) | | | | | +- f459(x17,x18,x20,x22,x242,x243,x244) = x20 >= x20 = f457(x17,x18,x20,x22,x242,x243,x244) | | | | | `- f457(x17,x18,x20,x22,x242,x243,x244) = x20 >= x20 = f450(x17,x18,x20,x22,x242,x243,x244) | | | `- Stopping timer: 2017-03-30 07:40:39.952869 UTC(+0.273456s) | +- SCC-DECOMPOSE ... | | | +- SCC: 8 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:39.95353 UTC | | | +- Open Constraints | | | | | `- f443(x8,x9,x10,x171,x172,x173) = f443(x8,x9,x10,x171,x172,x173) >= (1 + (2 * x8)) + x10 = f5(f437(),x9,x8) + x10 | | | +- Simplification ... | | | | | `- Substituted: f443(x8,x9,x10,x171,x172,x173) ≥ f5(f437(),x9,x8) + x10 ↦ f443(x8,x9,x10,0,0,0) ≥ f5(f437(),x9,x8) + x10 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.953602 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:39.961231 UTC(+0.007629s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.961244 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:39.966665 UTC(+0.005421s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.966671 UTC | | | | | +- Interpretation | | | | | | | `- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + 16*x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:39.974838 UTC(+0.008167s) | | | +- Interpretation | | | | | +- f437() = 0 | | | | | +- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | | | `- f5(x0,x1,x2) = 1 + 2*x2 | | | +- Constraints | | | | | `- f443(x8,x9,x10,x171,x172,x173) = 1 + ((2 * x8) + x10) >= (1 + (2 * x8)) + x10 = f5(f437(),x9,x8) + x10 | | | `- Stopping timer: 2017-03-30 07:40:39.974889 UTC(+0.021359s) | +- SCC-DECOMPOSE ... | | | +- SCC: 7 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:39.975477 UTC | | | +- Open Constraints | | | | | `- f20(x8,x9) + x10 = f20(x8,x9) + x10 >= (1 + ((2 * x8) + x10)) + 1 = f443(x8,x9,x10,x171,x172,x173) + 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.975544 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:39.980253 UTC(+0.004709s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.980266 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:39.984118 UTC(+0.003852s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.984125 UTC | | | | | +- Interpretation | | | | | | | `- f20(x0,x1) = 16 + 8*x0 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f20(x0,x1) = 2 + 2*x0 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:39.98959 UTC(+0.005465s) | | | +- Interpretation | | | | | +- f20(x0,x1) = 2 + 2*x0 | | | | | `- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | +- Constraints | | | | | `- f20(x8,x9) + x10 = (2 + (2 * x8)) + x10 >= (1 + ((2 * x8) + x10)) + 1 = f443(x8,x9,x10,x171,x172,x173) + 1 | | | `- Stopping timer: 2017-03-30 07:40:39.989638 UTC(+0.014161s) | +- SCC-DECOMPOSE ... | | | +- SCC: 6 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:39.99019 UTC | | | +- Open Constraints | | | | | +- f9(x99,f423(x4)) + x100 = f9(x99,f423(x4)) + x100 >= (2 + (2 * x4)) + x100 = f20(x4,x99) + x100 | | | | | +- f8(x99,f423(x4)) = f8(x99,f423(x4)) >= x99 + x4 = f19(x4,x99) | | | | | +- f10(x99,f423(x4),x100) + x101 = f10(x99,f423(x4),x100) + x101 >= x101 = x101 | | | | | +- f10(x346,f471(x38),x347) + x348 = f10(x346,f471(x38),x347) + x348 >= f10(x346,x38,x347) + x348 = f10(x346,x38,x347) + x348 | | | | | +- f9(x346,f471(x38)) + x347 = f9(x346,f471(x38)) + x347 >= f9(x346,x38) + x347 = f9(x346,x38) + x347 | | | | | `- f8(x346,f471(x38)) = f8(x346,f471(x38)) >= f8(x346,x38) = f8(x346,x38) | | | +- Simplification ... | | | | | `- Substituted: f10(x99,f423(x4),x100) + x101 ≥ x101 ↦ f10(0,f423(0),0) + x101 ≥ x101 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:39.990294 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.003587 UTC(+0.013293s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.003618 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.00977 UTC(+0.006152s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.009777 UTC | | | | | +- Interpretation | | | | | | | +- f10(x0,x1,x2) = 0 | | | | | | | +- f423(x0) = 9 + 11*x0 | | | | | | | +- f471(x0) = x0 | | | | | | | +- f8(x0,x1) = 16*x0 + 5*x1 | | | | | | | `- f9(x0,x1) = 5 + 15*x1 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f10(x0,x1,x2) = 0 | | | | | | | +- f423(x0) = 1 + x0 | | | | | | | +- f471(x0) = x0 | | | | | | | +- f8(x0,x1) = x0 + x1 | | | | | | | `- f9(x0,x1) = 2*x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:40.020335 UTC(+0.010558s) | | | +- Interpretation | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f19(x0,x1) = x0 + x1 | | | | | +- f20(x0,x1) = 2 + 2*x0 | | | | | +- f423(x0) = 1 + x0 | | | | | +- f471(x0) = x0 | | | | | +- f8(x0,x1) = x0 + x1 | | | | | `- f9(x0,x1) = 2*x1 | | | +- Constraints | | | | | +- f9(x99,f423(x4)) + x100 = (2 * (1 + x4)) + x100 >= (2 + (2 * x4)) + x100 = f20(x4,x99) + x100 | | | | | +- f8(x99,f423(x4)) = x99 + (1 + x4) >= x99 + x4 = f19(x4,x99) | | | | | +- f10(x99,f423(x4),x100) + x101 = x101 >= x101 = x101 | | | | | +- f10(x346,f471(x38),x347) + x348 = x348 >= x348 = f10(x346,x38,x347) + x348 | | | | | +- f9(x346,f471(x38)) + x347 = (2 * x38) + x347 >= (2 * x38) + x347 = f9(x346,x38) + x347 | | | | | `- f8(x346,f471(x38)) = x346 + x38 >= x346 + x38 = f8(x346,x38) | | | `- Stopping timer: 2017-03-30 07:40:40.02041 UTC(+0.03022s) | +- SCC-DECOMPOSE ... | | | +- SCC: 5 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:40.02068 UTC | | | +- Open Constraints | | | | | +- f466(x38,x39,x43,0,0,0) = f466(x38,x39,x43,0,0,0) >= f11(x38,x39,x43) = f11(f471(x38),x39,x43) | | | | | +- f11(x38,x39,x43 + 1) = f11(x38,x39,x43 + 1) >= f466(x38,x39,x43,x346,x347,x348) + x38 = f8(f466(x38,x39,x43,x346,x347,x348),x38) | | | | | `- f11(0,x50,0) = f11(0,x50,0) >= x50 = x50 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.020792 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.034328 UTC(+0.013536s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.03434 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.039075 UTC(+0.004735s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.039082 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.043711 UTC(+0.004629s) | | | +- SMT-MMI(2) ... | | | | | +- Staring timer: 2017-03-30 07:40:40.043717 UTC | | | | | +- Interpretation | | | | | | | +- f11(x0,x1,x2) = 7 + 8*x0 + 14*x0*x1 + 14*x0*x2 + 8*x1 + 14*x1*x2 + 15*x2 | | | | | | | `- f466(x0,x1,x2,x3,x4,x5) = 8 + 15*x0 + 14*x0*x1 + 14*x0*x2 + 15*x1 + 14*x1*x2 + 15*x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f11(x0,x1,x2) = 1 + x0*x2 + x1 | | | | | | | `- f466(x0,x1,x2,x3,x4,x5) = 1 + x0*x2 + x1 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | | | | | `- f466(x0,x1,x2,x3,x4,x5) = x0*x2 + x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:40.069014 UTC(+0.025297s) | | | +- Interpretation | | | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | | | +- f466(x0,x1,x2,x3,x4,x5) = x0*x2 + x1 | | | | | +- f471(x0) = x0 | | | | | `- f8(x0,x1) = x0 + x1 | | | +- Constraints | | | | | +- f466(x38,x39,x43,0,0,0) = (x38 * x43) + x39 >= (x38 * x43) + x39 = f11(f471(x38),x39,x43) | | | | | +- f11(x38,x39,x43 + 1) = (x38 * (x43 + 1)) + x39 >= ((x38 * x43) + x39) + x38 = f8(f466(x38,x39,x43,x346,x347,x348),x38) | | | | | `- f11(0,x50,0) = x50 >= x50 = x50 | | | `- Stopping timer: 2017-03-30 07:40:40.069068 UTC(+0.048388s) | +- SCC-DECOMPOSE ... | | | +- SCC: 4 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:40.069223 UTC | | | +- Open Constraints | | | | | +- f465(x38,x39,x41,x43,x346,x347,x348) = f465(x38,x39,x41,x43,x346,x347,x348) >= x41 = f10(f466(x38,x39,x43,x346,x347,x348),x38,f467(x38,x39,x41,x43,x346,x347,x348)) + x41 | | | | | +- f467(x38,x39,x41,x43,x346,x347,x348) = f467(x38,x39,x41,x43,x346,x347,x348) >= f12(x38,x39,x43) + f476(x38,x39,x41,x43,x346,x347,x348) = f12(f471(x38),x39,x43) + f476(x38,x39,x41,x43,x346,x347,x348) | | | | | +- f12(x38,x39,x43 + 1) + x41 = f12(x38,x39,x43 + 1) + x41 >= f477(x38,x39,x41,x43,x346,x347,x348) + 1 = f477(x38,x39,x41,x43,x346,x347,x348) + 1 | | | | | +- f477(x38,x39,x41,x43,x346,x347,x348) = f477(x38,x39,x41,x43,x346,x347,x348) >= (2 * x38) + f467(x38,x39,x41,x43,x346,x347,x348) = f9(f466(x38,x39,x43,x346,x347,x348),x38) + f467(x38 ,x39 ,x41 ,x43 ,x346 ,x347 ,x348) | | | | | +- f12(0,0,0) + x52 = f12(0,0,0) + x52 >= x52 + 1 = x52 + 1 | | | | | +- f476(x38,x39,x41,x43,x346,x347,x348) = f476(x38,x39,x41,x43,x346,x347,x348) >= f474(x38,x39,x41,x43,x346,x347,x348) = f474(x38,x39,x41,x43,x346,x347,x348) | | | | | +- f474(x38,x39,x41,x43,x346,x347,x348) = f474(x38,x39,x41,x43,x346,x347,x348) >= f472(x38,x39,x41,x43,x346,x347,x348) = f472(x38,x39,x41,x43,x346,x347,x348) | | | | | `- f472(x38,x39,x41,x43,x346,x347,x348) = f472(x38,x39,x41,x43,x346,x347,x348) >= f465(x38,x39,x41,x43,x346,x347,x348) = f465(x38,x39,x41,x43,x346,x347,x348) | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.069422 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.114592 UTC(+0.04517s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.114617 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.124174 UTC(+0.009557s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.124233 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.133514 UTC(+0.009281s) | | | +- SMT-MMI(2) ... | | | | | +- Staring timer: 2017-03-30 07:40:40.13352 UTC | | | | | +- Interpretation | | | | | | | +- f12(x0,x1,x2) = 9 + 5*x0 + 8*x0*x1 + 11*x0*x2 + x1 + 6*x1*x2 + x2 | | | | | | | +- f465(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f467(x0,x1,x2,x3,x4,x5,x6) = 9 + 5*x0 + 8*x0*x1 + 11*x0*x3 + 6*x1 + 6*x1*x3 + x2 + x3 | | | | | | | +- f472(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f474(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f476(x0,x1,x2,x3,x4,x5,x6) = x1 + x2 | | | | | | | `- f477(x0,x1,x2,x3,x4,x5,x6) = 9 + 9*x0 + 8*x0*x1 + 11*x0*x3 + 6*x1 + 6*x1*x3 + x2 + x3 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f12(x0,x1,x2) = 1 + 2*x0*x2 + x2 | | | | | | | +- f465(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f467(x0,x1,x2,x3,x4,x5,x6) = 1 + 2*x0*x3 + x2 + x3 | | | | | | | +- f472(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f474(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | +- f476(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | | | `- f477(x0,x1,x2,x3,x4,x5,x6) = 1 + 2*x0 + 2*x0*x3 + x2 + x3 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:40.250615 UTC(+0.117095s) | | | +- Interpretation | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f12(x0,x1,x2) = 1 + 2*x0*x2 + x2 | | | | | +- f465(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f466(x0,x1,x2,x3,x4,x5) = x0*x2 + x1 | | | | | +- f467(x0,x1,x2,x3,x4,x5,x6) = 1 + 2*x0*x3 + x2 + x3 | | | | | +- f471(x0) = x0 | | | | | +- f472(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f474(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f476(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f477(x0,x1,x2,x3,x4,x5,x6) = 1 + 2*x0 + 2*x0*x3 + x2 + x3 | | | | | `- f9(x0,x1) = 2*x1 | | | +- Constraints | | | | | +- f465(x38,x39,x41,x43,x346,x347,x348) = x41 >= x41 = f10(f466(x38,x39,x43,x346,x347,x348),x38,f467(x38,x39,x41,x43,x346,x347,x348)) + x41 | | | | | +- f467(x38,x39,x41,x43,x346,x347,x348) = 1 + ((2 * (x38 * x43)) + (x41 + x43)) >= (1 + ((2 * (x38 * x43)) + x43)) + x41 = f12(f471(x38),x39,x43) + f476(x38,x39,x41,x43,x346,x347,x348) | | | | | +- f12(x38,x39,x43 + 1) + x41 = (1 + ((2 * (x38 * (x43 + 1))) + (x43 + 1))) + x41 >= (1 + ((2 * x38) + ((2 * (x38 * x43)) + (x41 + x43)))) + 1 = f477(x38,x39,x41,x43,x346,x347,x348) + 1 | | | | | +- f477(x38,x39,x41,x43,x346,x347,x348) = 1 + ((2 * x38) + ((2 * (x38 * x43)) + (x41 + x43))) >= (2 * x38) + (1 + ((2 * (x38 * x43)) + (x41 + x43))) = f9(f466(x38,x39,x43,x346,x347,x348),x38) + f467(x38,x39,x41,x43,x346,x347,x348) | | | | | +- f12(0,0,0) + x52 = 1 + x52 >= x52 + 1 = x52 + 1 | | | | | +- f476(x38,x39,x41,x43,x346,x347,x348) = x41 >= x41 = f474(x38,x39,x41,x43,x346,x347,x348) | | | | | +- f474(x38,x39,x41,x43,x346,x347,x348) = x41 >= x41 = f472(x38,x39,x41,x43,x346,x347,x348) | | | | | `- f472(x38,x39,x41,x43,x346,x347,x348) = x41 >= x41 = f465(x38,x39,x41,x43,x346,x347,x348) | | | `- Stopping timer: 2017-03-30 07:40:40.250732 UTC(+0.181509s) | +- SCC-DECOMPOSE ... | | | +- SCC: 3 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:40.250761 UTC | | | +- Open Constraints | | | | | `- f23(x3,x4) = f23(x3,x4) >= (1 + x4) * x3 = f11(f423(x4),0,x3) | | | +- Simplification ... | | | | | `- Propagated: f23(x0,x1) ↦ x0 + x0*x1 | | | +- Interpretation | | | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | | | +- f23(x0,x1) = x0 + x0*x1 | | | | | `- f423(x0) = 1 + x0 | | | +- Constraints | | | | | `- f23(x3,x4) = (1 + x4) * x3 >= (1 + x4) * x3 = f11(f423(x4),0,x3) | | | `- Stopping timer: 2017-03-30 07:40:40.250891 UTC(+0.00013s) | +- SCC-DECOMPOSE ... | | | +- SCC: 2 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:40.250903 UTC | | | +- Open Constraints | | | | | `- f430(x3,x4,x5,x99,x100,x101) = f430(x3,x4,x5,x99,x100,x101) >= (1 + ((2 * ((1 + x4) * x3)) + x3)) + x5 = f12(f423(x4),0,x3) + x5 | | | +- Simplification ... | | | | | `- Substituted: f430(x3,x4,x5,x99,x100,x101) ≥ f12(f423(x4),0,x3) + x5 ↦ f430(x3,x4,x5,0,0,0) ≥ f12(f423(x4),0,x3) + x5 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.250953 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.255535 UTC(+0.004582s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.255545 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.258364 UTC(+0.002819s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.25837 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.261045 UTC(+0.002675s) | | | +- SMT-MMI(2) ... | | | | | +- Staring timer: 2017-03-30 07:40:40.26105 UTC | | | | | +- Interpretation | | | | | | | `- f430(x0,x1,x2,x3,x4,x5) = 8 + 7*x0 + 4*x0*x1 + 15*x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f430(x0,x1,x2,x3,x4,x5) = 1 + 3*x0 + 2*x0*x1 + x2 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:40.273459 UTC(+0.012409s) | | | +- Interpretation | | | | | +- f12(x0,x1,x2) = 1 + 2*x0*x2 + x2 | | | | | +- f423(x0) = 1 + x0 | | | | | `- f430(x0,x1,x2,x3,x4,x5) = 1 + 3*x0 + 2*x0*x1 + x2 | | | +- Constraints | | | | | `- f430(x3,x4,x5,x99,x100,x101) = 1 + ((3 * x3) + ((2 * (x3 * x4)) + x5)) >= (1 + ((2 * ((1 + x4) * x3)) + x3)) + x5 = f12(f423(x4),0,x3) + x5 | | | `- Stopping timer: 2017-03-30 07:40:40.273518 UTC(+0.022615s) | +- SCC-DECOMPOSE ... | | | +- SCC: 1 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:40:40.273535 UTC | | | +- Open Constraints | | | | | `- f24(x3,x4) + x5 = f24(x3,x4) + x5 >= (1 + ((3 * x3) + ((2 * (x3 * x4)) + x5))) + 1 = f430(x3,x4,x5,x99,x100,x101) + 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.273599 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.277419 UTC(+0.00382s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.277429 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.2803 UTC(+0.002871s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:40:40.280305 UTC | | | | | `- Stopping timer: 2017-03-30 07:40:40.282959 UTC(+0.002654s) | | | +- SMT-MMI(2) ... | | | | | +- Staring timer: 2017-03-30 07:40:40.282963 UTC | | | | | +- Interpretation | | | | | | | `- f24(x0,x1) = 6 + 3*x0 + 16*x0*x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f24(x0,x1) = 2 + 3*x0 + 2*x0*x1 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:40:40.288373 UTC(+0.00541s) | | | +- Interpretation | | | | | +- f24(x0,x1) = 2 + 3*x0 + 2*x0*x1 | | | | | `- f430(x0,x1,x2,x3,x4,x5) = 1 + 3*x0 + 2*x0*x1 + x2 | | | +- Constraints | | | | | `- f24(x3,x4) + x5 = (2 + ((3 * x3) + (2 * (x3 * x4)))) + x5 >= (1 + ((3 * x3) + ((2 * (x3 * x4)) + x5))) + 1 = f430(x3,x4,x5,x99,x100,x101) + 1 | | | `- Stopping timer: 2017-03-30 07:40:40.288425 UTC(+0.01489s) | +- Interpretation | | | +- f1(x0,x1) = 1 + x0 | | | +- f10(x0,x1,x2) = 0 | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | +- f12(x0,x1,x2) = 1 + 2*x0*x2 + x2 | | | +- f13(x0,x1,x2,x3) = 0 | | | +- f14(x0,x1,x2,x3,x4) = 0 | | | +- f15(x0) = 1 + x0 | | | +- f16(x0) = 1 | | | +- f17(x0,x1) = 0 | | | +- f18(x0,x1,x2) = 0 | | | +- f19(x0,x1) = x0 + x1 | | | +- f2(x0,x1) = 1 | | | +- f20(x0,x1) = 2 + 2*x0 | | | +- f21(x0,x1,x2) = 0 | | | +- f22(x0,x1,x2,x3) = 0 | | | +- f23(x0,x1) = x0 + x0*x1 | | | +- f24(x0,x1) = 2 + 3*x0 + 2*x0*x1 | | | +- f3(x0,x1,x2) = 0 | | | +- f4(x0,x1,x2) = x1 + x2 | | | +- f416(x0) = x0 | | | +- f417(x0) = x0 | | | +- f418(x0) = x0 | | | +- f419(x0) = x0 | | | +- f420(x0) = x0 | | | +- f421(x0) = x0 | | | +- f422(x0) = x0 | | | +- f423(x0) = 1 + x0 | | | +- f424(x0,x1,x2,x3,x4) = x1 | | | +- f425(x0,x1,x2,x3,x4,x5) = x2 | | | +- f426() = 0 | | | +- f427(x0) = x0 | | | +- f428(x0,x1,x2,x3,x4,x5) = x2 | | | +- f429(x0,x1,x2,x3,x4,x5) = x2 | | | +- f430(x0,x1,x2,x3,x4,x5) = 1 + 3*x0 + 2*x0*x1 + x2 | | | +- f431(x0) = x0 | | | +- f432(x0) = x0 | | | +- f433(x0) = x0 | | | +- f434(x0) = x0 | | | +- f435(x0) = x0 | | | +- f436(x0) = x0 | | | +- f437() = 0 | | | +- f438(x0,x1,x2,x3) = x0 | | | +- f439(x0) = x0 | | | +- f440(x0,x1,x2,x3,x4,x5) = x2 | | | +- f441(x0) = x0 | | | +- f442(x0,x1,x2,x3,x4,x5) = x2 | | | +- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | +- f444(x0) = x0 | | | +- f445(x0) = x0 | | | +- f446(x0) = x0 | | | +- f447(x0) = x0 | | | +- f448(x0) = x0 | | | +- f449(x0) = x0 | | | +- f450(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f451(x0,x1,x2,x3,x4,x5) = x1 + x2 | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 + 2*x3 | | | +- f453(x0) = x0 | | | +- f454(x0) = x0 | | | +- f455(x0) = x0 | | | +- f456(x0) = 0 | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f458(x0) = x0 | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f460(x0) = x0 | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 2 + x2 + 2*x3 | | | +- f463(x0) = x0 | | | +- f464(x0) = x0 | | | +- f465(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f466(x0,x1,x2,x3,x4,x5) = x0*x2 + x1 | | | +- f467(x0,x1,x2,x3,x4,x5,x6) = 1 + 2*x0*x3 + x2 + x3 | | | +- f468(x0) = x0 | | | +- f469(x0) = x0 | | | +- f470(x0) = x0 | | | +- f471(x0) = x0 | | | +- f472(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f473(x0) = x0 | | | +- f474(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f475(x0) = x0 | | | +- f476(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f477(x0,x1,x2,x3,x4,x5,x6) = 1 + 2*x0 + 2*x0*x3 + x2 + x3 | | | +- f478(x0) = x0 | | | +- f5(x0,x1,x2) = 1 + 2*x2 | | | +- f6(x0,x1,x2,x3) = 0 | | | +- f7(x0,x1,x2,x3,x4) = 0 | | | +- f8(x0,x1) = x0 + x1 | | | `- f9(x0,x1) = 2*x1 | +- Constraints | | | +- f416(x5) = x5 >= x5 = x5 | | | +- f417(x5) = x5 >= x5 = f416(x5) | | | +- f418(x4) = x4 >= x4 = x4 | | | +- f419(x5) = x5 >= x5 = f417(x5) | | | +- f420(x101) = x101 >= x101 = x101 | | | +- f421(x99) = x99 >= x99 = x99 | | | +- f422(x100) = x100 >= x100 = x100 | | | +- f8(x99,f423(x4)) = x99 + (1 + x4) >= x99 + x4 = f19(f418(x4),f421(x99)) | | | +- f9(x99,f423(x4)) + x100 = (2 * (1 + x4)) + x100 >= (2 + (2 * x4)) + x100 = f20(f418(x4),f421(x99)) + f422(x100) | | | +- f10(x99,f423(x4),x100) + x101 = x101 >= x101 = f21(f418(x4),f421(x99),f422(x100)) + f420(x101) | | | +- f424(x4,x5,x99,x100,x101) = x5 >= x5 = f22(f418(x4),f421(x99),f422(x100),f420(x101)) + f419(x5) | | | +- f425(x3,x4,x5,x99,x100,x101) = x5 >= x5 = f14(f423(x4),f426(),f427(x3),f428(x3,x4,x5,x99,x100,x101),f429(x3,x4,x5,x99,x100,x101)) + f424(x4,x5,x99,x100,x101) | | | +- f426() = 0 >= 0 = 0 | | | +- f429(x3,x4,x5,x99,x100,x101) = x5 >= x5 = f425(x3,x4,x5,x99,x100,x101) | | | +- f427(x3) = x3 >= x3 = x3 | | | +- f428(x3,x4,x5,x99,x100,x101) = x5 >= x5 = f13(f423(x4),f426(),f427(x3),f428(x3,x4,x5,x99,x100,x101)) + f429(x3,x4,x5,x99,x100,x101) | | | +- f430(x3,x4,x5,x99,x100,x101) = 1 + ((3 * x3) + ((2 * (x3 * x4)) + x5)) >= (1 + ((2 * ((1 + x4) * x3)) + x3)) + x5 = f12(f423(x4),f426(),f427(x3)) + f428(x3,x4,x5,x99,x100,x101) | | | +- f23(x3,x4) = (1 + x4) * x3 >= (1 + x4) * x3 = f11(f423(x4),f426(),f427(x3)) | | | +- f24(x3,x4) + x5 = (2 + ((3 * x3) + (2 * (x3 * x4)))) + x5 >= (1 + ((3 * x3) + ((2 * (x3 * x4)) + x5))) + 1 = f430(x3,x4,x5,x99,x100,x101) + 1 | | | +- f431(x10) = x10 >= x10 = x10 | | | +- f432(x10) = x10 >= x10 = f431(x10) | | | +- f433(x10) = x10 >= x10 = f432(x10) | | | +- f434(x173) = x173 >= x173 = x173 | | | +- f435(x171) = x171 >= x171 = x171 | | | +- f436(x172) = x172 >= x172 = x172 | | | +- f1(x171,f437()) = 1 + x171 >= x171 + 1 = f15(f435(x171)) | | | +- f2(x171,f437()) + x172 = 1 + x172 >= 1 + x172 = f16(f435(x171)) + f436(x172) | | | +- f3(x171,f437(),x172) + x173 = x173 >= x173 = f17(f435(x171),f436(x172)) + f434(x173) | | | +- f438(x10,x171,x172,x173) = x10 >= x10 = f18(f435(x171),f436(x172),f434(x173)) + f433(x10) | | | +- f439(x9) = x9 >= x9 = x9 | | | +- f440(x8,x9,x10,x171,x172,x173) = x10 >= x10 = f7(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173),f440(x8,x9,x10,x171,x172,x173)) + f438(x10,x171,x172,x173) | | | +- f441(x8) = x8 >= x8 = x8 | | | +- f442(x8,x9,x10,x171,x172,x173) = x10 >= x10 = f6(f437(),f439(x9),f441(x8),f442(x8,x9,x10,x171,x172,x173)) + f440(x8,x9,x10,x171,x172,x173) | | | +- f443(x8,x9,x10,x171,x172,x173) = 1 + ((2 * x8) + x10) >= (1 + (2 * x8)) + x10 = f5(f437(),f439(x9),f441(x8)) + f442(x8,x9,x10,x171,x172,x173) | | | +- f19(x8,x9) = x9 + x8 >= x9 + x8 = f4(f437(),f439(x9),f441(x8)) | | | +- f20(x8,x9) + x10 = (2 + (2 * x8)) + x10 >= (1 + ((2 * x8) + x10)) + 1 = f443(x8,x9,x10,x171,x172,x173) + 1 | | | +- f444(x14) = x14 >= x14 = x14 | | | +- f445(x14) = x14 >= x14 = f444(x14) | | | +- f446(x13) = x13 >= x13 = x13 | | | +- f447(x14) = x14 >= x14 = f445(x14) | | | +- f448(x14) = x14 >= x14 = f447(x14) | | | +- f15(x13) = x13 + 1 >= x13 + 1 = f446(x13) + 1 | | | +- f16(x13) + x14 = 1 + x14 >= x14 + 1 = f448(x14) + 1 | | | +- f449(x20) = x20 >= x20 = x20 | | | +- f450(x17,x18,x20,x22,x242,x243,x244) = x20 >= x20 = f3(f451(x17,x18,x22,x242,x243,x244),x17,f452(x17,x18,x20,x22,x242,x243,x244)) + f449(x20) | | | +- f453(x244) = x244 >= x244 = x244 | | | +- f454(x242) = x242 >= x242 = x242 | | | +- f455(x243) = x243 >= x243 = x243 | | | +- f1(x242,f456(x17)) = 1 + x242 >= 1 + x242 = f1(f454(x242),x17) | | | +- f2(x242,f456(x17)) + x243 = 1 + x243 >= 1 + x243 = f2(f454(x242),x17) + f455(x243) | | | +- f3(x242,f456(x17),x243) + x244 = x244 >= x244 = f3(f454(x242),x17,f455(x243)) + f453(x244) | | | +- f457(x17,x18,x20,x22,x242,x243,x244) = x20 >= x20 = f450(x17,x18,x20,x22,x242,x243,x244) | | | +- f458(x18) = x18 >= x18 = x18 | | | +- f459(x17,x18,x20,x22,x242,x243,x244) = x20 >= x20 = f7(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244),f459(x17,x18,x20,x22,x242,x243,x244)) + f457(x17,x18,x20,x22,x242,x243,x244) | | | +- f460(x22) = x22 >= x22 = x22 | | | +- f461(x17,x18,x20,x22,x242,x243,x244) = x20 >= x20 = f6(f456(x17),f458(x18),f460(x22),f461(x17,x18,x20,x22,x242,x243,x244)) + f459(x17,x18,x20,x22,x242,x243,x244) | | | +- f451(x17,x18,x22,x242,x243,x244) = x18 + x22 >= x18 + x22 = f4(f456(x17),f458(x18),f460(x22)) | | | +- f452(x17,x18,x20,x22,x242,x243,x244) = 1 + (x20 + (2 * x22)) >= (1 + (2 * x22)) + x20 = f5(f456(x17),f458(x18),f460(x22)) + f461(x17,x18,x20,x22,x242,x243,x244) | | | +- f462(x17,x18,x20,x22,x242,x243,x244) = 2 + (x20 + (2 * x22)) >= 1 + (1 + (x20 + (2 * x22))) = f2(f451(x17,x18,x22,x242,x243,x244),x17) + f452(x17,x18,x20,x22,x242,x243,x244) | | | +- f4(x17,x18,x22 + 1) = x18 + (x22 + 1) >= 1 + (x18 + x22) = f1(f451(x17,x18,x22,x242,x243,x244),x17) | | | +- f5(x17,x18,x22 + 1) + x20 = (1 + (2 * (x22 + 1))) + x20 >= (2 + (x20 + (2 * x22))) + 1 = f462(x17,x18,x20,x22,x242,x243,x244) + 1 | | | +- f463(x31) = x31 >= x31 = x31 | | | +- f4(x28,x29,0) = x29 >= x29 = x29 | | | +- f5(x28,x29,0) + x31 = 1 + x31 >= x31 + 1 = f463(x31) + 1 | | | +- f464(x41) = x41 >= x41 = x41 | | | +- f465(x38,x39,x41,x43,x346,x347,x348) = x41 >= x41 = f10(f466(x38,x39,x43,x346,x347,x348),x38,f467(x38,x39,x41,x43,x346,x347,x348)) + f464(x41) | | | +- f468(x348) = x348 >= x348 = x348 | | | +- f469(x346) = x346 >= x346 = x346 | | | +- f470(x347) = x347 >= x347 = x347 | | | +- f8(x346,f471(x38)) = x346 + x38 >= x346 + x38 = f8(f469(x346),x38) | | | +- f9(x346,f471(x38)) + x347 = (2 * x38) + x347 >= (2 * x38) + x347 = f9(f469(x346),x38) + f470(x347) | | | +- f10(x346,f471(x38),x347) + x348 = x348 >= x348 = f10(f469(x346),x38,f470(x347)) + f468(x348) | | | +- f472(x38,x39,x41,x43,x346,x347,x348) = x41 >= x41 = f465(x38,x39,x41,x43,x346,x347,x348) | | | +- f473(x39) = x39 >= x39 = x39 | | | +- f474(x38,x39,x41,x43,x346,x347,x348) = x41 >= x41 = f14(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348),f474(x38,x39,x41,x43,x346,x347,x348)) + f472(x38,x39,x41,x43,x346,x347,x348) | | | +- f475(x43) = x43 >= x43 = x43 | | | +- f476(x38,x39,x41,x43,x346,x347,x348) = x41 >= x41 = f13(f471(x38),f473(x39),f475(x43),f476(x38,x39,x41,x43,x346,x347,x348)) + f474(x38,x39,x41,x43,x346,x347,x348) | | | +- f466(x38,x39,x43,x346,x347,x348) = (x38 * x43) + x39 >= (x38 * x43) + x39 = f11(f471(x38),f473(x39),f475(x43)) | | | +- f467(x38,x39,x41,x43,x346,x347,x348) = 1 + ((2 * (x38 * x43)) + (x41 + x43)) >= (1 + ((2 * (x38 * x43)) + x43)) + x41 = f12(f471(x38),f473(x39),f475(x43)) + f476(x38,x39,x41,x43,x346,x347,x348) | | | +- f477(x38,x39,x41,x43,x346,x347,x348) = 1 + ((2 * x38) + ((2 * (x38 * x43)) + (x41 + x43))) >= (2 * x38) + (1 + ((2 * (x38 * x43)) + (x41 + x43))) = f9(f466(x38,x39,x43,x346,x347,x348),x38) + f467(x38,x39,x41,x43,x346,x347,x348) | | | +- f11(x38,x39,x43 + 1) = (x38 * (x43 + 1)) + x39 >= ((x38 * x43) + x39) + x38 = f8(f466(x38,x39,x43,x346,x347,x348),x38) | | | +- f12(x38,x39,x43 + 1) + x41 = (1 + ((2 * (x38 * (x43 + 1))) + (x43 + 1))) + x41 >= (1 + ((2 * x38) + ((2 * (x38 * x43)) + (x41 + x43)))) + 1 = f477(x38,x39,x41,x43,x346,x347,x348) + 1 | | | +- f478(x52) = x52 >= x52 = x52 | | | +- f11(x49,x50,0) = x50 >= x50 = x50 | | | `- f12(x49,x50,0) + x52 = 1 + x52 >= x52 + 1 = f478(x52) + 1 | `- Stopping timer: 2017-03-30 07:40:40.288939 UTC(+0.691703s)