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