SUCCESS(2) SUCCESS f1(x0,x1) = 9 + 9*x0 + x1; f10(x0,x1,x2) = 9 + 14*x0 + 10*x0*x1 + 14*x0*x2 + 15*x1 + 15*x1*x2 + 14*x2; f11(x0,x1,x2) = 15 + 8*x0 + 12*x0*x1 + 8*x0*x2 + 14*x1 + 15*x1*x2 + 8*x2; f12(x0,x1,x2) = 15 + 14*x0 + 15*x0*x1 + 14*x0*x2 + 8*x1 + 14*x1*x2 + 15*x2; f191(x0) = x0; f192(x0) = x0; f193(x0) = 3*x0; f194(x0) = x0; f195(x0) = 2*x0; f196(x0) = x0; f197(x0) = 1 + 2*x0; f198(x0,x1,x2,x3) = x1; f199(x0) = x0; f2(x0,x1) = 7 + 2*x0 + x1; f200(x0) = x0; f201(x0,x1,x2,x3,x4,x5) = 11*x0*x1 + x3; f202(x0,x1,x2,x3,x4,x5) = 14 + 14*x0 + 15*x0*x1 + 14*x0*x2 + 6*x1 + 10*x1*x2 + 15*x2 + x3; f203(x0) = x0; f204(x0) = x0; f205(x0) = x0; f206(x0) = x0; f207(x0) = x0; f208(x0) = 1 + x0; f209(x0,x1,x2) = x1; f210(x0,x1) = 12 + x0 + 9*x1; f211(x0,x1,x2) = 8 + x0 + x1 + 2*x2; f212(x0,x1,x2) = 8 + x0 + x1 + 2*x2; f213(x0) = 4 + x0; f214(x0) = x0; f215(x0) = x0; f216(x0) = x0; f217(x0,x1,x2,x3,x4) = 14*x0 + 2*x0*x1 + 7*x0*x2 + 12*x1 + 15*x1*x2 + x2; f218(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2; f219(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2; f220(x0) = x0; f221(x0) = x0; f222(x0) = x0; f223(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2; f224(x0) = x0; f225(x0) = x0; f226(x0,x1,x2,x3,x4,x5) = 5 + 3*x0 + 2*x1 + x2; f227(x0,x1,x2,x3,x4) = 7 + 3*x0 + 5*x0*x1 + 3*x0*x2 + 10*x1 + 15*x1*x2 + 3*x2; f228(x0,x1,x2,x3,x4,x5) = 13 + 12*x0 + x0*x1 + 7*x0*x3 + 7*x1 + 8*x1*x3 + x2 + 8*x3; f229(x0,x1,x2,x3,x4,x5) = 15 + 13*x0 + x0*x1 + 7*x0*x3 + 8*x1 + 8*x1*x3 + x2 + 8*x3; f230(x0) = x0; f231(x0) = 3 + x0; f232() = 0; f3(x0,x1,x2) = 0; f4(x0,x1) = 4*x0 + 2*x0*x1 + 14*x1; f5(x0,x1) = 5 + 2*x0 + 3*x1; f6(x0,x1,x2) = 7*x0 + 2*x0*x1 + 7*x0*x2 + 7*x1 + 15*x1*x2 + x2; f7(x0,x1,x2) = 6 + 3*x0 + 5*x0*x1 + 3*x0*x2 + 9*x1 + 15*x1*x2 + 3*x2; f8(x0,x1,x2) = 8 + 6*x0 + x0*x1 + 7*x0*x2 + 5*x1 + 8*x1*x2 + 8*x2; f9(x0,x1,x2,x3) = 0; ExecutionLog | `- SOLVE ... | +- Staring timer: 2017-03-30 07:32:40.807899 UTC | +- Open Constraints | | | +- f191(x5) = f191(x5) >= x5 = x5 | | | +- f192(x5) = f192(x5) >= f191(x5) = f191(x5) | | | +- f193(x2) = f193(x2) >= x2 = x2 | | | +- f194(x5) = f194(x5) >= f192(x5) = f192(x5) | | | +- f195(x66) = f195(x66) >= x66 = x66 | | | +- f196(x67) = f196(x67) >= x67 = x67 | | | +- f4(x66,f197(x2)) = f4(x66,f197(x2)) >= f1(f193(x2),f195(x66)) = f1(f193(x2),f195(x66)) | | | +- f5(x66,f197(x2)) + x67 = f5(x66,f197(x2)) + x67 >= f2(f193(x2),f195(x66)) + f196(x67) = f2(f193(x2),f195(x66)) + f196(x67) | | | +- f198(x2,x5,x66,x67) = f198(x2,x5,x66,x67) >= f3(f193(x2),f195(x66),f196(x67)) + f194(x5) = f3(f193(x2),f195(x66),f196(x67)) + f194(x5) | | | +- f199(x4) = f199(x4) >= x4 = x4 | | | +- f200(x3) = f200(x3) >= x3 = x3 | | | +- f201(x2,x3,x4,x5,x66,x67) = f201(x2,x3,x4,x5,x66,x67) >= f9(f197(x2),f200(x3),f199(x4),f201(x2,x3,x4,x5,x66,x67)) + f198(x2,x5,x66,x67) = f9(f197(x2),f200(x3),f199(x4),f201(x2,x3,x4,x5,x66,x67)) + f198(x2,x5,x66,x67) | | | +- f202(x2,x3,x4,x5,x66,x67) = f202(x2,x3,x4,x5,x66,x67) >= f8(f197(x2),f200(x3),f199(x4)) + f201(x2,x3,x4,x5,x66,x67) = f8(f197(x2),f200(x3),f199(x4)) + f201(x2,x3,x4,x5,x66,x67) | | | +- f11(x2,x3,x4) = f11(x2,x3,x4) >= f7(f197(x2),f200(x3),f199(x4)) = f7(f197(x2),f200(x3),f199(x4)) | | | +- f10(x2,x3,x4) = f10(x2,x3,x4) >= f6(f197(x2),f200(x3),f199(x4)) = f6(f197(x2),f200(x3),f199(x4)) | | | +- f12(x2,x3,x4) + x5 = f12(x2,x3,x4) + x5 >= f202(x2,x3,x4,x5,x66,x67) + 1 = f202(x2,x3,x4,x5,x66,x67) + 1 | | | +- f203(x9) = f203(x9) >= x9 = x9 | | | +- f204(x9) = f204(x9) >= f203(x9) = f203(x9) | | | +- f205(x9) = f205(x9) >= f204(x9) = f204(x9) | | | +- f206(x11) = f206(x11) >= x11 = x11 | | | +- f207(x9) = f207(x9) >= f205(x9) = f205(x9) | | | +- f208(x8) = f208(x8) >= x8 = x8 | | | +- f209(x8,x9,x11) = f209(x8,x9,x11) >= f3(f206(x11),f208(x8),f209(x8,x9,x11)) + f207(x9) = f3(f206(x11),f208(x8),f209(x8,x9,x11)) + f207(x9) | | | +- f210(x8,x11) = f210(x8,x11) >= f1(f206(x11),f208(x8)) = f1(f206(x11),f208(x8)) | | | +- f211(x8,x9,x11) = f211(x8,x9,x11) >= f2(f206(x11),f208(x8)) + f209(x8,x9,x11) = f2(f206(x11),f208(x8)) + f209(x8,x9,x11) | | | +- f212(x8,x9,x11) = f212(x8,x9,x11) >= f211(x8,x9,x11) = f211(x8,x9,x11) | | | +- f1(x11 + 1,x8) = f1(x11 + 1,x8) >= f210(x8,x11) + 1 = f210(x8,x11) + 1 | | | +- f2(x11 + 1,x8) + x9 = f2(x11 + 1,x8) + x9 >= f212(x8,x9,x11) + 1 = f212(x8,x9,x11) + 1 | | | +- f213(x15) = f213(x15) >= x15 = x15 | | | +- f1(0,x14) = f1(0,x14) >= x14 = x14 | | | +- f2(0,x14) + x15 = f2(0,x14) + x15 >= f213(x15) + 1 = f213(x15) + 1 | | | +- f214(x21) = f214(x21) >= x21 = x21 | | | +- f215(x19) = f215(x19) >= x19 = x19 | | | +- f216(x21) = f216(x21) >= f214(x21) = f214(x21) | | | +- f217(x18,x19,x23,x145,x146) = f217(x18,x19,x23,x145,x146) >= f4(f215(x19),x18) = f4(f215(x19),x18) | | | +- f218(x18,x19,x21) = f218(x18,x19,x21) >= f5(f215(x19),x18) + f216(x21) = f5(f215(x19),x18) + f216(x21) | | | +- f219(x18,x19,x21) = f219(x18,x19,x21) >= f218(x18,x19,x21) = f218(x18,x19,x21) | | | +- f220(x145) = f220(x145) >= x145 = x145 | | | +- f221(x146) = f221(x146) >= x146 = x146 | | | +- f4(x145,f222(x18)) = f4(x145,f222(x18)) >= f4(f220(x145),x18) = f4(f220(x145),x18) | | | +- f5(x145,f222(x18)) + x146 = f5(x145,f222(x18)) + x146 >= f5(f220(x145),x18) + f221(x146) = f5(f220(x145),x18) + f221(x146) | | | +- f223(x18,x19,x21) = f223(x18,x19,x21) >= f219(x18,x19,x21) = f219(x18,x19,x21) | | | +- f224(x23) = f224(x23) >= x23 = x23 | | | +- f225(x19) = f225(x19) >= x19 = x19 | | | +- f226(x18,x19,x21,x23,x145,x146) = f226(x18,x19,x21,x23,x145,x146) >= f9(f222(x18),f225(x19),f224(x23),f226(x18,x19,x21,x23,x145,x146)) + f223(x18,x19,x21) = f9(f222(x18) ,f225(x19) ,f224(x23) ,f226(x18,x19,x21,x23,x145,x146)) + f223(x18,x19,x21) | | | +- f227(x18,x19,x23,x145,x146) = f227(x18,x19,x23,x145,x146) >= f7(f222(x18),f225(x19),f224(x23)) = f7(f222(x18),f225(x19),f224(x23)) | | | +- f217(x18,x19,x23,x145,x146) = f217(x18,x19,x23,x145,x146) >= f6(f222(x18),f225(x19),f224(x23)) = f6(f222(x18),f225(x19),f224(x23)) | | | +- f228(x18,x19,x21,x23,x145,x146) = f228(x18,x19,x21,x23,x145,x146) >= f8(f222(x18),f225(x19),f224(x23)) + f226(x18,x19,x21,x23,x145,x146) = f8(f222(x18),f225(x19),f224(x23)) + f226(x18 ,x19 ,x21 ,x23 ,x145 ,x146) | | | +- f229(x18,x19,x21,x23,x145,x146) = f229(x18,x19,x21,x23,x145,x146) >= f228(x18,x19,x21,x23,x145,x146) = f228(x18,x19,x21,x23,x145,x146) | | | +- f7(x18,x19,x23 + 1) = f7(x18,x19,x23 + 1) >= f227(x18,x19,x23,x145,x146) + 1 = f227(x18,x19,x23,x145,x146) + 1 | | | +- f6(x18,x19,x23 + 1) = f6(x18,x19,x23 + 1) >= f217(x18,x19,x23,x145,x146) = f217(x18,x19,x23,x145,x146) | | | +- f8(x18,x19,x23 + 1) + x21 = f8(x18,x19,x23 + 1) + x21 >= f229(x18,x19,x21,x23,x145,x146) + 1 = f229(x18,x19,x21,x23,x145,x146) + 1 | | | +- f230(x30) = f230(x30) >= x30 = x30 | | | +- f231(x30) = f231(x30) >= f230(x30) = f230(x30) | | | +- f7(x27,x28,0) = f7(x27,x28,0) >= 0 = 0 | | | +- f6(x27,x28,0) = f6(x27,x28,0) >= f232() = f232() | | | `- f8(x27,x28,0) + x30 = f8(x27,x28,0) + x30 >= f231(x30) + 1 = f231(x30) + 1 | +- SMT-SLI ... | | | +- Staring timer: 2017-03-30 07:32:40.808128 UTC | | | `- Stopping timer: 2017-03-30 07:32:40.84668 UTC(+0.038552s) | +- SMT-LI ... | | | +- Staring timer: 2017-03-30 07:32:40.846687 UTC | | | `- Stopping timer: 2017-03-30 07:32:41.130606 UTC(+0.283919s) | +- SMT-MMI(2) ... | | | +- Staring timer: 2017-03-30 07:32:41.130614 UTC | | | +- Interpretation | | | | | +- f1(x0,x1) = 9 + 9*x0 + x1 | | | | | +- f10(x0,x1,x2) = 9 + 14*x0 + 10*x0*x1 + 14*x0*x2 + 15*x1 + 15*x1*x2 + 14*x2 | | | | | +- f11(x0,x1,x2) = 15 + 8*x0 + 12*x0*x1 + 8*x0*x2 + 14*x1 + 15*x1*x2 + 8*x2 | | | | | +- f12(x0,x1,x2) = 15 + 14*x0 + 15*x0*x1 + 14*x0*x2 + 8*x1 + 14*x1*x2 + 15*x2 | | | | | +- f191(x0) = x0 | | | | | +- f192(x0) = x0 | | | | | +- f193(x0) = 3*x0 | | | | | +- f194(x0) = x0 | | | | | +- f195(x0) = 2*x0 | | | | | +- f196(x0) = x0 | | | | | +- f197(x0) = 1 + 2*x0 | | | | | +- f198(x0,x1,x2,x3) = x1 | | | | | +- f199(x0) = x0 | | | | | +- f2(x0,x1) = 7 + 2*x0 + x1 | | | | | +- f200(x0) = x0 | | | | | +- f201(x0,x1,x2,x3,x4,x5) = 11*x0*x1 + x3 | | | | | +- f202(x0,x1,x2,x3,x4,x5) = 14 + 14*x0 + 15*x0*x1 + 14*x0*x2 + 6*x1 + 10*x1*x2 + 15*x2 + x3 | | | | | +- f203(x0) = x0 | | | | | +- f204(x0) = x0 | | | | | +- f205(x0) = x0 | | | | | +- f206(x0) = x0 | | | | | +- f207(x0) = x0 | | | | | +- f208(x0) = 1 + x0 | | | | | +- f209(x0,x1,x2) = x1 | | | | | +- f210(x0,x1) = 12 + x0 + 9*x1 | | | | | +- f211(x0,x1,x2) = 8 + x0 + x1 + 2*x2 | | | | | +- f212(x0,x1,x2) = 8 + x0 + x1 + 2*x2 | | | | | +- f213(x0) = 4 + x0 | | | | | +- f214(x0) = x0 | | | | | +- f215(x0) = x0 | | | | | +- f216(x0) = x0 | | | | | +- f217(x0,x1,x2,x3,x4) = 14*x0 + 2*x0*x1 + 7*x0*x2 + 12*x1 + 15*x1*x2 + x2 | | | | | +- f218(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2 | | | | | +- f219(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2 | | | | | +- f220(x0) = x0 | | | | | +- f221(x0) = x0 | | | | | +- f222(x0) = x0 | | | | | +- f223(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2 | | | | | +- f224(x0) = x0 | | | | | +- f225(x0) = x0 | | | | | +- f226(x0,x1,x2,x3,x4,x5) = 5 + 3*x0 + 2*x1 + x2 | | | | | +- f227(x0,x1,x2,x3,x4) = 7 + 3*x0 + 5*x0*x1 + 3*x0*x2 + 10*x1 + 15*x1*x2 + 3*x2 | | | | | +- f228(x0,x1,x2,x3,x4,x5) = 13 + 12*x0 + x0*x1 + 7*x0*x3 + 7*x1 + 8*x1*x3 + x2 + 8*x3 | | | | | +- f229(x0,x1,x2,x3,x4,x5) = 15 + 13*x0 + x0*x1 + 7*x0*x3 + 8*x1 + 8*x1*x3 + x2 + 8*x3 | | | | | +- f230(x0) = x0 | | | | | +- f231(x0) = 3 + x0 | | | | | +- f232() = 0 | | | | | +- f3(x0,x1,x2) = 0 | | | | | +- f4(x0,x1) = 4*x0 + 2*x0*x1 + 14*x1 | | | | | +- f5(x0,x1) = 5 + 2*x0 + 3*x1 | | | | | +- f6(x0,x1,x2) = 7*x0 + 2*x0*x1 + 7*x0*x2 + 7*x1 + 15*x1*x2 + x2 | | | | | +- f7(x0,x1,x2) = 6 + 3*x0 + 5*x0*x1 + 3*x0*x2 + 9*x1 + 15*x1*x2 + 3*x2 | | | | | +- f8(x0,x1,x2) = 8 + 6*x0 + x0*x1 + 7*x0*x2 + 5*x1 + 8*x1*x2 + 8*x2 | | | | | `- f9(x0,x1,x2,x3) = 0 | | | `- Stopping timer: 2017-03-30 07:32:45.852278 UTC(+4.721664s) | +- Interpretation | | | +- f1(x0,x1) = 9 + 9*x0 + x1 | | | +- f10(x0,x1,x2) = 9 + 14*x0 + 10*x0*x1 + 14*x0*x2 + 15*x1 + 15*x1*x2 + 14*x2 | | | +- f11(x0,x1,x2) = 15 + 8*x0 + 12*x0*x1 + 8*x0*x2 + 14*x1 + 15*x1*x2 + 8*x2 | | | +- f12(x0,x1,x2) = 15 + 14*x0 + 15*x0*x1 + 14*x0*x2 + 8*x1 + 14*x1*x2 + 15*x2 | | | +- f191(x0) = x0 | | | +- f192(x0) = x0 | | | +- f193(x0) = 3*x0 | | | +- f194(x0) = x0 | | | +- f195(x0) = 2*x0 | | | +- f196(x0) = x0 | | | +- f197(x0) = 1 + 2*x0 | | | +- f198(x0,x1,x2,x3) = x1 | | | +- f199(x0) = x0 | | | +- f2(x0,x1) = 7 + 2*x0 + x1 | | | +- f200(x0) = x0 | | | +- f201(x0,x1,x2,x3,x4,x5) = 11*x0*x1 + x3 | | | +- f202(x0,x1,x2,x3,x4,x5) = 14 + 14*x0 + 15*x0*x1 + 14*x0*x2 + 6*x1 + 10*x1*x2 + 15*x2 + x3 | | | +- f203(x0) = x0 | | | +- f204(x0) = x0 | | | +- f205(x0) = x0 | | | +- f206(x0) = x0 | | | +- f207(x0) = x0 | | | +- f208(x0) = 1 + x0 | | | +- f209(x0,x1,x2) = x1 | | | +- f210(x0,x1) = 12 + x0 + 9*x1 | | | +- f211(x0,x1,x2) = 8 + x0 + x1 + 2*x2 | | | +- f212(x0,x1,x2) = 8 + x0 + x1 + 2*x2 | | | +- f213(x0) = 4 + x0 | | | +- f214(x0) = x0 | | | +- f215(x0) = x0 | | | +- f216(x0) = x0 | | | +- f217(x0,x1,x2,x3,x4) = 14*x0 + 2*x0*x1 + 7*x0*x2 + 12*x1 + 15*x1*x2 + x2 | | | +- f218(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2 | | | +- f219(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2 | | | +- f220(x0) = x0 | | | +- f221(x0) = x0 | | | +- f222(x0) = x0 | | | +- f223(x0,x1,x2) = 5 + 3*x0 + 2*x1 + x2 | | | +- f224(x0) = x0 | | | +- f225(x0) = x0 | | | +- f226(x0,x1,x2,x3,x4,x5) = 5 + 3*x0 + 2*x1 + x2 | | | +- f227(x0,x1,x2,x3,x4) = 7 + 3*x0 + 5*x0*x1 + 3*x0*x2 + 10*x1 + 15*x1*x2 + 3*x2 | | | +- f228(x0,x1,x2,x3,x4,x5) = 13 + 12*x0 + x0*x1 + 7*x0*x3 + 7*x1 + 8*x1*x3 + x2 + 8*x3 | | | +- f229(x0,x1,x2,x3,x4,x5) = 15 + 13*x0 + x0*x1 + 7*x0*x3 + 8*x1 + 8*x1*x3 + x2 + 8*x3 | | | +- f230(x0) = x0 | | | +- f231(x0) = 3 + x0 | | | +- f232() = 0 | | | +- f3(x0,x1,x2) = 0 | | | +- f4(x0,x1) = 4*x0 + 2*x0*x1 + 14*x1 | | | +- f5(x0,x1) = 5 + 2*x0 + 3*x1 | | | +- f6(x0,x1,x2) = 7*x0 + 2*x0*x1 + 7*x0*x2 + 7*x1 + 15*x1*x2 + x2 | | | +- f7(x0,x1,x2) = 6 + 3*x0 + 5*x0*x1 + 3*x0*x2 + 9*x1 + 15*x1*x2 + 3*x2 | | | +- f8(x0,x1,x2) = 8 + 6*x0 + x0*x1 + 7*x0*x2 + 5*x1 + 8*x1*x2 + 8*x2 | | | `- f9(x0,x1,x2,x3) = 0 | +- Constraints | | | +- f191(x5) = x5 >= x5 = x5 | | | +- f192(x5) = x5 >= x5 = f191(x5) | | | +- f193(x2) = 3 * x2 >= x2 = x2 | | | +- f194(x5) = x5 >= x5 = f192(x5) | | | +- f195(x66) = 2 * x66 >= x66 = x66 | | | +- f196(x67) = x67 >= x67 = x67 | | | +- f4(x66,f197(x2)) = (4 * x66) + ((2 * (x66 * (1 + (2 * x2)))) + (14 * (1 + (2 * x2)))) >= 9 + ((9 * (3 * x2)) + (2 * x66)) = f1(f193(x2),f195(x66)) | | | +- f5(x66,f197(x2)) + x67 = (5 + ((2 * x66) + (3 * (1 + (2 * x2))))) + x67 >= (7 + ((2 * (3 * x2)) + (2 * x66))) + x67 = f2(f193(x2),f195(x66)) + f196(x67) | | | +- f198(x2,x5,x66,x67) = x5 >= x5 = f3(f193(x2),f195(x66),f196(x67)) + f194(x5) | | | +- f199(x4) = x4 >= x4 = x4 | | | +- f200(x3) = x3 >= x3 = x3 | | | +- f201(x2,x3,x4,x5,x66,x67) = (11 * (x2 * x3)) + x5 >= x5 = f9(f197(x2),f200(x3),f199(x4),f201(x2,x3,x4,x5,x66,x67)) + f198(x2,x5,x66,x67) | | | +- f202(x2,x3,x4,x5,x66,x67) = 14 + ((14 * x2) + ((15 * (x2 * x3)) + ((14 * (x2 * x4)) + ((6 * x3) + ((10 * (x3 * x4)) + ((15 * x4) + x5)))))) >= (8 + ((6 * (1 + (2 * x2))) + (((1 + (2 * x2)) * x3) + ((7 * ((1 + (2 * x2)) * x4)) + ((5 * x3) + ((8 * (x3 * x4)) + (8 * x4))))))) + ((11 * (x2 * x3)) + x5) = f8(f197(x2),f200(x3),f199(x4)) + f201(x2,x3,x4,x5,x66,x67) | | | +- f11(x2,x3,x4) = 15 + ((8 * x2) + ((12 * (x2 * x3)) + ((8 * (x2 * x4)) + ((14 * x3) + ((15 * (x3 * x4)) + (8 * x4)))))) >= 6 + ((3 * (1 + (2 * x2))) + ((5 * ((1 + (2 * x2)) * x3)) + ((3 * ((1 + (2 * x2)) * x4)) + ((9 * x3) + ((15 * (x3 * x4)) + (3 * x4)))))) = f7(f197(x2),f200(x3),f199(x4)) | | | +- f10(x2,x3,x4) = 9 + ((14 * x2) + ((10 * (x2 * x3)) + ((14 * (x2 * x4)) + ((15 * x3) + ((15 * (x3 * x4)) + (14 * x4)))))) >= (7 * (1 + (2 * x2))) + ((2 * ((1 + (2 * x2)) * x3)) + ((7 * ((1 + (2 * x2)) * x4)) + ((7 * x3) + ((15 * (x3 * x4)) + x4)))) = f6(f197(x2),f200(x3),f199(x4)) | | | +- f12(x2,x3,x4) + x5 = (15 + ((14 * x2) + ((15 * (x2 * x3)) + ((14 * (x2 * x4)) + ((8 * x3) + ((14 * (x3 * x4)) + (15 * x4))))))) + x5 >= (14 + ((14 * x2) + ((15 * (x2 * x3)) + ((14 * (x2 * x4)) + ((6 * x3) + ((10 * (x3 * x4)) + ((15 * x4) + x5))))))) + 1 = f202(x2,x3,x4,x5,x66,x67) + 1 | | | +- f203(x9) = x9 >= x9 = x9 | | | +- f204(x9) = x9 >= x9 = f203(x9) | | | +- f205(x9) = x9 >= x9 = f204(x9) | | | +- f206(x11) = x11 >= x11 = x11 | | | +- f207(x9) = x9 >= x9 = f205(x9) | | | +- f208(x8) = 1 + x8 >= x8 = x8 | | | +- f209(x8,x9,x11) = x9 >= x9 = f3(f206(x11),f208(x8),f209(x8,x9,x11)) + f207(x9) | | | +- f210(x8,x11) = 12 + (x8 + (9 * x11)) >= 9 + ((9 * x11) + (1 + x8)) = f1(f206(x11),f208(x8)) | | | +- f211(x8,x9,x11) = 8 + (x8 + (x9 + (2 * x11))) >= (7 + ((2 * x11) + (1 + x8))) + x9 = f2(f206(x11),f208(x8)) + f209(x8,x9,x11) | | | +- f212(x8,x9,x11) = 8 + (x8 + (x9 + (2 * x11))) >= 8 + (x8 + (x9 + (2 * x11))) = f211(x8,x9,x11) | | | +- f1(x11 + 1,x8) = 9 + ((9 * (x11 + 1)) + x8) >= (12 + (x8 + (9 * x11))) + 1 = f210(x8,x11) + 1 | | | +- f2(x11 + 1,x8) + x9 = (7 + ((2 * (x11 + 1)) + x8)) + x9 >= (8 + (x8 + (x9 + (2 * x11)))) + 1 = f212(x8,x9,x11) + 1 | | | +- f213(x15) = 4 + x15 >= x15 = x15 | | | +- f1(0,x14) = 9 + x14 >= x14 = x14 | | | +- f2(0,x14) + x15 = (7 + x14) + x15 >= (4 + x15) + 1 = f213(x15) + 1 | | | +- f214(x21) = x21 >= x21 = x21 | | | +- f215(x19) = x19 >= x19 = x19 | | | +- f216(x21) = x21 >= x21 = f214(x21) | | | +- f217(x18,x19,x23,x145,x146) = (14 * x18) + ((2 * (x18 * x19)) + ((7 * (x18 * x23)) + ((12 * x19) + ((15 * (x19 * x23)) + x23)))) >= (4 * x19) + ((2 * (x19 * x18)) + (14 * x18)) = f4(f215(x19),x18) | | | +- f218(x18,x19,x21) = 5 + ((3 * x18) + ((2 * x19) + x21)) >= (5 + ((2 * x19) + (3 * x18))) + x21 = f5(f215(x19),x18) + f216(x21) | | | +- f219(x18,x19,x21) = 5 + ((3 * x18) + ((2 * x19) + x21)) >= 5 + ((3 * x18) + ((2 * x19) + x21)) = f218(x18,x19,x21) | | | +- f220(x145) = x145 >= x145 = x145 | | | +- f221(x146) = x146 >= x146 = x146 | | | +- f4(x145,f222(x18)) = (4 * x145) + ((2 * (x145 * x18)) + (14 * x18)) >= (4 * x145) + ((2 * (x145 * x18)) + (14 * x18)) = f4(f220(x145),x18) | | | +- f5(x145,f222(x18)) + x146 = (5 + ((2 * x145) + (3 * x18))) + x146 >= (5 + ((2 * x145) + (3 * x18))) + x146 = f5(f220(x145),x18) + f221(x146) | | | +- f223(x18,x19,x21) = 5 + ((3 * x18) + ((2 * x19) + x21)) >= 5 + ((3 * x18) + ((2 * x19) + x21)) = f219(x18,x19,x21) | | | +- f224(x23) = x23 >= x23 = x23 | | | +- f225(x19) = x19 >= x19 = x19 | | | +- f226(x18,x19,x21,x23,x145,x146) = 5 + ((3 * x18) + ((2 * x19) + x21)) >= 5 + ((3 * x18) + ((2 * x19) + x21)) = f9(f222(x18),f225(x19),f224(x23),f226(x18,x19,x21,x23,x145,x146)) + f223(x18,x19,x21) | | | +- f227(x18,x19,x23,x145,x146) = 7 + ((3 * x18) + ((5 * (x18 * x19)) + ((3 * (x18 * x23)) + ((10 * x19) + ((15 * (x19 * x23)) + (3 * x23)))))) >= 6 + ((3 * x18) + ((5 * (x18 * x19)) + ((3 * (x18 * x23)) + ((9 * x19) + ((15 * (x19 * x23)) + (3 * x23)))))) = f7(f222(x18),f225(x19),f224(x23)) | | | +- f217(x18,x19,x23,x145,x146) = (14 * x18) + ((2 * (x18 * x19)) + ((7 * (x18 * x23)) + ((12 * x19) + ((15 * (x19 * x23)) + x23)))) >= (7 * x18) + ((2 * (x18 * x19)) + ((7 * (x18 * x23)) + ((7 * x19) + ((15 * (x19 * x23)) + x23)))) = f6(f222(x18),f225(x19),f224(x23)) | | | +- f228(x18,x19,x21,x23,x145,x146) = 13 + ((12 * x18) + ((x18 * x19) + ((7 * (x18 * x23)) + ((7 * x19) + ((8 * (x19 * x23)) + (x21 + (8 * x23))))))) >= (8 + ((6 * x18) + ((x18 * x19) + ((7 * (x18 * x23)) + ((5 * x19) + ((8 * (x19 * x23)) + (8 * x23))))))) + (5 + ((3 * x18) + ((2 * x19) + x21))) = f8(f222(x18),f225(x19),f224(x23)) + f226(x18,x19,x21,x23,x145,x146) | | | +- f229(x18,x19,x21,x23,x145,x146) = 15 + ((13 * x18) + ((x18 * x19) + ((7 * (x18 * x23)) + ((8 * x19) + ((8 * (x19 * x23)) + (x21 + (8 * x23))))))) >= 13 + ((12 * x18) + ((x18 * x19) + ((7 * (x18 * x23)) + ((7 * x19) + ((8 * (x19 * x23)) + (x21 + (8 * x23))))))) = f228(x18,x19,x21,x23,x145,x146) | | | +- f7(x18,x19,x23 + 1) = 6 + ((3 * x18) + ((5 * (x18 * x19)) + ((3 * (x18 * (x23 + 1))) + ((9 * x19) + ((15 * (x19 * (x23 + 1))) + (3 * (x23 + 1))))))) >= (7 + ((3 * x18) + ((5 * (x18 * x19)) + ((3 * (x18 * x23)) + ((10 * x19) + ((15 * (x19 * x23)) + (3 * x23))))))) + 1 = f227(x18,x19,x23,x145,x146) + 1 | | | +- f6(x18,x19,x23 + 1) = (7 * x18) + ((2 * (x18 * x19)) + ((7 * (x18 * (x23 + 1))) + ((7 * x19) + ((15 * (x19 * (x23 + 1))) + (x23 + 1))))) >= (14 * x18) + ((2 * (x18 * x19)) + ((7 * (x18 * x23)) + ((12 * x19) + ((15 * (x19 * x23)) + x23)))) = f217(x18,x19,x23,x145,x146) | | | +- f8(x18,x19,x23 + 1) + x21 = (8 + ((6 * x18) + ((x18 * x19) + ((7 * (x18 * (x23 + 1))) + ((5 * x19) + ((8 * (x19 * (x23 + 1))) + (8 * (x23 + 1)))))))) + x21 >= (15 + ((13 * x18) + ((x18 * x19) + ((7 * (x18 * x23)) + ((8 * x19) + ((8 * (x19 * x23)) + (x21 + (8 * x23)))))))) + 1 = f229(x18,x19,x21,x23,x145,x146) + 1 | | | +- f230(x30) = x30 >= x30 = x30 | | | +- f231(x30) = 3 + x30 >= x30 = f230(x30) | | | +- f7(x27,x28,0) = 6 + ((3 * x27) + ((5 * (x27 * x28)) + (9 * x28))) >= 0 = 0 | | | +- f6(x27,x28,0) = (7 * x27) + ((2 * (x27 * x28)) + (7 * x28)) >= 0 = f232() | | | `- f8(x27,x28,0) + x30 = (8 + ((6 * x27) + ((x27 * x28) + (5 * x28)))) + x30 >= (3 + x30) + 1 = f231(x30) + 1 | `- Stopping timer: 2017-03-30 07:32:45.852594 UTC(+5.044695s)