MAYBE

Problem:
 top(sent(x)) -> top(check(rest(x)))
 rest(nil()) -> sent(nil())
 rest(cons(x,y)) -> sent(y)
 check(sent(x)) -> sent(check(x))
 check(rest(x)) -> rest(check(x))
 check(cons(x,y)) -> cons(check(x),y)
 check(cons(x,y)) -> cons(x,check(y))
 check(cons(x,y)) -> cons(x,y)

Proof:
 DP Processor:
  DPs:
   top#(sent(x)) -> rest#(x)
   top#(sent(x)) -> check#(rest(x))
   top#(sent(x)) -> top#(check(rest(x)))
   check#(sent(x)) -> check#(x)
   check#(rest(x)) -> check#(x)
   check#(rest(x)) -> rest#(check(x))
   check#(cons(x,y)) -> check#(x)
   check#(cons(x,y)) -> check#(y)
  TRS:
   top(sent(x)) -> top(check(rest(x)))
   rest(nil()) -> sent(nil())
   rest(cons(x,y)) -> sent(y)
   check(sent(x)) -> sent(check(x))
   check(rest(x)) -> rest(check(x))
   check(cons(x,y)) -> cons(check(x),y)
   check(cons(x,y)) -> cons(x,check(y))
   check(cons(x,y)) -> cons(x,y)
  Usable Rule Processor:
   DPs:
    top#(sent(x)) -> rest#(x)
    top#(sent(x)) -> check#(rest(x))
    top#(sent(x)) -> top#(check(rest(x)))
    check#(sent(x)) -> check#(x)
    check#(rest(x)) -> check#(x)
    check#(rest(x)) -> rest#(check(x))
    check#(cons(x,y)) -> check#(x)
    check#(cons(x,y)) -> check#(y)
   TRS:
    rest(nil()) -> sent(nil())
    rest(cons(x,y)) -> sent(y)
    check(sent(x)) -> sent(check(x))
    check(rest(x)) -> rest(check(x))
    check(cons(x,y)) -> cons(check(x),y)
    check(cons(x,y)) -> cons(x,check(y))
    check(cons(x,y)) -> cons(x,y)
   CDG Processor:
    DPs:
     top#(sent(x)) -> rest#(x)
     top#(sent(x)) -> check#(rest(x))
     top#(sent(x)) -> top#(check(rest(x)))
     check#(sent(x)) -> check#(x)
     check#(rest(x)) -> check#(x)
     check#(rest(x)) -> rest#(check(x))
     check#(cons(x,y)) -> check#(x)
     check#(cons(x,y)) -> check#(y)
    TRS:
     rest(nil()) -> sent(nil())
     rest(cons(x,y)) -> sent(y)
     check(sent(x)) -> sent(check(x))
     check(rest(x)) -> rest(check(x))
     check(cons(x,y)) -> cons(check(x),y)
     check(cons(x,y)) -> cons(x,check(y))
     check(cons(x,y)) -> cons(x,y)
    graph:
     top#(sent(x)) -> check#(rest(x)) ->
     check#(sent(x)) -> check#(x)
     top#(sent(x)) -> check#(rest(x)) ->
     check#(rest(x)) -> check#(x)
     top#(sent(x)) -> check#(rest(x)) ->
     check#(rest(x)) -> rest#(check(x))
     top#(sent(x)) -> top#(check(rest(x))) ->
     top#(sent(x)) -> 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)) -> top#(check(rest(x)))
    Restore Modifier:
     DPs:
      top#(sent(x)) -> rest#(x)
      top#(sent(x)) -> check#(rest(x))
      top#(sent(x)) -> top#(check(rest(x)))
      check#(sent(x)) -> check#(x)
      check#(rest(x)) -> check#(x)
      check#(rest(x)) -> rest#(check(x))
      check#(cons(x,y)) -> check#(x)
      check#(cons(x,y)) -> check#(y)
     TRS:
      top(sent(x)) -> top(check(rest(x)))
      rest(nil()) -> sent(nil())
      rest(cons(x,y)) -> sent(y)
      check(sent(x)) -> sent(check(x))
      check(rest(x)) -> rest(check(x))
      check(cons(x,y)) -> cons(check(x),y)
      check(cons(x,y)) -> cons(x,check(y))
      check(cons(x,y)) -> cons(x,y)
     SCC Processor:
      #sccs: 1
      #rules: 1
      #arcs: 6/64
      DPs:
       top#(sent(x)) -> top#(check(rest(x)))
      TRS:
       top(sent(x)) -> top(check(rest(x)))
       rest(nil()) -> sent(nil())
       rest(cons(x,y)) -> sent(y)
       check(sent(x)) -> sent(check(x))
       check(rest(x)) -> rest(check(x))
       check(cons(x,y)) -> cons(check(x),y)
       check(cons(x,y)) -> cons(x,check(y))
       check(cons(x,y)) -> cons(x,y)
      Open