We consider the following Problem:

  Strict Trs:
    {  #less(@x, @y) -> #cklt(#compare(@x, @y))
     , findMin(@l) -> findMin#1(@l)
     , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
     , findMin#1(nil()) -> nil()
     , findMin#2(::(@y, @ys), @x) ->
       findMin#3(#less(@x, @y), @x, @y, @ys)
     , findMin#2(nil(), @x) -> ::(@x, nil())
     , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
     , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
     , minSort(@l) -> minSort#1(findMin(@l))
     , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
     , minSort#1(nil()) -> nil()}
  Weak Trs:
    {  #cklt(#EQ()) -> #false()
     , #cklt(#GT()) -> #false()
     , #cklt(#LT()) -> #true()
     , #compare(#0(), #0()) -> #EQ()
     , #compare(#0(), #neg(@y)) -> #GT()
     , #compare(#0(), #pos(@y)) -> #LT()
     , #compare(#0(), #s(@y)) -> #LT()
     , #compare(#neg(@x), #0()) -> #LT()
     , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
     , #compare(#neg(@x), #pos(@y)) -> #LT()
     , #compare(#pos(@x), #0()) -> #GT()
     , #compare(#pos(@x), #neg(@y)) -> #GT()
     , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
     , #compare(#s(@x), #0()) -> #GT()
     , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)}
  StartTerms: basic terms
  Strategy: innermost

