MAYBE
Time: 0.008203
TRS:
 {      top sent x -> top check rest x,
      check rest x -> rest check x,
      check sent x -> sent check x,
  check cons(x, y) -> cons(x, y),
  check cons(x, y) -> cons(x, check y),
  check cons(x, y) -> cons(check x, y),
        rest nil() -> sent nil(),
   rest cons(x, y) -> sent y}
 DP:
  DP:
   {      top# sent x -> top# check rest x,
          top# sent x -> check# rest x,
          top# sent x -> rest# x,
        check# rest x -> check# x,
        check# rest x -> rest# check x,
        check# sent x -> check# x,
    check# cons(x, y) -> check# x,
    check# cons(x, y) -> check# y}
  TRS:
  {      top sent x -> top check rest x,
       check rest x -> rest check x,
       check sent x -> sent check x,
   check cons(x, y) -> cons(x, y),
   check cons(x, y) -> cons(x, check y),
   check cons(x, y) -> cons(check x, y),
         rest nil() -> sent nil(),
    rest cons(x, y) -> sent y}
  EDG:
   {(check# sent x -> check# x, check# cons(x, y) -> check# y)
    (check# sent x -> check# x, check# cons(x, y) -> check# x)
    (check# sent x -> check# x, check# sent x -> check# x)
    (check# sent x -> check# x, check# rest x -> rest# check x)
    (check# sent x -> check# x, check# rest x -> check# x)
    (top# sent x -> check# rest x, check# cons(x, y) -> check# y)
    (top# sent x -> check# rest x, check# cons(x, y) -> check# x)
    (top# sent x -> check# rest x, check# sent x -> check# x)
    (top# sent x -> check# rest x, check# rest x -> rest# check x)
    (top# sent x -> check# rest x, check# rest x -> check# x)
    (check# cons(x, y) -> check# y, check# cons(x, y) -> check# y)
    (check# cons(x, y) -> check# y, check# cons(x, y) -> check# x)
    (check# cons(x, y) -> check# y, check# sent x -> check# x)
    (check# cons(x, y) -> check# y, check# rest x -> rest# check x)
    (check# cons(x, y) -> check# y, check# rest x -> check# x)
    (check# cons(x, y) -> check# x, check# rest x -> check# x)
    (check# cons(x, y) -> check# x, check# rest x -> rest# check x)
    (check# cons(x, y) -> check# x, check# sent x -> check# x)
    (check# cons(x, y) -> check# x, check# cons(x, y) -> check# x)
    (check# cons(x, y) -> check# x, check# cons(x, y) -> check# y)
    (check# rest x -> check# x, check# rest x -> check# x)
    (check# rest x -> check# x, check# rest x -> rest# check x)
    (check# rest x -> check# x, check# sent x -> check# x)
    (check# rest x -> check# x, check# cons(x, y) -> check# x)
    (check# rest x -> check# x, check# cons(x, y) -> check# y)
    (top# sent x -> top# check rest x, top# sent x -> top# check rest x)
    (top# sent x -> top# check rest x, top# sent x -> check# rest x)
    (top# sent x -> top# check rest x, top# sent x -> rest# x)}
   SCCS (2):
    Scc:
     {    check# rest x -> check# x,
          check# sent x -> check# x,
      check# cons(x, y) -> check# x,
      check# cons(x, y) -> check# y}
    Scc:
     {top# sent x -> top# check rest x}
    SCC (4):
     Strict:
      {    check# rest x -> check# x,
           check# sent x -> check# x,
       check# cons(x, y) -> check# x,
       check# cons(x, y) -> check# y}
     Weak:
     {      top sent x -> top check rest x,
          check rest x -> rest check x,
          check sent x -> sent check x,
      check cons(x, y) -> cons(x, y),
      check cons(x, y) -> cons(x, check y),
      check cons(x, y) -> cons(check x, y),
            rest nil() -> sent nil(),
       rest cons(x, y) -> sent y}
     SPSC:
      Simple Projection:
       pi(check#) = 0
      Strict:
       {    check# rest x -> check# x,
            check# sent x -> check# x,
        check# cons(x, y) -> check# y}
      EDG:
       {(check# sent x -> check# x, check# cons(x, y) -> check# y)
        (check# sent x -> check# x, check# sent x -> check# x)
        (check# sent x -> check# x, check# rest x -> check# x)
        (check# cons(x, y) -> check# y, check# rest x -> check# x)
        (check# cons(x, y) -> check# y, check# sent x -> check# x)
        (check# cons(x, y) -> check# y, check# cons(x, y) -> check# y)
        (check# rest x -> check# x, check# rest x -> check# x)
        (check# rest x -> check# x, check# sent x -> check# x)
        (check# rest x -> check# x, check# cons(x, y) -> check# y)}
       SCCS (1):
        Scc:
         {    check# rest x -> check# x,
              check# sent x -> check# x,
          check# cons(x, y) -> check# y}
        SCC (3):
         Strict:
          {    check# rest x -> check# x,
               check# sent x -> check# x,
           check# cons(x, y) -> check# y}
         Weak:
         {      top sent x -> top check rest x,
              check rest x -> rest check x,
              check sent x -> sent check x,
          check cons(x, y) -> cons(x, y),
          check cons(x, y) -> cons(x, check y),
          check cons(x, y) -> cons(check x, y),
                rest nil() -> sent nil(),
           rest cons(x, y) -> sent y}
         SPSC:
          Simple Projection:
           pi(check#) = 0
          Strict:
           {    check# rest x -> check# x,
            check# cons(x, y) -> check# y}
          EDG:
           {(check# cons(x, y) -> check# y, check# cons(x, y) -> check# y)
            (check# cons(x, y) -> check# y, check# rest x -> check# x)
            (check# rest x -> check# x, check# rest x -> check# x)
            (check# rest x -> check# x, check# cons(x, y) -> check# y)}
           SCCS (1):
            Scc:
             {    check# rest x -> check# x,
              check# cons(x, y) -> check# y}
            SCC (2):
             Strict:
              {    check# rest x -> check# x,
               check# cons(x, y) -> check# y}
             Weak:
             {      top sent x -> top check rest x,
                  check rest x -> rest check x,
                  check sent x -> sent check x,
              check cons(x, y) -> cons(x, y),
              check cons(x, y) -> cons(x, check y),
              check cons(x, y) -> cons(check x, y),
                    rest nil() -> sent nil(),
               rest cons(x, y) -> sent y}
             SPSC:
              Simple Projection:
               pi(check#) = 0
              Strict:
               {check# cons(x, y) -> check# y}
              EDG:
               {(check# cons(x, y) -> check# y, check# cons(x, y) -> check# y)}
               SCCS (1):
                Scc:
                 {check# cons(x, y) -> check# y}
                SCC (1):
                 Strict:
                  {check# cons(x, y) -> check# y}
                 Weak:
                 {      top sent x -> top check rest x,
                      check rest x -> rest check x,
                      check sent x -> sent check x,
                  check cons(x, y) -> cons(x, y),
                  check cons(x, y) -> cons(x, check y),
                  check cons(x, y) -> cons(check x, y),
                        rest nil() -> sent nil(),
                   rest cons(x, y) -> sent y}
                 SPSC:
                  Simple Projection:
                   pi(check#) = 0
                  Strict:
                   {}
                  Qed
    SCC (1):
     Strict:
      {top# sent x -> top# check rest x}
     Weak:
     {      top sent x -> top check rest x,
          check rest x -> rest check x,
          check sent x -> sent check x,
      check cons(x, y) -> cons(x, y),
      check cons(x, y) -> cons(x, check y),
      check cons(x, y) -> cons(check x, y),
            rest nil() -> sent nil(),
       rest cons(x, y) -> sent y}
     Fail