MAYBE

Problem:
 top1(free(x),y) -> top2(check(new(x)),y)
 top1(free(x),y) -> top2(new(x),check(y))
 top1(free(x),y) -> top2(check(x),new(y))
 top1(free(x),y) -> top2(x,check(new(y)))
 top2(x,free(y)) -> top1(check(new(x)),y)
 top2(x,free(y)) -> top1(new(x),check(y))
 top2(x,free(y)) -> top1(check(x),new(y))
 top2(x,free(y)) -> top1(x,check(new(y)))
 new(free(x)) -> free(new(x))
 old(free(x)) -> free(old(x))
 new(serve()) -> free(serve())
 old(serve()) -> free(serve())
 check(free(x)) -> free(check(x))
 check(new(x)) -> new(check(x))
 check(old(x)) -> old(check(x))
 check(old(x)) -> old(x)

Proof:
 Complexity Transformation Processor:
  strict:
   top1(free(x),y) -> top2(check(new(x)),y)
   top1(free(x),y) -> top2(new(x),check(y))
   top1(free(x),y) -> top2(check(x),new(y))
   top1(free(x),y) -> top2(x,check(new(y)))
   top2(x,free(y)) -> top1(check(new(x)),y)
   top2(x,free(y)) -> top1(new(x),check(y))
   top2(x,free(y)) -> top1(check(x),new(y))
   top2(x,free(y)) -> top1(x,check(new(y)))
   new(free(x)) -> free(new(x))
   old(free(x)) -> free(old(x))
   new(serve()) -> free(serve())
   old(serve()) -> free(serve())
   check(free(x)) -> free(check(x))
   check(new(x)) -> new(check(x))
   check(old(x)) -> old(check(x))
   check(old(x)) -> old(x)
  weak:
   
  Matrix Interpretation Processor:
   dimension: 1
   max_matrix:
    1
    interpretation:
     [serve] = 1,
     
     [old](x0) = x0 + 1,
     
     [top2](x0, x1) = x0 + x1,
     
     [check](x0) = x0 + 1,
     
     [new](x0) = x0,
     
     [top1](x0, x1) = x0 + x1,
     
     [free](x0) = x0 + 1
    orientation:
     top1(free(x),y) = x + y + 1 >= x + y + 1 = top2(check(new(x)),y)
     
     top1(free(x),y) = x + y + 1 >= x + y + 1 = top2(new(x),check(y))
     
     top1(free(x),y) = x + y + 1 >= x + y + 1 = top2(check(x),new(y))
     
     top1(free(x),y) = x + y + 1 >= x + y + 1 = top2(x,check(new(y)))
     
     top2(x,free(y)) = x + y + 1 >= x + y + 1 = top1(check(new(x)),y)
     
     top2(x,free(y)) = x + y + 1 >= x + y + 1 = top1(new(x),check(y))
     
     top2(x,free(y)) = x + y + 1 >= x + y + 1 = top1(check(x),new(y))
     
     top2(x,free(y)) = x + y + 1 >= x + y + 1 = top1(x,check(new(y)))
     
     new(free(x)) = x + 1 >= x + 1 = free(new(x))
     
     old(free(x)) = x + 2 >= x + 2 = free(old(x))
     
     new(serve()) = 1 >= 2 = free(serve())
     
     old(serve()) = 2 >= 2 = free(serve())
     
     check(free(x)) = x + 2 >= x + 2 = free(check(x))
     
     check(new(x)) = x + 1 >= x + 1 = new(check(x))
     
     check(old(x)) = x + 2 >= x + 2 = old(check(x))
     
     check(old(x)) = x + 2 >= x + 1 = old(x)
    problem:
     strict:
      top1(free(x),y) -> top2(check(new(x)),y)
      top1(free(x),y) -> top2(new(x),check(y))
      top1(free(x),y) -> top2(check(x),new(y))
      top1(free(x),y) -> top2(x,check(new(y)))
      top2(x,free(y)) -> top1(check(new(x)),y)
      top2(x,free(y)) -> top1(new(x),check(y))
      top2(x,free(y)) -> top1(check(x),new(y))
      top2(x,free(y)) -> top1(x,check(new(y)))
      new(free(x)) -> free(new(x))
      old(free(x)) -> free(old(x))
      new(serve()) -> free(serve())
      old(serve()) -> free(serve())
      check(free(x)) -> free(check(x))
      check(new(x)) -> new(check(x))
      check(old(x)) -> old(check(x))
     weak:
      check(old(x)) -> old(x)
    Matrix Interpretation Processor:
     dimension: 1
     max_matrix:
      1
      interpretation:
       [serve] = 0,
       
       [old](x0) = x0,
       
       [top2](x0, x1) = x0 + x1 + 1,
       
       [check](x0) = x0,
       
       [new](x0) = x0,
       
       [top1](x0, x1) = x0 + x1,
       
       [free](x0) = x0
      orientation:
       top1(free(x),y) = x + y >= x + y + 1 = top2(check(new(x)),y)
       
       top1(free(x),y) = x + y >= x + y + 1 = top2(new(x),check(y))
       
       top1(free(x),y) = x + y >= x + y + 1 = top2(check(x),new(y))
       
       top1(free(x),y) = x + y >= x + y + 1 = top2(x,check(new(y)))
       
       top2(x,free(y)) = x + y + 1 >= x + y = top1(check(new(x)),y)
       
       top2(x,free(y)) = x + y + 1 >= x + y = top1(new(x),check(y))
       
       top2(x,free(y)) = x + y + 1 >= x + y = top1(check(x),new(y))
       
       top2(x,free(y)) = x + y + 1 >= x + y = top1(x,check(new(y)))
       
       new(free(x)) = x >= x = free(new(x))
       
       old(free(x)) = x >= x = free(old(x))
       
       new(serve()) = 0 >= 0 = free(serve())
       
       old(serve()) = 0 >= 0 = free(serve())
       
       check(free(x)) = x >= x = free(check(x))
       
       check(new(x)) = x >= x = new(check(x))
       
       check(old(x)) = x >= x = old(check(x))
       
       check(old(x)) = x >= x = old(x)
      problem:
       strict:
        top1(free(x),y) -> top2(check(new(x)),y)
        top1(free(x),y) -> top2(new(x),check(y))
        top1(free(x),y) -> top2(check(x),new(y))
        top1(free(x),y) -> top2(x,check(new(y)))
        new(free(x)) -> free(new(x))
        old(free(x)) -> free(old(x))
        new(serve()) -> free(serve())
        old(serve()) -> free(serve())
        check(free(x)) -> free(check(x))
        check(new(x)) -> new(check(x))
        check(old(x)) -> old(check(x))
       weak:
        top2(x,free(y)) -> top1(check(new(x)),y)
        top2(x,free(y)) -> top1(new(x),check(y))
        top2(x,free(y)) -> top1(check(x),new(y))
        top2(x,free(y)) -> top1(x,check(new(y)))
        check(old(x)) -> old(x)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [serve] = 1,
         
         [old](x0) = x0,
         
         [top2](x0, x1) = x0 + x1,
         
         [check](x0) = x0,
         
         [new](x0) = x0,
         
         [top1](x0, x1) = x0 + x1 + 1,
         
         [free](x0) = x0 + 1
        orientation:
         top1(free(x),y) = x + y + 2 >= x + y = top2(check(new(x)),y)
         
         top1(free(x),y) = x + y + 2 >= x + y = top2(new(x),check(y))
         
         top1(free(x),y) = x + y + 2 >= x + y = top2(check(x),new(y))
         
         top1(free(x),y) = x + y + 2 >= x + y = top2(x,check(new(y)))
         
         new(free(x)) = x + 1 >= x + 1 = free(new(x))
         
         old(free(x)) = x + 1 >= x + 1 = free(old(x))
         
         new(serve()) = 1 >= 2 = free(serve())
         
         old(serve()) = 1 >= 2 = free(serve())
         
         check(free(x)) = x + 1 >= x + 1 = free(check(x))
         
         check(new(x)) = x >= x = new(check(x))
         
         check(old(x)) = x >= x = old(check(x))
         
         top2(x,free(y)) = x + y + 1 >= x + y + 1 = top1(check(new(x)),y)
         
         top2(x,free(y)) = x + y + 1 >= x + y + 1 = top1(new(x),check(y))
         
         top2(x,free(y)) = x + y + 1 >= x + y + 1 = top1(check(x),new(y))
         
         top2(x,free(y)) = x + y + 1 >= x + y + 1 = top1(x,check(new(y)))
         
         check(old(x)) = x >= x = old(x)
        problem:
         strict:
          new(free(x)) -> free(new(x))
          old(free(x)) -> free(old(x))
          new(serve()) -> free(serve())
          old(serve()) -> free(serve())
          check(free(x)) -> free(check(x))
          check(new(x)) -> new(check(x))
          check(old(x)) -> old(check(x))
         weak:
          top1(free(x),y) -> top2(check(new(x)),y)
          top1(free(x),y) -> top2(new(x),check(y))
          top1(free(x),y) -> top2(check(x),new(y))
          top1(free(x),y) -> top2(x,check(new(y)))
          top2(x,free(y)) -> top1(check(new(x)),y)
          top2(x,free(y)) -> top1(new(x),check(y))
          top2(x,free(y)) -> top1(check(x),new(y))
          top2(x,free(y)) -> top1(x,check(new(y)))
          check(old(x)) -> old(x)
        Matrix Interpretation Processor:
         dimension: 1
         max_matrix:
          1
          interpretation:
           [serve] = 0,
           
           [old](x0) = x0 + 1,
           
           [top2](x0, x1) = x0 + x1,
           
           [check](x0) = x0,
           
           [new](x0) = x0,
           
           [top1](x0, x1) = x0 + x1,
           
           [free](x0) = x0
          orientation:
           new(free(x)) = x >= x = free(new(x))
           
           old(free(x)) = x + 1 >= x + 1 = free(old(x))
           
           new(serve()) = 0 >= 0 = free(serve())
           
           old(serve()) = 1 >= 0 = free(serve())
           
           check(free(x)) = x >= x = free(check(x))
           
           check(new(x)) = x >= x = new(check(x))
           
           check(old(x)) = x + 1 >= x + 1 = old(check(x))
           
           top1(free(x),y) = x + y >= x + y = top2(check(new(x)),y)
           
           top1(free(x),y) = x + y >= x + y = top2(new(x),check(y))
           
           top1(free(x),y) = x + y >= x + y = top2(check(x),new(y))
           
           top1(free(x),y) = x + y >= x + y = top2(x,check(new(y)))
           
           top2(x,free(y)) = x + y >= x + y = top1(check(new(x)),y)
           
           top2(x,free(y)) = x + y >= x + y = top1(new(x),check(y))
           
           top2(x,free(y)) = x + y >= x + y = top1(check(x),new(y))
           
           top2(x,free(y)) = x + y >= x + y = top1(x,check(new(y)))
           
           check(old(x)) = x + 1 >= x + 1 = old(x)
          problem:
           strict:
            new(free(x)) -> free(new(x))
            old(free(x)) -> free(old(x))
            new(serve()) -> free(serve())
            check(free(x)) -> free(check(x))
            check(new(x)) -> new(check(x))
            check(old(x)) -> old(check(x))
           weak:
            old(serve()) -> free(serve())
            top1(free(x),y) -> top2(check(new(x)),y)
            top1(free(x),y) -> top2(new(x),check(y))
            top1(free(x),y) -> top2(check(x),new(y))
            top1(free(x),y) -> top2(x,check(new(y)))
            top2(x,free(y)) -> top1(check(new(x)),y)
            top2(x,free(y)) -> top1(new(x),check(y))
            top2(x,free(y)) -> top1(check(x),new(y))
            top2(x,free(y)) -> top1(x,check(new(y)))
            check(old(x)) -> old(x)
          Matrix Interpretation Processor:
           dimension: 2
           max_matrix:
            [1 1]
            [0 1]
            interpretation:
                       [0]
             [serve] = [0],
             
                         [1 1]     [1]
             [old](x0) = [0 1]x0 + [1],
             
                              [1 0]     [1 0]     [0]
             [top2](x0, x1) = [0 0]x0 + [0 0]x1 + [1],
             
                             
             [check](x0) = x0,
             
                              [0]
             [new](x0) = x0 + [1],
             
                              [1 0]     [1 0]     [0]
             [top1](x0, x1) = [0 0]x0 + [0 0]x1 + [1],
             
                               [0]
             [free](x0) = x0 + [1]
            orientation:
                                [0]        [0]               
             new(free(x)) = x + [2] >= x + [2] = free(new(x))
             
                            [1 1]    [2]    [1 1]    [1]               
             old(free(x)) = [0 1]x + [2] >= [0 1]x + [2] = free(old(x))
             
                            [0]    [0]                
             new(serve()) = [1] >= [1] = free(serve())
             
                                  [0]        [0]                 
             check(free(x)) = x + [1] >= x + [1] = free(check(x))
             
                                 [0]        [0]                
             check(new(x)) = x + [1] >= x + [1] = new(check(x))
             
                             [1 1]    [1]    [1 1]    [1]                
             check(old(x)) = [0 1]x + [1] >= [0 1]x + [1] = old(check(x))
             
                            [1]    [0]                
             old(serve()) = [1] >= [1] = free(serve())
             
                               [1 0]    [1 0]    [0]    [1 0]    [1 0]    [0]                        
             top1(free(x),y) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [1] = top2(check(new(x)),y)
             
                               [1 0]    [1 0]    [0]    [1 0]    [1 0]    [0]                        
             top1(free(x),y) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [1] = top2(new(x),check(y))
             
                               [1 0]    [1 0]    [0]    [1 0]    [1 0]    [0]                        
             top1(free(x),y) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [1] = top2(check(x),new(y))
             
                               [1 0]    [1 0]    [0]    [1 0]    [1 0]    [0]                        
             top1(free(x),y) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [1] = top2(x,check(new(y)))
             
                               [1 0]    [1 0]    [0]    [1 0]    [1 0]    [0]                        
             top2(x,free(y)) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [1] = top1(check(new(x)),y)
             
                               [1 0]    [1 0]    [0]    [1 0]    [1 0]    [0]                        
             top2(x,free(y)) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [1] = top1(new(x),check(y))
             
                               [1 0]    [1 0]    [0]    [1 0]    [1 0]    [0]                        
             top2(x,free(y)) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [1] = top1(check(x),new(y))
             
                               [1 0]    [1 0]    [0]    [1 0]    [1 0]    [0]                        
             top2(x,free(y)) = [0 0]x + [0 0]y + [1] >= [0 0]x + [0 0]y + [1] = top1(x,check(new(y)))
             
                             [1 1]    [1]    [1 1]    [1]         
             check(old(x)) = [0 1]x + [1] >= [0 1]x + [1] = old(x)
            problem:
             strict:
              new(free(x)) -> free(new(x))
              new(serve()) -> free(serve())
              check(free(x)) -> free(check(x))
              check(new(x)) -> new(check(x))
              check(old(x)) -> old(check(x))
             weak:
              old(free(x)) -> free(old(x))
              old(serve()) -> free(serve())
              top1(free(x),y) -> top2(check(new(x)),y)
              top1(free(x),y) -> top2(new(x),check(y))
              top1(free(x),y) -> top2(check(x),new(y))
              top1(free(x),y) -> top2(x,check(new(y)))
              top2(x,free(y)) -> top1(check(new(x)),y)
              top2(x,free(y)) -> top1(new(x),check(y))
              top2(x,free(y)) -> top1(check(x),new(y))
              top2(x,free(y)) -> top1(x,check(new(y)))
              check(old(x)) -> old(x)
            Open