SUCCESS(1)

SUCCESS
f1(x0,x1) = 1 + x0 + x1;
f2(x0) = 8 + 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.62594 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
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:40.625972 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f2(x0) = 8 + x0
   |  |  |
   |  |  +- f26(x0) = x0
   |  |  |
   |  |  +- f27() = 0
   |  |  |
   |  |  +- f28(x0) = x0
   |  |  |
   |  |  +- f29(x0) = x0
   |  |  |
   |  |  `- f30(x0) = 1 + x0
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:40.632812 UTC(+0.00684s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 1 + x0 + x1
   |  |
   |  +- f2(x0) = 8 + 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) = 8 + x2 >= 1 + x2 = f1(f26(x2),f27())
   |  |
   |  +- f28(x7) = x7 >= x7 = x7
   |  |
   |  +- f29(x5) = x5 >= x5 = x5
   |  |
   |  +- f30(x5) = 1 + x5 >= x5 + 1 = f29(x5) + 1
   |  |
   |  +- f1(x7 + 1,x5) = 1 + ((x7 + 1) + x5) >= 1 + (x7 + (1 + x5)) = f1(f28(x7),f30(x5))
   |  |
   |  `- f1(0,x10) = 1 + x10 >= x10 = x10
   |
   `- Stopping timer: 2017-03-30 07:32:40.632846 UTC(+0.006906s)