MAYBE
Time: 47.060925
TRS:
 {           a____(X, nil()) -> mark X,
               a____(X1, X2) -> __(X1, X2),
          a____(__(X, Y), Z) -> a____(mark X, a____(mark Y, mark Z)),
             a____(nil(), X) -> mark X,
             mark __(X1, X2) -> a____(mark X1, mark X2),
                  mark nil() -> nil(),
                   mark tt() -> tt(),
            mark and(X1, X2) -> a__and(mark X1, X2),
              mark isNePal X -> a__isNePal mark X,
              a__and(X1, X2) -> and(X1, X2),
             a__and(tt(), X) -> mark X,
                a__isNePal X -> isNePal X,
  a__isNePal __(I, __(P, I)) -> tt()}
 DP:
  DP:
   {   a____#(X, nil()) -> mark# X,
    a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)),
    a____#(__(X, Y), Z) -> a____#(mark Y, mark Z),
    a____#(__(X, Y), Z) -> mark# X,
    a____#(__(X, Y), Z) -> mark# Y,
    a____#(__(X, Y), Z) -> mark# Z,
       a____#(nil(), X) -> mark# X,
       mark# __(X1, X2) -> a____#(mark X1, mark X2),
       mark# __(X1, X2) -> mark# X1,
       mark# __(X1, X2) -> mark# X2,
      mark# and(X1, X2) -> mark# X1,
      mark# and(X1, X2) -> a__and#(mark X1, X2),
        mark# isNePal X -> mark# X,
        mark# isNePal X -> a__isNePal# mark X,
       a__and#(tt(), X) -> mark# X}
  TRS:
  {           a____(X, nil()) -> mark X,
                a____(X1, X2) -> __(X1, X2),
           a____(__(X, Y), Z) -> a____(mark X, a____(mark Y, mark Z)),
              a____(nil(), X) -> mark X,
              mark __(X1, X2) -> a____(mark X1, mark X2),
                   mark nil() -> nil(),
                    mark tt() -> tt(),
             mark and(X1, X2) -> a__and(mark X1, X2),
               mark isNePal X -> a__isNePal mark X,
               a__and(X1, X2) -> and(X1, X2),
              a__and(tt(), X) -> mark X,
                 a__isNePal X -> isNePal X,
   a__isNePal __(I, __(P, I)) -> tt()}
  UR:
   {           a____(X, nil()) -> mark X,
                 a____(X1, X2) -> __(X1, X2),
            a____(__(X, Y), Z) -> a____(mark X, a____(mark Y, mark Z)),
               a____(nil(), X) -> mark X,
               mark __(X1, X2) -> a____(mark X1, mark X2),
                    mark nil() -> nil(),
                     mark tt() -> tt(),
              mark and(X1, X2) -> a__and(mark X1, X2),
                mark isNePal X -> a__isNePal mark X,
                a__and(X1, X2) -> and(X1, X2),
               a__and(tt(), X) -> mark X,
                  a__isNePal X -> isNePal X,
    a__isNePal __(I, __(P, I)) -> tt()}
   EDG:
    {(a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(nil(), X) -> mark# X)
     (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# Z)
     (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# Y)
     (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# X)
     (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z))
     (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)))
     (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(X, nil()) -> mark# X)
     (a____#(__(X, Y), Z) -> mark# Z, mark# isNePal X -> a__isNePal# mark X)
     (a____#(__(X, Y), Z) -> mark# Z, mark# isNePal X -> mark# X)
     (a____#(__(X, Y), Z) -> mark# Z, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a____#(__(X, Y), Z) -> mark# Z, mark# and(X1, X2) -> mark# X1)
     (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> mark# X2)
     (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> mark# X1)
     (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> a__isNePal# mark X)
     (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> mark# X)
     (mark# __(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# __(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2)
     (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X1)
     (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (a____#(__(X, Y), Z) -> mark# X, mark# isNePal X -> a__isNePal# mark X)
     (a____#(__(X, Y), Z) -> mark# X, mark# isNePal X -> mark# X)
     (a____#(__(X, Y), Z) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a____#(__(X, Y), Z) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> mark# X2)
     (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> mark# X1)
     (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (mark# isNePal X -> mark# X, mark# isNePal X -> a__isNePal# mark X)
     (mark# isNePal X -> mark# X, mark# isNePal X -> mark# X)
     (mark# isNePal X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# isNePal X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X2)
     (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X1)
     (mark# isNePal X -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> a__isNePal# mark X)
     (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> mark# X)
     (mark# __(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# __(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> mark# X2)
     (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> mark# X1)
     (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (a__and#(tt(), X) -> mark# X, mark# __(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# __(X1, X2) -> mark# X2)
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a__and#(tt(), X) -> mark# X, mark# isNePal X -> mark# X)
     (a__and#(tt(), X) -> mark# X, mark# isNePal X -> a__isNePal# mark X)
     (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X1)
     (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X2)
     (a____#(nil(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a____#(nil(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a____#(nil(), X) -> mark# X, mark# isNePal X -> mark# X)
     (a____#(nil(), X) -> mark# X, mark# isNePal X -> a__isNePal# mark X)
     (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X1)
     (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X2)
     (a____#(X, nil()) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (a____#(X, nil()) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a____#(X, nil()) -> mark# X, mark# isNePal X -> mark# X)
     (a____#(X, nil()) -> mark# X, mark# isNePal X -> a__isNePal# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# isNePal X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# isNePal X -> a__isNePal# mark X)
     (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(X, nil()) -> mark# X)
     (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)))
     (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z))
     (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# X)
     (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# Y)
     (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# Z)
     (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(nil(), X) -> mark# X)
     (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(X, nil()) -> mark# X)
     (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)))
     (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z))
     (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# X)
     (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# Y)
     (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# Z)
     (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(nil(), X) -> mark# X)
     (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> a____#(mark X1, mark X2))
     (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> mark# X1)
     (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> mark# X2)
     (a____#(__(X, Y), Z) -> mark# Y, mark# and(X1, X2) -> mark# X1)
     (a____#(__(X, Y), Z) -> mark# Y, mark# and(X1, X2) -> a__and#(mark X1, X2))
     (a____#(__(X, Y), Z) -> mark# Y, mark# isNePal X -> mark# X)
     (a____#(__(X, Y), Z) -> mark# Y, mark# isNePal X -> a__isNePal# mark X)}
    STATUS:
     arrows: 0.591111
     SCCS (1):
      Scc:
       {   a____#(X, nil()) -> mark# X,
        a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)),
        a____#(__(X, Y), Z) -> a____#(mark Y, mark Z),
        a____#(__(X, Y), Z) -> mark# X,
        a____#(__(X, Y), Z) -> mark# Y,
        a____#(__(X, Y), Z) -> mark# Z,
           a____#(nil(), X) -> mark# X,
           mark# __(X1, X2) -> a____#(mark X1, mark X2),
           mark# __(X1, X2) -> mark# X1,
           mark# __(X1, X2) -> mark# X2,
          mark# and(X1, X2) -> mark# X1,
          mark# and(X1, X2) -> a__and#(mark X1, X2),
            mark# isNePal X -> mark# X,
           a__and#(tt(), X) -> mark# X}
      
      SCC (14):
       Strict:
        {   a____#(X, nil()) -> mark# X,
         a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)),
         a____#(__(X, Y), Z) -> a____#(mark Y, mark Z),
         a____#(__(X, Y), Z) -> mark# X,
         a____#(__(X, Y), Z) -> mark# Y,
         a____#(__(X, Y), Z) -> mark# Z,
            a____#(nil(), X) -> mark# X,
            mark# __(X1, X2) -> a____#(mark X1, mark X2),
            mark# __(X1, X2) -> mark# X1,
            mark# __(X1, X2) -> mark# X2,
           mark# and(X1, X2) -> mark# X1,
           mark# and(X1, X2) -> a__and#(mark X1, X2),
             mark# isNePal X -> mark# X,
            a__and#(tt(), X) -> mark# X}
       Weak:
       {           a____(X, nil()) -> mark X,
                     a____(X1, X2) -> __(X1, X2),
                a____(__(X, Y), Z) -> a____(mark X, a____(mark Y, mark Z)),
                   a____(nil(), X) -> mark X,
                   mark __(X1, X2) -> a____(mark X1, mark X2),
                        mark nil() -> nil(),
                         mark tt() -> tt(),
                  mark and(X1, X2) -> a__and(mark X1, X2),
                    mark isNePal X -> a__isNePal mark X,
                    a__and(X1, X2) -> and(X1, X2),
                   a__and(tt(), X) -> mark X,
                      a__isNePal X -> isNePal X,
        a__isNePal __(I, __(P, I)) -> tt()}
       Open