MAYBE
TRS:
 {  top(free(x)) -> top(check(new(x))),
   check(new(x)) -> new(check(x)),
  check(free(x)) -> free(check(x)),
   check(old(x)) -> old(x),
   check(old(x)) -> old(check(x)),
    new(free(x)) -> free(new(x)),
    new(serve()) -> free(serve()),
    old(free(x)) -> free(old(x)),
    old(serve()) -> free(serve())}
 DP:
  Strict:
   {  top#(free(x)) -> top#(check(new(x))),
      top#(free(x)) -> check#(new(x)),
      top#(free(x)) -> new#(x),
     check#(new(x)) -> check#(x),
     check#(new(x)) -> new#(check(x)),
    check#(free(x)) -> check#(x),
     check#(old(x)) -> check#(x),
     check#(old(x)) -> old#(check(x)),
      new#(free(x)) -> new#(x),
      old#(free(x)) -> old#(x)}
  Weak:
  {  top(free(x)) -> top(check(new(x))),
    check(new(x)) -> new(check(x)),
   check(free(x)) -> free(check(x)),
    check(old(x)) -> old(x),
    check(old(x)) -> old(check(x)),
     new(free(x)) -> free(new(x)),
     new(serve()) -> free(serve()),
     old(free(x)) -> free(old(x)),
     old(serve()) -> free(serve())}
  EDG:
   {(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#(free(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#(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#(free(x)) -> check#(x))
    (check#(old(x)) -> check#(x), check#(new(x)) -> new#(check(x)))
    (check#(old(x)) -> check#(x), check#(new(x)) -> check#(x))
    (old#(free(x)) -> old#(x), old#(free(x)) -> old#(x))
    (check#(new(x)) -> new#(check(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))))
    (check#(old(x)) -> old#(check(x)), old#(free(x)) -> old#(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#(free(x)) -> 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)))
    (new#(free(x)) -> new#(x), new#(free(x)) -> new#(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#(free(x)) -> check#(x))
    (check#(free(x)) -> check#(x), check#(old(x)) -> check#(x))
    (check#(free(x)) -> check#(x), check#(old(x)) -> old#(check(x)))
    (top#(free(x)) -> new#(x), new#(free(x)) -> new#(x))}
   SCCS:
    Scc:
     {old#(free(x)) -> old#(x)}
    Scc:
     {new#(free(x)) -> new#(x)}
    Scc:
     { check#(new(x)) -> check#(x),
      check#(free(x)) -> check#(x),
       check#(old(x)) -> check#(x)}
    Scc:
     {top#(free(x)) -> top#(check(new(x)))}
    SCC:
     Strict:
      {old#(free(x)) -> old#(x)}
     Weak:
     {  top(free(x)) -> top(check(new(x))),
       check(new(x)) -> new(check(x)),
      check(free(x)) -> free(check(x)),
       check(old(x)) -> old(x),
       check(old(x)) -> old(check(x)),
        new(free(x)) -> free(new(x)),
        new(serve()) -> free(serve()),
        old(free(x)) -> free(old(x)),
        old(serve()) -> free(serve())}
     SPSC:
      Simple Projection:
       pi(old#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      {new#(free(x)) -> new#(x)}
     Weak:
     {  top(free(x)) -> top(check(new(x))),
       check(new(x)) -> new(check(x)),
      check(free(x)) -> free(check(x)),
       check(old(x)) -> old(x),
       check(old(x)) -> old(check(x)),
        new(free(x)) -> free(new(x)),
        new(serve()) -> free(serve()),
        old(free(x)) -> free(old(x)),
        old(serve()) -> free(serve())}
     SPSC:
      Simple Projection:
       pi(new#) = 0
      Strict:
       {}
      Qed
    SCC:
     Strict:
      { check#(new(x)) -> check#(x),
       check#(free(x)) -> check#(x),
        check#(old(x)) -> check#(x)}
     Weak:
     {  top(free(x)) -> top(check(new(x))),
       check(new(x)) -> new(check(x)),
      check(free(x)) -> free(check(x)),
       check(old(x)) -> old(x),
       check(old(x)) -> old(check(x)),
        new(free(x)) -> free(new(x)),
        new(serve()) -> free(serve()),
        old(free(x)) -> free(old(x)),
        old(serve()) -> free(serve())}
     SPSC:
      Simple Projection:
       pi(check#) = 0
      Strict:
       {check#(new(x)) -> check#(x),
        check#(old(x)) -> check#(x)}
      EDG:
       {(check#(old(x)) -> check#(x), check#(old(x)) -> check#(x))
        (check#(old(x)) -> check#(x), check#(new(x)) -> check#(x))
        (check#(new(x)) -> check#(x), check#(new(x)) -> check#(x))
        (check#(new(x)) -> check#(x), check#(old(x)) -> check#(x))}
       SCCS:
        Scc:
         {check#(new(x)) -> check#(x),
          check#(old(x)) -> check#(x)}
        SCC:
         Strict:
          {check#(new(x)) -> check#(x),
           check#(old(x)) -> check#(x)}
         Weak:
         {  top(free(x)) -> top(check(new(x))),
           check(new(x)) -> new(check(x)),
          check(free(x)) -> free(check(x)),
           check(old(x)) -> old(x),
           check(old(x)) -> old(check(x)),
            new(free(x)) -> free(new(x)),
            new(serve()) -> free(serve()),
            old(free(x)) -> free(old(x)),
            old(serve()) -> free(serve())}
         SPSC:
          Simple Projection:
           pi(check#) = 0
          Strict:
           {check#(old(x)) -> check#(x)}
          EDG:
           {(check#(old(x)) -> check#(x), check#(old(x)) -> check#(x))}
           SCCS:
            Scc:
             {check#(old(x)) -> check#(x)}
            SCC:
             Strict:
              {check#(old(x)) -> check#(x)}
             Weak:
             {  top(free(x)) -> top(check(new(x))),
               check(new(x)) -> new(check(x)),
              check(free(x)) -> free(check(x)),
               check(old(x)) -> old(x),
               check(old(x)) -> old(check(x)),
                new(free(x)) -> free(new(x)),
                new(serve()) -> free(serve()),
                old(free(x)) -> free(old(x)),
                old(serve()) -> free(serve())}
             SPSC:
              Simple Projection:
               pi(check#) = 0
              Strict:
               {}
              Qed
    SCC:
     Strict:
      {top#(free(x)) -> top#(check(new(x)))}
     Weak:
     {  top(free(x)) -> top(check(new(x))),
       check(new(x)) -> new(check(x)),
      check(free(x)) -> free(check(x)),
       check(old(x)) -> old(x),
       check(old(x)) -> old(check(x)),
        new(free(x)) -> free(new(x)),
        new(serve()) -> free(serve()),
        old(free(x)) -> free(old(x)),
        old(serve()) -> free(serve())}
     Fail