YES Problem: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) Proof: String Reversal Processor: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) DP Processor: DPs: a#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) EDG Processor: DPs: a#(a(x1)) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(a(x1))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) graph: a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(x1)) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(x1))) -> a#(b(a(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(b(a(x1))) -> a#(b(b(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(b(a(x1))) -> a#(b(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(b(a(x1))) -> a#(b(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(x1))) -> a#(b(b(x1))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(x1)) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(x1))) -> a#(b(a(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(x1)) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(b(a(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(x1)) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(x1))) -> a#(b(a(x1))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(x1)) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(x1))) -> a#(b(a(x1))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(x1)) -> a#(b(x1)) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(x1))) -> a#(b(a(x1))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(b(a(b(a(b(b(x1))))))))) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(a(x1))) -> a#(b(a(x1))) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(b(a(x1)))) -> a#(b(b(b(x1)))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(b(b(a(x1))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(b(b(a(x1))))) -> a#(b(b(b(b(x1))))) SCC Processor: #sccs: 1 #rules: 34 #arcs: 523/1444 DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(a(b(a(x1))))) -> a#(a(b(b(a(b(a(a(b(x1))))))))) a#(a(a(b(a(x1))))) -> a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(b(a(x1))))) -> a#(b(a(a(b(x1))))) a#(a(a(b(a(x1))))) -> a#(a(b(x1))) a#(a(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(a(a(a(x1))))) -> a#(a(a(b(a(b(a(a(a(x1))))))))) a#(a(a(a(a(x1))))) -> a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(a(a(x1))))) -> a#(b(a(b(a(a(a(x1))))))) a#(a(a(a(a(x1))))) -> a#(b(a(a(a(x1))))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(a(a(x1)))) -> a#(a(b(a(b(a(a(x1))))))) a#(a(a(a(x1)))) -> a#(b(a(b(a(a(x1)))))) a#(a(a(a(x1)))) -> a#(b(a(a(x1)))) a#(a(a(x1))) -> a#(b(a(b(a(x1))))) a#(a(a(x1))) -> a#(b(a(x1))) a#(a(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) Arctic Interpretation Processor: dimension: 1 usable rules: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) interpretation: [a#](x0) = x0 + 15, [b](x0) = 0, [a](x0) = 1x0 + 15 orientation: a#(b(b(a(a(x1))))) = 15 >= 15 = a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) = 15 >= 15 = a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) = 15 >= 15 = a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) = 15 >= 15 = a#(b(x1)) a#(b(a(a(a(x1))))) = 15 >= 15 = a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(b(a(x1))))) = 15 >= 15 = a#(b(a(b(b(x1))))) a#(b(a(a(a(x1))))) = 15 >= 15 = a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) = 15 >= 15 = a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) = 15 >= 15 = a#(b(a(b(b(a(x1)))))) a#(b(a(a(x1)))) = 15 >= 15 = a#(b(b(a(x1)))) a#(b(a(x1))) = 15 >= 15 = a#(b(b(x1))) a#(a(b(b(a(x1))))) = 15 >= 15 = a#(b(b(x1))) a#(a(a(b(a(x1))))) = 16 >= 15 = a#(a(b(b(a(b(a(a(b(x1))))))))) a#(a(a(b(a(x1))))) = 16 >= 15 = a#(b(b(a(b(a(a(b(x1)))))))) a#(a(a(b(a(x1))))) = 16 >= 15 = a#(b(a(a(b(x1))))) a#(a(a(b(a(x1))))) = 16 >= 15 = a#(a(b(x1))) a#(a(a(b(a(x1))))) = 16 >= 15 = a#(b(x1)) a#(a(b(a(a(x1))))) = 15 >= 15 = a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(b(a(a(x1))))) = 15 >= 15 = a#(b(a(b(a(b(a(x1))))))) a#(a(b(a(a(x1))))) = 15 >= 15 = a#(b(a(b(a(x1))))) a#(a(b(a(a(x1))))) = 15 >= 15 = a#(b(a(x1))) a#(a(a(a(a(x1))))) = 4x1 + 18 >= 16 = a#(a(a(b(a(b(a(a(a(x1))))))))) a#(a(a(a(a(x1))))) = 4x1 + 18 >= 15 = a#(a(b(a(b(a(a(a(x1)))))))) a#(a(a(a(a(x1))))) = 4x1 + 18 >= 15 = a#(b(a(b(a(a(a(x1))))))) a#(a(a(a(a(x1))))) = 4x1 + 18 >= 15 = a#(b(a(a(a(x1))))) a#(a(b(a(x1)))) = 15 >= 15 = a#(b(b(a(b(a(b(x1))))))) a#(a(b(a(x1)))) = 15 >= 15 = a#(b(a(b(x1)))) a#(a(b(a(x1)))) = 15 >= 15 = a#(b(x1)) a#(a(a(a(x1)))) = 3x1 + 17 >= 15 = a#(a(b(a(b(a(a(x1))))))) a#(a(a(a(x1)))) = 3x1 + 17 >= 15 = a#(b(a(b(a(a(x1)))))) a#(a(a(a(x1)))) = 3x1 + 17 >= 15 = a#(b(a(a(x1)))) a#(a(a(x1))) = 2x1 + 16 >= 15 = a#(b(a(b(a(x1))))) a#(a(a(x1))) = 2x1 + 16 >= 15 = a#(b(a(x1))) a#(a(x1)) = 1x1 + 15 >= 15 = a#(b(x1)) a(a(x1)) = 2x1 + 16 >= 0 = b(a(b(x1))) a(a(a(x1))) = 3x1 + 17 >= 15 = a(b(a(b(a(x1))))) a(b(a(x1))) = 15 >= 0 = b(b(a(b(b(x1))))) a(a(a(a(x1)))) = 4x1 + 18 >= 16 = a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) = 15 >= 0 = b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) = 16 >= 15 = a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) = 15 >= 0 = b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) = 5x1 + 19 >= 17 = a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) = 15 >= 0 = b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) = 16 >= 15 = a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) = 15 >= 0 = b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) = 17 >= 16 = a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) = 15 >= 0 = b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) = 16 >= 15 = a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) = 15 >= 0 = b(b(b(b(a(b(b(b(b(x1))))))))) problem: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) Restore Modifier: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) EDG Processor: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(a(b(a(x1)))) -> a#(b(x1)) a#(a(x1)) -> a#(b(x1)) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) graph: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(b(a(x1))))) -> a#(b(b(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(a(x1))))) -> a#(b(a(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(b(a(x1)))) -> a#(b(x1)) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) -> a#(a(x1)) -> a#(b(x1)) a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(x1))) -> a#(b(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(b(a(x1))))) -> a#(b(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(b(a(x1))))) -> a#(b(a(b(b(x1))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(b(a(x1))))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(b(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(b(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(a(x1))))) -> a#(b(a(x1))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(x1)))) -> a#(b(b(a(b(a(b(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(x1)))) -> a#(b(a(b(x1)))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(b(a(x1)))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(a(x1)) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(a(b(a(b(b(a(a(x1)))))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(a(b(b(a(a(x1))))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(a(x1))))) -> a#(b(b(a(a(x1))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(a(b(b(a(x1)))))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(a(x1)))) -> a#(b(b(a(x1)))) a#(a(x1)) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) Arctic Interpretation Processor: dimension: 1 usable rules: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) interpretation: [a#](x0) = 1x0 + 0, [b](x0) = -4x0 + 7, [a](x0) = 3x0 + 11 orientation: a#(b(b(a(a(x1))))) = -1x1 + 8 >= -9x1 + 8 = a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) = -1x1 + 8 >= -13x1 + 8 = a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) = -1x1 + 8 >= -8x1 + 8 = a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) = -1x1 + 8 >= -3x1 + 8 = a#(b(x1)) a#(b(a(a(a(x1))))) = 6x1 + 14 >= 1x1 + 12 = a#(a(b(a(b(b(a(a(x1)))))))) a#(a(b(b(a(x1))))) = -1x1 + 12 >= -8x1 + 8 = a#(b(a(b(b(x1))))) a#(b(a(a(a(x1))))) = 6x1 + 14 >= -2x1 + 8 = a#(b(a(b(b(a(a(x1))))))) a#(b(a(a(a(x1))))) = 6x1 + 14 >= -1x1 + 8 = a#(b(b(a(a(x1))))) a#(b(a(a(x1)))) = 3x1 + 11 >= -5x1 + 8 = a#(b(a(b(b(a(x1)))))) a#(b(a(a(x1)))) = 3x1 + 11 >= -4x1 + 8 = a#(b(b(a(x1)))) a#(b(a(x1))) = x1 + 8 >= -7x1 + 8 = a#(b(b(x1))) a#(a(b(b(a(x1))))) = -1x1 + 12 >= -7x1 + 8 = a#(b(b(x1))) a#(a(b(a(a(x1))))) = 6x1 + 14 >= -3x1 + 8 = a#(b(a(b(a(b(a(b(a(x1))))))))) a#(a(b(a(a(x1))))) = 6x1 + 14 >= -2x1 + 8 = a#(b(a(b(a(b(a(x1))))))) a#(a(b(a(a(x1))))) = 6x1 + 14 >= -1x1 + 8 = a#(b(a(b(a(x1))))) a#(a(b(a(a(x1))))) = 6x1 + 14 >= x1 + 8 = a#(b(a(x1))) a#(a(b(a(x1)))) = 3x1 + 12 >= -9x1 + 8 = a#(b(b(a(b(a(b(x1))))))) a#(a(b(a(x1)))) = 3x1 + 12 >= -4x1 + 8 = a#(b(a(b(x1)))) a#(a(b(a(x1)))) = 3x1 + 12 >= -3x1 + 8 = a#(b(x1)) a#(a(x1)) = 4x1 + 12 >= -3x1 + 8 = a#(b(x1)) a(a(x1)) = 6x1 + 14 >= -5x1 + 7 = b(a(b(x1))) a(a(a(x1))) = 9x1 + 17 >= 1x1 + 11 = a(b(a(b(a(x1))))) a(b(a(x1))) = 2x1 + 11 >= -13x1 + 7 = b(b(a(b(b(x1))))) a(a(a(a(x1)))) = 12x1 + 20 >= 7x1 + 15 = a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) = 5x1 + 13 >= -7x1 + 7 = b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) = 5x1 + 14 >= -7x1 + 11 = a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) = -2x1 + 11 >= -21x1 + 7 = b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) = 15x1 + 23 >= 13x1 + 21 = a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) = 8x1 + 16 >= -1x1 + 10 = b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) = 8x1 + 16 >= -1x1 + 11 = a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) = 1x1 + 11 >= -15x1 + 7 = b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) = 8x1 + 17 >= -1x1 + 14 = a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) = 1x1 + 11 >= -15x1 + 7 = b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) = 1x1 + 14 >= -15x1 + 11 = a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) = -6x1 + 11 >= -29x1 + 7 = b(b(b(b(a(b(b(b(b(x1))))))))) problem: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(x1))) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) Restore Modifier: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(x1))) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) EDG Processor: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(x1))) -> a#(b(b(x1))) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) graph: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(x1))) -> a#(b(b(x1))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(x1)) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) -> a#(b(x1)) -> a#(b(a(b(a(x1))))) -> a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(x1))) -> a#(b(b(x1))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) Arctic Interpretation Processor: dimension: 1 usable rules: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) interpretation: [a#](x0) = 4x0 + 0, [b](x0) = -1x0 + 12, [a](x0) = 1x0 + 15 orientation: a#(b(b(a(a(x1))))) = 4x1 + 18 >= 2x1 + 18 = a#(b(a(b(b(b(a(x1))))))) a#(b(a(b(a(x1))))) = 4x1 + 18 >= 1x1 + 17 = a#(b(b(a(b(b(a(b(x1)))))))) a#(b(a(b(a(x1))))) = 4x1 + 18 >= 2x1 + 17 = a#(b(b(a(b(x1))))) a#(b(a(b(a(x1))))) = 4x1 + 18 >= 3x1 + 16 = a#(b(x1)) a#(b(a(x1))) = 4x1 + 18 >= 2x1 + 16 = a#(b(b(x1))) a(a(x1)) = 2x1 + 16 >= -1x1 + 14 = b(a(b(x1))) a(a(a(x1))) = 3x1 + 17 >= 1x1 + 15 = a(b(a(b(a(x1))))) a(b(a(x1))) = 1x1 + 15 >= -3x1 + 13 = b(b(a(b(b(x1))))) a(a(a(a(x1)))) = 4x1 + 18 >= 3x1 + 17 = a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) = 2x1 + 16 >= -1x1 + 14 = b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) = 2x1 + 16 >= -1x1 + 15 = a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) = x1 + 15 >= -5x1 + 12 = b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) = 5x1 + 19 >= 5x1 + 19 = a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) = 3x1 + 17 >= 1x1 + 15 = b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) = 3x1 + 17 >= 1x1 + 15 = a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) = 1x1 + 15 >= -3x1 + 13 = b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) = 3x1 + 17 >= 1x1 + 16 = a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) = 1x1 + 15 >= -3x1 + 14 = b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) = 1x1 + 16 >= -3x1 + 15 = a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) = -1x1 + 15 >= -7x1 + 12 = b(b(b(b(a(b(b(b(b(x1))))))))) problem: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) Restore Modifier: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) EDG Processor: DPs: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) graph: a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) -> a#(b(b(a(a(x1))))) -> a#(b(a(b(b(b(a(x1))))))) Bounds Processor: bound: 0 enrichment: match-dp automaton: final states: {4} transitions: a0(15) -> 16* a0(2) -> 1* a0(1) -> 1* a0(8) -> 9* a0(3) -> 5* a{#,0}(10) -> 4* b0(5) -> 6* b0(17) -> 18* b0(12) -> 13* b0(7) -> 8* b0(2) -> 2* b0(19) -> 20* b0(14) -> 15* b0(9) -> 10* b0(16) -> 17* b0(11) -> 12* b0(6) -> 7* b0(1) -> 2* b0(18) -> 19* b0(13) -> 14* 1 -> 3* 2 -> 5,1,3 3 -> 11* 20 -> 9* problem: DPs: TRS: a(a(x1)) -> b(a(b(x1))) a(a(a(x1))) -> a(b(a(b(a(x1))))) a(b(a(x1))) -> b(b(a(b(b(x1))))) a(a(a(a(x1)))) -> a(a(b(a(b(a(a(x1))))))) a(b(a(a(x1)))) -> b(a(b(a(b(b(a(x1))))))) a(a(b(a(x1)))) -> a(b(b(a(b(a(b(x1))))))) a(b(b(a(x1)))) -> b(b(b(a(b(b(b(x1))))))) a(a(a(a(a(x1))))) -> a(a(a(b(a(b(a(a(a(x1))))))))) a(b(a(a(a(x1))))) -> b(a(a(b(a(b(b(a(a(x1))))))))) a(a(b(a(a(x1))))) -> a(b(a(b(a(b(a(b(a(x1))))))))) a(b(b(a(a(x1))))) -> b(b(a(b(a(b(b(b(a(x1))))))))) a(a(a(b(a(x1))))) -> a(a(b(b(a(b(a(a(b(x1))))))))) a(b(a(b(a(x1))))) -> b(a(b(b(a(b(b(a(b(x1))))))))) a(a(b(b(a(x1))))) -> a(b(b(b(a(b(a(b(b(x1))))))))) a(b(b(b(a(x1))))) -> b(b(b(b(a(b(b(b(b(x1))))))))) Qed