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}
 LMPO:
  Quasi-Precedence:
  g2 > h, 
  g1 > h, 
  f > g2, 
  f > g1
  empty
  
Normal:
   pi(h) = [2], pi(g2) = [1,2,3], pi(f) = [1,2], pi(g1) = [1,2,3]
  
Safe:
   pi(h) = [1]
  
Predicative System:
   {   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(y;x),
    g1(y,x,x;) -> h(y;x),
    g2(x,y,y;) -> h(y;x),
    g2(y,y,x;) -> h(y;x),
        h(x;x) -> x}
  

   
  

  Qed