MAYBE

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

Proof:
 DP Processor:
  DPs:
   +#(a(),b()) -> +#(b(),a())
   +#(a(),+(b(),z)) -> +#(a(),z)
   +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
   +#(+(x,y),z) -> +#(y,z)
   +#(+(x,y),z) -> +#(x,+(y,z))
   f#(+(x,y),z) -> f#(y,z)
   f#(+(x,y),z) -> f#(x,z)
   f#(+(x,y),z) -> +#(f(x,z),f(y,z))
  TRS:
   +(a(),b()) -> +(b(),a())
   +(a(),+(b(),z)) -> +(b(),+(a(),z))
   +(+(x,y),z) -> +(x,+(y,z))
   f(a(),y) -> a()
   f(b(),y) -> b()
   f(+(x,y),z) -> +(f(x,z),f(y,z))
  ADG Processor:
   DPs:
    +#(a(),b()) -> +#(b(),a())
    +#(a(),+(b(),z)) -> +#(a(),z)
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z))
    f#(+(x,y),z) -> f#(y,z)
    f#(+(x,y),z) -> f#(x,z)
    f#(+(x,y),z) -> +#(f(x,z),f(y,z))
   TRS:
    +(a(),b()) -> +(b(),a())
    +(a(),+(b(),z)) -> +(b(),+(a(),z))
    +(+(x,y),z) -> +(x,+(y,z))
    f(a(),y) -> a()
    f(b(),y) -> b()
    f(+(x,y),z) -> +(f(x,z),f(y,z))
   graph:
    f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(y,z)
    f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> f#(x,z)
    f#(+(x,y),z) -> f#(y,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z))
    f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(y,z)
    f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> f#(x,z)
    f#(+(x,y),z) -> f#(x,z) -> f#(+(x,y),z) -> +#(f(x,z),f(y,z))
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) ->
    +#(a(),b()) -> +#(b(),a())
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) ->
    +#(a(),+(b(),z)) -> +#(a(),z)
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) ->
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(y,z)
    f#(+(x,y),z) -> +#(f(x,z),f(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(y,z) -> +#(a(),b()) -> +#(b(),a())
    +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(a(),z)
    +#(+(x,y),z) -> +#(y,z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(y,z) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(a(),+(b(),z)) -> +#(a(),z)
    +#(+(x,y),z) -> +#(x,+(y,z)) ->
    +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(y,z)
    +#(+(x,y),z) -> +#(x,+(y,z)) -> +#(+(x,y),z) -> +#(x,+(y,z))
    +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),b()) -> +#(b(),a())
    +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(a(),z)
    +#(a(),+(b(),z)) -> +#(a(),z) -> +#(a(),+(b(),z)) -> +#(b(),+(a(),z))
   SCC Processor:
    #sccs: 3
    #rules: 5
    #arcs: 23/64
    DPs:
     f#(+(x,y),z) -> f#(y,z)
     f#(+(x,y),z) -> f#(x,z)
    TRS:
     +(a(),b()) -> +(b(),a())
     +(a(),+(b(),z)) -> +(b(),+(a(),z))
     +(+(x,y),z) -> +(x,+(y,z))
     f(a(),y) -> a()
     f(b(),y) -> b()
     f(+(x,y),z) -> +(f(x,z),f(y,z))
    Open
    
    DPs:
     +#(+(x,y),z) -> +#(x,+(y,z))
     +#(+(x,y),z) -> +#(y,z)
    TRS:
     +(a(),b()) -> +(b(),a())
     +(a(),+(b(),z)) -> +(b(),+(a(),z))
     +(+(x,y),z) -> +(x,+(y,z))
     f(a(),y) -> a()
     f(b(),y) -> b()
     f(+(x,y),z) -> +(f(x,z),f(y,z))
    Open
    
    DPs:
     +#(a(),+(b(),z)) -> +#(a(),z)
    TRS:
     +(a(),b()) -> +(b(),a())
     +(a(),+(b(),z)) -> +(b(),+(a(),z))
     +(+(x,y),z) -> +(x,+(y,z))
     f(a(),y) -> a()
     f(b(),y) -> b()
     f(+(x,y),z) -> +(f(x,z),f(y,z))
    Open