SUCCESS(1)

SUCCESS
f1(x0,x1) = 1 + x0;
f2(x0,x1,x2) = 1 + x1;
f3(x0,x1,x2) = x2;
f4(x0,x1) = 1 + x0;
f5(x0,x1) = x1;
f60(x0) = x0;
f61() = 0;
f62(x0) = x0;
f63(x0) = x0;
f64(x0) = x0;
f65(x0) = 0;
f66(x0) = x0;
f67(x0) = x0;
f68(x0,x1,x2,x3) = x2;
f69(x0,x1,x2,x3,x4,x5) = 1 + x1;
f70(x0) = x0;
f71(x0) = 0;
f72(x0) = x0;
f73(x0) = x0;
f74(x0,x1,x2,x3) = x2;
f75(x0) = x0;
f76(x0,x1) = 1 + x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:19.278214 UTC
   |
   +- Open Constraints
   |  |
   |  +- f60(x21) = f60(x21) >= x21 = x21
   |  |
   |  +- f1(x21,f61()) = f1(x21,f61()) >= f60(x21) + 1 = f60(x21) + 1
   |  |
   |  +- f62(x2) = f62(x2) >= x2 = x2
   |  |
   |  +- f63(x1) = f63(x1) >= x1 = x1
   |  |
   |  +- f5(x1,x2) = f5(x1,x2) >= f3(f61(),f63(x1),f62(x2)) = f3(f61(),f63(x1),f62(x2))
   |  |
   |  +- f4(x1,x2) = f4(x1,x2) >= f2(f61(),f63(x1),f62(x2)) = f2(f61(),f63(x1),f62(x2))
   |  |
   |  +- f64(x35) = f64(x35) >= x35 = x35
   |  |
   |  +- f1(x35,f65(x3)) = f1(x35,f65(x3)) >= f1(f64(x35),x3) = f1(f64(x35),x3)
   |  |
   |  +- f66(x7) = f66(x7) >= x7 = x7
   |  |
   |  +- f67(x4) = f67(x4) >= x4 = x4
   |  |
   |  +- f68(x3,x4,x7,x35) = f68(x3,x4,x7,x35) >= f3(f65(x3),f67(x4),f66(x7)) = f3(f65(x3),f67(x4),f66(x7))
   |  |
   |  +- f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48) >= f2(f65(x3),f67(x4),f66(x7)) = f2(f65(x3),f67(x4),f66(x7))
   |  |
   |  +- f70(x48) = f70(x48) >= x48 = x48
   |  |
   |  +- f1(x48,f71(x3)) = f1(x48,f71(x3)) >= f1(f70(x48),x3) = f1(f70(x48),x3)
   |  |
   |  +- f72(x8) = f72(x8) >= x8 = x8
   |  |
   |  +- f73(x4) = f73(x4) >= x4 = x4
   |  |
   |  +- f74(x3,x4,x8,x48) = f74(x3,x4,x8,x48) >= f3(f71(x3),f73(x4),f72(x8)) = f3(f71(x3),f73(x4),f72(x8))
   |  |
   |  +- f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48) >= f2(f71(x3),f73(x4),f72(x8)) = f2(f71(x3),f73(x4),f72(x8))
   |  |
   |  +- f3(x3,x4,(x7 + x8) + 1) = f3(x3,x4,(x7 + x8) + 1) >= (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1 = (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1
   |  |
   |  +- f2(x3,x4,(x7 + x8) + 1) = f2(x3,x4,(x7 + x8) + 1) >= f69(x3,x4,x7,x8,x35,x48) = f69(x3,x4,x7,x8,x35,x48)
   |  |
   |  +- f75(x11) = f75(x11) >= x11 = x11
   |  |
   |  +- f76(x10,x11) = f76(x10,x11) >= f1(f75(x11),x10) = f1(f75(x11),x10)
   |  |
   |  +- f3(x10,x11,0) = f3(x10,x11,0) >= 0 = 0
   |  |
   |  `- f2(x10,x11,0) = f2(x10,x11,0) >= f76(x10,x11) = f76(x10,x11)
   |
   +- Simplification ...
   |  |
   |  +- Substituted: f68(x3,x4,x7,x35) ≥ f3(f65(x3),f67(x4),f66(x7)) ↦ f68(x3,x4,x7,0) ≥ f3(f65(x3),f67(x4),f66(x7))
   |  |
   |  +- Substituted: f69(x3,x4,x7,x8,x35,x48) ≥ f2(f65(x3),f67(x4),f66(x7)) ↦ f69(x3,x4,x7,0,0,0) ≥ f2(f65(x3),f67(x4),f66(x7))
   |  |
   |  +- Substituted: f74(x3,x4,x8,x48) ≥ f3(f71(x3),f73(x4),f72(x8)) ↦ f74(x3,x4,x8,0) ≥ f3(f71(x3),f73(x4),f72(x8))
   |  |
   |  +- Substituted: f69(x3,x4,x7,x8,x35,x48) ≥ f2(f71(x3),f73(x4),f72(x8)) ↦ f69(x3,x4,0,x8,0,0) ≥ f2(f71(x3),f73(x4),f72(x8))
   |  |
   |  +- Substituted: f3(x10,x11,0) ≥ 0 ↦ f3(0,0,0) ≥ 0
   |  |
   |  +- Propagated: f60(x0) ↦ x0
   |  |
   |  +- Propagated: f62(x0) ↦ x0
   |  |
   |  +- Propagated: f63(x0) ↦ x0
   |  |
   |  +- Propagated: f64(x0) ↦ x0
   |  |
   |  +- Propagated: f66(x0) ↦ x0
   |  |
   |  +- Propagated: f67(x0) ↦ x0
   |  |
   |  +- Propagated: f70(x0) ↦ x0
   |  |
   |  +- Propagated: f72(x0) ↦ x0
   |  |
   |  +- Propagated: f73(x0) ↦ x0
   |  |
   |  `- Propagated: f75(x0) ↦ x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:19.278688 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = max(7,3 + x0)
   |  |  |
   |  |  +- f2(x0,x1,x2) = max(9 + x0 + x2,7 + x0 + x1 + x2)
   |  |  |
   |  |  +- f3(x0,x1,x2) = x0 + x2
   |  |  |
   |  |  +- f4(x0,x1) = max(15 + x1,7 + x0 + x1)
   |  |  |
   |  |  +- f5(x0,x1) = max(12 + x0,12 + x1)
   |  |  |
   |  |  +- f61() = 0
   |  |  |
   |  |  +- f65(x0) = 0
   |  |  |
   |  |  +- f68(x0,x1,x2,x3) = x2
   |  |  |
   |  |  +- f69(x0,x1,x2,x3,x4,x5) = max(1 + x0 + x2 + x3,7 + x1 + x2 + x3,10 + x2 + x3)
   |  |  |
   |  |  +- f71(x0) = 0
   |  |  |
   |  |  +- f74(x0,x1,x2,x3) = x0 + x2
   |  |  |
   |  |  `- f76(x0,x1) = max(7 + x1,2 + x0)
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f2(x0,x1,x2) = 1 + x0 + x1
   |  |  |
   |  |  +- f3(x0,x1,x2) = x2
   |  |  |
   |  |  +- f4(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f5(x0,x1) = x1
   |  |  |
   |  |  +- f61() = 0
   |  |  |
   |  |  +- f65(x0) = 0
   |  |  |
   |  |  +- f68(x0,x1,x2,x3) = x2
   |  |  |
   |  |  +- f69(x0,x1,x2,x3,x4,x5) = 1 + x1
   |  |  |
   |  |  +- f71(x0) = 0
   |  |  |
   |  |  +- f74(x0,x1,x2,x3) = x2
   |  |  |
   |  |  `- f76(x0,x1) = 1 + x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f2(x0,x1,x2) = 1 + x1
   |  |  |
   |  |  +- f3(x0,x1,x2) = x2
   |  |  |
   |  |  +- f4(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f5(x0,x1) = x1
   |  |  |
   |  |  +- f61() = 0
   |  |  |
   |  |  +- f65(x0) = 0
   |  |  |
   |  |  +- f68(x0,x1,x2,x3) = x2
   |  |  |
   |  |  +- f69(x0,x1,x2,x3,x4,x5) = 1 + x1
   |  |  |
   |  |  +- f71(x0) = 0
   |  |  |
   |  |  +- f74(x0,x1,x2,x3) = x2
   |  |  |
   |  |  `- f76(x0,x1) = 1 + x1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with ShiftMax... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:19.45268 UTC(+0.173992s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 1 + x0
   |  |
   |  +- f2(x0,x1,x2) = 1 + x1
   |  |
   |  +- f3(x0,x1,x2) = x2
   |  |
   |  +- f4(x0,x1) = 1 + x0
   |  |
   |  +- f5(x0,x1) = x1
   |  |
   |  +- f60(x0) = x0
   |  |
   |  +- f61() = 0
   |  |
   |  +- f62(x0) = x0
   |  |
   |  +- f63(x0) = x0
   |  |
   |  +- f64(x0) = x0
   |  |
   |  +- f65(x0) = 0
   |  |
   |  +- f66(x0) = x0
   |  |
   |  +- f67(x0) = x0
   |  |
   |  +- f68(x0,x1,x2,x3) = x2
   |  |
   |  +- f69(x0,x1,x2,x3,x4,x5) = 1 + x1
   |  |
   |  +- f70(x0) = x0
   |  |
   |  +- f71(x0) = 0
   |  |
   |  +- f72(x0) = x0
   |  |
   |  +- f73(x0) = x0
   |  |
   |  +- f74(x0,x1,x2,x3) = x2
   |  |
   |  +- f75(x0) = x0
   |  |
   |  `- f76(x0,x1) = 1 + x1
   |
   +- Constraints
   |  |
   |  +- f60(x21) = x21 >= x21 = x21
   |  |
   |  +- f1(x21,f61()) = 1 + x21 >= x21 + 1 = f60(x21) + 1
   |  |
   |  +- f62(x2) = x2 >= x2 = x2
   |  |
   |  +- f63(x1) = x1 >= x1 = x1
   |  |
   |  +- f5(x1,x2) = x2 >= x2 = f3(f61(),f63(x1),f62(x2))
   |  |
   |  +- f4(x1,x2) = 1 + x1 >= 1 + x1 = f2(f61(),f63(x1),f62(x2))
   |  |
   |  +- f64(x35) = x35 >= x35 = x35
   |  |
   |  +- f1(x35,f65(x3)) = 1 + x35 >= 1 + x35 = f1(f64(x35),x3)
   |  |
   |  +- f66(x7) = x7 >= x7 = x7
   |  |
   |  +- f67(x4) = x4 >= x4 = x4
   |  |
   |  +- f68(x3,x4,x7,x35) = x7 >= x7 = f3(f65(x3),f67(x4),f66(x7))
   |  |
   |  +- f69(x3,x4,x7,x8,x35,x48) = 1 + x4 >= 1 + x4 = f2(f65(x3),f67(x4),f66(x7))
   |  |
   |  +- f70(x48) = x48 >= x48 = x48
   |  |
   |  +- f1(x48,f71(x3)) = 1 + x48 >= 1 + x48 = f1(f70(x48),x3)
   |  |
   |  +- f72(x8) = x8 >= x8 = x8
   |  |
   |  +- f73(x4) = x4 >= x4 = x4
   |  |
   |  +- f74(x3,x4,x8,x48) = x8 >= x8 = f3(f71(x3),f73(x4),f72(x8))
   |  |
   |  +- f69(x3,x4,x7,x8,x35,x48) = 1 + x4 >= 1 + x4 = f2(f71(x3),f73(x4),f72(x8))
   |  |
   |  +- f3(x3,x4,(x7 + x8) + 1) = (x7 + x8) + 1 >= (x7 + x8) + 1 = (f68(x3,x4,x7,x35) + f74(x3,x4,x8,x48)) + 1
   |  |
   |  +- f2(x3,x4,(x7 + x8) + 1) = 1 + x4 >= 1 + x4 = f69(x3,x4,x7,x8,x35,x48)
   |  |
   |  +- f75(x11) = x11 >= x11 = x11
   |  |
   |  +- f76(x10,x11) = 1 + x11 >= 1 + x11 = f1(f75(x11),x10)
   |  |
   |  +- f3(x10,x11,0) = 0 >= 0 = 0
   |  |
   |  `- f2(x10,x11,0) = 1 + x11 >= 1 + x11 = f76(x10,x11)
   |
   `- Stopping timer: 2017-03-30 07:32:19.452772 UTC(+0.174558s)