MAYBE
Time: 0.173275
TRS:
 {top2(x, free y) -> top1(x, check new y),
  top2(x, free y) -> top1(check x, new y),
  top2(x, free y) -> top1(check new x, y),
  top2(x, free y) -> top1(new x, check y),
      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(),
  top1(free x, y) -> top2(x, check new y),
  top1(free x, y) -> top2(check x, new y),
  top1(free x, y) -> top2(check new x, y),
  top1(free x, y) -> top2(new x, check y),
       old free x -> free old x,
      old serve() -> free serve()}
 DP:
  DP:
   {top2#(x, free y) -> check# x,
    top2#(x, free y) -> check# y,
    top2#(x, free y) -> check# new x,
    top2#(x, free y) -> check# new y,
    top2#(x, free y) -> new# x,
    top2#(x, free y) -> new# y,
    top2#(x, free y) -> top1#(x, check new y),
    top2#(x, free y) -> top1#(check x, new y),
    top2#(x, free y) -> top1#(check new x, y),
    top2#(x, free y) -> top1#(new x, check y),
        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,
    top1#(free x, y) -> top2#(x, check new y),
    top1#(free x, y) -> top2#(check x, new y),
    top1#(free x, y) -> top2#(check new x, y),
    top1#(free x, y) -> top2#(new x, check y),
    top1#(free x, y) -> check# x,
    top1#(free x, y) -> check# y,
    top1#(free x, y) -> check# new x,
    top1#(free x, y) -> check# new y,
    top1#(free x, y) -> new# x,
    top1#(free x, y) -> new# y,
         old# free x -> old# x}
  TRS:
  {top2(x, free y) -> top1(x, check new y),
   top2(x, free y) -> top1(check x, new y),
   top2(x, free y) -> top1(check new x, y),
   top2(x, free y) -> top1(new x, check y),
       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(),
   top1(free x, y) -> top2(x, check new y),
   top1(free x, y) -> top2(check x, new y),
   top1(free x, y) -> top2(check new x, y),
   top1(free x, y) -> top2(new x, check y),
        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:
    {(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) -> top1#(check new x, 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) -> top1#(x, check new y))
     (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) -> new# x)
     (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) -> check# new x)
     (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) -> check# x)
     (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) -> top1#(check new x, 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) -> top1#(x, check new y))
     (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) -> new# x)
     (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) -> check# new x)
     (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) -> 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) -> new# x)
     (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) -> check# new x)
     (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) -> check# x)
     (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) -> top2#(check new x, 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) -> top2#(x, check 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) -> top1#(check new x, 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) -> top1#(x, check new y))
     (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) -> new# x)
     (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) -> check# new x)
     (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) -> check# x)
     (top2#(x, free y) -> new# 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# free x -> check# x)
     (check# free x -> check# x, check# new x -> new# check x)
     (check# free x -> check# x, check# new x -> check# x)
     (new# free x -> new# x, new# free x -> new# x)
     (top1#(free x, y) -> new# x, new# free x -> new# x)
     (top2#(x, free y) -> check# new y, check# old x -> old# check x)
     (top2#(x, free y) -> check# new y, check# old x -> check# x)
     (top2#(x, free y) -> check# new y, check# free x -> check# x)
     (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 x, check# old x -> old# check x)
     (top2#(x, free y) -> check# new x, check# old x -> check# x)
     (top2#(x, free y) -> check# new x, 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)
     (check# old x -> old# check x, old# free x -> old# x)
     (top2#(x, free y) -> check# y, check# old x -> old# check x)
     (top2#(x, free y) -> check# y, check# old x -> check# x)
     (top2#(x, free y) -> check# y, 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)
     (top1#(free x, y) -> check# y, check# old x -> old# check x)
     (top1#(free x, y) -> check# y, check# old x -> check# x)
     (top1#(free x, y) -> check# y, 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) -> new# y, new# free x -> new# x)
     (top2#(x, free y) -> new# y, new# free x -> new# x)
     (top1#(free x, y) -> check# new x, check# new x -> check# x)
     (top1#(free x, y) -> check# new x, check# new x -> new# check x)
     (top1#(free x, y) -> check# new x, check# free x -> check# x)
     (top1#(free x, y) -> check# new x, check# old x -> check# x)
     (top1#(free x, y) -> check# new x, check# old x -> old# check x)
     (check# new x -> new# check x, new# free x -> new# x)
     (top1#(free x, y) -> check# new y, check# new x -> check# x)
     (top1#(free x, y) -> check# new y, check# new x -> new# check x)
     (top1#(free x, y) -> check# new y, check# free x -> check# x)
     (top1#(free x, y) -> check# new y, check# old x -> check# x)
     (top1#(free x, y) -> check# new y, check# old x -> old# check x)
     (old# free x -> old# x, old# free x -> old# x)
     (top1#(free x, y) -> check# x, check# new x -> check# x)
     (top1#(free x, y) -> check# x, check# new x -> new# check x)
     (top1#(free x, y) -> check# x, check# free x -> check# x)
     (top1#(free x, y) -> check# x, check# old x -> check# x)
     (top1#(free x, y) -> check# x, check# old x -> old# 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# free x -> 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# new x -> check# x)
     (check# new x -> check# x, check# new x -> new# check x)
     (check# new x -> check# x, check# free x -> check# x)
     (check# new x -> check# x, check# old x -> check# x)
     (check# new x -> check# x, check# old x -> old# check x)
     (top2#(x, free y) -> check# x, check# new x -> check# x)
     (top2#(x, free y) -> check# x, check# new x -> new# check x)
     (top2#(x, free y) -> check# x, check# free x -> check# x)
     (top2#(x, free y) -> check# x, check# old x -> check# x)
     (top2#(x, free y) -> check# x, check# old x -> old# check x)
     (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) -> check# 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) -> check# new y)
     (top1#(free x, y) -> top2#(check x, new y), top2#(x, free y) -> new# 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#(x, 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) -> top1#(check new x, y))
     (top1#(free x, y) -> top2#(check x, new y), top2#(x, free y) -> top1#(new x, check y))
     (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) -> top2#(check x, new 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) -> top2#(new x, check 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) -> check# 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) -> check# new y)
     (top2#(x, free y) -> top1#(check x, new y), top1#(free x, y) -> new# x)
     (top2#(x, free y) -> top1#(check x, new y), top1#(free x, y) -> new# y)
     (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) -> top2#(check x, new 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) -> top2#(new x, check 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) -> check# 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) -> check# new y)
     (top2#(x, free y) -> top1#(x, check new y), top1#(free x, y) -> new# x)
     (top2#(x, free y) -> top1#(x, check new y), top1#(free x, y) -> new# y)
     (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) -> top2#(check x, new 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) -> top2#(new x, check 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) -> check# 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) -> check# new y)
     (top2#(x, free y) -> top1#(check new x, y), top1#(free x, y) -> new# x)
     (top2#(x, free y) -> top1#(check new x, y), top1#(free x, y) -> new# y)}
    STATUS:
     arrows: 0.803841
     SCCS (4):
      Scc:
       {top2#(x, free y) -> top1#(x, check new y),
        top2#(x, free y) -> top1#(check x, new y),
        top2#(x, free y) -> top1#(check new x, y),
        top2#(x, free y) -> top1#(new x, check y),
        top1#(free x, y) -> top2#(x, check new y),
        top1#(free x, y) -> top2#(check x, new y),
        top1#(free x, y) -> top2#(check new x, y),
        top1#(free x, y) -> top2#(new x, check y)}
      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 (8):
       Strict:
        {top2#(x, free y) -> top1#(x, check new y),
         top2#(x, free y) -> top1#(check x, new y),
         top2#(x, free y) -> top1#(check new x, y),
         top2#(x, free y) -> top1#(new x, check y),
         top1#(free x, y) -> top2#(x, check new y),
         top1#(free x, y) -> top2#(check x, new y),
         top1#(free x, y) -> top2#(check new x, y),
         top1#(free x, y) -> top2#(new x, check y)}
       Weak:
       {top2(x, free y) -> top1(x, check new y),
        top2(x, free y) -> top1(check x, new y),
        top2(x, free y) -> top1(check new x, y),
        top2(x, free y) -> top1(new x, check y),
            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(),
        top1(free x, y) -> top2(x, check new y),
        top1(free x, y) -> top2(check x, new y),
        top1(free x, y) -> top2(check new x, y),
        top1(free x, y) -> top2(new x, check y),
             old free x -> free old x,
            old serve() -> free serve()}
       Open
      
      
      
      
      
      
      
      
      
      
      
      
      SCC (3):
       Strict:
        { check# new x -> check# x,
         check# free x -> check# x,
          check# old x -> check# x}
       Weak:
       {top2(x, free y) -> top1(x, check new y),
        top2(x, free y) -> top1(check x, new y),
        top2(x, free y) -> top1(check new x, y),
        top2(x, free y) -> top1(new x, check y),
            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(),
        top1(free x, y) -> top2(x, check new y),
        top1(free x, y) -> top2(check x, new y),
        top1(free x, y) -> top2(check new x, y),
        top1(free x, y) -> top2(new x, check y),
             old free x -> free old x,
            old serve() -> free serve()}
       Open
      
      SCC (1):
       Strict:
        {old# free x -> old# x}
       Weak:
       {top2(x, free y) -> top1(x, check new y),
        top2(x, free y) -> top1(check x, new y),
        top2(x, free y) -> top1(check new x, y),
        top2(x, free y) -> top1(new x, check y),
            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(),
        top1(free x, y) -> top2(x, check new y),
        top1(free x, y) -> top2(check x, new y),
        top1(free x, y) -> top2(check new x, y),
        top1(free x, y) -> top2(new x, check y),
             old free x -> free old x,
            old serve() -> free serve()}
       Open
      
      SCC (1):
       Strict:
        {new# free x -> new# x}
       Weak:
       {top2(x, free y) -> top1(x, check new y),
        top2(x, free y) -> top1(check x, new y),
        top2(x, free y) -> top1(check new x, y),
        top2(x, free y) -> top1(new x, check y),
            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(),
        top1(free x, y) -> top2(x, check new y),
        top1(free x, y) -> top2(check x, new y),
        top1(free x, y) -> top2(check new x, y),
        top1(free x, y) -> top2(new x, check y),
             old free x -> free old x,
            old serve() -> free serve()}
       Open