MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) , conj(Or(o1, o2)) -> False() , conj(T()) -> True() , conj(F()) -> True() , isAnd(And(t1, t2)) -> True() , isAnd(Or(t1, t2)) -> False() , isAnd(T()) -> False() , isAnd(F()) -> False() , isConsTerm(And(a1, a2), And(y1, y2)) -> True() , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() , isConsTerm(And(a1, a2), T()) -> False() , isConsTerm(And(a1, a2), F()) -> False() , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() , isConsTerm(Or(o1, o2), T()) -> False() , isConsTerm(Or(o1, o2), F()) -> False() , isConsTerm(T(), And(y1, y2)) -> False() , isConsTerm(T(), Or(x1, x2)) -> False() , isConsTerm(T(), T()) -> True() , isConsTerm(T(), F()) -> False() , isConsTerm(F(), And(y1, y2)) -> False() , isConsTerm(F(), Or(x1, x2)) -> False() , isConsTerm(F(), T()) -> False() , isConsTerm(F(), F()) -> True() , disj(And(a1, a2)) -> conj(And(a1, a2)) , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) , disj(T()) -> True() , disj(F()) -> True() , isOp(And(t1, t2)) -> True() , isOp(Or(t1, t2)) -> True() , isOp(T()) -> False() , isOp(F()) -> False() , getFirst(And(t1, t2)) -> t1 , getFirst(Or(t1, t2)) -> t1 , bool(And(a1, a2)) -> False() , bool(Or(o1, o2)) -> False() , bool(T()) -> True() , bool(F()) -> True() , getSecond(And(t1, t2)) -> t1 , getSecond(Or(t1, t2)) -> t1 , disjconj(p) -> disj(p) } Weak Trs: { and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() } 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: { conj^#(And(t1, t2)) -> c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) , conj^#(Or(o1, o2)) -> c_2() , conj^#(T()) -> c_3() , conj^#(F()) -> c_4() , disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) , disj^#(Or(t1, t2)) -> c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) , disj^#(T()) -> c_27() , disj^#(F()) -> c_28() , isAnd^#(And(t1, t2)) -> c_5() , isAnd^#(Or(t1, t2)) -> c_6() , isAnd^#(T()) -> c_7() , isAnd^#(F()) -> c_8() , isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() , isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() , isConsTerm^#(And(a1, a2), T()) -> c_11() , isConsTerm^#(And(a1, a2), F()) -> c_12() , isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() , isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() , isConsTerm^#(Or(o1, o2), T()) -> c_15() , isConsTerm^#(Or(o1, o2), F()) -> c_16() , isConsTerm^#(T(), And(y1, y2)) -> c_17() , isConsTerm^#(T(), Or(x1, x2)) -> c_18() , isConsTerm^#(T(), T()) -> c_19() , isConsTerm^#(T(), F()) -> c_20() , isConsTerm^#(F(), And(y1, y2)) -> c_21() , isConsTerm^#(F(), Or(x1, x2)) -> c_22() , isConsTerm^#(F(), T()) -> c_23() , isConsTerm^#(F(), F()) -> c_24() , isOp^#(And(t1, t2)) -> c_29() , isOp^#(Or(t1, t2)) -> c_30() , isOp^#(T()) -> c_31() , isOp^#(F()) -> c_32() , getFirst^#(And(t1, t2)) -> c_33() , getFirst^#(Or(t1, t2)) -> c_34() , bool^#(And(a1, a2)) -> c_35() , bool^#(Or(o1, o2)) -> c_36() , bool^#(T()) -> c_37() , bool^#(F()) -> c_38() , getSecond^#(And(t1, t2)) -> c_39() , getSecond^#(Or(t1, t2)) -> c_40() , disjconj^#(p) -> c_41(disj^#(p)) } Weak DPs: { and^#(True(), True()) -> c_42() , and^#(True(), False()) -> c_43() , and^#(False(), True()) -> c_44() , and^#(False(), False()) -> c_45() } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { conj^#(And(t1, t2)) -> c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) , conj^#(Or(o1, o2)) -> c_2() , conj^#(T()) -> c_3() , conj^#(F()) -> c_4() , disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) , disj^#(Or(t1, t2)) -> c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) , disj^#(T()) -> c_27() , disj^#(F()) -> c_28() , isAnd^#(And(t1, t2)) -> c_5() , isAnd^#(Or(t1, t2)) -> c_6() , isAnd^#(T()) -> c_7() , isAnd^#(F()) -> c_8() , isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() , isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() , isConsTerm^#(And(a1, a2), T()) -> c_11() , isConsTerm^#(And(a1, a2), F()) -> c_12() , isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() , isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() , isConsTerm^#(Or(o1, o2), T()) -> c_15() , isConsTerm^#(Or(o1, o2), F()) -> c_16() , isConsTerm^#(T(), And(y1, y2)) -> c_17() , isConsTerm^#(T(), Or(x1, x2)) -> c_18() , isConsTerm^#(T(), T()) -> c_19() , isConsTerm^#(T(), F()) -> c_20() , isConsTerm^#(F(), And(y1, y2)) -> c_21() , isConsTerm^#(F(), Or(x1, x2)) -> c_22() , isConsTerm^#(F(), T()) -> c_23() , isConsTerm^#(F(), F()) -> c_24() , isOp^#(And(t1, t2)) -> c_29() , isOp^#(Or(t1, t2)) -> c_30() , isOp^#(T()) -> c_31() , isOp^#(F()) -> c_32() , getFirst^#(And(t1, t2)) -> c_33() , getFirst^#(Or(t1, t2)) -> c_34() , bool^#(And(a1, a2)) -> c_35() , bool^#(Or(o1, o2)) -> c_36() , bool^#(T()) -> c_37() , bool^#(F()) -> c_38() , getSecond^#(And(t1, t2)) -> c_39() , getSecond^#(Or(t1, t2)) -> c_40() , disjconj^#(p) -> c_41(disj^#(p)) } Weak DPs: { and^#(True(), True()) -> c_42() , and^#(True(), False()) -> c_43() , and^#(False(), True()) -> c_44() , and^#(False(), False()) -> c_45() } Weak Trs: { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) , conj(Or(o1, o2)) -> False() , conj(T()) -> True() , conj(F()) -> True() , isAnd(And(t1, t2)) -> True() , isAnd(Or(t1, t2)) -> False() , isAnd(T()) -> False() , isAnd(F()) -> False() , isConsTerm(And(a1, a2), And(y1, y2)) -> True() , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() , isConsTerm(And(a1, a2), T()) -> False() , isConsTerm(And(a1, a2), F()) -> False() , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() , isConsTerm(Or(o1, o2), T()) -> False() , isConsTerm(Or(o1, o2), F()) -> False() , isConsTerm(T(), And(y1, y2)) -> False() , isConsTerm(T(), Or(x1, x2)) -> False() , isConsTerm(T(), T()) -> True() , isConsTerm(T(), F()) -> False() , isConsTerm(F(), And(y1, y2)) -> False() , isConsTerm(F(), Or(x1, x2)) -> False() , isConsTerm(F(), T()) -> False() , isConsTerm(F(), F()) -> True() , disj(And(a1, a2)) -> conj(And(a1, a2)) , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) , disj(T()) -> True() , disj(F()) -> True() , isOp(And(t1, t2)) -> True() , isOp(Or(t1, t2)) -> True() , isOp(T()) -> False() , isOp(F()) -> False() , getFirst(And(t1, t2)) -> t1 , getFirst(Or(t1, t2)) -> t1 , bool(And(a1, a2)) -> False() , bool(Or(o1, o2)) -> False() , bool(T()) -> True() , bool(F()) -> True() , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , getSecond(And(t1, t2)) -> t1 , getSecond(Or(t1, t2)) -> t1 , disjconj(p) -> disj(p) } Obligation: innermost runtime complexity Answer: MAYBE We estimate the number of application of {2,3,4,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40} by applications of Pre({2,3,4,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26,27,28,29,30,31,32,33,34,35,36,37,38,39,40}) = {1,6,41}. Here rules are labeled as follows: DPs: { 1: conj^#(And(t1, t2)) -> c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) , 2: conj^#(Or(o1, o2)) -> c_2() , 3: conj^#(T()) -> c_3() , 4: conj^#(F()) -> c_4() , 5: disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) , 6: disj^#(Or(t1, t2)) -> c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) , 7: disj^#(T()) -> c_27() , 8: disj^#(F()) -> c_28() , 9: isAnd^#(And(t1, t2)) -> c_5() , 10: isAnd^#(Or(t1, t2)) -> c_6() , 11: isAnd^#(T()) -> c_7() , 12: isAnd^#(F()) -> c_8() , 13: isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() , 14: isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() , 15: isConsTerm^#(And(a1, a2), T()) -> c_11() , 16: isConsTerm^#(And(a1, a2), F()) -> c_12() , 17: isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() , 18: isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() , 19: isConsTerm^#(Or(o1, o2), T()) -> c_15() , 20: isConsTerm^#(Or(o1, o2), F()) -> c_16() , 21: isConsTerm^#(T(), And(y1, y2)) -> c_17() , 22: isConsTerm^#(T(), Or(x1, x2)) -> c_18() , 23: isConsTerm^#(T(), T()) -> c_19() , 24: isConsTerm^#(T(), F()) -> c_20() , 25: isConsTerm^#(F(), And(y1, y2)) -> c_21() , 26: isConsTerm^#(F(), Or(x1, x2)) -> c_22() , 27: isConsTerm^#(F(), T()) -> c_23() , 28: isConsTerm^#(F(), F()) -> c_24() , 29: isOp^#(And(t1, t2)) -> c_29() , 30: isOp^#(Or(t1, t2)) -> c_30() , 31: isOp^#(T()) -> c_31() , 32: isOp^#(F()) -> c_32() , 33: getFirst^#(And(t1, t2)) -> c_33() , 34: getFirst^#(Or(t1, t2)) -> c_34() , 35: bool^#(And(a1, a2)) -> c_35() , 36: bool^#(Or(o1, o2)) -> c_36() , 37: bool^#(T()) -> c_37() , 38: bool^#(F()) -> c_38() , 39: getSecond^#(And(t1, t2)) -> c_39() , 40: getSecond^#(Or(t1, t2)) -> c_40() , 41: disjconj^#(p) -> c_41(disj^#(p)) , 42: and^#(True(), True()) -> c_42() , 43: and^#(True(), False()) -> c_43() , 44: and^#(False(), True()) -> c_44() , 45: and^#(False(), False()) -> c_45() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { conj^#(And(t1, t2)) -> c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) , disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) , disj^#(Or(t1, t2)) -> c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) , disjconj^#(p) -> c_41(disj^#(p)) } Weak DPs: { conj^#(Or(o1, o2)) -> c_2() , conj^#(T()) -> c_3() , conj^#(F()) -> c_4() , and^#(True(), True()) -> c_42() , and^#(True(), False()) -> c_43() , and^#(False(), True()) -> c_44() , and^#(False(), False()) -> c_45() , disj^#(T()) -> c_27() , disj^#(F()) -> c_28() , isAnd^#(And(t1, t2)) -> c_5() , isAnd^#(Or(t1, t2)) -> c_6() , isAnd^#(T()) -> c_7() , isAnd^#(F()) -> c_8() , isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() , isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() , isConsTerm^#(And(a1, a2), T()) -> c_11() , isConsTerm^#(And(a1, a2), F()) -> c_12() , isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() , isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() , isConsTerm^#(Or(o1, o2), T()) -> c_15() , isConsTerm^#(Or(o1, o2), F()) -> c_16() , isConsTerm^#(T(), And(y1, y2)) -> c_17() , isConsTerm^#(T(), Or(x1, x2)) -> c_18() , isConsTerm^#(T(), T()) -> c_19() , isConsTerm^#(T(), F()) -> c_20() , isConsTerm^#(F(), And(y1, y2)) -> c_21() , isConsTerm^#(F(), Or(x1, x2)) -> c_22() , isConsTerm^#(F(), T()) -> c_23() , isConsTerm^#(F(), F()) -> c_24() , isOp^#(And(t1, t2)) -> c_29() , isOp^#(Or(t1, t2)) -> c_30() , isOp^#(T()) -> c_31() , isOp^#(F()) -> c_32() , getFirst^#(And(t1, t2)) -> c_33() , getFirst^#(Or(t1, t2)) -> c_34() , bool^#(And(a1, a2)) -> c_35() , bool^#(Or(o1, o2)) -> c_36() , bool^#(T()) -> c_37() , bool^#(F()) -> c_38() , getSecond^#(And(t1, t2)) -> c_39() , getSecond^#(Or(t1, t2)) -> c_40() } Weak Trs: { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) , conj(Or(o1, o2)) -> False() , conj(T()) -> True() , conj(F()) -> True() , isAnd(And(t1, t2)) -> True() , isAnd(Or(t1, t2)) -> False() , isAnd(T()) -> False() , isAnd(F()) -> False() , isConsTerm(And(a1, a2), And(y1, y2)) -> True() , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() , isConsTerm(And(a1, a2), T()) -> False() , isConsTerm(And(a1, a2), F()) -> False() , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() , isConsTerm(Or(o1, o2), T()) -> False() , isConsTerm(Or(o1, o2), F()) -> False() , isConsTerm(T(), And(y1, y2)) -> False() , isConsTerm(T(), Or(x1, x2)) -> False() , isConsTerm(T(), T()) -> True() , isConsTerm(T(), F()) -> False() , isConsTerm(F(), And(y1, y2)) -> False() , isConsTerm(F(), Or(x1, x2)) -> False() , isConsTerm(F(), T()) -> False() , isConsTerm(F(), F()) -> True() , disj(And(a1, a2)) -> conj(And(a1, a2)) , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) , disj(T()) -> True() , disj(F()) -> True() , isOp(And(t1, t2)) -> True() , isOp(Or(t1, t2)) -> True() , isOp(T()) -> False() , isOp(F()) -> False() , getFirst(And(t1, t2)) -> t1 , getFirst(Or(t1, t2)) -> t1 , bool(And(a1, a2)) -> False() , bool(Or(o1, o2)) -> False() , bool(T()) -> True() , bool(F()) -> True() , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , getSecond(And(t1, t2)) -> t1 , getSecond(Or(t1, t2)) -> t1 , disjconj(p) -> disj(p) } 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. { conj^#(Or(o1, o2)) -> c_2() , conj^#(T()) -> c_3() , conj^#(F()) -> c_4() , and^#(True(), True()) -> c_42() , and^#(True(), False()) -> c_43() , and^#(False(), True()) -> c_44() , and^#(False(), False()) -> c_45() , disj^#(T()) -> c_27() , disj^#(F()) -> c_28() , isAnd^#(And(t1, t2)) -> c_5() , isAnd^#(Or(t1, t2)) -> c_6() , isAnd^#(T()) -> c_7() , isAnd^#(F()) -> c_8() , isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() , isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() , isConsTerm^#(And(a1, a2), T()) -> c_11() , isConsTerm^#(And(a1, a2), F()) -> c_12() , isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() , isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() , isConsTerm^#(Or(o1, o2), T()) -> c_15() , isConsTerm^#(Or(o1, o2), F()) -> c_16() , isConsTerm^#(T(), And(y1, y2)) -> c_17() , isConsTerm^#(T(), Or(x1, x2)) -> c_18() , isConsTerm^#(T(), T()) -> c_19() , isConsTerm^#(T(), F()) -> c_20() , isConsTerm^#(F(), And(y1, y2)) -> c_21() , isConsTerm^#(F(), Or(x1, x2)) -> c_22() , isConsTerm^#(F(), T()) -> c_23() , isConsTerm^#(F(), F()) -> c_24() , isOp^#(And(t1, t2)) -> c_29() , isOp^#(Or(t1, t2)) -> c_30() , isOp^#(T()) -> c_31() , isOp^#(F()) -> c_32() , getFirst^#(And(t1, t2)) -> c_33() , getFirst^#(Or(t1, t2)) -> c_34() , bool^#(And(a1, a2)) -> c_35() , bool^#(Or(o1, o2)) -> c_36() , bool^#(T()) -> c_37() , bool^#(F()) -> c_38() , getSecond^#(And(t1, t2)) -> c_39() , getSecond^#(Or(t1, t2)) -> c_40() } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { conj^#(And(t1, t2)) -> c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) , disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) , disj^#(Or(t1, t2)) -> c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) , disjconj^#(p) -> c_41(disj^#(p)) } Weak Trs: { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) , conj(Or(o1, o2)) -> False() , conj(T()) -> True() , conj(F()) -> True() , isAnd(And(t1, t2)) -> True() , isAnd(Or(t1, t2)) -> False() , isAnd(T()) -> False() , isAnd(F()) -> False() , isConsTerm(And(a1, a2), And(y1, y2)) -> True() , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() , isConsTerm(And(a1, a2), T()) -> False() , isConsTerm(And(a1, a2), F()) -> False() , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() , isConsTerm(Or(o1, o2), T()) -> False() , isConsTerm(Or(o1, o2), F()) -> False() , isConsTerm(T(), And(y1, y2)) -> False() , isConsTerm(T(), Or(x1, x2)) -> False() , isConsTerm(T(), T()) -> True() , isConsTerm(T(), F()) -> False() , isConsTerm(F(), And(y1, y2)) -> False() , isConsTerm(F(), Or(x1, x2)) -> False() , isConsTerm(F(), T()) -> False() , isConsTerm(F(), F()) -> True() , disj(And(a1, a2)) -> conj(And(a1, a2)) , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) , disj(T()) -> True() , disj(F()) -> True() , isOp(And(t1, t2)) -> True() , isOp(Or(t1, t2)) -> True() , isOp(T()) -> False() , isOp(F()) -> False() , getFirst(And(t1, t2)) -> t1 , getFirst(Or(t1, t2)) -> t1 , bool(And(a1, a2)) -> False() , bool(Or(o1, o2)) -> False() , bool(T()) -> True() , bool(F()) -> True() , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , getSecond(And(t1, t2)) -> t1 , getSecond(Or(t1, t2)) -> t1 , disjconj(p) -> disj(p) } Obligation: innermost runtime complexity Answer: MAYBE Due to missing edges in the dependency-graph, the right-hand sides of following rules could be simplified: { conj^#(And(t1, t2)) -> c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) , disj^#(Or(t1, t2)) -> c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) , disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) , disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) , disjconj^#(p) -> c_4(disj^#(p)) } Weak Trs: { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) , conj(Or(o1, o2)) -> False() , conj(T()) -> True() , conj(F()) -> True() , isAnd(And(t1, t2)) -> True() , isAnd(Or(t1, t2)) -> False() , isAnd(T()) -> False() , isAnd(F()) -> False() , isConsTerm(And(a1, a2), And(y1, y2)) -> True() , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() , isConsTerm(And(a1, a2), T()) -> False() , isConsTerm(And(a1, a2), F()) -> False() , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() , isConsTerm(Or(o1, o2), T()) -> False() , isConsTerm(Or(o1, o2), F()) -> False() , isConsTerm(T(), And(y1, y2)) -> False() , isConsTerm(T(), Or(x1, x2)) -> False() , isConsTerm(T(), T()) -> True() , isConsTerm(T(), F()) -> False() , isConsTerm(F(), And(y1, y2)) -> False() , isConsTerm(F(), Or(x1, x2)) -> False() , isConsTerm(F(), T()) -> False() , isConsTerm(F(), F()) -> True() , disj(And(a1, a2)) -> conj(And(a1, a2)) , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) , disj(T()) -> True() , disj(F()) -> True() , isOp(And(t1, t2)) -> True() , isOp(Or(t1, t2)) -> True() , isOp(T()) -> False() , isOp(F()) -> False() , getFirst(And(t1, t2)) -> t1 , getFirst(Or(t1, t2)) -> t1 , bool(And(a1, a2)) -> False() , bool(Or(o1, o2)) -> False() , bool(T()) -> True() , bool(F()) -> True() , and(True(), True()) -> True() , and(True(), False()) -> False() , and(False(), True()) -> False() , and(False(), False()) -> False() , getSecond(And(t1, t2)) -> t1 , getSecond(Or(t1, t2)) -> t1 , disjconj(p) -> disj(p) } Obligation: innermost runtime complexity Answer: MAYBE No rule is usable, rules are removed from the input problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) , disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) , disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) , disjconj^#(p) -> c_4(disj^#(p)) } Obligation: innermost runtime complexity Answer: MAYBE Consider the dependency graph 1: conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) -->_1 disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) :3 -->_1 disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) :2 -->_2 conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) :1 2: disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) -->_1 conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) :1 3: disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) -->_2 disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) :3 -->_2 disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) :2 -->_1 conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) :1 4: disjconj^#(p) -> c_4(disj^#(p)) -->_1 disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) :3 -->_1 disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) :2 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). { disjconj^#(p) -> c_4(disj^#(p)) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) , disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) , disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) } 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) 'Polynomial Path Order (PS)' failed due to the following reason: The input cannot be shown compatible 3) 'Fastest (timeout of 5 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 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: Computation stopped due to timeout after 30.0 seconds. 2) '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 input cannot be shown compatible 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The input cannot be shown compatible 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. Arrrr..