Problem:
 f(f(x,y),z) -> f(x,f(y,z))
 f(x,y) -> f(y,x)

Proof:
 Commute Transformation Processor:
  f(f(x,y),z) -> f(x,f(y,z))
  f(x,f(y,z)) -> f(f(x,y),z)
  f(x,y) -> f(y,x)
  Church Rosser Transformation Processor (dup):
   
   strict:
    
   weak:
    f(f(x,y),z) -> f(x,f(y,z))
    f(x,f(y,z)) -> f(f(x,y),z)
    f(x,y) -> f(y,x)
   critical peaks: 12
   f(f(x43,f(x44,y)),z) <-0|0[]- f(f(f(x43,x44),y),z) -0|[]-> f(f(x43,x44),f(y,z))
   f(x46,f(x47,f(y,z))) <-0|[]- f(f(x46,x47),f(y,z)) -1|[]-> f(f(f(x46,x47),y),z)
   f(x,f(x49,f(x50,z))) <-0|1[]- f(x,f(f(x49,x50),z)) -1|[]-> f(f(x,f(x49,x50)),z)
   f(x52,f(x53,y)) <-0|[]- f(f(x52,x53),y) -2|[]-> f(y,f(x52,x53))
   f(f(f(x,y),x56),x57) <-1|[]- f(f(x,y),f(x56,x57)) -0|[]-> f(x,f(y,f(x56,x57)))
   f(f(f(x,x59),x60),z) <-1|0[]- f(f(x,f(x59,x60)),z) -0|[]-> f(x,f(f(x59,x60),z))
   f(x,f(f(y,x62),x63)) <-1|1[]- f(x,f(y,f(x62,x63))) -1|[]-> f(f(x,y),f(x62,x63))
   f(f(x,x65),x66) <-1|[]- f(x,f(x65,x66)) -2|[]-> f(f(x65,x66),x)
   f(z,f(x,y)) <-2|[]- f(f(x,y),z) -0|[]-> f(x,f(y,z))
   f(f(y,x),z) <-2|0[]- f(f(x,y),z) -0|[]-> f(x,f(y,z))
   f(f(y,z),x) <-2|[]- f(x,f(y,z)) -1|[]-> f(f(x,y),z)
   f(x,f(z,y)) <-2|1[]- f(x,f(y,z)) -1|[]-> f(f(x,y),z)
   Shift Processor (no label):
    
    strict:
     
    weak:
     
    Shift Processor lab=left (dd):
     
     strict:
      f(f(f(x43,x44),y),z) -> f(f(x43,f(x44,y)),z)
      f(f(f(x43,x44),y),z) -> f(f(x43,x44),f(y,z))
      f(f(x43,f(x44,y)),z) -> f(f(f(x43,x44),y),z)
      f(f(x43,x44),f(y,z)) -> f(f(f(x43,x44),y),z)
      f(f(x46,x47),f(y,z)) -> f(x46,f(x47,f(y,z)))
      f(f(x46,x47),f(y,z)) -> f(f(f(x46,x47),y),z)
      f(x46,f(x47,f(y,z))) -> f(f(x46,x47),f(y,z))
      f(f(f(x46,x47),y),z) -> f(f(x46,x47),f(y,z))
      f(x,f(f(x49,x50),z)) -> f(x,f(x49,f(x50,z)))
      f(x,f(f(x49,x50),z)) -> f(f(x,f(x49,x50)),z)
      f(x,f(x49,f(x50,z))) -> f(x,f(f(x49,x50),z))
      f(f(x,f(x49,x50)),z) -> f(x,f(f(x49,x50),z))
      f(f(x52,x53),y) -> f(x52,f(x53,y))
      f(f(x52,x53),y) -> f(y,f(x52,x53))
      f(x52,f(x53,y)) -> f(f(x52,x53),y)
      f(y,f(x52,x53)) -> f(f(x52,x53),y)
      f(f(x,y),f(x56,x57)) -> f(f(f(x,y),x56),x57)
      f(f(x,y),f(x56,x57)) -> f(x,f(y,f(x56,x57)))
      f(f(f(x,y),x56),x57) -> f(f(x,y),f(x56,x57))
      f(x,f(y,f(x56,x57))) -> f(f(x,y),f(x56,x57))
      f(f(x,f(x59,x60)),z) -> f(f(f(x,x59),x60),z)
      f(f(x,f(x59,x60)),z) -> f(x,f(f(x59,x60),z))
      f(f(f(x,x59),x60),z) -> f(f(x,f(x59,x60)),z)
      f(x,f(f(x59,x60),z)) -> f(f(x,f(x59,x60)),z)
      f(x,f(y,f(x62,x63))) -> f(x,f(f(y,x62),x63))
      f(x,f(y,f(x62,x63))) -> f(f(x,y),f(x62,x63))
      f(x,f(f(y,x62),x63)) -> f(x,f(y,f(x62,x63)))
      f(f(x,y),f(x62,x63)) -> f(x,f(y,f(x62,x63)))
      f(x,f(x65,x66)) -> f(f(x,x65),x66)
      f(x,f(x65,x66)) -> f(f(x65,x66),x)
      f(f(x,x65),x66) -> f(x,f(x65,x66))
      f(f(x65,x66),x) -> f(x,f(x65,x66))
      f(f(x,y),z) -> f(z,f(x,y))
      f(f(x,y),z) -> f(x,f(y,z))
      f(z,f(x,y)) -> f(f(x,y),z)
      f(x,f(y,z)) -> f(f(x,y),z)
      f(f(x,y),z) -> f(f(y,x),z)
      f(f(x,y),z) -> f(x,f(y,z))
      f(f(y,x),z) -> f(f(x,y),z)
      f(x,f(y,z)) -> f(f(x,y),z)
      f(x,f(y,z)) -> f(f(y,z),x)
      f(x,f(y,z)) -> f(f(x,y),z)
      f(f(y,z),x) -> f(x,f(y,z))
      f(f(x,y),z) -> f(x,f(y,z))
      f(x,f(y,z)) -> f(x,f(z,y))
      f(x,f(y,z)) -> f(f(x,y),z)
      f(x,f(z,y)) -> f(x,f(y,z))
      f(f(x,y),z) -> f(x,f(y,z))
     weak:
      f(f(x,y),z) -> f(x,f(y,z))
      f(x,f(y,z)) -> f(f(x,y),z)
      f(x,y) -> f(y,x)
     Shift Processor (ldh) lab=left (force):
      
      strict:
       
      weak:
       
      Decreasing Processor:
       The following diagrams are decreasing:
       peak:
        f(f(x43,f(x44,y)),z) <-0|0[1]- f(f(f(x43,x44),y),z) -0|[1]-> f(f(x43,x44),f(y,z))
       joins:
        f(f(x43,f(x44,y)),z) -1|0[1]-> f(f(f(x43,x44),y),z)
        f(f(x43,x44),f(y,z)) -1|[1]-> f(f(f(x43,x44),y),z)
       peak:
        f(x46,f(x47,f(y,z))) <-0|[1]- f(f(x46,x47),f(y,z)) -1|[1]-> f(f(f(x46,x47),y),z)
       joins:
        f(x46,f(x47,f(y,z))) -1|[1]-> f(f(x46,x47),f(y,z))
        f(f(f(x46,x47),y),z) -0|[1]-> f(f(x46,x47),f(y,z))
       peak:
        f(x,f(x49,f(x50,z))) <-0|1[1]- f(x,f(f(x49,x50),z)) -1|[1]-> f(f(x,f(x49,x50)),z)
       joins:
        f(x,f(x49,f(x50,z))) -1|1[1]-> f(x,f(f(x49,x50),z))
        f(f(x,f(x49,x50)),z) -0|[1]-> f(x,f(f(x49,x50),z))
       peak:
        f(x52,f(x53,y)) <-0|[1]- f(f(x52,x53),y) -2|[1]-> f(y,f(x52,x53))
       joins:
        f(x52,f(x53,y)) -1|[1]-> f(f(x52,x53),y)
        f(y,f(x52,x53)) -2|[1]-> f(f(x52,x53),y)
       peak:
        f(f(f(x,y),x56),x57) <-1|[1]- f(f(x,y),f(x56,x57)) -0|[1]-> f(x,f(y,f(x56,x57)))
       joins:
        f(f(f(x,y),x56),x57) -0|[1]-> f(f(x,y),f(x56,x57))
        f(x,f(y,f(x56,x57))) -1|[1]-> f(f(x,y),f(x56,x57))
       peak:
        f(f(f(x,x59),x60),z) <-1|0[1]- f(f(x,f(x59,x60)),z) -0|[1]-> f(x,f(f(x59,x60),z))
       joins:
        f(f(f(x,x59),x60),z) -0|0[1]-> f(f(x,f(x59,x60)),z)
        f(x,f(f(x59,x60),z)) -1|[1]-> f(f(x,f(x59,x60)),z)
       peak:
        f(x,f(f(y,x62),x63)) <-1|1[1]- f(x,f(y,f(x62,x63))) -1|[1]-> f(f(x,y),f(x62,x63))
       joins:
        f(x,f(f(y,x62),x63)) -0|1[1]-> f(x,f(y,f(x62,x63)))
        f(f(x,y),f(x62,x63)) -0|[1]-> f(x,f(y,f(x62,x63)))
       peak:
        f(f(x,x65),x66) <-1|[1]- f(x,f(x65,x66)) -2|[1]-> f(f(x65,x66),x)
       joins:
        f(f(x,x65),x66) -0|[1]-> f(x,f(x65,x66))
        f(f(x65,x66),x) -2|[1]-> f(x,f(x65,x66))
       peak:
        f(z,f(x,y)) <-2|[1]- f(f(x,y),z) -0|[1]-> f(x,f(y,z))
       joins:
        f(z,f(x,y)) -2|[1]-> f(f(x,y),z)
        f(x,f(y,z)) -1|[1]-> f(f(x,y),z)
       peak:
        f(f(y,x),z) <-2|0[1]- f(f(x,y),z) -0|[1]-> f(x,f(y,z))
       joins:
        f(f(y,x),z) -2|0[1]-> f(f(x,y),z)
        f(x,f(y,z)) -1|[1]-> f(f(x,y),z)
       peak:
        f(f(y,z),x) <-2|[1]- f(x,f(y,z)) -1|[1]-> f(f(x,y),z)
       joins:
        f(f(y,z),x) -2|[1]-> f(x,f(y,z))
        f(f(x,y),z) -0|[1]-> f(x,f(y,z))
       peak:
        f(x,f(z,y)) <-2|1[1]- f(x,f(y,z)) -1|[1]-> f(f(x,y),z)
       joins:
        f(x,f(z,y)) -2|1[1]-> f(x,f(y,z))
        f(f(x,y),z) -0|[1]-> f(x,f(y,z))
       Qed