SUCCESS(1)

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

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:29:54.465367 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)
   |
   +- Simplification ...
   |  |
   |  +- Propagated: f4(x0) ↦ x0
   |  |
   |  +- Propagated: f53(x0) ↦ x0
   |  |
   |  +- Propagated: f54() ↦ 0
   |  |
   |  +- Propagated: f55(x0) ↦ x0
   |  |
   |  +- Propagated: f56(x0) ↦ x0
   |  |
   |  +- Propagated: f58(x0) ↦ x0
   |  |
   |  +- Propagated: f60(x0) ↦ x0
   |  |
   |  +- Propagated: f61(x0) ↦ x0
   |  |
   |  `- Propagated: f62(x0) ↦ x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:29:54.465642 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = max(7 + x0 + x1,8 + x1)
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2) = max(8 + x0 + x2,x1)
   |  |  |
   |  |  +- f5(x0) = 15 + x0
   |  |  |
   |  |  +- f57(x0) = 8 + x0
   |  |  |
   |  |  +- f59() = 0
   |  |  |
   |  |  +- f6(x0,x1) = 15 + x0 + x1
   |  |  |
   |  |  `- f63(x0,x1) = 1 + x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  +- f5(x0) = 1 + x0
   |  |  |
   |  |  +- f57(x0) = 1 + x0
   |  |  |
   |  |  +- f59() = 0
   |  |  |
   |  |  +- f6(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  `- f63(x0,x1) = 1 + x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  +- f5(x0) = 1 + x0
   |  |  |
   |  |  +- f57(x0) = x0
   |  |  |
   |  |  +- f59() = 0
   |  |  |
   |  |  +- f6(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f63(x0,x1) = 1 + x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  +- f5(x0) = x0
   |  |  |
   |  |  +- f57(x0) = x0
   |  |  |
   |  |  +- f59() = 0
   |  |  |
   |  |  +- f6(x0,x1) = x0 + x1
   |  |  |
   |  |  `- f63(x0,x1) = 1 + x1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with ShiftMax... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:29:54.534397 UTC(+0.068755s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + x1
   |  |
   |  +- f2(x0,x1) = 1 + x0
   |  |
   |  +- f3(x0,x1,x2) = 1 + x0 + x2
   |  |
   |  +- f4(x0) = x0
   |  |
   |  +- f5(x0) = x0
   |  |
   |  +- f53(x0) = x0
   |  |
   |  +- f54() = 0
   |  |
   |  +- f55(x0) = x0
   |  |
   |  +- f56(x0) = x0
   |  |
   |  +- f57(x0) = x0
   |  |
   |  +- f58(x0) = x0
   |  |
   |  +- f59() = 0
   |  |
   |  +- f6(x0,x1) = x0 + x1
   |  |
   |  +- f60(x0) = x0
   |  |
   |  +- f61(x0) = x0
   |  |
   |  +- f62(x0) = x0
   |  |
   |  `- f63(x0,x1) = 1 + x1
   |
   +- Constraints
   |  |
   |  +- f53(x2) = x2 >= x2 = x2
   |  |
   |  +- f54() = 0 >= 0 = 0
   |  |
   |  +- f5(x2) = x2 >= x2 = f6(f53(x2),f54())
   |  |
   |  +- f55(x7) = x7 >= x7 = x7
   |  |
   |  +- f56(x31) = x31 >= x31 = x31
   |  |
   |  +- f1(x31,f57(x7)) = x31 + x7 >= x7 + x31 = f6(f55(x7),f56(x31))
   |  |
   |  +- f58(x38) = x38 >= x38 = x38
   |  |
   |  +- f2(x38,f59()) = 1 + x38 >= x38 + 1 = f58(x38) + 1
   |  |
   |  +- f60(x5) = x5 >= x5 = x5
   |  |
   |  +- f6(x7 + 1,x5) = (x7 + 1) + x5 >= 1 + (x7 + x5) = f3(f57(x7),f59(),f60(x5))
   |  |
   |  +- f61(x10) = x10 >= x10 = x10
   |  |
   |  +- f6(0,x10) = x10 >= x10 = f4(f61(x10))
   |  |
   |  +- f4(x13) = x13 >= x13 = x13
   |  |
   |  +- f62(x17) = x17 >= x17 = x17
   |  |
   |  +- f63(x16,x17) = 1 + x17 >= 1 + x17 = f2(f62(x17),x16)
   |  |
   |  `- f3(x15,x16,x17) = 1 + (x15 + x17) >= (1 + x17) + x15 = f1(f63(x16,x17),x15)
   |
   `- Stopping timer: 2017-03-30 07:29:54.534469 UTC(+0.069102s)