(STRATEGY
    INNERMOST)

(VAR
    x2 x3 x4 x6 x8 x5 x1 x12 x16 x10 x18 x14)
(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]()))