YES Problem: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) Proof: DP Processor: DPs: a#(x1) -> b#(x1) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> b#(a(a(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(b(x1))) -> b#(a(b(x1))) a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) TDG Processor: DPs: a#(x1) -> b#(x1) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> b#(a(a(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(b(x1))) -> b#(a(b(x1))) a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) graph: b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(b(x1))) -> b#(b(a(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(b(x1))) -> b#(a(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> a#(b(a(a(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> b#(a(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(x1)) -> a#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(b(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(a(x1))) -> b#(a(a(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(x1)) -> b#(a(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(b(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> b#(a(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(x1)) -> a#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(b(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> b#(a(a(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(x1)) -> a#(b(a(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(x1)) -> b#(a(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(a(b(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(a(b(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(x1) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(x1)) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(x1) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(b(x1))) -> b#(a(b(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(a(x1))) -> b#(a(a(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(b(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(x1)) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(x1)) -> b#(a(x1)) a#(a(b(x1))) -> a#(b(b(a(b(x1))))) -> a#(x1) -> b#(x1) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) -> b#(x1) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(a(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) -> b#(x1) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(b(x1))) -> b#(a(b(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(a(x1))) -> b#(a(a(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) a#(a(a(x1))) -> a#(b(a(a(x1)))) -> a#(x1) -> b#(x1) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(b(x1))) -> b#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(a(x1))) -> b#(a(a(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(x1)) -> b#(b(x1)) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(x1)) -> b#(a(x1)) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(x1) -> b#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(x1)) -> b#(a(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(a(x1)) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(a(x1)) -> b#(x1) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(x1) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(b(x1))) -> a#(b(b(a(b(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(b(x1))) -> b#(b(a(b(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(b(x1))) -> b#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> a#(b(a(a(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> b#(a(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(x1)) -> b#(b(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(x1)) -> b#(b(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(x1) -> b#(x1) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = 0, [a#](x0) = x0 + 0, [b](x0) = 0, [a](x0) = 9x0 + 0 orientation: a#(x1) = x1 + 0 >= 0 = b#(x1) a#(a(x1)) = 9x1 + 0 >= 0 = b#(a(x1)) a#(a(x1)) = 9x1 + 0 >= 0 = a#(b(a(x1))) a#(b(x1)) = 0 >= 0 = b#(b(x1)) a#(b(x1)) = 0 >= 0 = b#(b(b(x1))) a#(a(a(x1))) = 18x1 + 9 >= 0 = b#(a(a(x1))) a#(a(a(x1))) = 18x1 + 9 >= 0 = a#(b(a(a(x1)))) a#(a(a(x1))) = 18x1 + 9 >= 9 = a#(a(b(a(a(x1))))) a#(a(b(x1))) = 9 >= 0 = b#(a(b(x1))) a#(a(b(x1))) = 9 >= 0 = b#(b(a(b(x1)))) a#(a(b(x1))) = 9 >= 0 = a#(b(b(a(b(x1))))) a#(b(a(x1))) = 0 >= 0 = b#(b(a(x1))) a#(b(a(x1))) = 0 >= 0 = a#(b(b(a(x1)))) a#(b(a(x1))) = 0 >= 0 = b#(a(b(b(a(x1))))) a#(b(b(x1))) = 0 >= 0 = b#(b(b(x1))) a#(b(b(x1))) = 0 >= 0 = b#(b(b(b(x1)))) a#(b(b(x1))) = 0 >= 0 = b#(b(b(b(b(x1))))) b#(a(x1)) = 0 >= 0 = b#(x1) b#(a(x1)) = 0 >= 0 = b#(b(x1)) b#(a(x1)) = 0 >= 0 = b#(b(b(x1))) a#(b(a(x1))) = 0 >= 0 = b#(x1) a#(b(a(x1))) = 0 >= 0 = a#(b(x1)) a#(b(a(x1))) = 0 >= 0 = b#(a(b(x1))) a#(b(a(x1))) = 0 >= 0 = b#(b(a(b(x1)))) a#(b(a(x1))) = 0 >= 0 = a#(b(b(a(b(x1))))) b#(a(a(x1))) = 0 >= 0 = b#(a(x1)) b#(a(a(x1))) = 0 >= 0 = b#(b(a(x1))) b#(a(a(x1))) = 0 >= 0 = a#(b(b(a(x1)))) b#(a(a(x1))) = 0 >= 0 = b#(a(b(b(a(x1))))) b#(b(a(x1))) = 0 >= 0 = b#(x1) b#(b(a(x1))) = 0 >= 0 = b#(b(x1)) b#(b(a(x1))) = 0 >= 0 = b#(b(b(x1))) b#(b(a(x1))) = 0 >= 0 = b#(b(b(b(x1)))) b#(b(a(x1))) = 0 >= 0 = b#(b(b(b(b(x1))))) a(x1) = 9x1 + 0 >= 0 = b(x1) a(a(x1)) = 18x1 + 9 >= 9 = a(b(a(x1))) a(b(x1)) = 9 >= 0 = b(b(b(x1))) a(a(a(x1))) = 27x1 + 18 >= 18 = a(a(b(a(a(x1))))) a(a(b(x1))) = 18 >= 9 = a(b(b(a(b(x1))))) a(b(a(x1))) = 9 >= 0 = b(a(b(b(a(x1))))) a(b(b(x1))) = 9 >= 0 = b(b(b(b(b(x1))))) b(a(x1)) = 0 >= 0 = b(b(b(x1))) a(b(a(x1))) = 9 >= 9 = a(b(b(a(b(x1))))) b(a(a(x1))) = 0 >= 0 = b(a(b(b(a(x1))))) b(b(a(x1))) = 0 >= 0 = b(b(b(b(b(x1))))) problem: DPs: a#(x1) -> b#(x1) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) EDG Processor: DPs: a#(x1) -> b#(x1) a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) graph: b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(x1)) -> a#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(x1)) -> b#(a(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(x1)) -> b#(a(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(x1)) -> a#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(x1)) -> b#(a(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(x1)) -> a#(b(a(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(x1) -> b#(x1) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(x1)) -> b#(a(x1)) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(x1)) -> b#(b(x1)) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(a(x1)) -> b#(a(x1)) -> b#(a(x1)) -> b#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(a(x1)) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(x1) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(x1)) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(a(x1)) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(x1) -> b#(x1) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> b#(a(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(x1)) -> a#(b(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(x1)) -> b#(b(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(x1)) -> b#(b(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(x1) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(x1)) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(a(x1)) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = 0, [a#](x0) = x0 + 0, [b](x0) = 0, [a](x0) = x0 + 2 orientation: a#(x1) = x1 + 0 >= 0 = b#(x1) a#(a(x1)) = x1 + 2 >= 0 = b#(a(x1)) a#(a(x1)) = x1 + 2 >= 0 = a#(b(a(x1))) a#(b(x1)) = 0 >= 0 = b#(b(x1)) a#(b(x1)) = 0 >= 0 = b#(b(b(x1))) a#(a(a(x1))) = x1 + 2 >= 2 = a#(a(b(a(a(x1))))) a#(b(a(x1))) = 0 >= 0 = b#(b(a(x1))) a#(b(a(x1))) = 0 >= 0 = a#(b(b(a(x1)))) a#(b(a(x1))) = 0 >= 0 = b#(a(b(b(a(x1))))) a#(b(b(x1))) = 0 >= 0 = b#(b(b(x1))) a#(b(b(x1))) = 0 >= 0 = b#(b(b(b(x1)))) a#(b(b(x1))) = 0 >= 0 = b#(b(b(b(b(x1))))) b#(a(x1)) = 0 >= 0 = b#(x1) b#(a(x1)) = 0 >= 0 = b#(b(x1)) b#(a(x1)) = 0 >= 0 = b#(b(b(x1))) a#(b(a(x1))) = 0 >= 0 = b#(x1) a#(b(a(x1))) = 0 >= 0 = a#(b(x1)) a#(b(a(x1))) = 0 >= 0 = b#(a(b(x1))) a#(b(a(x1))) = 0 >= 0 = b#(b(a(b(x1)))) a#(b(a(x1))) = 0 >= 0 = a#(b(b(a(b(x1))))) b#(a(a(x1))) = 0 >= 0 = b#(a(x1)) b#(a(a(x1))) = 0 >= 0 = b#(b(a(x1))) b#(a(a(x1))) = 0 >= 0 = a#(b(b(a(x1)))) b#(a(a(x1))) = 0 >= 0 = b#(a(b(b(a(x1))))) b#(b(a(x1))) = 0 >= 0 = b#(x1) b#(b(a(x1))) = 0 >= 0 = b#(b(x1)) b#(b(a(x1))) = 0 >= 0 = b#(b(b(x1))) b#(b(a(x1))) = 0 >= 0 = b#(b(b(b(x1)))) b#(b(a(x1))) = 0 >= 0 = b#(b(b(b(b(x1))))) a(x1) = x1 + 2 >= 0 = b(x1) a(a(x1)) = x1 + 2 >= 2 = a(b(a(x1))) a(b(x1)) = 2 >= 0 = b(b(b(x1))) a(a(a(x1))) = x1 + 2 >= 2 = a(a(b(a(a(x1))))) a(a(b(x1))) = 2 >= 2 = a(b(b(a(b(x1))))) a(b(a(x1))) = 2 >= 0 = b(a(b(b(a(x1))))) a(b(b(x1))) = 2 >= 0 = b(b(b(b(b(x1))))) b(a(x1)) = 0 >= 0 = b(b(b(x1))) a(b(a(x1))) = 2 >= 2 = a(b(b(a(b(x1))))) b(a(a(x1))) = 0 >= 0 = b(a(b(b(a(x1))))) b(b(a(x1))) = 0 >= 0 = b(b(b(b(b(x1))))) problem: DPs: a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) EDG Processor: DPs: a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) graph: b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(x1)) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(x1) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(a(a(x1))) -> a#(a(b(a(a(x1))))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(x1)) -> b#(b(b(x1))) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(x1)) -> b#(b(x1)) a#(a(a(x1))) -> a#(a(b(a(a(x1))))) -> a#(x1) -> b#(x1) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = 8, [a#](x0) = x0 + 8, [b](x0) = 0, [a](x0) = 8x0 + 1 orientation: a#(x1) = x1 + 8 >= 8 = b#(x1) a#(b(x1)) = 8 >= 8 = b#(b(x1)) a#(b(x1)) = 8 >= 8 = b#(b(b(x1))) a#(a(a(x1))) = 16x1 + 9 >= 8 = a#(a(b(a(a(x1))))) a#(b(a(x1))) = 8 >= 8 = b#(b(a(x1))) a#(b(a(x1))) = 8 >= 8 = a#(b(b(a(x1)))) a#(b(a(x1))) = 8 >= 8 = b#(a(b(b(a(x1))))) a#(b(b(x1))) = 8 >= 8 = b#(b(b(x1))) a#(b(b(x1))) = 8 >= 8 = b#(b(b(b(x1)))) a#(b(b(x1))) = 8 >= 8 = b#(b(b(b(b(x1))))) b#(a(x1)) = 8 >= 8 = b#(x1) b#(a(x1)) = 8 >= 8 = b#(b(x1)) b#(a(x1)) = 8 >= 8 = b#(b(b(x1))) a#(b(a(x1))) = 8 >= 8 = b#(x1) a#(b(a(x1))) = 8 >= 8 = a#(b(x1)) a#(b(a(x1))) = 8 >= 8 = b#(a(b(x1))) a#(b(a(x1))) = 8 >= 8 = b#(b(a(b(x1)))) a#(b(a(x1))) = 8 >= 8 = a#(b(b(a(b(x1))))) b#(a(a(x1))) = 8 >= 8 = b#(a(x1)) b#(a(a(x1))) = 8 >= 8 = b#(b(a(x1))) b#(a(a(x1))) = 8 >= 8 = a#(b(b(a(x1)))) b#(a(a(x1))) = 8 >= 8 = b#(a(b(b(a(x1))))) b#(b(a(x1))) = 8 >= 8 = b#(x1) b#(b(a(x1))) = 8 >= 8 = b#(b(x1)) b#(b(a(x1))) = 8 >= 8 = b#(b(b(x1))) b#(b(a(x1))) = 8 >= 8 = b#(b(b(b(x1)))) b#(b(a(x1))) = 8 >= 8 = b#(b(b(b(b(x1))))) a(x1) = 8x1 + 1 >= 0 = b(x1) a(a(x1)) = 16x1 + 9 >= 8 = a(b(a(x1))) a(b(x1)) = 8 >= 0 = b(b(b(x1))) a(a(a(x1))) = 24x1 + 17 >= 16 = a(a(b(a(a(x1))))) a(a(b(x1))) = 16 >= 8 = a(b(b(a(b(x1))))) a(b(a(x1))) = 8 >= 0 = b(a(b(b(a(x1))))) a(b(b(x1))) = 8 >= 0 = b(b(b(b(b(x1))))) b(a(x1)) = 0 >= 0 = b(b(b(x1))) a(b(a(x1))) = 8 >= 8 = a(b(b(a(b(x1))))) b(a(a(x1))) = 0 >= 0 = b(a(b(b(a(x1))))) b(b(a(x1))) = 0 >= 0 = b(b(b(b(b(x1))))) problem: DPs: a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) EDG Processor: DPs: a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) graph: b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(b(a(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(a(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(x1) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(x1)) -> b#(b(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(x1)) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(b(a(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(x1) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(a(b(x1))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> b#(b(a(b(x1)))) a#(b(a(x1))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(a(b(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = -16x0 + 0, [a#](x0) = -4x0 + 0, [b](x0) = -4x0 + 0, [a](x0) = 4x0 + 12 orientation: a#(x1) = -4x1 + 0 >= -16x1 + 0 = b#(x1) a#(b(x1)) = -8x1 + 0 >= -20x1 + 0 = b#(b(x1)) a#(b(x1)) = -8x1 + 0 >= -24x1 + 0 = b#(b(b(x1))) a#(b(a(x1))) = -4x1 + 4 >= -16x1 + 0 = b#(b(a(x1))) a#(b(a(x1))) = -4x1 + 4 >= -8x1 + 0 = a#(b(b(a(x1)))) a#(b(a(x1))) = -4x1 + 4 >= -16x1 + 0 = b#(a(b(b(a(x1))))) a#(b(b(x1))) = -12x1 + 0 >= -24x1 + 0 = b#(b(b(x1))) a#(b(b(x1))) = -12x1 + 0 >= -28x1 + 0 = b#(b(b(b(x1)))) a#(b(b(x1))) = -12x1 + 0 >= -32x1 + 0 = b#(b(b(b(b(x1))))) b#(a(x1)) = -12x1 + 0 >= -16x1 + 0 = b#(x1) b#(a(x1)) = -12x1 + 0 >= -20x1 + 0 = b#(b(x1)) b#(a(x1)) = -12x1 + 0 >= -24x1 + 0 = b#(b(b(x1))) a#(b(a(x1))) = -4x1 + 4 >= -16x1 + 0 = b#(x1) a#(b(a(x1))) = -4x1 + 4 >= -8x1 + 0 = a#(b(x1)) a#(b(a(x1))) = -4x1 + 4 >= -16x1 + 0 = b#(a(b(x1))) a#(b(a(x1))) = -4x1 + 4 >= -20x1 + 0 = b#(b(a(b(x1)))) a#(b(a(x1))) = -4x1 + 4 >= -12x1 + 0 = a#(b(b(a(b(x1))))) b#(a(a(x1))) = -8x1 + 0 >= -12x1 + 0 = b#(a(x1)) b#(a(a(x1))) = -8x1 + 0 >= -16x1 + 0 = b#(b(a(x1))) b#(a(a(x1))) = -8x1 + 0 >= -8x1 + 0 = a#(b(b(a(x1)))) b#(a(a(x1))) = -8x1 + 0 >= -16x1 + 0 = b#(a(b(b(a(x1))))) b#(b(a(x1))) = -16x1 + 0 >= -16x1 + 0 = b#(x1) b#(b(a(x1))) = -16x1 + 0 >= -20x1 + 0 = b#(b(x1)) b#(b(a(x1))) = -16x1 + 0 >= -24x1 + 0 = b#(b(b(x1))) b#(b(a(x1))) = -16x1 + 0 >= -28x1 + 0 = b#(b(b(b(x1)))) b#(b(a(x1))) = -16x1 + 0 >= -32x1 + 0 = b#(b(b(b(b(x1))))) a(x1) = 4x1 + 12 >= -4x1 + 0 = b(x1) a(a(x1)) = 8x1 + 16 >= 4x1 + 12 = a(b(a(x1))) a(b(x1)) = x1 + 12 >= -12x1 + 0 = b(b(b(x1))) a(a(a(x1))) = 12x1 + 20 >= 12x1 + 20 = a(a(b(a(a(x1))))) a(a(b(x1))) = 4x1 + 16 >= -4x1 + 12 = a(b(b(a(b(x1))))) a(b(a(x1))) = 4x1 + 12 >= -4x1 + 8 = b(a(b(b(a(x1))))) a(b(b(x1))) = -4x1 + 12 >= -20x1 + 0 = b(b(b(b(b(x1))))) b(a(x1)) = x1 + 8 >= -12x1 + 0 = b(b(b(x1))) a(b(a(x1))) = 4x1 + 12 >= -4x1 + 12 = a(b(b(a(b(x1))))) b(a(a(x1))) = 4x1 + 12 >= -4x1 + 8 = b(a(b(b(a(x1))))) b(b(a(x1))) = -4x1 + 4 >= -20x1 + 0 = b(b(b(b(b(x1))))) problem: DPs: a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) EDG Processor: DPs: a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) graph: b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(b(x1)))) -> b#(a(x1)) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(b(x1))) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(x1) CDG Processor: DPs: a#(x1) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(x1))) a#(b(b(x1))) -> b#(b(b(b(x1)))) a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(b(b(b(x1))))) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) graph: b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(b(a(x1))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> b#(a(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(x1) -> b#(x1) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(x1)) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(x1))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(x1)))) b#(a(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) b#(a(x1)) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) b#(a(x1)) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(x1)) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(x1)) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(x1) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(a(x1)) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(x1)) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(b(a(x1))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(x1) -> b#(x1) -> b#(a(a(x1))) -> b#(a(b(b(a(x1))))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(x1)) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(x1))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(x1)))) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(b(b(b(b(x1))))) SCC Processor: #sccs: 1 #rules: 10 #arcs: 110/324 DPs: b#(b(a(x1))) -> b#(b(x1)) b#(b(a(x1))) -> b#(x1) b#(a(a(x1))) -> b#(a(b(b(a(x1))))) b#(a(x1)) -> b#(b(x1)) b#(a(a(x1))) -> a#(b(b(a(x1)))) a#(b(x1)) -> b#(b(x1)) b#(a(a(x1))) -> b#(b(a(x1))) b#(a(a(x1))) -> b#(a(x1)) b#(a(x1)) -> b#(x1) a#(x1) -> b#(x1) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) Arctic Interpretation Processor: dimension: 1 interpretation: [b#](x0) = x0, [a#](x0) = x0 + 5, [b](x0) = -4x0 + 2, [a](x0) = 4x0 + 12 orientation: b#(b(a(x1))) = x1 + 8 >= -4x1 + 2 = b#(b(x1)) b#(b(a(x1))) = x1 + 8 >= x1 = b#(x1) b#(a(a(x1))) = 8x1 + 16 >= x1 + 12 = b#(a(b(b(a(x1))))) b#(a(x1)) = 4x1 + 12 >= -4x1 + 2 = b#(b(x1)) b#(a(a(x1))) = 8x1 + 16 >= -4x1 + 5 = a#(b(b(a(x1)))) a#(b(x1)) = -4x1 + 5 >= -4x1 + 2 = b#(b(x1)) b#(a(a(x1))) = 8x1 + 16 >= x1 + 8 = b#(b(a(x1))) b#(a(a(x1))) = 8x1 + 16 >= 4x1 + 12 = b#(a(x1)) b#(a(x1)) = 4x1 + 12 >= x1 = b#(x1) a#(x1) = x1 + 5 >= x1 = b#(x1) a(x1) = 4x1 + 12 >= -4x1 + 2 = b(x1) a(a(x1)) = 8x1 + 16 >= 4x1 + 12 = a(b(a(x1))) a(b(x1)) = x1 + 12 >= -12x1 + 2 = b(b(b(x1))) a(a(a(x1))) = 12x1 + 20 >= 12x1 + 20 = a(a(b(a(a(x1))))) a(a(b(x1))) = 4x1 + 16 >= -4x1 + 12 = a(b(b(a(b(x1))))) a(b(a(x1))) = 4x1 + 12 >= -4x1 + 8 = b(a(b(b(a(x1))))) a(b(b(x1))) = -4x1 + 12 >= -20x1 + 2 = b(b(b(b(b(x1))))) b(a(x1)) = x1 + 8 >= -12x1 + 2 = b(b(b(x1))) a(b(a(x1))) = 4x1 + 12 >= -4x1 + 12 = a(b(b(a(b(x1))))) b(a(a(x1))) = 4x1 + 12 >= -4x1 + 8 = b(a(b(b(a(x1))))) b(b(a(x1))) = -4x1 + 4 >= -20x1 + 2 = b(b(b(b(b(x1))))) problem: DPs: b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) EDG Processor: DPs: b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) graph: b#(b(a(x1))) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) a#(x1) -> b#(x1) -> b#(b(a(x1))) -> b#(x1) CDG Processor: DPs: b#(b(a(x1))) -> b#(x1) a#(b(x1)) -> b#(b(x1)) a#(x1) -> b#(x1) TRS: a(x1) -> b(x1) a(a(x1)) -> a(b(a(x1))) a(b(x1)) -> b(b(b(x1))) a(a(a(x1))) -> a(a(b(a(a(x1))))) a(a(b(x1))) -> a(b(b(a(b(x1))))) a(b(a(x1))) -> b(a(b(b(a(x1))))) a(b(b(x1))) -> b(b(b(b(b(x1))))) b(a(x1)) -> b(b(b(x1))) a(b(a(x1))) -> a(b(b(a(b(x1))))) b(a(a(x1))) -> b(a(b(b(a(x1))))) b(b(a(x1))) -> b(b(b(b(b(x1))))) graph: a#(b(x1)) -> b#(b(x1)) -> b#(b(a(x1))) -> b#(x1) SCC Processor: #sccs: 0 #rules: 0 #arcs: 1/9