SUCCESS(1)

SUCCESS
f1(x0,x1) = 4*x0 + x1;
f2(x0,x1) = 15 + 15*x0 + 13*x1;
f3(x0,x1) = 2 + x0 + 4*x1;
f4(x0,x1) = 6 + 13*x0 + 3*x1;
f41(x0) = x0;
f42(x0) = 1 + x0;
f43(x0) = x0;
f44(x0) = 3 + x0;
f45(x0) = x0;
f46(x0) = 1 + x0;
f47(x0,x1) = 3 + x0 + 4*x1;
f48(x0) = 3*x0;
f49(x0,x1) = 4 + 9*x0 + 3*x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:17.094467 UTC
   |
   +- Open Constraints
   |  |
   |  +- f41(x2) = f41(x2) >= x2 = x2
   |  |
   |  +- f42(x21) = f42(x21) >= x21 = x21
   |  |
   |  +- f3(x21,f43(x2)) = f3(x21,f43(x2)) >= f1(f41(x2),f42(x21)) = f1(f41(x2),f42(x21))
   |  |
   |  +- f44(x3) = f44(x3) >= x3 = x3
   |  |
   |  +- f2(x2,x3) = f2(x2,x3) >= f4(f43(x2),f44(x3)) = f4(f43(x2),f44(x3))
   |  |
   |  +- f45(x8) = f45(x8) >= x8 = x8
   |  |
   |  +- f46(x6) = f46(x6) >= x6 = x6
   |  |
   |  +- f47(x6,x8) = f47(x6,x8) >= f1(f45(x8),f46(x6)) = f1(f45(x8),f46(x6))
   |  |
   |  +- f1(x8 + 1,x6) = f1(x8 + 1,x6) >= f47(x6,x8) + 1 = f47(x6,x8) + 1
   |  |
   |  +- f1(0,x11) = f1(0,x11) >= x11 = x11
   |  |
   |  +- f48(x15) = f48(x15) >= x15 = x15
   |  |
   |  +- f49(x14,x15) = f49(x14,x15) >= f3(f48(x15),x14) = f3(f48(x15),x14)
   |  |
   |  `- f4(x14,x15) = f4(x14,x15) >= f3(f49(x14,x15),x14) = f3(f49(x14,x15),x14)
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:17.094541 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:17.263347 UTC(+0.168806s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:17.263364 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 4*x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 15 + 15*x0 + 13*x1
   |  |  |
   |  |  +- f3(x0,x1) = 2 + x0 + 4*x1
   |  |  |
   |  |  +- f4(x0,x1) = 6 + 13*x0 + 3*x1
   |  |  |
   |  |  +- f41(x0) = x0
   |  |  |
   |  |  +- f42(x0) = 1 + x0
   |  |  |
   |  |  +- f43(x0) = x0
   |  |  |
   |  |  +- f44(x0) = 3 + x0
   |  |  |
   |  |  +- f45(x0) = x0
   |  |  |
   |  |  +- f46(x0) = 1 + x0
   |  |  |
   |  |  +- f47(x0,x1) = 3 + x0 + 4*x1
   |  |  |
   |  |  +- f48(x0) = 3*x0
   |  |  |
   |  |  `- f49(x0,x1) = 4 + 9*x0 + 3*x1
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:17.34247 UTC(+0.079106s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 4*x0 + x1
   |  |
   |  +- f2(x0,x1) = 15 + 15*x0 + 13*x1
   |  |
   |  +- f3(x0,x1) = 2 + x0 + 4*x1
   |  |
   |  +- f4(x0,x1) = 6 + 13*x0 + 3*x1
   |  |
   |  +- f41(x0) = x0
   |  |
   |  +- f42(x0) = 1 + x0
   |  |
   |  +- f43(x0) = x0
   |  |
   |  +- f44(x0) = 3 + x0
   |  |
   |  +- f45(x0) = x0
   |  |
   |  +- f46(x0) = 1 + x0
   |  |
   |  +- f47(x0,x1) = 3 + x0 + 4*x1
   |  |
   |  +- f48(x0) = 3*x0
   |  |
   |  `- f49(x0,x1) = 4 + 9*x0 + 3*x1
   |
   +- Constraints
   |  |
   |  +- f41(x2) = x2 >= x2 = x2
   |  |
   |  +- f42(x21) = 1 + x21 >= x21 = x21
   |  |
   |  +- f3(x21,f43(x2)) = 2 + (x21 + (4 * x2)) >= (4 * x2) + (1 + x21) = f1(f41(x2),f42(x21))
   |  |
   |  +- f44(x3) = 3 + x3 >= x3 = x3
   |  |
   |  +- f2(x2,x3) = 15 + ((15 * x2) + (13 * x3)) >= 6 + ((13 * x2) + (3 * (3 + x3))) = f4(f43(x2),f44(x3))
   |  |
   |  +- f45(x8) = x8 >= x8 = x8
   |  |
   |  +- f46(x6) = 1 + x6 >= x6 = x6
   |  |
   |  +- f47(x6,x8) = 3 + (x6 + (4 * x8)) >= (4 * x8) + (1 + x6) = f1(f45(x8),f46(x6))
   |  |
   |  +- f1(x8 + 1,x6) = (4 * (x8 + 1)) + x6 >= (3 + (x6 + (4 * x8))) + 1 = f47(x6,x8) + 1
   |  |
   |  +- f1(0,x11) = x11 >= x11 = x11
   |  |
   |  +- f48(x15) = 3 * x15 >= x15 = x15
   |  |
   |  +- f49(x14,x15) = 4 + ((9 * x14) + (3 * x15)) >= 2 + ((3 * x15) + (4 * x14)) = f3(f48(x15),x14)
   |  |
   |  `- f4(x14,x15) = 6 + ((13 * x14) + (3 * x15)) >= 2 + ((4 + ((9 * x14) + (3 * x15))) + (4 * x14)) = f3(f49(x14,x15),x14)
   |
   `- Stopping timer: 2017-03-30 07:32:17.342569 UTC(+0.248102s)