YES

Problem:
 f(g(x),h(x),y,x) -> f(y,y,y,x)
 f(x,y,z,0()) -> 2()
 g(0()) -> 2()
 h(0()) -> 2()

Proof:
 Bounds Processor:
  bound: 2
  enrichment: top
  automaton:
   final states: {8,5,4,3,2,1}
   transitions:
    f0(4,4,2,5) -> 1*
    f0(8,3,4,4) -> 1*
    f0(2,4,3,5) -> 1*
    f0(2,1,4,1) -> 1*
    f0(1,5,8,8) -> 1*
    f0(2,8,4,2) -> 1*
    f0(2,5,1,3) -> 1*
    f0(5,5,8,5) -> 1*
    f0(3,3,4,4) -> 1*
    f0(1,4,3,2) -> 1*
    f0(4,5,8,2) -> 1*
    f0(4,2,5,3) -> 1*
    f0(8,5,4,4) -> 1*
    f0(4,2,1,8) -> 1*
    f0(2,3,4,1) -> 1*
    f0(8,2,1,5) -> 1*
    f0(5,8,2,8) -> 1*
    f0(3,5,4,4) -> 1*
    f0(3,2,1,5) -> 1*
    f0(5,2,2,2) -> 1*
    f0(4,4,5,3) -> 1*
    f0(4,1,2,4) -> 1*
    f0(4,8,2,5) -> 1*
    f0(4,4,1,8) -> 1*
    f0(2,5,4,1) -> 1*
    f0(2,1,3,4) -> 1*
    f0(2,8,3,5) -> 1*
    f0(8,4,1,5) -> 1*
    f0(2,2,1,2) -> 1*
    f0(5,2,8,4) -> 1*
    f0(3,4,1,5) -> 1*
    f0(1,1,3,1) -> 1*
    f0(1,8,3,2) -> 1*
    f0(5,4,2,2) -> 1*
    f0(4,2,8,1) -> 1*
    f0(4,3,2,4) -> 1*
    f0(8,2,4,3) -> 1*
    f0(2,3,3,4) -> 1*
    f0(2,4,1,2) -> 1*
    f0(1,1,5,8) -> 1*
    f0(5,4,8,4) -> 1*
    f0(5,1,5,5) -> 1*
    f0(3,2,4,3) -> 1*
    f0(1,3,3,1) -> 1*
    f0(4,4,8,1) -> 1*
    f0(4,1,5,2) -> 1*
    f0(4,8,5,3) -> 1*
    f0(4,5,2,4) -> 1*
    f0(8,4,4,3) -> 1*
    f0(4,8,1,8) -> 1*
    f0(2,5,3,4) -> 1*
    f0(8,8,1,5) -> 1*
    f0(8,1,1,4) -> 1*
    f0(1,3,5,8) -> 1*
    f0(5,3,5,5) -> 1*
    f0(3,4,4,3) -> 1*
    f0(3,1,1,4) -> 1*
    f0(3,8,1,5) -> 1*
    f0(1,5,3,1) -> 1*
    f0(5,1,2,1) -> 1*
    f0(5,8,2,2) -> 1*
    f0(4,3,5,2) -> 1*
    f0(8,3,1,4) -> 1*
    f0(2,1,1,1) -> 1*
    f0(5,1,8,3) -> 1*
    f0(5,8,8,4) -> 1*
    f0(1,5,5,8) -> 1*
    f0(2,8,1,2) -> 1*
    f0(5,5,5,5) -> 1*
    f0(5,1,4,8) -> 1*
    f0(3,3,1,4) -> 1*
    f0(2,1,3,8) -> 1*
    f0(5,3,2,1) -> 1*
    f0(4,8,8,1) -> 1*
    f0(4,5,5,2) -> 1*
    f0(4,1,4,5) -> 1*
    f0(8,8,4,3) -> 1*
    f0(8,1,4,2) -> 1*
    f0(2,2,3,3) -> 1*
    f0(8,5,1,4) -> 1*
    f0(2,3,1,1) -> 1*
    f0(5,3,8,3) -> 1*
    f0(5,3,4,8) -> 1*
    f0(3,1,4,2) -> 1*
    f0(3,8,4,3) -> 1*
    f0(3,5,1,4) -> 1*
    f0(2,3,3,8) -> 1*
    f0(5,5,2,1) -> 1*
    f0(4,3,4,5) -> 1*
    f0(8,3,4,2) -> 1*
    f0(2,4,3,3) -> 1*
    f0(2,5,1,1) -> 1*
    f0(5,5,8,3) -> 1*
    f0(5,2,5,4) -> 1*
    f0(5,5,4,8) -> 1*
    f0(3,3,4,2) -> 1*
    f0(2,5,3,8) -> 1*
    f0(4,5,4,5) -> 1*
    f0(4,2,5,1) -> 1*
    f0(8,5,4,2) -> 1*
    f0(8,1,3,5) -> 1*
    f0(8,2,1,3) -> 1*
    f0(5,4,5,4) -> 1*
    f0(1,1,2,8) -> 1*
    f0(5,1,2,5) -> 1*
    f0(3,5,4,2) -> 1*
    f0(3,1,3,5) -> 1*
    f0(2,2,8,8) -> 1*
    f0(3,2,1,3) -> 1*
    f0(1,2,2,3) -> 1*
    f0(4,4,5,1) -> 1*
    f0(8,3,3,5) -> 1*
    f0(4,8,2,3) -> 1*
    f0(2,1,3,2) -> 1*
    f0(8,4,1,3) -> 1*
    f0(1,2,8,5) -> 1*
    f0(2,8,3,3) -> 1*
    f0(5,2,8,2) -> 1*
    f0(1,3,2,8) -> 1*
    f0(5,3,2,5) -> 1*
    f0(3,3,3,5) -> 1*
    f0(2,4,8,8) -> 1*
    f0(3,4,1,3) -> 1*
    f0(1,4,2,3) -> 1*
    f0(4,2,4,4) -> 1*
    f0(8,5,3,5) -> 1*
    f0(8,2,4,1) -> 1*
    f0(2,3,3,2) -> 1*
    f0(1,4,8,5) -> 1*
    f0(5,4,8,2) -> 1*
    f0(5,1,5,3) -> 1*
    f0(1,5,2,8) -> 1*
    f0(5,8,5,4) -> 1*
    f0(5,5,2,5) -> 1*
    f0(5,1,1,8) -> 1*
    f0(3,5,3,5) -> 1*
    f0(3,2,4,1) -> 1*
    f0(4,4,4,4) -> 1*
    f0(4,8,5,1) -> 1*
    f0(4,1,1,5) -> 1*
    f0(8,4,4,1) -> 1*
    f0(2,5,3,2) -> 1*
    f0(8,8,1,3) -> 1*
    f0(8,1,1,2) -> 1*
    f0(5,3,5,3) -> 1*
    f0(5,3,1,8) -> 1*
    f0(3,4,4,1) -> 1*
    f0(2,8,8,8) -> 1*
    f0(3,1,1,2) -> 1*
    f0(3,8,1,3) -> 1*
    f0(1,1,2,2) -> 1*
    f0(4,3,1,5) -> 1*
    f0(8,2,3,4) -> 1*
    f0(8,3,1,2) -> 1*
    f0(1,8,8,5) -> 1*
    f0(1,1,8,4) -> 1*
    f0(5,8,8,2) -> 1*
    f0(5,1,8,1) -> 1*
    f0(5,5,5,3) -> 1*
    f0(5,2,2,4) -> 1*
    f0(5,5,1,8) -> 1*
    f0(3,2,3,4) -> 1*
    f0(3,3,1,2) -> 1*
    f0(1,3,2,2) -> 1*
    f0(4,1,4,3) -> 1*
    f0(4,8,4,4) -> 1*
    f0(4,5,1,5) -> 1*
    f0(8,4,3,4) -> 1*
    f0(8,8,4,1) -> 1*
    f0(2,2,3,1) -> 1*
    f0(8,5,1,2) -> 1*
    f0(1,3,8,4) -> 1*
    f0(5,3,8,1) -> 1*
    f0(5,4,2,4) -> 1*
    f0(3,4,3,4) -> 1*
    f0(3,8,4,1) -> 1*
    f0(3,5,1,2) -> 1*
    f0(2,2,5,8) -> 1*
    f0(1,5,2,2) -> 1*
    f0(4,3,4,3) -> 1*
    f0(2,4,3,1) -> 1*
    f0(1,5,8,4) -> 1*
    f0(1,2,5,5) -> 1*
    f0(5,5,8,1) -> 1*
    f0(5,2,5,2) -> 1*
    f0(2,4,5,8) -> 1*
    f0(4,5,4,3) -> 1*
    f0(4,2,1,4) -> 1*
    f0(8,1,3,3) -> 1*
    f0(8,8,3,4) -> 1*
    f0(8,2,1,1) -> 1*
    f0(1,4,5,5) -> 1*
    f0(5,4,5,2) -> 1*
    f0(5,8,2,4) -> 1*
    f0(3,1,3,3) -> 1*
    f0(3,8,3,4) -> 1*
    f0(3,2,1,1) -> 1*
    f0(8,2,3,8) -> 1*
    f0(1,2,2,1) -> 1*
    f0(4,4,1,4) -> 1*
    f0(8,3,3,3) -> 1*
    f0(8,4,1,1) -> 1*
    f0(1,2,8,3) -> 1*
    f0(3,2,3,8) -> 1*
    f0(2,8,3,1) -> 1*
    f0(1,2,4,8) -> 1*
    f0(5,2,4,5) -> 1*
    f0(3,3,3,3) -> 1*
    f0(3,4,1,1) -> 1*
    f0(8,4,3,8) -> 1*
    f0(2,8,5,8) -> 1*
    f0(1,4,2,1) -> 1*
    f0(4,2,4,2) -> 1*
    f0(8,5,3,3) -> 1*
    f0(1,4,8,3) -> 1*
    f0(3,4,3,8) -> 1*
    f0(1,1,5,4) -> 1*
    f0(1,4,4,8) -> 1*
    f0(1,8,5,5) -> 1*
    f0(5,4,4,5) -> 1*
    f0(5,1,5,1) -> 1*
    f0(5,8,5,2) -> 1*
    f0(5,5,2,3) -> 1*
    f0(8,1,8,8) -> 1*
    f0(3,5,3,3) -> 1*
    f0(4,4,4,2) -> 1*
    f0(3,1,8,8) -> 1*
    f0(4,1,1,3) -> 1*
    f0(4,8,1,4) -> 1*
    f0(2,1,2,3) -> 1*
    f0(8,8,1,1) -> 1*
    f0(1,3,5,4) -> 1*
    f0(5,3,5,1) -> 1*
    f0(8,3,8,8) -> 1*
    f0(2,1,8,5) -> 1*
    f0(8,8,3,8) -> 1*
    f0(3,8,1,1) -> 1*
    f0(2,2,2,8) -> 1*
    f0(1,8,2,1) -> 1*
    f0(4,2,3,5) -> 1*
    f0(3,3,8,8) -> 1*
    f0(4,3,1,3) -> 1*
    f0(8,2,3,2) -> 1*
    f0(2,3,2,3) -> 1*
    f0(1,8,8,3) -> 1*
    f0(1,1,8,2) -> 1*
    f0(3,8,3,8) -> 1*
    f0(1,5,5,4) -> 1*
    f0(1,8,4,8) -> 1*
    f0(1,2,2,5) -> 1*
    f0(5,5,5,1) -> 1*
    f0(5,1,4,4) -> 1*
    f0(5,8,4,5) -> 1*
    f0(8,5,8,8) -> 1*
    f0(3,2,3,2) -> 1*
    f0(2,3,8,5) -> 1*
    f0(2,4,2,8) -> 1*
    f0(4,4,3,5) -> 1*
    f0(4,1,4,1) -> 1*
    f0(3,5,8,8) -> 1*
    f0(4,8,4,2) -> 1*
    f0(4,5,1,3) -> 1*
    f0(8,4,3,2) -> 1*
    f0(1,3,8,2) -> 1*
    f0(1,4,2,5) -> 1*
    f0(5,3,4,4) -> 1*
    f0(3,4,3,2) -> 1*
    f0(2,5,8,5) -> 1*
    f0(4,3,4,1) -> 1*
    f0(1,5,8,2) -> 1*
    f0(1,2,5,3) -> 1*
    f0(5,5,4,4) -> 1*
    f0(1,2,1,8) -> 1*
    f0(5,2,1,5) -> 1*
    f0(2,8,2,8) -> 1*
    f0(4,5,4,1) -> 1*
    f0(4,1,3,4) -> 1*
    f0(4,8,3,5) -> 1*
    f0(4,2,1,2) -> 1*
    f0(8,8,3,2) -> 1*
    f0(8,1,3,1) -> 1*
    f0(2,2,2,2) -> 1*
    f0(1,4,5,3) -> 1*
    f0(1,1,2,4) -> 1*
    f0(1,4,1,8) -> 1*
    f0(1,8,2,5) -> 1*
    f0(5,4,1,5) -> 1*
    f0(3,1,3,1) -> 1*
    f0(8,1,5,8) -> 1*
    f0(2,2,8,4) -> 1*
    f0(3,8,3,2) -> 1*
    f0(4,3,3,4) -> 1*
    f0(4,4,1,2) -> 1*
    f0(3,1,5,8) -> 1*
    f0(8,3,3,1) -> 1*
    f0(2,4,2,2) -> 1*
    f0(1,2,8,1) -> 1*
    f0(1,3,2,4) -> 1*
    f0(5,2,4,3) -> 1*
    f0(3,3,3,1) -> 1*
    f0(8,3,5,8) -> 1*
    f0(2,4,8,4) -> 1*
    f0(2,1,5,5) -> 1*
    f0(4,5,3,4) -> 1*
    f0(3,3,5,8) -> 1*
    f0(8,5,3,1) -> 1*
    f0(1,4,8,1) -> 1*
    f0(1,1,5,2) -> 1*
    f0(1,8,5,3) -> 1*
    f0(1,5,2,4) -> 1*
    f0(5,4,4,3) -> 1*
    f0(1,8,1,8) -> 1*
    f0(5,1,1,4) -> 1*
    f0(5,8,1,5) -> 1*
    f0(3,5,3,1) -> 1*
    f0(8,5,5,8) -> 1*
    f0(2,3,5,5) -> 1*
    f0(4,1,1,1) -> 1*
    f0(3,5,5,8) -> 1*
    f0(4,8,1,2) -> 1*
    f0(2,1,2,1) -> 1*
    f0(2,8,2,2) -> 1*
    f0(1,3,5,2) -> 1*
    f0(5,3,1,4) -> 1*
    f0(2,1,8,3) -> 1*
    f0(2,8,8,4) -> 1*
    f0(4,1,3,8) -> 1*
    f0(2,5,5,5) -> 1*
    f0(2,1,4,8) -> 1*
    f0(4,2,3,3) -> 1*
    f0(4,3,1,1) -> 1*
    f0(2,3,2,1) -> 1*
    f0(1,8,8,1) -> 1*
    f0(1,5,5,2) -> 1*
    f0(1,1,4,5) -> 1*
    f0(5,1,4,2) -> 1*
    f0(5,8,4,3) -> 1*
    f0(5,5,1,4) -> 1*
    f0(2,3,8,3) -> 1*
    f0(4,3,3,8) -> 1*
    f0(2,3,4,8) -> 1*
    f0(4,4,3,3) -> 1*
    f0(4,5,1,1) -> 1*
    f0(2,5,2,1) -> 1*
    f0(1,3,4,5) -> 1*
    f0(5,3,4,2) -> 1*
    f0(4,5,3,8) -> 1*
    f0(2,5,8,3) -> 1*
    f0(2,2,5,4) -> 1*
    f0(8,1,2,8) -> 1*
    f0(2,5,4,8) -> 1*
    f0(8,2,2,3) -> 1*
    f0(3,1,2,8) -> 1*
    f0(1,5,4,5) -> 1*
    f0(1,2,5,1) -> 1*
    f0(5,5,4,2) -> 1*
    f0(5,1,3,5) -> 1*
    f0(4,2,8,8) -> 1*
    f0(5,2,1,3) -> 1*
    f0(8,2,8,5) -> 1*
    f0(3,2,2,3) -> 1*
    f0(2,4,5,4) -> 1*
    f0(8,3,2,8) -> 1*
    f0(2,1,2,5) -> 1*
    f0(4,1,3,2) -> 1*
    f0(4,8,3,3) -> 1*
    f0(3,2,8,5) -> 1*
    f0(8,4,2,3) -> 1*
    f0(3,3,2,8) -> 1*
    f0(1,4,5,1) -> 1*
    f0(5,3,3,5) -> 1*
    f0(4,4,8,8) -> 1*
    f0(1,8,2,3) -> 1*
    f0(5,4,1,3) -> 1*
    f0(8,4,8,5) -> 1*
    f0(3,4,2,3) -> 1*
    f0(2,2,8,2) -> 1*
    f0(8,5,2,8) -> 1*
    f0(2,3,2,5) -> 1*
    f0(4,3,3,2) -> 1*
    f0(3,4,8,5) -> 1*
    f0(3,5,2,8) -> 1*
    f0(1,2,4,4) -> 1*
    f0(5,5,3,5) -> 1*
    f0(5,2,4,1) -> 1*
    f0(2,4,8,2) -> 1*
    f0(2,1,5,3) -> 1*
    f0(2,8,5,4) -> 1*
    f0(2,5,2,5) -> 1*
    f0(2,1,1,8) -> 1*
    f0(4,5,3,2) -> 1*
    f0(8,1,2,2) -> 1*
    f0(1,4,4,4) -> 1*
    f0(1,8,5,1) -> 1*
    f0(1,1,1,5) -> 1*
    f0(5,4,4,1) -> 1*
    f0(4,8,8,8) -> 1*
    f0(5,1,1,2) -> 1*
    f0(8,8,8,5) -> 1*
    f0(8,1,8,4) -> 1*
    f0(5,8,1,3) -> 1*
    f0(3,1,2,2) -> 1*
    f0(2,3,5,3) -> 1*
    f0(2,3,1,8) -> 1*
    f0(3,8,8,5) -> 1*
    f0(3,1,8,4) -> 1*
    f0(8,3,2,2) -> 1*
    f0(1,3,1,5) -> 1*
    f0(5,2,3,4) -> 1*
    f0(5,3,1,2) -> 1*
    f0(8,3,8,4) -> 1*
    f0(3,3,2,2) -> 1*
    f0(2,8,8,2) -> 1*
    f0(2,1,8,1) -> 1*
    f0(2,5,5,3) -> 1*
    f0(2,2,2,4) -> 1*
    f0(2,5,1,8) -> 1*
    f0(4,2,3,1) -> 1*
    f0(3,3,8,4) -> 1*
    f0(8,5,2,2) -> 1*
    f0(1,1,4,3) -> 1*
    f0(1,8,4,4) -> 1*
    f0(1,5,1,5) -> 1*
    f0(5,4,3,4) -> 1*
    f0(5,8,4,1) -> 1*
    f0(5,5,1,2) -> 1*
    f0(4,2,5,8) -> 1*
    f0(8,5,8,4) -> 1*
    f0(3,5,2,2) -> 1*
    f0(8,2,5,5) -> 1*
    f0(2,3,8,1) -> 1*
    f0(2,4,2,4) -> 1*
    f0(4,4,3,1) -> 1*
    f0(3,5,8,4) -> 1*
    f0(3,2,5,5) -> 1*
    f0(1,3,4,3) -> 1*
    f0(4,4,5,8) -> 1*
    f0(8,4,5,5) -> 1*
    f0(2,5,8,1) -> 1*
    f0(2,2,5,2) -> 1*
    f0(3,4,5,5) -> 1*
    f0(8,2,2,1) -> 1*
    f0(1,5,4,3) -> 1*
    f0(1,2,1,4) -> 1*
    f0(5,1,3,3) -> 1*
    f0(5,8,3,4) -> 1*
    f0(5,2,1,1) -> 1*
    f0(8,2,8,3) -> 1*
    f0(3,2,2,1) -> 1*
    f0(8,2,4,8) -> 1*
    f0(2,4,5,2) -> 1*
    f0(2,8,2,4) -> 1*
    f0(5,2,3,8) -> 1*
    f0(4,8,3,1) -> 1*
    f0(3,2,8,3) -> 1*
    f0(3,2,4,8) -> 1*
    f0(8,4,2,1) -> 1*
    f0(1,4,1,4) -> 1*
    f0(5,3,3,3) -> 1*
    f0(5,4,1,1) -> 1*
    f0(4,8,5,8) -> 1*
    f0(8,4,8,3) -> 1*
    f0(3,4,2,1) -> 1*
    f0(8,4,4,8) -> 1*
    f0(8,8,5,5) -> 1*
    f0(8,1,5,4) -> 1*
    f0(2,2,4,5) -> 1*
    f0(5,4,3,8) -> 1*
    f0(3,4,8,3) -> 1*
    f0(3,1,5,4) -> 1*
    f0(3,4,4,8) -> 1*
    f0(3,8,5,5) -> 1*
    f0(1,2,4,2) -> 1*
    f0(5,5,3,3) -> 1*
    f0(8,3,5,4) -> 1*
    f0(2,4,4,5) -> 1*
    f0(2,1,5,1) -> 1*
    f0(2,8,5,2) -> 1*
    f0(2,5,2,3) -> 1*
    f0(5,1,8,8) -> 1*
    f0(4,1,2,3) -> 1*
    f0(3,3,5,4) -> 1*
    f0(8,8,2,1) -> 1*
    f0(1,4,4,2) -> 1*
    f0(1,1,1,3) -> 1*
    f0(1,8,1,4) -> 1*
    f0(4,1,8,5) -> 1*
    f0(8,8,8,3) -> 1*
    f0(8,1,8,2) -> 1*
    f0(5,8,1,1) -> 1*
    f0(4,2,2,8) -> 1*
    f0(8,8,4,8) -> 1*
    f0(3,8,2,1) -> 1*
    f0(8,5,5,4) -> 1*
    f0(2,3,5,1) -> 1*
    f0(8,2,2,5) -> 1*
    f0(5,3,8,8) -> 1*
    f0(4,3,2,3) -> 1*
    f0(3,8,8,3) -> 1*
    f0(5,8,3,8) -> 1*
    f0(3,1,8,2) -> 1*
    f0(3,5,5,4) -> 1*
    f0(3,8,4,8) -> 1*
    f0(3,2,2,5) -> 1*
    f0(1,2,3,5) -> 1*
    f0(1,3,1,3) -> 1*
    f0(5,2,3,2) -> 1*
    f0(4,3,8,5) -> 1*
    f0(8,3,8,2) -> 1*
    f0(4,4,2,8) -> 1*
    f0(2,5,5,1) -> 1*
    f0(2,1,4,4) -> 1*
    f0(2,8,4,5) -> 1*
    f0(8,4,2,5) -> 1*
    f0(5,5,8,8) -> 1*
    f0(3,3,8,2) -> 1*
    f0(3,4,2,5) -> 1*
    f0(1,4,3,5) -> 1*
    f0(1,1,4,1) -> 1*
    f0(1,8,4,2) -> 1*
    f0(1,5,1,3) -> 1*
    f0(5,4,3,2) -> 1*
    f0(4,5,8,5) -> 1*
    f0(8,5,8,2) -> 1*
    f0(8,2,5,3) -> 1*
    f0(2,3,4,4) -> 1*
    f0(8,2,1,8) -> 1*
    f0(3,5,8,2) -> 1*
    f0(3,2,5,3) -> 1*
    f0(3,2,1,8) -> 1*
    f0(1,3,4,1) -> 1*
    f0(4,8,2,8) -> 1*
    f0(8,4,5,3) -> 1*
    f0(2,5,4,4) -> 1*
    f0(8,4,1,8) -> 1*
    f0(8,8,2,5) -> 1*
    f0(8,1,2,4) -> 1*
    f0(2,2,1,5) -> 1*
    f0(4,2,2,2) -> 1*
    f0(3,4,5,3) -> 1*
    f0(3,1,2,4) -> 1*
    f0(3,8,2,5) -> 1*
    f0(3,4,1,8) -> 1*
    f0(1,5,4,1) -> 1*
    f0(1,1,3,4) -> 1*
    f0(1,8,3,5) -> 1*
    f0(1,2,1,2) -> 1*
    f0(5,1,3,1) -> 1*
    f0(5,8,3,2) -> 1*
    f0(4,2,8,4) -> 1*
    f0(8,2,8,1) -> 1*
    f0(8,3,2,4) -> 1*
    f0(2,4,1,5) -> 1*
    f0(5,1,5,8) -> 1*
    f0(4,4,2,2) -> 1*
    f0(3,2,8,1) -> 1*
    f0(3,3,2,4) -> 1*
    f0(1,3,3,4) -> 1*
    f0(1,4,1,2) -> 1*
    f0(5,3,3,1) -> 1*
    f0(4,4,8,4) -> 1*
    f0(4,1,5,5) -> 1*
    f0(8,4,8,1) -> 1*
    f0(8,8,5,3) -> 1*
    f0(8,1,5,2) -> 1*
    f0(2,2,4,3) -> 1*
    f0(8,8,1,8) -> 1*
    f0(8,5,2,4) -> 1*
    f0(5,3,5,8) -> 1*
    f0(3,4,8,1) -> 1*
    f0(3,1,5,2) -> 1*
    f0(3,8,5,3) -> 1*
    f0(3,5,2,4) -> 1*
    f0(3,8,1,8) -> 1*
    f0(1,5,3,4) -> 1*
    f0(5,5,3,1) -> 1*
    f0(4,3,5,5) -> 1*
    f0(8,3,5,2) -> 1*
    f0(2,4,4,3) -> 1*
    f0(2,1,1,4) -> 1*
    f0(2,8,1,5) -> 1*
    f0(5,5,5,8) -> 1*
    f0(4,1,2,1) -> 1*
    f0(4,8,2,2) -> 1*
    f0(3,3,5,2) -> 1*
    f0(1,1,1,1) -> 1*
    f0(4,8,8,4) -> 1*
    f0(1,8,1,2) -> 1*
    f0(4,1,8,3) -> 1*
    f0(4,5,5,5) -> 1*
    f0(8,8,8,1) -> 1*
    f0(4,1,4,8) -> 1*
    f0(8,5,5,2) -> 1*
    f0(8,1,4,5) -> 1*
    f0(2,3,1,4) -> 1*
    f0(1,1,3,8) -> 1*
    f0(4,3,2,1) -> 1*
    f0(3,8,8,1) -> 1*
    f0(3,5,5,2) -> 1*
    f0(3,1,4,5) -> 1*
    f0(1,2,3,3) -> 1*
    f0(1,3,1,1) -> 1*
    f0(4,3,8,3) -> 1*
    f0(4,3,4,8) -> 1*
    f0(8,3,4,5) -> 1*
    f0(2,1,4,2) -> 1*
    f0(2,8,4,3) -> 1*
    f0(2,5,1,4) -> 1*
    f0(1,3,3,8) -> 1*
    f0(4,5,2,1) -> 1*
    f0(3,3,4,5) -> 1*
    f0(1,4,3,3) -> 1*
    f0(1,5,1,1) -> 1*
    f0(4,5,8,3) -> 1*
    f0(4,2,5,4) -> 1*
    f0(4,5,4,8) -> 1*
    f0(8,5,4,5) -> 1*
    f0(8,2,5,1) -> 1*
    f0(2,3,4,2) -> 1*
    f0(1,5,3,8) -> 1*
    f0(5,1,2,8) -> 1*
    f0(3,5,4,5) -> 1*
    f0(3,2,5,1) -> 1*
    f0(5,2,2,3) -> 1*
    f0(4,4,5,4) -> 1*
    f0(4,1,2,5) -> 1*
    f0(8,4,5,1) -> 1*
    f0(2,5,4,2) -> 1*
    f0(2,1,3,5) -> 1*
    f0(1,2,8,8) -> 1*
    f0(8,8,2,3) -> 1*
    f0(2,2,1,3) -> 1*
    f0(5,2,8,5) -> 1*
    f0(5,3,2,8) -> 1*
    f0(3,4,5,1) -> 1*
    f0(3,8,2,3) -> 1*
    f0(1,1,3,2) -> 1*
    f0(1,8,3,3) -> 1*
    f0(5,4,2,3) -> 1*
    f0(4,2,8,2) -> 1*
    f0(4,3,2,5) -> 1*
    f0(8,2,4,4) -> 1*
    f0(2,3,3,5) -> 1*
    f0(1,4,8,8) -> 1*
    f0(2,4,1,3) -> 1*
    f0(5,4,8,5) -> 1*
    f0(5,5,2,8) -> 1*
    f0(3,2,4,4) -> 1*
    f0(1,3,3,2) -> 1*
    f0(4,4,8,2) -> 1*
    f0(4,1,5,3) -> 1*
    f0(4,8,5,4) -> 1*
    f0(4,5,2,5) -> 1*
    f0(8,8,5,1) -> 1*
    f0(8,4,4,4) -> 1*
    f0(4,1,1,8) -> 1*
    f0(2,5,3,5) -> 1*
    f0(2,2,4,1) -> 1*
    f0(8,1,1,5) -> 1*
    f0(3,4,4,4) -> 1*
    f0(3,8,5,1) -> 1*
    f0(3,1,1,5) -> 1*
    f0(1,5,3,2) -> 1*
    f0(5,1,2,2) -> 1*
    f0(4,3,5,3) -> 1*
    f0(4,3,1,8) -> 1*
    f0(2,4,4,1) -> 1*
    f0(1,8,8,8) -> 1*
    f0(8,3,1,5) -> 1*
    f0(2,1,1,2) -> 1*
    f0(2,8,1,3) -> 1*
    f0(5,1,8,4) -> 1*
    f0(5,8,8,5) -> 1*
    f0(3,3,1,5) -> 1*
    f0(5,3,2,2) -> 1*
    f0(4,8,8,2) -> 1*
    f0(4,1,8,1) -> 1*
    f0(4,5,5,3) -> 1*
    f0(4,2,2,4) -> 1*
    f0(8,8,4,4) -> 1*
    f0(8,1,4,3) -> 1*
    f0(4,5,1,8) -> 1*
    f0(2,2,3,4) -> 1*
    f0(8,5,1,5) -> 1*
    f0(2,3,1,2) -> 1*
    f0(5,3,8,4) -> 1*
    f0(3,1,4,3) -> 1*
    f0(3,8,4,4) -> 1*
    f0(3,5,1,5) -> 1*
    f0(1,2,3,1) -> 1*
    f0(5,5,2,2) -> 1*
    f0(4,3,8,1) -> 1*
    f0(4,4,2,4) -> 1*
    f0(8,3,4,3) -> 1*
    f0(2,4,3,4) -> 1*
    f0(2,8,4,1) -> 1*
    f0(2,5,1,2) -> 1*
    f0(5,5,8,4) -> 1*
    f0(1,2,5,8) -> 1*
    f0(5,2,5,5) -> 1*
    f0(3,3,4,3) -> 1*
    f0(1,4,3,1) -> 1*
    f0(4,5,8,1) -> 1*
    f0(4,2,5,2) -> 1*
    f0(8,5,4,3) -> 1*
    f0(8,2,1,4) -> 1*
    f0(1,4,5,8) -> 1*
    f0(5,4,5,5) -> 1*
    f0(3,5,4,3) -> 1*
    f0(3,2,1,4) -> 1*
    f0(5,2,2,1) -> 1*
    f0(4,4,5,2) -> 1*
    f0(4,8,2,4) -> 1*
    f0(2,1,3,3) -> 1*
    f0(8,4,1,4) -> 1*
    f0(2,8,3,4) -> 1*
    f0(2,2,1,1) -> 1*
    f0(5,2,8,3) -> 1*
    f0(5,2,4,8) -> 1*
    f0(3,4,1,4) -> 1*
    f0(2,2,3,8) -> 1*
    f0(1,8,3,1) -> 1*
    f0(5,4,2,1) -> 1*
    f0(4,2,4,5) -> 1*
    f0(8,2,4,2) -> 1*
    f0(2,3,3,3) -> 1*
    f0(2,4,1,1) -> 1*
    f0(5,4,8,3) -> 1*
    f0(1,8,5,8) -> 1*
    f0(5,1,5,4) -> 1*
    f0(5,4,4,8) -> 1*
    f0(5,8,5,5) -> 1*
    f0(3,2,4,2) -> 1*
    f0(2,4,3,8) -> 1*
    f0(4,4,4,5) -> 1*
    f0(4,1,5,1) -> 1*
    f0(4,8,5,2) -> 1*
    f0(4,5,2,3) -> 1*
    f0(8,4,4,2) -> 1*
    f0(2,5,3,3) -> 1*
    f0(8,1,1,3) -> 1*
    f0(8,8,1,4) -> 1*
    f0(5,3,5,4) -> 1*
    f0(3,4,4,2) -> 1*
    f0(2,1,8,8) -> 1*
    f0(3,1,1,3) -> 1*
    f0(3,8,1,4) -> 1*
    f0(1,1,2,3) -> 1*
    f0(5,8,2,1) -> 1*
    f0(4,3,5,1) -> 1*
    f0(8,2,3,5) -> 1*
    f0(8,3,1,3) -> 1*
    f0(1,1,8,5) -> 1*
    f0(5,8,8,3) -> 1*
    f0(5,1,8,2) -> 1*
    f0(2,8,1,1) -> 1*
    f0(5,5,5,4) -> 1*
    f0(5,8,4,8) -> 1*
    f0(1,2,2,8) -> 1*
    f0(5,2,2,5) -> 1*
    f0(3,2,3,5) -> 1*
    f0(2,3,8,8) -> 1*
    f0(3,3,1,3) -> 1*
    f0(1,3,2,3) -> 1*
    f0(2,8,3,8) -> 1*
    f0(4,5,5,1) -> 1*
    f0(4,1,4,4) -> 1*
    f0(4,8,4,5) -> 1*
    f0(8,8,4,2) -> 1*
    f0(8,4,3,5) -> 1*
    f0(8,1,4,1) -> 1*
    f0(2,2,3,2) -> 1*
    f0(1,3,8,5) -> 1*
    f0(8,5,1,3) -> 1*
    f0(5,3,8,2) -> 1*
    f0(1,4,2,8) -> 1*
    f0(5,4,2,5) -> 1*
    f0(3,4,3,5) -> 1*
    f0(3,1,4,1) -> 1*
    f0(2,5,8,8) -> 1*
    f0(3,8,4,2) -> 1*
    f0(3,5,1,3) -> 1*
    f0(4,3,4,4) -> 1*
    f0(8,3,4,1) -> 1*
    f0(2,4,3,2) -> 1*
    f0(1,5,8,5) -> 1*
    f0(5,5,8,2) -> 1*
    f0(5,2,5,3) -> 1*
    f0(5,2,1,8) -> 1*
    f0(3,3,4,1) -> 1*
    f0(4,5,4,4) -> 1*
    f0(4,2,1,5) -> 1*
    f0(8,8,3,5) -> 1*
    f0(8,5,4,1) -> 1*
    f0(8,1,3,4) -> 1*
    f0(8,2,1,2) -> 1*
    f0(5,4,5,3) -> 1*
    f0(1,8,2,8) -> 1*
    f0(5,1,2,4) -> 1*
    f0(5,4,1,8) -> 1*
    f0(5,8,2,5) -> 1*
    f0(3,5,4,1) -> 1*
    f0(3,1,3,4) -> 1*
    f0(3,8,3,5) -> 1*
    f0(3,2,1,2) -> 1*
    f0(1,2,2,2) -> 1*
    f0(4,4,1,5) -> 1*
    f0(8,3,3,4) -> 1*
    f0(2,1,3,1) -> 1*
    f0(1,2,8,4) -> 1*
    f0(8,4,1,2) -> 1*
    f0(2,8,3,2) -> 1*
    f0(5,2,8,1) -> 1*
    f0(5,3,2,4) -> 1*
    f0(3,3,3,4) -> 1*
    f0(3,4,1,2) -> 1*
    f0(2,1,5,8) -> 1*
    f0(1,4,2,2) -> 1*
    f0(4,2,4,3) -> 1*
    f0(8,5,3,4) -> 1*
    f0(2,3,3,1) -> 1*
    f0(1,4,8,4) -> 1*
    f0(1,1,5,5) -> 1*
    f0(5,4,8,1) -> 1*
    f0(5,1,5,2) -> 1*
    f0(5,8,5,3) -> 1*
    f0(5,5,2,4) -> 1*
    f0(5,8,1,8) -> 1*
    f0(3,5,3,4) -> 1*
    f0(2,3,5,8) -> 1*
    f0(4,4,4,3) -> 1*
    f0(4,1,1,4) -> 1*
    f0(4,8,1,5) -> 1*
    f0(2,5,3,1) -> 1*
    f0(8,8,1,2) -> 1*
    f0(8,1,1,1) -> 1*
    f0(1,3,5,5) -> 1*
    f0(5,3,5,2) -> 1*
    f0(3,1,1,1) -> 1*
    f0(8,1,3,8) -> 1*
    f0(2,5,5,8) -> 1*
    f0(3,8,1,2) -> 1*
    f0(1,1,2,1) -> 1*
    f0(1,8,2,2) -> 1*
    f0(4,3,1,4) -> 1*
    f0(8,2,3,3) -> 1*
    f0(1,1,8,3) -> 1*
    f0(1,8,8,4) -> 1*
    f0(8,3,1,1) -> 1*
    f0(3,1,3,8) -> 1*
    f0(1,5,5,5) -> 1*
    f0(5,8,8,1) -> 1*
    f0(1,1,4,8) -> 1*
    f0(5,5,5,2) -> 1*
    f0(5,1,4,5) -> 1*
    f0(3,2,3,3) -> 1*
    f0(3,3,1,1) -> 1*
    f0(8,3,3,8) -> 1*
    f0(1,3,2,1) -> 1*
    f0(4,1,4,2) -> 1*
    f0(4,8,4,3) -> 1*
    f0(4,5,1,4) -> 1*
    f0(8,4,3,3) -> 1*
    f0(1,3,8,3) -> 1*
    f0(8,5,1,1) -> 1*
    f0(3,3,3,8) -> 1*
    f0(1,3,4,8) -> 1*
    f0(5,3,4,5) -> 1*
    f0(3,4,3,3) -> 1*
    f0(3,5,1,1) -> 1*
    f0(8,5,3,8) -> 1*
    f0(1,5,2,1) -> 1*
    f0(4,3,4,2) -> 1*
    f0(1,5,8,3) -> 1*
    f0(3,5,3,8) -> 1*
    f0(1,2,5,4) -> 1*
    f0(1,5,4,8) -> 1*
    f0(5,5,4,5) -> 1*
    f0(5,2,5,1) -> 1*
    f0(8,2,8,8) -> 1*
    f0(2,1,2,8) -> 1*
    f0(4,5,4,2) -> 1*
    f0(4,1,3,5) -> 1*
    f0(3,2,8,8) -> 1*
    f0(4,2,1,3) -> 1*
    f0(8,8,3,3) -> 1*
    f0(8,1,3,2) -> 1*
    f0(2,2,2,3) -> 1*
    f0(1,4,5,4) -> 1*
    f0(1,1,2,5) -> 1*
    f0(5,4,5,1) -> 1*
    f0(5,8,2,3) -> 1*
    f0(8,4,8,8) -> 1*
    f0(3,1,3,2) -> 1*
    f0(2,2,8,5) -> 1*
    f0(3,8,3,3) -> 1*
    f0(2,3,2,8) -> 1*
    f0(4,3,3,5) -> 1*
    f0(3,4,8,8) -> 1*
    f0(4,4,1,3) -> 1*
    f0(8,3,3,2) -> 1*
    f0(2,4,2,3) -> 1*
    f0(1,2,8,2) -> 1*
    f0(1,3,2,5) -> 1*
    f0(5,2,4,4) -> 1*
    f0(3,3,3,2) -> 1*
    f0(2,4,8,5) -> 1*
    f0(2,5,2,8) -> 1*
    f0(4,5,3,5) -> 1*
    f0(4,2,4,1) -> 1*
    f0(8,5,3,2) -> 1*
    f0(1,4,8,2) -> 1*
    f0(1,1,5,3) -> 1*
    f0(1,8,5,4) -> 1*
    f0(1,5,2,5) -> 1*
    f0(5,4,4,4) -> 1*
    f0(1,1,1,8) -> 1*
    f0(5,8,5,1) -> 1*
    f0(5,1,1,5) -> 1*
    f0(8,8,8,8) -> 1*
    f0(3,5,3,2) -> 1*
    f0(4,4,4,1) -> 1*
    f0(3,8,8,8) -> 1*
    f0(4,1,1,2) -> 1*
    f0(4,8,1,3) -> 1*
    f0(2,1,2,2) -> 1*
    f0(1,3,5,3) -> 1*
    f0(1,3,1,8) -> 1*
    f0(5,3,1,5) -> 1*
    f0(2,8,8,5) -> 1*
    f0(2,1,8,4) -> 1*
    f0(4,2,3,4) -> 1*
    f0(4,3,1,2) -> 1*
    f0(8,2,3,1) -> 1*
    f0(2,3,2,2) -> 1*
    f0(1,8,8,2) -> 1*
    f0(1,1,8,1) -> 1*
    f0(1,5,5,3) -> 1*
    f0(1,2,2,4) -> 1*
    f0(5,1,4,3) -> 1*
    f0(1,5,1,8) -> 1*
    f0(5,8,4,4) -> 1*
    f0(5,5,1,5) -> 1*
    f0(3,2,3,1) -> 1*
    f0(8,2,5,8) -> 1*
    f0(2,3,8,4) -> 1*
    f0(4,4,3,4) -> 1*
    f0(4,8,4,1) -> 1*
    f0(4,5,1,2) -> 1*
    f0(3,2,5,8) -> 1*
    f0(8,4,3,1) -> 1*
    f0(2,5,2,2) -> 1*
    f0(1,3,8,1) -> 1*
    f0(1,4,2,4) -> 1*
    f0(5,3,4,3) -> 1*
    f0(3,4,3,1) -> 1*
    f0(8,4,5,8) -> 1*
    f0(2,5,8,4) -> 1*
    f0(2,2,5,5) -> 1*
    f0(3,4,5,8) -> 1*
    f0(1,5,8,1) -> 1*
    f0(1,2,5,2) -> 1*
    f0(5,5,4,3) -> 1*
    f0(5,2,1,4) -> 1*
    f0(2,4,5,5) -> 1*
    f0(4,1,3,3) -> 1*
    f0(4,8,3,4) -> 1*
    f0(4,2,1,1) -> 1*
    f0(8,8,3,1) -> 1*
    f0(2,2,2,1) -> 1*
    f0(1,4,5,2) -> 1*
    f0(1,8,2,4) -> 1*
    f0(5,4,1,4) -> 1*
    f0(8,8,5,8) -> 1*
    f0(2,2,8,3) -> 1*
    f0(4,2,3,8) -> 1*
    f0(3,8,3,1) -> 1*
    f0(2,2,4,8) -> 1*
    f0(4,3,3,3) -> 1*
    f0(4,4,1,1) -> 1*
    f0(3,8,5,8) -> 1*
    f0(2,4,2,1) -> 1*
    f0(1,2,4,5) -> 1*
    f0(5,2,4,2) -> 1*
    f0(2,4,8,3) -> 1*
    f0(4,4,3,8) -> 1*
    f0(2,1,5,4) -> 1*
    f0(2,4,4,8) -> 1*
    f0(2,8,5,5) -> 1*
    f0(4,5,3,3) -> 1*
    f0(8,1,2,3) -> 1*
    f0(1,4,4,5) -> 1*
    f0(1,1,5,1) -> 1*
    f0(1,8,5,2) -> 1*
    f0(1,5,2,3) -> 1*
    f0(5,4,4,2) -> 1*
    f0(4,1,8,8) -> 1*
    f0(5,1,1,3) -> 1*
    f0(8,1,8,5) -> 1*
    f0(5,8,1,4) -> 1*
    f0(3,1,2,3) -> 1*
    f0(2,3,5,4) -> 1*
    f0(8,2,2,8) -> 1*
    f0(3,1,8,5) -> 1*
    f0(8,3,2,3) -> 1*
    f0(4,8,1,1) -> 1*
    f0(3,2,2,8) -> 1*
    f0(2,8,2,1) -> 1*
    f0(1,3,5,1) -> 1*
    f0(5,2,3,5) -> 1*
    f0(4,3,8,8) -> 1*
    f0(5,3,1,3) -> 1*
    f0(8,3,8,5) -> 1*
    f0(3,3,2,3) -> 1*
    f0(2,8,8,3) -> 1*
    f0(4,8,3,8) -> 1*
    f0(2,1,8,2) -> 1*
    f0(2,5,5,4) -> 1*
    f0(2,8,4,8) -> 1*
    f0(8,4,2,8) -> 1*
    f0(2,2,2,5) -> 1*
    f0(4,2,3,2) -> 1*
    f0(3,3,8,5) -> 1*
    f0(3,4,2,8) -> 1*
    f0(1,5,5,1) -> 1*
    f0(1,1,4,4) -> 1*
    f0(1,8,4,5) -> 1*
    f0(5,4,3,5) -> 1*
    f0(5,1,4,1) -> 1*
    f0(4,5,8,8) -> 1*
    f0(5,8,4,2) -> 1*
    f0(5,5,1,3) -> 1*
    f0(8,5,8,5) -> 1*
    f0(2,3,8,2) -> 1*
    f0(2,4,2,5) -> 1*
    f0(4,4,3,2) -> 1*
    f0(3,5,8,5) -> 1*
    f0(1,3,4,4) -> 1*
    f0(5,3,4,1) -> 1*
    f0(2,5,8,2) -> 1*
    f0(2,2,5,3) -> 1*
    f0(8,8,2,8) -> 1*
    f0(2,2,1,8) -> 1*
    f0(8,2,2,2) -> 1*
    f0(3,8,2,8) -> 1*
    f0(1,5,4,4) -> 1*
    f0(1,2,1,5) -> 1*
    f0(5,5,4,1) -> 1*
    f0(5,1,3,4) -> 1*
    f0(5,8,3,5) -> 1*
    f0(5,2,1,2) -> 1*
    f0(8,2,8,4) -> 1*
    f0(3,2,2,2) -> 1*
    f0(2,4,5,3) -> 1*
    f0(2,1,2,4) -> 1*
    f0(2,8,2,5) -> 1*
    f0(2,4,1,8) -> 1*
    f0(4,1,3,1) -> 1*
    f0(3,2,8,4) -> 1*
    f0(4,8,3,2) -> 1*
    f0(8,4,2,2) -> 1*
    f0(1,4,1,5) -> 1*
    f0(5,3,3,4) -> 1*
    f0(5,4,1,2) -> 1*
    f0(8,4,8,4) -> 1*
    f0(4,1,5,8) -> 1*
    f0(3,4,2,2) -> 1*
    f0(2,2,8,1) -> 1*
    f0(8,1,5,5) -> 1*
    f0(2,3,2,4) -> 1*
    f0(4,3,3,1) -> 1*
    f0(3,4,8,4) -> 1*
    f0(3,1,5,5) -> 1*
    f0(1,2,4,3) -> 1*
    f0(5,5,3,4) -> 1*
    f0(4,3,5,8) -> 1*
    f0(2,4,8,1) -> 1*
    f0(8,3,5,5) -> 1*
    f0(2,1,5,2) -> 1*
    f0(2,8,5,3) -> 1*
    f0(2,5,2,4) -> 1*
    f0(2,8,1,8) -> 1*
    f0(4,5,3,1) -> 1*
    f0(3,3,5,5) -> 1*
    f0(8,1,2,1) -> 1*
    f0(8,8,2,2) -> 1*
    f0(1,4,4,3) -> 1*
    f0(1,1,1,4) -> 1*
    f0(1,8,1,5) -> 1*
    f0(5,1,1,1) -> 1*
    f0(8,1,8,3) -> 1*
    f0(8,8,8,4) -> 1*
    f0(5,8,1,2) -> 1*
    f0(4,5,5,8) -> 1*
    f0(3,1,2,1) -> 1*
    f0(8,1,4,8) -> 1*
    f0(8,5,5,5) -> 1*
    f0(3,8,2,2) -> 1*
    f0(2,3,5,2) -> 1*
    f0(3,8,8,4) -> 1*
    f0(3,1,8,3) -> 1*
    f0(5,1,3,8) -> 1*
    f0(3,5,5,5) -> 1*
    f0(8,3,2,1) -> 1*
    f0(3,1,4,8) -> 1*
    f0(1,3,1,4) -> 1*
    f0(5,2,3,3) -> 1*
    f0(5,3,1,1) -> 1*
    f0(8,3,8,3) -> 1*
    f0(3,3,2,1) -> 1*
    f0(8,3,4,8) -> 1*
    f0(2,8,8,1) -> 1*
    f0(2,5,5,2) -> 1*
    f0(2,1,4,5) -> 1*
    f0(3,3,8,3) -> 1*
    f0(5,3,3,8) -> 1*
    f0(8,5,2,1) -> 1*
    f0(3,3,4,8) -> 1*
    f0(1,1,4,2) -> 1*
    f0(1,8,4,3) -> 1*
    f0(1,5,1,4) -> 1*
    f0(5,4,3,3) -> 1*
    f0(5,5,1,1) -> 1*
    f0(8,5,8,3) -> 1*
    f0(3,5,2,1) -> 1*
    f0(8,5,4,8) -> 1*
    f0(8,2,5,4) -> 1*
    f0(2,3,4,5) -> 1*
    f0(3,5,8,3) -> 1*
    f0(5,5,3,8) -> 1*
    f0(3,2,5,4) -> 1*
    f0(3,5,4,8) -> 1*
    f0(1,3,4,2) -> 1*
    f0(4,1,2,8) -> 1*
    f0(8,4,5,4) -> 1*
    f0(2,5,4,5) -> 1*
    f0(2,2,5,1) -> 1*
    f0(8,1,2,5) -> 1*
    f0(5,2,8,8) -> 1*
    f0(4,2,2,3) -> 1*
    f0(3,4,5,4) -> 1*
    f0(3,1,2,5) -> 1*
    f0(1,5,4,2) -> 1*
    f0(1,1,3,5) -> 1*
    f0(1,2,1,3) -> 1*
    f0(5,1,3,2) -> 1*
    f0(4,2,8,5) -> 1*
    f0(5,8,3,3) -> 1*
    f0(8,2,8,2) -> 1*
    f0(4,3,2,8) -> 1*
    f0(2,4,5,1) -> 1*
    f0(8,3,2,5) -> 1*
    f0(5,4,8,8) -> 1*
    f0(2,8,2,3) -> 1*
    f0(4,4,2,3) -> 1*
    f0(3,2,8,2) -> 1*
    f0(3,3,2,5) -> 1*
    f0(1,3,3,5) -> 1*
    f0(1,4,1,3) -> 1*
    f0(5,3,3,2) -> 1*
    f0(4,4,8,5) -> 1*
    f0(8,4,8,2) -> 1*
    f0(4,5,2,8) -> 1*
    f0(8,1,5,3) -> 1*
    f0(8,8,5,4) -> 1*
    f0(2,2,4,4) -> 1*
    f0(8,1,1,8) -> 1*
    f0(8,5,2,5) -> 1*
    f0(3,4,8,2) -> 1*
    f0(3,1,5,3) -> 1*
    f0(3,8,5,4) -> 1*
    f0(3,5,2,5) -> 1*
    f0(3,1,1,8) -> 1*
    f0(1,5,3,5) -> 1*
    f0(1,2,4,1) -> 1*
    f0(5,5,3,2) -> 1*
    f0(8,3,5,3) -> 1*
    f0(2,4,4,4) -> 1*
    f0(8,3,1,8) -> 1*
    f0(2,8,5,1) -> 1*
    f0(2,1,1,5) -> 1*
    f0(5,8,8,8) -> 1*
    f0(4,1,2,2) -> 1*
    f0(3,3,5,3) -> 1*
    f0(3,3,1,8) -> 1*
    f0(1,4,4,1) -> 1*
    f0(1,1,1,2) -> 1*
    f0(4,8,8,5) -> 1*
    f0(4,1,8,4) -> 1*
    f0(1,8,1,3) -> 1*
    f0(8,8,8,2) -> 1*
    f0(8,1,8,1) -> 1*
    f0(8,5,5,3) -> 1*
    f0(8,5,1,8) -> 1*
    f0(8,2,2,4) -> 1*
    f0(2,3,1,5) -> 1*
    f0(4,3,2,2) -> 1*
    f0(3,1,8,1) -> 1*
    f0(3,8,8,2) -> 1*
    f0(3,5,5,3) -> 1*
    f0(3,2,2,4) -> 1*
    f0(3,5,1,8) -> 1*
    f0(1,2,3,4) -> 1*
    f0(1,3,1,2) -> 1*
    f0(5,2,3,1) -> 1*
    f0(4,3,8,4) -> 1*
    f0(8,3,8,1) -> 1*
    f0(2,1,4,3) -> 1*
    f0(8,4,2,4) -> 1*
    f0(2,8,4,4) -> 1*
    f0(2,5,1,5) -> 1*
    f0(5,2,5,8) -> 1*
    f0(4,5,2,2) -> 1*
    f0(3,3,8,1) -> 1*
    f0(3,4,2,4) -> 1*
    f0(1,4,3,4) -> 1*
    f0(1,8,4,1) -> 1*
    f0(1,5,1,2) -> 1*
    f0(5,4,3,1) -> 1*
    f0(4,5,8,4) -> 1*
    f0(4,2,5,5) -> 1*
    f0(8,5,8,1) -> 1*
    f0(8,2,5,2) -> 1*
    f0(2,3,4,3) -> 1*
    f0(5,4,5,8) -> 1*
    f0(3,5,8,1) -> 1*
    f0(3,2,5,2) -> 1*
    f0(4,4,5,5) -> 1*
    f0(8,4,5,2) -> 1*
    f0(2,5,4,3) -> 1*
    f0(8,8,2,4) -> 1*
    f0(2,2,1,4) -> 1*
    f0(4,2,2,1) -> 1*
    f0(3,4,5,2) -> 1*
    f0(3,8,2,4) -> 1*
    f0(1,1,3,3) -> 1*
    f0(1,8,3,4) -> 1*
    f0(1,2,1,1) -> 1*
    f0(5,8,3,1) -> 1*
    f0(4,2,8,3) -> 1*
    f0(4,2,4,8) -> 1*
    f0(8,2,4,5) -> 1*
    f0(2,4,1,4) -> 1*
    f0(1,2,3,8) -> 1*
    f0(5,8,5,8) -> 1*
    f0(4,4,2,1) -> 1*
    f0(3,2,4,5) -> 1*
    f0(1,3,3,3) -> 1*
    f0(1,4,1,1) -> 1*
    f0(4,4,8,3) -> 1*
    f0(4,1,5,4) -> 1*
    f0(4,8,5,5) -> 1*
    f0(4,4,4,8) -> 1*
    f0(8,4,4,5) -> 1*
    f0(8,1,5,1) -> 1*
    f0(8,8,5,2) -> 1*
    f0(2,2,4,2) -> 1*
    f0(8,5,2,3) -> 1*
    f0(1,4,3,8) -> 1*
    f0(3,4,4,5) -> 1*
    f0(3,1,5,1) -> 1*
    f0(3,8,5,2) -> 1*
    f0(3,5,2,3) -> 1*
    f0(1,5,3,3) -> 1*
    f0(5,1,2,3) -> 1*
    f0(4,3,5,4) -> 1*
    f0(8,3,5,1) -> 1*
    f0(2,4,4,2) -> 1*
    f0(1,1,8,8) -> 1*
    f0(2,1,1,3) -> 1*
    f0(2,8,1,4) -> 1*
    f0(5,1,8,5) -> 1*
    f0(4,8,2,1) -> 1*
    f0(5,2,2,8) -> 1*
    f0(3,3,5,1) -> 1*
    f0(5,3,2,3) -> 1*
    f0(1,8,1,1) -> 1*
    f0(4,1,8,2) -> 1*
    f0(4,8,8,3) -> 1*
    f0(4,5,5,4) -> 1*
    f0(4,8,4,8) -> 1*
    f0(4,2,2,5) -> 1*
    f0(8,5,5,1) -> 1*
    f0(8,1,4,4) -> 1*
    f0(8,8,4,5) -> 1*
    f0(2,2,3,5) -> 1*
    f0(1,3,8,8) -> 1*
    f0(2,3,1,3) -> 1*
    f0(5,3,8,5) -> 1*
    f0(1,8,3,8) -> 1*
    f0(5,4,2,8) -> 1*
    f0(3,5,5,1) -> 1*
    f0(3,1,4,4) -> 1*
    f0(3,8,4,5) -> 1*
    f0(1,2,3,2) -> 1*
    f0(4,3,8,2) -> 1*
    g0(5) -> 2*
    g0(2) -> 2*
    g0(4) -> 2*
    g0(1) -> 2*
    g0(8) -> 2*
    g0(3) -> 2*
    h0(5) -> 3*
    h0(2) -> 3*
    h0(4) -> 3*
    h0(1) -> 3*
    h0(8) -> 3*
    h0(3) -> 3*
    00() -> 4*
    20() -> 5*
    21() -> 8*,5,3,2,1
    f1(5,5,8,5) -> 1*
    f1(8,1,1,4) -> 1*
    f1(8,8,1,5) -> 1*
    f1(5,8,8,4) -> 1*
    f1(5,5,5,5) -> 1*
    f1(5,5,8,3) -> 1*
    f1(2,2,8,8) -> 1*
    f1(8,3,3,5) -> 1*
    f1(3,3,3,5) -> 1*
    f1(5,8,5,4) -> 1*
    f1(4,4,4,4) -> 1*
    f1(8,1,1,2) -> 1*
    f1(8,8,1,3) -> 1*
    f1(2,8,8,8) -> 1*
    f1(1,1,8,4) -> 1*
    f1(1,8,8,5) -> 1*
    f1(5,8,8,2) -> 1*
    f1(5,5,5,3) -> 1*
    f1(5,5,8,1) -> 1*
    f1(8,8,3,4) -> 1*
    f1(3,8,3,4) -> 1*
    f1(8,3,3,3) -> 1*
    f1(3,3,3,3) -> 1*
    f1(5,8,5,2) -> 1*
    f1(8,1,8,8) -> 1*
    f1(4,4,4,2) -> 1*
    f1(8,8,1,1) -> 1*
    f1(8,3,8,8) -> 1*
    f1(8,8,3,8) -> 1*
    f1(2,2,2,8) -> 1*
    f1(3,3,8,8) -> 1*
    f1(1,1,8,2) -> 1*
    f1(3,8,3,8) -> 1*
    f1(1,8,8,3) -> 1*
    f1(5,5,5,1) -> 1*
    f1(8,5,8,8) -> 1*
    f1(2,8,2,8) -> 1*
    f1(8,8,3,2) -> 1*
    f1(2,2,2,2) -> 1*
    f1(3,8,3,2) -> 1*
    f1(2,2,8,4) -> 1*
    f1(8,3,3,1) -> 1*
    f1(3,3,3,1) -> 1*
    f1(1,8,1,8) -> 1*
    f1(8,5,5,8) -> 1*
    f1(2,8,2,2) -> 1*
    f1(2,8,8,4) -> 1*
    f1(1,8,8,1) -> 1*
    f1(8,2,2,3) -> 1*
    f1(8,2,8,5) -> 1*
    f1(2,2,8,2) -> 1*
    f1(1,1,1,5) -> 1*
    f1(8,1,8,4) -> 1*
    f1(8,8,8,5) -> 1*
    f1(3,8,8,5) -> 1*
    f1(8,3,8,4) -> 1*
    f1(2,8,8,2) -> 1*
    f1(2,2,2,4) -> 1*
    f1(3,3,8,4) -> 1*
    f1(8,5,8,4) -> 1*
    f1(8,2,2,1) -> 1*
    f1(8,2,8,3) -> 1*
    f1(2,8,2,4) -> 1*
    f1(8,8,5,5) -> 1*
    f1(8,8,2,1) -> 1*
    f1(1,1,1,3) -> 1*
    f1(1,8,1,4) -> 1*
    f1(8,1,8,2) -> 1*
    f1(8,8,8,3) -> 1*
    f1(8,5,5,4) -> 1*
    f1(8,2,2,5) -> 1*
    f1(3,8,8,3) -> 1*
    f1(8,3,8,2) -> 1*
    f1(5,5,8,8) -> 1*
    f1(3,3,8,2) -> 1*
    f1(8,5,8,2) -> 1*
    f1(8,8,2,5) -> 1*
    f1(8,2,8,1) -> 1*
    f1(8,8,5,3) -> 1*
    f1(8,8,1,8) -> 1*
    f1(5,5,5,8) -> 1*
    f1(1,1,1,1) -> 1*
    f1(1,8,1,2) -> 1*
    f1(8,8,8,1) -> 1*
    f1(8,5,5,2) -> 1*
    f1(3,8,8,1) -> 1*
    f1(8,8,2,3) -> 1*
    f1(8,8,5,1) -> 1*
    f1(8,1,1,5) -> 1*
    f1(1,8,8,8) -> 1*
    f1(5,8,8,5) -> 1*
    f1(5,5,8,4) -> 1*
    f1(5,8,5,5) -> 1*
    f1(4,4,4,5) -> 1*
    f1(8,8,1,4) -> 1*
    f1(8,1,1,3) -> 1*
    f1(1,1,8,5) -> 1*
    f1(5,8,8,3) -> 1*
    f1(5,5,5,4) -> 1*
    f1(5,5,8,2) -> 1*
    f1(8,8,3,5) -> 1*
    f1(3,8,3,5) -> 1*
    f1(8,3,3,4) -> 1*
    f1(3,3,3,4) -> 1*
    f1(5,8,5,3) -> 1*
    f1(4,4,4,3) -> 1*
    f1(8,8,1,2) -> 1*
    f1(8,1,1,1) -> 1*
    f1(1,8,8,4) -> 1*
    f1(1,1,8,3) -> 1*
    f1(5,8,8,1) -> 1*
    f1(5,5,5,2) -> 1*
    f1(8,3,3,8) -> 1*
    f1(3,3,3,8) -> 1*
    f1(8,2,8,8) -> 1*
    f1(8,8,3,3) -> 1*
    f1(2,2,2,3) -> 1*
    f1(2,2,8,5) -> 1*
    f1(3,8,3,3) -> 1*
    f1(8,3,3,2) -> 1*
    f1(3,3,3,2) -> 1*
    f1(1,1,1,8) -> 1*
    f1(5,8,5,1) -> 1*
    f1(8,8,8,8) -> 1*
    f1(4,4,4,1) -> 1*
    f1(3,8,8,8) -> 1*
    f1(2,8,8,5) -> 1*
    f1(1,8,8,2) -> 1*
    f1(1,1,8,1) -> 1*
    f1(8,8,3,1) -> 1*
    f1(2,2,2,1) -> 1*
    f1(2,2,8,3) -> 1*
    f1(8,8,5,8) -> 1*
    f1(3,8,3,1) -> 1*
    f1(8,1,8,5) -> 1*
    f1(8,2,2,8) -> 1*
    f1(2,8,2,1) -> 1*
    f1(8,3,8,5) -> 1*
    f1(2,8,8,3) -> 1*
    f1(2,2,2,5) -> 1*
    f1(3,3,8,5) -> 1*
    f1(8,5,8,5) -> 1*
    f1(8,8,2,8) -> 1*
    f1(8,2,2,2) -> 1*
    f1(8,2,8,4) -> 1*
    f1(2,8,2,5) -> 1*
    f1(2,2,8,1) -> 1*
    f1(8,8,2,2) -> 1*
    f1(1,1,1,4) -> 1*
    f1(1,8,1,5) -> 1*
    f1(8,8,8,4) -> 1*
    f1(8,1,8,3) -> 1*
    f1(8,5,5,5) -> 1*
    f1(3,8,8,4) -> 1*
    f1(8,3,8,3) -> 1*
    f1(2,8,8,1) -> 1*
    f1(3,3,8,3) -> 1*
    f1(8,5,8,3) -> 1*
    f1(8,2,8,2) -> 1*
    f1(2,8,2,3) -> 1*
    f1(8,8,5,4) -> 1*
    f1(8,1,1,8) -> 1*
    f1(5,8,8,8) -> 1*
    f1(1,1,1,2) -> 1*
    f1(1,8,1,3) -> 1*
    f1(8,8,8,2) -> 1*
    f1(8,1,8,1) -> 1*
    f1(8,5,5,3) -> 1*
    f1(8,2,2,4) -> 1*
    f1(3,8,8,2) -> 1*
    f1(8,3,8,1) -> 1*
    f1(3,3,8,1) -> 1*
    f1(8,5,8,1) -> 1*
    f1(8,8,2,4) -> 1*
    f1(5,8,5,8) -> 1*
    f1(4,4,4,8) -> 1*
    f1(8,8,5,2) -> 1*
    f1(1,1,8,8) -> 1*
    f1(1,8,1,1) -> 1*
    f1(8,5,5,1) -> 1*
    22() -> 2,3,5,8*,1
  problem:
   
  Qed