MAYBE
Time: 0.008520
TRS:
 {          null nil() -> true(),
        null add(n, x) -> false(),
            tail nil() -> nil(),
        tail add(n, x) -> x,
        head add(n, x) -> n,
         app(nil(), y) -> y,
     app(add(n, x), y) -> add(n, app(x, y)),
         reverse nil() -> nil(),
     reverse add(n, x) -> app(reverse x, add(n, nil())),
           shuff(x, y) -> if(null x, x, y, app(y, add(head x, nil()))),
             shuffle x -> shuff(x, nil()),
   if(true(), x, y, z) -> y,
  if(false(), x, y, z) -> shuff(reverse tail x, z)}
 DP:
  DP:
   {   app#(add(n, x), y) -> app#(x, y),
       reverse# add(n, x) -> app#(reverse x, add(n, nil())),
       reverse# add(n, x) -> reverse# x,
             shuff#(x, y) -> null# x,
             shuff#(x, y) -> head# x,
             shuff#(x, y) -> app#(y, add(head x, nil())),
             shuff#(x, y) -> if#(null x, x, y, app(y, add(head x, nil()))),
               shuffle# x -> shuff#(x, nil()),
    if#(false(), x, y, z) -> tail# x,
    if#(false(), x, y, z) -> reverse# tail x,
    if#(false(), x, y, z) -> shuff#(reverse tail x, z)}
  TRS:
  {          null nil() -> true(),
         null add(n, x) -> false(),
             tail nil() -> nil(),
         tail add(n, x) -> x,
         head add(n, x) -> n,
          app(nil(), y) -> y,
      app(add(n, x), y) -> add(n, app(x, y)),
          reverse nil() -> nil(),
      reverse add(n, x) -> app(reverse x, add(n, nil())),
            shuff(x, y) -> if(null x, x, y, app(y, add(head x, nil()))),
              shuffle x -> shuff(x, nil()),
    if(true(), x, y, z) -> y,
   if(false(), x, y, z) -> shuff(reverse tail x, z)}
  EDG:
   {(reverse# add(n, x) -> app#(reverse x, add(n, nil())), app#(add(n, x), y) -> app#(x, y))
    (shuff#(x, y) -> if#(null x, x, y, app(y, add(head x, nil()))), if#(false(), x, y, z) -> shuff#(reverse tail x, z))
    (shuff#(x, y) -> if#(null x, x, y, app(y, add(head x, nil()))), if#(false(), x, y, z) -> reverse# tail x)
    (shuff#(x, y) -> if#(null x, x, y, app(y, add(head x, nil()))), if#(false(), x, y, z) -> tail# x)
    (app#(add(n, x), y) -> app#(x, y), app#(add(n, x), y) -> app#(x, y))
    (if#(false(), x, y, z) -> reverse# tail x, reverse# add(n, x) -> app#(reverse x, add(n, nil())))
    (if#(false(), x, y, z) -> reverse# tail x, reverse# add(n, x) -> reverse# x)
    (if#(false(), x, y, z) -> shuff#(reverse tail x, z), shuff#(x, y) -> null# x)
    (if#(false(), x, y, z) -> shuff#(reverse tail x, z), shuff#(x, y) -> head# x)
    (if#(false(), x, y, z) -> shuff#(reverse tail x, z), shuff#(x, y) -> app#(y, add(head x, nil())))
    (if#(false(), x, y, z) -> shuff#(reverse tail x, z), shuff#(x, y) -> if#(null x, x, y, app(y, add(head x, nil()))))
    (shuff#(x, y) -> app#(y, add(head x, nil())), app#(add(n, x), y) -> app#(x, y))
    (shuffle# x -> shuff#(x, nil()), shuff#(x, y) -> null# x)
    (shuffle# x -> shuff#(x, nil()), shuff#(x, y) -> head# x)
    (shuffle# x -> shuff#(x, nil()), shuff#(x, y) -> app#(y, add(head x, nil())))
    (shuffle# x -> shuff#(x, nil()), shuff#(x, y) -> if#(null x, x, y, app(y, add(head x, nil()))))
    (reverse# add(n, x) -> reverse# x, reverse# add(n, x) -> app#(reverse x, add(n, nil())))
    (reverse# add(n, x) -> reverse# x, reverse# add(n, x) -> reverse# x)}
   STATUS:
    arrows: 0.851240
    SCCS (3):
     Scc:
      {         shuff#(x, y) -> if#(null x, x, y, app(y, add(head x, nil()))),
       if#(false(), x, y, z) -> shuff#(reverse tail x, z)}
     Scc:
      {reverse# add(n, x) -> reverse# x}
     Scc:
      {app#(add(n, x), y) -> app#(x, y)}
     
     
     SCC (2):
      Strict:
       {         shuff#(x, y) -> if#(null x, x, y, app(y, add(head x, nil()))),
        if#(false(), x, y, z) -> shuff#(reverse tail x, z)}
      Weak:
      {          null nil() -> true(),
             null add(n, x) -> false(),
                 tail nil() -> nil(),
             tail add(n, x) -> x,
             head add(n, x) -> n,
              app(nil(), y) -> y,
          app(add(n, x), y) -> add(n, app(x, y)),
              reverse nil() -> nil(),
          reverse add(n, x) -> app(reverse x, add(n, nil())),
                shuff(x, y) -> if(null x, x, y, app(y, add(head x, nil()))),
                  shuffle x -> shuff(x, nil()),
        if(true(), x, y, z) -> y,
       if(false(), x, y, z) -> shuff(reverse tail x, z)}
      Open
     
     
     
     
     
     SCC (1):
      Strict:
       {reverse# add(n, x) -> reverse# x}
      Weak:
      {          null nil() -> true(),
             null add(n, x) -> false(),
                 tail nil() -> nil(),
             tail add(n, x) -> x,
             head add(n, x) -> n,
              app(nil(), y) -> y,
          app(add(n, x), y) -> add(n, app(x, y)),
              reverse nil() -> nil(),
          reverse add(n, x) -> app(reverse x, add(n, nil())),
                shuff(x, y) -> if(null x, x, y, app(y, add(head x, nil()))),
                  shuffle x -> shuff(x, nil()),
        if(true(), x, y, z) -> y,
       if(false(), x, y, z) -> shuff(reverse tail x, z)}
      Open
     
     SCC (1):
      Strict:
       {app#(add(n, x), y) -> app#(x, y)}
      Weak:
      {          null nil() -> true(),
             null add(n, x) -> false(),
                 tail nil() -> nil(),
             tail add(n, x) -> x,
             head add(n, x) -> n,
              app(nil(), y) -> y,
          app(add(n, x), y) -> add(n, app(x, y)),
              reverse nil() -> nil(),
          reverse add(n, x) -> app(reverse x, add(n, nil())),
                shuff(x, y) -> if(null x, x, y, app(y, add(head x, nil()))),
                  shuffle x -> shuff(x, nil()),
        if(true(), x, y, z) -> y,
       if(false(), x, y, z) -> shuff(reverse tail x, z)}
      Open