SUCCESS(1)

SUCCESS
f1(x0,x1) = 1 + x0 + x1;
f2(x0,x1) = 7 + x0;
f3(x0,x1,x2) = 0;
f36(x0) = x0;
f37(x0) = x0;
f38(x0) = x0;
f39(x0) = x0;
f40(x0) = x0;
f41(x0) = x0;
f42(x0,x1,x2) = x1;
f43(x0,x1) = 1 + x0 + x1;
f44(x0,x1,x2) = 7 + x1 + x2;
f45(x0,x1,x2) = 7 + x1 + x2;
f46(x0) = x0;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:32.017443 UTC
   |
   +- Open Constraints
   |  |
   |  +- f36(x4) = f36(x4) >= x4 = x4
   |  |
   |  +- f37(x4) = f37(x4) >= f36(x4) = f36(x4)
   |  |
   |  +- f38(x4) = f38(x4) >= f37(x4) = f37(x4)
   |  |
   |  +- f39(x6) = f39(x6) >= x6 = x6
   |  |
   |  +- f40(x4) = f40(x4) >= f38(x4) = f38(x4)
   |  |
   |  +- f41(x3) = f41(x3) >= x3 = x3
   |  |
   |  +- f42(x3,x4,x6) = f42(x3,x4,x6) >= f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4) = f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4)
   |  |
   |  +- f43(x3,x6) = f43(x3,x6) >= f1(f39(x6),f41(x3)) = f1(f39(x6),f41(x3))
   |  |
   |  +- f44(x3,x4,x6) = f44(x3,x4,x6) >= f2(f39(x6),f41(x3)) + f42(x3,x4,x6) = f2(f39(x6),f41(x3)) + f42(x3,x4,x6)
   |  |
   |  +- f45(x3,x4,x6) = f45(x3,x4,x6) >= f44(x3,x4,x6) = f44(x3,x4,x6)
   |  |
   |  +- f1(x6 + 1,x3) = f1(x6 + 1,x3) >= f43(x3,x6) + 1 = f43(x3,x6) + 1
   |  |
   |  +- f2(x6 + 1,x3) + x4 = f2(x6 + 1,x3) + x4 >= f45(x3,x4,x6) + 1 = f45(x3,x4,x6) + 1
   |  |
   |  +- f46(x10) = f46(x10) >= x10 = x10
   |  |
   |  +- f1(0,x9) = f1(0,x9) >= x9 = x9
   |  |
   |  `- f2(0,x9) + x10 = f2(0,x9) + x10 >= f46(x10) + 1 = f46(x10) + 1
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:32.017498 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 7 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2) = 0
   |  |  |
   |  |  +- f36(x0) = x0
   |  |  |
   |  |  +- f37(x0) = x0
   |  |  |
   |  |  +- f38(x0) = x0
   |  |  |
   |  |  +- f39(x0) = x0
   |  |  |
   |  |  +- f40(x0) = x0
   |  |  |
   |  |  +- f41(x0) = x0
   |  |  |
   |  |  +- f42(x0,x1,x2) = x1
   |  |  |
   |  |  +- f43(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f44(x0,x1,x2) = 7 + x1 + x2
   |  |  |
   |  |  +- f45(x0,x1,x2) = 7 + x1 + x2
   |  |  |
   |  |  `- f46(x0) = x0
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:32.036807 UTC(+0.019309s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 1 + x0 + x1
   |  |
   |  +- f2(x0,x1) = 7 + x0
   |  |
   |  +- f3(x0,x1,x2) = 0
   |  |
   |  +- f36(x0) = x0
   |  |
   |  +- f37(x0) = x0
   |  |
   |  +- f38(x0) = x0
   |  |
   |  +- f39(x0) = x0
   |  |
   |  +- f40(x0) = x0
   |  |
   |  +- f41(x0) = x0
   |  |
   |  +- f42(x0,x1,x2) = x1
   |  |
   |  +- f43(x0,x1) = 1 + x0 + x1
   |  |
   |  +- f44(x0,x1,x2) = 7 + x1 + x2
   |  |
   |  +- f45(x0,x1,x2) = 7 + x1 + x2
   |  |
   |  `- f46(x0) = x0
   |
   +- Constraints
   |  |
   |  +- f36(x4) = x4 >= x4 = x4
   |  |
   |  +- f37(x4) = x4 >= x4 = f36(x4)
   |  |
   |  +- f38(x4) = x4 >= x4 = f37(x4)
   |  |
   |  +- f39(x6) = x6 >= x6 = x6
   |  |
   |  +- f40(x4) = x4 >= x4 = f38(x4)
   |  |
   |  +- f41(x3) = x3 >= x3 = x3
   |  |
   |  +- f42(x3,x4,x6) = x4 >= x4 = f3(f39(x6),f41(x3),f42(x3,x4,x6)) + f40(x4)
   |  |
   |  +- f43(x3,x6) = 1 + (x3 + x6) >= 1 + (x6 + x3) = f1(f39(x6),f41(x3))
   |  |
   |  +- f44(x3,x4,x6) = 7 + (x4 + x6) >= (7 + x6) + x4 = f2(f39(x6),f41(x3)) + f42(x3,x4,x6)
   |  |
   |  +- f45(x3,x4,x6) = 7 + (x4 + x6) >= 7 + (x4 + x6) = f44(x3,x4,x6)
   |  |
   |  +- f1(x6 + 1,x3) = 1 + ((x6 + 1) + x3) >= (1 + (x3 + x6)) + 1 = f43(x3,x6) + 1
   |  |
   |  +- f2(x6 + 1,x3) + x4 = (7 + (x6 + 1)) + x4 >= (7 + (x4 + x6)) + 1 = f45(x3,x4,x6) + 1
   |  |
   |  +- f46(x10) = x10 >= x10 = x10
   |  |
   |  +- f1(0,x9) = 1 + x9 >= x9 = x9
   |  |
   |  `- f2(0,x9) + x10 = 7 + x10 >= x10 + 1 = f46(x10) + 1
   |
   `- Stopping timer: 2017-03-30 07:32:32.036869 UTC(+0.019426s)