*************************************
Proof
    { system = (VAR l n
                    m x
                    y v
                    u)
               (STRATEGY INNERMOST)
               (RULES sort (l) -> st (0, l)
                      st (n, l) -> cond1 (member (n, l), n, l)
                      cond1 (true, n, l) -> cons (n, st (s (n), l))
                      cond1 (false, n, l) -> cond2 (gt (n, max (l)), n, l)
                      cond2 (true, n, l) -> nil
                      cond2 (false, n, l) -> st (s (n), l)
                      member (n, nil) -> false
                      member (n, cons (m, l)) -> or (equal (n, m), member (n, l))
                      or (x, true) -> true
                      or (x, false) -> x
                      equal (0, 0) -> true
                      equal (s (x), 0) -> false
                      equal (0, s (y)) -> false
                      equal (s (x), s (y)) -> equal (x, y)
                      gt (0, v) -> false
                      gt (s (u), 0) -> true
                      gt (s (u), s (v)) -> gt (u, v)
                      max (nil) -> 0
                      max (cons (u, l)) -> if (gt (u, max (l)), u, max (l))
                      if (true, u, v) -> u
                      if (false, u, v) -> v)
    , property = Termination , truth = Nothing , transform = Ignore_Strategy
    , to = [ Proof
                 { system = (VAR l n
                                 m x
                                 y v
                                 u)
                            (STRATEGY INNERMOST)
                            (RULES sort (l) -> st (0, l)
                                   st (n, l) -> cond1 (member (n, l), n, l)
                                   cond1 (true, n, l) -> cons (n, st (s (n), l))
                                   cond1 (false, n, l) -> cond2 (gt (n, max (l)), n, l)
                                   cond2 (true, n, l) -> nil
                                   cond2 (false, n, l) -> st (s (n), l)
                                   member (n, nil) -> false
                                   member (n, cons (m, l)) -> or (equal (n, m), member (n, l))
                                   or (x, true) -> true
                                   or (x, false) -> x
                                   equal (0, 0) -> true
                                   equal (s (x), 0) -> false
                                   equal (0, s (y)) -> false
                                   equal (s (x), s (y)) -> equal (x, y)
                                   gt (0, v) -> false
                                   gt (s (u), 0) -> true
                                   gt (s (u), s (v)) -> gt (u, v)
                                   max (nil) -> 0
                                   max (cons (u, l)) -> if (gt (u, max (l)), u, max (l))
                                   if (true, u, v) -> u
                                   if (false, u, v) -> v)
                 , property = Termination , truth = Nothing , transform = Dependency_Pair_Transformation
                 , to = [ Proof
                              { system = (VAR l n
                                              m x
                                              y v
                                              u)
                                         (STRATEGY INNERMOST)
                                         (RULES sortP (l) -> stP (0, l)
                                                stP (n, l) -> cond1P (member (n, l), n, l)
                                                stP (n, l) -> memberP (n, l)
                                                cond1P (true, n, l) -> stP (s (n), l)
                                                cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l)
                                                cond1P (false, n, l) -> gtP (n, max (l))
                                                cond1P (false, n, l) -> maxP (l)
                                                cond2P (false, n, l) -> stP (s (n), l)
                                                memberP (n, cons (m, l)) -> orP (equal (n, m), member (n, l))
                                                memberP (n, cons (m, l)) -> equalP (n, m)
                                                memberP (n, cons (m, l)) -> memberP (n, l)
                                                equalP (s (x), s (y)) -> equalP (x, y)
                                                gtP (s (u), s (v)) -> gtP (u, v)
                                                maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l))
                                                maxP (cons (u, l)) -> gtP (u, max (l))
                                                maxP (cons (u, l)) -> maxP (l)
                                                maxP (cons (u, l)) -> maxP (l)
                                                sort (l) ->= st (0, l)
                                                st (n, l) ->= cond1 (member (n, l), n, l)
                                                cond1 (true, n, l) ->= cons (n, st (s (n), l))
                                                cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l)
                                                cond2 (true, n, l) ->= nil
                                                cond2 (false, n, l) ->= st (s (n), l)
                                                member (n, nil) ->= false
                                                member (n, cons (m, l)) ->= or (equal (n, m), member (n, l))
                                                or (x, true) ->= true
                                                or (x, false) ->= x
                                                equal (0, 0) ->= true
                                                equal (s (x), 0) ->= false
                                                equal (0, s (y)) ->= false
                                                equal (s (x), s (y)) ->= equal (x, y)
                                                gt (0, v) ->= false
                                                gt (s (u), 0) ->= true
                                                gt (s (u), s (v)) ->= gt (u, v)
                                                max (nil) ->= 0
                                                max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l))
                                                if (true, u, v) ->= u
                                                if (false, u, v) ->= v)
                              , property = Top_Termination , truth = Nothing
                              , transform = Remove
                                                { interpretation = Interpretation
                                                                       ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                                       orP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                       gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                       stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                       equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                       sort |-> (x) |-> E^0x0 * x + E^0x1
                                                                       0 |-> () |-> E^0x1
                                                                       s |-> (x) |-> E^0x0 * x + E^0x1
                                                                       false |-> () |-> E^0x1
                                                                       cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                       if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                       or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       sortP |-> (x) |-> E^1x0 * x + (2)
                                                                       cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                                       true |-> () |-> E^0x1
                                                                       memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                       equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       nil |-> () |-> E^0x1
                                                                       cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       maxP |-> (x) |-> E^1x0 * x + (2)
                                                                       member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                       cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                                       cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                       max |-> (x) |-> E^0x0 * x + E^0x1
                                                , removes_rules = [ memberP (n, cons (m, l)) -> orP (equal (n, m), member (n, l)) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                                                }
                              , to = [ Proof
                                           { system = (VAR l n
                                                           m x
                                                           y v
                                                           u)
                                                      (STRATEGY INNERMOST)
                                                      (RULES sortP (l) -> stP (0, l)
                                                             stP (n, l) -> cond1P (member (n, l), n, l)
                                                             stP (n, l) -> memberP (n, l)
                                                             cond1P (true, n, l) -> stP (s (n), l)
                                                             cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l)
                                                             cond1P (false, n, l) -> gtP (n, max (l))
                                                             cond1P (false, n, l) -> maxP (l)
                                                             cond2P (false, n, l) -> stP (s (n), l)
                                                             memberP (n, cons (m, l)) -> equalP (n, m)
                                                             memberP (n, cons (m, l)) -> memberP (n, l)
                                                             equalP (s (x), s (y)) -> equalP (x, y)
                                                             gtP (s (u), s (v)) -> gtP (u, v)
                                                             maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l))
                                                             maxP (cons (u, l)) -> gtP (u, max (l))
                                                             maxP (cons (u, l)) -> maxP (l)
                                                             maxP (cons (u, l)) -> maxP (l)
                                                             sort (l) ->= st (0, l)
                                                             st (n, l) ->= cond1 (member (n, l), n, l)
                                                             cond1 (true, n, l) ->= cons (n, st (s (n), l))
                                                             cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l)
                                                             cond2 (true, n, l) ->= nil
                                                             cond2 (false, n, l) ->= st (s (n), l)
                                                             member (n, nil) ->= false
                                                             member (n, cons (m, l)) ->= or (equal (n, m), member (n, l))
                                                             or (x, true) ->= true
                                                             or (x, false) ->= x
                                                             equal (0, 0) ->= true
                                                             equal (s (x), 0) ->= false
                                                             equal (0, s (y)) ->= false
                                                             equal (s (x), s (y)) ->= equal (x, y)
                                                             gt (0, v) ->= false
                                                             gt (s (u), 0) ->= true
                                                             gt (s (u), s (v)) ->= gt (u, v)
                                                             max (nil) ->= 0
                                                             max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l))
                                                             if (true, u, v) ->= u
                                                             if (false, u, v) ->= v)
                                           , property = Top_Termination , truth = Nothing
                                           , transform = Remove
                                                             { interpretation = Interpretation
                                                                                    ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                                                                    gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                                    stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                                    equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                                    sort |-> (x) |-> E^0x0 * x + E^0x1
                                                                                    0 |-> () |-> E^0x1
                                                                                    s |-> (x) |-> E^0x0 * x + E^0x1
                                                                                    false |-> () |-> E^0x1
                                                                                    cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                    if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                    or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    sortP |-> (x) |-> E^1x0 * x + (2)
                                                                                    cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                                                                    true |-> () |-> E^0x1
                                                                                    memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                                    equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    nil |-> () |-> E^0x1
                                                                                    cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    maxP |-> (x) |-> E^1x0 * x + (0)
                                                                                    member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                    cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                                                                    cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                    max |-> (x) |-> E^0x0 * x + E^0x1
                                                             , removes_rules = [ sortP (l) -> stP (0, l) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                                                             }
                                           , to = [ Proof
                                                        { system = (VAR l n
                                                                        m x
                                                                        y v
                                                                        u)
                                                                   (STRATEGY INNERMOST)
                                                                   (RULES stP (n, l) -> cond1P (member (n, l), n, l)
                                                                          stP (n, l) -> memberP (n, l)
                                                                          cond1P (true, n, l) -> stP (s (n), l)
                                                                          cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l)
                                                                          cond1P (false, n, l) -> gtP (n, max (l))
                                                                          cond1P (false, n, l) -> maxP (l)
                                                                          cond2P (false, n, l) -> stP (s (n), l)
                                                                          memberP (n, cons (m, l)) -> equalP (n, m)
                                                                          memberP (n, cons (m, l)) -> memberP (n, l)
                                                                          equalP (s (x), s (y)) -> equalP (x, y)
                                                                          gtP (s (u), s (v)) -> gtP (u, v)
                                                                          maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l))
                                                                          maxP (cons (u, l)) -> gtP (u, max (l))
                                                                          maxP (cons (u, l)) -> maxP (l)
                                                                          maxP (cons (u, l)) -> maxP (l)
                                                                          sort (l) ->= st (0, l)
                                                                          st (n, l) ->= cond1 (member (n, l), n, l)
                                                                          cond1 (true, n, l) ->= cons (n, st (s (n), l))
                                                                          cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l)
                                                                          cond2 (true, n, l) ->= nil
                                                                          cond2 (false, n, l) ->= st (s (n), l)
                                                                          member (n, nil) ->= false
                                                                          member (n, cons (m, l)) ->= or (equal (n, m), member (n, l))
                                                                          or (x, true) ->= true
                                                                          or (x, false) ->= x
                                                                          equal (0, 0) ->= true
                                                                          equal (s (x), 0) ->= false
                                                                          equal (0, s (y)) ->= false
                                                                          equal (s (x), s (y)) ->= equal (x, y)
                                                                          gt (0, v) ->= false
                                                                          gt (s (u), 0) ->= true
                                                                          gt (s (u), s (v)) ->= gt (u, v)
                                                                          max (nil) ->= 0
                                                                          max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l))
                                                                          if (true, u, v) ->= u
                                                                          if (false, u, v) ->= v)
                                                        , property = Top_Termination , truth = Nothing
                                                        , transform = Remove
                                                                          { interpretation = Interpretation
                                                                                                 ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                                                                                 gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                                                 stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                                                 equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                                                 sort |-> (x) |-> E^0x0 * x + E^0x1
                                                                                                 0 |-> () |-> E^0x1
                                                                                                 s |-> (x) |-> E^0x0 * x + E^0x1
                                                                                                 false |-> () |-> E^0x1
                                                                                                 cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                                 if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                                 or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                 gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                 st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                 cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                                                                 true |-> () |-> E^0x1
                                                                                                 memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                                                 equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                 nil |-> () |-> E^0x1
                                                                                                 cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                 maxP |-> (x) |-> E^1x0 * x + (2)
                                                                                                 member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                 cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                                                                 cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                                 max |-> (x) |-> E^0x0 * x + E^0x1
                                                                          , removes_rules = [ memberP (n, cons (m, l)) -> equalP (n, m) , maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l)) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                                                                          }
                                                        , to = [ Proof
                                                                     { system = (VAR l n
                                                                                     m x
                                                                                     y v
                                                                                     u)
                                                                                (STRATEGY INNERMOST)
                                                                                (RULES stP (n, l) -> cond1P (member (n, l), n, l)
                                                                                       stP (n, l) -> memberP (n, l)
                                                                                       cond1P (true, n, l) -> stP (s (n), l)
                                                                                       cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l)
                                                                                       cond1P (false, n, l) -> gtP (n, max (l))
                                                                                       cond1P (false, n, l) -> maxP (l)
                                                                                       cond2P (false, n, l) -> stP (s (n), l)
                                                                                       memberP (n, cons (m, l)) -> memberP (n, l)
                                                                                       equalP (s (x), s (y)) -> equalP (x, y)
                                                                                       gtP (s (u), s (v)) -> gtP (u, v)
                                                                                       maxP (cons (u, l)) -> gtP (u, max (l))
                                                                                       maxP (cons (u, l)) -> maxP (l)
                                                                                       maxP (cons (u, l)) -> maxP (l)
                                                                                       sort (l) ->= st (0, l)
                                                                                       st (n, l) ->= cond1 (member (n, l), n, l)
                                                                                       cond1 (true, n, l) ->= cons (n, st (s (n), l))
                                                                                       cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l)
                                                                                       cond2 (true, n, l) ->= nil
                                                                                       cond2 (false, n, l) ->= st (s (n), l)
                                                                                       member (n, nil) ->= false
                                                                                       member (n, cons (m, l)) ->= or (equal (n, m), member (n, l))
                                                                                       or (x, true) ->= true
                                                                                       or (x, false) ->= x
                                                                                       equal (0, 0) ->= true
                                                                                       equal (s (x), 0) ->= false
                                                                                       equal (0, s (y)) ->= false
                                                                                       equal (s (x), s (y)) ->= equal (x, y)
                                                                                       gt (0, v) ->= false
                                                                                       gt (s (u), 0) ->= true
                                                                                       gt (s (u), s (v)) ->= gt (u, v)
                                                                                       max (nil) ->= 0
                                                                                       max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l))
                                                                                       if (true, u, v) ->= u
                                                                                       if (false, u, v) ->= v)
                                                                     , property = Top_Termination , truth = Nothing
                                                                     , transform = Split
                                                                                       { interpretation = Interpretation
                                                                                                              ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                                                                                              gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                                                              stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                                                              equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                                                                              sort |-> (x) |-> E^0x0 * x + E^0x1
                                                                                                              0 |-> () |-> E^0x1
                                                                                                              s |-> (x) |-> E^0x0 * x + E^0x1
                                                                                                              false |-> () |-> E^0x1
                                                                                                              cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                                              if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                                              or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                              gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                              st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                              cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                                                                              true |-> () |-> E^0x1
                                                                                                              memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                                                                              equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                              nil |-> () |-> E^0x1
                                                                                                              cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                              maxP |-> (x) |-> E^1x0 * x + (2)
                                                                                                              member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                                                                              cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                                                                              cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                                                                              max |-> (x) |-> E^0x0 * x + E^0x1
                                                                                       , clusters = [ [ equalP (s (x), s (y)) -> equalP (x, y) ] , [ stP (n, l) -> cond1P (member (n, l), n, l) , stP (n, l) -> memberP (n, l) , cond1P (true, n, l) -> stP (s (n), l) , cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) , cond1P (false, n, l) -> gtP (n, max (l)) , cond1P (false, n, l) -> maxP (l) , cond2P (false, n, l) -> stP (s (n), l) , memberP (n, cons (m, l)) -> memberP (n, l) , gtP (s (u), s (v)) -> gtP (u, v) , maxP (cons (u, l)) -> gtP (u, max (l)) , maxP (cons (u, l)) -> maxP (l) , maxP (cons (u, l)) -> maxP (l) ] ]
                                                                                       , comment = size 0 , heights ( 3 , 7 ) , time 
                                                                                                   split_dimension:  0
                                                                                       }
                                                                     , to = [ Claim
                                                                                  { system = (VAR l n
                                                                                                  m x
                                                                                                  y v
                                                                                                  u)
                                                                                             (STRATEGY INNERMOST)
                                                                                             (RULES equalP (s (x), s (y)) -> equalP (x, y)
                                                                                                    sort (l) ->= st (0, l)
                                                                                                    st (n, l) ->= cond1 (member (n, l), n, l)
                                                                                                    cond1 (true, n, l) ->= cons (n, st (s (n), l))
                                                                                                    cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l)
                                                                                                    cond2 (true, n, l) ->= nil
                                                                                                    cond2 (false, n, l) ->= st (s (n), l)
                                                                                                    member (n, nil) ->= false
                                                                                                    member (n, cons (m, l)) ->= or (equal (n, m), member (n, l))
                                                                                                    or (x, true) ->= true
                                                                                                    or (x, false) ->= x
                                                                                                    equal (0, 0) ->= true
                                                                                                    equal (s (x), 0) ->= false
                                                                                                    equal (0, s (y)) ->= false
                                                                                                    equal (s (x), s (y)) ->= equal (x, y)
                                                                                                    gt (0, v) ->= false
                                                                                                    gt (s (u), 0) ->= true
                                                                                                    gt (s (u), s (v)) ->= gt (u, v)
                                                                                                    max (nil) ->= 0
                                                                                                    max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l))
                                                                                                    if (true, u, v) ->= u
                                                                                                    if (false, u, v) ->= v)
                                                                                  , property = Top_Termination
                                                                                  }
                                                                            , Claim
                                                                                  { system = (VAR l n
                                                                                                  m x
                                                                                                  y v
                                                                                                  u)
                                                                                             (STRATEGY INNERMOST)
                                                                                             (RULES stP (n, l) -> cond1P (member (n, l), n, l)
                                                                                                    stP (n, l) -> memberP (n, l)
                                                                                                    cond1P (true, n, l) -> stP (s (n), l)
                                                                                                    cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l)
                                                                                                    cond1P (false, n, l) -> gtP (n, max (l))
                                                                                                    cond1P (false, n, l) -> maxP (l)
                                                                                                    cond2P (false, n, l) -> stP (s (n), l)
                                                                                                    memberP (n, cons (m, l)) -> memberP (n, l)
                                                                                                    gtP (s (u), s (v)) -> gtP (u, v)
                                                                                                    maxP (cons (u, l)) -> gtP (u, max (l))
                                                                                                    maxP (cons (u, l)) -> maxP (l)
                                                                                                    maxP (cons (u, l)) -> maxP (l)
                                                                                                    sort (l) ->= st (0, l)
                                                                                                    st (n, l) ->= cond1 (member (n, l), n, l)
                                                                                                    cond1 (true, n, l) ->= cons (n, st (s (n), l))
                                                                                                    cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l)
                                                                                                    cond2 (true, n, l) ->= nil
                                                                                                    cond2 (false, n, l) ->= st (s (n), l)
                                                                                                    member (n, nil) ->= false
                                                                                                    member (n, cons (m, l)) ->= or (equal (n, m), member (n, l))
                                                                                                    or (x, true) ->= true
                                                                                                    or (x, false) ->= x
                                                                                                    equal (0, 0) ->= true
                                                                                                    equal (s (x), 0) ->= false
                                                                                                    equal (0, s (y)) ->= false
                                                                                                    equal (s (x), s (y)) ->= equal (x, y)
                                                                                                    gt (0, v) ->= false
                                                                                                    gt (s (u), 0) ->= true
                                                                                                    gt (s (u), s (v)) ->= gt (u, v)
                                                                                                    max (nil) ->= 0
                                                                                                    max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l))
                                                                                                    if (true, u, v) ->= u
                                                                                                    if (false, u, v) ->= v)
                                                                                  , property = Top_Termination
                                                                                  }
                                                                            ]
                                                                     }
                                                               ]
                                                        }
                                                  ]
                                           }
                                     ]
                              }
                        ]
                 }
           ]
    }


