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))
  EDG 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))))))
   Restore Modifier:
    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))
    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