MAYBE
Time: 0.087243
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:
  DP:
   {  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}
  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()}
  UR:
   { 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 -> 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# 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)
     (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)
     (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)}
    STATUS:
     arrows: 0.720000
     SCCS (4):
      Scc:
       {top# free x -> top# check new x}
      Scc:
       { check# new x -> check# x,
        check# free x -> check# x,
         check# old x -> check# x}
      Scc:
       {old# free x -> old# x}
      Scc:
       {new# free x -> new# x}
      
      SCC (1):
       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
      
      
      SCC (3):
       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()}
       POLY:
        Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
        Interpretation:
         [top](x0) = 0,
         
         [check](x0) = 0,
         
         [new](x0) = x0,
         
         [free](x0) = x0,
         
         [old](x0) = x0 + 1,
         
         [serve] = 1,
         
         [check#](x0) = x0
        Strict:
         check# old x -> check# x
         1 + 1x >= 0 + 1x
         check# free x -> check# x
         0 + 1x >= 0 + 1x
         check# new x -> check# x
         0 + 1x >= 0 + 1x
        Weak:
         old serve() -> free serve()
         2 >= 1
         old free x -> free old x
         1 + 1x >= 1 + 1x
         new serve() -> free serve()
         1 >= 1
         new free x -> free new x
         0 + 1x >= 0 + 1x
         check old x -> old check x
         0 + 0x >= 1 + 0x
         check old x -> old x
         0 + 0x >= 1 + 1x
         check free x -> free check x
         0 + 0x >= 0 + 0x
         check new x -> new check x
         0 + 0x >= 0 + 0x
         top free x -> top check new x
         0 + 0x >= 0 + 0x
       SCCS (1):
        Scc:
         { check# new x -> check# x,
          check# free x -> check# x}
        
        SCC (2):
         Strict:
          { check# new x -> check# x,
           check# free 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()}
         POLY:
          Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
          Interpretation:
           [top](x0) = x0,
           
           [check](x0) = x0 + 1,
           
           [new](x0) = x0 + 1,
           
           [free](x0) = x0,
           
           [old](x0) = 1,
           
           [serve] = 1,
           
           [check#](x0) = x0
          Strict:
           check# free x -> check# x
           0 + 1x >= 0 + 1x
           check# new x -> check# x
           1 + 1x >= 0 + 1x
          Weak:
           old serve() -> free serve()
           1 >= 1
           old free x -> free old x
           1 + 0x >= 1 + 0x
           new serve() -> free serve()
           2 >= 1
           new free x -> free new x
           1 + 1x >= 1 + 1x
           check old x -> old check x
           2 + 0x >= 1 + 0x
           check old x -> old x
           2 + 0x >= 1 + 0x
           check free x -> free check x
           1 + 1x >= 1 + 1x
           check new x -> new check x
           2 + 1x >= 2 + 1x
           top free x -> top check new x
           0 + 1x >= 2 + 1x
         SCCS (1):
          Scc:
           {check# free x -> check# x}
          
          SCC (1):
           Strict:
            {check# free 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()}
           POLY:
            Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
            Interpretation:
             [top](x0) = x0 + 1,
             
             [check](x0) = x0 + 1,
             
             [new](x0) = 1,
             
             [free](x0) = x0 + 1,
             
             [old](x0) = 0,
             
             [serve] = 1,
             
             [check#](x0) = x0
            Strict:
             check# free x -> check# x
             1 + 1x >= 0 + 1x
            Weak:
             old serve() -> free serve()
             0 >= 2
             old free x -> free old x
             0 + 0x >= 1 + 0x
             new serve() -> free serve()
             1 >= 2
             new free x -> free new x
             1 + 0x >= 2 + 0x
             check old x -> old check x
             1 + 0x >= 0 + 0x
             check old x -> old x
             1 + 0x >= 0 + 0x
             check free x -> free check x
             2 + 1x >= 2 + 1x
             check new x -> new check x
             2 + 0x >= 1 + 0x
             top free x -> top check new x
             2 + 1x >= 3 + 0x
           Qed
    
    SCC (1):
     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()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [top](x0) = x0 + 1,
       
       [check](x0) = x0 + 1,
       
       [new](x0) = 1,
       
       [free](x0) = x0 + 1,
       
       [old](x0) = 0,
       
       [serve] = 1,
       
       [old#](x0) = x0
      Strict:
       old# free x -> old# x
       1 + 1x >= 0 + 1x
      Weak:
       old serve() -> free serve()
       0 >= 2
       old free x -> free old x
       0 + 0x >= 1 + 0x
       new serve() -> free serve()
       1 >= 2
       new free x -> free new x
       1 + 0x >= 2 + 0x
       check old x -> old check x
       1 + 0x >= 0 + 0x
       check old x -> old x
       1 + 0x >= 0 + 0x
       check free x -> free check x
       2 + 1x >= 2 + 1x
       check new x -> new check x
       2 + 0x >= 1 + 0x
       top free x -> top check new x
       2 + 1x >= 3 + 0x
     Qed
    
    SCC (1):
     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()}
     POLY:
      Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true
      Interpretation:
       [top](x0) = x0 + 1,
       
       [check](x0) = x0 + 1,
       
       [new](x0) = 1,
       
       [free](x0) = x0 + 1,
       
       [old](x0) = 0,
       
       [serve] = 1,
       
       [new#](x0) = x0
      Strict:
       new# free x -> new# x
       1 + 1x >= 0 + 1x
      Weak:
       old serve() -> free serve()
       0 >= 2
       old free x -> free old x
       0 + 0x >= 1 + 0x
       new serve() -> free serve()
       1 >= 2
       new free x -> free new x
       1 + 0x >= 2 + 0x
       check old x -> old check x
       1 + 0x >= 0 + 0x
       check old x -> old x
       1 + 0x >= 0 + 0x
       check free x -> free check x
       2 + 1x >= 2 + 1x
       check new x -> new check x
       2 + 0x >= 1 + 0x
       top free x -> top check new x
       2 + 1x >= 3 + 0x
     Qed