We consider the following Problem:

  Strict Trs:
    {  min(0(), y) -> 0()
     , min(x, 0()) -> 0()
     , min(s(x), s(y)) -> s(min(x, y))
     , max(0(), y) -> y
     , max(x, 0()) -> x
     , max(s(x), s(y)) -> s(max(x, y))
     , twice(0()) -> 0()
     , twice(s(x)) -> s(s(twice(x)))
     , -(x, 0()) -> x
     , -(s(x), s(y)) -> -(x, y)
     , p(s(x)) -> x
     , f(s(x), s(y)) ->
       f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))}
  StartTerms: basic terms
  Strategy: innermost

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

Proof:
  We consider the following Problem:
  
    Strict Trs:
      {  min(0(), y) -> 0()
       , min(x, 0()) -> 0()
       , min(s(x), s(y)) -> s(min(x, y))
       , max(0(), y) -> y
       , max(x, 0()) -> x
       , max(s(x), s(y)) -> s(max(x, y))
       , twice(0()) -> 0()
       , twice(s(x)) -> s(s(twice(x)))
       , -(x, 0()) -> x
       , -(s(x), s(y)) -> -(x, y)
       , p(s(x)) -> x
       , f(s(x), s(y)) ->
         f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))}
    StartTerms: basic terms
    Strategy: innermost
  
  Certificate: YES(?,O(n^1))
  
  Proof:
    The weightgap principle applies, where following rules are oriented strictly:
    
    TRS Component:
      {  min(0(), y) -> 0()
       , min(x, 0()) -> 0()
       , twice(0()) -> 0()}
    
    Interpretation of nonconstant growth:
    -------------------------------------
      The following argument positions are usable:
        Uargs(min) = {}, Uargs(s) = {1}, Uargs(max) = {},
        Uargs(twice) = {1}, Uargs(-) = {1, 2}, Uargs(p) = {1},
        Uargs(f) = {1, 2}
      We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
      Interpretation Functions:
       min(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                     [0 0]      [1 0]      [1]
       0() = [0]
             [0]
       s(x1) = [1 0] x1 + [0]
               [0 0]      [1]
       max(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                     [0 0]      [0 0]      [1]
       twice(x1) = [1 0] x1 + [1]
                   [0 0]      [1]
       -(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                   [0 0]      [0 0]      [1]
       p(x1) = [1 0] x1 + [1]
               [0 0]      [1]
       f(x1, x2) = [1 0] x1 + [1 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:
        {  min(s(x), s(y)) -> s(min(x, y))
         , max(0(), y) -> y
         , max(x, 0()) -> x
         , max(s(x), s(y)) -> s(max(x, y))
         , twice(s(x)) -> s(s(twice(x)))
         , -(x, 0()) -> x
         , -(s(x), s(y)) -> -(x, y)
         , p(s(x)) -> x
         , f(s(x), s(y)) ->
           f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))}
      Weak Trs:
        {  min(0(), y) -> 0()
         , min(x, 0()) -> 0()
         , twice(0()) -> 0()}
      StartTerms: basic terms
      Strategy: innermost
    
    Certificate: YES(?,O(n^1))
    
    Proof:
      The weightgap principle applies, where following rules are oriented strictly:
      
      TRS Component: {max(x, 0()) -> x}
      
      Interpretation of nonconstant growth:
      -------------------------------------
        The following argument positions are usable:
          Uargs(min) = {}, Uargs(s) = {1}, Uargs(max) = {},
          Uargs(twice) = {1}, Uargs(-) = {1, 2}, Uargs(p) = {1},
          Uargs(f) = {1, 2}
        We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
        Interpretation Functions:
         min(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                       [0 0]      [0 0]      [0]
         0() = [1]
               [0]
         s(x1) = [1 0] x1 + [0]
                 [0 1]      [0]
         max(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                       [0 1]      [0 0]      [0]
         twice(x1) = [1 0] x1 + [0]
                     [0 0]      [0]
         -(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                     [0 0]      [0 0]      [0]
         p(x1) = [1 0] x1 + [0]
                 [0 0]      [0]
         f(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                     [0 0]      [0 0]      [1]
      
      The strictly oriented rules are moved into the weak component.
      
      We consider the following Problem:
      
        Strict Trs:
          {  min(s(x), s(y)) -> s(min(x, y))
           , max(0(), y) -> y
           , max(s(x), s(y)) -> s(max(x, y))
           , twice(s(x)) -> s(s(twice(x)))
           , -(x, 0()) -> x
           , -(s(x), s(y)) -> -(x, y)
           , p(s(x)) -> x
           , f(s(x), s(y)) ->
             f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))}
        Weak Trs:
          {  max(x, 0()) -> x
           , min(0(), y) -> 0()
           , min(x, 0()) -> 0()
           , twice(0()) -> 0()}
        StartTerms: basic terms
        Strategy: innermost
      
      Certificate: YES(?,O(n^1))
      
      Proof:
        The weightgap principle applies, where following rules are oriented strictly:
        
        TRS Component:
          {  max(0(), y) -> y
           , max(s(x), s(y)) -> s(max(x, y))
           , -(x, 0()) -> x
           , -(s(x), s(y)) -> -(x, y)}
        
        Interpretation of nonconstant growth:
        -------------------------------------
          The following argument positions are usable:
            Uargs(min) = {}, Uargs(s) = {1}, Uargs(max) = {},
            Uargs(twice) = {1}, Uargs(-) = {1, 2}, Uargs(p) = {1},
            Uargs(f) = {1, 2}
          We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
          Interpretation Functions:
           min(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                         [1 0]      [1 0]      [1]
           0() = [0]
                 [0]
           s(x1) = [1 0] x1 + [1]
                   [0 1]      [2]
           max(x1, x2) = [1 0] x1 + [1 0] x2 + [3]
                         [0 1]      [0 1]      [1]
           twice(x1) = [1 0] x1 + [0]
                       [0 1]      [0]
           -(x1, x2) = [1 0] x1 + [1 0] x2 + [2]
                       [0 1]      [0 1]      [2]
           p(x1) = [1 0] x1 + [0]
                   [0 0]      [3]
           f(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                       [0 1]      [0 1]      [0]
        
        The strictly oriented rules are moved into the weak component.
        
        We consider the following Problem:
        
          Strict Trs:
            {  min(s(x), s(y)) -> s(min(x, y))
             , twice(s(x)) -> s(s(twice(x)))
             , p(s(x)) -> x
             , f(s(x), s(y)) ->
               f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))}
          Weak Trs:
            {  max(0(), y) -> y
             , max(s(x), s(y)) -> s(max(x, y))
             , -(x, 0()) -> x
             , -(s(x), s(y)) -> -(x, y)
             , max(x, 0()) -> x
             , min(0(), y) -> 0()
             , min(x, 0()) -> 0()
             , twice(0()) -> 0()}
          StartTerms: basic terms
          Strategy: innermost
        
        Certificate: YES(?,O(n^1))
        
        Proof:
          The weightgap principle applies, where following rules are oriented strictly:
          
          TRS Component: {p(s(x)) -> x}
          
          Interpretation of nonconstant growth:
          -------------------------------------
            The following argument positions are usable:
              Uargs(min) = {}, Uargs(s) = {1}, Uargs(max) = {},
              Uargs(twice) = {1}, Uargs(-) = {1, 2}, Uargs(p) = {1},
              Uargs(f) = {1, 2}
            We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
            Interpretation Functions:
             min(x1, x2) = [0 0] x1 + [0 0] x2 + [1]
                           [0 0]      [1 0]      [1]
             0() = [0]
                   [0]
             s(x1) = [1 0] x1 + [0]
                     [0 1]      [0]
             max(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                           [0 1]      [0 1]      [1]
             twice(x1) = [1 0] x1 + [0]
                         [0 0]      [1]
             -(x1, x2) = [1 0] x1 + [1 0] x2 + [1]
                         [0 1]      [0 0]      [1]
             p(x1) = [1 0] x1 + [2]
                     [0 1]      [0]
             f(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                         [0 0]      [0 0]      [1]
          
          The strictly oriented rules are moved into the weak component.
          
          We consider the following Problem:
          
            Strict Trs:
              {  min(s(x), s(y)) -> s(min(x, y))
               , twice(s(x)) -> s(s(twice(x)))
               , f(s(x), s(y)) ->
                 f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))}
            Weak Trs:
              {  p(s(x)) -> x
               , max(0(), y) -> y
               , max(s(x), s(y)) -> s(max(x, y))
               , -(x, 0()) -> x
               , -(s(x), s(y)) -> -(x, y)
               , max(x, 0()) -> x
               , min(0(), y) -> 0()
               , min(x, 0()) -> 0()
               , twice(0()) -> 0()}
            StartTerms: basic terms
            Strategy: innermost
          
          Certificate: YES(?,O(n^1))
          
          Proof:
            The weightgap principle applies, where following rules are oriented strictly:
            
            TRS Component:
              {f(s(x), s(y)) ->
               f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))}
            
            Interpretation of nonconstant growth:
            -------------------------------------
              The following argument positions are usable:
                Uargs(min) = {}, Uargs(s) = {1}, Uargs(max) = {},
                Uargs(twice) = {1}, Uargs(-) = {1, 2}, Uargs(p) = {1},
                Uargs(f) = {1, 2}
              We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
              Interpretation Functions:
               min(x1, x2) = [0 0] x1 + [0 0] x2 + [0]
                             [0 0]      [0 0]      [0]
               0() = [0]
                     [0]
               s(x1) = [1 0] x1 + [0]
                       [0 1]      [1]
               max(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                             [0 1]      [0 1]      [0]
               twice(x1) = [1 2] x1 + [0]
                           [0 0]      [0]
               -(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                           [0 1]      [0 0]      [1]
               p(x1) = [1 0] x1 + [1]
                       [0 1]      [0]
               f(x1, x2) = [1 0] x1 + [1 2] x2 + [0]
                           [0 0]      [0 0]      [1]
            
            The strictly oriented rules are moved into the weak component.
            
            We consider the following Problem:
            
              Strict Trs:
                {  min(s(x), s(y)) -> s(min(x, y))
                 , twice(s(x)) -> s(s(twice(x)))}
              Weak Trs:
                {  f(s(x), s(y)) ->
                   f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                 , p(s(x)) -> x
                 , max(0(), y) -> y
                 , max(s(x), s(y)) -> s(max(x, y))
                 , -(x, 0()) -> x
                 , -(s(x), s(y)) -> -(x, y)
                 , max(x, 0()) -> x
                 , min(0(), y) -> 0()
                 , min(x, 0()) -> 0()
                 , twice(0()) -> 0()}
              StartTerms: basic terms
              Strategy: innermost
            
            Certificate: YES(?,O(n^1))
            
            Proof:
              The weightgap principle applies, where following rules are oriented strictly:
              
              TRS Component: {min(s(x), s(y)) -> s(min(x, y))}
              
              Interpretation of nonconstant growth:
              -------------------------------------
                The following argument positions are usable:
                  Uargs(min) = {}, Uargs(s) = {1}, Uargs(max) = {},
                  Uargs(twice) = {1}, Uargs(-) = {1, 2}, Uargs(p) = {1},
                  Uargs(f) = {1, 2}
                We have the following EDA-non-satisfying and IDA(1)-non-satisfying matrix interpretation:
                Interpretation Functions:
                 min(x1, x2) = [0 0] x1 + [0 1] x2 + [0]
                               [0 0]      [0 1]      [0]
                 0() = [0]
                       [0]
                 s(x1) = [1 0] x1 + [0]
                         [0 1]      [1]
                 max(x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                               [0 1]      [0 1]      [1]
                 twice(x1) = [1 0] x1 + [0]
                             [0 0]      [0]
                 -(x1, x2) = [1 0] x1 + [1 1] x2 + [0]
                             [0 1]      [0 0]      [1]
                 p(x1) = [1 0] x1 + [0]
                         [0 1]      [0]
                 f(x1, x2) = [1 0] x1 + [1 3] x2 + [0]
                             [0 0]      [0 0]      [1]
              
              The strictly oriented rules are moved into the weak component.
              
              We consider the following Problem:
              
                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                Weak Trs:
                  {  min(s(x), s(y)) -> s(min(x, y))
                   , f(s(x), s(y)) ->
                     f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                   , p(s(x)) -> x
                   , max(0(), y) -> y
                   , max(s(x), s(y)) -> s(max(x, y))
                   , -(x, 0()) -> x
                   , -(s(x), s(y)) -> -(x, y)
                   , max(x, 0()) -> x
                   , min(0(), y) -> 0()
                   , min(x, 0()) -> 0()
                   , twice(0()) -> 0()}
                StartTerms: basic terms
                Strategy: innermost
              
              Certificate: YES(?,O(n^1))
              
              Proof:
                We consider the following Problem:
                
                  Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                  Weak Trs:
                    {  min(s(x), s(y)) -> s(min(x, y))
                     , f(s(x), s(y)) ->
                       f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                     , p(s(x)) -> x
                     , max(0(), y) -> y
                     , max(s(x), s(y)) -> s(max(x, y))
                     , -(x, 0()) -> x
                     , -(s(x), s(y)) -> -(x, y)
                     , max(x, 0()) -> x
                     , min(0(), y) -> 0()
                     , min(x, 0()) -> 0()
                     , twice(0()) -> 0()}
                  StartTerms: basic terms
                  Strategy: innermost
                
                Certificate: YES(?,O(n^1))
                
                Proof:
                  We have computed the following dependency pairs
                  
                    Strict DPs: {twice^#(s(x)) -> twice^#(x)}
                    Weak DPs:
                      {  min^#(s(x), s(y)) -> min^#(x, y)
                       , f^#(s(x), s(y)) ->
                         f^#(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                       , p^#(s(x)) -> c_4()
                       , max^#(0(), y) -> c_5()
                       , max^#(s(x), s(y)) -> max^#(x, y)
                       , -^#(x, 0()) -> c_7()
                       , -^#(s(x), s(y)) -> -^#(x, y)
                       , max^#(x, 0()) -> c_9()
                       , min^#(0(), y) -> c_10()
                       , min^#(x, 0()) -> c_11()
                       , twice^#(0()) -> c_12()}
                  
                  We consider the following Problem:
                  
                    Strict DPs: {twice^#(s(x)) -> twice^#(x)}
                    Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                    Weak DPs:
                      {  min^#(s(x), s(y)) -> min^#(x, y)
                       , f^#(s(x), s(y)) ->
                         f^#(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                       , p^#(s(x)) -> c_4()
                       , max^#(0(), y) -> c_5()
                       , max^#(s(x), s(y)) -> max^#(x, y)
                       , -^#(x, 0()) -> c_7()
                       , -^#(s(x), s(y)) -> -^#(x, y)
                       , max^#(x, 0()) -> c_9()
                       , min^#(0(), y) -> c_10()
                       , min^#(x, 0()) -> c_11()
                       , twice^#(0()) -> c_12()}
                    Weak Trs:
                      {  min(s(x), s(y)) -> s(min(x, y))
                       , f(s(x), s(y)) ->
                         f(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                       , p(s(x)) -> x
                       , max(0(), y) -> y
                       , max(s(x), s(y)) -> s(max(x, y))
                       , -(x, 0()) -> x
                       , -(s(x), s(y)) -> -(x, y)
                       , max(x, 0()) -> x
                       , min(0(), y) -> 0()
                       , min(x, 0()) -> 0()
                       , twice(0()) -> 0()}
                    StartTerms: basic terms
                    Strategy: innermost
                  
                  Certificate: YES(?,O(n^1))
                  
                  Proof:
                    We replace strict/weak-rules by the corresponding usable rules:
                    
                      Strict Usable Rules: {twice(s(x)) -> s(s(twice(x)))}
                      Weak Usable Rules:
                        {  min(s(x), s(y)) -> s(min(x, y))
                         , p(s(x)) -> x
                         , max(0(), y) -> y
                         , max(s(x), s(y)) -> s(max(x, y))
                         , -(x, 0()) -> x
                         , -(s(x), s(y)) -> -(x, y)
                         , max(x, 0()) -> x
                         , min(0(), y) -> 0()
                         , min(x, 0()) -> 0()
                         , twice(0()) -> 0()}
                    
                    We consider the following Problem:
                    
                      Strict DPs: {twice^#(s(x)) -> twice^#(x)}
                      Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                      Weak DPs:
                        {  min^#(s(x), s(y)) -> min^#(x, y)
                         , f^#(s(x), s(y)) ->
                           f^#(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                         , p^#(s(x)) -> c_4()
                         , max^#(0(), y) -> c_5()
                         , max^#(s(x), s(y)) -> max^#(x, y)
                         , -^#(x, 0()) -> c_7()
                         , -^#(s(x), s(y)) -> -^#(x, y)
                         , max^#(x, 0()) -> c_9()
                         , min^#(0(), y) -> c_10()
                         , min^#(x, 0()) -> c_11()
                         , twice^#(0()) -> c_12()}
                      Weak Trs:
                        {  min(s(x), s(y)) -> s(min(x, y))
                         , p(s(x)) -> x
                         , max(0(), y) -> y
                         , max(s(x), s(y)) -> s(max(x, y))
                         , -(x, 0()) -> x
                         , -(s(x), s(y)) -> -(x, y)
                         , max(x, 0()) -> x
                         , min(0(), y) -> 0()
                         , min(x, 0()) -> 0()
                         , twice(0()) -> 0()}
                      StartTerms: basic terms
                      Strategy: innermost
                    
                    Certificate: YES(?,O(n^1))
                    
                    Proof:
                      We consider the following Problem:
                      
                        Strict DPs: {twice^#(s(x)) -> twice^#(x)}
                        Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                        Weak DPs:
                          {  min^#(s(x), s(y)) -> min^#(x, y)
                           , f^#(s(x), s(y)) ->
                             f^#(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                           , p^#(s(x)) -> c_4()
                           , max^#(0(), y) -> c_5()
                           , max^#(s(x), s(y)) -> max^#(x, y)
                           , -^#(x, 0()) -> c_7()
                           , -^#(s(x), s(y)) -> -^#(x, y)
                           , max^#(x, 0()) -> c_9()
                           , min^#(0(), y) -> c_10()
                           , min^#(x, 0()) -> c_11()
                           , twice^#(0()) -> c_12()}
                        Weak Trs:
                          {  min(s(x), s(y)) -> s(min(x, y))
                           , p(s(x)) -> x
                           , max(0(), y) -> y
                           , max(s(x), s(y)) -> s(max(x, y))
                           , -(x, 0()) -> x
                           , -(s(x), s(y)) -> -(x, y)
                           , max(x, 0()) -> x
                           , min(0(), y) -> 0()
                           , min(x, 0()) -> 0()
                           , twice(0()) -> 0()}
                        StartTerms: basic terms
                        Strategy: innermost
                      
                      Certificate: YES(?,O(n^1))
                      
                      Proof:
                        We use following congruence DG for path analysis
                        
                        ->11:{1}                                                    [   YES(?,O(n^1))    ]
                           |
                           `->12:{12}                                               [   YES(O(1),O(1))   ]
                        
                        ->8:{2}                                                     [      subsumed      ]
                           |
                           |->9:{10}                                                [   YES(O(1),O(1))   ]
                           |
                           `->10:{11}                                               [   YES(O(1),O(1))   ]
                        
                        ->7:{3}                                                     [   YES(O(1),O(1))   ]
                        
                        ->6:{4}                                                     [   YES(O(1),O(1))   ]
                        
                        ->3:{6}                                                     [      subsumed      ]
                           |
                           |->5:{5}                                                 [   YES(O(1),O(1))   ]
                           |
                           `->4:{9}                                                 [   YES(O(1),O(1))   ]
                        
                        ->1:{8}                                                     [      subsumed      ]
                           |
                           `->2:{7}                                                 [   YES(O(1),O(1))   ]
                        
                        
                        Here dependency-pairs are as follows:
                        
                        Strict DPs:
                          {1: twice^#(s(x)) -> twice^#(x)}
                        WeakDPs DPs:
                          {  2: min^#(s(x), s(y)) -> min^#(x, y)
                           , 3: f^#(s(x), s(y)) ->
                                f^#(-(max(s(x), s(y)), min(s(x), s(y))), p(twice(min(x, y))))
                           , 4: p^#(s(x)) -> c_4()
                           , 5: max^#(0(), y) -> c_5()
                           , 6: max^#(s(x), s(y)) -> max^#(x, y)
                           , 7: -^#(x, 0()) -> c_7()
                           , 8: -^#(s(x), s(y)) -> -^#(x, y)
                           , 9: max^#(x, 0()) -> c_9()
                           , 10: min^#(0(), y) -> c_10()
                           , 11: min^#(x, 0()) -> c_11()
                           , 12: twice^#(0()) -> c_12()}
                        
                        * Path 11:{1}: YES(?,O(n^1))
                          --------------------------
                          
                          We consider the following Problem:
                          
                            Strict DPs: {twice^#(s(x)) -> twice^#(x)}
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(?,O(n^1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict DPs: {twice^#(s(x)) -> twice^#(x)}
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(?,O(n^1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict DPs: {twice^#(s(x)) -> twice^#(x)}
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(?,O(n^1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  Strict DPs: {twice^#(s(x)) -> twice^#(x)}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(?,O(n^1))
                                
                                Proof:
                                  The problem is match-bounded by 1.
                                  The enriched problem is compatible with the following automaton:
                                  {  s_0(2) -> 2
                                   , twice^#_0(2) -> 1
                                   , twice^#_1(2) -> 1}
                        
                        * Path 11:{1}->12:{12}: YES(O(1),O(1))
                          ------------------------------------
                          
                          We consider the following Problem:
                          
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak DPs: {twice^#(s(x)) -> twice^#(x)}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(O(1),O(1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak DPs: {twice^#(s(x)) -> twice^#(x)}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(O(1),O(1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak DPs: {twice^#(s(x)) -> twice^#(x)}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(O(1),O(1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  Weak DPs: {twice^#(s(x)) -> twice^#(x)}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(O(1),O(1))
                                
                                Proof:
                                  Empty rules are trivially bounded
                        
                        * Path 8:{2}: subsumed
                          --------------------
                          
                          This path is subsumed by the proof of paths 8:{2}->10:{11},
                                                                      8:{2}->9:{10}.
                        
                        * Path 8:{2}->9:{10}: YES(O(1),O(1))
                          ----------------------------------
                          
                          We consider the following Problem:
                          
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak DPs: {min^#(s(x), s(y)) -> min^#(x, y)}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(O(1),O(1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak DPs: {min^#(s(x), s(y)) -> min^#(x, y)}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(O(1),O(1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak DPs: {min^#(s(x), s(y)) -> min^#(x, y)}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(O(1),O(1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  Weak DPs: {min^#(s(x), s(y)) -> min^#(x, y)}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(O(1),O(1))
                                
                                Proof:
                                  Empty rules are trivially bounded
                        
                        * Path 8:{2}->10:{11}: YES(O(1),O(1))
                          -----------------------------------
                          
                          We consider the following Problem:
                          
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak DPs: {min^#(s(x), s(y)) -> min^#(x, y)}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(O(1),O(1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak DPs: {min^#(s(x), s(y)) -> min^#(x, y)}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(O(1),O(1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak DPs: {min^#(s(x), s(y)) -> min^#(x, y)}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(O(1),O(1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  Weak DPs: {min^#(s(x), s(y)) -> min^#(x, y)}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(O(1),O(1))
                                
                                Proof:
                                  Empty rules are trivially bounded
                        
                        * Path 7:{3}: YES(O(1),O(1))
                          --------------------------
                          
                          We consider the following Problem:
                          
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(O(1),O(1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(O(1),O(1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(O(1),O(1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(O(1),O(1))
                                
                                Proof:
                                  Empty rules are trivially bounded
                        
                        * Path 6:{4}: YES(O(1),O(1))
                          --------------------------
                          
                          We consider the following Problem:
                          
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(O(1),O(1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(O(1),O(1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(O(1),O(1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(O(1),O(1))
                                
                                Proof:
                                  Empty rules are trivially bounded
                        
                        * Path 3:{6}: subsumed
                          --------------------
                          
                          This path is subsumed by the proof of paths 3:{6}->5:{5},
                                                                      3:{6}->4:{9}.
                        
                        * Path 3:{6}->5:{5}: YES(O(1),O(1))
                          ---------------------------------
                          
                          We consider the following Problem:
                          
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak DPs: {max^#(s(x), s(y)) -> max^#(x, y)}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(O(1),O(1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak DPs: {max^#(s(x), s(y)) -> max^#(x, y)}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(O(1),O(1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak DPs: {max^#(s(x), s(y)) -> max^#(x, y)}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(O(1),O(1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  Weak DPs: {max^#(s(x), s(y)) -> max^#(x, y)}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(O(1),O(1))
                                
                                Proof:
                                  Empty rules are trivially bounded
                        
                        * Path 3:{6}->4:{9}: YES(O(1),O(1))
                          ---------------------------------
                          
                          We consider the following Problem:
                          
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak DPs: {max^#(s(x), s(y)) -> max^#(x, y)}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(O(1),O(1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak DPs: {max^#(s(x), s(y)) -> max^#(x, y)}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(O(1),O(1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak DPs: {max^#(s(x), s(y)) -> max^#(x, y)}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(O(1),O(1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  Weak DPs: {max^#(s(x), s(y)) -> max^#(x, y)}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(O(1),O(1))
                                
                                Proof:
                                  Empty rules are trivially bounded
                        
                        * Path 1:{8}: subsumed
                          --------------------
                          
                          This path is subsumed by the proof of paths 1:{8}->2:{7}.
                        
                        * Path 1:{8}->2:{7}: YES(O(1),O(1))
                          ---------------------------------
                          
                          We consider the following Problem:
                          
                            Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                            Weak DPs: {-^#(s(x), s(y)) -> -^#(x, y)}
                            Weak Trs:
                              {  min(s(x), s(y)) -> s(min(x, y))
                               , p(s(x)) -> x
                               , max(0(), y) -> y
                               , max(s(x), s(y)) -> s(max(x, y))
                               , -(x, 0()) -> x
                               , -(s(x), s(y)) -> -(x, y)
                               , max(x, 0()) -> x
                               , min(0(), y) -> 0()
                               , min(x, 0()) -> 0()
                               , twice(0()) -> 0()}
                            StartTerms: basic terms
                            Strategy: innermost
                          
                          Certificate: YES(O(1),O(1))
                          
                          Proof:
                            We consider the following Problem:
                            
                              Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                              Weak DPs: {-^#(s(x), s(y)) -> -^#(x, y)}
                              Weak Trs:
                                {  min(s(x), s(y)) -> s(min(x, y))
                                 , p(s(x)) -> x
                                 , max(0(), y) -> y
                                 , max(s(x), s(y)) -> s(max(x, y))
                                 , -(x, 0()) -> x
                                 , -(s(x), s(y)) -> -(x, y)
                                 , max(x, 0()) -> x
                                 , min(0(), y) -> 0()
                                 , min(x, 0()) -> 0()
                                 , twice(0()) -> 0()}
                              StartTerms: basic terms
                              Strategy: innermost
                            
                            Certificate: YES(O(1),O(1))
                            
                            Proof:
                              We consider the following Problem:
                              
                                Strict Trs: {twice(s(x)) -> s(s(twice(x)))}
                                Weak DPs: {-^#(s(x), s(y)) -> -^#(x, y)}
                                Weak Trs:
                                  {  min(s(x), s(y)) -> s(min(x, y))
                                   , p(s(x)) -> x
                                   , max(0(), y) -> y
                                   , max(s(x), s(y)) -> s(max(x, y))
                                   , -(x, 0()) -> x
                                   , -(s(x), s(y)) -> -(x, y)
                                   , max(x, 0()) -> x
                                   , min(0(), y) -> 0()
                                   , min(x, 0()) -> 0()
                                   , twice(0()) -> 0()}
                                StartTerms: basic terms
                                Strategy: innermost
                              
                              Certificate: YES(O(1),O(1))
                              
                              Proof:
                                No rule is usable.
                                
                                We consider the following Problem:
                                
                                  Weak DPs: {-^#(s(x), s(y)) -> -^#(x, y)}
                                  StartTerms: basic terms
                                  Strategy: innermost
                                
                                Certificate: YES(O(1),O(1))
                                
                                Proof:
                                  Empty rules are trivially bounded

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