MAYBE Problem: a(x1) -> x1 a(a(b(x1))) -> c(c(c(x1))) c(x1) -> b(a(x1)) c(b(x1)) -> x1 Proof: DP Processor: DPs: a#(a(b(x1))) -> c#(x1) a#(a(b(x1))) -> c#(c(x1)) a#(a(b(x1))) -> c#(c(c(x1))) c#(x1) -> a#(x1) TRS: a(x1) -> x1 a(a(b(x1))) -> c(c(c(x1))) c(x1) -> b(a(x1)) c(b(x1)) -> x1 TDG Processor: DPs: a#(a(b(x1))) -> c#(x1) a#(a(b(x1))) -> c#(c(x1)) a#(a(b(x1))) -> c#(c(c(x1))) c#(x1) -> a#(x1) TRS: a(x1) -> x1 a(a(b(x1))) -> c(c(c(x1))) c(x1) -> b(a(x1)) c(b(x1)) -> x1 graph: c#(x1) -> a#(x1) -> a#(a(b(x1))) -> c#(c(c(x1))) c#(x1) -> a#(x1) -> a#(a(b(x1))) -> c#(c(x1)) c#(x1) -> a#(x1) -> a#(a(b(x1))) -> c#(x1) a#(a(b(x1))) -> c#(c(c(x1))) -> c#(x1) -> a#(x1) a#(a(b(x1))) -> c#(c(x1)) -> c#(x1) -> a#(x1) a#(a(b(x1))) -> c#(x1) -> c#(x1) -> a#(x1) Open