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 | `- SOLVE ... | +- Staring timer: 2017-03-30 07:32:18.430966 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 | +- 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 | +- SMT-MSLI ... | | | +- Staring timer: 2017-03-30 07:32:18.43154 UTC | | | +- Interpretation | | | | | +- f1(x0,x1) = max(x0 + x1,1) | | | | | +- f2(x0,x1) = 14 + x0 | | | | | +- f4(x0) = 12 + x0 | | | | | +- f5(x0) = 15 + x0 | | | | | +- f61(x0,x1) = 14 + x0 + x1 | | | | | `- f71(x0,x1,x2) = 14 + x1 + x2 | | | +- Minimizing with ZeroOut ... | | | +- Interpretation | | | | | +- f1(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = 1 + x0 | | | | | +- f4(x0) = 1 + x0 | | | | | +- f5(x0) = 2 + x0 | | | | | +- f61(x0,x1) = 1 + x0 + x1 | | | | | `- f71(x0,x1,x2) = 1 + x1 + x2 | | | +- Minimizing with ZeroOut ... | | | +- Interpretation | | | | | +- f1(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = 1 + x0 | | | | | +- f4(x0) = x0 | | | | | +- f5(x0) = 2 + x0 | | | | | +- f61(x0,x1) = 1 + x0 + x1 | | | | | `- f71(x0,x1,x2) = 1 + x1 + x2 | | | +- Minimizing with ZeroOut... Failed | | | +- Minimizing with ShiftMax... Failed | | | +- Minimizing with DecreaseCoeff... Failed | | | `- Stopping timer: 2017-03-30 07:32:18.476791 UTC(+0.045251s) | +- 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.476882 UTC(+0.045916s)