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
|
+- Staring timer: 2017-03-30 07:32:40.652011 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
|
+- 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
|
+- Interpretation
|  |
|  +- 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) = f2(x2) >= f1(x2,0) = 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) = f1(x7 + 1,x5) >= f1(x7,x5 + 1) = f1(f28(x7),f30(x5))
|  |
|  `- f1(0,x10) = f1(0,x10) >= x10 = x10
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:40.652267 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f1(x7 + 1,x5) = f1(x7 + 1,x5) >= f1(x7,x5 + 1) = f1(x7,x5 + 1)
|     |  |
|     |  `- f1(0,x10) = f1(0,x10) >= x10 = x10
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:40.65232 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f1(x0,x1) = 8 + x0 + x1
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f1(x0,x1) = x0 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:40.661702 UTC(+0.009382s)
|     |
|     +- Interpretation
|     |  |
|     |  `- f1(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f1(x7 + 1,x5) = (x7 + 1) + x5 >= x7 + (x5 + 1) = f1(x7,x5 + 1)
|     |  |
|     |  `- f1(0,x10) = x10 >= x10 = x10
|     |
|     `- Stopping timer: 2017-03-30 07:32:40.66173 UTC(+0.009463s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:40.661747 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f2(x2) = f2(x2) >= x2 = f1(x2,0)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f2(x0) ↦ x0
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  `- f2(x0) = x0
|     |
|     +- Constraints
|     |  |
|     |  `- f2(x2) = x2 >= x2 = f1(x2,0)
|     |
|     `- Stopping timer: 2017-03-30 07:32:40.661797 UTC(+0.00005s)
|
+- 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.661812 UTC(+0.009801s)