MAYBE

Problem:
 top(free(x)) -> top(check(new(x)))
 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:
   top(free(x)) -> top(check(new(x)))
   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] = 0,
     
     [old](x0) = x0,
     
     [check](x0) = x0 + 1,
     
     [new](x0) = x0,
     
     [top](x0) = x0 + 1,
     
     [free](x0) = x0
    orientation:
     top(free(x)) = x + 1 >= x + 2 = top(check(new(x)))
     
     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 + 1 >= x + 1 = free(check(x))
     
     check(new(x)) = x + 1 >= x + 1 = new(check(x))
     
     check(old(x)) = x + 1 >= x + 1 = old(check(x))
     
     check(old(x)) = x + 1 >= x = old(x)
    problem:
     strict:
      top(free(x)) -> top(check(new(x)))
      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] = 1,
       
       [old](x0) = x0,
       
       [check](x0) = x0,
       
       [new](x0) = x0 + 1,
       
       [top](x0) = x0,
       
       [free](x0) = x0
      orientation:
       top(free(x)) = x >= x + 1 = top(check(new(x)))
       
       new(free(x)) = x + 1 >= x + 1 = free(new(x))
       
       old(free(x)) = x >= x = free(old(x))
       
       new(serve()) = 2 >= 1 = free(serve())
       
       old(serve()) = 1 >= 1 = free(serve())
       
       check(free(x)) = x >= x = free(check(x))
       
       check(new(x)) = x + 1 >= x + 1 = new(check(x))
       
       check(old(x)) = x >= x = old(check(x))
       
       check(old(x)) = x >= x = old(x)
      problem:
       strict:
        top(free(x)) -> top(check(new(x)))
        new(free(x)) -> free(new(x))
        old(free(x)) -> free(old(x))
        old(serve()) -> free(serve())
        check(free(x)) -> free(check(x))
        check(new(x)) -> new(check(x))
        check(old(x)) -> old(check(x))
       weak:
        new(serve()) -> free(serve())
        check(old(x)) -> old(x)
      Matrix Interpretation Processor:
       dimension: 1
       max_matrix:
        1
        interpretation:
         [serve] = 0,
         
         [old](x0) = x0 + 1,
         
         [check](x0) = x0,
         
         [new](x0) = x0,
         
         [top](x0) = x0 + 1,
         
         [free](x0) = x0
        orientation:
         top(free(x)) = x + 1 >= x + 1 = top(check(new(x)))
         
         new(free(x)) = x >= x = free(new(x))
         
         old(free(x)) = x + 1 >= x + 1 = free(old(x))
         
         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))
         
         new(serve()) = 0 >= 0 = free(serve())
         
         check(old(x)) = x + 1 >= x + 1 = old(x)
        problem:
         strict:
          top(free(x)) -> top(check(new(x)))
          new(free(x)) -> free(new(x))
          old(free(x)) -> free(old(x))
          check(free(x)) -> free(check(x))
          check(new(x)) -> new(check(x))
          check(old(x)) -> old(check(x))
         weak:
          old(serve()) -> free(serve())
          new(serve()) -> free(serve())
          check(old(x)) -> old(x)
        Matrix Interpretation Processor:
         dimension: 2
         max_matrix:
          [1 1]
          [0 1]
          interpretation:
                     [0]
           [serve] = [0],
           
                       [1 1]     [0]
           [old](x0) = [0 1]x0 + [1],
           
                           
           [check](x0) = x0,
           
                            [0]
           [new](x0) = x0 + [1],
           
                         
           [top](x0) = x0,
           
                             [0]
           [free](x0) = x0 + [1]
          orientation:
                              [0]        [0]                     
           top(free(x)) = x + [1] >= x + [1] = top(check(new(x)))
           
                              [0]        [0]               
           new(free(x)) = x + [2] >= x + [2] = free(new(x))
           
                          [1 1]    [1]    [1 1]    [0]               
           old(free(x)) = [0 1]x + [2] >= [0 1]x + [2] = free(old(x))
           
                                [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]    [0]    [1 1]    [0]                
           check(old(x)) = [0 1]x + [1] >= [0 1]x + [1] = old(check(x))
           
                          [0]    [0]                
           old(serve()) = [1] >= [1] = free(serve())
           
                          [0]    [0]                
           new(serve()) = [1] >= [1] = free(serve())
           
                           [1 1]    [0]    [1 1]    [0]         
           check(old(x)) = [0 1]x + [1] >= [0 1]x + [1] = old(x)
          problem:
           strict:
            top(free(x)) -> top(check(new(x)))
            new(free(x)) -> free(new(x))
            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())
            new(serve()) -> free(serve())
            check(old(x)) -> old(x)
          Matrix Interpretation Processor:
           dimension: 3
           max_matrix:
            [1 1 1]
            [0 1 1]
            [0 0 1]
            interpretation:
                       [0]
             [serve] = [0]
                       [0],
             
                         [1 0 1]     [0]
             [old](x0) = [0 1 0]x0 + [1]
                         [0 0 1]     [1],
             
                           [1 1 0]  
             [check](x0) = [0 1 0]x0
                           [0 0 1]  ,
             
                              [0]
             [new](x0) = x0 + [0]
                              [1],
             
                         [1 0 0]     [0]
             [top](x0) = [0 0 1]x0 + [1]
                         [0 0 0]     [0],
             
                          [1 1 0]     [0]
             [free](x0) = [0 1 0]x0 + [0]
                          [0 0 1]     [1]
            orientation:
                            [1 1 0]    [0]    [1 1 0]    [0]                     
             top(free(x)) = [0 0 1]x + [2] >= [0 0 1]x + [2] = top(check(new(x)))
                            [0 0 0]    [0]    [0 0 0]    [0]                     
             
                            [1 1 0]    [0]    [1 1 0]    [0]               
             new(free(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = free(new(x))
                            [0 0 1]    [2]    [0 0 1]    [2]               
             
                              [1 2 0]    [0]    [1 2 0]    [0]                 
             check(free(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = free(check(x))
                              [0 0 1]    [1]    [0 0 1]    [1]                 
             
                             [1 1 0]    [0]    [1 1 0]    [0]                
             check(new(x)) = [0 1 0]x + [0] >= [0 1 0]x + [0] = new(check(x))
                             [0 0 1]    [1]    [0 0 1]    [1]                
             
                             [1 1 1]    [1]    [1 1 1]    [0]                
             check(old(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = old(check(x))
                             [0 0 1]    [1]    [0 0 1]    [1]                
             
                            [1 1 1]    [1]    [1 1 1]    [1]               
             old(free(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = free(old(x))
                            [0 0 1]    [2]    [0 0 1]    [2]               
             
                            [0]    [0]                
             old(serve()) = [1] >= [0] = free(serve())
                            [1]    [1]                
             
                            [0]    [0]                
             new(serve()) = [0] >= [0] = free(serve())
                            [1]    [1]                
             
                             [1 1 1]    [1]    [1 0 1]    [0]         
             check(old(x)) = [0 1 0]x + [1] >= [0 1 0]x + [1] = old(x)
                             [0 0 1]    [1]    [0 0 1]    [1]         
            problem:
             strict:
              top(free(x)) -> top(check(new(x)))
              new(free(x)) -> free(new(x))
              check(free(x)) -> free(check(x))
              check(new(x)) -> new(check(x))
             weak:
              check(old(x)) -> old(check(x))
              old(free(x)) -> free(old(x))
              old(serve()) -> free(serve())
              new(serve()) -> free(serve())
              check(old(x)) -> old(x)
            Open