SUCCESS(3) SUCCESS f1(x0,x1) = 0; f10(x0,x1,x2,x3,x4) = 0; f11(x0,x1,x2,x3,x4,x5) = 0; f12(x0,x1) = x0; f13(x0,x1) = x1; f14(x0,x1) = 2 + x0*x1^2 + 2*x1^2; f15(x0,x1,x2) = 0; f16(x0,x1,x2) = 1 + x0; f17(x0,x1,x2,x3) = 0; f18(x0,x1,x2) = x1; f19(x0,x1,x2) = x2; f2(x0,x1) = 1 + x0; f20(x0,x1,x2) = 1 + x1*x2^2 + 2*x2^2; f21(x0,x1,x2,x3) = 0; f3(x0,x1,x2) = 0; f4(x0,x1,x2) = 0; f5(x0,x1,x2) = 1 + x0; f6(x0,x1,x2,x3) = 0; f609(x0) = x0; f610(x0) = x0; f611(x0) = x0; f612(x0) = x0; f613(x0) = x0; f614(x0) = x0; f615() = 0; f616(x0) = x0; f617(x0) = x0; f618(x0) = x0; f619(x0,x1,x2,x3,x4,x5,x6) = x2; f620(x0,x1,x2,x3,x4,x5,x6) = 1 + x0*x1^2 + 2*x1^2 + x2; f621(x0) = x0; f622(x0) = x0; f623(x0) = x0; f624(x0) = x0; f625(x0,x1,x2) = x0; f626(x0,x1,x2) = 1 + x0 + x1; f627(x0) = x0; f628(x0) = x0; f629(x0) = x0; f630(x0) = x0; f631(x0) = x0; f632(x0) = x0; f633() = 0; f634(x0) = x0; f635(x0) = x0; f636(x0) = x0; f637(x0) = x0; f638(x0) = x0; f639(x0) = 0; f640(x0) = x0; f641(x0) = x0; f642(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2; f643(x0,x1,x2,x3,x4,x5,x6) = x1; f644(x0,x1,x2,x3,x4,x5,x6) = x2; f645(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 1 + x1*x3^2 + x2 + 2*x3^2; f646(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2; f647(x0) = x0; f648(x0) = x0; f649(x0) = x0; f650(x0) = x0; f651(x0) = 0; f652(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2; f653(x0) = x0; f654(x0) = x0; f655(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2; f656(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 2 + x1*x3 + x1*x3^2 + x2 + 2*x3 + 2*x3^2; f657(x0) = x0; f658(x0) = x0; f659(x0) = x0; f660(x0,x1,x2,x3) = x3; f661(x0,x1,x2,x3) = 1 + x1 + x3; f662(x0,x1) = max(x1,x0); f663(x0,x1,x2,x3) = 1 + x1 + x3; f664(x0,x1,x2,x3) = 1 + x1 + x3; f665(x0) = x0; f666(x0,x1,x2,x3) = 1 + x1 + x3; f667(x0) = x0; f668(x0,x1,x2,x3) = 1 + x1 + x3; f669(x0) = 1 + x0; f670(x0,x1,x2,x3) = 1 + x1 + x3; f671(x0,x1,x2,x3) = 1 + x1 + x3; f672(x0,x1,x2,x3,x4,x5,x6,x7) = max(x2,x1); f673(x0,x1,x2,x3,x4,x5,x6,x7) = 2 + x3; f674(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 3 + x1 + x1*x4 + x3 + 2*x4; f675(x0,x1,x2,x3) = 1 + x1 + x3; f676(x0,x1,x2,x3,x4,x5,x6,x7) = max(x1,x2); f677(x0,x1,x2,x3) = 1 + x1 + x3; f678(x0,x1,x2,x3) = 1 + x1 + x3; f679(x0) = x0; f680(x0) = x0; f681(x0) = x0; f682(x0) = x0; f683(x0) = 0; f684(x0,x1,x2,x3) = 1 + x1 + x3; f685(x0) = x0; f686(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3; f687(x0) = x0; f688(x0) = x0; f689(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3; f690(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x3; f691(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x1 + x1*x4 + x3 + 2*x4; f692(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x1 + x1*x4 + x3 + 2*x4; f693(x0) = x0; f694(x0) = x0; f695(x0) = x0; f696(x0) = x0; f697() = 0; f698() = 0; f699(x0) = x0; f7(x0,x1,x2,x3) = max(x2,x1); f700(x0) = x0; f8(x0,x1,x2,x3) = 1 + x3; f9(x0,x1,x2,x3) = 1 + x1*x3 + 2*x3; ExecutionLog | +- Staring timer: 2017-03-30 07:35:56.109808 UTC | +- Open Constraints | | | +- f609(x3) = f609(x3) >= x3 = x3 | | | +- f610(x3) = f610(x3) >= f609(x3) = f609(x3) | | | +- f611(x86) = f611(x86) >= x86 = x86 | | | +- f612(x89) = f612(x89) >= x89 = x89 | | | +- f613(x87) = f613(x87) >= x87 = x87 | | | +- f614(x88) = f614(x88) >= x88 = x88 | | | +- f15(x86,x87,f615()) = f15(x86,x87,f615()) >= f1(f611(x86),f613(x87)) = f1(f611(x86),f613(x87)) | | | +- f16(x86,x87,f615()) + x88 = f16(x86,x87,f615()) + x88 >= f2(f611(x86),f613(x87)) + f614(x88) = f2(f611(x86),f613(x87)) + f614(x88) | | | +- f17(x86,x87,f615(),x88) + x89 = f17(x86,x87,f615(),x88) + x89 >= f3(f611(x86),f613(x87),f614(x88)) + f612(x89) = f3(f611(x86),f613(x87),f614(x88)) + f612(x89) | | | +- f616(x3) = f616(x3) >= f610(x3) = f610(x3) | | | +- f617(x2) = f617(x2) >= x2 = x2 | | | +- f618(x1) = f618(x1) >= x1 = x1 | | | +- f619(x1,x2,x3,x86,x87,x88,x89) = f619(x1,x2,x3,x86,x87,x88,x89) >= f21(f615(),f618(x1),f617(x2),f619(x1,x2,x3,x86,x87,x88,x89)) + f616(x3) = f21(f615() ,f618(x1) ,f617(x2) ,f619(x1,x2,x3,x86,x87,x88,x89)) + f616(x3) | | | +- f620(x1,x2,x3,x86,x87,x88,x89) = f620(x1,x2,x3,x86,x87,x88,x89) >= f20(f615(),f618(x1),f617(x2)) + f619(x1,x2,x3,x86,x87,x88,x89) = f20(f615(),f618(x1),f617(x2)) + f619(x1,x2,x3,x86,x87,x88,x89) | | | +- f13(x1,x2) = f13(x1,x2) >= f19(f615(),f618(x1),f617(x2)) = f19(f615(),f618(x1),f617(x2)) | | | +- f12(x1,x2) = f12(x1,x2) >= f18(f615(),f618(x1),f617(x2)) = f18(f615(),f618(x1),f617(x2)) | | | +- f14(x1,x2) + x3 = f14(x1,x2) + x3 >= f620(x1,x2,x3,x86,x87,x88,x89) + 1 = f620(x1,x2,x3,x86,x87,x88,x89) + 1 | | | +- f621(x6) = f621(x6) >= x6 = x6 | | | +- f622(x7) = f622(x7) >= x7 = x7 | | | +- f623(x6) = f623(x6) >= f621(x6) = f621(x6) | | | +- f624(x8) = f624(x8) >= x8 = x8 | | | +- f625(x6,x7,x8) = f625(x6,x7,x8) >= f3(f622(x7),f624(x8),f625(x6,x7,x8)) + f623(x6) = f3(f622(x7),f624(x8),f625(x6,x7,x8)) + f623(x6) | | | +- f626(x6,x7,x8) = f626(x6,x7,x8) >= f2(f622(x7),f624(x8)) + f625(x6,x7,x8) = f2(f622(x7),f624(x8)) + f625(x6,x7,x8) | | | +- f1(x7 + 1,x8 + 1) = f1(x7 + 1,x8 + 1) >= f1(f622(x7),f624(x8)) = f1(f622(x7),f624(x8)) | | | +- f2(x7 + 1,x8 + 1) + x6 = f2(x7 + 1,x8 + 1) + x6 >= f626(x6,x7,x8) + 1 = f626(x6,x7,x8) + 1 | | | +- f627(x11) = f627(x11) >= x11 = x11 | | | +- f628(x11) = f628(x11) >= f627(x11) = f627(x11) | | | +- f1(x12 + 1,0) = f1(x12 + 1,0) >= 0 = 0 | | | +- f2(x12 + 1,0) + x11 = f2(x12 + 1,0) + x11 >= f628(x11) + 1 = f628(x11) + 1 | | | +- f629(x15) = f629(x15) >= x15 = x15 | | | +- f630(x15) = f630(x15) >= f629(x15) = f629(x15) | | | +- f1(0,x14) = f1(0,x14) >= 0 = 0 | | | +- f2(0,x14) + x15 = f2(0,x14) + x15 >= f630(x15) + 1 = f630(x15) + 1 | | | +- f631(x19) = f631(x19) >= x19 = x19 | | | +- f632(x19) = f632(x19) >= f631(x19) = f631(x19) | | | +- f19(x16,x17,0) = f19(x16,x17,0) >= 0 = 0 | | | +- f18(x16,x17,0) = f18(x16,x17,0) >= f633() = f633() | | | +- f20(x16,x17,0) + x19 = f20(x16,x17,0) + x19 >= f632(x19) + 1 = f632(x19) + 1 | | | +- f634(x28) = f634(x28) >= x28 = x28 | | | +- f635(x170) = f635(x170) >= x170 = x170 | | | +- f636(x173) = f636(x173) >= x173 = x173 | | | +- f637(x171) = f637(x171) >= x171 = x171 | | | +- f638(x172) = f638(x172) >= x172 = x172 | | | +- f4(x170,x171,f639(x25)) = f4(x170,x171,f639(x25)) >= f15(f635(x170),f637(x171),x25) = f15(f635(x170),f637(x171),x25) | | | +- f5(x170,x171,f639(x25)) + x172 = f5(x170,x171,f639(x25)) + x172 >= f16(f635(x170),f637(x171),x25) + f638(x172) = f16(f635(x170),f637(x171),x25) + f638(x172) | | | +- f6(x170,x171,f639(x25),x172) + x173 = f6(x170,x171,f639(x25),x172) + x173 >= f17(f635(x170),f637(x171),x25,f638(x172)) + f636(x173) = f17(f635(x170),f637(x171),x25,f638(x172)) + f636(x173) | | | +- f640(x28) = f640(x28) >= f634(x28) = f634(x28) | | | +- f641(x26) = f641(x26) >= x26 = x26 | | | +- f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f11(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) ,f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f640(x28) = f11(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) ,f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f640(x28) | | | +- f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f10(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f10(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f647(x238) = f647(x238) >= x238 = x238 | | | +- f648(x241) = f648(x241) >= x241 = x241 | | | +- f649(x239) = f649(x239) >= x239 = x239 | | | +- f650(x240) = f650(x240) >= x240 = x240 | | | +- f15(x238,x239,f651(x25)) = f15(x238,x239,f651(x25)) >= f15(f647(x238),f649(x239),x25) = f15(f647(x238),f649(x239),x25) | | | +- f16(x238,x239,f651(x25)) + x240 = f16(x238,x239,f651(x25)) + x240 >= f16(f647(x238),f649(x239),x25) + f650(x240) = f16(f647(x238),f649(x239),x25) + f650(x240) | | | +- f17(x238,x239,f651(x25),x240) + x241 = f17(x238,x239,f651(x25),x240) + x241 >= f17(f647(x238),f649(x239),x25,f650(x240)) + f648(x241) = f17(f647(x238),f649(x239),x25,f650(x240)) + f648(x241) | | | +- f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f653(x30) = f653(x30) >= x30 = x30 | | | +- f654(x26) = f654(x26) >= x26 = x26 | | | +- f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f21(f651(x25) ,f654(x26) ,f653(x30) ,f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f21(f651(x25) ,f654(x26) ,f653(x30) ,f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f644(x25,x26,x30,x238,x239,x240,x241) = f644(x25,x26,x30,x238,x239,x240,x241) >= f19(f651(x25),f654(x26),f653(x30)) = f19(f651(x25),f654(x26),f653(x30)) | | | +- f643(x25,x26,x30,x238,x239,x240,x241) = f643(x25,x26,x30,x238,x239,x240,x241) >= f18(f651(x25),f654(x26),f653(x30)) = f18(f651(x25),f654(x26),f653(x30)) | | | +- f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f20(f651(x25),f654(x26),f653(x30)) + f655(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) = f20(f651(x25) ,f654(x26) ,f653(x30)) + f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f9(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) + f645(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) = f9(f639(x25) ,f641(x26) ,f643(x25 ,x26 ,x30 ,x238 ,x239 ,x240 ,x241) ,f644(x25 ,x26 ,x30 ,x238 ,x239 ,x240 ,x241)) + f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f19(x25,x26,x30 + 1) = f19(x25,x26,x30 + 1) >= f8(f639(x25),f641(x26),f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) = f8(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) | | | +- f18(x25,x26,x30 + 1) = f18(x25,x26,x30 + 1) >= f7(f639(x25),f641(x26),f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) = f7(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) | | | +- f20(x25,x26,x30 + 1) + x28 = f20(x25,x26,x30 + 1) + x28 >= f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 | | | +- f657(x36) = f657(x36) >= x36 = x36 | | | +- f658(x39) = f658(x39) >= x39 = x39 | | | +- f659(x37) = f659(x37) >= x37 = x37 | | | +- f660(x35,x36,x37,x39) = f660(x35,x36,x37,x39) >= f6(f657(x36),f659(x37),x35,f660(x35,x36,x37,x39)) + f658(x39) = f6(f657(x36),f659(x37),x35,f660(x35,x36,x37,x39)) + f658(x39) | | | +- f661(x35,x36,x37,x39) = f661(x35,x36,x37,x39) >= f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) = f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) | | | +- f662(x36,x37) = f662(x36,x37) >= x36 = x36 | | | +- f663(x35,x36,x37,x39) = f663(x35,x36,x37,x39) >= f661(x35,x36,x37,x39) = f661(x35,x36,x37,x39) | | | +- f664(x35,x36,x37,x39) = f664(x35,x36,x37,x39) >= f663(x35,x36,x37,x39) = f663(x35,x36,x37,x39) | | | +- f665(x37) = f665(x37) >= x37 = x37 | | | +- f666(x35,x36,x37,x39) = f666(x35,x36,x37,x39) >= f664(x35,x36,x37,x39) = f664(x35,x36,x37,x39) | | | +- f667(x41) = f667(x41) >= x41 = x41 | | | +- f668(x35,x36,x37,x39) = f668(x35,x36,x37,x39) >= f666(x35,x36,x37,x39) = f666(x35,x36,x37,x39) | | | +- f669(x41) = f669(x41) >= f667(x41) + 1 = f667(x41) + 1 | | | +- f662(x36,x37) = f662(x36,x37) >= f665(x37) = f665(x37) | | | +- f670(x35,x36,x37,x39) = f670(x35,x36,x37,x39) >= f668(x35,x36,x37,x39) = f668(x35,x36,x37,x39) | | | +- f671(x35,x36,x37,x39) = f671(x35,x36,x37,x39) >= f670(x35,x36,x37,x39) = f670(x35,x36,x37,x39) | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) >= f662(x36,x37) = f662(x36,x37) | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) >= f669(x41) + 1 = f669(x41) + 1 | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f671(x35,x36,x37,x39) + 1 = f671(x35,x36,x37,x39) + 1 | | | +- f675(x35,x36,x37,x39) = f675(x35,x36,x37,x39) >= f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) = f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) | | | +- f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) >= x37 = x37 | | | +- f677(x35,x36,x37,x39) = f677(x35,x36,x37,x39) >= f675(x35,x36,x37,x39) = f675(x35,x36,x37,x39) | | | +- f678(x35,x36,x37,x39) = f678(x35,x36,x37,x39) >= f677(x35,x36,x37,x39) = f677(x35,x36,x37,x39) | | | +- f679(x475) = f679(x475) >= x475 = x475 | | | +- f680(x478) = f680(x478) >= x478 = x478 | | | +- f681(x476) = f681(x476) >= x476 = x476 | | | +- f682(x477) = f682(x477) >= x477 = x477 | | | +- f4(x475,x476,f683(x35)) = f4(x475,x476,f683(x35)) >= f4(f679(x475),f681(x476),x35) = f4(f679(x475),f681(x476),x35) | | | +- f5(x475,x476,f683(x35)) + x477 = f5(x475,x476,f683(x35)) + x477 >= f5(f679(x475),f681(x476),x35) + f682(x477) = f5(f679(x475),f681(x476),x35) + f682(x477) | | | +- f6(x475,x476,f683(x35),x477) + x478 = f6(x475,x476,f683(x35),x477) + x478 >= f6(f679(x475),f681(x476),x35,f682(x477)) + f680(x478) = f6(f679(x475),f681(x476),x35,f682(x477)) + f680(x478) | | | +- f684(x35,x36,x37,x39) = f684(x35,x36,x37,x39) >= f678(x35,x36,x37,x39) = f678(x35,x36,x37,x39) | | | +- f685(x36) = f685(x36) >= x36 = x36 | | | +- f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f11(f683(x35) ,f685(x36) ,f687(x37) ,f688(x41) ,f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) ,f686(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f684(x35,x36,x37,x39) = f11(f683(x35) ,f685(x36) ,f687(x37) ,f688(x41) ,f689(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478) ,f686(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478)) + f684(x35,x36,x37,x39) | | | +- f688(x41) = f688(x41) >= x41 = x41 | | | +- f687(x37) = f687(x37) >= x37 = x37 | | | +- f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f10(f683(x35),f685(x36),f687(x37),f688(x41),f689(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f686(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478) = f10(f683(x35),f685(x36),f687(x37),f688(x41),f689(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f690(x35,x36,x37,x41,x475,x476,x477,x478) = f690(x35,x36,x37,x41,x475,x476,x477,x478) >= f8(f683(x35),f685(x36),f687(x37),f688(x41)) = f8(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) >= f7(f683(x35),f685(x36),f687(x37),f688(x41)) = f7(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f9(f683(x35),f685(x36),f687(x37),f688(x41)) + f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f9(f683(x35),f685(x36),f687(x37),f688(x41)) + f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) >= f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 = f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) >= f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 | | | +- f8(x35,x36,x37,x41 + 1) = f8(x35,x36,x37,x41 + 1) >= f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f7(x35,x36,x37,x41 + 1) = f7(x35,x36,x37,x41 + 1) >= f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f9(x35,x36,x37,x41 + 1) + x39 = f9(x35,x36,x37,x41 + 1) + x39 >= f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f693(x50) = f693(x50) >= x50 = x50 | | | +- f694(x47) = f694(x47) >= x47 = x47 | | | +- f695(x50) = f695(x50) >= f693(x50) = f693(x50) | | | +- f696(x50) = f696(x50) >= f695(x50) = f695(x50) | | | +- f697() = f697() >= 0 = 0 | | | +- f694(x47) = f694(x47) >= f698() = f698() | | | +- f699(x50) = f699(x50) >= f696(x50) = f696(x50) | | | +- f700(x50) = f700(x50) >= f699(x50) = f699(x50) | | | +- f8(x46,x47,x48,0) = f8(x46,x47,x48,0) >= f697() + 1 = f697() + 1 | | | +- f7(x46,x47,x48,0) = f7(x46,x47,x48,0) >= f694(x47) = f694(x47) | | | `- f9(x46,x47,x48,0) + x50 = f9(x46,x47,x48,0) + x50 >= f700(x50) + 1 = f700(x50) + 1 | +- Open Constraints | | | +- f609(x3) = f609(x3) >= x3 = x3 | | | +- f610(x3) = f610(x3) >= f609(x3) = f609(x3) | | | +- f611(x86) = f611(x86) >= x86 = x86 | | | +- f612(x89) = f612(x89) >= x89 = x89 | | | +- f613(x87) = f613(x87) >= x87 = x87 | | | +- f614(x88) = f614(x88) >= x88 = x88 | | | +- f15(x86,x87,f615()) = f15(x86,x87,f615()) >= f1(f611(x86),f613(x87)) = f1(f611(x86),f613(x87)) | | | +- f16(x86,x87,f615()) + x88 = f16(x86,x87,f615()) + x88 >= f2(f611(x86),f613(x87)) + f614(x88) = f2(f611(x86),f613(x87)) + f614(x88) | | | +- f17(x86,x87,f615(),x88) + x89 = f17(x86,x87,f615(),x88) + x89 >= f3(f611(x86),f613(x87),f614(x88)) + f612(x89) = f3(f611(x86),f613(x87),f614(x88)) + f612(x89) | | | +- f616(x3) = f616(x3) >= f610(x3) = f610(x3) | | | +- f617(x2) = f617(x2) >= x2 = x2 | | | +- f618(x1) = f618(x1) >= x1 = x1 | | | +- f619(x1,x2,x3,x86,x87,x88,x89) = f619(x1,x2,x3,x86,x87,x88,x89) >= f21(f615(),f618(x1),f617(x2),f619(x1,x2,x3,x86,x87,x88,x89)) + f616(x3) = f21(f615() ,f618(x1) ,f617(x2) ,f619(x1,x2,x3,x86,x87,x88,x89)) + f616(x3) | | | +- f620(x1,x2,x3,x86,x87,x88,x89) = f620(x1,x2,x3,x86,x87,x88,x89) >= f20(f615(),f618(x1),f617(x2)) + f619(x1,x2,x3,x86,x87,x88,x89) = f20(f615(),f618(x1),f617(x2)) + f619(x1,x2,x3,x86,x87,x88,x89) | | | +- f13(x1,x2) = f13(x1,x2) >= f19(f615(),f618(x1),f617(x2)) = f19(f615(),f618(x1),f617(x2)) | | | +- f12(x1,x2) = f12(x1,x2) >= f18(f615(),f618(x1),f617(x2)) = f18(f615(),f618(x1),f617(x2)) | | | +- f14(x1,x2) + x3 = f14(x1,x2) + x3 >= f620(x1,x2,x3,x86,x87,x88,x89) + 1 = f620(x1,x2,x3,x86,x87,x88,x89) + 1 | | | +- f621(x6) = f621(x6) >= x6 = x6 | | | +- f622(x7) = f622(x7) >= x7 = x7 | | | +- f623(x6) = f623(x6) >= f621(x6) = f621(x6) | | | +- f624(x8) = f624(x8) >= x8 = x8 | | | +- f625(x6,x7,x8) = f625(x6,x7,x8) >= f3(f622(x7),f624(x8),f625(x6,x7,x8)) + f623(x6) = f3(f622(x7),f624(x8),f625(x6,x7,x8)) + f623(x6) | | | +- f626(x6,x7,x8) = f626(x6,x7,x8) >= f2(f622(x7),f624(x8)) + f625(x6,x7,x8) = f2(f622(x7),f624(x8)) + f625(x6,x7,x8) | | | +- f1(x7 + 1,x8 + 1) = f1(x7 + 1,x8 + 1) >= f1(f622(x7),f624(x8)) = f1(f622(x7),f624(x8)) | | | +- f2(x7 + 1,x8 + 1) + x6 = f2(x7 + 1,x8 + 1) + x6 >= f626(x6,x7,x8) + 1 = f626(x6,x7,x8) + 1 | | | +- f627(x11) = f627(x11) >= x11 = x11 | | | +- f628(x11) = f628(x11) >= f627(x11) = f627(x11) | | | +- f1(x12 + 1,0) = f1(x12 + 1,0) >= 0 = 0 | | | +- f2(x12 + 1,0) + x11 = f2(x12 + 1,0) + x11 >= f628(x11) + 1 = f628(x11) + 1 | | | +- f629(x15) = f629(x15) >= x15 = x15 | | | +- f630(x15) = f630(x15) >= f629(x15) = f629(x15) | | | +- f1(0,x14) = f1(0,x14) >= 0 = 0 | | | +- f2(0,x14) + x15 = f2(0,x14) + x15 >= f630(x15) + 1 = f630(x15) + 1 | | | +- f631(x19) = f631(x19) >= x19 = x19 | | | +- f632(x19) = f632(x19) >= f631(x19) = f631(x19) | | | +- f19(x16,x17,0) = f19(x16,x17,0) >= 0 = 0 | | | +- f18(x16,x17,0) = f18(x16,x17,0) >= f633() = f633() | | | +- f20(x16,x17,0) + x19 = f20(x16,x17,0) + x19 >= f632(x19) + 1 = f632(x19) + 1 | | | +- f634(x28) = f634(x28) >= x28 = x28 | | | +- f635(x170) = f635(x170) >= x170 = x170 | | | +- f636(x173) = f636(x173) >= x173 = x173 | | | +- f637(x171) = f637(x171) >= x171 = x171 | | | +- f638(x172) = f638(x172) >= x172 = x172 | | | +- f4(x170,x171,f639(x25)) = f4(x170,x171,f639(x25)) >= f15(f635(x170),f637(x171),x25) = f15(f635(x170),f637(x171),x25) | | | +- f5(x170,x171,f639(x25)) + x172 = f5(x170,x171,f639(x25)) + x172 >= f16(f635(x170),f637(x171),x25) + f638(x172) = f16(f635(x170),f637(x171),x25) + f638(x172) | | | +- f6(x170,x171,f639(x25),x172) + x173 = f6(x170,x171,f639(x25),x172) + x173 >= f17(f635(x170),f637(x171),x25,f638(x172)) + f636(x173) = f17(f635(x170),f637(x171),x25,f638(x172)) + f636(x173) | | | +- f640(x28) = f640(x28) >= f634(x28) = f634(x28) | | | +- f641(x26) = f641(x26) >= x26 = x26 | | | +- f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f11(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) ,f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f640(x28) = f11(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) ,f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f640(x28) | | | +- f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f10(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f10(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f647(x238) = f647(x238) >= x238 = x238 | | | +- f648(x241) = f648(x241) >= x241 = x241 | | | +- f649(x239) = f649(x239) >= x239 = x239 | | | +- f650(x240) = f650(x240) >= x240 = x240 | | | +- f15(x238,x239,f651(x25)) = f15(x238,x239,f651(x25)) >= f15(f647(x238),f649(x239),x25) = f15(f647(x238),f649(x239),x25) | | | +- f16(x238,x239,f651(x25)) + x240 = f16(x238,x239,f651(x25)) + x240 >= f16(f647(x238),f649(x239),x25) + f650(x240) = f16(f647(x238),f649(x239),x25) + f650(x240) | | | +- f17(x238,x239,f651(x25),x240) + x241 = f17(x238,x239,f651(x25),x240) + x241 >= f17(f647(x238),f649(x239),x25,f650(x240)) + f648(x241) = f17(f647(x238),f649(x239),x25,f650(x240)) + f648(x241) | | | +- f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f653(x30) = f653(x30) >= x30 = x30 | | | +- f654(x26) = f654(x26) >= x26 = x26 | | | +- f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f21(f651(x25) ,f654(x26) ,f653(x30) ,f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f21(f651(x25) ,f654(x26) ,f653(x30) ,f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f644(x25,x26,x30,x238,x239,x240,x241) = f644(x25,x26,x30,x238,x239,x240,x241) >= f19(f651(x25),f654(x26),f653(x30)) = f19(f651(x25),f654(x26),f653(x30)) | | | +- f643(x25,x26,x30,x238,x239,x240,x241) = f643(x25,x26,x30,x238,x239,x240,x241) >= f18(f651(x25),f654(x26),f653(x30)) = f18(f651(x25),f654(x26),f653(x30)) | | | +- f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f20(f651(x25),f654(x26),f653(x30)) + f655(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) = f20(f651(x25) ,f654(x26) ,f653(x30)) + f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f9(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) + f645(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) = f9(f639(x25) ,f641(x26) ,f643(x25 ,x26 ,x30 ,x238 ,x239 ,x240 ,x241) ,f644(x25 ,x26 ,x30 ,x238 ,x239 ,x240 ,x241)) + f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f19(x25,x26,x30 + 1) = f19(x25,x26,x30 + 1) >= f8(f639(x25),f641(x26),f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) = f8(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) | | | +- f18(x25,x26,x30 + 1) = f18(x25,x26,x30 + 1) >= f7(f639(x25),f641(x26),f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) = f7(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) | | | +- f20(x25,x26,x30 + 1) + x28 = f20(x25,x26,x30 + 1) + x28 >= f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 | | | +- f657(x36) = f657(x36) >= x36 = x36 | | | +- f658(x39) = f658(x39) >= x39 = x39 | | | +- f659(x37) = f659(x37) >= x37 = x37 | | | +- f660(x35,x36,x37,x39) = f660(x35,x36,x37,x39) >= f6(f657(x36),f659(x37),x35,f660(x35,x36,x37,x39)) + f658(x39) = f6(f657(x36),f659(x37),x35,f660(x35,x36,x37,x39)) + f658(x39) | | | +- f661(x35,x36,x37,x39) = f661(x35,x36,x37,x39) >= f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) = f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) | | | +- f662(x36,x37) = f662(x36,x37) >= x36 = x36 | | | +- f663(x35,x36,x37,x39) = f663(x35,x36,x37,x39) >= f661(x35,x36,x37,x39) = f661(x35,x36,x37,x39) | | | +- f664(x35,x36,x37,x39) = f664(x35,x36,x37,x39) >= f663(x35,x36,x37,x39) = f663(x35,x36,x37,x39) | | | +- f665(x37) = f665(x37) >= x37 = x37 | | | +- f666(x35,x36,x37,x39) = f666(x35,x36,x37,x39) >= f664(x35,x36,x37,x39) = f664(x35,x36,x37,x39) | | | +- f667(x41) = f667(x41) >= x41 = x41 | | | +- f668(x35,x36,x37,x39) = f668(x35,x36,x37,x39) >= f666(x35,x36,x37,x39) = f666(x35,x36,x37,x39) | | | +- f669(x41) = f669(x41) >= f667(x41) + 1 = f667(x41) + 1 | | | +- f662(x36,x37) = f662(x36,x37) >= f665(x37) = f665(x37) | | | +- f670(x35,x36,x37,x39) = f670(x35,x36,x37,x39) >= f668(x35,x36,x37,x39) = f668(x35,x36,x37,x39) | | | +- f671(x35,x36,x37,x39) = f671(x35,x36,x37,x39) >= f670(x35,x36,x37,x39) = f670(x35,x36,x37,x39) | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) >= f662(x36,x37) = f662(x36,x37) | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) >= f669(x41) + 1 = f669(x41) + 1 | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f671(x35,x36,x37,x39) + 1 = f671(x35,x36,x37,x39) + 1 | | | +- f675(x35,x36,x37,x39) = f675(x35,x36,x37,x39) >= f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) = f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) | | | +- f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) >= x37 = x37 | | | +- f677(x35,x36,x37,x39) = f677(x35,x36,x37,x39) >= f675(x35,x36,x37,x39) = f675(x35,x36,x37,x39) | | | +- f678(x35,x36,x37,x39) = f678(x35,x36,x37,x39) >= f677(x35,x36,x37,x39) = f677(x35,x36,x37,x39) | | | +- f679(x475) = f679(x475) >= x475 = x475 | | | +- f680(x478) = f680(x478) >= x478 = x478 | | | +- f681(x476) = f681(x476) >= x476 = x476 | | | +- f682(x477) = f682(x477) >= x477 = x477 | | | +- f4(x475,x476,f683(x35)) = f4(x475,x476,f683(x35)) >= f4(f679(x475),f681(x476),x35) = f4(f679(x475),f681(x476),x35) | | | +- f5(x475,x476,f683(x35)) + x477 = f5(x475,x476,f683(x35)) + x477 >= f5(f679(x475),f681(x476),x35) + f682(x477) = f5(f679(x475),f681(x476),x35) + f682(x477) | | | +- f6(x475,x476,f683(x35),x477) + x478 = f6(x475,x476,f683(x35),x477) + x478 >= f6(f679(x475),f681(x476),x35,f682(x477)) + f680(x478) = f6(f679(x475),f681(x476),x35,f682(x477)) + f680(x478) | | | +- f684(x35,x36,x37,x39) = f684(x35,x36,x37,x39) >= f678(x35,x36,x37,x39) = f678(x35,x36,x37,x39) | | | +- f685(x36) = f685(x36) >= x36 = x36 | | | +- f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f11(f683(x35) ,f685(x36) ,f687(x37) ,f688(x41) ,f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) ,f686(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f684(x35,x36,x37,x39) = f11(f683(x35) ,f685(x36) ,f687(x37) ,f688(x41) ,f689(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478) ,f686(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478)) + f684(x35,x36,x37,x39) | | | +- f688(x41) = f688(x41) >= x41 = x41 | | | +- f687(x37) = f687(x37) >= x37 = x37 | | | +- f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f10(f683(x35),f685(x36),f687(x37),f688(x41),f689(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f686(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478) = f10(f683(x35),f685(x36),f687(x37),f688(x41),f689(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f690(x35,x36,x37,x41,x475,x476,x477,x478) = f690(x35,x36,x37,x41,x475,x476,x477,x478) >= f8(f683(x35),f685(x36),f687(x37),f688(x41)) = f8(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) >= f7(f683(x35),f685(x36),f687(x37),f688(x41)) = f7(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f9(f683(x35),f685(x36),f687(x37),f688(x41)) + f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f9(f683(x35),f685(x36),f687(x37),f688(x41)) + f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) >= f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 = f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) >= f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 | | | +- f8(x35,x36,x37,x41 + 1) = f8(x35,x36,x37,x41 + 1) >= f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f7(x35,x36,x37,x41 + 1) = f7(x35,x36,x37,x41 + 1) >= f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f9(x35,x36,x37,x41 + 1) + x39 = f9(x35,x36,x37,x41 + 1) + x39 >= f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f693(x50) = f693(x50) >= x50 = x50 | | | +- f694(x47) = f694(x47) >= x47 = x47 | | | +- f695(x50) = f695(x50) >= f693(x50) = f693(x50) | | | +- f696(x50) = f696(x50) >= f695(x50) = f695(x50) | | | +- f697() = f697() >= 0 = 0 | | | +- f694(x47) = f694(x47) >= f698() = f698() | | | +- f699(x50) = f699(x50) >= f696(x50) = f696(x50) | | | +- f700(x50) = f700(x50) >= f699(x50) = f699(x50) | | | +- f8(x46,x47,x48,0) = f8(x46,x47,x48,0) >= f697() + 1 = f697() + 1 | | | +- f7(x46,x47,x48,0) = f7(x46,x47,x48,0) >= f694(x47) = f694(x47) | | | `- f9(x46,x47,x48,0) + x50 = f9(x46,x47,x48,0) + x50 >= f700(x50) + 1 = f700(x50) + 1 | +- Simplification ... | | | +- Substituted: f1(x12 + 1,0) ≥ 0 ↦ f1(1,0) ≥ 0 | | | +- Substituted: f2(x12 + 1,0) + x11 ≥ f628(x11) + 1 ↦ f2(1,0) + x11 ≥ f628(x11) + 1 | | | +- Substituted: f1(0,x14) ≥ 0 ↦ f1(0,0) ≥ 0 | | | +- Substituted: f2(0,x14) + x15 ≥ f630(x15) + 1 ↦ f2(0,0) + x15 ≥ f630(x15) + 1 | | | +- Substituted: f19(x16,x17,0) ≥ 0 ↦ f19(0,0,0) ≥ 0 | | | +- Substituted: f18(x16,x17,0) ≥ f633() ↦ f18(0,0,0) ≥ f633() | | | +- Substituted: f20(x16,x17,0) + x19 ≥ f632(x19) + 1 ↦ f20(0,0,0) + x19 ≥ f632(x19) + 1 | | | +- Substituted: f644(x25,x26,x30,x238,x239,x240,x241) ≥ f19(f651(x25),f654(x26),f653(x30)) ↦ f644(x25,x26,x30,0,0,0,0) ≥ f19(f651(x25),f654(x26),f653(x30)) | | | +- Substituted: f643(x25,x26,x30,x238,x239,x240,x241) ≥ f18(f651(x25),f654(x26),f653(x30)) ↦ f643(x25,x26,x30,0,0,0,0) ≥ f18(f651(x25),f654(x26),f653(x30)) | | | +- Substituted: f662(x36,x37) ≥ x36 ↦ f662(x36,0) ≥ x36 | | | +- Substituted: f662(x36,x37) ≥ f665(x37) ↦ f662(0,x37) ≥ f665(x37) | | | +- Substituted: f672(x35,x36,x37,x41,x475,x476,x477,x478) ≥ f662(x36,x37) ↦ f672(0,x36,x37,0,0,0,0,0) ≥ f662(x36,x37) | | | +- Substituted: f673(x35,x36,x37,x41,x475,x476,x477,x478) ≥ f669(x41) + 1 ↦ f673(0,0,0,x41,0,0,0,0) ≥ f669(x41) + 1 | | | +- Substituted: f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) ≥ f671(x35,x36,x37,x39) + 1 ↦ f674(x35,x36,x37,x39,0,0,0,0,0) ≥ f671(x35,x36,x37,x39) + 1 | | | +- Substituted: f676(x35,x36,x37,x41,x475,x476,x477,x478) ≥ x37 ↦ f676(0,0,x37,0,0,0,0,0) ≥ x37 | | | +- Substituted: f690(x35,x36,x37,x41,x475,x476,x477,x478) ≥ f8(f683(x35),f685(x36),f687(x37),f688(x41)) ↦ f690(x35,x36,x37,x41,0,0,0,0) ≥ f8(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- Substituted: f676(x35,x36,x37,x41,x475,x476,x477,x478) ≥ f7(f683(x35),f685(x36),f687(x37),f688(x41)) ↦ f676(x35,x36,x37,x41,0,0,0,0) ≥ f7(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- Substituted: f694(x47) ≥ f698() ↦ f694(0) ≥ f698() | | | +- Substituted: f8(x46,x47,x48,0) ≥ f697() + 1 ↦ f8(0,0,0,0) ≥ f697() + 1 | | | +- Substituted: f7(x46,x47,x48,0) ≥ f694(x47) ↦ f7(0,x47,0,0) ≥ f694(x47) | | | +- Substituted: f9(x46,x47,x48,0) + x50 ≥ f700(x50) + 1 ↦ f9(0,0,0,0) + x50 ≥ f700(x50) + 1 | | | +- Eliminated: f10/5 | | | +- Eliminated: f11/6 | | | +- Eliminated: f21/4 | | | +- Eliminated: f3/3 | | | +- Eliminated: f633/0 | | | +- Eliminated: f698/0 | | | +- Propagated: f609(x0) ↦ x0 | | | +- Propagated: f611(x0) ↦ x0 | | | +- Propagated: f612(x0) ↦ x0 | | | +- Propagated: f613(x0) ↦ x0 | | | +- Propagated: f614(x0) ↦ x0 | | | +- Propagated: f617(x0) ↦ x0 | | | +- Propagated: f618(x0) ↦ x0 | | | +- Propagated: f621(x0) ↦ x0 | | | +- Propagated: f622(x0) ↦ x0 | | | +- Propagated: f624(x0) ↦ x0 | | | +- Propagated: f627(x0) ↦ x0 | | | +- Propagated: f629(x0) ↦ x0 | | | +- Propagated: f631(x0) ↦ x0 | | | +- Propagated: f634(x0) ↦ x0 | | | +- Propagated: f635(x0) ↦ x0 | | | +- Propagated: f636(x0) ↦ x0 | | | +- Propagated: f637(x0) ↦ x0 | | | +- Propagated: f638(x0) ↦ x0 | | | +- Propagated: f641(x0) ↦ x0 | | | +- Propagated: f647(x0) ↦ x0 | | | +- Propagated: f648(x0) ↦ x0 | | | +- Propagated: f649(x0) ↦ x0 | | | +- Propagated: f650(x0) ↦ x0 | | | +- Propagated: f653(x0) ↦ x0 | | | +- Propagated: f654(x0) ↦ x0 | | | +- Propagated: f657(x0) ↦ x0 | | | +- Propagated: f658(x0) ↦ x0 | | | +- Propagated: f659(x0) ↦ x0 | | | +- Propagated: f665(x0) ↦ x0 | | | +- Propagated: f667(x0) ↦ x0 | | | +- Propagated: f679(x0) ↦ x0 | | | +- Propagated: f680(x0) ↦ x0 | | | +- Propagated: f681(x0) ↦ x0 | | | +- Propagated: f682(x0) ↦ x0 | | | +- Propagated: f685(x0) ↦ x0 | | | +- Propagated: f687(x0) ↦ x0 | | | +- Propagated: f688(x0) ↦ x0 | | | +- Propagated: f693(x0) ↦ x0 | | | +- Propagated: f697() ↦ 0 | | | +- Propagated: f610(x0) ↦ x0 | | | +- Propagated: f623(x0) ↦ x0 | | | +- Propagated: f628(x0) ↦ x0 | | | +- Propagated: f630(x0) ↦ x0 | | | +- Propagated: f632(x0) ↦ x0 | | | +- Propagated: f640(x0) ↦ x0 | | | +- Propagated: f669(x0) ↦ 1 + x0 | | | +- Propagated: f695(x0) ↦ x0 | | | +- Propagated: f616(x0) ↦ x0 | | | +- Propagated: f625(x0,x1,x2) ↦ x0 | | | +- Propagated: f642(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ↦ x2 | | | +- Propagated: f696(x0) ↦ x0 | | | +- Propagated: f619(x0,x1,x2,x3,x4,x5,x6) ↦ x2 | | | +- Propagated: f646(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ↦ x2 | | | +- Propagated: f699(x0) ↦ x0 | | | +- Propagated: f652(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ↦ x2 | | | +- Propagated: f700(x0) ↦ x0 | | | `- Propagated: f655(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) ↦ x2 | +- Interpretation | | | +- f10(x0,x1,x2,x3,x4) = 0 | | | +- f11(x0,x1,x2,x3,x4,x5) = 0 | | | +- f21(x0,x1,x2,x3) = 0 | | | +- f3(x0,x1,x2) = 0 | | | +- f609(x0) = x0 | | | +- f610(x0) = x0 | | | +- f611(x0) = x0 | | | +- f612(x0) = x0 | | | +- f613(x0) = x0 | | | +- f614(x0) = x0 | | | +- f616(x0) = x0 | | | +- f617(x0) = x0 | | | +- f618(x0) = x0 | | | +- f619(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f621(x0) = x0 | | | +- f622(x0) = x0 | | | +- f623(x0) = x0 | | | +- f624(x0) = x0 | | | +- f625(x0,x1,x2) = x0 | | | +- f627(x0) = x0 | | | +- f628(x0) = x0 | | | +- f629(x0) = x0 | | | +- f630(x0) = x0 | | | +- f631(x0) = x0 | | | +- f632(x0) = x0 | | | +- f633() = 0 | | | +- f634(x0) = x0 | | | +- f635(x0) = x0 | | | +- f636(x0) = x0 | | | +- f637(x0) = x0 | | | +- f638(x0) = x0 | | | +- f640(x0) = x0 | | | +- f641(x0) = x0 | | | +- f642(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2 | | | +- f646(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2 | | | +- f647(x0) = x0 | | | +- f648(x0) = x0 | | | +- f649(x0) = x0 | | | +- f650(x0) = x0 | | | +- f652(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2 | | | +- f653(x0) = x0 | | | +- f654(x0) = x0 | | | +- f655(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2 | | | +- f657(x0) = x0 | | | +- f658(x0) = x0 | | | +- f659(x0) = x0 | | | +- f665(x0) = x0 | | | +- f667(x0) = x0 | | | +- f669(x0) = 1 + x0 | | | +- f679(x0) = x0 | | | +- f680(x0) = x0 | | | +- f681(x0) = x0 | | | +- f682(x0) = x0 | | | +- f685(x0) = x0 | | | +- f687(x0) = x0 | | | +- f688(x0) = x0 | | | +- f693(x0) = x0 | | | +- f695(x0) = x0 | | | +- f696(x0) = x0 | | | +- f697() = 0 | | | +- f698() = 0 | | | +- f699(x0) = x0 | | | `- f700(x0) = x0 | +- Constraints | | | +- f609(x3) = x3 >= x3 = x3 | | | +- f610(x3) = x3 >= x3 = f609(x3) | | | +- f611(x86) = x86 >= x86 = x86 | | | +- f612(x89) = x89 >= x89 = x89 | | | +- f613(x87) = x87 >= x87 = x87 | | | +- f614(x88) = x88 >= x88 = x88 | | | +- f15(x86,x87,f615()) = f15(x86,x87,f615()) >= f1(x86,x87) = f1(f611(x86),f613(x87)) | | | +- f16(x86,x87,f615()) + x88 = f16(x86,x87,f615()) + x88 >= f2(x86,x87) + x88 = f2(f611(x86),f613(x87)) + f614(x88) | | | +- f17(x86,x87,f615(),x88) + x89 = f17(x86,x87,f615(),x88) + x89 >= x89 = f3(f611(x86),f613(x87),f614(x88)) + f612(x89) | | | +- f616(x3) = x3 >= x3 = f610(x3) | | | +- f617(x2) = x2 >= x2 = x2 | | | +- f618(x1) = x1 >= x1 = x1 | | | +- f619(x1,x2,x3,x86,x87,x88,x89) = x3 >= x3 = f21(f615(),f618(x1),f617(x2),f619(x1,x2,x3,x86,x87,x88,x89)) + f616(x3) | | | +- f620(x1,x2,x3,x86,x87,x88,x89) = f620(x1,x2,x3,x86,x87,x88,x89) >= f20(f615(),x1,x2) + x3 = f20(f615(),f618(x1),f617(x2)) + f619(x1,x2,x3,x86,x87,x88,x89) | | | +- f13(x1,x2) = f13(x1,x2) >= f19(f615(),x1,x2) = f19(f615(),f618(x1),f617(x2)) | | | +- f12(x1,x2) = f12(x1,x2) >= f18(f615(),x1,x2) = f18(f615(),f618(x1),f617(x2)) | | | +- f14(x1,x2) + x3 = f14(x1,x2) + x3 >= f620(x1,x2,x3,x86,x87,x88,x89) + 1 = f620(x1,x2,x3,x86,x87,x88,x89) + 1 | | | +- f621(x6) = x6 >= x6 = x6 | | | +- f622(x7) = x7 >= x7 = x7 | | | +- f623(x6) = x6 >= x6 = f621(x6) | | | +- f624(x8) = x8 >= x8 = x8 | | | +- f625(x6,x7,x8) = x6 >= x6 = f3(f622(x7),f624(x8),f625(x6,x7,x8)) + f623(x6) | | | +- f626(x6,x7,x8) = f626(x6,x7,x8) >= f2(x7,x8) + x6 = f2(f622(x7),f624(x8)) + f625(x6,x7,x8) | | | +- f1(x7 + 1,x8 + 1) = f1(x7 + 1,x8 + 1) >= f1(x7,x8) = f1(f622(x7),f624(x8)) | | | +- f2(x7 + 1,x8 + 1) + x6 = f2(x7 + 1,x8 + 1) + x6 >= f626(x6,x7,x8) + 1 = f626(x6,x7,x8) + 1 | | | +- f627(x11) = x11 >= x11 = x11 | | | +- f628(x11) = x11 >= x11 = f627(x11) | | | +- f1(x12 + 1,0) = f1(x12 + 1,0) >= 0 = 0 | | | +- f2(x12 + 1,0) + x11 = f2(x12 + 1,0) + x11 >= x11 + 1 = f628(x11) + 1 | | | +- f629(x15) = x15 >= x15 = x15 | | | +- f630(x15) = x15 >= x15 = f629(x15) | | | +- f1(0,x14) = f1(0,x14) >= 0 = 0 | | | +- f2(0,x14) + x15 = f2(0,x14) + x15 >= x15 + 1 = f630(x15) + 1 | | | +- f631(x19) = x19 >= x19 = x19 | | | +- f632(x19) = x19 >= x19 = f631(x19) | | | +- f19(x16,x17,0) = f19(x16,x17,0) >= 0 = 0 | | | +- f18(x16,x17,0) = f18(x16,x17,0) >= 0 = f633() | | | +- f20(x16,x17,0) + x19 = f20(x16,x17,0) + x19 >= x19 + 1 = f632(x19) + 1 | | | +- f634(x28) = x28 >= x28 = x28 | | | +- f635(x170) = x170 >= x170 = x170 | | | +- f636(x173) = x173 >= x173 = x173 | | | +- f637(x171) = x171 >= x171 = x171 | | | +- f638(x172) = x172 >= x172 = x172 | | | +- f4(x170,x171,f639(x25)) = f4(x170,x171,f639(x25)) >= f15(x170,x171,x25) = f15(f635(x170),f637(x171),x25) | | | +- f5(x170,x171,f639(x25)) + x172 = f5(x170,x171,f639(x25)) + x172 >= f16(x170,x171,x25) + x172 = f16(f635(x170),f637(x171),x25) + f638(x172) | | | +- f6(x170,x171,f639(x25),x172) + x173 = f6(x170,x171,f639(x25),x172) + x173 >= f17(x170,x171,x25,x172) + x173 = f17(f635(x170),f637(x171),x25,f638(x172)) + f636(x173) | | | +- f640(x28) = x28 >= x28 = f634(x28) | | | +- f641(x26) = x26 >= x26 = x26 | | | +- f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = x28 >= x28 = f11(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) ,f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f640(x28) | | | +- f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = x28 >= x28 = f10(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f642(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) | | | +- f647(x238) = x238 >= x238 = x238 | | | +- f648(x241) = x241 >= x241 = x241 | | | +- f649(x239) = x239 >= x239 = x239 | | | +- f650(x240) = x240 >= x240 = x240 | | | +- f15(x238,x239,f651(x25)) = f15(x238,x239,f651(x25)) >= f15(x238,x239,x25) = f15(f647(x238),f649(x239),x25) | | | +- f16(x238,x239,f651(x25)) + x240 = f16(x238,x239,f651(x25)) + x240 >= f16(x238,x239,x25) + x240 = f16(f647(x238),f649(x239),x25) + f650(x240) | | | +- f17(x238,x239,f651(x25),x240) + x241 = f17(x238,x239,f651(x25),x240) + x241 >= f17(x238,x239,x25,x240) + x241 = f17(f647(x238),f649(x239),x25,f650(x240)) + f648(x241) | | | +- f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = x28 >= x28 = f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f653(x30) = x30 >= x30 = x30 | | | +- f654(x26) = x26 >= x26 = x26 | | | +- f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = x28 >= x28 = f21(f651(x25),f654(x26),f653(x30),f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f652(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) | | | +- f644(x25,x26,x30,x238,x239,x240,x241) = f644(x25,x26,x30,x238,x239,x240,x241) >= f19(f651(x25),x26,x30) = f19(f651(x25),f654(x26),f653(x30)) | | | +- f643(x25,x26,x30,x238,x239,x240,x241) = f643(x25,x26,x30,x238,x239,x240,x241) >= f18(f651(x25),x26,x30) = f18(f651(x25),f654(x26),f653(x30)) | | | +- f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f20(f651(x25),x26,x30) + x28 = f20(f651(x25),f654(x26),f653(x30)) + f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f9(f639(x25) ,x26 ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) + f645(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) = f9(f639(x25) ,f641(x26) ,f643(x25 ,x26 ,x30 ,x238 ,x239 ,x240 ,x241) ,f644(x25 ,x26 ,x30 ,x238 ,x239 ,x240 ,x241)) + f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f19(x25,x26,x30 + 1) = f19(x25,x26,x30 + 1) >= f8(f639(x25),x26,f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) = f8(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) | | | +- f18(x25,x26,x30 + 1) = f18(x25,x26,x30 + 1) >= f7(f639(x25),x26,f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) = f7(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) | | | +- f20(x25,x26,x30 + 1) + x28 = f20(x25,x26,x30 + 1) + x28 >= f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 | | | +- f657(x36) = x36 >= x36 = x36 | | | +- f658(x39) = x39 >= x39 = x39 | | | +- f659(x37) = x37 >= x37 = x37 | | | +- f660(x35,x36,x37,x39) = f660(x35,x36,x37,x39) >= f6(x36,x37,x35,f660(x35,x36,x37,x39)) + x39 = f6(f657(x36),f659(x37),x35,f660(x35,x36,x37,x39)) + f658(x39) | | | +- f661(x35,x36,x37,x39) = f661(x35,x36,x37,x39) >= f5(x36,x37,x35) + f660(x35,x36,x37,x39) = f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) | | | +- f662(x36,x37) = f662(x36,x37) >= x36 = x36 | | | +- f663(x35,x36,x37,x39) = f663(x35,x36,x37,x39) >= f661(x35,x36,x37,x39) = f661(x35,x36,x37,x39) | | | +- f664(x35,x36,x37,x39) = f664(x35,x36,x37,x39) >= f663(x35,x36,x37,x39) = f663(x35,x36,x37,x39) | | | +- f665(x37) = x37 >= x37 = x37 | | | +- f666(x35,x36,x37,x39) = f666(x35,x36,x37,x39) >= f664(x35,x36,x37,x39) = f664(x35,x36,x37,x39) | | | +- f667(x41) = x41 >= x41 = x41 | | | +- f668(x35,x36,x37,x39) = f668(x35,x36,x37,x39) >= f666(x35,x36,x37,x39) = f666(x35,x36,x37,x39) | | | +- f669(x41) = x41 + 1 >= x41 + 1 = f667(x41) + 1 | | | +- f662(x36,x37) = f662(x36,x37) >= x37 = f665(x37) | | | +- f670(x35,x36,x37,x39) = f670(x35,x36,x37,x39) >= f668(x35,x36,x37,x39) = f668(x35,x36,x37,x39) | | | +- f671(x35,x36,x37,x39) = f671(x35,x36,x37,x39) >= f670(x35,x36,x37,x39) = f670(x35,x36,x37,x39) | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) >= f662(x36,x37) = f662(x36,x37) | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) >= (x41 + 1) + 1 = f669(x41) + 1 | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f671(x35,x36,x37,x39) + 1 = f671(x35,x36,x37,x39) + 1 | | | +- f675(x35,x36,x37,x39) = f675(x35,x36,x37,x39) >= f5(x36,x37,x35) + f660(x35,x36,x37,x39) = f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) | | | +- f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) >= x37 = x37 | | | +- f677(x35,x36,x37,x39) = f677(x35,x36,x37,x39) >= f675(x35,x36,x37,x39) = f675(x35,x36,x37,x39) | | | +- f678(x35,x36,x37,x39) = f678(x35,x36,x37,x39) >= f677(x35,x36,x37,x39) = f677(x35,x36,x37,x39) | | | +- f679(x475) = x475 >= x475 = x475 | | | +- f680(x478) = x478 >= x478 = x478 | | | +- f681(x476) = x476 >= x476 = x476 | | | +- f682(x477) = x477 >= x477 = x477 | | | +- f4(x475,x476,f683(x35)) = f4(x475,x476,f683(x35)) >= f4(x475,x476,x35) = f4(f679(x475),f681(x476),x35) | | | +- f5(x475,x476,f683(x35)) + x477 = f5(x475,x476,f683(x35)) + x477 >= f5(x475,x476,x35) + x477 = f5(f679(x475),f681(x476),x35) + f682(x477) | | | +- f6(x475,x476,f683(x35),x477) + x478 = f6(x475,x476,f683(x35),x477) + x478 >= f6(x475,x476,x35,x477) + x478 = f6(f679(x475),f681(x476),x35,f682(x477)) + f680(x478) | | | +- f684(x35,x36,x37,x39) = f684(x35,x36,x37,x39) >= f678(x35,x36,x37,x39) = f678(x35,x36,x37,x39) | | | +- f685(x36) = x36 >= x36 = x36 | | | +- f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f684(x35,x36,x37,x39) = f11(f683(x35) ,f685(x36) ,f687(x37) ,f688(x41) ,f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) ,f686(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f684(x35,x36,x37,x39) | | | +- f688(x41) = x41 >= x41 = x41 | | | +- f687(x37) = x37 >= x37 = x37 | | | +- f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f10(f683(x35) ,f685(x36) ,f687(x37) ,f688(x41) ,f689(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f690(x35,x36,x37,x41,x475,x476,x477,x478) = f690(x35,x36,x37,x41,x475,x476,x477,x478) >= f8(f683(x35),x36,x37,x41) = f8(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) >= f7(f683(x35),x36,x37,x41) = f7(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f9(f683(x35),x36,x37,x41) + f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f9(f683(x35) ,f685(x36) ,f687(x37) ,f688(x41)) + f689(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478) | | | +- f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) >= f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 = f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) >= f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 | | | +- f8(x35,x36,x37,x41 + 1) = f8(x35,x36,x37,x41 + 1) >= f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f7(x35,x36,x37,x41 + 1) = f7(x35,x36,x37,x41 + 1) >= f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f9(x35,x36,x37,x41 + 1) + x39 = f9(x35,x36,x37,x41 + 1) + x39 >= f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f693(x50) = x50 >= x50 = x50 | | | +- f694(x47) = f694(x47) >= x47 = x47 | | | +- f695(x50) = x50 >= x50 = f693(x50) | | | +- f696(x50) = x50 >= x50 = f695(x50) | | | +- f697() = 0 >= 0 = 0 | | | +- f694(x47) = f694(x47) >= 0 = f698() | | | +- f699(x50) = x50 >= x50 = f696(x50) | | | +- f700(x50) = x50 >= x50 = f699(x50) | | | +- f8(x46,x47,x48,0) = f8(x46,x47,x48,0) >= 1 = f697() + 1 | | | +- f7(x46,x47,x48,0) = f7(x46,x47,x48,0) >= f694(x47) = f694(x47) | | | `- f9(x46,x47,x48,0) + x50 = f9(x46,x47,x48,0) + x50 >= x50 + 1 = f700(x50) + 1 | +- SCC-DECOMPOSE ... | | | +- SCC: 29 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.131327 UTC | | | +- Open Constraints | | | | | +- f694(x47) = f694(x47) >= x47 = x47 | | | | | `- f694(0) = f694(0) >= 0 = 0 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.131409 UTC | | | | | +- Interpretation | | | | | | | `- f694(x0) = x0 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.136535 UTC(+0.005126s) | | | +- Interpretation | | | | | `- f694(x0) = x0 | | | +- Constraints | | | | | +- f694(x47) = x47 >= x47 = x47 | | | | | `- f694(0) = 0 >= 0 = 0 | | | `- Stopping timer: 2017-03-30 07:35:56.136588 UTC(+0.005261s) | +- SCC-DECOMPOSE ... | | | +- SCC: 28 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.142208 UTC | | | +- Open Constraints | | | | | +- f2(x7 + 1,x8 + 1) + x6 = f2(x7 + 1,x8 + 1) + x6 >= f626(x6,x7,x8) + 1 = f626(x6,x7,x8) + 1 | | | | | +- f2(1,0) + x11 = f2(1,0) + x11 >= x11 + 1 = x11 + 1 | | | | | +- f2(0,0) + x15 = f2(0,0) + x15 >= x15 + 1 = x15 + 1 | | | | | `- f626(x6,x7,x8) = f626(x6,x7,x8) >= f2(x7,x8) + x6 = f2(x7,x8) + x6 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.14231 UTC | | | | | +- Interpretation | | | | | | | +- f2(x0,x1) = 14 + x0 + x1 | | | | | | | `- f626(x0,x1,x2) = max(14 + x0 + x1 + x2,15 + x0) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f2(x0,x1) = 1 + x0 | | | | | | | `- f626(x0,x1,x2) = 1 + x0 + x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.162922 UTC(+0.020612s) | | | +- Interpretation | | | | | +- f2(x0,x1) = 1 + x0 | | | | | `- f626(x0,x1,x2) = 1 + x0 + x1 | | | +- Constraints | | | | | +- f2(x7 + 1,x8 + 1) + x6 = (1 + (x7 + 1)) + x6 >= (1 + (x6 + x7)) + 1 = f626(x6,x7,x8) + 1 | | | | | +- f2(1,0) + x11 = 2 + x11 >= x11 + 1 = x11 + 1 | | | | | +- f2(0,0) + x15 = 1 + x15 >= x15 + 1 = x15 + 1 | | | | | `- f626(x6,x7,x8) = 1 + (x6 + x7) >= (1 + x7) + x6 = f2(x7,x8) + x6 | | | `- Stopping timer: 2017-03-30 07:35:56.162984 UTC(+0.020776s) | +- SCC-DECOMPOSE ... | | | +- SCC: 27 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.167259 UTC | | | +- Open Constraints | | | | | +- f662(x36,0) = f662(x36,0) >= x36 = x36 | | | | | `- f662(0,x37) = f662(0,x37) >= x37 = x37 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.167321 UTC | | | | | +- Interpretation | | | | | | | `- f662(x0,x1) = x0 + x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax ... | | | | | +- Interpretation | | | | | | | `- f662(x0,x1) = max(x1,x0) | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.175414 UTC(+0.008093s) | | | +- Interpretation | | | | | `- f662(x0,x1) = max(x1,x0) | | | +- Constraints | | | | | +- f662(x36,0) = x36 >= x36 = x36 | | | | | `- f662(0,x37) = x37 >= x37 = x37 | | | `- Stopping timer: 2017-03-30 07:35:56.175464 UTC(+0.008205s) | +- SCC-DECOMPOSE ... | | | +- SCC: 26 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.17951 UTC | | | +- Open Constraints | | | | | +- f1(x7 + 1,x8 + 1) = f1(x7 + 1,x8 + 1) >= f1(x7,x8) = f1(x7,x8) | | | | | +- f1(1,0) = f1(1,0) >= 0 = 0 | | | | | `- f1(0,0) = f1(0,0) >= 0 = 0 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.179627 UTC | | | | | +- Interpretation | | | | | | | `- f1(x0,x1) = x0 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | `- f1(x0,x1) = 0 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.187605 UTC(+0.007978s) | | | +- Interpretation | | | | | `- f1(x0,x1) = 0 | | | +- Constraints | | | | | +- f1(x7 + 1,x8 + 1) = 0 >= 0 = f1(x7,x8) | | | | | +- f1(1,0) = 0 >= 0 = 0 | | | | | `- f1(0,0) = 0 >= 0 = 0 | | | `- Stopping timer: 2017-03-30 07:35:56.187655 UTC(+0.008145s) | +- SCC-DECOMPOSE ... | | | +- SCC: 25 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.191424 UTC | | | +- Open Constraints | | | | | +- f15(x86,x87,f615()) = f15(x86,x87,f615()) >= 0 = f1(x86,x87) | | | | | +- f16(x86,x87,f615()) + x88 = f16(x86,x87,f615()) + x88 >= (1 + x86) + x88 = f2(x86,x87) + x88 | | | | | +- f17(x86,x87,f615(),x88) + x89 = f17(x86,x87,f615(),x88) + x89 >= x89 = x89 | | | | | +- f17(x238,x239,f651(x25),x240) + x241 = f17(x238,x239,f651(x25),x240) + x241 >= f17(x238,x239,x25,x240) + x241 = f17(x238,x239,x25,x240) + x241 | | | | | +- f16(x238,x239,f651(x25)) + x240 = f16(x238,x239,f651(x25)) + x240 >= f16(x238,x239,x25) + x240 = f16(x238,x239,x25) + x240 | | | | | `- f15(x238,x239,f651(x25)) = f15(x238,x239,f651(x25)) >= f15(x238,x239,x25) = f15(x238,x239,x25) | | | +- Simplification ... | | | | | `- Substituted: f17(x86,x87,f615(),x88) + x89 ≥ x89 ↦ f17(0,0,f615(),0) + x89 ≥ x89 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.191547 UTC | | | | | +- Interpretation | | | | | | | +- f15(x0,x1,x2) = max(15 + x2,x0 + x1 + x2) | | | | | | | +- f16(x0,x1,x2) = max(15 + x0 + x2,15 + x1) | | | | | | | +- f17(x0,x1,x2,x3) = max(14 + x0 + x1 + x2,15 + x2,14 + x3) | | | | | | | +- f615() = 0 | | | | | | | `- f651(x0) = 15 + x0 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f15(x0,x1,x2) = 0 | | | | | | | +- f16(x0,x1,x2) = max(1 + x0,2) | | | | | | | +- f17(x0,x1,x2,x3) = 0 | | | | | | | +- f615() = 0 | | | | | | | `- f651(x0) = 0 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f15(x0,x1,x2) = 0 | | | | | | | +- f16(x0,x1,x2) = 1 + x0 | | | | | | | +- f17(x0,x1,x2,x3) = 0 | | | | | | | +- f615() = 0 | | | | | | | `- f651(x0) = 0 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.238366 UTC(+0.046819s) | | | +- Interpretation | | | | | +- f1(x0,x1) = 0 | | | | | +- f15(x0,x1,x2) = 0 | | | | | +- f16(x0,x1,x2) = 1 + x0 | | | | | +- f17(x0,x1,x2,x3) = 0 | | | | | +- f2(x0,x1) = 1 + x0 | | | | | +- f615() = 0 | | | | | `- f651(x0) = 0 | | | +- Constraints | | | | | +- f15(x86,x87,f615()) = 0 >= 0 = f1(x86,x87) | | | | | +- f16(x86,x87,f615()) + x88 = (1 + x86) + x88 >= (1 + x86) + x88 = f2(x86,x87) + x88 | | | | | +- f17(x86,x87,f615(),x88) + x89 = x89 >= x89 = x89 | | | | | +- f17(x238,x239,f651(x25),x240) + x241 = x241 >= x241 = f17(x238,x239,x25,x240) + x241 | | | | | +- f16(x238,x239,f651(x25)) + x240 = (1 + x238) + x240 >= (1 + x238) + x240 = f16(x238,x239,x25) + x240 | | | | | `- f15(x238,x239,f651(x25)) = 0 >= 0 = f15(x238,x239,x25) | | | `- Stopping timer: 2017-03-30 07:35:56.23846 UTC(+0.047036s) | +- SCC-DECOMPOSE ... | | | +- SCC: 24 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.2415 UTC | | | +- Open Constraints | | | | | +- f4(x170,x171,f639(x25)) = f4(x170,x171,f639(x25)) >= 0 = f15(x170,x171,x25) | | | | | +- f5(x170,x171,f639(x25)) + x172 = f5(x170,x171,f639(x25)) + x172 >= (1 + x170) + x172 = f16(x170,x171,x25) + x172 | | | | | +- f6(x170,x171,f639(x25),x172) + x173 = f6(x170,x171,f639(x25),x172) + x173 >= x173 = f17(x170,x171,x25,x172) + x173 | | | | | +- f6(x475,x476,f683(x35),x477) + x478 = f6(x475,x476,f683(x35),x477) + x478 >= f6(x475,x476,x35,x477) + x478 = f6(x475,x476,x35,x477) + x478 | | | | | +- f5(x475,x476,f683(x35)) + x477 = f5(x475,x476,f683(x35)) + x477 >= f5(x475,x476,x35) + x477 = f5(x475,x476,x35) + x477 | | | | | `- f4(x475,x476,f683(x35)) = f4(x475,x476,f683(x35)) >= f4(x475,x476,x35) = f4(x475,x476,x35) | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.241622 UTC | | | | | +- Interpretation | | | | | | | +- f4(x0,x1,x2) = max(1 + x1 + x2,10 + x0 + x2) | | | | | | | +- f5(x0,x1,x2) = max(1 + x2,x0 + x2) | | | | | | | +- f6(x0,x1,x2,x3) = max(5 + x2,9) | | | | | | | +- f639(x0) = 15 | | | | | | | `- f683(x0) = 5 + x0 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f4(x0,x1,x2) = 0 | | | | | | | +- f5(x0,x1,x2) = 1 + x0 | | | | | | | +- f6(x0,x1,x2,x3) = 0 | | | | | | | +- f639(x0) = 0 | | | | | | | `- f683(x0) = 0 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.282649 UTC(+0.041027s) | | | +- Interpretation | | | | | +- f15(x0,x1,x2) = 0 | | | | | +- f16(x0,x1,x2) = 1 + x0 | | | | | +- f17(x0,x1,x2,x3) = 0 | | | | | +- f4(x0,x1,x2) = 0 | | | | | +- f5(x0,x1,x2) = 1 + x0 | | | | | +- f6(x0,x1,x2,x3) = 0 | | | | | +- f639(x0) = 0 | | | | | `- f683(x0) = 0 | | | +- Constraints | | | | | +- f4(x170,x171,f639(x25)) = 0 >= 0 = f15(x170,x171,x25) | | | | | +- f5(x170,x171,f639(x25)) + x172 = (1 + x170) + x172 >= (1 + x170) + x172 = f16(x170,x171,x25) + x172 | | | | | +- f6(x170,x171,f639(x25),x172) + x173 = x173 >= x173 = f17(x170,x171,x25,x172) + x173 | | | | | +- f6(x475,x476,f683(x35),x477) + x478 = x478 >= x478 = f6(x475,x476,x35,x477) + x478 | | | | | +- f5(x475,x476,f683(x35)) + x477 = (1 + x475) + x477 >= (1 + x475) + x477 = f5(x475,x476,x35) + x477 | | | | | `- f4(x475,x476,f683(x35)) = 0 >= 0 = f4(x475,x476,x35) | | | `- Stopping timer: 2017-03-30 07:35:56.282747 UTC(+0.041247s) | +- SCC-DECOMPOSE ... | | | +- SCC: 23 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.285066 UTC | | | +- Open Constraints | | | | | +- f676(x35,x36,x37,x41,0,0,0,0) = f676(x35,x36,x37,x41,0,0,0,0) >= f7(0,x36,x37,x41) = f7(f683(x35),x36,x37,x41) | | | | | +- f676(0,0,x37,0,0,0,0,0) = f676(0,0,x37,0,0,0,0,0) >= x37 = x37 | | | | | +- f7(x35,x36,x37,x41 + 1) = f7(x35,x36,x37,x41 + 1) >= f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) | | | | | +- f672(0,x36,x37,0,0,0,0,0) = f672(0,x36,x37,0,0,0,0,0) >= max(x37,x36) = f662(x36,x37) | | | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = f672(x35,x36,x37,x41,x475,x476,x477,x478) >= f676(x35,x36,x37,x41,x475,x476,x477,x478) = f676(x35,x36,x37,x41,x475,x476,x477,x478) | | | | | `- f7(0,x47,0,0) = f7(0,x47,0,0) >= x47 = f694(x47) | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.285221 UTC | | | | | +- Interpretation | | | | | | | +- f672(x0,x1,x2,x3,x4,x5,x6,x7) = max(1 + x0 + x1,8 + x1 + x2) | | | | | | | +- f676(x0,x1,x2,x3,x4,x5,x6,x7) = max(8 + x1 + x2,x0 + x1) | | | | | | | `- f7(x0,x1,x2,x3) = 8 + x0 + x1 + x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f672(x0,x1,x2,x3,x4,x5,x6,x7) = x1 + x2 | | | | | | | +- f676(x0,x1,x2,x3,x4,x5,x6,x7) = x1 + x2 | | | | | | | `- f7(x0,x1,x2,x3) = x0 + x1 + x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f672(x0,x1,x2,x3,x4,x5,x6,x7) = x1 + x2 | | | | | | | +- f676(x0,x1,x2,x3,x4,x5,x6,x7) = x1 + x2 | | | | | | | `- f7(x0,x1,x2,x3) = x1 + x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax ... | | | | | +- Interpretation | | | | | | | +- f672(x0,x1,x2,x3,x4,x5,x6,x7) = max(x2,x1) | | | | | | | +- f676(x0,x1,x2,x3,x4,x5,x6,x7) = max(x1,x2) | | | | | | | `- f7(x0,x1,x2,x3) = max(x2,x1) | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.385062 UTC(+0.099841s) | | | +- Interpretation | | | | | +- f662(x0,x1) = max(x1,x0) | | | | | +- f672(x0,x1,x2,x3,x4,x5,x6,x7) = max(x2,x1) | | | | | +- f676(x0,x1,x2,x3,x4,x5,x6,x7) = max(x1,x2) | | | | | +- f683(x0) = 0 | | | | | +- f694(x0) = x0 | | | | | `- f7(x0,x1,x2,x3) = max(x2,x1) | | | +- Constraints | | | | | +- f676(x35,x36,x37,x41,0,0,0,0) = max(x36,x37) >= max(x37,x36) = f7(f683(x35),x36,x37,x41) | | | | | +- f676(0,0,x37,0,0,0,0,0) = x37 >= x37 = x37 | | | | | +- f7(x35,x36,x37,x41 + 1) = max(x37,x36) >= max(x37,x36) = f672(x35,x36,x37,x41,x475,x476,x477,x478) | | | | | +- f672(0,x36,x37,0,0,0,0,0) = max(x37,x36) >= max(x37,x36) = f662(x36,x37) | | | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = max(x37,x36) >= max(x36,x37) = f676(x35,x36,x37,x41,x475,x476,x477,x478) | | | | | `- f7(0,x47,0,0) = x47 >= x47 = f694(x47) | | | `- Stopping timer: 2017-03-30 07:35:56.38516 UTC(+0.100094s) | +- SCC-DECOMPOSE ... | | | +- SCC: 22 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.387025 UTC | | | +- Open Constraints | | | | | `- f660(x35,x36,x37,x39) = f660(x35,x36,x37,x39) >= x39 = f6(x36,x37,x35,f660(x35,x36,x37,x39)) + x39 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.387112 UTC | | | | | +- Interpretation | | | | | | | `- f660(x0,x1,x2,x3) = max(15,4 + x0 + x1 + x2 + x3) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | `- f660(x0,x1,x2,x3) = x2 + x3 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | `- f660(x0,x1,x2,x3) = x3 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.404493 UTC(+0.017381s) | | | +- Interpretation | | | | | +- f6(x0,x1,x2,x3) = 0 | | | | | `- f660(x0,x1,x2,x3) = x3 | | | +- Constraints | | | | | `- f660(x35,x36,x37,x39) = x39 >= x39 = f6(x36,x37,x35,f660(x35,x36,x37,x39)) + x39 | | | `- Stopping timer: 2017-03-30 07:35:56.404555 UTC(+0.01753s) | +- SCC-DECOMPOSE ... | | | +- SCC: 21 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.406254 UTC | | | +- Open Constraints | | | | | +- f690(x35,x36,x37,x41,0,0,0,0) = f690(x35,x36,x37,x41,0,0,0,0) >= f8(0,x36,x37,x41) = f8(f683(x35),x36,x37,x41) | | | | | +- f8(x35,x36,x37,x41 + 1) = f8(x35,x36,x37,x41 + 1) >= f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) | | | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = f673(x35,x36,x37,x41,x475,x476,x477,x478) >= f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 = f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 | | | | | +- f673(0,0,0,x41,0,0,0,0) = f673(0,0,0,x41,0,0,0,0) >= (x41 + 1) + 1 = (x41 + 1) + 1 | | | | | `- f8(0,0,0,0) = f8(0,0,0,0) >= 1 = 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.406395 UTC | | | | | +- Interpretation | | | | | | | +- f673(x0,x1,x2,x3,x4,x5,x6,x7) = max(12 + x1 + x2 + x3,14 + x3,11 + x0 + x1 + x3) | | | | | | | +- f690(x0,x1,x2,x3,x4,x5,x6,x7) = max(x0 + x3,13 + x3,11 + x1 + x2 + x3) | | | | | | | `- f8(x0,x1,x2,x3) = max(13 + x3,11 + x0 + x1 + x2 + x3) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f673(x0,x1,x2,x3,x4,x5,x6,x7) = 2 + x3 | | | | | | | +- f690(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x3 | | | | | | | `- f8(x0,x1,x2,x3) = max(1 + x3,1 + x0) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f673(x0,x1,x2,x3,x4,x5,x6,x7) = 2 + x3 | | | | | | | +- f690(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x3 | | | | | | | `- f8(x0,x1,x2,x3) = max(1 + x3,x0) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f673(x0,x1,x2,x3,x4,x5,x6,x7) = 2 + x3 | | | | | | | +- f690(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x3 | | | | | | | `- f8(x0,x1,x2,x3) = 1 + x3 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.510352 UTC(+0.103957s) | | | +- Interpretation | | | | | +- f673(x0,x1,x2,x3,x4,x5,x6,x7) = 2 + x3 | | | | | +- f683(x0) = 0 | | | | | +- f690(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x3 | | | | | `- f8(x0,x1,x2,x3) = 1 + x3 | | | +- Constraints | | | | | +- f690(x35,x36,x37,x41,0,0,0,0) = 1 + x41 >= 1 + x41 = f8(f683(x35),x36,x37,x41) | | | | | +- f8(x35,x36,x37,x41 + 1) = 1 + (x41 + 1) >= 2 + x41 = f673(x35,x36,x37,x41,x475,x476,x477,x478) | | | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = 2 + x41 >= (1 + x41) + 1 = f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 | | | | | +- f673(0,0,0,x41,0,0,0,0) = 2 + x41 >= (x41 + 1) + 1 = (x41 + 1) + 1 | | | | | `- f8(0,0,0,0) = 1 >= 1 = 1 | | | `- Stopping timer: 2017-03-30 07:35:56.510486 UTC(+0.104232s) | +- SCC-DECOMPOSE ... | | | +- SCC: 20 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.511785 UTC | | | +- Open Constraints | | | | | `- f661(x35,x36,x37,x39) = f661(x35,x36,x37,x39) >= (1 + x36) + x39 = f5(x36,x37,x35) + f660(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f661(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f5(x0,x1,x2) = 1 + x0 | | | | | +- f660(x0,x1,x2,x3) = x3 | | | | | `- f661(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f661(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f5(x36,x37,x35) + f660(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.511883 UTC(+0.000098s) | +- SCC-DECOMPOSE ... | | | +- SCC: 19 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.513058 UTC | | | +- Open Constraints | | | | | +- f19(x25,x26,x30 + 1) = f19(x25,x26,x30 + 1) >= 1 + f644(x25,x26,x30,x238,x239,x240,x241) = f8(f639(x25),x26,f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) | | | | | +- f643(x25,x26,x30,0,0,0,0) = f643(x25,x26,x30,0,0,0,0) >= f18(0,x26,x30) = f18(f651(x25),x26,x30) | | | | | +- f18(x25,x26,x30 + 1) = f18(x25,x26,x30 + 1) >= max(f643(x25,x26,x30,x238,x239,x240,x241),x26) = f7(f639(x25),x26,f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) | | | | | +- f18(0,0,0) = f18(0,0,0) >= 0 = 0 | | | | | +- f644(x25,x26,x30,0,0,0,0) = f644(x25,x26,x30,0,0,0,0) >= f19(0,x26,x30) = f19(f651(x25),x26,x30) | | | | | `- f19(0,0,0) = f19(0,0,0) >= 0 = 0 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.513179 UTC | | | | | +- Interpretation | | | | | | | +- f18(x0,x1,x2) = max(7 + x0 + x2,15,13 + x1 + x2) | | | | | | | +- f19(x0,x1,x2) = max(15 + x0,15 + x1 + x2) | | | | | | | +- f643(x0,x1,x2,x3,x4,x5,x6) = max(5 + x0,15,14 + x1 + x2) | | | | | | | `- f644(x0,x1,x2,x3,x4,x5,x6) = max(15 + x1 + x2,12 + x0) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f18(x0,x1,x2) = 1 + x1 | | | | | | | +- f19(x0,x1,x2) = 1 + x2 | | | | | | | +- f643(x0,x1,x2,x3,x4,x5,x6) = 1 + x1 | | | | | | | `- f644(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f18(x0,x1,x2) = x1 | | | | | | | +- f19(x0,x1,x2) = 1 + x2 | | | | | | | +- f643(x0,x1,x2,x3,x4,x5,x6) = x1 | | | | | | | `- f644(x0,x1,x2,x3,x4,x5,x6) = 1 + x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f18(x0,x1,x2) = x1 | | | | | | | +- f19(x0,x1,x2) = x2 | | | | | | | +- f643(x0,x1,x2,x3,x4,x5,x6) = x1 | | | | | | | `- f644(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.611578 UTC(+0.098399s) | | | +- Interpretation | | | | | +- f18(x0,x1,x2) = x1 | | | | | +- f19(x0,x1,x2) = x2 | | | | | +- f639(x0) = 0 | | | | | +- f643(x0,x1,x2,x3,x4,x5,x6) = x1 | | | | | +- f644(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f651(x0) = 0 | | | | | +- f7(x0,x1,x2,x3) = max(x2,x1) | | | | | `- f8(x0,x1,x2,x3) = 1 + x3 | | | +- Constraints | | | | | +- f19(x25,x26,x30 + 1) = x30 + 1 >= 1 + x30 = f8(f639(x25),x26,f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) | | | | | +- f643(x25,x26,x30,0,0,0,0) = x26 >= x26 = f18(f651(x25),x26,x30) | | | | | +- f18(x25,x26,x30 + 1) = x26 >= max(x26,x26) = f7(f639(x25),x26,f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) | | | | | +- f18(0,0,0) = 0 >= 0 = 0 | | | | | +- f644(x25,x26,x30,0,0,0,0) = x30 >= x30 = f19(f651(x25),x26,x30) | | | | | `- f19(0,0,0) = 0 >= 0 = 0 | | | `- Stopping timer: 2017-03-30 07:35:56.611678 UTC(+0.09862s) | +- SCC-DECOMPOSE ... | | | +- SCC: 18 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.612552 UTC | | | +- Open Constraints | | | | | `- f663(x35,x36,x37,x39) = f663(x35,x36,x37,x39) >= (1 + x36) + x39 = f661(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f663(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f661(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f663(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f663(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f661(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.612638 UTC(+0.000086s) | +- SCC-DECOMPOSE ... | | | +- SCC: 17 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.613427 UTC | | | +- Open Constraints | | | | | `- f12(x1,x2) = f12(x1,x2) >= x1 = f18(f615(),x1,x2) | | | +- Simplification ... | | | | | `- Propagated: f12(x0,x1) ↦ x0 | | | +- Interpretation | | | | | +- f12(x0,x1) = x0 | | | | | +- f18(x0,x1,x2) = x1 | | | | | `- f615() = 0 | | | +- Constraints | | | | | `- f12(x1,x2) = x1 >= x1 = f18(f615(),x1,x2) | | | `- Stopping timer: 2017-03-30 07:35:56.613497 UTC(+0.00007s) | +- SCC-DECOMPOSE ... | | | +- SCC: 16 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.614197 UTC | | | +- Open Constraints | | | | | `- f664(x35,x36,x37,x39) = f664(x35,x36,x37,x39) >= (1 + x36) + x39 = f663(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f664(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f663(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f664(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f664(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f663(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.614262 UTC(+0.000065s) | +- SCC-DECOMPOSE ... | | | +- SCC: 15 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.614916 UTC | | | +- Open Constraints | | | | | `- f13(x1,x2) = f13(x1,x2) >= x2 = f19(f615(),x1,x2) | | | +- Simplification ... | | | | | `- Propagated: f13(x0,x1) ↦ x1 | | | +- Interpretation | | | | | +- f13(x0,x1) = x1 | | | | | +- f19(x0,x1,x2) = x2 | | | | | `- f615() = 0 | | | +- Constraints | | | | | `- f13(x1,x2) = x2 >= x2 = f19(f615(),x1,x2) | | | `- Stopping timer: 2017-03-30 07:35:56.615017 UTC(+0.000101s) | +- SCC-DECOMPOSE ... | | | +- SCC: 14 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.615605 UTC | | | +- Open Constraints | | | | | `- f666(x35,x36,x37,x39) = f666(x35,x36,x37,x39) >= (1 + x36) + x39 = f664(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f666(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f664(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f666(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f666(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f664(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.615705 UTC(+0.0001s) | +- SCC-DECOMPOSE ... | | | +- SCC: 13 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.616957 UTC | | | +- Open Constraints | | | | | `- f675(x35,x36,x37,x39) = f675(x35,x36,x37,x39) >= (1 + x36) + x39 = f5(x36,x37,x35) + f660(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f675(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f5(x0,x1,x2) = 1 + x0 | | | | | +- f660(x0,x1,x2,x3) = x3 | | | | | `- f675(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f675(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f5(x36,x37,x35) + f660(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.617051 UTC(+0.000094s) | +- SCC-DECOMPOSE ... | | | +- SCC: 12 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.617606 UTC | | | +- Open Constraints | | | | | `- f668(x35,x36,x37,x39) = f668(x35,x36,x37,x39) >= (1 + x36) + x39 = f666(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f668(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f666(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f668(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f668(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f666(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.617673 UTC(+0.000067s) | +- SCC-DECOMPOSE ... | | | +- SCC: 11 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.618159 UTC | | | +- Open Constraints | | | | | `- f677(x35,x36,x37,x39) = f677(x35,x36,x37,x39) >= (1 + x36) + x39 = f675(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f677(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f675(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f677(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f677(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f675(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.618224 UTC(+0.000065s) | +- SCC-DECOMPOSE ... | | | +- SCC: 10 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.618675 UTC | | | +- Open Constraints | | | | | `- f670(x35,x36,x37,x39) = f670(x35,x36,x37,x39) >= (1 + x36) + x39 = f668(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f670(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f668(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f670(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f670(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f668(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.618741 UTC(+0.000066s) | +- SCC-DECOMPOSE ... | | | +- SCC: 9 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.619155 UTC | | | +- Open Constraints | | | | | `- f678(x35,x36,x37,x39) = f678(x35,x36,x37,x39) >= (1 + x36) + x39 = f677(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f678(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f677(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f678(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f678(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f677(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.619221 UTC(+0.000066s) | +- SCC-DECOMPOSE ... | | | +- SCC: 8 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.619602 UTC | | | +- Open Constraints | | | | | `- f671(x35,x36,x37,x39) = f671(x35,x36,x37,x39) >= (1 + x36) + x39 = f670(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f671(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f670(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f671(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f671(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f670(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.619669 UTC(+0.000067s) | +- SCC-DECOMPOSE ... | | | +- SCC: 7 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.620019 UTC | | | +- Open Constraints | | | | | `- f684(x35,x36,x37,x39) = f684(x35,x36,x37,x39) >= (1 + x36) + x39 = f678(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Propagated: f684(x0,x1,x2,x3) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f678(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f684(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f684(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f678(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.620085 UTC(+0.000066s) | +- SCC-DECOMPOSE ... | | | +- SCC: 6 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.620372 UTC | | | +- Open Constraints | | | | | `- f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= (1 + x36) + x39 = f684(x35,x36,x37,x39) | | | +- Simplification ... | | | | | `- Substituted: f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) ≥ f684(x35,x36,x37,x39) ↦ f686(x35,x36,x37,x39,0,0,0,0,0) ≥ f684(x35,x36,x37,x39) | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.620434 UTC | | | | | +- Interpretation | | | | | | | `- f686(x0,x1,x2,x3,x4,x5,x6,x7,x8) = max(14 + x6 + x8,14 + x0 + x1 + x3,14 + x1 + x2 + x3 + x4 + x5 + x7) | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | `- f686(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.646454 UTC(+0.02602s) | | | +- Interpretation | | | | | +- f684(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | `- f686(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 1 + (x36 + x39) >= (1 + x36) + x39 = f684(x35,x36,x37,x39) | | | `- Stopping timer: 2017-03-30 07:35:56.646522 UTC(+0.02615s) | +- SCC-DECOMPOSE ... | | | +- SCC: 5 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.646822 UTC | | | +- Open Constraints | | | | | `- f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= 1 + (x36 + x39) = f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- Simplification ... | | | | | `- Propagated: f689(x0,x1,x2,x3,x4,x5,x6,x7,x8) ↦ 1 + x1 + x3 | | | +- Interpretation | | | | | +- f686(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3 | | | | | `- f689(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3 | | | +- Constraints | | | | | `- f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 1 + (x36 + x39) >= 1 + (x36 + x39) = f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | `- Stopping timer: 2017-03-30 07:35:56.646918 UTC(+0.000096s) | +- SCC-DECOMPOSE ... | | | +- SCC: 4 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.647147 UTC | | | +- Open Constraints | | | | | +- f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f9(0,x36,x37,x41) + (1 + (x36 + x39)) = f9(f683(x35),x36,x37,x41) + f689(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478) | | | | | +- f9(x35,x36,x37,x41 + 1) + x39 = f9(x35,x36,x37,x41 + 1) + x39 >= f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | | | +- f674(x35,x36,x37,x39,0,0,0,0,0) = f674(x35,x36,x37,x39,0,0,0,0,0) >= ((1 + x36) + x39) + 1 = f671(x35,x36,x37,x39) + 1 | | | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 | | | | | +- f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) >= f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | | | `- f9(0,0,0,0) + x50 = f9(0,0,0,0) + x50 >= x50 + 1 = x50 + 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.647286 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:56.685647 UTC(+0.038361s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.685662 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:56.694104 UTC(+0.008442s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.694111 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:56.704796 UTC(+0.010685s) | | | +- SMT-MMI(2) ... | | | | | +- Staring timer: 2017-03-30 07:35:56.704804 UTC | | | | | +- Interpretation | | | | | | | +- f674(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 16 + 14*x0 + 14*x0*x1 + 12*x0*x2 + 14*x0*x4 + 14*x1 + 14*x1*x2 + 14*x1*x4 + 14*x2 + 14*x2*x4 + x3 + 14*x4 | | | | | | | +- f691(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 12 + x0*x2 + 12*x1 + 14*x1*x2 + 14*x1*x4 + 14*x2*x4 + x3 + 14*x4 | | | | | | | +- f692(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 15 + 14*x0 + 14*x0*x1 + 12*x0*x2 + 14*x0*x4 + 14*x1 + 14*x1*x2 + 14*x1*x4 + 14*x2 + 14*x2*x4 + x3 + 14*x4 | | | | | | | `- f9(x0,x1,x2,x3) = 3 + 15*x0 + 14*x0*x1 + 14*x0*x2 + 15*x0*x3 + 14*x1*x2 + 14*x1*x3 + 14*x2*x3 + 14*x3 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f674(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 3 + x1 + x1*x4 + x3 + 2*x4 | | | | | | | +- f691(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x1 + x1*x4 + x3 + 2*x4 | | | | | | | +- f692(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x1 + x1*x4 + x3 + 2*x4 | | | | | | | `- f9(x0,x1,x2,x3) = 1 + x1*x3 + 2*x3 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:35:56.846557 UTC(+0.141753s) | | | +- Interpretation | | | | | +- f671(x0,x1,x2,x3) = 1 + x1 + x3 | | | | | +- f674(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 3 + x1 + x1*x4 + x3 + 2*x4 | | | | | +- f683(x0) = 0 | | | | | +- f689(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3 | | | | | +- f691(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x1 + x1*x4 + x3 + 2*x4 | | | | | +- f692(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x1 + x1*x4 + x3 + 2*x4 | | | | | `- f9(x0,x1,x2,x3) = 1 + x1*x3 + 2*x3 | | | +- Constraints | | | | | +- f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 2 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) >= (1 + ((x36 * x41) + (2 * x41))) + (1 + (x36 + x39)) = f9(f683(x35),x36,x37,x41) + f689(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478) | | | | | +- f9(x35,x36,x37,x41 + 1) + x39 = (1 + ((x36 * (x41 + 1)) + (2 * (x41 + 1)))) + x39 >= 3 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | | | +- f674(x35,x36,x37,x39,0,0,0,0,0) = 3 + (x36 + x39) >= ((1 + x36) + x39) + 1 = f671(x35,x36,x37,x39) + 1 | | | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 3 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) >= (2 + (x36 + ((x36 * x41) + (x39 + (2 * x41))))) + 1 = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 | | | | | +- f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 2 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) >= 2 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | | | `- f9(0,0,0,0) + x50 = 1 + x50 >= x50 + 1 = x50 + 1 | | | `- Stopping timer: 2017-03-30 07:35:56.846667 UTC(+0.19952s) | +- SCC-DECOMPOSE ... | | | +- SCC: 3 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:35:56.846739 UTC | | | +- Open Constraints | | | | | +- f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= (1 + ((x26 * x30) + (2 * x30))) + f645(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) = f9(f639(x25) ,x26 ,f643(x25 ,x26 ,x30 ,x238 ,x239 ,x240 ,x241) ,f644(x25 ,x26 ,x30 ,x238 ,x239 ,x240 ,x241)) + f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | | | +- f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) >= f20(0,x26,x30) + x28 = f20(f651(x25),x26,x30) + x28 | | | | | +- f20(x25,x26,x30 + 1) + x28 = f20(x25,x26,x30 + 1) + x28 >= f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 | | | | | `- f20(0,0,0) + x19 = f20(0,0,0) + x19 >= x19 + 1 = x19 + 1 | | | +- Simplification ... | | | | | `- Substituted: f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) ≥ f20(f651(x25),x26,x30) + x28 ↦ f645(x25,x26,x28,x30,0,0,0,0,0,0,0,0) ≥ f20(f651(x25),x26,x30) + x28 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.846865 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:56.864639 UTC(+0.017774s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.864653 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:56.870046 UTC(+0.005393s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:35:56.870052 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:56.874821 UTC(+0.004769s) | | | +- SMT-MMI(2) ... | | | | | +- Staring timer: 2017-03-30 07:35:56.874827 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:56.896266 UTC(+0.021439s) | | | +- SMT-MI(2) ... | | | | | +- Staring timer: 2017-03-30 07:35:56.896273 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:57.223939 UTC(+0.327666s) | | | +- SMT-MMI(3) ... | | | | | +- Staring timer: 2017-03-30 07:35:57.223947 UTC | | | | | `- Stopping timer: 2017-03-30 07:35:57.300002 UTC(+0.076055s) | | | +- SMT-MI(3) ... | | | | | +- Staring timer: 2017-03-30 07:35:57.300009 UTC | | | | | +- Interpretation | | | | | | | +- f20(x0,x1,x2) = 1 + 14*x0 + 15*x0*x1 + 15*x0*x1*x2 + 14*x0*x1^2 + 14*x0*x2 + 15*x0*x2^2 + 15*x0^2 + 14*x0^2*x1 + 15*x0^2*x2 + 14*x0^3 + x1*x2 + 15*x1*x2^2 + 14*x1^2*x2 + 14*x1^3 + 4*x2 + 7*x2^2 + 15*x2^3 | | | | | | | +- f645(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 7 + 2*x0*x1 + 14*x1 + 2*x1*x3 + 15*x1*x3^2 + 8*x1^2 + 14*x1^2*x3 + 14*x1^3 + x2 + 6*x3 + 15*x3^2 + 15*x3^3 | | | | | | | `- f656(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 15 + 2*x0 + 12*x0*x1 + 8*x0*x1*x3 + 10*x0*x1^2 + 4*x0*x3 + 15*x1 + 15*x1*x3 + 15*x1*x3^2 + 8*x1^2 + 14*x1^2*x3 + 14*x1^3 + x2 + 8*x3 + 15*x3^2 + 15*x3^3 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f20(x0,x1,x2) = 1 + x1*x2^2 + 2*x2^2 | | | | | | | +- f645(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 1 + x1*x3^2 + x2 + 2*x3^2 | | | | | | | `- f656(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 2 + x1*x3 + x1*x3^2 + x2 + 3*x3 + 2*x3^2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | +- f20(x0,x1,x2) = 1 + x1*x2^2 + 2*x2^2 | | | | | | | +- f645(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 1 + x1*x3^2 + x2 + 2*x3^2 | | | | | | | `- f656(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 2 + x1*x3 + x1*x3^2 + x2 + 2*x3 + 2*x3^2 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:36:08.972773 UTC(+11.672764s) | | | +- Interpretation | | | | | +- f20(x0,x1,x2) = 1 + x1*x2^2 + 2*x2^2 | | | | | +- f639(x0) = 0 | | | | | +- f643(x0,x1,x2,x3,x4,x5,x6) = x1 | | | | | +- f644(x0,x1,x2,x3,x4,x5,x6) = x2 | | | | | +- f645(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 1 + x1*x3^2 + x2 + 2*x3^2 | | | | | +- f651(x0) = 0 | | | | | +- f656(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 2 + x1*x3 + x1*x3^2 + x2 + 2*x3 + 2*x3^2 | | | | | `- f9(x0,x1,x2,x3) = 1 + x1*x3 + 2*x3 | | | +- Constraints | | | | | +- f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = 2 + ((x26 * x30) + ((x26 * (x30 * x30)) + (x28 + ((2 * x30) + (2 * (x30 * x30)))))) >= (1 + ((x26 * x30) + (2 * x30))) + (1 + ((x26 * (x30 * x30)) + (x28 + (2 * (x30 * x30))))) = f9(f639(x25) ,x26 ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) + f645(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) | | | | | +- f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = 1 + ((x26 * (x30 * x30)) + (x28 + (2 * (x30 * x30)))) >= (1 + ((x26 * (x30 * x30)) + (2 * (x30 * x30)))) + x28 = f20(f651(x25),x26,x30) + x28 | | | | | +- f20(x25,x26,x30 + 1) + x28 = (1 + ((x26 * ((x30 + 1) * (x30 + 1))) + (2 * ((x30 + 1) * (x30 + 1))))) + x28 >= (2 + ((x26 * x30) + ((x26 * (x30 * x30)) + (x28 + ((2 * x30) + (2 * (x30 * x30))))))) + 1 = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 | | | | | `- f20(0,0,0) + x19 = 1 + x19 >= x19 + 1 = x19 + 1 | | | `- Stopping timer: 2017-03-30 07:36:08.972888 UTC(+12.126149s) | +- SCC-DECOMPOSE ... | | | +- SCC: 2 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:36:08.972913 UTC | | | +- Open Constraints | | | | | `- f620(x1,x2,x3,x86,x87,x88,x89) = f620(x1,x2,x3,x86,x87,x88,x89) >= (1 + ((x1 * (x2 * x2)) + (2 * (x2 * x2)))) + x3 = f20(f615(),x1,x2) + x3 | | | +- Simplification ... | | | | | `- Substituted: f620(x1,x2,x3,x86,x87,x88,x89) ≥ f20(f615(),x1,x2) + x3 ↦ f620(x1,x2,x3,0,0,0,0) ≥ f20(f615(),x1,x2) + x3 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:36:08.972989 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:08.978313 UTC(+0.005324s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:36:08.978324 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:08.981809 UTC(+0.003485s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:36:08.981815 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:08.984331 UTC(+0.002516s) | | | +- SMT-MMI(2) ... | | | | | +- Staring timer: 2017-03-30 07:36:08.984337 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:08.987824 UTC(+0.003487s) | | | +- SMT-MI(2) ... | | | | | +- Staring timer: 2017-03-30 07:36:08.987829 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:08.991816 UTC(+0.003987s) | | | +- SMT-MMI(3) ... | | | | | +- Staring timer: 2017-03-30 07:36:08.991821 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:08.99683 UTC(+0.005009s) | | | +- SMT-MI(3) ... | | | | | +- Staring timer: 2017-03-30 07:36:08.996836 UTC | | | | | +- Interpretation | | | | | | | `- f620(x0,x1,x2,x3,x4,x5,x6) = 16 + 12*x0*x1^2 + 6*x1^2 + 12*x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f620(x0,x1,x2,x3,x4,x5,x6) = 1 + x0*x1^2 + 2*x1^2 + x2 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:36:09.056081 UTC(+0.059245s) | | | +- Interpretation | | | | | +- f20(x0,x1,x2) = 1 + x1*x2^2 + 2*x2^2 | | | | | +- f615() = 0 | | | | | `- f620(x0,x1,x2,x3,x4,x5,x6) = 1 + x0*x1^2 + 2*x1^2 + x2 | | | +- Constraints | | | | | `- f620(x1,x2,x3,x86,x87,x88,x89) = 1 + ((x1 * (x2 * x2)) + ((2 * (x2 * x2)) + x3)) >= (1 + ((x1 * (x2 * x2)) + (2 * (x2 * x2)))) + x3 = f20(f615(),x1,x2) + x3 | | | `- Stopping timer: 2017-03-30 07:36:09.056149 UTC(+0.083236s) | +- SCC-DECOMPOSE ... | | | +- SCC: 1 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:36:09.056167 UTC | | | +- Open Constraints | | | | | `- f14(x1,x2) + x3 = f14(x1,x2) + x3 >= (1 + ((x1 * (x2 * x2)) + ((2 * (x2 * x2)) + x3))) + 1 = f620(x1,x2,x3,x86,x87,x88,x89) + 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:36:09.056231 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:09.05918 UTC(+0.002949s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:36:09.05919 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:09.061965 UTC(+0.002775s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:36:09.061971 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:09.064605 UTC(+0.002634s) | | | +- SMT-MMI(2) ... | | | | | +- Staring timer: 2017-03-30 07:36:09.06461 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:09.067238 UTC(+0.002628s) | | | +- SMT-MI(2) ... | | | | | +- Staring timer: 2017-03-30 07:36:09.067243 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:09.069881 UTC(+0.002638s) | | | +- SMT-MMI(3) ... | | | | | +- Staring timer: 2017-03-30 07:36:09.069887 UTC | | | | | `- Stopping timer: 2017-03-30 07:36:09.072553 UTC(+0.002666s) | | | +- SMT-MI(3) ... | | | | | +- Staring timer: 2017-03-30 07:36:09.072559 UTC | | | | | +- Interpretation | | | | | | | `- f14(x0,x1) = 14 + 12*x0*x1^2 + 8*x1^2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f14(x0,x1) = 2 + x0*x1^2 + 2*x1^2 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:36:09.0801 UTC(+0.007541s) | | | +- Interpretation | | | | | +- f14(x0,x1) = 2 + x0*x1^2 + 2*x1^2 | | | | | `- f620(x0,x1,x2,x3,x4,x5,x6) = 1 + x0*x1^2 + 2*x1^2 + x2 | | | +- Constraints | | | | | `- f14(x1,x2) + x3 = (2 + ((x1 * (x2 * x2)) + (2 * (x2 * x2)))) + x3 >= (1 + ((x1 * (x2 * x2)) + ((2 * (x2 * x2)) + x3))) + 1 = f620(x1,x2,x3,x86,x87,x88,x89) + 1 | | | `- Stopping timer: 2017-03-30 07:36:09.080162 UTC(+0.023995s) | +- Interpretation | | | +- f1(x0,x1) = 0 | | | +- f10(x0,x1,x2,x3,x4) = 0 | | | +- f11(x0,x1,x2,x3,x4,x5) = 0 | | | +- f12(x0,x1) = x0 | | | +- f13(x0,x1) = x1 | | | +- f14(x0,x1) = 2 + x0*x1^2 + 2*x1^2 | | | +- f15(x0,x1,x2) = 0 | | | +- f16(x0,x1,x2) = 1 + x0 | | | +- f17(x0,x1,x2,x3) = 0 | | | +- f18(x0,x1,x2) = x1 | | | +- f19(x0,x1,x2) = x2 | | | +- f2(x0,x1) = 1 + x0 | | | +- f20(x0,x1,x2) = 1 + x1*x2^2 + 2*x2^2 | | | +- f21(x0,x1,x2,x3) = 0 | | | +- f3(x0,x1,x2) = 0 | | | +- f4(x0,x1,x2) = 0 | | | +- f5(x0,x1,x2) = 1 + x0 | | | +- f6(x0,x1,x2,x3) = 0 | | | +- f609(x0) = x0 | | | +- f610(x0) = x0 | | | +- f611(x0) = x0 | | | +- f612(x0) = x0 | | | +- f613(x0) = x0 | | | +- f614(x0) = x0 | | | +- f615() = 0 | | | +- f616(x0) = x0 | | | +- f617(x0) = x0 | | | +- f618(x0) = x0 | | | +- f619(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f620(x0,x1,x2,x3,x4,x5,x6) = 1 + x0*x1^2 + 2*x1^2 + x2 | | | +- f621(x0) = x0 | | | +- f622(x0) = x0 | | | +- f623(x0) = x0 | | | +- f624(x0) = x0 | | | +- f625(x0,x1,x2) = x0 | | | +- f626(x0,x1,x2) = 1 + x0 + x1 | | | +- f627(x0) = x0 | | | +- f628(x0) = x0 | | | +- f629(x0) = x0 | | | +- f630(x0) = x0 | | | +- f631(x0) = x0 | | | +- f632(x0) = x0 | | | +- f633() = 0 | | | +- f634(x0) = x0 | | | +- f635(x0) = x0 | | | +- f636(x0) = x0 | | | +- f637(x0) = x0 | | | +- f638(x0) = x0 | | | +- f639(x0) = 0 | | | +- f640(x0) = x0 | | | +- f641(x0) = x0 | | | +- f642(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2 | | | +- f643(x0,x1,x2,x3,x4,x5,x6) = x1 | | | +- f644(x0,x1,x2,x3,x4,x5,x6) = x2 | | | +- f645(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 1 + x1*x3^2 + x2 + 2*x3^2 | | | +- f646(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2 | | | +- f647(x0) = x0 | | | +- f648(x0) = x0 | | | +- f649(x0) = x0 | | | +- f650(x0) = x0 | | | +- f651(x0) = 0 | | | +- f652(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2 | | | +- f653(x0) = x0 | | | +- f654(x0) = x0 | | | +- f655(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = x2 | | | +- f656(x0,x1,x2,x3,x4,x5,x6,x7,x8,x9,x10,x11) = 2 + x1*x3 + x1*x3^2 + x2 + 2*x3 + 2*x3^2 | | | +- f657(x0) = x0 | | | +- f658(x0) = x0 | | | +- f659(x0) = x0 | | | +- f660(x0,x1,x2,x3) = x3 | | | +- f661(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f662(x0,x1) = max(x1,x0) | | | +- f663(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f664(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f665(x0) = x0 | | | +- f666(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f667(x0) = x0 | | | +- f668(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f669(x0) = 1 + x0 | | | +- f670(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f671(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f672(x0,x1,x2,x3,x4,x5,x6,x7) = max(x2,x1) | | | +- f673(x0,x1,x2,x3,x4,x5,x6,x7) = 2 + x3 | | | +- f674(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 3 + x1 + x1*x4 + x3 + 2*x4 | | | +- f675(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f676(x0,x1,x2,x3,x4,x5,x6,x7) = max(x1,x2) | | | +- f677(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f678(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f679(x0) = x0 | | | +- f680(x0) = x0 | | | +- f681(x0) = x0 | | | +- f682(x0) = x0 | | | +- f683(x0) = 0 | | | +- f684(x0,x1,x2,x3) = 1 + x1 + x3 | | | +- f685(x0) = x0 | | | +- f686(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3 | | | +- f687(x0) = x0 | | | +- f688(x0) = x0 | | | +- f689(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x1 + x3 | | | +- f690(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x3 | | | +- f691(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x1 + x1*x4 + x3 + 2*x4 | | | +- f692(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x1 + x1*x4 + x3 + 2*x4 | | | +- f693(x0) = x0 | | | +- f694(x0) = x0 | | | +- f695(x0) = x0 | | | +- f696(x0) = x0 | | | +- f697() = 0 | | | +- f698() = 0 | | | +- f699(x0) = x0 | | | +- f7(x0,x1,x2,x3) = max(x2,x1) | | | +- f700(x0) = x0 | | | +- f8(x0,x1,x2,x3) = 1 + x3 | | | `- f9(x0,x1,x2,x3) = 1 + x1*x3 + 2*x3 | +- Constraints | | | +- f609(x3) = x3 >= x3 = x3 | | | +- f610(x3) = x3 >= x3 = f609(x3) | | | +- f611(x86) = x86 >= x86 = x86 | | | +- f612(x89) = x89 >= x89 = x89 | | | +- f613(x87) = x87 >= x87 = x87 | | | +- f614(x88) = x88 >= x88 = x88 | | | +- f15(x86,x87,f615()) = 0 >= 0 = f1(f611(x86),f613(x87)) | | | +- f16(x86,x87,f615()) + x88 = (1 + x86) + x88 >= (1 + x86) + x88 = f2(f611(x86),f613(x87)) + f614(x88) | | | +- f17(x86,x87,f615(),x88) + x89 = x89 >= x89 = f3(f611(x86),f613(x87),f614(x88)) + f612(x89) | | | +- f616(x3) = x3 >= x3 = f610(x3) | | | +- f617(x2) = x2 >= x2 = x2 | | | +- f618(x1) = x1 >= x1 = x1 | | | +- f619(x1,x2,x3,x86,x87,x88,x89) = x3 >= x3 = f21(f615(),f618(x1),f617(x2),f619(x1,x2,x3,x86,x87,x88,x89)) + f616(x3) | | | +- f620(x1,x2,x3,x86,x87,x88,x89) = 1 + ((x1 * (x2 * x2)) + ((2 * (x2 * x2)) + x3)) >= (1 + ((x1 * (x2 * x2)) + (2 * (x2 * x2)))) + x3 = f20(f615(),f618(x1),f617(x2)) + f619(x1,x2,x3,x86,x87,x88,x89) | | | +- f13(x1,x2) = x2 >= x2 = f19(f615(),f618(x1),f617(x2)) | | | +- f12(x1,x2) = x1 >= x1 = f18(f615(),f618(x1),f617(x2)) | | | +- f14(x1,x2) + x3 = (2 + ((x1 * (x2 * x2)) + (2 * (x2 * x2)))) + x3 >= (1 + ((x1 * (x2 * x2)) + ((2 * (x2 * x2)) + x3))) + 1 = f620(x1,x2,x3,x86,x87,x88,x89) + 1 | | | +- f621(x6) = x6 >= x6 = x6 | | | +- f622(x7) = x7 >= x7 = x7 | | | +- f623(x6) = x6 >= x6 = f621(x6) | | | +- f624(x8) = x8 >= x8 = x8 | | | +- f625(x6,x7,x8) = x6 >= x6 = f3(f622(x7),f624(x8),f625(x6,x7,x8)) + f623(x6) | | | +- f626(x6,x7,x8) = 1 + (x6 + x7) >= (1 + x7) + x6 = f2(f622(x7),f624(x8)) + f625(x6,x7,x8) | | | +- f1(x7 + 1,x8 + 1) = 0 >= 0 = f1(f622(x7),f624(x8)) | | | +- f2(x7 + 1,x8 + 1) + x6 = (1 + (x7 + 1)) + x6 >= (1 + (x6 + x7)) + 1 = f626(x6,x7,x8) + 1 | | | +- f627(x11) = x11 >= x11 = x11 | | | +- f628(x11) = x11 >= x11 = f627(x11) | | | +- f1(x12 + 1,0) = 0 >= 0 = 0 | | | +- f2(x12 + 1,0) + x11 = (1 + (x12 + 1)) + x11 >= x11 + 1 = f628(x11) + 1 | | | +- f629(x15) = x15 >= x15 = x15 | | | +- f630(x15) = x15 >= x15 = f629(x15) | | | +- f1(0,x14) = 0 >= 0 = 0 | | | +- f2(0,x14) + x15 = 1 + x15 >= x15 + 1 = f630(x15) + 1 | | | +- f631(x19) = x19 >= x19 = x19 | | | +- f632(x19) = x19 >= x19 = f631(x19) | | | +- f19(x16,x17,0) = 0 >= 0 = 0 | | | +- f18(x16,x17,0) = x17 >= 0 = f633() | | | +- f20(x16,x17,0) + x19 = 1 + x19 >= x19 + 1 = f632(x19) + 1 | | | +- f634(x28) = x28 >= x28 = x28 | | | +- f635(x170) = x170 >= x170 = x170 | | | +- f636(x173) = x173 >= x173 = x173 | | | +- f637(x171) = x171 >= x171 = x171 | | | +- f638(x172) = x172 >= x172 = x172 | | | +- f4(x170,x171,f639(x25)) = 0 >= 0 = f15(f635(x170),f637(x171),x25) | | | +- f5(x170,x171,f639(x25)) + x172 = (1 + x170) + x172 >= (1 + x170) + x172 = f16(f635(x170),f637(x171),x25) + f638(x172) | | | +- f6(x170,x171,f639(x25),x172) + x173 = x173 >= x173 = f17(f635(x170),f637(x171),x25,f638(x172)) + f636(x173) | | | +- f640(x28) = x28 >= x28 = f634(x28) | | | +- f641(x26) = x26 >= x26 = x26 | | | +- f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = x28 >= x28 = f11(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) ,f642(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f640(x28) | | | +- f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = x28 >= x28 = f10(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241) ,f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f642(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) | | | +- f647(x238) = x238 >= x238 = x238 | | | +- f648(x241) = x241 >= x241 = x241 | | | +- f649(x239) = x239 >= x239 = x239 | | | +- f650(x240) = x240 >= x240 = x240 | | | +- f15(x238,x239,f651(x25)) = 0 >= 0 = f15(f647(x238),f649(x239),x25) | | | +- f16(x238,x239,f651(x25)) + x240 = (1 + x238) + x240 >= (1 + x238) + x240 = f16(f647(x238),f649(x239),x25) + f650(x240) | | | +- f17(x238,x239,f651(x25),x240) + x241 = x241 >= x241 = f17(f647(x238),f649(x239),x25,f650(x240)) + f648(x241) | | | +- f652(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = x28 >= x28 = f646(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f653(x30) = x30 >= x30 = x30 | | | +- f654(x26) = x26 >= x26 = x26 | | | +- f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = x28 >= x28 = f21(f651(x25),f654(x26),f653(x30),f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241)) + f652(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) | | | +- f644(x25,x26,x30,x238,x239,x240,x241) = x30 >= x30 = f19(f651(x25),f654(x26),f653(x30)) | | | +- f643(x25,x26,x30,x238,x239,x240,x241) = x26 >= x26 = f18(f651(x25),f654(x26),f653(x30)) | | | +- f645(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = 1 + ((x26 * (x30 * x30)) + (x28 + (2 * (x30 * x30)))) >= (1 + ((x26 * (x30 * x30)) + (2 * (x30 * x30)))) + x28 = f20(f651(x25) ,f654(x26) ,f653(x30)) + f655(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) | | | +- f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) = 2 + ((x26 * x30) + ((x26 * (x30 * x30)) + (x28 + ((2 * x30) + (2 * (x30 * x30)))))) >= (1 + ((x26 * x30) + (2 * x30))) + (1 + ((x26 * (x30 * x30)) + (x28 + (2 * (x30 * x30))))) = f9(f639(x25) ,f641(x26) ,f643(x25,x26,x30,x238,x239,x240,x241) ,f644(x25,x26,x30,x238,x239,x240,x241)) + f645(x25 ,x26 ,x28 ,x30 ,x170 ,x171 ,x172 ,x173 ,x238 ,x239 ,x240 ,x241) | | | +- f19(x25,x26,x30 + 1) = x30 + 1 >= 1 + x30 = f8(f639(x25),f641(x26),f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) | | | +- f18(x25,x26,x30 + 1) = x26 >= max(x26,x26) = f7(f639(x25),f641(x26),f643(x25,x26,x30,x238,x239,x240,x241),f644(x25,x26,x30,x238,x239,x240,x241)) | | | +- f20(x25,x26,x30 + 1) + x28 = (1 + ((x26 * ((x30 + 1) * (x30 + 1))) + (2 * ((x30 + 1) * (x30 + 1))))) + x28 >= (2 + ((x26 * x30) + ((x26 * (x30 * x30)) + (x28 + ((2 * x30) + (2 * (x30 * x30))))))) + 1 = f656(x25,x26,x28,x30,x170,x171,x172,x173,x238,x239,x240,x241) + 1 | | | +- f657(x36) = x36 >= x36 = x36 | | | +- f658(x39) = x39 >= x39 = x39 | | | +- f659(x37) = x37 >= x37 = x37 | | | +- f660(x35,x36,x37,x39) = x39 >= x39 = f6(f657(x36),f659(x37),x35,f660(x35,x36,x37,x39)) + f658(x39) | | | +- f661(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) | | | +- f662(x36,x37) = max(x37,x36) >= x36 = x36 | | | +- f663(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f661(x35,x36,x37,x39) | | | +- f664(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f663(x35,x36,x37,x39) | | | +- f665(x37) = x37 >= x37 = x37 | | | +- f666(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f664(x35,x36,x37,x39) | | | +- f667(x41) = x41 >= x41 = x41 | | | +- f668(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f666(x35,x36,x37,x39) | | | +- f669(x41) = x41 + 1 >= x41 + 1 = f667(x41) + 1 | | | +- f662(x36,x37) = max(x37,x36) >= x37 = f665(x37) | | | +- f670(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f668(x35,x36,x37,x39) | | | +- f671(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f670(x35,x36,x37,x39) | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = max(x37,x36) >= max(x37,x36) = f662(x36,x37) | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = 2 + x41 >= (x41 + 1) + 1 = f669(x41) + 1 | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 3 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) >= ((1 + x36) + x39) + 1 = f671(x35,x36,x37,x39) + 1 | | | +- f675(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f5(f657(x36),f659(x37),x35) + f660(x35,x36,x37,x39) | | | +- f676(x35,x36,x37,x41,x475,x476,x477,x478) = max(x36,x37) >= x37 = x37 | | | +- f677(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f675(x35,x36,x37,x39) | | | +- f678(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f677(x35,x36,x37,x39) | | | +- f679(x475) = x475 >= x475 = x475 | | | +- f680(x478) = x478 >= x478 = x478 | | | +- f681(x476) = x476 >= x476 = x476 | | | +- f682(x477) = x477 >= x477 = x477 | | | +- f4(x475,x476,f683(x35)) = 0 >= 0 = f4(f679(x475),f681(x476),x35) | | | +- f5(x475,x476,f683(x35)) + x477 = (1 + x475) + x477 >= (1 + x475) + x477 = f5(f679(x475),f681(x476),x35) + f682(x477) | | | +- f6(x475,x476,f683(x35),x477) + x478 = x478 >= x478 = f6(f679(x475),f681(x476),x35,f682(x477)) + f680(x478) | | | +- f684(x35,x36,x37,x39) = (1 + x36) + x39 >= (1 + x36) + x39 = f678(x35,x36,x37,x39) | | | +- f685(x36) = x36 >= x36 = x36 | | | +- f686(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 1 + (x36 + x39) >= (1 + x36) + x39 = f11(f683(x35) ,f685(x36) ,f687(x37) ,f688(x41) ,f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) ,f686(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f684(x35,x36,x37,x39) | | | +- f688(x41) = x41 >= x41 = x41 | | | +- f687(x37) = x37 >= x37 = x37 | | | +- f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 1 + (x36 + x39) >= 1 + (x36 + x39) = f10(f683(x35),f685(x36),f687(x37),f688(x41),f689(x35,x36,x37,x39,x41,x475,x476,x477,x478)) + f686(x35 ,x36 ,x37 ,x39 ,x41 ,x475 ,x476 ,x477 ,x478) | | | +- f690(x35,x36,x37,x41,x475,x476,x477,x478) = 1 + x41 >= 1 + x41 = f8(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- f676(x35,x36,x37,x41,x475,x476,x477,x478) = max(x36,x37) >= max(x37,x36) = f7(f683(x35),f685(x36),f687(x37),f688(x41)) | | | +- f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 2 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) >= (1 + ((x36 * x41) + (2 * x41))) + (1 + (x36 + x39)) = f9(f683(x35),f685(x36),f687(x37),f688(x41)) + f689(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 2 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) >= 2 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) = f691(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f673(x35,x36,x37,x41,x475,x476,x477,x478) = 2 + x41 >= (1 + x41) + 1 = f690(x35,x36,x37,x41,x475,x476,x477,x478) + 1 | | | +- f672(x35,x36,x37,x41,x475,x476,x477,x478) = max(x37,x36) >= max(x36,x37) = f676(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) = 3 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) >= (2 + (x36 + ((x36 * x41) + (x39 + (2 * x41))))) + 1 = f692(x35,x36,x37,x39,x41,x475,x476,x477,x478) + 1 | | | +- f8(x35,x36,x37,x41 + 1) = 1 + (x41 + 1) >= 2 + x41 = f673(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f7(x35,x36,x37,x41 + 1) = max(x37,x36) >= max(x37,x36) = f672(x35,x36,x37,x41,x475,x476,x477,x478) | | | +- f9(x35,x36,x37,x41 + 1) + x39 = (1 + ((x36 * (x41 + 1)) + (2 * (x41 + 1)))) + x39 >= 3 + (x36 + ((x36 * x41) + (x39 + (2 * x41)))) = f674(x35,x36,x37,x39,x41,x475,x476,x477,x478) | | | +- f693(x50) = x50 >= x50 = x50 | | | +- f694(x47) = x47 >= x47 = x47 | | | +- f695(x50) = x50 >= x50 = f693(x50) | | | +- f696(x50) = x50 >= x50 = f695(x50) | | | +- f697() = 0 >= 0 = 0 | | | +- f694(x47) = x47 >= 0 = f698() | | | +- f699(x50) = x50 >= x50 = f696(x50) | | | +- f700(x50) = x50 >= x50 = f699(x50) | | | +- f8(x46,x47,x48,0) = 1 >= 1 = f697() + 1 | | | +- f7(x46,x47,x48,0) = max(x48,x47) >= x47 = f694(x47) | | | `- f9(x46,x47,x48,0) + x50 = 1 + x50 >= x50 + 1 = f700(x50) + 1 | `- Stopping timer: 2017-03-30 07:36:09.080889 UTC(+12.971081s)