YES
Time: 0.191857
TRS:
 {  f(x, y, z, 0()) -> 2(),
  f(g x, h x, y, x) -> f(y, y, y, x),
              g 0() -> 2(),
              h 0() -> 2()}
 BOUND:
  Bound: top(-raise)-bounded by 2
  Automaton:
   {
              0_0() -> 5*
              2_2() -> 6* | 4 | 3 | 2 | 1
              2_1() -> 6* | 4 | 3 | 2 | 1
              2_0() -> 4*
             h_0(6) -> 3*
             h_0(5) -> 3*
             h_0(4) -> 3*
             h_0(3) -> 3*
             h_0(2) -> 3*
             h_0(1) -> 3*
             g_0(6) -> 2*
             g_0(5) -> 2*
             g_0(4) -> 2*
             g_0(3) -> 2*
             g_0(2) -> 2*
             g_0(1) -> 2*
    f_1(6, 6, 6, 6) -> 1*
    f_1(6, 6, 6, 5) -> 1*
    f_1(6, 6, 6, 4) -> 1*
    f_1(6, 6, 6, 3) -> 1*
    f_1(6, 6, 6, 2) -> 1*
    f_1(6, 6, 6, 1) -> 1*
    f_1(6, 6, 4, 6) -> 1*
    f_1(6, 6, 4, 5) -> 1*
    f_1(6, 6, 4, 4) -> 1*
    f_1(6, 6, 4, 3) -> 1*
    f_1(6, 6, 4, 2) -> 1*
    f_1(6, 6, 4, 1) -> 1*
    f_1(6, 6, 3, 6) -> 1*
    f_1(6, 6, 3, 5) -> 1*
    f_1(6, 6, 3, 4) -> 1*
    f_1(6, 6, 3, 3) -> 1*
    f_1(6, 6, 3, 2) -> 1*
    f_1(6, 6, 3, 1) -> 1*
    f_1(6, 6, 2, 6) -> 1*
    f_1(6, 6, 2, 5) -> 1*
    f_1(6, 6, 2, 4) -> 1*
    f_1(6, 6, 2, 3) -> 1*
    f_1(6, 6, 2, 2) -> 1*
    f_1(6, 6, 2, 1) -> 1*
    f_1(6, 6, 1, 6) -> 1*
    f_1(6, 6, 1, 5) -> 1*
    f_1(6, 6, 1, 4) -> 1*
    f_1(6, 6, 1, 3) -> 1*
    f_1(6, 6, 1, 2) -> 1*
    f_1(6, 6, 1, 1) -> 1*
    f_1(6, 4, 6, 6) -> 1*
    f_1(6, 4, 6, 5) -> 1*
    f_1(6, 4, 6, 4) -> 1*
    f_1(6, 4, 6, 3) -> 1*
    f_1(6, 4, 6, 2) -> 1*
    f_1(6, 4, 6, 1) -> 1*
    f_1(6, 4, 4, 6) -> 1*
    f_1(6, 4, 4, 5) -> 1*
    f_1(6, 4, 4, 4) -> 1*
    f_1(6, 4, 4, 3) -> 1*
    f_1(6, 4, 4, 2) -> 1*
    f_1(6, 4, 4, 1) -> 1*
    f_1(6, 3, 6, 6) -> 1*
    f_1(6, 3, 6, 5) -> 1*
    f_1(6, 3, 6, 4) -> 1*
    f_1(6, 3, 6, 3) -> 1*
    f_1(6, 3, 6, 2) -> 1*
    f_1(6, 3, 6, 1) -> 1*
    f_1(6, 3, 3, 6) -> 1*
    f_1(6, 3, 3, 5) -> 1*
    f_1(6, 3, 3, 4) -> 1*
    f_1(6, 3, 3, 3) -> 1*
    f_1(6, 3, 3, 2) -> 1*
    f_1(6, 3, 3, 1) -> 1*
    f_1(6, 2, 6, 6) -> 1*
    f_1(6, 2, 6, 5) -> 1*
    f_1(6, 2, 6, 4) -> 1*
    f_1(6, 2, 6, 3) -> 1*
    f_1(6, 2, 6, 2) -> 1*
    f_1(6, 2, 6, 1) -> 1*
    f_1(6, 2, 2, 6) -> 1*
    f_1(6, 2, 2, 5) -> 1*
    f_1(6, 2, 2, 4) -> 1*
    f_1(6, 2, 2, 3) -> 1*
    f_1(6, 2, 2, 2) -> 1*
    f_1(6, 2, 2, 1) -> 1*
    f_1(6, 1, 6, 6) -> 1*
    f_1(6, 1, 6, 5) -> 1*
    f_1(6, 1, 6, 4) -> 1*
    f_1(6, 1, 6, 3) -> 1*
    f_1(6, 1, 6, 2) -> 1*
    f_1(6, 1, 6, 1) -> 1*
    f_1(6, 1, 1, 6) -> 1*
    f_1(6, 1, 1, 5) -> 1*
    f_1(6, 1, 1, 4) -> 1*
    f_1(6, 1, 1, 3) -> 1*
    f_1(6, 1, 1, 2) -> 1*
    f_1(6, 1, 1, 1) -> 1*
    f_1(5, 5, 5, 6) -> 1*
    f_1(5, 5, 5, 5) -> 1*
    f_1(5, 5, 5, 4) -> 1*
    f_1(5, 5, 5, 3) -> 1*
    f_1(5, 5, 5, 2) -> 1*
    f_1(5, 5, 5, 1) -> 1*
    f_1(4, 6, 6, 6) -> 1*
    f_1(4, 6, 6, 5) -> 1*
    f_1(4, 6, 6, 4) -> 1*
    f_1(4, 6, 6, 3) -> 1*
    f_1(4, 6, 6, 2) -> 1*
    f_1(4, 6, 6, 1) -> 1*
    f_1(4, 6, 4, 6) -> 1*
    f_1(4, 6, 4, 5) -> 1*
    f_1(4, 6, 4, 4) -> 1*
    f_1(4, 6, 4, 3) -> 1*
    f_1(4, 6, 4, 2) -> 1*
    f_1(4, 6, 4, 1) -> 1*
    f_1(4, 4, 6, 6) -> 1*
    f_1(4, 4, 6, 5) -> 1*
    f_1(4, 4, 6, 4) -> 1*
    f_1(4, 4, 6, 3) -> 1*
    f_1(4, 4, 6, 2) -> 1*
    f_1(4, 4, 6, 1) -> 1*
    f_1(4, 4, 4, 6) -> 1*
    f_1(4, 4, 4, 5) -> 1*
    f_1(4, 4, 4, 4) -> 1*
    f_1(4, 4, 4, 3) -> 1*
    f_1(4, 4, 4, 2) -> 1*
    f_1(4, 4, 4, 1) -> 1*
    f_1(3, 6, 6, 6) -> 1*
    f_1(3, 6, 6, 5) -> 1*
    f_1(3, 6, 6, 4) -> 1*
    f_1(3, 6, 6, 3) -> 1*
    f_1(3, 6, 6, 2) -> 1*
    f_1(3, 6, 6, 1) -> 1*
    f_1(3, 6, 3, 6) -> 1*
    f_1(3, 6, 3, 5) -> 1*
    f_1(3, 6, 3, 4) -> 1*
    f_1(3, 6, 3, 3) -> 1*
    f_1(3, 6, 3, 2) -> 1*
    f_1(3, 6, 3, 1) -> 1*
    f_1(3, 3, 6, 6) -> 1*
    f_1(3, 3, 6, 5) -> 1*
    f_1(3, 3, 6, 4) -> 1*
    f_1(3, 3, 6, 3) -> 1*
    f_1(3, 3, 6, 2) -> 1*
    f_1(3, 3, 6, 1) -> 1*
    f_1(3, 3, 3, 6) -> 1*
    f_1(3, 3, 3, 5) -> 1*
    f_1(3, 3, 3, 4) -> 1*
    f_1(3, 3, 3, 3) -> 1*
    f_1(3, 3, 3, 2) -> 1*
    f_1(3, 3, 3, 1) -> 1*
    f_1(2, 6, 6, 6) -> 1*
    f_1(2, 6, 6, 5) -> 1*
    f_1(2, 6, 6, 4) -> 1*
    f_1(2, 6, 6, 3) -> 1*
    f_1(2, 6, 6, 2) -> 1*
    f_1(2, 6, 6, 1) -> 1*
    f_1(2, 6, 2, 6) -> 1*
    f_1(2, 6, 2, 5) -> 1*
    f_1(2, 6, 2, 4) -> 1*
    f_1(2, 6, 2, 3) -> 1*
    f_1(2, 6, 2, 2) -> 1*
    f_1(2, 6, 2, 1) -> 1*
    f_1(2, 2, 6, 6) -> 1*
    f_1(2, 2, 6, 5) -> 1*
    f_1(2, 2, 6, 4) -> 1*
    f_1(2, 2, 6, 3) -> 1*
    f_1(2, 2, 6, 2) -> 1*
    f_1(2, 2, 6, 1) -> 1*
    f_1(2, 2, 2, 6) -> 1*
    f_1(2, 2, 2, 5) -> 1*
    f_1(2, 2, 2, 4) -> 1*
    f_1(2, 2, 2, 3) -> 1*
    f_1(2, 2, 2, 2) -> 1*
    f_1(2, 2, 2, 1) -> 1*
    f_1(1, 6, 6, 6) -> 1*
    f_1(1, 6, 6, 5) -> 1*
    f_1(1, 6, 6, 4) -> 1*
    f_1(1, 6, 6, 3) -> 1*
    f_1(1, 6, 6, 2) -> 1*
    f_1(1, 6, 6, 1) -> 1*
    f_1(1, 6, 1, 6) -> 1*
    f_1(1, 6, 1, 5) -> 1*
    f_1(1, 6, 1, 4) -> 1*
    f_1(1, 6, 1, 3) -> 1*
    f_1(1, 6, 1, 2) -> 1*
    f_1(1, 6, 1, 1) -> 1*
    f_1(1, 1, 6, 6) -> 1*
    f_1(1, 1, 6, 5) -> 1*
    f_1(1, 1, 6, 4) -> 1*
    f_1(1, 1, 6, 3) -> 1*
    f_1(1, 1, 6, 2) -> 1*
    f_1(1, 1, 6, 1) -> 1*
    f_1(1, 1, 1, 6) -> 1*
    f_1(1, 1, 1, 5) -> 1*
    f_1(1, 1, 1, 4) -> 1*
    f_1(1, 1, 1, 3) -> 1*
    f_1(1, 1, 1, 2) -> 1*
    f_1(1, 1, 1, 1) -> 1*
    f_0(6, 6, 6, 6) -> 1*
    f_0(6, 6, 6, 5) -> 1*
    f_0(6, 6, 6, 4) -> 1*
    f_0(6, 6, 6, 3) -> 1*
    f_0(6, 6, 6, 2) -> 1*
    f_0(6, 6, 6, 1) -> 1*
    f_0(6, 6, 5, 6) -> 1*
    f_0(6, 6, 5, 5) -> 1*
    f_0(6, 6, 5, 4) -> 1*
    f_0(6, 6, 5, 3) -> 1*
    f_0(6, 6, 5, 2) -> 1*
    f_0(6, 6, 5, 1) -> 1*
    f_0(6, 6, 4, 6) -> 1*
    f_0(6, 6, 4, 5) -> 1*
    f_0(6, 6, 4, 4) -> 1*
    f_0(6, 6, 4, 3) -> 1*
    f_0(6, 6, 4, 2) -> 1*
    f_0(6, 6, 4, 1) -> 1*
    f_0(6, 6, 3, 6) -> 1*
    f_0(6, 6, 3, 5) -> 1*
    f_0(6, 6, 3, 4) -> 1*
    f_0(6, 6, 3, 3) -> 1*
    f_0(6, 6, 3, 2) -> 1*
    f_0(6, 6, 3, 1) -> 1*
    f_0(6, 6, 2, 6) -> 1*
    f_0(6, 6, 2, 5) -> 1*
    f_0(6, 6, 2, 4) -> 1*
    f_0(6, 6, 2, 3) -> 1*
    f_0(6, 6, 2, 2) -> 1*
    f_0(6, 6, 2, 1) -> 1*
    f_0(6, 6, 1, 6) -> 1*
    f_0(6, 6, 1, 5) -> 1*
    f_0(6, 6, 1, 4) -> 1*
    f_0(6, 6, 1, 3) -> 1*
    f_0(6, 6, 1, 2) -> 1*
    f_0(6, 6, 1, 1) -> 1*
    f_0(6, 5, 6, 6) -> 1*
    f_0(6, 5, 6, 5) -> 1*
    f_0(6, 5, 6, 4) -> 1*
    f_0(6, 5, 6, 3) -> 1*
    f_0(6, 5, 6, 2) -> 1*
    f_0(6, 5, 6, 1) -> 1*
    f_0(6, 5, 5, 6) -> 1*
    f_0(6, 5, 5, 5) -> 1*
    f_0(6, 5, 5, 4) -> 1*
    f_0(6, 5, 5, 3) -> 1*
    f_0(6, 5, 5, 2) -> 1*
    f_0(6, 5, 5, 1) -> 1*
    f_0(6, 5, 4, 6) -> 1*
    f_0(6, 5, 4, 5) -> 1*
    f_0(6, 5, 4, 4) -> 1*
    f_0(6, 5, 4, 3) -> 1*
    f_0(6, 5, 4, 2) -> 1*
    f_0(6, 5, 4, 1) -> 1*
    f_0(6, 5, 3, 6) -> 1*
    f_0(6, 5, 3, 5) -> 1*
    f_0(6, 5, 3, 4) -> 1*
    f_0(6, 5, 3, 3) -> 1*
    f_0(6, 5, 3, 2) -> 1*
    f_0(6, 5, 3, 1) -> 1*
    f_0(6, 5, 2, 6) -> 1*
    f_0(6, 5, 2, 5) -> 1*
    f_0(6, 5, 2, 4) -> 1*
    f_0(6, 5, 2, 3) -> 1*
    f_0(6, 5, 2, 2) -> 1*
    f_0(6, 5, 2, 1) -> 1*
    f_0(6, 5, 1, 6) -> 1*
    f_0(6, 5, 1, 5) -> 1*
    f_0(6, 5, 1, 4) -> 1*
    f_0(6, 5, 1, 3) -> 1*
    f_0(6, 5, 1, 2) -> 1*
    f_0(6, 5, 1, 1) -> 1*
    f_0(6, 4, 6, 6) -> 1*
    f_0(6, 4, 6, 5) -> 1*
    f_0(6, 4, 6, 4) -> 1*
    f_0(6, 4, 6, 3) -> 1*
    f_0(6, 4, 6, 2) -> 1*
    f_0(6, 4, 6, 1) -> 1*
    f_0(6, 4, 5, 6) -> 1*
    f_0(6, 4, 5, 5) -> 1*
    f_0(6, 4, 5, 4) -> 1*
    f_0(6, 4, 5, 3) -> 1*
    f_0(6, 4, 5, 2) -> 1*
    f_0(6, 4, 5, 1) -> 1*
    f_0(6, 4, 4, 6) -> 1*
    f_0(6, 4, 4, 5) -> 1*
    f_0(6, 4, 4, 4) -> 1*
    f_0(6, 4, 4, 3) -> 1*
    f_0(6, 4, 4, 2) -> 1*
    f_0(6, 4, 4, 1) -> 1*
    f_0(6, 4, 3, 6) -> 1*
    f_0(6, 4, 3, 5) -> 1*
    f_0(6, 4, 3, 4) -> 1*
    f_0(6, 4, 3, 3) -> 1*
    f_0(6, 4, 3, 2) -> 1*
    f_0(6, 4, 3, 1) -> 1*
    f_0(6, 4, 2, 6) -> 1*
    f_0(6, 4, 2, 5) -> 1*
    f_0(6, 4, 2, 4) -> 1*
    f_0(6, 4, 2, 3) -> 1*
    f_0(6, 4, 2, 2) -> 1*
    f_0(6, 4, 2, 1) -> 1*
    f_0(6, 4, 1, 6) -> 1*
    f_0(6, 4, 1, 5) -> 1*
    f_0(6, 4, 1, 4) -> 1*
    f_0(6, 4, 1, 3) -> 1*
    f_0(6, 4, 1, 2) -> 1*
    f_0(6, 4, 1, 1) -> 1*
    f_0(6, 3, 6, 6) -> 1*
    f_0(6, 3, 6, 5) -> 1*
    f_0(6, 3, 6, 4) -> 1*
    f_0(6, 3, 6, 3) -> 1*
    f_0(6, 3, 6, 2) -> 1*
    f_0(6, 3, 6, 1) -> 1*
    f_0(6, 3, 5, 6) -> 1*
    f_0(6, 3, 5, 5) -> 1*
    f_0(6, 3, 5, 4) -> 1*
    f_0(6, 3, 5, 3) -> 1*
    f_0(6, 3, 5, 2) -> 1*
    f_0(6, 3, 5, 1) -> 1*
    f_0(6, 3, 4, 6) -> 1*
    f_0(6, 3, 4, 5) -> 1*
    f_0(6, 3, 4, 4) -> 1*
    f_0(6, 3, 4, 3) -> 1*
    f_0(6, 3, 4, 2) -> 1*
    f_0(6, 3, 4, 1) -> 1*
    f_0(6, 3, 3, 6) -> 1*
    f_0(6, 3, 3, 5) -> 1*
    f_0(6, 3, 3, 4) -> 1*
    f_0(6, 3, 3, 3) -> 1*
    f_0(6, 3, 3, 2) -> 1*
    f_0(6, 3, 3, 1) -> 1*
    f_0(6, 3, 2, 6) -> 1*
    f_0(6, 3, 2, 5) -> 1*
    f_0(6, 3, 2, 4) -> 1*
    f_0(6, 3, 2, 3) -> 1*
    f_0(6, 3, 2, 2) -> 1*
    f_0(6, 3, 2, 1) -> 1*
    f_0(6, 3, 1, 6) -> 1*
    f_0(6, 3, 1, 5) -> 1*
    f_0(6, 3, 1, 4) -> 1*
    f_0(6, 3, 1, 3) -> 1*
    f_0(6, 3, 1, 2) -> 1*
    f_0(6, 3, 1, 1) -> 1*
    f_0(6, 2, 6, 6) -> 1*
    f_0(6, 2, 6, 5) -> 1*
    f_0(6, 2, 6, 4) -> 1*
    f_0(6, 2, 6, 3) -> 1*
    f_0(6, 2, 6, 2) -> 1*
    f_0(6, 2, 6, 1) -> 1*
    f_0(6, 2, 5, 6) -> 1*
    f_0(6, 2, 5, 5) -> 1*
    f_0(6, 2, 5, 4) -> 1*
    f_0(6, 2, 5, 3) -> 1*
    f_0(6, 2, 5, 2) -> 1*
    f_0(6, 2, 5, 1) -> 1*
    f_0(6, 2, 4, 6) -> 1*
    f_0(6, 2, 4, 5) -> 1*
    f_0(6, 2, 4, 4) -> 1*
    f_0(6, 2, 4, 3) -> 1*
    f_0(6, 2, 4, 2) -> 1*
    f_0(6, 2, 4, 1) -> 1*
    f_0(6, 2, 3, 6) -> 1*
    f_0(6, 2, 3, 5) -> 1*
    f_0(6, 2, 3, 4) -> 1*
    f_0(6, 2, 3, 3) -> 1*
    f_0(6, 2, 3, 2) -> 1*
    f_0(6, 2, 3, 1) -> 1*
    f_0(6, 2, 2, 6) -> 1*
    f_0(6, 2, 2, 5) -> 1*
    f_0(6, 2, 2, 4) -> 1*
    f_0(6, 2, 2, 3) -> 1*
    f_0(6, 2, 2, 2) -> 1*
    f_0(6, 2, 2, 1) -> 1*
    f_0(6, 2, 1, 6) -> 1*
    f_0(6, 2, 1, 5) -> 1*
    f_0(6, 2, 1, 4) -> 1*
    f_0(6, 2, 1, 3) -> 1*
    f_0(6, 2, 1, 2) -> 1*
    f_0(6, 2, 1, 1) -> 1*
    f_0(6, 1, 6, 6) -> 1*
    f_0(6, 1, 6, 5) -> 1*
    f_0(6, 1, 6, 4) -> 1*
    f_0(6, 1, 6, 3) -> 1*
    f_0(6, 1, 6, 2) -> 1*
    f_0(6, 1, 6, 1) -> 1*
    f_0(6, 1, 5, 6) -> 1*
    f_0(6, 1, 5, 5) -> 1*
    f_0(6, 1, 5, 4) -> 1*
    f_0(6, 1, 5, 3) -> 1*
    f_0(6, 1, 5, 2) -> 1*
    f_0(6, 1, 5, 1) -> 1*
    f_0(6, 1, 4, 6) -> 1*
    f_0(6, 1, 4, 5) -> 1*
    f_0(6, 1, 4, 4) -> 1*
    f_0(6, 1, 4, 3) -> 1*
    f_0(6, 1, 4, 2) -> 1*
    f_0(6, 1, 4, 1) -> 1*
    f_0(6, 1, 3, 6) -> 1*
    f_0(6, 1, 3, 5) -> 1*
    f_0(6, 1, 3, 4) -> 1*
    f_0(6, 1, 3, 3) -> 1*
    f_0(6, 1, 3, 2) -> 1*
    f_0(6, 1, 3, 1) -> 1*
    f_0(6, 1, 2, 6) -> 1*
    f_0(6, 1, 2, 5) -> 1*
    f_0(6, 1, 2, 4) -> 1*
    f_0(6, 1, 2, 3) -> 1*
    f_0(6, 1, 2, 2) -> 1*
    f_0(6, 1, 2, 1) -> 1*
    f_0(6, 1, 1, 6) -> 1*
    f_0(6, 1, 1, 5) -> 1*
    f_0(6, 1, 1, 4) -> 1*
    f_0(6, 1, 1, 3) -> 1*
    f_0(6, 1, 1, 2) -> 1*
    f_0(6, 1, 1, 1) -> 1*
    f_0(5, 6, 6, 6) -> 1*
    f_0(5, 6, 6, 5) -> 1*
    f_0(5, 6, 6, 4) -> 1*
    f_0(5, 6, 6, 3) -> 1*
    f_0(5, 6, 6, 2) -> 1*
    f_0(5, 6, 6, 1) -> 1*
    f_0(5, 6, 5, 6) -> 1*
    f_0(5, 6, 5, 5) -> 1*
    f_0(5, 6, 5, 4) -> 1*
    f_0(5, 6, 5, 3) -> 1*
    f_0(5, 6, 5, 2) -> 1*
    f_0(5, 6, 5, 1) -> 1*
    f_0(5, 6, 4, 6) -> 1*
    f_0(5, 6, 4, 5) -> 1*
    f_0(5, 6, 4, 4) -> 1*
    f_0(5, 6, 4, 3) -> 1*
    f_0(5, 6, 4, 2) -> 1*
    f_0(5, 6, 4, 1) -> 1*
    f_0(5, 6, 3, 6) -> 1*
    f_0(5, 6, 3, 5) -> 1*
    f_0(5, 6, 3, 4) -> 1*
    f_0(5, 6, 3, 3) -> 1*
    f_0(5, 6, 3, 2) -> 1*
    f_0(5, 6, 3, 1) -> 1*
    f_0(5, 6, 2, 6) -> 1*
    f_0(5, 6, 2, 5) -> 1*
    f_0(5, 6, 2, 4) -> 1*
    f_0(5, 6, 2, 3) -> 1*
    f_0(5, 6, 2, 2) -> 1*
    f_0(5, 6, 2, 1) -> 1*
    f_0(5, 6, 1, 6) -> 1*
    f_0(5, 6, 1, 5) -> 1*
    f_0(5, 6, 1, 4) -> 1*
    f_0(5, 6, 1, 3) -> 1*
    f_0(5, 6, 1, 2) -> 1*
    f_0(5, 6, 1, 1) -> 1*
    f_0(5, 5, 6, 6) -> 1*
    f_0(5, 5, 6, 5) -> 1*
    f_0(5, 5, 6, 4) -> 1*
    f_0(5, 5, 6, 3) -> 1*
    f_0(5, 5, 6, 2) -> 1*
    f_0(5, 5, 6, 1) -> 1*
    f_0(5, 5, 5, 6) -> 1*
    f_0(5, 5, 5, 5) -> 1*
    f_0(5, 5, 5, 4) -> 1*
    f_0(5, 5, 5, 3) -> 1*
    f_0(5, 5, 5, 2) -> 1*
    f_0(5, 5, 5, 1) -> 1*
    f_0(5, 5, 4, 6) -> 1*
    f_0(5, 5, 4, 5) -> 1*
    f_0(5, 5, 4, 4) -> 1*
    f_0(5, 5, 4, 3) -> 1*
    f_0(5, 5, 4, 2) -> 1*
    f_0(5, 5, 4, 1) -> 1*
    f_0(5, 5, 3, 6) -> 1*
    f_0(5, 5, 3, 5) -> 1*
    f_0(5, 5, 3, 4) -> 1*
    f_0(5, 5, 3, 3) -> 1*
    f_0(5, 5, 3, 2) -> 1*
    f_0(5, 5, 3, 1) -> 1*
    f_0(5, 5, 2, 6) -> 1*
    f_0(5, 5, 2, 5) -> 1*
    f_0(5, 5, 2, 4) -> 1*
    f_0(5, 5, 2, 3) -> 1*
    f_0(5, 5, 2, 2) -> 1*
    f_0(5, 5, 2, 1) -> 1*
    f_0(5, 5, 1, 6) -> 1*
    f_0(5, 5, 1, 5) -> 1*
    f_0(5, 5, 1, 4) -> 1*
    f_0(5, 5, 1, 3) -> 1*
    f_0(5, 5, 1, 2) -> 1*
    f_0(5, 5, 1, 1) -> 1*
    f_0(5, 4, 6, 6) -> 1*
    f_0(5, 4, 6, 5) -> 1*
    f_0(5, 4, 6, 4) -> 1*
    f_0(5, 4, 6, 3) -> 1*
    f_0(5, 4, 6, 2) -> 1*
    f_0(5, 4, 6, 1) -> 1*
    f_0(5, 4, 5, 6) -> 1*
    f_0(5, 4, 5, 5) -> 1*
    f_0(5, 4, 5, 4) -> 1*
    f_0(5, 4, 5, 3) -> 1*
    f_0(5, 4, 5, 2) -> 1*
    f_0(5, 4, 5, 1) -> 1*
    f_0(5, 4, 4, 6) -> 1*
    f_0(5, 4, 4, 5) -> 1*
    f_0(5, 4, 4, 4) -> 1*
    f_0(5, 4, 4, 3) -> 1*
    f_0(5, 4, 4, 2) -> 1*
    f_0(5, 4, 4, 1) -> 1*
    f_0(5, 4, 3, 6) -> 1*
    f_0(5, 4, 3, 5) -> 1*
    f_0(5, 4, 3, 4) -> 1*
    f_0(5, 4, 3, 3) -> 1*
    f_0(5, 4, 3, 2) -> 1*
    f_0(5, 4, 3, 1) -> 1*
    f_0(5, 4, 2, 6) -> 1*
    f_0(5, 4, 2, 5) -> 1*
    f_0(5, 4, 2, 4) -> 1*
    f_0(5, 4, 2, 3) -> 1*
    f_0(5, 4, 2, 2) -> 1*
    f_0(5, 4, 2, 1) -> 1*
    f_0(5, 4, 1, 6) -> 1*
    f_0(5, 4, 1, 5) -> 1*
    f_0(5, 4, 1, 4) -> 1*
    f_0(5, 4, 1, 3) -> 1*
    f_0(5, 4, 1, 2) -> 1*
    f_0(5, 4, 1, 1) -> 1*
    f_0(5, 3, 6, 6) -> 1*
    f_0(5, 3, 6, 5) -> 1*
    f_0(5, 3, 6, 4) -> 1*
    f_0(5, 3, 6, 3) -> 1*
    f_0(5, 3, 6, 2) -> 1*
    f_0(5, 3, 6, 1) -> 1*
    f_0(5, 3, 5, 6) -> 1*
    f_0(5, 3, 5, 5) -> 1*
    f_0(5, 3, 5, 4) -> 1*
    f_0(5, 3, 5, 3) -> 1*
    f_0(5, 3, 5, 2) -> 1*
    f_0(5, 3, 5, 1) -> 1*
    f_0(5, 3, 4, 6) -> 1*
    f_0(5, 3, 4, 5) -> 1*
    f_0(5, 3, 4, 4) -> 1*
    f_0(5, 3, 4, 3) -> 1*
    f_0(5, 3, 4, 2) -> 1*
    f_0(5, 3, 4, 1) -> 1*
    f_0(5, 3, 3, 6) -> 1*
    f_0(5, 3, 3, 5) -> 1*
    f_0(5, 3, 3, 4) -> 1*
    f_0(5, 3, 3, 3) -> 1*
    f_0(5, 3, 3, 2) -> 1*
    f_0(5, 3, 3, 1) -> 1*
    f_0(5, 3, 2, 6) -> 1*
    f_0(5, 3, 2, 5) -> 1*
    f_0(5, 3, 2, 4) -> 1*
    f_0(5, 3, 2, 3) -> 1*
    f_0(5, 3, 2, 2) -> 1*
    f_0(5, 3, 2, 1) -> 1*
    f_0(5, 3, 1, 6) -> 1*
    f_0(5, 3, 1, 5) -> 1*
    f_0(5, 3, 1, 4) -> 1*
    f_0(5, 3, 1, 3) -> 1*
    f_0(5, 3, 1, 2) -> 1*
    f_0(5, 3, 1, 1) -> 1*
    f_0(5, 2, 6, 6) -> 1*
    f_0(5, 2, 6, 5) -> 1*
    f_0(5, 2, 6, 4) -> 1*
    f_0(5, 2, 6, 3) -> 1*
    f_0(5, 2, 6, 2) -> 1*
    f_0(5, 2, 6, 1) -> 1*
    f_0(5, 2, 5, 6) -> 1*
    f_0(5, 2, 5, 5) -> 1*
    f_0(5, 2, 5, 4) -> 1*
    f_0(5, 2, 5, 3) -> 1*
    f_0(5, 2, 5, 2) -> 1*
    f_0(5, 2, 5, 1) -> 1*
    f_0(5, 2, 4, 6) -> 1*
    f_0(5, 2, 4, 5) -> 1*
    f_0(5, 2, 4, 4) -> 1*
    f_0(5, 2, 4, 3) -> 1*
    f_0(5, 2, 4, 2) -> 1*
    f_0(5, 2, 4, 1) -> 1*
    f_0(5, 2, 3, 6) -> 1*
    f_0(5, 2, 3, 5) -> 1*
    f_0(5, 2, 3, 4) -> 1*
    f_0(5, 2, 3, 3) -> 1*
    f_0(5, 2, 3, 2) -> 1*
    f_0(5, 2, 3, 1) -> 1*
    f_0(5, 2, 2, 6) -> 1*
    f_0(5, 2, 2, 5) -> 1*
    f_0(5, 2, 2, 4) -> 1*
    f_0(5, 2, 2, 3) -> 1*
    f_0(5, 2, 2, 2) -> 1*
    f_0(5, 2, 2, 1) -> 1*
    f_0(5, 2, 1, 6) -> 1*
    f_0(5, 2, 1, 5) -> 1*
    f_0(5, 2, 1, 4) -> 1*
    f_0(5, 2, 1, 3) -> 1*
    f_0(5, 2, 1, 2) -> 1*
    f_0(5, 2, 1, 1) -> 1*
    f_0(5, 1, 6, 6) -> 1*
    f_0(5, 1, 6, 5) -> 1*
    f_0(5, 1, 6, 4) -> 1*
    f_0(5, 1, 6, 3) -> 1*
    f_0(5, 1, 6, 2) -> 1*
    f_0(5, 1, 6, 1) -> 1*
    f_0(5, 1, 5, 6) -> 1*
    f_0(5, 1, 5, 5) -> 1*
    f_0(5, 1, 5, 4) -> 1*
    f_0(5, 1, 5, 3) -> 1*
    f_0(5, 1, 5, 2) -> 1*
    f_0(5, 1, 5, 1) -> 1*
    f_0(5, 1, 4, 6) -> 1*
    f_0(5, 1, 4, 5) -> 1*
    f_0(5, 1, 4, 4) -> 1*
    f_0(5, 1, 4, 3) -> 1*
    f_0(5, 1, 4, 2) -> 1*
    f_0(5, 1, 4, 1) -> 1*
    f_0(5, 1, 3, 6) -> 1*
    f_0(5, 1, 3, 5) -> 1*
    f_0(5, 1, 3, 4) -> 1*
    f_0(5, 1, 3, 3) -> 1*
    f_0(5, 1, 3, 2) -> 1*
    f_0(5, 1, 3, 1) -> 1*
    f_0(5, 1, 2, 6) -> 1*
    f_0(5, 1, 2, 5) -> 1*
    f_0(5, 1, 2, 4) -> 1*
    f_0(5, 1, 2, 3) -> 1*
    f_0(5, 1, 2, 2) -> 1*
    f_0(5, 1, 2, 1) -> 1*
    f_0(5, 1, 1, 6) -> 1*
    f_0(5, 1, 1, 5) -> 1*
    f_0(5, 1, 1, 4) -> 1*
    f_0(5, 1, 1, 3) -> 1*
    f_0(5, 1, 1, 2) -> 1*
    f_0(5, 1, 1, 1) -> 1*
    f_0(4, 6, 6, 6) -> 1*
    f_0(4, 6, 6, 5) -> 1*
    f_0(4, 6, 6, 4) -> 1*
    f_0(4, 6, 6, 3) -> 1*
    f_0(4, 6, 6, 2) -> 1*
    f_0(4, 6, 6, 1) -> 1*
    f_0(4, 6, 5, 6) -> 1*
    f_0(4, 6, 5, 5) -> 1*
    f_0(4, 6, 5, 4) -> 1*
    f_0(4, 6, 5, 3) -> 1*
    f_0(4, 6, 5, 2) -> 1*
    f_0(4, 6, 5, 1) -> 1*
    f_0(4, 6, 4, 6) -> 1*
    f_0(4, 6, 4, 5) -> 1*
    f_0(4, 6, 4, 4) -> 1*
    f_0(4, 6, 4, 3) -> 1*
    f_0(4, 6, 4, 2) -> 1*
    f_0(4, 6, 4, 1) -> 1*
    f_0(4, 6, 3, 6) -> 1*
    f_0(4, 6, 3, 5) -> 1*
    f_0(4, 6, 3, 4) -> 1*
    f_0(4, 6, 3, 3) -> 1*
    f_0(4, 6, 3, 2) -> 1*
    f_0(4, 6, 3, 1) -> 1*
    f_0(4, 6, 2, 6) -> 1*
    f_0(4, 6, 2, 5) -> 1*
    f_0(4, 6, 2, 4) -> 1*
    f_0(4, 6, 2, 3) -> 1*
    f_0(4, 6, 2, 2) -> 1*
    f_0(4, 6, 2, 1) -> 1*
    f_0(4, 6, 1, 6) -> 1*
    f_0(4, 6, 1, 5) -> 1*
    f_0(4, 6, 1, 4) -> 1*
    f_0(4, 6, 1, 3) -> 1*
    f_0(4, 6, 1, 2) -> 1*
    f_0(4, 6, 1, 1) -> 1*
    f_0(4, 5, 6, 6) -> 1*
    f_0(4, 5, 6, 5) -> 1*
    f_0(4, 5, 6, 4) -> 1*
    f_0(4, 5, 6, 3) -> 1*
    f_0(4, 5, 6, 2) -> 1*
    f_0(4, 5, 6, 1) -> 1*
    f_0(4, 5, 5, 6) -> 1*
    f_0(4, 5, 5, 5) -> 1*
    f_0(4, 5, 5, 4) -> 1*
    f_0(4, 5, 5, 3) -> 1*
    f_0(4, 5, 5, 2) -> 1*
    f_0(4, 5, 5, 1) -> 1*
    f_0(4, 5, 4, 6) -> 1*
    f_0(4, 5, 4, 5) -> 1*
    f_0(4, 5, 4, 4) -> 1*
    f_0(4, 5, 4, 3) -> 1*
    f_0(4, 5, 4, 2) -> 1*
    f_0(4, 5, 4, 1) -> 1*
    f_0(4, 5, 3, 6) -> 1*
    f_0(4, 5, 3, 5) -> 1*
    f_0(4, 5, 3, 4) -> 1*
    f_0(4, 5, 3, 3) -> 1*
    f_0(4, 5, 3, 2) -> 1*
    f_0(4, 5, 3, 1) -> 1*
    f_0(4, 5, 2, 6) -> 1*
    f_0(4, 5, 2, 5) -> 1*
    f_0(4, 5, 2, 4) -> 1*
    f_0(4, 5, 2, 3) -> 1*
    f_0(4, 5, 2, 2) -> 1*
    f_0(4, 5, 2, 1) -> 1*
    f_0(4, 5, 1, 6) -> 1*
    f_0(4, 5, 1, 5) -> 1*
    f_0(4, 5, 1, 4) -> 1*
    f_0(4, 5, 1, 3) -> 1*
    f_0(4, 5, 1, 2) -> 1*
    f_0(4, 5, 1, 1) -> 1*
    f_0(4, 4, 6, 6) -> 1*
    f_0(4, 4, 6, 5) -> 1*
    f_0(4, 4, 6, 4) -> 1*
    f_0(4, 4, 6, 3) -> 1*
    f_0(4, 4, 6, 2) -> 1*
    f_0(4, 4, 6, 1) -> 1*
    f_0(4, 4, 5, 6) -> 1*
    f_0(4, 4, 5, 5) -> 1*
    f_0(4, 4, 5, 4) -> 1*
    f_0(4, 4, 5, 3) -> 1*
    f_0(4, 4, 5, 2) -> 1*
    f_0(4, 4, 5, 1) -> 1*
    f_0(4, 4, 4, 6) -> 1*
    f_0(4, 4, 4, 5) -> 1*
    f_0(4, 4, 4, 4) -> 1*
    f_0(4, 4, 4, 3) -> 1*
    f_0(4, 4, 4, 2) -> 1*
    f_0(4, 4, 4, 1) -> 1*
    f_0(4, 4, 3, 6) -> 1*
    f_0(4, 4, 3, 5) -> 1*
    f_0(4, 4, 3, 4) -> 1*
    f_0(4, 4, 3, 3) -> 1*
    f_0(4, 4, 3, 2) -> 1*
    f_0(4, 4, 3, 1) -> 1*
    f_0(4, 4, 2, 6) -> 1*
    f_0(4, 4, 2, 5) -> 1*
    f_0(4, 4, 2, 4) -> 1*
    f_0(4, 4, 2, 3) -> 1*
    f_0(4, 4, 2, 2) -> 1*
    f_0(4, 4, 2, 1) -> 1*
    f_0(4, 4, 1, 6) -> 1*
    f_0(4, 4, 1, 5) -> 1*
    f_0(4, 4, 1, 4) -> 1*
    f_0(4, 4, 1, 3) -> 1*
    f_0(4, 4, 1, 2) -> 1*
    f_0(4, 4, 1, 1) -> 1*
    f_0(4, 3, 6, 6) -> 1*
    f_0(4, 3, 6, 5) -> 1*
    f_0(4, 3, 6, 4) -> 1*
    f_0(4, 3, 6, 3) -> 1*
    f_0(4, 3, 6, 2) -> 1*
    f_0(4, 3, 6, 1) -> 1*
    f_0(4, 3, 5, 6) -> 1*
    f_0(4, 3, 5, 5) -> 1*
    f_0(4, 3, 5, 4) -> 1*
    f_0(4, 3, 5, 3) -> 1*
    f_0(4, 3, 5, 2) -> 1*
    f_0(4, 3, 5, 1) -> 1*
    f_0(4, 3, 4, 6) -> 1*
    f_0(4, 3, 4, 5) -> 1*
    f_0(4, 3, 4, 4) -> 1*
    f_0(4, 3, 4, 3) -> 1*
    f_0(4, 3, 4, 2) -> 1*
    f_0(4, 3, 4, 1) -> 1*
    f_0(4, 3, 3, 6) -> 1*
    f_0(4, 3, 3, 5) -> 1*
    f_0(4, 3, 3, 4) -> 1*
    f_0(4, 3, 3, 3) -> 1*
    f_0(4, 3, 3, 2) -> 1*
    f_0(4, 3, 3, 1) -> 1*
    f_0(4, 3, 2, 6) -> 1*
    f_0(4, 3, 2, 5) -> 1*
    f_0(4, 3, 2, 4) -> 1*
    f_0(4, 3, 2, 3) -> 1*
    f_0(4, 3, 2, 2) -> 1*
    f_0(4, 3, 2, 1) -> 1*
    f_0(4, 3, 1, 6) -> 1*
    f_0(4, 3, 1, 5) -> 1*
    f_0(4, 3, 1, 4) -> 1*
    f_0(4, 3, 1, 3) -> 1*
    f_0(4, 3, 1, 2) -> 1*
    f_0(4, 3, 1, 1) -> 1*
    f_0(4, 2, 6, 6) -> 1*
    f_0(4, 2, 6, 5) -> 1*
    f_0(4, 2, 6, 4) -> 1*
    f_0(4, 2, 6, 3) -> 1*
    f_0(4, 2, 6, 2) -> 1*
    f_0(4, 2, 6, 1) -> 1*
    f_0(4, 2, 5, 6) -> 1*
    f_0(4, 2, 5, 5) -> 1*
    f_0(4, 2, 5, 4) -> 1*
    f_0(4, 2, 5, 3) -> 1*
    f_0(4, 2, 5, 2) -> 1*
    f_0(4, 2, 5, 1) -> 1*
    f_0(4, 2, 4, 6) -> 1*
    f_0(4, 2, 4, 5) -> 1*
    f_0(4, 2, 4, 4) -> 1*
    f_0(4, 2, 4, 3) -> 1*
    f_0(4, 2, 4, 2) -> 1*
    f_0(4, 2, 4, 1) -> 1*
    f_0(4, 2, 3, 6) -> 1*
    f_0(4, 2, 3, 5) -> 1*
    f_0(4, 2, 3, 4) -> 1*
    f_0(4, 2, 3, 3) -> 1*
    f_0(4, 2, 3, 2) -> 1*
    f_0(4, 2, 3, 1) -> 1*
    f_0(4, 2, 2, 6) -> 1*
    f_0(4, 2, 2, 5) -> 1*
    f_0(4, 2, 2, 4) -> 1*
    f_0(4, 2, 2, 3) -> 1*
    f_0(4, 2, 2, 2) -> 1*
    f_0(4, 2, 2, 1) -> 1*
    f_0(4, 2, 1, 6) -> 1*
    f_0(4, 2, 1, 5) -> 1*
    f_0(4, 2, 1, 4) -> 1*
    f_0(4, 2, 1, 3) -> 1*
    f_0(4, 2, 1, 2) -> 1*
    f_0(4, 2, 1, 1) -> 1*
    f_0(4, 1, 6, 6) -> 1*
    f_0(4, 1, 6, 5) -> 1*
    f_0(4, 1, 6, 4) -> 1*
    f_0(4, 1, 6, 3) -> 1*
    f_0(4, 1, 6, 2) -> 1*
    f_0(4, 1, 6, 1) -> 1*
    f_0(4, 1, 5, 6) -> 1*
    f_0(4, 1, 5, 5) -> 1*
    f_0(4, 1, 5, 4) -> 1*
    f_0(4, 1, 5, 3) -> 1*
    f_0(4, 1, 5, 2) -> 1*
    f_0(4, 1, 5, 1) -> 1*
    f_0(4, 1, 4, 6) -> 1*
    f_0(4, 1, 4, 5) -> 1*
    f_0(4, 1, 4, 4) -> 1*
    f_0(4, 1, 4, 3) -> 1*
    f_0(4, 1, 4, 2) -> 1*
    f_0(4, 1, 4, 1) -> 1*
    f_0(4, 1, 3, 6) -> 1*
    f_0(4, 1, 3, 5) -> 1*
    f_0(4, 1, 3, 4) -> 1*
    f_0(4, 1, 3, 3) -> 1*
    f_0(4, 1, 3, 2) -> 1*
    f_0(4, 1, 3, 1) -> 1*
    f_0(4, 1, 2, 6) -> 1*
    f_0(4, 1, 2, 5) -> 1*
    f_0(4, 1, 2, 4) -> 1*
    f_0(4, 1, 2, 3) -> 1*
    f_0(4, 1, 2, 2) -> 1*
    f_0(4, 1, 2, 1) -> 1*
    f_0(4, 1, 1, 6) -> 1*
    f_0(4, 1, 1, 5) -> 1*
    f_0(4, 1, 1, 4) -> 1*
    f_0(4, 1, 1, 3) -> 1*
    f_0(4, 1, 1, 2) -> 1*
    f_0(4, 1, 1, 1) -> 1*
    f_0(3, 6, 6, 6) -> 1*
    f_0(3, 6, 6, 5) -> 1*
    f_0(3, 6, 6, 4) -> 1*
    f_0(3, 6, 6, 3) -> 1*
    f_0(3, 6, 6, 2) -> 1*
    f_0(3, 6, 6, 1) -> 1*
    f_0(3, 6, 5, 6) -> 1*
    f_0(3, 6, 5, 5) -> 1*
    f_0(3, 6, 5, 4) -> 1*
    f_0(3, 6, 5, 3) -> 1*
    f_0(3, 6, 5, 2) -> 1*
    f_0(3, 6, 5, 1) -> 1*
    f_0(3, 6, 4, 6) -> 1*
    f_0(3, 6, 4, 5) -> 1*
    f_0(3, 6, 4, 4) -> 1*
    f_0(3, 6, 4, 3) -> 1*
    f_0(3, 6, 4, 2) -> 1*
    f_0(3, 6, 4, 1) -> 1*
    f_0(3, 6, 3, 6) -> 1*
    f_0(3, 6, 3, 5) -> 1*
    f_0(3, 6, 3, 4) -> 1*
    f_0(3, 6, 3, 3) -> 1*
    f_0(3, 6, 3, 2) -> 1*
    f_0(3, 6, 3, 1) -> 1*
    f_0(3, 6, 2, 6) -> 1*
    f_0(3, 6, 2, 5) -> 1*
    f_0(3, 6, 2, 4) -> 1*
    f_0(3, 6, 2, 3) -> 1*
    f_0(3, 6, 2, 2) -> 1*
    f_0(3, 6, 2, 1) -> 1*
    f_0(3, 6, 1, 6) -> 1*
    f_0(3, 6, 1, 5) -> 1*
    f_0(3, 6, 1, 4) -> 1*
    f_0(3, 6, 1, 3) -> 1*
    f_0(3, 6, 1, 2) -> 1*
    f_0(3, 6, 1, 1) -> 1*
    f_0(3, 5, 6, 6) -> 1*
    f_0(3, 5, 6, 5) -> 1*
    f_0(3, 5, 6, 4) -> 1*
    f_0(3, 5, 6, 3) -> 1*
    f_0(3, 5, 6, 2) -> 1*
    f_0(3, 5, 6, 1) -> 1*
    f_0(3, 5, 5, 6) -> 1*
    f_0(3, 5, 5, 5) -> 1*
    f_0(3, 5, 5, 4) -> 1*
    f_0(3, 5, 5, 3) -> 1*
    f_0(3, 5, 5, 2) -> 1*
    f_0(3, 5, 5, 1) -> 1*
    f_0(3, 5, 4, 6) -> 1*
    f_0(3, 5, 4, 5) -> 1*
    f_0(3, 5, 4, 4) -> 1*
    f_0(3, 5, 4, 3) -> 1*
    f_0(3, 5, 4, 2) -> 1*
    f_0(3, 5, 4, 1) -> 1*
    f_0(3, 5, 3, 6) -> 1*
    f_0(3, 5, 3, 5) -> 1*
    f_0(3, 5, 3, 4) -> 1*
    f_0(3, 5, 3, 3) -> 1*
    f_0(3, 5, 3, 2) -> 1*
    f_0(3, 5, 3, 1) -> 1*
    f_0(3, 5, 2, 6) -> 1*
    f_0(3, 5, 2, 5) -> 1*
    f_0(3, 5, 2, 4) -> 1*
    f_0(3, 5, 2, 3) -> 1*
    f_0(3, 5, 2, 2) -> 1*
    f_0(3, 5, 2, 1) -> 1*
    f_0(3, 5, 1, 6) -> 1*
    f_0(3, 5, 1, 5) -> 1*
    f_0(3, 5, 1, 4) -> 1*
    f_0(3, 5, 1, 3) -> 1*
    f_0(3, 5, 1, 2) -> 1*
    f_0(3, 5, 1, 1) -> 1*
    f_0(3, 4, 6, 6) -> 1*
    f_0(3, 4, 6, 5) -> 1*
    f_0(3, 4, 6, 4) -> 1*
    f_0(3, 4, 6, 3) -> 1*
    f_0(3, 4, 6, 2) -> 1*
    f_0(3, 4, 6, 1) -> 1*
    f_0(3, 4, 5, 6) -> 1*
    f_0(3, 4, 5, 5) -> 1*
    f_0(3, 4, 5, 4) -> 1*
    f_0(3, 4, 5, 3) -> 1*
    f_0(3, 4, 5, 2) -> 1*
    f_0(3, 4, 5, 1) -> 1*
    f_0(3, 4, 4, 6) -> 1*
    f_0(3, 4, 4, 5) -> 1*
    f_0(3, 4, 4, 4) -> 1*
    f_0(3, 4, 4, 3) -> 1*
    f_0(3, 4, 4, 2) -> 1*
    f_0(3, 4, 4, 1) -> 1*
    f_0(3, 4, 3, 6) -> 1*
    f_0(3, 4, 3, 5) -> 1*
    f_0(3, 4, 3, 4) -> 1*
    f_0(3, 4, 3, 3) -> 1*
    f_0(3, 4, 3, 2) -> 1*
    f_0(3, 4, 3, 1) -> 1*
    f_0(3, 4, 2, 6) -> 1*
    f_0(3, 4, 2, 5) -> 1*
    f_0(3, 4, 2, 4) -> 1*
    f_0(3, 4, 2, 3) -> 1*
    f_0(3, 4, 2, 2) -> 1*
    f_0(3, 4, 2, 1) -> 1*
    f_0(3, 4, 1, 6) -> 1*
    f_0(3, 4, 1, 5) -> 1*
    f_0(3, 4, 1, 4) -> 1*
    f_0(3, 4, 1, 3) -> 1*
    f_0(3, 4, 1, 2) -> 1*
    f_0(3, 4, 1, 1) -> 1*
    f_0(3, 3, 6, 6) -> 1*
    f_0(3, 3, 6, 5) -> 1*
    f_0(3, 3, 6, 4) -> 1*
    f_0(3, 3, 6, 3) -> 1*
    f_0(3, 3, 6, 2) -> 1*
    f_0(3, 3, 6, 1) -> 1*
    f_0(3, 3, 5, 6) -> 1*
    f_0(3, 3, 5, 5) -> 1*
    f_0(3, 3, 5, 4) -> 1*
    f_0(3, 3, 5, 3) -> 1*
    f_0(3, 3, 5, 2) -> 1*
    f_0(3, 3, 5, 1) -> 1*
    f_0(3, 3, 4, 6) -> 1*
    f_0(3, 3, 4, 5) -> 1*
    f_0(3, 3, 4, 4) -> 1*
    f_0(3, 3, 4, 3) -> 1*
    f_0(3, 3, 4, 2) -> 1*
    f_0(3, 3, 4, 1) -> 1*
    f_0(3, 3, 3, 6) -> 1*
    f_0(3, 3, 3, 5) -> 1*
    f_0(3, 3, 3, 4) -> 1*
    f_0(3, 3, 3, 3) -> 1*
    f_0(3, 3, 3, 2) -> 1*
    f_0(3, 3, 3, 1) -> 1*
    f_0(3, 3, 2, 6) -> 1*
    f_0(3, 3, 2, 5) -> 1*
    f_0(3, 3, 2, 4) -> 1*
    f_0(3, 3, 2, 3) -> 1*
    f_0(3, 3, 2, 2) -> 1*
    f_0(3, 3, 2, 1) -> 1*
    f_0(3, 3, 1, 6) -> 1*
    f_0(3, 3, 1, 5) -> 1*
    f_0(3, 3, 1, 4) -> 1*
    f_0(3, 3, 1, 3) -> 1*
    f_0(3, 3, 1, 2) -> 1*
    f_0(3, 3, 1, 1) -> 1*
    f_0(3, 2, 6, 6) -> 1*
    f_0(3, 2, 6, 5) -> 1*
    f_0(3, 2, 6, 4) -> 1*
    f_0(3, 2, 6, 3) -> 1*
    f_0(3, 2, 6, 2) -> 1*
    f_0(3, 2, 6, 1) -> 1*
    f_0(3, 2, 5, 6) -> 1*
    f_0(3, 2, 5, 5) -> 1*
    f_0(3, 2, 5, 4) -> 1*
    f_0(3, 2, 5, 3) -> 1*
    f_0(3, 2, 5, 2) -> 1*
    f_0(3, 2, 5, 1) -> 1*
    f_0(3, 2, 4, 6) -> 1*
    f_0(3, 2, 4, 5) -> 1*
    f_0(3, 2, 4, 4) -> 1*
    f_0(3, 2, 4, 3) -> 1*
    f_0(3, 2, 4, 2) -> 1*
    f_0(3, 2, 4, 1) -> 1*
    f_0(3, 2, 3, 6) -> 1*
    f_0(3, 2, 3, 5) -> 1*
    f_0(3, 2, 3, 4) -> 1*
    f_0(3, 2, 3, 3) -> 1*
    f_0(3, 2, 3, 2) -> 1*
    f_0(3, 2, 3, 1) -> 1*
    f_0(3, 2, 2, 6) -> 1*
    f_0(3, 2, 2, 5) -> 1*
    f_0(3, 2, 2, 4) -> 1*
    f_0(3, 2, 2, 3) -> 1*
    f_0(3, 2, 2, 2) -> 1*
    f_0(3, 2, 2, 1) -> 1*
    f_0(3, 2, 1, 6) -> 1*
    f_0(3, 2, 1, 5) -> 1*
    f_0(3, 2, 1, 4) -> 1*
    f_0(3, 2, 1, 3) -> 1*
    f_0(3, 2, 1, 2) -> 1*
    f_0(3, 2, 1, 1) -> 1*
    f_0(3, 1, 6, 6) -> 1*
    f_0(3, 1, 6, 5) -> 1*
    f_0(3, 1, 6, 4) -> 1*
    f_0(3, 1, 6, 3) -> 1*
    f_0(3, 1, 6, 2) -> 1*
    f_0(3, 1, 6, 1) -> 1*
    f_0(3, 1, 5, 6) -> 1*
    f_0(3, 1, 5, 5) -> 1*
    f_0(3, 1, 5, 4) -> 1*
    f_0(3, 1, 5, 3) -> 1*
    f_0(3, 1, 5, 2) -> 1*
    f_0(3, 1, 5, 1) -> 1*
    f_0(3, 1, 4, 6) -> 1*
    f_0(3, 1, 4, 5) -> 1*
    f_0(3, 1, 4, 4) -> 1*
    f_0(3, 1, 4, 3) -> 1*
    f_0(3, 1, 4, 2) -> 1*
    f_0(3, 1, 4, 1) -> 1*
    f_0(3, 1, 3, 6) -> 1*
    f_0(3, 1, 3, 5) -> 1*
    f_0(3, 1, 3, 4) -> 1*
    f_0(3, 1, 3, 3) -> 1*
    f_0(3, 1, 3, 2) -> 1*
    f_0(3, 1, 3, 1) -> 1*
    f_0(3, 1, 2, 6) -> 1*
    f_0(3, 1, 2, 5) -> 1*
    f_0(3, 1, 2, 4) -> 1*
    f_0(3, 1, 2, 3) -> 1*
    f_0(3, 1, 2, 2) -> 1*
    f_0(3, 1, 2, 1) -> 1*
    f_0(3, 1, 1, 6) -> 1*
    f_0(3, 1, 1, 5) -> 1*
    f_0(3, 1, 1, 4) -> 1*
    f_0(3, 1, 1, 3) -> 1*
    f_0(3, 1, 1, 2) -> 1*
    f_0(3, 1, 1, 1) -> 1*
    f_0(2, 6, 6, 6) -> 1*
    f_0(2, 6, 6, 5) -> 1*
    f_0(2, 6, 6, 4) -> 1*
    f_0(2, 6, 6, 3) -> 1*
    f_0(2, 6, 6, 2) -> 1*
    f_0(2, 6, 6, 1) -> 1*
    f_0(2, 6, 5, 6) -> 1*
    f_0(2, 6, 5, 5) -> 1*
    f_0(2, 6, 5, 4) -> 1*
    f_0(2, 6, 5, 3) -> 1*
    f_0(2, 6, 5, 2) -> 1*
    f_0(2, 6, 5, 1) -> 1*
    f_0(2, 6, 4, 6) -> 1*
    f_0(2, 6, 4, 5) -> 1*
    f_0(2, 6, 4, 4) -> 1*
    f_0(2, 6, 4, 3) -> 1*
    f_0(2, 6, 4, 2) -> 1*
    f_0(2, 6, 4, 1) -> 1*
    f_0(2, 6, 3, 6) -> 1*
    f_0(2, 6, 3, 5) -> 1*
    f_0(2, 6, 3, 4) -> 1*
    f_0(2, 6, 3, 3) -> 1*
    f_0(2, 6, 3, 2) -> 1*
    f_0(2, 6, 3, 1) -> 1*
    f_0(2, 6, 2, 6) -> 1*
    f_0(2, 6, 2, 5) -> 1*
    f_0(2, 6, 2, 4) -> 1*
    f_0(2, 6, 2, 3) -> 1*
    f_0(2, 6, 2, 2) -> 1*
    f_0(2, 6, 2, 1) -> 1*
    f_0(2, 6, 1, 6) -> 1*
    f_0(2, 6, 1, 5) -> 1*
    f_0(2, 6, 1, 4) -> 1*
    f_0(2, 6, 1, 3) -> 1*
    f_0(2, 6, 1, 2) -> 1*
    f_0(2, 6, 1, 1) -> 1*
    f_0(2, 5, 6, 6) -> 1*
    f_0(2, 5, 6, 5) -> 1*
    f_0(2, 5, 6, 4) -> 1*
    f_0(2, 5, 6, 3) -> 1*
    f_0(2, 5, 6, 2) -> 1*
    f_0(2, 5, 6, 1) -> 1*
    f_0(2, 5, 5, 6) -> 1*
    f_0(2, 5, 5, 5) -> 1*
    f_0(2, 5, 5, 4) -> 1*
    f_0(2, 5, 5, 3) -> 1*
    f_0(2, 5, 5, 2) -> 1*
    f_0(2, 5, 5, 1) -> 1*
    f_0(2, 5, 4, 6) -> 1*
    f_0(2, 5, 4, 5) -> 1*
    f_0(2, 5, 4, 4) -> 1*
    f_0(2, 5, 4, 3) -> 1*
    f_0(2, 5, 4, 2) -> 1*
    f_0(2, 5, 4, 1) -> 1*
    f_0(2, 5, 3, 6) -> 1*
    f_0(2, 5, 3, 5) -> 1*
    f_0(2, 5, 3, 4) -> 1*
    f_0(2, 5, 3, 3) -> 1*
    f_0(2, 5, 3, 2) -> 1*
    f_0(2, 5, 3, 1) -> 1*
    f_0(2, 5, 2, 6) -> 1*
    f_0(2, 5, 2, 5) -> 1*
    f_0(2, 5, 2, 4) -> 1*
    f_0(2, 5, 2, 3) -> 1*
    f_0(2, 5, 2, 2) -> 1*
    f_0(2, 5, 2, 1) -> 1*
    f_0(2, 5, 1, 6) -> 1*
    f_0(2, 5, 1, 5) -> 1*
    f_0(2, 5, 1, 4) -> 1*
    f_0(2, 5, 1, 3) -> 1*
    f_0(2, 5, 1, 2) -> 1*
    f_0(2, 5, 1, 1) -> 1*
    f_0(2, 4, 6, 6) -> 1*
    f_0(2, 4, 6, 5) -> 1*
    f_0(2, 4, 6, 4) -> 1*
    f_0(2, 4, 6, 3) -> 1*
    f_0(2, 4, 6, 2) -> 1*
    f_0(2, 4, 6, 1) -> 1*
    f_0(2, 4, 5, 6) -> 1*
    f_0(2, 4, 5, 5) -> 1*
    f_0(2, 4, 5, 4) -> 1*
    f_0(2, 4, 5, 3) -> 1*
    f_0(2, 4, 5, 2) -> 1*
    f_0(2, 4, 5, 1) -> 1*
    f_0(2, 4, 4, 6) -> 1*
    f_0(2, 4, 4, 5) -> 1*
    f_0(2, 4, 4, 4) -> 1*
    f_0(2, 4, 4, 3) -> 1*
    f_0(2, 4, 4, 2) -> 1*
    f_0(2, 4, 4, 1) -> 1*
    f_0(2, 4, 3, 6) -> 1*
    f_0(2, 4, 3, 5) -> 1*
    f_0(2, 4, 3, 4) -> 1*
    f_0(2, 4, 3, 3) -> 1*
    f_0(2, 4, 3, 2) -> 1*
    f_0(2, 4, 3, 1) -> 1*
    f_0(2, 4, 2, 6) -> 1*
    f_0(2, 4, 2, 5) -> 1*
    f_0(2, 4, 2, 4) -> 1*
    f_0(2, 4, 2, 3) -> 1*
    f_0(2, 4, 2, 2) -> 1*
    f_0(2, 4, 2, 1) -> 1*
    f_0(2, 4, 1, 6) -> 1*
    f_0(2, 4, 1, 5) -> 1*
    f_0(2, 4, 1, 4) -> 1*
    f_0(2, 4, 1, 3) -> 1*
    f_0(2, 4, 1, 2) -> 1*
    f_0(2, 4, 1, 1) -> 1*
    f_0(2, 3, 6, 6) -> 1*
    f_0(2, 3, 6, 5) -> 1*
    f_0(2, 3, 6, 4) -> 1*
    f_0(2, 3, 6, 3) -> 1*
    f_0(2, 3, 6, 2) -> 1*
    f_0(2, 3, 6, 1) -> 1*
    f_0(2, 3, 5, 6) -> 1*
    f_0(2, 3, 5, 5) -> 1*
    f_0(2, 3, 5, 4) -> 1*
    f_0(2, 3, 5, 3) -> 1*
    f_0(2, 3, 5, 2) -> 1*
    f_0(2, 3, 5, 1) -> 1*
    f_0(2, 3, 4, 6) -> 1*
    f_0(2, 3, 4, 5) -> 1*
    f_0(2, 3, 4, 4) -> 1*
    f_0(2, 3, 4, 3) -> 1*
    f_0(2, 3, 4, 2) -> 1*
    f_0(2, 3, 4, 1) -> 1*
    f_0(2, 3, 3, 6) -> 1*
    f_0(2, 3, 3, 5) -> 1*
    f_0(2, 3, 3, 4) -> 1*
    f_0(2, 3, 3, 3) -> 1*
    f_0(2, 3, 3, 2) -> 1*
    f_0(2, 3, 3, 1) -> 1*
    f_0(2, 3, 2, 6) -> 1*
    f_0(2, 3, 2, 5) -> 1*
    f_0(2, 3, 2, 4) -> 1*
    f_0(2, 3, 2, 3) -> 1*
    f_0(2, 3, 2, 2) -> 1*
    f_0(2, 3, 2, 1) -> 1*
    f_0(2, 3, 1, 6) -> 1*
    f_0(2, 3, 1, 5) -> 1*
    f_0(2, 3, 1, 4) -> 1*
    f_0(2, 3, 1, 3) -> 1*
    f_0(2, 3, 1, 2) -> 1*
    f_0(2, 3, 1, 1) -> 1*
    f_0(2, 2, 6, 6) -> 1*
    f_0(2, 2, 6, 5) -> 1*
    f_0(2, 2, 6, 4) -> 1*
    f_0(2, 2, 6, 3) -> 1*
    f_0(2, 2, 6, 2) -> 1*
    f_0(2, 2, 6, 1) -> 1*
    f_0(2, 2, 5, 6) -> 1*
    f_0(2, 2, 5, 5) -> 1*
    f_0(2, 2, 5, 4) -> 1*
    f_0(2, 2, 5, 3) -> 1*
    f_0(2, 2, 5, 2) -> 1*
    f_0(2, 2, 5, 1) -> 1*
    f_0(2, 2, 4, 6) -> 1*
    f_0(2, 2, 4, 5) -> 1*
    f_0(2, 2, 4, 4) -> 1*
    f_0(2, 2, 4, 3) -> 1*
    f_0(2, 2, 4, 2) -> 1*
    f_0(2, 2, 4, 1) -> 1*
    f_0(2, 2, 3, 6) -> 1*
    f_0(2, 2, 3, 5) -> 1*
    f_0(2, 2, 3, 4) -> 1*
    f_0(2, 2, 3, 3) -> 1*
    f_0(2, 2, 3, 2) -> 1*
    f_0(2, 2, 3, 1) -> 1*
    f_0(2, 2, 2, 6) -> 1*
    f_0(2, 2, 2, 5) -> 1*
    f_0(2, 2, 2, 4) -> 1*
    f_0(2, 2, 2, 3) -> 1*
    f_0(2, 2, 2, 2) -> 1*
    f_0(2, 2, 2, 1) -> 1*
    f_0(2, 2, 1, 6) -> 1*
    f_0(2, 2, 1, 5) -> 1*
    f_0(2, 2, 1, 4) -> 1*
    f_0(2, 2, 1, 3) -> 1*
    f_0(2, 2, 1, 2) -> 1*
    f_0(2, 2, 1, 1) -> 1*
    f_0(2, 1, 6, 6) -> 1*
    f_0(2, 1, 6, 5) -> 1*
    f_0(2, 1, 6, 4) -> 1*
    f_0(2, 1, 6, 3) -> 1*
    f_0(2, 1, 6, 2) -> 1*
    f_0(2, 1, 6, 1) -> 1*
    f_0(2, 1, 5, 6) -> 1*
    f_0(2, 1, 5, 5) -> 1*
    f_0(2, 1, 5, 4) -> 1*
    f_0(2, 1, 5, 3) -> 1*
    f_0(2, 1, 5, 2) -> 1*
    f_0(2, 1, 5, 1) -> 1*
    f_0(2, 1, 4, 6) -> 1*
    f_0(2, 1, 4, 5) -> 1*
    f_0(2, 1, 4, 4) -> 1*
    f_0(2, 1, 4, 3) -> 1*
    f_0(2, 1, 4, 2) -> 1*
    f_0(2, 1, 4, 1) -> 1*
    f_0(2, 1, 3, 6) -> 1*
    f_0(2, 1, 3, 5) -> 1*
    f_0(2, 1, 3, 4) -> 1*
    f_0(2, 1, 3, 3) -> 1*
    f_0(2, 1, 3, 2) -> 1*
    f_0(2, 1, 3, 1) -> 1*
    f_0(2, 1, 2, 6) -> 1*
    f_0(2, 1, 2, 5) -> 1*
    f_0(2, 1, 2, 4) -> 1*
    f_0(2, 1, 2, 3) -> 1*
    f_0(2, 1, 2, 2) -> 1*
    f_0(2, 1, 2, 1) -> 1*
    f_0(2, 1, 1, 6) -> 1*
    f_0(2, 1, 1, 5) -> 1*
    f_0(2, 1, 1, 4) -> 1*
    f_0(2, 1, 1, 3) -> 1*
    f_0(2, 1, 1, 2) -> 1*
    f_0(2, 1, 1, 1) -> 1*
    f_0(1, 6, 6, 6) -> 1*
    f_0(1, 6, 6, 5) -> 1*
    f_0(1, 6, 6, 4) -> 1*
    f_0(1, 6, 6, 3) -> 1*
    f_0(1, 6, 6, 2) -> 1*
    f_0(1, 6, 6, 1) -> 1*
    f_0(1, 6, 5, 6) -> 1*
    f_0(1, 6, 5, 5) -> 1*
    f_0(1, 6, 5, 4) -> 1*
    f_0(1, 6, 5, 3) -> 1*
    f_0(1, 6, 5, 2) -> 1*
    f_0(1, 6, 5, 1) -> 1*
    f_0(1, 6, 4, 6) -> 1*
    f_0(1, 6, 4, 5) -> 1*
    f_0(1, 6, 4, 4) -> 1*
    f_0(1, 6, 4, 3) -> 1*
    f_0(1, 6, 4, 2) -> 1*
    f_0(1, 6, 4, 1) -> 1*
    f_0(1, 6, 3, 6) -> 1*
    f_0(1, 6, 3, 5) -> 1*
    f_0(1, 6, 3, 4) -> 1*
    f_0(1, 6, 3, 3) -> 1*
    f_0(1, 6, 3, 2) -> 1*
    f_0(1, 6, 3, 1) -> 1*
    f_0(1, 6, 2, 6) -> 1*
    f_0(1, 6, 2, 5) -> 1*
    f_0(1, 6, 2, 4) -> 1*
    f_0(1, 6, 2, 3) -> 1*
    f_0(1, 6, 2, 2) -> 1*
    f_0(1, 6, 2, 1) -> 1*
    f_0(1, 6, 1, 6) -> 1*
    f_0(1, 6, 1, 5) -> 1*
    f_0(1, 6, 1, 4) -> 1*
    f_0(1, 6, 1, 3) -> 1*
    f_0(1, 6, 1, 2) -> 1*
    f_0(1, 6, 1, 1) -> 1*
    f_0(1, 5, 6, 6) -> 1*
    f_0(1, 5, 6, 5) -> 1*
    f_0(1, 5, 6, 4) -> 1*
    f_0(1, 5, 6, 3) -> 1*
    f_0(1, 5, 6, 2) -> 1*
    f_0(1, 5, 6, 1) -> 1*
    f_0(1, 5, 5, 6) -> 1*
    f_0(1, 5, 5, 5) -> 1*
    f_0(1, 5, 5, 4) -> 1*
    f_0(1, 5, 5, 3) -> 1*
    f_0(1, 5, 5, 2) -> 1*
    f_0(1, 5, 5, 1) -> 1*
    f_0(1, 5, 4, 6) -> 1*
    f_0(1, 5, 4, 5) -> 1*
    f_0(1, 5, 4, 4) -> 1*
    f_0(1, 5, 4, 3) -> 1*
    f_0(1, 5, 4, 2) -> 1*
    f_0(1, 5, 4, 1) -> 1*
    f_0(1, 5, 3, 6) -> 1*
    f_0(1, 5, 3, 5) -> 1*
    f_0(1, 5, 3, 4) -> 1*
    f_0(1, 5, 3, 3) -> 1*
    f_0(1, 5, 3, 2) -> 1*
    f_0(1, 5, 3, 1) -> 1*
    f_0(1, 5, 2, 6) -> 1*
    f_0(1, 5, 2, 5) -> 1*
    f_0(1, 5, 2, 4) -> 1*
    f_0(1, 5, 2, 3) -> 1*
    f_0(1, 5, 2, 2) -> 1*
    f_0(1, 5, 2, 1) -> 1*
    f_0(1, 5, 1, 6) -> 1*
    f_0(1, 5, 1, 5) -> 1*
    f_0(1, 5, 1, 4) -> 1*
    f_0(1, 5, 1, 3) -> 1*
    f_0(1, 5, 1, 2) -> 1*
    f_0(1, 5, 1, 1) -> 1*
    f_0(1, 4, 6, 6) -> 1*
    f_0(1, 4, 6, 5) -> 1*
    f_0(1, 4, 6, 4) -> 1*
    f_0(1, 4, 6, 3) -> 1*
    f_0(1, 4, 6, 2) -> 1*
    f_0(1, 4, 6, 1) -> 1*
    f_0(1, 4, 5, 6) -> 1*
    f_0(1, 4, 5, 5) -> 1*
    f_0(1, 4, 5, 4) -> 1*
    f_0(1, 4, 5, 3) -> 1*
    f_0(1, 4, 5, 2) -> 1*
    f_0(1, 4, 5, 1) -> 1*
    f_0(1, 4, 4, 6) -> 1*
    f_0(1, 4, 4, 5) -> 1*
    f_0(1, 4, 4, 4) -> 1*
    f_0(1, 4, 4, 3) -> 1*
    f_0(1, 4, 4, 2) -> 1*
    f_0(1, 4, 4, 1) -> 1*
    f_0(1, 4, 3, 6) -> 1*
    f_0(1, 4, 3, 5) -> 1*
    f_0(1, 4, 3, 4) -> 1*
    f_0(1, 4, 3, 3) -> 1*
    f_0(1, 4, 3, 2) -> 1*
    f_0(1, 4, 3, 1) -> 1*
    f_0(1, 4, 2, 6) -> 1*
    f_0(1, 4, 2, 5) -> 1*
    f_0(1, 4, 2, 4) -> 1*
    f_0(1, 4, 2, 3) -> 1*
    f_0(1, 4, 2, 2) -> 1*
    f_0(1, 4, 2, 1) -> 1*
    f_0(1, 4, 1, 6) -> 1*
    f_0(1, 4, 1, 5) -> 1*
    f_0(1, 4, 1, 4) -> 1*
    f_0(1, 4, 1, 3) -> 1*
    f_0(1, 4, 1, 2) -> 1*
    f_0(1, 4, 1, 1) -> 1*
    f_0(1, 3, 6, 6) -> 1*
    f_0(1, 3, 6, 5) -> 1*
    f_0(1, 3, 6, 4) -> 1*
    f_0(1, 3, 6, 3) -> 1*
    f_0(1, 3, 6, 2) -> 1*
    f_0(1, 3, 6, 1) -> 1*
    f_0(1, 3, 5, 6) -> 1*
    f_0(1, 3, 5, 5) -> 1*
    f_0(1, 3, 5, 4) -> 1*
    f_0(1, 3, 5, 3) -> 1*
    f_0(1, 3, 5, 2) -> 1*
    f_0(1, 3, 5, 1) -> 1*
    f_0(1, 3, 4, 6) -> 1*
    f_0(1, 3, 4, 5) -> 1*
    f_0(1, 3, 4, 4) -> 1*
    f_0(1, 3, 4, 3) -> 1*
    f_0(1, 3, 4, 2) -> 1*
    f_0(1, 3, 4, 1) -> 1*
    f_0(1, 3, 3, 6) -> 1*
    f_0(1, 3, 3, 5) -> 1*
    f_0(1, 3, 3, 4) -> 1*
    f_0(1, 3, 3, 3) -> 1*
    f_0(1, 3, 3, 2) -> 1*
    f_0(1, 3, 3, 1) -> 1*
    f_0(1, 3, 2, 6) -> 1*
    f_0(1, 3, 2, 5) -> 1*
    f_0(1, 3, 2, 4) -> 1*
    f_0(1, 3, 2, 3) -> 1*
    f_0(1, 3, 2, 2) -> 1*
    f_0(1, 3, 2, 1) -> 1*
    f_0(1, 3, 1, 6) -> 1*
    f_0(1, 3, 1, 5) -> 1*
    f_0(1, 3, 1, 4) -> 1*
    f_0(1, 3, 1, 3) -> 1*
    f_0(1, 3, 1, 2) -> 1*
    f_0(1, 3, 1, 1) -> 1*
    f_0(1, 2, 6, 6) -> 1*
    f_0(1, 2, 6, 5) -> 1*
    f_0(1, 2, 6, 4) -> 1*
    f_0(1, 2, 6, 3) -> 1*
    f_0(1, 2, 6, 2) -> 1*
    f_0(1, 2, 6, 1) -> 1*
    f_0(1, 2, 5, 6) -> 1*
    f_0(1, 2, 5, 5) -> 1*
    f_0(1, 2, 5, 4) -> 1*
    f_0(1, 2, 5, 3) -> 1*
    f_0(1, 2, 5, 2) -> 1*
    f_0(1, 2, 5, 1) -> 1*
    f_0(1, 2, 4, 6) -> 1*
    f_0(1, 2, 4, 5) -> 1*
    f_0(1, 2, 4, 4) -> 1*
    f_0(1, 2, 4, 3) -> 1*
    f_0(1, 2, 4, 2) -> 1*
    f_0(1, 2, 4, 1) -> 1*
    f_0(1, 2, 3, 6) -> 1*
    f_0(1, 2, 3, 5) -> 1*
    f_0(1, 2, 3, 4) -> 1*
    f_0(1, 2, 3, 3) -> 1*
    f_0(1, 2, 3, 2) -> 1*
    f_0(1, 2, 3, 1) -> 1*
    f_0(1, 2, 2, 6) -> 1*
    f_0(1, 2, 2, 5) -> 1*
    f_0(1, 2, 2, 4) -> 1*
    f_0(1, 2, 2, 3) -> 1*
    f_0(1, 2, 2, 2) -> 1*
    f_0(1, 2, 2, 1) -> 1*
    f_0(1, 2, 1, 6) -> 1*
    f_0(1, 2, 1, 5) -> 1*
    f_0(1, 2, 1, 4) -> 1*
    f_0(1, 2, 1, 3) -> 1*
    f_0(1, 2, 1, 2) -> 1*
    f_0(1, 2, 1, 1) -> 1*
    f_0(1, 1, 6, 6) -> 1*
    f_0(1, 1, 6, 5) -> 1*
    f_0(1, 1, 6, 4) -> 1*
    f_0(1, 1, 6, 3) -> 1*
    f_0(1, 1, 6, 2) -> 1*
    f_0(1, 1, 6, 1) -> 1*
    f_0(1, 1, 5, 6) -> 1*
    f_0(1, 1, 5, 5) -> 1*
    f_0(1, 1, 5, 4) -> 1*
    f_0(1, 1, 5, 3) -> 1*
    f_0(1, 1, 5, 2) -> 1*
    f_0(1, 1, 5, 1) -> 1*
    f_0(1, 1, 4, 6) -> 1*
    f_0(1, 1, 4, 5) -> 1*
    f_0(1, 1, 4, 4) -> 1*
    f_0(1, 1, 4, 3) -> 1*
    f_0(1, 1, 4, 2) -> 1*
    f_0(1, 1, 4, 1) -> 1*
    f_0(1, 1, 3, 6) -> 1*
    f_0(1, 1, 3, 5) -> 1*
    f_0(1, 1, 3, 4) -> 1*
    f_0(1, 1, 3, 3) -> 1*
    f_0(1, 1, 3, 2) -> 1*
    f_0(1, 1, 3, 1) -> 1*
    f_0(1, 1, 2, 6) -> 1*
    f_0(1, 1, 2, 5) -> 1*
    f_0(1, 1, 2, 4) -> 1*
    f_0(1, 1, 2, 3) -> 1*
    f_0(1, 1, 2, 2) -> 1*
    f_0(1, 1, 2, 1) -> 1*
    f_0(1, 1, 1, 6) -> 1*
    f_0(1, 1, 1, 5) -> 1*
    f_0(1, 1, 1, 4) -> 1*
    f_0(1, 1, 1, 3) -> 1*
    f_0(1, 1, 1, 2) -> 1*
    f_0(1, 1, 1, 1) -> 1*
   }
  Strict:
   {}
  Qed