SUCCESS(1) SUCCESS f1(x0,x1) = 1 + x0; f2(x0,x1) = 0; f208(x0) = x0; f209(x0) = x0; f210(x0) = x0; f211(x0) = x0; f212() = 0; f213(x0) = x0; f214(x0) = x0; f215(x0) = x0; f216(x0,x1,x2,x3,x4) = x2; f217(x0,x1,x2,x3,x4) = 1 + 2*x1 + x2; f218(x0) = x0; f219(x0) = x0; f220(x0) = x0; f221(x0) = x0; f222(x0) = 0; f223(x0) = x0; f224(x0) = x0; f225(x0) = x0; f226(x0,x1,x2,x3,x4,x5) = x2; f227(x0,x1,x2,x3,x4) = x2; f228(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x1; f229(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3; f230(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3; f231(x0) = x0; f232(x0) = x0; f233(x0) = 0; f234(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3; f235(x0) = x0; f236(x0) = x0; f237(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x2 + 2*x3; f238(x0,x1,x2,x3,x4) = x2; f239(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x2 + 2*x3 + 2*x4; f240(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x2 + 2*x3 + 2*x4; f241(x0) = x0; f242(x0) = x0; f243(x0) = x0; f244(x0,x1) = 1 + x1; f245(x0,x1,x2) = x2; f246(x0,x1,x2) = x2; f3(x0,x1,x2) = 1 + x1; f4(x0,x1,x2) = x2; f5(x0,x1,x2) = 1 + 2*x2; f6(x0,x1,x2,x3) = 0; f7(x0,x1) = 1 + x0; f8(x0,x1) = x1; f9(x0,x1) = 2 + 2*x1; ExecutionLog | +- Staring timer: 2017-03-30 07:29:50.404065 UTC | +- Open Constraints | | | +- f208(x3) = f208(x3) >= x3 = x3 | | | +- f209(x3) = f209(x3) >= f208(x3) = f208(x3) | | | +- f210(x42) = f210(x42) >= x42 = x42 | | | +- f211(x43) = f211(x43) >= x43 = x43 | | | +- f1(x42,f212()) = f1(x42,f212()) >= f210(x42) + 1 = f210(x42) + 1 | | | +- f2(x42,f212()) + x43 = f2(x42,f212()) + x43 >= f211(x43) = f211(x43) | | | +- f213(x3) = f213(x3) >= f209(x3) = f209(x3) | | | +- f214(x2) = f214(x2) >= x2 = x2 | | | +- f215(x1) = f215(x1) >= x1 = x1 | | | +- f216(x1,x2,x3,x42,x43) = f216(x1,x2,x3,x42,x43) >= f6(f212(),f215(x1),f214(x2),f216(x1,x2,x3,x42,x43)) + f213(x3) = f6(f212(),f215(x1),f214(x2),f216(x1,x2,x3,x42,x43)) + f213(x3) | | | +- f217(x1,x2,x3,x42,x43) = f217(x1,x2,x3,x42,x43) >= f5(f212(),f215(x1),f214(x2)) + f216(x1,x2,x3,x42,x43) = f5(f212(),f215(x1),f214(x2)) + f216(x1,x2,x3,x42,x43) | | | +- f8(x1,x2) = f8(x1,x2) >= f4(f212(),f215(x1),f214(x2)) = f4(f212(),f215(x1),f214(x2)) | | | +- f7(x1,x2) = f7(x1,x2) >= f3(f212(),f215(x1),f214(x2)) = f3(f212(),f215(x1),f214(x2)) | | | +- f9(x1,x2) + x3 = f9(x1,x2) + x3 >= f217(x1,x2,x3,x42,x43) + 1 = f217(x1,x2,x3,x42,x43) + 1 | | | +- f218(x7) = f218(x7) >= x7 = x7 | | | +- f219(x7) = f219(x7) >= f218(x7) = f218(x7) | | | +- f220(x85) = f220(x85) >= x85 = x85 | | | +- f221(x86) = f221(x86) >= x86 = x86 | | | +- f1(x85,f222(x4)) = f1(x85,f222(x4)) >= f1(f220(x85),x4) = f1(f220(x85),x4) | | | +- f2(x85,f222(x4)) + x86 = f2(x85,f222(x4)) + x86 >= f2(f220(x85),x4) + f221(x86) = f2(f220(x85),x4) + f221(x86) | | | +- f223(x7) = f223(x7) >= f219(x7) = f219(x7) | | | +- f224(x9) = f224(x9) >= x9 = x9 | | | +- f225(x5) = f225(x5) >= x5 = x5 | | | +- f226(x4,x5,x7,x9,x85,x86) = f226(x4,x5,x7,x9,x85,x86) >= f6(f222(x4),f225(x5),f224(x9),f226(x4,x5,x7,x9,x85,x86)) + f223(x7) = f6(f222(x4),f225(x5),f224(x9),f226(x4,x5,x7,x9,x85,x86)) + f223(x7) | | | +- f227(x4,x5,x9,x85,x86) = f227(x4,x5,x9,x85,x86) >= f4(f222(x4),f225(x5),f224(x9)) = f4(f222(x4),f225(x5),f224(x9)) | | | +- f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) >= f3(f222(x4),f225(x5),f224(x9)) = f3(f222(x4),f225(x5),f224(x9)) | | | +- f229(x4,x5,x7,x9,x85,x86) = f229(x4,x5,x7,x9,x85,x86) >= f5(f222(x4),f225(x5),f224(x9)) + f226(x4,x5,x7,x9,x85,x86) = f5(f222(x4),f225(x5),f224(x9)) + f226(x4,x5,x7,x9,x85,x86) | | | +- f230(x4,x5,x7,x9,x85,x86) = f230(x4,x5,x7,x9,x85,x86) >= f229(x4,x5,x7,x9,x85,x86) = f229(x4,x5,x7,x9,x85,x86) | | | +- f231(x134) = f231(x134) >= x134 = x134 | | | +- f232(x135) = f232(x135) >= x135 = x135 | | | +- f1(x134,f233(x4)) = f1(x134,f233(x4)) >= f1(f231(x134),x4) = f1(f231(x134),x4) | | | +- f2(x134,f233(x4)) + x135 = f2(x134,f233(x4)) + x135 >= f2(f231(x134),x4) + f232(x135) = f2(f231(x134),x4) + f232(x135) | | | +- f234(x4,x5,x7,x9,x85,x86) = f234(x4,x5,x7,x9,x85,x86) >= f230(x4,x5,x7,x9,x85,x86) = f230(x4,x5,x7,x9,x85,x86) | | | +- f235(x10) = f235(x10) >= x10 = x10 | | | +- f236(x5) = f236(x5) >= x5 = x5 | | | +- f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f6(f233(x4),f236(x5),f235(x10),f237(x4,x5,x7,x9,x10,x85,x86,x134,x135)) + f234(x4,x5,x7,x9,x85,x86) = f6(f233(x4),f236(x5),f235(x10),f237(x4,x5,x7,x9,x10,x85,x86,x134,x135)) + f234(x4,x5,x7,x9,x85,x86) | | | +- f238(x4,x5,x10,x134,x135) = f238(x4,x5,x10,x134,x135) >= f4(f233(x4),f236(x5),f235(x10)) = f4(f233(x4),f236(x5),f235(x10)) | | | +- f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) >= f3(f233(x4),f236(x5),f235(x10)) = f3(f233(x4),f236(x5),f235(x10)) | | | +- f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f5(f233(x4),f236(x5),f235(x10)) + f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f5(f233(x4),f236(x5),f235(x10)) + f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | +- f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | +- f4(x4,x5,(x9 + x10) + 1) = f4(x4,x5,(x9 + x10) + 1) >= (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 = (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 | | | +- f3(x4,x5,(x9 + x10) + 1) = f3(x4,x5,(x9 + x10) + 1) >= f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) | | | +- f5(x4,x5,(x9 + x10) + 1) + x7 = f5(x4,x5,(x9 + x10) + 1) + x7 >= f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 | | | +- f241(x16) = f241(x16) >= x16 = x16 | | | +- f242(x14) = f242(x14) >= x14 = x14 | | | +- f243(x16) = f243(x16) >= f241(x16) = f241(x16) | | | +- f244(x13,x14) = f244(x13,x14) >= f1(f242(x14),x13) = f1(f242(x14),x13) | | | +- f245(x13,x14,x16) = f245(x13,x14,x16) >= f2(f242(x14),x13) + f243(x16) = f2(f242(x14),x13) + f243(x16) | | | +- f246(x13,x14,x16) = f246(x13,x14,x16) >= f245(x13,x14,x16) = f245(x13,x14,x16) | | | +- f4(x13,x14,0) = f4(x13,x14,0) >= 0 = 0 | | | +- f3(x13,x14,0) = f3(x13,x14,0) >= f244(x13,x14) = f244(x13,x14) | | | `- f5(x13,x14,0) + x16 = f5(x13,x14,0) + x16 >= f246(x13,x14,x16) + 1 = f246(x13,x14,x16) + 1 | +- Open Constraints | | | +- f208(x3) = f208(x3) >= x3 = x3 | | | +- f209(x3) = f209(x3) >= f208(x3) = f208(x3) | | | +- f210(x42) = f210(x42) >= x42 = x42 | | | +- f211(x43) = f211(x43) >= x43 = x43 | | | +- f1(x42,f212()) = f1(x42,f212()) >= f210(x42) + 1 = f210(x42) + 1 | | | +- f2(x42,f212()) + x43 = f2(x42,f212()) + x43 >= f211(x43) = f211(x43) | | | +- f213(x3) = f213(x3) >= f209(x3) = f209(x3) | | | +- f214(x2) = f214(x2) >= x2 = x2 | | | +- f215(x1) = f215(x1) >= x1 = x1 | | | +- f216(x1,x2,x3,x42,x43) = f216(x1,x2,x3,x42,x43) >= f6(f212(),f215(x1),f214(x2),f216(x1,x2,x3,x42,x43)) + f213(x3) = f6(f212(),f215(x1),f214(x2),f216(x1,x2,x3,x42,x43)) + f213(x3) | | | +- f217(x1,x2,x3,x42,x43) = f217(x1,x2,x3,x42,x43) >= f5(f212(),f215(x1),f214(x2)) + f216(x1,x2,x3,x42,x43) = f5(f212(),f215(x1),f214(x2)) + f216(x1,x2,x3,x42,x43) | | | +- f8(x1,x2) = f8(x1,x2) >= f4(f212(),f215(x1),f214(x2)) = f4(f212(),f215(x1),f214(x2)) | | | +- f7(x1,x2) = f7(x1,x2) >= f3(f212(),f215(x1),f214(x2)) = f3(f212(),f215(x1),f214(x2)) | | | +- f9(x1,x2) + x3 = f9(x1,x2) + x3 >= f217(x1,x2,x3,x42,x43) + 1 = f217(x1,x2,x3,x42,x43) + 1 | | | +- f218(x7) = f218(x7) >= x7 = x7 | | | +- f219(x7) = f219(x7) >= f218(x7) = f218(x7) | | | +- f220(x85) = f220(x85) >= x85 = x85 | | | +- f221(x86) = f221(x86) >= x86 = x86 | | | +- f1(x85,f222(x4)) = f1(x85,f222(x4)) >= f1(f220(x85),x4) = f1(f220(x85),x4) | | | +- f2(x85,f222(x4)) + x86 = f2(x85,f222(x4)) + x86 >= f2(f220(x85),x4) + f221(x86) = f2(f220(x85),x4) + f221(x86) | | | +- f223(x7) = f223(x7) >= f219(x7) = f219(x7) | | | +- f224(x9) = f224(x9) >= x9 = x9 | | | +- f225(x5) = f225(x5) >= x5 = x5 | | | +- f226(x4,x5,x7,x9,x85,x86) = f226(x4,x5,x7,x9,x85,x86) >= f6(f222(x4),f225(x5),f224(x9),f226(x4,x5,x7,x9,x85,x86)) + f223(x7) = f6(f222(x4),f225(x5),f224(x9),f226(x4,x5,x7,x9,x85,x86)) + f223(x7) | | | +- f227(x4,x5,x9,x85,x86) = f227(x4,x5,x9,x85,x86) >= f4(f222(x4),f225(x5),f224(x9)) = f4(f222(x4),f225(x5),f224(x9)) | | | +- f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) >= f3(f222(x4),f225(x5),f224(x9)) = f3(f222(x4),f225(x5),f224(x9)) | | | +- f229(x4,x5,x7,x9,x85,x86) = f229(x4,x5,x7,x9,x85,x86) >= f5(f222(x4),f225(x5),f224(x9)) + f226(x4,x5,x7,x9,x85,x86) = f5(f222(x4),f225(x5),f224(x9)) + f226(x4,x5,x7,x9,x85,x86) | | | +- f230(x4,x5,x7,x9,x85,x86) = f230(x4,x5,x7,x9,x85,x86) >= f229(x4,x5,x7,x9,x85,x86) = f229(x4,x5,x7,x9,x85,x86) | | | +- f231(x134) = f231(x134) >= x134 = x134 | | | +- f232(x135) = f232(x135) >= x135 = x135 | | | +- f1(x134,f233(x4)) = f1(x134,f233(x4)) >= f1(f231(x134),x4) = f1(f231(x134),x4) | | | +- f2(x134,f233(x4)) + x135 = f2(x134,f233(x4)) + x135 >= f2(f231(x134),x4) + f232(x135) = f2(f231(x134),x4) + f232(x135) | | | +- f234(x4,x5,x7,x9,x85,x86) = f234(x4,x5,x7,x9,x85,x86) >= f230(x4,x5,x7,x9,x85,x86) = f230(x4,x5,x7,x9,x85,x86) | | | +- f235(x10) = f235(x10) >= x10 = x10 | | | +- f236(x5) = f236(x5) >= x5 = x5 | | | +- f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f6(f233(x4),f236(x5),f235(x10),f237(x4,x5,x7,x9,x10,x85,x86,x134,x135)) + f234(x4,x5,x7,x9,x85,x86) = f6(f233(x4),f236(x5),f235(x10),f237(x4,x5,x7,x9,x10,x85,x86,x134,x135)) + f234(x4,x5,x7,x9,x85,x86) | | | +- f238(x4,x5,x10,x134,x135) = f238(x4,x5,x10,x134,x135) >= f4(f233(x4),f236(x5),f235(x10)) = f4(f233(x4),f236(x5),f235(x10)) | | | +- f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) >= f3(f233(x4),f236(x5),f235(x10)) = f3(f233(x4),f236(x5),f235(x10)) | | | +- f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f5(f233(x4),f236(x5),f235(x10)) + f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f5(f233(x4),f236(x5),f235(x10)) + f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | +- f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | +- f4(x4,x5,(x9 + x10) + 1) = f4(x4,x5,(x9 + x10) + 1) >= (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 = (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 | | | +- f3(x4,x5,(x9 + x10) + 1) = f3(x4,x5,(x9 + x10) + 1) >= f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) | | | +- f5(x4,x5,(x9 + x10) + 1) + x7 = f5(x4,x5,(x9 + x10) + 1) + x7 >= f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 | | | +- f241(x16) = f241(x16) >= x16 = x16 | | | +- f242(x14) = f242(x14) >= x14 = x14 | | | +- f243(x16) = f243(x16) >= f241(x16) = f241(x16) | | | +- f244(x13,x14) = f244(x13,x14) >= f1(f242(x14),x13) = f1(f242(x14),x13) | | | +- f245(x13,x14,x16) = f245(x13,x14,x16) >= f2(f242(x14),x13) + f243(x16) = f2(f242(x14),x13) + f243(x16) | | | +- f246(x13,x14,x16) = f246(x13,x14,x16) >= f245(x13,x14,x16) = f245(x13,x14,x16) | | | +- f4(x13,x14,0) = f4(x13,x14,0) >= 0 = 0 | | | +- f3(x13,x14,0) = f3(x13,x14,0) >= f244(x13,x14) = f244(x13,x14) | | | `- f5(x13,x14,0) + x16 = f5(x13,x14,0) + x16 >= f246(x13,x14,x16) + 1 = f246(x13,x14,x16) + 1 | +- Simplification ... | | | +- Substituted: f2(x42,f212()) + x43 ≥ f211(x43) ↦ f2(0,f212()) + x43 ≥ f211(x43) | | | +- Substituted: f227(x4,x5,x9,x85,x86) ≥ f4(f222(x4),f225(x5),f224(x9)) ↦ f227(x4,x5,x9,0,0) ≥ f4(f222(x4),f225(x5),f224(x9)) | | | +- Substituted: f228(x4,x5,x9,x10,x85,x86,x134,x135) ≥ f3(f222(x4),f225(x5),f224(x9)) ↦ f228(x4,x5,x9,0,0,0,0,0) ≥ f3(f222(x4),f225(x5),f224(x9)) | | | +- Substituted: f238(x4,x5,x10,x134,x135) ≥ f4(f233(x4),f236(x5),f235(x10)) ↦ f238(x4,x5,x10,0,0) ≥ f4(f233(x4),f236(x5),f235(x10)) | | | +- Substituted: f228(x4,x5,x9,x10,x85,x86,x134,x135) ≥ f3(f233(x4),f236(x5),f235(x10)) ↦ f228(x4,x5,0,x10,0,0,0,0) ≥ f3(f233(x4),f236(x5),f235(x10)) | | | +- Substituted: f4(x13,x14,0) ≥ 0 ↦ f4(0,0,0) ≥ 0 | | | +- Eliminated: f6/4 | | | +- Propagated: f208(x0) ↦ x0 | | | +- Propagated: f210(x0) ↦ x0 | | | +- Propagated: f211(x0) ↦ x0 | | | +- Propagated: f214(x0) ↦ x0 | | | +- Propagated: f215(x0) ↦ x0 | | | +- Propagated: f218(x0) ↦ x0 | | | +- Propagated: f220(x0) ↦ x0 | | | +- Propagated: f221(x0) ↦ x0 | | | +- Propagated: f224(x0) ↦ x0 | | | +- Propagated: f225(x0) ↦ x0 | | | +- Propagated: f231(x0) ↦ x0 | | | +- Propagated: f232(x0) ↦ x0 | | | +- Propagated: f235(x0) ↦ x0 | | | +- Propagated: f236(x0) ↦ x0 | | | +- Propagated: f241(x0) ↦ x0 | | | +- Propagated: f242(x0) ↦ x0 | | | +- Propagated: f209(x0) ↦ x0 | | | +- Propagated: f219(x0) ↦ x0 | | | +- Propagated: f243(x0) ↦ x0 | | | +- Propagated: f213(x0) ↦ x0 | | | +- Propagated: f223(x0) ↦ x0 | | | +- Propagated: f216(x0,x1,x2,x3,x4) ↦ x2 | | | `- Propagated: f226(x0,x1,x2,x3,x4,x5) ↦ x2 | +- Interpretation | | | +- f208(x0) = x0 | | | +- f209(x0) = x0 | | | +- f210(x0) = x0 | | | +- f211(x0) = x0 | | | +- f213(x0) = x0 | | | +- f214(x0) = x0 | | | +- f215(x0) = x0 | | | +- f216(x0,x1,x2,x3,x4) = x2 | | | +- f218(x0) = x0 | | | +- f219(x0) = x0 | | | +- f220(x0) = x0 | | | +- f221(x0) = x0 | | | +- f223(x0) = x0 | | | +- f224(x0) = x0 | | | +- f225(x0) = x0 | | | +- f226(x0,x1,x2,x3,x4,x5) = x2 | | | +- f231(x0) = x0 | | | +- f232(x0) = x0 | | | +- f235(x0) = x0 | | | +- f236(x0) = x0 | | | +- f241(x0) = x0 | | | +- f242(x0) = x0 | | | +- f243(x0) = x0 | | | `- f6(x0,x1,x2,x3) = 0 | +- Constraints | | | +- f208(x3) = x3 >= x3 = x3 | | | +- f209(x3) = x3 >= x3 = f208(x3) | | | +- f210(x42) = x42 >= x42 = x42 | | | +- f211(x43) = x43 >= x43 = x43 | | | +- f1(x42,f212()) = f1(x42,f212()) >= x42 + 1 = f210(x42) + 1 | | | +- f2(x42,f212()) + x43 = f2(x42,f212()) + x43 >= x43 = f211(x43) | | | +- f213(x3) = x3 >= x3 = f209(x3) | | | +- f214(x2) = x2 >= x2 = x2 | | | +- f215(x1) = x1 >= x1 = x1 | | | +- f216(x1,x2,x3,x42,x43) = x3 >= x3 = f6(f212(),f215(x1),f214(x2),f216(x1,x2,x3,x42,x43)) + f213(x3) | | | +- f217(x1,x2,x3,x42,x43) = f217(x1,x2,x3,x42,x43) >= f5(f212(),x1,x2) + x3 = f5(f212(),f215(x1),f214(x2)) + f216(x1,x2,x3,x42,x43) | | | +- f8(x1,x2) = f8(x1,x2) >= f4(f212(),x1,x2) = f4(f212(),f215(x1),f214(x2)) | | | +- f7(x1,x2) = f7(x1,x2) >= f3(f212(),x1,x2) = f3(f212(),f215(x1),f214(x2)) | | | +- f9(x1,x2) + x3 = f9(x1,x2) + x3 >= f217(x1,x2,x3,x42,x43) + 1 = f217(x1,x2,x3,x42,x43) + 1 | | | +- f218(x7) = x7 >= x7 = x7 | | | +- f219(x7) = x7 >= x7 = f218(x7) | | | +- f220(x85) = x85 >= x85 = x85 | | | +- f221(x86) = x86 >= x86 = x86 | | | +- f1(x85,f222(x4)) = f1(x85,f222(x4)) >= f1(x85,x4) = f1(f220(x85),x4) | | | +- f2(x85,f222(x4)) + x86 = f2(x85,f222(x4)) + x86 >= f2(x85,x4) + x86 = f2(f220(x85),x4) + f221(x86) | | | +- f223(x7) = x7 >= x7 = f219(x7) | | | +- f224(x9) = x9 >= x9 = x9 | | | +- f225(x5) = x5 >= x5 = x5 | | | +- f226(x4,x5,x7,x9,x85,x86) = x7 >= x7 = f6(f222(x4),f225(x5),f224(x9),f226(x4,x5,x7,x9,x85,x86)) + f223(x7) | | | +- f227(x4,x5,x9,x85,x86) = f227(x4,x5,x9,x85,x86) >= f4(f222(x4),x5,x9) = f4(f222(x4),f225(x5),f224(x9)) | | | +- f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) >= f3(f222(x4),x5,x9) = f3(f222(x4),f225(x5),f224(x9)) | | | +- f229(x4,x5,x7,x9,x85,x86) = f229(x4,x5,x7,x9,x85,x86) >= f5(f222(x4),x5,x9) + x7 = f5(f222(x4),f225(x5),f224(x9)) + f226(x4,x5,x7,x9,x85,x86) | | | +- f230(x4,x5,x7,x9,x85,x86) = f230(x4,x5,x7,x9,x85,x86) >= f229(x4,x5,x7,x9,x85,x86) = f229(x4,x5,x7,x9,x85,x86) | | | +- f231(x134) = x134 >= x134 = x134 | | | +- f232(x135) = x135 >= x135 = x135 | | | +- f1(x134,f233(x4)) = f1(x134,f233(x4)) >= f1(x134,x4) = f1(f231(x134),x4) | | | +- f2(x134,f233(x4)) + x135 = f2(x134,f233(x4)) + x135 >= f2(x134,x4) + x135 = f2(f231(x134),x4) + f232(x135) | | | +- f234(x4,x5,x7,x9,x85,x86) = f234(x4,x5,x7,x9,x85,x86) >= f230(x4,x5,x7,x9,x85,x86) = f230(x4,x5,x7,x9,x85,x86) | | | +- f235(x10) = x10 >= x10 = x10 | | | +- f236(x5) = x5 >= x5 = x5 | | | +- f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f234(x4,x5,x7,x9,x85,x86) = f6(f233(x4),f236(x5),f235(x10),f237(x4,x5,x7,x9,x10,x85,x86,x134,x135)) + f234(x4 ,x5 ,x7 ,x9 ,x85 ,x86) | | | +- f238(x4,x5,x10,x134,x135) = f238(x4,x5,x10,x134,x135) >= f4(f233(x4),x5,x10) = f4(f233(x4),f236(x5),f235(x10)) | | | +- f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) >= f3(f233(x4),x5,x10) = f3(f233(x4),f236(x5),f235(x10)) | | | +- f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f5(f233(x4),x5,x10) + f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f5(f233(x4),f236(x5),f235(x10)) + f237(x4 ,x5 ,x7 ,x9 ,x10 ,x85 ,x86 ,x134 ,x135) | | | +- f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | +- f4(x4,x5,(x9 + x10) + 1) = f4(x4,x5,(x9 + x10) + 1) >= (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 = (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 | | | +- f3(x4,x5,(x9 + x10) + 1) = f3(x4,x5,(x9 + x10) + 1) >= f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) | | | +- f5(x4,x5,(x9 + x10) + 1) + x7 = f5(x4,x5,(x9 + x10) + 1) + x7 >= f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 | | | +- f241(x16) = x16 >= x16 = x16 | | | +- f242(x14) = x14 >= x14 = x14 | | | +- f243(x16) = x16 >= x16 = f241(x16) | | | +- f244(x13,x14) = f244(x13,x14) >= f1(x14,x13) = f1(f242(x14),x13) | | | +- f245(x13,x14,x16) = f245(x13,x14,x16) >= f2(x14,x13) + x16 = f2(f242(x14),x13) + f243(x16) | | | +- f246(x13,x14,x16) = f246(x13,x14,x16) >= f245(x13,x14,x16) = f245(x13,x14,x16) | | | +- f4(x13,x14,0) = f4(x13,x14,0) >= 0 = 0 | | | +- f3(x13,x14,0) = f3(x13,x14,0) >= f244(x13,x14) = f244(x13,x14) | | | `- f5(x13,x14,0) + x16 = f5(x13,x14,0) + x16 >= f246(x13,x14,x16) + 1 = f246(x13,x14,x16) + 1 | +- SCC-DECOMPOSE ... | | | +- SCC: 11 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.407083 UTC | | | +- Open Constraints | | | | | +- f2(x85,f222(x4)) + x86 = f2(x85,f222(x4)) + x86 >= f2(x85,x4) + x86 = f2(x85,x4) + x86 | | | | | +- f2(x134,f233(x4)) + x135 = f2(x134,f233(x4)) + x135 >= f2(x134,x4) + x135 = f2(x134,x4) + x135 | | | | | +- f2(0,f212()) + x43 = f2(0,f212()) + x43 >= x43 = x43 | | | | | +- f1(x42,f212()) = f1(x42,f212()) >= x42 + 1 = x42 + 1 | | | | | +- f1(x85,f222(x4)) = f1(x85,f222(x4)) >= f1(x85,x4) = f1(x85,x4) | | | | | `- f1(x134,f233(x4)) = f1(x134,f233(x4)) >= f1(x134,x4) = f1(x134,x4) | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.407151 UTC | | | | | +- Interpretation | | | | | | | +- f1(x0,x1) = max(14 + x0,15 + x1) | | | | | | | +- f2(x0,x1) = max(15 + x1,2 + x0) | | | | | | | +- f212() = 0 | | | | | | | +- f222(x0) = 15 + x0 | | | | | | | `- f233(x0) = 15 + x0 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f1(x0,x1) = 1 + x0 | | | | | | | +- f2(x0,x1) = 0 | | | | | | | +- f212() = 0 | | | | | | | +- f222(x0) = 0 | | | | | | | `- f233(x0) = x0 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f1(x0,x1) = 1 + x0 | | | | | | | +- f2(x0,x1) = 0 | | | | | | | +- f212() = 0 | | | | | | | +- f222(x0) = 0 | | | | | | | `- f233(x0) = 0 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:50.431417 UTC(+0.024266s) | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | +- f2(x0,x1) = 0 | | | | | +- f212() = 0 | | | | | +- f222(x0) = 0 | | | | | `- f233(x0) = 0 | | | +- Constraints | | | | | +- f2(x85,f222(x4)) + x86 = x86 >= x86 = f2(x85,x4) + x86 | | | | | +- f2(x134,f233(x4)) + x135 = x135 >= x135 = f2(x134,x4) + x135 | | | | | +- f2(0,f212()) + x43 = x43 >= x43 = x43 | | | | | +- f1(x42,f212()) = 1 + x42 >= x42 + 1 = x42 + 1 | | | | | +- f1(x85,f222(x4)) = 1 + x85 >= 1 + x85 = f1(x85,x4) | | | | | `- f1(x134,f233(x4)) = 1 + x134 >= 1 + x134 = f1(x134,x4) | | | `- Stopping timer: 2017-03-30 07:29:50.431512 UTC(+0.024429s) | +- SCC-DECOMPOSE ... | | | +- SCC: 10 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.432271 UTC | | | +- Open Constraints | | | | | `- f245(x13,x14,x16) = f245(x13,x14,x16) >= x16 = f2(x14,x13) + x16 | | | +- Simplification ... | | | | | `- Propagated: f245(x0,x1,x2) ↦ x2 | | | +- Interpretation | | | | | +- f2(x0,x1) = 0 | | | | | `- f245(x0,x1,x2) = x2 | | | +- Constraints | | | | | `- f245(x13,x14,x16) = x16 >= x16 = f2(x14,x13) + x16 | | | `- Stopping timer: 2017-03-30 07:29:50.432356 UTC(+0.000085s) | +- SCC-DECOMPOSE ... | | | +- SCC: 9 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.432957 UTC | | | +- Open Constraints | | | | | `- f244(x13,x14) = f244(x13,x14) >= 1 + x14 = f1(x14,x13) | | | +- Simplification ... | | | | | `- Propagated: f244(x0,x1) ↦ 1 + x1 | | | +- Interpretation | | | | | +- f1(x0,x1) = 1 + x0 | | | | | `- f244(x0,x1) = 1 + x1 | | | +- Constraints | | | | | `- f244(x13,x14) = 1 + x14 >= 1 + x14 = f1(x14,x13) | | | `- Stopping timer: 2017-03-30 07:29:50.43302 UTC(+0.000063s) | +- SCC-DECOMPOSE ... | | | +- SCC: 8 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.433647 UTC | | | +- Open Constraints | | | | | `- f246(x13,x14,x16) = f246(x13,x14,x16) >= x16 = f245(x13,x14,x16) | | | +- Simplification ... | | | | | `- Propagated: f246(x0,x1,x2) ↦ x2 | | | +- Interpretation | | | | | +- f245(x0,x1,x2) = x2 | | | | | `- f246(x0,x1,x2) = x2 | | | +- Constraints | | | | | `- f246(x13,x14,x16) = x16 >= x16 = f245(x13,x14,x16) | | | `- Stopping timer: 2017-03-30 07:29:50.433711 UTC(+0.000064s) | +- SCC-DECOMPOSE ... | | | +- SCC: 7 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.434293 UTC | | | +- Open Constraints | | | | | +- f3(x13,x14,0) = f3(x13,x14,0) >= 1 + x14 = f244(x13,x14) | | | | | +- f3(x4,x5,(x9 + x10) + 1) = f3(x4,x5,(x9 + x10) + 1) >= f228(x4,x5,x9,x10,x85,x86,x134,x135) = f228(x4,x5,x9,x10,x85,x86,x134,x135) | | | | | +- f228(x4,x5,x9,0,0,0,0,0) = f228(x4,x5,x9,0,0,0,0,0) >= f3(0,x5,x9) = f3(f222(x4),x5,x9) | | | | | `- f228(x4,x5,0,x10,0,0,0,0) = f228(x4,x5,0,x10,0,0,0,0) >= f3(0,x5,x10) = f3(f233(x4),x5,x10) | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.434383 UTC | | | | | +- Interpretation | | | | | | | +- f228(x0,x1,x2,x3,x4,x5,x6,x7) = max(15 + x1 + x3,14 + x0,14 + x1 + x2 + x3) | | | | | | | `- f3(x0,x1,x2) = 14 + x0 + x1 + x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f228(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x1 | | | | | | | `- f3(x0,x1,x2) = 1 + x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:50.468594 UTC(+0.034211s) | | | +- Interpretation | | | | | +- f222(x0) = 0 | | | | | +- f228(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x1 | | | | | +- f233(x0) = 0 | | | | | +- f244(x0,x1) = 1 + x1 | | | | | `- f3(x0,x1,x2) = 1 + x1 | | | +- Constraints | | | | | +- f3(x13,x14,0) = 1 + x14 >= 1 + x14 = f244(x13,x14) | | | | | +- f3(x4,x5,(x9 + x10) + 1) = 1 + x5 >= 1 + x5 = f228(x4,x5,x9,x10,x85,x86,x134,x135) | | | | | +- f228(x4,x5,x9,0,0,0,0,0) = 1 + x5 >= 1 + x5 = f3(f222(x4),x5,x9) | | | | | `- f228(x4,x5,0,x10,0,0,0,0) = 1 + x5 >= 1 + x5 = f3(f233(x4),x5,x10) | | | `- Stopping timer: 2017-03-30 07:29:50.468644 UTC(+0.034351s) | +- SCC-DECOMPOSE ... | | | +- SCC: 6 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.468973 UTC | | | +- Open Constraints | | | | | +- f5(x13,x14,0) + x16 = f5(x13,x14,0) + x16 >= x16 + 1 = f246(x13,x14,x16) + 1 | | | | | +- f5(x4,x5,(x9 + x10) + 1) + x7 = f5(x4,x5,(x9 + x10) + 1) + x7 >= f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 | | | | | +- f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | | | +- f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f5(0,x5,x10) + f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f5(f233(x4),x5,x10) + f237(x4 ,x5 ,x7 ,x9 ,x10 ,x85 ,x86 ,x134 ,x135) | | | | | +- f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) >= f234(x4,x5,x7,x9,x85,x86) = f234(x4,x5,x7,x9,x85,x86) | | | | | +- f234(x4,x5,x7,x9,x85,x86) = f234(x4,x5,x7,x9,x85,x86) >= f230(x4,x5,x7,x9,x85,x86) = f230(x4,x5,x7,x9,x85,x86) | | | | | +- f230(x4,x5,x7,x9,x85,x86) = f230(x4,x5,x7,x9,x85,x86) >= f229(x4,x5,x7,x9,x85,x86) = f229(x4,x5,x7,x9,x85,x86) | | | | | `- f229(x4,x5,x7,x9,x85,x86) = f229(x4,x5,x7,x9,x85,x86) >= f5(0,x5,x9) + x7 = f5(f222(x4),x5,x9) + x7 | | | +- Simplification ... | | | | | +- Substituted: f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) ≥ f234(x4,x5,x7,x9,x85,x86) ↦ f237(x4,x5,x7,x9,0,x85,x86,0,0) ≥ f234(x4,x5,x7,x9,x85,x86) | | | | | `- Substituted: f229(x4,x5,x7,x9,x85,x86) ≥ f5(f222(x4),x5,x9) + x7 ↦ f229(x4,x5,x7,x9,0,0) ≥ f5(f222(x4),x5,x9) + x7 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.46911 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:50.612905 UTC(+0.143795s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.612934 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:50.624435 UTC(+0.011501s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.624442 UTC | | | | | +- Interpretation | | | | | | | +- f229(x0,x1,x2,x3,x4,x5) = 4 + x2 + 10*x3 | | | | | | | +- f230(x0,x1,x2,x3,x4,x5) = 7 + 14*x0 + x2 + 10*x3 | | | | | | | +- f234(x0,x1,x2,x3,x4,x5) = 8 + 14*x0 + x2 + 10*x3 | | | | | | | +- f237(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 9 + 14*x0 + x2 + 10*x3 | | | | | | | +- f239(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 13 + 14*x0 + x2 + 10*x3 + 10*x4 | | | | | | | +- f240(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 13 + 14*x0 + x2 + 10*x3 + 10*x4 | | | | | | | `- f5(x0,x1,x2) = 4 + 14*x0 + 10*x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f229(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | | | | | +- f230(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | | | | | +- f234(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | | | | | +- f237(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x2 + 2*x3 | | | | | | | +- f239(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x2 + 2*x3 + 2*x4 | | | | | | | +- f240(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x2 + 2*x3 + 2*x4 | | | | | | | `- f5(x0,x1,x2) = 1 + 2*x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:50.659026 UTC(+0.034584s) | | | +- Interpretation | | | | | +- f222(x0) = 0 | | | | | +- f229(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | | | +- f230(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | | | +- f233(x0) = 0 | | | | | +- f234(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | | | +- f237(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x2 + 2*x3 | | | | | +- f239(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x2 + 2*x3 + 2*x4 | | | | | +- f240(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x2 + 2*x3 + 2*x4 | | | | | +- f246(x0,x1,x2) = x2 | | | | | `- f5(x0,x1,x2) = 1 + 2*x2 | | | +- Constraints | | | | | +- f5(x13,x14,0) + x16 = 1 + x16 >= x16 + 1 = f246(x13,x14,x16) + 1 | | | | | +- f5(x4,x5,(x9 + x10) + 1) + x7 = (1 + (2 * ((x9 + x10) + 1))) + x7 >= (2 + (x7 + ((2 * x9) + (2 * x10)))) + 1 = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 | | | | | +- f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) = 2 + (x7 + ((2 * x9) + (2 * x10))) >= 2 + (x7 + ((2 * x9) + (2 * x10))) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | | | +- f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = 2 + (x7 + ((2 * x9) + (2 * x10))) >= (1 + (2 * x10)) + (1 + (x7 + (2 * x9))) = f5(f233(x4),x5,x10) + f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | | | +- f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = 1 + (x7 + (2 * x9)) >= 1 + (x7 + (2 * x9)) = f234(x4,x5,x7,x9,x85,x86) | | | | | +- f234(x4,x5,x7,x9,x85,x86) = 1 + (x7 + (2 * x9)) >= 1 + (x7 + (2 * x9)) = f230(x4,x5,x7,x9,x85,x86) | | | | | +- f230(x4,x5,x7,x9,x85,x86) = 1 + (x7 + (2 * x9)) >= 1 + (x7 + (2 * x9)) = f229(x4,x5,x7,x9,x85,x86) | | | | | `- f229(x4,x5,x7,x9,x85,x86) = 1 + (x7 + (2 * x9)) >= (1 + (2 * x9)) + x7 = f5(f222(x4),x5,x9) + x7 | | | `- Stopping timer: 2017-03-30 07:29:50.659092 UTC(+0.190119s) | +- SCC-DECOMPOSE ... | | | +- SCC: 5 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.659206 UTC | | | +- Open Constraints | | | | | `- f7(x1,x2) = f7(x1,x2) >= 1 + x1 = f3(f212(),x1,x2) | | | +- Simplification ... | | | | | `- Propagated: f7(x0,x1) ↦ 1 + x0 | | | +- Interpretation | | | | | +- f212() = 0 | | | | | +- f3(x0,x1,x2) = 1 + x1 | | | | | `- f7(x0,x1) = 1 + x0 | | | +- Constraints | | | | | `- f7(x1,x2) = 1 + x1 >= 1 + x1 = f3(f212(),x1,x2) | | | `- Stopping timer: 2017-03-30 07:29:50.659276 UTC(+0.00007s) | +- SCC-DECOMPOSE ... | | | +- SCC: 4 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.659326 UTC | | | +- Open Constraints | | | | | `- f217(x1,x2,x3,x42,x43) = f217(x1,x2,x3,x42,x43) >= (1 + (2 * x2)) + x3 = f5(f212(),x1,x2) + x3 | | | +- Simplification ... | | | | | `- Substituted: f217(x1,x2,x3,x42,x43) ≥ f5(f212(),x1,x2) + x3 ↦ f217(x1,x2,x3,0,0) ≥ f5(f212(),x1,x2) + x3 | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.65937 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:50.666485 UTC(+0.007115s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.666497 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:50.670314 UTC(+0.003817s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.67032 UTC | | | | | +- Interpretation | | | | | | | `- f217(x0,x1,x2,x3,x4) = 3 + 16*x1 + 16*x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f217(x0,x1,x2,x3,x4) = 1 + 2*x1 + x2 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:50.676057 UTC(+0.005737s) | | | +- Interpretation | | | | | +- f212() = 0 | | | | | +- f217(x0,x1,x2,x3,x4) = 1 + 2*x1 + x2 | | | | | `- f5(x0,x1,x2) = 1 + 2*x2 | | | +- Constraints | | | | | `- f217(x1,x2,x3,x42,x43) = 1 + ((2 * x2) + x3) >= (1 + (2 * x2)) + x3 = f5(f212(),x1,x2) + x3 | | | `- Stopping timer: 2017-03-30 07:29:50.676095 UTC(+0.016769s) | +- SCC-DECOMPOSE ... | | | +- SCC: 3 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.676147 UTC | | | +- Open Constraints | | | | | +- f227(x4,x5,x9,0,0) = f227(x4,x5,x9,0,0) >= f4(0,x5,x9) = f4(f222(x4),x5,x9) | | | | | +- f4(x4,x5,(x9 + x10) + 1) = f4(x4,x5,(x9 + x10) + 1) >= (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 = (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 | | | | | +- f238(x4,x5,x10,0,0) = f238(x4,x5,x10,0,0) >= f4(0,x5,x10) = f4(f233(x4),x5,x10) | | | | | `- f4(0,0,0) = f4(0,0,0) >= 0 = 0 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.676234 UTC | | | | | +- Interpretation | | | | | | | +- f227(x0,x1,x2,x3,x4) = x2 | | | | | | | +- f238(x0,x1,x2,x3,x4) = max(x0,x2) | | | | | | | `- f4(x0,x1,x2) = x0 + x2 | | | | | +- Minimizing with ZeroOut ... | | | | | +- Interpretation | | | | | | | +- f227(x0,x1,x2,x3,x4) = x2 | | | | | | | +- f238(x0,x1,x2,x3,x4) = x2 | | | | | | | `- f4(x0,x1,x2) = x2 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with ShiftMax... Failed | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:50.736047 UTC(+0.059813s) | | | +- Interpretation | | | | | +- f222(x0) = 0 | | | | | +- f227(x0,x1,x2,x3,x4) = x2 | | | | | +- f233(x0) = 0 | | | | | +- f238(x0,x1,x2,x3,x4) = x2 | | | | | `- f4(x0,x1,x2) = x2 | | | +- Constraints | | | | | +- f227(x4,x5,x9,0,0) = x9 >= x9 = f4(f222(x4),x5,x9) | | | | | +- f4(x4,x5,(x9 + x10) + 1) = (x9 + x10) + 1 >= (x9 + x10) + 1 = (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 | | | | | +- f238(x4,x5,x10,0,0) = x10 >= x10 = f4(f233(x4),x5,x10) | | | | | `- f4(0,0,0) = 0 >= 0 = 0 | | | `- Stopping timer: 2017-03-30 07:29:50.7361 UTC(+0.059953s) | +- SCC-DECOMPOSE ... | | | +- SCC: 2 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.736122 UTC | | | +- Open Constraints | | | | | `- f9(x1,x2) + x3 = f9(x1,x2) + x3 >= (1 + ((2 * x2) + x3)) + 1 = f217(x1,x2,x3,x42,x43) + 1 | | | +- Simplification ... | | | +- SMT-MSLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.736176 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:50.740529 UTC(+0.004353s) | | | +- SMT-SLI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.740539 UTC | | | | | `- Stopping timer: 2017-03-30 07:29:50.745471 UTC(+0.004932s) | | | +- SMT-LI ... | | | | | +- Staring timer: 2017-03-30 07:29:50.745484 UTC | | | | | +- Interpretation | | | | | | | `- f9(x0,x1) = 16 + 8*x1 | | | | | +- Minimizing with ZeroOut... Failed | | | | | +- Minimizing with DecreaseCoeff ... | | | | | +- Interpretation | | | | | | | `- f9(x0,x1) = 2 + 2*x1 | | | | | +- Minimizing with DecreaseCoeff... Failed | | | | | `- Stopping timer: 2017-03-30 07:29:50.750935 UTC(+0.005451s) | | | +- Interpretation | | | | | +- f217(x0,x1,x2,x3,x4) = 1 + 2*x1 + x2 | | | | | `- f9(x0,x1) = 2 + 2*x1 | | | +- Constraints | | | | | `- f9(x1,x2) + x3 = (2 + (2 * x2)) + x3 >= (1 + ((2 * x2) + x3)) + 1 = f217(x1,x2,x3,x42,x43) + 1 | | | `- Stopping timer: 2017-03-30 07:29:50.750985 UTC(+0.014863s) | +- SCC-DECOMPOSE ... | | | +- SCC: 1 SCCs | | | `- SOLVE ... | | | +- Staring timer: 2017-03-30 07:29:50.751003 UTC | | | +- Open Constraints | | | | | `- f8(x1,x2) = f8(x1,x2) >= x2 = f4(f212(),x1,x2) | | | +- Simplification ... | | | | | `- Propagated: f8(x0,x1) ↦ x1 | | | +- Interpretation | | | | | +- f212() = 0 | | | | | +- f4(x0,x1,x2) = x2 | | | | | `- f8(x0,x1) = x1 | | | +- Constraints | | | | | `- f8(x1,x2) = x2 >= x2 = f4(f212(),x1,x2) | | | `- Stopping timer: 2017-03-30 07:29:50.751076 UTC(+0.000073s) | +- Interpretation | | | +- f1(x0,x1) = 1 + x0 | | | +- f2(x0,x1) = 0 | | | +- f208(x0) = x0 | | | +- f209(x0) = x0 | | | +- f210(x0) = x0 | | | +- f211(x0) = x0 | | | +- f212() = 0 | | | +- f213(x0) = x0 | | | +- f214(x0) = x0 | | | +- f215(x0) = x0 | | | +- f216(x0,x1,x2,x3,x4) = x2 | | | +- f217(x0,x1,x2,x3,x4) = 1 + 2*x1 + x2 | | | +- f218(x0) = x0 | | | +- f219(x0) = x0 | | | +- f220(x0) = x0 | | | +- f221(x0) = x0 | | | +- f222(x0) = 0 | | | +- f223(x0) = x0 | | | +- f224(x0) = x0 | | | +- f225(x0) = x0 | | | +- f226(x0,x1,x2,x3,x4,x5) = x2 | | | +- f227(x0,x1,x2,x3,x4) = x2 | | | +- f228(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x1 | | | +- f229(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | +- f230(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | +- f231(x0) = x0 | | | +- f232(x0) = x0 | | | +- f233(x0) = 0 | | | +- f234(x0,x1,x2,x3,x4,x5) = 1 + x2 + 2*x3 | | | +- f235(x0) = x0 | | | +- f236(x0) = x0 | | | +- f237(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 1 + x2 + 2*x3 | | | +- f238(x0,x1,x2,x3,x4) = x2 | | | +- f239(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x2 + 2*x3 + 2*x4 | | | +- f240(x0,x1,x2,x3,x4,x5,x6,x7,x8) = 2 + x2 + 2*x3 + 2*x4 | | | +- f241(x0) = x0 | | | +- f242(x0) = x0 | | | +- f243(x0) = x0 | | | +- f244(x0,x1) = 1 + x1 | | | +- f245(x0,x1,x2) = x2 | | | +- f246(x0,x1,x2) = x2 | | | +- f3(x0,x1,x2) = 1 + x1 | | | +- f4(x0,x1,x2) = x2 | | | +- f5(x0,x1,x2) = 1 + 2*x2 | | | +- f6(x0,x1,x2,x3) = 0 | | | +- f7(x0,x1) = 1 + x0 | | | +- f8(x0,x1) = x1 | | | `- f9(x0,x1) = 2 + 2*x1 | +- Constraints | | | +- f208(x3) = x3 >= x3 = x3 | | | +- f209(x3) = x3 >= x3 = f208(x3) | | | +- f210(x42) = x42 >= x42 = x42 | | | +- f211(x43) = x43 >= x43 = x43 | | | +- f1(x42,f212()) = 1 + x42 >= x42 + 1 = f210(x42) + 1 | | | +- f2(x42,f212()) + x43 = x43 >= x43 = f211(x43) | | | +- f213(x3) = x3 >= x3 = f209(x3) | | | +- f214(x2) = x2 >= x2 = x2 | | | +- f215(x1) = x1 >= x1 = x1 | | | +- f216(x1,x2,x3,x42,x43) = x3 >= x3 = f6(f212(),f215(x1),f214(x2),f216(x1,x2,x3,x42,x43)) + f213(x3) | | | +- f217(x1,x2,x3,x42,x43) = 1 + ((2 * x2) + x3) >= (1 + (2 * x2)) + x3 = f5(f212(),f215(x1),f214(x2)) + f216(x1,x2,x3,x42,x43) | | | +- f8(x1,x2) = x2 >= x2 = f4(f212(),f215(x1),f214(x2)) | | | +- f7(x1,x2) = 1 + x1 >= 1 + x1 = f3(f212(),f215(x1),f214(x2)) | | | +- f9(x1,x2) + x3 = (2 + (2 * x2)) + x3 >= (1 + ((2 * x2) + x3)) + 1 = f217(x1,x2,x3,x42,x43) + 1 | | | +- f218(x7) = x7 >= x7 = x7 | | | +- f219(x7) = x7 >= x7 = f218(x7) | | | +- f220(x85) = x85 >= x85 = x85 | | | +- f221(x86) = x86 >= x86 = x86 | | | +- f1(x85,f222(x4)) = 1 + x85 >= 1 + x85 = f1(f220(x85),x4) | | | +- f2(x85,f222(x4)) + x86 = x86 >= x86 = f2(f220(x85),x4) + f221(x86) | | | +- f223(x7) = x7 >= x7 = f219(x7) | | | +- f224(x9) = x9 >= x9 = x9 | | | +- f225(x5) = x5 >= x5 = x5 | | | +- f226(x4,x5,x7,x9,x85,x86) = x7 >= x7 = f6(f222(x4),f225(x5),f224(x9),f226(x4,x5,x7,x9,x85,x86)) + f223(x7) | | | +- f227(x4,x5,x9,x85,x86) = x9 >= x9 = f4(f222(x4),f225(x5),f224(x9)) | | | +- f228(x4,x5,x9,x10,x85,x86,x134,x135) = 1 + x5 >= 1 + x5 = f3(f222(x4),f225(x5),f224(x9)) | | | +- f229(x4,x5,x7,x9,x85,x86) = 1 + (x7 + (2 * x9)) >= (1 + (2 * x9)) + x7 = f5(f222(x4),f225(x5),f224(x9)) + f226(x4,x5,x7,x9,x85,x86) | | | +- f230(x4,x5,x7,x9,x85,x86) = 1 + (x7 + (2 * x9)) >= 1 + (x7 + (2 * x9)) = f229(x4,x5,x7,x9,x85,x86) | | | +- f231(x134) = x134 >= x134 = x134 | | | +- f232(x135) = x135 >= x135 = x135 | | | +- f1(x134,f233(x4)) = 1 + x134 >= 1 + x134 = f1(f231(x134),x4) | | | +- f2(x134,f233(x4)) + x135 = x135 >= x135 = f2(f231(x134),x4) + f232(x135) | | | +- f234(x4,x5,x7,x9,x85,x86) = 1 + (x7 + (2 * x9)) >= 1 + (x7 + (2 * x9)) = f230(x4,x5,x7,x9,x85,x86) | | | +- f235(x10) = x10 >= x10 = x10 | | | +- f236(x5) = x5 >= x5 = x5 | | | +- f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) = 1 + (x7 + (2 * x9)) >= 1 + (x7 + (2 * x9)) = f6(f233(x4),f236(x5),f235(x10),f237(x4,x5,x7,x9,x10,x85,x86,x134,x135)) + f234(x4,x5,x7,x9,x85,x86) | | | +- f238(x4,x5,x10,x134,x135) = x10 >= x10 = f4(f233(x4),f236(x5),f235(x10)) | | | +- f228(x4,x5,x9,x10,x85,x86,x134,x135) = 1 + x5 >= 1 + x5 = f3(f233(x4),f236(x5),f235(x10)) | | | +- f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) = 2 + (x7 + ((2 * x9) + (2 * x10))) >= (1 + (2 * x10)) + (1 + (x7 + (2 * x9))) = f5(f233(x4),f236(x5),f235(x10)) + f237(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | +- f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) = 2 + (x7 + ((2 * x9) + (2 * x10))) >= 2 + (x7 + ((2 * x9) + (2 * x10))) = f239(x4,x5,x7,x9,x10,x85,x86,x134,x135) | | | +- f4(x4,x5,(x9 + x10) + 1) = (x9 + x10) + 1 >= (x9 + x10) + 1 = (f227(x4,x5,x9,x85,x86) + f238(x4,x5,x10,x134,x135)) + 1 | | | +- f3(x4,x5,(x9 + x10) + 1) = 1 + x5 >= 1 + x5 = f228(x4,x5,x9,x10,x85,x86,x134,x135) | | | +- f5(x4,x5,(x9 + x10) + 1) + x7 = (1 + (2 * ((x9 + x10) + 1))) + x7 >= (2 + (x7 + ((2 * x9) + (2 * x10)))) + 1 = f240(x4,x5,x7,x9,x10,x85,x86,x134,x135) + 1 | | | +- f241(x16) = x16 >= x16 = x16 | | | +- f242(x14) = x14 >= x14 = x14 | | | +- f243(x16) = x16 >= x16 = f241(x16) | | | +- f244(x13,x14) = 1 + x14 >= 1 + x14 = f1(f242(x14),x13) | | | +- f245(x13,x14,x16) = x16 >= x16 = f2(f242(x14),x13) + f243(x16) | | | +- f246(x13,x14,x16) = x16 >= x16 = f245(x13,x14,x16) | | | +- f4(x13,x14,0) = 0 >= 0 = 0 | | | +- f3(x13,x14,0) = 1 + x14 >= 1 + x14 = f244(x13,x14) | | | `- f5(x13,x14,0) + x16 = 1 + x16 >= x16 + 1 = f246(x13,x14,x16) + 1 | `- Stopping timer: 2017-03-30 07:29:50.751274 UTC(+0.347209s)