SUCCESS(1)

SUCCESS
f1(x0,x1) = 7 + x0 + x1;
f2(x0,x1) = 7 + x0;
f3(x0,x1,x2) = 0;
f4(x0) = 14 + x0;
f5(x0) = 15 + x0;
f55(x0) = x0;
f56(x0) = 3 + x0;
f57(x0) = 4 + x0;
f58(x0,x1) = 4 + x1;
f59() = 0;
f60(x0,x1) = 4 + x1;
f61(x0,x1) = 14 + 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) = 7 + x1 + x2;
f72(x0) = 3 + x0;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:18.401896 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
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:18.401955 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 7 + x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 7 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2) = 0
   |  |  |
   |  |  +- f4(x0) = 14 + x0
   |  |  |
   |  |  +- f5(x0) = 15 + x0
   |  |  |
   |  |  +- f55(x0) = x0
   |  |  |
   |  |  +- f56(x0) = 3 + x0
   |  |  |
   |  |  +- f57(x0) = 4 + x0
   |  |  |
   |  |  +- f58(x0,x1) = 4 + x1
   |  |  |
   |  |  +- f59() = 0
   |  |  |
   |  |  +- f60(x0,x1) = 4 + x1
   |  |  |
   |  |  +- f61(x0,x1) = 14 + 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) = 7 + x1 + x2
   |  |  |
   |  |  `- f72(x0) = 3 + x0
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:18.424361 UTC(+0.022406s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 7 + x0 + x1
   |  |
   |  +- f2(x0,x1) = 7 + x0
   |  |
   |  +- f3(x0,x1,x2) = 0
   |  |
   |  +- f4(x0) = 14 + x0
   |  |
   |  +- f5(x0) = 15 + x0
   |  |
   |  +- f55(x0) = x0
   |  |
   |  +- f56(x0) = 3 + x0
   |  |
   |  +- f57(x0) = 4 + x0
   |  |
   |  +- f58(x0,x1) = 4 + x1
   |  |
   |  +- f59() = 0
   |  |
   |  +- f60(x0,x1) = 4 + x1
   |  |
   |  +- f61(x0,x1) = 14 + 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) = 7 + x1 + x2
   |  |
   |  `- f72(x0) = 3 + x0
   |
   +- Constraints
   |  |
   |  +- f55(x3) = x3 >= x3 = x3
   |  |
   |  +- f56(x2) = 3 + x2 >= x2 = x2
   |  |
   |  +- f57(x3) = 4 + x3 >= x3 = f55(x3)
   |  |
   |  +- f58(x2,x3) = 4 + x3 >= 4 + x3 = f3(f56(x2),f59(),f60(x2,x3)) + f57(x3)
   |  |
   |  +- f59() = 0 >= 0 = 0
   |  |
   |  +- f60(x2,x3) = 4 + x3 >= 4 + x3 = f58(x2,x3)
   |  |
   |  +- f61(x2,x3) = 14 + (x2 + x3) >= (7 + (3 + x2)) + (4 + x3) = f2(f56(x2),f59()) + f60(x2,x3)
   |  |
   |  +- f4(x2) = 14 + x2 >= 7 + (3 + x2) = f1(f56(x2),f59())
   |  |
   |  +- f5(x2) + x3 = (15 + x2) + x3 >= (14 + (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) = 1 + x6 >= x6 + 1 = f69(x6) + 1
   |  |
   |  +- f67(x6,x7,x9) = x7 >= x7 = f70(x6,x7,x9)
   |  |
   |  +- f71(x6,x7,x9) = 7 + (x7 + x9) >= (7 + x9) + x7 = f2(f63(x9),f66(x6)) + f67(x6,x7,x9)
   |  |
   |  +- f1(x9 + 1,x6) = 7 + ((x9 + 1) + x6) >= 7 + (x9 + (1 + x6)) = f1(f63(x9),f66(x6))
   |  |
   |  +- f2(x9 + 1,x6) + x7 = (7 + (x9 + 1)) + x7 >= (7 + (x7 + x9)) + 1 = f71(x6,x7,x9) + 1
   |  |
   |  +- f72(x13) = 3 + x13 >= x13 = x13
   |  |
   |  +- f1(0,x12) = 7 + x12 >= x12 = x12
   |  |
   |  `- f2(0,x12) + x13 = 7 + x13 >= (3 + x13) + 1 = f72(x13) + 1
   |
   `- Stopping timer: 2017-03-30 07:32:18.424443 UTC(+0.022547s)