(STRATEGY
    INNERMOST)

(VAR
    x1 x10 x12 x14 x16 x18 x2 x3 x4
    x5 x6 x8)
(DATATYPES
    A = µX.< f_p(X, X), snd, x(X), Leaf(X), bot[2], bot[3], fst, P(X, X), rpm_t_m_9(X, X, X), Node(X, X), bot[5], bot[6], rpm_t_m_2(X), rpm_t_m_10(X, X), rpm_t_m_3(X), bot[9], bot[10], bot[7], bot[8], 0, S(X), f(X), bot[11], bot[0], bot[1] >)
(SIGNATURES
    rpm_t_m_2#1 :: [A x A] -> A
    rpm_t_m_9#1 :: [A x A x A x A] -> A
    rpm_t_m_8#1 :: [A x A x A] -> A
    rpm#3 :: [A x A x A] -> A
    cond_fst_p#1 :: [A x A] -> A
    fst#2 :: [A x A] -> A
    snd#2 :: [A x A] -> A
    min#2 :: [A x A] -> A
    x#1 :: [A x A] -> A
    main :: [A] -> A)
(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]()))