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