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: innermost 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) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: We add the following dependency tuples: Strict DPs: { __^#(X, nil()) -> c_1() , __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)), __^#(Y, Z)) , __^#(nil(), X) -> c_3() , U11^#(tt()) -> c_4() , U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , U22^#(tt()) -> c_6() , isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , isList^#() -> c_8() , isList^#() -> c_9(U21^#(isList()), isList^#()) , isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) , isNeList^#() -> c_14(U41^#(isList()), isList^#()) , isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) , U31^#(tt()) -> c_10() , U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , U42^#(tt()) -> c_12() , isQid^#() -> c_24() , U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , U81^#(tt()) -> c_23() , isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) , isNePal^#() -> c_26(U71^#(isQid()), 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, Y), Z) -> c_2(__^#(X, __(Y, Z)), __^#(Y, Z)) , __^#(nil(), X) -> c_3() , U11^#(tt()) -> c_4() , U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , U22^#(tt()) -> c_6() , isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , isList^#() -> c_8() , isList^#() -> c_9(U21^#(isList()), isList^#()) , isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) , isNeList^#() -> c_14(U41^#(isList()), isList^#()) , isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) , U31^#(tt()) -> c_10() , U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , U42^#(tt()) -> c_12() , isQid^#() -> c_24() , U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , U81^#(tt()) -> c_23() , isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) , isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) } 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() , 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: innermost runtime complexity Answer: MAYBE Consider the dependency graph: 1: __^#(X, nil()) -> c_1() 2: __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)), __^#(Y, Z)) -->_2 __^#(__(X, Y), Z) -> c_2(__^#(X, __(Y, Z)), __^#(Y, Z)) :2 -->_2 __^#(X, nil()) -> c_1() :1 -->_1 __^#(X, nil()) -> c_1() :1 3: __^#(nil(), X) -> c_3() 4: U11^#(tt()) -> c_4() 5: U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) -->_2 isList^#() -> c_9(U21^#(isList()), isList^#()) :9 -->_2 isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) :7 -->_2 isList^#() -> c_8() :8 -->_1 U22^#(tt()) -> c_6() :6 6: U22^#(tt()) -> c_6() 7: isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) -->_2 isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) :12 -->_2 isNeList^#() -> c_14(U41^#(isList()), isList^#()) :11 -->_2 isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) :10 -->_1 U11^#(tt()) -> c_4() :4 8: isList^#() -> c_8() 9: isList^#() -> c_9(U21^#(isList()), isList^#()) -->_2 isList^#() -> c_9(U21^#(isList()), isList^#()) :9 -->_2 isList^#() -> c_8() :8 -->_2 isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) :7 -->_1 U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) :5 10: isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) -->_2 isQid^#() -> c_24() :16 -->_1 U31^#(tt()) -> c_10() :13 11: isNeList^#() -> c_14(U41^#(isList()), isList^#()) -->_1 U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) :14 -->_2 isList^#() -> c_9(U21^#(isList()), isList^#()) :9 -->_2 isList^#() -> c_8() :8 -->_2 isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) :7 12: isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) -->_1 U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) :17 -->_2 isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) :12 -->_2 isNeList^#() -> c_14(U41^#(isList()), isList^#()) :11 -->_2 isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) :10 13: U31^#(tt()) -> c_10() 14: U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) -->_1 U42^#(tt()) -> c_12() :15 -->_2 isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) :12 -->_2 isNeList^#() -> c_14(U41^#(isList()), isList^#()) :11 -->_2 isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) :10 15: U42^#(tt()) -> c_12() 16: isQid^#() -> c_24() 17: U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) -->_1 U52^#(tt()) -> c_17() :18 -->_2 isList^#() -> c_9(U21^#(isList()), isList^#()) :9 -->_2 isList^#() -> c_8() :8 -->_2 isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) :7 18: U52^#(tt()) -> c_17() 19: U61^#(tt()) -> c_18() 20: U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) -->_2 isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) :23 -->_2 isPal^#() -> c_21() :22 -->_1 U72^#(tt()) -> c_20() :21 21: U72^#(tt()) -> c_20() 22: isPal^#() -> c_21() 23: isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) -->_2 isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) :26 -->_2 isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) :25 -->_1 U81^#(tt()) -> c_23() :24 24: U81^#(tt()) -> c_23() 25: isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) -->_1 U61^#(tt()) -> c_18() :19 -->_2 isQid^#() -> c_24() :16 26: isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) -->_1 U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) :20 -->_2 isQid^#() -> c_24() :16 Only the nodes {1,3,4,5,9,8,7,12,17,18,11,14,15,10,16,13,6,19,20,23,26,25,24,22,21} are reachable from nodes {1,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { __^#(X, nil()) -> c_1() , __^#(nil(), X) -> c_3() , U11^#(tt()) -> c_4() , U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , U22^#(tt()) -> c_6() , isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , isList^#() -> c_8() , isList^#() -> c_9(U21^#(isList()), isList^#()) , isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) , isNeList^#() -> c_14(U41^#(isList()), isList^#()) , isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) , U31^#(tt()) -> c_10() , U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , U42^#(tt()) -> c_12() , isQid^#() -> c_24() , U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , U81^#(tt()) -> c_23() , isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) , isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) } 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() , 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: innermost runtime complexity Answer: MAYBE We estimate the number of application of {1,2,3,5,7,12,14,15,17,18,20,21,23} by applications of Pre({1,2,3,5,7,12,14,15,17,18,20,21,23}) = {4,6,8,9,10,13,16,19,22,24,25}. Here rules are labeled as follows: DPs: { 1: __^#(X, nil()) -> c_1() , 2: __^#(nil(), X) -> c_3() , 3: U11^#(tt()) -> c_4() , 4: U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , 5: U22^#(tt()) -> c_6() , 6: isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , 7: isList^#() -> c_8() , 8: isList^#() -> c_9(U21^#(isList()), isList^#()) , 9: isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) , 10: isNeList^#() -> c_14(U41^#(isList()), isList^#()) , 11: isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) , 12: U31^#(tt()) -> c_10() , 13: U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , 14: U42^#(tt()) -> c_12() , 15: isQid^#() -> c_24() , 16: U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , 17: U52^#(tt()) -> c_17() , 18: U61^#(tt()) -> c_18() , 19: U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , 20: U72^#(tt()) -> c_20() , 21: isPal^#() -> c_21() , 22: isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , 23: U81^#(tt()) -> c_23() , 24: isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) , 25: isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , isList^#() -> c_9(U21^#(isList()), isList^#()) , isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) , isNeList^#() -> c_14(U41^#(isList()), isList^#()) , isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) , U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) , isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) } Weak DPs: { __^#(X, nil()) -> c_1() , __^#(nil(), X) -> c_3() , U11^#(tt()) -> c_4() , U22^#(tt()) -> c_6() , isList^#() -> c_8() , U31^#(tt()) -> c_10() , U42^#(tt()) -> c_12() , isQid^#() -> c_24() , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , U81^#(tt()) -> c_23() } 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() , 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: innermost runtime complexity Answer: MAYBE We estimate the number of application of {4,11} by applications of Pre({4,11}) = {2,6,7,10}. Here rules are labeled as follows: DPs: { 1: U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , 2: isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , 3: isList^#() -> c_9(U21^#(isList()), isList^#()) , 4: isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) , 5: isNeList^#() -> c_14(U41^#(isList()), isList^#()) , 6: isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) , 7: U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , 8: U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , 9: U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , 10: isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , 11: isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) , 12: isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) , 13: __^#(X, nil()) -> c_1() , 14: __^#(nil(), X) -> c_3() , 15: U11^#(tt()) -> c_4() , 16: U22^#(tt()) -> c_6() , 17: isList^#() -> c_8() , 18: U31^#(tt()) -> c_10() , 19: U42^#(tt()) -> c_12() , 20: isQid^#() -> c_24() , 21: U52^#(tt()) -> c_17() , 22: U61^#(tt()) -> c_18() , 23: U72^#(tt()) -> c_20() , 24: isPal^#() -> c_21() , 25: U81^#(tt()) -> c_23() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , isList^#() -> c_9(U21^#(isList()), isList^#()) , isNeList^#() -> c_14(U41^#(isList()), isList^#()) , isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) , U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) } Weak DPs: { __^#(X, nil()) -> c_1() , __^#(nil(), X) -> c_3() , U11^#(tt()) -> c_4() , U22^#(tt()) -> c_6() , isList^#() -> c_8() , isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) , U31^#(tt()) -> c_10() , U42^#(tt()) -> c_12() , isQid^#() -> c_24() , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , U81^#(tt()) -> c_23() , isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) } 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() , 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: innermost runtime complexity Answer: MAYBE The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. { __^#(X, nil()) -> c_1() , __^#(nil(), X) -> c_3() , U11^#(tt()) -> c_4() , U22^#(tt()) -> c_6() , isList^#() -> c_8() , isNeList^#() -> c_13(U31^#(isQid()), isQid^#()) , U31^#(tt()) -> c_10() , U42^#(tt()) -> c_12() , isQid^#() -> c_24() , U52^#(tt()) -> c_17() , U61^#(tt()) -> c_18() , U72^#(tt()) -> c_20() , isPal^#() -> c_21() , U81^#(tt()) -> c_23() , isNePal^#() -> c_25(U61^#(isQid()), isQid^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , isList^#() -> c_9(U21^#(isList()), isList^#()) , isNeList^#() -> c_14(U41^#(isList()), isList^#()) , isNeList^#() -> c_15(U51^#(isNeList()), isNeList^#()) , U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) } 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() , 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: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { U21^#(tt()) -> c_5(U22^#(isList()), isList^#()) , isList^#() -> c_7(U11^#(isNeList()), isNeList^#()) , U41^#(tt()) -> c_11(U42^#(isNeList()), isNeList^#()) , U51^#(tt()) -> c_16(U52^#(isList()), isList^#()) , U71^#(tt()) -> c_19(U72^#(isPal()), isPal^#()) , isPal^#() -> c_22(U81^#(isNePal()), isNePal^#()) , isNePal^#() -> c_26(U71^#(isQid()), isQid^#()) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U21^#(tt()) -> c_1(isList^#()) , isList^#() -> c_2(U21^#(isList()), isList^#()) , isList^#() -> c_3(isNeList^#()) , isNeList^#() -> c_4(U41^#(isList()), isList^#()) , isNeList^#() -> c_5(U51^#(isNeList()), isNeList^#()) , U41^#(tt()) -> c_6(isNeList^#()) , U51^#(tt()) -> c_7(isList^#()) , U71^#(tt()) -> c_8(isPal^#()) , isPal^#() -> c_9(isNePal^#()) , isNePal^#() -> c_10(U71^#(isQid())) } 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() , 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: innermost runtime complexity Answer: MAYBE We replace rewrite rules by usable rules: Weak Usable Rules: { 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() , isQid() -> tt() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { U21^#(tt()) -> c_1(isList^#()) , isList^#() -> c_2(U21^#(isList()), isList^#()) , isList^#() -> c_3(isNeList^#()) , isNeList^#() -> c_4(U41^#(isList()), isList^#()) , isNeList^#() -> c_5(U51^#(isNeList()), isNeList^#()) , U41^#(tt()) -> c_6(isNeList^#()) , U51^#(tt()) -> c_7(isList^#()) , U71^#(tt()) -> c_8(isPal^#()) , isPal^#() -> c_9(isNePal^#()) , isNePal^#() -> c_10(U71^#(isQid())) } Weak Trs: { 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() , isQid() -> tt() } Obligation: innermost 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) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) 'Fastest (timeout of 5 seconds)' failed due to the following reason: Computation stopped due to timeout after 5.0 seconds. 3) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 2) '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: innermost 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: innermost 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: innermost 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: innermost 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: innermost 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: innermost 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: innermost 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: innermost 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: innermost 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: innermost 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) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 2) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible Arrrr..