MAYBE
Time: 0.050716
TRS:
 {           is_empty nil() -> true(),
        is_empty cons(x, l) -> false(),
              hd cons(x, l) -> x,
              tl cons(x, l) -> l,
   ifappend(l1, l2, true()) -> l2,
  ifappend(l1, l2, false()) -> cons(hd l1, append(tl l1, l2)),
             append(l1, l2) -> ifappend(l1, l2, is_empty l1)}
 DP:
  DP:
   {ifappend#(l1, l2, false()) -> hd# l1,
    ifappend#(l1, l2, false()) -> tl# l1,
    ifappend#(l1, l2, false()) -> append#(tl l1, l2),
               append#(l1, l2) -> is_empty# l1,
               append#(l1, l2) -> ifappend#(l1, l2, is_empty l1)}
  TRS:
  {           is_empty nil() -> true(),
         is_empty cons(x, l) -> false(),
               hd cons(x, l) -> x,
               tl cons(x, l) -> l,
    ifappend(l1, l2, true()) -> l2,
   ifappend(l1, l2, false()) -> cons(hd l1, append(tl l1, l2)),
              append(l1, l2) -> ifappend(l1, l2, is_empty l1)}
  UR:
   {     is_empty nil() -> true(),
    is_empty cons(x, l) -> false(),
          tl cons(x, l) -> l,
                a(y, z) -> y,
                a(y, z) -> z}
   EDG:
    {(append#(l1, l2) -> ifappend#(l1, l2, is_empty l1), ifappend#(l1, l2, false()) -> append#(tl l1, l2))
     (append#(l1, l2) -> ifappend#(l1, l2, is_empty l1), ifappend#(l1, l2, false()) -> tl# l1)
     (append#(l1, l2) -> ifappend#(l1, l2, is_empty l1), ifappend#(l1, l2, false()) -> hd# l1)
     (ifappend#(l1, l2, false()) -> append#(tl l1, l2), append#(l1, l2) -> is_empty# l1)
     (ifappend#(l1, l2, false()) -> append#(tl l1, l2), append#(l1, l2) -> ifappend#(l1, l2, is_empty l1))}
    STATUS:
     arrows: 0.800000
     SCCS (1):
      Scc:
       {ifappend#(l1, l2, false()) -> append#(tl l1, l2),
                   append#(l1, l2) -> ifappend#(l1, l2, is_empty l1)}
      
      SCC (2):
       Strict:
        {ifappend#(l1, l2, false()) -> append#(tl l1, l2),
                    append#(l1, l2) -> ifappend#(l1, l2, is_empty l1)}
       Weak:
       {           is_empty nil() -> true(),
              is_empty cons(x, l) -> false(),
                    hd cons(x, l) -> x,
                    tl cons(x, l) -> l,
         ifappend(l1, l2, true()) -> l2,
        ifappend(l1, l2, false()) -> cons(hd l1, append(tl l1, l2)),
                   append(l1, l2) -> ifappend(l1, l2, is_empty l1)}
       Fail