SUCCESS(2)

SUCCESS
f1(x0,x1) = x0 + x1;
f10(x0,x1,x2) = 1 + x0 + x1;
f11(x0,x1,x2) = x2;
f12(x0,x1,x2) = 2 + x0*x2 + 2*x2;
f191(x0) = x0;
f192(x0) = x0;
f193(x0) = x0;
f194(x0) = x0;
f195(x0) = x0;
f196(x0) = x0;
f197(x0) = 1 + x0;
f198(x0,x1,x2,x3) = x1;
f199(x0) = x0;
f2(x0,x1) = 1 + x0;
f200(x0) = x0;
f201(x0,x1,x2,x3,x4,x5) = x3;
f202(x0,x1,x2,x3,x4,x5) = 1 + x0*x2 + 2*x2 + x3;
f203(x0) = x0;
f204(x0) = x0;
f205(x0) = x0;
f206(x0) = x0;
f207(x0) = x0;
f208(x0) = x0;
f209(x0,x1,x2) = x1;
f210(x0,x1) = x0 + x1;
f211(x0,x1,x2) = 1 + x1 + x2;
f212(x0,x1,x2) = 1 + x1 + x2;
f213(x0) = x0;
f214(x0) = x0;
f215(x0) = x0;
f216(x0) = x0;
f217(x0,x1,x2,x3,x4) = x0 + x1;
f218(x0,x1,x2) = x0 + x2;
f219(x0,x1,x2) = x0 + x2;
f220(x0) = x0;
f221(x0) = x0;
f222(x0) = x0;
f223(x0,x1,x2) = x0 + x2;
f224(x0) = x0;
f225(x0) = x0;
f226(x0,x1,x2,x3,x4,x5) = x0 + x2;
f227(x0,x1,x2,x3,x4) = x2;
f228(x0,x1,x2,x3,x4,x5) = 1 + x0 + x0*x3 + x2 + x3;
f229(x0,x1,x2,x3,x4,x5) = 1 + x0 + x0*x3 + x2 + x3;
f230(x0) = x0;
f231(x0) = x0;
f232() = 0;
f3(x0,x1,x2) = 0;
f4(x0,x1) = x0 + x1;
f5(x0,x1) = x1;
f6(x0,x1,x2) = x0 + x1;
f7(x0,x1,x2) = x2;
f8(x0,x1,x2) = 1 + x0*x2 + x2;
f9(x0,x1,x2,x3) = 0;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:45.864639 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
   |
   +- Simplification ...
   |  |
   |  +- Substituted: f2(0,x14) + x15 ≥ f213(x15) + 1 ↦ f2(0,0) + x15 ≥ f213(x15) + 1
   |  |
   |  +- Substituted: f217(x18,x19,x23,x145,x146) ≥ f4(f215(x19),x18) ↦ f217(x18,x19,0,0,0) ≥ f4(f215(x19),x18)
   |  |
   |  +- Substituted: f227(x18,x19,x23,x145,x146) ≥ f7(f222(x18),f225(x19),f224(x23)) ↦ f227(x18,x19,x23,0,0) ≥ f7(f222(x18),f225(x19),f224(x23))
   |  |
   |  +- Substituted: f217(x18,x19,x23,x145,x146) ≥ f6(f222(x18),f225(x19),f224(x23)) ↦ f217(x18,x19,x23,0,0) ≥ f6(f222(x18),f225(x19),f224(x23))
   |  |
   |  +- Substituted: f7(x27,x28,0) ≥ 0 ↦ f7(0,0,0) ≥ 0
   |  |
   |  +- Substituted: f6(x27,x28,0) ≥ f232() ↦ f6(0,0,0) ≥ f232()
   |  |
   |  +- Substituted: f8(x27,x28,0) + x30 ≥ f231(x30) + 1 ↦ f8(0,0,0) + x30 ≥ f231(x30) + 1
   |  |
   |  +- Eliminated: f232/0
   |  |
   |  +- Eliminated: f3/3
   |  |
   |  +- Eliminated: f9/4
   |  |
   |  +- Propagated: f191(x0) ↦ x0
   |  |
   |  +- Propagated: f193(x0) ↦ x0
   |  |
   |  +- Propagated: f195(x0) ↦ x0
   |  |
   |  +- Propagated: f196(x0) ↦ x0
   |  |
   |  +- Propagated: f199(x0) ↦ x0
   |  |
   |  +- Propagated: f200(x0) ↦ x0
   |  |
   |  +- Propagated: f203(x0) ↦ x0
   |  |
   |  +- Propagated: f206(x0) ↦ x0
   |  |
   |  +- Propagated: f208(x0) ↦ x0
   |  |
   |  +- Propagated: f213(x0) ↦ x0
   |  |
   |  +- Propagated: f214(x0) ↦ x0
   |  |
   |  +- Propagated: f215(x0) ↦ x0
   |  |
   |  +- Propagated: f220(x0) ↦ x0
   |  |
   |  +- Propagated: f221(x0) ↦ x0
   |  |
   |  +- Propagated: f224(x0) ↦ x0
   |  |
   |  +- Propagated: f225(x0) ↦ x0
   |  |
   |  +- Propagated: f230(x0) ↦ x0
   |  |
   |  +- Propagated: f192(x0) ↦ x0
   |  |
   |  +- Propagated: f204(x0) ↦ x0
   |  |
   |  +- Propagated: f216(x0) ↦ x0
   |  |
   |  +- Propagated: f231(x0) ↦ x0
   |  |
   |  +- Propagated: f194(x0) ↦ x0
   |  |
   |  +- Propagated: f205(x0) ↦ x0
   |  |
   |  +- Propagated: f198(x0,x1,x2,x3) ↦ x1
   |  |
   |  +- Propagated: f207(x0) ↦ x0
   |  |
   |  +- Propagated: f201(x0,x1,x2,x3,x4,x5) ↦ x3
   |  |
   |  `- Propagated: f209(x0,x1,x2) ↦ x1
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:46.066878 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:46.090992 UTC(+0.024114s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:46.091 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:46.138987 UTC(+0.047987s)
   |
   +- SMT-MMI(2) ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:46.138996 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = 7 + 6*x0 + 2*x1
   |  |  |
   |  |  +- f10(x0,x1,x2) = 15 + 9*x0 + 11*x0*x1 + 15*x0*x2 + 12*x1 + 15*x1*x2 + 12*x2
   |  |  |
   |  |  +- f11(x0,x1,x2) = 11 + 11*x0 + 13*x0*x1 + 14*x0*x2 + 15*x1 + 15*x1*x2 + 10*x2
   |  |  |
   |  |  +- f12(x0,x1,x2) = 14 + 14*x0 + 14*x0*x1 + 14*x0*x2 + 14*x1 + 14*x1*x2 + 15*x2
   |  |  |
   |  |  +- f197(x0) = 1 + x0
   |  |  |
   |  |  +- f2(x0,x1) = 1 + 2*x0
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5) = 13 + 12*x0 + 10*x0*x1 + 12*x0*x2 + 14*x1 + 10*x1*x2 + 15*x2 + x3
   |  |  |
   |  |  +- f210(x0,x1) = 12 + 2*x0 + 6*x1
   |  |  |
   |  |  +- f211(x0,x1,x2) = 1 + x1 + 2*x2
   |  |  |
   |  |  +- f212(x0,x1,x2) = 2 + x1 + 2*x2
   |  |  |
   |  |  +- f217(x0,x1,x2,x3,x4) = 9 + 7*x0 + 5*x0*x1 + x0*x2 + 14*x1 + 9*x1*x2 + x2
   |  |  |
   |  |  +- f218(x0,x1,x2) = 3*x0 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2) = 1 + 4*x0 + x2
   |  |  |
   |  |  +- f222(x0) = x0
   |  |  |
   |  |  +- f223(x0,x1,x2) = 1 + 7*x0 + x2
   |  |  |
   |  |  +- f226(x0,x1,x2,x3,x4,x5) = 1 + 9*x0 + x2
   |  |  |
   |  |  +- f227(x0,x1,x2,x3,x4) = 5*x0 + 11*x0*x1 + 8*x1 + 9*x1*x2 + 4*x2
   |  |  |
   |  |  +- f228(x0,x1,x2,x3,x4,x5) = 8 + 14*x0 + 8*x0*x1 + 9*x0*x3 + 8*x1 + 8*x1*x3 + x2 + 4*x3
   |  |  |
   |  |  +- f229(x0,x1,x2,x3,x4,x5) = 9 + 14*x0 + 8*x0*x1 + 9*x0*x3 + 8*x1 + 8*x1*x3 + x2 + 4*x3
   |  |  |
   |  |  +- f4(x0,x1) = 9 + 2*x0 + 6*x1
   |  |  |
   |  |  +- f5(x0,x1) = 2*x1
   |  |  |
   |  |  +- f6(x0,x1,x2) = 8 + 7*x0 + 5*x0*x1 + x0*x2 + 5*x1 + 9*x1*x2 + x2
   |  |  |
   |  |  +- f7(x0,x1,x2) = 5*x0 + 11*x0*x1 + 4*x1 + 9*x1*x2 + 4*x2
   |  |  |
   |  |  `- f8(x0,x1,x2) = 7 + 5*x0 + 8*x0*x1 + 9*x0*x2 + 3*x1 + 8*x1*x2 + 4*x2
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0,x1,x2) = x0 + x0*x2 + x1 + x2
   |  |  |
   |  |  +- f11(x0,x1,x2) = x0*x1 + x2
   |  |  |
   |  |  +- f12(x0,x1,x2) = 2 + x0*x2 + x1 + 2*x2
   |  |  |
   |  |  +- f197(x0) = 1 + x0
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5) = 1 + x0*x2 + x1 + 2*x2 + x3
   |  |  |
   |  |  +- f210(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f211(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f212(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f217(x0,x1,x2,x3,x4) = x0 + x0*x2 + x1
   |  |  |
   |  |  +- f218(x0,x1,x2) = x0 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2) = x0 + x2
   |  |  |
   |  |  +- f222(x0) = x0
   |  |  |
   |  |  +- f223(x0,x1,x2) = x0 + x2
   |  |  |
   |  |  +- f226(x0,x1,x2,x3,x4,x5) = x0 + x2
   |  |  |
   |  |  +- f227(x0,x1,x2,x3,x4) = x2
   |  |  |
   |  |  +- f228(x0,x1,x2,x3,x4,x5) = 1 + x0 + x0*x3 + x1 + x2 + x3
   |  |  |
   |  |  +- f229(x0,x1,x2,x3,x4,x5) = 1 + x0 + x0*x3 + x1 + x2 + x3
   |  |  |
   |  |  +- f4(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f5(x0,x1) = x1
   |  |  |
   |  |  +- f6(x0,x1,x2) = x0*x2 + x1
   |  |  |
   |  |  +- f7(x0,x1,x2) = x2
   |  |  |
   |  |  `- f8(x0,x1,x2) = 1 + x0*x2 + x1 + x2
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0,x1,x2) = 1 + x0 + x1
   |  |  |
   |  |  +- f11(x0,x1,x2) = x2
   |  |  |
   |  |  +- f12(x0,x1,x2) = 2 + x0*x2 + 2*x2
   |  |  |
   |  |  +- f197(x0) = 1 + x0
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5) = 1 + x0*x2 + 2*x2 + x3
   |  |  |
   |  |  +- f210(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f211(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f212(x0,x1,x2) = 1 + x1 + x2
   |  |  |
   |  |  +- f217(x0,x1,x2,x3,x4) = x0 + x1
   |  |  |
   |  |  +- f218(x0,x1,x2) = x0 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2) = x0 + x2
   |  |  |
   |  |  +- f222(x0) = x0
   |  |  |
   |  |  +- f223(x0,x1,x2) = x0 + x2
   |  |  |
   |  |  +- f226(x0,x1,x2,x3,x4,x5) = x0 + x2
   |  |  |
   |  |  +- f227(x0,x1,x2,x3,x4) = x2
   |  |  |
   |  |  +- f228(x0,x1,x2,x3,x4,x5) = 1 + x0 + x0*x3 + x2 + x3
   |  |  |
   |  |  +- f229(x0,x1,x2,x3,x4,x5) = 1 + x0 + x0*x3 + x2 + x3
   |  |  |
   |  |  +- f4(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f5(x0,x1) = x1
   |  |  |
   |  |  +- f6(x0,x1,x2) = x0 + x1
   |  |  |
   |  |  +- f7(x0,x1,x2) = x2
   |  |  |
   |  |  `- f8(x0,x1,x2) = 1 + x0*x2 + x2
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with DecreaseCoeff... Failed
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:46.605013 UTC(+0.466017s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + x1
   |  |
   |  +- f10(x0,x1,x2) = 1 + x0 + x1
   |  |
   |  +- f11(x0,x1,x2) = x2
   |  |
   |  +- f12(x0,x1,x2) = 2 + x0*x2 + 2*x2
   |  |
   |  +- f191(x0) = x0
   |  |
   |  +- f192(x0) = x0
   |  |
   |  +- f193(x0) = x0
   |  |
   |  +- f194(x0) = x0
   |  |
   |  +- f195(x0) = x0
   |  |
   |  +- f196(x0) = x0
   |  |
   |  +- f197(x0) = 1 + x0
   |  |
   |  +- f198(x0,x1,x2,x3) = x1
   |  |
   |  +- f199(x0) = x0
   |  |
   |  +- f2(x0,x1) = 1 + x0
   |  |
   |  +- f200(x0) = x0
   |  |
   |  +- f201(x0,x1,x2,x3,x4,x5) = x3
   |  |
   |  +- f202(x0,x1,x2,x3,x4,x5) = 1 + x0*x2 + 2*x2 + x3
   |  |
   |  +- f203(x0) = x0
   |  |
   |  +- f204(x0) = x0
   |  |
   |  +- f205(x0) = x0
   |  |
   |  +- f206(x0) = x0
   |  |
   |  +- f207(x0) = x0
   |  |
   |  +- f208(x0) = x0
   |  |
   |  +- f209(x0,x1,x2) = x1
   |  |
   |  +- f210(x0,x1) = x0 + x1
   |  |
   |  +- f211(x0,x1,x2) = 1 + x1 + x2
   |  |
   |  +- f212(x0,x1,x2) = 1 + x1 + x2
   |  |
   |  +- f213(x0) = x0
   |  |
   |  +- f214(x0) = x0
   |  |
   |  +- f215(x0) = x0
   |  |
   |  +- f216(x0) = x0
   |  |
   |  +- f217(x0,x1,x2,x3,x4) = x0 + x1
   |  |
   |  +- f218(x0,x1,x2) = x0 + x2
   |  |
   |  +- f219(x0,x1,x2) = x0 + x2
   |  |
   |  +- f220(x0) = x0
   |  |
   |  +- f221(x0) = x0
   |  |
   |  +- f222(x0) = x0
   |  |
   |  +- f223(x0,x1,x2) = x0 + x2
   |  |
   |  +- f224(x0) = x0
   |  |
   |  +- f225(x0) = x0
   |  |
   |  +- f226(x0,x1,x2,x3,x4,x5) = x0 + x2
   |  |
   |  +- f227(x0,x1,x2,x3,x4) = x2
   |  |
   |  +- f228(x0,x1,x2,x3,x4,x5) = 1 + x0 + x0*x3 + x2 + x3
   |  |
   |  +- f229(x0,x1,x2,x3,x4,x5) = 1 + x0 + x0*x3 + x2 + x3
   |  |
   |  +- f230(x0) = x0
   |  |
   |  +- f231(x0) = x0
   |  |
   |  +- f232() = 0
   |  |
   |  +- f3(x0,x1,x2) = 0
   |  |
   |  +- f4(x0,x1) = x0 + x1
   |  |
   |  +- f5(x0,x1) = x1
   |  |
   |  +- f6(x0,x1,x2) = x0 + x1
   |  |
   |  +- f7(x0,x1,x2) = x2
   |  |
   |  +- f8(x0,x1,x2) = 1 + x0*x2 + x2
   |  |
   |  `- f9(x0,x1,x2,x3) = 0
   |
   +- Constraints
   |  |
   |  +- f191(x5) = x5 >= x5 = x5
   |  |
   |  +- f192(x5) = x5 >= x5 = f191(x5)
   |  |
   |  +- f193(x2) = x2 >= x2 = x2
   |  |
   |  +- f194(x5) = x5 >= x5 = f192(x5)
   |  |
   |  +- f195(x66) = x66 >= x66 = x66
   |  |
   |  +- f196(x67) = x67 >= x67 = x67
   |  |
   |  +- f4(x66,f197(x2)) = x66 + (1 + x2) >= x2 + x66 = f1(f193(x2),f195(x66))
   |  |
   |  +- f5(x66,f197(x2)) + x67 = (1 + x2) + x67 >= (1 + x2) + 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) = 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) = 1 + ((x2 * x4) + ((2 * x4) + x5)) >= (1 + (((1 + x2) * x4) + x4)) + x5 = f8(f197(x2),f200(x3),f199(x4)) + f201(x2,x3,x4,x5,x66,x67)
   |  |
   |  +- f11(x2,x3,x4) = x4 >= x4 = f7(f197(x2),f200(x3),f199(x4))
   |  |
   |  +- f10(x2,x3,x4) = 1 + (x2 + x3) >= (1 + x2) + x3 = f6(f197(x2),f200(x3),f199(x4))
   |  |
   |  +- f12(x2,x3,x4) + x5 = (2 + ((x2 * x4) + (2 * x4))) + x5 >= (1 + ((x2 * x4) + ((2 * 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) = x8 >= x8 = x8
   |  |
   |  +- f209(x8,x9,x11) = x9 >= x9 = f3(f206(x11),f208(x8),f209(x8,x9,x11)) + f207(x9)
   |  |
   |  +- f210(x8,x11) = x8 + x11 >= x11 + x8 = f1(f206(x11),f208(x8))
   |  |
   |  +- f211(x8,x9,x11) = 1 + (x9 + x11) >= (1 + x11) + x9 = f2(f206(x11),f208(x8)) + f209(x8,x9,x11)
   |  |
   |  +- f212(x8,x9,x11) = 1 + (x9 + x11) >= 1 + (x9 + x11) = f211(x8,x9,x11)
   |  |
   |  +- f1(x11 + 1,x8) = (x11 + 1) + x8 >= (x8 + x11) + 1 = f210(x8,x11) + 1
   |  |
   |  +- f2(x11 + 1,x8) + x9 = (1 + (x11 + 1)) + x9 >= (1 + (x9 + x11)) + 1 = f212(x8,x9,x11) + 1
   |  |
   |  +- f213(x15) = x15 >= x15 = x15
   |  |
   |  +- f1(0,x14) = x14 >= x14 = x14
   |  |
   |  +- f2(0,x14) + x15 = 1 + x15 >= 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) = x18 + x19 >= x19 + x18 = f4(f215(x19),x18)
   |  |
   |  +- f218(x18,x19,x21) = x18 + x21 >= x18 + x21 = f5(f215(x19),x18) + f216(x21)
   |  |
   |  +- f219(x18,x19,x21) = x18 + x21 >= x18 + x21 = f218(x18,x19,x21)
   |  |
   |  +- f220(x145) = x145 >= x145 = x145
   |  |
   |  +- f221(x146) = x146 >= x146 = x146
   |  |
   |  +- f4(x145,f222(x18)) = x145 + x18 >= x145 + x18 = f4(f220(x145),x18)
   |  |
   |  +- f5(x145,f222(x18)) + x146 = x18 + x146 >= x18 + x146 = f5(f220(x145),x18) + f221(x146)
   |  |
   |  +- f223(x18,x19,x21) = x18 + x21 >= x18 + x21 = f219(x18,x19,x21)
   |  |
   |  +- f224(x23) = x23 >= x23 = x23
   |  |
   |  +- f225(x19) = x19 >= x19 = x19
   |  |
   |  +- f226(x18,x19,x21,x23,x145,x146) = x18 + x21 >= x18 + 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) = x23 >= x23 = f7(f222(x18),f225(x19),f224(x23))
   |  |
   |  +- f217(x18,x19,x23,x145,x146) = x18 + x19 >= x18 + x19 = f6(f222(x18),f225(x19),f224(x23))
   |  |
   |  +- f228(x18,x19,x21,x23,x145,x146) = 1 + (x18 + ((x18 * x23) + (x21 + x23))) >= (1 + ((x18 * x23) + x23)) + (x18 + x21) = f8(f222(x18),f225(x19),f224(x23)) + f226(x18,x19,x21,x23,x145,x146)
   |  |
   |  +- f229(x18,x19,x21,x23,x145,x146) = 1 + (x18 + ((x18 * x23) + (x21 + x23))) >= 1 + (x18 + ((x18 * x23) + (x21 + x23))) = f228(x18,x19,x21,x23,x145,x146)
   |  |
   |  +- f7(x18,x19,x23 + 1) = x23 + 1 >= x23 + 1 = f227(x18,x19,x23,x145,x146) + 1
   |  |
   |  +- f6(x18,x19,x23 + 1) = x18 + x19 >= x18 + x19 = f217(x18,x19,x23,x145,x146)
   |  |
   |  +- f8(x18,x19,x23 + 1) + x21 = (1 + ((x18 * (x23 + 1)) + (x23 + 1))) + x21 >= (1 + (x18 + ((x18 * x23) + (x21 + x23)))) + 1 = f229(x18,x19,x21,x23,x145,x146) + 1
   |  |
   |  +- f230(x30) = x30 >= x30 = x30
   |  |
   |  +- f231(x30) = x30 >= x30 = f230(x30)
   |  |
   |  +- f7(x27,x28,0) = 0 >= 0 = 0
   |  |
   |  +- f6(x27,x28,0) = x27 + x28 >= 0 = f232()
   |  |
   |  `- f8(x27,x28,0) + x30 = 1 + x30 >= x30 + 1 = f231(x30) + 1
   |
   `- Stopping timer: 2017-03-30 07:32:46.60565 UTC(+0.741011s)