MAYBE
Time: 0.108530
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 isNePal X -> isNePal active X,
  active isNePal __(I, __(P, I)) -> mark tt(),
                and(mark X1, X2) -> mark and(X1, X2),
               and(ok X1, ok X2) -> ok and(X1, X2),
                  isNePal mark X -> mark isNePal X,
                    isNePal ok X -> ok isNePal 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 isNePal X -> isNePal proper X,
                      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# isNePal X -> active# X,
          active# isNePal X -> isNePal# active X,
          and#(mark X1, X2) -> and#(X1, X2),
         and#(ok X1, ok X2) -> and#(X1, X2),
            isNePal# mark X -> isNePal# X,
              isNePal# ok X -> isNePal# 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# isNePal X -> isNePal# proper X,
          proper# isNePal 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 isNePal X -> isNePal active X,
   active isNePal __(I, __(P, I)) -> mark tt(),
                 and(mark X1, X2) -> mark and(X1, X2),
                and(ok X1, ok X2) -> ok and(X1, X2),
                   isNePal mark X -> mark isNePal X,
                     isNePal ok X -> ok isNePal 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 isNePal X -> isNePal proper X,
                       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 isNePal X -> isNePal active X,
    active isNePal __(I, __(P, I)) -> mark tt(),
                  and(mark X1, X2) -> mark and(X1, X2),
                 and(ok X1, ok X2) -> ok and(X1, X2),
                    isNePal mark X -> mark isNePal X,
                      isNePal ok X -> ok isNePal 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 isNePal X -> isNePal proper X}
   EDG:
    {(active# and(X1, X2) -> and#(active X1, X2), and#(mark X1, X2) -> and#(X1, X2))
     (active# isNePal X -> isNePal# active X, isNePal# ok X -> isNePal# X)
     (active# isNePal X -> isNePal# active X, isNePal# mark X -> isNePal# X)
     (top# mark X -> top# proper X, top# ok X -> top# active X)
     (top# mark X -> top# proper X, top# ok X -> active# X)
     (top# mark X -> top# proper X, top# mark X -> top# proper X)
     (top# mark X -> top# proper X, top# mark X -> proper# X)
     (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(ok X1, ok X2) -> __#(X1, X2))
     (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2))
     (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(ok X1, ok X2) -> and#(X1, X2))
     (active# __(X1, X2) -> __#(X1, active X2), __#(X1, mark X2) -> __#(X1, X2))
     (top# ok X -> top# active X, top# mark X -> proper# X)
     (top# ok X -> top# active X, top# mark X -> top# proper X)
     (top# ok X -> top# active X, top# ok X -> active# X)
     (top# ok X -> top# active X, top# ok X -> top# active X)
     (proper# isNePal X -> isNePal# proper X, isNePal# ok X -> isNePal# X)
     (active# __(X1, X2) -> __#(active X1, X2), __#(mark X1, X2) -> __#(X1, X2))}
    STATUS:
     arrows: 0.979786
     SCCS (1):
      Scc:
       {top# mark X -> top# proper X,
          top# ok X -> top# active X}
      
      
      
      
      
      
      
      
      
      
      
      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 isNePal X -> isNePal active X,
        active isNePal __(I, __(P, I)) -> mark tt(),
                      and(mark X1, X2) -> mark and(X1, X2),
                     and(ok X1, ok X2) -> ok and(X1, X2),
                        isNePal mark X -> mark isNePal X,
                          isNePal ok X -> ok isNePal 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 isNePal X -> isNePal proper X,
                            top mark X -> top proper X,
                              top ok X -> top active X}
       Open