MAYBE Problem: a(a(x)) -> b(c(x)) b(b(x)) -> a(c(x)) c(c(x)) -> a(b(x)) Proof: DP Processor: DPs: a#(a(x)) -> c#(x) a#(a(x)) -> b#(c(x)) b#(b(x)) -> c#(x) b#(b(x)) -> a#(c(x)) c#(c(x)) -> b#(x) c#(c(x)) -> a#(b(x)) TRS: a(a(x)) -> b(c(x)) b(b(x)) -> a(c(x)) c(c(x)) -> a(b(x)) ADG Processor: DPs: a#(a(x)) -> c#(x) a#(a(x)) -> b#(c(x)) b#(b(x)) -> c#(x) b#(b(x)) -> a#(c(x)) c#(c(x)) -> b#(x) c#(c(x)) -> a#(b(x)) TRS: a(a(x)) -> b(c(x)) b(b(x)) -> a(c(x)) c(c(x)) -> a(b(x)) graph: b#(b(x)) -> c#(x) -> c#(c(x)) -> b#(x) b#(b(x)) -> c#(x) -> c#(c(x)) -> a#(b(x)) b#(b(x)) -> a#(c(x)) -> a#(a(x)) -> c#(x) b#(b(x)) -> a#(c(x)) -> a#(a(x)) -> b#(c(x)) c#(c(x)) -> b#(x) -> b#(b(x)) -> c#(x) c#(c(x)) -> b#(x) -> b#(b(x)) -> a#(c(x)) c#(c(x)) -> a#(b(x)) -> a#(a(x)) -> c#(x) c#(c(x)) -> a#(b(x)) -> a#(a(x)) -> b#(c(x)) a#(a(x)) -> b#(c(x)) -> b#(b(x)) -> c#(x) a#(a(x)) -> b#(c(x)) -> b#(b(x)) -> a#(c(x)) a#(a(x)) -> c#(x) -> c#(c(x)) -> b#(x) a#(a(x)) -> c#(x) -> c#(c(x)) -> a#(b(x)) Restore Modifier: DPs: a#(a(x)) -> c#(x) a#(a(x)) -> b#(c(x)) b#(b(x)) -> c#(x) b#(b(x)) -> a#(c(x)) c#(c(x)) -> b#(x) c#(c(x)) -> a#(b(x)) TRS: a(a(x)) -> b(c(x)) b(b(x)) -> a(c(x)) c(c(x)) -> a(b(x)) SCC Processor: #sccs: 1 #rules: 6 #arcs: 12/36 DPs: b#(b(x)) -> c#(x) c#(c(x)) -> a#(b(x)) a#(a(x)) -> b#(c(x)) b#(b(x)) -> a#(c(x)) a#(a(x)) -> c#(x) c#(c(x)) -> b#(x) TRS: a(a(x)) -> b(c(x)) b(b(x)) -> a(c(x)) c(c(x)) -> a(b(x)) Open