SUCCESS(2)

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*x2;
f179(x0) = x0;
f180(x0) = x0;
f181(x0,x1) = x0 + x1;
f182(x0) = x0;
f183(x0) = x0;
f184(x0) = 1 + x0;
f185(x0,x1,x2,x3,x4,x5) = x1 + x2;
f186(x0,x1,x2,x3,x4,x5) = 2 + x3;
f187(x0,x1,x2,x3,x4,x5) = 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) = x1 + x2;
f4(x0,x1,x2,x3) = 1 + x3;
f5(x0,x1) = x0*x1;
f6(x0,x1) = x1;
f7(x0,x1,x2) = 0;
f8(x0,x1,x2) = x1*x2;
f9(x0,x1,x2) = x2;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:31:26.175455 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)
   |
   +- 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
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:31:26.376692 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:31:26.403574 UTC(+0.026882s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:31:26.403582 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:31:26.52692 UTC(+0.123338s)
   |
   +- SMT-MMI(2) ...
   |  |
   |  +- Staring timer: 2017-03-30 07:31:26.526929 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 2 + 2*x0
   |  |  |
   |  |  +- f162() = 0
   |  |  |
   |  |  +- f170(x0) = 15 + 2*x0
   |  |  |
   |  |  +- f174(x0) = 0
   |  |  |
   |  |  +- f177(x0,x1,x2,x3,x4) = 11 + 6*x0 + 3*x0*x1 + 4*x0*x2 + 8*x2
   |  |  |
   |  |  +- f178(x0,x1,x2,x3,x4) = 11 + 15*x0 + 4*x0*x1 + 15*x1 + 12*x1*x2 + 6*x2
   |  |  |
   |  |  +- f181(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f185(x0,x1,x2,x3,x4,x5) = 2*x1 + x2
   |  |  |
   |  |  +- f186(x0,x1,x2,x3,x4,x5) = 5 + x3
   |  |  |
   |  |  +- f187(x0,x1,x2,x3,x4,x5) = 2*x1 + x2
   |  |  |
   |  |  +- f190(x0) = 3 + 4*x0
   |  |  |
   |  |  +- f194(x0,x1,x2,x3,x4,x5) = 4 + x3
   |  |  |
   |  |  +- f195(x0) = x0
   |  |  |
   |  |  +- f2(x0,x1,x2) = 12 + 3*x0 + 15*x0*x1 + 15*x0*x2 + 11*x1 + 15*x1*x2 + 4*x2
   |  |  |
   |  |  +- f3(x0,x1,x2,x3) = 2*x1 + x2
   |  |  |
   |  |  +- f4(x0,x1,x2,x3) = 4 + x3
   |  |  |
   |  |  +- f5(x0,x1) = 15 + 15*x0 + 14*x0*x1 + 8*x1
   |  |  |
   |  |  +- f6(x0,x1) = 9 + 14*x0 + 14*x0*x1 + 14*x1
   |  |  |
   |  |  +- f7(x0,x1,x2) = 9 + 8*x0 + 15*x0*x1 + x1
   |  |  |
   |  |  +- f8(x0,x1,x2) = 9 + x0 + 5*x0*x1 + 14*x0*x2 + 9*x1 + 12*x1*x2 + 6*x2
   |  |  |
   |  |  `- f9(x0,x1,x2) = 7 + 8*x0 + 8*x0*x1 + 10*x0*x2 + 8*x2
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 0
   |  |  |
   |  |  +- f162() = 0
   |  |  |
   |  |  +- f170(x0) = 0
   |  |  |
   |  |  +- f174(x0) = 0
   |  |  |
   |  |  +- f177(x0,x1,x2,x3,x4) = x2
   |  |  |
   |  |  +- f178(x0,x1,x2,x3,x4) = x1 + x1*x2
   |  |  |
   |  |  +- f181(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f185(x0,x1,x2,x3,x4,x5) = x1 + x2
   |  |  |
   |  |  +- f186(x0,x1,x2,x3,x4,x5) = 2 + x3
   |  |  |
   |  |  +- f187(x0,x1,x2,x3,x4,x5) = x1 + x2
   |  |  |
   |  |  +- f190(x0) = 0
   |  |  |
   |  |  +- f194(x0,x1,x2,x3,x4,x5) = 1 + x3
   |  |  |
   |  |  +- f195(x0) = x0
   |  |  |
   |  |  +- f2(x0,x1,x2) = 0
   |  |  |
   |  |  +- f3(x0,x1,x2,x3) = x1 + x2
   |  |  |
   |  |  +- f4(x0,x1,x2,x3) = 1 + x3
   |  |  |
   |  |  +- f5(x0,x1) = x0 + x0*x1
   |  |  |
   |  |  +- f6(x0,x1) = x1
   |  |  |
   |  |  +- f7(x0,x1,x2) = 0
   |  |  |
   |  |  +- f8(x0,x1,x2) = x1 + x1*x2
   |  |  |
   |  |  `- f9(x0,x1,x2) = x2
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 0
   |  |  |
   |  |  +- f162() = 0
   |  |  |
   |  |  +- f170(x0) = 0
   |  |  |
   |  |  +- f174(x0) = 0
   |  |  |
   |  |  +- f177(x0,x1,x2,x3,x4) = x2
   |  |  |
   |  |  +- f178(x0,x1,x2,x3,x4) = x1*x2
   |  |  |
   |  |  +- f181(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f185(x0,x1,x2,x3,x4,x5) = x1 + x2
   |  |  |
   |  |  +- f186(x0,x1,x2,x3,x4,x5) = 2 + x3
   |  |  |
   |  |  +- f187(x0,x1,x2,x3,x4,x5) = x1 + x2
   |  |  |
   |  |  +- f190(x0) = 0
   |  |  |
   |  |  +- f194(x0,x1,x2,x3,x4,x5) = 1 + x3
   |  |  |
   |  |  +- f195(x0) = x0
   |  |  |
   |  |  +- f2(x0,x1,x2) = 0
   |  |  |
   |  |  +- f3(x0,x1,x2,x3) = x1 + x2
   |  |  |
   |  |  +- f4(x0,x1,x2,x3) = 1 + x3
   |  |  |
   |  |  +- f5(x0,x1) = x0*x1
   |  |  |
   |  |  +- f6(x0,x1) = x1
   |  |  |
   |  |  +- f7(x0,x1,x2) = 0
   |  |  |
   |  |  +- f8(x0,x1,x2) = x1*x2
   |  |  |
   |  |  `- f9(x0,x1,x2) = x2
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:31:47.634416 UTC(+21.107487s)
   |
   +- 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*x2
   |  |
   |  +- f179(x0) = x0
   |  |
   |  +- f180(x0) = x0
   |  |
   |  +- f181(x0,x1) = x0 + x1
   |  |
   |  +- f182(x0) = x0
   |  |
   |  +- f183(x0) = x0
   |  |
   |  +- f184(x0) = 1 + x0
   |  |
   |  +- f185(x0,x1,x2,x3,x4,x5) = x1 + x2
   |  |
   |  +- f186(x0,x1,x2,x3,x4,x5) = 2 + x3
   |  |
   |  +- f187(x0,x1,x2,x3,x4,x5) = 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) = x1 + x2
   |  |
   |  +- f4(x0,x1,x2,x3) = 1 + x3
   |  |
   |  +- f5(x0,x1) = x0*x1
   |  |
   |  +- f6(x0,x1) = x1
   |  |
   |  +- f7(x0,x1,x2) = 0
   |  |
   |  +- f8(x0,x1,x2) = x1*x2
   |  |
   |  `- 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 * x2 >= x1 * x2 = 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) = 0 >= 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 * x22 >= x19 * x22 = 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 * (x22 + 1) >= x19 + (x19 * x22) = 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) = 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) = x26 + x27 >= x27 = f182(x27)
   |  |
   |  +- f185(x25,x26,x27,x30,x134,x135) = x26 + x27 >= x26 + x27 = 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) = 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) = x26 + x27 >= x26 + x27 = 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) = x26 + x27 >= 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) = x26 + x27 >= 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) = x34 + x35 >= x34 = f195(x34)
   |
   `- Stopping timer: 2017-03-30 07:31:47.634641 UTC(+21.459186s)