SUCCESS(2) SUCCESS f1(x0,x1) = 2 + x0; f10(x0,x1,x2) = 0; f11(x0,x1,x2) = 8 + 2*x0 + 7*x0*x2 + x1 + 6*x2; f12(x0,x1,x2) = 1 + 2*x0 + x0*x1 + 7*x0*x2 + 8*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) = 12 + 6*x0 + x1; f2(x0,x1) = 2; f20(x0,x1) = 11 + 7*x0; f21(x0,x1,x2) = 0; f22(x0,x1,x2,x3) = 0; f23(x0,x1) = 15 + 15*x0 + 14*x0*x1 + 10*x1; f24(x0,x1) = 12 + 15*x0 + 14*x0*x1 + 14*x1; f3(x0,x1,x2) = 0; f4(x0,x1,x2) = 12*x0 + 12*x0*x1 + 13*x0*x2 + x1 + 3*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 + 2*x0; f424(x0,x1,x2,x3,x4) = x1; f425(x0,x1,x2,x3,x4,x5) = x2; f426() = 5; 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) = 9 + 15*x0 + 14*x0*x1 + 14*x1 + x2; f431(x0) = x0; f432(x0) = x0; f433(x0) = x0; f434(x0) = x0; f435(x0) = 1 + x0; f436(x0) = x0; f437() = 0; f438(x0,x1,x2,x3) = x0; f439(x0) = 2 + x0; f440(x0,x1,x2,x3,x4,x5) = x2; f441(x0) = 3 + 2*x0; f442(x0,x1,x2,x3,x4,x5) = x0 + x2; f443(x0,x1,x2,x3,x4,x5) = 10 + 7*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) = 1 + 8*x0 + 11*x0*x1 + 13*x0*x2 + x1 + 3*x2; f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x0*x1 + 14*x0*x3 + x2 + 3*x3; f453(x0) = x0; f454(x0) = x0; f455(x0) = x0; f456(x0) = 0; f457(x0,x1,x2,x3,x4,x5,x6) = x2; f458(x0) = 1 + x0; f459(x0,x1,x2,x3,x4,x5,x6) = x0*x1 + x2; f460(x0) = x0; f461(x0,x1,x2,x3,x4,x5,x6) = x0*x1 + 14*x0*x3 + x2; f462(x0,x1,x2,x3,x4,x5,x6) = 3 + 9*x0 + 7*x0*x1 + 14*x0*x3 + x2 + 3*x3; f463(x0) = x0; f464(x0) = x0; f465(x0,x1,x2,x3,x4,x5,x6) = x2; f466(x0,x1,x2,x3,x4,x5) = 9 + 2*x0 + 7*x0*x2 + x1 + 6*x2; f467(x0,x1,x2,x3,x4,x5,x6) = 1 + 4*x0 + x0*x1 + 7*x0*x3 + x2 + 8*x3; f468(x0) = x0; f469(x0) = x0; f470(x0) = x0; f471(x0) = x0; f472(x0,x1,x2,x3,x4,x5,x6) = x2; f473(x0) = 1 + 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) = 8 + 9*x0 + x0*x1 + 7*x0*x3 + x2 + 8*x3; f478(x0) = x0; f5(x0,x1,x2) = 1 + 8*x0*x1 + 14*x0*x2 + 3*x2; f6(x0,x1,x2,x3) = 3*x0 + 12*x0*x1 + 13*x0*x2 + 7*x0*x3; f7(x0,x1,x2,x3,x4) = x0 + 13*x0*x1 + 14*x0*x2 + 4*x0*x3 + 7*x0*x4; f8(x0,x1) = 5 + x0 + 7*x1; f9(x0,x1) = 6 + 5*x1; ExecutionLog | `- SOLVE ... | +- Staring timer: 2017-03-30 07:39:23.220271 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 | +- SMT-SLI ... | | | +- Staring timer: 2017-03-30 07:39:23.220607 UTC | | | `- Stopping timer: 2017-03-30 07:39:23.331655 UTC(+0.111048s) | +- SMT-LI ... | | | +- Staring timer: 2017-03-30 07:39:23.331664 UTC | | | `- Stopping timer: 2017-03-30 07:39:24.702011 UTC(+1.370347s) | +- SMT-MMI(2) ... | | | +- Staring timer: 2017-03-30 07:39:24.702027 UTC | | | +- Interpretation | | | | | +- f1(x0,x1) = 2 + x0 | | | | | +- f10(x0,x1,x2) = 0 | | | | | +- f11(x0,x1,x2) = 8 + 2*x0 + 7*x0*x2 + x1 + 6*x2 | | | | | +- f12(x0,x1,x2) = 1 + 2*x0 + x0*x1 + 7*x0*x2 + 8*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) = 12 + 6*x0 + x1 | | | | | +- f2(x0,x1) = 2 | | | | | +- f20(x0,x1) = 11 + 7*x0 | | | | | +- f21(x0,x1,x2) = 0 | | | | | +- f22(x0,x1,x2,x3) = 0 | | | | | +- f23(x0,x1) = 15 + 15*x0 + 14*x0*x1 + 10*x1 | | | | | +- f24(x0,x1) = 12 + 15*x0 + 14*x0*x1 + 14*x1 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f4(x0,x1,x2) = 12*x0 + 12*x0*x1 + 13*x0*x2 + x1 + 3*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 + 2*x0 | | | | | +- f424(x0,x1,x2,x3,x4) = x1 | | | | | +- f425(x0,x1,x2,x3,x4,x5) = x2 | | | | | +- f426() = 5 | | | | | +- 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) = 9 + 15*x0 + 14*x0*x1 + 14*x1 + x2 | | | | | +- f431(x0) = x0 | | | | | +- f432(x0) = x0 | | | | | +- f433(x0) = x0 | | | | | +- f434(x0) = x0 | | | | | +- f435(x0) = 1 + x0 | | | | | +- f436(x0) = x0 | | | | | +- f437() = 0 | | | | | +- f438(x0,x1,x2,x3) = x0 | | | | | +- f439(x0) = 2 + x0 | | | | | +- f440(x0,x1,x2,x3,x4,x5) = x2 | | | | | +- f441(x0) = 3 + 2*x0 | | | | | +- f442(x0,x1,x2,x3,x4,x5) = x0 + x2 | | | | | +- f443(x0,x1,x2,x3,x4,x5) = 10 + 7*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) = 1 + 8*x0 + 11*x0*x1 + 13*x0*x2 + x1 + 3*x2 | | | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x0*x1 + 14*x0*x3 + x2 + 3*x3 | | | | | +- f453(x0) = x0 | | | | | +- f454(x0) = x0 | | | | | +- f455(x0) = x0 | | | | | +- f456(x0) = 0 | | | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f458(x0) = 1 + x0 | | | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = x0*x1 + x2 | | | | | +- f460(x0) = x0 | | | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = x0*x1 + 14*x0*x3 + x2 | | | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 3 + 9*x0 + 7*x0*x1 + 14*x0*x3 + x2 + 3*x3 | | | | | +- f463(x0) = x0 | | | | | +- f464(x0) = x0 | | | | | +- f465(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f466(x0,x1,x2,x3,x4,x5) = 9 + 2*x0 + 7*x0*x2 + x1 + 6*x2 | | | | | +- f467(x0,x1,x2,x3,x4,x5,x6) = 1 + 4*x0 + x0*x1 + 7*x0*x3 + x2 + 8*x3 | | | | | +- f468(x0) = x0 | | | | | +- f469(x0) = x0 | | | | | +- f470(x0) = x0 | | | | | +- f471(x0) = x0 | | | | | +- f472(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f473(x0) = 1 + 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) = 8 + 9*x0 + x0*x1 + 7*x0*x3 + x2 + 8*x3 | | | | | +- f478(x0) = x0 | | | | | +- f5(x0,x1,x2) = 1 + 8*x0*x1 + 14*x0*x2 + 3*x2 | | | | | +- f6(x0,x1,x2,x3) = 3*x0 + 12*x0*x1 + 13*x0*x2 + 7*x0*x3 | | | | | +- f7(x0,x1,x2,x3,x4) = x0 + 13*x0*x1 + 14*x0*x2 + 4*x0*x3 + 7*x0*x4 | | | | | +- f8(x0,x1) = 5 + x0 + 7*x1 | | | | | `- f9(x0,x1) = 6 + 5*x1 | | | `- Stopping timer: 2017-03-30 07:40:26.405622 UTC(+61.703595s) | +- Interpretation | | | +- f1(x0,x1) = 2 + x0 | | | +- f10(x0,x1,x2) = 0 | | | +- f11(x0,x1,x2) = 8 + 2*x0 + 7*x0*x2 + x1 + 6*x2 | | | +- f12(x0,x1,x2) = 1 + 2*x0 + x0*x1 + 7*x0*x2 + 8*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) = 12 + 6*x0 + x1 | | | +- f2(x0,x1) = 2 | | | +- f20(x0,x1) = 11 + 7*x0 | | | +- f21(x0,x1,x2) = 0 | | | +- f22(x0,x1,x2,x3) = 0 | | | +- f23(x0,x1) = 15 + 15*x0 + 14*x0*x1 + 10*x1 | | | +- f24(x0,x1) = 12 + 15*x0 + 14*x0*x1 + 14*x1 | | | +- f3(x0,x1,x2) = 0 | | | +- f4(x0,x1,x2) = 12*x0 + 12*x0*x1 + 13*x0*x2 + x1 + 3*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 + 2*x0 | | | +- f424(x0,x1,x2,x3,x4) = x1 | | | +- f425(x0,x1,x2,x3,x4,x5) = x2 | | | +- f426() = 5 | | | +- 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) = 9 + 15*x0 + 14*x0*x1 + 14*x1 + x2 | | | +- f431(x0) = x0 | | | +- f432(x0) = x0 | | | +- f433(x0) = x0 | | | +- f434(x0) = x0 | | | +- f435(x0) = 1 + x0 | | | +- f436(x0) = x0 | | | +- f437() = 0 | | | +- f438(x0,x1,x2,x3) = x0 | | | +- f439(x0) = 2 + x0 | | | +- f440(x0,x1,x2,x3,x4,x5) = x2 | | | +- f441(x0) = 3 + 2*x0 | | | +- f442(x0,x1,x2,x3,x4,x5) = x0 + x2 | | | +- f443(x0,x1,x2,x3,x4,x5) = 10 + 7*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) = 1 + 8*x0 + 11*x0*x1 + 13*x0*x2 + x1 + 3*x2 | | | +- f452(x0,x1,x2,x3,x4,x5,x6) = 1 + x0*x1 + 14*x0*x3 + x2 + 3*x3 | | | +- f453(x0) = x0 | | | +- f454(x0) = x0 | | | +- f455(x0) = x0 | | | +- f456(x0) = 0 | | | +- f457(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f458(x0) = 1 + x0 | | | +- f459(x0,x1,x2,x3,x4,x5,x6) = x0*x1 + x2 | | | +- f460(x0) = x0 | | | +- f461(x0,x1,x2,x3,x4,x5,x6) = x0*x1 + 14*x0*x3 + x2 | | | +- f462(x0,x1,x2,x3,x4,x5,x6) = 3 + 9*x0 + 7*x0*x1 + 14*x0*x3 + x2 + 3*x3 | | | +- f463(x0) = x0 | | | +- f464(x0) = x0 | | | +- f465(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f466(x0,x1,x2,x3,x4,x5) = 9 + 2*x0 + 7*x0*x2 + x1 + 6*x2 | | | +- f467(x0,x1,x2,x3,x4,x5,x6) = 1 + 4*x0 + x0*x1 + 7*x0*x3 + x2 + 8*x3 | | | +- f468(x0) = x0 | | | +- f469(x0) = x0 | | | +- f470(x0) = x0 | | | +- f471(x0) = x0 | | | +- f472(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f473(x0) = 1 + 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) = 8 + 9*x0 + x0*x1 + 7*x0*x3 + x2 + 8*x3 | | | +- f478(x0) = x0 | | | +- f5(x0,x1,x2) = 1 + 8*x0*x1 + 14*x0*x2 + 3*x2 | | | +- f6(x0,x1,x2,x3) = 3*x0 + 12*x0*x1 + 13*x0*x2 + 7*x0*x3 | | | +- f7(x0,x1,x2,x3,x4) = x0 + 13*x0*x1 + 14*x0*x2 + 4*x0*x3 + 7*x0*x4 | | | +- f8(x0,x1) = 5 + x0 + 7*x1 | | | `- f9(x0,x1) = 6 + 5*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)) = 5 + (x99 + (7 * (1 + (2 * x4)))) >= 12 + ((6 * x4) + x99) = f19(f418(x4),f421(x99)) | | | +- f9(x99,f423(x4)) + x100 = (6 + (5 * (1 + (2 * x4)))) + x100 >= (11 + (7 * 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() = 5 >= 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) = 9 + ((15 * x3) + ((14 * (x3 * x4)) + ((14 * x4) + x5))) >= (1 + ((2 * (1 + (2 * x4))) + (((1 + (2 * x4)) * 5) + ((7 * ((1 + (2 * x4)) * x3)) + (8 * x3))))) + x5 = f12(f423(x4),f426(),f427(x3)) + f428(x3,x4,x5,x99,x100,x101) | | | +- f23(x3,x4) = 15 + ((15 * x3) + ((14 * (x3 * x4)) + (10 * x4))) >= 8 + ((2 * (1 + (2 * x4))) + ((7 * ((1 + (2 * x4)) * x3)) + (5 + (6 * x3)))) = f11(f423(x4),f426(),f427(x3)) | | | +- f24(x3,x4) + x5 = (12 + ((15 * x3) + ((14 * (x3 * x4)) + (14 * x4)))) + x5 >= (9 + ((15 * x3) + ((14 * (x3 * x4)) + ((14 * 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) = 1 + x171 >= x171 = x171 | | | +- f436(x172) = x172 >= x172 = x172 | | | +- f1(x171,f437()) = 2 + x171 >= 1 + (1 + x171) = f15(f435(x171)) | | | +- f2(x171,f437()) + x172 = 2 + 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) = 2 + 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) = 3 + (2 * x8) >= x8 = x8 | | | +- f442(x8,x9,x10,x171,x172,x173) = x8 + 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) = 10 + ((7 * x8) + x10) >= (1 + (3 * (3 + (2 * x8)))) + (x8 + x10) = f5(f437(),f439(x9),f441(x8)) + f442(x8,x9,x10,x171,x172,x173) | | | +- f19(x8,x9) = 12 + ((6 * x8) + x9) >= (2 + x9) + (3 * (3 + (2 * x8))) = f4(f437(),f439(x9),f441(x8)) | | | +- f20(x8,x9) + x10 = (11 + (7 * x8)) + x10 >= (10 + ((7 * 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) = 1 + x13 >= 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)) = 2 + x242 >= 2 + x242 = f1(f454(x242),x17) | | | +- f2(x242,f456(x17)) + x243 = 2 + x243 >= 2 + 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) = 1 + x18 >= x18 = x18 | | | +- f459(x17,x18,x20,x22,x242,x243,x244) = (x17 * x18) + 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) = (x17 * x18) + ((14 * (x17 * x22)) + x20) >= (x17 * x18) + 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) = 1 + ((8 * x17) + ((11 * (x17 * x18)) + ((13 * (x17 * x22)) + (x18 + (3 * x22))))) >= (1 + x18) + (3 * x22) = f4(f456(x17),f458(x18),f460(x22)) | | | +- f452(x17,x18,x20,x22,x242,x243,x244) = 1 + ((x17 * x18) + ((14 * (x17 * x22)) + (x20 + (3 * x22)))) >= (1 + (3 * x22)) + ((x17 * x18) + ((14 * (x17 * 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) = 3 + ((9 * x17) + ((7 * (x17 * x18)) + ((14 * (x17 * x22)) + (x20 + (3 * x22))))) >= 2 + (1 + ((x17 * x18) + ((14 * (x17 * x22)) + (x20 + (3 * x22))))) = f2(f451(x17,x18,x22,x242,x243,x244),x17) + f452(x17,x18,x20,x22,x242,x243,x244) | | | +- f4(x17,x18,x22 + 1) = (12 * x17) + ((12 * (x17 * x18)) + ((13 * (x17 * (x22 + 1))) + (x18 + (3 * (x22 + 1))))) >= 2 + (1 + ((8 * x17) + ((11 * (x17 * x18)) + ((13 * (x17 * x22)) + (x18 + (3 * x22)))))) = f1(f451(x17,x18,x22,x242,x243,x244),x17) | | | +- f5(x17,x18,x22 + 1) + x20 = (1 + ((8 * (x17 * x18)) + ((14 * (x17 * (x22 + 1))) + (3 * (x22 + 1))))) + x20 >= (3 + ((9 * x17) + ((7 * (x17 * x18)) + ((14 * (x17 * x22)) + (x20 + (3 * x22)))))) + 1 = f462(x17,x18,x20,x22,x242,x243,x244) + 1 | | | +- f463(x31) = x31 >= x31 = x31 | | | +- f4(x28,x29,0) = (12 * x28) + ((12 * (x28 * x29)) + x29) >= x29 = x29 | | | +- f5(x28,x29,0) + x31 = (1 + (8 * (x28 * x29))) + 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)) = 5 + (x346 + (7 * x38)) >= 5 + (x346 + (7 * x38)) = f8(f469(x346),x38) | | | +- f9(x346,f471(x38)) + x347 = (6 + (5 * x38)) + x347 >= (6 + (5 * 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) = 1 + 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) = 9 + ((2 * x38) + ((7 * (x38 * x43)) + (x39 + (6 * x43)))) >= 8 + ((2 * x38) + ((7 * (x38 * x43)) + ((1 + x39) + (6 * x43)))) = f11(f471(x38),f473(x39),f475(x43)) | | | +- f467(x38,x39,x41,x43,x346,x347,x348) = 1 + ((4 * x38) + ((x38 * x39) + ((7 * (x38 * x43)) + (x41 + (8 * x43))))) >= (1 + ((2 * x38) + ((x38 * (1 + x39)) + ((7 * (x38 * x43)) + (8 * 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) = 8 + ((9 * x38) + ((x38 * x39) + ((7 * (x38 * x43)) + (x41 + (8 * x43))))) >= (6 + (5 * x38)) + (1 + ((4 * x38) + ((x38 * x39) + ((7 * (x38 * x43)) + (x41 + (8 * x43)))))) = f9(f466(x38,x39,x43,x346,x347,x348),x38) + f467(x38,x39,x41,x43,x346,x347,x348) | | | +- f11(x38,x39,x43 + 1) = 8 + ((2 * x38) + ((7 * (x38 * (x43 + 1))) + (x39 + (6 * (x43 + 1))))) >= 5 + ((9 + ((2 * x38) + ((7 * (x38 * x43)) + (x39 + (6 * x43))))) + (7 * x38)) = f8(f466(x38 ,x39 ,x43 ,x346 ,x347 ,x348) ,x38) | | | +- f12(x38,x39,x43 + 1) + x41 = (1 + ((2 * x38) + ((x38 * x39) + ((7 * (x38 * (x43 + 1))) + (8 * (x43 + 1)))))) + x41 >= (8 + ((9 * x38) + ((x38 * x39) + ((7 * (x38 * x43)) + (x41 + (8 * x43)))))) + 1 = f477(x38,x39,x41,x43,x346,x347,x348) + 1 | | | +- f478(x52) = x52 >= x52 = x52 | | | +- f11(x49,x50,0) = 8 + ((2 * x49) + x50) >= x50 = x50 | | | `- f12(x49,x50,0) + x52 = (1 + ((2 * x49) + (x49 * x50))) + x52 >= x52 + 1 = f478(x52) + 1 | `- Stopping timer: 2017-03-30 07:40:26.406421 UTC(+63.18615s)