MAYBE
Time: 1.010960
TRS:
 {               mark __(X1, X2) -> active __(mark X1, mark X2),
                      mark nil() -> active nil(),
                mark and(X1, X2) -> active and(mark X1, X2),
                       mark tt() -> active tt(),
                  mark isNePal X -> active isNePal mark X,
                 __(X1, mark X2) -> __(X1, X2),
               __(X1, active X2) -> __(X1, X2),
                 __(mark X1, X2) -> __(X1, X2),
               __(active X1, X2) -> __(X1, X2),
             active __(X, nil()) -> mark X,
          active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
             active __(nil(), X) -> mark X,
             active and(tt(), X) -> mark X,
  active isNePal __(I, __(P, I)) -> mark tt(),
                and(X1, mark X2) -> and(X1, X2),
              and(X1, active X2) -> and(X1, X2),
                and(mark X1, X2) -> and(X1, X2),
              and(active X1, X2) -> and(X1, X2),
                  isNePal mark X -> isNePal X,
                isNePal active X -> isNePal X}
 DP:
  DP:
   {               mark# __(X1, X2) -> mark# X1,
                   mark# __(X1, X2) -> mark# X2,
                   mark# __(X1, X2) -> __#(mark X1, mark X2),
                   mark# __(X1, X2) -> active# __(mark X1, mark X2),
                        mark# nil() -> active# nil(),
                  mark# and(X1, X2) -> mark# X1,
                  mark# and(X1, X2) -> active# and(mark X1, X2),
                  mark# and(X1, X2) -> and#(mark X1, X2),
                         mark# tt() -> active# tt(),
                    mark# isNePal X -> mark# X,
                    mark# isNePal X -> active# isNePal mark X,
                    mark# isNePal X -> isNePal# mark X,
                   __#(X1, mark X2) -> __#(X1, X2),
                 __#(X1, active X2) -> __#(X1, X2),
                   __#(mark X1, X2) -> __#(X1, X2),
                 __#(active X1, X2) -> __#(X1, X2),
               active# __(X, nil()) -> mark# X,
            active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)),
            active# __(__(X, Y), Z) -> __#(X, __(Y, Z)),
            active# __(__(X, Y), Z) -> __#(Y, Z),
               active# __(nil(), X) -> mark# X,
               active# and(tt(), X) -> mark# X,
    active# isNePal __(I, __(P, I)) -> mark# tt(),
                  and#(X1, mark X2) -> and#(X1, X2),
                and#(X1, active X2) -> and#(X1, X2),
                  and#(mark X1, X2) -> and#(X1, X2),
                and#(active X1, X2) -> and#(X1, X2),
                    isNePal# mark X -> isNePal# X,
                  isNePal# active X -> isNePal# X}
  TRS:
  {               mark __(X1, X2) -> active __(mark X1, mark X2),
                       mark nil() -> active nil(),
                 mark and(X1, X2) -> active and(mark X1, X2),
                        mark tt() -> active tt(),
                   mark isNePal X -> active isNePal mark X,
                  __(X1, mark X2) -> __(X1, X2),
                __(X1, active X2) -> __(X1, X2),
                  __(mark X1, X2) -> __(X1, X2),
                __(active X1, X2) -> __(X1, X2),
              active __(X, nil()) -> mark X,
           active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
              active __(nil(), X) -> mark X,
              active and(tt(), X) -> mark X,
   active isNePal __(I, __(P, I)) -> mark tt(),
                 and(X1, mark X2) -> and(X1, X2),
               and(X1, active X2) -> and(X1, X2),
                 and(mark X1, X2) -> and(X1, X2),
               and(active X1, X2) -> and(X1, X2),
                   isNePal mark X -> isNePal X,
                 isNePal active X -> isNePal X}
  EDG:
   {
    (mark# and(X1, X2) -> mark# X1, mark# isNePal X -> isNePal# mark X)
    (mark# and(X1, X2) -> mark# X1, mark# isNePal X -> active# isNePal mark X)
    (mark# and(X1, X2) -> mark# X1, mark# isNePal X -> mark# X)
    (mark# and(X1, X2) -> mark# X1, mark# tt() -> active# tt())
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# and(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> __#(mark X1, mark X2))
    (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2)
    (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X1)
    (mark# isNePal X -> mark# X, mark# isNePal X -> isNePal# mark X)
    (mark# isNePal X -> mark# X, mark# isNePal X -> active# isNePal mark X)
    (mark# isNePal X -> mark# X, mark# isNePal X -> mark# X)
    (mark# isNePal X -> mark# X, mark# tt() -> active# tt())
    (mark# isNePal X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# isNePal X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# isNePal X -> mark# X, mark# and(X1, X2) -> mark# X1)
    (mark# isNePal X -> mark# X, mark# nil() -> active# nil())
    (mark# isNePal X -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (mark# isNePal X -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2))
    (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X2)
    (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X1)
    (active# __(nil(), X) -> mark# X, mark# isNePal X -> isNePal# mark X)
    (active# __(nil(), X) -> mark# X, mark# isNePal X -> active# isNePal mark X)
    (active# __(nil(), X) -> mark# X, mark# isNePal X -> mark# X)
    (active# __(nil(), X) -> mark# X, mark# tt() -> active# tt())
    (active# __(nil(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (active# __(nil(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# __(nil(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (active# __(nil(), X) -> mark# X, mark# nil() -> active# nil())
    (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2))
    (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X2)
    (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X1)
    (isNePal# mark X -> isNePal# X, isNePal# active X -> isNePal# X)
    (isNePal# mark X -> isNePal# X, isNePal# mark X -> isNePal# X)
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (mark# isNePal X -> isNePal# mark X, isNePal# active X -> isNePal# X)
    (mark# isNePal X -> isNePal# mark X, isNePal# mark X -> isNePal# X)
    (mark# tt() -> active# tt(), active# isNePal __(I, __(P, I)) -> mark# tt())
    (mark# tt() -> active# tt(), active# and(tt(), X) -> mark# X)
    (mark# tt() -> active# tt(), active# __(nil(), X) -> mark# X)
    (mark# tt() -> active# tt(), active# __(__(X, Y), Z) -> __#(Y, Z))
    (mark# tt() -> active# tt(), active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
    (mark# tt() -> active# tt(), active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)))
    (mark# tt() -> active# tt(), active# __(X, nil()) -> mark# X)
    (__#(X1, mark X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2))
    (__#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
    (__#(X1, mark X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2))
    (__#(X1, mark X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
    (__#(mark X1, X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2))
    (__#(mark X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
    (__#(mark X1, X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2))
    (__#(mark X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(active X1, X2) -> __#(X1, X2))
    (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(mark X1, X2) -> __#(X1, X2))
    (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(X1, active X2) -> __#(X1, X2))
    (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(X1, mark X2) -> __#(X1, X2))
    (mark# isNePal X -> active# isNePal mark X, active# isNePal __(I, __(P, I)) -> mark# tt())
    (mark# isNePal X -> active# isNePal mark X, active# and(tt(), X) -> mark# X)
    (mark# isNePal X -> active# isNePal mark X, active# __(nil(), X) -> mark# X)
    (mark# isNePal X -> active# isNePal mark X, active# __(__(X, Y), Z) -> __#(Y, Z))
    (mark# isNePal X -> active# isNePal mark X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
    (mark# isNePal X -> active# isNePal mark X, active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)))
    (mark# isNePal X -> active# isNePal mark X, active# __(X, nil()) -> mark# X)
    (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(active X1, X2) -> __#(X1, X2))
    (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(mark X1, X2) -> __#(X1, X2))
    (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, active X2) -> __#(X1, X2))
    (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(X, nil()) -> mark# X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(__(X, Y), Z) -> __#(Y, Z))
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(nil(), X) -> mark# X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(tt(), X) -> mark# X)
    (mark# and(X1, X2) -> active# and(mark X1, X2), active# isNePal __(I, __(P, I)) -> mark# tt())
    (mark# __(X1, X2) -> mark# X2, mark# __(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 X2))
    (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (mark# __(X1, X2) -> mark# X2, mark# nil() -> active# nil())
    (mark# __(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
    (mark# __(X1, X2) -> mark# X2, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# __(X1, X2) -> mark# X2, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# __(X1, X2) -> mark# X2, mark# tt() -> active# tt())
    (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> mark# X)
    (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> active# isNePal mark X)
    (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> isNePal# mark X)
    (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(X, nil()) -> mark# X)
    (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)))
    (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
    (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(__(X, Y), Z) -> __#(Y, Z))
    (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(nil(), X) -> mark# X)
    (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# and(tt(), X) -> mark# X)
    (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# isNePal __(I, __(P, I)) -> mark# tt())
    (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(active X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
    (and#(X1, active X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
    (__#(active X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
    (__#(active X1, X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2))
    (__#(active X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
    (__#(active X1, X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2))
    (__#(X1, active X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
    (__#(X1, active X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2))
    (__#(X1, active X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
    (__#(X1, active X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2))
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# __(X1, X2) -> mark# X1)
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# __(X1, X2) -> mark# X2)
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# __(X1, X2) -> __#(mark X1, mark X2))
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# nil() -> active# nil())
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# and(X1, X2) -> mark# X1)
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# and(X1, X2) -> and#(mark X1, X2))
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# tt() -> active# tt())
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# isNePal X -> mark# X)
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# isNePal X -> active# isNePal mark X)
    (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# isNePal X -> isNePal# mark X)
    (mark# nil() -> active# nil(), active# __(X, nil()) -> mark# X)
    (mark# nil() -> active# nil(), active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)))
    (mark# nil() -> active# nil(), active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
    (mark# nil() -> active# nil(), active# __(__(X, Y), Z) -> __#(Y, Z))
    (mark# nil() -> active# nil(), active# __(nil(), X) -> mark# X)
    (mark# nil() -> active# nil(), active# and(tt(), X) -> mark# X)
    (mark# nil() -> active# nil(), active# isNePal __(I, __(P, I)) -> mark# tt())
    (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, mark X2) -> __#(X1, X2))
    (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, active X2) -> __#(X1, X2))
    (active# __(__(X, Y), Z) -> __#(Y, Z), __#(mark X1, X2) -> __#(X1, X2))
    (active# __(__(X, Y), Z) -> __#(Y, Z), __#(active X1, X2) -> __#(X1, X2))
    (isNePal# active X -> isNePal# X, isNePal# mark X -> isNePal# X)
    (isNePal# active X -> isNePal# X, isNePal# active X -> isNePal# X)
    (active# and(tt(), X) -> mark# X, mark# __(X1, X2) -> mark# X1)
    (active# and(tt(), X) -> mark# X, mark# __(X1, X2) -> mark# X2)
    (active# and(tt(), X) -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2))
    (active# and(tt(), X) -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (active# and(tt(), X) -> mark# X, mark# nil() -> active# nil())
    (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (active# and(tt(), X) -> mark# X, mark# tt() -> active# tt())
    (active# and(tt(), X) -> mark# X, mark# isNePal X -> mark# X)
    (active# and(tt(), X) -> mark# X, mark# isNePal X -> active# isNePal mark X)
    (active# and(tt(), X) -> mark# X, mark# isNePal X -> isNePal# mark X)
    (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X1)
    (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X2)
    (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2))
    (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (active# __(X, nil()) -> mark# X, mark# nil() -> active# nil())
    (active# __(X, nil()) -> mark# X, mark# and(X1, X2) -> mark# X1)
    (active# __(X, nil()) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# __(X, nil()) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
    (active# __(X, nil()) -> mark# X, mark# tt() -> active# tt())
    (active# __(X, nil()) -> mark# X, mark# isNePal X -> mark# X)
    (active# __(X, nil()) -> mark# X, mark# isNePal X -> active# isNePal mark X)
    (active# __(X, nil()) -> mark# X, mark# isNePal X -> isNePal# mark X)
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# __(X1, X2) -> mark# X1)
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# __(X1, X2) -> mark# X2)
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# __(X1, X2) -> __#(mark X1, mark X2))
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# nil() -> active# nil())
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# and(X1, X2) -> mark# X1)
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# and(X1, X2) -> active# and(mark X1, X2))
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# and(X1, X2) -> and#(mark X1, X2))
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# tt() -> active# tt())
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# isNePal X -> mark# X)
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# isNePal X -> active# isNePal mark X)
    (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# isNePal X -> isNePal# mark X)
    (mark# __(X1, X2) -> mark# X1, mark# __(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 X2))
    (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> active# __(mark X1, mark X2))
    (mark# __(X1, X2) -> mark# X1, mark# nil() -> active# nil())
    (mark# __(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
    (mark# __(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
    (mark# __(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
    (mark# __(X1, X2) -> mark# X1, mark# tt() -> active# tt())
    (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> mark# X)
    (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> active# isNePal mark X)
    (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> isNePal# mark X)
   }
   EDG:
    {
     (mark# and(X1, X2) -> mark# X1, mark# isNePal X -> isNePal# mark X)
     (mark# and(X1, X2) -> mark# X1, mark# isNePal X -> active# isNePal mark X)
     (mark# and(X1, X2) -> mark# X1, mark# isNePal X -> mark# X)
     (mark# and(X1, X2) -> mark# X1, mark# tt() -> active# tt())
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# and(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> active# __(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> __#(mark X1, mark X2))
     (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2)
     (mark# and(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X1)
     (mark# isNePal X -> mark# X, mark# isNePal X -> isNePal# mark X)
     (mark# isNePal X -> mark# X, mark# isNePal X -> active# isNePal mark X)
     (mark# isNePal X -> mark# X, mark# isNePal X -> mark# X)
     (mark# isNePal X -> mark# X, mark# tt() -> active# tt())
     (mark# isNePal X -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# isNePal X -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# isNePal X -> mark# X, mark# and(X1, X2) -> mark# X1)
     (mark# isNePal X -> mark# X, mark# nil() -> active# nil())
     (mark# isNePal X -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2))
     (mark# isNePal X -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2))
     (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X2)
     (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X1)
     (active# __(nil(), X) -> mark# X, mark# isNePal X -> isNePal# mark X)
     (active# __(nil(), X) -> mark# X, mark# isNePal X -> active# isNePal mark X)
     (active# __(nil(), X) -> mark# X, mark# isNePal X -> mark# X)
     (active# __(nil(), X) -> mark# X, mark# tt() -> active# tt())
     (active# __(nil(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
     (active# __(nil(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# __(nil(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (active# __(nil(), X) -> mark# X, mark# nil() -> active# nil())
     (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2))
     (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2))
     (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X2)
     (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X1)
     (isNePal# mark X -> isNePal# X, isNePal# active X -> isNePal# X)
     (isNePal# mark X -> isNePal# X, isNePal# mark X -> isNePal# X)
     (mark# and(X1, X2) -> and#(mark X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (mark# and(X1, X2) -> and#(mark X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, active X2) -> and#(X1, X2))
     (mark# and(X1, X2) -> and#(mark X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (mark# isNePal X -> isNePal# mark X, isNePal# active X -> isNePal# X)
     (mark# isNePal X -> isNePal# mark X, isNePal# mark X -> isNePal# X)
     (__#(X1, mark X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2))
     (__#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
     (__#(X1, mark X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2))
     (__#(X1, mark X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
     (__#(mark X1, X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2))
     (__#(mark X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
     (__#(mark X1, X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2))
     (__#(mark X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
     (and#(X1, mark X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (and#(X1, mark X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(X1, mark X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
     (and#(X1, mark X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(active X1, X2) -> __#(X1, X2))
     (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(mark X1, X2) -> __#(X1, X2))
     (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(X1, active X2) -> __#(X1, X2))
     (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(X1, mark X2) -> __#(X1, X2))
     (mark# isNePal X -> active# isNePal mark X, active# isNePal __(I, __(P, I)) -> mark# tt())
     (mark# isNePal X -> active# isNePal mark X, active# and(tt(), X) -> mark# X)
     (mark# isNePal X -> active# isNePal mark X, active# __(nil(), X) -> mark# X)
     (mark# isNePal X -> active# isNePal mark X, active# __(__(X, Y), Z) -> __#(Y, Z))
     (mark# isNePal X -> active# isNePal mark X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
     (mark# isNePal X -> active# isNePal mark X, active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)))
     (mark# isNePal X -> active# isNePal mark X, active# __(X, nil()) -> mark# X)
     (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(active X1, X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(mark X1, X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, active X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(X, nil()) -> mark# X)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(__(X, Y), Z) -> __#(Y, Z))
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# __(nil(), X) -> mark# X)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# and(tt(), X) -> mark# X)
     (mark# and(X1, X2) -> active# and(mark X1, X2), active# isNePal __(I, __(P, I)) -> mark# tt())
     (mark# __(X1, X2) -> mark# X2, mark# __(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 X2))
     (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> active# __(mark X1, mark X2))
     (mark# __(X1, X2) -> mark# X2, mark# nil() -> active# nil())
     (mark# __(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1)
     (mark# __(X1, X2) -> mark# X2, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# __(X1, X2) -> mark# X2, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# __(X1, X2) -> mark# X2, mark# tt() -> active# tt())
     (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> mark# X)
     (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> active# isNePal mark X)
     (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> isNePal# mark X)
     (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(X, nil()) -> mark# X)
     (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)))
     (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
     (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(__(X, Y), Z) -> __#(Y, Z))
     (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(nil(), X) -> mark# X)
     (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# and(tt(), X) -> mark# X)
     (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# isNePal __(I, __(P, I)) -> mark# tt())
     (and#(active X1, X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (and#(active X1, X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
     (and#(active X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(active X1, X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (and#(X1, active X2) -> and#(X1, X2), and#(X1, mark X2) -> and#(X1, X2))
     (and#(X1, active X2) -> and#(X1, X2), and#(X1, active X2) -> and#(X1, X2))
     (and#(X1, active X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(X1, active X2) -> and#(X1, X2), and#(active X1, X2) -> and#(X1, X2))
     (__#(active X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
     (__#(active X1, X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2))
     (__#(active X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
     (__#(active X1, X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2))
     (__#(X1, active X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
     (__#(X1, active X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2))
     (__#(X1, active X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
     (__#(X1, active X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2))
     (active# isNePal __(I, __(P, I)) -> mark# tt(), mark# tt() -> active# tt())
     (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, mark X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, active X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(Y, Z), __#(mark X1, X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(Y, Z), __#(active X1, X2) -> __#(X1, X2))
     (isNePal# active X -> isNePal# X, isNePal# mark X -> isNePal# X)
     (isNePal# active X -> isNePal# X, isNePal# active X -> isNePal# X)
     (active# and(tt(), X) -> mark# X, mark# __(X1, X2) -> mark# X1)
     (active# and(tt(), X) -> mark# X, mark# __(X1, X2) -> mark# X2)
     (active# and(tt(), X) -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2))
     (active# and(tt(), X) -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2))
     (active# and(tt(), X) -> mark# X, mark# nil() -> active# nil())
     (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# and(tt(), X) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
     (active# and(tt(), X) -> mark# X, mark# tt() -> active# tt())
     (active# and(tt(), X) -> mark# X, mark# isNePal X -> mark# X)
     (active# and(tt(), X) -> mark# X, mark# isNePal X -> active# isNePal mark X)
     (active# and(tt(), X) -> mark# X, mark# isNePal X -> isNePal# mark X)
     (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X1)
     (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X2)
     (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2))
     (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2))
     (active# __(X, nil()) -> mark# X, mark# nil() -> active# nil())
     (active# __(X, nil()) -> mark# X, mark# and(X1, X2) -> mark# X1)
     (active# __(X, nil()) -> mark# X, mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# __(X, nil()) -> mark# X, mark# and(X1, X2) -> and#(mark X1, X2))
     (active# __(X, nil()) -> mark# X, mark# tt() -> active# tt())
     (active# __(X, nil()) -> mark# X, mark# isNePal X -> mark# X)
     (active# __(X, nil()) -> mark# X, mark# isNePal X -> active# isNePal mark X)
     (active# __(X, nil()) -> mark# X, mark# isNePal X -> isNePal# mark X)
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# __(X1, X2) -> mark# X1)
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# __(X1, X2) -> mark# X2)
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# __(X1, X2) -> __#(mark X1, mark X2))
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# __(X1, X2) -> active# __(mark X1, mark X2))
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# and(X1, X2) -> mark# X1)
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# and(X1, X2) -> active# and(mark X1, X2))
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# and(X1, X2) -> and#(mark X1, X2))
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# isNePal X -> mark# X)
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# isNePal X -> active# isNePal mark X)
     (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# isNePal X -> isNePal# mark X)
     (mark# __(X1, X2) -> mark# X1, mark# __(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 X2))
     (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> active# __(mark X1, mark X2))
     (mark# __(X1, X2) -> mark# X1, mark# nil() -> active# nil())
     (mark# __(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1)
     (mark# __(X1, X2) -> mark# X1, mark# and(X1, X2) -> active# and(mark X1, X2))
     (mark# __(X1, X2) -> mark# X1, mark# and(X1, X2) -> and#(mark X1, X2))
     (mark# __(X1, X2) -> mark# X1, mark# tt() -> active# tt())
     (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> mark# X)
     (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> active# isNePal mark X)
     (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> isNePal# mark X)
    }
    STATUS:
     arrows: 0.866825
     SCCS (1):
      Scc:
       {       mark# __(X1, X2) -> mark# X1,
               mark# __(X1, X2) -> mark# X2,
               mark# __(X1, X2) -> active# __(mark X1, mark X2),
              mark# and(X1, X2) -> mark# X1,
              mark# and(X1, X2) -> active# and(mark X1, X2),
                mark# isNePal X -> mark# X,
           active# __(X, nil()) -> mark# X,
        active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)),
           active# __(nil(), X) -> mark# X,
           active# and(tt(), X) -> mark# X}
      
      
      
      SCC (10):
       Strict:
        {       mark# __(X1, X2) -> mark# X1,
                mark# __(X1, X2) -> mark# X2,
                mark# __(X1, X2) -> active# __(mark X1, mark X2),
               mark# and(X1, X2) -> mark# X1,
               mark# and(X1, X2) -> active# and(mark X1, X2),
                 mark# isNePal X -> mark# X,
            active# __(X, nil()) -> mark# X,
         active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)),
            active# __(nil(), X) -> mark# X,
            active# and(tt(), X) -> mark# X}
       Weak:
       {               mark __(X1, X2) -> active __(mark X1, mark X2),
                            mark nil() -> active nil(),
                      mark and(X1, X2) -> active and(mark X1, X2),
                             mark tt() -> active tt(),
                        mark isNePal X -> active isNePal mark X,
                       __(X1, mark X2) -> __(X1, X2),
                     __(X1, active X2) -> __(X1, X2),
                       __(mark X1, X2) -> __(X1, X2),
                     __(active X1, X2) -> __(X1, X2),
                   active __(X, nil()) -> mark X,
                active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
                   active __(nil(), X) -> mark X,
                   active and(tt(), X) -> mark X,
        active isNePal __(I, __(P, I)) -> mark tt(),
                      and(X1, mark X2) -> and(X1, X2),
                    and(X1, active X2) -> and(X1, X2),
                      and(mark X1, X2) -> and(X1, X2),
                    and(active X1, X2) -> and(X1, X2),
                        isNePal mark X -> isNePal X,
                      isNePal active X -> isNePal X}
       Open