SUCCESS(1) SUCCESS f1(x0) = 10 + 14*x0; f131(x0) = x0; f132(x0) = 1 + x0; f133(x0) = x0; f134(x0) = 3 + x0; f135() = 4; f136(x0) = 1 + x0; f137(x0) = x0; f138(x0,x1,x2,x3) = 4 + x1; f139(x0,x1,x2,x3) = 14 + 15*x0 + x1; f140(x0) = x0; f141(x0) = x0; f142(x0) = x0; f143(x0) = x0; f144(x0) = 4; f145(x0) = x0; f146(x0) = x0; f147(x0,x1,x2,x3,x4) = x1; f148(x0,x1) = x1; f149(x0,x1,x2,x3,x4) = 4 + x1; f150(x0,x1,x2,x3,x4) = 14 + x1 + 13*x2; f151(x0) = x0; f152(x0) = x0; f2(x0) = 15 + 15*x0; f3(x0,x1) = x0; f4(x0,x1) = 4; f5(x0,x1) = x0 + 12*x1; f6(x0,x1) = 2 + 2*x0 + 13*x1; f7(x0,x1,x2) = 0; f8(x0) = x0; f9(x0) = 1; ExecutionLog | `- SOLVE ... | +- Staring timer: 2017-03-30 07:44:00.854599 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 | +- SMT-SLI ... | | | +- Staring timer: 2017-03-30 07:44:00.854682 UTC | | | `- Stopping timer: 2017-03-30 07:44:00.8813 UTC(+0.026618s) | +- SMT-LI ... | | | +- Staring timer: 2017-03-30 07:44:00.881308 UTC | | | +- Interpretation | | | | | +- f1(x0) = 10 + 14*x0 | | | | | +- f131(x0) = x0 | | | | | +- f132(x0) = 1 + x0 | | | | | +- f133(x0) = x0 | | | | | +- f134(x0) = 3 + x0 | | | | | +- f135() = 4 | | | | | +- f136(x0) = 1 + x0 | | | | | +- f137(x0) = x0 | | | | | +- f138(x0,x1,x2,x3) = 4 + x1 | | | | | +- f139(x0,x1,x2,x3) = 14 + 15*x0 + x1 | | | | | +- f140(x0) = x0 | | | | | +- f141(x0) = x0 | | | | | +- f142(x0) = x0 | | | | | +- f143(x0) = x0 | | | | | +- f144(x0) = 4 | | | | | +- f145(x0) = x0 | | | | | +- f146(x0) = x0 | | | | | +- f147(x0,x1,x2,x3,x4) = x1 | | | | | +- f148(x0,x1) = x1 | | | | | +- f149(x0,x1,x2,x3,x4) = 4 + x1 | | | | | +- f150(x0,x1,x2,x3,x4) = 14 + x1 + 13*x2 | | | | | +- f151(x0) = x0 | | | | | +- f152(x0) = x0 | | | | | +- f2(x0) = 15 + 15*x0 | | | | | +- f3(x0,x1) = x0 | | | | | +- f4(x0,x1) = 4 | | | | | +- f5(x0,x1) = x0 + 12*x1 | | | | | +- f6(x0,x1) = 2 + 2*x0 + 13*x1 | | | | | +- f7(x0,x1,x2) = 0 | | | | | +- f8(x0) = x0 | | | | | `- f9(x0) = 1 | | | `- Stopping timer: 2017-03-30 07:44:00.985111 UTC(+0.103803s) | +- Interpretation | | | +- f1(x0) = 10 + 14*x0 | | | +- f131(x0) = x0 | | | +- f132(x0) = 1 + x0 | | | +- f133(x0) = x0 | | | +- f134(x0) = 3 + x0 | | | +- f135() = 4 | | | +- f136(x0) = 1 + x0 | | | +- f137(x0) = x0 | | | +- f138(x0,x1,x2,x3) = 4 + x1 | | | +- f139(x0,x1,x2,x3) = 14 + 15*x0 + x1 | | | +- f140(x0) = x0 | | | +- f141(x0) = x0 | | | +- f142(x0) = x0 | | | +- f143(x0) = x0 | | | +- f144(x0) = 4 | | | +- f145(x0) = x0 | | | +- f146(x0) = x0 | | | +- f147(x0,x1,x2,x3,x4) = x1 | | | +- f148(x0,x1) = x1 | | | +- f149(x0,x1,x2,x3,x4) = 4 + x1 | | | +- f150(x0,x1,x2,x3,x4) = 14 + x1 + 13*x2 | | | +- f151(x0) = x0 | | | +- f152(x0) = x0 | | | +- f2(x0) = 15 + 15*x0 | | | +- f3(x0,x1) = x0 | | | +- f4(x0,x1) = 4 | | | +- f5(x0,x1) = x0 + 12*x1 | | | +- f6(x0,x1) = 2 + 2*x0 + 13*x1 | | | +- f7(x0,x1,x2) = 0 | | | +- f8(x0) = x0 | | | `- f9(x0) = 1 | +- Constraints | | | +- f131(x4) = x4 >= x4 = x4 | | | +- f132(x4) = 1 + x4 >= x4 = f131(x4) | | | +- f133(x50) = x50 >= x50 = x50 | | | +- f134(x51) = 3 + x51 >= x51 = x51 | | | +- f3(x50,f135()) = x50 >= x50 = f8(f133(x50)) | | | +- f4(x50,f135()) + x51 = 4 + x51 >= 1 + (3 + x51) = f9(f133(x50)) + f134(x51) | | | +- f136(x4) = 1 + x4 >= 1 + x4 = f132(x4) | | | +- f137(x3) = x3 >= x3 = x3 | | | +- f138(x3,x4,x50,x51) = 4 + x4 >= 1 + x4 = f7(f135(),f137(x3),f138(x3,x4,x50,x51)) + f136(x4) | | | +- f139(x3,x4,x50,x51) = 14 + ((15 * x3) + x4) >= (2 + (8 + (13 * x3))) + (4 + x4) = f6(f135(),f137(x3)) + f138(x3,x4,x50,x51) | | | +- f1(x3) = 10 + (14 * x3) >= 4 + (12 * x3) = f5(f135(),f137(x3)) | | | +- f2(x3) + x4 = (15 + (15 * x3)) + x4 >= (14 + ((15 * 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 = 4 + x83 >= 4 + 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) = 4 + x14 >= 4 + x14 = f4(f146(x16),x12) + f147(x12,x14,x16,x82,x83) | | | +- f150(x12,x14,x16,x82,x83) = 14 + (x14 + (13 * x16)) >= (2 + (8 + (13 * x16))) + (4 + x14) = f6(f144(x12),f148(x12,x16)) + f149(x12,x14,x16,x82,x83) | | | +- f5(x12,x16 + 1) = x12 + (12 * (x16 + 1)) >= 4 + (12 * x16) = f5(f144(x12),f148(x12,x16)) | | | +- f6(x12,x16 + 1) + x14 = (2 + ((2 * x12) + (13 * (x16 + 1)))) + x14 >= (14 + (x14 + (13 * x16))) + 1 = f150(x12,x14,x16,x82,x83) + 1 | | | +- f151(x23) = x23 >= x23 = x23 | | | +- f152(x23) = x23 >= x23 = f151(x23) | | | +- f5(x21,0) = x21 >= 0 = 0 | | | `- f6(x21,0) + x23 = (2 + (2 * x21)) + x23 >= x23 + 1 = f152(x23) + 1 | `- Stopping timer: 2017-03-30 07:44:00.985241 UTC(+0.130642s)