MAYBE Problem: a(b(x1)) -> c(d(x1)) d(d(x1)) -> b(e(x1)) b(x1) -> d(c(x1)) d(x1) -> x1 e(c(x1)) -> d(a(x1)) a(x1) -> e(d(x1)) Proof: DP Processor: DPs: a#(b(x1)) -> d#(x1) d#(d(x1)) -> e#(x1) d#(d(x1)) -> b#(e(x1)) b#(x1) -> d#(c(x1)) e#(c(x1)) -> a#(x1) e#(c(x1)) -> d#(a(x1)) a#(x1) -> d#(x1) a#(x1) -> e#(d(x1)) TRS: a(b(x1)) -> c(d(x1)) d(d(x1)) -> b(e(x1)) b(x1) -> d(c(x1)) d(x1) -> x1 e(c(x1)) -> d(a(x1)) a(x1) -> e(d(x1)) TDG Processor: DPs: a#(b(x1)) -> d#(x1) d#(d(x1)) -> e#(x1) d#(d(x1)) -> b#(e(x1)) b#(x1) -> d#(c(x1)) e#(c(x1)) -> a#(x1) e#(c(x1)) -> d#(a(x1)) a#(x1) -> d#(x1) a#(x1) -> e#(d(x1)) TRS: a(b(x1)) -> c(d(x1)) d(d(x1)) -> b(e(x1)) b(x1) -> d(c(x1)) d(x1) -> x1 e(c(x1)) -> d(a(x1)) a(x1) -> e(d(x1)) graph: b#(x1) -> d#(c(x1)) -> d#(d(x1)) -> b#(e(x1)) b#(x1) -> d#(c(x1)) -> d#(d(x1)) -> e#(x1) e#(c(x1)) -> d#(a(x1)) -> d#(d(x1)) -> b#(e(x1)) e#(c(x1)) -> d#(a(x1)) -> d#(d(x1)) -> e#(x1) e#(c(x1)) -> a#(x1) -> a#(x1) -> e#(d(x1)) e#(c(x1)) -> a#(x1) -> a#(x1) -> d#(x1) e#(c(x1)) -> a#(x1) -> a#(b(x1)) -> d#(x1) d#(d(x1)) -> b#(e(x1)) -> b#(x1) -> d#(c(x1)) d#(d(x1)) -> e#(x1) -> e#(c(x1)) -> d#(a(x1)) d#(d(x1)) -> e#(x1) -> e#(c(x1)) -> a#(x1) a#(b(x1)) -> d#(x1) -> d#(d(x1)) -> b#(e(x1)) a#(b(x1)) -> d#(x1) -> d#(d(x1)) -> e#(x1) a#(x1) -> e#(d(x1)) -> e#(c(x1)) -> d#(a(x1)) a#(x1) -> e#(d(x1)) -> e#(c(x1)) -> a#(x1) a#(x1) -> d#(x1) -> d#(d(x1)) -> b#(e(x1)) a#(x1) -> d#(x1) -> d#(d(x1)) -> e#(x1) EDG Processor: DPs: a#(b(x1)) -> d#(x1) d#(d(x1)) -> e#(x1) d#(d(x1)) -> b#(e(x1)) b#(x1) -> d#(c(x1)) e#(c(x1)) -> a#(x1) e#(c(x1)) -> d#(a(x1)) a#(x1) -> d#(x1) a#(x1) -> e#(d(x1)) TRS: a(b(x1)) -> c(d(x1)) d(d(x1)) -> b(e(x1)) b(x1) -> d(c(x1)) d(x1) -> x1 e(c(x1)) -> d(a(x1)) a(x1) -> e(d(x1)) graph: e#(c(x1)) -> d#(a(x1)) -> d#(d(x1)) -> e#(x1) e#(c(x1)) -> d#(a(x1)) -> d#(d(x1)) -> b#(e(x1)) e#(c(x1)) -> a#(x1) -> a#(b(x1)) -> d#(x1) e#(c(x1)) -> a#(x1) -> a#(x1) -> d#(x1) e#(c(x1)) -> a#(x1) -> a#(x1) -> e#(d(x1)) d#(d(x1)) -> b#(e(x1)) -> b#(x1) -> d#(c(x1)) d#(d(x1)) -> e#(x1) -> e#(c(x1)) -> a#(x1) d#(d(x1)) -> e#(x1) -> e#(c(x1)) -> d#(a(x1)) a#(b(x1)) -> d#(x1) -> d#(d(x1)) -> e#(x1) a#(b(x1)) -> d#(x1) -> d#(d(x1)) -> b#(e(x1)) a#(x1) -> e#(d(x1)) -> e#(c(x1)) -> a#(x1) a#(x1) -> e#(d(x1)) -> e#(c(x1)) -> d#(a(x1)) a#(x1) -> d#(x1) -> d#(d(x1)) -> e#(x1) a#(x1) -> d#(x1) -> d#(d(x1)) -> b#(e(x1)) SCC Processor: #sccs: 1 #rules: 6 #arcs: 14/64 DPs: e#(c(x1)) -> d#(a(x1)) d#(d(x1)) -> e#(x1) e#(c(x1)) -> a#(x1) a#(x1) -> e#(d(x1)) a#(x1) -> d#(x1) a#(b(x1)) -> d#(x1) TRS: a(b(x1)) -> c(d(x1)) d(d(x1)) -> b(e(x1)) b(x1) -> d(c(x1)) d(x1) -> x1 e(c(x1)) -> d(a(x1)) a(x1) -> e(d(x1)) Open