MAYBE Problem: b(b(x1)) -> a(a(a(x1))) b(a(b(x1))) -> a(x1) b(a(a(x1))) -> b(a(b(x1))) Proof: DP Processor: DPs: b#(a(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(x1))) TRS: b(b(x1)) -> a(a(a(x1))) b(a(b(x1))) -> a(x1) b(a(a(x1))) -> b(a(b(x1))) SCC Processor: #sccs: 1 #rules: 2 #arcs: 4/4 DPs: b#(a(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(x1))) TRS: b(b(x1)) -> a(a(a(x1))) b(a(b(x1))) -> a(x1) b(a(a(x1))) -> b(a(b(x1))) Open