SUCCESS(1)

SUCCESS
f1(x0,x1) = 0;
f160(x0) = x0;
f161(x0) = x0;
f162() = 0;
f163(x0) = x0;
f164(x0) = x0;
f165(x0) = x0;
f166(x0) = x0;
f167() = 0;
f168(x0) = x0;
f169(x0) = x0;
f170(x0) = 0;
f171(x0) = x0;
f172(x0) = x0;
f173(x0) = x0;
f174(x0) = 0;
f175(x0) = x0;
f176(x0) = x0;
f177(x0,x1,x2,x3,x4) = x2;
f178(x0,x1,x2,x3,x4) = x1;
f179(x0) = x0;
f180(x0) = x0;
f181(x0,x1) = max(x1,x0);
f182(x0) = x0;
f183(x0) = x0;
f184(x0) = 1 + x0;
f185(x0,x1,x2,x3,x4,x5) = max(x1,x2);
f186(x0,x1,x2,x3,x4,x5) = 2 + x3;
f187(x0,x1,x2,x3,x4,x5) = max(x1,x2);
f188(x0) = x0;
f189(x0) = x0;
f190(x0) = 0;
f191(x0) = x0;
f192(x0) = x0;
f193(x0) = x0;
f194(x0,x1,x2,x3,x4,x5) = 1 + x3;
f195(x0) = x0;
f196() = 0;
f197() = 0;
f2(x0,x1,x2) = 0;
f3(x0,x1,x2,x3) = max(x2,x1);
f4(x0,x1,x2,x3) = 1 + x3;
f5(x0,x1) = x0;
f6(x0,x1) = x1;
f7(x0,x1,x2) = 0;
f8(x0,x1,x2) = x1;
f9(x0,x1,x2) = x2;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:31:47.644906 UTC
|
+- Open Constraints
|  |
|  +- f160(x46) = f160(x46) >= x46 = x46
|  |
|  +- f161(x47) = f161(x47) >= x47 = x47
|  |
|  +- f7(x46,x47,f162()) = f7(x46,x47,f162()) >= f1(f160(x46),f161(x47)) = f1(f160(x46),f161(x47))
|  |
|  +- f163(x2) = f163(x2) >= x2 = x2
|  |
|  +- f164(x1) = f164(x1) >= x1 = x1
|  |
|  +- f6(x1,x2) = f6(x1,x2) >= f9(f162(),f164(x1),f163(x2)) = f9(f162(),f164(x1),f163(x2))
|  |
|  +- f5(x1,x2) = f5(x1,x2) >= f8(f162(),f164(x1),f163(x2)) = f8(f162(),f164(x1),f163(x2))
|  |
|  +- f165(x5) = f165(x5) >= x5 = x5
|  |
|  +- f166(x6) = f166(x6) >= x6 = x6
|  |
|  +- f1(x5 + 1,x6 + 1) = f1(x5 + 1,x6 + 1) >= f1(f165(x5),f166(x6)) = f1(f165(x5),f166(x6))
|  |
|  +- f1(x9 + 1,0) = f1(x9 + 1,0) >= 0 = 0
|  |
|  +- f1(0,x11) = f1(0,x11) >= 0 = 0
|  |
|  +- f9(x12,x13,0) = f9(x12,x13,0) >= 0 = 0
|  |
|  +- f8(x12,x13,0) = f8(x12,x13,0) >= f167() = f167()
|  |
|  +- f168(x66) = f168(x66) >= x66 = x66
|  |
|  +- f169(x67) = f169(x67) >= x67 = x67
|  |
|  +- f2(x66,x67,f170(x18)) = f2(x66,x67,f170(x18)) >= f7(f168(x66),f169(x67),x18) = f7(f168(x66),f169(x67),x18)
|  |
|  +- f171(x19) = f171(x19) >= x19 = x19
|  |
|  +- f172(x82) = f172(x82) >= x82 = x82
|  |
|  +- f173(x83) = f173(x83) >= x83 = x83
|  |
|  +- f7(x82,x83,f174(x18)) = f7(x82,x83,f174(x18)) >= f7(f172(x82),f173(x83),x18) = f7(f172(x82),f173(x83),x18)
|  |
|  +- f175(x22) = f175(x22) >= x22 = x22
|  |
|  +- f176(x19) = f176(x19) >= x19 = x19
|  |
|  +- f177(x18,x19,x22,x82,x83) = f177(x18,x19,x22,x82,x83) >= f9(f174(x18),f176(x19),f175(x22)) = f9(f174(x18),f176(x19),f175(x22))
|  |
|  +- f178(x18,x19,x22,x82,x83) = f178(x18,x19,x22,x82,x83) >= f8(f174(x18),f176(x19),f175(x22)) = f8(f174(x18),f176(x19),f175(x22))
|  |
|  +- f9(x18,x19,x22 + 1) = f9(x18,x19,x22 + 1) >= f4(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83)) = f4(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|  |
|  +- f8(x18,x19,x22 + 1) = f8(x18,x19,x22 + 1) >= f3(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83)) = f3(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|  |
|  +- f179(x26) = f179(x26) >= x26 = x26
|  |
|  +- f180(x27) = f180(x27) >= x27 = x27
|  |
|  +- f181(x26,x27) = f181(x26,x27) >= x26 = x26
|  |
|  +- f182(x27) = f182(x27) >= x27 = x27
|  |
|  +- f183(x30) = f183(x30) >= x30 = x30
|  |
|  +- f184(x30) = f184(x30) >= f183(x30) + 1 = f183(x30) + 1
|  |
|  +- f181(x26,x27) = f181(x26,x27) >= f182(x27) = f182(x27)
|  |
|  +- f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135) >= f181(x26,x27) = f181(x26,x27)
|  |
|  +- f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135) >= f184(x30) + 1 = f184(x30) + 1
|  |
|  +- f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135) >= x27 = x27
|  |
|  +- f188(x134) = f188(x134) >= x134 = x134
|  |
|  +- f189(x135) = f189(x135) >= x135 = x135
|  |
|  +- f2(x134,x135,f190(x25)) = f2(x134,x135,f190(x25)) >= f2(f188(x134),f189(x135),x25) = f2(f188(x134),f189(x135),x25)
|  |
|  +- f191(x26) = f191(x26) >= x26 = x26
|  |
|  +- f192(x30) = f192(x30) >= x30 = x30
|  |
|  +- f193(x27) = f193(x27) >= x27 = x27
|  |
|  +- f194(x25,x26,x27,x30,x134,x135) = f194(x25,x26,x27,x30,x134,x135) >= f4(f190(x25),f191(x26),f193(x27),f192(x30)) = f4(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135) >= f3(f190(x25),f191(x26),f193(x27),f192(x30)) = f3(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135) >= f194(x25,x26,x27,x30,x134,x135) + 1 = f194(x25,x26,x27,x30,x134,x135) + 1
|  |
|  +- f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135) >= f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135)
|  |
|  +- f4(x25,x26,x27,x30 + 1) = f4(x25,x26,x27,x30 + 1) >= f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135)
|  |
|  +- f3(x25,x26,x27,x30 + 1) = f3(x25,x26,x27,x30 + 1) >= f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135)
|  |
|  +- f195(x34) = f195(x34) >= x34 = x34
|  |
|  +- f196() = f196() >= 0 = 0
|  |
|  +- f195(x34) = f195(x34) >= f197() = f197()
|  |
|  +- f4(x33,x34,x35,0) = f4(x33,x34,x35,0) >= f196() + 1 = f196() + 1
|  |
|  `- f3(x33,x34,x35,0) = f3(x33,x34,x35,0) >= f195(x34) = f195(x34)
|
+- Open Constraints
|  |
|  +- f160(x46) = f160(x46) >= x46 = x46
|  |
|  +- f161(x47) = f161(x47) >= x47 = x47
|  |
|  +- f7(x46,x47,f162()) = f7(x46,x47,f162()) >= f1(f160(x46),f161(x47)) = f1(f160(x46),f161(x47))
|  |
|  +- f163(x2) = f163(x2) >= x2 = x2
|  |
|  +- f164(x1) = f164(x1) >= x1 = x1
|  |
|  +- f6(x1,x2) = f6(x1,x2) >= f9(f162(),f164(x1),f163(x2)) = f9(f162(),f164(x1),f163(x2))
|  |
|  +- f5(x1,x2) = f5(x1,x2) >= f8(f162(),f164(x1),f163(x2)) = f8(f162(),f164(x1),f163(x2))
|  |
|  +- f165(x5) = f165(x5) >= x5 = x5
|  |
|  +- f166(x6) = f166(x6) >= x6 = x6
|  |
|  +- f1(x5 + 1,x6 + 1) = f1(x5 + 1,x6 + 1) >= f1(f165(x5),f166(x6)) = f1(f165(x5),f166(x6))
|  |
|  +- f1(x9 + 1,0) = f1(x9 + 1,0) >= 0 = 0
|  |
|  +- f1(0,x11) = f1(0,x11) >= 0 = 0
|  |
|  +- f9(x12,x13,0) = f9(x12,x13,0) >= 0 = 0
|  |
|  +- f8(x12,x13,0) = f8(x12,x13,0) >= f167() = f167()
|  |
|  +- f168(x66) = f168(x66) >= x66 = x66
|  |
|  +- f169(x67) = f169(x67) >= x67 = x67
|  |
|  +- f2(x66,x67,f170(x18)) = f2(x66,x67,f170(x18)) >= f7(f168(x66),f169(x67),x18) = f7(f168(x66),f169(x67),x18)
|  |
|  +- f171(x19) = f171(x19) >= x19 = x19
|  |
|  +- f172(x82) = f172(x82) >= x82 = x82
|  |
|  +- f173(x83) = f173(x83) >= x83 = x83
|  |
|  +- f7(x82,x83,f174(x18)) = f7(x82,x83,f174(x18)) >= f7(f172(x82),f173(x83),x18) = f7(f172(x82),f173(x83),x18)
|  |
|  +- f175(x22) = f175(x22) >= x22 = x22
|  |
|  +- f176(x19) = f176(x19) >= x19 = x19
|  |
|  +- f177(x18,x19,x22,x82,x83) = f177(x18,x19,x22,x82,x83) >= f9(f174(x18),f176(x19),f175(x22)) = f9(f174(x18),f176(x19),f175(x22))
|  |
|  +- f178(x18,x19,x22,x82,x83) = f178(x18,x19,x22,x82,x83) >= f8(f174(x18),f176(x19),f175(x22)) = f8(f174(x18),f176(x19),f175(x22))
|  |
|  +- f9(x18,x19,x22 + 1) = f9(x18,x19,x22 + 1) >= f4(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83)) = f4(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|  |
|  +- f8(x18,x19,x22 + 1) = f8(x18,x19,x22 + 1) >= f3(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83)) = f3(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|  |
|  +- f179(x26) = f179(x26) >= x26 = x26
|  |
|  +- f180(x27) = f180(x27) >= x27 = x27
|  |
|  +- f181(x26,x27) = f181(x26,x27) >= x26 = x26
|  |
|  +- f182(x27) = f182(x27) >= x27 = x27
|  |
|  +- f183(x30) = f183(x30) >= x30 = x30
|  |
|  +- f184(x30) = f184(x30) >= f183(x30) + 1 = f183(x30) + 1
|  |
|  +- f181(x26,x27) = f181(x26,x27) >= f182(x27) = f182(x27)
|  |
|  +- f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135) >= f181(x26,x27) = f181(x26,x27)
|  |
|  +- f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135) >= f184(x30) + 1 = f184(x30) + 1
|  |
|  +- f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135) >= x27 = x27
|  |
|  +- f188(x134) = f188(x134) >= x134 = x134
|  |
|  +- f189(x135) = f189(x135) >= x135 = x135
|  |
|  +- f2(x134,x135,f190(x25)) = f2(x134,x135,f190(x25)) >= f2(f188(x134),f189(x135),x25) = f2(f188(x134),f189(x135),x25)
|  |
|  +- f191(x26) = f191(x26) >= x26 = x26
|  |
|  +- f192(x30) = f192(x30) >= x30 = x30
|  |
|  +- f193(x27) = f193(x27) >= x27 = x27
|  |
|  +- f194(x25,x26,x27,x30,x134,x135) = f194(x25,x26,x27,x30,x134,x135) >= f4(f190(x25),f191(x26),f193(x27),f192(x30)) = f4(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135) >= f3(f190(x25),f191(x26),f193(x27),f192(x30)) = f3(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135) >= f194(x25,x26,x27,x30,x134,x135) + 1 = f194(x25,x26,x27,x30,x134,x135) + 1
|  |
|  +- f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135) >= f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135)
|  |
|  +- f4(x25,x26,x27,x30 + 1) = f4(x25,x26,x27,x30 + 1) >= f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135)
|  |
|  +- f3(x25,x26,x27,x30 + 1) = f3(x25,x26,x27,x30 + 1) >= f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135)
|  |
|  +- f195(x34) = f195(x34) >= x34 = x34
|  |
|  +- f196() = f196() >= 0 = 0
|  |
|  +- f195(x34) = f195(x34) >= f197() = f197()
|  |
|  +- f4(x33,x34,x35,0) = f4(x33,x34,x35,0) >= f196() + 1 = f196() + 1
|  |
|  `- f3(x33,x34,x35,0) = f3(x33,x34,x35,0) >= f195(x34) = f195(x34)
|
+- Simplification ...
|  |
|  +- Substituted: f1(x9 + 1,0) ≥ 0 ↦ f1(1,0) ≥ 0
|  |
|  +- Substituted: f1(0,x11) ≥ 0 ↦ f1(0,0) ≥ 0
|  |
|  +- Substituted: f9(x12,x13,0) ≥ 0 ↦ f9(0,0,0) ≥ 0
|  |
|  +- Substituted: f8(x12,x13,0) ≥ f167() ↦ f8(0,0,0) ≥ f167()
|  |
|  +- Substituted: f177(x18,x19,x22,x82,x83) ≥ f9(f174(x18),f176(x19),f175(x22)) ↦ f177(x18,x19,x22,0,0) ≥ f9(f174(x18),f176(x19),f175(x22))
|  |
|  +- Substituted: f178(x18,x19,x22,x82,x83) ≥ f8(f174(x18),f176(x19),f175(x22)) ↦ f178(x18,x19,x22,0,0) ≥ f8(f174(x18),f176(x19),f175(x22))
|  |
|  +- Substituted: f181(x26,x27) ≥ x26 ↦ f181(x26,0) ≥ x26
|  |
|  +- Substituted: f181(x26,x27) ≥ f182(x27) ↦ f181(0,x27) ≥ f182(x27)
|  |
|  +- Substituted: f185(x25,x26,x27,x30,x134,x135) ≥ f181(x26,x27) ↦ f185(0,x26,x27,0,0,0) ≥ f181(x26,x27)
|  |
|  +- Substituted: f186(x25,x26,x27,x30,x134,x135) ≥ f184(x30) + 1 ↦ f186(0,0,0,x30,0,0) ≥ f184(x30) + 1
|  |
|  +- Substituted: f187(x25,x26,x27,x30,x134,x135) ≥ x27 ↦ f187(0,0,x27,0,0,0) ≥ x27
|  |
|  +- Substituted: f194(x25,x26,x27,x30,x134,x135) ≥ f4(f190(x25),f191(x26),f193(x27),f192(x30)) ↦ f194(x25,x26,x27,x30,0,0) ≥ f4(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- Substituted: f187(x25,x26,x27,x30,x134,x135) ≥ f3(f190(x25),f191(x26),f193(x27),f192(x30)) ↦ f187(x25,x26,x27,x30,0,0) ≥ f3(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- Substituted: f195(x34) ≥ f197() ↦ f195(0) ≥ f197()
|  |
|  +- Substituted: f4(x33,x34,x35,0) ≥ f196() + 1 ↦ f4(0,0,0,0) ≥ f196() + 1
|  |
|  +- Substituted: f3(x33,x34,x35,0) ≥ f195(x34) ↦ f3(0,x34,0,0) ≥ f195(x34)
|  |
|  +- Eliminated: f167/0
|  |
|  +- Eliminated: f197/0
|  |
|  +- Propagated: f160(x0) ↦ x0
|  |
|  +- Propagated: f161(x0) ↦ x0
|  |
|  +- Propagated: f163(x0) ↦ x0
|  |
|  +- Propagated: f164(x0) ↦ x0
|  |
|  +- Propagated: f165(x0) ↦ x0
|  |
|  +- Propagated: f166(x0) ↦ x0
|  |
|  +- Propagated: f168(x0) ↦ x0
|  |
|  +- Propagated: f169(x0) ↦ x0
|  |
|  +- Propagated: f171(x0) ↦ x0
|  |
|  +- Propagated: f172(x0) ↦ x0
|  |
|  +- Propagated: f173(x0) ↦ x0
|  |
|  +- Propagated: f175(x0) ↦ x0
|  |
|  +- Propagated: f176(x0) ↦ x0
|  |
|  +- Propagated: f179(x0) ↦ x0
|  |
|  +- Propagated: f180(x0) ↦ x0
|  |
|  +- Propagated: f182(x0) ↦ x0
|  |
|  +- Propagated: f183(x0) ↦ x0
|  |
|  +- Propagated: f188(x0) ↦ x0
|  |
|  +- Propagated: f189(x0) ↦ x0
|  |
|  +- Propagated: f191(x0) ↦ x0
|  |
|  +- Propagated: f192(x0) ↦ x0
|  |
|  +- Propagated: f193(x0) ↦ x0
|  |
|  +- Propagated: f196() ↦ 0
|  |
|  `- Propagated: f184(x0) ↦ 1 + x0
|
+- Interpretation
|  |
|  +- f160(x0) = x0
|  |
|  +- f161(x0) = x0
|  |
|  +- f163(x0) = x0
|  |
|  +- f164(x0) = x0
|  |
|  +- f165(x0) = x0
|  |
|  +- f166(x0) = x0
|  |
|  +- f167() = 0
|  |
|  +- f168(x0) = x0
|  |
|  +- f169(x0) = x0
|  |
|  +- f171(x0) = x0
|  |
|  +- f172(x0) = x0
|  |
|  +- f173(x0) = x0
|  |
|  +- f175(x0) = x0
|  |
|  +- f176(x0) = x0
|  |
|  +- f179(x0) = x0
|  |
|  +- f180(x0) = x0
|  |
|  +- f182(x0) = x0
|  |
|  +- f183(x0) = x0
|  |
|  +- f184(x0) = 1 + x0
|  |
|  +- f188(x0) = x0
|  |
|  +- f189(x0) = x0
|  |
|  +- f191(x0) = x0
|  |
|  +- f192(x0) = x0
|  |
|  +- f193(x0) = x0
|  |
|  +- f196() = 0
|  |
|  `- f197() = 0
|
+- Constraints
|  |
|  +- f160(x46) = x46 >= x46 = x46
|  |
|  +- f161(x47) = x47 >= x47 = x47
|  |
|  +- f7(x46,x47,f162()) = f7(x46,x47,f162()) >= f1(x46,x47) = f1(f160(x46),f161(x47))
|  |
|  +- f163(x2) = x2 >= x2 = x2
|  |
|  +- f164(x1) = x1 >= x1 = x1
|  |
|  +- f6(x1,x2) = f6(x1,x2) >= f9(f162(),x1,x2) = f9(f162(),f164(x1),f163(x2))
|  |
|  +- f5(x1,x2) = f5(x1,x2) >= f8(f162(),x1,x2) = f8(f162(),f164(x1),f163(x2))
|  |
|  +- f165(x5) = x5 >= x5 = x5
|  |
|  +- f166(x6) = x6 >= x6 = x6
|  |
|  +- f1(x5 + 1,x6 + 1) = f1(x5 + 1,x6 + 1) >= f1(x5,x6) = f1(f165(x5),f166(x6))
|  |
|  +- f1(x9 + 1,0) = f1(x9 + 1,0) >= 0 = 0
|  |
|  +- f1(0,x11) = f1(0,x11) >= 0 = 0
|  |
|  +- f9(x12,x13,0) = f9(x12,x13,0) >= 0 = 0
|  |
|  +- f8(x12,x13,0) = f8(x12,x13,0) >= 0 = f167()
|  |
|  +- f168(x66) = x66 >= x66 = x66
|  |
|  +- f169(x67) = x67 >= x67 = x67
|  |
|  +- f2(x66,x67,f170(x18)) = f2(x66,x67,f170(x18)) >= f7(x66,x67,x18) = f7(f168(x66),f169(x67),x18)
|  |
|  +- f171(x19) = x19 >= x19 = x19
|  |
|  +- f172(x82) = x82 >= x82 = x82
|  |
|  +- f173(x83) = x83 >= x83 = x83
|  |
|  +- f7(x82,x83,f174(x18)) = f7(x82,x83,f174(x18)) >= f7(x82,x83,x18) = f7(f172(x82),f173(x83),x18)
|  |
|  +- f175(x22) = x22 >= x22 = x22
|  |
|  +- f176(x19) = x19 >= x19 = x19
|  |
|  +- f177(x18,x19,x22,x82,x83) = f177(x18,x19,x22,x82,x83) >= f9(f174(x18),x19,x22) = f9(f174(x18),f176(x19),f175(x22))
|  |
|  +- f178(x18,x19,x22,x82,x83) = f178(x18,x19,x22,x82,x83) >= f8(f174(x18),x19,x22) = f8(f174(x18),f176(x19),f175(x22))
|  |
|  +- f9(x18,x19,x22 + 1) = f9(x18,x19,x22 + 1) >= f4(f170(x18),x19,f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83)) = f4(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|  |
|  +- f8(x18,x19,x22 + 1) = f8(x18,x19,x22 + 1) >= f3(f170(x18),x19,f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83)) = f3(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|  |
|  +- f179(x26) = x26 >= x26 = x26
|  |
|  +- f180(x27) = x27 >= x27 = x27
|  |
|  +- f181(x26,x27) = f181(x26,x27) >= x26 = x26
|  |
|  +- f182(x27) = x27 >= x27 = x27
|  |
|  +- f183(x30) = x30 >= x30 = x30
|  |
|  +- f184(x30) = x30 + 1 >= x30 + 1 = f183(x30) + 1
|  |
|  +- f181(x26,x27) = f181(x26,x27) >= x27 = f182(x27)
|  |
|  +- f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135) >= f181(x26,x27) = f181(x26,x27)
|  |
|  +- f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135) >= (x30 + 1) + 1 = f184(x30) + 1
|  |
|  +- f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135) >= x27 = x27
|  |
|  +- f188(x134) = x134 >= x134 = x134
|  |
|  +- f189(x135) = x135 >= x135 = x135
|  |
|  +- f2(x134,x135,f190(x25)) = f2(x134,x135,f190(x25)) >= f2(x134,x135,x25) = f2(f188(x134),f189(x135),x25)
|  |
|  +- f191(x26) = x26 >= x26 = x26
|  |
|  +- f192(x30) = x30 >= x30 = x30
|  |
|  +- f193(x27) = x27 >= x27 = x27
|  |
|  +- f194(x25,x26,x27,x30,x134,x135) = f194(x25,x26,x27,x30,x134,x135) >= f4(f190(x25),x26,x27,x30) = f4(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135) >= f3(f190(x25),x26,x27,x30) = f3(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135) >= f194(x25,x26,x27,x30,x134,x135) + 1 = f194(x25,x26,x27,x30,x134,x135) + 1
|  |
|  +- f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135) >= f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135)
|  |
|  +- f4(x25,x26,x27,x30 + 1) = f4(x25,x26,x27,x30 + 1) >= f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135)
|  |
|  +- f3(x25,x26,x27,x30 + 1) = f3(x25,x26,x27,x30 + 1) >= f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135)
|  |
|  +- f195(x34) = f195(x34) >= x34 = x34
|  |
|  +- f196() = 0 >= 0 = 0
|  |
|  +- f195(x34) = f195(x34) >= 0 = f197()
|  |
|  +- f4(x33,x34,x35,0) = f4(x33,x34,x35,0) >= 1 = f196() + 1
|  |
|  `- f3(x33,x34,x35,0) = f3(x33,x34,x35,0) >= f195(x34) = f195(x34)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 10 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.647337 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f195(x34) = f195(x34) >= x34 = x34
|     |  |
|     |  `- f195(0) = f195(0) >= 0 = 0
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:31:47.647374 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f195(x0) = x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:31:47.651948 UTC(+0.004574s)
|     |
|     +- Interpretation
|     |  |
|     |  `- f195(x0) = x0
|     |
|     +- Constraints
|     |  |
|     |  +- f195(x34) = x34 >= x34 = x34
|     |  |
|     |  `- f195(0) = 0 >= 0 = 0
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.651985 UTC(+0.004648s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 9 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.652813 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f1(x5 + 1,x6 + 1) = f1(x5 + 1,x6 + 1) >= f1(x5,x6) = f1(x5,x6)
|     |  |
|     |  +- f1(1,0) = f1(1,0) >= 0 = 0
|     |  |
|     |  `- f1(0,0) = f1(0,0) >= 0 = 0
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:31:47.652881 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f1(x0,x1) = x0
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f1(x0,x1) = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:31:47.659602 UTC(+0.006721s)
|     |
|     +- Interpretation
|     |  |
|     |  `- f1(x0,x1) = 0
|     |
|     +- Constraints
|     |  |
|     |  +- f1(x5 + 1,x6 + 1) = 0 >= 0 = f1(x5,x6)
|     |  |
|     |  +- f1(1,0) = 0 >= 0 = 0
|     |  |
|     |  `- f1(0,0) = 0 >= 0 = 0
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.65964 UTC(+0.006827s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 8 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.660335 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f181(x26,0) = f181(x26,0) >= x26 = x26
|     |  |
|     |  `- f181(0,x27) = f181(0,x27) >= x27 = x27
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:31:47.66038 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f181(x0,x1) = x0 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with  ShiftMax ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f181(x0,x1) = max(x1,x0)
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:31:47.668047 UTC(+0.007667s)
|     |
|     +- Interpretation
|     |  |
|     |  `- f181(x0,x1) = max(x1,x0)
|     |
|     +- Constraints
|     |  |
|     |  +- f181(x26,0) = x26 >= x26 = x26
|     |  |
|     |  `- f181(0,x27) = x27 >= x27 = x27
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.668092 UTC(+0.007757s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 7 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.668869 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f7(x46,x47,f162()) = f7(x46,x47,f162()) >= 0 = f1(x46,x47)
|     |  |
|     |  `- f7(x82,x83,f174(x18)) = f7(x82,x83,f174(x18)) >= f7(x82,x83,x18) = f7(x82,x83,x18)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:31:47.668958 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f162() = 0
|     |  |  |
|     |  |  +- f174(x0) = 12 + x0
|     |  |  |
|     |  |  `- f7(x0,x1,x2) = max(12 + x1,15 + x2)
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f162() = 0
|     |  |  |
|     |  |  +- f174(x0) = 0
|     |  |  |
|     |  |  `- f7(x0,x1,x2) = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:31:47.683486 UTC(+0.014528s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = 0
|     |  |
|     |  +- f162() = 0
|     |  |
|     |  +- f174(x0) = 0
|     |  |
|     |  `- f7(x0,x1,x2) = 0
|     |
|     +- Constraints
|     |  |
|     |  +- f7(x46,x47,f162()) = 0 >= 0 = f1(x46,x47)
|     |  |
|     |  `- f7(x82,x83,f174(x18)) = 0 >= 0 = f7(x82,x83,x18)
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.683539 UTC(+0.01467s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 6 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.684058 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f2(x66,x67,f170(x18)) = f2(x66,x67,f170(x18)) >= 0 = f7(x66,x67,x18)
|     |  |
|     |  `- f2(x134,x135,f190(x25)) = f2(x134,x135,f190(x25)) >= f2(x134,x135,x25) = f2(x134,x135,x25)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:31:47.68413 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f170(x0) = 0
|     |  |  |
|     |  |  +- f190(x0) = 12 + x0
|     |  |  |
|     |  |  `- f2(x0,x1,x2) = max(12 + x1,15 + x2)
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f170(x0) = 0
|     |  |  |
|     |  |  +- f190(x0) = 0
|     |  |  |
|     |  |  `- f2(x0,x1,x2) = 0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:31:47.698128 UTC(+0.013998s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f170(x0) = 0
|     |  |
|     |  +- f190(x0) = 0
|     |  |
|     |  +- f2(x0,x1,x2) = 0
|     |  |
|     |  `- f7(x0,x1,x2) = 0
|     |
|     +- Constraints
|     |  |
|     |  +- f2(x66,x67,f170(x18)) = 0 >= 0 = f7(x66,x67,x18)
|     |  |
|     |  `- f2(x134,x135,f190(x25)) = 0 >= 0 = f2(x134,x135,x25)
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.698181 UTC(+0.014123s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 5 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.698613 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f187(x25,x26,x27,x30,0,0) = f187(x25,x26,x27,x30,0,0) >= f3(0,x26,x27,x30) = f3(f190(x25),x26,x27,x30)
|     |  |
|     |  +- f187(0,0,x27,0,0,0) = f187(0,0,x27,0,0,0) >= x27 = x27
|     |  |
|     |  +- f3(x25,x26,x27,x30 + 1) = f3(x25,x26,x27,x30 + 1) >= f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135)
|     |  |
|     |  +- f185(0,x26,x27,0,0,0) = f185(0,x26,x27,0,0,0) >= max(x27,x26) = f181(x26,x27)
|     |  |
|     |  +- f185(x25,x26,x27,x30,x134,x135) = f185(x25,x26,x27,x30,x134,x135) >= f187(x25,x26,x27,x30,x134,x135) = f187(x25,x26,x27,x30,x134,x135)
|     |  |
|     |  `- f3(0,x34,0,0) = f3(0,x34,0,0) >= x34 = f195(x34)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:31:47.698759 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f185(x0,x1,x2,x3,x4,x5) = 15 + x1 + x2 + x3
|     |  |  |
|     |  |  +- f187(x0,x1,x2,x3,x4,x5) = 15 + x1 + x2 + x3
|     |  |  |
|     |  |  `- f3(x0,x1,x2,x3) = 15 + x1 + x2 + x3
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f185(x0,x1,x2,x3,x4,x5) = x1 + x2
|     |  |  |
|     |  |  +- f187(x0,x1,x2,x3,x4,x5) = x1 + x2
|     |  |  |
|     |  |  `- f3(x0,x1,x2,x3) = x1 + x2
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with  ShiftMax ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f185(x0,x1,x2,x3,x4,x5) = max(x1,x2)
|     |  |  |
|     |  |  +- f187(x0,x1,x2,x3,x4,x5) = max(x1,x2)
|     |  |  |
|     |  |  `- f3(x0,x1,x2,x3) = max(x2,x1)
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:31:47.752614 UTC(+0.053855s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f181(x0,x1) = max(x1,x0)
|     |  |
|     |  +- f185(x0,x1,x2,x3,x4,x5) = max(x1,x2)
|     |  |
|     |  +- f187(x0,x1,x2,x3,x4,x5) = max(x1,x2)
|     |  |
|     |  +- f190(x0) = 0
|     |  |
|     |  +- f195(x0) = x0
|     |  |
|     |  `- f3(x0,x1,x2,x3) = max(x2,x1)
|     |
|     +- Constraints
|     |  |
|     |  +- f187(x25,x26,x27,x30,0,0) = max(x26,x27) >= max(x27,x26) = f3(f190(x25),x26,x27,x30)
|     |  |
|     |  +- f187(0,0,x27,0,0,0) = x27 >= x27 = x27
|     |  |
|     |  +- f3(x25,x26,x27,x30 + 1) = max(x27,x26) >= max(x26,x27) = f185(x25,x26,x27,x30,x134,x135)
|     |  |
|     |  +- f185(0,x26,x27,0,0,0) = max(x26,x27) >= max(x27,x26) = f181(x26,x27)
|     |  |
|     |  +- f185(x25,x26,x27,x30,x134,x135) = max(x26,x27) >= max(x26,x27) = f187(x25,x26,x27,x30,x134,x135)
|     |  |
|     |  `- f3(0,x34,0,0) = x34 >= x34 = f195(x34)
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.752669 UTC(+0.054056s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.752901 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f194(x25,x26,x27,x30,0,0) = f194(x25,x26,x27,x30,0,0) >= f4(0,x26,x27,x30) = f4(f190(x25),x26,x27,x30)
|     |  |
|     |  +- f4(x25,x26,x27,x30 + 1) = f4(x25,x26,x27,x30 + 1) >= f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135)
|     |  |
|     |  +- f186(x25,x26,x27,x30,x134,x135) = f186(x25,x26,x27,x30,x134,x135) >= f194(x25,x26,x27,x30,x134,x135) + 1 = f194(x25,x26,x27,x30,x134,x135) + 1
|     |  |
|     |  +- f186(0,0,0,x30,0,0) = f186(0,0,0,x30,0,0) >= (x30 + 1) + 1 = (x30 + 1) + 1
|     |  |
|     |  `- f4(0,0,0,0) = f4(0,0,0,0) >= 1 = 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:31:47.752987 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f186(x0,x1,x2,x3,x4,x5) = max(9 + x1 + x2 + x3,8 + x0)
|     |  |  |
|     |  |  +- f194(x0,x1,x2,x3,x4,x5) = 8 + x1 + x2 + x3
|     |  |  |
|     |  |  `- f4(x0,x1,x2,x3) = max(8 + x1 + x2 + x3,8 + x0)
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f186(x0,x1,x2,x3,x4,x5) = 2 + x3
|     |  |  |
|     |  |  +- f194(x0,x1,x2,x3,x4,x5) = 1 + x3
|     |  |  |
|     |  |  `- f4(x0,x1,x2,x3) = 1 + x3
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:31:47.812722 UTC(+0.059735s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f186(x0,x1,x2,x3,x4,x5) = 2 + x3
|     |  |
|     |  +- f190(x0) = 0
|     |  |
|     |  +- f194(x0,x1,x2,x3,x4,x5) = 1 + x3
|     |  |
|     |  `- f4(x0,x1,x2,x3) = 1 + x3
|     |
|     +- Constraints
|     |  |
|     |  +- f194(x25,x26,x27,x30,0,0) = 1 + x30 >= 1 + x30 = f4(f190(x25),x26,x27,x30)
|     |  |
|     |  +- f4(x25,x26,x27,x30 + 1) = 1 + (x30 + 1) >= 2 + x30 = f186(x25,x26,x27,x30,x134,x135)
|     |  |
|     |  +- f186(x25,x26,x27,x30,x134,x135) = 2 + x30 >= (1 + x30) + 1 = f194(x25,x26,x27,x30,x134,x135) + 1
|     |  |
|     |  +- f186(0,0,0,x30,0,0) = 2 + x30 >= (x30 + 1) + 1 = (x30 + 1) + 1
|     |  |
|     |  `- f4(0,0,0,0) = 1 >= 1 = 1
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.812776 UTC(+0.059875s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.812853 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f9(x18,x19,x22 + 1) = f9(x18,x19,x22 + 1) >= 1 + f177(x18,x19,x22,x82,x83) = f4(f170(x18),x19,f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|     |  |
|     |  +- f177(x18,x19,x22,0,0) = f177(x18,x19,x22,0,0) >= f9(0,x19,x22) = f9(f174(x18),x19,x22)
|     |  |
|     |  +- f9(0,0,0) = f9(0,0,0) >= 0 = 0
|     |  |
|     |  +- f178(x18,x19,x22,0,0) = f178(x18,x19,x22,0,0) >= f8(0,x19,x22) = f8(f174(x18),x19,x22)
|     |  |
|     |  +- f8(x18,x19,x22 + 1) = f8(x18,x19,x22 + 1) >= max(f178(x18,x19,x22,x82,x83),x19) = f3(f170(x18),x19,f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|     |  |
|     |  `- f8(0,0,0) = f8(0,0,0) >= 0 = 0
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:31:47.812957 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f177(x0,x1,x2,x3,x4) = max(15 + x2,x1 + x2)
|     |  |  |
|     |  |  +- f178(x0,x1,x2,x3,x4) = max(3 + x1,4 + x0,10)
|     |  |  |
|     |  |  +- f8(x0,x1,x2) = max(10 + x0,3 + x1)
|     |  |  |
|     |  |  `- f9(x0,x1,x2) = max(7 + x0 + x2,x1 + x2,15 + x2)
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f177(x0,x1,x2,x3,x4) = x2
|     |  |  |
|     |  |  +- f178(x0,x1,x2,x3,x4) = x1
|     |  |  |
|     |  |  +- f8(x0,x1,x2) = x1
|     |  |  |
|     |  |  `- f9(x0,x1,x2) = x0 + x2
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f177(x0,x1,x2,x3,x4) = x2
|     |  |  |
|     |  |  +- f178(x0,x1,x2,x3,x4) = x1
|     |  |  |
|     |  |  +- f8(x0,x1,x2) = x1
|     |  |  |
|     |  |  `- f9(x0,x1,x2) = x2
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:31:47.869125 UTC(+0.056168s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f170(x0) = 0
|     |  |
|     |  +- f174(x0) = 0
|     |  |
|     |  +- f177(x0,x1,x2,x3,x4) = x2
|     |  |
|     |  +- f178(x0,x1,x2,x3,x4) = x1
|     |  |
|     |  +- f3(x0,x1,x2,x3) = max(x2,x1)
|     |  |
|     |  +- f4(x0,x1,x2,x3) = 1 + x3
|     |  |
|     |  +- f8(x0,x1,x2) = x1
|     |  |
|     |  `- f9(x0,x1,x2) = x2
|     |
|     +- Constraints
|     |  |
|     |  +- f9(x18,x19,x22 + 1) = x22 + 1 >= 1 + x22 = f4(f170(x18),x19,f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|     |  |
|     |  +- f177(x18,x19,x22,0,0) = x22 >= x22 = f9(f174(x18),x19,x22)
|     |  |
|     |  +- f9(0,0,0) = 0 >= 0 = 0
|     |  |
|     |  +- f178(x18,x19,x22,0,0) = x19 >= x19 = f8(f174(x18),x19,x22)
|     |  |
|     |  +- f8(x18,x19,x22 + 1) = x19 >= max(x19,x19) = f3(f170(x18),x19,f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|     |  |
|     |  `- f8(0,0,0) = 0 >= 0 = 0
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.869193 UTC(+0.05634s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.869214 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f6(x1,x2) = f6(x1,x2) >= x2 = f9(f162(),x1,x2)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f6(x0,x1) ↦ x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f162() = 0
|     |  |
|     |  +- f6(x0,x1) = x1
|     |  |
|     |  `- f9(x0,x1,x2) = x2
|     |
|     +- Constraints
|     |  |
|     |  `- f6(x1,x2) = x2 >= x2 = f9(f162(),x1,x2)
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.869294 UTC(+0.00008s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:31:47.869303 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f5(x1,x2) = f5(x1,x2) >= x1 = f8(f162(),x1,x2)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f5(x0,x1) ↦ x0
|     |
|     +- Interpretation
|     |  |
|     |  +- f162() = 0
|     |  |
|     |  +- f5(x0,x1) = x0
|     |  |
|     |  `- f8(x0,x1,x2) = x1
|     |
|     +- Constraints
|     |  |
|     |  `- f5(x1,x2) = x1 >= x1 = f8(f162(),x1,x2)
|     |
|     `- Stopping timer: 2017-03-30 07:31:47.869422 UTC(+0.000119s)
|
+- Interpretation
|  |
|  +- f1(x0,x1) = 0
|  |
|  +- f160(x0) = x0
|  |
|  +- f161(x0) = x0
|  |
|  +- f162() = 0
|  |
|  +- f163(x0) = x0
|  |
|  +- f164(x0) = x0
|  |
|  +- f165(x0) = x0
|  |
|  +- f166(x0) = x0
|  |
|  +- f167() = 0
|  |
|  +- f168(x0) = x0
|  |
|  +- f169(x0) = x0
|  |
|  +- f170(x0) = 0
|  |
|  +- f171(x0) = x0
|  |
|  +- f172(x0) = x0
|  |
|  +- f173(x0) = x0
|  |
|  +- f174(x0) = 0
|  |
|  +- f175(x0) = x0
|  |
|  +- f176(x0) = x0
|  |
|  +- f177(x0,x1,x2,x3,x4) = x2
|  |
|  +- f178(x0,x1,x2,x3,x4) = x1
|  |
|  +- f179(x0) = x0
|  |
|  +- f180(x0) = x0
|  |
|  +- f181(x0,x1) = max(x1,x0)
|  |
|  +- f182(x0) = x0
|  |
|  +- f183(x0) = x0
|  |
|  +- f184(x0) = 1 + x0
|  |
|  +- f185(x0,x1,x2,x3,x4,x5) = max(x1,x2)
|  |
|  +- f186(x0,x1,x2,x3,x4,x5) = 2 + x3
|  |
|  +- f187(x0,x1,x2,x3,x4,x5) = max(x1,x2)
|  |
|  +- f188(x0) = x0
|  |
|  +- f189(x0) = x0
|  |
|  +- f190(x0) = 0
|  |
|  +- f191(x0) = x0
|  |
|  +- f192(x0) = x0
|  |
|  +- f193(x0) = x0
|  |
|  +- f194(x0,x1,x2,x3,x4,x5) = 1 + x3
|  |
|  +- f195(x0) = x0
|  |
|  +- f196() = 0
|  |
|  +- f197() = 0
|  |
|  +- f2(x0,x1,x2) = 0
|  |
|  +- f3(x0,x1,x2,x3) = max(x2,x1)
|  |
|  +- f4(x0,x1,x2,x3) = 1 + x3
|  |
|  +- f5(x0,x1) = x0
|  |
|  +- f6(x0,x1) = x1
|  |
|  +- f7(x0,x1,x2) = 0
|  |
|  +- f8(x0,x1,x2) = x1
|  |
|  `- f9(x0,x1,x2) = x2
|
+- Constraints
|  |
|  +- f160(x46) = x46 >= x46 = x46
|  |
|  +- f161(x47) = x47 >= x47 = x47
|  |
|  +- f7(x46,x47,f162()) = 0 >= 0 = f1(f160(x46),f161(x47))
|  |
|  +- f163(x2) = x2 >= x2 = x2
|  |
|  +- f164(x1) = x1 >= x1 = x1
|  |
|  +- f6(x1,x2) = x2 >= x2 = f9(f162(),f164(x1),f163(x2))
|  |
|  +- f5(x1,x2) = x1 >= x1 = f8(f162(),f164(x1),f163(x2))
|  |
|  +- f165(x5) = x5 >= x5 = x5
|  |
|  +- f166(x6) = x6 >= x6 = x6
|  |
|  +- f1(x5 + 1,x6 + 1) = 0 >= 0 = f1(f165(x5),f166(x6))
|  |
|  +- f1(x9 + 1,0) = 0 >= 0 = 0
|  |
|  +- f1(0,x11) = 0 >= 0 = 0
|  |
|  +- f9(x12,x13,0) = 0 >= 0 = 0
|  |
|  +- f8(x12,x13,0) = x13 >= 0 = f167()
|  |
|  +- f168(x66) = x66 >= x66 = x66
|  |
|  +- f169(x67) = x67 >= x67 = x67
|  |
|  +- f2(x66,x67,f170(x18)) = 0 >= 0 = f7(f168(x66),f169(x67),x18)
|  |
|  +- f171(x19) = x19 >= x19 = x19
|  |
|  +- f172(x82) = x82 >= x82 = x82
|  |
|  +- f173(x83) = x83 >= x83 = x83
|  |
|  +- f7(x82,x83,f174(x18)) = 0 >= 0 = f7(f172(x82),f173(x83),x18)
|  |
|  +- f175(x22) = x22 >= x22 = x22
|  |
|  +- f176(x19) = x19 >= x19 = x19
|  |
|  +- f177(x18,x19,x22,x82,x83) = x22 >= x22 = f9(f174(x18),f176(x19),f175(x22))
|  |
|  +- f178(x18,x19,x22,x82,x83) = x19 >= x19 = f8(f174(x18),f176(x19),f175(x22))
|  |
|  +- f9(x18,x19,x22 + 1) = x22 + 1 >= 1 + x22 = f4(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|  |
|  +- f8(x18,x19,x22 + 1) = x19 >= max(x19,x19) = f3(f170(x18),f171(x19),f178(x18,x19,x22,x82,x83),f177(x18,x19,x22,x82,x83))
|  |
|  +- f179(x26) = x26 >= x26 = x26
|  |
|  +- f180(x27) = x27 >= x27 = x27
|  |
|  +- f181(x26,x27) = max(x27,x26) >= x26 = x26
|  |
|  +- f182(x27) = x27 >= x27 = x27
|  |
|  +- f183(x30) = x30 >= x30 = x30
|  |
|  +- f184(x30) = x30 + 1 >= x30 + 1 = f183(x30) + 1
|  |
|  +- f181(x26,x27) = max(x27,x26) >= x27 = f182(x27)
|  |
|  +- f185(x25,x26,x27,x30,x134,x135) = max(x26,x27) >= max(x27,x26) = f181(x26,x27)
|  |
|  +- f186(x25,x26,x27,x30,x134,x135) = 2 + x30 >= (x30 + 1) + 1 = f184(x30) + 1
|  |
|  +- f187(x25,x26,x27,x30,x134,x135) = max(x26,x27) >= x27 = x27
|  |
|  +- f188(x134) = x134 >= x134 = x134
|  |
|  +- f189(x135) = x135 >= x135 = x135
|  |
|  +- f2(x134,x135,f190(x25)) = 0 >= 0 = f2(f188(x134),f189(x135),x25)
|  |
|  +- f191(x26) = x26 >= x26 = x26
|  |
|  +- f192(x30) = x30 >= x30 = x30
|  |
|  +- f193(x27) = x27 >= x27 = x27
|  |
|  +- f194(x25,x26,x27,x30,x134,x135) = 1 + x30 >= 1 + x30 = f4(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- f187(x25,x26,x27,x30,x134,x135) = max(x26,x27) >= max(x27,x26) = f3(f190(x25),f191(x26),f193(x27),f192(x30))
|  |
|  +- f186(x25,x26,x27,x30,x134,x135) = 2 + x30 >= (1 + x30) + 1 = f194(x25,x26,x27,x30,x134,x135) + 1
|  |
|  +- f185(x25,x26,x27,x30,x134,x135) = max(x26,x27) >= max(x26,x27) = f187(x25,x26,x27,x30,x134,x135)
|  |
|  +- f4(x25,x26,x27,x30 + 1) = 1 + (x30 + 1) >= 2 + x30 = f186(x25,x26,x27,x30,x134,x135)
|  |
|  +- f3(x25,x26,x27,x30 + 1) = max(x27,x26) >= max(x26,x27) = f185(x25,x26,x27,x30,x134,x135)
|  |
|  +- f195(x34) = x34 >= x34 = x34
|  |
|  +- f196() = 0 >= 0 = 0
|  |
|  +- f195(x34) = x34 >= 0 = f197()
|  |
|  +- f4(x33,x34,x35,0) = 1 >= 1 = f196() + 1
|  |
|  `- f3(x33,x34,x35,0) = max(x35,x34) >= x34 = f195(x34)
|
`- Stopping timer: 2017-03-30 07:31:47.869596 UTC(+0.22469s)