YES Problem: tower(0(x1)) -> s(0(p(s(p(s(x1)))))) tower(s(x1)) -> p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) twoto(0(x1)) -> s(0(x1)) twoto(s(x1)) -> p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) twice(0(x1)) -> 0(x1) twice(s(x1)) -> p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1))))))))) Proof: Arctic Interpretation Processor: dimension: 1 interpretation: [twice](x0) = x0, [twoto](x0) = x0, [p](x0) = x0, [s](x0) = x0, [tower](x0) = 4x0, [0](x0) = 1x0 orientation: tower(0(x1)) = 5x1 >= 1x1 = s(0(p(s(p(s(x1)))))) tower(s(x1)) = 4x1 >= 4x1 = p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) twoto(0(x1)) = 1x1 >= 1x1 = s(0(x1)) twoto(s(x1)) = x1 >= x1 = p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) twice(0(x1)) = 1x1 >= 1x1 = 0(x1) twice(s(x1)) = x1 >= x1 = p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 p(0(x1)) = 1x1 >= 1x1 = 0(s(s(s(s(s(s(s(s(x1))))))))) problem: tower(s(x1)) -> p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) twoto(0(x1)) -> s(0(x1)) twoto(s(x1)) -> p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) twice(0(x1)) -> 0(x1) twice(s(x1)) -> p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1))))))))) Matrix Interpretation Processor: dim=2 interpretation: [twice](x0) = x0, [1 2] [twoto](x0) = [0 2]x0, [p](x0) = x0, [s](x0) = x0, [2 0] [3] [tower](x0) = [0 0]x0 + [0], [2 2] [0] [0](x0) = [1 1]x0 + [2] orientation: [2 0] [3] [2 0] [3] tower(s(x1)) = [0 0]x1 + [0] >= [0 0]x1 + [0] = p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) [4 4] [4] [2 2] [0] twoto(0(x1)) = [2 2]x1 + [4] >= [1 1]x1 + [2] = s(0(x1)) [1 2] [1 2] twoto(s(x1)) = [0 2]x1 >= [0 2]x1 = p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) [2 2] [0] [2 2] [0] twice(0(x1)) = [1 1]x1 + [2] >= [1 1]x1 + [2] = 0(x1) twice(s(x1)) = x1 >= x1 = p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) p(p(s(x1))) = x1 >= x1 = p(x1) p(s(x1)) = x1 >= x1 = x1 [2 2] [0] [2 2] [0] p(0(x1)) = [1 1]x1 + [2] >= [1 1]x1 + [2] = 0(s(s(s(s(s(s(s(s(x1))))))))) problem: tower(s(x1)) -> p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) twoto(s(x1)) -> p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) twice(0(x1)) -> 0(x1) twice(s(x1)) -> p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) p(p(s(x1))) -> p(x1) p(s(x1)) -> x1 p(0(x1)) -> 0(s(s(s(s(s(s(s(s(x1))))))))) String Reversal Processor: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0(twice(x1)) -> 0(x1) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) Matrix Interpretation Processor: dim=2 interpretation: [1 0] [0] [twice](x0) = [0 2]x0 + [1], [1 0] [0] [twoto](x0) = [0 0]x0 + [3], [p](x0) = x0, [s](x0) = x0, [2 0] [2] [tower](x0) = [3 0]x0 + [0], [1 1] [3] [0](x0) = [0 1]x0 + [2] orientation: [2 0] [2] [2 0] [2] s(tower(x1)) = [3 0]x1 + [0] >= [3 0]x1 + [0] = s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) [1 0] [0] [1 0] [0] s(twoto(x1)) = [0 0]x1 + [3] >= [0 0]x1 + [3] = s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) [1 2] [4] [1 1] [3] 0(twice(x1)) = [0 2]x1 + [3] >= [0 1]x1 + [2] = 0(x1) [1 0] [0] [1 0] [0] s(twice(x1)) = [0 2]x1 + [1] >= [0 2]x1 + [1] = s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) = x1 >= x1 = p(x1) s(p(x1)) = x1 >= x1 = x1 [1 1] [3] [1 1] [3] 0(p(x1)) = [0 1]x1 + [2] >= [0 1]x1 + [2] = s(s(s(s(s(s(s(s(0(x1))))))))) problem: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) DP Processor: DPs: s#(tower(x1)) -> s#(p(x1)) s#(tower(x1)) -> s#(p(s(p(x1)))) s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(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#(s(s(s(s(0(x1)))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) TDG Processor: DPs: s#(tower(x1)) -> s#(p(x1)) s#(tower(x1)) -> s#(p(s(p(x1)))) s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(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#(s(s(s(s(0(x1)))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) graph: ... EDG Processor: DPs: s#(tower(x1)) -> s#(p(x1)) s#(tower(x1)) -> s#(p(s(p(x1)))) s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(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#(s(s(s(s(0(x1)))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(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#(s(s(s(s(0(x1)))))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) 0#(p(x1)) -> 0#(x1) -> 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(tower(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(s(0(x1))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(tower(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(s(0(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(tower(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(s(0(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(tower(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(s(0(x1)))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(tower(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(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#(p(p(p(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(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(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(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(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(s(0(x1))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(tower(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(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#(p(p(p(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(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(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(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(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(s(0(x1)))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(tower(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(s(0(x1))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(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#(p(p(p(s(p(p(x1))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(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(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(s(0(x1))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(tower(x1)) -> s#(p(x1)) 0#(p(x1)) -> s#(0(x1)) -> s#(tower(x1)) -> s#(p(s(p(x1)))) 0#(p(x1)) -> s#(0(x1)) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(x1))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(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(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(p(p(x1)))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) 0#(p(x1)) -> s#(0(x1)) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(x1)) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(x1)))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(twoto(s(p(s(p(x1))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(twoto(s(p(s(p(x1))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(tower(x1)) -> s#(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(x1))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(p(x1))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(p(p(s(p(p(x1)))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twoto(x1)) -> s#(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(x1)))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) SCC Processor: #sccs: 2 #rules: 12 #arcs: 560/1444 DPs: 0#(p(x1)) -> 0#(x1) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [0#](x0) = x0 + 1, [twice](x0) = 0, [twoto](x0) = x0 + -16, [p](x0) = 3x0 + 3, [s](x0) = -3x0 + 0, [tower](x0) = 0, [0](x0) = 5 orientation: 0#(p(x1)) = 3x1 + 3 >= x1 + 1 = 0#(x1) s(tower(x1)) = 0 >= 0 = s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) = -3x1 + 0 >= 0 = s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) = 0 >= 0 = s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) = 3x1 + 3 >= 3x1 + 3 = p(x1) s(p(x1)) = x1 + 0 >= x1 = x1 0(p(x1)) = 5 >= 0 = s(s(s(s(s(s(s(s(0(x1))))))))) problem: DPs: TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) Qed DPs: s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twoto(x1)) -> s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) -> s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) -> s#(s(p(p(p(s(p(p(x1)))))))) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) Arctic Interpretation Processor: dimension: 1 interpretation: [s#](x0) = x0, [twice](x0) = x0, [twoto](x0) = 12x0, [p](x0) = x0, [s](x0) = x0, [tower](x0) = 2, [0](x0) = -12x0 + 3 orientation: s#(twice(x1)) = x1 >= x1 = s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) = x1 >= x1 = s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) = x1 >= x1 = s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) = x1 >= x1 = s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) = x1 >= x1 = s#(s(s(p(p(p(x1)))))) s#(twice(x1)) = x1 >= x1 = s#(s(p(p(p(x1))))) s#(twoto(x1)) = 12x1 >= x1 = s#(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1))))))))))))))))))))))))))) s#(twoto(x1)) = 12x1 >= x1 = s#(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))) s#(twoto(x1)) = 12x1 >= x1 = s#(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))) s#(twoto(x1)) = 12x1 >= x1 = s#(s(p(s(s(p(p(p(s(p(p(x1))))))))))) s#(twoto(x1)) = 12x1 >= x1 = s#(s(p(p(p(s(p(p(x1)))))))) s(tower(x1)) = 2 >= 2 = s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) = 12x1 >= 12x1 = s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) = x1 >= x1 = s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) = x1 >= x1 = p(x1) s(p(x1)) = x1 >= x1 = x1 0(p(x1)) = -12x1 + 3 >= -12x1 + 3 = s(s(s(s(s(s(s(s(0(x1))))))))) problem: DPs: s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) EDG Processor: DPs: s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) graph: s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(p(p(p(x1))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(x1)))))) s#(twice(x1)) -> s#(s(s(s(s(p(p(p(x1)))))))) -> s#(twice(x1)) -> s#(s(p(p(p(x1))))) Arctic Interpretation Processor: dimension: 1 interpretation: [s#](x0) = 8x0, [twice](x0) = 8x0 + -8, [twoto](x0) = 14, [p](x0) = x0, [s](x0) = x0, [tower](x0) = 10, [0](x0) = 8x0 + -12 orientation: s#(twice(x1)) = 16x1 + 0 >= 16x1 + 0 = s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) = 16x1 + 0 >= 16x1 + 0 = s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) = 16x1 + 0 >= 8x1 = s#(s(s(s(s(p(p(p(x1)))))))) s#(twice(x1)) = 16x1 + 0 >= 8x1 = s#(s(s(s(p(p(p(x1))))))) s#(twice(x1)) = 16x1 + 0 >= 8x1 = s#(s(s(p(p(p(x1)))))) s#(twice(x1)) = 16x1 + 0 >= 8x1 = s#(s(p(p(p(x1))))) s(tower(x1)) = 10 >= 10 = s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) = 14 >= 14 = s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) = 8x1 + -8 >= 8x1 + -8 = s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) = x1 >= x1 = p(x1) s(p(x1)) = x1 >= x1 = x1 0(p(x1)) = 8x1 + -12 >= 8x1 + -12 = s(s(s(s(s(s(s(s(0(x1))))))))) problem: DPs: s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) EDG Processor: DPs: s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) graph: s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) -> s#(twice(x1)) -> s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) Matrix Interpretation Processor: dim=1 interpretation: [s#](x0) = 11/2x0 + 1/2, [twice](x0) = 1/2, [twoto](x0) = 4, [p](x0) = 1/2x0, [s](x0) = 2x0, [tower](x0) = 0, [0](x0) = 0 orientation: s#(twice(x1)) = 13/4 >= 15/8 = s#(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s#(twice(x1)) = 13/4 >= 19/16 = s#(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1)))))))))))))) s(tower(x1)) = 0 >= 0 = s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) = 8 >= 4 = s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s(p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) = 1 >= 1/2 = s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) = 1/2x1 >= 1/2x1 = p(x1) s(p(x1)) = x1 >= x1 = x1 0(p(x1)) = 0 >= 0 = s(s(s(s(s(s(s(s(0(x1))))))))) problem: DPs: TRS: s(tower(x1)) -> s(p(s(p(tower(s(p(s(p(twoto(s(p(s(p(x1)))))))))))))) s(twoto(x1)) -> s(p(s(p(twoto(s(s(s(p(p(p(s(p(s(p(twice(s(p(s(s(p(s(s ( p(s(s(p(p(p(s(p(p(x1)))))))))))))))))))))))))))))))) s(twice(x1)) -> s(s(s(p(p(p(twice(s(s(s(s(s(p(p(p(x1))))))))))))))) s(p(p(x1))) -> p(x1) s(p(x1)) -> x1 0(p(x1)) -> s(s(s(s(s(s(s(s(0(x1))))))))) Qed