SUCCESS(1)

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

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:16.118991 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)
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:16.119047 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1,x2) = 1 + x0 + x1 + x2
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2,x3) = 2 + x0 + x1 + x3
   |  |  |
   |  |  +- f4(x0) = 7 + x0
   |  |  |
   |  |  +- f5(x0) = 15 + x0
   |  |  |
   |  |  +- f6(x0,x1) = 13 + x0 + x1
   |  |  |
   |  |  +- f65(x0) = 2 + x0
   |  |  |
   |  |  +- f66() = 0
   |  |  |
   |  |  +- f67(x0) = x0
   |  |  |
   |  |  +- f68(x0) = x0
   |  |  |
   |  |  +- f69() = 12
   |  |  |
   |  |  +- f70(x0) = x0
   |  |  |
   |  |  +- f71(x0) = x0
   |  |  |
   |  |  +- f72() = 0
   |  |  |
   |  |  +- f73(x0) = x0
   |  |  |
   |  |  +- f74(x0) = 3 + x0
   |  |  |
   |  |  +- f75(x0) = x0
   |  |  |
   |  |  +- f76(x0) = x0
   |  |  |
   |  |  `- f77(x0,x1) = 1 + x1
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:16.14122 UTC(+0.022173s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1,x2) = 1 + x0 + x1 + x2
   |  |
   |  +- f2(x0,x1) = 1 + x0
   |  |
   |  +- f3(x0,x1,x2,x3) = 2 + x0 + x1 + x3
   |  |
   |  +- f4(x0) = 7 + x0
   |  |
   |  +- f5(x0) = 15 + x0
   |  |
   |  +- f6(x0,x1) = 13 + x0 + x1
   |  |
   |  +- f65(x0) = 2 + x0
   |  |
   |  +- f66() = 0
   |  |
   |  +- f67(x0) = x0
   |  |
   |  +- f68(x0) = x0
   |  |
   |  +- f69() = 12
   |  |
   |  +- f70(x0) = x0
   |  |
   |  +- f71(x0) = x0
   |  |
   |  +- f72() = 0
   |  |
   |  +- f73(x0) = x0
   |  |
   |  +- f74(x0) = 3 + x0
   |  |
   |  +- f75(x0) = x0
   |  |
   |  +- f76(x0) = x0
   |  |
   |  `- f77(x0,x1) = 1 + x1
   |
   +- Constraints
   |  |
   |  +- f65(x2) = 2 + x2 >= x2 = x2
   |  |
   |  +- f66() = 0 >= 0 = 0
   |  |
   |  +- f5(x2) = 15 + x2 >= 13 + (2 + x2) = f6(f65(x2),f66())
   |  |
   |  +- f67(x34) = x34 >= x34 = x34
   |  |
   |  +- f68(x35) = x35 >= x35 = x35
   |  |
   |  +- f1(x34,x35,f69()) = 1 + (x34 + (x35 + 12)) >= 13 + (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) = 13 + ((x7 + 1) + x5) >= 2 + (12 + (x7 + x5)) = f3(f69(),f70(x7),f72(),f73(x5))
   |  |
   |  +- f74(x10) = 3 + x10 >= x10 = x10
   |  |
   |  +- f6(0,x10) = 13 + x10 >= 7 + (3 + x10) = f4(f74(x10))
   |  |
   |  +- f4(x13) = 7 + 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) = 2 + (x15 + (x16 + x18)) >= 1 + (x16 + ((1 + x18) + x15)) = f1(f75(x16),f77(x17,x18),x15)
   |
   `- Stopping timer: 2017-03-30 07:32:16.141303 UTC(+0.022312s)