SUCCESS(1)

SUCCESS
f1(x0,x1) = 6 + x0 + x1;
f2(x0,x1) = x0 + x1;
f3(x0,x1,x2) = 3 + x0 + x1;
f4(x0,x1,x2) = 1 + x0 + x2;
f5(x0,x1,x2) = 15 + x0 + x1;
f6(x0,x1,x2) = 15 + x0 + x2;
f71(x0) = 1 + x0;
f72(x0) = x0;
f73(x0) = 7 + x0;
f74(x0) = 7 + x0;
f75(x0) = 5 + x0;
f76(x0) = x0;
f77(x0) = x0;
f78(x0,x1) = 6 + x0 + x1;
f79(x0) = x0;
f80(x0,x1,x2,x3) = 3 + x0 + x1;
f81(x0) = x0;
f82(x0) = x0;
f83(x0) = x0;
f84(x0) = x0;
f85(x0,x1,x2,x3) = 1 + x0 + x2;
f86() = 0;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:30.154845 UTC
   |
   +- Open Constraints
   |  |
   |  +- f71(x2) = f71(x2) >= x2 = x2
   |  |
   |  +- f72(x34) = f72(x34) >= x34 = x34
   |  |
   |  +- f2(x34,f73(x2)) = f2(x34,f73(x2)) >= f1(f71(x2),f72(x34)) = f1(f71(x2),f72(x34))
   |  |
   |  +- f74(x4) = f74(x4) >= x4 = x4
   |  |
   |  +- f75(x3) = f75(x3) >= x3 = x3
   |  |
   |  +- f6(x2,x3,x4) = f6(x2,x3,x4) >= f4(f73(x2),f75(x3),f74(x4)) = f4(f73(x2),f75(x3),f74(x4))
   |  |
   |  +- f5(x2,x3,x4) = f5(x2,x3,x4) >= f3(f73(x2),f75(x3),f74(x4)) = f3(f73(x2),f75(x3),f74(x4))
   |  |
   |  +- f76(x9) = f76(x9) >= x9 = x9
   |  |
   |  +- f77(x7) = f77(x7) >= x7 = x7
   |  |
   |  +- f78(x7,x9) = f78(x7,x9) >= f1(f76(x9),f77(x7)) = f1(f76(x9),f77(x7))
   |  |
   |  +- f1(x9 + 1,x7) = f1(x9 + 1,x7) >= f78(x7,x9) + 1 = f78(x7,x9) + 1
   |  |
   |  +- f1(0,x12) = f1(0,x12) >= x12 = x12
   |  |
   |  +- f79(x16) = f79(x16) >= x16 = x16
   |  |
   |  +- f80(x15,x16,x19,x63) = f80(x15,x16,x19,x63) >= f2(f79(x16),x15) = f2(f79(x16),x15)
   |  |
   |  +- f81(x63) = f81(x63) >= x63 = x63
   |  |
   |  +- f2(x63,f82(x15)) = f2(x63,f82(x15)) >= f2(f81(x63),x15) = f2(f81(x63),x15)
   |  |
   |  +- f83(x19) = f83(x19) >= x19 = x19
   |  |
   |  +- f84(x16) = f84(x16) >= x16 = x16
   |  |
   |  +- f85(x15,x16,x19,x63) = f85(x15,x16,x19,x63) >= f4(f82(x15),f84(x16),f83(x19)) = f4(f82(x15),f84(x16),f83(x19))
   |  |
   |  +- f80(x15,x16,x19,x63) = f80(x15,x16,x19,x63) >= f3(f82(x15),f84(x16),f83(x19)) = f3(f82(x15),f84(x16),f83(x19))
   |  |
   |  +- f4(x15,x16,x19 + 1) = f4(x15,x16,x19 + 1) >= f85(x15,x16,x19,x63) + 1 = f85(x15,x16,x19,x63) + 1
   |  |
   |  +- f3(x15,x16,x19 + 1) = f3(x15,x16,x19 + 1) >= f80(x15,x16,x19,x63) = f80(x15,x16,x19,x63)
   |  |
   |  +- f4(x22,x23,0) = f4(x22,x23,0) >= 0 = 0
   |  |
   |  `- f3(x22,x23,0) = f3(x22,x23,0) >= f86() = f86()
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:30.154907 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 6 + x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f3(x0,x1,x2) = 3 + x0 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  +- f5(x0,x1,x2) = 15 + x0 + x1
   |  |  |
   |  |  +- f6(x0,x1,x2) = 15 + x0 + x2
   |  |  |
   |  |  +- f71(x0) = 1 + x0
   |  |  |
   |  |  +- f72(x0) = x0
   |  |  |
   |  |  +- f73(x0) = 7 + x0
   |  |  |
   |  |  +- f74(x0) = 7 + x0
   |  |  |
   |  |  +- f75(x0) = 5 + x0
   |  |  |
   |  |  +- f76(x0) = x0
   |  |  |
   |  |  +- f77(x0) = x0
   |  |  |
   |  |  +- f78(x0,x1) = 6 + x0 + x1
   |  |  |
   |  |  +- f79(x0) = x0
   |  |  |
   |  |  +- f80(x0,x1,x2,x3) = 3 + x0 + x1
   |  |  |
   |  |  +- f81(x0) = x0
   |  |  |
   |  |  +- f82(x0) = x0
   |  |  |
   |  |  +- f83(x0) = x0
   |  |  |
   |  |  +- f84(x0) = x0
   |  |  |
   |  |  +- f85(x0,x1,x2,x3) = 1 + x0 + x2
   |  |  |
   |  |  `- f86() = 0
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:30.179539 UTC(+0.024632s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 6 + x0 + x1
   |  |
   |  +- f2(x0,x1) = x0 + x1
   |  |
   |  +- f3(x0,x1,x2) = 3 + x0 + x1
   |  |
   |  +- f4(x0,x1,x2) = 1 + x0 + x2
   |  |
   |  +- f5(x0,x1,x2) = 15 + x0 + x1
   |  |
   |  +- f6(x0,x1,x2) = 15 + x0 + x2
   |  |
   |  +- f71(x0) = 1 + x0
   |  |
   |  +- f72(x0) = x0
   |  |
   |  +- f73(x0) = 7 + x0
   |  |
   |  +- f74(x0) = 7 + x0
   |  |
   |  +- f75(x0) = 5 + x0
   |  |
   |  +- f76(x0) = x0
   |  |
   |  +- f77(x0) = x0
   |  |
   |  +- f78(x0,x1) = 6 + x0 + x1
   |  |
   |  +- f79(x0) = x0
   |  |
   |  +- f80(x0,x1,x2,x3) = 3 + x0 + x1
   |  |
   |  +- f81(x0) = x0
   |  |
   |  +- f82(x0) = x0
   |  |
   |  +- f83(x0) = x0
   |  |
   |  +- f84(x0) = x0
   |  |
   |  +- f85(x0,x1,x2,x3) = 1 + x0 + x2
   |  |
   |  `- f86() = 0
   |
   +- Constraints
   |  |
   |  +- f71(x2) = 1 + x2 >= x2 = x2
   |  |
   |  +- f72(x34) = x34 >= x34 = x34
   |  |
   |  +- f2(x34,f73(x2)) = x34 + (7 + x2) >= 6 + ((1 + x2) + x34) = f1(f71(x2),f72(x34))
   |  |
   |  +- f74(x4) = 7 + x4 >= x4 = x4
   |  |
   |  +- f75(x3) = 5 + x3 >= x3 = x3
   |  |
   |  +- f6(x2,x3,x4) = 15 + (x2 + x4) >= 1 + ((7 + x2) + (7 + x4)) = f4(f73(x2),f75(x3),f74(x4))
   |  |
   |  +- f5(x2,x3,x4) = 15 + (x2 + x3) >= 3 + ((7 + x2) + (5 + x3)) = f3(f73(x2),f75(x3),f74(x4))
   |  |
   |  +- f76(x9) = x9 >= x9 = x9
   |  |
   |  +- f77(x7) = x7 >= x7 = x7
   |  |
   |  +- f78(x7,x9) = 6 + (x7 + x9) >= 6 + (x9 + x7) = f1(f76(x9),f77(x7))
   |  |
   |  +- f1(x9 + 1,x7) = 6 + ((x9 + 1) + x7) >= (6 + (x7 + x9)) + 1 = f78(x7,x9) + 1
   |  |
   |  +- f1(0,x12) = 6 + x12 >= x12 = x12
   |  |
   |  +- f79(x16) = x16 >= x16 = x16
   |  |
   |  +- f80(x15,x16,x19,x63) = 3 + (x15 + x16) >= x16 + x15 = f2(f79(x16),x15)
   |  |
   |  +- f81(x63) = x63 >= x63 = x63
   |  |
   |  +- f2(x63,f82(x15)) = x63 + x15 >= x63 + x15 = f2(f81(x63),x15)
   |  |
   |  +- f83(x19) = x19 >= x19 = x19
   |  |
   |  +- f84(x16) = x16 >= x16 = x16
   |  |
   |  +- f85(x15,x16,x19,x63) = 1 + (x15 + x19) >= 1 + (x15 + x19) = f4(f82(x15),f84(x16),f83(x19))
   |  |
   |  +- f80(x15,x16,x19,x63) = 3 + (x15 + x16) >= 3 + (x15 + x16) = f3(f82(x15),f84(x16),f83(x19))
   |  |
   |  +- f4(x15,x16,x19 + 1) = 1 + (x15 + (x19 + 1)) >= (1 + (x15 + x19)) + 1 = f85(x15,x16,x19,x63) + 1
   |  |
   |  +- f3(x15,x16,x19 + 1) = 3 + (x15 + x16) >= 3 + (x15 + x16) = f80(x15,x16,x19,x63)
   |  |
   |  +- f4(x22,x23,0) = 1 + x22 >= 0 = 0
   |  |
   |  `- f3(x22,x23,0) = 3 + (x22 + x23) >= 0 = f86()
   |
   `- Stopping timer: 2017-03-30 07:32:30.179625 UTC(+0.02478s)