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)
  TDG 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)
   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#(old(x)) -> old#(check(x))
    check#(old(x)) -> check#(x) -> check#(old(x)) -> check#(x)
    check#(old(x)) -> check#(x) -> check#(new(x)) -> new#(check(x))
    check#(old(x)) -> check#(x) -> check#(new(x)) -> check#(x)
    check#(old(x)) -> check#(x) -> check#(free(x)) -> check#(x)
    check#(new(x)) -> check#(x) -> check#(old(x)) -> old#(check(x))
    check#(new(x)) -> check#(x) -> check#(old(x)) -> check#(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#(old(x)) -> old#(check(x))
    check#(free(x)) -> check#(x) -> check#(old(x)) -> check#(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)
    top#(free(x)) -> check#(new(x)) ->
    check#(old(x)) -> old#(check(x))
    top#(free(x)) -> check#(new(x)) -> check#(old(x)) -> check#(x)
    top#(free(x)) -> check#(new(x)) ->
    check#(new(x)) -> new#(check(x))
    top#(free(x)) -> check#(new(x)) -> check#(new(x)) -> check#(x)
    top#(free(x)) -> check#(new(x)) -> check#(free(x)) -> check#(x)
    top#(free(x)) -> new#(x) -> new#(free(x)) -> new#(x)
    top#(free(x)) -> top#(check(new(x))) ->
    top#(free(x)) -> top#(check(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)) -> new#(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#(free(x)) -> check#(x)
     check#(new(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)
    Subterm Criterion Processor:
     simple projection:
      pi(check#) = 0
     problem:
      DPs:
       
      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)
     Qed
    
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(new#) = 0
     problem:
      DPs:
       
      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)
     Qed
    
    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)
    Subterm Criterion Processor:
     simple projection:
      pi(old#) = 0
     problem:
      DPs:
       
      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)
     Qed