MAYBE Time: 1.063016 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) -> active# X1, active# isNePal X -> isNePal# active X) (active# and(X1, X2) -> active# X1, active# isNePal X -> active# X) (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# and(X1, X2) -> proper# X1, proper# isNePal X -> proper# X) (proper# and(X1, X2) -> proper# X1, proper# isNePal X -> isNePal# proper X) (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2) (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1) (proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2)) (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2) (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X1) (proper# and(X1, X2) -> proper# X1, proper# __(X1, X2) -> __#(proper X1, proper X2)) (isNePal# mark X -> isNePal# X, isNePal# ok X -> isNePal# X) (isNePal# mark X -> isNePal# X, isNePal# mark X -> isNePal# X) (proper# isNePal X -> proper# X, proper# isNePal X -> proper# X) (proper# isNePal X -> proper# X, proper# isNePal X -> isNePal# proper X) (proper# isNePal X -> proper# X, proper# and(X1, X2) -> proper# X2) (proper# isNePal X -> proper# X, proper# and(X1, X2) -> proper# X1) (proper# isNePal X -> proper# X, proper# and(X1, X2) -> and#(proper X1, proper X2)) (proper# isNePal X -> proper# X, proper# __(X1, X2) -> proper# X2) (proper# isNePal X -> proper# X, proper# __(X1, X2) -> proper# X1) (proper# isNePal X -> proper# X, proper# __(X1, X2) -> __#(proper X1, proper X2)) (top# ok X -> active# X, active# isNePal X -> isNePal# active X) (top# ok X -> active# X, active# isNePal X -> active# X) (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# and(X1, X2) -> and#(active X1, X2), and#(ok X1, ok X2) -> and#(X1, X2)) (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) (__#(X1, mark X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(X1, mark X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (__#(ok X1, ok X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)) (__#(ok X1, ok X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(ok X1, ok X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (and#(ok X1, ok X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2)) (and#(ok X1, ok X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(ok X1, ok X2) -> __#(X1, X2)) (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(mark X1, X2) -> __#(X1, X2)) (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(X1, mark X2) -> __#(X1, X2)) (active# __(X1, X2) -> active# X2, active# isNePal X -> isNePal# active X) (active# __(X1, X2) -> active# X2, active# isNePal X -> active# X) (active# __(X1, X2) -> active# X2, active# and(X1, X2) -> and#(active X1, X2)) (active# __(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1) (active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(Y, Z)) (active# __(X1, X2) -> active# X2, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X2) (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> active# X1) (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(active X1, X2)) (active# __(X1, X2) -> active# X2, active# __(X1, X2) -> __#(X1, active X2)) (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# 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# 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# isNePal X -> isNePal# proper X) (proper# and(X1, X2) -> proper# X2, proper# isNePal X -> proper# X) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(mark X1, X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(ok X1, ok X2) -> __#(X1, X2)) (proper# and(X1, X2) -> and#(proper X1, proper X2), and#(mark X1, X2) -> and#(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)) (active# __(X1, X2) -> __#(X1, active X2), __#(mark X1, X2) -> __#(X1, X2)) (active# __(X1, X2) -> __#(X1, active X2), __#(ok X1, ok X2) -> __#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(mark X1, X2) -> and#(X1, X2)) (and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (__#(mark X1, X2) -> __#(X1, X2), __#(ok X1, ok 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# mark X -> isNePal# X) (proper# isNePal X -> isNePal# proper X, isNePal# ok X -> isNePal# X) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(X1, mark X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(mark X1, X2) -> __#(X1, X2)) (active# __(__(X, Y), Z) -> __#(Y, Z), __#(ok X1, ok X2) -> __#(X1, X2)) (active# __(X1, X2) -> __#(active X1, X2), __#(X1, mark X2) -> __#(X1, X2)) (active# __(X1, X2) -> __#(active X1, X2), __#(mark X1, X2) -> __#(X1, X2)) (active# __(X1, X2) -> __#(active X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)) (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# isNePal X -> isNePal# proper X) (top# mark X -> proper# X, proper# isNePal X -> proper# X) (isNePal# ok X -> isNePal# X, isNePal# mark X -> isNePal# X) (isNePal# ok X -> isNePal# X, isNePal# ok X -> isNePal# X) (active# isNePal X -> active# X, active# __(X1, X2) -> __#(X1, active X2)) (active# isNePal X -> active# X, active# __(X1, X2) -> __#(active X1, X2)) (active# isNePal X -> active# X, active# __(X1, X2) -> active# X1) (active# isNePal X -> active# X, active# __(X1, X2) -> active# X2) (active# isNePal X -> active# X, active# __(__(X, Y), Z) -> __#(X, __(Y, Z))) (active# isNePal X -> active# X, active# __(__(X, Y), Z) -> __#(Y, Z)) (active# isNePal X -> active# X, active# and(X1, X2) -> active# X1) (active# isNePal X -> active# X, active# and(X1, X2) -> and#(active X1, X2)) (active# isNePal X -> active# X, active# isNePal X -> active# X) (active# isNePal X -> active# X, active# isNePal X -> isNePal# active X) (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> __#(proper X1, proper X2)) (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X1) (proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2) (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> and#(proper X1, proper X2)) (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X1) (proper# __(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2) (proper# __(X1, X2) -> proper# X1, proper# isNePal X -> isNePal# proper X) (proper# __(X1, X2) -> proper# X1, proper# isNePal X -> proper# X) (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# isNePal X -> active# X) (active# __(X1, X2) -> active# X1, active# isNePal X -> isNePal# active X) } STATUS: arrows: 0.826397 SCCS (6): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} Scc: { proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2, proper# isNePal X -> proper# X} Scc: { active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1, active# isNePal X -> active# X} Scc: {isNePal# mark X -> isNePal# X, isNePal# ok X -> isNePal# X} Scc: { and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2)} Scc: { __#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)} 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 SCC (5): Strict: { proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# and(X1, X2) -> proper# X1, proper# and(X1, X2) -> proper# X2, proper# isNePal X -> proper# 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 SCC (4): Strict: { active# __(X1, X2) -> active# X1, active# __(X1, X2) -> active# X2, active# and(X1, X2) -> active# X1, active# isNePal X -> 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 SCC (2): Strict: {isNePal# mark X -> isNePal# X, isNePal# ok X -> isNePal# 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 SCC (2): Strict: { and#(mark X1, X2) -> and#(X1, X2), and#(ok X1, ok X2) -> and#(X1, X2)} 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 SCC (3): Strict: { __#(X1, mark X2) -> __#(X1, X2), __#(mark X1, X2) -> __#(X1, X2), __#(ok X1, ok X2) -> __#(X1, X2)} 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