SUCCESS(1) SUCCESS f1(x0,x1) = x0 + x1; f2(x0,x1) = x0 + x1; f3(x0,x1,x2) = x0 + x1; f4(x0,x1,x2) = x2; f5(x0,x1,x2) = x0 + x1; f6(x0,x1,x2) = x2; f71(x0) = x0; f72(x0) = x0; f73(x0) = x0; f74(x0) = x0; f75(x0) = x0; f76(x0) = x0; f77(x0) = x0; f78(x0,x1) = x0 + x1; f79(x0) = x0; f80(x0,x1,x2,x3) = x0 + x1; f81(x0) = x0; f82(x0) = x0; f83(x0) = x0; f84(x0) = x0; f85(x0,x1,x2,x3) = x2; f86() = 0; ExecutionLog | `- SOLVE ... | +- Staring timer: 2017-03-30 07:32:30.187326 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() | +- Simplification ... | | | +- Substituted: f80(x15,x16,x19,x63) ≥ f2(f79(x16),x15) ↦ f80(x15,x16,0,0) ≥ f2(f79(x16),x15) | | | +- Substituted: f85(x15,x16,x19,x63) ≥ f4(f82(x15),f84(x16),f83(x19)) ↦ f85(x15,x16,x19,0) ≥ f4(f82(x15),f84(x16),f83(x19)) | | | +- Substituted: f80(x15,x16,x19,x63) ≥ f3(f82(x15),f84(x16),f83(x19)) ↦ f80(x15,x16,x19,0) ≥ f3(f82(x15),f84(x16),f83(x19)) | | | +- Substituted: f4(x22,x23,0) ≥ 0 ↦ f4(0,0,0) ≥ 0 | | | +- Substituted: f3(x22,x23,0) ≥ f86() ↦ f3(0,0,0) ≥ f86() | | | +- Eliminated: f86/0 | | | +- Propagated: f71(x0) ↦ x0 | | | +- Propagated: f72(x0) ↦ x0 | | | +- Propagated: f74(x0) ↦ x0 | | | +- Propagated: f75(x0) ↦ x0 | | | +- Propagated: f76(x0) ↦ x0 | | | +- Propagated: f77(x0) ↦ x0 | | | +- Propagated: f79(x0) ↦ x0 | | | +- Propagated: f81(x0) ↦ x0 | | | +- Propagated: f83(x0) ↦ x0 | | | `- Propagated: f84(x0) ↦ x0 | +- SMT-MSLI ... | | | +- Staring timer: 2017-03-30 07:32:30.187714 UTC | | | +- Interpretation | | | | | +- f1(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = max(x0 + x1,6) | | | | | +- f3(x0,x1,x2) = 15 + x0 + x1 + x2 | | | | | +- f4(x0,x1,x2) = max(9 + x1 + x2,15 + x2) | | | | | +- f5(x0,x1,x2) = 15 + x0 + x1 + x2 | | | | | +- f6(x0,x1,x2) = max(15 + x1 + x2,4 + x0 + x1 + x2) | | | | | +- f73(x0) = x0 | | | | | +- f78(x0,x1) = x0 + x1 | | | | | +- f80(x0,x1,x2,x3) = 15 + x0 + x1 + x2 | | | | | +- f82(x0) = x0 | | | | | `- f85(x0,x1,x2,x3) = max(9 + x1 + x2,15 + x2) | | | +- Minimizing with ZeroOut ... | | | +- Interpretation | | | | | +- f1(x0,x1) = x0 + x1 | | | | | +- f2(x0,x1) = x0 + x1 | | | | | +- f3(x0,x1,x2) = x0 + x1 | | | | | +- f4(x0,x1,x2) = x2 | | | | | +- f5(x0,x1,x2) = x0 + x1 | | | | | +- f6(x0,x1,x2) = x2 | | | | | +- f73(x0) = x0 | | | | | +- f78(x0,x1) = x0 + x1 | | | | | +- f80(x0,x1,x2,x3) = x0 + x1 | | | | | +- f82(x0) = x0 | | | | | `- f85(x0,x1,x2,x3) = x2 | | | +- Minimizing with ZeroOut... Failed | | | +- Minimizing with ShiftMax... Failed | | | +- Minimizing with DecreaseCoeff... Failed | | | `- Stopping timer: 2017-03-30 07:32:30.325487 UTC(+0.137773s) | +- Interpretation | | | +- f1(x0,x1) = x0 + x1 | | | +- f2(x0,x1) = x0 + x1 | | | +- f3(x0,x1,x2) = x0 + x1 | | | +- f4(x0,x1,x2) = x2 | | | +- f5(x0,x1,x2) = x0 + x1 | | | +- f6(x0,x1,x2) = x2 | | | +- f71(x0) = x0 | | | +- f72(x0) = x0 | | | +- f73(x0) = x0 | | | +- f74(x0) = x0 | | | +- f75(x0) = x0 | | | +- f76(x0) = x0 | | | +- f77(x0) = x0 | | | +- f78(x0,x1) = x0 + x1 | | | +- f79(x0) = x0 | | | +- f80(x0,x1,x2,x3) = x0 + x1 | | | +- f81(x0) = x0 | | | +- f82(x0) = x0 | | | +- f83(x0) = x0 | | | +- f84(x0) = x0 | | | +- f85(x0,x1,x2,x3) = x2 | | | `- f86() = 0 | +- Constraints | | | +- f71(x2) = x2 >= x2 = x2 | | | +- f72(x34) = x34 >= x34 = x34 | | | +- f2(x34,f73(x2)) = x34 + x2 >= x2 + x34 = f1(f71(x2),f72(x34)) | | | +- f74(x4) = x4 >= x4 = x4 | | | +- f75(x3) = x3 >= x3 = x3 | | | +- f6(x2,x3,x4) = x4 >= x4 = f4(f73(x2),f75(x3),f74(x4)) | | | +- f5(x2,x3,x4) = x2 + x3 >= x2 + x3 = f3(f73(x2),f75(x3),f74(x4)) | | | +- f76(x9) = x9 >= x9 = x9 | | | +- f77(x7) = x7 >= x7 = x7 | | | +- f78(x7,x9) = x7 + x9 >= x9 + x7 = f1(f76(x9),f77(x7)) | | | +- f1(x9 + 1,x7) = (x9 + 1) + x7 >= (x7 + x9) + 1 = f78(x7,x9) + 1 | | | +- f1(0,x12) = x12 >= x12 = x12 | | | +- f79(x16) = x16 >= x16 = x16 | | | +- f80(x15,x16,x19,x63) = 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) = x19 >= x19 = f4(f82(x15),f84(x16),f83(x19)) | | | +- f80(x15,x16,x19,x63) = x15 + x16 >= x15 + x16 = f3(f82(x15),f84(x16),f83(x19)) | | | +- f4(x15,x16,x19 + 1) = x19 + 1 >= x19 + 1 = f85(x15,x16,x19,x63) + 1 | | | +- f3(x15,x16,x19 + 1) = x15 + x16 >= x15 + x16 = f80(x15,x16,x19,x63) | | | +- f4(x22,x23,0) = 0 >= 0 = 0 | | | `- f3(x22,x23,0) = x22 + x23 >= 0 = f86() | `- Stopping timer: 2017-03-30 07:32:30.325585 UTC(+0.138259s)