SUCCESS(1) SUCCESS f1(x0,x1,x2) = x0 + x1; f10(x0,x1,x2,x3,x4,x5,x6) = 0; f11(x0) = x0; f12(x0) = 1; f13(x0) = x0; f14(x0) = 3 + 2*x0; f15(x0,x1) = x0 + x1; f16(x0,x1) = 1 + 2*x0; f17(x0,x1,x2) = 1; f2(x0,x1,x2) = 1 + 2*x0; f264(x0) = x0; f265(x0) = x0; f266(x0) = x0; f267(x0,x1) = 1 + x1; f268() = 0; f269(x0,x1) = 1 + x1; f270(x0,x1) = 2 + 2*x0 + x1; f271(x0) = x0; f272(x0) = x0; f273(x0) = x0; f274(x0) = x0; f275(x0) = x0; f276(x0) = x0; f277() = 0; f278(x0) = x0; f279(x0) = x0; f280(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2; f281() = 0; f282(x0) = x0; f283(x0) = x0; f284(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2; f285(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2; f286(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2; f287(x0) = x0; f288(x0) = x0; f289(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2; f290(x0) = x0; f291(x0) = x0; f292(x0) = x0; f293(x0) = x0; f294(x0) = x0; f295(x0) = x0; f296(x0) = x0; f297(x0) = x0; f298(x0,x1,x2,x3,x4) = 1 + x4; f299(x0,x1,x2,x3) = 1 + x3; f3(x0,x1,x2,x3) = 1; f300(x0,x1,x2,x3,x4) = 1 + x4; f301(x0,x1,x2,x3,x4) = 2 + 2*x1 + x4; f4(x0,x1,x2,x3) = 1 + x2; f5(x0,x1,x2,x3) = 0; f6(x0,x1,x2,x3) = 1 + x1 + x3; f7(x0,x1,x2,x3) = 3 + 2*x1; f8(x0,x1,x2,x3,x4) = 0; f9(x0,x1,x2,x3,x4,x5) = 0; ExecutionLog | +- Staring timer: 2017-03-30 07:29:43.255001 UTC | +- Open Constraints | | | +- f264(x3) = f264(x3) >= x3 = x3 | | | +- f265(x2) = f265(x2) >= x2 = x2 | | | +- f266(x3) = f266(x3) >= f264(x3) = f264(x3) | | | +- f267(x2,x3) = f267(x2,x3) >= f17(f265(x2),f268(),f269(x2,x3)) + f266(x3) = f17(f265(x2),f268(),f269(x2,x3)) + f266(x3) | | | +- f268() = f268() >= 0 = 0 | | | +- f269(x2,x3) = f269(x2,x3) >= f267(x2,x3) = f267(x2,x3) | | | +- f270(x2,x3) = f270(x2,x3) >= f16(f265(x2),f268()) + f269(x2,x3) = f16(f265(x2),f268()) + f269(x2,x3) | | | +- f13(x2) = f13(x2) >= f15(f265(x2),f268()) = f15(f265(x2),f268()) | | | +- f14(x2) + x3 = f14(x2) + x3 >= f270(x2,x3) + 1 = f270(x2,x3) + 1 | | | +- f271(x8) = f271(x8) >= x8 = x8 | | | +- f272(x8) = f272(x8) >= f271(x8) = f271(x8) | | | +- f273(x84) = f273(x84) >= x84 = x84 | | | +- f274(x87) = f274(x87) >= x87 = x87 | | | +- f275(x85) = f275(x85) >= x85 = x85 | | | +- f276(x86) = f276(x86) >= x86 = x86 | | | +- f1(x84,x85,f277()) = f1(x84,x85,f277()) >= f15(f273(x84),f275(x85)) = f15(f273(x84),f275(x85)) | | | +- f2(x84,x85,f277()) + x86 = f2(x84,x85,f277()) + x86 >= f16(f273(x84),f275(x85)) + f276(x86) = f16(f273(x84),f275(x85)) + f276(x86) | | | +- f3(x84,x85,f277(),x86) + x87 = f3(x84,x85,f277(),x86) + x87 >= f17(f273(x84),f275(x85),f276(x86)) + f274(x87) = f17(f273(x84),f275(x85),f276(x86)) + f274(x87) | | | +- f278(x8) = f278(x8) >= f272(x8) = f272(x8) | | | +- f279(x10) = f279(x10) >= x10 = x10 | | | +- f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f10(f277() ,f279(x10) ,f281() ,f282(x6) ,f283(x7) ,f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) ,f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f278(x8) = f10(f277() ,f279(x10) ,f281() ,f282(x6) ,f283(x7) ,f284(x6 ,x7 ,x8 ,x10 ,x84 ,x85 ,x86 ,x87 ,x163 ,x164) ,f280(x6 ,x7 ,x8 ,x10 ,x84 ,x85 ,x86 ,x87 ,x163 ,x164)) + f278(x8) | | | +- f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f9(f277(),f279(x10),f281(),f282(x6),f283(x7),f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f280(x6 ,x7 ,x8 ,x10 ,x84 ,x85 ,x86 ,x87 ,x163 ,x164) = f9(f277(),f279(x10),f281(),f282(x6),f283(x7),f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f287(x163) = f287(x163) >= x163 = x163 | | | +- f288(x164) = f288(x164) >= x164 = x164 | | | +- f4(f277(),f279(x10),x163,f281()) = f4(f277(),f279(x10),x163,f281()) >= f287(x163) + 1 = f287(x163) + 1 | | | +- f5(f277(),f279(x10),x163,f281()) + x164 = f5(f277(),f279(x10),x163,f281()) + x164 >= f288(x164) = f288(x164) | | | +- f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f8(f277(),f279(x10),f281(),f282(x6),f283(x7)) + f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f8(f277(),f279(x10),f281(),f282(x6),f283(x7)) + f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f282(x6) = f282(x6) >= x6 = x6 | | | +- f283(x7) = f283(x7) >= x7 = x7 | | | +- f15(x10 + 1,x6) = f15(x10 + 1,x6) >= f6(f277(),f279(x10),f281(),f282(x6)) = f6(f277(),f279(x10),f281(),f282(x6)) | | | +- f16(x10 + 1,x6) + x7 = f16(x10 + 1,x6) + x7 >= f7(f277(),f279(x10),f281(),f282(x6)) + f283(x7) = f7(f277(),f279(x10),f281(),f282(x6)) + f283(x7) | | | +- f17(x10 + 1,x6,x7) + x8 = f17(x10 + 1,x6,x7) + x8 >= f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) + 1 = f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) + 1 | | | +- f290(x15) = f290(x15) >= x15 = x15 | | | +- f291(x15) = f291(x15) >= f290(x15) = f290(x15) | | | +- f292(x13) = f292(x13) >= x13 = x13 | | | +- f293(x14) = f293(x14) >= x14 = x14 | | | +- f15(0,x13) = f15(0,x13) >= f11(f292(x13)) = f11(f292(x13)) | | | +- f16(0,x13) + x14 = f16(0,x13) + x14 >= f12(f292(x13)) + f293(x14) = f12(f292(x13)) + f293(x14) | | | +- f17(0,x13,x14) + x15 = f17(0,x13,x14) + x15 >= f291(x15) + 1 = f291(x15) + 1 | | | +- f294(x19) = f294(x19) >= x19 = x19 | | | +- f11(x18) = f11(x18) >= x18 = x18 | | | +- f12(x18) + x19 = f12(x18) + x19 >= f294(x19) + 1 = f294(x19) + 1 | | | +- f295(x22) = f295(x22) >= x22 = x22 | | | +- f296(x25) = f296(x25) >= x25 = x25 | | | +- f297(x24) = f297(x24) >= x24 = x24 | | | +- f298(x21,x22,x23,x24,x25) = f298(x21,x22,x23,x24,x25) >= f3(f295(x22),f299(x21,x22,x23,x24),x21,f300(x21,x22,x23,x24,x25)) + f296(x25) = f3(f295(x22) ,f299(x21,x22,x23,x24) ,x21 ,f300(x21,x22,x23,x24,x25)) + f296(x25) | | | +- f299(x21,x22,x23,x24) = f299(x21,x22,x23,x24) >= f4(x21,x22,f297(x24),x23) = f4(x21,x22,f297(x24),x23) | | | +- f300(x21,x22,x23,x24,x25) = f300(x21,x22,x23,x24,x25) >= f5(x21,x22,f297(x24),x23) + f298(x21,x22,x23,x24,x25) = f5(x21,x22,f297(x24),x23) + f298(x21,x22,x23,x24,x25) | | | +- f301(x21,x22,x23,x24,x25) = f301(x21,x22,x23,x24,x25) >= f2(f295(x22),f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) = f2(f295(x22),f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) | | | +- f6(x21,x22,x23,x24) = f6(x21,x22,x23,x24) >= f1(f295(x22),f299(x21,x22,x23,x24),x21) = f1(f295(x22),f299(x21,x22,x23,x24),x21) | | | `- f7(x21,x22,x23,x24) + x25 = f7(x21,x22,x23,x24) + x25 >= f301(x21,x22,x23,x24,x25) + 1 = f301(x21,x22,x23,x24,x25) + 1 | +- Open Constraints | | | +- f264(x3) = f264(x3) >= x3 = x3 | | | +- f265(x2) = f265(x2) >= x2 = x2 | | | +- f266(x3) = f266(x3) >= f264(x3) = f264(x3) | | | +- f267(x2,x3) = f267(x2,x3) >= f17(f265(x2),f268(),f269(x2,x3)) + f266(x3) = f17(f265(x2),f268(),f269(x2,x3)) + f266(x3) | | | +- f268() = f268() >= 0 = 0 | | | +- f269(x2,x3) = f269(x2,x3) >= f267(x2,x3) = f267(x2,x3) | | | +- f270(x2,x3) = f270(x2,x3) >= f16(f265(x2),f268()) + f269(x2,x3) = f16(f265(x2),f268()) + f269(x2,x3) | | | +- f13(x2) = f13(x2) >= f15(f265(x2),f268()) = f15(f265(x2),f268()) | | | +- f14(x2) + x3 = f14(x2) + x3 >= f270(x2,x3) + 1 = f270(x2,x3) + 1 | | | +- f271(x8) = f271(x8) >= x8 = x8 | | | +- f272(x8) = f272(x8) >= f271(x8) = f271(x8) | | | +- f273(x84) = f273(x84) >= x84 = x84 | | | +- f274(x87) = f274(x87) >= x87 = x87 | | | +- f275(x85) = f275(x85) >= x85 = x85 | | | +- f276(x86) = f276(x86) >= x86 = x86 | | | +- f1(x84,x85,f277()) = f1(x84,x85,f277()) >= f15(f273(x84),f275(x85)) = f15(f273(x84),f275(x85)) | | | +- f2(x84,x85,f277()) + x86 = f2(x84,x85,f277()) + x86 >= f16(f273(x84),f275(x85)) + f276(x86) = f16(f273(x84),f275(x85)) + f276(x86) | | | +- f3(x84,x85,f277(),x86) + x87 = f3(x84,x85,f277(),x86) + x87 >= f17(f273(x84),f275(x85),f276(x86)) + f274(x87) = f17(f273(x84),f275(x85),f276(x86)) + f274(x87) | | | +- f278(x8) = f278(x8) >= f272(x8) = f272(x8) | | | +- f279(x10) = f279(x10) >= x10 = x10 | | | +- f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f10(f277() ,f279(x10) ,f281() ,f282(x6) ,f283(x7) ,f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) ,f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f278(x8) = f10(f277() ,f279(x10) ,f281() ,f282(x6) ,f283(x7) ,f284(x6 ,x7 ,x8 ,x10 ,x84 ,x85 ,x86 ,x87 ,x163 ,x164) ,f280(x6 ,x7 ,x8 ,x10 ,x84 ,x85 ,x86 ,x87 ,x163 ,x164)) + f278(x8) | | | +- f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f9(f277(),f279(x10),f281(),f282(x6),f283(x7),f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f280(x6 ,x7 ,x8 ,x10 ,x84 ,x85 ,x86 ,x87 ,x163 ,x164) = f9(f277(),f279(x10),f281(),f282(x6),f283(x7),f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f287(x163) = f287(x163) >= x163 = x163 | | | +- f288(x164) = f288(x164) >= x164 = x164 | | | +- f4(f277(),f279(x10),x163,f281()) = f4(f277(),f279(x10),x163,f281()) >= f287(x163) + 1 = f287(x163) + 1 | | | +- f5(f277(),f279(x10),x163,f281()) + x164 = f5(f277(),f279(x10),x163,f281()) + x164 >= f288(x164) = f288(x164) | | | +- f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) >= f8(f277(),f279(x10),f281(),f282(x6),f283(x7)) + f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = f8(f277(),f279(x10),f281(),f282(x6),f283(x7)) + f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f282(x6) = f282(x6) >= x6 = x6 | | | +- f283(x7) = f283(x7) >= x7 = x7 | | | +- f15(x10 + 1,x6) = f15(x10 + 1,x6) >= f6(f277(),f279(x10),f281(),f282(x6)) = f6(f277(),f279(x10),f281(),f282(x6)) | | | +- f16(x10 + 1,x6) + x7 = f16(x10 + 1,x6) + x7 >= f7(f277(),f279(x10),f281(),f282(x6)) + f283(x7) = f7(f277(),f279(x10),f281(),f282(x6)) + f283(x7) | | | +- f17(x10 + 1,x6,x7) + x8 = f17(x10 + 1,x6,x7) + x8 >= f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) + 1 = f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) + 1 | | | +- f290(x15) = f290(x15) >= x15 = x15 | | | +- f291(x15) = f291(x15) >= f290(x15) = f290(x15) | | | +- f292(x13) = f292(x13) >= x13 = x13 | | | +- f293(x14) = f293(x14) >= x14 = x14 | | | +- f15(0,x13) = f15(0,x13) >= f11(f292(x13)) = f11(f292(x13)) | | | +- f16(0,x13) + x14 = f16(0,x13) + x14 >= f12(f292(x13)) + f293(x14) = f12(f292(x13)) + f293(x14) | | | +- f17(0,x13,x14) + x15 = f17(0,x13,x14) + x15 >= f291(x15) + 1 = f291(x15) + 1 | | | +- f294(x19) = f294(x19) >= x19 = x19 | | | +- f11(x18) = f11(x18) >= x18 = x18 | | | +- f12(x18) + x19 = f12(x18) + x19 >= f294(x19) + 1 = f294(x19) + 1 | | | +- f295(x22) = f295(x22) >= x22 = x22 | | | +- f296(x25) = f296(x25) >= x25 = x25 | | | +- f297(x24) = f297(x24) >= x24 = x24 | | | +- f298(x21,x22,x23,x24,x25) = f298(x21,x22,x23,x24,x25) >= f3(f295(x22),f299(x21,x22,x23,x24),x21,f300(x21,x22,x23,x24,x25)) + f296(x25) = f3(f295(x22) ,f299(x21,x22,x23,x24) ,x21 ,f300(x21,x22,x23,x24,x25)) + f296(x25) | | | +- f299(x21,x22,x23,x24) = f299(x21,x22,x23,x24) >= f4(x21,x22,f297(x24),x23) = f4(x21,x22,f297(x24),x23) | | | +- f300(x21,x22,x23,x24,x25) = f300(x21,x22,x23,x24,x25) >= f5(x21,x22,f297(x24),x23) + f298(x21,x22,x23,x24,x25) = f5(x21,x22,f297(x24),x23) + f298(x21,x22,x23,x24,x25) | | | +- f301(x21,x22,x23,x24,x25) = f301(x21,x22,x23,x24,x25) >= f2(f295(x22),f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) = f2(f295(x22),f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) | | | +- f6(x21,x22,x23,x24) = f6(x21,x22,x23,x24) >= f1(f295(x22),f299(x21,x22,x23,x24),x21) = f1(f295(x22),f299(x21,x22,x23,x24),x21) | | | `- f7(x21,x22,x23,x24) + x25 = f7(x21,x22,x23,x24) + x25 >= f301(x21,x22,x23,x24,x25) + 1 = f301(x21,x22,x23,x24,x25) + 1 | +- Simplification ... | | | +- Substituted: f4(f277(),f279(x10),x163,f281()) ≥ f287(x163) + 1 ↦ f4(f277(),f279(0),x163,f281()) ≥ f287(x163) + 1 | | | +- Substituted: f5(f277(),f279(x10),x163,f281()) + x164 ≥ f288(x164) ↦ f5(f277(),f279(0),0,f281()) + x164 ≥ f288(x164) | | | +- Substituted: f17(0,x13,x14) + x15 ≥ f291(x15) + 1 ↦ f17(0,0,0) + x15 ≥ f291(x15) + 1 | | | +- Substituted: f12(x18) + x19 ≥ f294(x19) + 1 ↦ f12(0) + x19 ≥ f294(x19) + 1 | | | +- Eliminated: f10/7 | | | +- Eliminated: f8/5 | | | +- Eliminated: f9/6 | | | +- Propagated: f11(x0) ↦ x0 | | | +- Propagated: f264(x0) ↦ x0 | | | +- Propagated: f265(x0) ↦ x0 | | | +- Propagated: f268() ↦ 0 | | | +- Propagated: f271(x0) ↦ x0 | | | +- Propagated: f273(x0) ↦ x0 | | | +- Propagated: f274(x0) ↦ x0 | | | +- Propagated: f275(x0) ↦ x0 | | | +- Propagated: f276(x0) ↦ x0 | | | +- Propagated: f282(x0) ↦ x0 | | | +- Propagated: f283(x0) ↦ x0 | | | +- Propagated: f287(x0) ↦ x0 | | | +- Propagated: f288(x0) ↦ x0 | | | +- Propagated: f290(x0) ↦ x0 | | | +- Propagated: f292(x0) ↦ x0 | | | +- Propagated: f293(x0) ↦ x0 | | | +- Propagated: f294(x0) ↦ x0 | | | +- Propagated: f295(x0) ↦ x0 | | | +- Propagated: f296(x0) ↦ x0 | | | +- Propagated: f297(x0) ↦ x0 | | | +- Propagated: f266(x0) ↦ x0 | | | +- Propagated: f272(x0) ↦ x0 | | | +- Propagated: f291(x0) ↦ x0 | | | +- Propagated: f278(x0) ↦ x0 | | | +- Propagated: f280(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ↦ x2 | | | +- Propagated: f285(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ↦ x2 | | | +- Propagated: f286(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ↦ x2 | | | +- Propagated: f284(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ↦ x2 | | | `- Propagated: f289(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) ↦ x2 | +- Interpretation | | | +- f10(x0,x1,x2,x3,x4,x5,x6) = 0 | | | +- f11(x0) = x0 | | | +- f264(x0) = x0 | | | +- f265(x0) = x0 | | | +- f266(x0) = x0 | | | +- f268() = 0 | | | +- f271(x0) = x0 | | | +- f272(x0) = x0 | | | +- f273(x0) = x0 | | | +- f274(x0) = x0 | | | +- f275(x0) = x0 | | | +- f276(x0) = x0 | | | +- f278(x0) = x0 | | | +- f280(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f282(x0) = x0 | | | +- f283(x0) = x0 | | | +- f284(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f285(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f286(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f287(x0) = x0 | | | +- f288(x0) = x0 | | | +- f289(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f290(x0) = x0 | | | +- f291(x0) = x0 | | | +- f292(x0) = x0 | | | +- f293(x0) = x0 | | | +- f294(x0) = x0 | | | +- f295(x0) = x0 | | | +- f296(x0) = x0 | | | +- f297(x0) = x0 | | | +- f8(x0,x1,x2,x3,x4) = 0 | | | `- f9(x0,x1,x2,x3,x4,x5) = 0 | +- Constraints | | | +- f264(x3) = x3 >= x3 = x3 | | | +- f265(x2) = x2 >= x2 = x2 | | | +- f266(x3) = x3 >= x3 = f264(x3) | | | +- f267(x2,x3) = f267(x2,x3) >= f17(x2,0,f269(x2,x3)) + x3 = f17(f265(x2),f268(),f269(x2,x3)) + f266(x3) | | | +- f268() = 0 >= 0 = 0 | | | +- f269(x2,x3) = f269(x2,x3) >= f267(x2,x3) = f267(x2,x3) | | | +- f270(x2,x3) = f270(x2,x3) >= f16(x2,0) + f269(x2,x3) = f16(f265(x2),f268()) + f269(x2,x3) | | | +- f13(x2) = f13(x2) >= f15(x2,0) = f15(f265(x2),f268()) | | | +- f14(x2) + x3 = f14(x2) + x3 >= f270(x2,x3) + 1 = f270(x2,x3) + 1 | | | +- f271(x8) = x8 >= x8 = x8 | | | +- f272(x8) = x8 >= x8 = f271(x8) | | | +- f273(x84) = x84 >= x84 = x84 | | | +- f274(x87) = x87 >= x87 = x87 | | | +- f275(x85) = x85 >= x85 = x85 | | | +- f276(x86) = x86 >= x86 = x86 | | | +- f1(x84,x85,f277()) = f1(x84,x85,f277()) >= f15(x84,x85) = f15(f273(x84),f275(x85)) | | | +- f2(x84,x85,f277()) + x86 = f2(x84,x85,f277()) + x86 >= f16(x84,x85) + x86 = f16(f273(x84),f275(x85)) + f276(x86) | | | +- f3(x84,x85,f277(),x86) + x87 = f3(x84,x85,f277(),x86) + x87 >= f17(x84,x85,x86) + x87 = f17(f273(x84),f275(x85),f276(x86)) + f274(x87) | | | +- f278(x8) = x8 >= x8 = f272(x8) | | | +- f279(x10) = f279(x10) >= x10 = x10 | | | +- f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f10(f277(),f279(x10),f281(),f282(x6),f283(x7),f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164),f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f278(x8) | | | +- f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f9(f277(),f279(x10),f281(),f282(x6),f283(x7),f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f287(x163) = x163 >= x163 = x163 | | | +- f288(x164) = x164 >= x164 = x164 | | | +- f4(f277(),f279(x10),x163,f281()) = f4(f277(),f279(x10),x163,f281()) >= x163 + 1 = f287(x163) + 1 | | | +- f5(f277(),f279(x10),x163,f281()) + x164 = f5(f277(),f279(x10),x163,f281()) + x164 >= x164 = f288(x164) | | | +- f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f8(f277(),f279(x10),f281(),f282(x6),f283(x7)) + f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f282(x6) = x6 >= x6 = x6 | | | +- f283(x7) = x7 >= x7 = x7 | | | +- f15(x10 + 1,x6) = f15(x10 + 1,x6) >= f6(f277(),f279(x10),f281(),x6) = f6(f277(),f279(x10),f281(),f282(x6)) | | | +- f16(x10 + 1,x6) + x7 = f16(x10 + 1,x6) + x7 >= f7(f277(),f279(x10),f281(),x6) + x7 = f7(f277(),f279(x10),f281(),f282(x6)) + f283(x7) | | | +- f17(x10 + 1,x6,x7) + x8 = f17(x10 + 1,x6,x7) + x8 >= x8 + 1 = f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) + 1 | | | +- f290(x15) = x15 >= x15 = x15 | | | +- f291(x15) = x15 >= x15 = f290(x15) | | | +- f292(x13) = x13 >= x13 = x13 | | | +- f293(x14) = x14 >= x14 = x14 | | | +- f15(0,x13) = f15(0,x13) >= x13 = f11(f292(x13)) | | | +- f16(0,x13) + x14 = f16(0,x13) + x14 >= f12(x13) + x14 = f12(f292(x13)) + f293(x14) | | | +- f17(0,x13,x14) + x15 = f17(0,x13,x14) + x15 >= x15 + 1 = f291(x15) + 1 | | | +- f294(x19) = x19 >= x19 = x19 | | | +- f11(x18) = x18 >= x18 = x18 | | | +- f12(x18) + x19 = f12(x18) + x19 >= x19 + 1 = f294(x19) + 1 | | | +- f295(x22) = x22 >= x22 = x22 | | | +- f296(x25) = x25 >= x25 = x25 | | | +- f297(x24) = x24 >= x24 = x24 | | | +- f298(x21,x22,x23,x24,x25) = f298(x21,x22,x23,x24,x25) >= f3(x22,f299(x21,x22,x23,x24),x21,f300(x21,x22,x23,x24,x25)) + x25 = f3(f295(x22),f299(x21,x22,x23,x24),x21,f300(x21,x22,x23,x24,x25)) + f296(x25) | | | +- f299(x21,x22,x23,x24) = f299(x21,x22,x23,x24) >= f4(x21,x22,x24,x23) = f4(x21,x22,f297(x24),x23) | | | +- f300(x21,x22,x23,x24,x25) = f300(x21,x22,x23,x24,x25) >= f5(x21,x22,x24,x23) + f298(x21,x22,x23,x24,x25) = f5(x21,x22,f297(x24),x23) + f298(x21,x22,x23,x24,x25) | | | +- f301(x21,x22,x23,x24,x25) = f301(x21,x22,x23,x24,x25) >= f2(x22,f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) = f2(f295(x22),f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) | | | +- f6(x21,x22,x23,x24) = f6(x21,x22,x23,x24) >= f1(x22,f299(x21,x22,x23,x24),x21) = f1(f295(x22),f299(x21,x22,x23,x24),x21) | | | `- f7(x21,x22,x23,x24) + x25 = f7(x21,x22,x23,x24) + x25 >= f301(x21,x22,x23,x24,x25) + 1 = f301(x21,x22,x23,x24,x25) + 1 | +- SCC-DECOMPOSE ... | | | +- SCC: 7 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:43.258406 UTC | | | +- Open Constraints | | | | | `- f12(0) + x19 = f12(0) + x19 >= x19 + 1 = x19 + 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:43.258441 UTC | | | | | +- Interpretation | | | | | | | `- f12(x0) = 16 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f12(x0) = 1 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:43.263664 UTC(+0.005223s) | | | +- Interpretation | | | | | `- f12(x0) = 1 | | | +- Constraints | | | | | `- f12(0) + x19 = 1 + x19 >= x19 + 1 = x19 + 1 | | | `- Stopping timer: 2017-03-30 07:29:43.263702 UTC(+0.005296s) | +- SCC-DECOMPOSE ... | | | +- SCC: 6 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:43.264388 UTC | | | +- Open Constraints | | | | | +- f17(x10 + 1,x6,x7) + x8 = f17(x10 + 1,x6,x7) + x8 >= x8 + 1 = x8 + 1 | | | | | `- f17(0,0,0) + x15 = f17(0,0,0) + x15 >= x15 + 1 = x15 + 1 | | | +- Simplification ... | | | | | `- Substituted: f17(x10 + 1,x6,x7) + x8 ≥ x8 + 1 ↦ f17(1,0,0) + x8 ≥ x8 + 1 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:43.264437 UTC | | | | | +- Interpretation | | | | | | | `- f17(x0,x1,x2) = max(7 + x0 + x1,x2) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | `- f17(x0,x1,x2) = 1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:43.2746 UTC(+0.010163s) | | | +- Interpretation | | | | | `- f17(x0,x1,x2) = 1 | | | +- Constraints | | | | | +- f17(x10 + 1,x6,x7) + x8 = 1 + x8 >= x8 + 1 = x8 + 1 | | | | | `- f17(0,0,0) + x15 = 1 + x15 >= x15 + 1 = x15 + 1 | | | `- Stopping timer: 2017-03-30 07:29:43.274652 UTC(+0.010264s) | +- SCC-DECOMPOSE ... | | | +- SCC: 5 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:43.27526 UTC | | | +- Open Constraints | | | | | +- f3(x84,x85,f277(),x86) + x87 = f3(x84,x85,f277(),x86) + x87 >= 1 + x87 = f17(x84,x85,x86) + x87 | | | | | +- f2(x84,x85,f277()) + x86 = f2(x84,x85,f277()) + x86 >= f16(x84,x85) + x86 = f16(x84,x85) + x86 | | | | | +- f5(f277(),f279(0),0,f281()) + x164 = f5(f277(),f279(0),0,f281()) + x164 >= x164 = x164 | | | | | +- f1(x84,x85,f277()) = f1(x84,x85,f277()) >= f15(x84,x85) = f15(x84,x85) | | | | | +- f15(x10 + 1,x6) = f15(x10 + 1,x6) >= f6(f277(),f279(x10),f281(),x6) = f6(f277(),f279(x10),f281(),x6) | | | | | +- f15(0,x13) = f15(0,x13) >= x13 = x13 | | | | | +- f279(x10) = f279(x10) >= x10 = x10 | | | | | +- f4(f277(),f279(0),x163,f281()) = f4(f277(),f279(0),x163,f281()) >= x163 + 1 = x163 + 1 | | | | | +- f6(x21,x22,x23,x24) = f6(x21,x22,x23,x24) >= f1(x22,f299(x21,x22,x23,x24),x21) = f1(x22,f299(x21,x22,x23,x24),x21) | | | | | +- f299(x21,x22,x23,x24) = f299(x21,x22,x23,x24) >= f4(x21,x22,x24,x23) = f4(x21,x22,x24,x23) | | | | | +- f16(x10 + 1,x6) + x7 = f16(x10 + 1,x6) + x7 >= f7(f277(),f279(x10),f281(),x6) + x7 = f7(f277(),f279(x10),f281(),x6) + x7 | | | | | +- f16(0,x13) + x14 = f16(0,x13) + x14 >= 1 + x14 = f12(x13) + x14 | | | | | +- f7(x21,x22,x23,x24) + x25 = f7(x21,x22,x23,x24) + x25 >= f301(x21,x22,x23,x24,x25) + 1 = f301(x21,x22,x23,x24,x25) + 1 | | | | | +- f301(x21,x22,x23,x24,x25) = f301(x21,x22,x23,x24,x25) >= f2(x22,f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) = f2(x22,f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) | | | | | +- f300(x21,x22,x23,x24,x25) = f300(x21,x22,x23,x24,x25) >= f5(x21,x22,x24,x23) + f298(x21,x22,x23,x24,x25) = f5(x21,x22,x24,x23) + f298(x21,x22,x23,x24,x25) | | | | | `- f298(x21,x22,x23,x24,x25) = f298(x21,x22,x23,x24,x25) >= f3(x22,f299(x21,x22,x23,x24),x21,f300(x21,x22,x23,x24,x25)) + x25 = f3(x22,f299(x21,x22,x23,x24),x21,f300(x21,x22,x23,x24,x25)) + x25 | | | +- Simplification ... | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:29:43.476081 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:43.536858 UTC(+0.060777s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:29:43.536867 UTC | | | | | +- Interpretation | | | | | | | +- f1(x0,x1,x2) = 1 + 11*x0 + x1 + 4*x2 | | | | | | | +- f15(x0,x1) = 13 + 11*x0 + x1 | | | | | | | +- f16(x0,x1) = 11 + 10*x0 + 4*x1 | | | | | | | +- f2(x0,x1,x2) = 2 + 10*x0 + 4*x1 + 3*x2 | | | | | | | +- f277() = 3 | | | | | | | +- f279(x0) = x0 | | | | | | | +- f281() = 2 | | | | | | | +- f298(x0,x1,x2,x3,x4) = 1 + x4 | | | | | | | +- f299(x0,x1,x2,x3) = 2 + x3 | | | | | | | +- f3(x0,x1,x2,x3) = 1 | | | | | | | +- f300(x0,x1,x2,x3,x4) = 1 + x4 | | | | | | | +- f301(x0,x1,x2,x3,x4) = 11 + 3*x0 + 10*x1 + 4*x3 + x4 | | | | | | | +- f4(x0,x1,x2,x3) = 2 + x2 | | | | | | | +- f5(x0,x1,x2,x3) = 0 | | | | | | | +- f6(x0,x1,x2,x3) = 8 + 4*x0 + 11*x1 + 2*x2 + x3 | | | | | | | `- f7(x0,x1,x2,x3) = 12 + 3*x0 + 10*x1 + 4*x3 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f1(x0,x1,x2) = 2*x0 + x1 | | | | | | | +- f15(x0,x1) = 2*x0 + x1 | | | | | | | +- f16(x0,x1) = 1 + 3*x0 | | | | | | | +- f2(x0,x1,x2) = 1 + 3*x0 | | | | | | | +- f277() = 1 | | | | | | | +- f279(x0) = x0 | | | | | | | +- f281() = 0 | | | | | | | +- f298(x0,x1,x2,x3,x4) = 1 + x4 | | | | | | | +- f299(x0,x1,x2,x3) = 1 + x3 | | | | | | | +- f3(x0,x1,x2,x3) = 1 | | | | | | | +- f300(x0,x1,x2,x3,x4) = 1 + x4 | | | | | | | +- f301(x0,x1,x2,x3,x4) = 2 + x0 + 3*x1 + x4 | | | | | | | +- f4(x0,x1,x2,x3) = 1 + x2 | | | | | | | +- f5(x0,x1,x2,x3) = 0 | | | | | | | +- f6(x0,x1,x2,x3) = 1 + x0 + 2*x1 + x2 + x3 | | | | | | | `- f7(x0,x1,x2,x3) = 3 + x0 + 3*x1 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f1(x0,x1,x2) = x0 + x1 | | | | | | | +- f15(x0,x1) = x0 + x1 | | | | | | | +- f16(x0,x1) = 1 + 2*x0 | | | | | | | +- f2(x0,x1,x2) = 1 + 2*x0 | | | | | | | +- f277() = 1 | | | | | | | +- f279(x0) = x0 | | | | | | | +- f281() = 0 | | | | | | | +- f298(x0,x1,x2,x3,x4) = 1 + x4 | | | | | | | +- f299(x0,x1,x2,x3) = 1 + x3 | | | | | | | +- f3(x0,x1,x2,x3) = 1 | | | | | | | +- f300(x0,x1,x2,x3,x4) = 1 + x4 | | | | | | | +- f301(x0,x1,x2,x3,x4) = 2 + 2*x1 + x4 | | | | | | | +- f4(x0,x1,x2,x3) = 1 + x2 | | | | | | | +- f5(x0,x1,x2,x3) = 0 | | | | | | | +- f6(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | | | `- f7(x0,x1,x2,x3) = 3 + 2*x1 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f1(x0,x1,x2) = x0 + x1 | | | | | | | +- f15(x0,x1) = x0 + x1 | | | | | | | +- f16(x0,x1) = 1 + 2*x0 | | | | | | | +- f2(x0,x1,x2) = 1 + 2*x0 | | | | | | | +- f277() = 0 | | | | | | | +- f279(x0) = x0 | | | | | | | +- f281() = 0 | | | | | | | +- f298(x0,x1,x2,x3,x4) = 1 + x4 | | | | | | | +- f299(x0,x1,x2,x3) = 1 + x3 | | | | | | | +- f3(x0,x1,x2,x3) = 1 | | | | | | | +- f300(x0,x1,x2,x3,x4) = 1 + x4 | | | | | | | +- f301(x0,x1,x2,x3,x4) = 2 + 2*x1 + x4 | | | | | | | +- f4(x0,x1,x2,x3) = 1 + x2 | | | | | | | +- f5(x0,x1,x2,x3) = 0 | | | | | | | +- f6(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | | | `- f7(x0,x1,x2,x3) = 3 + 2*x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:43.710949 UTC(+0.174082s) | | | +- Interpretation | | | | | +- f1(x0,x1,x2) = x0 + x1 | | | | | +- f12(x0) = 1 | | | | | +- f15(x0,x1) = x0 + x1 | | | | | +- f16(x0,x1) = 1 + 2*x0 | | | | | +- f17(x0,x1,x2) = 1 | | | | | +- f2(x0,x1,x2) = 1 + 2*x0 | | | | | +- f277() = 0 | | | | | +- f279(x0) = x0 | | | | | +- f281() = 0 | | | | | +- f298(x0,x1,x2,x3,x4) = 1 + x4 | | | | | +- f299(x0,x1,x2,x3) = 1 + x3 | | | | | +- f3(x0,x1,x2,x3) = 1 | | | | | +- f300(x0,x1,x2,x3,x4) = 1 + x4 | | | | | +- f301(x0,x1,x2,x3,x4) = 2 + 2*x1 + x4 | | | | | +- f4(x0,x1,x2,x3) = 1 + x2 | | | | | +- f5(x0,x1,x2,x3) = 0 | | | | | +- f6(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f7(x0,x1,x2,x3) = 3 + 2*x1 | | | +- Constraints | | | | | +- f3(x84,x85,f277(),x86) + x87 = 1 + x87 >= 1 + x87 = f17(x84,x85,x86) + x87 | | | | | +- f2(x84,x85,f277()) + x86 = (1 + (2 * x84)) + x86 >= (1 + (2 * x84)) + x86 = f16(x84,x85) + x86 | | | | | +- f5(f277(),f279(0),0,f281()) + x164 = x164 >= x164 = x164 | | | | | +- f1(x84,x85,f277()) = x84 + x85 >= x84 + x85 = f15(x84,x85) | | | | | +- f15(x10 + 1,x6) = (x10 + 1) + x6 >= 1 + (x10 + x6) = f6(f277(),f279(x10),f281(),x6) | | | | | +- f15(0,x13) = x13 >= x13 = x13 | | | | | +- f279(x10) = x10 >= x10 = x10 | | | | | +- f4(f277(),f279(0),x163,f281()) = 1 + x163 >= x163 + 1 = x163 + 1 | | | | | +- f6(x21,x22,x23,x24) = 1 + (x22 + x24) >= x22 + (1 + x24) = f1(x22,f299(x21,x22,x23,x24),x21) | | | | | +- f299(x21,x22,x23,x24) = 1 + x24 >= 1 + x24 = f4(x21,x22,x24,x23) | | | | | +- f16(x10 + 1,x6) + x7 = (1 + (2 * (x10 + 1))) + x7 >= (3 + (2 * x10)) + x7 = f7(f277(),f279(x10),f281(),x6) + x7 | | | | | +- f16(0,x13) + x14 = 1 + x14 >= 1 + x14 = f12(x13) + x14 | | | | | +- f7(x21,x22,x23,x24) + x25 = (3 + (2 * x22)) + x25 >= (2 + ((2 * x22) + x25)) + 1 = f301(x21,x22,x23,x24,x25) + 1 | | | | | +- f301(x21,x22,x23,x24,x25) = 2 + ((2 * x22) + x25) >= (1 + (2 * x22)) + (1 + x25) = f2(x22,f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) | | | | | +- f300(x21,x22,x23,x24,x25) = 1 + x25 >= 1 + x25 = f5(x21,x22,x24,x23) + f298(x21,x22,x23,x24,x25) | | | | | `- f298(x21,x22,x23,x24,x25) = 1 + x25 >= 1 + x25 = f3(x22,f299(x21,x22,x23,x24),x21,f300(x21,x22,x23,x24,x25)) + x25 | | | `- Stopping timer: 2017-03-30 07:29:43.711131 UTC(+0.435871s) | +- SCC-DECOMPOSE ... | | | +- SCC: 4 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:43.711177 UTC | | | +- Open Constraints | | | | | +- f267(x2,x3) = f267(x2,x3) >= 1 + x3 = f17(x2,0,f269(x2,x3)) + x3 | | | | | `- f269(x2,x3) = f269(x2,x3) >= f267(x2,x3) = f267(x2,x3) | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:43.711259 UTC | | | | | +- Interpretation | | | | | | | +- f267(x0,x1) = 10 + x1 | | | | | | | `- f269(x0,x1) = max(15,14 + x1) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f267(x0,x1) = 1 + x1 | | | | | | | `- f269(x0,x1) = 1 + x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:43.723856 UTC(+0.012597s) | | | +- Interpretation | | | | | +- f17(x0,x1,x2) = 1 | | | | | +- f267(x0,x1) = 1 + x1 | | | | | `- f269(x0,x1) = 1 + x1 | | | +- Constraints | | | | | +- f267(x2,x3) = 1 + x3 >= 1 + x3 = f17(x2,0,f269(x2,x3)) + x3 | | | | | `- f269(x2,x3) = 1 + x3 >= 1 + x3 = f267(x2,x3) | | | `- Stopping timer: 2017-03-30 07:29:43.723914 UTC(+0.012737s) | +- SCC-DECOMPOSE ... | | | +- SCC: 3 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:43.723941 UTC | | | +- Open Constraints | | | | | `- f13(x2) = f13(x2) >= x2 = f15(x2,0) | | | +- Simplification ... | | | | | `- Propagated: f13(x0) ↦ x0 | | | +- Interpretation | | | | | +- f13(x0) = x0 | | | | | `- f15(x0,x1) = x0 + x1 | | | +- Constraints | | | | | `- f13(x2) = x2 >= x2 = f15(x2,0) | | | `- Stopping timer: 2017-03-30 07:29:43.724014 UTC(+0.000073s) | +- SCC-DECOMPOSE ... | | | +- SCC: 2 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:43.724025 UTC | | | +- Open Constraints | | | | | `- f270(x2,x3) = f270(x2,x3) >= (1 + (2 * x2)) + (1 + x3) = f16(x2,0) + f269(x2,x3) | | | +- Simplification ... | | | | | `- Propagated: f270(x0,x1) ↦ 2 + 2*x0 + x1 | | | +- Interpretation | | | | | +- f16(x0,x1) = 1 + 2*x0 | | | | | +- f269(x0,x1) = 1 + x1 | | | | | `- f270(x0,x1) = 2 + 2*x0 + x1 | | | +- Constraints | | | | | `- f270(x2,x3) = (1 + (2 * x2)) + (1 + x3) >= (1 + (2 * x2)) + (1 + x3) = f16(x2,0) + f269(x2,x3) | | | `- Stopping timer: 2017-03-30 07:29:43.724081 UTC(+0.000056s) | +- SCC-DECOMPOSE ... | | | +- SCC: 1 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:43.724089 UTC | | | +- Open Constraints | | | | | `- f14(x2) + x3 = f14(x2) + x3 >= ((1 + (2 * x2)) + (1 + x3)) + 1 = f270(x2,x3) + 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:43.724127 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:43.727942 UTC(+0.003815s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:29:43.727956 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:43.731679 UTC(+0.003723s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:29:43.731686 UTC | | | | | +- Interpretation | | | | | | | `- f14(x0) = 11 + 10*x0 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f14(x0) = 3 + 2*x0 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:43.736794 UTC(+0.005108s) | | | +- Interpretation | | | | | +- f14(x0) = 3 + 2*x0 | | | | | `- f270(x0,x1) = 2 + 2*x0 + x1 | | | +- Constraints | | | | | `- f14(x2) + x3 = (3 + (2 * x2)) + x3 >= ((1 + (2 * x2)) + (1 + x3)) + 1 = f270(x2,x3) + 1 | | | `- Stopping timer: 2017-03-30 07:29:43.736837 UTC(+0.012748s) | +- Interpretation | | | +- f1(x0,x1,x2) = x0 + x1 | | | +- f10(x0,x1,x2,x3,x4,x5,x6) = 0 | | | +- f11(x0) = x0 | | | +- f12(x0) = 1 | | | +- f13(x0) = x0 | | | +- f14(x0) = 3 + 2*x0 | | | +- f15(x0,x1) = x0 + x1 | | | +- f16(x0,x1) = 1 + 2*x0 | | | +- f17(x0,x1,x2) = 1 | | | +- f2(x0,x1,x2) = 1 + 2*x0 | | | +- f264(x0) = x0 | | | +- f265(x0) = x0 | | | +- f266(x0) = x0 | | | +- f267(x0,x1) = 1 + x1 | | | +- f268() = 0 | | | +- f269(x0,x1) = 1 + x1 | | | +- f270(x0,x1) = 2 + 2*x0 + x1 | | | +- f271(x0) = x0 | | | +- f272(x0) = x0 | | | +- f273(x0) = x0 | | | +- f274(x0) = x0 | | | +- f275(x0) = x0 | | | +- f276(x0) = x0 | | | +- f277() = 0 | | | +- f278(x0) = x0 | | | +- f279(x0) = x0 | | | +- f280(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f281() = 0 | | | +- f282(x0) = x0 | | | +- f283(x0) = x0 | | | +- f284(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f285(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f286(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f287(x0) = x0 | | | +- f288(x0) = x0 | | | +- f289(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9) = x2 | | | +- f290(x0) = x0 | | | +- f291(x0) = x0 | | | +- f292(x0) = x0 | | | +- f293(x0) = x0 | | | +- f294(x0) = x0 | | | +- f295(x0) = x0 | | | +- f296(x0) = x0 | | | +- f297(x0) = x0 | | | +- f298(x0,x1,x2,x3,x4) = 1 + x4 | | | +- f299(x0,x1,x2,x3) = 1 + x3 | | | +- f3(x0,x1,x2,x3) = 1 | | | +- f300(x0,x1,x2,x3,x4) = 1 + x4 | | | +- f301(x0,x1,x2,x3,x4) = 2 + 2*x1 + x4 | | | +- f4(x0,x1,x2,x3) = 1 + x2 | | | +- f5(x0,x1,x2,x3) = 0 | | | +- f6(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f7(x0,x1,x2,x3) = 3 + 2*x1 | | | +- f8(x0,x1,x2,x3,x4) = 0 | | | `- f9(x0,x1,x2,x3,x4,x5) = 0 | +- Constraints | | | +- f264(x3) = x3 >= x3 = x3 | | | +- f265(x2) = x2 >= x2 = x2 | | | +- f266(x3) = x3 >= x3 = f264(x3) | | | +- f267(x2,x3) = 1 + x3 >= 1 + x3 = f17(f265(x2),f268(),f269(x2,x3)) + f266(x3) | | | +- f268() = 0 >= 0 = 0 | | | +- f269(x2,x3) = 1 + x3 >= 1 + x3 = f267(x2,x3) | | | +- f270(x2,x3) = (1 + (2 * x2)) + (1 + x3) >= (1 + (2 * x2)) + (1 + x3) = f16(f265(x2),f268()) + f269(x2,x3) | | | +- f13(x2) = x2 >= x2 = f15(f265(x2),f268()) | | | +- f14(x2) + x3 = (3 + (2 * x2)) + x3 >= ((1 + (2 * x2)) + (1 + x3)) + 1 = f270(x2,x3) + 1 | | | +- f271(x8) = x8 >= x8 = x8 | | | +- f272(x8) = x8 >= x8 = f271(x8) | | | +- f273(x84) = x84 >= x84 = x84 | | | +- f274(x87) = x87 >= x87 = x87 | | | +- f275(x85) = x85 >= x85 = x85 | | | +- f276(x86) = x86 >= x86 = x86 | | | +- f1(x84,x85,f277()) = x84 + x85 >= x84 + x85 = f15(f273(x84),f275(x85)) | | | +- f2(x84,x85,f277()) + x86 = (1 + (2 * x84)) + x86 >= (1 + (2 * x84)) + x86 = f16(f273(x84),f275(x85)) + f276(x86) | | | +- f3(x84,x85,f277(),x86) + x87 = 1 + x87 >= 1 + x87 = f17(f273(x84),f275(x85),f276(x86)) + f274(x87) | | | +- f278(x8) = x8 >= x8 = f272(x8) | | | +- f279(x10) = x10 >= x10 = x10 | | | +- f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f10(f277(),f279(x10),f281(),f282(x6),f283(x7),f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164),f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f278(x8) | | | +- f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f9(f277(),f279(x10),f281(),f282(x6),f283(x7),f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164)) + f280(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f285(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f287(x163) = x163 >= x163 = x163 | | | +- f288(x164) = x164 >= x164 = x164 | | | +- f4(f277(),f279(x10),x163,f281()) = 1 + x163 >= x163 + 1 = f287(x163) + 1 | | | +- f5(f277(),f279(x10),x163,f281()) + x164 = x164 >= x164 = f288(x164) | | | +- f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f286(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) = x8 >= x8 = f8(f277(),f279(x10),f281(),f282(x6),f283(x7)) + f284(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) | | | +- f282(x6) = x6 >= x6 = x6 | | | +- f283(x7) = x7 >= x7 = x7 | | | +- f15(x10 + 1,x6) = (x10 + 1) + x6 >= 1 + (x10 + x6) = f6(f277(),f279(x10),f281(),f282(x6)) | | | +- f16(x10 + 1,x6) + x7 = (1 + (2 * (x10 + 1))) + x7 >= (3 + (2 * x10)) + x7 = f7(f277(),f279(x10),f281(),f282(x6)) + f283(x7) | | | +- f17(x10 + 1,x6,x7) + x8 = 1 + x8 >= x8 + 1 = f289(x6,x7,x8,x10,x84,x85,x86,x87,x163,x164) + 1 | | | +- f290(x15) = x15 >= x15 = x15 | | | +- f291(x15) = x15 >= x15 = f290(x15) | | | +- f292(x13) = x13 >= x13 = x13 | | | +- f293(x14) = x14 >= x14 = x14 | | | +- f15(0,x13) = x13 >= x13 = f11(f292(x13)) | | | +- f16(0,x13) + x14 = 1 + x14 >= 1 + x14 = f12(f292(x13)) + f293(x14) | | | +- f17(0,x13,x14) + x15 = 1 + x15 >= x15 + 1 = f291(x15) + 1 | | | +- f294(x19) = x19 >= x19 = x19 | | | +- f11(x18) = x18 >= x18 = x18 | | | +- f12(x18) + x19 = 1 + x19 >= x19 + 1 = f294(x19) + 1 | | | +- f295(x22) = x22 >= x22 = x22 | | | +- f296(x25) = x25 >= x25 = x25 | | | +- f297(x24) = x24 >= x24 = x24 | | | +- f298(x21,x22,x23,x24,x25) = 1 + x25 >= 1 + x25 = f3(f295(x22),f299(x21,x22,x23,x24),x21,f300(x21,x22,x23,x24,x25)) + f296(x25) | | | +- f299(x21,x22,x23,x24) = 1 + x24 >= 1 + x24 = f4(x21,x22,f297(x24),x23) | | | +- f300(x21,x22,x23,x24,x25) = 1 + x25 >= 1 + x25 = f5(x21,x22,f297(x24),x23) + f298(x21,x22,x23,x24,x25) | | | +- f301(x21,x22,x23,x24,x25) = 2 + ((2 * x22) + x25) >= (1 + (2 * x22)) + (1 + x25) = f2(f295(x22),f299(x21,x22,x23,x24),x21) + f300(x21,x22,x23,x24,x25) | | | +- f6(x21,x22,x23,x24) = 1 + (x22 + x24) >= x22 + (1 + x24) = f1(f295(x22),f299(x21,x22,x23,x24),x21) | | | `- f7(x21,x22,x23,x24) + x25 = (3 + (2 * x22)) + x25 >= (2 + ((2 * x22) + x25)) + 1 = f301(x21,x22,x23,x24,x25) + 1 | `- Stopping timer: 2017-03-30 07:29:43.737071 UTC(+0.48207s)