MAYBE

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

Proof:
 DP Processor:
  DPs:
   a#(a(f(x,y))) -> a#(y)
   a#(a(f(x,y))) -> a#(b(a(y)))
   a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
   a#(a(f(x,y))) -> a#(x)
   a#(a(f(x,y))) -> a#(b(a(x)))
   a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
   a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
   f#(a(x),a(y)) -> f#(x,y)
   f#(a(x),a(y)) -> a#(f(x,y))
   f#(b(x),b(y)) -> f#(x,y)
  TRS:
   a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
   f(a(x),a(y)) -> a(f(x,y))
   f(b(x),b(y)) -> b(f(x,y))
  ADG Processor:
   DPs:
    a#(a(f(x,y))) -> a#(y)
    a#(a(f(x,y))) -> a#(b(a(y)))
    a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
    a#(a(f(x,y))) -> a#(x)
    a#(a(f(x,y))) -> a#(b(a(x)))
    a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    f#(a(x),a(y)) -> f#(x,y)
    f#(a(x),a(y)) -> a#(f(x,y))
    f#(b(x),b(y)) -> f#(x,y)
   TRS:
    a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    f(a(x),a(y)) -> a(f(x,y))
    f(b(x),b(y)) -> b(f(x,y))
   graph:
    f#(b(x),b(y)) -> f#(x,y) -> f#(a(x),a(y)) -> f#(x,y)
    f#(b(x),b(y)) -> f#(x,y) -> f#(a(x),a(y)) -> a#(f(x,y))
    f#(b(x),b(y)) -> f#(x,y) -> f#(b(x),b(y)) -> f#(x,y)
    f#(a(x),a(y)) -> f#(x,y) -> f#(a(x),a(y)) -> f#(x,y)
    f#(a(x),a(y)) -> f#(x,y) -> f#(a(x),a(y)) -> a#(f(x,y))
    f#(a(x),a(y)) -> f#(x,y) -> f#(b(x),b(y)) -> f#(x,y)
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(y)
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(y)))
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(x)
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(x)))
    f#(a(x),a(y)) -> a#(f(x,y)) -> a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
    f#(a(x),a(y)) -> a#(f(x,y)) ->
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) ->
    f#(a(x),a(y)) -> f#(x,y)
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y)))))) ->
    f#(a(x),a(y)) -> a#(f(x,y))
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(y)
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(y)))
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(x)
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(x)))
    a#(a(f(x,y))) -> a#(y) -> a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
    a#(a(f(x,y))) -> a#(y) ->
    a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(y)
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(y)))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(b(a(y)))))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(x)
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(x)))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> a#(b(a(b(a(x)))))
    a#(a(f(x,y))) -> a#(x) -> a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
   SCC Processor:
    #sccs: 1
    #rules: 6
    #arcs: 29/100
    DPs:
     f#(b(x),b(y)) -> f#(x,y)
     f#(a(x),a(y)) -> a#(f(x,y))
     a#(a(f(x,y))) -> f#(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
     f#(a(x),a(y)) -> f#(x,y)
     a#(a(f(x,y))) -> a#(x)
     a#(a(f(x,y))) -> a#(y)
    TRS:
     a(a(f(x,y))) -> f(a(b(a(b(a(x))))),a(b(a(b(a(y))))))
     f(a(x),a(y)) -> a(f(x,y))
     f(b(x),b(y)) -> b(f(x,y))
    Open