SUCCESS(1)

SUCCESS
f1(x0,x1) = x0 + x1;
f10(x0) = 1;
f11(x0) = x0;
f12(x0) = 6 + 2*x0;
f13(x0,x1) = x0 + x1;
f14(x0,x1) = 1 + x0;
f15(x0,x1,x2) = 1 + x0;
f187(x0) = x0;
f188(x0) = x0;
f189(x0) = x0;
f190(x0,x1) = 1 + x0 + x1;
f191() = 0;
f192(x0,x1) = 1 + x0 + x1;
f193(x0,x1) = 5 + 2*x0 + x1;
f194(x0) = x0;
f195(x0) = x0;
f196(x0) = x0;
f197(x0) = x0;
f198(x0) = x0;
f199(x0) = x0;
f2(x0,x1) = 1 + x1;
f200(x0) = x0;
f201(x0,x1,x2,x3) = 1 + x0 + x1;
f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3;
f203() = 0;
f204(x0) = x0;
f205(x0) = x0;
f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3;
f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3;
f208(x0) = x0;
f209(x0) = x0;
f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + 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) = 1 + x2;
f219(x0,x1,x2,x3) = x3;
f220(x0,x1,x2,x3) = 1 + x0 + x3;
f3(x0,x1,x2) = 1 + x1;
f4(x0,x1,x2) = 0;
f5(x0,x1,x2) = 1 + x0 + x2;
f6(x0,x1,x2) = 2 + x0;
f7(x0,x1,x2,x3) = 0;
f8(x0,x1,x2,x3,x4) = 0;
f9(x0) = x0;

