YES Problem: twoto(0(x1)) -> p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1)))))))))))))))) twoto(s(x1)) -> p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))) twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1))))))))))))) twice(s(x1)) -> s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1))))))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(p(s(x1))))))) 0(x1) -> x1 Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [twice](x0) = x0, [p](x0) = x0, [s](x0) = x0, [twoto](x0) = 8x0, [0](x0) = x0 orientation: twoto(0(x1)) = 8x1 >= x1 = p(p(s(s(s(p(p(p(s(s(s(0(p(p(s(s(x1)))))))))))))))) twoto(s(x1)) = 8x1 >= 8x1 = p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))) twice(0(x1)) = x1 >= x1 = p(s(p(s(0(s(p(s(s(s(s(p(s(x1))))))))))))) twice(s(x1)) = x1 >= x1 = s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1))))))))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = x1 >= x1 = 0(s(s(s(s(p(s(x1))))))) 0(x1) = x1 >= x1 = x1 problem: twoto(s(x1)) -> p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))) twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1))))))))))))) twice(s(x1)) -> s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1))))))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(p(s(x1))))))) 0(x1) -> x1 Arctic Interpretation Processor: dimension: 1 interpretation: [twice](x0) = x0, [p](x0) = x0, [s](x0) = x0, [twoto](x0) = 3x0, [0](x0) = 4x0 orientation: twoto(s(x1)) = 3x1 >= 3x1 = p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))) twice(0(x1)) = 4x1 >= 4x1 = p(s(p(s(0(s(p(s(s(s(s(p(s(x1))))))))))))) twice(s(x1)) = x1 >= x1 = s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1))))))))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = 4x1 >= 4x1 = 0(s(s(s(s(p(s(x1))))))) 0(x1) = 4x1 >= x1 = x1 problem: twoto(s(x1)) -> p(p(s(s(p(p(p(s(s(s(twice(p(p(s(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))) twice(0(x1)) -> p(s(p(s(0(s(p(s(s(s(s(p(s(x1))))))))))))) twice(s(x1)) -> s(p(p(p(p(s(s(s(s(s(twice(p(s(p(s(p(s(p(s(x1))))))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(p(s(x1))))))) String Reversal Processor: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0(twice(x1)) -> s(p(s(s(s(s(p(s(0(s(p(s(p(x1))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) Matrix Interpretation Processor: dim=2 interpretation: [1 0] [0] [twice](x0) = [0 2]x0 + [3], [p](x0) = x0, [s](x0) = x0, [1 0] [twoto](x0) = [0 0]x0, [2 2] [0](x0) = [2 0]x0 orientation: [1 0] [1 0] s(twoto(x1)) = [0 0]x1 >= [0 0]x1 = s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) [2 4] [6] [2 2] 0(twice(x1)) = [2 0]x1 + [0] >= [2 0]x1 = s(p(s(s(s(s(p(s(0(s(p(s(p(x1))))))))))))) [1 0] [0] [1 0] [0] s(twice(x1)) = [0 2]x1 + [3] >= [0 2]x1 + [3] = s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) = x1 >= x1 = p(x1) s(p(x1)) = x1 >= x1 = x1 [2 2] [2 2] 0(p(x1)) = [2 0]x1 >= [2 0]x1 = s(p(s(s(s(s(0(x1))))))) problem: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) DP Processor: DPs: s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> s#(s(0(x1))) 0#(p(x1)) -> s#(s(s(0(x1)))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) TDG Processor: DPs: s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> s#(s(0(x1))) 0#(p(x1)) -> s#(s(s(0(x1)))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) graph: 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(s(s(0(x1))))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(s(0(x1)))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(0(x1))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(p(x1))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) EDG Processor: DPs: s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> s#(s(0(x1))) 0#(p(x1)) -> s#(s(s(0(x1)))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) graph: 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> 0#(x1) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(0(x1)) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(0(x1))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(s(0(x1)))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(s(s(0(x1))))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(p(s(s(s(s(0(x1))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(x1) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(x1)))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(p(p(p(s(x1)))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) -> s#(twice(x1)) -> s#(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) SCC Processor: #sccs: 2 #rules: 12 #arcs: 336/784 DPs: 0#(p(x1)) -> 0#(x1) TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [0#](x0) = x0, [twice](x0) = x0 + -16, [p](x0) = 1x0 + 0, [s](x0) = -1x0 + 7, [twoto](x0) = 5, [0](x0) = 15 orientation: 0#(p(x1)) = 1x1 + 0 >= x1 = 0#(x1) s(twoto(x1)) = 7 >= 7 = s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) = -1x1 + 7 >= -2x1 + 7 = s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) = 1x1 + 7 >= 1x1 + 0 = p(x1) s(p(x1)) = x1 + 7 >= x1 = x1 0(p(x1)) = 15 >= 11 = s(p(s(s(s(s(0(x1))))))) problem: DPs: TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) Qed DPs: s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(x1) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(x1)))) TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [s#](x0) = 1x0 + 0, [twice](x0) = x0, [p](x0) = x0, [s](x0) = x0, [twoto](x0) = 1x0 + 1, [0](x0) = 2x0 + 12 orientation: s#(twice(x1)) = 1x1 + 0 >= 1x1 + 0 = s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) = 1x1 + 0 >= 1x1 + 0 = s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) = 1x1 + 0 >= 1x1 + 0 = s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) = 1x1 + 0 >= 1x1 + 0 = s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) = 1x1 + 0 >= 1x1 + 0 = s#(x1) s#(twoto(x1)) = 2x1 + 2 >= 1x1 + 0 = s#(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) = 2x1 + 2 >= 1x1 + 0 = s#(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))) s#(twoto(x1)) = 2x1 + 2 >= 1x1 + 0 = s#(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1))))))))))))))) s#(twoto(x1)) = 2x1 + 2 >= 1x1 + 0 = s#(s(s(p(p(p(s(s(p(p(x1)))))))))) s#(twoto(x1)) = 2x1 + 2 >= 1x1 + 0 = s#(s(p(p(p(s(s(p(p(x1))))))))) s#(twoto(x1)) = 2x1 + 2 >= 1x1 + 0 = s#(s(p(p(x1)))) s(twoto(x1)) = 1x1 + 1 >= 1x1 + 1 = s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) = x1 >= x1 = s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) = x1 >= x1 = p(x1) s(p(x1)) = x1 >= x1 = x1 0(p(x1)) = 2x1 + 12 >= 2x1 + 12 = s(p(s(s(s(s(0(x1))))))) problem: DPs: s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(x1) TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) EDG Processor: DPs: s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(x1) TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) graph: s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) -> s#(twice(x1)) -> s#(x1) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) -> s#(x1) -> s#(twice(x1)) -> s#(x1) Arctic Interpretation Processor: dimension: 1 interpretation: [s#](x0) = 4x0, [twice](x0) = 8x0, [p](x0) = x0, [s](x0) = x0, [twoto](x0) = 4, [0](x0) = 1x0 + -8 orientation: s#(twice(x1)) = 12x1 >= 4x1 = s#(s(s(s(s(p(p(p(p(s(x1)))))))))) s#(twice(x1)) = 12x1 >= 4x1 = s#(s(s(s(p(p(p(p(s(x1))))))))) s#(twice(x1)) = 12x1 >= 4x1 = s#(s(s(p(p(p(p(s(x1)))))))) s#(twice(x1)) = 12x1 >= 4x1 = s#(s(p(p(p(p(s(x1))))))) s#(twice(x1)) = 12x1 >= 4x1 = s#(x1) s(twoto(x1)) = 4 >= 4 = s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) = 8x1 >= 8x1 = s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) = x1 >= x1 = p(x1) s(p(x1)) = x1 >= x1 = x1 0(p(x1)) = 1x1 + -8 >= 1x1 + -8 = s(p(s(s(s(s(0(x1))))))) problem: DPs: TRS: s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(s(p(p(twice(s(s(s(p(p(p(s(s(p(p(x1)))))))))))))))))))))))))) s(twice(x1)) -> s(p(s(p(s(p(s(p(twice(s(s(s(s(s(p(p(p(p(s(x1))))))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(p(s(s(s(s(0(x1))))))) Qed