MAYBE * Step 1: Failure MAYBE + Considered Problem: - Strict 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) a__and(X1,X2) -> and(X1,X2) a__and(tt(),X) -> mark(X) a__isList(V) -> a__isNeList(V) a__isList(X) -> isList(X) a__isList(__(V1,V2)) -> a__and(a__isList(V1),isList(V2)) a__isList(nil()) -> tt() a__isNeList(V) -> a__isQid(V) a__isNeList(X) -> isNeList(X) a__isNeList(__(V1,V2)) -> a__and(a__isList(V1),isNeList(V2)) a__isNeList(__(V1,V2)) -> a__and(a__isNeList(V1),isList(V2)) a__isNePal(V) -> a__isQid(V) a__isNePal(X) -> isNePal(X) a__isNePal(__(I,__(P,I))) -> a__and(a__isQid(I),isPal(P)) a__isPal(V) -> a__isNePal(V) a__isPal(X) -> isPal(X) a__isPal(nil()) -> tt() a__isQid(X) -> isQid(X) a__isQid(a()) -> tt() a__isQid(e()) -> tt() a__isQid(i()) -> tt() a__isQid(o()) -> tt() a__isQid(u()) -> tt() mark(__(X1,X2)) -> a____(mark(X1),mark(X2)) mark(a()) -> a() mark(and(X1,X2)) -> a__and(mark(X1),X2) mark(e()) -> e() mark(i()) -> i() mark(isList(X)) -> a__isList(X) mark(isNeList(X)) -> a__isNeList(X) mark(isNePal(X)) -> a__isNePal(X) mark(isPal(X)) -> a__isPal(X) mark(isQid(X)) -> a__isQid(X) mark(nil()) -> nil() mark(o()) -> o() mark(tt()) -> tt() mark(u()) -> u() - Signature: {a____/2,a__and/2,a__isList/1,a__isNeList/1,a__isNePal/1,a__isPal/1,a__isQid/1,mark/1} / {__/2,a/0,and/2,e/0 ,i/0,isList/1,isNeList/1,isNePal/1,isPal/1,isQid/1,nil/0,o/0,tt/0,u/0} - Obligation: innermost runtime complexity wrt. defined symbols {a____,a__and,a__isList,a__isNeList,a__isNePal,a__isPal ,a__isQid,mark} and constructors {__,a,and,e,i,isList,isNeList,isNePal,isPal,isQid,nil,o,tt,u} + Applied Processor: Ara {heuristics_ = NoHeuristics, minDegree = 1, maxDegree = 3, araTimeout = 60, araFindStrictRules = Nothing, araSmtSolver = MiniSMT} + Details: The input can not be schown compatible. MAYBE