SUCCESS(1)

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

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:29.905217 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
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:29.905248 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 9 + x0 + x1
   |  |  |
   |  |  +- f18(x0) = x0
   |  |  |
   |  |  +- f19(x0) = x0
   |  |  |
   |  |  `- f20(x0,x1) = 9 + x0 + x1
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:29.911958 UTC(+0.00671s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 9 + x0 + x1
   |  |
   |  +- f18(x0) = x0
   |  |
   |  +- f19(x0) = x0
   |  |
   |  `- f20(x0,x1) = 9 + x0 + x1
   |
   +- Constraints
   |  |
   |  +- f18(x5) = x5 >= x5 = x5
   |  |
   |  +- f19(x3) = x3 >= x3 = x3
   |  |
   |  +- f20(x3,x5) = 9 + (x3 + x5) >= 9 + (x5 + x3) = f1(f18(x5),f19(x3))
   |  |
   |  +- f1(x5 + 1,x3) = 9 + ((x5 + 1) + x3) >= (9 + (x3 + x5)) + 1 = f20(x3,x5) + 1
   |  |
   |  `- f1(0,x8) = 9 + x8 >= x8 = x8
   |
   `- Stopping timer: 2017-03-30 07:32:29.911991 UTC(+0.006774s)