MAYBE Time: 0.055111 TRS: { mark __(X1, X2) -> active __(mark X1, mark X2), mark nil() -> active nil(), mark U12 X -> active U12 mark X, mark tt() -> active tt(), mark U11 X -> active U11 mark X, 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 U12 tt() -> mark tt(), active U11 tt() -> mark U12 tt(), active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> U12 X, U12 active X -> U12 X, U11 mark X -> U11 X, U11 active X -> U11 X, 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# U12 X -> mark# X, mark# U12 X -> active# U12 mark X, mark# U12 X -> U12# mark X, mark# tt() -> active# tt(), mark# U11 X -> mark# X, mark# U11 X -> active# U11 mark X, mark# U11 X -> U11# mark X, 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# U12 tt() -> mark# tt(), active# U11 tt() -> mark# U12 tt(), active# U11 tt() -> U12# tt(), active# isNePal __(I, __(P, I)) -> mark# U11 tt(), active# isNePal __(I, __(P, I)) -> U11# tt(), U12# mark X -> U12# X, U12# active X -> U12# X, U11# mark X -> U11# X, U11# active X -> U11# X, isNePal# mark X -> isNePal# X, isNePal# active X -> isNePal# X} TRS: { mark __(X1, X2) -> active __(mark X1, mark X2), mark nil() -> active nil(), mark U12 X -> active U12 mark X, mark tt() -> active tt(), mark U11 X -> active U11 mark X, 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 U12 tt() -> mark tt(), active U11 tt() -> mark U12 tt(), active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> U12 X, U12 active X -> U12 X, U11 mark X -> U11 X, U11 active X -> U11 X, isNePal mark X -> isNePal X, isNePal active X -> isNePal X} UR: { mark __(X1, X2) -> active __(mark X1, mark X2), mark nil() -> active nil(), mark U12 X -> active U12 mark X, mark tt() -> active tt(), mark U11 X -> active U11 mark X, 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 U12 tt() -> mark tt(), active U11 tt() -> mark U12 tt(), active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> U12 X, U12 active X -> U12 X, U11 mark X -> U11 X, U11 active X -> U11 X, isNePal mark X -> isNePal X, isNePal active X -> isNePal X} EDG: { (active# __(__(X, Y), Z) -> __#(Y, Z), __#(active X1, X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(mark X1, X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, active X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, mark X2) -> __#(X1, X2)) (mark# tt() -> active# tt(), active# isNePal __(I, __(P, I)) -> U11# tt()) (mark# tt() -> active# tt(), active# isNePal __(I, __(P, I)) -> mark# U11 tt()) (mark# tt() -> active# tt(), active# U11 tt() -> U12# tt()) (mark# tt() -> active# tt(), active# U11 tt() -> mark# U12 tt()) (mark# tt() -> active# tt(), active# U12 tt() -> mark# tt()) (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) (active# U11 tt() -> U12# tt(), U12# active X -> U12# X) (active# U11 tt() -> U12# tt(), U12# mark X -> U12# X) (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> isNePal# mark X) (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> active# isNePal mark X) (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# U11 X -> U11# mark X) (mark# __(X1, X2) -> mark# X1, mark# U11 X -> active# U11 mark X) (mark# __(X1, X2) -> mark# X1, mark# U11 X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# tt() -> active# tt()) (mark# __(X1, X2) -> mark# X1, mark# U12 X -> U12# mark X) (mark# __(X1, X2) -> mark# X1, mark# U12 X -> active# U12 mark X) (mark# __(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> active# __(mark X1, mark X2)) (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> __#(mark X1, mark X2)) (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2) (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# isNePal X -> isNePal# mark X) (mark# U11 X -> mark# X, mark# isNePal X -> active# isNePal mark X) (mark# U11 X -> mark# X, mark# isNePal X -> mark# X) (mark# U11 X -> mark# X, mark# U11 X -> U11# mark X) (mark# U11 X -> mark# X, mark# U11 X -> active# U11 mark X) (mark# U11 X -> mark# X, mark# U11 X -> mark# X) (mark# U11 X -> mark# X, mark# tt() -> active# tt()) (mark# U11 X -> mark# X, mark# U12 X -> U12# mark X) (mark# U11 X -> mark# X, mark# U12 X -> active# U12 mark X) (mark# U11 X -> mark# X, mark# U12 X -> mark# X) (mark# U11 X -> mark# X, mark# nil() -> active# nil()) (mark# U11 X -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2)) (mark# U11 X -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2)) (mark# U11 X -> mark# X, mark# __(X1, X2) -> mark# X2) (mark# U11 X -> mark# X, mark# __(X1, X2) -> mark# X1) (active# __(X, nil()) -> mark# X, mark# isNePal X -> isNePal# mark X) (active# __(X, nil()) -> mark# X, mark# isNePal X -> active# isNePal mark X) (active# __(X, nil()) -> mark# X, mark# isNePal X -> mark# X) (active# __(X, nil()) -> mark# X, mark# U11 X -> U11# mark X) (active# __(X, nil()) -> mark# X, mark# U11 X -> active# U11 mark X) (active# __(X, nil()) -> mark# X, mark# U11 X -> mark# X) (active# __(X, nil()) -> mark# X, mark# tt() -> active# tt()) (active# __(X, nil()) -> mark# X, mark# U12 X -> U12# mark X) (active# __(X, nil()) -> mark# X, mark# U12 X -> active# U12 mark X) (active# __(X, nil()) -> mark# X, mark# U12 X -> mark# X) (active# __(X, nil()) -> mark# X, mark# nil() -> active# nil()) (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2)) (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2)) (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X2) (active# __(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X1) (U12# mark X -> U12# X, U12# active X -> U12# X) (U12# mark X -> U12# X, U12# mark X -> U12# X) (U11# mark X -> U11# X, U11# active X -> U11# X) (U11# mark X -> U11# X, U11# mark X -> U11# X) (isNePal# mark X -> isNePal# X, isNePal# active X -> isNePal# X) (isNePal# mark X -> isNePal# X, isNePal# mark X -> isNePal# X) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# isNePal X -> isNePal# 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 -> mark# X) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# U11 X -> U11# mark X) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# U11 X -> active# U11 mark X) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# U11 X -> mark# X) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# tt() -> active# tt()) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# U12 X -> U12# mark X) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# U12 X -> active# U12 mark X) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# U12 X -> mark# X) (active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), mark# nil() -> active# nil()) (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# __(X1, X2) -> __#(mark X1, mark X2)) (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) (__#(X1, active X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2)) (__#(X1, active X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(X1, active X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2)) (__#(X1, active X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (__#(active X1, X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2)) (__#(active X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(active X1, X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2)) (__#(active X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# isNePal __(I, __(P, I)) -> U11# tt()) (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# isNePal __(I, __(P, I)) -> mark# U11 tt()) (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# U11 tt() -> U12# tt()) (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# U11 tt() -> mark# U12 tt()) (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# U12 tt() -> mark# tt()) (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(nil(), X) -> mark# X) (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(__(X, Y), Z) -> __#(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) -> mark# __(X, __(Y, Z))) (mark# __(X1, X2) -> active# __(mark X1, mark X2), active# __(X, nil()) -> mark# X) (mark# U12 X -> active# U12 mark X, active# isNePal __(I, __(P, I)) -> U11# tt()) (mark# U12 X -> active# U12 mark X, active# isNePal __(I, __(P, I)) -> mark# U11 tt()) (mark# U12 X -> active# U12 mark X, active# U11 tt() -> U12# tt()) (mark# U12 X -> active# U12 mark X, active# U11 tt() -> mark# U12 tt()) (mark# U12 X -> active# U12 mark X, active# U12 tt() -> mark# tt()) (mark# U12 X -> active# U12 mark X, active# __(nil(), X) -> mark# X) (mark# U12 X -> active# U12 mark X, active# __(__(X, Y), Z) -> __#(Y, Z)) (mark# U12 X -> active# U12 mark X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (mark# U12 X -> active# U12 mark X, active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z))) (mark# U12 X -> active# U12 mark X, active# __(X, nil()) -> mark# X) (mark# isNePal X -> active# isNePal mark X, active# isNePal __(I, __(P, I)) -> U11# tt()) (mark# isNePal X -> active# isNePal mark X, active# isNePal __(I, __(P, I)) -> mark# U11 tt()) (mark# isNePal X -> active# isNePal mark X, active# U11 tt() -> U12# tt()) (mark# isNePal X -> active# isNePal mark X, active# U11 tt() -> mark# U12 tt()) (mark# isNePal X -> active# isNePal mark X, active# U12 tt() -> mark# tt()) (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# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# isNePal X -> isNePal# mark X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# isNePal X -> active# isNePal mark X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# isNePal X -> mark# X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# U11 X -> U11# mark X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# U11 X -> active# U11 mark X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# U11 X -> mark# X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# tt() -> active# tt()) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# U12 X -> U12# mark X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# U12 X -> active# U12 mark X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# U12 X -> mark# X) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# nil() -> active# nil()) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# __(X1, X2) -> active# __(mark X1, mark X2)) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# __(X1, X2) -> __#(mark X1, mark X2)) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# __(X1, X2) -> mark# X2) (active# isNePal __(I, __(P, I)) -> mark# U11 tt(), mark# __(X1, X2) -> mark# X1) (mark# U11 X -> U11# mark X, U11# active X -> U11# X) (mark# U11 X -> U11# mark X, U11# mark X -> U11# X) (mark# isNePal X -> isNePal# mark X, isNePal# mark X -> isNePal# X) (mark# isNePal X -> isNePal# mark X, isNePal# active X -> isNePal# X) (mark# U12 X -> U12# mark X, U12# mark X -> U12# X) (mark# U12 X -> U12# mark X, U12# active X -> U12# X) (active# U11 tt() -> mark# U12 tt(), mark# __(X1, X2) -> mark# X1) (active# U11 tt() -> mark# U12 tt(), mark# __(X1, X2) -> mark# X2) (active# U11 tt() -> mark# U12 tt(), mark# __(X1, X2) -> __#(mark X1, mark X2)) (active# U11 tt() -> mark# U12 tt(), mark# __(X1, X2) -> active# __(mark X1, mark X2)) (active# U11 tt() -> mark# U12 tt(), mark# nil() -> active# nil()) (active# U11 tt() -> mark# U12 tt(), mark# U12 X -> mark# X) (active# U11 tt() -> mark# U12 tt(), mark# U12 X -> active# U12 mark X) (active# U11 tt() -> mark# U12 tt(), mark# U12 X -> U12# mark X) (active# U11 tt() -> mark# U12 tt(), mark# tt() -> active# tt()) (active# U11 tt() -> mark# U12 tt(), mark# U11 X -> mark# X) (active# U11 tt() -> mark# U12 tt(), mark# U11 X -> active# U11 mark X) (active# U11 tt() -> mark# U12 tt(), mark# U11 X -> U11# mark X) (active# U11 tt() -> mark# U12 tt(), mark# isNePal X -> mark# X) (active# U11 tt() -> mark# U12 tt(), mark# isNePal X -> active# isNePal mark X) (active# U11 tt() -> mark# U12 tt(), mark# isNePal X -> isNePal# mark X) (mark# U11 X -> active# U11 mark X, active# __(X, nil()) -> mark# X) (mark# U11 X -> active# U11 mark X, active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z))) (mark# U11 X -> active# U11 mark X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (mark# U11 X -> active# U11 mark X, active# __(__(X, Y), Z) -> __#(Y, Z)) (mark# U11 X -> active# U11 mark X, active# __(nil(), X) -> mark# X) (mark# U11 X -> active# U11 mark X, active# U12 tt() -> mark# tt()) (mark# U11 X -> active# U11 mark X, active# U11 tt() -> mark# U12 tt()) (mark# U11 X -> active# U11 mark X, active# U11 tt() -> U12# tt()) (mark# U11 X -> active# U11 mark X, active# isNePal __(I, __(P, I)) -> mark# U11 tt()) (mark# U11 X -> active# U11 mark X, active# isNePal __(I, __(P, I)) -> U11# 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# U12 X -> mark# X) (mark# __(X1, X2) -> mark# X2, mark# U12 X -> active# U12 mark X) (mark# __(X1, X2) -> mark# X2, mark# U12 X -> U12# mark X) (mark# __(X1, X2) -> mark# X2, mark# tt() -> active# tt()) (mark# __(X1, X2) -> mark# X2, mark# U11 X -> mark# X) (mark# __(X1, X2) -> mark# X2, mark# U11 X -> active# U11 mark X) (mark# __(X1, X2) -> mark# X2, mark# U11 X -> U11# mark X) (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) -> __#(mark X1, mark X2), __#(X1, mark X2) -> __#(X1, X2)) (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(X1, active X2) -> __#(X1, X2)) (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(mark X1, X2) -> __#(X1, X2)) (mark# __(X1, X2) -> __#(mark X1, mark X2), __#(active X1, X2) -> __#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(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) (U11# active X -> U11# X, U11# mark X -> U11# X) (U11# active X -> U11# X, U11# active X -> U11# X) (U12# active X -> U12# X, U12# mark X -> U12# X) (U12# active X -> U12# X, U12# active X -> U12# X) (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X1) (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X2) (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2)) (active# __(nil(), X) -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2)) (active# __(nil(), X) -> mark# X, mark# nil() -> active# nil()) (active# __(nil(), X) -> mark# X, mark# U12 X -> mark# X) (active# __(nil(), X) -> mark# X, mark# U12 X -> active# U12 mark X) (active# __(nil(), X) -> mark# X, mark# U12 X -> U12# mark X) (active# __(nil(), X) -> mark# X, mark# tt() -> active# tt()) (active# __(nil(), X) -> mark# X, mark# U11 X -> mark# X) (active# __(nil(), X) -> mark# X, mark# U11 X -> active# U11 mark X) (active# __(nil(), X) -> mark# X, mark# U11 X -> U11# mark X) (active# __(nil(), X) -> mark# X, mark# isNePal X -> mark# X) (active# __(nil(), X) -> mark# X, mark# isNePal X -> active# isNePal mark X) (active# __(nil(), X) -> mark# X, mark# isNePal X -> isNePal# mark X) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X1) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X2) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2)) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2)) (mark# isNePal X -> mark# X, mark# nil() -> active# nil()) (mark# isNePal X -> mark# X, mark# U12 X -> mark# X) (mark# isNePal X -> mark# X, mark# U12 X -> active# U12 mark X) (mark# isNePal X -> mark# X, mark# U12 X -> U12# mark X) (mark# isNePal X -> mark# X, mark# tt() -> active# tt()) (mark# isNePal X -> mark# X, mark# U11 X -> mark# X) (mark# isNePal X -> mark# X, mark# U11 X -> active# U11 mark X) (mark# isNePal X -> mark# X, mark# U11 X -> U11# mark X) (mark# isNePal X -> mark# X, mark# isNePal X -> mark# X) (mark# isNePal X -> mark# X, mark# isNePal X -> active# isNePal mark X) (mark# isNePal X -> mark# X, mark# isNePal X -> isNePal# mark X) (mark# U12 X -> mark# X, mark# __(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# __(X1, X2) -> mark# X2) (mark# U12 X -> mark# X, mark# __(X1, X2) -> __#(mark X1, mark X2)) (mark# U12 X -> mark# X, mark# __(X1, X2) -> active# __(mark X1, mark X2)) (mark# U12 X -> mark# X, mark# nil() -> active# nil()) (mark# U12 X -> mark# X, mark# U12 X -> mark# X) (mark# U12 X -> mark# X, mark# U12 X -> active# U12 mark X) (mark# U12 X -> mark# X, mark# U12 X -> U12# mark X) (mark# U12 X -> mark# X, mark# tt() -> active# tt()) (mark# U12 X -> mark# X, mark# U11 X -> mark# X) (mark# U12 X -> mark# X, mark# U11 X -> active# U11 mark X) (mark# U12 X -> mark# X, mark# U11 X -> U11# mark X) (mark# U12 X -> mark# X, mark# isNePal X -> mark# X) (mark# U12 X -> mark# X, mark# isNePal X -> active# isNePal mark X) (mark# U12 X -> mark# X, mark# isNePal X -> isNePal# mark X) (active# isNePal __(I, __(P, I)) -> U11# tt(), U11# mark X -> U11# X) (active# isNePal __(I, __(P, I)) -> U11# tt(), U11# active X -> U11# X) (active# U12 tt() -> mark# tt(), mark# __(X1, X2) -> mark# X1) (active# U12 tt() -> mark# tt(), mark# __(X1, X2) -> mark# X2) (active# U12 tt() -> mark# tt(), mark# __(X1, X2) -> __#(mark X1, mark X2)) (active# U12 tt() -> mark# tt(), mark# __(X1, X2) -> active# __(mark X1, mark X2)) (active# U12 tt() -> mark# tt(), mark# nil() -> active# nil()) (active# U12 tt() -> mark# tt(), mark# U12 X -> mark# X) (active# U12 tt() -> mark# tt(), mark# U12 X -> active# U12 mark X) (active# U12 tt() -> mark# tt(), mark# U12 X -> U12# mark X) (active# U12 tt() -> mark# tt(), mark# tt() -> active# tt()) (active# U12 tt() -> mark# tt(), mark# U11 X -> mark# X) (active# U12 tt() -> mark# tt(), mark# U11 X -> active# U11 mark X) (active# U12 tt() -> mark# tt(), mark# U11 X -> U11# mark X) (active# U12 tt() -> mark# tt(), mark# isNePal X -> mark# X) (active# U12 tt() -> mark# tt(), mark# isNePal X -> active# isNePal mark X) (active# U12 tt() -> 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# U12 tt() -> mark# tt()) (mark# nil() -> active# nil(), active# U11 tt() -> mark# U12 tt()) (mark# nil() -> active# nil(), active# U11 tt() -> U12# tt()) (mark# nil() -> active# nil(), active# isNePal __(I, __(P, I)) -> mark# U11 tt()) (mark# nil() -> active# nil(), active# isNePal __(I, __(P, I)) -> U11# tt()) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, active X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(mark X1, X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(active X1, X2) -> __#(X1, X2)) } STATUS: arrows: 0.775510 SCCS (5): Scc: { mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> active# __(mark X1, mark X2), mark# nil() -> active# nil(), mark# U12 X -> mark# X, mark# U12 X -> active# U12 mark X, mark# tt() -> active# tt(), mark# U11 X -> mark# X, mark# U11 X -> active# U11 mark X, mark# isNePal X -> mark# X, mark# isNePal X -> active# isNePal mark X, active# __(X, nil()) -> mark# X, active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), active# __(nil(), X) -> mark# X, active# U12 tt() -> mark# tt(), active# U11 tt() -> mark# U12 tt(), active# isNePal __(I, __(P, I)) -> mark# U11 tt()} Scc: { isNePal# mark X -> isNePal# X, isNePal# active X -> isNePal# X} Scc: { U11# mark X -> U11# X, U11# active X -> U11# X} Scc: { U12# mark X -> U12# X, U12# active X -> U12# X} Scc: { __#(X1, mark X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2)} SCC (17): Strict: { mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> active# __(mark X1, mark X2), mark# nil() -> active# nil(), mark# U12 X -> mark# X, mark# U12 X -> active# U12 mark X, mark# tt() -> active# tt(), mark# U11 X -> mark# X, mark# U11 X -> active# U11 mark X, mark# isNePal X -> mark# X, mark# isNePal X -> active# isNePal mark X, active# __(X, nil()) -> mark# X, active# __(__(X, Y), Z) -> mark# __(X, __(Y, Z)), active# __(nil(), X) -> mark# X, active# U12 tt() -> mark# tt(), active# U11 tt() -> mark# U12 tt(), active# isNePal __(I, __(P, I)) -> mark# U11 tt()} Weak: { mark __(X1, X2) -> active __(mark X1, mark X2), mark nil() -> active nil(), mark U12 X -> active U12 mark X, mark tt() -> active tt(), mark U11 X -> active U11 mark X, 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 U12 tt() -> mark tt(), active U11 tt() -> mark U12 tt(), active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> U12 X, U12 active X -> U12 X, U11 mark X -> U11 X, U11 active X -> U11 X, isNePal mark X -> isNePal X, isNePal active X -> isNePal X} Open SCC (2): Strict: { isNePal# mark X -> isNePal# X, isNePal# active X -> isNePal# X} Weak: { mark __(X1, X2) -> active __(mark X1, mark X2), mark nil() -> active nil(), mark U12 X -> active U12 mark X, mark tt() -> active tt(), mark U11 X -> active U11 mark X, 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 U12 tt() -> mark tt(), active U11 tt() -> mark U12 tt(), active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> U12 X, U12 active X -> U12 X, U11 mark X -> U11 X, U11 active X -> U11 X, isNePal mark X -> isNePal X, isNePal active X -> isNePal X} Open SCC (2): Strict: { U11# mark X -> U11# X, U11# active X -> U11# X} Weak: { mark __(X1, X2) -> active __(mark X1, mark X2), mark nil() -> active nil(), mark U12 X -> active U12 mark X, mark tt() -> active tt(), mark U11 X -> active U11 mark X, 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 U12 tt() -> mark tt(), active U11 tt() -> mark U12 tt(), active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> U12 X, U12 active X -> U12 X, U11 mark X -> U11 X, U11 active X -> U11 X, isNePal mark X -> isNePal X, isNePal active X -> isNePal X} Open SCC (2): Strict: { U12# mark X -> U12# X, U12# active X -> U12# X} Weak: { mark __(X1, X2) -> active __(mark X1, mark X2), mark nil() -> active nil(), mark U12 X -> active U12 mark X, mark tt() -> active tt(), mark U11 X -> active U11 mark X, 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 U12 tt() -> mark tt(), active U11 tt() -> mark U12 tt(), active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> U12 X, U12 active X -> U12 X, U11 mark X -> U11 X, U11 active X -> U11 X, isNePal mark X -> isNePal X, isNePal active X -> isNePal X} Open SCC (4): Strict: { __#(X1, mark X2) -> __#(X1, X2), __#(X1, active X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2), __#(active X1, X2) -> __#(X1, X2)} Weak: { mark __(X1, X2) -> active __(mark X1, mark X2), mark nil() -> active nil(), mark U12 X -> active U12 mark X, mark tt() -> active tt(), mark U11 X -> active U11 mark X, 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 U12 tt() -> mark tt(), active U11 tt() -> mark U12 tt(), active isNePal __(I, __(P, I)) -> mark U11 tt(), U12 mark X -> U12 X, U12 active X -> U12 X, U11 mark X -> U11 X, U11 active X -> U11 X, isNePal mark X -> isNePal X, isNePal active X -> isNePal X} Open