YES
Time: 0.251405
TRS:
 {    g1(x, x, y, a()) -> h(x, y),
      g1(y, x, x, a()) -> h(x, y),
    f(x, y, w, w, a()) -> g1(x, x, y, w),
  f(x, y, w, a(), a()) -> g1(y, x, x, w),
    f(x, y, a(), w, w) -> g2(y, y, x, w),
  f(x, y, a(), a(), w) -> g2(x, y, y, w),
      g2(x, y, y, a()) -> h(x, y),
      g2(y, y, x, a()) -> h(x, y),
               h(x, x) -> x}
 BOUND:
  Bound: top(-raise)-bounded by 2
  Automaton:
   {
             h_2(3, 3) -> 1*
             h_2(3, 2) -> 1*
             h_2(3, 1) -> 1*
             h_2(2, 3) -> 1*
             h_2(2, 2) -> 1*
             h_2(2, 1) -> 1*
             h_2(1, 3) -> 1*
             h_2(1, 2) -> 1*
             h_2(1, 1) -> 1*
             h_1(3, 3) -> 1*
             h_1(3, 2) -> 1*
             h_1(3, 1) -> 1*
             h_1(2, 3) -> 1*
             h_1(2, 2) -> 1*
             h_1(2, 1) -> 1*
             h_1(1, 3) -> 1*
             h_1(1, 2) -> 1*
             h_1(1, 1) -> 1*
             h_0(3, 3) -> 1*
             h_0(3, 2) -> 1*
             h_0(3, 1) -> 1*
             h_0(2, 3) -> 1*
             h_0(2, 2) -> 1*
             h_0(2, 1) -> 1*
             h_0(1, 3) -> 1*
             h_0(1, 2) -> 1*
             h_0(1, 1) -> 1*
      g2_1(3, 3, 3, 3) -> 1*
      g2_1(3, 3, 3, 2) -> 1*
      g2_1(3, 3, 3, 1) -> 1*
      g2_1(3, 3, 2, 3) -> 1*
      g2_1(3, 3, 2, 2) -> 1*
      g2_1(3, 3, 2, 1) -> 1*
      g2_1(3, 3, 1, 3) -> 1*
      g2_1(3, 3, 1, 2) -> 1*
      g2_1(3, 3, 1, 1) -> 1*
      g2_1(3, 2, 3, 3) -> 1*
      g2_1(3, 2, 3, 2) -> 1*
      g2_1(3, 2, 3, 1) -> 1*
      g2_1(3, 2, 2, 3) -> 1*
      g2_1(3, 2, 2, 2) -> 1*
      g2_1(3, 2, 2, 1) -> 1*
      g2_1(3, 2, 1, 3) -> 1*
      g2_1(3, 2, 1, 2) -> 1*
      g2_1(3, 2, 1, 1) -> 1*
      g2_1(3, 1, 3, 3) -> 1*
      g2_1(3, 1, 3, 2) -> 1*
      g2_1(3, 1, 3, 1) -> 1*
      g2_1(3, 1, 2, 3) -> 1*
      g2_1(3, 1, 2, 2) -> 1*
      g2_1(3, 1, 2, 1) -> 1*
      g2_1(3, 1, 1, 3) -> 1*
      g2_1(3, 1, 1, 2) -> 1*
      g2_1(3, 1, 1, 1) -> 1*
      g2_1(2, 3, 3, 3) -> 1*
      g2_1(2, 3, 3, 2) -> 1*
      g2_1(2, 3, 3, 1) -> 1*
      g2_1(2, 3, 2, 3) -> 1*
      g2_1(2, 3, 2, 2) -> 1*
      g2_1(2, 3, 2, 1) -> 1*
      g2_1(2, 3, 1, 3) -> 1*
      g2_1(2, 3, 1, 2) -> 1*
      g2_1(2, 3, 1, 1) -> 1*
      g2_1(2, 2, 3, 3) -> 1*
      g2_1(2, 2, 3, 2) -> 1*
      g2_1(2, 2, 3, 1) -> 1*
      g2_1(2, 2, 2, 3) -> 1*
      g2_1(2, 2, 2, 2) -> 1*
      g2_1(2, 2, 2, 1) -> 1*
      g2_1(2, 2, 1, 3) -> 1*
      g2_1(2, 2, 1, 2) -> 1*
      g2_1(2, 2, 1, 1) -> 1*
      g2_1(2, 1, 3, 3) -> 1*
      g2_1(2, 1, 3, 2) -> 1*
      g2_1(2, 1, 3, 1) -> 1*
      g2_1(2, 1, 2, 3) -> 1*
      g2_1(2, 1, 2, 2) -> 1*
      g2_1(2, 1, 2, 1) -> 1*
      g2_1(2, 1, 1, 3) -> 1*
      g2_1(2, 1, 1, 2) -> 1*
      g2_1(2, 1, 1, 1) -> 1*
      g2_1(1, 3, 3, 3) -> 1*
      g2_1(1, 3, 3, 2) -> 1*
      g2_1(1, 3, 3, 1) -> 1*
      g2_1(1, 3, 2, 3) -> 1*
      g2_1(1, 3, 2, 2) -> 1*
      g2_1(1, 3, 2, 1) -> 1*
      g2_1(1, 3, 1, 3) -> 1*
      g2_1(1, 3, 1, 2) -> 1*
      g2_1(1, 3, 1, 1) -> 1*
      g2_1(1, 2, 3, 3) -> 1*
      g2_1(1, 2, 3, 2) -> 1*
      g2_1(1, 2, 3, 1) -> 1*
      g2_1(1, 2, 2, 3) -> 1*
      g2_1(1, 2, 2, 2) -> 1*
      g2_1(1, 2, 2, 1) -> 1*
      g2_1(1, 2, 1, 3) -> 1*
      g2_1(1, 2, 1, 2) -> 1*
      g2_1(1, 2, 1, 1) -> 1*
      g2_1(1, 1, 3, 3) -> 1*
      g2_1(1, 1, 3, 2) -> 1*
      g2_1(1, 1, 3, 1) -> 1*
      g2_1(1, 1, 2, 3) -> 1*
      g2_1(1, 1, 2, 2) -> 1*
      g2_1(1, 1, 2, 1) -> 1*
      g2_1(1, 1, 1, 3) -> 1*
      g2_1(1, 1, 1, 2) -> 1*
      g2_1(1, 1, 1, 1) -> 1*
      g2_0(3, 3, 3, 3) -> 1*
      g2_0(3, 3, 3, 2) -> 1*
      g2_0(3, 3, 3, 1) -> 1*
      g2_0(3, 3, 2, 3) -> 1*
      g2_0(3, 3, 2, 2) -> 1*
      g2_0(3, 3, 2, 1) -> 1*
      g2_0(3, 3, 1, 3) -> 1*
      g2_0(3, 3, 1, 2) -> 1*
      g2_0(3, 3, 1, 1) -> 1*
      g2_0(3, 2, 3, 3) -> 1*
      g2_0(3, 2, 3, 2) -> 1*
      g2_0(3, 2, 3, 1) -> 1*
      g2_0(3, 2, 2, 3) -> 1*
      g2_0(3, 2, 2, 2) -> 1*
      g2_0(3, 2, 2, 1) -> 1*
      g2_0(3, 2, 1, 3) -> 1*
      g2_0(3, 2, 1, 2) -> 1*
      g2_0(3, 2, 1, 1) -> 1*
      g2_0(3, 1, 3, 3) -> 1*
      g2_0(3, 1, 3, 2) -> 1*
      g2_0(3, 1, 3, 1) -> 1*
      g2_0(3, 1, 2, 3) -> 1*
      g2_0(3, 1, 2, 2) -> 1*
      g2_0(3, 1, 2, 1) -> 1*
      g2_0(3, 1, 1, 3) -> 1*
      g2_0(3, 1, 1, 2) -> 1*
      g2_0(3, 1, 1, 1) -> 1*
      g2_0(2, 3, 3, 3) -> 1*
      g2_0(2, 3, 3, 2) -> 1*
      g2_0(2, 3, 3, 1) -> 1*
      g2_0(2, 3, 2, 3) -> 1*
      g2_0(2, 3, 2, 2) -> 1*
      g2_0(2, 3, 2, 1) -> 1*
      g2_0(2, 3, 1, 3) -> 1*
      g2_0(2, 3, 1, 2) -> 1*
      g2_0(2, 3, 1, 1) -> 1*
      g2_0(2, 2, 3, 3) -> 1*
      g2_0(2, 2, 3, 2) -> 1*
      g2_0(2, 2, 3, 1) -> 1*
      g2_0(2, 2, 2, 3) -> 1*
      g2_0(2, 2, 2, 2) -> 1*
      g2_0(2, 2, 2, 1) -> 1*
      g2_0(2, 2, 1, 3) -> 1*
      g2_0(2, 2, 1, 2) -> 1*
      g2_0(2, 2, 1, 1) -> 1*
      g2_0(2, 1, 3, 3) -> 1*
      g2_0(2, 1, 3, 2) -> 1*
      g2_0(2, 1, 3, 1) -> 1*
      g2_0(2, 1, 2, 3) -> 1*
      g2_0(2, 1, 2, 2) -> 1*
      g2_0(2, 1, 2, 1) -> 1*
      g2_0(2, 1, 1, 3) -> 1*
      g2_0(2, 1, 1, 2) -> 1*
      g2_0(2, 1, 1, 1) -> 1*
      g2_0(1, 3, 3, 3) -> 1*
      g2_0(1, 3, 3, 2) -> 1*
      g2_0(1, 3, 3, 1) -> 1*
      g2_0(1, 3, 2, 3) -> 1*
      g2_0(1, 3, 2, 2) -> 1*
      g2_0(1, 3, 2, 1) -> 1*
      g2_0(1, 3, 1, 3) -> 1*
      g2_0(1, 3, 1, 2) -> 1*
      g2_0(1, 3, 1, 1) -> 1*
      g2_0(1, 2, 3, 3) -> 1*
      g2_0(1, 2, 3, 2) -> 1*
      g2_0(1, 2, 3, 1) -> 1*
      g2_0(1, 2, 2, 3) -> 1*
      g2_0(1, 2, 2, 2) -> 1*
      g2_0(1, 2, 2, 1) -> 1*
      g2_0(1, 2, 1, 3) -> 1*
      g2_0(1, 2, 1, 2) -> 1*
      g2_0(1, 2, 1, 1) -> 1*
      g2_0(1, 1, 3, 3) -> 1*
      g2_0(1, 1, 3, 2) -> 1*
      g2_0(1, 1, 3, 1) -> 1*
      g2_0(1, 1, 2, 3) -> 1*
      g2_0(1, 1, 2, 2) -> 1*
      g2_0(1, 1, 2, 1) -> 1*
      g2_0(1, 1, 1, 3) -> 1*
      g2_0(1, 1, 1, 2) -> 1*
      g2_0(1, 1, 1, 1) -> 1*
                 a_0() -> 3* | 2 | 1
    f_0(3, 3, 3, 3, 3) -> 1*
    f_0(3, 3, 3, 3, 2) -> 1*
    f_0(3, 3, 3, 3, 1) -> 1*
    f_0(3, 3, 3, 2, 3) -> 1*
    f_0(3, 3, 3, 2, 2) -> 1*
    f_0(3, 3, 3, 2, 1) -> 1*
    f_0(3, 3, 3, 1, 3) -> 1*
    f_0(3, 3, 3, 1, 2) -> 1*
    f_0(3, 3, 3, 1, 1) -> 1*
    f_0(3, 3, 2, 3, 3) -> 1*
    f_0(3, 3, 2, 3, 2) -> 1*
    f_0(3, 3, 2, 3, 1) -> 1*
    f_0(3, 3, 2, 2, 3) -> 1*
    f_0(3, 3, 2, 2, 2) -> 1*
    f_0(3, 3, 2, 2, 1) -> 1*
    f_0(3, 3, 2, 1, 3) -> 1*
    f_0(3, 3, 2, 1, 2) -> 1*
    f_0(3, 3, 2, 1, 1) -> 1*
    f_0(3, 3, 1, 3, 3) -> 1*
    f_0(3, 3, 1, 3, 2) -> 1*
    f_0(3, 3, 1, 3, 1) -> 1*
    f_0(3, 3, 1, 2, 3) -> 1*
    f_0(3, 3, 1, 2, 2) -> 1*
    f_0(3, 3, 1, 2, 1) -> 1*
    f_0(3, 3, 1, 1, 3) -> 1*
    f_0(3, 3, 1, 1, 2) -> 1*
    f_0(3, 3, 1, 1, 1) -> 1*
    f_0(3, 2, 3, 3, 3) -> 1*
    f_0(3, 2, 3, 3, 2) -> 1*
    f_0(3, 2, 3, 3, 1) -> 1*
    f_0(3, 2, 3, 2, 3) -> 1*
    f_0(3, 2, 3, 2, 2) -> 1*
    f_0(3, 2, 3, 2, 1) -> 1*
    f_0(3, 2, 3, 1, 3) -> 1*
    f_0(3, 2, 3, 1, 2) -> 1*
    f_0(3, 2, 3, 1, 1) -> 1*
    f_0(3, 2, 2, 3, 3) -> 1*
    f_0(3, 2, 2, 3, 2) -> 1*
    f_0(3, 2, 2, 3, 1) -> 1*
    f_0(3, 2, 2, 2, 3) -> 1*
    f_0(3, 2, 2, 2, 2) -> 1*
    f_0(3, 2, 2, 2, 1) -> 1*
    f_0(3, 2, 2, 1, 3) -> 1*
    f_0(3, 2, 2, 1, 2) -> 1*
    f_0(3, 2, 2, 1, 1) -> 1*
    f_0(3, 2, 1, 3, 3) -> 1*
    f_0(3, 2, 1, 3, 2) -> 1*
    f_0(3, 2, 1, 3, 1) -> 1*
    f_0(3, 2, 1, 2, 3) -> 1*
    f_0(3, 2, 1, 2, 2) -> 1*
    f_0(3, 2, 1, 2, 1) -> 1*
    f_0(3, 2, 1, 1, 3) -> 1*
    f_0(3, 2, 1, 1, 2) -> 1*
    f_0(3, 2, 1, 1, 1) -> 1*
    f_0(3, 1, 3, 3, 3) -> 1*
    f_0(3, 1, 3, 3, 2) -> 1*
    f_0(3, 1, 3, 3, 1) -> 1*
    f_0(3, 1, 3, 2, 3) -> 1*
    f_0(3, 1, 3, 2, 2) -> 1*
    f_0(3, 1, 3, 2, 1) -> 1*
    f_0(3, 1, 3, 1, 3) -> 1*
    f_0(3, 1, 3, 1, 2) -> 1*
    f_0(3, 1, 3, 1, 1) -> 1*
    f_0(3, 1, 2, 3, 3) -> 1*
    f_0(3, 1, 2, 3, 2) -> 1*
    f_0(3, 1, 2, 3, 1) -> 1*
    f_0(3, 1, 2, 2, 3) -> 1*
    f_0(3, 1, 2, 2, 2) -> 1*
    f_0(3, 1, 2, 2, 1) -> 1*
    f_0(3, 1, 2, 1, 3) -> 1*
    f_0(3, 1, 2, 1, 2) -> 1*
    f_0(3, 1, 2, 1, 1) -> 1*
    f_0(3, 1, 1, 3, 3) -> 1*
    f_0(3, 1, 1, 3, 2) -> 1*
    f_0(3, 1, 1, 3, 1) -> 1*
    f_0(3, 1, 1, 2, 3) -> 1*
    f_0(3, 1, 1, 2, 2) -> 1*
    f_0(3, 1, 1, 2, 1) -> 1*
    f_0(3, 1, 1, 1, 3) -> 1*
    f_0(3, 1, 1, 1, 2) -> 1*
    f_0(3, 1, 1, 1, 1) -> 1*
    f_0(2, 3, 3, 3, 3) -> 1*
    f_0(2, 3, 3, 3, 2) -> 1*
    f_0(2, 3, 3, 3, 1) -> 1*
    f_0(2, 3, 3, 2, 3) -> 1*
    f_0(2, 3, 3, 2, 2) -> 1*
    f_0(2, 3, 3, 2, 1) -> 1*
    f_0(2, 3, 3, 1, 3) -> 1*
    f_0(2, 3, 3, 1, 2) -> 1*
    f_0(2, 3, 3, 1, 1) -> 1*
    f_0(2, 3, 2, 3, 3) -> 1*
    f_0(2, 3, 2, 3, 2) -> 1*
    f_0(2, 3, 2, 3, 1) -> 1*
    f_0(2, 3, 2, 2, 3) -> 1*
    f_0(2, 3, 2, 2, 2) -> 1*
    f_0(2, 3, 2, 2, 1) -> 1*
    f_0(2, 3, 2, 1, 3) -> 1*
    f_0(2, 3, 2, 1, 2) -> 1*
    f_0(2, 3, 2, 1, 1) -> 1*
    f_0(2, 3, 1, 3, 3) -> 1*
    f_0(2, 3, 1, 3, 2) -> 1*
    f_0(2, 3, 1, 3, 1) -> 1*
    f_0(2, 3, 1, 2, 3) -> 1*
    f_0(2, 3, 1, 2, 2) -> 1*
    f_0(2, 3, 1, 2, 1) -> 1*
    f_0(2, 3, 1, 1, 3) -> 1*
    f_0(2, 3, 1, 1, 2) -> 1*
    f_0(2, 3, 1, 1, 1) -> 1*
    f_0(2, 2, 3, 3, 3) -> 1*
    f_0(2, 2, 3, 3, 2) -> 1*
    f_0(2, 2, 3, 3, 1) -> 1*
    f_0(2, 2, 3, 2, 3) -> 1*
    f_0(2, 2, 3, 2, 2) -> 1*
    f_0(2, 2, 3, 2, 1) -> 1*
    f_0(2, 2, 3, 1, 3) -> 1*
    f_0(2, 2, 3, 1, 2) -> 1*
    f_0(2, 2, 3, 1, 1) -> 1*
    f_0(2, 2, 2, 3, 3) -> 1*
    f_0(2, 2, 2, 3, 2) -> 1*
    f_0(2, 2, 2, 3, 1) -> 1*
    f_0(2, 2, 2, 2, 3) -> 1*
    f_0(2, 2, 2, 2, 2) -> 1*
    f_0(2, 2, 2, 2, 1) -> 1*
    f_0(2, 2, 2, 1, 3) -> 1*
    f_0(2, 2, 2, 1, 2) -> 1*
    f_0(2, 2, 2, 1, 1) -> 1*
    f_0(2, 2, 1, 3, 3) -> 1*
    f_0(2, 2, 1, 3, 2) -> 1*
    f_0(2, 2, 1, 3, 1) -> 1*
    f_0(2, 2, 1, 2, 3) -> 1*
    f_0(2, 2, 1, 2, 2) -> 1*
    f_0(2, 2, 1, 2, 1) -> 1*
    f_0(2, 2, 1, 1, 3) -> 1*
    f_0(2, 2, 1, 1, 2) -> 1*
    f_0(2, 2, 1, 1, 1) -> 1*
    f_0(2, 1, 3, 3, 3) -> 1*
    f_0(2, 1, 3, 3, 2) -> 1*
    f_0(2, 1, 3, 3, 1) -> 1*
    f_0(2, 1, 3, 2, 3) -> 1*
    f_0(2, 1, 3, 2, 2) -> 1*
    f_0(2, 1, 3, 2, 1) -> 1*
    f_0(2, 1, 3, 1, 3) -> 1*
    f_0(2, 1, 3, 1, 2) -> 1*
    f_0(2, 1, 3, 1, 1) -> 1*
    f_0(2, 1, 2, 3, 3) -> 1*
    f_0(2, 1, 2, 3, 2) -> 1*
    f_0(2, 1, 2, 3, 1) -> 1*
    f_0(2, 1, 2, 2, 3) -> 1*
    f_0(2, 1, 2, 2, 2) -> 1*
    f_0(2, 1, 2, 2, 1) -> 1*
    f_0(2, 1, 2, 1, 3) -> 1*
    f_0(2, 1, 2, 1, 2) -> 1*
    f_0(2, 1, 2, 1, 1) -> 1*
    f_0(2, 1, 1, 3, 3) -> 1*
    f_0(2, 1, 1, 3, 2) -> 1*
    f_0(2, 1, 1, 3, 1) -> 1*
    f_0(2, 1, 1, 2, 3) -> 1*
    f_0(2, 1, 1, 2, 2) -> 1*
    f_0(2, 1, 1, 2, 1) -> 1*
    f_0(2, 1, 1, 1, 3) -> 1*
    f_0(2, 1, 1, 1, 2) -> 1*
    f_0(2, 1, 1, 1, 1) -> 1*
    f_0(1, 3, 3, 3, 3) -> 1*
    f_0(1, 3, 3, 3, 2) -> 1*
    f_0(1, 3, 3, 3, 1) -> 1*
    f_0(1, 3, 3, 2, 3) -> 1*
    f_0(1, 3, 3, 2, 2) -> 1*
    f_0(1, 3, 3, 2, 1) -> 1*
    f_0(1, 3, 3, 1, 3) -> 1*
    f_0(1, 3, 3, 1, 2) -> 1*
    f_0(1, 3, 3, 1, 1) -> 1*
    f_0(1, 3, 2, 3, 3) -> 1*
    f_0(1, 3, 2, 3, 2) -> 1*
    f_0(1, 3, 2, 3, 1) -> 1*
    f_0(1, 3, 2, 2, 3) -> 1*
    f_0(1, 3, 2, 2, 2) -> 1*
    f_0(1, 3, 2, 2, 1) -> 1*
    f_0(1, 3, 2, 1, 3) -> 1*
    f_0(1, 3, 2, 1, 2) -> 1*
    f_0(1, 3, 2, 1, 1) -> 1*
    f_0(1, 3, 1, 3, 3) -> 1*
    f_0(1, 3, 1, 3, 2) -> 1*
    f_0(1, 3, 1, 3, 1) -> 1*
    f_0(1, 3, 1, 2, 3) -> 1*
    f_0(1, 3, 1, 2, 2) -> 1*
    f_0(1, 3, 1, 2, 1) -> 1*
    f_0(1, 3, 1, 1, 3) -> 1*
    f_0(1, 3, 1, 1, 2) -> 1*
    f_0(1, 3, 1, 1, 1) -> 1*
    f_0(1, 2, 3, 3, 3) -> 1*
    f_0(1, 2, 3, 3, 2) -> 1*
    f_0(1, 2, 3, 3, 1) -> 1*
    f_0(1, 2, 3, 2, 3) -> 1*
    f_0(1, 2, 3, 2, 2) -> 1*
    f_0(1, 2, 3, 2, 1) -> 1*
    f_0(1, 2, 3, 1, 3) -> 1*
    f_0(1, 2, 3, 1, 2) -> 1*
    f_0(1, 2, 3, 1, 1) -> 1*
    f_0(1, 2, 2, 3, 3) -> 1*
    f_0(1, 2, 2, 3, 2) -> 1*
    f_0(1, 2, 2, 3, 1) -> 1*
    f_0(1, 2, 2, 2, 3) -> 1*
    f_0(1, 2, 2, 2, 2) -> 1*
    f_0(1, 2, 2, 2, 1) -> 1*
    f_0(1, 2, 2, 1, 3) -> 1*
    f_0(1, 2, 2, 1, 2) -> 1*
    f_0(1, 2, 2, 1, 1) -> 1*
    f_0(1, 2, 1, 3, 3) -> 1*
    f_0(1, 2, 1, 3, 2) -> 1*
    f_0(1, 2, 1, 3, 1) -> 1*
    f_0(1, 2, 1, 2, 3) -> 1*
    f_0(1, 2, 1, 2, 2) -> 1*
    f_0(1, 2, 1, 2, 1) -> 1*
    f_0(1, 2, 1, 1, 3) -> 1*
    f_0(1, 2, 1, 1, 2) -> 1*
    f_0(1, 2, 1, 1, 1) -> 1*
    f_0(1, 1, 3, 3, 3) -> 1*
    f_0(1, 1, 3, 3, 2) -> 1*
    f_0(1, 1, 3, 3, 1) -> 1*
    f_0(1, 1, 3, 2, 3) -> 1*
    f_0(1, 1, 3, 2, 2) -> 1*
    f_0(1, 1, 3, 2, 1) -> 1*
    f_0(1, 1, 3, 1, 3) -> 1*
    f_0(1, 1, 3, 1, 2) -> 1*
    f_0(1, 1, 3, 1, 1) -> 1*
    f_0(1, 1, 2, 3, 3) -> 1*
    f_0(1, 1, 2, 3, 2) -> 1*
    f_0(1, 1, 2, 3, 1) -> 1*
    f_0(1, 1, 2, 2, 3) -> 1*
    f_0(1, 1, 2, 2, 2) -> 1*
    f_0(1, 1, 2, 2, 1) -> 1*
    f_0(1, 1, 2, 1, 3) -> 1*
    f_0(1, 1, 2, 1, 2) -> 1*
    f_0(1, 1, 2, 1, 1) -> 1*
    f_0(1, 1, 1, 3, 3) -> 1*
    f_0(1, 1, 1, 3, 2) -> 1*
    f_0(1, 1, 1, 3, 1) -> 1*
    f_0(1, 1, 1, 2, 3) -> 1*
    f_0(1, 1, 1, 2, 2) -> 1*
    f_0(1, 1, 1, 2, 1) -> 1*
    f_0(1, 1, 1, 1, 3) -> 1*
    f_0(1, 1, 1, 1, 2) -> 1*
    f_0(1, 1, 1, 1, 1) -> 1*
      g1_1(3, 3, 3, 3) -> 1*
      g1_1(3, 3, 3, 2) -> 1*
      g1_1(3, 3, 3, 1) -> 1*
      g1_1(3, 3, 2, 3) -> 1*
      g1_1(3, 3, 2, 2) -> 1*
      g1_1(3, 3, 2, 1) -> 1*
      g1_1(3, 3, 1, 3) -> 1*
      g1_1(3, 3, 1, 2) -> 1*
      g1_1(3, 3, 1, 1) -> 1*
      g1_1(3, 2, 3, 3) -> 1*
      g1_1(3, 2, 3, 2) -> 1*
      g1_1(3, 2, 3, 1) -> 1*
      g1_1(3, 2, 2, 3) -> 1*
      g1_1(3, 2, 2, 2) -> 1*
      g1_1(3, 2, 2, 1) -> 1*
      g1_1(3, 2, 1, 3) -> 1*
      g1_1(3, 2, 1, 2) -> 1*
      g1_1(3, 2, 1, 1) -> 1*
      g1_1(3, 1, 3, 3) -> 1*
      g1_1(3, 1, 3, 2) -> 1*
      g1_1(3, 1, 3, 1) -> 1*
      g1_1(3, 1, 2, 3) -> 1*
      g1_1(3, 1, 2, 2) -> 1*
      g1_1(3, 1, 2, 1) -> 1*
      g1_1(3, 1, 1, 3) -> 1*
      g1_1(3, 1, 1, 2) -> 1*
      g1_1(3, 1, 1, 1) -> 1*
      g1_1(2, 3, 3, 3) -> 1*
      g1_1(2, 3, 3, 2) -> 1*
      g1_1(2, 3, 3, 1) -> 1*
      g1_1(2, 3, 2, 3) -> 1*
      g1_1(2, 3, 2, 2) -> 1*
      g1_1(2, 3, 2, 1) -> 1*
      g1_1(2, 3, 1, 3) -> 1*
      g1_1(2, 3, 1, 2) -> 1*
      g1_1(2, 3, 1, 1) -> 1*
      g1_1(2, 2, 3, 3) -> 1*
      g1_1(2, 2, 3, 2) -> 1*
      g1_1(2, 2, 3, 1) -> 1*
      g1_1(2, 2, 2, 3) -> 1*
      g1_1(2, 2, 2, 2) -> 1*
      g1_1(2, 2, 2, 1) -> 1*
      g1_1(2, 2, 1, 3) -> 1*
      g1_1(2, 2, 1, 2) -> 1*
      g1_1(2, 2, 1, 1) -> 1*
      g1_1(2, 1, 3, 3) -> 1*
      g1_1(2, 1, 3, 2) -> 1*
      g1_1(2, 1, 3, 1) -> 1*
      g1_1(2, 1, 2, 3) -> 1*
      g1_1(2, 1, 2, 2) -> 1*
      g1_1(2, 1, 2, 1) -> 1*
      g1_1(2, 1, 1, 3) -> 1*
      g1_1(2, 1, 1, 2) -> 1*
      g1_1(2, 1, 1, 1) -> 1*
      g1_1(1, 3, 3, 3) -> 1*
      g1_1(1, 3, 3, 2) -> 1*
      g1_1(1, 3, 3, 1) -> 1*
      g1_1(1, 3, 2, 3) -> 1*
      g1_1(1, 3, 2, 2) -> 1*
      g1_1(1, 3, 2, 1) -> 1*
      g1_1(1, 3, 1, 3) -> 1*
      g1_1(1, 3, 1, 2) -> 1*
      g1_1(1, 3, 1, 1) -> 1*
      g1_1(1, 2, 3, 3) -> 1*
      g1_1(1, 2, 3, 2) -> 1*
      g1_1(1, 2, 3, 1) -> 1*
      g1_1(1, 2, 2, 3) -> 1*
      g1_1(1, 2, 2, 2) -> 1*
      g1_1(1, 2, 2, 1) -> 1*
      g1_1(1, 2, 1, 3) -> 1*
      g1_1(1, 2, 1, 2) -> 1*
      g1_1(1, 2, 1, 1) -> 1*
      g1_1(1, 1, 3, 3) -> 1*
      g1_1(1, 1, 3, 2) -> 1*
      g1_1(1, 1, 3, 1) -> 1*
      g1_1(1, 1, 2, 3) -> 1*
      g1_1(1, 1, 2, 2) -> 1*
      g1_1(1, 1, 2, 1) -> 1*
      g1_1(1, 1, 1, 3) -> 1*
      g1_1(1, 1, 1, 2) -> 1*
      g1_1(1, 1, 1, 1) -> 1*
      g1_0(3, 3, 3, 3) -> 1*
      g1_0(3, 3, 3, 2) -> 1*
      g1_0(3, 3, 3, 1) -> 1*
      g1_0(3, 3, 2, 3) -> 1*
      g1_0(3, 3, 2, 2) -> 1*
      g1_0(3, 3, 2, 1) -> 1*
      g1_0(3, 3, 1, 3) -> 1*
      g1_0(3, 3, 1, 2) -> 1*
      g1_0(3, 3, 1, 1) -> 1*
      g1_0(3, 2, 3, 3) -> 1*
      g1_0(3, 2, 3, 2) -> 1*
      g1_0(3, 2, 3, 1) -> 1*
      g1_0(3, 2, 2, 3) -> 1*
      g1_0(3, 2, 2, 2) -> 1*
      g1_0(3, 2, 2, 1) -> 1*
      g1_0(3, 2, 1, 3) -> 1*
      g1_0(3, 2, 1, 2) -> 1*
      g1_0(3, 2, 1, 1) -> 1*
      g1_0(3, 1, 3, 3) -> 1*
      g1_0(3, 1, 3, 2) -> 1*
      g1_0(3, 1, 3, 1) -> 1*
      g1_0(3, 1, 2, 3) -> 1*
      g1_0(3, 1, 2, 2) -> 1*
      g1_0(3, 1, 2, 1) -> 1*
      g1_0(3, 1, 1, 3) -> 1*
      g1_0(3, 1, 1, 2) -> 1*
      g1_0(3, 1, 1, 1) -> 1*
      g1_0(2, 3, 3, 3) -> 1*
      g1_0(2, 3, 3, 2) -> 1*
      g1_0(2, 3, 3, 1) -> 1*
      g1_0(2, 3, 2, 3) -> 1*
      g1_0(2, 3, 2, 2) -> 1*
      g1_0(2, 3, 2, 1) -> 1*
      g1_0(2, 3, 1, 3) -> 1*
      g1_0(2, 3, 1, 2) -> 1*
      g1_0(2, 3, 1, 1) -> 1*
      g1_0(2, 2, 3, 3) -> 1*
      g1_0(2, 2, 3, 2) -> 1*
      g1_0(2, 2, 3, 1) -> 1*
      g1_0(2, 2, 2, 3) -> 1*
      g1_0(2, 2, 2, 2) -> 1*
      g1_0(2, 2, 2, 1) -> 1*
      g1_0(2, 2, 1, 3) -> 1*
      g1_0(2, 2, 1, 2) -> 1*
      g1_0(2, 2, 1, 1) -> 1*
      g1_0(2, 1, 3, 3) -> 1*
      g1_0(2, 1, 3, 2) -> 1*
      g1_0(2, 1, 3, 1) -> 1*
      g1_0(2, 1, 2, 3) -> 1*
      g1_0(2, 1, 2, 2) -> 1*
      g1_0(2, 1, 2, 1) -> 1*
      g1_0(2, 1, 1, 3) -> 1*
      g1_0(2, 1, 1, 2) -> 1*
      g1_0(2, 1, 1, 1) -> 1*
      g1_0(1, 3, 3, 3) -> 1*
      g1_0(1, 3, 3, 2) -> 1*
      g1_0(1, 3, 3, 1) -> 1*
      g1_0(1, 3, 2, 3) -> 1*
      g1_0(1, 3, 2, 2) -> 1*
      g1_0(1, 3, 2, 1) -> 1*
      g1_0(1, 3, 1, 3) -> 1*
      g1_0(1, 3, 1, 2) -> 1*
      g1_0(1, 3, 1, 1) -> 1*
      g1_0(1, 2, 3, 3) -> 1*
      g1_0(1, 2, 3, 2) -> 1*
      g1_0(1, 2, 3, 1) -> 1*
      g1_0(1, 2, 2, 3) -> 1*
      g1_0(1, 2, 2, 2) -> 1*
      g1_0(1, 2, 2, 1) -> 1*
      g1_0(1, 2, 1, 3) -> 1*
      g1_0(1, 2, 1, 2) -> 1*
      g1_0(1, 2, 1, 1) -> 1*
      g1_0(1, 1, 3, 3) -> 1*
      g1_0(1, 1, 3, 2) -> 1*
      g1_0(1, 1, 3, 1) -> 1*
      g1_0(1, 1, 2, 3) -> 1*
      g1_0(1, 1, 2, 2) -> 1*
      g1_0(1, 1, 2, 1) -> 1*
      g1_0(1, 1, 1, 3) -> 1*
      g1_0(1, 1, 1, 2) -> 1*
      g1_0(1, 1, 1, 1) -> 1*
                     3 -> 1*
                     2 -> 1*
   }
  Strict:
   {}
  Qed