SUCCESS(1)

SUCCESS
f1(x0) = 0;
f131(x0) = x0;
f132(x0) = x0;
f133(x0) = x0;
f134(x0) = x0;
f135() = 0;
f136(x0) = x0;
f137(x0) = x0;
f138(x0,x1,x2,x3) = x1;
f139(x0,x1,x2,x3) = 1 + 2*x0 + x1;
f140(x0) = x0;
f141(x0) = x0;
f142(x0) = x0;
f143(x0) = x0;
f144(x0) = 0;
f145(x0) = x0;
f146(x0) = x0;
f147(x0,x1,x2,x3,x4) = x1;
f148(x0,x1) = x1;
f149(x0,x1,x2,x3,x4) = 1 + x1;
f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2;
f151(x0) = x0;
f152(x0) = x0;
f2(x0) = 2 + 2*x0;
f3(x0,x1) = x0;
f4(x0,x1) = 1;
f5(x0,x1) = 0;
f6(x0,x1) = 1 + 2*x1;
f7(x0,x1,x2) = 0;
f8(x0) = x0;
f9(x0) = 1;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:44:00.99314 UTC
   |
   +- Open Constraints
   |  |
   |  +- f131(x4) = f131(x4) >= x4 = x4
   |  |
   |  +- f132(x4) = f132(x4) >= f131(x4) = f131(x4)
   |  |
   |  +- f133(x50) = f133(x50) >= x50 = x50
   |  |
   |  +- f134(x51) = f134(x51) >= x51 = x51
   |  |
   |  +- f3(x50,f135()) = f3(x50,f135()) >= f8(f133(x50)) = f8(f133(x50))
   |  |
   |  +- f4(x50,f135()) + x51 = f4(x50,f135()) + x51 >= f9(f133(x50)) + f134(x51) = f9(f133(x50)) + f134(x51)
   |  |
   |  +- f136(x4) = f136(x4) >= f132(x4) = f132(x4)
   |  |
   |  +- f137(x3) = f137(x3) >= x3 = x3
   |  |
   |  +- f138(x3,x4,x50,x51) = f138(x3,x4,x50,x51) >= f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4) = f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4)
   |  |
   |  +- f139(x3,x4,x50,x51) = f139(x3,x4,x50,x51) >= f6(f135(),f137(x3)) + f138(x3,x4,x50,x51) = f6(f135(),f137(x3)) + f138(x3,x4,x50,x51)
   |  |
   |  +- f1(x3) = f1(x3) >= f5(f135(),f137(x3)) = f5(f135(),f137(x3))
   |  |
   |  +- f2(x3) + x4 = f2(x3) + x4 >= f139(x3,x4,x50,x51) + 1 = f139(x3,x4,x50,x51) + 1
   |  |
   |  +- f140(x7) = f140(x7) >= x7 = x7
   |  |
   |  +- f8(x9 + 1) = f8(x9 + 1) >= x9 = x9
   |  |
   |  +- f9(x9 + 1) + x7 = f9(x9 + 1) + x7 >= f140(x7) + 1 = f140(x7) + 1
   |  |
   |  +- f141(x14) = f141(x14) >= x14 = x14
   |  |
   |  +- f142(x82) = f142(x82) >= x82 = x82
   |  |
   |  +- f143(x83) = f143(x83) >= x83 = x83
   |  |
   |  +- f3(x82,f144(x12)) = f3(x82,f144(x12)) >= f3(f142(x82),x12) = f3(f142(x82),x12)
   |  |
   |  +- f4(x82,f144(x12)) + x83 = f4(x82,f144(x12)) + x83 >= f4(f142(x82),x12) + f143(x83) = f4(f142(x82),x12) + f143(x83)
   |  |
   |  +- f145(x14) = f145(x14) >= f141(x14) = f141(x14)
   |  |
   |  +- f146(x16) = f146(x16) >= x16 = x16
   |  |
   |  +- f147(x12,x14,x16,x82,x83) = f147(x12,x14,x16,x82,x83) >= f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14) = f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14)
   |  |
   |  +- f148(x12,x16) = f148(x12,x16) >= f3(f146(x16),x12) = f3(f146(x16),x12)
   |  |
   |  +- f149(x12,x14,x16,x82,x83) = f149(x12,x14,x16,x82,x83) >= f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83) = f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83)
   |  |
   |  +- f150(x12,x14,x16,x82,x83) = f150(x12,x14,x16,x82,x83) >= f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83)
   |  |
   |  +- f5(x12,x16 + 1) = f5(x12,x16 + 1) >= f5(f144(x12),f148(x12,x16)) = f5(f144(x12),f148(x12,x16))
   |  |
   |  +- f6(x12,x16 + 1) + x14 = f6(x12,x16 + 1) + x14 >= f150(x12,x14,x16,x82,x83) + 1 = f150(x12,x14,x16,x82,x83) + 1
   |  |
   |  +- f151(x23) = f151(x23) >= x23 = x23
   |  |
   |  +- f152(x23) = f152(x23) >= f151(x23) = f151(x23)
   |  |
   |  +- f5(x21,0) = f5(x21,0) >= 0 = 0
   |  |
   |  `- f6(x21,0) + x23 = f6(x21,0) + x23 >= f152(x23) + 1 = f152(x23) + 1
   |
   +- Simplification ...
   |  |
   |  +- Substituted: f9(x9 + 1) + x7 ≥ f140(x7) + 1 ↦ f9(1) + x7 ≥ f140(x7) + 1
   |  |
   |  +- Substituted: f5(x21,0) ≥ 0 ↦ f5(0,0) ≥ 0
   |  |
   |  +- Substituted: f6(x21,0) + x23 ≥ f152(x23) + 1 ↦ f6(0,0) + x23 ≥ f152(x23) + 1
   |  |
   |  +- Eliminated: f7/3
   |  |
   |  +- Propagated: f131(x0) ↦ x0
   |  |
   |  +- Propagated: f133(x0) ↦ x0
   |  |
   |  +- Propagated: f134(x0) ↦ x0
   |  |
   |  +- Propagated: f137(x0) ↦ x0
   |  |
   |  +- Propagated: f140(x0) ↦ x0
   |  |
   |  +- Propagated: f141(x0) ↦ x0
   |  |
   |  +- Propagated: f142(x0) ↦ x0
   |  |
   |  +- Propagated: f143(x0) ↦ x0
   |  |
   |  +- Propagated: f146(x0) ↦ x0
   |  |
   |  +- Propagated: f151(x0) ↦ x0
   |  |
   |  +- Propagated: f132(x0) ↦ x0
   |  |
   |  +- Propagated: f145(x0) ↦ x0
   |  |
   |  +- Propagated: f152(x0) ↦ x0
   |  |
   |  +- Propagated: f136(x0) ↦ x0
   |  |
   |  +- Propagated: f147(x0,x1,x2,x3,x4) ↦ x1
   |  |
   |  `- Propagated: f138(x0,x1,x2,x3) ↦ x1
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:44:00.993924 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:44:01.124067 UTC(+0.130143s)
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:44:01.124099 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:44:01.138899 UTC(+0.0148s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:44:01.138918 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 15 + 14*x0
   |  |  |
   |  |  +- f135() = 1
   |  |  |
   |  |  +- f139(x0,x1,x2,x3) = 13 + 11*x0 + x1
   |  |  |
   |  |  +- f144(x0) = 1
   |  |  |
   |  |  +- f148(x0,x1) = x1
   |  |  |
   |  |  +- f149(x0,x1,x2,x3,x4) = 4 + x1
   |  |  |
   |  |  +- f150(x0,x1,x2,x3,x4) = 9 + x0 + x1 + 9*x2
   |  |  |
   |  |  +- f2(x0) = 14 + 15*x0
   |  |  |
   |  |  +- f3(x0,x1) = x0
   |  |  |
   |  |  +- f4(x0,x1) = 2
   |  |  |
   |  |  +- f5(x0,x1) = 2 + 13*x0 + 14*x1
   |  |  |
   |  |  +- f6(x0,x1) = 1 + 4*x0 + 9*x1
   |  |  |
   |  |  +- f8(x0) = x0
   |  |  |
   |  |  `- f9(x0) = 1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 0
   |  |  |
   |  |  +- f135() = 1
   |  |  |
   |  |  +- f139(x0,x1,x2,x3) = 2 + 3*x0 + x1
   |  |  |
   |  |  +- f144(x0) = 1
   |  |  |
   |  |  +- f148(x0,x1) = x1
   |  |  |
   |  |  +- f149(x0,x1,x2,x3,x4) = 1 + x1
   |  |  |
   |  |  +- f150(x0,x1,x2,x3,x4) = 3 + x1 + 3*x2
   |  |  |
   |  |  +- f2(x0) = 3 + 3*x0
   |  |  |
   |  |  +- f3(x0,x1) = x0
   |  |  |
   |  |  +- f4(x0,x1) = 1
   |  |  |
   |  |  +- f5(x0,x1) = 0
   |  |  |
   |  |  +- f6(x0,x1) = 1 + x0 + 3*x1
   |  |  |
   |  |  +- f8(x0) = x0
   |  |  |
   |  |  `- f9(x0) = 1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 0
   |  |  |
   |  |  +- f135() = 1
   |  |  |
   |  |  +- f139(x0,x1,x2,x3) = 2 + 2*x0 + x1
   |  |  |
   |  |  +- f144(x0) = 0
   |  |  |
   |  |  +- f148(x0,x1) = x1
   |  |  |
   |  |  +- f149(x0,x1,x2,x3,x4) = 1 + x1
   |  |  |
   |  |  +- f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2
   |  |  |
   |  |  +- f2(x0) = 3 + 2*x0
   |  |  |
   |  |  +- f3(x0,x1) = x0
   |  |  |
   |  |  +- f4(x0,x1) = 1
   |  |  |
   |  |  +- f5(x0,x1) = 0
   |  |  |
   |  |  +- f6(x0,x1) = 1 + x0 + 2*x1
   |  |  |
   |  |  +- f8(x0) = x0
   |  |  |
   |  |  `- f9(x0) = 1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 0
   |  |  |
   |  |  +- f135() = 1
   |  |  |
   |  |  +- f139(x0,x1,x2,x3) = 2 + 2*x0 + x1
   |  |  |
   |  |  +- f144(x0) = 0
   |  |  |
   |  |  +- f148(x0,x1) = x1
   |  |  |
   |  |  +- f149(x0,x1,x2,x3,x4) = 1 + x1
   |  |  |
   |  |  +- f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2
   |  |  |
   |  |  +- f2(x0) = 3 + 2*x0
   |  |  |
   |  |  +- f3(x0,x1) = x0
   |  |  |
   |  |  +- f4(x0,x1) = 1
   |  |  |
   |  |  +- f5(x0,x1) = 0
   |  |  |
   |  |  +- f6(x0,x1) = 1 + 2*x1
   |  |  |
   |  |  +- f8(x0) = x0
   |  |  |
   |  |  `- f9(x0) = 1
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 0
   |  |  |
   |  |  +- f135() = 0
   |  |  |
   |  |  +- f139(x0,x1,x2,x3) = 2 + 2*x0 + x1
   |  |  |
   |  |  +- f144(x0) = 0
   |  |  |
   |  |  +- f148(x0,x1) = x1
   |  |  |
   |  |  +- f149(x0,x1,x2,x3,x4) = 1 + x1
   |  |  |
   |  |  +- f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2
   |  |  |
   |  |  +- f2(x0) = 3 + 2*x0
   |  |  |
   |  |  +- f3(x0,x1) = x0
   |  |  |
   |  |  +- f4(x0,x1) = 1
   |  |  |
   |  |  +- f5(x0,x1) = 0
   |  |  |
   |  |  +- f6(x0,x1) = 1 + 2*x1
   |  |  |
   |  |  +- f8(x0) = x0
   |  |  |
   |  |  `- f9(x0) = 1
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with  DecreaseCoeff ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0) = 0
   |  |  |
   |  |  +- f135() = 0
   |  |  |
   |  |  +- f139(x0,x1,x2,x3) = 1 + 2*x0 + x1
   |  |  |
   |  |  +- f144(x0) = 0
   |  |  |
   |  |  +- f148(x0,x1) = x1
   |  |  |
   |  |  +- f149(x0,x1,x2,x3,x4) = 1 + x1
   |  |  |
   |  |  +- f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2
   |  |  |
   |  |  +- f2(x0) = 2 + 2*x0
   |  |  |
   |  |  +- f3(x0,x1) = x0
   |  |  |
   |  |  +- f4(x0,x1) = 1
   |  |  |
   |  |  +- f5(x0,x1) = 0
   |  |  |
   |  |  +- f6(x0,x1) = 1 + 2*x1
   |  |  |
   |  |  +- f8(x0) = x0
   |  |  |
   |  |  `- f9(x0) = 1
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:44:01.221699 UTC(+0.082781s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0) = 0
   |  |
   |  +- f131(x0) = x0
   |  |
   |  +- f132(x0) = x0
   |  |
   |  +- f133(x0) = x0
   |  |
   |  +- f134(x0) = x0
   |  |
   |  +- f135() = 0
   |  |
   |  +- f136(x0) = x0
   |  |
   |  +- f137(x0) = x0
   |  |
   |  +- f138(x0,x1,x2,x3) = x1
   |  |
   |  +- f139(x0,x1,x2,x3) = 1 + 2*x0 + x1
   |  |
   |  +- f140(x0) = x0
   |  |
   |  +- f141(x0) = x0
   |  |
   |  +- f142(x0) = x0
   |  |
   |  +- f143(x0) = x0
   |  |
   |  +- f144(x0) = 0
   |  |
   |  +- f145(x0) = x0
   |  |
   |  +- f146(x0) = x0
   |  |
   |  +- f147(x0,x1,x2,x3,x4) = x1
   |  |
   |  +- f148(x0,x1) = x1
   |  |
   |  +- f149(x0,x1,x2,x3,x4) = 1 + x1
   |  |
   |  +- f150(x0,x1,x2,x3,x4) = 2 + x1 + 2*x2
   |  |
   |  +- f151(x0) = x0
   |  |
   |  +- f152(x0) = x0
   |  |
   |  +- f2(x0) = 2 + 2*x0
   |  |
   |  +- f3(x0,x1) = x0
   |  |
   |  +- f4(x0,x1) = 1
   |  |
   |  +- f5(x0,x1) = 0
   |  |
   |  +- f6(x0,x1) = 1 + 2*x1
   |  |
   |  +- f7(x0,x1,x2) = 0
   |  |
   |  +- f8(x0) = x0
   |  |
   |  `- f9(x0) = 1
   |
   +- Constraints
   |  |
   |  +- f131(x4) = x4 >= x4 = x4
   |  |
   |  +- f132(x4) = x4 >= x4 = f131(x4)
   |  |
   |  +- f133(x50) = x50 >= x50 = x50
   |  |
   |  +- f134(x51) = x51 >= x51 = x51
   |  |
   |  +- f3(x50,f135()) = x50 >= x50 = f8(f133(x50))
   |  |
   |  +- f4(x50,f135()) + x51 = 1 + x51 >= 1 + x51 = f9(f133(x50)) + f134(x51)
   |  |
   |  +- f136(x4) = x4 >= x4 = f132(x4)
   |  |
   |  +- f137(x3) = x3 >= x3 = x3
   |  |
   |  +- f138(x3,x4,x50,x51) = x4 >= x4 = f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4)
   |  |
   |  +- f139(x3,x4,x50,x51) = 1 + ((2 * x3) + x4) >= (1 + (2 * x3)) + x4 = f6(f135(),f137(x3)) + f138(x3,x4,x50,x51)
   |  |
   |  +- f1(x3) = 0 >= 0 = f5(f135(),f137(x3))
   |  |
   |  +- f2(x3) + x4 = (2 + (2 * x3)) + x4 >= (1 + ((2 * x3) + x4)) + 1 = f139(x3,x4,x50,x51) + 1
   |  |
   |  +- f140(x7) = x7 >= x7 = x7
   |  |
   |  +- f8(x9 + 1) = x9 + 1 >= x9 = x9
   |  |
   |  +- f9(x9 + 1) + x7 = 1 + x7 >= x7 + 1 = f140(x7) + 1
   |  |
   |  +- f141(x14) = x14 >= x14 = x14
   |  |
   |  +- f142(x82) = x82 >= x82 = x82
   |  |
   |  +- f143(x83) = x83 >= x83 = x83
   |  |
   |  +- f3(x82,f144(x12)) = x82 >= x82 = f3(f142(x82),x12)
   |  |
   |  +- f4(x82,f144(x12)) + x83 = 1 + x83 >= 1 + x83 = f4(f142(x82),x12) + f143(x83)
   |  |
   |  +- f145(x14) = x14 >= x14 = f141(x14)
   |  |
   |  +- f146(x16) = x16 >= x16 = x16
   |  |
   |  +- f147(x12,x14,x16,x82,x83) = x14 >= x14 = f7(f144(x12),f148(x12,x16),f149(x12,x14,x16,x82,x83)) + f145(x14)
   |  |
   |  +- f148(x12,x16) = x16 >= x16 = f3(f146(x16),x12)
   |  |
   |  +- f149(x12,x14,x16,x82,x83) = 1 + x14 >= 1 + x14 = f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83)
   |  |
   |  +- f150(x12,x14,x16,x82,x83) = 2 + (x14 + (2 * x16)) >= (1 + (2 * x16)) + (1 + x14) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83)
   |  |
   |  +- f5(x12,x16 + 1) = 0 >= 0 = f5(f144(x12),f148(x12,x16))
   |  |
   |  +- f6(x12,x16 + 1) + x14 = (1 + (2 * (x16 + 1))) + x14 >= (2 + (x14 + (2 * x16))) + 1 = f150(x12,x14,x16,x82,x83) + 1
   |  |
   |  +- f151(x23) = x23 >= x23 = x23
   |  |
   |  +- f152(x23) = x23 >= x23 = f151(x23)
   |  |
   |  +- f5(x21,0) = 0 >= 0 = 0
   |  |
   |  `- f6(x21,0) + x23 = 1 + x23 >= x23 + 1 = f152(x23) + 1
   |
   `- Stopping timer: 2017-03-30 07:44:01.221831 UTC(+0.228691s)