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 + x0*x2 + 3*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) = 2*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) = 2*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 + x0*x3 + x2 + 3*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) = 3 + x0 + x0*x3 + x2 + 3*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 | `- SOLVE ... | +- Staring timer: 2017-03-30 07:40:26.43461 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 | +- 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 | +- SMT-SLI ... | | | +- Staring timer: 2017-03-30 07:40:26.639045 UTC | | | `- Stopping timer: 2017-03-30 07:40:26.683766 UTC(+0.044721s) | +- SMT-LI ... | | | +- Staring timer: 2017-03-30 07:40:26.683773 UTC | | | `- Stopping timer: 2017-03-30 07:40:26.864971 UTC(+0.181198s) | +- SMT-MMI(2) ... | | | +- Staring timer: 2017-03-30 07:40:26.864978 UTC | | | +- Interpretation | | | | | +- f1(x0,x1) = x0 + x1 | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f11(x0,x1,x2) = x0 + 4*x0*x1 + x0*x2 + 4*x1 + 15*x1*x2 + 15*x2 | | | | | +- f12(x0,x1,x2) = 3 + x0 + 15*x0*x1 + x0*x2 + 10*x1*x2 + 13*x2 | | | | | +- f16(x0) = 1 | | | | | +- f19(x0,x1) = 4 + 12*x0 + x1 | | | | | +- f2(x0,x1) = 2 | | | | | +- f20(x0,x1) = 10 + 12*x0 | | | | | +- f23(x0,x1) = 14 + 15*x0 + 14*x0*x1 + 14*x1 | | | | | +- f24(x0,x1) = 15 + 15*x0 + 14*x0*x1 + 14*x1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f4(x0,x1,x2) = 3 + x0*x2 + x1 | | | | | +- f423(x0) = 12*x0 | | | | | +- f430(x0,x1,x2,x3,x4,x5) = 12 + 15*x0 + 14*x0*x1 + 14*x1 + x2 | | | | | +- f437() = 12 | | | | | +- f443(x0,x1,x2,x3,x4,x5) = 8 + 12*x0 + x2 | | | | | +- f450(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f451(x0,x1,x2,x3,x4,x5) = 3 + x0*x2 + x1 | | | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 12 + x2 + 9*x3 | | | | | +- f456(x0) = x0 | | | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 | | | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 | | | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 | | | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 15 + x2 + 9*x3 | | | | | +- f465(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f466(x0,x1,x2,x3,x4,x5) = 6 + x0 + 4*x0*x1 + x0*x2 + 9*x1 + 15*x1*x2 + 15*x2 | | | | | +- f467(x0,x1,x2,x3,x4,x5,x6) = 5 + x0 + 15*x0*x1 + x0*x3 + 5*x1 + 10*x1*x3 + x2 + 13*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) = 15 + 2*x0 + 15*x0*x1 + x0*x3 + 7*x1 + 10*x1*x3 + x2 + 13*x3 | | | | | +- f5(x0,x1,x2) = 8 + 9*x2 | | | | | +- f8(x0,x1) = 6 + x0 + x1 | | | | | `- f9(x0,x1) = 10 + x1 | | | +- Minimizing with ZeroOut ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f11(x0,x1,x2) = 1 + x0*x2 + x1 | | | | | +- f12(x0,x1,x2) = 3 + x0*x2 + 3*x2 | | | | | +- f16(x0) = 1 | | | | | +- f19(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = 1 | | | | | +- f20(x0,x1) = 2 + 2*x0 | | | | | +- f23(x0,x1) = 1 + 2*x0*x1 | | | | | +- f24(x0,x1) = 4 + 3*x0 + 2*x0*x1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f4(x0,x1,x2) = x1 + x2 | | | | | +- f423(x0) = 2*x0 | | | | | +- f430(x0,x1,x2,x3,x4,x5) = 3 + 3*x0 + 2*x0*x1 + x2 | | | | | +- f437() = 1 | | | | | +- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | | | +- 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 | | | | | +- f465(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f466(x0,x1,x2,x3,x4,x5) = 1 + x0*x2 + x1 | | | | | +- f467(x0,x1,x2,x3,x4,x5,x6) = 3 + x0*x3 + x2 + 3*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) = 5 + x0 + x0*x3 + x2 + 3*x3 | | | | | +- f5(x0,x1,x2) = 1 + 2*x2 | | | | | +- f8(x0,x1) = x0 + x1 | | | | | `- f9(x0,x1) = 2 + x1 | | | +- Minimizing with ZeroOut ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | | | +- f12(x0,x1,x2) = 3 + x0*x2 + 3*x2 | | | | | +- f16(x0) = 1 | | | | | +- f19(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = 1 | | | | | +- f20(x0,x1) = 2 + 2*x0 | | | | | +- f23(x0,x1) = 2*x0*x1 | | | | | +- f24(x0,x1) = 4 + 3*x0 + 2*x0*x1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f4(x0,x1,x2) = x1 + x2 | | | | | +- f423(x0) = 2*x0 | | | | | +- f430(x0,x1,x2,x3,x4,x5) = 3 + 3*x0 + 2*x0*x1 + x2 | | | | | +- f437() = 1 | | | | | +- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | | | +- 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 | | | | | +- 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) = 3 + x0*x3 + x2 + 3*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) = 5 + x0 + x0*x3 + x2 + 3*x3 | | | | | +- f5(x0,x1,x2) = 1 + 2*x2 | | | | | +- f8(x0,x1) = x0 + x1 | | | | | `- f9(x0,x1) = 2 + x1 | | | +- Minimizing with ZeroOut ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | | | +- f12(x0,x1,x2) = 3 + x0*x2 + 3*x2 | | | | | +- f16(x0) = 1 | | | | | +- f19(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = 1 | | | | | +- f20(x0,x1) = 2 + 2*x0 | | | | | +- f23(x0,x1) = 2*x0*x1 | | | | | +- f24(x0,x1) = 4 + 3*x0 + 2*x0*x1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f4(x0,x1,x2) = x1 + x2 | | | | | +- f423(x0) = 2*x0 | | | | | +- f430(x0,x1,x2,x3,x4,x5) = 3 + 3*x0 + 2*x0*x1 + x2 | | | | | +- f437() = 0 | | | | | +- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | | | +- 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 | | | | | +- 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) = 3 + x0*x3 + x2 + 3*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) = 5 + x0 + x0*x3 + x2 + 3*x3 | | | | | +- f5(x0,x1,x2) = 1 + 2*x2 | | | | | +- f8(x0,x1) = x0 + x1 | | | | | `- f9(x0,x1) = 2 + x1 | | | +- Minimizing with ZeroOut... Failed | | | +- Minimizing with DecreaseCoeff ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | | | +- f12(x0,x1,x2) = 1 + x0*x2 + 3*x2 | | | | | +- f16(x0) = 1 | | | | | +- f19(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = 1 | | | | | +- f20(x0,x1) = 2 + 2*x0 | | | | | +- f23(x0,x1) = 2*x0*x1 | | | | | +- f24(x0,x1) = 3 + 3*x0 + 2*x0*x1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f4(x0,x1,x2) = x1 + x2 | | | | | +- f423(x0) = 2*x0 | | | | | +- f430(x0,x1,x2,x3,x4,x5) = 2 + 3*x0 + 2*x0*x1 + x2 | | | | | +- f437() = 0 | | | | | +- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | | | +- 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 | | | | | +- 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 + x0*x3 + x2 + 3*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) = 3 + x0 + x0*x3 + x2 + 3*x3 | | | | | +- f5(x0,x1,x2) = 1 + 2*x2 | | | | | +- f8(x0,x1) = x0 + x1 | | | | | `- f9(x0,x1) = 2 + x1 | | | +- Minimizing with DecreaseCoeff ... | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | | | +- f12(x0,x1,x2) = 1 + x0*x2 + 3*x2 | | | | | +- f16(x0) = 1 | | | | | +- f19(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = 1 | | | | | +- f20(x0,x1) = 2 + 2*x0 | | | | | +- f23(x0,x1) = 2*x0*x1 | | | | | +- f24(x0,x1) = 2 + 3*x0 + 2*x0*x1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f4(x0,x1,x2) = x1 + x2 | | | | | +- f423(x0) = 2*x0 | | | | | +- f430(x0,x1,x2,x3,x4,x5) = 1 + 3*x0 + 2*x0*x1 + x2 | | | | | +- f437() = 0 | | | | | +- f443(x0,x1,x2,x3,x4,x5) = 1 + 2*x0 + x2 | | | | | +- 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 | | | | | +- 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 + x0*x3 + x2 + 3*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) = 3 + x0 + x0*x3 + x2 + 3*x3 | | | | | +- f5(x0,x1,x2) = 1 + 2*x2 | | | | | +- f8(x0,x1) = x0 + x1 | | | | | `- f9(x0,x1) = 2 + x1 | | | +- Minimizing with DecreaseCoeff... Failed | | | `- Stopping timer: 2017-03-30 07:40:39.568708 UTC(+12.70373s) | +- Interpretation | | | +- f1(x0,x1) = 1 + x0 | | | +- f10(x0,x1,x2) = 0 | | | +- f11(x0,x1,x2) = x0*x2 + x1 | | | +- f12(x0,x1,x2) = 1 + x0*x2 + 3*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) = 2*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) = 2*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 + x0*x3 + x2 + 3*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) = 3 + x0 + x0*x3 + x2 + 3*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 + (2 * x4) >= x4 + x99 = f19(f418(x4),f421(x99)) | | | +- f9(x99,f423(x4)) + x100 = (2 + (2 * 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 * x4) * x3) + (3 * x3))) + x5 = f12(f423(x4),f426(),f427(x3)) + f428(x3,x4,x5,x99,x100,x101) | | | +- f23(x3,x4) = 2 * (x3 * x4) >= (2 * 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) = x8 + x9 >= 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 + ((x38 * x43) + (x41 + (3 * x43))) >= (1 + ((x38 * x43) + (3 * 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) = 3 + (x38 + ((x38 * x43) + (x41 + (3 * x43)))) >= (2 + x38) + (1 + ((x38 * x43) + (x41 + (3 * 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 + ((x38 * (x43 + 1)) + (3 * (x43 + 1)))) + x41 >= (3 + (x38 + ((x38 * x43) + (x41 + (3 * 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:39.569315 UTC(+13.134705s)