SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + 3*x1;
f10(x0) = 2;
f11(x0) = 13 + 15*x0;
f12(x0) = 15 + 15*x0;
f13(x0,x1) = 15*x0 + x1;
f14(x0,x1) = 2 + 10*x0 + 3*x1;
f15(x0,x1,x2) = 3 + 5*x0;
f187(x0) = x0;
f188(x0) = x0;
f189(x0) = x0;
f190(x0,x1) = 3 + 5*x0 + x1;
f191() = 3;
f192(x0,x1) = 3 + 5*x0 + x1;
f193(x0,x1) = 14 + 15*x0 + x1;
f194(x0) = x0;
f195(x0) = x0;
f196(x0) = x0;
f197(x0) = x0;
f198(x0) = x0;
f199(x0) = x0;
f2(x0,x1) = 3*x0 + 2*x1;
f200(x0) = 1 + 5*x0;
f201(x0,x1,x2,x3) = 4 + x0 + 5*x1;
f202(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3;
f203() = 1;
f204(x0) = x0;
f205(x0) = x0;
f206(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3;
f207(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3;
f208(x0) = x0;
f209(x0) = x0;
f210(x0,x1,x2,x3,x4,x5,x6,x7) = 7 + x2 + 5*x3;
f211(x0) = x0;
f212(x0) = x0;
f213(x0) = x0;
f214(x0) = x0;
f215(x0) = x0;
f216(x0) = x0;
f217(x0) = x0;
f218(x0,x1,x2) = 2*x1 + x2;
f219(x0,x1,x2,x3) = 2*x1 + x3;
f220(x0,x1,x2,x3) = 2*x0 + 8*x1 + 3*x2 + x3;
f3(x0,x1,x2) = x1 + x2;
f4(x0,x1,x2) = 2*x2;
f5(x0,x1,x2) = 3*x0 + 12*x1 + x2;
f6(x0,x1,x2) = 1 + 2*x0 + 8*x1 + 3*x2;
f7(x0,x1,x2,x3) = 0;
f8(x0,x1,x2,x3,x4) = 2*x1;
f9(x0) = x0;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:21.00277 UTC
   |
   +- Open Constraints
   |  |
   |  +- f187(x3) = f187(x3) >= x3 = x3
   |  |
   |  +- f188(x2) = f188(x2) >= x2 = x2
   |  |
   |  +- f189(x3) = f189(x3) >= f187(x3) = f187(x3)
   |  |
   |  +- f190(x2,x3) = f190(x2,x3) >= f15(f188(x2),f191(),f192(x2,x3)) + f189(x3) = f15(f188(x2),f191(),f192(x2,x3)) + f189(x3)
   |  |
   |  +- f191() = f191() >= 0 = 0
   |  |
   |  +- f192(x2,x3) = f192(x2,x3) >= f190(x2,x3) = f190(x2,x3)
   |  |
   |  +- f193(x2,x3) = f193(x2,x3) >= f14(f188(x2),f191()) + f192(x2,x3) = f14(f188(x2),f191()) + f192(x2,x3)
   |  |
   |  +- f11(x2) = f11(x2) >= f13(f188(x2),f191()) = f13(f188(x2),f191())
   |  |
   |  +- f12(x2) + x3 = f12(x2) + x3 >= f193(x2,x3) + 1 = f193(x2,x3) + 1
   |  |
   |  +- f194(x8) = f194(x8) >= x8 = x8
   |  |
   |  +- f195(x8) = f195(x8) >= f194(x8) = f194(x8)
   |  |
   |  +- f196(x10) = f196(x10) >= x10 = x10
   |  |
   |  +- f197(x8) = f197(x8) >= f195(x8) = f195(x8)
   |  |
   |  +- f198(x83) = f198(x83) >= x83 = x83
   |  |
   |  +- f199(x84) = f199(x84) >= x84 = x84
   |  |
   |  +- f1(x83,f200(x10)) = f1(x83,f200(x10)) >= f13(f196(x10),f198(x83)) = f13(f196(x10),f198(x83))
   |  |
   |  +- f2(x83,f200(x10)) + x84 = f2(x83,f200(x10)) + x84 >= f14(f196(x10),f198(x83)) + f199(x84) = f14(f196(x10),f198(x83)) + f199(x84)
   |  |
   |  +- f201(x8,x10,x83,x84) = f201(x8,x10,x83,x84) >= f15(f196(x10),f198(x83),f199(x84)) + f197(x8) = f15(f196(x10),f198(x83),f199(x84)) + f197(x8)
   |  |
   |  +- f202(x6,x7,x8,x10,x83,x84,x124,x125) = f202(x6,x7,x8,x10,x83,x84,x124,x125) >= f8(f200(x10),f203(),f204(x6),f205(x7),f206(x6,x7,x8,x10,x83,x84,x124,x125)) + f201(x8,x10,x83,x84) = f8(f200(x10)
                                                                                                                                                                                      ,f203()
                                                                                                                                                                                      ,f204(x6)
                                                                                                                                                                                      ,f205(x7)
                                                                                                                                                                                      ,f206(x6
                                                                                                                                                                                           ,x7
                                                                                                                                                                                           ,x8
                                                                                                                                                                                           ,x10
                                                                                                                                                                                           ,x83
                                                                                                                                                                                           ,x84
                                                                                                                                                                                           ,x124
                                                                                                                                                                                           ,x125))
                                       + f201(x8,x10,x83,x84)
   |  |
   |  +- f207(x6,x7,x8,x10,x83,x84,x124,x125) = f207(x6,x7,x8,x10,x83,x84,x124,x125) >= f202(x6,x7,x8,x10,x83,x84,x124,x125) = f202(x6,x7,x8,x10,x83,x84,x124,x125)
   |  |
   |  +- f208(x124) = f208(x124) >= x124 = x124
   |  |
   |  +- f209(x125) = f209(x125) >= x125 = x125
   |  |
   |  +- f3(f200(x10),x124,f203()) = f3(f200(x10),x124,f203()) >= f208(x124) + 1 = f208(x124) + 1
   |  |
   |  +- f4(f200(x10),x124,f203()) + x125 = f4(f200(x10),x124,f203()) + x125 >= f209(x125) = f209(x125)
   |  |
   |  +- f206(x6,x7,x8,x10,x83,x84,x124,x125) = f206(x6,x7,x8,x10,x83,x84,x124,x125) >= f207(x6,x7,x8,x10,x83,x84,x124,x125) = f207(x6,x7,x8,x10,x83,x84,x124,x125)
   |  |
   |  +- f210(x6,x7,x8,x10,x83,x84,x124,x125) = f210(x6,x7,x8,x10,x83,x84,x124,x125) >= f7(f200(x10),f203(),f204(x6),f205(x7)) + f206(x6,x7,x8,x10,x83,x84,x124,x125) = f7(f200(x10),f203(),f204(x6),f205(x7))
                                       + f206(x6,x7,x8,x10,x83,x84,x124,x125)
   |  |
   |  +- f204(x6) = f204(x6) >= x6 = x6
   |  |
   |  +- f205(x7) = f205(x7) >= x7 = x7
   |  |
   |  +- f13(x10 + 1,x6) = f13(x10 + 1,x6) >= f5(f200(x10),f203(),f204(x6)) = f5(f200(x10),f203(),f204(x6))
   |  |
   |  +- f14(x10 + 1,x6) + x7 = f14(x10 + 1,x6) + x7 >= f6(f200(x10),f203(),f204(x6)) + f205(x7) = f6(f200(x10),f203(),f204(x6)) + f205(x7)
   |  |
   |  +- f15(x10 + 1,x6,x7) + x8 = f15(x10 + 1,x6,x7) + x8 >= f210(x6,x7,x8,x10,x83,x84,x124,x125) + 1 = f210(x6,x7,x8,x10,x83,x84,x124,x125) + 1
   |  |
   |  +- f211(x15) = f211(x15) >= x15 = x15
   |  |
   |  +- f212(x15) = f212(x15) >= f211(x15) = f211(x15)
   |  |
   |  +- f213(x13) = f213(x13) >= x13 = x13
   |  |
   |  +- f214(x14) = f214(x14) >= x14 = x14
   |  |
   |  +- f13(0,x13) = f13(0,x13) >= f9(f213(x13)) = f9(f213(x13))
   |  |
   |  +- f14(0,x13) + x14 = f14(0,x13) + x14 >= f10(f213(x13)) + f214(x14) = f10(f213(x13)) + f214(x14)
   |  |
   |  +- f15(0,x13,x14) + x15 = f15(0,x13,x14) + x15 >= f212(x15) + 1 = f212(x15) + 1
   |  |
   |  +- f215(x19) = f215(x19) >= x19 = x19
   |  |
   |  +- f9(x18) = f9(x18) >= x18 = x18
   |  |
   |  +- f10(x18) + x19 = f10(x18) + x19 >= f215(x19) + 1 = f215(x19) + 1
   |  |
   |  +- f216(x23) = f216(x23) >= x23 = x23
   |  |
   |  +- f217(x24) = f217(x24) >= x24 = x24
   |  |
   |  +- f218(x21,x22,x23) = f218(x21,x22,x23) >= f3(x21,f216(x23),x22) = f3(x21,f216(x23),x22)
   |  |
   |  +- f219(x21,x22,x23,x24) = f219(x21,x22,x23,x24) >= f4(x21,f216(x23),x22) + f217(x24) = f4(x21,f216(x23),x22) + f217(x24)
   |  |
   |  +- f220(x21,x22,x23,x24) = f220(x21,x22,x23,x24) >= f2(f218(x21,x22,x23),x21) + f219(x21,x22,x23,x24) = f2(f218(x21,x22,x23),x21) + f219(x21,x22,x23,x24)
   |  |
   |  +- f5(x21,x22,x23) = f5(x21,x22,x23) >= f1(f218(x21,x22,x23),x21) = f1(f218(x21,x22,x23),x21)
   |  |
   |  `- f6(x21,x22,x23) + x24 = f6(x21,x22,x23) + x24 >= f220(x21,x22,x23,x24) + 1 = f220(x21,x22,x23,x24) + 1
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:21.002949 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:21.132476 UTC(+0.129527s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:21.132492 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + 3*x1
   |  |  |
   |  |  +- f10(x0) = 2
   |  |  |
   |  |  +- f11(x0) = 13 + 15*x0
   |  |  |
   |  |  +- f12(x0) = 15 + 15*x0
   |  |  |
   |  |  +- f13(x0,x1) = 15*x0 + x1
   |  |  |
   |  |  +- f14(x0,x1) = 2 + 10*x0 + 3*x1
   |  |  |
   |  |  +- f15(x0,x1,x2) = 3 + 5*x0
   |  |  |
   |  |  +- f187(x0) = x0
   |  |  |
   |  |  +- f188(x0) = x0
   |  |  |
   |  |  +- f189(x0) = x0
   |  |  |
   |  |  +- f190(x0,x1) = 3 + 5*x0 + x1
   |  |  |
   |  |  +- f191() = 3
   |  |  |
   |  |  +- f192(x0,x1) = 3 + 5*x0 + x1
   |  |  |
   |  |  +- f193(x0,x1) = 14 + 15*x0 + x1
   |  |  |
   |  |  +- f194(x0) = x0
   |  |  |
   |  |  +- f195(x0) = x0
   |  |  |
   |  |  +- f196(x0) = x0
   |  |  |
   |  |  +- f197(x0) = x0
   |  |  |
   |  |  +- f198(x0) = x0
   |  |  |
   |  |  +- f199(x0) = x0
   |  |  |
   |  |  +- f2(x0,x1) = 3*x0 + 2*x1
   |  |  |
   |  |  +- f200(x0) = 1 + 5*x0
   |  |  |
   |  |  +- f201(x0,x1,x2,x3) = 4 + x0 + 5*x1
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3
   |  |  |
   |  |  +- f203() = 1
   |  |  |
   |  |  +- f204(x0) = x0
   |  |  |
   |  |  +- f205(x0) = x0
   |  |  |
   |  |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3
   |  |  |
   |  |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3
   |  |  |
   |  |  +- f208(x0) = x0
   |  |  |
   |  |  +- f209(x0) = x0
   |  |  |
   |  |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 7 + x2 + 5*x3
   |  |  |
   |  |  +- f211(x0) = x0
   |  |  |
   |  |  +- f212(x0) = x0
   |  |  |
   |  |  +- f213(x0) = x0
   |  |  |
   |  |  +- f214(x0) = x0
   |  |  |
   |  |  +- f215(x0) = x0
   |  |  |
   |  |  +- f216(x0) = x0
   |  |  |
   |  |  +- f217(x0) = x0
   |  |  |
   |  |  +- f218(x0,x1,x2) = 2*x1 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2,x3) = 2*x1 + x3
   |  |  |
   |  |  +- f220(x0,x1,x2,x3) = 2*x0 + 8*x1 + 3*x2 + x3
   |  |  |
   |  |  +- f3(x0,x1,x2) = x1 + x2
   |  |  |
   |  |  +- f4(x0,x1,x2) = 2*x2
   |  |  |
   |  |  +- f5(x0,x1,x2) = 3*x0 + 12*x1 + x2
   |  |  |
   |  |  +- f6(x0,x1,x2) = 1 + 2*x0 + 8*x1 + 3*x2
   |  |  |
   |  |  +- f7(x0,x1,x2,x3) = 0
   |  |  |
   |  |  +- f8(x0,x1,x2,x3,x4) = 2*x1
   |  |  |
   |  |  `- f9(x0) = x0
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:21.425043 UTC(+0.292551s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + 3*x1
   |  |
   |  +- f10(x0) = 2
   |  |
   |  +- f11(x0) = 13 + 15*x0
   |  |
   |  +- f12(x0) = 15 + 15*x0
   |  |
   |  +- f13(x0,x1) = 15*x0 + x1
   |  |
   |  +- f14(x0,x1) = 2 + 10*x0 + 3*x1
   |  |
   |  +- f15(x0,x1,x2) = 3 + 5*x0
   |  |
   |  +- f187(x0) = x0
   |  |
   |  +- f188(x0) = x0
   |  |
   |  +- f189(x0) = x0
   |  |
   |  +- f190(x0,x1) = 3 + 5*x0 + x1
   |  |
   |  +- f191() = 3
   |  |
   |  +- f192(x0,x1) = 3 + 5*x0 + x1
   |  |
   |  +- f193(x0,x1) = 14 + 15*x0 + x1
   |  |
   |  +- f194(x0) = x0
   |  |
   |  +- f195(x0) = x0
   |  |
   |  +- f196(x0) = x0
   |  |
   |  +- f197(x0) = x0
   |  |
   |  +- f198(x0) = x0
   |  |
   |  +- f199(x0) = x0
   |  |
   |  +- f2(x0,x1) = 3*x0 + 2*x1
   |  |
   |  +- f200(x0) = 1 + 5*x0
   |  |
   |  +- f201(x0,x1,x2,x3) = 4 + x0 + 5*x1
   |  |
   |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3
   |  |
   |  +- f203() = 1
   |  |
   |  +- f204(x0) = x0
   |  |
   |  +- f205(x0) = x0
   |  |
   |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3
   |  |
   |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 6 + x2 + 5*x3
   |  |
   |  +- f208(x0) = x0
   |  |
   |  +- f209(x0) = x0
   |  |
   |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 7 + x2 + 5*x3
   |  |
   |  +- f211(x0) = x0
   |  |
   |  +- f212(x0) = x0
   |  |
   |  +- f213(x0) = x0
   |  |
   |  +- f214(x0) = x0
   |  |
   |  +- f215(x0) = x0
   |  |
   |  +- f216(x0) = x0
   |  |
   |  +- f217(x0) = x0
   |  |
   |  +- f218(x0,x1,x2) = 2*x1 + x2
   |  |
   |  +- f219(x0,x1,x2,x3) = 2*x1 + x3
   |  |
   |  +- f220(x0,x1,x2,x3) = 2*x0 + 8*x1 + 3*x2 + x3
   |  |
   |  +- f3(x0,x1,x2) = x1 + x2
   |  |
   |  +- f4(x0,x1,x2) = 2*x2
   |  |
   |  +- f5(x0,x1,x2) = 3*x0 + 12*x1 + x2
   |  |
   |  +- f6(x0,x1,x2) = 1 + 2*x0 + 8*x1 + 3*x2
   |  |
   |  +- f7(x0,x1,x2,x3) = 0
   |  |
   |  +- f8(x0,x1,x2,x3,x4) = 2*x1
   |  |
   |  `- f9(x0) = x0
   |
   +- Constraints
   |  |
   |  +- f187(x3) = x3 >= x3 = x3
   |  |
   |  +- f188(x2) = x2 >= x2 = x2
   |  |
   |  +- f189(x3) = x3 >= x3 = f187(x3)
   |  |
   |  +- f190(x2,x3) = 3 + ((5 * x2) + x3) >= (3 + (5 * x2)) + x3 = f15(f188(x2),f191(),f192(x2,x3)) + f189(x3)
   |  |
   |  +- f191() = 3 >= 0 = 0
   |  |
   |  +- f192(x2,x3) = 3 + ((5 * x2) + x3) >= 3 + ((5 * x2) + x3) = f190(x2,x3)
   |  |
   |  +- f193(x2,x3) = 14 + ((15 * x2) + x3) >= (2 + ((10 * x2) + 9)) + (3 + ((5 * x2) + x3)) = f14(f188(x2),f191()) + f192(x2,x3)
   |  |
   |  +- f11(x2) = 13 + (15 * x2) >= (15 * x2) + 3 = f13(f188(x2),f191())
   |  |
   |  +- f12(x2) + x3 = (15 + (15 * x2)) + x3 >= (14 + ((15 * x2) + x3)) + 1 = f193(x2,x3) + 1
   |  |
   |  +- f194(x8) = x8 >= x8 = x8
   |  |
   |  +- f195(x8) = x8 >= x8 = f194(x8)
   |  |
   |  +- f196(x10) = x10 >= x10 = x10
   |  |
   |  +- f197(x8) = x8 >= x8 = f195(x8)
   |  |
   |  +- f198(x83) = x83 >= x83 = x83
   |  |
   |  +- f199(x84) = x84 >= x84 = x84
   |  |
   |  +- f1(x83,f200(x10)) = x83 + (3 * (1 + (5 * x10))) >= (15 * x10) + x83 = f13(f196(x10),f198(x83))
   |  |
   |  +- f2(x83,f200(x10)) + x84 = ((3 * x83) + (2 * (1 + (5 * x10)))) + x84 >= (2 + ((10 * x10) + (3 * x83))) + x84 = f14(f196(x10),f198(x83)) + f199(x84)
   |  |
   |  +- f201(x8,x10,x83,x84) = 4 + (x8 + (5 * x10)) >= (3 + (5 * x10)) + x8 = f15(f196(x10),f198(x83),f199(x84)) + f197(x8)
   |  |
   |  +- f202(x6,x7,x8,x10,x83,x84,x124,x125) = 6 + (x8 + (5 * x10)) >= 2 + (4 + (x8 + (5 * x10))) = f8(f200(x10),f203(),f204(x6),f205(x7),f206(x6,x7,x8,x10,x83,x84,x124,x125)) + f201(x8,x10,x83,x84)
   |  |
   |  +- f207(x6,x7,x8,x10,x83,x84,x124,x125) = 6 + (x8 + (5 * x10)) >= 6 + (x8 + (5 * x10)) = f202(x6,x7,x8,x10,x83,x84,x124,x125)
   |  |
   |  +- f208(x124) = x124 >= x124 = x124
   |  |
   |  +- f209(x125) = x125 >= x125 = x125
   |  |
   |  +- f3(f200(x10),x124,f203()) = x124 + 1 >= x124 + 1 = f208(x124) + 1
   |  |
   |  +- f4(f200(x10),x124,f203()) + x125 = 2 + x125 >= x125 = f209(x125)
   |  |
   |  +- f206(x6,x7,x8,x10,x83,x84,x124,x125) = 6 + (x8 + (5 * x10)) >= 6 + (x8 + (5 * x10)) = f207(x6,x7,x8,x10,x83,x84,x124,x125)
   |  |
   |  +- f210(x6,x7,x8,x10,x83,x84,x124,x125) = 7 + (x8 + (5 * x10)) >= 6 + (x8 + (5 * x10)) = f7(f200(x10),f203(),f204(x6),f205(x7)) + f206(x6,x7,x8,x10,x83,x84,x124,x125)
   |  |
   |  +- f204(x6) = x6 >= x6 = x6
   |  |
   |  +- f205(x7) = x7 >= x7 = x7
   |  |
   |  +- f13(x10 + 1,x6) = (15 * (x10 + 1)) + x6 >= (3 * (1 + (5 * x10))) + (12 + x6) = f5(f200(x10),f203(),f204(x6))
   |  |
   |  +- f14(x10 + 1,x6) + x7 = (2 + ((10 * (x10 + 1)) + (3 * x6))) + x7 >= (1 + ((2 * (1 + (5 * x10))) + (8 + (3 * x6)))) + x7 = f6(f200(x10),f203(),f204(x6)) + f205(x7)
   |  |
   |  +- f15(x10 + 1,x6,x7) + x8 = (3 + (5 * (x10 + 1))) + x8 >= (7 + (x8 + (5 * x10))) + 1 = f210(x6,x7,x8,x10,x83,x84,x124,x125) + 1
   |  |
   |  +- f211(x15) = x15 >= x15 = x15
   |  |
   |  +- f212(x15) = x15 >= x15 = f211(x15)
   |  |
   |  +- f213(x13) = x13 >= x13 = x13
   |  |
   |  +- f214(x14) = x14 >= x14 = x14
   |  |
   |  +- f13(0,x13) = x13 >= x13 = f9(f213(x13))
   |  |
   |  +- f14(0,x13) + x14 = (2 + (3 * x13)) + x14 >= 2 + x14 = f10(f213(x13)) + f214(x14)
   |  |
   |  +- f15(0,x13,x14) + x15 = 3 + x15 >= x15 + 1 = f212(x15) + 1
   |  |
   |  +- f215(x19) = x19 >= x19 = x19
   |  |
   |  +- f9(x18) = x18 >= x18 = x18
   |  |
   |  +- f10(x18) + x19 = 2 + x19 >= x19 + 1 = f215(x19) + 1
   |  |
   |  +- f216(x23) = x23 >= x23 = x23
   |  |
   |  +- f217(x24) = x24 >= x24 = x24
   |  |
   |  +- f218(x21,x22,x23) = (2 * x22) + x23 >= x23 + x22 = f3(x21,f216(x23),x22)
   |  |
   |  +- f219(x21,x22,x23,x24) = (2 * x22) + x24 >= (2 * x22) + x24 = f4(x21,f216(x23),x22) + f217(x24)
   |  |
   |  +- f220(x21,x22,x23,x24) = (2 * x21) + ((8 * x22) + ((3 * x23) + x24)) >= ((3 * ((2 * x22) + x23)) + (2 * x21)) + ((2 * x22) + x24) = f2(f218(x21,x22,x23),x21) + f219(x21,x22,x23,x24)
   |  |
   |  +- f5(x21,x22,x23) = (3 * x21) + ((12 * x22) + x23) >= ((2 * x22) + x23) + (3 * x21) = f1(f218(x21,x22,x23),x21)
   |  |
   |  `- f6(x21,x22,x23) + x24 = (1 + ((2 * x21) + ((8 * x22) + (3 * x23)))) + x24 >= ((2 * x21) + ((8 * x22) + ((3 * x23) + x24))) + 1 = f220(x21,x22,x23,x24) + 1
   |
   `- Stopping timer: 2017-03-30 07:32:21.425235 UTC(+0.422465s)