SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f2(x0) = x0;
f26(x0) = x0;
f27() = 0;
f28(x0) = x0;
f29(x0) = x0;
f30(x0) = 1 + x0;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:40.637484 UTC
   |
   +- Open Constraints
   |  |
   |  +- f26(x2) = f26(x2) >= x2 = x2
   |  |
   |  +- f27() = f27() >= 0 = 0
   |  |
   |  +- f2(x2) = f2(x2) >= f1(f26(x2),f27()) = f1(f26(x2),f27())
   |  |
   |  +- f28(x7) = f28(x7) >= x7 = x7
   |  |
   |  +- f29(x5) = f29(x5) >= x5 = x5
   |  |
   |  +- f30(x5) = f30(x5) >= f29(x5) + 1 = f29(x5) + 1
   |  |
   |  +- f1(x7 + 1,x5) = f1(x7 + 1,x5) >= f1(f28(x7),f30(x5)) = f1(f28(x7),f30(x5))
   |  |
   |  `- f1(0,x10) = f1(0,x10) >= x10 = x10
   |
   +- Simplification ...
   |  |
   |  +- Propagated: f26(x0) ↦ x0
   |  |
   |  +- Propagated: f27() ↦ 0
   |  |
   |  +- Propagated: f28(x0) ↦ x0
   |  |
   |  +- Propagated: f29(x0) ↦ x0
   |  |
   |  `- Propagated: f30(x0) ↦ 1 + x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:40.637667 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f2(x0) = 14 + x0
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f2(x0) = x0
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with ShiftMax... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:40.646818 UTC(+0.009151s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + x1
   |  |
   |  +- f2(x0) = x0
   |  |
   |  +- f26(x0) = x0
   |  |
   |  +- f27() = 0
   |  |
   |  +- f28(x0) = x0
   |  |
   |  +- f29(x0) = x0
   |  |
   |  `- f30(x0) = 1 + x0
   |
   +- Constraints
   |  |
   |  +- f26(x2) = x2 >= x2 = x2
   |  |
   |  +- f27() = 0 >= 0 = 0
   |  |
   |  +- f2(x2) = x2 >= x2 = f1(f26(x2),f27())
   |  |
   |  +- f28(x7) = x7 >= x7 = x7
   |  |
   |  +- f29(x5) = x5 >= x5 = x5
   |  |
   |  +- f30(x5) = x5 + 1 >= x5 + 1 = f29(x5) + 1
   |  |
   |  +- f1(x7 + 1,x5) = (x7 + 1) + x5 >= x7 + (x5 + 1) = f1(f28(x7),f30(x5))
   |  |
   |  `- f1(0,x10) = x10 >= x10 = x10
   |
   `- Stopping timer: 2017-03-30 07:32:40.64685 UTC(+0.009366s)