SUCCESS(1)

SUCCESS
f1(x0,x1,x2) = x0 + x1;
f2(x0,x1) = 1 + x0;
f3(x0,x1,x2,x3) = 1 + x1 + x3;
f4(x0) = x0;
f5(x0) = x0;
f6(x0,x1) = x0 + x1;
f65(x0) = x0;
f66() = 0;
f67(x0) = x0;
f68(x0) = x0;
f69() = 0;
f70(x0) = x0;
f71(x0) = x0;
f72() = 0;
f73(x0) = x0;
f74(x0) = x0;
f75(x0) = x0;
f76(x0) = x0;
f77(x0,x1) = 1 + x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:16.147974 UTC
   |
   +- Open Constraints
   |  |
   |  +- f65(x2) = f65(x2) >= x2 = x2
   |  |
   |  +- f66() = f66() >= 0 = 0
   |  |
   |  +- f5(x2) = f5(x2) >= f6(f65(x2),f66()) = f6(f65(x2),f66())
   |  |
   |  +- f67(x34) = f67(x34) >= x34 = x34
   |  |
   |  +- f68(x35) = f68(x35) >= x35 = x35
   |  |
   |  +- f1(x34,x35,f69()) = f1(x34,x35,f69()) >= f6(f67(x34),f68(x35)) = f6(f67(x34),f68(x35))
   |  |
   |  +- f70(x7) = f70(x7) >= x7 = x7
   |  |
   |  +- f71(x43) = f71(x43) >= x43 = x43
   |  |
   |  +- f2(x43,f72()) = f2(x43,f72()) >= f71(x43) + 1 = f71(x43) + 1
   |  |
   |  +- f73(x5) = f73(x5) >= x5 = x5
   |  |
   |  +- f6(x7 + 1,x5) = f6(x7 + 1,x5) >= f3(f69(),f70(x7),f72(),f73(x5)) = f3(f69(),f70(x7),f72(),f73(x5))
   |  |
   |  +- f74(x10) = f74(x10) >= x10 = x10
   |  |
   |  +- f6(0,x10) = f6(0,x10) >= f4(f74(x10)) = f4(f74(x10))
   |  |
   |  +- f4(x13) = f4(x13) >= x13 = x13
   |  |
   |  +- f75(x16) = f75(x16) >= x16 = x16
   |  |
   |  +- f76(x18) = f76(x18) >= x18 = x18
   |  |
   |  +- f77(x17,x18) = f77(x17,x18) >= f2(f76(x18),x17) = f2(f76(x18),x17)
   |  |
   |  `- f3(x15,x16,x17,x18) = f3(x15,x16,x17,x18) >= f1(f75(x16),f77(x17,x18),x15) = f1(f75(x16),f77(x17,x18),x15)
   |
   +- Simplification ...
   |  |
   |  +- Propagated: f4(x0) ↦ x0
   |  |
   |  +- Propagated: f65(x0) ↦ x0
   |  |
   |  +- Propagated: f66() ↦ 0
   |  |
   |  +- Propagated: f67(x0) ↦ x0
   |  |
   |  +- Propagated: f68(x0) ↦ x0
   |  |
   |  +- Propagated: f70(x0) ↦ x0
   |  |
   |  +- Propagated: f71(x0) ↦ x0
   |  |
   |  +- Propagated: f73(x0) ↦ x0
   |  |
   |  +- Propagated: f74(x0) ↦ x0
   |  |
   |  +- Propagated: f75(x0) ↦ x0
   |  |
   |  `- Propagated: f76(x0) ↦ x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:16.148305 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1,x2) = max(8 + x0,x0 + x1 + x2)
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2,x3) = max(1 + x0 + x1 + x3,2 + x0 + x1 + x2,8 + x0 + x1)
   |  |  |
   |  |  +- f5(x0) = 15 + x0
   |  |  |
   |  |  +- f6(x0,x1) = max(x0 + x1,7 + x0)
   |  |  |
   |  |  +- f69() = 0
   |  |  |
   |  |  +- f72() = 0
   |  |  |
   |  |  `- f77(x0,x1) = max(1 + x1,2)
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1,x2) = x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2,x3) = 1 + x1 + x3
   |  |  |
   |  |  +- f5(x0) = x0
   |  |  |
   |  |  +- f6(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f69() = 0
   |  |  |
   |  |  +- f72() = 0
   |  |  |
   |  |  `- f77(x0,x1) = 1 + x1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with ShiftMax... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:16.207249 UTC(+0.058944s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1,x2) = x0 + x1
   |  |
   |  +- f2(x0,x1) = 1 + x0
   |  |
   |  +- f3(x0,x1,x2,x3) = 1 + x1 + x3
   |  |
   |  +- f4(x0) = x0
   |  |
   |  +- f5(x0) = x0
   |  |
   |  +- f6(x0,x1) = x0 + x1
   |  |
   |  +- f65(x0) = x0
   |  |
   |  +- f66() = 0
   |  |
   |  +- f67(x0) = x0
   |  |
   |  +- f68(x0) = x0
   |  |
   |  +- f69() = 0
   |  |
   |  +- f70(x0) = x0
   |  |
   |  +- f71(x0) = x0
   |  |
   |  +- f72() = 0
   |  |
   |  +- f73(x0) = x0
   |  |
   |  +- f74(x0) = x0
   |  |
   |  +- f75(x0) = x0
   |  |
   |  +- f76(x0) = x0
   |  |
   |  `- f77(x0,x1) = 1 + x1
   |
   +- Constraints
   |  |
   |  +- f65(x2) = x2 >= x2 = x2
   |  |
   |  +- f66() = 0 >= 0 = 0
   |  |
   |  +- f5(x2) = x2 >= x2 = f6(f65(x2),f66())
   |  |
   |  +- f67(x34) = x34 >= x34 = x34
   |  |
   |  +- f68(x35) = x35 >= x35 = x35
   |  |
   |  +- f1(x34,x35,f69()) = x34 + x35 >= x34 + x35 = f6(f67(x34),f68(x35))
   |  |
   |  +- f70(x7) = x7 >= x7 = x7
   |  |
   |  +- f71(x43) = x43 >= x43 = x43
   |  |
   |  +- f2(x43,f72()) = 1 + x43 >= x43 + 1 = f71(x43) + 1
   |  |
   |  +- f73(x5) = x5 >= x5 = x5
   |  |
   |  +- f6(x7 + 1,x5) = (x7 + 1) + x5 >= 1 + (x7 + x5) = f3(f69(),f70(x7),f72(),f73(x5))
   |  |
   |  +- f74(x10) = x10 >= x10 = x10
   |  |
   |  +- f6(0,x10) = x10 >= x10 = f4(f74(x10))
   |  |
   |  +- f4(x13) = x13 >= x13 = x13
   |  |
   |  +- f75(x16) = x16 >= x16 = x16
   |  |
   |  +- f76(x18) = x18 >= x18 = x18
   |  |
   |  +- f77(x17,x18) = 1 + x18 >= 1 + x18 = f2(f76(x18),x17)
   |  |
   |  `- f3(x15,x16,x17,x18) = 1 + (x16 + x18) >= x16 + (1 + x18) = f1(f75(x16),f77(x17,x18),x15)
   |
   `- Stopping timer: 2017-03-30 07:32:16.207331 UTC(+0.059357s)