(STRATEGY INNERMOST) (VAR x2 x1 x6 x5 x3 x4 x18 x14 x12 x16) (RULES rpm_t_m_2#1(f_p(x(f(x2))),x1) -> Leaf(snd#2(x#1(f(x2),bot[2]()),bot[3]())) rpm_t_m_9#1(P(rpm_t_m_9(x6,x5),rpm_t_m_10(x3,x4)),x2,x1) -> Node(rpm_t_m_9#1(x6,x5,bot[5]()),fst#2(x2)) rpm_t_m_9#1(P(rpm_t_m_2(f_p(x(f(x4)))),rpm_t_m_3(x3)),x2,x1) -> Node(rpm_t_m_2#1(f_p(x(f(x4))),bot[5]()),fst#2(x2)) rpm_t_m_8#1(x3,x2,x1) -> P(rpm_t_m_9(x3,x2),rpm_t_m_10(x3,x2)) rpm#3(Leaf(x3),f_p(x(f(x2))),x1) -> P(rpm_t_m_2(f_p(x(f(x2)))) ,rpm_t_m_3(x3)) rpm#3(Node(x4,x3),f_p(x(f(x2))),x1) -> rpm_t_m_8#1(rpm#3(x4 ,f_p(x(f(x2))) ,bot[9]()) ,rpm#3(x3 ,f_p(x(f(x2))) ,bot[10]()) ,x1) cond_fst_p#1(P(rpm_t_m_2(f_p(x(f(x2)))),rpm_t_m_3(x1))) -> rpm_t_m_2#1(f_p(x(f(x2))),bot[1]()) cond_fst_p#1(P(rpm_t_m_9(x4,x3),rpm_t_m_10(x1,x2))) -> rpm_t_m_9#1(x4 ,x3 ,bot[1]()) fst#2(P(rpm_t_m_9(x4,x3),rpm_t_m_10(x1,x2))) -> rpm_t_m_9#1(x4,x3,bot[6]()) fst#2(P(rpm_t_m_2(f_p(x(f(x2)))),rpm_t_m_3(x1))) -> rpm_t_m_2#1(f_p(x(f(x2))),bot[6]()) snd#2(P(x18,rpm_t_m_3(x14)),x18) -> x14 snd#2(P(x2,rpm_t_m_10(x6,x4)),x2) -> min#2(snd#2(x6,bot[7]()) ,snd#2(x4,bot[8]())) min#2(0(),x12) -> 0() min#2(S(x16),0()) -> 0() min#2(S(x4),S(x2)) -> S(min#2(x4,x2)) x#1(f(x4),x3) -> rpm#3(x4,f_p(x(f(x4))),bot[11]()) main(x1) -> cond_fst_p#1(x#1(f(x1),bot[0]())))