SUCCESS(1)

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

ExecutionLog
|
+- Staring timer: 2017-03-30 07:32:29.939735 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
|
+- 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
|
+- Simplification ...
|  |
|  +- Propagated: f18(x0) ↦ x0
|  |
|  `- Propagated: f19(x0) ↦ x0
|
+- Interpretation
|  |
|  +- f18(x0) = x0
|  |
|  `- f19(x0) = x0
|
+- Constraints
|  |
|  +- f18(x5) = x5 >= x5 = x5
|  |
|  +- f19(x3) = x3 >= x3 = x3
|  |
|  +- f20(x3,x5) = f20(x3,x5) >= f1(x5,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
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:29.939874 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f1(x5 + 1,x3) = f1(x5 + 1,x3) >= f20(x3,x5) + 1 = f20(x3,x5) + 1
|     |  |
|     |  +- f1(0,x8) = f1(0,x8) >= x8 = x8
|     |  |
|     |  `- f20(x3,x5) = f20(x3,x5) >= f1(x5,x3) = f1(x5,x3)
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:29.939929 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = 8 + x0 + x1
|     |  |  |
|     |  |  `- f20(x0,x1) = 8 + x0 + x1
|     |  |
|     |  +- Minimizing with  ZeroOut ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f1(x0,x1) = x0 + x1
|     |  |  |
|     |  |  `- f20(x0,x1) = x0 + x1
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:29.952273 UTC(+0.012344s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  `- f20(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f1(x5 + 1,x3) = (x5 + 1) + x3 >= (x3 + x5) + 1 = f20(x3,x5) + 1
|     |  |
|     |  +- f1(0,x8) = x8 >= x8 = x8
|     |  |
|     |  `- f20(x3,x5) = x3 + x5 >= x5 + x3 = f1(x5,x3)
|     |
|     `- Stopping timer: 2017-03-30 07:32:29.952301 UTC(+0.012427s)
|
+- Interpretation
|  |
|  +- f1(x0,x1) = x0 + x1
|  |
|  +- f18(x0) = x0
|  |
|  +- f19(x0) = x0
|  |
|  `- f20(x0,x1) = x0 + x1
|
+- Constraints
|  |
|  +- f18(x5) = x5 >= x5 = x5
|  |
|  +- f19(x3) = x3 >= x3 = x3
|  |
|  +- f20(x3,x5) = x3 + x5 >= x5 + x3 = f1(f18(x5),f19(x3))
|  |
|  +- f1(x5 + 1,x3) = (x5 + 1) + x3 >= (x3 + x5) + 1 = f20(x3,x5) + 1
|  |
|  `- f1(0,x8) = x8 >= x8 = x8
|
`- Stopping timer: 2017-03-30 07:32:29.952311 UTC(+0.012576s)