MAYBE Time: 1.680320 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 U11 X -> U11 active X, active U11 tt() -> mark tt(), active U22 X -> U22 active X, active U22 tt() -> mark tt(), active isList V -> mark U11 isNeList V, active isList __(V1, V2) -> mark U21(isList V1, V2), active isList nil() -> mark tt(), active U21(X1, X2) -> U21(active X1, X2), active U21(tt(), V2) -> mark U22 isList V2, active U31 X -> U31 active X, active U31 tt() -> mark tt(), active U42 X -> U42 active X, active U42 tt() -> mark tt(), active isNeList V -> mark U31 isQid V, active isNeList __(V1, V2) -> mark U41(isList V1, V2), active isNeList __(V1, V2) -> mark U51(isNeList V1, V2), active U41(X1, X2) -> U41(active X1, X2), active U41(tt(), V2) -> mark U42 isNeList V2, active U52 X -> U52 active X, active U52 tt() -> mark tt(), active U51(X1, X2) -> U51(active X1, X2), active U51(tt(), V2) -> mark U52 isList V2, active U61 X -> U61 active X, active U61 tt() -> mark tt(), active U72 X -> U72 active X, active U72 tt() -> mark tt(), active isPal V -> mark U81 isNePal V, active isPal nil() -> mark tt(), active U71(X1, X2) -> U71(active X1, X2), active U71(tt(), P) -> mark U72 isPal P, active U81 X -> U81 active X, active U81 tt() -> mark tt(), active isQid a() -> mark tt(), active isQid e() -> mark tt(), active isQid i() -> mark tt(), active isQid o() -> mark tt(), active isQid u() -> mark tt(), active isNePal V -> mark U61 isQid V, active isNePal __(I, __(P, I)) -> mark U71(isQid I, P), U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, U22 mark X -> mark U22 X, U22 ok X -> ok U22 X, isList ok X -> ok isList X, U21(mark X1, X2) -> mark U21(X1, X2), U21(ok X1, ok X2) -> ok U21(X1, X2), U31 mark X -> mark U31 X, U31 ok X -> ok U31 X, U42 mark X -> mark U42 X, U42 ok X -> ok U42 X, isNeList ok X -> ok isNeList X, U41(mark X1, X2) -> mark U41(X1, X2), U41(ok X1, ok X2) -> ok U41(X1, X2), U52 mark X -> mark U52 X, U52 ok X -> ok U52 X, U51(mark X1, X2) -> mark U51(X1, X2), U51(ok X1, ok X2) -> ok U51(X1, X2), U61 mark X -> mark U61 X, U61 ok X -> ok U61 X, U72 mark X -> mark U72 X, U72 ok X -> ok U72 X, isPal ok X -> ok isPal X, U71(mark X1, X2) -> mark U71(X1, X2), U71(ok X1, ok X2) -> ok U71(X1, X2), U81 mark X -> mark U81 X, U81 ok X -> ok U81 X, isQid ok X -> ok isQid X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper U22 X -> U22 proper X, proper isList X -> isList proper X, proper U21(X1, X2) -> U21(proper X1, proper X2), proper U31 X -> U31 proper X, proper U42 X -> U42 proper X, proper isNeList X -> isNeList proper X, proper U41(X1, X2) -> U41(proper X1, proper X2), proper U52 X -> U52 proper X, proper U51(X1, X2) -> U51(proper X1, proper X2), proper U61 X -> U61 proper X, proper U72 X -> U72 proper X, proper isPal X -> isPal proper X, proper U71(X1, X2) -> U71(proper X1, proper X2), proper U81 X -> U81 proper X, proper isQid X -> isQid proper X, proper isNePal X -> isNePal proper X, proper a() -> ok a(), proper e() -> ok e(), proper i() -> ok i(), proper o() -> ok o(), proper u() -> ok u(), 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# U11 X -> active# X, active# U11 X -> U11# active X, active# U22 X -> active# X, active# U22 X -> U22# active X, active# isList V -> U11# isNeList V, active# isList V -> isNeList# V, active# isList __(V1, V2) -> isList# V1, active# isList __(V1, V2) -> U21#(isList V1, V2), active# U21(X1, X2) -> active# X1, active# U21(X1, X2) -> U21#(active X1, X2), active# U21(tt(), V2) -> U22# isList V2, active# U21(tt(), V2) -> isList# V2, active# U31 X -> active# X, active# U31 X -> U31# active X, active# U42 X -> active# X, active# U42 X -> U42# active X, active# isNeList V -> U31# isQid V, active# isNeList V -> isQid# V, active# isNeList __(V1, V2) -> isList# V1, active# isNeList __(V1, V2) -> isNeList# V1, active# isNeList __(V1, V2) -> U41#(isList V1, V2), active# isNeList __(V1, V2) -> U51#(isNeList V1, V2), active# U41(X1, X2) -> active# X1, active# U41(X1, X2) -> U41#(active X1, X2), active# U41(tt(), V2) -> U42# isNeList V2, active# U41(tt(), V2) -> isNeList# V2, active# U52 X -> active# X, active# U52 X -> U52# active X, active# U51(X1, X2) -> active# X1, active# U51(X1, X2) -> U51#(active X1, X2), active# U51(tt(), V2) -> isList# V2, active# U51(tt(), V2) -> U52# isList V2, active# U61 X -> active# X, active# U61 X -> U61# active X, active# U72 X -> active# X, active# U72 X -> U72# active X, active# isPal V -> U81# isNePal V, active# isPal V -> isNePal# V, active# U71(X1, X2) -> active# X1, active# U71(X1, X2) -> U71#(active X1, X2), active# U71(tt(), P) -> U72# isPal P, active# U71(tt(), P) -> isPal# P, active# U81 X -> active# X, active# U81 X -> U81# active X, active# isNePal V -> U61# isQid V, active# isNePal V -> isQid# V, active# isNePal __(I, __(P, I)) -> U71#(isQid I, P), active# isNePal __(I, __(P, I)) -> isQid# I, U11# mark X -> U11# X, U11# ok X -> U11# X, U22# mark X -> U22# X, U22# ok X -> U22# X, isList# ok X -> isList# X, U21#(mark X1, X2) -> U21#(X1, X2), U21#(ok X1, ok X2) -> U21#(X1, X2), U31# mark X -> U31# X, U31# ok X -> U31# X, U42# mark X -> U42# X, U42# ok X -> U42# X, isNeList# ok X -> isNeList# X, U41#(mark X1, X2) -> U41#(X1, X2), U41#(ok X1, ok X2) -> U41#(X1, X2), U52# mark X -> U52# X, U52# ok X -> U52# X, U51#(mark X1, X2) -> U51#(X1, X2), U51#(ok X1, ok X2) -> U51#(X1, X2), U61# mark X -> U61# X, U61# ok X -> U61# X, U72# mark X -> U72# X, U72# ok X -> U72# X, isPal# ok X -> isPal# X, U71#(mark X1, X2) -> U71#(X1, X2), U71#(ok X1, ok X2) -> U71#(X1, X2), U81# mark X -> U81# X, U81# ok X -> U81# X, isQid# ok X -> isQid# X, isNePal# ok X -> isNePal# X, proper# __(X1, X2) -> __#(proper X1, proper X2), proper# __(X1, X2) -> proper# X1, proper# __(X1, X2) -> proper# X2, proper# U11 X -> U11# proper X, proper# U11 X -> proper# X, proper# U22 X -> U22# proper X, proper# U22 X -> proper# X, proper# isList X -> isList# proper X, proper# isList X -> proper# X, proper# U21(X1, X2) -> U21#(proper X1, proper X2), proper# U21(X1, X2) -> proper# X1, proper# U21(X1, X2) -> proper# X2, proper# U31 X -> U31# proper X, proper# U31 X -> proper# X, proper# U42 X -> U42# proper X, proper# U42 X -> proper# X, proper# isNeList X -> isNeList# proper X, proper# isNeList X -> proper# X, proper# U41(X1, X2) -> U41#(proper X1, proper X2), proper# U41(X1, X2) -> proper# X1, proper# U41(X1, X2) -> proper# X2, proper# U52 X -> U52# proper X, proper# U52 X -> proper# X, proper# U51(X1, X2) -> U51#(proper X1, proper X2), proper# U51(X1, X2) -> proper# X1, proper# U51(X1, X2) -> proper# X2, proper# U61 X -> U61# proper X, proper# U61 X -> proper# X, proper# U72 X -> U72# proper X, proper# U72 X -> proper# X, proper# isPal X -> isPal# proper X, proper# isPal X -> proper# X, proper# U71(X1, X2) -> U71#(proper X1, proper X2), proper# U71(X1, X2) -> proper# X1, proper# U71(X1, X2) -> proper# X2, proper# U81 X -> U81# proper X, proper# U81 X -> proper# X, proper# isQid X -> isQid# proper X, proper# isQid X -> proper# X, 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 U11 X -> U11 active X, active U11 tt() -> mark tt(), active U22 X -> U22 active X, active U22 tt() -> mark tt(), active isList V -> mark U11 isNeList V, active isList __(V1, V2) -> mark U21(isList V1, V2), active isList nil() -> mark tt(), active U21(X1, X2) -> U21(active X1, X2), active U21(tt(), V2) -> mark U22 isList V2, active U31 X -> U31 active X, active U31 tt() -> mark tt(), active U42 X -> U42 active X, active U42 tt() -> mark tt(), active isNeList V -> mark U31 isQid V, active isNeList __(V1, V2) -> mark U41(isList V1, V2), active isNeList __(V1, V2) -> mark U51(isNeList V1, V2), active U41(X1, X2) -> U41(active X1, X2), active U41(tt(), V2) -> mark U42 isNeList V2, active U52 X -> U52 active X, active U52 tt() -> mark tt(), active U51(X1, X2) -> U51(active X1, X2), active U51(tt(), V2) -> mark U52 isList V2, active U61 X -> U61 active X, active U61 tt() -> mark tt(), active U72 X -> U72 active X, active U72 tt() -> mark tt(), active isPal V -> mark U81 isNePal V, active isPal nil() -> mark tt(), active U71(X1, X2) -> U71(active X1, X2), active U71(tt(), P) -> mark U72 isPal P, active U81 X -> U81 active X, active U81 tt() -> mark tt(), active isQid a() -> mark tt(), active isQid e() -> mark tt(), active isQid i() -> mark tt(), active isQid o() -> mark tt(), active isQid u() -> mark tt(), active isNePal V -> mark U61 isQid V, active isNePal __(I, __(P, I)) -> mark U71(isQid I, P), U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, U22 mark X -> mark U22 X, U22 ok X -> ok U22 X, isList ok X -> ok isList X, U21(mark X1, X2) -> mark U21(X1, X2), U21(ok X1, ok X2) -> ok U21(X1, X2), U31 mark X -> mark U31 X, U31 ok X -> ok U31 X, U42 mark X -> mark U42 X, U42 ok X -> ok U42 X, isNeList ok X -> ok isNeList X, U41(mark X1, X2) -> mark U41(X1, X2), U41(ok X1, ok X2) -> ok U41(X1, X2), U52 mark X -> mark U52 X, U52 ok X -> ok U52 X, U51(mark X1, X2) -> mark U51(X1, X2), U51(ok X1, ok X2) -> ok U51(X1, X2), U61 mark X -> mark U61 X, U61 ok X -> ok U61 X, U72 mark X -> mark U72 X, U72 ok X -> ok U72 X, isPal ok X -> ok isPal X, U71(mark X1, X2) -> mark U71(X1, X2), U71(ok X1, ok X2) -> ok U71(X1, X2), U81 mark X -> mark U81 X, U81 ok X -> ok U81 X, isQid ok X -> ok isQid X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper U22 X -> U22 proper X, proper isList X -> isList proper X, proper U21(X1, X2) -> U21(proper X1, proper X2), proper U31 X -> U31 proper X, proper U42 X -> U42 proper X, proper isNeList X -> isNeList proper X, proper U41(X1, X2) -> U41(proper X1, proper X2), proper U52 X -> U52 proper X, proper U51(X1, X2) -> U51(proper X1, proper X2), proper U61 X -> U61 proper X, proper U72 X -> U72 proper X, proper isPal X -> isPal proper X, proper U71(X1, X2) -> U71(proper X1, proper X2), proper U81 X -> U81 proper X, proper isQid X -> isQid proper X, proper isNePal X -> isNePal proper X, proper a() -> ok a(), proper e() -> ok e(), proper i() -> ok i(), proper o() -> ok o(), proper u() -> ok u(), top mark X -> top proper X, top ok X -> top active X} EDG: {(active# __(__(X, Y), Z) -> __#(X, __(Y, Z)), __#(X1, mark X2) -> __#(X1, X2)) (active# U21(X1, X2) -> U21#(active X1, X2), U21#(mark X1, X2) -> U21#(X1, X2)) (active# U51(X1, X2) -> U51#(active X1, X2), U51#(mark X1, X2) -> U51#(X1, X2)) (active# isList V -> U11# isNeList V, U11# ok X -> U11# X) (active# isPal V -> U81# isNePal V, U81# ok X -> U81# X) (active# U71(tt(), P) -> U72# isPal P, U72# ok X -> U72# X) (active# U41(tt(), V2) -> U42# isNeList V2, U42# ok X -> U42# X) (active# U11 X -> U11# active X, U11# ok X -> U11# X) (active# U11 X -> U11# active X, U11# mark X -> U11# X) (active# U31 X -> U31# active X, U31# ok X -> U31# X) (active# U31 X -> U31# active X, U31# mark X -> U31# X) (active# U52 X -> U52# active X, U52# ok X -> U52# X) (active# U52 X -> U52# active X, U52# mark X -> U52# X) (active# U72 X -> U72# active X, U72# ok X -> U72# X) (active# U72 X -> U72# active X, U72# mark X -> U72# X) (proper# U11 X -> U11# proper X, U11# ok X -> U11# X) (proper# isList X -> isList# proper X, isList# ok X -> isList# X) (proper# U42 X -> U42# proper X, U42# ok X -> U42# X) (proper# U52 X -> U52# proper X, U52# ok X -> U52# X) (proper# U72 X -> U72# proper X, U72# ok X -> U72# X) (proper# U81 X -> U81# proper X, U81# ok X -> U81# X) (proper# isNePal X -> isNePal# proper X, isNePal# ok X -> isNePal# X) (top# ok X -> top# active X, top# ok X -> top# active X) (top# ok X -> top# active X, top# ok X -> active# X) (top# ok X -> top# active X, top# mark X -> top# proper X) (top# ok X -> top# active X, top# mark X -> proper# X) (proper# __(X1, X2) -> __#(proper X1, proper X2), __#(ok X1, ok X2) -> __#(X1, X2)) (proper# U41(X1, X2) -> U41#(proper X1, proper X2), U41#(ok X1, ok X2) -> U41#(X1, X2)) (proper# U71(X1, X2) -> U71#(proper X1, proper X2), U71#(ok X1, ok X2) -> U71#(X1, X2)) (proper# U51(X1, X2) -> U51#(proper X1, proper X2), U51#(ok X1, ok X2) -> U51#(X1, X2)) (proper# U21(X1, X2) -> U21#(proper X1, proper X2), U21#(ok X1, ok X2) -> U21#(X1, X2)) (active# __(X1, X2) -> __#(X1, active X2), __#(X1, mark X2) -> __#(X1, X2)) (top# mark X -> top# proper X, top# mark X -> proper# X) (top# mark X -> top# proper X, top# mark X -> top# proper X) (top# mark X -> top# proper X, top# ok X -> active# X) (top# mark X -> top# proper X, top# ok X -> top# active X) (proper# isQid X -> isQid# proper X, isQid# ok X -> isQid# X) (proper# isPal X -> isPal# proper X, isPal# ok X -> isPal# X) (proper# U61 X -> U61# proper X, U61# ok X -> U61# X) (proper# isNeList X -> isNeList# proper X, isNeList# ok X -> isNeList# X) (proper# U31 X -> U31# proper X, U31# ok X -> U31# X) (proper# U22 X -> U22# proper X, U22# ok X -> U22# X) (active# U81 X -> U81# active X, U81# mark X -> U81# X) (active# U81 X -> U81# active X, U81# ok X -> U81# X) (active# U61 X -> U61# active X, U61# mark X -> U61# X) (active# U61 X -> U61# active X, U61# ok X -> U61# X) (active# U42 X -> U42# active X, U42# mark X -> U42# X) (active# U42 X -> U42# active X, U42# ok X -> U42# X) (active# U22 X -> U22# active X, U22# mark X -> U22# X) (active# U22 X -> U22# active X, U22# ok X -> U22# X) (active# U51(tt(), V2) -> U52# isList V2, U52# ok X -> U52# X) (active# U21(tt(), V2) -> U22# isList V2, U22# ok X -> U22# X) (active# isNePal V -> U61# isQid V, U61# ok X -> U61# X) (active# isNeList V -> U31# isQid V, U31# ok X -> U31# X) (active# U71(X1, X2) -> U71#(active X1, X2), U71#(mark X1, X2) -> U71#(X1, X2)) (active# U41(X1, X2) -> U41#(active X1, X2), U41#(mark X1, X2) -> U41#(X1, X2)) (active# __(X1, X2) -> __#(active X1, X2), __#(mark X1, X2) -> __#(X1, X2))} STATUS: arrows: 0.996679 SCCS (1): Scc: {top# mark X -> top# proper X, top# ok X -> top# active X} SCC (2): Strict: {top# mark X -> top# proper X, top# ok X -> top# active X} Weak: { __(X1, mark X2) -> mark __(X1, X2), __(mark X1, X2) -> mark __(X1, X2), __(ok X1, ok X2) -> ok __(X1, X2), active __(X, nil()) -> mark X, active __(X1, X2) -> __(X1, active X2), active __(X1, X2) -> __(active X1, X2), active __(__(X, Y), Z) -> mark __(X, __(Y, Z)), active __(nil(), X) -> mark X, active U11 X -> U11 active X, active U11 tt() -> mark tt(), active U22 X -> U22 active X, active U22 tt() -> mark tt(), active isList V -> mark U11 isNeList V, active isList __(V1, V2) -> mark U21(isList V1, V2), active isList nil() -> mark tt(), active U21(X1, X2) -> U21(active X1, X2), active U21(tt(), V2) -> mark U22 isList V2, active U31 X -> U31 active X, active U31 tt() -> mark tt(), active U42 X -> U42 active X, active U42 tt() -> mark tt(), active isNeList V -> mark U31 isQid V, active isNeList __(V1, V2) -> mark U41(isList V1, V2), active isNeList __(V1, V2) -> mark U51(isNeList V1, V2), active U41(X1, X2) -> U41(active X1, X2), active U41(tt(), V2) -> mark U42 isNeList V2, active U52 X -> U52 active X, active U52 tt() -> mark tt(), active U51(X1, X2) -> U51(active X1, X2), active U51(tt(), V2) -> mark U52 isList V2, active U61 X -> U61 active X, active U61 tt() -> mark tt(), active U72 X -> U72 active X, active U72 tt() -> mark tt(), active isPal V -> mark U81 isNePal V, active isPal nil() -> mark tt(), active U71(X1, X2) -> U71(active X1, X2), active U71(tt(), P) -> mark U72 isPal P, active U81 X -> U81 active X, active U81 tt() -> mark tt(), active isQid a() -> mark tt(), active isQid e() -> mark tt(), active isQid i() -> mark tt(), active isQid o() -> mark tt(), active isQid u() -> mark tt(), active isNePal V -> mark U61 isQid V, active isNePal __(I, __(P, I)) -> mark U71(isQid I, P), U11 mark X -> mark U11 X, U11 ok X -> ok U11 X, U22 mark X -> mark U22 X, U22 ok X -> ok U22 X, isList ok X -> ok isList X, U21(mark X1, X2) -> mark U21(X1, X2), U21(ok X1, ok X2) -> ok U21(X1, X2), U31 mark X -> mark U31 X, U31 ok X -> ok U31 X, U42 mark X -> mark U42 X, U42 ok X -> ok U42 X, isNeList ok X -> ok isNeList X, U41(mark X1, X2) -> mark U41(X1, X2), U41(ok X1, ok X2) -> ok U41(X1, X2), U52 mark X -> mark U52 X, U52 ok X -> ok U52 X, U51(mark X1, X2) -> mark U51(X1, X2), U51(ok X1, ok X2) -> ok U51(X1, X2), U61 mark X -> mark U61 X, U61 ok X -> ok U61 X, U72 mark X -> mark U72 X, U72 ok X -> ok U72 X, isPal ok X -> ok isPal X, U71(mark X1, X2) -> mark U71(X1, X2), U71(ok X1, ok X2) -> ok U71(X1, X2), U81 mark X -> mark U81 X, U81 ok X -> ok U81 X, isQid ok X -> ok isQid X, isNePal ok X -> ok isNePal X, proper __(X1, X2) -> __(proper X1, proper X2), proper nil() -> ok nil(), proper tt() -> ok tt(), proper U11 X -> U11 proper X, proper U22 X -> U22 proper X, proper isList X -> isList proper X, proper U21(X1, X2) -> U21(proper X1, proper X2), proper U31 X -> U31 proper X, proper U42 X -> U42 proper X, proper isNeList X -> isNeList proper X, proper U41(X1, X2) -> U41(proper X1, proper X2), proper U52 X -> U52 proper X, proper U51(X1, X2) -> U51(proper X1, proper X2), proper U61 X -> U61 proper X, proper U72 X -> U72 proper X, proper isPal X -> isPal proper X, proper U71(X1, X2) -> U71(proper X1, proper X2), proper U81 X -> U81 proper X, proper isQid X -> isQid proper X, proper isNePal X -> isNePal proper X, proper a() -> ok a(), proper e() -> ok e(), proper i() -> ok i(), proper o() -> ok o(), proper u() -> ok u(), top mark X -> top proper X, top ok X -> top active X} Open