MAYBE

Problem:
 f(f(f(a(),x),y),z) -> f(f(x,z),f(y,z))
 f(f(b(),x),y) -> x
 f(c(),y) -> y

Proof:
 Uncurry Processor:
  a3(x,y,z) -> f(f(x,z),f(y,z))
  b2(x,y) -> x
  c1(y) -> y
  f(a2(x4,x3),x5) -> a3(x4,x3,x5)
  f(a1(x4),x5) -> a2(x4,x5)
  f(a(),x5) -> a1(x5)
  f(b1(x4),x5) -> b2(x4,x5)
  f(b(),x5) -> b1(x5)
  f(c(),x5) -> c1(x5)
  DP Processor:
   DPs:
    a{3,#}(x,y,z) -> f#(y,z)
    a{3,#}(x,y,z) -> f#(x,z)
    a{3,#}(x,y,z) -> f#(f(x,z),f(y,z))
    f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
    f#(b1(x4),x5) -> b{2,#}(x4,x5)
    f#(c(),x5) -> c{1,#}(x5)
   TRS:
    a3(x,y,z) -> f(f(x,z),f(y,z))
    b2(x,y) -> x
    c1(y) -> y
    f(a2(x4,x3),x5) -> a3(x4,x3,x5)
    f(a1(x4),x5) -> a2(x4,x5)
    f(a(),x5) -> a1(x5)
    f(b1(x4),x5) -> b2(x4,x5)
    f(b(),x5) -> b1(x5)
    f(c(),x5) -> c1(x5)
   TDG Processor:
    DPs:
     a{3,#}(x,y,z) -> f#(y,z)
     a{3,#}(x,y,z) -> f#(x,z)
     a{3,#}(x,y,z) -> f#(f(x,z),f(y,z))
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
     f#(b1(x4),x5) -> b{2,#}(x4,x5)
     f#(c(),x5) -> c{1,#}(x5)
    TRS:
     a3(x,y,z) -> f(f(x,z),f(y,z))
     b2(x,y) -> x
     c1(y) -> y
     f(a2(x4,x3),x5) -> a3(x4,x3,x5)
     f(a1(x4),x5) -> a2(x4,x5)
     f(a(),x5) -> a1(x5)
     f(b1(x4),x5) -> b2(x4,x5)
     f(b(),x5) -> b1(x5)
     f(c(),x5) -> c1(x5)
    graph:
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5) ->
     a{3,#}(x,y,z) -> f#(f(x,z),f(y,z))
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5) ->
     a{3,#}(x,y,z) -> f#(x,z)
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5) ->
     a{3,#}(x,y,z) -> f#(y,z)
     a{3,#}(x,y,z) -> f#(f(x,z),f(y,z)) ->
     f#(c(),x5) -> c{1,#}(x5)
     a{3,#}(x,y,z) -> f#(f(x,z),f(y,z)) ->
     f#(b1(x4),x5) -> b{2,#}(x4,x5)
     a{3,#}(x,y,z) -> f#(f(x,z),f(y,z)) ->
     f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
     a{3,#}(x,y,z) -> f#(y,z) -> f#(c(),x5) -> c{1,#}(x5)
     a{3,#}(x,y,z) -> f#(y,z) -> f#(b1(x4),x5) -> b{2,#}(x4,x5)
     a{3,#}(x,y,z) -> f#(y,z) -> f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
     a{3,#}(x,y,z) -> f#(x,z) -> f#(c(),x5) -> c{1,#}(x5)
     a{3,#}(x,y,z) -> f#(x,z) -> f#(b1(x4),x5) -> b{2,#}(x4,x5)
     a{3,#}(x,y,z) -> f#(x,z) -> f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
    SCC Processor:
     #sccs: 1
     #rules: 4
     #arcs: 12/36
     DPs:
      f#(a2(x4,x3),x5) -> a{3,#}(x4,x3,x5)
      a{3,#}(x,y,z) -> f#(y,z)
      a{3,#}(x,y,z) -> f#(x,z)
      a{3,#}(x,y,z) -> f#(f(x,z),f(y,z))
     TRS:
      a3(x,y,z) -> f(f(x,z),f(y,z))
      b2(x,y) -> x
      c1(y) -> y
      f(a2(x4,x3),x5) -> a3(x4,x3,x5)
      f(a1(x4),x5) -> a2(x4,x5)
      f(a(),x5) -> a1(x5)
      f(b1(x4),x5) -> b2(x4,x5)
      f(b(),x5) -> b1(x5)
      f(c(),x5) -> c1(x5)
     Open