MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , isList() -> U21(isList()) , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , isPal() -> U81(isNePal()) , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [0] [nil] = [2] [U11](x1) = [1] x1 + [0] [tt] = [0] [U21](x1) = [1] x1 + [4] [U22](x1) = [1] x1 + [0] [isList] = [0] [U31](x1) = [1] x1 + [0] [U41](x1) = [1] x1 + [0] [U42](x1) = [1] x1 + [0] [isNeList] = [0] [U51](x1) = [1] x1 + [0] [U52](x1) = [1] x1 + [0] [U61](x1) = [1] x1 + [0] [U71](x1) = [1] x1 + [0] [U72](x1) = [1] x1 + [0] [isPal] = [0] [U81](x1) = [1] x1 + [0] [isQid] = [0] [isNePal] = [0] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [2] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [0] >= [1] X + [1] Y + [1] Z + [0] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [2] > [1] X + [0] = [X] [U11(tt())] = [0] >= [0] = [tt()] [U21(tt())] = [4] > [0] = [U22(isList())] [U22(tt())] = [0] >= [0] = [tt()] [isList()] = [0] >= [0] = [U11(isNeList())] [isList()] = [0] >= [0] = [tt()] [isList()] = [0] ? [4] = [U21(isList())] [U31(tt())] = [0] >= [0] = [tt()] [U41(tt())] = [0] >= [0] = [U42(isNeList())] [U42(tt())] = [0] >= [0] = [tt()] [isNeList()] = [0] >= [0] = [U31(isQid())] [isNeList()] = [0] >= [0] = [U41(isList())] [isNeList()] = [0] >= [0] = [U51(isNeList())] [U51(tt())] = [0] >= [0] = [U52(isList())] [U52(tt())] = [0] >= [0] = [tt()] [U61(tt())] = [0] >= [0] = [tt()] [U71(tt())] = [0] >= [0] = [U72(isPal())] [U72(tt())] = [0] >= [0] = [tt()] [isPal()] = [0] >= [0] = [tt()] [isPal()] = [0] >= [0] = [U81(isNePal())] [U81(tt())] = [0] >= [0] = [tt()] [isQid()] = [0] >= [0] = [tt()] [isNePal()] = [0] >= [0] = [U61(isQid())] [isNePal()] = [0] >= [0] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , U11(tt()) -> tt() , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , isList() -> U21(isList()) , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , isPal() -> U81(isNePal()) , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U21(tt()) -> U22(isList()) } Obligation: runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [U11](x1) = [1] x1 + [0] [tt] = [1] [U21](x1) = [1] x1 + [0] [U22](x1) = [1] x1 + [0] [isList] = [1] [U31](x1) = [1] x1 + [0] [U41](x1) = [1] x1 + [0] [U42](x1) = [1] x1 + [0] [isNeList] = [0] [U51](x1) = [1] x1 + [0] [U52](x1) = [1] x1 + [0] [U61](x1) = [1] x1 + [0] [U71](x1) = [1] x1 + [0] [U72](x1) = [1] x1 + [0] [isPal] = [0] [U81](x1) = [1] x1 + [0] [isQid] = [0] [isNePal] = [0] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [14] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [14] >= [1] X + [1] Y + [1] Z + [14] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [14] > [1] X + [0] = [X] [U11(tt())] = [1] >= [1] = [tt()] [U21(tt())] = [1] >= [1] = [U22(isList())] [U22(tt())] = [1] >= [1] = [tt()] [isList()] = [1] > [0] = [U11(isNeList())] [isList()] = [1] >= [1] = [tt()] [isList()] = [1] >= [1] = [U21(isList())] [U31(tt())] = [1] >= [1] = [tt()] [U41(tt())] = [1] > [0] = [U42(isNeList())] [U42(tt())] = [1] >= [1] = [tt()] [isNeList()] = [0] >= [0] = [U31(isQid())] [isNeList()] = [0] ? [1] = [U41(isList())] [isNeList()] = [0] >= [0] = [U51(isNeList())] [U51(tt())] = [1] >= [1] = [U52(isList())] [U52(tt())] = [1] >= [1] = [tt()] [U61(tt())] = [1] >= [1] = [tt()] [U71(tt())] = [1] > [0] = [U72(isPal())] [U72(tt())] = [1] >= [1] = [tt()] [isPal()] = [0] ? [1] = [tt()] [isPal()] = [0] >= [0] = [U81(isNePal())] [U81(tt())] = [1] >= [1] = [tt()] [isQid()] = [0] ? [1] = [tt()] [isNePal()] = [0] >= [0] = [U61(isQid())] [isNePal()] = [0] >= [0] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , U11(tt()) -> tt() , U22(tt()) -> tt() , isList() -> tt() , isList() -> U21(isList()) , U31(tt()) -> tt() , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U72(tt()) -> tt() , isPal() -> tt() , isPal() -> U81(isNePal()) , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U21(tt()) -> U22(isList()) , isList() -> U11(isNeList()) , U41(tt()) -> U42(isNeList()) , U71(tt()) -> U72(isPal()) } Obligation: runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [U11](x1) = [1] x1 + [0] [tt] = [0] [U21](x1) = [1] x1 + [0] [U22](x1) = [1] x1 + [0] [isList] = [0] [U31](x1) = [1] x1 + [0] [U41](x1) = [1] x1 + [0] [U42](x1) = [1] x1 + [0] [isNeList] = [0] [U51](x1) = [1] x1 + [0] [U52](x1) = [1] x1 + [0] [U61](x1) = [1] x1 + [0] [U71](x1) = [1] x1 + [0] [U72](x1) = [1] x1 + [0] [isPal] = [0] [U81](x1) = [1] x1 + [0] [isQid] = [0] [isNePal] = [4] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [14] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [14] >= [1] X + [1] Y + [1] Z + [14] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [14] > [1] X + [0] = [X] [U11(tt())] = [0] >= [0] = [tt()] [U21(tt())] = [0] >= [0] = [U22(isList())] [U22(tt())] = [0] >= [0] = [tt()] [isList()] = [0] >= [0] = [U11(isNeList())] [isList()] = [0] >= [0] = [tt()] [isList()] = [0] >= [0] = [U21(isList())] [U31(tt())] = [0] >= [0] = [tt()] [U41(tt())] = [0] >= [0] = [U42(isNeList())] [U42(tt())] = [0] >= [0] = [tt()] [isNeList()] = [0] >= [0] = [U31(isQid())] [isNeList()] = [0] >= [0] = [U41(isList())] [isNeList()] = [0] >= [0] = [U51(isNeList())] [U51(tt())] = [0] >= [0] = [U52(isList())] [U52(tt())] = [0] >= [0] = [tt()] [U61(tt())] = [0] >= [0] = [tt()] [U71(tt())] = [0] >= [0] = [U72(isPal())] [U72(tt())] = [0] >= [0] = [tt()] [isPal()] = [0] >= [0] = [tt()] [isPal()] = [0] ? [4] = [U81(isNePal())] [U81(tt())] = [0] >= [0] = [tt()] [isQid()] = [0] >= [0] = [tt()] [isNePal()] = [4] > [0] = [U61(isQid())] [isNePal()] = [4] > [0] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , U11(tt()) -> tt() , U22(tt()) -> tt() , isList() -> tt() , isList() -> U21(isList()) , U31(tt()) -> tt() , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U72(tt()) -> tt() , isPal() -> tt() , isPal() -> U81(isNePal()) , U81(tt()) -> tt() , isQid() -> tt() } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U21(tt()) -> U22(isList()) , isList() -> U11(isNeList()) , U41(tt()) -> U42(isNeList()) , U71(tt()) -> U72(isPal()) , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [U11](x1) = [1] x1 + [3] [tt] = [7] [U21](x1) = [1] x1 + [7] [U22](x1) = [1] x1 + [7] [isList] = [7] [U31](x1) = [1] x1 + [7] [U41](x1) = [1] x1 + [7] [U42](x1) = [1] x1 + [7] [isNeList] = [3] [U51](x1) = [1] x1 + [7] [U52](x1) = [1] x1 + [7] [U61](x1) = [1] x1 + [7] [U71](x1) = [1] x1 + [7] [U72](x1) = [1] x1 + [7] [isPal] = [7] [U81](x1) = [1] x1 + [7] [isQid] = [0] [isNePal] = [7] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [14] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [14] >= [1] X + [1] Y + [1] Z + [14] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [14] > [1] X + [0] = [X] [U11(tt())] = [10] > [7] = [tt()] [U21(tt())] = [14] >= [14] = [U22(isList())] [U22(tt())] = [14] > [7] = [tt()] [isList()] = [7] > [6] = [U11(isNeList())] [isList()] = [7] >= [7] = [tt()] [isList()] = [7] ? [14] = [U21(isList())] [U31(tt())] = [14] > [7] = [tt()] [U41(tt())] = [14] > [10] = [U42(isNeList())] [U42(tt())] = [14] > [7] = [tt()] [isNeList()] = [3] ? [7] = [U31(isQid())] [isNeList()] = [3] ? [14] = [U41(isList())] [isNeList()] = [3] ? [10] = [U51(isNeList())] [U51(tt())] = [14] >= [14] = [U52(isList())] [U52(tt())] = [14] > [7] = [tt()] [U61(tt())] = [14] > [7] = [tt()] [U71(tt())] = [14] >= [14] = [U72(isPal())] [U72(tt())] = [14] > [7] = [tt()] [isPal()] = [7] >= [7] = [tt()] [isPal()] = [7] ? [14] = [U81(isNePal())] [U81(tt())] = [14] > [7] = [tt()] [isQid()] = [0] ? [7] = [tt()] [isNePal()] = [7] >= [7] = [U61(isQid())] [isNePal()] = [7] >= [7] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , isList() -> tt() , isList() -> U21(isList()) , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , isPal() -> tt() , isPal() -> U81(isNePal()) , isQid() -> tt() } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , U81(tt()) -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [U11](x1) = [1] x1 + [0] [tt] = [0] [U21](x1) = [1] x1 + [4] [U22](x1) = [1] x1 + [0] [isList] = [4] [U31](x1) = [1] x1 + [7] [U41](x1) = [1] x1 + [0] [U42](x1) = [1] x1 + [0] [isNeList] = [0] [U51](x1) = [1] x1 + [0] [U52](x1) = [1] x1 + [7] [U61](x1) = [1] x1 + [0] [U71](x1) = [1] x1 + [0] [U72](x1) = [1] x1 + [0] [isPal] = [0] [U81](x1) = [1] x1 + [7] [isQid] = [0] [isNePal] = [4] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [14] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [14] >= [1] X + [1] Y + [1] Z + [14] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [14] > [1] X + [0] = [X] [U11(tt())] = [0] >= [0] = [tt()] [U21(tt())] = [4] >= [4] = [U22(isList())] [U22(tt())] = [0] >= [0] = [tt()] [isList()] = [4] > [0] = [U11(isNeList())] [isList()] = [4] > [0] = [tt()] [isList()] = [4] ? [8] = [U21(isList())] [U31(tt())] = [7] > [0] = [tt()] [U41(tt())] = [0] >= [0] = [U42(isNeList())] [U42(tt())] = [0] >= [0] = [tt()] [isNeList()] = [0] ? [7] = [U31(isQid())] [isNeList()] = [0] ? [4] = [U41(isList())] [isNeList()] = [0] >= [0] = [U51(isNeList())] [U51(tt())] = [0] ? [11] = [U52(isList())] [U52(tt())] = [7] > [0] = [tt()] [U61(tt())] = [0] >= [0] = [tt()] [U71(tt())] = [0] >= [0] = [U72(isPal())] [U72(tt())] = [0] >= [0] = [tt()] [isPal()] = [0] >= [0] = [tt()] [isPal()] = [0] ? [11] = [U81(isNePal())] [U81(tt())] = [7] > [0] = [tt()] [isQid()] = [0] >= [0] = [tt()] [isNePal()] = [4] > [0] = [U61(isQid())] [isNePal()] = [4] > [0] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , isList() -> U21(isList()) , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , isPal() -> tt() , isPal() -> U81(isNePal()) , isQid() -> tt() } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , U81(tt()) -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [U11](x1) = [1] x1 + [0] [tt] = [4] [U21](x1) = [1] x1 + [4] [U22](x1) = [1] x1 + [3] [isList] = [4] [U31](x1) = [1] x1 + [7] [U41](x1) = [1] x1 + [0] [U42](x1) = [1] x1 + [3] [isNeList] = [0] [U51](x1) = [1] x1 + [4] [U52](x1) = [1] x1 + [3] [U61](x1) = [1] x1 + [0] [U71](x1) = [1] x1 + [0] [U72](x1) = [1] x1 + [3] [isPal] = [0] [U81](x1) = [1] x1 + [7] [isQid] = [0] [isNePal] = [0] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [14] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [14] >= [1] X + [1] Y + [1] Z + [14] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [14] > [1] X + [0] = [X] [U11(tt())] = [4] >= [4] = [tt()] [U21(tt())] = [8] > [7] = [U22(isList())] [U22(tt())] = [7] > [4] = [tt()] [isList()] = [4] > [0] = [U11(isNeList())] [isList()] = [4] >= [4] = [tt()] [isList()] = [4] ? [8] = [U21(isList())] [U31(tt())] = [11] > [4] = [tt()] [U41(tt())] = [4] > [3] = [U42(isNeList())] [U42(tt())] = [7] > [4] = [tt()] [isNeList()] = [0] ? [7] = [U31(isQid())] [isNeList()] = [0] ? [4] = [U41(isList())] [isNeList()] = [0] ? [4] = [U51(isNeList())] [U51(tt())] = [8] > [7] = [U52(isList())] [U52(tt())] = [7] > [4] = [tt()] [U61(tt())] = [4] >= [4] = [tt()] [U71(tt())] = [4] > [3] = [U72(isPal())] [U72(tt())] = [7] > [4] = [tt()] [isPal()] = [0] ? [4] = [tt()] [isPal()] = [0] ? [7] = [U81(isNePal())] [U81(tt())] = [11] > [4] = [tt()] [isQid()] = [0] ? [4] = [tt()] [isNePal()] = [0] >= [0] = [U61(isQid())] [isNePal()] = [0] >= [0] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , isList() -> U21(isList()) , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , isPal() -> tt() , isPal() -> U81(isNePal()) , isQid() -> tt() } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , U81(tt()) -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [U11](x1) = [1] x1 + [0] [tt] = [0] [U21](x1) = [1] x1 + [4] [U22](x1) = [1] x1 + [3] [isList] = [0] [U31](x1) = [1] x1 + [7] [U41](x1) = [1] x1 + [0] [U42](x1) = [1] x1 + [0] [isNeList] = [0] [U51](x1) = [1] x1 + [4] [U52](x1) = [1] x1 + [3] [U61](x1) = [1] x1 + [0] [U71](x1) = [1] x1 + [0] [U72](x1) = [1] x1 + [0] [isPal] = [0] [U81](x1) = [1] x1 + [7] [isQid] = [1] [isNePal] = [4] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [14] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [14] >= [1] X + [1] Y + [1] Z + [14] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [14] > [1] X + [0] = [X] [U11(tt())] = [0] >= [0] = [tt()] [U21(tt())] = [4] > [3] = [U22(isList())] [U22(tt())] = [3] > [0] = [tt()] [isList()] = [0] >= [0] = [U11(isNeList())] [isList()] = [0] >= [0] = [tt()] [isList()] = [0] ? [4] = [U21(isList())] [U31(tt())] = [7] > [0] = [tt()] [U41(tt())] = [0] >= [0] = [U42(isNeList())] [U42(tt())] = [0] >= [0] = [tt()] [isNeList()] = [0] ? [8] = [U31(isQid())] [isNeList()] = [0] >= [0] = [U41(isList())] [isNeList()] = [0] ? [4] = [U51(isNeList())] [U51(tt())] = [4] > [3] = [U52(isList())] [U52(tt())] = [3] > [0] = [tt()] [U61(tt())] = [0] >= [0] = [tt()] [U71(tt())] = [0] >= [0] = [U72(isPal())] [U72(tt())] = [0] >= [0] = [tt()] [isPal()] = [0] >= [0] = [tt()] [isPal()] = [0] ? [11] = [U81(isNePal())] [U81(tt())] = [7] > [0] = [tt()] [isQid()] = [1] > [0] = [tt()] [isNePal()] = [4] > [1] = [U61(isQid())] [isNePal()] = [4] > [1] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , isList() -> U21(isList()) , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , isPal() -> tt() , isPal() -> U81(isNePal()) } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [U11](x1) = [1] x1 + [0] [tt] = [0] [U21](x1) = [1] x1 + [0] [U22](x1) = [1] x1 + [0] [isList] = [0] [U31](x1) = [1] x1 + [7] [U41](x1) = [1] x1 + [0] [U42](x1) = [1] x1 + [0] [isNeList] = [0] [U51](x1) = [1] x1 + [0] [U52](x1) = [1] x1 + [0] [U61](x1) = [1] x1 + [4] [U71](x1) = [1] x1 + [4] [U72](x1) = [1] x1 + [0] [isPal] = [4] [U81](x1) = [1] x1 + [7] [isQid] = [0] [isNePal] = [4] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [14] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [14] >= [1] X + [1] Y + [1] Z + [14] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [14] > [1] X + [0] = [X] [U11(tt())] = [0] >= [0] = [tt()] [U21(tt())] = [0] >= [0] = [U22(isList())] [U22(tt())] = [0] >= [0] = [tt()] [isList()] = [0] >= [0] = [U11(isNeList())] [isList()] = [0] >= [0] = [tt()] [isList()] = [0] >= [0] = [U21(isList())] [U31(tt())] = [7] > [0] = [tt()] [U41(tt())] = [0] >= [0] = [U42(isNeList())] [U42(tt())] = [0] >= [0] = [tt()] [isNeList()] = [0] ? [7] = [U31(isQid())] [isNeList()] = [0] >= [0] = [U41(isList())] [isNeList()] = [0] >= [0] = [U51(isNeList())] [U51(tt())] = [0] >= [0] = [U52(isList())] [U52(tt())] = [0] >= [0] = [tt()] [U61(tt())] = [4] > [0] = [tt()] [U71(tt())] = [4] >= [4] = [U72(isPal())] [U72(tt())] = [0] >= [0] = [tt()] [isPal()] = [4] > [0] = [tt()] [isPal()] = [4] ? [11] = [U81(isNePal())] [U81(tt())] = [7] > [0] = [tt()] [isQid()] = [0] >= [0] = [tt()] [isNePal()] = [4] >= [4] = [U61(isQid())] [isNePal()] = [4] >= [4] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , isList() -> U21(isList()) , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , isPal() -> U81(isNePal()) } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE The weightgap principle applies (using the following nonconstant growth matrix-interpretation) The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following matrix interpretation satisfying not(EDA) and not(IDA(1)). [__](x1, x2) = [1] x1 + [1] x2 + [7] [nil] = [7] [U11](x1) = [1] x1 + [0] [tt] = [0] [U21](x1) = [1] x1 + [4] [U22](x1) = [1] x1 + [0] [isList] = [4] [U31](x1) = [1] x1 + [0] [U41](x1) = [1] x1 + [1] [U42](x1) = [1] x1 + [0] [isNeList] = [1] [U51](x1) = [1] x1 + [4] [U52](x1) = [1] x1 + [0] [U61](x1) = [1] x1 + [0] [U71](x1) = [1] x1 + [0] [U72](x1) = [1] x1 + [0] [isPal] = [0] [U81](x1) = [1] x1 + [7] [isQid] = [0] [isNePal] = [4] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [1] X + [14] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [1] X + [1] Y + [1] Z + [14] >= [1] X + [1] Y + [1] Z + [14] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [14] > [1] X + [0] = [X] [U11(tt())] = [0] >= [0] = [tt()] [U21(tt())] = [4] >= [4] = [U22(isList())] [U22(tt())] = [0] >= [0] = [tt()] [isList()] = [4] > [1] = [U11(isNeList())] [isList()] = [4] > [0] = [tt()] [isList()] = [4] ? [8] = [U21(isList())] [U31(tt())] = [0] >= [0] = [tt()] [U41(tt())] = [1] >= [1] = [U42(isNeList())] [U42(tt())] = [0] >= [0] = [tt()] [isNeList()] = [1] > [0] = [U31(isQid())] [isNeList()] = [1] ? [5] = [U41(isList())] [isNeList()] = [1] ? [5] = [U51(isNeList())] [U51(tt())] = [4] >= [4] = [U52(isList())] [U52(tt())] = [0] >= [0] = [tt()] [U61(tt())] = [0] >= [0] = [tt()] [U71(tt())] = [0] >= [0] = [U72(isPal())] [U72(tt())] = [0] >= [0] = [tt()] [isPal()] = [0] >= [0] = [tt()] [isPal()] = [0] ? [11] = [U81(isNePal())] [U81(tt())] = [7] > [0] = [tt()] [isQid()] = [0] >= [0] = [tt()] [isNePal()] = [4] > [0] = [U61(isQid())] [isNePal()] = [4] > [0] = [U71(isQid())] Further, it can be verified that all rules not oriented are covered by the weightgap condition. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) , isList() -> U21(isList()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , isPal() -> U81(isNePal()) } Weak Trs: { __(X, nil()) -> X , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE We use the processor 'matrix interpretation of dimension 1' to orient following rules strictly. Trs: { __(__(X, Y), Z) -> __(X, __(Y, Z)) } The induced complexity on above rules (modulo remaining rules) is YES(?,O(n^1)) . These rules are moved into the corresponding weak component(s). Sub-proof: ---------- The following argument positions are usable: Uargs(__) = {2}, Uargs(U11) = {1}, Uargs(U21) = {1}, Uargs(U22) = {1}, Uargs(U31) = {1}, Uargs(U41) = {1}, Uargs(U42) = {1}, Uargs(U51) = {1}, Uargs(U52) = {1}, Uargs(U61) = {1}, Uargs(U71) = {1}, Uargs(U72) = {1}, Uargs(U81) = {1} TcT has computed the following constructor-based matrix interpretation satisfying not(EDA). [__](x1, x2) = [3] x1 + [1] x2 + [2] [nil] = [1] [U11](x1) = [4] x1 + [0] [tt] = [0] [U21](x1) = [1] x1 + [0] [U22](x1) = [1] x1 + [0] [isList] = [0] [U31](x1) = [1] x1 + [0] [U41](x1) = [2] x1 + [0] [U42](x1) = [1] x1 + [0] [isNeList] = [0] [U51](x1) = [1] x1 + [0] [U52](x1) = [4] x1 + [0] [U61](x1) = [4] x1 + [0] [U71](x1) = [1] x1 + [0] [U72](x1) = [1] x1 + [0] [isPal] = [0] [U81](x1) = [2] x1 + [0] [isQid] = [0] [isNePal] = [0] The following symbols are considered usable {__, U11, U21, U22, isList, U31, U41, U42, isNeList, U51, U52, U61, U71, U72, isPal, U81, isQid, isNePal} The order satisfies the following ordering constraints: [__(X, nil())] = [3] X + [3] > [1] X + [0] = [X] [__(__(X, Y), Z)] = [9] X + [3] Y + [1] Z + [8] > [3] X + [3] Y + [1] Z + [4] = [__(X, __(Y, Z))] [__(nil(), X)] = [1] X + [5] > [1] X + [0] = [X] [U11(tt())] = [0] >= [0] = [tt()] [U21(tt())] = [0] >= [0] = [U22(isList())] [U22(tt())] = [0] >= [0] = [tt()] [isList()] = [0] >= [0] = [U11(isNeList())] [isList()] = [0] >= [0] = [tt()] [isList()] = [0] >= [0] = [U21(isList())] [U31(tt())] = [0] >= [0] = [tt()] [U41(tt())] = [0] >= [0] = [U42(isNeList())] [U42(tt())] = [0] >= [0] = [tt()] [isNeList()] = [0] >= [0] = [U31(isQid())] [isNeList()] = [0] >= [0] = [U41(isList())] [isNeList()] = [0] >= [0] = [U51(isNeList())] [U51(tt())] = [0] >= [0] = [U52(isList())] [U52(tt())] = [0] >= [0] = [tt()] [U61(tt())] = [0] >= [0] = [tt()] [U71(tt())] = [0] >= [0] = [U72(isPal())] [U72(tt())] = [0] >= [0] = [tt()] [isPal()] = [0] >= [0] = [tt()] [isPal()] = [0] >= [0] = [U81(isNePal())] [U81(tt())] = [0] >= [0] = [tt()] [isQid()] = [0] >= [0] = [tt()] [isNePal()] = [0] >= [0] = [U61(isQid())] [isNePal()] = [0] >= [0] = [U71(isQid())] We return to the main proof. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { isList() -> U21(isList()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , isPal() -> U81(isNePal()) } Weak Trs: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'empty' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'WithProblem' failed due to the following reason: Empty strict component of the problem is NOT empty. 2) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 5.0 seconds. 3) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { __^#(X, nil()) -> c_1(X) , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_3(X) , U11^#(tt()) -> c_4() , U21^#(tt()) -> c_5(U22^#(isList())) , U22^#(tt()) -> c_6() , isList^#() -> c_7(U11^#(isNeList())) , isList^#() -> c_8() , isList^#() -> c_9(U21^#(isList())) , U31^#(tt()) -> c_10() , U41^#(tt()) -> c_11(U42^#(isNeList())) , U42^#(tt()) -> c_12() , isNeList^#() -> c_13(U31^#(isQid())) , isNeList^#() -> c_14(U41^#(isList())) , isNeList^#() -> c_15(U51^#(isNeList())) , U51^#(tt()) -> c_16(U52^#(isList())) , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U71^#(tt()) -> c_19(U72^#(isPal())) , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , isPal^#() -> c_22(U81^#(isNePal())) , U81^#(tt()) -> c_23() , isQid^#() -> c_24() , isNePal^#() -> c_25(U61^#(isQid())) , isNePal^#() -> c_26(U71^#(isQid())) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X, nil()) -> c_1(X) , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_3(X) , U11^#(tt()) -> c_4() , U21^#(tt()) -> c_5(U22^#(isList())) , U22^#(tt()) -> c_6() , isList^#() -> c_7(U11^#(isNeList())) , isList^#() -> c_8() , isList^#() -> c_9(U21^#(isList())) , U31^#(tt()) -> c_10() , U41^#(tt()) -> c_11(U42^#(isNeList())) , U42^#(tt()) -> c_12() , isNeList^#() -> c_13(U31^#(isQid())) , isNeList^#() -> c_14(U41^#(isList())) , isNeList^#() -> c_15(U51^#(isNeList())) , U51^#(tt()) -> c_16(U52^#(isList())) , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U71^#(tt()) -> c_19(U72^#(isPal())) , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , isPal^#() -> c_22(U81^#(isNePal())) , U81^#(tt()) -> c_23() , isQid^#() -> c_24() , isNePal^#() -> c_25(U61^#(isQid())) , isNePal^#() -> c_26(U71^#(isQid())) } Strict Trs: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , isList() -> U21(isList()) , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , isPal() -> U81(isNePal()) , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {4,6,8,10,12,17,18,20,21,23,24} by applications of Pre({4,6,8,10,12,17,18,20,21,23,24}) = {1,3,5,7,11,13,16,19,22,25}. Here rules are labeled as follows: DPs: { 1: __^#(X, nil()) -> c_1(X) , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z))) , 3: __^#(nil(), X) -> c_3(X) , 4: U11^#(tt()) -> c_4() , 5: U21^#(tt()) -> c_5(U22^#(isList())) , 6: U22^#(tt()) -> c_6() , 7: isList^#() -> c_7(U11^#(isNeList())) , 8: isList^#() -> c_8() , 9: isList^#() -> c_9(U21^#(isList())) , 10: U31^#(tt()) -> c_10() , 11: U41^#(tt()) -> c_11(U42^#(isNeList())) , 12: U42^#(tt()) -> c_12() , 13: isNeList^#() -> c_13(U31^#(isQid())) , 14: isNeList^#() -> c_14(U41^#(isList())) , 15: isNeList^#() -> c_15(U51^#(isNeList())) , 16: U51^#(tt()) -> c_16(U52^#(isList())) , 17: U52^#(tt()) -> c_17() , 18: U61^#(tt()) -> c_18() , 19: U71^#(tt()) -> c_19(U72^#(isPal())) , 20: U72^#(tt()) -> c_20() , 21: isPal^#() -> c_21() , 22: isPal^#() -> c_22(U81^#(isNePal())) , 23: U81^#(tt()) -> c_23() , 24: isQid^#() -> c_24() , 25: isNePal^#() -> c_25(U61^#(isQid())) , 26: isNePal^#() -> c_26(U71^#(isQid())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X, nil()) -> c_1(X) , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_3(X) , U21^#(tt()) -> c_5(U22^#(isList())) , isList^#() -> c_7(U11^#(isNeList())) , isList^#() -> c_9(U21^#(isList())) , U41^#(tt()) -> c_11(U42^#(isNeList())) , isNeList^#() -> c_13(U31^#(isQid())) , isNeList^#() -> c_14(U41^#(isList())) , isNeList^#() -> c_15(U51^#(isNeList())) , U51^#(tt()) -> c_16(U52^#(isList())) , U71^#(tt()) -> c_19(U72^#(isPal())) , isPal^#() -> c_22(U81^#(isNePal())) , isNePal^#() -> c_25(U61^#(isQid())) , isNePal^#() -> c_26(U71^#(isQid())) } Strict Trs: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , isList() -> U21(isList()) , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , isPal() -> U81(isNePal()) , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Weak DPs: { U11^#(tt()) -> c_4() , U22^#(tt()) -> c_6() , isList^#() -> c_8() , U31^#(tt()) -> c_10() , U42^#(tt()) -> c_12() , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , U81^#(tt()) -> c_23() , isQid^#() -> c_24() } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {4,5,7,8,11,12,13,14} by applications of Pre({4,5,7,8,11,12,13,14}) = {1,3,6,9,10,15}. Here rules are labeled as follows: DPs: { 1: __^#(X, nil()) -> c_1(X) , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z))) , 3: __^#(nil(), X) -> c_3(X) , 4: U21^#(tt()) -> c_5(U22^#(isList())) , 5: isList^#() -> c_7(U11^#(isNeList())) , 6: isList^#() -> c_9(U21^#(isList())) , 7: U41^#(tt()) -> c_11(U42^#(isNeList())) , 8: isNeList^#() -> c_13(U31^#(isQid())) , 9: isNeList^#() -> c_14(U41^#(isList())) , 10: isNeList^#() -> c_15(U51^#(isNeList())) , 11: U51^#(tt()) -> c_16(U52^#(isList())) , 12: U71^#(tt()) -> c_19(U72^#(isPal())) , 13: isPal^#() -> c_22(U81^#(isNePal())) , 14: isNePal^#() -> c_25(U61^#(isQid())) , 15: isNePal^#() -> c_26(U71^#(isQid())) , 16: U11^#(tt()) -> c_4() , 17: U22^#(tt()) -> c_6() , 18: isList^#() -> c_8() , 19: U31^#(tt()) -> c_10() , 20: U42^#(tt()) -> c_12() , 21: U52^#(tt()) -> c_17() , 22: U61^#(tt()) -> c_18() , 23: U72^#(tt()) -> c_20() , 24: isPal^#() -> c_21() , 25: U81^#(tt()) -> c_23() , 26: isQid^#() -> c_24() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X, nil()) -> c_1(X) , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_3(X) , isList^#() -> c_9(U21^#(isList())) , isNeList^#() -> c_14(U41^#(isList())) , isNeList^#() -> c_15(U51^#(isNeList())) , isNePal^#() -> c_26(U71^#(isQid())) } Strict Trs: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , isList() -> U21(isList()) , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , isPal() -> U81(isNePal()) , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Weak DPs: { U11^#(tt()) -> c_4() , U21^#(tt()) -> c_5(U22^#(isList())) , U22^#(tt()) -> c_6() , isList^#() -> c_7(U11^#(isNeList())) , isList^#() -> c_8() , U31^#(tt()) -> c_10() , U41^#(tt()) -> c_11(U42^#(isNeList())) , U42^#(tt()) -> c_12() , isNeList^#() -> c_13(U31^#(isQid())) , U51^#(tt()) -> c_16(U52^#(isList())) , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U71^#(tt()) -> c_19(U72^#(isPal())) , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , isPal^#() -> c_22(U81^#(isNePal())) , U81^#(tt()) -> c_23() , isQid^#() -> c_24() , isNePal^#() -> c_25(U61^#(isQid())) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {4,5,6,7} by applications of Pre({4,5,6,7}) = {1,3}. Here rules are labeled as follows: DPs: { 1: __^#(X, nil()) -> c_1(X) , 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z))) , 3: __^#(nil(), X) -> c_3(X) , 4: isList^#() -> c_9(U21^#(isList())) , 5: isNeList^#() -> c_14(U41^#(isList())) , 6: isNeList^#() -> c_15(U51^#(isNeList())) , 7: isNePal^#() -> c_26(U71^#(isQid())) , 8: U11^#(tt()) -> c_4() , 9: U21^#(tt()) -> c_5(U22^#(isList())) , 10: U22^#(tt()) -> c_6() , 11: isList^#() -> c_7(U11^#(isNeList())) , 12: isList^#() -> c_8() , 13: U31^#(tt()) -> c_10() , 14: U41^#(tt()) -> c_11(U42^#(isNeList())) , 15: U42^#(tt()) -> c_12() , 16: isNeList^#() -> c_13(U31^#(isQid())) , 17: U51^#(tt()) -> c_16(U52^#(isList())) , 18: U52^#(tt()) -> c_17() , 19: U61^#(tt()) -> c_18() , 20: U71^#(tt()) -> c_19(U72^#(isPal())) , 21: U72^#(tt()) -> c_20() , 22: isPal^#() -> c_21() , 23: isPal^#() -> c_22(U81^#(isNePal())) , 24: U81^#(tt()) -> c_23() , 25: isQid^#() -> c_24() , 26: isNePal^#() -> c_25(U61^#(isQid())) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X, nil()) -> c_1(X) , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z))) , __^#(nil(), X) -> c_3(X) } Strict Trs: { __(X, nil()) -> X , __(__(X, Y), Z) -> __(X, __(Y, Z)) , __(nil(), X) -> X , U11(tt()) -> tt() , U21(tt()) -> U22(isList()) , U22(tt()) -> tt() , isList() -> U11(isNeList()) , isList() -> tt() , isList() -> U21(isList()) , U31(tt()) -> tt() , U41(tt()) -> U42(isNeList()) , U42(tt()) -> tt() , isNeList() -> U31(isQid()) , isNeList() -> U41(isList()) , isNeList() -> U51(isNeList()) , U51(tt()) -> U52(isList()) , U52(tt()) -> tt() , U61(tt()) -> tt() , U71(tt()) -> U72(isPal()) , U72(tt()) -> tt() , isPal() -> tt() , isPal() -> U81(isNePal()) , U81(tt()) -> tt() , isQid() -> tt() , isNePal() -> U61(isQid()) , isNePal() -> U71(isQid()) } Weak DPs: { U11^#(tt()) -> c_4() , U21^#(tt()) -> c_5(U22^#(isList())) , U22^#(tt()) -> c_6() , isList^#() -> c_7(U11^#(isNeList())) , isList^#() -> c_8() , isList^#() -> c_9(U21^#(isList())) , U31^#(tt()) -> c_10() , U41^#(tt()) -> c_11(U42^#(isNeList())) , U42^#(tt()) -> c_12() , isNeList^#() -> c_13(U31^#(isQid())) , isNeList^#() -> c_14(U41^#(isList())) , isNeList^#() -> c_15(U51^#(isNeList())) , U51^#(tt()) -> c_16(U52^#(isList())) , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U71^#(tt()) -> c_19(U72^#(isPal())) , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , isPal^#() -> c_22(U81^#(isNePal())) , U81^#(tt()) -> c_23() , isQid^#() -> c_24() , isNePal^#() -> c_25(U61^#(isQid())) , isNePal^#() -> c_26(U71^#(isQid())) } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..