SUCCESS(1)

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

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:19.217734 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)
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:19.217858 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f2(x0,x1,x2) = 3 + x0 + x1 + x2
   |  |  |
   |  |  +- f3(x0,x1,x2) = x2
   |  |  |
   |  |  +- f4(x0,x1) = 15 + x0 + x1
   |  |  |
   |  |  +- f5(x0,x1) = 13 + x1
   |  |  |
   |  |  +- f60(x0) = x0
   |  |  |
   |  |  +- f61() = 9
   |  |  |
   |  |  +- f62(x0) = 3 + x0
   |  |  |
   |  |  +- f63(x0) = x0
   |  |  |
   |  |  +- f64(x0) = x0
   |  |  |
   |  |  +- f65(x0) = x0
   |  |  |
   |  |  +- f66(x0) = x0
   |  |  |
   |  |  +- f67(x0) = 1 + x0
   |  |  |
   |  |  +- f68(x0,x1,x2,x3) = x2
   |  |  |
   |  |  +- f69(x0,x1,x2,x3,x4,x5) = 4 + x0 + x1 + x2 + x3
   |  |  |
   |  |  +- f70(x0) = x0
   |  |  |
   |  |  +- f71(x0) = x0
   |  |  |
   |  |  +- f72(x0) = x0
   |  |  |
   |  |  +- f73(x0) = x0
   |  |  |
   |  |  +- f74(x0,x1,x2,x3) = x2
   |  |  |
   |  |  +- f75(x0) = x0
   |  |  |
   |  |  `- f76(x0,x1) = 1 + x0 + x1
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:19.269445 UTC(+0.051587s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 1 + x0 + x1
   |  |
   |  +- f2(x0,x1,x2) = 3 + x0 + x1 + x2
   |  |
   |  +- f3(x0,x1,x2) = x2
   |  |
   |  +- f4(x0,x1) = 15 + x0 + x1
   |  |
   |  +- f5(x0,x1) = 13 + x1
   |  |
   |  +- f60(x0) = x0
   |  |
   |  +- f61() = 9
   |  |
   |  +- f62(x0) = 3 + x0
   |  |
   |  +- f63(x0) = x0
   |  |
   |  +- f64(x0) = x0
   |  |
   |  +- f65(x0) = x0
   |  |
   |  +- f66(x0) = x0
   |  |
   |  +- f67(x0) = 1 + x0
   |  |
   |  +- f68(x0,x1,x2,x3) = x2
   |  |
   |  +- f69(x0,x1,x2,x3,x4,x5) = 4 + x0 + x1 + x2 + x3
   |  |
   |  +- f70(x0) = x0
   |  |
   |  +- f71(x0) = x0
   |  |
   |  +- f72(x0) = x0
   |  |
   |  +- f73(x0) = x0
   |  |
   |  +- f74(x0,x1,x2,x3) = x2
   |  |
   |  +- f75(x0) = x0
   |  |
   |  `- f76(x0,x1) = 1 + x0 + x1
   |
   +- Constraints
   |  |
   |  +- f60(x21) = x21 >= x21 = x21
   |  |
   |  +- f1(x21,f61()) = 1 + (x21 + 9) >= x21 + 1 = f60(x21) + 1
   |  |
   |  +- f62(x2) = 3 + x2 >= x2 = x2
   |  |
   |  +- f63(x1) = x1 >= x1 = x1
   |  |
   |  +- f5(x1,x2) = 13 + x2 >= 3 + x2 = f3(f61(),f63(x1),f62(x2))
   |  |
   |  +- f4(x1,x2) = 15 + (x1 + x2) >= 3 + (9 + (x1 + (3 + x2))) = f2(f61(),f63(x1),f62(x2))
   |  |
   |  +- f64(x35) = x35 >= x35 = x35
   |  |
   |  +- f1(x35,f65(x3)) = 1 + (x35 + x3) >= 1 + (x35 + x3) = f1(f64(x35),x3)
   |  |
   |  +- f66(x7) = x7 >= x7 = x7
   |  |
   |  +- f67(x4) = 1 + x4 >= x4 = x4
   |  |
   |  +- f68(x3,x4,x7,x35) = x7 >= x7 = f3(f65(x3),f67(x4),f66(x7))
   |  |
   |  +- f69(x3,x4,x7,x8,x35,x48) = 4 + (x3 + (x4 + (x7 + x8))) >= 3 + (x3 + ((1 + x4) + x7)) = f2(f65(x3),f67(x4),f66(x7))
   |  |
   |  +- f70(x48) = x48 >= x48 = x48
   |  |
   |  +- f1(x48,f71(x3)) = 1 + (x48 + x3) >= 1 + (x48 + x3) = 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) = 4 + (x3 + (x4 + (x7 + x8))) >= 3 + (x3 + (x4 + x8)) = 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) = 3 + (x3 + (x4 + ((x7 + x8) + 1))) >= 4 + (x3 + (x4 + (x7 + x8))) = f69(x3,x4,x7,x8,x35,x48)
   |  |
   |  +- f75(x11) = x11 >= x11 = x11
   |  |
   |  +- f76(x10,x11) = 1 + (x10 + x11) >= 1 + (x11 + x10) = f1(f75(x11),x10)
   |  |
   |  +- f3(x10,x11,0) = 0 >= 0 = 0
   |  |
   |  `- f2(x10,x11,0) = 3 + (x10 + x11) >= 1 + (x10 + x11) = f76(x10,x11)
   |
   `- Stopping timer: 2017-03-30 07:32:19.269559 UTC(+0.051825s)