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:
 DP Processor:
  DPs:
   top#(free(x)) -> new#(x)
   top#(free(x)) -> check#(new(x))
   top#(free(x)) -> top#(check(new(x)))
   new#(free(x)) -> new#(x)
   old#(free(x)) -> old#(x)
   check#(free(x)) -> check#(x)
   check#(new(x)) -> check#(x)
   check#(new(x)) -> new#(check(x))
   check#(old(x)) -> check#(x)
   check#(old(x)) -> old#(check(x))
  TRS:
   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)
  Usable Rule Processor:
   DPs:
    top#(free(x)) -> new#(x)
    top#(free(x)) -> check#(new(x))
    top#(free(x)) -> top#(check(new(x)))
    new#(free(x)) -> new#(x)
    old#(free(x)) -> old#(x)
    check#(free(x)) -> check#(x)
    check#(new(x)) -> check#(x)
    check#(new(x)) -> new#(check(x))
    check#(old(x)) -> check#(x)
    check#(old(x)) -> old#(check(x))
   TRS:
    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)
    old(free(x)) -> free(old(x))
    old(serve()) -> free(serve())
   ADG Processor:
    DPs:
     top#(free(x)) -> new#(x)
     top#(free(x)) -> check#(new(x))
     top#(free(x)) -> top#(check(new(x)))
     new#(free(x)) -> new#(x)
     old#(free(x)) -> old#(x)
     check#(free(x)) -> check#(x)
     check#(new(x)) -> check#(x)
     check#(new(x)) -> new#(check(x))
     check#(old(x)) -> check#(x)
     check#(old(x)) -> old#(check(x))
    TRS:
     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)
     old(free(x)) -> free(old(x))
     old(serve()) -> free(serve())
    graph:
     old#(free(x)) -> old#(x) -> old#(free(x)) -> old#(x)
     check#(old(x)) -> old#(check(x)) -> old#(free(x)) -> old#(x)
     check#(old(x)) -> check#(x) -> check#(free(x)) -> check#(x)
     check#(old(x)) -> check#(x) -> check#(new(x)) -> check#(x)
     check#(old(x)) -> check#(x) -> check#(new(x)) -> new#(check(x))
     check#(old(x)) -> check#(x) -> check#(old(x)) -> check#(x)
     check#(old(x)) -> check#(x) -> check#(old(x)) -> old#(check(x))
     check#(new(x)) -> check#(x) -> check#(free(x)) -> check#(x)
     check#(new(x)) -> check#(x) -> check#(new(x)) -> check#(x)
     check#(new(x)) -> check#(x) -> check#(new(x)) -> new#(check(x))
     check#(new(x)) -> check#(x) -> check#(old(x)) -> check#(x)
     check#(new(x)) -> check#(x) ->
     check#(old(x)) -> old#(check(x))
     check#(new(x)) -> new#(check(x)) -> new#(free(x)) -> new#(x)
     check#(free(x)) -> check#(x) -> check#(free(x)) -> check#(x)
     check#(free(x)) -> check#(x) -> check#(new(x)) -> check#(x)
     check#(free(x)) -> check#(x) -> check#(new(x)) -> new#(check(x))
     check#(free(x)) -> check#(x) -> check#(old(x)) -> check#(x)
     check#(free(x)) -> check#(x) -> check#(old(x)) -> old#(check(x))
     new#(free(x)) -> new#(x) -> new#(free(x)) -> new#(x)
     top#(free(x)) -> check#(new(x)) -> check#(free(x)) -> check#(x)
     top#(free(x)) -> check#(new(x)) -> check#(new(x)) -> check#(x)
     top#(free(x)) -> check#(new(x)) ->
     check#(new(x)) -> new#(check(x))
     top#(free(x)) -> check#(new(x)) -> check#(old(x)) -> check#(x)
     top#(free(x)) -> check#(new(x)) -> check#(old(x)) -> old#(check(x))
     top#(free(x)) -> new#(x) -> new#(free(x)) -> new#(x)
     top#(free(x)) -> top#(check(new(x))) ->
     top#(free(x)) -> new#(x)
     top#(free(x)) -> top#(check(new(x))) ->
     top#(free(x)) -> check#(new(x))
     top#(free(x)) -> top#(check(new(x))) -> top#(free(x)) -> top#(check(new(x)))
    Restore Modifier:
     DPs:
      top#(free(x)) -> new#(x)
      top#(free(x)) -> check#(new(x))
      top#(free(x)) -> top#(check(new(x)))
      new#(free(x)) -> new#(x)
      old#(free(x)) -> old#(x)
      check#(free(x)) -> check#(x)
      check#(new(x)) -> check#(x)
      check#(new(x)) -> new#(check(x))
      check#(old(x)) -> check#(x)
      check#(old(x)) -> old#(check(x))
     TRS:
      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)
     SCC Processor:
      #sccs: 4
      #rules: 6
      #arcs: 28/100
      DPs:
       top#(free(x)) -> top#(check(new(x)))
      TRS:
       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)
      Open
      
      DPs:
       check#(old(x)) -> check#(x)
       check#(new(x)) -> check#(x)
       check#(free(x)) -> check#(x)
      TRS:
       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)
      Open
      
      DPs:
       new#(free(x)) -> new#(x)
      TRS:
       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)
      Open
      
      DPs:
       old#(free(x)) -> old#(x)
      TRS:
       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)
      Open