SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f18(x0) = x0;
f19(x0) = x0;
f20(x0,x1) = x0 + x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:29.91681 UTC
   |
   +- Open Constraints
   |  |
   |  +- f18(x5) = f18(x5) >= x5 = x5
   |  |
   |  +- f19(x3) = f19(x3) >= x3 = x3
   |  |
   |  +- f20(x3,x5) = f20(x3,x5) >= f1(f18(x5),f19(x3)) = f1(f18(x5),f19(x3))
   |  |
   |  +- f1(x5 + 1,x3) = f1(x5 + 1,x3) >= f20(x3,x5) + 1 = f20(x3,x5) + 1
   |  |
   |  `- f1(0,x8) = f1(0,x8) >= x8 = x8
   |
   +- Simplification ...
   |  |
   |  +- Propagated: f18(x0) ↦ x0
   |  |
   |  `- Propagated: f19(x0) ↦ x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:29.916919 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 8 + x0 + x1
   |  |  |
   |  |  `- f20(x0,x1) = 8 + x0 + x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f20(x0,x1) = x0 + x1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with ShiftMax... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:29.931114 UTC(+0.014195s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + x1
   |  |
   |  +- f18(x0) = x0
   |  |
   |  +- f19(x0) = x0
   |  |
   |  `- f20(x0,x1) = x0 + x1
   |
   +- Constraints
   |  |
   |  +- f18(x5) = x5 >= x5 = x5
   |  |
   |  +- f19(x3) = x3 >= x3 = x3
   |  |
   |  +- f20(x3,x5) = x3 + x5 >= x5 + x3 = f1(f18(x5),f19(x3))
   |  |
   |  +- f1(x5 + 1,x3) = (x5 + 1) + x3 >= (x3 + x5) + 1 = f20(x3,x5) + 1
   |  |
   |  `- f1(0,x8) = x8 >= x8 = x8
   |
   `- Stopping timer: 2017-03-30 07:32:29.931176 UTC(+0.014366s)