SUCCESS(1)

SUCCESS
f1(x0,x1) = 1 + x0;
f2(x0,x1,x2) = 1 + x1 + x2;
f3(x0) = 1 + x0;
f4(x0,x1) = x0 + x1;
f82(x0) = x0;
f83() = 0;
f84(x0) = x0;
f85() = 0;
f86(x0,x1) = 1 + x0;
f87() = 0;
f88(x0) = x0;
f89(x0) = 0;
f90(x0) = x0;
f91(x0) = x0;
f92(x0) = 0;
f93(x0) = x0;
f94(x0) = x0;
f95(x0,x1,x2,x3) = 1 + x1 + x2;
f96(x0) = x0;
f97(x0) = x0;
f98(x0) = x0;
f99(x0) = 1 + x0;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:32.903059 UTC
   |
   +- Open Constraints
   |  |
   |  +- f82(x38) = f82(x38) >= x38 = x38
   |  |
   |  +- f1(x38,f83()) = f1(x38,f83()) >= f82(x38) + 1 = f82(x38) + 1
   |  |
   |  +- f84(x2) = f84(x2) >= x2 = x2
   |  |
   |  +- f85() = f85() >= 0 = 0
   |  |
   |  +- f86(x2,x38) = f86(x2,x38) >= f2(f83(),f84(x2),f85()) = f2(f83(),f84(x2),f85())
   |  |
   |  +- f87() = f87() >= 0 = 0
   |  |
   |  +- f3(x2) = f3(x2) >= f4(f86(x2,x38),f87()) = f4(f86(x2,x38),f87())
   |  |
   |  +- f88(x51) = f88(x51) >= x51 = x51
   |  |
   |  +- f1(x51,f89(x4)) = f1(x51,f89(x4)) >= f1(f88(x51),x4) = f1(f88(x51),x4)
   |  |
   |  +- f90(x9) = f90(x9) >= x9 = x9
   |  |
   |  +- f91(x63) = f91(x63) >= x63 = x63
   |  |
   |  +- f1(x63,f92(x4)) = f1(x63,f92(x4)) >= f1(f91(x63),x4) = f1(f91(x63),x4)
   |  |
   |  +- f93(x8) = f93(x8) >= x8 = x8
   |  |
   |  +- f94(x6) = f94(x6) >= x6 = x6
   |  |
   |  +- f95(x4,x6,x8,x63) = f95(x4,x6,x8,x63) >= f2(f92(x4),f93(x8),f94(x6)) = f2(f92(x4),f93(x8),f94(x6))
   |  |
   |  +- f2(x4,(x8 + x9) + 1,x6) = f2(x4,(x8 + x9) + 1,x6) >= f2(f89(x4),f90(x9),f95(x4,x6,x8,x63)) = f2(f89(x4),f90(x9),f95(x4,x6,x8,x63))
   |  |
   |  +- f96(x14) = f96(x14) >= x14 = x14
   |  |
   |  +- f2(x12,0,x14) = f2(x12,0,x14) >= f1(f96(x14),x12) = f1(f96(x14),x12)
   |  |
   |  +- f97(x21) = f97(x21) >= x21 = x21
   |  |
   |  +- f98(x19) = f98(x19) >= x19 = x19
   |  |
   |  +- f99(x19) = f99(x19) >= f98(x19) + 1 = f98(x19) + 1
   |  |
   |  +- f4(x21 + 1,x19) = f4(x21 + 1,x19) >= f4(f97(x21),f99(x19)) = f4(f97(x21),f99(x19))
   |  |
   |  `- f4(0,x24) = f4(0,x24) >= x24 = x24
   |
   +- Simplification ...
   |  |
   |  +- Substituted: f86(x2,x38) ≥ f2(f83(),f84(x2),f85()) ↦ f86(x2,0) ≥ f2(f83(),f84(x2),f85())
   |  |
   |  +- Substituted: f95(x4,x6,x8,x63) ≥ f2(f92(x4),f93(x8),f94(x6)) ↦ f95(x4,x6,x8,0) ≥ f2(f92(x4),f93(x8),f94(x6))
   |  |
   |  +- Propagated: f82(x0) ↦ x0
   |  |
   |  +- Propagated: f84(x0) ↦ x0
   |  |
   |  +- Propagated: f85() ↦ 0
   |  |
   |  +- Propagated: f87() ↦ 0
   |  |
   |  +- Propagated: f88(x0) ↦ x0
   |  |
   |  +- Propagated: f90(x0) ↦ x0
   |  |
   |  +- Propagated: f91(x0) ↦ x0
   |  |
   |  +- Propagated: f93(x0) ↦ x0
   |  |
   |  +- Propagated: f94(x0) ↦ x0
   |  |
   |  +- Propagated: f96(x0) ↦ x0
   |  |
   |  +- Propagated: f97(x0) ↦ x0
   |  |
   |  +- Propagated: f98(x0) ↦ x0
   |  |
   |  `- Propagated: f99(x0) ↦ 1 + x0
   |
   +- SMT-MSLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:32.90353 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f2(x0,x1,x2) = max(6 + x0,15 + x1,1 + x1 + x2)
   |  |  |
   |  |  +- f3(x0) = 15 + x0
   |  |  |
   |  |  +- f4(x0,x1) = max(x0 + x1,7)
   |  |  |
   |  |  +- f83() = 0
   |  |  |
   |  |  +- f86(x0,x1) = 15 + x0
   |  |  |
   |  |  +- f89(x0) = 6
   |  |  |
   |  |  +- f92(x0) = 0
   |  |  |
   |  |  `- f95(x0,x1,x2,x3) = max(15 + x2,1 + x1 + x2)
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f2(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f3(x0) = 1 + x0
   |  |  |
   |  |  +- f4(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f83() = 0
   |  |  |
   |  |  +- f86(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f89(x0) = 0
   |  |  |
   |  |  +- f92(x0) = 0
   |  |  |
   |  |  `- f95(x0,x1,x2,x3) = 1 + x1 + x2
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with ShiftMax... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:33.010895 UTC(+0.107365s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = 1 + x0
   |  |
   |  +- f2(x0,x1,x2) = 1 + x1 + x2
   |  |
   |  +- f3(x0) = 1 + x0
   |  |
   |  +- f4(x0,x1) = x0 + x1
   |  |
   |  +- f82(x0) = x0
   |  |
   |  +- f83() = 0
   |  |
   |  +- f84(x0) = x0
   |  |
   |  +- f85() = 0
   |  |
   |  +- f86(x0,x1) = 1 + x0
   |  |
   |  +- f87() = 0
   |  |
   |  +- f88(x0) = x0
   |  |
   |  +- f89(x0) = 0
   |  |
   |  +- f90(x0) = x0
   |  |
   |  +- f91(x0) = x0
   |  |
   |  +- f92(x0) = 0
   |  |
   |  +- f93(x0) = x0
   |  |
   |  +- f94(x0) = x0
   |  |
   |  +- f95(x0,x1,x2,x3) = 1 + x1 + x2
   |  |
   |  +- f96(x0) = x0
   |  |
   |  +- f97(x0) = x0
   |  |
   |  +- f98(x0) = x0
   |  |
   |  `- f99(x0) = 1 + x0
   |
   +- Constraints
   |  |
   |  +- f82(x38) = x38 >= x38 = x38
   |  |
   |  +- f1(x38,f83()) = 1 + x38 >= x38 + 1 = f82(x38) + 1
   |  |
   |  +- f84(x2) = x2 >= x2 = x2
   |  |
   |  +- f85() = 0 >= 0 = 0
   |  |
   |  +- f86(x2,x38) = 1 + x2 >= 1 + x2 = f2(f83(),f84(x2),f85())
   |  |
   |  +- f87() = 0 >= 0 = 0
   |  |
   |  +- f3(x2) = 1 + x2 >= 1 + x2 = f4(f86(x2,x38),f87())
   |  |
   |  +- f88(x51) = x51 >= x51 = x51
   |  |
   |  +- f1(x51,f89(x4)) = 1 + x51 >= 1 + x51 = f1(f88(x51),x4)
   |  |
   |  +- f90(x9) = x9 >= x9 = x9
   |  |
   |  +- f91(x63) = x63 >= x63 = x63
   |  |
   |  +- f1(x63,f92(x4)) = 1 + x63 >= 1 + x63 = f1(f91(x63),x4)
   |  |
   |  +- f93(x8) = x8 >= x8 = x8
   |  |
   |  +- f94(x6) = x6 >= x6 = x6
   |  |
   |  +- f95(x4,x6,x8,x63) = 1 + (x6 + x8) >= 1 + (x8 + x6) = f2(f92(x4),f93(x8),f94(x6))
   |  |
   |  +- f2(x4,(x8 + x9) + 1,x6) = 1 + (((x8 + x9) + 1) + x6) >= 1 + (x9 + (1 + (x6 + x8))) = f2(f89(x4),f90(x9),f95(x4,x6,x8,x63))
   |  |
   |  +- f96(x14) = x14 >= x14 = x14
   |  |
   |  +- f2(x12,0,x14) = 1 + x14 >= 1 + x14 = f1(f96(x14),x12)
   |  |
   |  +- f97(x21) = x21 >= x21 = x21
   |  |
   |  +- f98(x19) = x19 >= x19 = x19
   |  |
   |  +- f99(x19) = x19 + 1 >= x19 + 1 = f98(x19) + 1
   |  |
   |  +- f4(x21 + 1,x19) = (x21 + 1) + x19 >= x21 + (x19 + 1) = f4(f97(x21),f99(x19))
   |  |
   |  `- f4(0,x24) = x24 >= x24 = x24
   |
   `- Stopping timer: 2017-03-30 07:32:33.010986 UTC(+0.107927s)