MAYBE Problem: g(x,a(),b()) -> g(b(),b(),a()) Proof: DP Processor: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: g(x,a(),b()) -> g(b(),b(),a()) Usable Rule Processor: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: Restore Modifier: DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: g(x,a(),b()) -> g(b(),b(),a()) SCC Processor: #sccs: 1 #rules: 1 #arcs: 1/1 DPs: g#(x,a(),b()) -> g#(b(),b(),a()) TRS: g(x,a(),b()) -> g(b(),b(),a()) Open