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