SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f2(x0,x1) = 1 + x0;
f3(x0,x1,x2) = 0;
f4(x0) = x0;
f5(x0) = 2 + x0;
f55(x0) = x0;
f56(x0) = x0;
f57(x0) = x0;
f58(x0,x1) = x1;
f59() = 0;
f60(x0,x1) = x1;
f61(x0,x1) = 1 + x0 + x1;
f62(x0) = x0;
f63(x0) = x0;
f64(x0) = x0;
f65(x0,x1,x2) = x1;
f66(x0) = 1 + x0;
f67(x0,x1,x2) = x1;
f68(x0,x1,x2) = x1;
f69(x0) = x0;
f70(x0,x1,x2) = x1;
f71(x0,x1,x2) = 1 + x1 + x2;
f72(x0) = x0;

ExecutionLog
|
+- Staring timer: 2017-03-30 07:32:18.483908 UTC
|
+- Open Constraints
|  |
|  +- f55(x3) = f55(x3) >= x3 = x3
|  |
|  +- f56(x2) = f56(x2) >= x2 = x2
|  |
|  +- f57(x3) = f57(x3) >= f55(x3) = f55(x3)
|  |
|  +- f58(x2,x3) = f58(x2,x3) >= f3(f56(x2),f59(),f60(x2,x3)) + f57(x3) = f3(f56(x2),f59(),f60(x2,x3)) + f57(x3)
|  |
|  +- f59() = f59() >= 0 = 0
|  |
|  +- f60(x2,x3) = f60(x2,x3) >= f58(x2,x3) = f58(x2,x3)
|  |
|  +- f61(x2,x3) = f61(x2,x3) >= f2(f56(x2),f59()) + f60(x2,x3) = f2(f56(x2),f59()) + f60(x2,x3)
|  |
|  +- f4(x2) = f4(x2) >= f1(f56(x2),f59()) = f1(f56(x2),f59())
|  |
|  +- f5(x2) + x3 = f5(x2) + x3 >= f61(x2,x3) + 1 = f61(x2,x3) + 1
|  |
|  +- f62(x7) = f62(x7) >= x7 = x7
|  |
|  +- f63(x9) = f63(x9) >= x9 = x9
|  |
|  +- f64(x7) = f64(x7) >= f62(x7) = f62(x7)
|  |
|  +- f65(x6,x7,x9) = f65(x6,x7,x9) >= f3(f63(x9),f66(x6),f67(x6,x7,x9)) + f64(x7) = f3(f63(x9),f66(x6),f67(x6,x7,x9)) + f64(x7)
|  |
|  +- f68(x6,x7,x9) = f68(x6,x7,x9) >= f65(x6,x7,x9) = f65(x6,x7,x9)
|  |
|  +- f69(x6) = f69(x6) >= x6 = x6
|  |
|  +- f70(x6,x7,x9) = f70(x6,x7,x9) >= f68(x6,x7,x9) = f68(x6,x7,x9)
|  |
|  +- f66(x6) = f66(x6) >= f69(x6) + 1 = f69(x6) + 1
|  |
|  +- f67(x6,x7,x9) = f67(x6,x7,x9) >= f70(x6,x7,x9) = f70(x6,x7,x9)
|  |
|  +- f71(x6,x7,x9) = f71(x6,x7,x9) >= f2(f63(x9),f66(x6)) + f67(x6,x7,x9) = f2(f63(x9),f66(x6)) + f67(x6,x7,x9)
|  |
|  +- f1(x9 + 1,x6) = f1(x9 + 1,x6) >= f1(f63(x9),f66(x6)) = f1(f63(x9),f66(x6))
|  |
|  +- f2(x9 + 1,x6) + x7 = f2(x9 + 1,x6) + x7 >= f71(x6,x7,x9) + 1 = f71(x6,x7,x9) + 1
|  |
|  +- f72(x13) = f72(x13) >= x13 = x13
|  |
|  +- f1(0,x12) = f1(0,x12) >= x12 = x12
|  |
|  `- f2(0,x12) + x13 = f2(0,x12) + x13 >= f72(x13) + 1 = f72(x13) + 1
|
+- Open Constraints
|  |
|  +- f55(x3) = f55(x3) >= x3 = x3
|  |
|  +- f56(x2) = f56(x2) >= x2 = x2
|  |
|  +- f57(x3) = f57(x3) >= f55(x3) = f55(x3)
|  |
|  +- f58(x2,x3) = f58(x2,x3) >= f3(f56(x2),f59(),f60(x2,x3)) + f57(x3) = f3(f56(x2),f59(),f60(x2,x3)) + f57(x3)
|  |
|  +- f59() = f59() >= 0 = 0
|  |
|  +- f60(x2,x3) = f60(x2,x3) >= f58(x2,x3) = f58(x2,x3)
|  |
|  +- f61(x2,x3) = f61(x2,x3) >= f2(f56(x2),f59()) + f60(x2,x3) = f2(f56(x2),f59()) + f60(x2,x3)
|  |
|  +- f4(x2) = f4(x2) >= f1(f56(x2),f59()) = f1(f56(x2),f59())
|  |
|  +- f5(x2) + x3 = f5(x2) + x3 >= f61(x2,x3) + 1 = f61(x2,x3) + 1
|  |
|  +- f62(x7) = f62(x7) >= x7 = x7
|  |
|  +- f63(x9) = f63(x9) >= x9 = x9
|  |
|  +- f64(x7) = f64(x7) >= f62(x7) = f62(x7)
|  |
|  +- f65(x6,x7,x9) = f65(x6,x7,x9) >= f3(f63(x9),f66(x6),f67(x6,x7,x9)) + f64(x7) = f3(f63(x9),f66(x6),f67(x6,x7,x9)) + f64(x7)
|  |
|  +- f68(x6,x7,x9) = f68(x6,x7,x9) >= f65(x6,x7,x9) = f65(x6,x7,x9)
|  |
|  +- f69(x6) = f69(x6) >= x6 = x6
|  |
|  +- f70(x6,x7,x9) = f70(x6,x7,x9) >= f68(x6,x7,x9) = f68(x6,x7,x9)
|  |
|  +- f66(x6) = f66(x6) >= f69(x6) + 1 = f69(x6) + 1
|  |
|  +- f67(x6,x7,x9) = f67(x6,x7,x9) >= f70(x6,x7,x9) = f70(x6,x7,x9)
|  |
|  +- f71(x6,x7,x9) = f71(x6,x7,x9) >= f2(f63(x9),f66(x6)) + f67(x6,x7,x9) = f2(f63(x9),f66(x6)) + f67(x6,x7,x9)
|  |
|  +- f1(x9 + 1,x6) = f1(x9 + 1,x6) >= f1(f63(x9),f66(x6)) = f1(f63(x9),f66(x6))
|  |
|  +- f2(x9 + 1,x6) + x7 = f2(x9 + 1,x6) + x7 >= f71(x6,x7,x9) + 1 = f71(x6,x7,x9) + 1
|  |
|  +- f72(x13) = f72(x13) >= x13 = x13
|  |
|  +- f1(0,x12) = f1(0,x12) >= x12 = x12
|  |
|  `- f2(0,x12) + x13 = f2(0,x12) + x13 >= f72(x13) + 1 = f72(x13) + 1
|
+- Simplification ...
|  |
|  +- Substituted: f2(0,x12) + x13 ≥ f72(x13) + 1 ↦ f2(0,0) + x13 ≥ f72(x13) + 1
|  |
|  +- Eliminated: f3/3
|  |
|  +- Propagated: f55(x0) ↦ x0
|  |
|  +- Propagated: f56(x0) ↦ x0
|  |
|  +- Propagated: f59() ↦ 0
|  |
|  +- Propagated: f62(x0) ↦ x0
|  |
|  +- Propagated: f63(x0) ↦ x0
|  |
|  +- Propagated: f69(x0) ↦ x0
|  |
|  +- Propagated: f72(x0) ↦ x0
|  |
|  +- Propagated: f57(x0) ↦ x0
|  |
|  +- Propagated: f64(x0) ↦ x0
|  |
|  +- Propagated: f66(x0) ↦ 1 + x0
|  |
|  +- Propagated: f58(x0,x1) ↦ x1
|  |
|  +- Propagated: f65(x0,x1,x2) ↦ x1
|  |
|  +- Propagated: f60(x0,x1) ↦ x1
|  |
|  +- Propagated: f68(x0,x1,x2) ↦ x1
|  |
|  +- Propagated: f70(x0,x1,x2) ↦ x1
|  |
|  `- Propagated: f67(x0,x1,x2) ↦ x1
|
+- Interpretation
|  |
|  +- f3(x0,x1,x2) = 0
|  |
|  +- f55(x0) = x0
|  |
|  +- f56(x0) = x0
|  |
|  +- f57(x0) = x0
|  |
|  +- f58(x0,x1) = x1
|  |
|  +- f59() = 0
|  |
|  +- f60(x0,x1) = x1
|  |
|  +- f62(x0) = x0
|  |
|  +- f63(x0) = x0
|  |
|  +- f64(x0) = x0
|  |
|  +- f65(x0,x1,x2) = x1
|  |
|  +- f66(x0) = 1 + x0
|  |
|  +- f67(x0,x1,x2) = x1
|  |
|  +- f68(x0,x1,x2) = x1
|  |
|  +- f69(x0) = x0
|  |
|  +- f70(x0,x1,x2) = x1
|  |
|  `- f72(x0) = x0
|
+- Constraints
|  |
|  +- f55(x3) = x3 >= x3 = x3
|  |
|  +- f56(x2) = x2 >= x2 = x2
|  |
|  +- f57(x3) = x3 >= x3 = f55(x3)
|  |
|  +- f58(x2,x3) = x3 >= x3 = f3(f56(x2),f59(),f60(x2,x3)) + f57(x3)
|  |
|  +- f59() = 0 >= 0 = 0
|  |
|  +- f60(x2,x3) = x3 >= x3 = f58(x2,x3)
|  |
|  +- f61(x2,x3) = f61(x2,x3) >= f2(x2,0) + x3 = f2(f56(x2),f59()) + f60(x2,x3)
|  |
|  +- f4(x2) = f4(x2) >= f1(x2,0) = f1(f56(x2),f59())
|  |
|  +- f5(x2) + x3 = f5(x2) + x3 >= f61(x2,x3) + 1 = f61(x2,x3) + 1
|  |
|  +- f62(x7) = x7 >= x7 = x7
|  |
|  +- f63(x9) = x9 >= x9 = x9
|  |
|  +- f64(x7) = x7 >= x7 = f62(x7)
|  |
|  +- f65(x6,x7,x9) = x7 >= x7 = f3(f63(x9),f66(x6),f67(x6,x7,x9)) + f64(x7)
|  |
|  +- f68(x6,x7,x9) = x7 >= x7 = f65(x6,x7,x9)
|  |
|  +- f69(x6) = x6 >= x6 = x6
|  |
|  +- f70(x6,x7,x9) = x7 >= x7 = f68(x6,x7,x9)
|  |
|  +- f66(x6) = x6 + 1 >= x6 + 1 = f69(x6) + 1
|  |
|  +- f67(x6,x7,x9) = x7 >= x7 = f70(x6,x7,x9)
|  |
|  +- f71(x6,x7,x9) = f71(x6,x7,x9) >= f2(x9,x6 + 1) + x7 = f2(f63(x9),f66(x6)) + f67(x6,x7,x9)
|  |
|  +- f1(x9 + 1,x6) = f1(x9 + 1,x6) >= f1(x9,x6 + 1) = f1(f63(x9),f66(x6))
|  |
|  +- f2(x9 + 1,x6) + x7 = f2(x9 + 1,x6) + x7 >= f71(x6,x7,x9) + 1 = f71(x6,x7,x9) + 1
|  |
|  +- f72(x13) = x13 >= x13 = x13
|  |
|  +- f1(0,x12) = f1(0,x12) >= x12 = x12
|  |
|  `- f2(0,x12) + x13 = f2(0,x12) + x13 >= x13 + 1 = f72(x13) + 1
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 5 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:18.484734 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f1(x9 + 1,x6) = f1(x9 + 1,x6) >= f1(x9,x6 + 1) = f1(x9,x6 + 1)
|     |  |
|     |  `- f1(0,x12) = f1(0,x12) >= x12 = x12
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:18.484781 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:18.494012 UTC(+0.009231s)
|     |
|     +- Interpretation
|     |  |
|     |  `- f1(x0,x1) = x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  +- f1(x9 + 1,x6) = (x9 + 1) + x6 >= x9 + (x6 + 1) = f1(x9,x6 + 1)
|     |  |
|     |  `- f1(0,x12) = x12 >= x12 = x12
|     |
|     `- Stopping timer: 2017-03-30 07:32:18.494047 UTC(+0.009313s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 4 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:18.494093 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  +- f2(x9 + 1,x6) + x7 = f2(x9 + 1,x6) + x7 >= f71(x6,x7,x9) + 1 = f71(x6,x7,x9) + 1
|     |  |
|     |  +- f2(0,0) + x13 = f2(0,0) + x13 >= x13 + 1 = x13 + 1
|     |  |
|     |  `- f71(x6,x7,x9) = f71(x6,x7,x9) >= f2(x9,x6 + 1) + x7 = f2(x9,x6 + 1) + x7
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:18.494164 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = 8 + x0
|     |  |  |
|     |  |  `- f71(x0,x1,x2) = 8 + x1 + x2
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with  DecreaseCoeff ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  +- f2(x0,x1) = 1 + x0
|     |  |  |
|     |  |  `- f71(x0,x1,x2) = 1 + x1 + x2
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:18.511809 UTC(+0.017645s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = 1 + x0
|     |  |
|     |  `- f71(x0,x1,x2) = 1 + x1 + x2
|     |
|     +- Constraints
|     |  |
|     |  +- f2(x9 + 1,x6) + x7 = (1 + (x9 + 1)) + x7 >= (1 + (x7 + x9)) + 1 = f71(x6,x7,x9) + 1
|     |  |
|     |  +- f2(0,0) + x13 = 1 + x13 >= x13 + 1 = x13 + 1
|     |  |
|     |  `- f71(x6,x7,x9) = 1 + (x7 + x9) >= (1 + x9) + x7 = f2(x9,x6 + 1) + x7
|     |
|     `- Stopping timer: 2017-03-30 07:32:18.51185 UTC(+0.017757s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 3 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:18.511876 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f4(x2) = f4(x2) >= x2 = f1(x2,0)
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f4(x0) ↦ x0
|     |
|     +- Interpretation
|     |  |
|     |  +- f1(x0,x1) = x0 + x1
|     |  |
|     |  `- f4(x0) = x0
|     |
|     +- Constraints
|     |  |
|     |  `- f4(x2) = x2 >= x2 = f1(x2,0)
|     |
|     `- Stopping timer: 2017-03-30 07:32:18.511934 UTC(+0.000058s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 2 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:18.511945 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f61(x2,x3) = f61(x2,x3) >= (1 + x2) + x3 = f2(x2,0) + x3
|     |
|     +- Simplification ...
|     |  |
|     |  `- Propagated: f61(x0,x1) ↦ 1 + x0 + x1
|     |
|     +- Interpretation
|     |  |
|     |  +- f2(x0,x1) = 1 + x0
|     |  |
|     |  `- f61(x0,x1) = 1 + x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f61(x2,x3) = (1 + x2) + x3 >= (1 + x2) + x3 = f2(x2,0) + x3
|     |
|     `- Stopping timer: 2017-03-30 07:32:18.511982 UTC(+0.000037s)
|
+- SCC-DECOMPOSE ...
|  |
|  +- SCC: 1 SCCs
|  |
|  `- SOLVE ...
|     |
|     +- Staring timer: 2017-03-30 07:32:18.51199 UTC
|     |
|     +- Open Constraints
|     |  |
|     |  `- f5(x2) + x3 = f5(x2) + x3 >= ((1 + x2) + x3) + 1 = f61(x2,x3) + 1
|     |
|     +- Simplification ...
|     |
|     +- SMT-MSLI ...
|     |  |
|     |  +- Staring timer: 2017-03-30 07:32:18.512023 UTC
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f5(x0) = 14 + x0
|     |  |
|     |  +- Minimizing with ZeroOut... Failed
|     |  |
|     |  +- Minimizing with ShiftMax... Failed
|     |  |
|     |  +- Minimizing with  DecreaseCoeff ...
|     |  |
|     |  +- Interpretation
|     |  |  |
|     |  |  `- f5(x0) = 2 + x0
|     |  |
|     |  +- Minimizing with DecreaseCoeff... Failed
|     |  |
|     |  `- Stopping timer: 2017-03-30 07:32:18.517057 UTC(+0.005034s)
|     |
|     +- Interpretation
|     |  |
|     |  +- f5(x0) = 2 + x0
|     |  |
|     |  `- f61(x0,x1) = 1 + x0 + x1
|     |
|     +- Constraints
|     |  |
|     |  `- f5(x2) + x3 = (2 + x2) + x3 >= ((1 + x2) + x3) + 1 = f61(x2,x3) + 1
|     |
|     `- Stopping timer: 2017-03-30 07:32:18.517092 UTC(+0.005102s)
|
+- Interpretation
|  |
|  +- f1(x0,x1) = x0 + x1
|  |
|  +- f2(x0,x1) = 1 + x0
|  |
|  +- f3(x0,x1,x2) = 0
|  |
|  +- f4(x0) = x0
|  |
|  +- f5(x0) = 2 + x0
|  |
|  +- f55(x0) = x0
|  |
|  +- f56(x0) = x0
|  |
|  +- f57(x0) = x0
|  |
|  +- f58(x0,x1) = x1
|  |
|  +- f59() = 0
|  |
|  +- f60(x0,x1) = x1
|  |
|  +- f61(x0,x1) = 1 + x0 + x1
|  |
|  +- f62(x0) = x0
|  |
|  +- f63(x0) = x0
|  |
|  +- f64(x0) = x0
|  |
|  +- f65(x0,x1,x2) = x1
|  |
|  +- f66(x0) = 1 + x0
|  |
|  +- f67(x0,x1,x2) = x1
|  |
|  +- f68(x0,x1,x2) = x1
|  |
|  +- f69(x0) = x0
|  |
|  +- f70(x0,x1,x2) = x1
|  |
|  +- f71(x0,x1,x2) = 1 + x1 + x2
|  |
|  `- f72(x0) = x0
|
+- Constraints
|  |
|  +- f55(x3) = x3 >= x3 = x3
|  |
|  +- f56(x2) = x2 >= x2 = x2
|  |
|  +- f57(x3) = x3 >= x3 = f55(x3)
|  |
|  +- f58(x2,x3) = x3 >= x3 = f3(f56(x2),f59(),f60(x2,x3)) + f57(x3)
|  |
|  +- f59() = 0 >= 0 = 0
|  |
|  +- f60(x2,x3) = x3 >= x3 = f58(x2,x3)
|  |
|  +- f61(x2,x3) = (1 + x2) + x3 >= (1 + x2) + x3 = f2(f56(x2),f59()) + f60(x2,x3)
|  |
|  +- f4(x2) = x2 >= x2 = f1(f56(x2),f59())
|  |
|  +- f5(x2) + x3 = (2 + x2) + x3 >= ((1 + x2) + x3) + 1 = f61(x2,x3) + 1
|  |
|  +- f62(x7) = x7 >= x7 = x7
|  |
|  +- f63(x9) = x9 >= x9 = x9
|  |
|  +- f64(x7) = x7 >= x7 = f62(x7)
|  |
|  +- f65(x6,x7,x9) = x7 >= x7 = f3(f63(x9),f66(x6),f67(x6,x7,x9)) + f64(x7)
|  |
|  +- f68(x6,x7,x9) = x7 >= x7 = f65(x6,x7,x9)
|  |
|  +- f69(x6) = x6 >= x6 = x6
|  |
|  +- f70(x6,x7,x9) = x7 >= x7 = f68(x6,x7,x9)
|  |
|  +- f66(x6) = x6 + 1 >= x6 + 1 = f69(x6) + 1
|  |
|  +- f67(x6,x7,x9) = x7 >= x7 = f70(x6,x7,x9)
|  |
|  +- f71(x6,x7,x9) = 1 + (x7 + x9) >= (1 + x9) + x7 = f2(f63(x9),f66(x6)) + f67(x6,x7,x9)
|  |
|  +- f1(x9 + 1,x6) = (x9 + 1) + x6 >= x9 + (x6 + 1) = f1(f63(x9),f66(x6))
|  |
|  +- f2(x9 + 1,x6) + x7 = (1 + (x9 + 1)) + x7 >= (1 + (x7 + x9)) + 1 = f71(x6,x7,x9) + 1
|  |
|  +- f72(x13) = x13 >= x13 = x13
|  |
|  +- f1(0,x12) = x12 >= x12 = x12
|  |
|  `- f2(0,x12) + x13 = 1 + x13 >= x13 + 1 = f72(x13) + 1
|
`- Stopping timer: 2017-03-30 07:32:18.517158 UTC(+0.03325s)