SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f10(x0,x1) = 3 + 2*x0;
f108(x0) = x0;
f109(x0) = x0;
f11(x0,x1,x2) = 0;
f110(x0) = x0;
f111(x0) = x0;
f112(x0) = x0;
f113(x0) = x0;
f114(x0) = x0;
f115(x0,x1,x2,x3) = x1;
f116(x0) = x0;
f117(x0,x1,x2,x3,x4) = x2;
f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + 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) = 1 + x1 + x2;
f128(x0,x1,x2) = 1 + x1 + x2;
f129(x0) = x0;
f130(x0) = x0;
f131(x0) = x0;
f132(x0,x1) = x0 + x1;
f133(x0,x1,x2) = 1 + x0 + x2;
f134(x0,x1,x2) = 2 + 2*x0 + x2;
f2(x0,x1) = 1 + x0;
f3(x0,x1,x2) = 0;
f4(x0,x1) = 2*x0 + x1;
f5(x0,x1) = 4 + 2*x0;
f7(x0,x1) = x0 + x1;
f8(x0,x1) = 1 + x1;
f9(x0,x1) = 2*x0 + x1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:11.695259 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
   |
   +- Simplification ...
   |  |
   |  +- Substituted: f2(0,x13) + x14 ≥ f129(x14) + 1 ↦ f2(0,0) + x14 ≥ f129(x14) + 1
   |  |
   |  +- Eliminated: f11/3
   |  |
   |  +- Eliminated: f3/3
   |  |
   |  +- Propagated: f108(x0) ↦ x0
   |  |
   |  +- Propagated: f110(x0) ↦ x0
   |  |
   |  +- Propagated: f112(x0) ↦ x0
   |  |
   |  +- Propagated: f113(x0) ↦ x0
   |  |
   |  +- Propagated: f116(x0) ↦ x0
   |  |
   |  +- Propagated: f119(x0) ↦ x0
   |  |
   |  +- Propagated: f122(x0) ↦ x0
   |  |
   |  +- Propagated: f124(x0) ↦ x0
   |  |
   |  +- Propagated: f129(x0) ↦ x0
   |  |
   |  +- Propagated: f130(x0) ↦ x0
   |  |
   |  +- Propagated: f131(x0) ↦ x0
   |  |
   |  +- Propagated: f109(x0) ↦ x0
   |  |
   |  +- Propagated: f120(x0) ↦ x0
   |  |
   |  +- Propagated: f111(x0) ↦ x0
   |  |
   |  +- Propagated: f121(x0) ↦ x0
   |  |
   |  +- Propagated: f115(x0,x1,x2,x3) ↦ x1
   |  |
   |  +- Propagated: f123(x0) ↦ x0
   |  |
   |  +- Propagated: f117(x0,x1,x2,x3,x4) ↦ x2
   |  |
   |  `- Propagated: f125(x0,x1,x2) ↦ x1
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:11.697044 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:11.833466 UTC(+0.136422s)
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:11.8335 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:13.460485 UTC(+1.626985s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:13.460501 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0,x1) = 3 + 15*x0 + 15*x1
   |  |  |
   |  |  +- f114(x0) = x0
   |  |  |
   |  |  +- f118(x0,x1,x2,x3,x4) = 12 + 15*x0 + 15*x1 + x2
   |  |  |
   |  |  +- f126(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f127(x0,x1,x2) = 1 + x1 + 4*x2
   |  |  |
   |  |  +- f128(x0,x1,x2) = 3 + x1 + 4*x2
   |  |  |
   |  |  +- f132(x0,x1) = x0 + 2*x1
   |  |  |
   |  |  +- f133(x0,x1,x2) = 1 + 6*x0 + 7*x1 + x2
   |  |  |
   |  |  +- f134(x0,x1,x2) = 2 + 13*x0 + 15*x1 + x2
   |  |  |
   |  |  +- f2(x0,x1) = 1 + 4*x0
   |  |  |
   |  |  +- f4(x0,x1) = 13 + 10*x0 + 14*x1
   |  |  |
   |  |  +- f5(x0,x1) = 15 + 15*x0 + 15*x1
   |  |  |
   |  |  +- f7(x0,x1) = 2*x0 + x1
   |  |  |
   |  |  +- f8(x0,x1) = 1 + 3*x0 + 4*x1
   |  |  |
   |  |  `- f9(x0,x1) = 11 + 4*x0 + 10*x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0,x1) = 3 + 2*x0 + x1
   |  |  |
   |  |  +- f114(x0) = x0
   |  |  |
   |  |  +- f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + x1 + x2
   |  |  |
   |  |  +- f126(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f127(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f128(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f132(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f133(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  +- f134(x0,x1,x2) = 2 + 2*x0 + x2
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f4(x0,x1) = 1 + 2*x0 + 10*x1
   |  |  |
   |  |  +- f5(x0,x1) = 4 + 2*x0 + x1
   |  |  |
   |  |  +- f7(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f8(x0,x1) = 1 + x1
   |  |  |
   |  |  `- f9(x0,x1) = 1 + 2*x0 + 10*x1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0,x1) = 3 + 2*x0
   |  |  |
   |  |  +- f114(x0) = x0
   |  |  |
   |  |  +- f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + x2
   |  |  |
   |  |  +- f126(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f127(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f128(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f132(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f133(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  +- f134(x0,x1,x2) = 2 + 2*x0 + x2
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f4(x0,x1) = 2*x0 + x1
   |  |  |
   |  |  +- f5(x0,x1) = 4 + 2*x0
   |  |  |
   |  |  +- f7(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f8(x0,x1) = 1 + x1
   |  |  |
   |  |  `- f9(x0,x1) = 2*x0 + x1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:13.731227 UTC(+0.270726s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + x1
   |  |
   |  +- f10(x0,x1) = 3 + 2*x0
   |  |
   |  +- f108(x0) = x0
   |  |
   |  +- f109(x0) = x0
   |  |
   |  +- f11(x0,x1,x2) = 0
   |  |
   |  +- f110(x0) = x0
   |  |
   |  +- f111(x0) = x0
   |  |
   |  +- f112(x0) = x0
   |  |
   |  +- f113(x0) = x0
   |  |
   |  +- f114(x0) = x0
   |  |
   |  +- f115(x0,x1,x2,x3) = x1
   |  |
   |  +- f116(x0) = x0
   |  |
   |  +- f117(x0,x1,x2,x3,x4) = x2
   |  |
   |  +- f118(x0,x1,x2,x3,x4) = 3 + 2*x0 + 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) = 1 + x1 + x2
   |  |
   |  +- f128(x0,x1,x2) = 1 + x1 + x2
   |  |
   |  +- f129(x0) = x0
   |  |
   |  +- f130(x0) = x0
   |  |
   |  +- f131(x0) = x0
   |  |
   |  +- f132(x0,x1) = x0 + x1
   |  |
   |  +- f133(x0,x1,x2) = 1 + x0 + x2
   |  |
   |  +- f134(x0,x1,x2) = 2 + 2*x0 + x2
   |  |
   |  +- f2(x0,x1) = 1 + x0
   |  |
   |  +- f3(x0,x1,x2) = 0
   |  |
   |  +- f4(x0,x1) = 2*x0 + x1
   |  |
   |  +- f5(x0,x1) = 4 + 2*x0
   |  |
   |  +- f7(x0,x1) = x0 + x1
   |  |
   |  +- f8(x0,x1) = 1 + x1
   |  |
   |  `- f9(x0,x1) = 2*x0 + 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) = x50 >= x50 = x50
   |  |
   |  +- f113(x51) = x51 >= x51 = x51
   |  |
   |  +- f7(x50,f114(x2)) = x50 + x2 >= x2 + x50 = f1(f110(x2),f112(x50))
   |  |
   |  +- f8(x50,f114(x2)) + x51 = (1 + x2) + x51 >= (1 + x2) + x51 = f2(f110(x2),f112(x50)) + f113(x51)
   |  |
   |  +- f115(x2,x4,x50,x51) = x4 >= x4 = f3(f110(x2),f112(x50),f113(x51)) + f111(x4)
   |  |
   |  +- f116(x3) = x3 >= x3 = x3
   |  |
   |  +- f117(x2,x3,x4,x50,x51) = x4 >= x4 = f11(f114(x2),f116(x3),f117(x2,x3,x4,x50,x51)) + f115(x2,x4,x50,x51)
   |  |
   |  +- f118(x2,x3,x4,x50,x51) = 3 + ((2 * x2) + x4) >= (3 + (2 * x2)) + x4 = f10(f114(x2),f116(x3)) + f117(x2,x3,x4,x50,x51)
   |  |
   |  +- f4(x2,x3) = (2 * x2) + x3 >= (2 * x2) + x3 = f9(f114(x2),f116(x3))
   |  |
   |  +- f5(x2,x3) + x4 = (4 + (2 * x2)) + x4 >= (3 + ((2 * x2) + 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) = 1 + (x8 + x10) >= (1 + x10) + x8 = f2(f122(x10),f124(x7)) + f125(x7,x8,x10)
   |  |
   |  +- f128(x7,x8,x10) = 1 + (x8 + x10) >= 1 + (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 = (1 + (x10 + 1)) + x8 >= (1 + (x8 + x10)) + 1 = f128(x7,x8,x10) + 1
   |  |
   |  +- f129(x14) = x14 >= x14 = x14
   |  |
   |  +- f1(0,x13) = x13 >= x13 = x13
   |  |
   |  +- f2(0,x13) + x14 = 1 + x14 >= x14 + 1 = f129(x14) + 1
   |  |
   |  +- f130(x18) = x18 >= x18 = x18
   |  |
   |  +- f131(x19) = x19 >= x19 = x19
   |  |
   |  +- f132(x17,x18) = x17 + x18 >= x18 + x17 = f7(f130(x18),x17)
   |  |
   |  +- f133(x17,x18,x19) = 1 + (x17 + x19) >= (1 + x17) + x19 = f8(f130(x18),x17) + f131(x19)
   |  |
   |  +- f134(x17,x18,x19) = 2 + ((2 * x17) + x19) >= (1 + x17) + (1 + (x17 + x19)) = f8(f132(x17,x18),x17) + f133(x17,x18,x19)
   |  |
   |  +- f9(x17,x18) = (2 * x17) + x18 >= (x17 + x18) + x17 = f7(f132(x17,x18),x17)
   |  |
   |  `- f10(x17,x18) + x19 = (3 + (2 * x17)) + x19 >= (2 + ((2 * x17) + x19)) + 1 = f134(x17,x18,x19) + 1
   |
   `- Stopping timer: 2017-03-30 07:32:13.731621 UTC(+2.036362s)