SUCCESS(1)

SUCCESS
f1(x0) = 0;
f2(x0,x1) = x0;
f3(x0,x1) = 0;
f4(x0) = x0;
f46(x0) = x0;
f47() = 0;
f48(x0) = x0;
f49(x0) = x0;
f50(x0) = 0;
f51(x0) = x0;
f52(x0,x1) = x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:29:55.475687 UTC
   |
   +- Open Constraints
   |  |
   |  +- f46(x27) = f46(x27) >= x27 = x27
   |  |
   |  +- f2(x27,f47()) = f2(x27,f47()) >= f4(f46(x27)) = f4(f46(x27))
   |  |
   |  +- f48(x3) = f48(x3) >= x3 = x3
   |  |
   |  +- f1(x3) = f1(x3) >= f3(f47(),f48(x3)) = f3(f47(),f48(x3))
   |  |
   |  +- f4(x7 + 1) = f4(x7 + 1) >= x7 = x7
   |  |
   |  +- f49(x37) = f49(x37) >= x37 = x37
   |  |
   |  +- f2(x37,f50(x10)) = f2(x37,f50(x10)) >= f2(f49(x37),x10) = f2(f49(x37),x10)
   |  |
   |  +- f51(x13) = f51(x13) >= x13 = x13
   |  |
   |  +- f52(x10,x13) = f52(x10,x13) >= f2(f51(x13),x10) = f2(f51(x13),x10)
   |  |
   |  +- f3(x10,x13 + 1) = f3(x10,x13 + 1) >= f3(f50(x10),f52(x10,x13)) = f3(f50(x10),f52(x10,x13))
   |  |
   |  `- f3(x17,0) = f3(x17,0) >= 0 = 0
   |
   +- Simplification ...
   |  |
   |  +- Substituted: f3(x17,0) ≥ 0 ↦ f3(0,0) ≥ 0
   |  |
   |  +- Propagated: f46(x0) ↦ x0
   |  |
   |  +- Propagated: f48(x0) ↦ x0
   |  |
   |  +- Propagated: f49(x0) ↦ x0
   |  |
   |  `- Propagated: f51(x0) ↦ x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:29:55.475904 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 15
   |  |  |
   |  |  +- f2(x0,x1) = x0
   |  |  |
   |  |  +- f3(x0,x1) = max(8,7 + x0)
   |  |  |
   |  |  +- f4(x0) = x0
   |  |  |
   |  |  +- f47() = 0
   |  |  |
   |  |  +- f50(x0) = x0
   |  |  |
   |  |  `- f52(x0,x1) = max(14 + x0 + x1,15 + x1)
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 0
   |  |  |
   |  |  +- f2(x0,x1) = x0
   |  |  |
   |  |  +- f3(x0,x1) = 0
   |  |  |
   |  |  +- f4(x0) = x0
   |  |  |
   |  |  +- f47() = 0
   |  |  |
   |  |  +- f50(x0) = 0
   |  |  |
   |  |  `- f52(x0,x1) = x1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with ShiftMax... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:29:55.501622 UTC(+0.025718s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0) = 0
   |  |
   |  +- f2(x0,x1) = x0
   |  |
   |  +- f3(x0,x1) = 0
   |  |
   |  +- f4(x0) = x0
   |  |
   |  +- f46(x0) = x0
   |  |
   |  +- f47() = 0
   |  |
   |  +- f48(x0) = x0
   |  |
   |  +- f49(x0) = x0
   |  |
   |  +- f50(x0) = 0
   |  |
   |  +- f51(x0) = x0
   |  |
   |  `- f52(x0,x1) = x1
   |
   +- Constraints
   |  |
   |  +- f46(x27) = x27 >= x27 = x27
   |  |
   |  +- f2(x27,f47()) = x27 >= x27 = f4(f46(x27))
   |  |
   |  +- f48(x3) = x3 >= x3 = x3
   |  |
   |  +- f1(x3) = 0 >= 0 = f3(f47(),f48(x3))
   |  |
   |  +- f4(x7 + 1) = x7 + 1 >= x7 = x7
   |  |
   |  +- f49(x37) = x37 >= x37 = x37
   |  |
   |  +- f2(x37,f50(x10)) = x37 >= x37 = f2(f49(x37),x10)
   |  |
   |  +- f51(x13) = x13 >= x13 = x13
   |  |
   |  +- f52(x10,x13) = x13 >= x13 = f2(f51(x13),x10)
   |  |
   |  +- f3(x10,x13 + 1) = 0 >= 0 = f3(f50(x10),f52(x10,x13))
   |  |
   |  `- f3(x17,0) = 0 >= 0 = 0
   |
   `- Stopping timer: 2017-03-30 07:29:55.501682 UTC(+0.025995s)