MAYBE Time: 1.013996 TRS: { a____(X, nil()) -> mark X, a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark X, a____(mark Y, mark Z)), a____(nil(), X) -> mark X, mark __(X1, X2) -> a____(mark X1, mark X2), mark nil() -> nil(), mark tt() -> tt(), mark U11 X -> a__U11 mark X, mark U12 X -> a__U12 mark X, mark isNePal X -> a__isNePal mark X, a__U12 X -> U12 X, a__U12 tt() -> tt(), a__U11 X -> U11 X, a__U11 tt() -> a__U12 tt(), a__isNePal X -> isNePal X, a__isNePal __(I, __(P, I)) -> a__U11 tt()} DP: DP: { a____#(X, nil()) -> mark# X, a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# X, a____#(__(X, Y), Z) -> mark# Y, a____#(__(X, Y), Z) -> mark# Z, a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2), mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2, mark# U11 X -> mark# X, mark# U11 X -> a__U11# mark X, mark# U12 X -> mark# X, mark# U12 X -> a__U12# mark X, mark# isNePal X -> mark# X, mark# isNePal X -> a__isNePal# mark X, a__U11# tt() -> a__U12# tt(), a__isNePal# __(I, __(P, I)) -> a__U11# tt()} TRS: { a____(X, nil()) -> mark X, a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark X, a____(mark Y, mark Z)), a____(nil(), X) -> mark X, mark __(X1, X2) -> a____(mark X1, mark X2), mark nil() -> nil(), mark tt() -> tt(), mark U11 X -> a__U11 mark X, mark U12 X -> a__U12 mark X, mark isNePal X -> a__isNePal mark X, a__U12 X -> U12 X, a__U12 tt() -> tt(), a__U11 X -> U11 X, a__U11 tt() -> a__U12 tt(), a__isNePal X -> isNePal X, a__isNePal __(I, __(P, I)) -> a__U11 tt()} UR: { a____(X, nil()) -> mark X, a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark X, a____(mark Y, mark Z)), a____(nil(), X) -> mark X, mark __(X1, X2) -> a____(mark X1, mark X2), mark nil() -> nil(), mark tt() -> tt(), mark U11 X -> a__U11 mark X, mark U12 X -> a__U12 mark X, mark isNePal X -> a__isNePal mark X, a__U12 X -> U12 X, a__U12 tt() -> tt(), a__U11 X -> U11 X, a__U11 tt() -> a__U12 tt(), a__isNePal X -> isNePal X, a__isNePal __(I, __(P, I)) -> a__U11 tt()} EDG: {(mark# U11 X -> a__U11# mark X, a__U11# tt() -> a__U12# tt()) (mark# isNePal X -> a__isNePal# mark X, a__isNePal# __(I, __(P, I)) -> a__U11# tt()) (a__isNePal# __(I, __(P, I)) -> a__U11# tt(), a__U11# tt() -> a__U12# tt()) (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> a__isNePal# mark X) (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> mark# X) (mark# __(X1, X2) -> mark# X2, mark# U12 X -> a__U12# mark X) (mark# __(X1, X2) -> mark# X2, mark# U12 X -> mark# X) (mark# __(X1, X2) -> mark# X2, mark# U11 X -> a__U11# mark X) (mark# __(X1, X2) -> mark# X2, mark# U11 X -> mark# X) (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> mark# X2) (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> mark# X1) (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(nil(), X) -> mark# X) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# Z) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# Y) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# X) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z)) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z))) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(X, nil()) -> mark# X) (a____#(__(X, Y), Z) -> mark# X, mark# isNePal X -> a__isNePal# mark X) (a____#(__(X, Y), Z) -> mark# X, mark# isNePal X -> mark# X) (a____#(__(X, Y), Z) -> mark# X, mark# U12 X -> a__U12# mark X) (a____#(__(X, Y), Z) -> mark# X, mark# U12 X -> mark# X) (a____#(__(X, Y), Z) -> mark# X, mark# U11 X -> a__U11# mark X) (a____#(__(X, Y), Z) -> mark# X, mark# U11 X -> mark# X) (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> mark# X2) (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> mark# X1) (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (mark# U11 X -> mark# X, mark# isNePal X -> a__isNePal# mark X) (mark# U11 X -> mark# X, mark# isNePal X -> mark# X) (mark# U11 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U11 X -> mark# X, mark# U12 X -> mark# X) (mark# U11 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U11 X -> mark# X, mark# U11 X -> mark# X) (mark# U11 X -> mark# X, mark# __(X1, X2) -> mark# X2) (mark# U11 X -> mark# X, mark# __(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (mark# isNePal X -> mark# X, mark# isNePal X -> a__isNePal# mark X) (mark# isNePal X -> mark# X, mark# isNePal X -> mark# X) (mark# isNePal X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# isNePal X -> mark# X, mark# U12 X -> mark# X) (mark# isNePal X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# isNePal X -> mark# X, mark# U11 X -> mark# X) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X2) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X1) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(nil(), X) -> mark# X) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# Z) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# Y) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# X) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z)) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z))) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(X, nil()) -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (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# U11 X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# __(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> a__isNePal# mark X) (mark# U12 X -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (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# U11 X -> mark# X) (mark# U12 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U12 X -> mark# X, mark# U12 X -> mark# X) (mark# U12 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U12 X -> mark# X, mark# isNePal X -> mark# X) (mark# U12 X -> mark# X, mark# isNePal X -> a__isNePal# mark X) (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X1) (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X2) (a____#(nil(), X) -> mark# X, mark# U11 X -> mark# X) (a____#(nil(), X) -> mark# X, mark# U11 X -> a__U11# mark X) (a____#(nil(), X) -> mark# X, mark# U12 X -> mark# X) (a____#(nil(), X) -> mark# X, mark# U12 X -> a__U12# mark X) (a____#(nil(), X) -> mark# X, mark# isNePal X -> mark# X) (a____#(nil(), X) -> mark# X, mark# isNePal X -> a__isNePal# mark X) (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X1) (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X2) (a____#(X, nil()) -> mark# X, mark# U11 X -> mark# X) (a____#(X, nil()) -> mark# X, mark# U11 X -> a__U11# mark X) (a____#(X, nil()) -> mark# X, mark# U12 X -> mark# X) (a____#(X, nil()) -> mark# X, mark# U12 X -> a__U12# mark X) (a____#(X, nil()) -> mark# X, mark# isNePal X -> mark# X) (a____#(X, nil()) -> mark# X, mark# isNePal X -> a__isNePal# mark X) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(X, nil()) -> mark# X) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z))) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z)) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# X) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# Y) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# Z) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(nil(), X) -> mark# X) (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> mark# X1) (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> mark# X2) (a____#(__(X, Y), Z) -> mark# Y, mark# U11 X -> mark# X) (a____#(__(X, Y), Z) -> mark# Y, mark# U11 X -> a__U11# mark X) (a____#(__(X, Y), Z) -> mark# Y, mark# U12 X -> mark# X) (a____#(__(X, Y), Z) -> mark# Y, mark# U12 X -> a__U12# mark X) (a____#(__(X, Y), Z) -> mark# Y, mark# isNePal X -> mark# X) (a____#(__(X, Y), Z) -> mark# Y, mark# isNePal X -> a__isNePal# mark X) (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> mark# X1) (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> mark# X2) (a____#(__(X, Y), Z) -> mark# Z, mark# U11 X -> mark# X) (a____#(__(X, Y), Z) -> mark# Z, mark# U11 X -> a__U11# mark X) (a____#(__(X, Y), Z) -> mark# Z, mark# U12 X -> mark# X) (a____#(__(X, Y), Z) -> mark# Z, mark# U12 X -> a__U12# mark X) (a____#(__(X, Y), Z) -> mark# Z, mark# isNePal X -> mark# X) (a____#(__(X, Y), Z) -> mark# Z, mark# isNePal X -> a__isNePal# mark X)} EDG: {(mark# U11 X -> a__U11# mark X, a__U11# tt() -> a__U12# tt()) (mark# isNePal X -> a__isNePal# mark X, a__isNePal# __(I, __(P, I)) -> a__U11# tt()) (a__isNePal# __(I, __(P, I)) -> a__U11# tt(), a__U11# tt() -> a__U12# tt()) (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> a__isNePal# mark X) (mark# __(X1, X2) -> mark# X2, mark# isNePal X -> mark# X) (mark# __(X1, X2) -> mark# X2, mark# U12 X -> a__U12# mark X) (mark# __(X1, X2) -> mark# X2, mark# U12 X -> mark# X) (mark# __(X1, X2) -> mark# X2, mark# U11 X -> a__U11# mark X) (mark# __(X1, X2) -> mark# X2, mark# U11 X -> mark# X) (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> mark# X2) (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> mark# X1) (mark# __(X1, X2) -> mark# X2, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(nil(), X) -> mark# X) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# Z) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# Y) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> mark# X) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z)) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z))) (mark# __(X1, X2) -> a____#(mark X1, mark X2), a____#(X, nil()) -> mark# X) (a____#(__(X, Y), Z) -> mark# X, mark# isNePal X -> a__isNePal# mark X) (a____#(__(X, Y), Z) -> mark# X, mark# isNePal X -> mark# X) (a____#(__(X, Y), Z) -> mark# X, mark# U12 X -> a__U12# mark X) (a____#(__(X, Y), Z) -> mark# X, mark# U12 X -> mark# X) (a____#(__(X, Y), Z) -> mark# X, mark# U11 X -> a__U11# mark X) (a____#(__(X, Y), Z) -> mark# X, mark# U11 X -> mark# X) (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> mark# X2) (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> mark# X1) (a____#(__(X, Y), Z) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (mark# U11 X -> mark# X, mark# isNePal X -> a__isNePal# mark X) (mark# U11 X -> mark# X, mark# isNePal X -> mark# X) (mark# U11 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U11 X -> mark# X, mark# U12 X -> mark# X) (mark# U11 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U11 X -> mark# X, mark# U11 X -> mark# X) (mark# U11 X -> mark# X, mark# __(X1, X2) -> mark# X2) (mark# U11 X -> mark# X, mark# __(X1, X2) -> mark# X1) (mark# U11 X -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (mark# isNePal X -> mark# X, mark# isNePal X -> a__isNePal# mark X) (mark# isNePal X -> mark# X, mark# isNePal X -> mark# X) (mark# isNePal X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# isNePal X -> mark# X, mark# U12 X -> mark# X) (mark# isNePal X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# isNePal X -> mark# X, mark# U11 X -> mark# X) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X2) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> mark# X1) (mark# isNePal X -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(nil(), X) -> mark# X) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# Z) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# Y) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> mark# X) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z)) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z))) (a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(X, nil()) -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (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# U11 X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# U11 X -> a__U11# mark X) (mark# __(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> mark# X) (mark# __(X1, X2) -> mark# X1, mark# isNePal X -> a__isNePal# mark X) (mark# U12 X -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (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# U11 X -> mark# X) (mark# U12 X -> mark# X, mark# U11 X -> a__U11# mark X) (mark# U12 X -> mark# X, mark# U12 X -> mark# X) (mark# U12 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U12 X -> mark# X, mark# isNePal X -> mark# X) (mark# U12 X -> mark# X, mark# isNePal X -> a__isNePal# mark X) (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X1) (a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> mark# X2) (a____#(nil(), X) -> mark# X, mark# U11 X -> mark# X) (a____#(nil(), X) -> mark# X, mark# U11 X -> a__U11# mark X) (a____#(nil(), X) -> mark# X, mark# U12 X -> mark# X) (a____#(nil(), X) -> mark# X, mark# U12 X -> a__U12# mark X) (a____#(nil(), X) -> mark# X, mark# isNePal X -> mark# X) (a____#(nil(), X) -> mark# X, mark# isNePal X -> a__isNePal# mark X) (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X1) (a____#(X, nil()) -> mark# X, mark# __(X1, X2) -> mark# X2) (a____#(X, nil()) -> mark# X, mark# U11 X -> mark# X) (a____#(X, nil()) -> mark# X, mark# U11 X -> a__U11# mark X) (a____#(X, nil()) -> mark# X, mark# U12 X -> mark# X) (a____#(X, nil()) -> mark# X, mark# U12 X -> a__U12# mark X) (a____#(X, nil()) -> mark# X, mark# isNePal X -> mark# X) (a____#(X, nil()) -> mark# X, mark# isNePal X -> a__isNePal# mark X) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(X, nil()) -> mark# X) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z))) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z)) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# X) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# Y) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# Z) (a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(nil(), X) -> mark# X) (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> mark# X1) (a____#(__(X, Y), Z) -> mark# Y, mark# __(X1, X2) -> mark# X2) (a____#(__(X, Y), Z) -> mark# Y, mark# U11 X -> mark# X) (a____#(__(X, Y), Z) -> mark# Y, mark# U11 X -> a__U11# mark X) (a____#(__(X, Y), Z) -> mark# Y, mark# U12 X -> mark# X) (a____#(__(X, Y), Z) -> mark# Y, mark# U12 X -> a__U12# mark X) (a____#(__(X, Y), Z) -> mark# Y, mark# isNePal X -> mark# X) (a____#(__(X, Y), Z) -> mark# Y, mark# isNePal X -> a__isNePal# mark X) (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> a____#(mark X1, mark X2)) (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> mark# X1) (a____#(__(X, Y), Z) -> mark# Z, mark# __(X1, X2) -> mark# X2) (a____#(__(X, Y), Z) -> mark# Z, mark# U11 X -> mark# X) (a____#(__(X, Y), Z) -> mark# Z, mark# U11 X -> a__U11# mark X) (a____#(__(X, Y), Z) -> mark# Z, mark# U12 X -> mark# X) (a____#(__(X, Y), Z) -> mark# Z, mark# U12 X -> a__U12# mark X) (a____#(__(X, Y), Z) -> mark# Z, mark# isNePal X -> mark# X) (a____#(__(X, Y), Z) -> mark# Z, mark# isNePal X -> a__isNePal# mark X)} STATUS: arrows: 0.648148 SCCS (1): Scc: { a____#(X, nil()) -> mark# X, a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# X, a____#(__(X, Y), Z) -> mark# Y, a____#(__(X, Y), Z) -> mark# Z, a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2), mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2, mark# U11 X -> mark# X, mark# U12 X -> mark# X, mark# isNePal X -> mark# X} SCC (13): Strict: { a____#(X, nil()) -> mark# X, a____#(__(X, Y), Z) -> a____#(mark X, a____(mark Y, mark Z)), a____#(__(X, Y), Z) -> a____#(mark Y, mark Z), a____#(__(X, Y), Z) -> mark# X, a____#(__(X, Y), Z) -> mark# Y, a____#(__(X, Y), Z) -> mark# Z, a____#(nil(), X) -> mark# X, mark# __(X1, X2) -> a____#(mark X1, mark X2), mark# __(X1, X2) -> mark# X1, mark# __(X1, X2) -> mark# X2, mark# U11 X -> mark# X, mark# U12 X -> mark# X, mark# isNePal X -> mark# X} Weak: { a____(X, nil()) -> mark X, a____(X1, X2) -> __(X1, X2), a____(__(X, Y), Z) -> a____(mark X, a____(mark Y, mark Z)), a____(nil(), X) -> mark X, mark __(X1, X2) -> a____(mark X1, mark X2), mark nil() -> nil(), mark tt() -> tt(), mark U11 X -> a__U11 mark X, mark U12 X -> a__U12 mark X, mark isNePal X -> a__isNePal mark X, a__U12 X -> U12 X, a__U12 tt() -> tt(), a__U11 X -> U11 X, a__U11 tt() -> a__U12 tt(), a__isNePal X -> isNePal X, a__isNePal __(I, __(P, I)) -> a__U11 tt()} Open