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:
 Matrix Interpretation Processor: dim=1
  
  interpretation:
   [serve] = 1,
   
   [old](x0) = 4x0 + 1,
   
   [top2](x0, x1) = 4x0 + 4x1,
   
   [check](x0) = x0,
   
   [new](x0) = x0 + 4,
   
   [top1](x0, x1) = 4x0 + 4x1,
   
   [free](x0) = x0 + 4
  orientation:
   top1(free(x),y) = 4x + 4y + 16 >= 4x + 4y + 16 = top2(check(new(x)),y)
   
   top1(free(x),y) = 4x + 4y + 16 >= 4x + 4y + 16 = top2(new(x),check(y))
   
   top1(free(x),y) = 4x + 4y + 16 >= 4x + 4y + 16 = top2(check(x),new(y))
   
   top1(free(x),y) = 4x + 4y + 16 >= 4x + 4y + 16 = top2(x,check(new(y)))
   
   top2(x,free(y)) = 4x + 4y + 16 >= 4x + 4y + 16 = top1(check(new(x)),y)
   
   top2(x,free(y)) = 4x + 4y + 16 >= 4x + 4y + 16 = top1(new(x),check(y))
   
   top2(x,free(y)) = 4x + 4y + 16 >= 4x + 4y + 16 = top1(check(x),new(y))
   
   top2(x,free(y)) = 4x + 4y + 16 >= 4x + 4y + 16 = top1(x,check(new(y)))
   
   new(free(x)) = x + 8 >= x + 8 = free(new(x))
   
   old(free(x)) = 4x + 17 >= 4x + 5 = free(old(x))
   
   new(serve()) = 5 >= 5 = free(serve())
   
   old(serve()) = 5 >= 5 = free(serve())
   
   check(free(x)) = x + 4 >= x + 4 = free(check(x))
   
   check(new(x)) = x + 4 >= x + 4 = new(check(x))
   
   check(old(x)) = 4x + 1 >= 4x + 1 = old(check(x))
   
   check(old(x)) = 4x + 1 >= 4x + 1 = old(x)
  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))
   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)
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [serve] = 0,
    
    [old](x0) = x0 + 5,
    
    [top2](x0, x1) = 2x0 + 2x1 + 5,
    
    [check](x0) = x0,
    
    [new](x0) = x0 + 1,
    
    [top1](x0, x1) = 2x0 + 2x1 + 5,
    
    [free](x0) = x0 + 1
   orientation:
    top1(free(x),y) = 2x + 2y + 7 >= 2x + 2y + 7 = top2(check(new(x)),y)
    
    top1(free(x),y) = 2x + 2y + 7 >= 2x + 2y + 7 = top2(new(x),check(y))
    
    top1(free(x),y) = 2x + 2y + 7 >= 2x + 2y + 7 = top2(check(x),new(y))
    
    top1(free(x),y) = 2x + 2y + 7 >= 2x + 2y + 7 = top2(x,check(new(y)))
    
    top2(x,free(y)) = 2x + 2y + 7 >= 2x + 2y + 7 = top1(check(new(x)),y)
    
    top2(x,free(y)) = 2x + 2y + 7 >= 2x + 2y + 7 = top1(new(x),check(y))
    
    top2(x,free(y)) = 2x + 2y + 7 >= 2x + 2y + 7 = top1(check(x),new(y))
    
    top2(x,free(y)) = 2x + 2y + 7 >= 2x + 2y + 7 = top1(x,check(new(y)))
    
    new(free(x)) = x + 2 >= x + 2 = free(new(x))
    
    new(serve()) = 1 >= 1 = free(serve())
    
    old(serve()) = 5 >= 1 = 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 + 5 >= x + 5 = old(check(x))
    
    check(old(x)) = x + 5 >= x + 5 = old(x)
   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))
    new(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)
   Matrix Interpretation Processor: dim=1
    
    interpretation:
     [serve] = 0,
     
     [old](x0) = 2x0 + 4,
     
     [top2](x0, x1) = 2x0 + 2x1,
     
     [check](x0) = 2x0,
     
     [new](x0) = x0,
     
     [top1](x0, x1) = x0 + 4x1,
     
     [free](x0) = 4x0
    orientation:
     top1(free(x),y) = 4x + 4y >= 4x + 2y = top2(check(new(x)),y)
     
     top1(free(x),y) = 4x + 4y >= 2x + 4y = top2(new(x),check(y))
     
     top1(free(x),y) = 4x + 4y >= 4x + 2y = top2(check(x),new(y))
     
     top1(free(x),y) = 4x + 4y >= 2x + 4y = top2(x,check(new(y)))
     
     top2(x,free(y)) = 2x + 8y >= 2x + 4y = top1(check(new(x)),y)
     
     top2(x,free(y)) = 2x + 8y >= x + 8y = top1(new(x),check(y))
     
     top2(x,free(y)) = 2x + 8y >= 2x + 4y = top1(check(x),new(y))
     
     top2(x,free(y)) = 2x + 8y >= x + 8y = top1(x,check(new(y)))
     
     new(free(x)) = 4x >= 4x = free(new(x))
     
     new(serve()) = 0 >= 0 = free(serve())
     
     check(free(x)) = 8x >= 8x = free(check(x))
     
     check(new(x)) = 2x >= 2x = new(check(x))
     
     check(old(x)) = 4x + 8 >= 4x + 4 = old(check(x))
     
     check(old(x)) = 4x + 8 >= 2x + 4 = old(x)
    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))
     new(serve()) -> free(serve())
     check(free(x)) -> free(check(x))
     check(new(x)) -> new(check(x))
    DP Processor:
     DPs:
      top1#(free(x),y) -> new#(x)
      top1#(free(x),y) -> check#(new(x))
      top1#(free(x),y) -> top2#(check(new(x)),y)
      top1#(free(x),y) -> check#(y)
      top1#(free(x),y) -> top2#(new(x),check(y))
      top1#(free(x),y) -> new#(y)
      top1#(free(x),y) -> check#(x)
      top1#(free(x),y) -> top2#(check(x),new(y))
      top1#(free(x),y) -> check#(new(y))
      top1#(free(x),y) -> top2#(x,check(new(y)))
      top2#(x,free(y)) -> new#(x)
      top2#(x,free(y)) -> check#(new(x))
      top2#(x,free(y)) -> top1#(check(new(x)),y)
      top2#(x,free(y)) -> check#(y)
      top2#(x,free(y)) -> top1#(new(x),check(y))
      top2#(x,free(y)) -> new#(y)
      top2#(x,free(y)) -> check#(x)
      top2#(x,free(y)) -> top1#(check(x),new(y))
      top2#(x,free(y)) -> check#(new(y))
      top2#(x,free(y)) -> top1#(x,check(new(y)))
      new#(free(x)) -> new#(x)
      check#(free(x)) -> check#(x)
      check#(new(x)) -> check#(x)
      check#(new(x)) -> new#(check(x))
     TRS:
      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))
      new(serve()) -> free(serve())
      check(free(x)) -> free(check(x))
      check(new(x)) -> new(check(x))
     TDG Processor:
      DPs:
       top1#(free(x),y) -> new#(x)
       top1#(free(x),y) -> check#(new(x))
       top1#(free(x),y) -> top2#(check(new(x)),y)
       top1#(free(x),y) -> check#(y)
       top1#(free(x),y) -> top2#(new(x),check(y))
       top1#(free(x),y) -> new#(y)
       top1#(free(x),y) -> check#(x)
       top1#(free(x),y) -> top2#(check(x),new(y))
       top1#(free(x),y) -> check#(new(y))
       top1#(free(x),y) -> top2#(x,check(new(y)))
       top2#(x,free(y)) -> new#(x)
       top2#(x,free(y)) -> check#(new(x))
       top2#(x,free(y)) -> top1#(check(new(x)),y)
       top2#(x,free(y)) -> check#(y)
       top2#(x,free(y)) -> top1#(new(x),check(y))
       top2#(x,free(y)) -> new#(y)
       top2#(x,free(y)) -> check#(x)
       top2#(x,free(y)) -> top1#(check(x),new(y))
       top2#(x,free(y)) -> check#(new(y))
       top2#(x,free(y)) -> top1#(x,check(new(y)))
       new#(free(x)) -> new#(x)
       check#(free(x)) -> check#(x)
       check#(new(x)) -> check#(x)
       check#(new(x)) -> new#(check(x))
      TRS:
       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))
       new(serve()) -> free(serve())
       check(free(x)) -> free(check(x))
       check(new(x)) -> new(check(x))
      graph:
       top2#(x,free(y)) -> check#(new(y)) ->
       check#(new(x)) -> new#(check(x))
       top2#(x,free(y)) -> check#(new(y)) ->
       check#(new(x)) -> check#(x)
       top2#(x,free(y)) -> check#(new(y)) ->
       check#(free(x)) -> check#(x)
       top2#(x,free(y)) -> check#(new(x)) ->
       check#(new(x)) -> new#(check(x))
       top2#(x,free(y)) -> check#(new(x)) ->
       check#(new(x)) -> check#(x)
       top2#(x,free(y)) -> check#(new(x)) ->
       check#(free(x)) -> check#(x)
       top2#(x,free(y)) -> check#(y) ->
       check#(new(x)) -> new#(check(x))
       top2#(x,free(y)) -> check#(y) -> check#(new(x)) -> check#(x)
       top2#(x,free(y)) -> check#(y) -> check#(free(x)) -> check#(x)
       top2#(x,free(y)) -> check#(x) ->
       check#(new(x)) -> new#(check(x))
       top2#(x,free(y)) -> check#(x) -> check#(new(x)) -> check#(x)
       top2#(x,free(y)) -> check#(x) -> check#(free(x)) -> check#(x)
       top2#(x,free(y)) -> new#(y) -> new#(free(x)) -> new#(x)
       top2#(x,free(y)) -> new#(x) ->
       new#(free(x)) -> new#(x)
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> top2#(x,check(new(y)))
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> check#(new(y))
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> top2#(check(x),new(y))
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> check#(x)
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> new#(y)
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> top2#(new(x),check(y))
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> check#(y)
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> top2#(check(new(x)),y)
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> check#(new(x))
       top2#(x,free(y)) -> top1#(check(new(x)),y) ->
       top1#(free(x),y) -> new#(x)
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> top2#(x,check(new(y)))
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> check#(new(y))
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> top2#(check(x),new(y))
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> check#(x)
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> new#(y)
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> top2#(new(x),check(y))
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> check#(y)
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> top2#(check(new(x)),y)
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> check#(new(x))
       top2#(x,free(y)) -> top1#(check(x),new(y)) ->
       top1#(free(x),y) -> new#(x)
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> top2#(x,check(new(y)))
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> check#(new(y))
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> top2#(check(x),new(y))
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> check#(x)
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> new#(y)
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> top2#(new(x),check(y))
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> check#(y)
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> top2#(check(new(x)),y)
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> check#(new(x))
       top2#(x,free(y)) -> top1#(new(x),check(y)) ->
       top1#(free(x),y) -> new#(x)
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> top2#(x,check(new(y)))
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> check#(new(y))
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> top2#(check(x),new(y))
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> check#(x)
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> new#(y)
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> top2#(new(x),check(y))
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> check#(y)
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> top2#(check(new(x)),y)
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> check#(new(x))
       top2#(x,free(y)) -> top1#(x,check(new(y))) ->
       top1#(free(x),y) -> new#(x)
       check#(new(x)) -> check#(x) -> check#(new(x)) -> new#(check(x))
       check#(new(x)) -> check#(x) -> check#(new(x)) -> check#(x)
       check#(new(x)) -> check#(x) -> check#(free(x)) -> check#(x)
       check#(new(x)) -> new#(check(x)) -> new#(free(x)) -> new#(x)
       check#(free(x)) -> check#(x) -> check#(new(x)) -> new#(check(x))
       check#(free(x)) -> check#(x) -> check#(new(x)) -> check#(x)
       check#(free(x)) -> check#(x) -> check#(free(x)) -> check#(x)
       new#(free(x)) -> new#(x) ->
       new#(free(x)) -> new#(x)
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> top1#(x,check(new(y)))
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> check#(new(y))
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> top1#(check(x),new(y))
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> check#(x)
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> new#(y)
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> top1#(new(x),check(y))
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> check#(y)
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> top1#(check(new(x)),y)
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> check#(new(x))
       top1#(free(x),y) -> top2#(check(new(x)),y) ->
       top2#(x,free(y)) -> new#(x)
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> top1#(x,check(new(y)))
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> check#(new(y))
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> top1#(check(x),new(y))
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> check#(x)
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> new#(y)
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> top1#(new(x),check(y))
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> check#(y)
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> top1#(check(new(x)),y)
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> check#(new(x))
       top1#(free(x),y) -> top2#(check(x),new(y)) ->
       top2#(x,free(y)) -> new#(x)
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> top1#(x,check(new(y)))
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> check#(new(y))
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> top1#(check(x),new(y))
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> check#(x)
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> new#(y)
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> top1#(new(x),check(y))
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> check#(y)
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> top1#(check(new(x)),y)
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> check#(new(x))
       top1#(free(x),y) -> top2#(new(x),check(y)) ->
       top2#(x,free(y)) -> new#(x)
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> top1#(x,check(new(y)))
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> check#(new(y))
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> top1#(check(x),new(y))
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> check#(x)
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> new#(y)
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> top1#(new(x),check(y))
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> check#(y)
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> top1#(check(new(x)),y)
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> check#(new(x))
       top1#(free(x),y) -> top2#(x,check(new(y))) ->
       top2#(x,free(y)) -> new#(x)
       top1#(free(x),y) -> check#(new(y)) ->
       check#(new(x)) -> new#(check(x))
       top1#(free(x),y) -> check#(new(y)) ->
       check#(new(x)) -> check#(x)
       top1#(free(x),y) -> check#(new(y)) ->
       check#(free(x)) -> check#(x)
       top1#(free(x),y) -> check#(new(x)) ->
       check#(new(x)) -> new#(check(x))
       top1#(free(x),y) -> check#(new(x)) ->
       check#(new(x)) -> check#(x)
       top1#(free(x),y) -> check#(new(x)) ->
       check#(free(x)) -> check#(x)
       top1#(free(x),y) -> check#(y) ->
       check#(new(x)) -> new#(check(x))
       top1#(free(x),y) -> check#(y) -> check#(new(x)) -> check#(x)
       top1#(free(x),y) -> check#(y) -> check#(free(x)) -> check#(x)
       top1#(free(x),y) -> check#(x) ->
       check#(new(x)) -> new#(check(x))
       top1#(free(x),y) -> check#(x) -> check#(new(x)) -> check#(x)
       top1#(free(x),y) -> check#(x) -> check#(free(x)) -> check#(x)
       top1#(free(x),y) -> new#(y) -> new#(free(x)) -> new#(x)
       top1#(free(x),y) -> new#(x) -> new#(free(x)) -> new#(x)
      SCC Processor:
       #sccs: 3
       #rules: 11
       #arcs: 116/576
       DPs:
        top2#(x,free(y)) -> top1#(check(new(x)),y)
        top1#(free(x),y) -> top2#(check(new(x)),y)
        top2#(x,free(y)) -> top1#(new(x),check(y))
        top1#(free(x),y) -> top2#(new(x),check(y))
        top2#(x,free(y)) -> top1#(check(x),new(y))
        top1#(free(x),y) -> top2#(check(x),new(y))
        top2#(x,free(y)) -> top1#(x,check(new(y)))
        top1#(free(x),y) -> top2#(x,check(new(y)))
       TRS:
        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))
        new(serve()) -> free(serve())
        check(free(x)) -> free(check(x))
        check(new(x)) -> new(check(x))
       Open
       
       DPs:
        check#(free(x)) -> check#(x)
        check#(new(x)) -> check#(x)
       TRS:
        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))
        new(serve()) -> free(serve())
        check(free(x)) -> free(check(x))
        check(new(x)) -> new(check(x))
       Subterm Criterion Processor:
        simple projection:
         pi(check#) = 0
        problem:
         DPs:
          
         TRS:
          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))
          new(serve()) -> free(serve())
          check(free(x)) -> free(check(x))
          check(new(x)) -> new(check(x))
        Qed
       
       DPs:
        new#(free(x)) -> new#(x)
       TRS:
        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))
        new(serve()) -> free(serve())
        check(free(x)) -> free(check(x))
        check(new(x)) -> new(check(x))
       Subterm Criterion Processor:
        simple projection:
         pi(new#) = 0
        problem:
         DPs:
          
         TRS:
          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))
          new(serve()) -> free(serve())
          check(free(x)) -> free(check(x))
          check(new(x)) -> new(check(x))
        Qed