SUCCESS(1)

SUCCESS
f1(x0,x1) = 4 + x0 + x1;
f2(x0,x1) = x0 + x1;
f3(x0,x1,x2) = 4 + x0 + x1 + x2;
f4(x0) = 3 + x0;
f5(x0) = 15 + x0;
f53(x0) = 4 + x0;
f54() = 4;
f55(x0) = x0;
f56(x0) = x0;
f57(x0) = 3 + x0;
f58(x0) = x0;
f59() = 1;
f6(x0,x1) = 7 + x0 + x1;
f60(x0) = x0;
f61(x0) = 1 + x0;
f62(x0) = x0;
f63(x0,x1) = x0 + x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:29:54.431695 UTC
   |
   +- Open Constraints
   |  |
   |  +- f53(x2) = f53(x2) >= x2 = x2
   |  |
   |  +- f54() = f54() >= 0 = 0
   |  |
   |  +- f5(x2) = f5(x2) >= f6(f53(x2),f54()) = f6(f53(x2),f54())
   |  |
   |  +- f55(x7) = f55(x7) >= x7 = x7
   |  |
   |  +- f56(x31) = f56(x31) >= x31 = x31
   |  |
   |  +- f1(x31,f57(x7)) = f1(x31,f57(x7)) >= f6(f55(x7),f56(x31)) = f6(f55(x7),f56(x31))
   |  |
   |  +- f58(x38) = f58(x38) >= x38 = x38
   |  |
   |  +- f2(x38,f59()) = f2(x38,f59()) >= f58(x38) + 1 = f58(x38) + 1
   |  |
   |  +- f60(x5) = f60(x5) >= x5 = x5
   |  |
   |  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f57(x7),f59(),f60(x5)) = f3(f57(x7),f59(),f60(x5))
   |  |
   |  +- f61(x10) = f61(x10) >= x10 = x10
   |  |
   |  +- f6(0,x10) = f6(0,x10) >= f4(f61(x10)) = f4(f61(x10))
   |  |
   |  +- f4(x13) = f4(x13) >= x13 = x13
   |  |
   |  +- f62(x17) = f62(x17) >= x17 = x17
   |  |
   |  +- f63(x16,x17) = f63(x16,x17) >= f2(f62(x17),x16) = f2(f62(x17),x16)
   |  |
   |  `- f3(x15,x16,x17) = f3(x15,x16,x17) >= f1(f63(x16,x17),x15) = f1(f63(x16,x17),x15)
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:29:54.431752 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 4 + x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f3(x0,x1,x2) = 4 + x0 + x1 + x2
   |  |  |
   |  |  +- f4(x0) = 3 + x0
   |  |  |
   |  |  +- f5(x0) = 15 + x0
   |  |  |
   |  |  +- f53(x0) = 4 + x0
   |  |  |
   |  |  +- f54() = 4
   |  |  |
   |  |  +- f55(x0) = x0
   |  |  |
   |  |  +- f56(x0) = x0
   |  |  |
   |  |  +- f57(x0) = 3 + x0
   |  |  |
   |  |  +- f58(x0) = x0
   |  |  |
   |  |  +- f59() = 1
   |  |  |
   |  |  +- f6(x0,x1) = 7 + x0 + x1
   |  |  |
   |  |  +- f60(x0) = x0
   |  |  |
   |  |  +- f61(x0) = 1 + x0
   |  |  |
   |  |  +- f62(x0) = x0
   |  |  |
   |  |  `- f63(x0,x1) = x0 + x1
   |  |
   |  `- Stopping timer: 2017-03-30 07:29:54.456673 UTC(+0.024921s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 4 + x0 + x1
   |  |
   |  +- f2(x0,x1) = x0 + x1
   |  |
   |  +- f3(x0,x1,x2) = 4 + x0 + x1 + x2
   |  |
   |  +- f4(x0) = 3 + x0
   |  |
   |  +- f5(x0) = 15 + x0
   |  |
   |  +- f53(x0) = 4 + x0
   |  |
   |  +- f54() = 4
   |  |
   |  +- f55(x0) = x0
   |  |
   |  +- f56(x0) = x0
   |  |
   |  +- f57(x0) = 3 + x0
   |  |
   |  +- f58(x0) = x0
   |  |
   |  +- f59() = 1
   |  |
   |  +- f6(x0,x1) = 7 + x0 + x1
   |  |
   |  +- f60(x0) = x0
   |  |
   |  +- f61(x0) = 1 + x0
   |  |
   |  +- f62(x0) = x0
   |  |
   |  `- f63(x0,x1) = x0 + x1
   |
   +- Constraints
   |  |
   |  +- f53(x2) = 4 + x2 >= x2 = x2
   |  |
   |  +- f54() = 4 >= 0 = 0
   |  |
   |  +- f5(x2) = 15 + x2 >= 7 + ((4 + x2) + 4) = f6(f53(x2),f54())
   |  |
   |  +- f55(x7) = x7 >= x7 = x7
   |  |
   |  +- f56(x31) = x31 >= x31 = x31
   |  |
   |  +- f1(x31,f57(x7)) = 4 + (x31 + (3 + x7)) >= 7 + (x7 + x31) = f6(f55(x7),f56(x31))
   |  |
   |  +- f58(x38) = x38 >= x38 = x38
   |  |
   |  +- f2(x38,f59()) = x38 + 1 >= x38 + 1 = f58(x38) + 1
   |  |
   |  +- f60(x5) = x5 >= x5 = x5
   |  |
   |  +- f6(x7 + 1,x5) = 7 + ((x7 + 1) + x5) >= 4 + ((3 + x7) + (1 + x5)) = f3(f57(x7),f59(),f60(x5))
   |  |
   |  +- f61(x10) = 1 + x10 >= x10 = x10
   |  |
   |  +- f6(0,x10) = 7 + x10 >= 3 + (1 + x10) = f4(f61(x10))
   |  |
   |  +- f4(x13) = 3 + x13 >= x13 = x13
   |  |
   |  +- f62(x17) = x17 >= x17 = x17
   |  |
   |  +- f63(x16,x17) = x16 + x17 >= x17 + x16 = f2(f62(x17),x16)
   |  |
   |  `- f3(x15,x16,x17) = 4 + (x15 + (x16 + x17)) >= 4 + ((x16 + x17) + x15) = f1(f63(x16,x17),x15)
   |
   `- Stopping timer: 2017-03-30 07:29:54.456763 UTC(+0.025068s)