ExecutionLog
|
`- SOLVE ...
   |
   +- Staring timer: 2017-03-30 07:32:21.435818 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
   |
   +- Simplification ...
   |  |
   |  +- Substituted: f3(f200(x10),x124,f203()) ≥ f208(x124) + 1 ↦ f3(f200(0),x124,f203()) ≥ f208(x124) + 1
   |  |
   |  +- Substituted: f4(f200(x10),x124,f203()) + x125 ≥ f209(x125) ↦ f4(f200(0),0,f203()) + x125 ≥ f209(x125)
   |  |
   |  +- Substituted: f15(0,x13,x14) + x15 ≥ f212(x15) + 1 ↦ f15(0,0,0) + x15 ≥ f212(x15) + 1
   |  |
   |  +- Substituted: f10(x18) + x19 ≥ f215(x19) + 1 ↦ f10(0) + x19 ≥ f215(x19) + 1
   |  |
   |  +- Eliminated: f7/4
   |  |
   |  +- Eliminated: f8/5
   |  |
   |  +- Propagated: f187(x0) ↦ x0
   |  |
   |  +- Propagated: f188(x0) ↦ x0
   |  |
   |  +- Propagated: f191() ↦ 0
   |  |
   |  +- Propagated: f194(x0) ↦ x0
   |  |
   |  +- Propagated: f196(x0) ↦ x0
   |  |
   |  +- Propagated: f198(x0) ↦ x0
   |  |
   |  +- Propagated: f199(x0) ↦ x0
   |  |
   |  +- Propagated: f204(x0) ↦ x0
   |  |
   |  +- Propagated: f205(x0) ↦ x0
   |  |
   |  +- Propagated: f208(x0) ↦ x0
   |  |
   |  +- Propagated: f209(x0) ↦ x0
   |  |
   |  +- Propagated: f211(x0) ↦ x0
   |  |
   |  +- Propagated: f213(x0) ↦ x0
   |  |
   |  +- Propagated: f214(x0) ↦ x0
   |  |
   |  +- Propagated: f215(x0) ↦ x0
   |  |
   |  +- Propagated: f216(x0) ↦ x0
   |  |
   |  +- Propagated: f217(x0) ↦ x0
   |  |
   |  +- Propagated: f9(x0) ↦ x0
   |  |
   |  +- Propagated: f189(x0) ↦ x0
   |  |
   |  +- Propagated: f195(x0) ↦ x0
   |  |
   |  +- Propagated: f212(x0) ↦ x0
   |  |
   |  `- Propagated: f197(x0) ↦ x0
   |
   +- SMT-SLI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:21.637361 UTC
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:21.712907 UTC(+0.075546s)
   |
   +- SMT-LI ...
   |  |
   |  +- Staring timer: 2017-03-30 07:32:21.712914 UTC
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + 6*x1
   |  |  |
   |  |  +- f10(x0) = 13
   |  |  |
   |  |  +- f11(x0) = 15 + 14*x0
   |  |  |
   |  |  +- f12(x0) = 15 + 15*x0
   |  |  |
   |  |  +- f13(x0,x1) = 1 + 12*x0 + x1
   |  |  |
   |  |  +- f14(x0,x1) = 13 + 14*x0 + x1
   |  |  |
   |  |  +- f15(x0,x1,x2) = 1 + x0
   |  |  |
   |  |  +- f190(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f192(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f193(x0,x1) = 14 + 15*x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 6 + x0 + 7*x1
   |  |  |
   |  |  +- f200(x0) = 1 + 2*x0
   |  |  |
   |  |  +- f201(x0,x1,x2,x3) = 1 + x0 + x1
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f203() = 12
   |  |  |
   |  |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f218(x0,x1,x2) = 1 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2,x3) = x1 + x3
   |  |  |
   |  |  +- f220(x0,x1,x2,x3) = 7 + 7*x0 + x1 + x2 + x3
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 0
   |  |  |
   |  |  +- f5(x0,x1,x2) = 1 + 6*x0 + x2
   |  |  |
   |  |  `- f6(x0,x1,x2) = 8 + 7*x0 + x1 + x2
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0) = 13
   |  |  |
   |  |  +- f11(x0) = 1 + x0
   |  |  |
   |  |  +- f12(x0) = 15 + 8*x0
   |  |  |
   |  |  +- f13(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f14(x0,x1) = 13 + 7*x0
   |  |  |
   |  |  +- f15(x0,x1,x2) = 1 + x0
   |  |  |
   |  |  +- f190(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f192(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f193(x0,x1) = 14 + 8*x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 6 + 7*x1
   |  |  |
   |  |  +- f200(x0) = 1 + x0
   |  |  |
   |  |  +- f201(x0,x1,x2,x3) = 1 + x0 + x1
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f203() = 1
   |  |  |
   |  |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f218(x0,x1,x2) = 1 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2,x3) = x3
   |  |  |
   |  |  +- f220(x0,x1,x2,x3) = 6 + 7*x0 + x3
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 0
   |  |  |
   |  |  +- f5(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  `- f6(x0,x1,x2) = 7 + 7*x0
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0) = 6
   |  |  |
   |  |  +- f11(x0) = x0
   |  |  |
   |  |  +- f12(x0) = 8 + 2*x0
   |  |  |
   |  |  +- f13(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f14(x0,x1) = 6 + x0
   |  |  |
   |  |  +- f15(x0,x1,x2) = 1 + x0
   |  |  |
   |  |  +- f190(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f192(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f193(x0,x1) = 7 + 2*x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 6 + x1
   |  |  |
   |  |  +- f200(x0) = x0
   |  |  |
   |  |  +- f201(x0,x1,x2,x3) = 1 + x0 + x1
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f203() = 1
   |  |  |
   |  |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f218(x0,x1,x2) = 1 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2,x3) = x3
   |  |  |
   |  |  +- f220(x0,x1,x2,x3) = 6 + x0 + x3
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 0
   |  |  |
   |  |  +- f5(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  `- f6(x0,x1,x2) = 7 + x0
   |  |
   |  +- Minimizing with  ZeroOut ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0) = 6
   |  |  |
   |  |  +- f11(x0) = x0
   |  |  |
   |  |  +- f12(x0) = 8 + 2*x0
   |  |  |
   |  |  +- f13(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f14(x0,x1) = 6 + x0
   |  |  |
   |  |  +- f15(x0,x1,x2) = 1 + x0
   |  |  |
   |  |  +- f190(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f192(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f193(x0,x1) = 7 + 2*x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 6 + x1
   |  |  |
   |  |  +- f200(x0) = x0
   |  |  |
   |  |  +- f201(x0,x1,x2,x3) = 1 + x0 + x1
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f203() = 0
   |  |  |
   |  |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f218(x0,x1,x2) = 1 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2,x3) = x3
   |  |  |
   |  |  +- f220(x0,x1,x2,x3) = 6 + x0 + x3
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 0
   |  |  |
   |  |  +- f5(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  `- f6(x0,x1,x2) = 7 + x0
   |  |
   |  +- Minimizing with ZeroOut... Failed
   |  |
   |  +- Minimizing with  DecreaseCoeff ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0) = 1
   |  |  |
   |  |  +- f11(x0) = x0
   |  |  |
   |  |  +- f12(x0) = 8 + 2*x0
   |  |  |
   |  |  +- f13(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f14(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f15(x0,x1,x2) = 1 + x0
   |  |  |
   |  |  +- f190(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f192(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f193(x0,x1) = 7 + 2*x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x1
   |  |  |
   |  |  +- f200(x0) = x0
   |  |  |
   |  |  +- f201(x0,x1,x2,x3) = 1 + x0 + x1
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f203() = 0
   |  |  |
   |  |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f218(x0,x1,x2) = 1 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2,x3) = x3
   |  |  |
   |  |  +- f220(x0,x1,x2,x3) = 1 + x0 + x3
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 0
   |  |  |
   |  |  +- f5(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  `- f6(x0,x1,x2) = 2 + x0
   |  |
   |  +- Minimizing with  DecreaseCoeff ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0) = 1
   |  |  |
   |  |  +- f11(x0) = x0
   |  |  |
   |  |  +- f12(x0) = 7 + 2*x0
   |  |  |
   |  |  +- f13(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f14(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f15(x0,x1,x2) = 1 + x0
   |  |  |
   |  |  +- f190(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f192(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f193(x0,x1) = 6 + 2*x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x1
   |  |  |
   |  |  +- f200(x0) = x0
   |  |  |
   |  |  +- f201(x0,x1,x2,x3) = 1 + x0 + x1
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f203() = 0
   |  |  |
   |  |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f218(x0,x1,x2) = 1 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2,x3) = x3
   |  |  |
   |  |  +- f220(x0,x1,x2,x3) = 1 + x0 + x3
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 0
   |  |  |
   |  |  +- f5(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  `- f6(x0,x1,x2) = 2 + x0
   |  |
   |  +- Minimizing with  DecreaseCoeff ...
   |  |
   |  +- Interpretation
   |  |  |
   |  |  +- f1(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f10(x0) = 1
   |  |  |
   |  |  +- f11(x0) = x0
   |  |  |
   |  |  +- f12(x0) = 6 + 2*x0
   |  |  |
   |  |  +- f13(x0,x1) = x0 + x1
   |  |  |
   |  |  +- f14(x0,x1) = 1 + x0
   |  |  |
   |  |  +- f15(x0,x1,x2) = 1 + x0
   |  |  |
   |  |  +- f190(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f192(x0,x1) = 1 + x0 + x1
   |  |  |
   |  |  +- f193(x0,x1) = 5 + 2*x0 + x1
   |  |  |
   |  |  +- f2(x0,x1) = 1 + x1
   |  |  |
   |  |  +- f200(x0) = x0
   |  |  |
   |  |  +- f201(x0,x1,x2,x3) = 1 + x0 + x1
   |  |  |
   |  |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f203() = 0
   |  |  |
   |  |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |  |
   |  |  +- f218(x0,x1,x2) = 1 + x2
   |  |  |
   |  |  +- f219(x0,x1,x2,x3) = x3
   |  |  |
   |  |  +- f220(x0,x1,x2,x3) = 1 + x0 + x3
   |  |  |
   |  |  +- f3(x0,x1,x2) = 1 + x1
   |  |  |
   |  |  +- f4(x0,x1,x2) = 0
   |  |  |
   |  |  +- f5(x0,x1,x2) = 1 + x0 + x2
   |  |  |
   |  |  `- f6(x0,x1,x2) = 2 + x0
   |  |
   |  `- Stopping timer: 2017-03-30 07:32:22.127964 UTC(+0.41505s)
   |
   +- Interpretation
   |  |
   |  +- f1(x0,x1) = x0 + x1
   |  |
   |  +- f10(x0) = 1
   |  |
   |  +- f11(x0) = x0
   |  |
   |  +- f12(x0) = 6 + 2*x0
   |  |
   |  +- f13(x0,x1) = x0 + x1
   |  |
   |  +- f14(x0,x1) = 1 + x0
   |  |
   |  +- f15(x0,x1,x2) = 1 + x0
   |  |
   |  +- f187(x0) = x0
   |  |
   |  +- f188(x0) = x0
   |  |
   |  +- f189(x0) = x0
   |  |
   |  +- f190(x0,x1) = 1 + x0 + x1
   |  |
   |  +- f191() = 0
   |  |
   |  +- f192(x0,x1) = 1 + x0 + x1
   |  |
   |  +- f193(x0,x1) = 5 + 2*x0 + x1
   |  |
   |  +- f194(x0) = x0
   |  |
   |  +- f195(x0) = x0
   |  |
   |  +- f196(x0) = x0
   |  |
   |  +- f197(x0) = x0
   |  |
   |  +- f198(x0) = x0
   |  |
   |  +- f199(x0) = x0
   |  |
   |  +- f2(x0,x1) = 1 + x1
   |  |
   |  +- f200(x0) = x0
   |  |
   |  +- f201(x0,x1,x2,x3) = 1 + x0 + x1
   |  |
   |  +- f202(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |
   |  +- f203() = 0
   |  |
   |  +- f204(x0) = x0
   |  |
   |  +- f205(x0) = x0
   |  |
   |  +- f206(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |
   |  +- f207(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + x3
   |  |
   |  +- f208(x0) = x0
   |  |
   |  +- f209(x0) = x0
   |  |
   |  +- f210(x0,x1,x2,x3,x4,x5,x6,x7) = 1 + x2 + 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) = 1 + x2
   |  |
   |  +- f219(x0,x1,x2,x3) = x3
   |  |
   |  +- f220(x0,x1,x2,x3) = 1 + x0 + x3
   |  |
   |  +- f3(x0,x1,x2) = 1 + x1
   |  |
   |  +- f4(x0,x1,x2) = 0
   |  |
   |  +- f5(x0,x1,x2) = 1 + x0 + x2
   |  |
   |  +- f6(x0,x1,x2) = 2 + x0
   |  |
   |  +- f7(x0,x1,x2,x3) = 0
   |  |
   |  +- f8(x0,x1,x2,x3,x4) = 0
   |  |
   |  `- f9(x0) = x0
   |
   +- Constraints
   |  |
   |  +- f187(x3) = x3 >= x3 = x3
   |  |
   |  +- f188(x2) = x2 >= x2 = x2
   |  |
   |  +- f189(x3) = x3 >= x3 = f187(x3)
   |  |
   |  +- f190(x2,x3) = 1 + (x2 + x3) >= (1 + x2) + x3 = f15(f188(x2),f191(),f192(x2,x3)) + f189(x3)
   |  |
   |  +- f191() = 0 >= 0 = 0
   |  |
   |  +- f192(x2,x3) = 1 + (x2 + x3) >= 1 + (x2 + x3) = f190(x2,x3)
   |  |
   |  +- f193(x2,x3) = 5 + ((2 * x2) + x3) >= (1 + x2) + (1 + (x2 + x3)) = f14(f188(x2),f191()) + f192(x2,x3)
   |  |
   |  +- f11(x2) = x2 >= x2 = f13(f188(x2),f191())
   |  |
   |  +- f12(x2) + x3 = (6 + (2 * x2)) + x3 >= (5 + ((2 * 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 + x10 >= x10 + x83 = f13(f196(x10),f198(x83))
   |  |
   |  +- f2(x83,f200(x10)) + x84 = (1 + x10) + x84 >= (1 + x10) + x84 = f14(f196(x10),f198(x83)) + f199(x84)
   |  |
   |  +- f201(x8,x10,x83,x84) = 1 + (x8 + x10) >= (1 + x10) + x8 = f15(f196(x10),f198(x83),f199(x84)) + f197(x8)
   |  |
   |  +- f202(x6,x7,x8,x10,x83,x84,x124,x125) = 1 + (x8 + x10) >= 1 + (x8 + 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) = 1 + (x8 + x10) >= 1 + (x8 + 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()) = 1 + x124 >= x124 + 1 = f208(x124) + 1
   |  |
   |  +- f4(f200(x10),x124,f203()) + x125 = x125 >= x125 = f209(x125)
   |  |
   |  +- f206(x6,x7,x8,x10,x83,x84,x124,x125) = 1 + (x8 + x10) >= 1 + (x8 + x10) = f207(x6,x7,x8,x10,x83,x84,x124,x125)
   |  |
   |  +- f210(x6,x7,x8,x10,x83,x84,x124,x125) = 1 + (x8 + x10) >= 1 + (x8 + 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) = (x10 + 1) + x6 >= 1 + (x10 + x6) = f5(f200(x10),f203(),f204(x6))
   |  |
   |  +- f14(x10 + 1,x6) + x7 = (1 + (x10 + 1)) + x7 >= (2 + x10) + x7 = f6(f200(x10),f203(),f204(x6)) + f205(x7)
   |  |
   |  +- f15(x10 + 1,x6,x7) + x8 = (1 + (x10 + 1)) + x8 >= (1 + (x8 + 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 = 1 + x14 >= 1 + x14 = f10(f213(x13)) + f214(x14)
   |  |
   |  +- f15(0,x13,x14) + x15 = 1 + x15 >= x15 + 1 = f212(x15) + 1
   |  |
   |  +- f215(x19) = x19 >= x19 = x19
   |  |
   |  +- f9(x18) = x18 >= x18 = x18
   |  |
   |  +- f10(x18) + x19 = 1 + x19 >= x19 + 1 = f215(x19) + 1
   |  |
   |  +- f216(x23) = x23 >= x23 = x23
   |  |
   |  +- f217(x24) = x24 >= x24 = x24
   |  |
   |  +- f218(x21,x22,x23) = 1 + x23 >= 1 + x23 = f3(x21,f216(x23),x22)
   |  |
   |  +- f219(x21,x22,x23,x24) = x24 >= x24 = f4(x21,f216(x23),x22) + f217(x24)
   |  |
   |  +- f220(x21,x22,x23,x24) = 1 + (x21 + x24) >= (1 + x21) + x24 = f2(f218(x21,x22,x23),x21) + f219(x21,x22,x23,x24)
   |  |
   |  +- f5(x21,x22,x23) = 1 + (x21 + x23) >= (1 + x23) + x21 = f1(f218(x21,x22,x23),x21)
   |  |
   |  `- f6(x21,x22,x23) + x24 = (2 + x21) + x24 >= (1 + (x21 + x24)) + 1 = f220(x21,x22,x23,x24) + 1
   |
   `- Stopping timer: 2017-03-30 07:32:22.128181 UTC(+0.692363s)