MAYBE Problem: c(c(b(c(x)))) -> b(a(0(),c(x))) c(c(x)) -> b(c(b(c(x)))) a(0(),x) -> c(c(x)) Proof: DP Processor: DPs: c#(c(b(c(x)))) -> a#(0(),c(x)) c#(c(x)) -> c#(b(c(x))) a#(0(),x) -> c#(x) a#(0(),x) -> c#(c(x)) TRS: c(c(b(c(x)))) -> b(a(0(),c(x))) c(c(x)) -> b(c(b(c(x)))) a(0(),x) -> c(c(x)) ADG Processor: DPs: c#(c(b(c(x)))) -> a#(0(),c(x)) c#(c(x)) -> c#(b(c(x))) a#(0(),x) -> c#(x) a#(0(),x) -> c#(c(x)) TRS: c(c(b(c(x)))) -> b(a(0(),c(x))) c(c(x)) -> b(c(b(c(x)))) a(0(),x) -> c(c(x)) graph: a#(0(),x) -> c#(c(x)) -> c#(c(b(c(x)))) -> a#(0(),c(x)) a#(0(),x) -> c#(c(x)) -> c#(c(x)) -> c#(b(c(x))) a#(0(),x) -> c#(x) -> c#(c(b(c(x)))) -> a#(0(),c(x)) a#(0(),x) -> c#(x) -> c#(c(x)) -> c#(b(c(x))) c#(c(b(c(x)))) -> a#(0(),c(x)) -> a#(0(),x) -> c#(x) c#(c(b(c(x)))) -> a#(0(),c(x)) -> a#(0(),x) -> c#(c(x)) SCC Processor: #sccs: 1 #rules: 3 #arcs: 6/16 DPs: a#(0(),x) -> c#(c(x)) c#(c(b(c(x)))) -> a#(0(),c(x)) a#(0(),x) -> c#(x) TRS: c(c(b(c(x)))) -> b(a(0(),c(x))) c(c(x)) -> b(c(b(c(x)))) a(0(),x) -> c(c(x)) Open