TRS:
 {  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}
 POP*:
  Precedence:
  g2 > h, 
  g1 > h, 
  f > g2, 
  f > g1
  empty
  
Normal:
   pi(h) = [1], pi(g2) = [1,2,3], pi(f) = [1,2,3,4,5], pi(g1) = [1,2,3,4]
  
Safe:
   pi(h) = [2], pi(g2) = [4]
  
Predicative System:
   {  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}
  Qed