YES

Problem:
 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(),a(),w) -> g2(x,y,y,w)
 f(x,y,a(),w,w) -> g2(y,y,x,w)
 g1(x,x,y,a()) -> h(x,y)
 g1(y,x,x,a()) -> h(x,y)
 g2(x,y,y,a()) -> h(x,y)
 g2(y,y,x,a()) -> h(x,y)
 h(x,x) -> x

Proof:
 Bounds Processor:
  bound: 2
  enrichment: roof
  automaton:
   final states: {6,1,2}
   transitions:
    f0(6,1,2,2,2) -> 1*
    f0(1,1,2,2,2) -> 1*
    f0(2,1,2,2,2) -> 1*
    f0(6,2,2,2,2) -> 1*
    f0(1,2,2,2,2) -> 1*
    f0(2,2,2,2,2) -> 1*
    f0(1,6,2,2,2) -> 1*
    f0(6,6,2,2,2) -> 1*
    f0(2,6,2,2,2) -> 1*
    f0(1,1,2,6,2) -> 1*
    f0(6,1,2,6,2) -> 1*
    f0(2,1,2,6,2) -> 1*
    f0(1,2,2,6,2) -> 1*
    f0(6,2,2,6,2) -> 1*
    f0(2,2,2,6,2) -> 1*
    f0(1,1,6,2,1) -> 1*
    f0(6,1,6,2,1) -> 1*
    f0(2,1,6,2,1) -> 1*
    f0(1,2,6,2,1) -> 1*
    f0(6,2,6,2,1) -> 1*
    f0(2,2,6,2,1) -> 1*
    f0(1,6,2,6,2) -> 1*
    f0(6,6,2,6,2) -> 1*
    f0(2,6,2,6,2) -> 1*
    f0(6,1,1,2,1) -> 1*
    f0(1,6,6,2,1) -> 1*
    f0(6,6,6,2,1) -> 1*
    f0(2,6,6,2,1) -> 1*
    f0(1,1,1,2,1) -> 1*
    f0(2,1,1,2,1) -> 1*
    f0(6,2,1,2,1) -> 1*
    f0(1,2,1,2,1) -> 1*
    f0(2,2,1,2,1) -> 1*
    f0(1,6,1,2,1) -> 1*
    f0(6,6,1,2,1) -> 1*
    f0(2,6,1,2,1) -> 1*
    f0(1,1,6,6,1) -> 1*
    f0(6,1,6,6,1) -> 1*
    f0(2,1,6,6,1) -> 1*
    f0(1,2,6,6,1) -> 1*
    f0(6,2,6,6,1) -> 1*
    f0(2,2,6,6,1) -> 1*
    f0(1,1,1,6,1) -> 1*
    f0(6,1,1,6,1) -> 1*
    f0(2,1,1,6,1) -> 1*
    f0(1,6,6,6,1) -> 1*
    f0(6,6,6,6,1) -> 1*
    f0(2,6,6,6,1) -> 1*
    f0(1,2,1,6,1) -> 1*
    f0(6,2,1,6,1) -> 1*
    f0(2,2,1,6,1) -> 1*
    f0(1,6,1,6,1) -> 1*
    f0(6,6,1,6,1) -> 1*
    f0(2,6,1,6,1) -> 1*
    f0(6,1,2,1,1) -> 1*
    f0(1,1,2,1,1) -> 1*
    f0(2,1,2,1,1) -> 1*
    f0(6,2,2,1,1) -> 1*
    f0(1,2,2,1,1) -> 1*
    f0(2,2,2,1,1) -> 1*
    f0(1,6,2,1,1) -> 1*
    f0(6,6,2,1,1) -> 1*
    f0(2,6,2,1,1) -> 1*
    f0(1,1,6,1,6) -> 1*
    f0(6,1,6,1,6) -> 1*
    f0(2,1,6,1,6) -> 1*
    f0(1,2,6,1,6) -> 1*
    f0(6,2,6,1,6) -> 1*
    f0(2,2,6,1,6) -> 1*
    f0(1,1,1,1,6) -> 1*
    f0(6,1,1,1,6) -> 1*
    f0(2,1,1,1,6) -> 1*
    f0(1,6,6,1,6) -> 1*
    f0(6,6,6,1,6) -> 1*
    f0(2,6,6,1,6) -> 1*
    f0(1,2,1,1,6) -> 1*
    f0(6,2,1,1,6) -> 1*
    f0(2,2,1,1,6) -> 1*
    f0(1,6,1,1,6) -> 1*
    f0(6,6,1,1,6) -> 1*
    f0(2,6,1,1,6) -> 1*
    f0(1,1,2,2,6) -> 1*
    f0(6,1,2,2,6) -> 1*
    f0(2,1,2,2,6) -> 1*
    f0(1,2,2,2,6) -> 1*
    f0(6,2,2,2,6) -> 1*
    f0(2,2,2,2,6) -> 1*
    f0(1,6,2,2,6) -> 1*
    f0(6,6,2,2,6) -> 1*
    f0(2,6,2,2,6) -> 1*
    f0(1,1,2,6,6) -> 1*
    f0(6,1,2,6,6) -> 1*
    f0(2,1,2,6,6) -> 1*
    f0(1,2,2,6,6) -> 1*
    f0(6,2,2,6,6) -> 1*
    f0(2,2,2,6,6) -> 1*
    f0(1,6,2,6,6) -> 1*
    f0(6,6,2,6,6) -> 1*
    f0(2,6,2,6,6) -> 1*
    f0(1,1,6,2,2) -> 1*
    f0(6,1,6,2,2) -> 1*
    f0(2,1,6,2,2) -> 1*
    f0(1,2,6,2,2) -> 1*
    f0(6,2,6,2,2) -> 1*
    f0(2,2,6,2,2) -> 1*
    f0(6,1,1,2,2) -> 1*
    f0(1,6,6,2,2) -> 1*
    f0(6,6,6,2,2) -> 1*
    f0(2,6,6,2,2) -> 1*
    f0(1,1,1,2,2) -> 1*
    f0(2,1,1,2,2) -> 1*
    f0(6,2,1,2,2) -> 1*
    f0(1,2,1,2,2) -> 1*
    f0(2,2,1,2,2) -> 1*
    f0(1,6,1,2,2) -> 1*
    f0(6,6,1,2,2) -> 1*
    f0(2,6,1,2,2) -> 1*
    f0(1,1,6,6,2) -> 1*
    f0(6,1,6,6,2) -> 1*
    f0(2,1,6,6,2) -> 1*
    f0(1,2,6,6,2) -> 1*
    f0(6,2,6,6,2) -> 1*
    f0(2,2,6,6,2) -> 1*
    f0(1,1,1,6,2) -> 1*
    f0(6,1,1,6,2) -> 1*
    f0(2,1,1,6,2) -> 1*
    f0(1,6,6,6,2) -> 1*
    f0(6,6,6,6,2) -> 1*
    f0(2,6,6,6,2) -> 1*
    f0(1,2,1,6,2) -> 1*
    f0(6,2,1,6,2) -> 1*
    f0(2,2,1,6,2) -> 1*
    f0(1,6,1,6,2) -> 1*
    f0(6,6,1,6,2) -> 1*
    f0(2,6,1,6,2) -> 1*
    f0(6,1,2,1,2) -> 1*
    f0(1,1,2,1,2) -> 1*
    f0(2,1,2,1,2) -> 1*
    f0(6,2,2,1,2) -> 1*
    f0(1,2,2,1,2) -> 1*
    f0(2,2,2,1,2) -> 1*
    f0(1,6,2,1,2) -> 1*
    f0(6,6,2,1,2) -> 1*
    f0(2,6,2,1,2) -> 1*
    f0(1,1,6,1,1) -> 1*
    f0(6,1,6,1,1) -> 1*
    f0(2,1,6,1,1) -> 1*
    f0(1,2,6,1,1) -> 1*
    f0(6,2,6,1,1) -> 1*
    f0(2,2,6,1,1) -> 1*
    f0(6,1,1,1,1) -> 1*
    f0(1,6,6,1,1) -> 1*
    f0(6,6,6,1,1) -> 1*
    f0(2,6,6,1,1) -> 1*
    f0(1,1,1,1,1) -> 1*
    f0(2,1,1,1,1) -> 1*
    f0(6,2,1,1,1) -> 1*
    f0(1,2,1,1,1) -> 1*
    f0(2,2,1,1,1) -> 1*
    f0(1,6,1,1,1) -> 1*
    f0(6,6,1,1,1) -> 1*
    f0(2,6,1,1,1) -> 1*
    f0(6,1,2,2,1) -> 1*
    f0(1,1,2,2,1) -> 1*
    f0(2,1,2,2,1) -> 1*
    f0(6,2,2,2,1) -> 1*
    f0(1,2,2,2,1) -> 1*
    f0(2,2,2,2,1) -> 1*
    f0(1,6,2,2,1) -> 1*
    f0(6,6,2,2,1) -> 1*
    f0(2,6,2,2,1) -> 1*
    f0(1,1,2,6,1) -> 1*
    f0(6,1,2,6,1) -> 1*
    f0(2,1,2,6,1) -> 1*
    f0(1,2,2,6,1) -> 1*
    f0(6,2,2,6,1) -> 1*
    f0(2,2,2,6,1) -> 1*
    f0(1,6,2,6,1) -> 1*
    f0(6,6,2,6,1) -> 1*
    f0(2,6,2,6,1) -> 1*
    f0(1,1,6,2,6) -> 1*
    f0(6,1,6,2,6) -> 1*
    f0(2,1,6,2,6) -> 1*
    f0(1,2,6,2,6) -> 1*
    f0(6,2,6,2,6) -> 1*
    f0(2,2,6,2,6) -> 1*
    f0(1,1,1,2,6) -> 1*
    f0(6,1,1,2,6) -> 1*
    f0(2,1,1,2,6) -> 1*
    f0(1,6,6,2,6) -> 1*
    f0(6,6,6,2,6) -> 1*
    f0(2,6,6,2,6) -> 1*
    f0(1,2,1,2,6) -> 1*
    f0(6,2,1,2,6) -> 1*
    f0(2,2,1,2,6) -> 1*
    f0(1,6,1,2,6) -> 1*
    f0(6,6,1,2,6) -> 1*
    f0(2,6,1,2,6) -> 1*
    f0(1,1,6,6,6) -> 1*
    f0(6,1,6,6,6) -> 1*
    f0(2,1,6,6,6) -> 1*
    f0(1,2,6,6,6) -> 1*
    f0(6,2,6,6,6) -> 1*
    f0(2,2,6,6,6) -> 1*
    f0(1,1,1,6,6) -> 1*
    f0(6,1,1,6,6) -> 1*
    f0(2,1,1,6,6) -> 1*
    f0(1,6,6,6,6) -> 1*
    f0(6,6,6,6,6) -> 1*
    f0(2,6,6,6,6) -> 1*
    f0(1,2,1,6,6) -> 1*
    f0(6,2,1,6,6) -> 1*
    f0(2,2,1,6,6) -> 1*
    f0(1,6,1,6,6) -> 1*
    f0(6,6,1,6,6) -> 1*
    f0(2,6,1,6,6) -> 1*
    f0(1,1,2,1,6) -> 1*
    f0(6,1,2,1,6) -> 1*
    f0(2,1,2,1,6) -> 1*
    f0(1,2,2,1,6) -> 1*
    f0(6,2,2,1,6) -> 1*
    f0(2,2,2,1,6) -> 1*
    f0(1,6,2,1,6) -> 1*
    f0(6,6,2,1,6) -> 1*
    f0(2,6,2,1,6) -> 1*
    f0(1,1,6,1,2) -> 1*
    f0(6,1,6,1,2) -> 1*
    f0(2,1,6,1,2) -> 1*
    f0(1,2,6,1,2) -> 1*
    f0(6,2,6,1,2) -> 1*
    f0(2,2,6,1,2) -> 1*
    f0(6,1,1,1,2) -> 1*
    f0(1,6,6,1,2) -> 1*
    f0(6,6,6,1,2) -> 1*
    f0(2,6,6,1,2) -> 1*
    f0(1,1,1,1,2) -> 1*
    f0(2,1,1,1,2) -> 1*
    f0(6,2,1,1,2) -> 1*
    f0(1,2,1,1,2) -> 1*
    f0(2,2,1,1,2) -> 1*
    f0(1,6,1,1,2) -> 1*
    f0(6,6,1,1,2) -> 1*
    f0(2,6,1,1,2) -> 1*
    a0() -> 6*,1,2
    g10(6,6,6,6) -> 1*
    g10(1,6,6,6) -> 1*
    g10(2,2,1,2) -> 1*
    g10(2,1,6,2) -> 1*
    g10(2,6,1,2) -> 1*
    g10(2,1,1,1) -> 1*
    g10(2,1,6,6) -> 1*
    g10(2,2,6,1) -> 1*
    g10(2,6,6,1) -> 1*
    g10(6,1,2,2) -> 1*
    g10(1,1,2,2) -> 1*
    g10(6,1,2,6) -> 1*
    g10(6,2,2,1) -> 1*
    g10(1,1,2,6) -> 1*
    g10(1,2,2,1) -> 1*
    g10(6,6,2,1) -> 1*
    g10(1,6,2,1) -> 1*
    g10(2,2,2,2) -> 1*
    g10(2,6,2,2) -> 1*
    g10(2,1,2,1) -> 1*
    g10(2,2,2,6) -> 1*
    g10(2,6,2,6) -> 1*
    g10(6,2,1,6) -> 1*
    g10(1,2,1,6) -> 1*
    g10(6,6,1,6) -> 1*
    g10(1,6,1,6) -> 1*
    g10(2,1,1,6) -> 1*
    g10(6,2,1,2) -> 1*
    g10(1,2,1,2) -> 1*
    g10(6,1,6,2) -> 1*
    g10(6,6,1,2) -> 1*
    g10(1,1,6,2) -> 1*
    g10(1,6,1,2) -> 1*
    g10(6,1,1,1) -> 1*
    g10(1,1,1,1) -> 1*
    g10(6,1,6,6) -> 1*
    g10(6,2,6,1) -> 1*
    g10(1,1,6,6) -> 1*
    g10(1,2,6,1) -> 1*
    g10(6,6,6,1) -> 1*
    g10(1,6,6,1) -> 1*
    g10(2,1,1,2) -> 1*
    g10(2,2,6,2) -> 1*
    g10(2,2,1,1) -> 1*
    g10(2,6,6,2) -> 1*
    g10(2,1,6,1) -> 1*
    g10(2,6,1,1) -> 1*
    g10(2,2,6,6) -> 1*
    g10(2,6,6,6) -> 1*
    g10(6,2,2,2) -> 1*
    g10(1,2,2,2) -> 1*
    g10(6,6,2,2) -> 1*
    g10(1,6,2,2) -> 1*
    g10(6,1,2,1) -> 1*
    g10(1,1,2,1) -> 1*
    g10(6,2,2,6) -> 1*
    g10(1,2,2,6) -> 1*
    g10(6,6,2,6) -> 1*
    g10(1,6,2,6) -> 1*
    g10(2,1,2,2) -> 1*
    g10(2,1,2,6) -> 1*
    g10(2,2,2,1) -> 1*
    g10(6,1,1,6) -> 1*
    g10(2,6,2,1) -> 1*
    g10(1,1,1,6) -> 1*
    g10(2,2,1,6) -> 1*
    g10(2,6,1,6) -> 1*
    g10(6,1,1,2) -> 1*
    g10(1,1,1,2) -> 1*
    g10(6,2,6,2) -> 1*
    g10(1,2,6,2) -> 1*
    g10(6,2,1,1) -> 1*
    g10(1,2,1,1) -> 1*
    g10(6,6,6,2) -> 1*
    g10(1,6,6,2) -> 1*
    g10(6,1,6,1) -> 1*
    g10(6,6,1,1) -> 1*
    g10(1,1,6,1) -> 1*
    g10(6,2,6,6) -> 1*
    g10(1,6,1,1) -> 1*
    g10(1,2,6,6) -> 1*
    g20(6,6,6,6) -> 1*
    g20(1,6,6,6) -> 1*
    g20(2,2,1,2) -> 1*
    g20(2,1,6,2) -> 1*
    g20(2,6,1,2) -> 1*
    g20(2,1,1,1) -> 1*
    g20(2,1,6,6) -> 1*
    g20(2,2,6,1) -> 1*
    g20(2,6,6,1) -> 1*
    g20(6,1,2,2) -> 1*
    g20(1,1,2,2) -> 1*
    g20(6,1,2,6) -> 1*
    g20(6,2,2,1) -> 1*
    g20(1,1,2,6) -> 1*
    g20(1,2,2,1) -> 1*
    g20(6,6,2,1) -> 1*
    g20(1,6,2,1) -> 1*
    g20(2,2,2,2) -> 1*
    g20(2,6,2,2) -> 1*
    g20(2,1,2,1) -> 1*
    g20(2,2,2,6) -> 1*
    g20(2,6,2,6) -> 1*
    g20(6,2,1,6) -> 1*
    g20(1,2,1,6) -> 1*
    g20(6,6,1,6) -> 1*
    g20(1,6,1,6) -> 1*
    g20(2,1,1,6) -> 1*
    g20(6,2,1,2) -> 1*
    g20(1,2,1,2) -> 1*
    g20(6,1,6,2) -> 1*
    g20(6,6,1,2) -> 1*
    g20(1,1,6,2) -> 1*
    g20(1,6,1,2) -> 1*
    g20(6,1,1,1) -> 1*
    g20(1,1,1,1) -> 1*
    g20(6,1,6,6) -> 1*
    g20(6,2,6,1) -> 1*
    g20(1,1,6,6) -> 1*
    g20(1,2,6,1) -> 1*
    g20(6,6,6,1) -> 1*
    g20(1,6,6,1) -> 1*
    g20(2,1,1,2) -> 1*
    g20(2,2,6,2) -> 1*
    g20(2,2,1,1) -> 1*
    g20(2,6,6,2) -> 1*
    g20(2,1,6,1) -> 1*
    g20(2,6,1,1) -> 1*
    g20(2,2,6,6) -> 1*
    g20(2,6,6,6) -> 1*
    g20(6,2,2,2) -> 1*
    g20(1,2,2,2) -> 1*
    g20(6,6,2,2) -> 1*
    g20(1,6,2,2) -> 1*
    g20(6,1,2,1) -> 1*
    g20(1,1,2,1) -> 1*
    g20(6,2,2,6) -> 1*
    g20(1,2,2,6) -> 1*
    g20(6,6,2,6) -> 1*
    g20(1,6,2,6) -> 1*
    g20(2,1,2,2) -> 1*
    g20(2,1,2,6) -> 1*
    g20(2,2,2,1) -> 1*
    g20(6,1,1,6) -> 1*
    g20(2,6,2,1) -> 1*
    g20(1,1,1,6) -> 1*
    g20(2,2,1,6) -> 1*
    g20(2,6,1,6) -> 1*
    g20(6,1,1,2) -> 1*
    g20(1,1,1,2) -> 1*
    g20(6,2,6,2) -> 1*
    g20(1,2,6,2) -> 1*
    g20(6,2,1,1) -> 1*
    g20(1,2,1,1) -> 1*
    g20(6,6,6,2) -> 1*
    g20(1,6,6,2) -> 1*
    g20(6,1,6,1) -> 1*
    g20(6,6,1,1) -> 1*
    g20(1,1,6,1) -> 1*
    g20(6,2,6,6) -> 1*
    g20(1,6,1,1) -> 1*
    g20(1,2,6,6) -> 1*
    h0(6,2) -> 1*
    h0(1,2) -> 1*
    h0(6,6) -> 1*
    h0(1,6) -> 1*
    h0(2,1) -> 1*
    h0(6,1) -> 1*
    h0(1,1) -> 1*
    h0(2,2) -> 1*
    h0(2,6) -> 1*
    h1(6,2) -> 1*
    h1(1,2) -> 1*
    h1(6,6) -> 1*
    h1(1,6) -> 1*
    h1(2,1) -> 1*
    h1(6,1) -> 1*
    h1(1,1) -> 1*
    h1(2,2) -> 1*
    h1(2,6) -> 1*
    g21(6,6,6,6) -> 1*
    g21(1,6,6,6) -> 1*
    g21(2,2,1,2) -> 1*
    g21(2,1,6,2) -> 1*
    g21(2,6,1,2) -> 1*
    g21(2,1,1,1) -> 1*
    g21(2,1,6,6) -> 1*
    g21(2,2,6,1) -> 1*
    g21(2,6,6,1) -> 1*
    g21(6,1,2,2) -> 1*
    g21(1,1,2,2) -> 1*
    g21(6,1,2,6) -> 1*
    g21(6,2,2,1) -> 1*
    g21(1,1,2,6) -> 1*
    g21(1,2,2,1) -> 1*
    g21(6,6,2,1) -> 1*
    g21(1,6,2,1) -> 1*
    g21(2,2,2,2) -> 1*
    g21(2,6,2,2) -> 1*
    g21(2,2,2,6) -> 1*
    g21(2,6,2,6) -> 1*
    g21(6,2,1,6) -> 1*
    g21(6,6,1,6) -> 1*
    g21(1,6,1,6) -> 1*
    g21(2,1,1,6) -> 1*
    g21(6,2,1,2) -> 1*
    g21(6,1,6,2) -> 1*
    g21(6,6,1,2) -> 1*
    g21(1,1,6,2) -> 1*
    g21(1,6,1,2) -> 1*
    g21(6,1,1,1) -> 1*
    g21(1,1,1,1) -> 1*
    g21(6,1,6,6) -> 1*
    g21(6,2,6,1) -> 1*
    g21(1,1,6,6) -> 1*
    g21(1,2,6,1) -> 1*
    g21(6,6,6,1) -> 1*
    g21(1,6,6,1) -> 1*
    g21(2,1,1,2) -> 1*
    g21(2,2,6,2) -> 1*
    g21(2,2,1,1) -> 1*
    g21(2,6,6,2) -> 1*
    g21(2,1,6,1) -> 1*
    g21(2,6,1,1) -> 1*
    g21(2,2,6,6) -> 1*
    g21(2,6,6,6) -> 1*
    g21(6,2,2,2) -> 1*
    g21(1,2,2,2) -> 1*
    g21(6,6,2,2) -> 1*
    g21(1,6,2,2) -> 1*
    g21(6,1,2,1) -> 1*
    g21(1,1,2,1) -> 1*
    g21(6,2,2,6) -> 1*
    g21(1,2,2,6) -> 1*
    g21(6,6,2,6) -> 1*
    g21(1,6,2,6) -> 1*
    g21(2,2,2,1) -> 1*
    g21(6,1,1,6) -> 1*
    g21(2,6,2,1) -> 1*
    g21(1,1,1,6) -> 1*
    g21(2,2,1,6) -> 1*
    g21(2,6,1,6) -> 1*
    g21(6,1,1,2) -> 1*
    g21(1,1,1,2) -> 1*
    g21(6,2,6,2) -> 1*
    g21(1,2,6,2) -> 1*
    g21(6,2,1,1) -> 1*
    g21(6,6,6,2) -> 1*
    g21(1,6,6,2) -> 1*
    g21(6,1,6,1) -> 1*
    g21(6,6,1,1) -> 1*
    g21(1,1,6,1) -> 1*
    g21(6,2,6,6) -> 1*
    g21(1,6,1,1) -> 1*
    g21(1,2,6,6) -> 1*
    g11(6,6,6,6) -> 1*
    g11(1,6,6,6) -> 1*
    g11(2,2,1,2) -> 1*
    g11(2,1,6,2) -> 1*
    g11(2,6,1,2) -> 1*
    g11(2,1,1,1) -> 1*
    g11(2,1,6,6) -> 1*
    g11(2,2,6,1) -> 1*
    g11(2,6,6,1) -> 1*
    g11(6,1,2,2) -> 1*
    g11(1,1,2,2) -> 1*
    g11(6,1,2,6) -> 1*
    g11(6,2,2,1) -> 1*
    g11(1,1,2,6) -> 1*
    g11(1,2,2,1) -> 1*
    g11(6,6,2,1) -> 1*
    g11(1,6,2,1) -> 1*
    g11(2,2,2,2) -> 1*
    g11(2,6,2,2) -> 1*
    g11(2,2,2,6) -> 1*
    g11(2,6,2,6) -> 1*
    g11(6,2,1,6) -> 1*
    g11(6,6,1,6) -> 1*
    g11(1,6,1,6) -> 1*
    g11(2,1,1,6) -> 1*
    g11(6,2,1,2) -> 1*
    g11(6,1,6,2) -> 1*
    g11(6,6,1,2) -> 1*
    g11(1,1,6,2) -> 1*
    g11(1,6,1,2) -> 1*
    g11(6,1,1,1) -> 1*
    g11(1,1,1,1) -> 1*
    g11(6,1,6,6) -> 1*
    g11(6,2,6,1) -> 1*
    g11(1,1,6,6) -> 1*
    g11(1,2,6,1) -> 1*
    g11(6,6,6,1) -> 1*
    g11(1,6,6,1) -> 1*
    g11(2,1,1,2) -> 1*
    g11(2,2,6,2) -> 1*
    g11(2,2,1,1) -> 1*
    g11(2,6,6,2) -> 1*
    g11(2,1,6,1) -> 1*
    g11(2,6,1,1) -> 1*
    g11(2,2,6,6) -> 1*
    g11(2,6,6,6) -> 1*
    g11(6,2,2,2) -> 1*
    g11(1,2,2,2) -> 1*
    g11(6,6,2,2) -> 1*
    g11(1,6,2,2) -> 1*
    g11(6,1,2,1) -> 1*
    g11(1,1,2,1) -> 1*
    g11(6,2,2,6) -> 1*
    g11(1,2,2,6) -> 1*
    g11(6,6,2,6) -> 1*
    g11(1,6,2,6) -> 1*
    g11(2,2,2,1) -> 1*
    g11(6,1,1,6) -> 1*
    g11(2,6,2,1) -> 1*
    g11(1,1,1,6) -> 1*
    g11(2,2,1,6) -> 1*
    g11(2,6,1,6) -> 1*
    g11(6,1,1,2) -> 1*
    g11(1,1,1,2) -> 1*
    g11(6,2,6,2) -> 1*
    g11(1,2,6,2) -> 1*
    g11(6,2,1,1) -> 1*
    g11(6,6,6,2) -> 1*
    g11(1,6,6,2) -> 1*
    g11(6,1,6,1) -> 1*
    g11(6,6,1,1) -> 1*
    g11(1,1,6,1) -> 1*
    g11(6,2,6,6) -> 1*
    g11(1,6,1,1) -> 1*
    g11(1,2,6,6) -> 1*
    h2(6,2) -> 1*
    h2(6,6) -> 1*
    h2(1,6) -> 1*
    h2(2,1) -> 1*
    h2(6,1) -> 1*
    h2(1,1) -> 1*
    h2(2,6) -> 1*
    2 -> 1*
    6 -> 1*
  problem:
   
  Qed