YES Problem: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) Proof: DP Processor: DPs: a#(a(a(a(x1)))) -> b#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(b(b(x1))) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(b(b(c(c(x1)))))) -> a#(x1) b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) b#(b(b(b(x1)))) -> a#(x1) b#(b(b(b(x1)))) -> a#(a(x1)) b#(b(b(b(x1)))) -> a#(a(a(x1))) b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) -> c#(x1) c#(c(a(a(x1)))) -> c#(c(x1)) c#(c(a(a(x1)))) -> a#(c(c(x1))) c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) TDG Processor: DPs: a#(a(a(a(x1)))) -> b#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(b(b(x1))) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(b(b(c(c(x1)))))) -> a#(x1) b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) b#(b(b(b(x1)))) -> a#(x1) b#(b(b(b(x1)))) -> a#(a(x1)) b#(b(b(b(x1)))) -> a#(a(a(x1))) b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) -> c#(x1) c#(c(a(a(x1)))) -> c#(c(x1)) c#(c(a(a(x1)))) -> a#(c(c(x1))) c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) graph: c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> a#(c(c(x1))) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> c#(c(x1)) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> c#(x1) c#(c(a(a(x1)))) -> c#(x1) -> c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) c#(c(a(a(x1)))) -> c#(x1) -> c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) -> c#(x1) -> c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) c#(c(a(a(x1)))) -> c#(x1) -> c#(c(a(a(x1)))) -> a#(c(c(x1))) c#(c(a(a(x1)))) -> c#(x1) -> c#(c(a(a(x1)))) -> c#(c(x1)) c#(c(a(a(x1)))) -> c#(x1) -> c#(c(a(a(x1)))) -> c#(x1) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(x1)) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(x1) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(c(c(x1)))))) -> a#(x1) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(a(a(x1)))) -> b#(b(x1)) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(a(a(x1)))) -> b#(x1) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(x1)) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(x1) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(c(c(x1)))))) -> a#(x1) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(a(a(x1)))) -> b#(b(x1)) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(a(a(x1)))) -> b#(x1) c#(c(a(a(x1)))) -> a#(c(c(x1))) -> a#(a(a(a(x1)))) -> b#(b(x1)) c#(c(a(a(x1)))) -> a#(c(c(x1))) -> a#(a(a(a(x1)))) -> b#(x1) c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) -> a#(a(a(a(x1)))) -> b#(b(x1)) c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> a#(c(c(x1))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> c#(c(x1)) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> c#(x1) b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) -> c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) -> c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) -> c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) -> c#(c(a(a(x1)))) -> a#(c(c(x1))) b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) -> c#(c(a(a(x1)))) -> c#(c(x1)) b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) -> c#(c(a(a(x1)))) -> c#(x1) b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(c(c(x1)))))) -> a#(x1) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(c(c(x1)))))) -> a#(x1) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(a(x1))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(a(x1))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(x1)) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> a#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(x1)) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> a#(x1) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> a#(b(b(x1))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(b(b(x1))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) -> a#(a(a(a(x1)))) -> b#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(x1)) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> a#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> b#(b(x1)) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> b#(x1) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(x1)) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> c#(a(a(x1))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> a#(a(x1)) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> a#(x1) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> b#(b(x1)) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> b#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [c#](x0) = 4x0 + 0, [b#](x0) = x0, [a#](x0) = x0 + 0, [c](x0) = 4x0 + 11, [b](x0) = x0 + 0, [a](x0) = x0 + 0 orientation: a#(a(a(a(x1)))) = x1 + 0 >= x1 = b#(x1) a#(a(a(a(x1)))) = x1 + 0 >= x1 + 0 = b#(b(x1)) b#(b(a(a(x1)))) = x1 + 0 >= x1 = b#(x1) b#(b(a(a(x1)))) = x1 + 0 >= x1 + 0 = b#(b(x1)) b#(b(a(a(x1)))) = x1 + 0 >= x1 + 0 = a#(b(b(x1))) b#(b(a(a(x1)))) = x1 + 0 >= x1 + 0 = a#(a(b(b(x1)))) b#(b(b(b(c(c(x1)))))) = 8x1 + 15 >= x1 + 0 = a#(x1) b#(b(b(b(c(c(x1)))))) = 8x1 + 15 >= x1 + 0 = a#(a(x1)) b#(b(b(b(c(c(x1)))))) = 8x1 + 15 >= 4x1 + 4 = c#(a(a(x1))) b#(b(b(b(c(c(x1)))))) = 8x1 + 15 >= 8x1 + 15 = c#(c(a(a(x1)))) b#(b(b(b(x1)))) = x1 + 0 >= x1 + 0 = a#(x1) b#(b(b(b(x1)))) = x1 + 0 >= x1 + 0 = a#(a(x1)) b#(b(b(b(x1)))) = x1 + 0 >= x1 + 0 = a#(a(a(x1))) b#(b(b(b(x1)))) = x1 + 0 >= x1 + 0 = a#(a(a(a(x1)))) b#(b(b(b(x1)))) = x1 + 0 >= x1 + 0 = a#(a(a(a(a(x1))))) b#(b(b(b(x1)))) = x1 + 0 >= x1 + 0 = a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) = 8x1 + 15 >= 4x1 + 0 = c#(x1) c#(c(a(a(x1)))) = 8x1 + 15 >= 8x1 + 15 = c#(c(x1)) c#(c(a(a(x1)))) = 8x1 + 15 >= 8x1 + 15 = a#(c(c(x1))) c#(c(a(a(x1)))) = 8x1 + 15 >= 8x1 + 15 = a#(a(c(c(x1)))) c#(c(a(a(x1)))) = 8x1 + 15 >= 8x1 + 15 = b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) = 8x1 + 15 >= 8x1 + 15 = b#(b(a(a(c(c(x1)))))) a(a(a(a(x1)))) = x1 + 0 >= x1 + 0 = b(b(x1)) b(b(a(a(x1)))) = x1 + 0 >= x1 + 0 = a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) = 8x1 + 15 >= 8x1 + 15 = c(c(a(a(x1)))) b(b(b(b(x1)))) = x1 + 0 >= x1 + 0 = a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) = 8x1 + 15 >= 8x1 + 15 = b(b(a(a(c(c(x1)))))) problem: DPs: a#(a(a(a(x1)))) -> b#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(b(b(x1))) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) b#(b(b(b(x1)))) -> a#(x1) b#(b(b(b(x1)))) -> a#(a(x1)) b#(b(b(b(x1)))) -> a#(a(a(x1))) b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) -> c#(c(x1)) c#(c(a(a(x1)))) -> a#(c(c(x1))) c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) EDG Processor: DPs: a#(a(a(a(x1)))) -> b#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(b(b(x1))) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) b#(b(b(b(x1)))) -> a#(x1) b#(b(b(b(x1)))) -> a#(a(x1)) b#(b(b(b(x1)))) -> a#(a(a(x1))) b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) -> c#(c(x1)) c#(c(a(a(x1)))) -> a#(c(c(x1))) c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) graph: c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> c#(c(x1)) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> a#(c(c(x1))) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) -> c#(c(x1)) -> c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(a(a(x1)))) -> b#(x1) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(a(a(x1)))) -> b#(b(x1)) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(x1) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(x1)) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(a(a(x1)))) -> b#(x1) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(a(a(x1)))) -> b#(b(x1)) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(x1) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(x1)) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) -> a#(c(c(x1))) -> a#(a(a(a(x1)))) -> b#(x1) c#(c(a(a(x1)))) -> a#(c(c(x1))) -> a#(a(a(a(x1)))) -> b#(b(x1)) c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) -> a#(a(a(a(x1)))) -> b#(x1) c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> c#(c(x1)) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> a#(c(c(x1))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> a#(a(c(c(x1)))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> b#(a(a(c(c(x1))))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) -> c#(c(a(a(x1)))) -> b#(b(a(a(c(c(x1)))))) b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(a(x1))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(a(x1))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(a(x1)) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(b(b(x1)))) -> a#(x1) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(x1) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(x1)) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) b#(b(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(x1)) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) b#(b(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) b#(b(a(a(x1)))) -> a#(b(b(x1))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> a#(b(b(x1))) -> a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) -> a#(a(a(a(x1)))) -> b#(x1) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) -> a#(a(a(a(x1)))) -> b#(b(x1)) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> b#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> b#(b(x1)) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(x1)) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> b#(x1) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> b#(b(x1)) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(x1) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(x1)) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(x1))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(x1)))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(x1))))) a#(a(a(a(x1)))) -> b#(x1) -> b#(b(b(b(x1)))) -> a#(a(a(a(a(a(x1)))))) Matrix Interpretation Processor: dim=1 interpretation: [c#](x0) = 4x0 + 8, [b#](x0) = 2x0 + 10, [a#](x0) = 2x0 + 8, [c](x0) = 2x0 + 1, [b](x0) = x0 + 2, [a](x0) = x0 + 1 orientation: a#(a(a(a(x1)))) = 2x1 + 14 >= 2x1 + 10 = b#(x1) a#(a(a(a(x1)))) = 2x1 + 14 >= 2x1 + 14 = b#(b(x1)) b#(b(a(a(x1)))) = 2x1 + 18 >= 2x1 + 10 = b#(x1) b#(b(a(a(x1)))) = 2x1 + 18 >= 2x1 + 14 = b#(b(x1)) b#(b(a(a(x1)))) = 2x1 + 18 >= 2x1 + 16 = a#(b(b(x1))) b#(b(a(a(x1)))) = 2x1 + 18 >= 2x1 + 18 = a#(a(b(b(x1)))) b#(b(b(b(c(c(x1)))))) = 8x1 + 28 >= 8x1 + 28 = c#(c(a(a(x1)))) b#(b(b(b(x1)))) = 2x1 + 22 >= 2x1 + 8 = a#(x1) b#(b(b(b(x1)))) = 2x1 + 22 >= 2x1 + 10 = a#(a(x1)) b#(b(b(b(x1)))) = 2x1 + 22 >= 2x1 + 12 = a#(a(a(x1))) b#(b(b(b(x1)))) = 2x1 + 22 >= 2x1 + 14 = a#(a(a(a(x1)))) b#(b(b(b(x1)))) = 2x1 + 22 >= 2x1 + 16 = a#(a(a(a(a(x1))))) b#(b(b(b(x1)))) = 2x1 + 22 >= 2x1 + 18 = a#(a(a(a(a(a(x1)))))) c#(c(a(a(x1)))) = 8x1 + 28 >= 8x1 + 12 = c#(c(x1)) c#(c(a(a(x1)))) = 8x1 + 28 >= 8x1 + 14 = a#(c(c(x1))) c#(c(a(a(x1)))) = 8x1 + 28 >= 8x1 + 16 = a#(a(c(c(x1)))) c#(c(a(a(x1)))) = 8x1 + 28 >= 8x1 + 20 = b#(a(a(c(c(x1))))) c#(c(a(a(x1)))) = 8x1 + 28 >= 8x1 + 24 = b#(b(a(a(c(c(x1)))))) a(a(a(a(x1)))) = x1 + 4 >= x1 + 4 = b(b(x1)) b(b(a(a(x1)))) = x1 + 6 >= x1 + 6 = a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) = 4x1 + 11 >= 4x1 + 11 = c(c(a(a(x1)))) b(b(b(b(x1)))) = x1 + 8 >= x1 + 6 = a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) = 4x1 + 11 >= 4x1 + 9 = b(b(a(a(c(c(x1)))))) problem: DPs: a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) EDG Processor: DPs: a#(a(a(a(x1)))) -> b#(b(x1)) b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) graph: b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) -> a#(a(a(a(x1)))) -> b#(b(x1)) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(b(b(c(c(x1)))))) -> c#(c(a(a(x1)))) a#(a(a(a(x1)))) -> b#(b(x1)) -> b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) SCC Processor: #sccs: 1 #rules: 2 #arcs: 3/9 DPs: b#(b(a(a(x1)))) -> a#(a(b(b(x1)))) a#(a(a(a(x1)))) -> b#(b(x1)) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) Matrix Interpretation Processor: dim=2 interpretation: [b#](x0) = [0 1]x0 + [2], [a#](x0) = [0 1]x0 + [1], [0 1] [c](x0) = [3 0]x0, [0 1] [0] [b](x0) = [1 0]x0 + [3], [0 1] [0] [a](x0) = [1 0]x0 + [2] orientation: b#(b(a(a(x1)))) = [1 0]x1 + [7] >= [1 0]x1 + [6] = a#(a(b(b(x1)))) a#(a(a(a(x1)))) = [1 0]x1 + [5] >= [1 0]x1 + [5] = b#(b(x1)) [4] [3] a(a(a(a(x1)))) = x1 + [4] >= x1 + [3] = b(b(x1)) [5] [5] b(b(a(a(x1)))) = x1 + [5] >= x1 + [5] = a(a(b(b(x1)))) [3 0] [6] [3 0] [6] b(b(b(b(c(c(x1)))))) = [0 3]x1 + [6] >= [0 3]x1 + [6] = c(c(a(a(x1)))) [6] [6] b(b(b(b(x1)))) = x1 + [6] >= x1 + [6] = a(a(a(a(a(a(x1)))))) [3 0] [6] [3 0] [5] c(c(a(a(x1)))) = [0 3]x1 + [6] >= [0 3]x1 + [5] = b(b(a(a(c(c(x1)))))) problem: DPs: a#(a(a(a(x1)))) -> b#(b(x1)) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) EDG Processor: DPs: a#(a(a(a(x1)))) -> b#(b(x1)) TRS: a(a(a(a(x1)))) -> b(b(x1)) b(b(a(a(x1)))) -> a(a(b(b(x1)))) b(b(b(b(c(c(x1)))))) -> c(c(a(a(x1)))) b(b(b(b(x1)))) -> a(a(a(a(a(a(x1)))))) c(c(a(a(x1)))) -> b(b(a(a(c(c(x1)))))) graph: Qed