Certificate: YES(?,O(n^2))

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {  #less(@x, @y) -> #cklt(#compare(@x, @y))
       , findMin(@l) -> findMin#1(@l)
       , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
       , findMin#1(nil()) -> nil()
       , findMin#2(::(@y, @ys), @x) ->
         findMin#3(#less(@x, @y), @x, @y, @ys)
       , findMin#2(nil(), @x) -> ::(@x, nil())
       , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
       , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
       , minSort(@l) -> minSort#1(findMin(@l))
       , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
       , minSort#1(nil()) -> nil()}
    Weak Trs:
      {  #cklt(#EQ()) -> #false()
       , #cklt(#GT()) -> #false()
       , #cklt(#LT()) -> #true()
       , #compare(#0(), #0()) -> #EQ()
       , #compare(#0(), #neg(@y)) -> #GT()
       , #compare(#0(), #pos(@y)) -> #LT()
       , #compare(#0(), #s(@y)) -> #LT()
       , #compare(#neg(@x), #0()) -> #LT()
       , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
       , #compare(#neg(@x), #pos(@y)) -> #LT()
       , #compare(#pos(@x), #0()) -> #GT()
       , #compare(#pos(@x), #neg(@y)) -> #GT()
       , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
       , #compare(#s(@x), #0()) -> #GT()
       , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^2))
  
  Proof:
    The weightgap principle applies, where following rules are oriented strictly:
    
    TRS Component:
      {  findMin#1(nil()) -> nil()
       , findMin#2(nil(), @x) -> ::(@x, nil())
       , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
       , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
       , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
       , minSort#1(nil()) -> nil()}
    
    Interpretation of nonconstant growth:
    -------------------------------------
      The following argument positions are usable:
        Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
        Uargs(findMin#1) = {}, Uargs(#cklt) = {1}, Uargs(#pos) = {},
        Uargs(findMin) = {}, Uargs(#neg) = {}, Uargs(#less) = {},
        Uargs(minSort) = {}, Uargs(#compare) = {}, Uargs(#s) = {},
        Uargs(findMin#2) = {1}
      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
      Interpretation Functions:
       minSort#1(x1) = [1 0] x1 + [1]
                       [0 0]      [1]
       #true() = [0]
                 [0]
       #false() = [0]
                  [0]
       findMin#3(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [1]
                                   [1 1]      [1 1]      [1 1]      [0 0]      [1]
       ::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                    [0 0]      [0 0]      [1]
       #LT() = [0]
               [0]
       findMin#1(x1) = [0 0] x1 + [1]
                       [0 0]      [1]
       #cklt(x1) = [1 0] x1 + [1]
                   [0 0]      [1]
       #pos(x1) = [0 0] x1 + [0]
                  [0 0]      [0]
       #0() = [0]
              [0]
       findMin(x1) = [0 0] x1 + [0]
                     [0 0]      [0]
       #neg(x1) = [0 0] x1 + [0]
                  [0 0]      [0]
       #EQ() = [0]
               [0]
       #less(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                       [0 0]      [0 0]      [0]
       minSort(x1) = [0 0] x1 + [0]
                     [0 0]      [0]
       #compare(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                          [0 0]      [0 0]      [1]
       #s(x1) = [0 0] x1 + [0]
                [0 0]      [0]
       #GT() = [0]
               [0]
       nil() = [0]
               [0]
       findMin#2(x1, x2) = [1 0] x1 + [0 0] x2 + [1]
                           [0 0]      [0 0]      [1]
    
    The strictly oriented rules are moved into the weak component.
    
    We consider the following Problem:
    
      Strict Trs:
        {  #less(@x, @y) -> #cklt(#compare(@x, @y))
         , findMin(@l) -> findMin#1(@l)
         , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
         , findMin#2(::(@y, @ys), @x) ->
           findMin#3(#less(@x, @y), @x, @y, @ys)
         , minSort(@l) -> minSort#1(findMin(@l))}
      Weak Trs:
        {  findMin#1(nil()) -> nil()
         , findMin#2(nil(), @x) -> ::(@x, nil())
         , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
         , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
         , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
         , minSort#1(nil()) -> nil()
         , #cklt(#EQ()) -> #false()
         , #cklt(#GT()) -> #false()
         , #cklt(#LT()) -> #true()
         , #compare(#0(), #0()) -> #EQ()
         , #compare(#0(), #neg(@y)) -> #GT()
         , #compare(#0(), #pos(@y)) -> #LT()
         , #compare(#0(), #s(@y)) -> #LT()
         , #compare(#neg(@x), #0()) -> #LT()
         , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
         , #compare(#neg(@x), #pos(@y)) -> #LT()
         , #compare(#pos(@x), #0()) -> #GT()
         , #compare(#pos(@x), #neg(@y)) -> #GT()
         , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
         , #compare(#s(@x), #0()) -> #GT()
         , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^2))
    
    Proof:
      The weightgap principle applies, where following rules are oriented strictly:
      
      TRS Component: {minSort(@l) -> minSort#1(findMin(@l))}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
          Uargs(findMin#1) = {}, Uargs(#cklt) = {1}, Uargs(#pos) = {},
          Uargs(findMin) = {}, Uargs(#neg) = {}, Uargs(#less) = {},
          Uargs(minSort) = {}, Uargs(#compare) = {}, Uargs(#s) = {},
          Uargs(findMin#2) = {1}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         minSort#1(x1) = [1 1] x1 + [1]
                         [0 0]      [1]
         #true() = [0]
                   [0]
         #false() = [1]
                    [0]
         findMin#3(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [1]
                                     [0 0]      [1 1]      [1 1]      [0 0]      [1]
         ::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                      [0 0]      [0 0]      [1]
         #LT() = [0]
                 [0]
         findMin#1(x1) = [0 0] x1 + [1]
                         [0 0]      [1]
         #cklt(x1) = [1 0] x1 + [1]
                     [0 0]      [1]
         #pos(x1) = [0 0] x1 + [0]
                    [0 0]      [0]
         #0() = [0]
                [0]
         findMin(x1) = [0 0] x1 + [0]
                       [0 0]      [0]
         #neg(x1) = [0 0] x1 + [0]
                    [0 0]      [0]
         #EQ() = [0]
                 [0]
         #less(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                         [0 0]      [0 0]      [0]
         minSort(x1) = [0 0] x1 + [2]
                       [0 0]      [1]
         #compare(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                            [0 0]      [0 0]      [1]
         #s(x1) = [0 0] x1 + [0]
                  [0 0]      [0]
         #GT() = [0]
                 [0]
         nil() = [0]
                 [0]
         findMin#2(x1, x2) = [1 0] x1 + [0 0] x2 + [1]
                             [0 0]      [0 0]      [1]
      
      The strictly oriented rules are moved into the weak component.
      
      We consider the following Problem:
      
        Strict Trs:
          {  #less(@x, @y) -> #cklt(#compare(@x, @y))
           , findMin(@l) -> findMin#1(@l)
           , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
           , findMin#2(::(@y, @ys), @x) ->
             findMin#3(#less(@x, @y), @x, @y, @ys)}
        Weak Trs:
          {  minSort(@l) -> minSort#1(findMin(@l))
           , findMin#1(nil()) -> nil()
           , findMin#2(nil(), @x) -> ::(@x, nil())
           , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
           , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
           , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
           , minSort#1(nil()) -> nil()
           , #cklt(#EQ()) -> #false()
           , #cklt(#GT()) -> #false()
           , #cklt(#LT()) -> #true()
           , #compare(#0(), #0()) -> #EQ()
           , #compare(#0(), #neg(@y)) -> #GT()
           , #compare(#0(), #pos(@y)) -> #LT()
           , #compare(#0(), #s(@y)) -> #LT()
           , #compare(#neg(@x), #0()) -> #LT()
           , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
           , #compare(#neg(@x), #pos(@y)) -> #LT()
           , #compare(#pos(@x), #0()) -> #GT()
           , #compare(#pos(@x), #neg(@y)) -> #GT()
           , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
           , #compare(#s(@x), #0()) -> #GT()
           , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^2))
      
      Proof:
        The weightgap principle applies, where following rules are oriented strictly:
        
        TRS Component: {#less(@x, @y) -> #cklt(#compare(@x, @y))}
        
        Interpretation of nonconstant growth:
        -------------------------------------
          The following argument positions are usable:
            Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
            Uargs(findMin#1) = {}, Uargs(#cklt) = {1}, Uargs(#pos) = {},
            Uargs(findMin) = {}, Uargs(#neg) = {}, Uargs(#less) = {},
            Uargs(minSort) = {}, Uargs(#compare) = {}, Uargs(#s) = {},
            Uargs(findMin#2) = {1}
          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
          Interpretation Functions:
           minSort#1(x1) = [1 0] x1 + [1]
                           [0 0]      [1]
           #true() = [0]
                     [0]
           #false() = [0]
                      [0]
           findMin#3(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [1]
                                       [0 0]      [1 1]      [1 1]      [0 0]      [1]
           ::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                        [0 0]      [0 0]      [1]
           #LT() = [0]
                   [0]
           findMin#1(x1) = [0 0] x1 + [1]
                           [0 0]      [1]
           #cklt(x1) = [1 0] x1 + [1]
                       [0 0]      [1]
           #pos(x1) = [0 0] x1 + [0]
                      [0 0]      [0]
           #0() = [0]
                  [0]
           findMin(x1) = [0 0] x1 + [0]
                         [0 0]      [0]
           #neg(x1) = [0 0] x1 + [0]
                      [0 0]      [0]
           #EQ() = [0]
                   [0]
           #less(x1, x2) = [0 0] x1 + [0 0] x2 + [2]
                           [0 0]      [0 0]      [1]
           minSort(x1) = [0 0] x1 + [1]
                         [0 0]      [2]
           #compare(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                              [0 0]      [0 0]      [1]
           #s(x1) = [0 0] x1 + [0]
                    [0 0]      [0]
           #GT() = [0]
                   [0]
           nil() = [0]
                   [0]
           findMin#2(x1, x2) = [1 0] x1 + [0 0] x2 + [1]
                               [0 0]      [0 0]      [1]
        
        The strictly oriented rules are moved into the weak component.
        
        We consider the following Problem:
        
          Strict Trs:
            {  findMin(@l) -> findMin#1(@l)
             , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
             , findMin#2(::(@y, @ys), @x) ->
               findMin#3(#less(@x, @y), @x, @y, @ys)}
          Weak Trs:
            {  #less(@x, @y) -> #cklt(#compare(@x, @y))
             , minSort(@l) -> minSort#1(findMin(@l))
             , findMin#1(nil()) -> nil()
             , findMin#2(nil(), @x) -> ::(@x, nil())
             , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
             , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
             , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
             , minSort#1(nil()) -> nil()
             , #cklt(#EQ()) -> #false()
             , #cklt(#GT()) -> #false()
             , #cklt(#LT()) -> #true()
             , #compare(#0(), #0()) -> #EQ()
             , #compare(#0(), #neg(@y)) -> #GT()
             , #compare(#0(), #pos(@y)) -> #LT()
             , #compare(#0(), #s(@y)) -> #LT()
             , #compare(#neg(@x), #0()) -> #LT()
             , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
             , #compare(#neg(@x), #pos(@y)) -> #LT()
             , #compare(#pos(@x), #0()) -> #GT()
             , #compare(#pos(@x), #neg(@y)) -> #GT()
             , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
             , #compare(#s(@x), #0()) -> #GT()
             , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(?,O(n^2))
        
        Proof:
          The weightgap principle applies, where following rules are oriented strictly:
          
          TRS Component:
            {findMin#2(::(@y, @ys), @x) ->
             findMin#3(#less(@x, @y), @x, @y, @ys)}
          
          Interpretation of nonconstant growth:
          -------------------------------------
            The following argument positions are usable:
              Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
              Uargs(findMin#1) = {}, Uargs(#cklt) = {1}, Uargs(#pos) = {},
              Uargs(findMin) = {}, Uargs(#neg) = {}, Uargs(#less) = {},
              Uargs(minSort) = {}, Uargs(#compare) = {}, Uargs(#s) = {},
              Uargs(findMin#2) = {1}
            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
            Interpretation Functions:
             minSort#1(x1) = [1 0] x1 + [1]
                             [0 0]      [1]
             #true() = [0]
                       [0]
             #false() = [0]
                        [0]
             findMin#3(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [0]
                                         [0 0]      [1 1]      [0 0]      [0 0]      [1]
             ::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                          [0 0]      [0 0]      [1]
             #LT() = [0]
                     [0]
             findMin#1(x1) = [0 0] x1 + [1]
                             [0 0]      [1]
             #cklt(x1) = [1 0] x1 + [0]
                         [0 0]      [1]
             #pos(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
             #0() = [0]
                    [0]
             findMin(x1) = [0 0] x1 + [0]
                           [0 0]      [0]
             #neg(x1) = [0 0] x1 + [0]
                        [0 0]      [0]
             #EQ() = [0]
                     [0]
             #less(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [1]
             minSort(x1) = [0 0] x1 + [1]
                           [0 0]      [2]
             #compare(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                [0 0]      [0 0]      [1]
             #s(x1) = [0 0] x1 + [0]
                      [0 0]      [0]
             #GT() = [0]
                     [0]
             nil() = [0]
                     [0]
             findMin#2(x1, x2) = [1 0] x1 + [0 0] x2 + [1]
                                 [0 0]      [1 1]      [1]
          
          The strictly oriented rules are moved into the weak component.
          
          We consider the following Problem:
          
            Strict Trs:
              {  findMin(@l) -> findMin#1(@l)
               , findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)}
            Weak Trs:
              {  findMin#2(::(@y, @ys), @x) ->
                 findMin#3(#less(@x, @y), @x, @y, @ys)
               , #less(@x, @y) -> #cklt(#compare(@x, @y))
               , minSort(@l) -> minSort#1(findMin(@l))
               , findMin#1(nil()) -> nil()
               , findMin#2(nil(), @x) -> ::(@x, nil())
               , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
               , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
               , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
               , minSort#1(nil()) -> nil()
               , #cklt(#EQ()) -> #false()
               , #cklt(#GT()) -> #false()
               , #cklt(#LT()) -> #true()
               , #compare(#0(), #0()) -> #EQ()
               , #compare(#0(), #neg(@y)) -> #GT()
               , #compare(#0(), #pos(@y)) -> #LT()
               , #compare(#0(), #s(@y)) -> #LT()
               , #compare(#neg(@x), #0()) -> #LT()
               , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
               , #compare(#neg(@x), #pos(@y)) -> #LT()
               , #compare(#pos(@x), #0()) -> #GT()
               , #compare(#pos(@x), #neg(@y)) -> #GT()
               , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
               , #compare(#s(@x), #0()) -> #GT()
               , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(?,O(n^2))
          
          Proof:
            The weightgap principle applies, where following rules are oriented strictly:
            
            TRS Component:
              {findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)}
            
            Interpretation of nonconstant growth:
            -------------------------------------
              The following argument positions are usable:
                Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
                Uargs(findMin#1) = {}, Uargs(#cklt) = {1}, Uargs(#pos) = {},
                Uargs(findMin) = {}, Uargs(#neg) = {}, Uargs(#less) = {},
                Uargs(minSort) = {}, Uargs(#compare) = {}, Uargs(#s) = {},
                Uargs(findMin#2) = {1}
              We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
              Interpretation Functions:
               minSort#1(x1) = [1 3] x1 + [2]
                               [0 0]      [3]
               #true() = [0]
                         [0]
               #false() = [0]
                          [0]
               findMin#3(x1, x2, x3, x4) = [1 0] x1 + [0 0] x2 + [0 0] x3 + [1 0] x4 + [0]
                                           [0 0]      [0 0]      [0 0]      [0 0]      [2]
               ::(x1, x2) = [0 0] x1 + [1 0] x2 + [0]
                            [0 0]      [0 0]      [2]
               #LT() = [0]
                       [0]
               findMin#1(x1) = [0 0] x1 + [1]
                               [0 0]      [3]
               #cklt(x1) = [1 0] x1 + [0]
                           [0 0]      [1]
               #pos(x1) = [0 0] x1 + [0]
                          [0 1]      [0]
               #0() = [0]
                      [1]
               findMin(x1) = [0 0] x1 + [0]
                             [0 0]      [0]
               #neg(x1) = [0 0] x1 + [0]
                          [0 1]      [0]
               #EQ() = [0]
                       [0]
               #less(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                               [0 0]      [0 0]      [2]
               minSort(x1) = [0 0] x1 + [2]
                             [0 0]      [3]
               #compare(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                                  [0 1]      [0 1]      [1]
               #s(x1) = [0 0] x1 + [0]
                        [0 1]      [0]
               #GT() = [0]
                       [0]
               nil() = [0]
                       [2]
               findMin#2(x1, x2) = [1 2] x1 + [0 0] x2 + [0]
                                   [0 0]      [0 0]      [3]
            
            The strictly oriented rules are moved into the weak component.
            
            We consider the following Problem:
            
              Strict Trs: {findMin(@l) -> findMin#1(@l)}
              Weak Trs:
                {  findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
                 , findMin#2(::(@y, @ys), @x) ->
                   findMin#3(#less(@x, @y), @x, @y, @ys)
                 , #less(@x, @y) -> #cklt(#compare(@x, @y))
                 , minSort(@l) -> minSort#1(findMin(@l))
                 , findMin#1(nil()) -> nil()
                 , findMin#2(nil(), @x) -> ::(@x, nil())
                 , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
                 , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
                 , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
                 , minSort#1(nil()) -> nil()
                 , #cklt(#EQ()) -> #false()
                 , #cklt(#GT()) -> #false()
                 , #cklt(#LT()) -> #true()
                 , #compare(#0(), #0()) -> #EQ()
                 , #compare(#0(), #neg(@y)) -> #GT()
                 , #compare(#0(), #pos(@y)) -> #LT()
                 , #compare(#0(), #s(@y)) -> #LT()
                 , #compare(#neg(@x), #0()) -> #LT()
                 , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
                 , #compare(#neg(@x), #pos(@y)) -> #LT()
                 , #compare(#pos(@x), #0()) -> #GT()
                 , #compare(#pos(@x), #neg(@y)) -> #GT()
                 , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
                 , #compare(#s(@x), #0()) -> #GT()
                 , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: YES(?,O(n^2))
            
            Proof:
              We consider the following Problem:
              
                Strict Trs: {findMin(@l) -> findMin#1(@l)}
                Weak Trs:
                  {  findMin#1(::(@x, @xs)) -> findMin#2(findMin(@xs), @x)
                   , findMin#2(::(@y, @ys), @x) ->
                     findMin#3(#less(@x, @y), @x, @y, @ys)
                   , #less(@x, @y) -> #cklt(#compare(@x, @y))
                   , minSort(@l) -> minSort#1(findMin(@l))
                   , findMin#1(nil()) -> nil()
                   , findMin#2(nil(), @x) -> ::(@x, nil())
                   , findMin#3(#false(), @x, @y, @ys) -> ::(@y, ::(@x, @ys))
                   , findMin#3(#true(), @x, @y, @ys) -> ::(@x, ::(@y, @ys))
                   , minSort#1(::(@x, @xs)) -> ::(@x, minSort(@xs))
                   , minSort#1(nil()) -> nil()
                   , #cklt(#EQ()) -> #false()
                   , #cklt(#GT()) -> #false()
                   , #cklt(#LT()) -> #true()
                   , #compare(#0(), #0()) -> #EQ()
                   , #compare(#0(), #neg(@y)) -> #GT()
                   , #compare(#0(), #pos(@y)) -> #LT()
                   , #compare(#0(), #s(@y)) -> #LT()
                   , #compare(#neg(@x), #0()) -> #LT()
                   , #compare(#neg(@x), #neg(@y)) -> #compare(@y, @x)
                   , #compare(#neg(@x), #pos(@y)) -> #LT()
                   , #compare(#pos(@x), #0()) -> #GT()
                   , #compare(#pos(@x), #neg(@y)) -> #GT()
                   , #compare(#pos(@x), #pos(@y)) -> #compare(@x, @y)
                   , #compare(#s(@x), #0()) -> #GT()
                   , #compare(#s(@x), #s(@y)) -> #compare(@x, @y)}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(?,O(n^2))
              
              Proof:
                The following argument positions are usable:
                  Uargs(minSort#1) = {1}, Uargs(findMin#3) = {1}, Uargs(::) = {2},
                  Uargs(findMin#1) = {}, Uargs(#cklt) = {1}, Uargs(#pos) = {},
                  Uargs(findMin) = {}, Uargs(#neg) = {}, Uargs(#less) = {},
                  Uargs(minSort) = {}, Uargs(#compare) = {}, Uargs(#s) = {},
                  Uargs(findMin#2) = {1}
                We have the following constructor-based EDA-non-satisfying and IDA(2)-non-satisfying matrix interpretation:
                Interpretation Functions:
                 minSort#1(x1) = [1 0 2] x1 + [0]
                                 [0 2 0]      [0]
                                 [0 0 2]      [2]
                 #true() = [0]
                           [2]
                           [0]
                 #false() = [0]
                            [2]
                            [0]
                 findMin#3(x1, x2, x3, x4) = [1 0 0] x1 + [0 0 0] x2 + [0 0 0] x3 + [1 0 0] x4 + [0]
                                             [0 2 0]      [0 0 0]      [0 0 0]      [0 1 0]      [0]
                                             [0 2 0]      [0 0 0]      [0 0 0]      [0 2 1]      [0]
                 ::(x1, x2) = [0 0 0] x1 + [1 0 0] x2 + [0]
                              [0 0 0]      [0 1 0]      [2]
                              [0 0 0]      [0 1 1]      [1]
                 #LT() = [0]
                         [0]
                         [0]
                 findMin#1(x1) = [0 2 0] x1 + [0]
                                 [0 1 0]      [0]
                                 [0 0 1]      [0]
                 #cklt(x1) = [2 0 0] x1 + [0]
                             [0 0 0]      [2]
                             [0 1 0]      [0]
                 #pos(x1) = [1 0 0] x1 + [0]
                            [0 1 0]      [1]
                            [0 0 0]      [0]
                 #0() = [0]
                        [2]
                        [0]
                 findMin(x1) = [0 2 0] x1 + [1]
                               [0 1 0]      [0]
                               [0 0 1]      [0]
                 #neg(x1) = [0 0 0] x1 + [0]
                            [0 1 0]      [0]
                            [0 0 0]      [0]
                 #EQ() = [0]
                         [1]
                         [0]
                 #less(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                                 [0 0 0]      [0 0 0]      [2]
                                 [0 1 0]      [0 1 0]      [1]
                 minSort(x1) = [0 2 2] x1 + [1]
                               [0 2 0]      [0]
                               [0 0 2]      [2]
                 #compare(x1, x2) = [0 0 0] x1 + [0 0 0] x2 + [0]
                                    [0 1 0]      [0 1 0]      [1]
                                    [0 1 0]      [0 1 0]      [0]
                 #s(x1) = [0 0 0] x1 + [0]
                          [0 1 0]      [0]
                          [0 0 1]      [0]
                 #GT() = [0]
                         [0]
                         [0]
                 nil() = [0]
                         [0]
                         [0]
                 findMin#2(x1, x2) = [1 0 0] x1 + [0 0 0] x2 + [0]
                                     [0 1 0]      [0 0 0]      [2]
                                     [0 1 1]      [0 0 0]      [1]

Hurray, we answered YES(?,O(n^2))