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