Proof summary:

value Nothing
for property Termination
for system with 21 strict rules and 0 non-strict rules
follows by transformation
    Ignore_Strategy
from
    value Nothing
    for property Termination
    for system with 21 strict rules and 0 non-strict rules
    follows by transformation
        Dependency_Pair_Transformation
    from
        value Nothing
        for property Top_Termination
        for system with 17 strict rules and 21 non-strict rules
        follows by transformation
            Remove
                { interpretation = Interpretation
                                       ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                       orP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                       gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                       stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                       equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                       sort |-> (x) |-> E^0x0 * x + E^0x1
                                       0 |-> () |-> E^0x1
                                       s |-> (x) |-> E^0x0 * x + E^0x1
                                       false |-> () |-> E^0x1
                                       cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                       if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                       or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       sortP |-> (x) |-> E^1x0 * x + (2)
                                       cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                       true |-> () |-> E^0x1
                                       memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                       equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       nil |-> () |-> E^0x1
                                       cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       maxP |-> (x) |-> E^1x0 * x + (2)
                                       member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                       cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                       cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                       max |-> (x) |-> E^0x0 * x + E^0x1
                , removes_rules = [ memberP (n, cons (m, l)) -> orP (equal (n, m), member (n, l)) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                }
        from
            value Nothing
            for property Top_Termination
            for system with 16 strict rules and 21 non-strict rules
            follows by transformation
                Remove
                    { interpretation = Interpretation
                                           ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                           gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                           stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                           equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                           sort |-> (x) |-> E^0x0 * x + E^0x1
                                           0 |-> () |-> E^0x1
                                           s |-> (x) |-> E^0x0 * x + E^0x1
                                           false |-> () |-> E^0x1
                                           cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                           if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                           or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           sortP |-> (x) |-> E^1x0 * x + (2)
                                           cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                           true |-> () |-> E^0x1
                                           memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                           equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           nil |-> () |-> E^0x1
                                           cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           maxP |-> (x) |-> E^1x0 * x + (0)
                                           member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                           cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                           cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                           max |-> (x) |-> E^0x0 * x + E^0x1
                    , removes_rules = [ sortP (l) -> stP (0, l) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                    }
            from
                value Nothing
                for property Top_Termination
                for system with 15 strict rules and 21 non-strict rules
                follows by transformation
                    Remove
                        { interpretation = Interpretation
                                               ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                               gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                               stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                               equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                               sort |-> (x) |-> E^0x0 * x + E^0x1
                                               0 |-> () |-> E^0x1
                                               s |-> (x) |-> E^0x0 * x + E^0x1
                                               false |-> () |-> E^0x1
                                               cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                               if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                               or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                               gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                               st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                               cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                               true |-> () |-> E^0x1
                                               memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                               equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                               nil |-> () |-> E^0x1
                                               cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                               maxP |-> (x) |-> E^1x0 * x + (2)
                                               member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                               cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                               cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                               max |-> (x) |-> E^0x0 * x + E^0x1
                        , removes_rules = [ memberP (n, cons (m, l)) -> equalP (n, m) , maxP (cons (u, l)) -> ifP (gt (u, max (l)), u, max (l)) ] , comment = size 0 , heights ( 3 , 7 ) , time 
                        }
                from
                    value Nothing
                    for property Top_Termination
                    for system with 13 strict rules and 21 non-strict rules
                    follows by transformation
                        Split
                            { interpretation = Interpretation
                                                   ifP |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (0)
                                                   gtP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                   stP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                   equalP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (0)
                                                   sort |-> (x) |-> E^0x0 * x + E^0x1
                                                   0 |-> () |-> E^0x1
                                                   s |-> (x) |-> E^0x0 * x + E^0x1
                                                   false |-> () |-> E^0x1
                                                   cond1 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                   if |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                   or |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                   gt |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                   st |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                   cond2P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                   true |-> () |-> E^0x1
                                                   memberP |-> (x , y) |-> E^1x0 * x + E^1x0 * y + (2)
                                                   equal |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                   nil |-> () |-> E^0x1
                                                   cons |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                   maxP |-> (x) |-> E^1x0 * x + (2)
                                                   member |-> (x , y) |-> E^0x0 * x + E^0x0 * y + E^0x1
                                                   cond1P |-> (x , y , z) |-> E^1x0 * x + E^1x0 * y + E^1x0 * z + (2)
                                                   cond2 |-> (x , y , z) |-> E^0x0 * x + E^0x0 * y + E^0x0 * z + E^0x1
                                                   max |-> (x) |-> E^0x0 * x + E^0x1
                            , clusters = [ [ equalP (s (x), s (y)) -> equalP (x, y) ] , [ stP (n, l) -> cond1P (member (n, l), n, l) , stP (n, l) -> memberP (n, l) , cond1P (true, n, l) -> stP (s (n), l) , cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l) , cond1P (false, n, l) -> gtP (n, max (l)) , cond1P (false, n, l) -> maxP (l) , cond2P (false, n, l) -> stP (s (n), l) , memberP (n, cons (m, l)) -> memberP (n, l) , gtP (s (u), s (v)) -> gtP (u, v) , maxP (cons (u, l)) -> gtP (u, max (l)) , maxP (cons (u, l)) -> maxP (l) , maxP (cons (u, l)) -> maxP (l) ] ]
                            , comment = size 0 , heights ( 3 , 7 ) , time 
                                        split_dimension:  0
                            }
                    from
                        Claim
                            { system = (VAR l n
                                            m x
                                            y v
                                            u)
                                       (STRATEGY INNERMOST)
                                       (RULES equalP (s (x), s (y)) -> equalP (x, y)
                                              sort (l) ->= st (0, l)
                                              st (n, l) ->= cond1 (member (n, l), n, l)
                                              cond1 (true, n, l) ->= cons (n, st (s (n), l))
                                              cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l)
                                              cond2 (true, n, l) ->= nil
                                              cond2 (false, n, l) ->= st (s (n), l)
                                              member (n, nil) ->= false
                                              member (n, cons (m, l)) ->= or (equal (n, m), member (n, l))
                                              or (x, true) ->= true
                                              or (x, false) ->= x
                                              equal (0, 0) ->= true
                                              equal (s (x), 0) ->= false
                                              equal (0, s (y)) ->= false
                                              equal (s (x), s (y)) ->= equal (x, y)
                                              gt (0, v) ->= false
                                              gt (s (u), 0) ->= true
                                              gt (s (u), s (v)) ->= gt (u, v)
                                              max (nil) ->= 0
                                              max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l))
                                              if (true, u, v) ->= u
                                              if (false, u, v) ->= v)
                            , property = Top_Termination
                            }
                        Claim
                            { system = (VAR l n
                                            m x
                                            y v
                                            u)
                                       (STRATEGY INNERMOST)
                                       (RULES stP (n, l) -> cond1P (member (n, l), n, l)
                                              stP (n, l) -> memberP (n, l)
                                              cond1P (true, n, l) -> stP (s (n), l)
                                              cond1P (false, n, l) -> cond2P (gt (n, max (l)), n, l)
                                              cond1P (false, n, l) -> gtP (n, max (l))
                                              cond1P (false, n, l) -> maxP (l)
                                              cond2P (false, n, l) -> stP (s (n), l)
                                              memberP (n, cons (m, l)) -> memberP (n, l)
                                              gtP (s (u), s (v)) -> gtP (u, v)
                                              maxP (cons (u, l)) -> gtP (u, max (l))
                                              maxP (cons (u, l)) -> maxP (l)
                                              maxP (cons (u, l)) -> maxP (l)
                                              sort (l) ->= st (0, l)
                                              st (n, l) ->= cond1 (member (n, l), n, l)
                                              cond1 (true, n, l) ->= cons (n, st (s (n), l))
                                              cond1 (false, n, l) ->= cond2 (gt (n, max (l)), n, l)
                                              cond2 (true, n, l) ->= nil
                                              cond2 (false, n, l) ->= st (s (n), l)
                                              member (n, nil) ->= false
                                              member (n, cons (m, l)) ->= or (equal (n, m), member (n, l))
                                              or (x, true) ->= true
                                              or (x, false) ->= x
                                              equal (0, 0) ->= true
                                              equal (s (x), 0) ->= false
                                              equal (0, s (y)) ->= false
                                              equal (s (x), s (y)) ->= equal (x, y)
                                              gt (0, v) ->= false
                                              gt (s (u), 0) ->= true
                                              gt (s (u), s (v)) ->= gt (u, v)
                                              max (nil) ->= 0
                                              max (cons (u, l)) ->= if (gt (u, max (l)), u, max (l))
                                              if (true, u, v) ->= u
                                              if (false, u, v) ->= v)
                            , property = Top_Termination
                            }
------------------------------------------------------------------
matchbox general information (including details on proof methods):
http://dfa.imn.htwk-leipzig.de/matchbox/

this matchbox implementation uses the SAT solver
SatELite/MiniSat by Niklas Een and Niklas Sörensson
http://www.cs.chalmers.se/Cs/Research/FormalMethods/MiniSat/

matchbox process information
arguments      : --solver=/home/nowonder/forschung/increasing/wst06/matchbox/SatELiteGTI --timeout-command=/home/nowonder/forschung/increasing/wst06/matchbox/timeout --tmpdir=/home/nowonder/forschung/increasing/wst06/matchbox --timeout=60 /tmp/tmpOwPakZ/ex15.trs
started        : Thu Feb 22 16:50:44 CET 2007
finished       : Thu Feb 22 16:51:36 CET 2007
run system     : Linux aprove 2.6.14-gentoo-r5 #1 SMP Sun Dec 25 15:42:02 CET 2005 x86_64
release date   : Thu Jun 8 23:18:07 CEST 2006
build date     : Thu Jun 8 23:18:07 CEST 2006
build system   : Linux dfa 2.6.8-2-k7 #1 Tue Aug 16 14:00:15 UTC 2005 i686 GNU/Linux

used clock time: 52 secs