SUCCESS(2)

SUCCESS
f1(x0,x1) = 1 + x0;
f110(x0) = x0;
f111(x0) = x0;
f112(x0) = x0;
f113() = 0;
f114(x0) = x0;
f115(x0) = x0;
f116() = 0;
f117(x0) = x0;
f118(x0) = x0;
f119(x0) = x0;
f120(x0) = x0;
f121(x0) = 0;
f122(x0) = x0;
f123(x0) = x0;
f124(x0,x1,x2,x3) = x1 + x2;
f125(x0) = x0;
f126(x0) = x0;
f127(x0) = x0;
f128(x0) = x0;
f129(x0,x1,x2,x3) = x0*x2 + x1;
f2(x0,x1,x2) = x1 + x2;
f3(x0,x1) = x0 + x1;
f4(x0,x1,x2) = x0*x2 + x1;
f5(x0) = 1 + x0;
f6(x0,x1) = x0 + x1;
f7(x0,x1) = x0*x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:43:55.249714 UTC
   |
   +- Open Constraints
   |  |
   |  +- f110(x4) = f110(x4) >= x4 = x4
   |  |
   |  +- f111(x50) = f111(x50) >= x50 = x50
   |  |
   |  +- f3(x50,f112(x4)) = f3(x50,f112(x4)) >= f6(f110(x4),f111(x50)) = f6(f110(x4),f111(x50))
   |  |
   |  +- f113() = f113() >= 0 = 0
   |  |
   |  +- f114(x3) = f114(x3) >= x3 = x3
   |  |
   |  +- f7(x3,x4) = f7(x3,x4) >= f4(f112(x4),f113(),f114(x3)) = f4(f112(x4),f113(),f114(x3))
   |  |
   |  +- f115(x66) = f115(x66) >= x66 = x66
   |  |
   |  +- f1(x66,f116()) = f1(x66,f116()) >= f5(f115(x66)) = f5(f115(x66))
   |  |
   |  +- f117(x8) = f117(x8) >= x8 = x8
   |  |
   |  +- f118(x7) = f118(x7) >= x7 = x7
   |  |
   |  +- f6(x7,x8) = f6(x7,x8) >= f2(f116(),f117(x8),f118(x7)) = f2(f116(),f117(x8),f118(x7))
   |  |
   |  +- f119(x11) = f119(x11) >= x11 = x11
   |  |
   |  +- f5(x11) = f5(x11) >= f119(x11) + 1 = f119(x11) + 1
   |  |
   |  +- f120(x85) = f120(x85) >= x85 = x85
   |  |
   |  +- f1(x85,f121(x14)) = f1(x85,f121(x14)) >= f1(f120(x85),x14) = f1(f120(x85),x14)
   |  |
   |  +- f122(x15) = f122(x15) >= x15 = x15
   |  |
   |  +- f123(x18) = f123(x18) >= x18 = x18
   |  |
   |  +- f124(x14,x15,x18,x85) = f124(x14,x15,x18,x85) >= f2(f121(x14),f122(x15),f123(x18)) = f2(f121(x14),f122(x15),f123(x18))
   |  |
   |  +- f2(x14,x15,x18 + 1) = f2(x14,x15,x18 + 1) >= f1(f124(x14,x15,x18,x85),x14) = f1(f124(x14,x15,x18,x85),x14)
   |  |
   |  +- f2(x22,x23,0) = f2(x22,x23,0) >= x23 = x23
   |  |
   |  +- f125(x103) = f125(x103) >= x103 = x103
   |  |
   |  +- f3(x103,f126(x29)) = f3(x103,f126(x29)) >= f3(f125(x103),x29) = f3(f125(x103),x29)
   |  |
   |  +- f127(x30) = f127(x30) >= x30 = x30
   |  |
   |  +- f128(x33) = f128(x33) >= x33 = x33
   |  |
   |  +- f129(x29,x30,x33,x103) = f129(x29,x30,x33,x103) >= f4(f126(x29),f127(x30),f128(x33)) = f4(f126(x29),f127(x30),f128(x33))
   |  |
   |  +- f4(x29,x30,x33 + 1) = f4(x29,x30,x33 + 1) >= f3(f129(x29,x30,x33,x103),x29) = f3(f129(x29,x30,x33,x103),x29)
   |  |
   |  `- f4(x37,x38,0) = f4(x37,x38,0) >= x38 = x38
   |
   +- Simplification ...
   |  |
   |  +- Substituted: f124(x14,x15,x18,x85) ≥ f2(f121(x14),f122(x15),f123(x18)) ↦ f124(x14,x15,x18,0) ≥ f2(f121(x14),f122(x15),f123(x18))
   |  |
   |  +- Substituted: f2(x22,x23,0) ≥ x23 ↦ f2(0,x23,0) ≥ x23
   |  |
   |  +- Substituted: f129(x29,x30,x33,x103) ≥ f4(f126(x29),f127(x30),f128(x33)) ↦ f129(x29,x30,x33,0) ≥ f4(f126(x29),f127(x30),f128(x33))
   |  |
   |  +- Substituted: f4(x37,x38,0) ≥ x38 ↦ f4(0,x38,0) ≥ x38
   |  |
   |  +- Propagated: f110(x0) ↦ x0
   |  |
   |  +- Propagated: f111(x0) ↦ x0
   |  |
   |  +- Propagated: f113() ↦ 0
   |  |
   |  +- Propagated: f114(x0) ↦ x0
   |  |
   |  +- Propagated: f115(x0) ↦ x0
   |  |
   |  +- Propagated: f117(x0) ↦ x0
   |  |
   |  +- Propagated: f118(x0) ↦ x0
   |  |
   |  +- Propagated: f119(x0) ↦ x0
   |  |
   |  +- Propagated: f120(x0) ↦ x0
   |  |
   |  +- Propagated: f122(x0) ↦ x0
   |  |
   |  +- Propagated: f123(x0) ↦ x0
   |  |
   |  +- Propagated: f125(x0) ↦ x0
   |  |
   |  +- Propagated: f127(x0) ↦ x0
   |  |
   |  +- Propagated: f128(x0) ↦ x0
   |  |
   |  `- Propagated: f5(x0) ↦ 1 + x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:43:55.250088 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:43:55.420546 UTC(+0.170458s)
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:43:55.420562 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:43:55.431735 UTC(+0.011173s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:43:55.431742 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:43:56.457405 UTC(+1.025663s)
   |
   +- SMT-MMI(2) ...
   |  |
   |  +- Staring timer: 2017-03-30 07:43:56.457412 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f112(x0) = x0
   |  |  |
   |  |  +- f116() = 0
   |  |  |
   |  |  +- f121(x0) = 0
   |  |  |
   |  |  +- f124(x0,x1,x2,x3) = 7*x0*x1 + x1 + x2
   |  |  |
   |  |  +- f126(x0) = x0
   |  |  |
   |  |  +- f129(x0,x1,x2,x3) = 8 + 13*x0 + 4*x0*x2 + 8*x1 + 5*x1*x2 + x2
   |  |  |
   |  |  +- f2(x0,x1,x2) = 8*x0*x1 + 2*x0*x2 + x1 + x2
   |  |  |
   |  |  +- f3(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 7 + 10*x0 + 4*x0*x2 + 3*x1 + 5*x1*x2 + x2
   |  |  |
   |  |  +- f6(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f7(x0,x1) = 9 + 15*x0 + 10*x0*x1 + 12*x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f112(x0) = x0
   |  |  |
   |  |  +- f116() = 0
   |  |  |
   |  |  +- f121(x0) = 0
   |  |  |
   |  |  +- f124(x0,x1,x2,x3) = x1 + x2
   |  |  |
   |  |  +- f126(x0) = x0
   |  |  |
   |  |  +- f129(x0,x1,x2,x3) = x0 + x0*x2 + x1
   |  |  |
   |  |  +- f2(x0,x1,x2) = x1 + x2
   |  |  |
   |  |  +- f3(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = x0 + x0*x2 + x1
   |  |  |
   |  |  +- f6(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f7(x0,x1) = x0*x1 + x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f112(x0) = x0
   |  |  |
   |  |  +- f116() = 0
   |  |  |
   |  |  +- f121(x0) = 0
   |  |  |
   |  |  +- f124(x0,x1,x2,x3) = x1 + x2
   |  |  |
   |  |  +- f126(x0) = x0
   |  |  |
   |  |  +- f129(x0,x1,x2,x3) = x0*x2 + x1
   |  |  |
   |  |  +- f2(x0,x1,x2) = x1 + x2
   |  |  |
   |  |  +- f3(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = x0*x2 + x1
   |  |  |
   |  |  +- f6(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f7(x0,x1) = x0*x1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:43:56.651605 UTC(+0.194193s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 1 + x0
   |  |
   |  +- f110(x0) = x0
   |  |
   |  +- f111(x0) = x0
   |  |
   |  +- f112(x0) = x0
   |  |
   |  +- f113() = 0
   |  |
   |  +- f114(x0) = x0
   |  |
   |  +- f115(x0) = x0
   |  |
   |  +- f116() = 0
   |  |
   |  +- f117(x0) = x0
   |  |
   |  +- f118(x0) = x0
   |  |
   |  +- f119(x0) = x0
   |  |
   |  +- f120(x0) = x0
   |  |
   |  +- f121(x0) = 0
   |  |
   |  +- f122(x0) = x0
   |  |
   |  +- f123(x0) = x0
   |  |
   |  +- f124(x0,x1,x2,x3) = x1 + x2
   |  |
   |  +- f125(x0) = x0
   |  |
   |  +- f126(x0) = x0
   |  |
   |  +- f127(x0) = x0
   |  |
   |  +- f128(x0) = x0
   |  |
   |  +- f129(x0,x1,x2,x3) = x0*x2 + x1
   |  |
   |  +- f2(x0,x1,x2) = x1 + x2
   |  |
   |  +- f3(x0,x1) = x0 + x1
   |  |
   |  +- f4(x0,x1,x2) = x0*x2 + x1
   |  |
   |  +- f5(x0) = 1 + x0
   |  |
   |  +- f6(x0,x1) = x0 + x1
   |  |
   |  `- f7(x0,x1) = x0*x1
   |
   +- Constraints
   |  |
   |  +- f110(x4) = x4 >= x4 = x4
   |  |
   |  +- f111(x50) = x50 >= x50 = x50
   |  |
   |  +- f3(x50,f112(x4)) = x50 + x4 >= x4 + x50 = f6(f110(x4),f111(x50))
   |  |
   |  +- f113() = 0 >= 0 = 0
   |  |
   |  +- f114(x3) = x3 >= x3 = x3
   |  |
   |  +- f7(x3,x4) = x3 * x4 >= x4 * x3 = f4(f112(x4),f113(),f114(x3))
   |  |
   |  +- f115(x66) = x66 >= x66 = x66
   |  |
   |  +- f1(x66,f116()) = 1 + x66 >= x66 + 1 = f5(f115(x66))
   |  |
   |  +- f117(x8) = x8 >= x8 = x8
   |  |
   |  +- f118(x7) = x7 >= x7 = x7
   |  |
   |  +- f6(x7,x8) = x7 + x8 >= x8 + x7 = f2(f116(),f117(x8),f118(x7))
   |  |
   |  +- f119(x11) = x11 >= x11 = x11
   |  |
   |  +- f5(x11) = x11 + 1 >= x11 + 1 = f119(x11) + 1
   |  |
   |  +- f120(x85) = x85 >= x85 = x85
   |  |
   |  +- f1(x85,f121(x14)) = 1 + x85 >= 1 + x85 = f1(f120(x85),x14)
   |  |
   |  +- f122(x15) = x15 >= x15 = x15
   |  |
   |  +- f123(x18) = x18 >= x18 = x18
   |  |
   |  +- f124(x14,x15,x18,x85) = x15 + x18 >= x15 + x18 = f2(f121(x14),f122(x15),f123(x18))
   |  |
   |  +- f2(x14,x15,x18 + 1) = x15 + (x18 + 1) >= 1 + (x15 + x18) = f1(f124(x14,x15,x18,x85),x14)
   |  |
   |  +- f2(x22,x23,0) = x23 >= x23 = x23
   |  |
   |  +- f125(x103) = x103 >= x103 = x103
   |  |
   |  +- f3(x103,f126(x29)) = x103 + x29 >= x103 + x29 = f3(f125(x103),x29)
   |  |
   |  +- f127(x30) = x30 >= x30 = x30
   |  |
   |  +- f128(x33) = x33 >= x33 = x33
   |  |
   |  +- f129(x29,x30,x33,x103) = (x29 * x33) + x30 >= (x29 * x33) + x30 = f4(f126(x29),f127(x30),f128(x33))
   |  |
   |  +- f4(x29,x30,x33 + 1) = (x29 * (x33 + 1)) + x30 >= ((x29 * x33) + x30) + x29 = f3(f129(x29,x30,x33,x103),x29)
   |  |
   |  `- f4(x37,x38,0) = x38 >= x38 = x38
   |
   `- Stopping timer: 2017-03-30 07:43:56.651701 UTC(+1.401987s)