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

Proof:
 Church Rosser Transformation Processor:
  strict:
   
  weak:
   
  critical peaks: 12
   f(h(g(x)),g(x)) <-0|[]- f(g(x),h(g(x))) -1|[]-> f(g(h(g(x))),g(x))
   f(h(x),x) <-0|[]- f(x,h(x)) -2|[]-> f(h(x),x)
   f(g(h(g(x76))),g(x76)) <-1|[]- f(g(x76),h(g(x76))) -0|[]-> f(h(g(x76)),g(x76))
   f(g(y),g(x78)) <-1|[]- f(g(x78),y) -2|[]-> f(y,g(x78))
   f(h(x),x) <-2|[]- f(x,h(x)) -0|[]-> f(h(x),x)
   f(y,g(x)) <-2|[]- f(g(x),y) -1|[]-> f(g(y),g(x))
   f(h(h(x84)),y) <-3|0[]- f(g(h(x84)),y) -1|[]-> f(g(y),g(h(x84)))
   h(h(x85)) <-3|[]- g(h(x85)) -5|[]-> h(x85)
   f(x,g(x)) <-4|1[]- f(x,h(x)) -0|[]-> f(h(x),x)
   g(g(x)) <-4|0[]- g(h(x)) -3|[]-> h(h(x))
   f(x,y) <-5|0[]- f(g(x),y) -1|[]-> f(g(y),g(x))
   h(x) <-5|[]- g(h(x)) -3|[]-> h(h(x))
  Redundant Rules Transformation:
   f(x,y) -> f(y,x)
   h(x) -> g(x)
   g(x) -> x
   Qed (ToyamaOyamaguchi95Cor22)