SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f10(x0,x1) = 5 + 12*x0;
f108(x0) = x0;
f109(x0) = x0;
f11(x0,x1,x2) = 2*x0 + 2*x1;
f110(x0) = x0;
f111(x0) = x0;
f112(x0) = 1 + x0;
f113(x0) = x0;
f114(x0) = x0;
f115(x0,x1,x2,x3) = 5 + x0 + x1;
f116(x0) = 2 + 3*x0;
f117(x0,x1,x2,x3,x4) = 9 + 3*x0 + 8*x1 + x2;
f118(x0,x1,x2,x3,x4) = 14 + 15*x0 + 10*x1 + x2;
f119(x0) = x0;
f120(x0) = x0;
f121(x0) = x0;
f122(x0) = x0;
f123(x0) = x0;
f124(x0) = x0;
f125(x0,x1,x2) = x1;
f126(x0,x1) = x0 + x1;
f127(x0,x1,x2) = 2 + x1 + x2;
f128(x0,x1,x2) = 2 + x1 + x2;
f129(x0) = x0;
f130(x0) = 1 + x0;
f131(x0) = x0;
f132(x0,x1) = 4 + 9*x0 + 4*x1;
f133(x0,x1,x2) = 2 + 8*x0 + x2;
f134(x0,x1,x2) = 4 + 12*x0 + x2;
f2(x0,x1) = 2 + x0;
f3(x0,x1,x2) = 0;
f4(x0,x1) = 14 + 15*x0 + 14*x1;
f5(x0,x1) = 15 + 15*x0 + 14*x1;
f7(x0,x1) = 2 + x0 + 4*x1;
f8(x0,x1) = 2 + 4*x1;
f9(x0,x1) = 6 + 13*x0 + 4*x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:11.447269 UTC
   |
   +- Open Constraints
   |  |
   |  +- f108(x4) = f108(x4) >= x4 = x4
   |  |
   |  +- f109(x4) = f109(x4) >= f108(x4) = f108(x4)
   |  |
   |  +- f110(x2) = f110(x2) >= x2 = x2
   |  |
   |  +- f111(x4) = f111(x4) >= f109(x4) = f109(x4)
   |  |
   |  +- f112(x50) = f112(x50) >= x50 = x50
   |  |
   |  +- f113(x51) = f113(x51) >= x51 = x51
   |  |
   |  +- f7(x50,f114(x2)) = f7(x50,f114(x2)) >= f1(f110(x2),f112(x50)) = f1(f110(x2),f112(x50))
   |  |
   |  +- f8(x50,f114(x2)) + x51 = f8(x50,f114(x2)) + x51 >= f2(f110(x2),f112(x50)) + f113(x51) = f2(f110(x2),f112(x50)) + f113(x51)
   |  |
   |  +- f115(x2,x4,x50,x51) = f115(x2,x4,x50,x51) >= f3(f110(x2),f112(x50),f113(x51)) + f111(x4) = f3(f110(x2),f112(x50),f113(x51)) + f111(x4)
   |  |
   |  +- f116(x3) = f116(x3) >= x3 = x3
   |  |
   |  +- f117(x2,x3,x4,x50,x51) = f117(x2,x3,x4,x50,x51) >= f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51) = f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51)
   |  |
   |  +- f118(x2,x3,x4,x50,x51) = f118(x2,x3,x4,x50,x51) >= f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51) = f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51)
   |  |
   |  +- f4(x2,x3) = f4(x2,x3) >= f9(f114(x2),f116(x3)) = f9(f114(x2),f116(x3))
   |  |
   |  +- f5(x2,x3) + x4 = f5(x2,x3) + x4 >= f118(x2,x3,x4,x50,x51) + 1 = f118(x2,x3,x4,x50,x51) + 1
   |  |
   |  +- f119(x8) = f119(x8) >= x8 = x8
   |  |
   |  +- f120(x8) = f120(x8) >= f119(x8) = f119(x8)
   |  |
   |  +- f121(x8) = f121(x8) >= f120(x8) = f120(x8)
   |  |
   |  +- f122(x10) = f122(x10) >= x10 = x10
   |  |
   |  +- f123(x8) = f123(x8) >= f121(x8) = f121(x8)
   |  |
   |  +- f124(x7) = f124(x7) >= x7 = x7
   |  |
   |  +- f125(x7,x8,x10) = f125(x7,x8,x10) >= f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8) = f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8)
   |  |
   |  +- f126(x7,x10) = f126(x7,x10) >= f1(f122(x10),f124(x7)) = f1(f122(x10),f124(x7))
   |  |
   |  +- f127(x7,x8,x10) = f127(x7,x8,x10) >= f2(f122(x10),f124(x7)) + f125(x7,x8,x10) = f2(f122(x10),f124(x7)) + f125(x7,x8,x10)
   |  |
   |  +- f128(x7,x8,x10) = f128(x7,x8,x10) >= f127(x7,x8,x10) = f127(x7,x8,x10)
   |  |
   |  +- f1(x10 + 1,x7) = f1(x10 + 1,x7) >= f126(x7,x10) + 1 = f126(x7,x10) + 1
   |  |
   |  +- f2(x10 + 1,x7) + x8 = f2(x10 + 1,x7) + x8 >= f128(x7,x8,x10) + 1 = f128(x7,x8,x10) + 1
   |  |
   |  +- f129(x14) = f129(x14) >= x14 = x14
   |  |
   |  +- f1(0,x13) = f1(0,x13) >= x13 = x13
   |  |
   |  +- f2(0,x13) + x14 = f2(0,x13) + x14 >= f129(x14) + 1 = f129(x14) + 1
   |  |
   |  +- f130(x18) = f130(x18) >= x18 = x18
   |  |
   |  +- f131(x19) = f131(x19) >= x19 = x19
   |  |
   |  +- f132(x17,x18) = f132(x17,x18) >= f7(f130(x18),x17) = f7(f130(x18),x17)
   |  |
   |  +- f133(x17,x18,x19) = f133(x17,x18,x19) >= f8(f130(x18),x17) + f131(x19) = f8(f130(x18),x17) + f131(x19)
   |  |
   |  +- f134(x17,x18,x19) = f134(x17,x18,x19) >= f8(f132(x17,x18),x17) + f133(x17,x18,x19) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
   |  |
   |  +- f9(x17,x18) = f9(x17,x18) >= f7(f132(x17,x18),x17) = f7(f132(x17,x18),x17)
   |  |
   |  `- f10(x17,x18) + x19 = f10(x17,x18) + x19 >= f134(x17,x18,x19) + 1 = f134(x17,x18,x19) + 1
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:11.447371 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:11.535308 UTC(+0.087937s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:11.535324 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0,x1) = 5 + 12*x0
   |  |  |
   |  |  +- f108(x0) = x0
   |  |  |
   |  |  +- f109(x0) = x0
   |  |  |
   |  |  +- f11(x0,x1,x2) = 2*x0 + 2*x1
   |  |  |
   |  |  +- f110(x0) = x0
   |  |  |
   |  |  +- f111(x0) = x0
   |  |  |
   |  |  +- f112(x0) = 1 + x0
   |  |  |
   |  |  +- f113(x0) = x0
   |  |  |
   |  |  +- f114(x0) = x0
   |  |  |
   |  |  +- f115(x0,x1,x2,x3) = 5 + x0 + x1
   |  |  |
   |  |  +- f116(x0) = 2 + 3*x0
   |  |  |
   |  |  +- f117(x0,x1,x2,x3,x4) = 9 + 3*x0 + 8*x1 + x2
   |  |  |
   |  |  +- f118(x0,x1,x2,x3,x4) = 14 + 15*x0 + 10*x1 + x2
   |  |  |
   |  |  +- f119(x0) = x0
   |  |  |
   |  |  +- f120(x0) = x0
   |  |  |
   |  |  +- f121(x0) = x0
   |  |  |
   |  |  +- f122(x0) = x0
   |  |  |
   |  |  +- f123(x0) = x0
   |  |  |
   |  |  +- f124(x0) = x0
   |  |  |
   |  |  +- f125(x0,x1,x2) = x1
   |  |  |
   |  |  +- f126(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f127(x0,x1,x2) = 2 + x1 + x2
   |  |  |
   |  |  +- f128(x0,x1,x2) = 2 + x1 + x2
   |  |  |
   |  |  +- f129(x0) = x0
   |  |  |
   |  |  +- f130(x0) = 1 + x0
   |  |  |
   |  |  +- f131(x0) = x0
   |  |  |
   |  |  +- f132(x0,x1) = 4 + 9*x0 + 4*x1
   |  |  |
   |  |  +- f133(x0,x1,x2) = 2 + 8*x0 + x2
   |  |  |
   |  |  +- f134(x0,x1,x2) = 4 + 12*x0 + x2
   |  |  |
   |  |  +- f2(x0,x1) = 2 + x0
   |  |  |
   |  |  +- f3(x0,x1,x2) = 0
   |  |  |
   |  |  +- f4(x0,x1) = 14 + 15*x0 + 14*x1
   |  |  |
   |  |  +- f5(x0,x1) = 15 + 15*x0 + 14*x1
   |  |  |
   |  |  +- f7(x0,x1) = 2 + x0 + 4*x1
   |  |  |
   |  |  +- f8(x0,x1) = 2 + 4*x1
   |  |  |
   |  |  `- f9(x0,x1) = 6 + 13*x0 + 4*x1
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:11.680687 UTC(+0.145363s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + x1
   |  |
   |  +- f10(x0,x1) = 5 + 12*x0
   |  |
   |  +- f108(x0) = x0
   |  |
   |  +- f109(x0) = x0
   |  |
   |  +- f11(x0,x1,x2) = 2*x0 + 2*x1
   |  |
   |  +- f110(x0) = x0
   |  |
   |  +- f111(x0) = x0
   |  |
   |  +- f112(x0) = 1 + x0
   |  |
   |  +- f113(x0) = x0
   |  |
   |  +- f114(x0) = x0
   |  |
   |  +- f115(x0,x1,x2,x3) = 5 + x0 + x1
   |  |
   |  +- f116(x0) = 2 + 3*x0
   |  |
   |  +- f117(x0,x1,x2,x3,x4) = 9 + 3*x0 + 8*x1 + x2
   |  |
   |  +- f118(x0,x1,x2,x3,x4) = 14 + 15*x0 + 10*x1 + x2
   |  |
   |  +- f119(x0) = x0
   |  |
   |  +- f120(x0) = x0
   |  |
   |  +- f121(x0) = x0
   |  |
   |  +- f122(x0) = x0
   |  |
   |  +- f123(x0) = x0
   |  |
   |  +- f124(x0) = x0
   |  |
   |  +- f125(x0,x1,x2) = x1
   |  |
   |  +- f126(x0,x1) = x0 + x1
   |  |
   |  +- f127(x0,x1,x2) = 2 + x1 + x2
   |  |
   |  +- f128(x0,x1,x2) = 2 + x1 + x2
   |  |
   |  +- f129(x0) = x0
   |  |
   |  +- f130(x0) = 1 + x0
   |  |
   |  +- f131(x0) = x0
   |  |
   |  +- f132(x0,x1) = 4 + 9*x0 + 4*x1
   |  |
   |  +- f133(x0,x1,x2) = 2 + 8*x0 + x2
   |  |
   |  +- f134(x0,x1,x2) = 4 + 12*x0 + x2
   |  |
   |  +- f2(x0,x1) = 2 + x0
   |  |
   |  +- f3(x0,x1,x2) = 0
   |  |
   |  +- f4(x0,x1) = 14 + 15*x0 + 14*x1
   |  |
   |  +- f5(x0,x1) = 15 + 15*x0 + 14*x1
   |  |
   |  +- f7(x0,x1) = 2 + x0 + 4*x1
   |  |
   |  +- f8(x0,x1) = 2 + 4*x1
   |  |
   |  `- f9(x0,x1) = 6 + 13*x0 + 4*x1
   |
   +- Constraints
   |  |
   |  +- f108(x4) = x4 >= x4 = x4
   |  |
   |  +- f109(x4) = x4 >= x4 = f108(x4)
   |  |
   |  +- f110(x2) = x2 >= x2 = x2
   |  |
   |  +- f111(x4) = x4 >= x4 = f109(x4)
   |  |
   |  +- f112(x50) = 1 + x50 >= x50 = x50
   |  |
   |  +- f113(x51) = x51 >= x51 = x51
   |  |
   |  +- f7(x50,f114(x2)) = 2 + (x50 + (4 * x2)) >= x2 + (1 + x50) = f1(f110(x2),f112(x50))
   |  |
   |  +- f8(x50,f114(x2)) + x51 = (2 + (4 * x2)) + x51 >= (2 + x2) + x51 = f2(f110(x2),f112(x50)) + f113(x51)
   |  |
   |  +- f115(x2,x4,x50,x51) = 5 + (x2 + x4) >= x4 = f3(f110(x2),f112(x50),f113(x51)) + f111(x4)
   |  |
   |  +- f116(x3) = 2 + (3 * x3) >= x3 = x3
   |  |
   |  +- f117(x2,x3,x4,x50,x51) = 9 + ((3 * x2) + ((8 * x3) + x4)) >= ((2 * x2) + (2 * (2 + (3 * x3)))) + (5 + (x2 + x4)) = f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51)
   |  |
   |  +- f118(x2,x3,x4,x50,x51) = 14 + ((15 * x2) + ((10 * x3) + x4)) >= (5 + (12 * x2)) + (9 + ((3 * x2) + ((8 * x3) + x4))) = f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51)
   |  |
   |  +- f4(x2,x3) = 14 + ((15 * x2) + (14 * x3)) >= 6 + ((13 * x2) + (4 * (2 + (3 * x3)))) = f9(f114(x2),f116(x3))
   |  |
   |  +- f5(x2,x3) + x4 = (15 + ((15 * x2) + (14 * x3))) + x4 >= (14 + ((15 * x2) + ((10 * x3) + x4))) + 1 = f118(x2,x3,x4,x50,x51) + 1
   |  |
   |  +- f119(x8) = x8 >= x8 = x8
   |  |
   |  +- f120(x8) = x8 >= x8 = f119(x8)
   |  |
   |  +- f121(x8) = x8 >= x8 = f120(x8)
   |  |
   |  +- f122(x10) = x10 >= x10 = x10
   |  |
   |  +- f123(x8) = x8 >= x8 = f121(x8)
   |  |
   |  +- f124(x7) = x7 >= x7 = x7
   |  |
   |  +- f125(x7,x8,x10) = x8 >= x8 = f3(f122(x10),f124(x7),f125(x7,x8,x10)) + f123(x8)
   |  |
   |  +- f126(x7,x10) = x7 + x10 >= x10 + x7 = f1(f122(x10),f124(x7))
   |  |
   |  +- f127(x7,x8,x10) = 2 + (x8 + x10) >= (2 + x10) + x8 = f2(f122(x10),f124(x7)) + f125(x7,x8,x10)
   |  |
   |  +- f128(x7,x8,x10) = 2 + (x8 + x10) >= 2 + (x8 + x10) = f127(x7,x8,x10)
   |  |
   |  +- f1(x10 + 1,x7) = (x10 + 1) + x7 >= (x7 + x10) + 1 = f126(x7,x10) + 1
   |  |
   |  +- f2(x10 + 1,x7) + x8 = (2 + (x10 + 1)) + x8 >= (2 + (x8 + x10)) + 1 = f128(x7,x8,x10) + 1
   |  |
   |  +- f129(x14) = x14 >= x14 = x14
   |  |
   |  +- f1(0,x13) = x13 >= x13 = x13
   |  |
   |  +- f2(0,x13) + x14 = 2 + x14 >= x14 + 1 = f129(x14) + 1
   |  |
   |  +- f130(x18) = 1 + x18 >= x18 = x18
   |  |
   |  +- f131(x19) = x19 >= x19 = x19
   |  |
   |  +- f132(x17,x18) = 4 + ((9 * x17) + (4 * x18)) >= 2 + ((1 + x18) + (4 * x17)) = f7(f130(x18),x17)
   |  |
   |  +- f133(x17,x18,x19) = 2 + ((8 * x17) + x19) >= (2 + (4 * x17)) + x19 = f8(f130(x18),x17) + f131(x19)
   |  |
   |  +- f134(x17,x18,x19) = 4 + ((12 * x17) + x19) >= (2 + (4 * x17)) + (2 + ((8 * x17) + x19)) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
   |  |
   |  +- f9(x17,x18) = 6 + ((13 * x17) + (4 * x18)) >= 2 + ((4 + ((9 * x17) + (4 * x18))) + (4 * x17)) = f7(f132(x17,x18),x17)
   |  |
   |  `- f10(x17,x18) + x19 = (5 + (12 * x17)) + x19 >= (4 + ((12 * x17) + x19)) + 1 = f134(x17,x18,x19) + 1
   |
   `- Stopping timer: 2017-03-30 07:32:11.680942 UTC(+0.233673s)