TRS:
 {    f(x, y) -> g1(x, x, y),
      f(x, y) -> g1(y, x, x),
      f(x, y) -> g2(x, y, y),
      f(x, y) -> g2(y, y, x),
  g1(x, x, y) -> h(x, y),
  g1(y, x, x) -> h(x, y),
  g2(x, y, y) -> h(x, y),
  g2(y, y, x) -> h(x, y),
      h(x, x) -> x}
 POP*:
  Precedence:
  g2 > h, 
  g1 > h, 
  f > g2, 
  f > g1
  empty
  
Normal:
   pi(h) = [1], pi(g2) = [1,2,3], pi(f) = [1,2], pi(g1) = [1,3]
  
Safe:
   pi(h) = [2], pi(g1) = [2]
  
Predicative System:
   {   f(x,y;) -> g1(x,y;x),
       f(x,y;) -> g1(y,x;x),
       f(x,y;) -> g2(x,y,y;),
       f(x,y;) -> g2(y,y,x;),
     g1(x,y;x) -> h(x;y),
     g1(y,x;x) -> h(x;y),
    g2(x,y,y;) -> h(x;y),
    g2(y,y,x;) -> h(x;y),
        h(x;x) -> x}
  Qed