SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f2(x0,x1) = 2*x0 + x1;
f3(x0,x1) = x0 + x1;
f4(x0,x1) = 2*x0 + x1;
f41(x0) = x0;
f42(x0) = x0;
f43(x0) = x0;
f44(x0) = x0;
f45(x0) = x0;
f46(x0) = x0;
f47(x0,x1) = x0 + x1;
f48(x0) = x0;
f49(x0,x1) = x0 + x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:17.353324 UTC
   |
   +- Open Constraints
   |  |
   |  +- f41(x2) = f41(x2) >= x2 = x2
   |  |
   |  +- f42(x21) = f42(x21) >= x21 = x21
   |  |
   |  +- f3(x21,f43(x2)) = f3(x21,f43(x2)) >= f1(f41(x2),f42(x21)) = f1(f41(x2),f42(x21))
   |  |
   |  +- f44(x3) = f44(x3) >= x3 = x3
   |  |
   |  +- f2(x2,x3) = f2(x2,x3) >= f4(f43(x2),f44(x3)) = f4(f43(x2),f44(x3))
   |  |
   |  +- f45(x8) = f45(x8) >= x8 = x8
   |  |
   |  +- f46(x6) = f46(x6) >= x6 = x6
   |  |
   |  +- f47(x6,x8) = f47(x6,x8) >= f1(f45(x8),f46(x6)) = f1(f45(x8),f46(x6))
   |  |
   |  +- f1(x8 + 1,x6) = f1(x8 + 1,x6) >= f47(x6,x8) + 1 = f47(x6,x8) + 1
   |  |
   |  +- f1(0,x11) = f1(0,x11) >= x11 = x11
   |  |
   |  +- f48(x15) = f48(x15) >= x15 = x15
   |  |
   |  +- f49(x14,x15) = f49(x14,x15) >= f3(f48(x15),x14) = f3(f48(x15),x14)
   |  |
   |  `- f4(x14,x15) = f4(x14,x15) >= f3(f49(x14,x15),x14) = f3(f49(x14,x15),x14)
   |
   +- Simplification ...
   |  |
   |  +- Propagated: f41(x0) ↦ x0
   |  |
   |  +- Propagated: f42(x0) ↦ x0
   |  |
   |  +- Propagated: f44(x0) ↦ x0
   |  |
   |  +- Propagated: f45(x0) ↦ x0
   |  |
   |  +- Propagated: f46(x0) ↦ x0
   |  |
   |  `- Propagated: f48(x0) ↦ x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:17.353715 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:17.397397 UTC(+0.043682s)
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:17.397435 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:17.425443 UTC(+0.028008s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:17.425454 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 15 + 14*x0 + 14*x1
   |  |  |
   |  |  +- f3(x0,x1) = 2*x0 + x1
   |  |  |
   |  |  +- f4(x0,x1) = 3 + 12*x0 + 14*x1
   |  |  |
   |  |  +- f43(x0) = 1 + x0
   |  |  |
   |  |  +- f47(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  `- f49(x0,x1) = 1 + 5*x0 + 7*x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 2 + 2*x0 + x1
   |  |  |
   |  |  +- f3(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f4(x0,x1) = 2*x0 + x1
   |  |  |
   |  |  +- f43(x0) = 1 + x0
   |  |  |
   |  |  +- f47(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  `- f49(x0,x1) = x0 + x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 2 + 2*x0 + x1
   |  |  |
   |  |  +- f3(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f4(x0,x1) = 2*x0 + x1
   |  |  |
   |  |  +- f43(x0) = 1 + x0
   |  |  |
   |  |  +- f47(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f49(x0,x1) = x0 + x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 2*x0 + x1
   |  |  |
   |  |  +- f3(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f4(x0,x1) = 2*x0 + x1
   |  |  |
   |  |  +- f43(x0) = x0
   |  |  |
   |  |  +- f47(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f49(x0,x1) = x0 + x1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:17.487633 UTC(+0.062179s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + x1
   |  |
   |  +- f2(x0,x1) = 2*x0 + x1
   |  |
   |  +- f3(x0,x1) = x0 + x1
   |  |
   |  +- f4(x0,x1) = 2*x0 + x1
   |  |
   |  +- f41(x0) = x0
   |  |
   |  +- f42(x0) = x0
   |  |
   |  +- f43(x0) = x0
   |  |
   |  +- f44(x0) = x0
   |  |
   |  +- f45(x0) = x0
   |  |
   |  +- f46(x0) = x0
   |  |
   |  +- f47(x0,x1) = x0 + x1
   |  |
   |  +- f48(x0) = x0
   |  |
   |  `- f49(x0,x1) = x0 + x1
   |
   +- Constraints
   |  |
   |  +- f41(x2) = x2 >= x2 = x2
   |  |
   |  +- f42(x21) = x21 >= x21 = x21
   |  |
   |  +- f3(x21,f43(x2)) = x21 + x2 >= x2 + x21 = f1(f41(x2),f42(x21))
   |  |
   |  +- f44(x3) = x3 >= x3 = x3
   |  |
   |  +- f2(x2,x3) = (2 * x2) + x3 >= (2 * x2) + x3 = f4(f43(x2),f44(x3))
   |  |
   |  +- f45(x8) = x8 >= x8 = x8
   |  |
   |  +- f46(x6) = x6 >= x6 = x6
   |  |
   |  +- f47(x6,x8) = x6 + x8 >= x8 + x6 = f1(f45(x8),f46(x6))
   |  |
   |  +- f1(x8 + 1,x6) = (x8 + 1) + x6 >= (x6 + x8) + 1 = f47(x6,x8) + 1
   |  |
   |  +- f1(0,x11) = x11 >= x11 = x11
   |  |
   |  +- f48(x15) = x15 >= x15 = x15
   |  |
   |  +- f49(x14,x15) = x14 + x15 >= x15 + x14 = f3(f48(x15),x14)
   |  |
   |  `- f4(x14,x15) = (2 * x14) + x15 >= (x14 + x15) + x14 = f3(f49(x14,x15),x14)
   |
   `- Stopping timer: 2017-03-30 07:32:17.487696 UTC(+0.134372s)