SUCCESS(1)

SUCCESS
f1(x0) = 14;
f2(x0,x1) = 9 + x0 + x1;
f3(x0,x1) = 0;
f4(x0) = 1 + x0;
f46(x0) = 7 + x0;
f47() = 15;
f48(x0) = x0;
f49(x0) = 3 + x0;
f50(x0) = 12 + x0;
f51(x0) = x0;
f52(x0,x1) = 15 + x0 + x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:29:55.45792 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
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:29:55.457963 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 14
   |  |  |
   |  |  +- f2(x0,x1) = 9 + x0 + x1
   |  |  |
   |  |  +- f3(x0,x1) = 0
   |  |  |
   |  |  +- f4(x0) = 1 + x0
   |  |  |
   |  |  +- f46(x0) = 7 + x0
   |  |  |
   |  |  +- f47() = 15
   |  |  |
   |  |  +- f48(x0) = x0
   |  |  |
   |  |  +- f49(x0) = 3 + x0
   |  |  |
   |  |  +- f50(x0) = 12 + x0
   |  |  |
   |  |  +- f51(x0) = x0
   |  |  |
   |  |  `- f52(x0,x1) = 15 + x0 + x1
   |  |
   |  `- Stopping timer: 2017-03-30 07:29:55.470131 UTC(+0.012168s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0) = 14
   |  |
   |  +- f2(x0,x1) = 9 + x0 + x1
   |  |
   |  +- f3(x0,x1) = 0
   |  |
   |  +- f4(x0) = 1 + x0
   |  |
   |  +- f46(x0) = 7 + x0
   |  |
   |  +- f47() = 15
   |  |
   |  +- f48(x0) = x0
   |  |
   |  +- f49(x0) = 3 + x0
   |  |
   |  +- f50(x0) = 12 + x0
   |  |
   |  +- f51(x0) = x0
   |  |
   |  `- f52(x0,x1) = 15 + x0 + x1
   |
   +- Constraints
   |  |
   |  +- f46(x27) = 7 + x27 >= x27 = x27
   |  |
   |  +- f2(x27,f47()) = 9 + (x27 + 15) >= 1 + (7 + x27) = f4(f46(x27))
   |  |
   |  +- f48(x3) = x3 >= x3 = x3
   |  |
   |  +- f1(x3) = 14 >= 0 = f3(f47(),f48(x3))
   |  |
   |  +- f4(x7 + 1) = 1 + (x7 + 1) >= x7 = x7
   |  |
   |  +- f49(x37) = 3 + x37 >= x37 = x37
   |  |
   |  +- f2(x37,f50(x10)) = 9 + (x37 + (12 + x10)) >= 9 + ((3 + x37) + x10) = f2(f49(x37),x10)
   |  |
   |  +- f51(x13) = x13 >= x13 = x13
   |  |
   |  +- f52(x10,x13) = 15 + (x10 + x13) >= 9 + (x13 + x10) = 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.470169 UTC(+0.012249s)