MAYBE
Time: 0.794276
TRS:
 {               __(X1, mark X2) -> mark __(X1, X2),
                 __(mark X1, X2) -> mark __(X1, X2),
                __(ok X1, ok X2) -> ok __(X1, X2),
             active __(X, nil()) -> mark X,
               active __(X1, X2) -> __(X1, active X2),
               active __(X1, X2) -> __(active X1, X2),
          active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
             active __(nil(), X) -> mark X,
              active and(X1, X2) -> and(active X1, X2),
             active and(tt(), X) -> mark X,
               active isNeList V -> mark isQid V,
      active isNeList __(V1, V2) -> mark and(isNeList V1, isList V2),
      active isNeList __(V1, V2) -> mark and(isList V1, isNeList V2),
                 active isList V -> mark isNeList V,
        active isList __(V1, V2) -> mark and(isList V1, isList V2),
             active isList nil() -> mark tt(),
                active isQid a() -> mark tt(),
                active isQid e() -> mark tt(),
                active isQid i() -> mark tt(),
                active isQid o() -> mark tt(),
                active isQid u() -> mark tt(),
                active isNePal V -> mark isQid V,
  active isNePal __(I, __(P, I)) -> mark and(isQid I, isPal P),
                  active isPal V -> mark isNePal V,
              active isPal nil() -> mark tt(),
                and(mark X1, X2) -> mark and(X1, X2),
               and(ok X1, ok X2) -> ok and(X1, X2),
                   isNeList ok X -> ok isNeList X,
                     isList ok X -> ok isList X,
                      isQid ok X -> ok isQid X,
                    isNePal ok X -> ok isNePal X,
                      isPal ok X -> ok isPal X,
               proper __(X1, X2) -> __(proper X1, proper X2),
                    proper nil() -> ok nil(),
              proper and(X1, X2) -> and(proper X1, proper X2),
                     proper tt() -> ok tt(),
               proper isNeList X -> isNeList proper X,
                 proper isList X -> isList proper X,
                  proper isQid X -> isQid proper X,
                proper isNePal X -> isNePal proper X,
                  proper isPal X -> isPal proper X,
                      proper a() -> ok a(),
                      proper e() -> ok e(),
                      proper i() -> ok i(),
                      proper o() -> ok o(),
                      proper u() -> ok u(),
                      top mark X -> top proper X,
                        top ok X -> top active X}
 DP:
  DP:
   {               __#(X1, mark X2) -> __#(X1, X2),
                   __#(mark X1, X2) -> __#(X1, X2),
                  __#(ok X1, ok X2) -> __#(X1, X2),
                 active# __(X1, X2) -> __#(X1, active X2),
                 active# __(X1, X2) -> __#(active X1, X2),
                 active# __(X1, X2) -> active# X1,
                 active# __(X1, X2) -> active# X2,
            active# __(__(X, Y), Z) -> __#(X, __(Y, Z)),
            active# __(__(X, Y), Z) -> __#(Y, Z),
                active# and(X1, X2) -> active# X1,
                active# and(X1, X2) -> and#(active X1, X2),
                 active# isNeList V -> isQid# V,
        active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2),
        active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2),
        active# isNeList __(V1, V2) -> isNeList# V1,
        active# isNeList __(V1, V2) -> isNeList# V2,
        active# isNeList __(V1, V2) -> isList# V1,
        active# isNeList __(V1, V2) -> isList# V2,
                   active# isList V -> isNeList# V,
          active# isList __(V1, V2) -> and#(isList V1, isList V2),
          active# isList __(V1, V2) -> isList# V1,
          active# isList __(V1, V2) -> isList# V2,
                  active# isNePal V -> isQid# V,
    active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P),
    active# isNePal __(I, __(P, I)) -> isQid# I,
    active# isNePal __(I, __(P, I)) -> isPal# P,
                    active# isPal V -> isNePal# V,
                  and#(mark X1, X2) -> and#(X1, X2),
                 and#(ok X1, ok X2) -> and#(X1, X2),
                     isNeList# ok X -> isNeList# X,
                       isList# ok X -> isList# X,
                        isQid# ok X -> isQid# X,
                      isNePal# ok X -> isNePal# X,
                        isPal# ok X -> isPal# X,
                 proper# __(X1, X2) -> __#(proper X1, proper X2),
                 proper# __(X1, X2) -> proper# X1,
                 proper# __(X1, X2) -> proper# X2,
                proper# and(X1, X2) -> and#(proper X1, proper X2),
                proper# and(X1, X2) -> proper# X1,
                proper# and(X1, X2) -> proper# X2,
                 proper# isNeList X -> isNeList# proper X,
                 proper# isNeList X -> proper# X,
                   proper# isList X -> isList# proper X,
                   proper# isList X -> proper# X,
                    proper# isQid X -> isQid# proper X,
                    proper# isQid X -> proper# X,
                  proper# isNePal X -> isNePal# proper X,
                  proper# isNePal X -> proper# X,
                    proper# isPal X -> isPal# proper X,
                    proper# isPal X -> proper# X,
                        top# mark X -> proper# X,
                        top# mark X -> top# proper X,
                          top# ok X -> active# X,
                          top# ok X -> top# active X}
  TRS:
  {               __(X1, mark X2) -> mark __(X1, X2),
                  __(mark X1, X2) -> mark __(X1, X2),
                 __(ok X1, ok X2) -> ok __(X1, X2),
              active __(X, nil()) -> mark X,
                active __(X1, X2) -> __(X1, active X2),
                active __(X1, X2) -> __(active X1, X2),
           active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
              active __(nil(), X) -> mark X,
               active and(X1, X2) -> and(active X1, X2),
              active and(tt(), X) -> mark X,
                active isNeList V -> mark isQid V,
       active isNeList __(V1, V2) -> mark and(isNeList V1, isList V2),
       active isNeList __(V1, V2) -> mark and(isList V1, isNeList V2),
                  active isList V -> mark isNeList V,
         active isList __(V1, V2) -> mark and(isList V1, isList V2),
              active isList nil() -> mark tt(),
                 active isQid a() -> mark tt(),
                 active isQid e() -> mark tt(),
                 active isQid i() -> mark tt(),
                 active isQid o() -> mark tt(),
                 active isQid u() -> mark tt(),
                 active isNePal V -> mark isQid V,
   active isNePal __(I, __(P, I)) -> mark and(isQid I, isPal P),
                   active isPal V -> mark isNePal V,
               active isPal nil() -> mark tt(),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                    isNeList ok X -> ok isNeList X,
                      isList ok X -> ok isList X,
                       isQid ok X -> ok isQid X,
                     isNePal ok X -> ok isNePal X,
                       isPal ok X -> ok isPal X,
                proper __(X1, X2) -> __(proper X1, proper X2),
                     proper nil() -> ok nil(),
               proper and(X1, X2) -> and(proper X1, proper X2),
                      proper tt() -> ok tt(),
                proper isNeList X -> isNeList proper X,
                  proper isList X -> isList proper X,
                   proper isQid X -> isQid proper X,
                 proper isNePal X -> isNePal proper X,
                   proper isPal X -> isPal proper X,
                       proper a() -> ok a(),
                       proper e() -> ok e(),
                       proper i() -> ok i(),
                       proper o() -> ok o(),
                       proper u() -> ok u(),
                       top mark X -> top proper X,
                         top ok X -> top active X}
  UR:
   {               __(X1, mark X2) -> mark __(X1, X2),
                   __(mark X1, X2) -> mark __(X1, X2),
                  __(ok X1, ok X2) -> ok __(X1, X2),
               active __(X, nil()) -> mark X,
                 active __(X1, X2) -> __(X1, active X2),
                 active __(X1, X2) -> __(active X1, X2),
            active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
               active __(nil(), X) -> mark X,
                active and(X1, X2) -> and(active X1, X2),
               active and(tt(), X) -> mark X,
                 active isNeList V -> mark isQid V,
        active isNeList __(V1, V2) -> mark and(isNeList V1, isList V2),
        active isNeList __(V1, V2) -> mark and(isList V1, isNeList V2),
                   active isList V -> mark isNeList V,
          active isList __(V1, V2) -> mark and(isList V1, isList V2),
               active isList nil() -> mark tt(),
                  active isQid a() -> mark tt(),
                  active isQid e() -> mark tt(),
                  active isQid i() -> mark tt(),
                  active isQid o() -> mark tt(),
                  active isQid u() -> mark tt(),
                  active isNePal V -> mark isQid V,
    active isNePal __(I, __(P, I)) -> mark and(isQid I, isPal P),
                    active isPal V -> mark isNePal V,
                active isPal nil() -> mark tt(),
                  and(mark X1, X2) -> mark and(X1, X2),
                 and(ok X1, ok X2) -> ok and(X1, X2),
                     isNeList ok X -> ok isNeList X,
                       isList ok X -> ok isList X,
                        isQid ok X -> ok isQid X,
                      isNePal ok X -> ok isNePal X,
                        isPal ok X -> ok isPal X,
                 proper __(X1, X2) -> __(proper X1, proper X2),
                      proper nil() -> ok nil(),
                proper and(X1, X2) -> and(proper X1, proper X2),
                       proper tt() -> ok tt(),
                 proper isNeList X -> isNeList proper X,
                   proper isList X -> isList proper X,
                    proper isQid X -> isQid proper X,
                  proper isNePal X -> isNePal proper X,
                    proper isPal X -> isPal proper X,
                        proper a() -> ok a(),
                        proper e() -> ok e(),
                        proper i() -> ok i(),
                        proper o() -> ok o(),
                        proper u() -> ok u()}
   EDG:
    {
     (active# __(X1, X2) -> __#(X1, active X2), __#(ok X1, ok X2) -> __#(X1, X2))
     (active# __(X1, X2) -> __#(X1, active X2), __#(mark X1, X2) -> __#(X1, X2))
     (active# __(X1, X2) -> __#(X1, active X2), __#(X1, mark X2) -> __#(X1, X2))
     (active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2), and#(mark X1, X2) -> and#(X1, X2))
     (active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P), and#(mark X1, X2) -> and#(X1, X2))
     (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
     (isList# ok X -> isList# X, isList# ok X -> isList# X)
     (isNePal# ok X -> isNePal# X, isNePal# ok X -> isNePal# X)
     (proper# isNeList X -> proper# X, proper# isPal X -> proper# X)
     (proper# isNeList X -> proper# X, proper# isPal X -> isPal# proper X)
     (proper# isNeList X -> proper# X, proper# isNePal X -> proper# X)
     (proper# isNeList X -> proper# X, proper# isNePal X -> isNePal# proper X)
     (proper# isNeList X -> proper# X, proper# isQid X -> proper# X)
     (proper# isNeList X -> proper# X, proper# isQid X -> isQid# proper X)
     (proper# isNeList X -> proper# X, proper# isList X -> proper# X)
     (proper# isNeList X -> proper# X, proper# isList X -> isList# proper X)
     (proper# isNeList X -> proper# X, proper# isNeList X -> proper# X)
     (proper# isNeList X -> proper# X, proper# isNeList X -> isNeList# proper X)
     (proper# isNeList X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# isNeList X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# isNeList X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# isNeList X -> proper# X, proper# __(X1, X2) -> proper# X2)
     (proper# isNeList X -> proper# X, proper# __(X1, X2) -> proper# X1)
     (proper# isNeList X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (proper# isQid X -> proper# X, proper# isPal X -> proper# X)
     (proper# isQid X -> proper# X, proper# isPal X -> isPal# proper X)
     (proper# isQid X -> proper# X, proper# isNePal X -> proper# X)
     (proper# isQid X -> proper# X, proper# isNePal X -> isNePal# proper X)
     (proper# isQid X -> proper# X, proper# isQid X -> proper# X)
     (proper# isQid X -> proper# X, proper# isQid X -> isQid# proper X)
     (proper# isQid X -> proper# X, proper# isList X -> proper# X)
     (proper# isQid X -> proper# X, proper# isList X -> isList# proper X)
     (proper# isQid X -> proper# X, proper# isNeList X -> proper# X)
     (proper# isQid X -> proper# X, proper# isNeList X -> isNeList# proper X)
     (proper# isQid X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# isQid X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# isQid X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# isQid X -> proper# X, proper# __(X1, X2) -> proper# X2)
     (proper# isQid X -> proper# X, proper# __(X1, X2) -> proper# X1)
     (proper# isQid X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (proper# isPal X -> proper# X, proper# isPal X -> proper# X)
     (proper# isPal X -> proper# X, proper# isPal X -> isPal# proper X)
     (proper# isPal X -> proper# X, proper# isNePal X -> proper# X)
     (proper# isPal X -> proper# X, proper# isNePal X -> isNePal# proper X)
     (proper# isPal X -> proper# X, proper# isQid X -> proper# X)
     (proper# isPal X -> proper# X, proper# isQid X -> isQid# proper X)
     (proper# isPal X -> proper# X, proper# isList X -> proper# X)
     (proper# isPal X -> proper# X, proper# isList X -> isList# proper X)
     (proper# isPal X -> proper# X, proper# isNeList X -> proper# X)
     (proper# isPal X -> proper# X, proper# isNeList X -> isNeList# proper X)
     (proper# isPal X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# isPal X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# isPal X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# isPal X -> proper# X, proper# __(X1, X2) -> proper# X2)
     (proper# isPal X -> proper# X, proper# __(X1, X2) -> proper# X1)
     (proper# isPal X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (top# ok X -> active# X, active# isPal V -> isNePal# V)
     (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> isPal# P)
     (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> isQid# I)
     (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
     (top# ok X -> active# X, active# isNePal V -> isQid# V)
     (top# ok X -> active# X, active# isList __(V1, V2) -> isList# V2)
     (top# ok X -> active# X, active# isList __(V1, V2) -> isList# V1)
     (top# ok X -> active# X, active# isList __(V1, V2) -> and#(isList V1, isList V2))
     (top# ok X -> active# X, active# isList V -> isNeList# V)
     (top# ok X -> active# X, active# isNeList __(V1, V2) -> isList# V2)
     (top# ok X -> active# X, active# isNeList __(V1, V2) -> isList# V1)
     (top# ok X -> active# X, active# isNeList __(V1, V2) -> isNeList# V2)
     (top# ok X -> active# X, active# isNeList __(V1, V2) -> isNeList# V1)
     (top# ok X -> active# X, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
     (top# ok X -> active# X, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
     (top# ok X -> active# X, active# isNeList V -> isQid# V)
     (top# ok X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
     (top# ok X -> active# X, active# and(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z))
     (top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
     (top# ok X -> active# X, active# __(X1, X2) -> active# X2)
     (top# ok X -> active# X, active# __(X1, X2) -> active# X1)
     (top# ok X -> active# X, active# __(X1, X2) -> __#(active X1, X2))
     (top# ok X -> active# X, active# __(X1, X2) -> __#(X1, active X2))
     (active# isNeList __(V1, V2) -> isList# V1, isList# ok X -> isList# X)
     (active# __(X1, X2) -> __#(active X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
     (active# __(X1, X2) -> __#(active X1, X2), __#(mark X1, X2) -> __#(X1, X2))
     (active# __(X1, X2) -> __#(active X1, X2), __#(X1, mark X2) -> __#(X1, X2))
     (active# and(X1, X2) -> active# X1, active# isPal V -> isNePal# V)
     (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isPal# P)
     (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isQid# I)
     (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
     (active# and(X1, X2) -> active# X1, active# isNePal V -> isQid# V)
     (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V2)
     (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V1)
     (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> and#(isList V1, isList V2))
     (active# and(X1, X2) -> active# X1, active# isList V -> isNeList# V)
     (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V2)
     (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V1)
     (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V2)
     (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V1)
     (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
     (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
     (active# and(X1, X2) -> active# X1, active# isNeList V -> isQid# V)
     (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(Y, Z))
     (active# and(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
     (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2)
     (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> active# X1)
     (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> __#(active X1, X2))
     (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> __#(X1, active X2))
     (proper# __(X1, X2) -> proper# X1, proper# isPal X -> proper# X)
     (proper# __(X1, X2) -> proper# X1, proper# isPal X -> isPal# proper X)
     (proper# __(X1, X2) -> proper# X1, proper# isNePal X -> proper# X)
     (proper# __(X1, X2) -> proper# X1, proper# isNePal X -> isNePal# proper X)
     (proper# __(X1, X2) -> proper# X1, proper# isQid X -> proper# X)
     (proper# __(X1, X2) -> proper# X1, proper# isQid X -> isQid# proper X)
     (proper# __(X1, X2) -> proper# X1, proper# isList X -> proper# X)
     (proper# __(X1, X2) -> proper# X1, proper# isList X -> isList# proper X)
     (proper# __(X1, X2) -> proper# X1, proper# isNeList X -> proper# X)
     (proper# __(X1, X2) -> proper# X1, proper# isNeList X -> isNeList# proper X)
     (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2)
     (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X1)
     (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(ok X1, ok X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(mark X1, X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2))
     (__#(mark X1, X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
     (__#(mark X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
     (__#(mark X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (active# isNeList __(V1, V2) -> isNeList# V2, isNeList# ok X -> isNeList# X)
     (active# isList __(V1, V2) -> isList# V2, isList# ok X -> isList# X)
     (proper# __(X1, X2) -> proper# X2, proper# isPal X -> proper# X)
     (proper# __(X1, X2) -> proper# X2, proper# isPal X -> isPal# proper X)
     (proper# __(X1, X2) -> proper# X2, proper# isNePal X -> proper# X)
     (proper# __(X1, X2) -> proper# X2, proper# isNePal X -> isNePal# proper X)
     (proper# __(X1, X2) -> proper# X2, proper# isQid X -> proper# X)
     (proper# __(X1, X2) -> proper# X2, proper# isQid X -> isQid# proper X)
     (proper# __(X1, X2) -> proper# X2, proper# isList X -> proper# X)
     (proper# __(X1, X2) -> proper# X2, proper# isList X -> isList# proper X)
     (proper# __(X1, X2) -> proper# X2, proper# isNeList X -> proper# X)
     (proper# __(X1, X2) -> proper# X2, proper# isNeList X -> isNeList# proper X)
     (proper# __(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# __(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# __(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X2)
     (proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X1)
     (proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (proper# isNeList X -> isNeList# proper X, isNeList# ok X -> isNeList# X)
     (proper# isQid X -> isQid# proper X, isQid# ok X -> isQid# X)
     (proper# isPal X -> isPal# proper X, isPal# ok X -> isPal# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (active# __(__(X, Y), Z) -> __#(Y, Z), __#(ok X1, ok X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(Y, Z), __#(mark X1, X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, mark X2) -> __#(X1, X2))
     (active# isList V -> isNeList# V, isNeList# ok X -> isNeList# X)
     (active# isPal V -> isNePal# V, isNePal# ok X -> isNePal# X)
     (active# isNePal V -> isQid# V, isQid# ok X -> isQid# X)
     (active# isNeList V -> isQid# V, isQid# ok X -> isQid# X)
     (active# isNePal __(I, __(P, I)) -> isQid# I, isQid# ok X -> isQid# X)
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (proper# isNePal X -> isNePal# proper X, isNePal# ok X -> isNePal# X)
     (proper# isList X -> isList# proper X, isList# ok X -> isList# X)
     (proper# and(X1, X2) -> proper# X2, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X2, proper# isNeList X -> isNeList# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# isNeList X -> proper# X)
     (proper# and(X1, X2) -> proper# X2, proper# isList X -> isList# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# isList X -> proper# X)
     (proper# and(X1, X2) -> proper# X2, proper# isQid X -> isQid# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# isQid X -> proper# X)
     (proper# and(X1, X2) -> proper# X2, proper# isNePal X -> isNePal# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# isNePal X -> proper# X)
     (proper# and(X1, X2) -> proper# X2, proper# isPal X -> isPal# proper X)
     (proper# and(X1, X2) -> proper# X2, proper# isPal X -> proper# X)
     (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(X1, active X2))
     (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(active X1, X2))
     (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X1)
     (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X2)
     (active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
     (active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(Y, Z))
     (active# __(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
     (active# __(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
     (active# __(X1, X2) -> active# X2, active# isNeList V -> isQid# V)
     (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
     (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
     (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isNeList# V1)
     (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isNeList# V2)
     (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isList# V1)
     (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isList# V2)
     (active# __(X1, X2) -> active# X2, active# isList V -> isNeList# V)
     (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> and#(isList V1, isList V2))
     (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> isList# V1)
     (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> isList# V2)
     (active# __(X1, X2) -> active# X2, active# isNePal V -> isQid# V)
     (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
     (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> isQid# I)
     (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> isPal# P)
     (active# __(X1, X2) -> active# X2, active# isPal V -> isNePal# V)
     (active# isNeList __(V1, V2) -> isList# V2, isList# ok X -> isList# X)
     (and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (__#(ok X1, ok X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
     (__#(ok X1, ok X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
     (__#(ok X1, ok X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
     (__#(X1, mark X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
     (__#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
     (__#(X1, mark X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
     (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
     (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
     (proper# and(X1, X2) -> proper# X1, proper# isNeList X -> isNeList# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# isNeList X -> proper# X)
     (proper# and(X1, X2) -> proper# X1, proper# isList X -> isList# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# isList X -> proper# X)
     (proper# and(X1, X2) -> proper# X1, proper# isQid X -> isQid# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# isQid X -> proper# X)
     (proper# and(X1, X2) -> proper# X1, proper# isNePal X -> isNePal# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# isNePal X -> proper# X)
     (proper# and(X1, X2) -> proper# X1, proper# isPal X -> isPal# proper X)
     (proper# and(X1, X2) -> proper# X1, proper# isPal X -> proper# X)
     (active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(X1, active X2))
     (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(active X1, X2))
     (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X1)
     (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2)
     (active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
     (active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(Y, Z))
     (active# __(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
     (active# __(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
     (active# __(X1, X2) -> active# X1, active# isNeList V -> isQid# V)
     (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
     (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
     (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V1)
     (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V2)
     (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V1)
     (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V2)
     (active# __(X1, X2) -> active# X1, active# isList V -> isNeList# V)
     (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> and#(isList V1, isList V2))
     (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V1)
     (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V2)
     (active# __(X1, X2) -> active# X1, active# isNePal V -> isQid# V)
     (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
     (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isQid# I)
     (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isPal# P)
     (active# __(X1, X2) -> active# X1, active# isPal V -> isNePal# V)
     (active# isList __(V1, V2) -> isList# V1, isList# ok X -> isList# X)
     (active# isNeList __(V1, V2) -> isNeList# V1, isNeList# ok X -> isNeList# X)
     (top# mark X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# __(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# __(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (top# mark X -> proper# X, proper# isNeList X -> isNeList# proper X)
     (top# mark X -> proper# X, proper# isNeList X -> proper# X)
     (top# mark X -> proper# X, proper# isList X -> isList# proper X)
     (top# mark X -> proper# X, proper# isList X -> proper# X)
     (top# mark X -> proper# X, proper# isQid X -> isQid# proper X)
     (top# mark X -> proper# X, proper# isQid X -> proper# X)
     (top# mark X -> proper# X, proper# isNePal X -> isNePal# proper X)
     (top# mark X -> proper# X, proper# isNePal X -> proper# X)
     (top# mark X -> proper# X, proper# isPal X -> isPal# proper X)
     (top# mark X -> proper# X, proper# isPal X -> proper# X)
     (proper# isNePal X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (proper# isNePal X -> proper# X, proper# __(X1, X2) -> proper# X1)
     (proper# isNePal X -> proper# X, proper# __(X1, X2) -> proper# X2)
     (proper# isNePal X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# isNePal X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# isNePal X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# isNePal X -> proper# X, proper# isNeList X -> isNeList# proper X)
     (proper# isNePal X -> proper# X, proper# isNeList X -> proper# X)
     (proper# isNePal X -> proper# X, proper# isList X -> isList# proper X)
     (proper# isNePal X -> proper# X, proper# isList X -> proper# X)
     (proper# isNePal X -> proper# X, proper# isQid X -> isQid# proper X)
     (proper# isNePal X -> proper# X, proper# isQid X -> proper# X)
     (proper# isNePal X -> proper# X, proper# isNePal X -> isNePal# proper X)
     (proper# isNePal X -> proper# X, proper# isNePal X -> proper# X)
     (proper# isNePal X -> proper# X, proper# isPal X -> isPal# proper X)
     (proper# isNePal X -> proper# X, proper# isPal X -> proper# X)
     (proper# isList X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
     (proper# isList X -> proper# X, proper# __(X1, X2) -> proper# X1)
     (proper# isList X -> proper# X, proper# __(X1, X2) -> proper# X2)
     (proper# isList X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
     (proper# isList X -> proper# X, proper# and(X1, X2) -> proper# X1)
     (proper# isList X -> proper# X, proper# and(X1, X2) -> proper# X2)
     (proper# isList X -> proper# X, proper# isNeList X -> isNeList# proper X)
     (proper# isList X -> proper# X, proper# isNeList X -> proper# X)
     (proper# isList X -> proper# X, proper# isList X -> isList# proper X)
     (proper# isList X -> proper# X, proper# isList X -> proper# X)
     (proper# isList X -> proper# X, proper# isQid X -> isQid# proper X)
     (proper# isList X -> proper# X, proper# isQid X -> proper# X)
     (proper# isList X -> proper# X, proper# isNePal X -> isNePal# proper X)
     (proper# isList X -> proper# X, proper# isNePal X -> proper# X)
     (proper# isList X -> proper# X, proper# isPal X -> isPal# proper X)
     (proper# isList X -> proper# X, proper# isPal X -> proper# X)
     (isPal# ok X -> isPal# X, isPal# ok X -> isPal# X)
     (isQid# ok X -> isQid# X, isQid# ok X -> isQid# X)
     (isNeList# ok X -> isNeList# X, isNeList# ok X -> isNeList# X)
     (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(X1, mark X2) -> __#(X1, X2))
     (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(mark X1, X2) -> __#(X1, X2))
     (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(ok X1, ok X2) -> __#(X1, X2))
     (active# isList __(V1, V2) -> and#(isList V1, isList V2), and#(mark X1, X2) -> and#(X1, X2))
     (active# isList __(V1, V2) -> and#(isList V1, isList V2), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2), and#(mark X1, X2) -> and#(X1, X2))
     (active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# isNePal __(I, __(P, I)) -> isPal# P, isPal# ok X -> isPal# X)
    }
    EDG:
     {
      (active# __(X1, X2) -> __#(X1, active X2), __#(ok X1, ok X2) -> __#(X1, X2))
      (active# __(X1, X2) -> __#(X1, active X2), __#(mark X1, X2) -> __#(X1, X2))
      (active# __(X1, X2) -> __#(X1, active X2), __#(X1, mark X2) -> __#(X1, X2))
      (active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2), and#(ok X1, ok X2) -> and#(X1, X2))
      (active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2), and#(mark X1, X2) -> and#(X1, X2))
      (active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P), and#(ok X1, ok X2) -> and#(X1, X2))
      (active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P), and#(mark X1, X2) -> and#(X1, X2))
      (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
      (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(X1, X2))
      (isList# ok X -> isList# X, isList# ok X -> isList# X)
      (isNePal# ok X -> isNePal# X, isNePal# ok X -> isNePal# X)
      (proper# isNeList X -> proper# X, proper# isPal X -> proper# X)
      (proper# isNeList X -> proper# X, proper# isPal X -> isPal# proper X)
      (proper# isNeList X -> proper# X, proper# isNePal X -> proper# X)
      (proper# isNeList X -> proper# X, proper# isNePal X -> isNePal# proper X)
      (proper# isNeList X -> proper# X, proper# isQid X -> proper# X)
      (proper# isNeList X -> proper# X, proper# isQid X -> isQid# proper X)
      (proper# isNeList X -> proper# X, proper# isList X -> proper# X)
      (proper# isNeList X -> proper# X, proper# isList X -> isList# proper X)
      (proper# isNeList X -> proper# X, proper# isNeList X -> proper# X)
      (proper# isNeList X -> proper# X, proper# isNeList X -> isNeList# proper X)
      (proper# isNeList X -> proper# X, proper# and(X1, X2) -> proper# X2)
      (proper# isNeList X -> proper# X, proper# and(X1, X2) -> proper# X1)
      (proper# isNeList X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# isNeList X -> proper# X, proper# __(X1, X2) -> proper# X2)
      (proper# isNeList X -> proper# X, proper# __(X1, X2) -> proper# X1)
      (proper# isNeList X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (proper# isQid X -> proper# X, proper# isPal X -> proper# X)
      (proper# isQid X -> proper# X, proper# isPal X -> isPal# proper X)
      (proper# isQid X -> proper# X, proper# isNePal X -> proper# X)
      (proper# isQid X -> proper# X, proper# isNePal X -> isNePal# proper X)
      (proper# isQid X -> proper# X, proper# isQid X -> proper# X)
      (proper# isQid X -> proper# X, proper# isQid X -> isQid# proper X)
      (proper# isQid X -> proper# X, proper# isList X -> proper# X)
      (proper# isQid X -> proper# X, proper# isList X -> isList# proper X)
      (proper# isQid X -> proper# X, proper# isNeList X -> proper# X)
      (proper# isQid X -> proper# X, proper# isNeList X -> isNeList# proper X)
      (proper# isQid X -> proper# X, proper# and(X1, X2) -> proper# X2)
      (proper# isQid X -> proper# X, proper# and(X1, X2) -> proper# X1)
      (proper# isQid X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# isQid X -> proper# X, proper# __(X1, X2) -> proper# X2)
      (proper# isQid X -> proper# X, proper# __(X1, X2) -> proper# X1)
      (proper# isQid X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (proper# isPal X -> proper# X, proper# isPal X -> proper# X)
      (proper# isPal X -> proper# X, proper# isPal X -> isPal# proper X)
      (proper# isPal X -> proper# X, proper# isNePal X -> proper# X)
      (proper# isPal X -> proper# X, proper# isNePal X -> isNePal# proper X)
      (proper# isPal X -> proper# X, proper# isQid X -> proper# X)
      (proper# isPal X -> proper# X, proper# isQid X -> isQid# proper X)
      (proper# isPal X -> proper# X, proper# isList X -> proper# X)
      (proper# isPal X -> proper# X, proper# isList X -> isList# proper X)
      (proper# isPal X -> proper# X, proper# isNeList X -> proper# X)
      (proper# isPal X -> proper# X, proper# isNeList X -> isNeList# proper X)
      (proper# isPal X -> proper# X, proper# and(X1, X2) -> proper# X2)
      (proper# isPal X -> proper# X, proper# and(X1, X2) -> proper# X1)
      (proper# isPal X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# isPal X -> proper# X, proper# __(X1, X2) -> proper# X2)
      (proper# isPal X -> proper# X, proper# __(X1, X2) -> proper# X1)
      (proper# isPal X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (top# ok X -> active# X, active# isPal V -> isNePal# V)
      (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> isPal# P)
      (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> isQid# I)
      (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
      (top# ok X -> active# X, active# isNePal V -> isQid# V)
      (top# ok X -> active# X, active# isList __(V1, V2) -> isList# V2)
      (top# ok X -> active# X, active# isList __(V1, V2) -> isList# V1)
      (top# ok X -> active# X, active# isList __(V1, V2) -> and#(isList V1, isList V2))
      (top# ok X -> active# X, active# isList V -> isNeList# V)
      (top# ok X -> active# X, active# isNeList __(V1, V2) -> isList# V2)
      (top# ok X -> active# X, active# isNeList __(V1, V2) -> isList# V1)
      (top# ok X -> active# X, active# isNeList __(V1, V2) -> isNeList# V2)
      (top# ok X -> active# X, active# isNeList __(V1, V2) -> isNeList# V1)
      (top# ok X -> active# X, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
      (top# ok X -> active# X, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
      (top# ok X -> active# X, active# isNeList V -> isQid# V)
      (top# ok X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
      (top# ok X -> active# X, active# and(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z))
      (top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
      (top# ok X -> active# X, active# __(X1, X2) -> active# X2)
      (top# ok X -> active# X, active# __(X1, X2) -> active# X1)
      (top# ok X -> active# X, active# __(X1, X2) -> __#(active X1, X2))
      (top# ok X -> active# X, active# __(X1, X2) -> __#(X1, active X2))
      (active# isNeList __(V1, V2) -> isList# V1, isList# ok X -> isList# X)
      (active# __(X1, X2) -> __#(active X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
      (active# __(X1, X2) -> __#(active X1, X2), __#(mark X1, X2) -> __#(X1, X2))
      (active# __(X1, X2) -> __#(active X1, X2), __#(X1, mark X2) -> __#(X1, X2))
      (active# and(X1, X2) -> active# X1, active# isPal V -> isNePal# V)
      (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isPal# P)
      (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isQid# I)
      (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
      (active# and(X1, X2) -> active# X1, active# isNePal V -> isQid# V)
      (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V2)
      (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V1)
      (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> and#(isList V1, isList V2))
      (active# and(X1, X2) -> active# X1, active# isList V -> isNeList# V)
      (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V2)
      (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V1)
      (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V2)
      (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V1)
      (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
      (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
      (active# and(X1, X2) -> active# X1, active# isNeList V -> isQid# V)
      (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
      (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
      (active# and(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(Y, Z))
      (active# and(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
      (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2)
      (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> active# X1)
      (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> __#(active X1, X2))
      (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> __#(X1, active X2))
      (proper# __(X1, X2) -> proper# X1, proper# isPal X -> proper# X)
      (proper# __(X1, X2) -> proper# X1, proper# isPal X -> isPal# proper X)
      (proper# __(X1, X2) -> proper# X1, proper# isNePal X -> proper# X)
      (proper# __(X1, X2) -> proper# X1, proper# isNePal X -> isNePal# proper X)
      (proper# __(X1, X2) -> proper# X1, proper# isQid X -> proper# X)
      (proper# __(X1, X2) -> proper# X1, proper# isQid X -> isQid# proper X)
      (proper# __(X1, X2) -> proper# X1, proper# isList X -> proper# X)
      (proper# __(X1, X2) -> proper# X1, proper# isList X -> isList# proper X)
      (proper# __(X1, X2) -> proper# X1, proper# isNeList X -> proper# X)
      (proper# __(X1, X2) -> proper# X1, proper# isNeList X -> isNeList# proper X)
      (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
      (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
      (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2)
      (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X1)
      (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(ok X1, ok X2) -> __#(X1, X2))
      (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(mark X1, X2) -> __#(X1, X2))
      (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2))
      (__#(mark X1, X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
      (__#(mark X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
      (__#(mark X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
      (and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
      (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
      (active# isNeList __(V1, V2) -> isNeList# V2, isNeList# ok X -> isNeList# X)
      (active# isList __(V1, V2) -> isList# V2, isList# ok X -> isList# X)
      (proper# __(X1, X2) -> proper# X2, proper# isPal X -> proper# X)
      (proper# __(X1, X2) -> proper# X2, proper# isPal X -> isPal# proper X)
      (proper# __(X1, X2) -> proper# X2, proper# isNePal X -> proper# X)
      (proper# __(X1, X2) -> proper# X2, proper# isNePal X -> isNePal# proper X)
      (proper# __(X1, X2) -> proper# X2, proper# isQid X -> proper# X)
      (proper# __(X1, X2) -> proper# X2, proper# isQid X -> isQid# proper X)
      (proper# __(X1, X2) -> proper# X2, proper# isList X -> proper# X)
      (proper# __(X1, X2) -> proper# X2, proper# isList X -> isList# proper X)
      (proper# __(X1, X2) -> proper# X2, proper# isNeList X -> proper# X)
      (proper# __(X1, X2) -> proper# X2, proper# isNeList X -> isNeList# proper X)
      (proper# __(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
      (proper# __(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
      (proper# __(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X2)
      (proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X1)
      (proper# __(X1, X2) -> proper# X2, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (proper# isNeList X -> isNeList# proper X, isNeList# ok X -> isNeList# X)
      (proper# isQid X -> isQid# proper X, isQid# ok X -> isQid# X)
      (proper# isPal X -> isPal# proper X, isPal# ok X -> isPal# X)
      (top# ok X -> top# active X, top# ok X -> top# active X)
      (top# ok X -> top# active X, top# ok X -> active# X)
      (top# ok X -> top# active X, top# mark X -> top# proper X)
      (top# ok X -> top# active X, top# mark X -> proper# X)
      (active# __(__(X, Y), Z) -> __#(Y, Z), __#(ok X1, ok X2) -> __#(X1, X2))
      (active# __(__(X, Y), Z) -> __#(Y, Z), __#(mark X1, X2) -> __#(X1, X2))
      (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, mark X2) -> __#(X1, X2))
      (active# isList V -> isNeList# V, isNeList# ok X -> isNeList# X)
      (active# isPal V -> isNePal# V, isNePal# ok X -> isNePal# X)
      (active# isNePal V -> isQid# V, isQid# ok X -> isQid# X)
      (active# isNeList V -> isQid# V, isQid# ok X -> isQid# X)
      (active# isNePal __(I, __(P, I)) -> isQid# I, isQid# ok X -> isQid# X)
      (top# mark X -> top# proper X, top# mark X -> proper# X)
      (top# mark X -> top# proper X, top# mark X -> top# proper X)
      (top# mark X -> top# proper X, top# ok X -> active# X)
      (top# mark X -> top# proper X, top# ok X -> top# active X)
      (proper# isNePal X -> isNePal# proper X, isNePal# ok X -> isNePal# X)
      (proper# isList X -> isList# proper X, isList# ok X -> isList# X)
      (proper# and(X1, X2) -> proper# X2, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (proper# and(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X2, proper# __(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X2, proper# isNeList X -> isNeList# proper X)
      (proper# and(X1, X2) -> proper# X2, proper# isNeList X -> proper# X)
      (proper# and(X1, X2) -> proper# X2, proper# isList X -> isList# proper X)
      (proper# and(X1, X2) -> proper# X2, proper# isList X -> proper# X)
      (proper# and(X1, X2) -> proper# X2, proper# isQid X -> isQid# proper X)
      (proper# and(X1, X2) -> proper# X2, proper# isQid X -> proper# X)
      (proper# and(X1, X2) -> proper# X2, proper# isNePal X -> isNePal# proper X)
      (proper# and(X1, X2) -> proper# X2, proper# isNePal X -> proper# X)
      (proper# and(X1, X2) -> proper# X2, proper# isPal X -> isPal# proper X)
      (proper# and(X1, X2) -> proper# X2, proper# isPal X -> proper# X)
      (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(X1, active X2))
      (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(active X1, X2))
      (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X1)
      (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X2)
      (active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
      (active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(Y, Z))
      (active# __(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
      (active# __(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
      (active# __(X1, X2) -> active# X2, active# isNeList V -> isQid# V)
      (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
      (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
      (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isNeList# V1)
      (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isNeList# V2)
      (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isList# V1)
      (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isList# V2)
      (active# __(X1, X2) -> active# X2, active# isList V -> isNeList# V)
      (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> and#(isList V1, isList V2))
      (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> isList# V1)
      (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> isList# V2)
      (active# __(X1, X2) -> active# X2, active# isNePal V -> isQid# V)
      (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
      (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> isQid# I)
      (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> isPal# P)
      (active# __(X1, X2) -> active# X2, active# isPal V -> isNePal# V)
      (active# isNeList __(V1, V2) -> isList# V2, isList# ok X -> isList# X)
      (and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2))
      (and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
      (__#(ok X1, ok X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
      (__#(ok X1, ok X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
      (__#(ok X1, ok X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
      (__#(X1, mark X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2))
      (__#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2))
      (__#(X1, mark X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
      (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1)
      (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2)
      (proper# and(X1, X2) -> proper# X1, proper# isNeList X -> isNeList# proper X)
      (proper# and(X1, X2) -> proper# X1, proper# isNeList X -> proper# X)
      (proper# and(X1, X2) -> proper# X1, proper# isList X -> isList# proper X)
      (proper# and(X1, X2) -> proper# X1, proper# isList X -> proper# X)
      (proper# and(X1, X2) -> proper# X1, proper# isQid X -> isQid# proper X)
      (proper# and(X1, X2) -> proper# X1, proper# isQid X -> proper# X)
      (proper# and(X1, X2) -> proper# X1, proper# isNePal X -> isNePal# proper X)
      (proper# and(X1, X2) -> proper# X1, proper# isNePal X -> proper# X)
      (proper# and(X1, X2) -> proper# X1, proper# isPal X -> isPal# proper X)
      (proper# and(X1, X2) -> proper# X1, proper# isPal X -> proper# X)
      (active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
      (active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
      (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(X1, active X2))
      (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(active X1, X2))
      (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X1)
      (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2)
      (active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
      (active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(Y, Z))
      (active# __(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
      (active# __(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
      (active# __(X1, X2) -> active# X1, active# isNeList V -> isQid# V)
      (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
      (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
      (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V1)
      (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V2)
      (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V1)
      (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V2)
      (active# __(X1, X2) -> active# X1, active# isList V -> isNeList# V)
      (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> and#(isList V1, isList V2))
      (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V1)
      (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V2)
      (active# __(X1, X2) -> active# X1, active# isNePal V -> isQid# V)
      (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
      (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isQid# I)
      (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isPal# P)
      (active# __(X1, X2) -> active# X1, active# isPal V -> isNePal# V)
      (active# isList __(V1, V2) -> isList# V1, isList# ok X -> isList# X)
      (active# isNeList __(V1, V2) -> isNeList# V1, isNeList# ok X -> isNeList# X)
      (top# mark X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# __(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# __(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X1)
      (top# mark X -> proper# X, proper# and(X1, X2) -> proper# X2)
      (top# mark X -> proper# X, proper# isNeList X -> isNeList# proper X)
      (top# mark X -> proper# X, proper# isNeList X -> proper# X)
      (top# mark X -> proper# X, proper# isList X -> isList# proper X)
      (top# mark X -> proper# X, proper# isList X -> proper# X)
      (top# mark X -> proper# X, proper# isQid X -> isQid# proper X)
      (top# mark X -> proper# X, proper# isQid X -> proper# X)
      (top# mark X -> proper# X, proper# isNePal X -> isNePal# proper X)
      (top# mark X -> proper# X, proper# isNePal X -> proper# X)
      (top# mark X -> proper# X, proper# isPal X -> isPal# proper X)
      (top# mark X -> proper# X, proper# isPal X -> proper# X)
      (proper# isNePal X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (proper# isNePal X -> proper# X, proper# __(X1, X2) -> proper# X1)
      (proper# isNePal X -> proper# X, proper# __(X1, X2) -> proper# X2)
      (proper# isNePal X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# isNePal X -> proper# X, proper# and(X1, X2) -> proper# X1)
      (proper# isNePal X -> proper# X, proper# and(X1, X2) -> proper# X2)
      (proper# isNePal X -> proper# X, proper# isNeList X -> isNeList# proper X)
      (proper# isNePal X -> proper# X, proper# isNeList X -> proper# X)
      (proper# isNePal X -> proper# X, proper# isList X -> isList# proper X)
      (proper# isNePal X -> proper# X, proper# isList X -> proper# X)
      (proper# isNePal X -> proper# X, proper# isQid X -> isQid# proper X)
      (proper# isNePal X -> proper# X, proper# isQid X -> proper# X)
      (proper# isNePal X -> proper# X, proper# isNePal X -> isNePal# proper X)
      (proper# isNePal X -> proper# X, proper# isNePal X -> proper# X)
      (proper# isNePal X -> proper# X, proper# isPal X -> isPal# proper X)
      (proper# isNePal X -> proper# X, proper# isPal X -> proper# X)
      (proper# isList X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2))
      (proper# isList X -> proper# X, proper# __(X1, X2) -> proper# X1)
      (proper# isList X -> proper# X, proper# __(X1, X2) -> proper# X2)
      (proper# isList X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2))
      (proper# isList X -> proper# X, proper# and(X1, X2) -> proper# X1)
      (proper# isList X -> proper# X, proper# and(X1, X2) -> proper# X2)
      (proper# isList X -> proper# X, proper# isNeList X -> isNeList# proper X)
      (proper# isList X -> proper# X, proper# isNeList X -> proper# X)
      (proper# isList X -> proper# X, proper# isList X -> isList# proper X)
      (proper# isList X -> proper# X, proper# isList X -> proper# X)
      (proper# isList X -> proper# X, proper# isQid X -> isQid# proper X)
      (proper# isList X -> proper# X, proper# isQid X -> proper# X)
      (proper# isList X -> proper# X, proper# isNePal X -> isNePal# proper X)
      (proper# isList X -> proper# X, proper# isNePal X -> proper# X)
      (proper# isList X -> proper# X, proper# isPal X -> isPal# proper X)
      (proper# isList X -> proper# X, proper# isPal X -> proper# X)
      (isPal# ok X -> isPal# X, isPal# ok X -> isPal# X)
      (isQid# ok X -> isQid# X, isQid# ok X -> isQid# X)
      (isNeList# ok X -> isNeList# X, isNeList# ok X -> isNeList# X)
      (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(X1, mark X2) -> __#(X1, X2))
      (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(mark X1, X2) -> __#(X1, X2))
      (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(ok X1, ok X2) -> __#(X1, X2))
      (active# isList __(V1, V2) -> and#(isList V1, isList V2), and#(mark X1, X2) -> and#(X1, X2))
      (active# isList __(V1, V2) -> and#(isList V1, isList V2), and#(ok X1, ok X2) -> and#(X1, X2))
      (active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2), and#(mark X1, X2) -> and#(X1, X2))
      (active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2), and#(ok X1, ok X2) -> and#(X1, X2))
      (active# isNePal __(I, __(P, I)) -> isPal# P, isPal# ok X -> isPal# X)
     }
     EDG:
      {(active# __(X1, X2) -> __#(X1, active X2), __#(ok X1, ok X2) -> __#(X1, X2))
       (active# __(X1, X2) -> __#(X1, active X2), __#(X1, mark X2) -> __#(X1, X2))
       (active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2), and#(ok X1, ok X2) -> and#(X1, X2))
       (active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P), and#(ok X1, ok X2) -> and#(X1, X2))
       (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
       (top# ok X -> active# X, active# isPal V -> isNePal# V)
       (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> isPal# P)
       (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> isQid# I)
       (top# ok X -> active# X, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
       (top# ok X -> active# X, active# isNePal V -> isQid# V)
       (top# ok X -> active# X, active# isList __(V1, V2) -> isList# V2)
       (top# ok X -> active# X, active# isList __(V1, V2) -> isList# V1)
       (top# ok X -> active# X, active# isList __(V1, V2) -> and#(isList V1, isList V2))
       (top# ok X -> active# X, active# isList V -> isNeList# V)
       (top# ok X -> active# X, active# isNeList __(V1, V2) -> isList# V2)
       (top# ok X -> active# X, active# isNeList __(V1, V2) -> isList# V1)
       (top# ok X -> active# X, active# isNeList __(V1, V2) -> isNeList# V2)
       (top# ok X -> active# X, active# isNeList __(V1, V2) -> isNeList# V1)
       (top# ok X -> active# X, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
       (top# ok X -> active# X, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
       (top# ok X -> active# X, active# isNeList V -> isQid# V)
       (top# ok X -> active# X, active# and(X1, X2) -> and#(active X1, X2))
       (top# ok X -> active# X, active# and(X1, X2) -> active# X1)
       (top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z))
       (top# ok X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
       (top# ok X -> active# X, active# __(X1, X2) -> active# X2)
       (top# ok X -> active# X, active# __(X1, X2) -> active# X1)
       (top# ok X -> active# X, active# __(X1, X2) -> __#(active X1, X2))
       (top# ok X -> active# X, active# __(X1, X2) -> __#(X1, active X2))
       (active# __(X1, X2) -> __#(active X1, X2), __#(ok X1, ok X2) -> __#(X1, X2))
       (active# __(X1, X2) -> __#(active X1, X2), __#(mark X1, X2) -> __#(X1, X2))
       (active# and(X1, X2) -> active# X1, active# isPal V -> isNePal# V)
       (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isPal# P)
       (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isQid# I)
       (active# and(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
       (active# and(X1, X2) -> active# X1, active# isNePal V -> isQid# V)
       (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V2)
       (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V1)
       (active# and(X1, X2) -> active# X1, active# isList __(V1, V2) -> and#(isList V1, isList V2))
       (active# and(X1, X2) -> active# X1, active# isList V -> isNeList# V)
       (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V2)
       (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V1)
       (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V2)
       (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V1)
       (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
       (active# and(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
       (active# and(X1, X2) -> active# X1, active# isNeList V -> isQid# V)
       (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
       (active# and(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
       (active# and(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(Y, Z))
       (active# and(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
       (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2)
       (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> active# X1)
       (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> __#(active X1, X2))
       (active# and(X1, X2) -> active# X1, active# __(X1, X2) -> __#(X1, active X2))
       (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2))
       (proper# isNeList X -> isNeList# proper X, isNeList# ok X -> isNeList# X)
       (proper# isQid X -> isQid# proper X, isQid# ok X -> isQid# X)
       (proper# isPal X -> isPal# proper X, isPal# ok X -> isPal# X)
       (top# ok X -> top# active X, top# ok X -> top# active X)
       (top# ok X -> top# active X, top# ok X -> active# X)
       (top# ok X -> top# active X, top# mark X -> top# proper X)
       (top# ok X -> top# active X, top# mark X -> proper# X)
       (top# mark X -> top# proper X, top# mark X -> proper# X)
       (top# mark X -> top# proper X, top# mark X -> top# proper X)
       (top# mark X -> top# proper X, top# ok X -> active# X)
       (top# mark X -> top# proper X, top# ok X -> top# active X)
       (proper# isNePal X -> isNePal# proper X, isNePal# ok X -> isNePal# X)
       (proper# isList X -> isList# proper X, isList# ok X -> isList# X)
       (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(X1, active X2))
       (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(active X1, X2))
       (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X1)
       (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X2)
       (active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
       (active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(Y, Z))
       (active# __(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1)
       (active# __(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2))
       (active# __(X1, X2) -> active# X2, active# isNeList V -> isQid# V)
       (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
       (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
       (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isNeList# V1)
       (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isNeList# V2)
       (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isList# V1)
       (active# __(X1, X2) -> active# X2, active# isNeList __(V1, V2) -> isList# V2)
       (active# __(X1, X2) -> active# X2, active# isList V -> isNeList# V)
       (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> and#(isList V1, isList V2))
       (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> isList# V1)
       (active# __(X1, X2) -> active# X2, active# isList __(V1, V2) -> isList# V2)
       (active# __(X1, X2) -> active# X2, active# isNePal V -> isQid# V)
       (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
       (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> isQid# I)
       (active# __(X1, X2) -> active# X2, active# isNePal __(I, __(P, I)) -> isPal# P)
       (active# __(X1, X2) -> active# X2, active# isPal V -> isNePal# V)
       (active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
       (active# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2))
       (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(X1, active X2))
       (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> __#(active X1, X2))
       (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X1)
       (active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2)
       (active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(X, __(Y, Z)))
       (active# __(X1, X2) -> active# X1, active# __(__(X, Y), Z) -> __#(Y, Z))
       (active# __(X1, X2) -> active# X1, active# and(X1, X2) -> active# X1)
       (active# __(X1, X2) -> active# X1, active# and(X1, X2) -> and#(active X1, X2))
       (active# __(X1, X2) -> active# X1, active# isNeList V -> isQid# V)
       (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2))
       (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> and#(isList V1, isNeList V2))
       (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V1)
       (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isNeList# V2)
       (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V1)
       (active# __(X1, X2) -> active# X1, active# isNeList __(V1, V2) -> isList# V2)
       (active# __(X1, X2) -> active# X1, active# isList V -> isNeList# V)
       (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> and#(isList V1, isList V2))
       (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V1)
       (active# __(X1, X2) -> active# X1, active# isList __(V1, V2) -> isList# V2)
       (active# __(X1, X2) -> active# X1, active# isNePal V -> isQid# V)
       (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> and#(isQid I, isPal P))
       (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isQid# I)
       (active# __(X1, X2) -> active# X1, active# isNePal __(I, __(P, I)) -> isPal# P)
       (active# __(X1, X2) -> active# X1, active# isPal V -> isNePal# V)
       (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(ok X1, ok X2) -> __#(X1, X2))
       (active# isList __(V1, V2) -> and#(isList V1, isList V2), and#(ok X1, ok X2) -> and#(X1, X2))
       (active# isNeList __(V1, V2) -> and#(isNeList V1, isList V2), and#(ok X1, ok X2) -> and#(X1, X2))}
      STATUS:
       arrows: 0.960219
       SCCS (2):
        Scc:
         {top# mark X -> top# proper X,
            top# ok X -> top# active X}
        Scc:
         { active# __(X1, X2) -> active# X1,
           active# __(X1, X2) -> active# X2,
          active# and(X1, X2) -> active# X1}
        
        SCC (2):
         Strict:
          {top# mark X -> top# proper X,
             top# ok X -> top# active X}
         Weak:
         {               __(X1, mark X2) -> mark __(X1, X2),
                         __(mark X1, X2) -> mark __(X1, X2),
                        __(ok X1, ok X2) -> ok __(X1, X2),
                     active __(X, nil()) -> mark X,
                       active __(X1, X2) -> __(X1, active X2),
                       active __(X1, X2) -> __(active X1, X2),
                  active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
                     active __(nil(), X) -> mark X,
                      active and(X1, X2) -> and(active X1, X2),
                     active and(tt(), X) -> mark X,
                       active isNeList V -> mark isQid V,
              active isNeList __(V1, V2) -> mark and(isNeList V1, isList V2),
              active isNeList __(V1, V2) -> mark and(isList V1, isNeList V2),
                         active isList V -> mark isNeList V,
                active isList __(V1, V2) -> mark and(isList V1, isList V2),
                     active isList nil() -> mark tt(),
                        active isQid a() -> mark tt(),
                        active isQid e() -> mark tt(),
                        active isQid i() -> mark tt(),
                        active isQid o() -> mark tt(),
                        active isQid u() -> mark tt(),
                        active isNePal V -> mark isQid V,
          active isNePal __(I, __(P, I)) -> mark and(isQid I, isPal P),
                          active isPal V -> mark isNePal V,
                      active isPal nil() -> mark tt(),
                        and(mark X1, X2) -> mark and(X1, X2),
                       and(ok X1, ok X2) -> ok and(X1, X2),
                           isNeList ok X -> ok isNeList X,
                             isList ok X -> ok isList X,
                              isQid ok X -> ok isQid X,
                            isNePal ok X -> ok isNePal X,
                              isPal ok X -> ok isPal X,
                       proper __(X1, X2) -> __(proper X1, proper X2),
                            proper nil() -> ok nil(),
                      proper and(X1, X2) -> and(proper X1, proper X2),
                             proper tt() -> ok tt(),
                       proper isNeList X -> isNeList proper X,
                         proper isList X -> isList proper X,
                          proper isQid X -> isQid proper X,
                        proper isNePal X -> isNePal proper X,
                          proper isPal X -> isPal proper X,
                              proper a() -> ok a(),
                              proper e() -> ok e(),
                              proper i() -> ok i(),
                              proper o() -> ok o(),
                              proper u() -> ok u(),
                              top mark X -> top proper X,
                                top ok X -> top active X}
         Open
        
        
        
        
        
        
        
        
        
        
        SCC (3):
         Strict:
          { active# __(X1, X2) -> active# X1,
            active# __(X1, X2) -> active# X2,
           active# and(X1, X2) -> active# X1}
         Weak:
         {               __(X1, mark X2) -> mark __(X1, X2),
                         __(mark X1, X2) -> mark __(X1, X2),
                        __(ok X1, ok X2) -> ok __(X1, X2),
                     active __(X, nil()) -> mark X,
                       active __(X1, X2) -> __(X1, active X2),
                       active __(X1, X2) -> __(active X1, X2),
                  active __(__(X, Y), Z) -> mark __(X, __(Y, Z)),
                     active __(nil(), X) -> mark X,
                      active and(X1, X2) -> and(active X1, X2),
                     active and(tt(), X) -> mark X,
                       active isNeList V -> mark isQid V,
              active isNeList __(V1, V2) -> mark and(isNeList V1, isList V2),
              active isNeList __(V1, V2) -> mark and(isList V1, isNeList V2),
                         active isList V -> mark isNeList V,
                active isList __(V1, V2) -> mark and(isList V1, isList V2),
                     active isList nil() -> mark tt(),
                        active isQid a() -> mark tt(),
                        active isQid e() -> mark tt(),
                        active isQid i() -> mark tt(),
                        active isQid o() -> mark tt(),
                        active isQid u() -> mark tt(),
                        active isNePal V -> mark isQid V,
          active isNePal __(I, __(P, I)) -> mark and(isQid I, isPal P),
                          active isPal V -> mark isNePal V,
                      active isPal nil() -> mark tt(),
                        and(mark X1, X2) -> mark and(X1, X2),
                       and(ok X1, ok X2) -> ok and(X1, X2),
                           isNeList ok X -> ok isNeList X,
                             isList ok X -> ok isList X,
                              isQid ok X -> ok isQid X,
                            isNePal ok X -> ok isNePal X,
                              isPal ok X -> ok isPal X,
                       proper __(X1, X2) -> __(proper X1, proper X2),
                            proper nil() -> ok nil(),
                      proper and(X1, X2) -> and(proper X1, proper X2),
                             proper tt() -> ok tt(),
                       proper isNeList X -> isNeList proper X,
                         proper isList X -> isList proper X,
                          proper isQid X -> isQid proper X,
                        proper isNePal X -> isNePal proper X,
                          proper isPal X -> isPal proper X,
                              proper a() -> ok a(),
                              proper e() -> ok e(),
                              proper i() -> ok i(),
                              proper o() -> ok o(),
                              proper u() -> ok u(),
                              top mark X -> top proper X,
                                top ok X -> top active X}
         Open