MAYBE 109.07/40.01 MAYBE 109.07/40.01 109.07/40.01 We are left with following problem, upon which TcT provides the 109.07/40.01 certificate MAYBE. 109.07/40.01 109.07/40.01 Strict Trs: 109.07/40.01 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.01 , conj(Or(o1, o2)) -> False() 109.07/40.01 , conj(T()) -> True() 109.07/40.01 , conj(F()) -> True() 109.07/40.01 , isAnd(And(t1, t2)) -> True() 109.07/40.01 , isAnd(Or(t1, t2)) -> False() 109.07/40.01 , isAnd(T()) -> False() 109.07/40.01 , isAnd(F()) -> False() 109.07/40.01 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.01 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.01 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.01 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.01 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.01 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.01 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.01 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.01 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.01 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.01 , isConsTerm(T(), T()) -> True() 109.07/40.01 , isConsTerm(T(), F()) -> False() 109.07/40.01 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.01 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.01 , isConsTerm(F(), T()) -> False() 109.07/40.01 , isConsTerm(F(), F()) -> True() 109.07/40.01 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.01 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.01 , disj(T()) -> True() 109.07/40.01 , disj(F()) -> True() 109.07/40.01 , isOp(And(t1, t2)) -> True() 109.07/40.01 , isOp(Or(t1, t2)) -> True() 109.07/40.01 , isOp(T()) -> False() 109.07/40.01 , isOp(F()) -> False() 109.07/40.01 , getFirst(And(t1, t2)) -> t1 109.07/40.01 , getFirst(Or(t1, t2)) -> t1 109.07/40.01 , bool(And(a1, a2)) -> False() 109.07/40.01 , bool(Or(o1, o2)) -> False() 109.07/40.01 , bool(T()) -> True() 109.07/40.01 , bool(F()) -> True() 109.07/40.01 , getSecond(And(t1, t2)) -> t1 109.07/40.01 , getSecond(Or(t1, t2)) -> t1 109.07/40.01 , disjconj(p) -> disj(p) } 109.07/40.01 Weak Trs: 109.07/40.01 { and(True(), True()) -> True() 109.07/40.01 , and(True(), False()) -> False() 109.07/40.01 , and(False(), True()) -> False() 109.07/40.01 , and(False(), False()) -> False() } 109.07/40.01 Obligation: 109.07/40.01 innermost runtime complexity 109.07/40.01 Answer: 109.07/40.01 MAYBE 109.07/40.01 109.07/40.01 None of the processors succeeded. 109.07/40.01 109.07/40.01 Details of failed attempt(s): 109.07/40.01 ----------------------------- 109.07/40.01 1) 'empty' failed due to the following reason: 109.07/40.01 109.07/40.01 Empty strict component of the problem is NOT empty. 109.07/40.01 109.07/40.01 2) 'Best' failed due to the following reason: 109.07/40.01 109.07/40.01 None of the processors succeeded. 109.07/40.01 109.07/40.01 Details of failed attempt(s): 109.07/40.01 ----------------------------- 109.07/40.01 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 109.07/40.01 following reason: 109.07/40.01 109.07/40.01 We add the following dependency tuples: 109.07/40.01 109.07/40.01 Strict DPs: 109.07/40.01 { conj^#(And(t1, t2)) -> 109.07/40.01 c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) 109.07/40.01 , conj^#(Or(o1, o2)) -> c_2() 109.07/40.01 , conj^#(T()) -> c_3() 109.07/40.01 , conj^#(F()) -> c_4() 109.07/40.01 , disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) 109.07/40.01 , disj^#(Or(t1, t2)) -> 109.07/40.01 c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) 109.07/40.01 , disj^#(T()) -> c_27() 109.07/40.01 , disj^#(F()) -> c_28() 109.07/40.01 , isAnd^#(And(t1, t2)) -> c_5() 109.07/40.01 , isAnd^#(Or(t1, t2)) -> c_6() 109.07/40.01 , isAnd^#(T()) -> c_7() 109.07/40.01 , isAnd^#(F()) -> c_8() 109.07/40.01 , isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() 109.07/40.01 , isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() 109.07/40.01 , isConsTerm^#(And(a1, a2), T()) -> c_11() 109.07/40.01 , isConsTerm^#(And(a1, a2), F()) -> c_12() 109.07/40.01 , isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() 109.07/40.01 , isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() 109.07/40.01 , isConsTerm^#(Or(o1, o2), T()) -> c_15() 109.07/40.01 , isConsTerm^#(Or(o1, o2), F()) -> c_16() 109.07/40.01 , isConsTerm^#(T(), And(y1, y2)) -> c_17() 109.07/40.01 , isConsTerm^#(T(), Or(x1, x2)) -> c_18() 109.07/40.01 , isConsTerm^#(T(), T()) -> c_19() 109.07/40.01 , isConsTerm^#(T(), F()) -> c_20() 109.07/40.01 , isConsTerm^#(F(), And(y1, y2)) -> c_21() 109.07/40.01 , isConsTerm^#(F(), Or(x1, x2)) -> c_22() 109.07/40.01 , isConsTerm^#(F(), T()) -> c_23() 109.07/40.01 , isConsTerm^#(F(), F()) -> c_24() 109.07/40.01 , isOp^#(And(t1, t2)) -> c_29() 109.07/40.01 , isOp^#(Or(t1, t2)) -> c_30() 109.07/40.01 , isOp^#(T()) -> c_31() 109.07/40.01 , isOp^#(F()) -> c_32() 109.07/40.01 , getFirst^#(And(t1, t2)) -> c_33() 109.07/40.01 , getFirst^#(Or(t1, t2)) -> c_34() 109.07/40.01 , bool^#(And(a1, a2)) -> c_35() 109.07/40.01 , bool^#(Or(o1, o2)) -> c_36() 109.07/40.01 , bool^#(T()) -> c_37() 109.07/40.01 , bool^#(F()) -> c_38() 109.07/40.01 , getSecond^#(And(t1, t2)) -> c_39() 109.07/40.01 , getSecond^#(Or(t1, t2)) -> c_40() 109.07/40.01 , disjconj^#(p) -> c_41(disj^#(p)) } 109.07/40.01 Weak DPs: 109.07/40.01 { and^#(True(), True()) -> c_42() 109.07/40.01 , and^#(True(), False()) -> c_43() 109.07/40.01 , and^#(False(), True()) -> c_44() 109.07/40.01 , and^#(False(), False()) -> c_45() } 109.07/40.01 109.07/40.01 and mark the set of starting terms. 109.07/40.01 109.07/40.01 We are left with following problem, upon which TcT provides the 109.07/40.01 certificate MAYBE. 109.07/40.01 109.07/40.01 Strict DPs: 109.07/40.01 { conj^#(And(t1, t2)) -> 109.07/40.01 c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) 109.07/40.01 , conj^#(Or(o1, o2)) -> c_2() 109.07/40.01 , conj^#(T()) -> c_3() 109.07/40.01 , conj^#(F()) -> c_4() 109.07/40.01 , disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) 109.07/40.01 , disj^#(Or(t1, t2)) -> 109.07/40.01 c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) 109.07/40.01 , disj^#(T()) -> c_27() 109.07/40.01 , disj^#(F()) -> c_28() 109.07/40.01 , isAnd^#(And(t1, t2)) -> c_5() 109.07/40.01 , isAnd^#(Or(t1, t2)) -> c_6() 109.07/40.01 , isAnd^#(T()) -> c_7() 109.07/40.01 , isAnd^#(F()) -> c_8() 109.07/40.01 , isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() 109.07/40.01 , isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() 109.07/40.01 , isConsTerm^#(And(a1, a2), T()) -> c_11() 109.07/40.01 , isConsTerm^#(And(a1, a2), F()) -> c_12() 109.07/40.01 , isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() 109.07/40.01 , isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() 109.07/40.01 , isConsTerm^#(Or(o1, o2), T()) -> c_15() 109.07/40.01 , isConsTerm^#(Or(o1, o2), F()) -> c_16() 109.07/40.01 , isConsTerm^#(T(), And(y1, y2)) -> c_17() 109.07/40.01 , isConsTerm^#(T(), Or(x1, x2)) -> c_18() 109.07/40.01 , isConsTerm^#(T(), T()) -> c_19() 109.07/40.01 , isConsTerm^#(T(), F()) -> c_20() 109.07/40.01 , isConsTerm^#(F(), And(y1, y2)) -> c_21() 109.07/40.01 , isConsTerm^#(F(), Or(x1, x2)) -> c_22() 109.07/40.01 , isConsTerm^#(F(), T()) -> c_23() 109.07/40.01 , isConsTerm^#(F(), F()) -> c_24() 109.07/40.01 , isOp^#(And(t1, t2)) -> c_29() 109.07/40.01 , isOp^#(Or(t1, t2)) -> c_30() 109.07/40.01 , isOp^#(T()) -> c_31() 109.07/40.01 , isOp^#(F()) -> c_32() 109.07/40.01 , getFirst^#(And(t1, t2)) -> c_33() 109.07/40.01 , getFirst^#(Or(t1, t2)) -> c_34() 109.07/40.01 , bool^#(And(a1, a2)) -> c_35() 109.07/40.01 , bool^#(Or(o1, o2)) -> c_36() 109.07/40.01 , bool^#(T()) -> c_37() 109.07/40.01 , bool^#(F()) -> c_38() 109.07/40.01 , getSecond^#(And(t1, t2)) -> c_39() 109.07/40.01 , getSecond^#(Or(t1, t2)) -> c_40() 109.07/40.01 , disjconj^#(p) -> c_41(disj^#(p)) } 109.07/40.01 Weak DPs: 109.07/40.01 { and^#(True(), True()) -> c_42() 109.07/40.01 , and^#(True(), False()) -> c_43() 109.07/40.01 , and^#(False(), True()) -> c_44() 109.07/40.01 , and^#(False(), False()) -> c_45() } 109.07/40.01 Weak Trs: 109.07/40.01 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.01 , conj(Or(o1, o2)) -> False() 109.07/40.01 , conj(T()) -> True() 109.07/40.01 , conj(F()) -> True() 109.07/40.01 , isAnd(And(t1, t2)) -> True() 109.07/40.01 , isAnd(Or(t1, t2)) -> False() 109.07/40.01 , isAnd(T()) -> False() 109.07/40.01 , isAnd(F()) -> False() 109.07/40.01 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.01 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.01 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.01 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.01 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.01 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.01 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.01 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.01 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.01 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.01 , isConsTerm(T(), T()) -> True() 109.07/40.01 , isConsTerm(T(), F()) -> False() 109.07/40.01 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.01 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.01 , isConsTerm(F(), T()) -> False() 109.07/40.01 , isConsTerm(F(), F()) -> True() 109.07/40.01 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.01 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.01 , disj(T()) -> True() 109.07/40.01 , disj(F()) -> True() 109.07/40.01 , isOp(And(t1, t2)) -> True() 109.07/40.01 , isOp(Or(t1, t2)) -> True() 109.07/40.01 , isOp(T()) -> False() 109.07/40.01 , isOp(F()) -> False() 109.07/40.01 , getFirst(And(t1, t2)) -> t1 109.07/40.01 , getFirst(Or(t1, t2)) -> t1 109.07/40.01 , bool(And(a1, a2)) -> False() 109.07/40.02 , bool(Or(o1, o2)) -> False() 109.07/40.02 , bool(T()) -> True() 109.07/40.02 , bool(F()) -> True() 109.07/40.02 , and(True(), True()) -> True() 109.07/40.02 , and(True(), False()) -> False() 109.07/40.02 , and(False(), True()) -> False() 109.07/40.02 , and(False(), False()) -> False() 109.07/40.02 , getSecond(And(t1, t2)) -> t1 109.07/40.02 , getSecond(Or(t1, t2)) -> t1 109.07/40.02 , disjconj(p) -> disj(p) } 109.07/40.02 Obligation: 109.07/40.02 innermost runtime complexity 109.07/40.02 Answer: 109.07/40.02 MAYBE 109.07/40.02 109.07/40.02 We estimate the number of application of 109.07/40.02 {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} 109.07/40.02 by applications of 109.07/40.02 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}) 109.07/40.02 = {1,6,41}. Here rules are labeled as follows: 109.07/40.02 109.07/40.02 DPs: 109.07/40.02 { 1: conj^#(And(t1, t2)) -> 109.07/40.02 c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) 109.07/40.02 , 2: conj^#(Or(o1, o2)) -> c_2() 109.07/40.02 , 3: conj^#(T()) -> c_3() 109.07/40.02 , 4: conj^#(F()) -> c_4() 109.07/40.02 , 5: disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) 109.07/40.02 , 6: disj^#(Or(t1, t2)) -> 109.07/40.02 c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) 109.07/40.02 , 7: disj^#(T()) -> c_27() 109.07/40.02 , 8: disj^#(F()) -> c_28() 109.07/40.02 , 9: isAnd^#(And(t1, t2)) -> c_5() 109.07/40.02 , 10: isAnd^#(Or(t1, t2)) -> c_6() 109.07/40.02 , 11: isAnd^#(T()) -> c_7() 109.07/40.02 , 12: isAnd^#(F()) -> c_8() 109.07/40.02 , 13: isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() 109.07/40.02 , 14: isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() 109.07/40.02 , 15: isConsTerm^#(And(a1, a2), T()) -> c_11() 109.07/40.02 , 16: isConsTerm^#(And(a1, a2), F()) -> c_12() 109.07/40.02 , 17: isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() 109.07/40.02 , 18: isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() 109.07/40.02 , 19: isConsTerm^#(Or(o1, o2), T()) -> c_15() 109.07/40.02 , 20: isConsTerm^#(Or(o1, o2), F()) -> c_16() 109.07/40.02 , 21: isConsTerm^#(T(), And(y1, y2)) -> c_17() 109.07/40.02 , 22: isConsTerm^#(T(), Or(x1, x2)) -> c_18() 109.07/40.02 , 23: isConsTerm^#(T(), T()) -> c_19() 109.07/40.02 , 24: isConsTerm^#(T(), F()) -> c_20() 109.07/40.02 , 25: isConsTerm^#(F(), And(y1, y2)) -> c_21() 109.07/40.02 , 26: isConsTerm^#(F(), Or(x1, x2)) -> c_22() 109.07/40.02 , 27: isConsTerm^#(F(), T()) -> c_23() 109.07/40.02 , 28: isConsTerm^#(F(), F()) -> c_24() 109.07/40.02 , 29: isOp^#(And(t1, t2)) -> c_29() 109.07/40.02 , 30: isOp^#(Or(t1, t2)) -> c_30() 109.07/40.02 , 31: isOp^#(T()) -> c_31() 109.07/40.02 , 32: isOp^#(F()) -> c_32() 109.07/40.02 , 33: getFirst^#(And(t1, t2)) -> c_33() 109.07/40.02 , 34: getFirst^#(Or(t1, t2)) -> c_34() 109.07/40.02 , 35: bool^#(And(a1, a2)) -> c_35() 109.07/40.02 , 36: bool^#(Or(o1, o2)) -> c_36() 109.07/40.02 , 37: bool^#(T()) -> c_37() 109.07/40.02 , 38: bool^#(F()) -> c_38() 109.07/40.02 , 39: getSecond^#(And(t1, t2)) -> c_39() 109.07/40.02 , 40: getSecond^#(Or(t1, t2)) -> c_40() 109.07/40.02 , 41: disjconj^#(p) -> c_41(disj^#(p)) 109.07/40.02 , 42: and^#(True(), True()) -> c_42() 109.07/40.02 , 43: and^#(True(), False()) -> c_43() 109.07/40.02 , 44: and^#(False(), True()) -> c_44() 109.07/40.02 , 45: and^#(False(), False()) -> c_45() } 109.07/40.02 109.07/40.02 We are left with following problem, upon which TcT provides the 109.07/40.02 certificate MAYBE. 109.07/40.02 109.07/40.02 Strict DPs: 109.07/40.02 { conj^#(And(t1, t2)) -> 109.07/40.02 c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) 109.07/40.02 , disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) 109.07/40.02 , disj^#(Or(t1, t2)) -> 109.07/40.02 c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) 109.07/40.02 , disjconj^#(p) -> c_41(disj^#(p)) } 109.07/40.02 Weak DPs: 109.07/40.02 { conj^#(Or(o1, o2)) -> c_2() 109.07/40.02 , conj^#(T()) -> c_3() 109.07/40.02 , conj^#(F()) -> c_4() 109.07/40.02 , and^#(True(), True()) -> c_42() 109.07/40.02 , and^#(True(), False()) -> c_43() 109.07/40.02 , and^#(False(), True()) -> c_44() 109.07/40.02 , and^#(False(), False()) -> c_45() 109.07/40.02 , disj^#(T()) -> c_27() 109.07/40.02 , disj^#(F()) -> c_28() 109.07/40.02 , isAnd^#(And(t1, t2)) -> c_5() 109.07/40.02 , isAnd^#(Or(t1, t2)) -> c_6() 109.07/40.02 , isAnd^#(T()) -> c_7() 109.07/40.02 , isAnd^#(F()) -> c_8() 109.07/40.02 , isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() 109.07/40.02 , isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() 109.07/40.02 , isConsTerm^#(And(a1, a2), T()) -> c_11() 109.07/40.02 , isConsTerm^#(And(a1, a2), F()) -> c_12() 109.07/40.02 , isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() 109.07/40.02 , isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() 109.07/40.02 , isConsTerm^#(Or(o1, o2), T()) -> c_15() 109.07/40.02 , isConsTerm^#(Or(o1, o2), F()) -> c_16() 109.07/40.02 , isConsTerm^#(T(), And(y1, y2)) -> c_17() 109.07/40.02 , isConsTerm^#(T(), Or(x1, x2)) -> c_18() 109.07/40.02 , isConsTerm^#(T(), T()) -> c_19() 109.07/40.02 , isConsTerm^#(T(), F()) -> c_20() 109.07/40.02 , isConsTerm^#(F(), And(y1, y2)) -> c_21() 109.07/40.02 , isConsTerm^#(F(), Or(x1, x2)) -> c_22() 109.07/40.02 , isConsTerm^#(F(), T()) -> c_23() 109.07/40.02 , isConsTerm^#(F(), F()) -> c_24() 109.07/40.02 , isOp^#(And(t1, t2)) -> c_29() 109.07/40.02 , isOp^#(Or(t1, t2)) -> c_30() 109.07/40.02 , isOp^#(T()) -> c_31() 109.07/40.02 , isOp^#(F()) -> c_32() 109.07/40.02 , getFirst^#(And(t1, t2)) -> c_33() 109.07/40.02 , getFirst^#(Or(t1, t2)) -> c_34() 109.07/40.02 , bool^#(And(a1, a2)) -> c_35() 109.07/40.02 , bool^#(Or(o1, o2)) -> c_36() 109.07/40.02 , bool^#(T()) -> c_37() 109.07/40.02 , bool^#(F()) -> c_38() 109.07/40.02 , getSecond^#(And(t1, t2)) -> c_39() 109.07/40.02 , getSecond^#(Or(t1, t2)) -> c_40() } 109.07/40.02 Weak Trs: 109.07/40.02 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.02 , conj(Or(o1, o2)) -> False() 109.07/40.02 , conj(T()) -> True() 109.07/40.02 , conj(F()) -> True() 109.07/40.02 , isAnd(And(t1, t2)) -> True() 109.07/40.02 , isAnd(Or(t1, t2)) -> False() 109.07/40.02 , isAnd(T()) -> False() 109.07/40.02 , isAnd(F()) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.02 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.02 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.02 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(T(), T()) -> True() 109.07/40.02 , isConsTerm(T(), F()) -> False() 109.07/40.02 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(F(), T()) -> False() 109.07/40.02 , isConsTerm(F(), F()) -> True() 109.07/40.02 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.02 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.02 , disj(T()) -> True() 109.07/40.02 , disj(F()) -> True() 109.07/40.02 , isOp(And(t1, t2)) -> True() 109.07/40.02 , isOp(Or(t1, t2)) -> True() 109.07/40.02 , isOp(T()) -> False() 109.07/40.02 , isOp(F()) -> False() 109.07/40.02 , getFirst(And(t1, t2)) -> t1 109.07/40.02 , getFirst(Or(t1, t2)) -> t1 109.07/40.02 , bool(And(a1, a2)) -> False() 109.07/40.02 , bool(Or(o1, o2)) -> False() 109.07/40.02 , bool(T()) -> True() 109.07/40.02 , bool(F()) -> True() 109.07/40.02 , and(True(), True()) -> True() 109.07/40.02 , and(True(), False()) -> False() 109.07/40.02 , and(False(), True()) -> False() 109.07/40.02 , and(False(), False()) -> False() 109.07/40.02 , getSecond(And(t1, t2)) -> t1 109.07/40.02 , getSecond(Or(t1, t2)) -> t1 109.07/40.02 , disjconj(p) -> disj(p) } 109.07/40.02 Obligation: 109.07/40.02 innermost runtime complexity 109.07/40.02 Answer: 109.07/40.02 MAYBE 109.07/40.02 109.07/40.02 The following weak DPs constitute a sub-graph of the DG that is 109.07/40.02 closed under successors. The DPs are removed. 109.07/40.02 109.07/40.02 { conj^#(Or(o1, o2)) -> c_2() 109.07/40.02 , conj^#(T()) -> c_3() 109.07/40.02 , conj^#(F()) -> c_4() 109.07/40.02 , and^#(True(), True()) -> c_42() 109.07/40.02 , and^#(True(), False()) -> c_43() 109.07/40.02 , and^#(False(), True()) -> c_44() 109.07/40.02 , and^#(False(), False()) -> c_45() 109.07/40.02 , disj^#(T()) -> c_27() 109.07/40.02 , disj^#(F()) -> c_28() 109.07/40.02 , isAnd^#(And(t1, t2)) -> c_5() 109.07/40.02 , isAnd^#(Or(t1, t2)) -> c_6() 109.07/40.02 , isAnd^#(T()) -> c_7() 109.07/40.02 , isAnd^#(F()) -> c_8() 109.07/40.02 , isConsTerm^#(And(a1, a2), And(y1, y2)) -> c_9() 109.07/40.02 , isConsTerm^#(And(a1, a2), Or(x1, x2)) -> c_10() 109.07/40.02 , isConsTerm^#(And(a1, a2), T()) -> c_11() 109.07/40.02 , isConsTerm^#(And(a1, a2), F()) -> c_12() 109.07/40.02 , isConsTerm^#(Or(o1, o2), And(y1, y2)) -> c_13() 109.07/40.02 , isConsTerm^#(Or(o1, o2), Or(x1, x2)) -> c_14() 109.07/40.02 , isConsTerm^#(Or(o1, o2), T()) -> c_15() 109.07/40.02 , isConsTerm^#(Or(o1, o2), F()) -> c_16() 109.07/40.02 , isConsTerm^#(T(), And(y1, y2)) -> c_17() 109.07/40.02 , isConsTerm^#(T(), Or(x1, x2)) -> c_18() 109.07/40.02 , isConsTerm^#(T(), T()) -> c_19() 109.07/40.02 , isConsTerm^#(T(), F()) -> c_20() 109.07/40.02 , isConsTerm^#(F(), And(y1, y2)) -> c_21() 109.07/40.02 , isConsTerm^#(F(), Or(x1, x2)) -> c_22() 109.07/40.02 , isConsTerm^#(F(), T()) -> c_23() 109.07/40.02 , isConsTerm^#(F(), F()) -> c_24() 109.07/40.02 , isOp^#(And(t1, t2)) -> c_29() 109.07/40.02 , isOp^#(Or(t1, t2)) -> c_30() 109.07/40.02 , isOp^#(T()) -> c_31() 109.07/40.02 , isOp^#(F()) -> c_32() 109.07/40.02 , getFirst^#(And(t1, t2)) -> c_33() 109.07/40.02 , getFirst^#(Or(t1, t2)) -> c_34() 109.07/40.02 , bool^#(And(a1, a2)) -> c_35() 109.07/40.02 , bool^#(Or(o1, o2)) -> c_36() 109.07/40.02 , bool^#(T()) -> c_37() 109.07/40.02 , bool^#(F()) -> c_38() 109.07/40.02 , getSecond^#(And(t1, t2)) -> c_39() 109.07/40.02 , getSecond^#(Or(t1, t2)) -> c_40() } 109.07/40.02 109.07/40.02 We are left with following problem, upon which TcT provides the 109.07/40.02 certificate MAYBE. 109.07/40.02 109.07/40.02 Strict DPs: 109.07/40.02 { conj^#(And(t1, t2)) -> 109.07/40.02 c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) 109.07/40.02 , disj^#(And(a1, a2)) -> c_25(conj^#(And(a1, a2))) 109.07/40.02 , disj^#(Or(t1, t2)) -> 109.07/40.02 c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) 109.07/40.02 , disjconj^#(p) -> c_41(disj^#(p)) } 109.07/40.02 Weak Trs: 109.07/40.02 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.02 , conj(Or(o1, o2)) -> False() 109.07/40.02 , conj(T()) -> True() 109.07/40.02 , conj(F()) -> True() 109.07/40.02 , isAnd(And(t1, t2)) -> True() 109.07/40.02 , isAnd(Or(t1, t2)) -> False() 109.07/40.02 , isAnd(T()) -> False() 109.07/40.02 , isAnd(F()) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.02 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.02 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.02 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(T(), T()) -> True() 109.07/40.02 , isConsTerm(T(), F()) -> False() 109.07/40.02 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(F(), T()) -> False() 109.07/40.02 , isConsTerm(F(), F()) -> True() 109.07/40.02 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.02 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.02 , disj(T()) -> True() 109.07/40.02 , disj(F()) -> True() 109.07/40.02 , isOp(And(t1, t2)) -> True() 109.07/40.02 , isOp(Or(t1, t2)) -> True() 109.07/40.02 , isOp(T()) -> False() 109.07/40.02 , isOp(F()) -> False() 109.07/40.02 , getFirst(And(t1, t2)) -> t1 109.07/40.02 , getFirst(Or(t1, t2)) -> t1 109.07/40.02 , bool(And(a1, a2)) -> False() 109.07/40.02 , bool(Or(o1, o2)) -> False() 109.07/40.02 , bool(T()) -> True() 109.07/40.02 , bool(F()) -> True() 109.07/40.02 , and(True(), True()) -> True() 109.07/40.02 , and(True(), False()) -> False() 109.07/40.02 , and(False(), True()) -> False() 109.07/40.02 , and(False(), False()) -> False() 109.07/40.02 , getSecond(And(t1, t2)) -> t1 109.07/40.02 , getSecond(Or(t1, t2)) -> t1 109.07/40.02 , disjconj(p) -> disj(p) } 109.07/40.02 Obligation: 109.07/40.02 innermost runtime complexity 109.07/40.02 Answer: 109.07/40.02 MAYBE 109.07/40.02 109.07/40.02 Due to missing edges in the dependency-graph, the right-hand sides 109.07/40.02 of following rules could be simplified: 109.07/40.02 109.07/40.02 { conj^#(And(t1, t2)) -> 109.07/40.02 c_1(and^#(disj(t1), conj(t1)), disj^#(t1), conj^#(t1)) 109.07/40.02 , disj^#(Or(t1, t2)) -> 109.07/40.02 c_26(and^#(conj(t1), disj(t1)), conj^#(t1), disj^#(t1)) } 109.07/40.02 109.07/40.02 We are left with following problem, upon which TcT provides the 109.07/40.02 certificate MAYBE. 109.07/40.02 109.07/40.02 Strict DPs: 109.07/40.02 { conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) 109.07/40.02 , disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) 109.07/40.02 , disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) 109.07/40.02 , disjconj^#(p) -> c_4(disj^#(p)) } 109.07/40.02 Weak Trs: 109.07/40.02 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.02 , conj(Or(o1, o2)) -> False() 109.07/40.02 , conj(T()) -> True() 109.07/40.02 , conj(F()) -> True() 109.07/40.02 , isAnd(And(t1, t2)) -> True() 109.07/40.02 , isAnd(Or(t1, t2)) -> False() 109.07/40.02 , isAnd(T()) -> False() 109.07/40.02 , isAnd(F()) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.02 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.02 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.02 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.02 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.02 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(T(), T()) -> True() 109.07/40.02 , isConsTerm(T(), F()) -> False() 109.07/40.02 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.02 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.02 , isConsTerm(F(), T()) -> False() 109.07/40.02 , isConsTerm(F(), F()) -> True() 109.07/40.02 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.02 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.02 , disj(T()) -> True() 109.07/40.02 , disj(F()) -> True() 109.07/40.02 , isOp(And(t1, t2)) -> True() 109.07/40.02 , isOp(Or(t1, t2)) -> True() 109.07/40.02 , isOp(T()) -> False() 109.07/40.02 , isOp(F()) -> False() 109.07/40.02 , getFirst(And(t1, t2)) -> t1 109.07/40.02 , getFirst(Or(t1, t2)) -> t1 109.07/40.02 , bool(And(a1, a2)) -> False() 109.07/40.02 , bool(Or(o1, o2)) -> False() 109.07/40.02 , bool(T()) -> True() 109.07/40.02 , bool(F()) -> True() 109.07/40.02 , and(True(), True()) -> True() 109.07/40.02 , and(True(), False()) -> False() 109.07/40.02 , and(False(), True()) -> False() 109.07/40.02 , and(False(), False()) -> False() 109.07/40.02 , getSecond(And(t1, t2)) -> t1 109.07/40.02 , getSecond(Or(t1, t2)) -> t1 109.07/40.02 , disjconj(p) -> disj(p) } 109.07/40.02 Obligation: 109.07/40.02 innermost runtime complexity 109.07/40.02 Answer: 109.07/40.02 MAYBE 109.07/40.02 109.07/40.02 No rule is usable, rules are removed from the input problem. 109.07/40.02 109.07/40.02 We are left with following problem, upon which TcT provides the 109.07/40.02 certificate MAYBE. 109.07/40.02 109.07/40.02 Strict DPs: 109.07/40.02 { conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) 109.07/40.02 , disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) 109.07/40.02 , disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) 109.07/40.02 , disjconj^#(p) -> c_4(disj^#(p)) } 109.07/40.02 Obligation: 109.07/40.02 innermost runtime complexity 109.07/40.02 Answer: 109.07/40.02 MAYBE 109.07/40.02 109.07/40.02 Consider the dependency graph 109.07/40.02 109.07/40.02 1: conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) 109.07/40.02 -->_1 disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) :3 109.07/40.02 -->_1 disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) :2 109.07/40.02 -->_2 conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) :1 109.07/40.02 109.07/40.02 2: disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) 109.07/40.02 -->_1 conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) :1 109.07/40.02 109.07/40.02 3: disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) 109.07/40.02 -->_2 disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) :3 109.07/40.02 -->_2 disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) :2 109.07/40.02 -->_1 conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) :1 109.07/40.02 109.07/40.02 4: disjconj^#(p) -> c_4(disj^#(p)) 109.07/40.02 -->_1 disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) :3 109.07/40.02 -->_1 disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) :2 109.07/40.02 109.07/40.02 109.07/40.02 Following roots of the dependency graph are removed, as the 109.07/40.02 considered set of starting terms is closed under reduction with 109.07/40.02 respect to these rules (modulo compound contexts). 109.07/40.02 109.07/40.02 { disjconj^#(p) -> c_4(disj^#(p)) } 109.07/40.02 109.07/40.02 109.07/40.02 We are left with following problem, upon which TcT provides the 109.07/40.02 certificate MAYBE. 109.07/40.02 109.07/40.02 Strict DPs: 109.07/40.02 { conj^#(And(t1, t2)) -> c_1(disj^#(t1), conj^#(t1)) 109.07/40.02 , disj^#(And(a1, a2)) -> c_2(conj^#(And(a1, a2))) 109.07/40.02 , disj^#(Or(t1, t2)) -> c_3(conj^#(t1), disj^#(t1)) } 109.07/40.02 Obligation: 109.07/40.02 innermost runtime complexity 109.07/40.02 Answer: 109.07/40.02 MAYBE 109.07/40.02 109.07/40.02 None of the processors succeeded. 109.07/40.02 109.07/40.02 Details of failed attempt(s): 109.07/40.02 ----------------------------- 109.07/40.02 1) 'empty' failed due to the following reason: 109.07/40.02 109.07/40.02 Empty strict component of the problem is NOT empty. 109.07/40.02 109.07/40.02 2) 'With Problem ...' failed due to the following reason: 109.07/40.02 109.07/40.02 None of the processors succeeded. 109.07/40.02 109.07/40.02 Details of failed attempt(s): 109.07/40.02 ----------------------------- 109.07/40.02 1) 'empty' failed due to the following reason: 109.07/40.02 109.07/40.02 Empty strict component of the problem is NOT empty. 109.07/40.02 109.07/40.02 2) 'Fastest' failed due to the following reason: 109.07/40.02 109.07/40.02 None of the processors succeeded. 109.07/40.02 109.07/40.02 Details of failed attempt(s): 109.07/40.02 ----------------------------- 109.07/40.02 1) 'With Problem ...' failed due to the following reason: 109.07/40.02 109.07/40.02 None of the processors succeeded. 109.07/40.02 109.07/40.02 Details of failed attempt(s): 109.07/40.02 ----------------------------- 109.07/40.02 1) 'empty' failed due to the following reason: 109.07/40.02 109.07/40.02 Empty strict component of the problem is NOT empty. 109.07/40.02 109.07/40.02 2) 'Polynomial Path Order (PS)' failed due to the following reason: 109.07/40.02 109.07/40.02 The input cannot be shown compatible 109.07/40.02 109.07/40.02 109.07/40.02 2) 'Polynomial Path Order (PS)' failed due to the following reason: 109.07/40.02 109.07/40.02 The input cannot be shown compatible 109.07/40.02 109.07/40.02 3) 'Fastest (timeout of 24 seconds)' failed due to the following 109.07/40.02 reason: 109.07/40.02 109.07/40.02 None of the processors succeeded. 109.07/40.02 109.07/40.02 Details of failed attempt(s): 109.07/40.02 ----------------------------- 109.07/40.02 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 109.07/40.02 failed due to the following reason: 109.07/40.02 109.07/40.02 match-boundness of the problem could not be verified. 109.07/40.02 109.07/40.02 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 109.07/40.02 failed due to the following reason: 109.07/40.02 109.07/40.02 match-boundness of the problem could not be verified. 109.07/40.02 109.07/40.02 109.07/40.02 109.07/40.02 109.07/40.02 109.07/40.02 2) 'Best' failed due to the following reason: 109.07/40.02 109.07/40.02 None of the processors succeeded. 109.07/40.02 109.07/40.02 Details of failed attempt(s): 109.07/40.02 ----------------------------- 109.07/40.02 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 109.07/40.02 seconds)' failed due to the following reason: 109.07/40.02 109.07/40.02 The weightgap principle applies (using the following nonconstant 109.07/40.02 growth matrix-interpretation) 109.07/40.02 109.07/40.02 The following argument positions are usable: 109.07/40.02 Uargs(and) = {1, 2} 109.07/40.02 109.07/40.02 TcT has computed the following matrix interpretation satisfying 109.07/40.02 not(EDA) and not(IDA(1)). 109.07/40.02 109.07/40.02 [conj](x1) = [0] 109.07/40.02 109.07/40.02 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.02 109.07/40.02 [isAnd](x1) = [0] 109.07/40.02 109.07/40.02 [isConsTerm](x1, x2) = [0] 109.07/40.02 109.07/40.02 [True] = [4] 109.07/40.02 109.07/40.02 [disj](x1) = [0] 109.07/40.02 109.07/40.02 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.02 109.07/40.02 [isOp](x1) = [0] 109.07/40.02 109.07/40.02 [getFirst](x1) = [1] x1 + [0] 109.07/40.02 109.07/40.02 [bool](x1) = [0] 109.07/40.02 109.07/40.02 [and](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.02 109.07/40.02 [getSecond](x1) = [1] x1 + [0] 109.07/40.02 109.07/40.02 [T] = [0] 109.07/40.02 109.07/40.02 [disjconj](x1) = [1] x1 + [7] 109.07/40.02 109.07/40.02 [F] = [0] 109.07/40.02 109.07/40.02 [False] = [4] 109.07/40.02 109.07/40.02 The order satisfies the following ordering constraints: 109.07/40.02 109.07/40.02 [conj(And(t1, t2))] = [0] 109.07/40.02 >= [0] 109.07/40.02 = [and(disj(t1), conj(t1))] 109.07/40.02 109.07/40.02 [conj(Or(o1, o2))] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [False()] 109.07/40.02 109.07/40.02 [conj(T())] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [True()] 109.07/40.02 109.07/40.02 [conj(F())] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [True()] 109.07/40.02 109.07/40.02 [isAnd(And(t1, t2))] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [True()] 109.07/40.02 109.07/40.02 [isAnd(Or(t1, t2))] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [False()] 109.07/40.02 109.07/40.02 [isAnd(T())] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [False()] 109.07/40.02 109.07/40.02 [isAnd(F())] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [False()] 109.07/40.02 109.07/40.02 [isConsTerm(And(a1, a2), And(y1, y2))] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [True()] 109.07/40.02 109.07/40.02 [isConsTerm(And(a1, a2), Or(x1, x2))] = [0] 109.07/40.02 ? [4] 109.07/40.02 = [False()] 109.07/40.02 109.07/40.03 [isConsTerm(And(a1, a2), T())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), F())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), And(y1, y2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), T())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), F())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), And(y1, y2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), Or(x1, x2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), T())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), F())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(F(), And(y1, y2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(F(), Or(x1, x2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(F(), T())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(F(), F())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [disj(And(a1, a2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [conj(And(a1, a2))] 109.07/40.03 109.07/40.03 [disj(Or(t1, t2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [and(conj(t1), disj(t1))] 109.07/40.03 109.07/40.03 [disj(T())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [disj(F())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isOp(And(t1, t2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isOp(Or(t1, t2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isOp(T())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isOp(F())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.03 >= [1] t1 + [0] 109.07/40.03 = [t1] 109.07/40.03 109.07/40.03 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.03 >= [1] t1 + [0] 109.07/40.03 = [t1] 109.07/40.03 109.07/40.03 [bool(And(a1, a2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [bool(Or(o1, o2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [bool(T())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [bool(F())] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [and(True(), True())] = [8] 109.07/40.03 > [4] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [and(True(), False())] = [8] 109.07/40.03 > [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [and(False(), True())] = [8] 109.07/40.03 > [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [and(False(), False())] = [8] 109.07/40.03 > [4] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.03 >= [1] t1 + [0] 109.07/40.03 = [t1] 109.07/40.03 109.07/40.03 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.03 >= [1] t1 + [0] 109.07/40.03 = [t1] 109.07/40.03 109.07/40.03 [disjconj(p)] = [1] p + [7] 109.07/40.03 > [0] 109.07/40.03 = [disj(p)] 109.07/40.03 109.07/40.03 109.07/40.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.03 109.07/40.03 We are left with following problem, upon which TcT provides the 109.07/40.03 certificate MAYBE. 109.07/40.03 109.07/40.03 Strict Trs: 109.07/40.03 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.03 , conj(Or(o1, o2)) -> False() 109.07/40.03 , conj(T()) -> True() 109.07/40.03 , conj(F()) -> True() 109.07/40.03 , isAnd(And(t1, t2)) -> True() 109.07/40.03 , isAnd(Or(t1, t2)) -> False() 109.07/40.03 , isAnd(T()) -> False() 109.07/40.03 , isAnd(F()) -> False() 109.07/40.03 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.03 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.03 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.03 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.03 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.03 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.03 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.03 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.03 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.03 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.03 , isConsTerm(T(), T()) -> True() 109.07/40.03 , isConsTerm(T(), F()) -> False() 109.07/40.03 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.03 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.03 , isConsTerm(F(), T()) -> False() 109.07/40.03 , isConsTerm(F(), F()) -> True() 109.07/40.03 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.03 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.03 , disj(T()) -> True() 109.07/40.03 , disj(F()) -> True() 109.07/40.03 , isOp(And(t1, t2)) -> True() 109.07/40.03 , isOp(Or(t1, t2)) -> True() 109.07/40.03 , isOp(T()) -> False() 109.07/40.03 , isOp(F()) -> False() 109.07/40.03 , getFirst(And(t1, t2)) -> t1 109.07/40.03 , getFirst(Or(t1, t2)) -> t1 109.07/40.03 , bool(And(a1, a2)) -> False() 109.07/40.03 , bool(Or(o1, o2)) -> False() 109.07/40.03 , bool(T()) -> True() 109.07/40.03 , bool(F()) -> True() 109.07/40.03 , getSecond(And(t1, t2)) -> t1 109.07/40.03 , getSecond(Or(t1, t2)) -> t1 } 109.07/40.03 Weak Trs: 109.07/40.03 { and(True(), True()) -> True() 109.07/40.03 , and(True(), False()) -> False() 109.07/40.03 , and(False(), True()) -> False() 109.07/40.03 , and(False(), False()) -> False() 109.07/40.03 , disjconj(p) -> disj(p) } 109.07/40.03 Obligation: 109.07/40.03 innermost runtime complexity 109.07/40.03 Answer: 109.07/40.03 MAYBE 109.07/40.03 109.07/40.03 The weightgap principle applies (using the following nonconstant 109.07/40.03 growth matrix-interpretation) 109.07/40.03 109.07/40.03 The following argument positions are usable: 109.07/40.03 Uargs(and) = {1, 2} 109.07/40.03 109.07/40.03 TcT has computed the following matrix interpretation satisfying 109.07/40.03 not(EDA) and not(IDA(1)). 109.07/40.03 109.07/40.03 [conj](x1) = [0] 109.07/40.03 109.07/40.03 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.03 109.07/40.03 [isAnd](x1) = [0] 109.07/40.03 109.07/40.03 [isConsTerm](x1, x2) = [0] 109.07/40.03 109.07/40.03 [True] = [0] 109.07/40.03 109.07/40.03 [disj](x1) = [4] 109.07/40.03 109.07/40.03 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.03 109.07/40.03 [isOp](x1) = [0] 109.07/40.03 109.07/40.03 [getFirst](x1) = [1] x1 + [0] 109.07/40.03 109.07/40.03 [bool](x1) = [0] 109.07/40.03 109.07/40.03 [and](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.03 109.07/40.03 [getSecond](x1) = [1] x1 + [0] 109.07/40.03 109.07/40.03 [T] = [0] 109.07/40.03 109.07/40.03 [disjconj](x1) = [1] x1 + [7] 109.07/40.03 109.07/40.03 [F] = [0] 109.07/40.03 109.07/40.03 [False] = [0] 109.07/40.03 109.07/40.03 The order satisfies the following ordering constraints: 109.07/40.03 109.07/40.03 [conj(And(t1, t2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [and(disj(t1), conj(t1))] 109.07/40.03 109.07/40.03 [conj(Or(o1, o2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [conj(T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [conj(F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isAnd(And(t1, t2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isAnd(Or(t1, t2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isAnd(T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isAnd(F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), And(y1, y2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), Or(x1, x2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), And(y1, y2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), And(y1, y2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), Or(x1, x2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(F(), And(y1, y2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(F(), Or(x1, x2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(F(), T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(F(), F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [disj(And(a1, a2))] = [4] 109.07/40.03 > [0] 109.07/40.03 = [conj(And(a1, a2))] 109.07/40.03 109.07/40.03 [disj(Or(t1, t2))] = [4] 109.07/40.03 >= [4] 109.07/40.03 = [and(conj(t1), disj(t1))] 109.07/40.03 109.07/40.03 [disj(T())] = [4] 109.07/40.03 > [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [disj(F())] = [4] 109.07/40.03 > [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isOp(And(t1, t2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isOp(Or(t1, t2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isOp(T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isOp(F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.03 >= [1] t1 + [0] 109.07/40.03 = [t1] 109.07/40.03 109.07/40.03 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.03 >= [1] t1 + [0] 109.07/40.03 = [t1] 109.07/40.03 109.07/40.03 [bool(And(a1, a2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [bool(Or(o1, o2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [bool(T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [bool(F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [and(True(), True())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [and(True(), False())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [and(False(), True())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [and(False(), False())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.03 >= [1] t1 + [0] 109.07/40.03 = [t1] 109.07/40.03 109.07/40.03 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.03 >= [1] t1 + [0] 109.07/40.03 = [t1] 109.07/40.03 109.07/40.03 [disjconj(p)] = [1] p + [7] 109.07/40.03 > [4] 109.07/40.03 = [disj(p)] 109.07/40.03 109.07/40.03 109.07/40.03 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.03 109.07/40.03 We are left with following problem, upon which TcT provides the 109.07/40.03 certificate MAYBE. 109.07/40.03 109.07/40.03 Strict Trs: 109.07/40.03 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.03 , conj(Or(o1, o2)) -> False() 109.07/40.03 , conj(T()) -> True() 109.07/40.03 , conj(F()) -> True() 109.07/40.03 , isAnd(And(t1, t2)) -> True() 109.07/40.03 , isAnd(Or(t1, t2)) -> False() 109.07/40.03 , isAnd(T()) -> False() 109.07/40.03 , isAnd(F()) -> False() 109.07/40.03 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.03 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.03 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.03 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.03 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.03 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.03 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.03 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.03 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.03 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.03 , isConsTerm(T(), T()) -> True() 109.07/40.03 , isConsTerm(T(), F()) -> False() 109.07/40.03 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.03 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.03 , isConsTerm(F(), T()) -> False() 109.07/40.03 , isConsTerm(F(), F()) -> True() 109.07/40.03 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.03 , isOp(And(t1, t2)) -> True() 109.07/40.03 , isOp(Or(t1, t2)) -> True() 109.07/40.03 , isOp(T()) -> False() 109.07/40.03 , isOp(F()) -> False() 109.07/40.03 , getFirst(And(t1, t2)) -> t1 109.07/40.03 , getFirst(Or(t1, t2)) -> t1 109.07/40.03 , bool(And(a1, a2)) -> False() 109.07/40.03 , bool(Or(o1, o2)) -> False() 109.07/40.03 , bool(T()) -> True() 109.07/40.03 , bool(F()) -> True() 109.07/40.03 , getSecond(And(t1, t2)) -> t1 109.07/40.03 , getSecond(Or(t1, t2)) -> t1 } 109.07/40.03 Weak Trs: 109.07/40.03 { disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.03 , disj(T()) -> True() 109.07/40.03 , disj(F()) -> True() 109.07/40.03 , and(True(), True()) -> True() 109.07/40.03 , and(True(), False()) -> False() 109.07/40.03 , and(False(), True()) -> False() 109.07/40.03 , and(False(), False()) -> False() 109.07/40.03 , disjconj(p) -> disj(p) } 109.07/40.03 Obligation: 109.07/40.03 innermost runtime complexity 109.07/40.03 Answer: 109.07/40.03 MAYBE 109.07/40.03 109.07/40.03 The weightgap principle applies (using the following nonconstant 109.07/40.03 growth matrix-interpretation) 109.07/40.03 109.07/40.03 The following argument positions are usable: 109.07/40.03 Uargs(and) = {1, 2} 109.07/40.03 109.07/40.03 TcT has computed the following matrix interpretation satisfying 109.07/40.03 not(EDA) and not(IDA(1)). 109.07/40.03 109.07/40.03 [conj](x1) = [0] 109.07/40.03 109.07/40.03 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.03 109.07/40.03 [isAnd](x1) = [0] 109.07/40.03 109.07/40.03 [isConsTerm](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.03 109.07/40.03 [True] = [0] 109.07/40.03 109.07/40.03 [disj](x1) = [0] 109.07/40.03 109.07/40.03 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.03 109.07/40.03 [isOp](x1) = [0] 109.07/40.03 109.07/40.03 [getFirst](x1) = [1] x1 + [0] 109.07/40.03 109.07/40.03 [bool](x1) = [0] 109.07/40.03 109.07/40.03 [and](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.03 109.07/40.03 [getSecond](x1) = [1] x1 + [0] 109.07/40.03 109.07/40.03 [T] = [0] 109.07/40.03 109.07/40.03 [disjconj](x1) = [1] x1 + [7] 109.07/40.03 109.07/40.03 [F] = [4] 109.07/40.03 109.07/40.03 [False] = [0] 109.07/40.03 109.07/40.03 The order satisfies the following ordering constraints: 109.07/40.03 109.07/40.03 [conj(And(t1, t2))] = [0] 109.07/40.03 ? [4] 109.07/40.03 = [and(disj(t1), conj(t1))] 109.07/40.03 109.07/40.03 [conj(Or(o1, o2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [conj(T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [conj(F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isAnd(And(t1, t2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isAnd(Or(t1, t2))] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isAnd(T())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isAnd(F())] = [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), And(y1, y2))] = [1] a1 + [1] a2 + [1] y1 + [1] y2 + [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), Or(x1, x2))] = [1] a1 + [1] a2 + [1] x1 + [1] x2 + [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), T())] = [1] a1 + [1] a2 + [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(And(a1, a2), F())] = [1] a1 + [1] a2 + [4] 109.07/40.03 > [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), And(y1, y2))] = [1] o1 + [1] o2 + [1] y1 + [1] y2 + [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [1] o1 + [1] o2 + [1] x1 + [1] x2 + [0] 109.07/40.03 >= [0] 109.07/40.03 = [True()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), T())] = [1] o1 + [1] o2 + [0] 109.07/40.03 >= [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(Or(o1, o2), F())] = [1] o1 + [1] o2 + [4] 109.07/40.03 > [0] 109.07/40.03 = [False()] 109.07/40.03 109.07/40.03 [isConsTerm(T(), And(y1, y2))] = [1] y1 + [1] y2 + [0] 109.07/40.03 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(T(), Or(x1, x2))] = [1] x1 + [1] x2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(T(), T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isConsTerm(T(), F())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(F(), And(y1, y2))] = [1] y1 + [1] y2 + [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(F(), Or(x1, x2))] = [1] x1 + [1] x2 + [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(F(), T())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(F(), F())] = [8] 109.07/40.04 > [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [disj(And(a1, a2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [conj(And(a1, a2))] 109.07/40.04 109.07/40.04 [disj(Or(t1, t2))] = [0] 109.07/40.04 ? [4] 109.07/40.04 = [and(conj(t1), disj(t1))] 109.07/40.04 109.07/40.04 [disj(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [disj(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isOp(And(t1, t2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isOp(Or(t1, t2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isOp(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isOp(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [1] t1 + [0] 109.07/40.04 = [t1] 109.07/40.04 109.07/40.04 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [1] t1 + [0] 109.07/40.04 = [t1] 109.07/40.04 109.07/40.04 [bool(And(a1, a2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [bool(Or(o1, o2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [bool(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [bool(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [and(True(), True())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [and(True(), False())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [and(False(), True())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [and(False(), False())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [1] t1 + [0] 109.07/40.04 = [t1] 109.07/40.04 109.07/40.04 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [1] t1 + [0] 109.07/40.04 = [t1] 109.07/40.04 109.07/40.04 [disjconj(p)] = [1] p + [7] 109.07/40.04 > [0] 109.07/40.04 = [disj(p)] 109.07/40.04 109.07/40.04 109.07/40.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.04 109.07/40.04 We are left with following problem, upon which TcT provides the 109.07/40.04 certificate MAYBE. 109.07/40.04 109.07/40.04 Strict Trs: 109.07/40.04 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.04 , conj(Or(o1, o2)) -> False() 109.07/40.04 , conj(T()) -> True() 109.07/40.04 , conj(F()) -> True() 109.07/40.04 , isAnd(And(t1, t2)) -> True() 109.07/40.04 , isAnd(Or(t1, t2)) -> False() 109.07/40.04 , isAnd(T()) -> False() 109.07/40.04 , isAnd(F()) -> False() 109.07/40.04 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.04 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.04 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.04 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.04 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.04 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.04 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.04 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.04 , isConsTerm(T(), T()) -> True() 109.07/40.04 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.04 , isOp(And(t1, t2)) -> True() 109.07/40.04 , isOp(Or(t1, t2)) -> True() 109.07/40.04 , isOp(T()) -> False() 109.07/40.04 , isOp(F()) -> False() 109.07/40.04 , getFirst(And(t1, t2)) -> t1 109.07/40.04 , getFirst(Or(t1, t2)) -> t1 109.07/40.04 , bool(And(a1, a2)) -> False() 109.07/40.04 , bool(Or(o1, o2)) -> False() 109.07/40.04 , bool(T()) -> True() 109.07/40.04 , bool(F()) -> True() 109.07/40.04 , getSecond(And(t1, t2)) -> t1 109.07/40.04 , getSecond(Or(t1, t2)) -> t1 } 109.07/40.04 Weak Trs: 109.07/40.04 { isConsTerm(And(a1, a2), F()) -> False() 109.07/40.04 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.04 , isConsTerm(T(), F()) -> False() 109.07/40.04 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.04 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.04 , isConsTerm(F(), T()) -> False() 109.07/40.04 , isConsTerm(F(), F()) -> True() 109.07/40.04 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.04 , disj(T()) -> True() 109.07/40.04 , disj(F()) -> True() 109.07/40.04 , and(True(), True()) -> True() 109.07/40.04 , and(True(), False()) -> False() 109.07/40.04 , and(False(), True()) -> False() 109.07/40.04 , and(False(), False()) -> False() 109.07/40.04 , disjconj(p) -> disj(p) } 109.07/40.04 Obligation: 109.07/40.04 innermost runtime complexity 109.07/40.04 Answer: 109.07/40.04 MAYBE 109.07/40.04 109.07/40.04 The weightgap principle applies (using the following nonconstant 109.07/40.04 growth matrix-interpretation) 109.07/40.04 109.07/40.04 The following argument positions are usable: 109.07/40.04 Uargs(and) = {1, 2} 109.07/40.04 109.07/40.04 TcT has computed the following matrix interpretation satisfying 109.07/40.04 not(EDA) and not(IDA(1)). 109.07/40.04 109.07/40.04 [conj](x1) = [0] 109.07/40.04 109.07/40.04 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.04 109.07/40.04 [isAnd](x1) = [1] x1 + [0] 109.07/40.04 109.07/40.04 [isConsTerm](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.04 109.07/40.04 [True] = [0] 109.07/40.04 109.07/40.04 [disj](x1) = [0] 109.07/40.04 109.07/40.04 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.04 109.07/40.04 [isOp](x1) = [0] 109.07/40.04 109.07/40.04 [getFirst](x1) = [1] x1 + [0] 109.07/40.04 109.07/40.04 [bool](x1) = [0] 109.07/40.04 109.07/40.04 [and](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.04 109.07/40.04 [getSecond](x1) = [1] x1 + [0] 109.07/40.04 109.07/40.04 [T] = [0] 109.07/40.04 109.07/40.04 [disjconj](x1) = [1] x1 + [7] 109.07/40.04 109.07/40.04 [F] = [4] 109.07/40.04 109.07/40.04 [False] = [0] 109.07/40.04 109.07/40.04 The order satisfies the following ordering constraints: 109.07/40.04 109.07/40.04 [conj(And(t1, t2))] = [0] 109.07/40.04 ? [4] 109.07/40.04 = [and(disj(t1), conj(t1))] 109.07/40.04 109.07/40.04 [conj(Or(o1, o2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [conj(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [conj(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isAnd(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isAnd(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isAnd(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isAnd(F())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(And(a1, a2), And(y1, y2))] = [1] a1 + [1] a2 + [1] y1 + [1] y2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isConsTerm(And(a1, a2), Or(x1, x2))] = [1] a1 + [1] a2 + [1] x1 + [1] x2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(And(a1, a2), T())] = [1] a1 + [1] a2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(And(a1, a2), F())] = [1] a1 + [1] a2 + [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(Or(o1, o2), And(y1, y2))] = [1] o1 + [1] o2 + [1] y1 + [1] y2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [1] o1 + [1] o2 + [1] x1 + [1] x2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isConsTerm(Or(o1, o2), T())] = [1] o1 + [1] o2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(Or(o1, o2), F())] = [1] o1 + [1] o2 + [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(T(), And(y1, y2))] = [1] y1 + [1] y2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(T(), Or(x1, x2))] = [1] x1 + [1] x2 + [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(T(), T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isConsTerm(T(), F())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(F(), And(y1, y2))] = [1] y1 + [1] y2 + [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(F(), Or(x1, x2))] = [1] x1 + [1] x2 + [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(F(), T())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(F(), F())] = [8] 109.07/40.04 > [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [disj(And(a1, a2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [conj(And(a1, a2))] 109.07/40.04 109.07/40.04 [disj(Or(t1, t2))] = [0] 109.07/40.04 ? [4] 109.07/40.04 = [and(conj(t1), disj(t1))] 109.07/40.04 109.07/40.04 [disj(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [disj(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isOp(And(t1, t2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isOp(Or(t1, t2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isOp(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isOp(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [1] t1 + [0] 109.07/40.04 = [t1] 109.07/40.04 109.07/40.04 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [1] t1 + [0] 109.07/40.04 = [t1] 109.07/40.04 109.07/40.04 [bool(And(a1, a2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [bool(Or(o1, o2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [bool(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [bool(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [and(True(), True())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [and(True(), False())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [and(False(), True())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [and(False(), False())] = [4] 109.07/40.04 > [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [1] t1 + [0] 109.07/40.04 = [t1] 109.07/40.04 109.07/40.04 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.04 >= [1] t1 + [0] 109.07/40.04 = [t1] 109.07/40.04 109.07/40.04 [disjconj(p)] = [1] p + [7] 109.07/40.04 > [0] 109.07/40.04 = [disj(p)] 109.07/40.04 109.07/40.04 109.07/40.04 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.04 109.07/40.04 We are left with following problem, upon which TcT provides the 109.07/40.04 certificate MAYBE. 109.07/40.04 109.07/40.04 Strict Trs: 109.07/40.04 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.04 , conj(Or(o1, o2)) -> False() 109.07/40.04 , conj(T()) -> True() 109.07/40.04 , conj(F()) -> True() 109.07/40.04 , isAnd(And(t1, t2)) -> True() 109.07/40.04 , isAnd(Or(t1, t2)) -> False() 109.07/40.04 , isAnd(T()) -> False() 109.07/40.04 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.04 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.04 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.04 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.04 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.04 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.04 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.04 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.04 , isConsTerm(T(), T()) -> True() 109.07/40.04 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.04 , isOp(And(t1, t2)) -> True() 109.07/40.04 , isOp(Or(t1, t2)) -> True() 109.07/40.04 , isOp(T()) -> False() 109.07/40.04 , isOp(F()) -> False() 109.07/40.04 , getFirst(And(t1, t2)) -> t1 109.07/40.04 , getFirst(Or(t1, t2)) -> t1 109.07/40.04 , bool(And(a1, a2)) -> False() 109.07/40.04 , bool(Or(o1, o2)) -> False() 109.07/40.04 , bool(T()) -> True() 109.07/40.04 , bool(F()) -> True() 109.07/40.04 , getSecond(And(t1, t2)) -> t1 109.07/40.04 , getSecond(Or(t1, t2)) -> t1 } 109.07/40.04 Weak Trs: 109.07/40.04 { isAnd(F()) -> False() 109.07/40.04 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.04 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.04 , isConsTerm(T(), F()) -> False() 109.07/40.04 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.04 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.04 , isConsTerm(F(), T()) -> False() 109.07/40.04 , isConsTerm(F(), F()) -> True() 109.07/40.04 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.04 , disj(T()) -> True() 109.07/40.04 , disj(F()) -> True() 109.07/40.04 , and(True(), True()) -> True() 109.07/40.04 , and(True(), False()) -> False() 109.07/40.04 , and(False(), True()) -> False() 109.07/40.04 , and(False(), False()) -> False() 109.07/40.04 , disjconj(p) -> disj(p) } 109.07/40.04 Obligation: 109.07/40.04 innermost runtime complexity 109.07/40.04 Answer: 109.07/40.04 MAYBE 109.07/40.04 109.07/40.04 The weightgap principle applies (using the following nonconstant 109.07/40.04 growth matrix-interpretation) 109.07/40.04 109.07/40.04 The following argument positions are usable: 109.07/40.04 Uargs(and) = {1, 2} 109.07/40.04 109.07/40.04 TcT has computed the following matrix interpretation satisfying 109.07/40.04 not(EDA) and not(IDA(1)). 109.07/40.04 109.07/40.04 [conj](x1) = [0] 109.07/40.04 109.07/40.04 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.04 109.07/40.04 [isAnd](x1) = [0] 109.07/40.04 109.07/40.04 [isConsTerm](x1, x2) = [0] 109.07/40.04 109.07/40.04 [True] = [0] 109.07/40.04 109.07/40.04 [disj](x1) = [0] 109.07/40.04 109.07/40.04 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.04 109.07/40.04 [isOp](x1) = [0] 109.07/40.04 109.07/40.04 [getFirst](x1) = [1] x1 + [0] 109.07/40.04 109.07/40.04 [bool](x1) = [1] x1 + [0] 109.07/40.04 109.07/40.04 [and](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.04 109.07/40.04 [getSecond](x1) = [1] x1 + [0] 109.07/40.04 109.07/40.04 [T] = [0] 109.07/40.04 109.07/40.04 [disjconj](x1) = [1] x1 + [7] 109.07/40.04 109.07/40.04 [F] = [4] 109.07/40.04 109.07/40.04 [False] = [0] 109.07/40.04 109.07/40.04 The order satisfies the following ordering constraints: 109.07/40.04 109.07/40.04 [conj(And(t1, t2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [and(disj(t1), conj(t1))] 109.07/40.04 109.07/40.04 [conj(Or(o1, o2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [conj(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [conj(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isAnd(And(t1, t2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isAnd(Or(t1, t2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isAnd(T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isAnd(F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(And(a1, a2), And(y1, y2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [True()] 109.07/40.04 109.07/40.04 [isConsTerm(And(a1, a2), Or(x1, x2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(And(a1, a2), T())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(And(a1, a2), F())] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.04 109.07/40.04 [isConsTerm(Or(o1, o2), And(y1, y2))] = [0] 109.07/40.04 >= [0] 109.07/40.04 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [disj(And(a1, a2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [conj(And(a1, a2))] 109.07/40.05 109.07/40.05 [disj(Or(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [and(conj(t1), disj(t1))] 109.07/40.05 109.07/40.05 [disj(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [disj(F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isOp(And(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isOp(Or(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isOp(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isOp(F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.05 >= [1] t1 + [0] 109.07/40.05 = [t1] 109.07/40.05 109.07/40.05 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.05 >= [1] t1 + [0] 109.07/40.05 = [t1] 109.07/40.05 109.07/40.05 [bool(And(a1, a2))] = [1] a1 + [1] a2 + [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [bool(Or(o1, o2))] = [1] o1 + [1] o2 + [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [bool(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [bool(F())] = [4] 109.07/40.05 > [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [and(True(), True())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [and(True(), False())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [and(False(), True())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [and(False(), False())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.05 >= [1] t1 + [0] 109.07/40.05 = [t1] 109.07/40.05 109.07/40.05 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.05 >= [1] t1 + [0] 109.07/40.05 = [t1] 109.07/40.05 109.07/40.05 [disjconj(p)] = [1] p + [7] 109.07/40.05 > [0] 109.07/40.05 = [disj(p)] 109.07/40.05 109.07/40.05 109.07/40.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.05 109.07/40.05 We are left with following problem, upon which TcT provides the 109.07/40.05 certificate MAYBE. 109.07/40.05 109.07/40.05 Strict Trs: 109.07/40.05 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.05 , conj(Or(o1, o2)) -> False() 109.07/40.05 , conj(T()) -> True() 109.07/40.05 , conj(F()) -> True() 109.07/40.05 , isAnd(And(t1, t2)) -> True() 109.07/40.05 , isAnd(Or(t1, t2)) -> False() 109.07/40.05 , isAnd(T()) -> False() 109.07/40.05 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.05 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.05 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.05 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.05 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.05 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.05 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.05 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.05 , isConsTerm(T(), T()) -> True() 109.07/40.05 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.05 , isOp(And(t1, t2)) -> True() 109.07/40.05 , isOp(Or(t1, t2)) -> True() 109.07/40.05 , isOp(T()) -> False() 109.07/40.05 , isOp(F()) -> False() 109.07/40.05 , getFirst(And(t1, t2)) -> t1 109.07/40.05 , getFirst(Or(t1, t2)) -> t1 109.07/40.05 , bool(And(a1, a2)) -> False() 109.07/40.05 , bool(Or(o1, o2)) -> False() 109.07/40.05 , bool(T()) -> True() 109.07/40.05 , getSecond(And(t1, t2)) -> t1 109.07/40.05 , getSecond(Or(t1, t2)) -> t1 } 109.07/40.05 Weak Trs: 109.07/40.05 { isAnd(F()) -> False() 109.07/40.05 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.05 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.05 , isConsTerm(T(), F()) -> False() 109.07/40.05 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.05 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.05 , isConsTerm(F(), T()) -> False() 109.07/40.05 , isConsTerm(F(), F()) -> True() 109.07/40.05 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.05 , disj(T()) -> True() 109.07/40.05 , disj(F()) -> True() 109.07/40.05 , bool(F()) -> True() 109.07/40.05 , and(True(), True()) -> True() 109.07/40.05 , and(True(), False()) -> False() 109.07/40.05 , and(False(), True()) -> False() 109.07/40.05 , and(False(), False()) -> False() 109.07/40.05 , disjconj(p) -> disj(p) } 109.07/40.05 Obligation: 109.07/40.05 innermost runtime complexity 109.07/40.05 Answer: 109.07/40.05 MAYBE 109.07/40.05 109.07/40.05 The weightgap principle applies (using the following nonconstant 109.07/40.05 growth matrix-interpretation) 109.07/40.05 109.07/40.05 The following argument positions are usable: 109.07/40.05 Uargs(and) = {1, 2} 109.07/40.05 109.07/40.05 TcT has computed the following matrix interpretation satisfying 109.07/40.05 not(EDA) and not(IDA(1)). 109.07/40.05 109.07/40.05 [conj](x1) = [0] 109.07/40.05 109.07/40.05 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.05 109.07/40.05 [isAnd](x1) = [0] 109.07/40.05 109.07/40.05 [isConsTerm](x1, x2) = [0] 109.07/40.05 109.07/40.05 [True] = [0] 109.07/40.05 109.07/40.05 [disj](x1) = [0] 109.07/40.05 109.07/40.05 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.05 109.07/40.05 [isOp](x1) = [0] 109.07/40.05 109.07/40.05 [getFirst](x1) = [1] x1 + [0] 109.07/40.05 109.07/40.05 [bool](x1) = [4] 109.07/40.05 109.07/40.05 [and](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.05 109.07/40.05 [getSecond](x1) = [1] x1 + [0] 109.07/40.05 109.07/40.05 [T] = [0] 109.07/40.05 109.07/40.05 [disjconj](x1) = [1] x1 + [7] 109.07/40.05 109.07/40.05 [F] = [0] 109.07/40.05 109.07/40.05 [False] = [0] 109.07/40.05 109.07/40.05 The order satisfies the following ordering constraints: 109.07/40.05 109.07/40.05 [conj(And(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [and(disj(t1), conj(t1))] 109.07/40.05 109.07/40.05 [conj(Or(o1, o2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [conj(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [conj(F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isAnd(And(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isAnd(Or(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isAnd(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isAnd(F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(And(a1, a2), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isConsTerm(And(a1, a2), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(And(a1, a2), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(And(a1, a2), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [disj(And(a1, a2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [conj(And(a1, a2))] 109.07/40.05 109.07/40.05 [disj(Or(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [and(conj(t1), disj(t1))] 109.07/40.05 109.07/40.05 [disj(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [disj(F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isOp(And(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isOp(Or(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isOp(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isOp(F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.05 >= [1] t1 + [0] 109.07/40.05 = [t1] 109.07/40.05 109.07/40.05 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.05 >= [1] t1 + [0] 109.07/40.05 = [t1] 109.07/40.05 109.07/40.05 [bool(And(a1, a2))] = [4] 109.07/40.05 > [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [bool(Or(o1, o2))] = [4] 109.07/40.05 > [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [bool(T())] = [4] 109.07/40.05 > [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [bool(F())] = [4] 109.07/40.05 > [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [and(True(), True())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [and(True(), False())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [and(False(), True())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [and(False(), False())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.05 >= [1] t1 + [0] 109.07/40.05 = [t1] 109.07/40.05 109.07/40.05 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.05 >= [1] t1 + [0] 109.07/40.05 = [t1] 109.07/40.05 109.07/40.05 [disjconj(p)] = [1] p + [7] 109.07/40.05 > [0] 109.07/40.05 = [disj(p)] 109.07/40.05 109.07/40.05 109.07/40.05 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.05 109.07/40.05 We are left with following problem, upon which TcT provides the 109.07/40.05 certificate MAYBE. 109.07/40.05 109.07/40.05 Strict Trs: 109.07/40.05 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.05 , conj(Or(o1, o2)) -> False() 109.07/40.05 , conj(T()) -> True() 109.07/40.05 , conj(F()) -> True() 109.07/40.05 , isAnd(And(t1, t2)) -> True() 109.07/40.05 , isAnd(Or(t1, t2)) -> False() 109.07/40.05 , isAnd(T()) -> False() 109.07/40.05 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.05 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.05 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.05 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.05 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.05 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.05 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.05 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.05 , isConsTerm(T(), T()) -> True() 109.07/40.05 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.05 , isOp(And(t1, t2)) -> True() 109.07/40.05 , isOp(Or(t1, t2)) -> True() 109.07/40.05 , isOp(T()) -> False() 109.07/40.05 , isOp(F()) -> False() 109.07/40.05 , getFirst(And(t1, t2)) -> t1 109.07/40.05 , getFirst(Or(t1, t2)) -> t1 109.07/40.05 , getSecond(And(t1, t2)) -> t1 109.07/40.05 , getSecond(Or(t1, t2)) -> t1 } 109.07/40.05 Weak Trs: 109.07/40.05 { isAnd(F()) -> False() 109.07/40.05 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.05 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.05 , isConsTerm(T(), F()) -> False() 109.07/40.05 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.05 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.05 , isConsTerm(F(), T()) -> False() 109.07/40.05 , isConsTerm(F(), F()) -> True() 109.07/40.05 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.05 , disj(T()) -> True() 109.07/40.05 , disj(F()) -> True() 109.07/40.05 , bool(And(a1, a2)) -> False() 109.07/40.05 , bool(Or(o1, o2)) -> False() 109.07/40.05 , bool(T()) -> True() 109.07/40.05 , bool(F()) -> True() 109.07/40.05 , and(True(), True()) -> True() 109.07/40.05 , and(True(), False()) -> False() 109.07/40.05 , and(False(), True()) -> False() 109.07/40.05 , and(False(), False()) -> False() 109.07/40.05 , disjconj(p) -> disj(p) } 109.07/40.05 Obligation: 109.07/40.05 innermost runtime complexity 109.07/40.05 Answer: 109.07/40.05 MAYBE 109.07/40.05 109.07/40.05 The weightgap principle applies (using the following nonconstant 109.07/40.05 growth matrix-interpretation) 109.07/40.05 109.07/40.05 The following argument positions are usable: 109.07/40.05 Uargs(and) = {1, 2} 109.07/40.05 109.07/40.05 TcT has computed the following matrix interpretation satisfying 109.07/40.05 not(EDA) and not(IDA(1)). 109.07/40.05 109.07/40.05 [conj](x1) = [0] 109.07/40.05 109.07/40.05 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.05 109.07/40.05 [isAnd](x1) = [0] 109.07/40.05 109.07/40.05 [isConsTerm](x1, x2) = [0] 109.07/40.05 109.07/40.05 [True] = [0] 109.07/40.05 109.07/40.05 [disj](x1) = [0] 109.07/40.05 109.07/40.05 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.05 109.07/40.05 [isOp](x1) = [1] x1 + [0] 109.07/40.05 109.07/40.05 [getFirst](x1) = [1] x1 + [0] 109.07/40.05 109.07/40.05 [bool](x1) = [4] 109.07/40.05 109.07/40.05 [and](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.05 109.07/40.05 [getSecond](x1) = [1] x1 + [0] 109.07/40.05 109.07/40.05 [T] = [0] 109.07/40.05 109.07/40.05 [disjconj](x1) = [1] x1 + [7] 109.07/40.05 109.07/40.05 [F] = [4] 109.07/40.05 109.07/40.05 [False] = [0] 109.07/40.05 109.07/40.05 The order satisfies the following ordering constraints: 109.07/40.05 109.07/40.05 [conj(And(t1, t2))] = [0] 109.07/40.05 ? [4] 109.07/40.05 = [and(disj(t1), conj(t1))] 109.07/40.05 109.07/40.05 [conj(Or(o1, o2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [conj(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [conj(F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isAnd(And(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isAnd(Or(t1, t2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isAnd(T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isAnd(F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(And(a1, a2), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isConsTerm(And(a1, a2), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(And(a1, a2), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(And(a1, a2), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(Or(o1, o2), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), T())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [True()] 109.07/40.05 109.07/40.05 [isConsTerm(T(), F())] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), And(y1, y2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.05 [isConsTerm(F(), Or(x1, x2))] = [0] 109.07/40.05 >= [0] 109.07/40.05 = [False()] 109.07/40.05 109.07/40.06 [isConsTerm(F(), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [disj(And(a1, a2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [conj(And(a1, a2))] 109.07/40.06 109.07/40.06 [disj(Or(t1, t2))] = [0] 109.07/40.06 ? [4] 109.07/40.06 = [and(conj(t1), disj(t1))] 109.07/40.06 109.07/40.06 [disj(T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [disj(F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isOp(F())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.06 >= [1] t1 + [0] 109.07/40.06 = [t1] 109.07/40.06 109.07/40.06 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.06 >= [1] t1 + [0] 109.07/40.06 = [t1] 109.07/40.06 109.07/40.06 [bool(And(a1, a2))] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [bool(Or(o1, o2))] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [bool(T())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [bool(F())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [and(True(), True())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [and(True(), False())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [and(False(), True())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [and(False(), False())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.06 >= [1] t1 + [0] 109.07/40.06 = [t1] 109.07/40.06 109.07/40.06 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.06 >= [1] t1 + [0] 109.07/40.06 = [t1] 109.07/40.06 109.07/40.06 [disjconj(p)] = [1] p + [7] 109.07/40.06 > [0] 109.07/40.06 = [disj(p)] 109.07/40.06 109.07/40.06 109.07/40.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.06 109.07/40.06 We are left with following problem, upon which TcT provides the 109.07/40.06 certificate MAYBE. 109.07/40.06 109.07/40.06 Strict Trs: 109.07/40.06 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.06 , conj(Or(o1, o2)) -> False() 109.07/40.06 , conj(T()) -> True() 109.07/40.06 , conj(F()) -> True() 109.07/40.06 , isAnd(And(t1, t2)) -> True() 109.07/40.06 , isAnd(Or(t1, t2)) -> False() 109.07/40.06 , isAnd(T()) -> False() 109.07/40.06 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.06 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.06 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.06 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.06 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.06 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.06 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.06 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.06 , isConsTerm(T(), T()) -> True() 109.07/40.06 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.06 , isOp(And(t1, t2)) -> True() 109.07/40.06 , isOp(Or(t1, t2)) -> True() 109.07/40.06 , isOp(T()) -> False() 109.07/40.06 , getFirst(And(t1, t2)) -> t1 109.07/40.06 , getFirst(Or(t1, t2)) -> t1 109.07/40.06 , getSecond(And(t1, t2)) -> t1 109.07/40.06 , getSecond(Or(t1, t2)) -> t1 } 109.07/40.06 Weak Trs: 109.07/40.06 { isAnd(F()) -> False() 109.07/40.06 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.06 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.06 , isConsTerm(T(), F()) -> False() 109.07/40.06 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.06 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.06 , isConsTerm(F(), T()) -> False() 109.07/40.06 , isConsTerm(F(), F()) -> True() 109.07/40.06 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.06 , disj(T()) -> True() 109.07/40.06 , disj(F()) -> True() 109.07/40.06 , isOp(F()) -> False() 109.07/40.06 , bool(And(a1, a2)) -> False() 109.07/40.06 , bool(Or(o1, o2)) -> False() 109.07/40.06 , bool(T()) -> True() 109.07/40.06 , bool(F()) -> True() 109.07/40.06 , and(True(), True()) -> True() 109.07/40.06 , and(True(), False()) -> False() 109.07/40.06 , and(False(), True()) -> False() 109.07/40.06 , and(False(), False()) -> False() 109.07/40.06 , disjconj(p) -> disj(p) } 109.07/40.06 Obligation: 109.07/40.06 innermost runtime complexity 109.07/40.06 Answer: 109.07/40.06 MAYBE 109.07/40.06 109.07/40.06 The weightgap principle applies (using the following nonconstant 109.07/40.06 growth matrix-interpretation) 109.07/40.06 109.07/40.06 The following argument positions are usable: 109.07/40.06 Uargs(and) = {1, 2} 109.07/40.06 109.07/40.06 TcT has computed the following matrix interpretation satisfying 109.07/40.06 not(EDA) and not(IDA(1)). 109.07/40.06 109.07/40.06 [conj](x1) = [0] 109.07/40.06 109.07/40.06 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.06 109.07/40.06 [isAnd](x1) = [4] 109.07/40.06 109.07/40.06 [isConsTerm](x1, x2) = [0] 109.07/40.06 109.07/40.06 [True] = [0] 109.07/40.06 109.07/40.06 [disj](x1) = [0] 109.07/40.06 109.07/40.06 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.06 109.07/40.06 [isOp](x1) = [0] 109.07/40.06 109.07/40.06 [getFirst](x1) = [1] x1 + [1] 109.07/40.06 109.07/40.06 [bool](x1) = [4] 109.07/40.06 109.07/40.06 [and](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.06 109.07/40.06 [getSecond](x1) = [1] x1 + [0] 109.07/40.06 109.07/40.06 [T] = [0] 109.07/40.06 109.07/40.06 [disjconj](x1) = [1] x1 + [7] 109.07/40.06 109.07/40.06 [F] = [0] 109.07/40.06 109.07/40.06 [False] = [0] 109.07/40.06 109.07/40.06 The order satisfies the following ordering constraints: 109.07/40.06 109.07/40.06 [conj(And(t1, t2))] = [0] 109.07/40.06 ? [4] 109.07/40.06 = [and(disj(t1), conj(t1))] 109.07/40.06 109.07/40.06 [conj(Or(o1, o2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [conj(T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [conj(F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isAnd(And(t1, t2))] = [4] 109.07/40.06 > [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isAnd(Or(t1, t2))] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isAnd(T())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isAnd(F())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(And(a1, a2), And(y1, y2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isConsTerm(And(a1, a2), Or(x1, x2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(And(a1, a2), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(And(a1, a2), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(Or(o1, o2), And(y1, y2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isConsTerm(Or(o1, o2), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(Or(o1, o2), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(T(), And(y1, y2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(T(), Or(x1, x2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(T(), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isConsTerm(T(), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), And(y1, y2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), Or(x1, x2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [disj(And(a1, a2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [conj(And(a1, a2))] 109.07/40.06 109.07/40.06 [disj(Or(t1, t2))] = [0] 109.07/40.06 ? [4] 109.07/40.06 = [and(conj(t1), disj(t1))] 109.07/40.06 109.07/40.06 [disj(T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [disj(F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(And(t1, t2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(Or(t1, t2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isOp(F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [1] 109.07/40.06 > [1] t1 + [0] 109.07/40.06 = [t1] 109.07/40.06 109.07/40.06 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [1] 109.07/40.06 > [1] t1 + [0] 109.07/40.06 = [t1] 109.07/40.06 109.07/40.06 [bool(And(a1, a2))] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [bool(Or(o1, o2))] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [bool(T())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [bool(F())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [and(True(), True())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [and(True(), False())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [and(False(), True())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [and(False(), False())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.06 >= [1] t1 + [0] 109.07/40.06 = [t1] 109.07/40.06 109.07/40.06 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.06 >= [1] t1 + [0] 109.07/40.06 = [t1] 109.07/40.06 109.07/40.06 [disjconj(p)] = [1] p + [7] 109.07/40.06 > [0] 109.07/40.06 = [disj(p)] 109.07/40.06 109.07/40.06 109.07/40.06 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.06 109.07/40.06 We are left with following problem, upon which TcT provides the 109.07/40.06 certificate MAYBE. 109.07/40.06 109.07/40.06 Strict Trs: 109.07/40.06 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.06 , conj(Or(o1, o2)) -> False() 109.07/40.06 , conj(T()) -> True() 109.07/40.06 , conj(F()) -> True() 109.07/40.06 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.06 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.06 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.06 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.06 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.06 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.06 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.06 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.06 , isConsTerm(T(), T()) -> True() 109.07/40.06 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.06 , isOp(And(t1, t2)) -> True() 109.07/40.06 , isOp(Or(t1, t2)) -> True() 109.07/40.06 , isOp(T()) -> False() 109.07/40.06 , getSecond(And(t1, t2)) -> t1 109.07/40.06 , getSecond(Or(t1, t2)) -> t1 } 109.07/40.06 Weak Trs: 109.07/40.06 { isAnd(And(t1, t2)) -> True() 109.07/40.06 , isAnd(Or(t1, t2)) -> False() 109.07/40.06 , isAnd(T()) -> False() 109.07/40.06 , isAnd(F()) -> False() 109.07/40.06 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.06 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.06 , isConsTerm(T(), F()) -> False() 109.07/40.06 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.06 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.06 , isConsTerm(F(), T()) -> False() 109.07/40.06 , isConsTerm(F(), F()) -> True() 109.07/40.06 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.06 , disj(T()) -> True() 109.07/40.06 , disj(F()) -> True() 109.07/40.06 , isOp(F()) -> False() 109.07/40.06 , getFirst(And(t1, t2)) -> t1 109.07/40.06 , getFirst(Or(t1, t2)) -> t1 109.07/40.06 , bool(And(a1, a2)) -> False() 109.07/40.06 , bool(Or(o1, o2)) -> False() 109.07/40.06 , bool(T()) -> True() 109.07/40.06 , bool(F()) -> True() 109.07/40.06 , and(True(), True()) -> True() 109.07/40.06 , and(True(), False()) -> False() 109.07/40.06 , and(False(), True()) -> False() 109.07/40.06 , and(False(), False()) -> False() 109.07/40.06 , disjconj(p) -> disj(p) } 109.07/40.06 Obligation: 109.07/40.06 innermost runtime complexity 109.07/40.06 Answer: 109.07/40.06 MAYBE 109.07/40.06 109.07/40.06 The weightgap principle applies (using the following nonconstant 109.07/40.06 growth matrix-interpretation) 109.07/40.06 109.07/40.06 The following argument positions are usable: 109.07/40.06 Uargs(and) = {1, 2} 109.07/40.06 109.07/40.06 TcT has computed the following matrix interpretation satisfying 109.07/40.06 not(EDA) and not(IDA(1)). 109.07/40.06 109.07/40.06 [conj](x1) = [0] 109.07/40.06 109.07/40.06 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.06 109.07/40.06 [isAnd](x1) = [4] 109.07/40.06 109.07/40.06 [isConsTerm](x1, x2) = [0] 109.07/40.06 109.07/40.06 [True] = [0] 109.07/40.06 109.07/40.06 [disj](x1) = [0] 109.07/40.06 109.07/40.06 [Or](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.06 109.07/40.06 [isOp](x1) = [0] 109.07/40.06 109.07/40.06 [getFirst](x1) = [1] x1 + [7] 109.07/40.06 109.07/40.06 [bool](x1) = [4] 109.07/40.06 109.07/40.06 [and](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.06 109.07/40.06 [getSecond](x1) = [1] x1 + [4] 109.07/40.06 109.07/40.06 [T] = [0] 109.07/40.06 109.07/40.06 [disjconj](x1) = [1] x1 + [7] 109.07/40.06 109.07/40.06 [F] = [0] 109.07/40.06 109.07/40.06 [False] = [0] 109.07/40.06 109.07/40.06 The order satisfies the following ordering constraints: 109.07/40.06 109.07/40.06 [conj(And(t1, t2))] = [0] 109.07/40.06 ? [4] 109.07/40.06 = [and(disj(t1), conj(t1))] 109.07/40.06 109.07/40.06 [conj(Or(o1, o2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [conj(T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [conj(F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isAnd(And(t1, t2))] = [4] 109.07/40.06 > [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isAnd(Or(t1, t2))] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isAnd(T())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isAnd(F())] = [4] 109.07/40.06 > [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(And(a1, a2), And(y1, y2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isConsTerm(And(a1, a2), Or(x1, x2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(And(a1, a2), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(And(a1, a2), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(Or(o1, o2), And(y1, y2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isConsTerm(Or(o1, o2), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(Or(o1, o2), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(T(), And(y1, y2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(T(), Or(x1, x2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(T(), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isConsTerm(T(), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), And(y1, y2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), Or(x1, x2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isConsTerm(F(), F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [disj(And(a1, a2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [conj(And(a1, a2))] 109.07/40.06 109.07/40.06 [disj(Or(t1, t2))] = [0] 109.07/40.06 ? [4] 109.07/40.06 = [and(conj(t1), disj(t1))] 109.07/40.06 109.07/40.06 [disj(T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [disj(F())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(And(t1, t2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(Or(t1, t2))] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [True()] 109.07/40.06 109.07/40.06 [isOp(T())] = [0] 109.07/40.06 >= [0] 109.07/40.06 = [False()] 109.07/40.06 109.07/40.06 [isOp(F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.07 > [1] t1 + [0] 109.07/40.07 = [t1] 109.07/40.07 109.07/40.07 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [11] 109.07/40.07 > [1] t1 + [0] 109.07/40.07 = [t1] 109.07/40.07 109.07/40.07 [bool(And(a1, a2))] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [bool(Or(o1, o2))] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [bool(T())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [bool(F())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [and(True(), True())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [and(True(), False())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [and(False(), True())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [and(False(), False())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [4] 109.07/40.07 > [1] t1 + [0] 109.07/40.07 = [t1] 109.07/40.07 109.07/40.07 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [8] 109.07/40.07 > [1] t1 + [0] 109.07/40.07 = [t1] 109.07/40.07 109.07/40.07 [disjconj(p)] = [1] p + [7] 109.07/40.07 > [0] 109.07/40.07 = [disj(p)] 109.07/40.07 109.07/40.07 109.07/40.07 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.07 109.07/40.07 We are left with following problem, upon which TcT provides the 109.07/40.07 certificate MAYBE. 109.07/40.07 109.07/40.07 Strict Trs: 109.07/40.07 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.07 , conj(Or(o1, o2)) -> False() 109.07/40.07 , conj(T()) -> True() 109.07/40.07 , conj(F()) -> True() 109.07/40.07 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.07 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.07 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.07 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.07 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.07 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.07 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.07 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.07 , isConsTerm(T(), T()) -> True() 109.07/40.07 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.07 , isOp(And(t1, t2)) -> True() 109.07/40.07 , isOp(Or(t1, t2)) -> True() 109.07/40.07 , isOp(T()) -> False() } 109.07/40.07 Weak Trs: 109.07/40.07 { isAnd(And(t1, t2)) -> True() 109.07/40.07 , isAnd(Or(t1, t2)) -> False() 109.07/40.07 , isAnd(T()) -> False() 109.07/40.07 , isAnd(F()) -> False() 109.07/40.07 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.07 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.07 , isConsTerm(T(), F()) -> False() 109.07/40.07 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.07 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.07 , isConsTerm(F(), T()) -> False() 109.07/40.07 , isConsTerm(F(), F()) -> True() 109.07/40.07 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.07 , disj(T()) -> True() 109.07/40.07 , disj(F()) -> True() 109.07/40.07 , isOp(F()) -> False() 109.07/40.07 , getFirst(And(t1, t2)) -> t1 109.07/40.07 , getFirst(Or(t1, t2)) -> t1 109.07/40.07 , bool(And(a1, a2)) -> False() 109.07/40.07 , bool(Or(o1, o2)) -> False() 109.07/40.07 , bool(T()) -> True() 109.07/40.07 , bool(F()) -> True() 109.07/40.07 , and(True(), True()) -> True() 109.07/40.07 , and(True(), False()) -> False() 109.07/40.07 , and(False(), True()) -> False() 109.07/40.07 , and(False(), False()) -> False() 109.07/40.07 , getSecond(And(t1, t2)) -> t1 109.07/40.07 , getSecond(Or(t1, t2)) -> t1 109.07/40.07 , disjconj(p) -> disj(p) } 109.07/40.07 Obligation: 109.07/40.07 innermost runtime complexity 109.07/40.07 Answer: 109.07/40.07 MAYBE 109.07/40.07 109.07/40.07 The weightgap principle applies (using the following nonconstant 109.07/40.07 growth matrix-interpretation) 109.07/40.07 109.07/40.07 The following argument positions are usable: 109.07/40.07 Uargs(and) = {1, 2} 109.07/40.07 109.07/40.07 TcT has computed the following matrix interpretation satisfying 109.07/40.07 not(EDA) and not(IDA(1)). 109.07/40.07 109.07/40.07 [conj](x1) = [0] 109.07/40.07 109.07/40.07 [And](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.07 109.07/40.07 [isAnd](x1) = [4] 109.07/40.07 109.07/40.07 [isConsTerm](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.07 109.07/40.07 [True] = [0] 109.07/40.07 109.07/40.07 [disj](x1) = [0] 109.07/40.07 109.07/40.07 [Or](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.07 109.07/40.07 [isOp](x1) = [0] 109.07/40.07 109.07/40.07 [getFirst](x1) = [1] x1 + [3] 109.07/40.07 109.07/40.07 [bool](x1) = [4] 109.07/40.07 109.07/40.07 [and](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.07 109.07/40.07 [getSecond](x1) = [1] x1 + [3] 109.07/40.07 109.07/40.07 [T] = [0] 109.07/40.07 109.07/40.07 [disjconj](x1) = [1] x1 + [7] 109.07/40.07 109.07/40.07 [F] = [0] 109.07/40.07 109.07/40.07 [False] = [0] 109.07/40.07 109.07/40.07 The order satisfies the following ordering constraints: 109.07/40.07 109.07/40.07 [conj(And(t1, t2))] = [0] 109.07/40.07 ? [4] 109.07/40.07 = [and(disj(t1), conj(t1))] 109.07/40.07 109.07/40.07 [conj(Or(o1, o2))] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [conj(T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [conj(F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isAnd(And(t1, t2))] = [4] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isAnd(Or(t1, t2))] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isAnd(T())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isAnd(F())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(And(a1, a2), And(y1, y2))] = [1] a1 + [1] a2 + [1] y1 + [1] y2 + [8] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isConsTerm(And(a1, a2), Or(x1, x2))] = [1] a1 + [1] a2 + [1] x1 + [1] x2 + [8] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(And(a1, a2), T())] = [1] a1 + [1] a2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(And(a1, a2), F())] = [1] a1 + [1] a2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(Or(o1, o2), And(y1, y2))] = [1] o1 + [1] o2 + [1] y1 + [1] y2 + [8] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [1] o1 + [1] o2 + [1] x1 + [1] x2 + [8] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isConsTerm(Or(o1, o2), T())] = [1] o1 + [1] o2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(Or(o1, o2), F())] = [1] o1 + [1] o2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(T(), And(y1, y2))] = [1] y1 + [1] y2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(T(), Or(x1, x2))] = [1] x1 + [1] x2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(T(), T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isConsTerm(T(), F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(F(), And(y1, y2))] = [1] y1 + [1] y2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(F(), Or(x1, x2))] = [1] x1 + [1] x2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(F(), T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(F(), F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [disj(And(a1, a2))] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [conj(And(a1, a2))] 109.07/40.07 109.07/40.07 [disj(Or(t1, t2))] = [0] 109.07/40.07 ? [4] 109.07/40.07 = [and(conj(t1), disj(t1))] 109.07/40.07 109.07/40.07 [disj(T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [disj(F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isOp(And(t1, t2))] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isOp(Or(t1, t2))] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isOp(T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isOp(F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.07 > [1] t1 + [0] 109.07/40.07 = [t1] 109.07/40.07 109.07/40.07 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.07 > [1] t1 + [0] 109.07/40.07 = [t1] 109.07/40.07 109.07/40.07 [bool(And(a1, a2))] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [bool(Or(o1, o2))] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [bool(T())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [bool(F())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [and(True(), True())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [and(True(), False())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [and(False(), True())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [and(False(), False())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.07 > [1] t1 + [0] 109.07/40.07 = [t1] 109.07/40.07 109.07/40.07 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.07 > [1] t1 + [0] 109.07/40.07 = [t1] 109.07/40.07 109.07/40.07 [disjconj(p)] = [1] p + [7] 109.07/40.07 > [0] 109.07/40.07 = [disj(p)] 109.07/40.07 109.07/40.07 109.07/40.07 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.07 109.07/40.07 We are left with following problem, upon which TcT provides the 109.07/40.07 certificate MAYBE. 109.07/40.07 109.07/40.07 Strict Trs: 109.07/40.07 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.07 , conj(Or(o1, o2)) -> False() 109.07/40.07 , conj(T()) -> True() 109.07/40.07 , conj(F()) -> True() 109.07/40.07 , isConsTerm(T(), T()) -> True() 109.07/40.07 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.07 , isOp(And(t1, t2)) -> True() 109.07/40.07 , isOp(Or(t1, t2)) -> True() 109.07/40.07 , isOp(T()) -> False() } 109.07/40.07 Weak Trs: 109.07/40.07 { isAnd(And(t1, t2)) -> True() 109.07/40.07 , isAnd(Or(t1, t2)) -> False() 109.07/40.07 , isAnd(T()) -> False() 109.07/40.07 , isAnd(F()) -> False() 109.07/40.07 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.07 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.07 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.07 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.07 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.07 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.07 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.07 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.07 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.07 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.07 , isConsTerm(T(), F()) -> False() 109.07/40.07 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.07 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.07 , isConsTerm(F(), T()) -> False() 109.07/40.07 , isConsTerm(F(), F()) -> True() 109.07/40.07 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.07 , disj(T()) -> True() 109.07/40.07 , disj(F()) -> True() 109.07/40.07 , isOp(F()) -> False() 109.07/40.07 , getFirst(And(t1, t2)) -> t1 109.07/40.07 , getFirst(Or(t1, t2)) -> t1 109.07/40.07 , bool(And(a1, a2)) -> False() 109.07/40.07 , bool(Or(o1, o2)) -> False() 109.07/40.07 , bool(T()) -> True() 109.07/40.07 , bool(F()) -> True() 109.07/40.07 , and(True(), True()) -> True() 109.07/40.07 , and(True(), False()) -> False() 109.07/40.07 , and(False(), True()) -> False() 109.07/40.07 , and(False(), False()) -> False() 109.07/40.07 , getSecond(And(t1, t2)) -> t1 109.07/40.07 , getSecond(Or(t1, t2)) -> t1 109.07/40.07 , disjconj(p) -> disj(p) } 109.07/40.07 Obligation: 109.07/40.07 innermost runtime complexity 109.07/40.07 Answer: 109.07/40.07 MAYBE 109.07/40.07 109.07/40.07 The weightgap principle applies (using the following nonconstant 109.07/40.07 growth matrix-interpretation) 109.07/40.07 109.07/40.07 The following argument positions are usable: 109.07/40.07 Uargs(and) = {1, 2} 109.07/40.07 109.07/40.07 TcT has computed the following matrix interpretation satisfying 109.07/40.07 not(EDA) and not(IDA(1)). 109.07/40.07 109.07/40.07 [conj](x1) = [0] 109.07/40.07 109.07/40.07 [And](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.07 109.07/40.07 [isAnd](x1) = [4] 109.07/40.07 109.07/40.07 [isConsTerm](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.07 109.07/40.07 [True] = [0] 109.07/40.07 109.07/40.07 [disj](x1) = [0] 109.07/40.07 109.07/40.07 [Or](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.07 109.07/40.07 [isOp](x1) = [1] x1 + [0] 109.07/40.07 109.07/40.07 [getFirst](x1) = [1] x1 + [3] 109.07/40.07 109.07/40.07 [bool](x1) = [4] 109.07/40.07 109.07/40.07 [and](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.07 109.07/40.07 [getSecond](x1) = [1] x1 + [3] 109.07/40.07 109.07/40.07 [T] = [0] 109.07/40.07 109.07/40.07 [disjconj](x1) = [1] x1 + [7] 109.07/40.07 109.07/40.07 [F] = [0] 109.07/40.07 109.07/40.07 [False] = [0] 109.07/40.07 109.07/40.07 The order satisfies the following ordering constraints: 109.07/40.07 109.07/40.07 [conj(And(t1, t2))] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [and(disj(t1), conj(t1))] 109.07/40.07 109.07/40.07 [conj(Or(o1, o2))] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [conj(T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [conj(F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isAnd(And(t1, t2))] = [4] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isAnd(Or(t1, t2))] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isAnd(T())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isAnd(F())] = [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(And(a1, a2), And(y1, y2))] = [1] a1 + [1] a2 + [1] y1 + [1] y2 + [8] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isConsTerm(And(a1, a2), Or(x1, x2))] = [1] a1 + [1] a2 + [1] x1 + [1] x2 + [8] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(And(a1, a2), T())] = [1] a1 + [1] a2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(And(a1, a2), F())] = [1] a1 + [1] a2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(Or(o1, o2), And(y1, y2))] = [1] o1 + [1] o2 + [1] y1 + [1] y2 + [8] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [1] o1 + [1] o2 + [1] x1 + [1] x2 + [8] 109.07/40.07 > [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isConsTerm(Or(o1, o2), T())] = [1] o1 + [1] o2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(Or(o1, o2), F())] = [1] o1 + [1] o2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(T(), And(y1, y2))] = [1] y1 + [1] y2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(T(), Or(x1, x2))] = [1] x1 + [1] x2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(T(), T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [isConsTerm(T(), F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(F(), And(y1, y2))] = [1] y1 + [1] y2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(F(), Or(x1, x2))] = [1] x1 + [1] x2 + [4] 109.07/40.07 > [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(F(), T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [False()] 109.07/40.07 109.07/40.07 [isConsTerm(F(), F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [disj(And(a1, a2))] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [conj(And(a1, a2))] 109.07/40.07 109.07/40.07 [disj(Or(t1, t2))] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [and(conj(t1), disj(t1))] 109.07/40.07 109.07/40.07 [disj(T())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.07 109.07/40.07 [disj(F())] = [0] 109.07/40.07 >= [0] 109.07/40.07 = [True()] 109.07/40.08 109.07/40.08 [isOp(And(t1, t2))] = [1] t1 + [1] t2 + [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isOp(Or(t1, t2))] = [1] t1 + [1] t2 + [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isOp(T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isOp(F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [bool(And(a1, a2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [bool(Or(o1, o2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [bool(T())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [bool(F())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [and(True(), True())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [and(True(), False())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [and(False(), True())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [and(False(), False())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [disjconj(p)] = [1] p + [7] 109.07/40.08 > [0] 109.07/40.08 = [disj(p)] 109.07/40.08 109.07/40.08 109.07/40.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.08 109.07/40.08 We are left with following problem, upon which TcT provides the 109.07/40.08 certificate MAYBE. 109.07/40.08 109.07/40.08 Strict Trs: 109.07/40.08 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.08 , conj(Or(o1, o2)) -> False() 109.07/40.08 , conj(T()) -> True() 109.07/40.08 , conj(F()) -> True() 109.07/40.08 , isConsTerm(T(), T()) -> True() 109.07/40.08 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) 109.07/40.08 , isOp(T()) -> False() } 109.07/40.08 Weak Trs: 109.07/40.08 { isAnd(And(t1, t2)) -> True() 109.07/40.08 , isAnd(Or(t1, t2)) -> False() 109.07/40.08 , isAnd(T()) -> False() 109.07/40.08 , isAnd(F()) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.08 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.08 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.08 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(T(), F()) -> False() 109.07/40.08 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(F(), T()) -> False() 109.07/40.08 , isConsTerm(F(), F()) -> True() 109.07/40.08 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.08 , disj(T()) -> True() 109.07/40.08 , disj(F()) -> True() 109.07/40.08 , isOp(And(t1, t2)) -> True() 109.07/40.08 , isOp(Or(t1, t2)) -> True() 109.07/40.08 , isOp(F()) -> False() 109.07/40.08 , getFirst(And(t1, t2)) -> t1 109.07/40.08 , getFirst(Or(t1, t2)) -> t1 109.07/40.08 , bool(And(a1, a2)) -> False() 109.07/40.08 , bool(Or(o1, o2)) -> False() 109.07/40.08 , bool(T()) -> True() 109.07/40.08 , bool(F()) -> True() 109.07/40.08 , and(True(), True()) -> True() 109.07/40.08 , and(True(), False()) -> False() 109.07/40.08 , and(False(), True()) -> False() 109.07/40.08 , and(False(), False()) -> False() 109.07/40.08 , getSecond(And(t1, t2)) -> t1 109.07/40.08 , getSecond(Or(t1, t2)) -> t1 109.07/40.08 , disjconj(p) -> disj(p) } 109.07/40.08 Obligation: 109.07/40.08 innermost runtime complexity 109.07/40.08 Answer: 109.07/40.08 MAYBE 109.07/40.08 109.07/40.08 The weightgap principle applies (using the following nonconstant 109.07/40.08 growth matrix-interpretation) 109.07/40.08 109.07/40.08 The following argument positions are usable: 109.07/40.08 Uargs(and) = {1, 2} 109.07/40.08 109.07/40.08 TcT has computed the following matrix interpretation satisfying 109.07/40.08 not(EDA) and not(IDA(1)). 109.07/40.08 109.07/40.08 [conj](x1) = [0] 109.07/40.08 109.07/40.08 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.08 109.07/40.08 [isAnd](x1) = [4] 109.07/40.08 109.07/40.08 [isConsTerm](x1, x2) = [0] 109.07/40.08 109.07/40.08 [True] = [0] 109.07/40.08 109.07/40.08 [disj](x1) = [0] 109.07/40.08 109.07/40.08 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.08 109.07/40.08 [isOp](x1) = [1] x1 + [0] 109.07/40.08 109.07/40.08 [getFirst](x1) = [1] x1 + [7] 109.07/40.08 109.07/40.08 [bool](x1) = [4] 109.07/40.08 109.07/40.08 [and](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.08 109.07/40.08 [getSecond](x1) = [1] x1 + [7] 109.07/40.08 109.07/40.08 [T] = [4] 109.07/40.08 109.07/40.08 [disjconj](x1) = [1] x1 + [7] 109.07/40.08 109.07/40.08 [F] = [0] 109.07/40.08 109.07/40.08 [False] = [0] 109.07/40.08 109.07/40.08 The order satisfies the following ordering constraints: 109.07/40.08 109.07/40.08 [conj(And(t1, t2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [and(disj(t1), conj(t1))] 109.07/40.08 109.07/40.08 [conj(Or(o1, o2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [conj(T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [conj(F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isAnd(And(t1, t2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isAnd(Or(t1, t2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isAnd(T())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isAnd(F())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(And(a1, a2), And(y1, y2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isConsTerm(And(a1, a2), Or(x1, x2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(And(a1, a2), T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(And(a1, a2), F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(Or(o1, o2), And(y1, y2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isConsTerm(Or(o1, o2), T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(Or(o1, o2), F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(T(), And(y1, y2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(T(), Or(x1, x2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(T(), T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isConsTerm(T(), F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(F(), And(y1, y2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(F(), Or(x1, x2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(F(), T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(F(), F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [disj(And(a1, a2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [conj(And(a1, a2))] 109.07/40.08 109.07/40.08 [disj(Or(t1, t2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [and(conj(t1), disj(t1))] 109.07/40.08 109.07/40.08 [disj(T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [disj(F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isOp(And(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isOp(Or(t1, t2))] = [1] t1 + [1] t2 + [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isOp(T())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isOp(F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [bool(And(a1, a2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [bool(Or(o1, o2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [bool(T())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [bool(F())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [and(True(), True())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [and(True(), False())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [and(False(), True())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [and(False(), False())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [disjconj(p)] = [1] p + [7] 109.07/40.08 > [0] 109.07/40.08 = [disj(p)] 109.07/40.08 109.07/40.08 109.07/40.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.08 109.07/40.08 We are left with following problem, upon which TcT provides the 109.07/40.08 certificate MAYBE. 109.07/40.08 109.07/40.08 Strict Trs: 109.07/40.08 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.08 , conj(Or(o1, o2)) -> False() 109.07/40.08 , conj(T()) -> True() 109.07/40.08 , conj(F()) -> True() 109.07/40.08 , isConsTerm(T(), T()) -> True() 109.07/40.08 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) } 109.07/40.08 Weak Trs: 109.07/40.08 { isAnd(And(t1, t2)) -> True() 109.07/40.08 , isAnd(Or(t1, t2)) -> False() 109.07/40.08 , isAnd(T()) -> False() 109.07/40.08 , isAnd(F()) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.08 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.08 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.08 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(T(), F()) -> False() 109.07/40.08 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(F(), T()) -> False() 109.07/40.08 , isConsTerm(F(), F()) -> True() 109.07/40.08 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.08 , disj(T()) -> True() 109.07/40.08 , disj(F()) -> True() 109.07/40.08 , isOp(And(t1, t2)) -> True() 109.07/40.08 , isOp(Or(t1, t2)) -> True() 109.07/40.08 , isOp(T()) -> False() 109.07/40.08 , isOp(F()) -> False() 109.07/40.08 , getFirst(And(t1, t2)) -> t1 109.07/40.08 , getFirst(Or(t1, t2)) -> t1 109.07/40.08 , bool(And(a1, a2)) -> False() 109.07/40.08 , bool(Or(o1, o2)) -> False() 109.07/40.08 , bool(T()) -> True() 109.07/40.08 , bool(F()) -> True() 109.07/40.08 , and(True(), True()) -> True() 109.07/40.08 , and(True(), False()) -> False() 109.07/40.08 , and(False(), True()) -> False() 109.07/40.08 , and(False(), False()) -> False() 109.07/40.08 , getSecond(And(t1, t2)) -> t1 109.07/40.08 , getSecond(Or(t1, t2)) -> t1 109.07/40.08 , disjconj(p) -> disj(p) } 109.07/40.08 Obligation: 109.07/40.08 innermost runtime complexity 109.07/40.08 Answer: 109.07/40.08 MAYBE 109.07/40.08 109.07/40.08 The weightgap principle applies (using the following nonconstant 109.07/40.08 growth matrix-interpretation) 109.07/40.08 109.07/40.08 The following argument positions are usable: 109.07/40.08 Uargs(and) = {1, 2} 109.07/40.08 109.07/40.08 TcT has computed the following matrix interpretation satisfying 109.07/40.08 not(EDA) and not(IDA(1)). 109.07/40.08 109.07/40.08 [conj](x1) = [0] 109.07/40.08 109.07/40.08 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.08 109.07/40.08 [isAnd](x1) = [4] 109.07/40.08 109.07/40.08 [isConsTerm](x1, x2) = [1] 109.07/40.08 109.07/40.08 [True] = [0] 109.07/40.08 109.07/40.08 [disj](x1) = [0] 109.07/40.08 109.07/40.08 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.08 109.07/40.08 [isOp](x1) = [4] 109.07/40.08 109.07/40.08 [getFirst](x1) = [1] x1 + [7] 109.07/40.08 109.07/40.08 [bool](x1) = [4] 109.07/40.08 109.07/40.08 [and](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.08 109.07/40.08 [getSecond](x1) = [1] x1 + [7] 109.07/40.08 109.07/40.08 [T] = [0] 109.07/40.08 109.07/40.08 [disjconj](x1) = [1] x1 + [7] 109.07/40.08 109.07/40.08 [F] = [0] 109.07/40.08 109.07/40.08 [False] = [0] 109.07/40.08 109.07/40.08 The order satisfies the following ordering constraints: 109.07/40.08 109.07/40.08 [conj(And(t1, t2))] = [0] 109.07/40.08 ? [4] 109.07/40.08 = [and(disj(t1), conj(t1))] 109.07/40.08 109.07/40.08 [conj(Or(o1, o2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [conj(T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [conj(F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isAnd(And(t1, t2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isAnd(Or(t1, t2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isAnd(T())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isAnd(F())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(And(a1, a2), And(y1, y2))] = [1] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isConsTerm(And(a1, a2), Or(x1, x2))] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(And(a1, a2), T())] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(And(a1, a2), F())] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(Or(o1, o2), And(y1, y2))] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [1] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isConsTerm(Or(o1, o2), T())] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(Or(o1, o2), F())] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(T(), And(y1, y2))] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(T(), Or(x1, x2))] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(T(), T())] = [1] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isConsTerm(T(), F())] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(F(), And(y1, y2))] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(F(), Or(x1, x2))] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(F(), T())] = [1] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isConsTerm(F(), F())] = [1] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [disj(And(a1, a2))] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [conj(And(a1, a2))] 109.07/40.08 109.07/40.08 [disj(Or(t1, t2))] = [0] 109.07/40.08 ? [4] 109.07/40.08 = [and(conj(t1), disj(t1))] 109.07/40.08 109.07/40.08 [disj(T())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [disj(F())] = [0] 109.07/40.08 >= [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isOp(And(t1, t2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isOp(Or(t1, t2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [isOp(T())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [isOp(F())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [bool(And(a1, a2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [bool(Or(o1, o2))] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [bool(T())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [bool(F())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [and(True(), True())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [True()] 109.07/40.08 109.07/40.08 [and(True(), False())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [and(False(), True())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [and(False(), False())] = [4] 109.07/40.08 > [0] 109.07/40.08 = [False()] 109.07/40.08 109.07/40.08 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.08 > [1] t1 + [0] 109.07/40.08 = [t1] 109.07/40.08 109.07/40.08 [disjconj(p)] = [1] p + [7] 109.07/40.08 > [0] 109.07/40.08 = [disj(p)] 109.07/40.08 109.07/40.08 109.07/40.08 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.08 109.07/40.08 We are left with following problem, upon which TcT provides the 109.07/40.08 certificate MAYBE. 109.07/40.08 109.07/40.08 Strict Trs: 109.07/40.08 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.08 , conj(Or(o1, o2)) -> False() 109.07/40.08 , conj(T()) -> True() 109.07/40.08 , conj(F()) -> True() 109.07/40.08 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) } 109.07/40.08 Weak Trs: 109.07/40.08 { isAnd(And(t1, t2)) -> True() 109.07/40.08 , isAnd(Or(t1, t2)) -> False() 109.07/40.08 , isAnd(T()) -> False() 109.07/40.08 , isAnd(F()) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.08 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.08 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.08 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.08 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.08 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(T(), T()) -> True() 109.07/40.08 , isConsTerm(T(), F()) -> False() 109.07/40.08 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.08 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.08 , isConsTerm(F(), T()) -> False() 109.07/40.08 , isConsTerm(F(), F()) -> True() 109.07/40.08 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.08 , disj(T()) -> True() 109.07/40.08 , disj(F()) -> True() 109.07/40.08 , isOp(And(t1, t2)) -> True() 109.07/40.09 , isOp(Or(t1, t2)) -> True() 109.07/40.09 , isOp(T()) -> False() 109.07/40.09 , isOp(F()) -> False() 109.07/40.09 , getFirst(And(t1, t2)) -> t1 109.07/40.09 , getFirst(Or(t1, t2)) -> t1 109.07/40.09 , bool(And(a1, a2)) -> False() 109.07/40.09 , bool(Or(o1, o2)) -> False() 109.07/40.09 , bool(T()) -> True() 109.07/40.09 , bool(F()) -> True() 109.07/40.09 , and(True(), True()) -> True() 109.07/40.09 , and(True(), False()) -> False() 109.07/40.09 , and(False(), True()) -> False() 109.07/40.09 , and(False(), False()) -> False() 109.07/40.09 , getSecond(And(t1, t2)) -> t1 109.07/40.09 , getSecond(Or(t1, t2)) -> t1 109.07/40.09 , disjconj(p) -> disj(p) } 109.07/40.09 Obligation: 109.07/40.09 innermost runtime complexity 109.07/40.09 Answer: 109.07/40.09 MAYBE 109.07/40.09 109.07/40.09 The weightgap principle applies (using the following nonconstant 109.07/40.09 growth matrix-interpretation) 109.07/40.09 109.07/40.09 The following argument positions are usable: 109.07/40.09 Uargs(and) = {1, 2} 109.07/40.09 109.07/40.09 TcT has computed the following matrix interpretation satisfying 109.07/40.09 not(EDA) and not(IDA(1)). 109.07/40.09 109.07/40.09 [conj](x1) = [4] 109.07/40.09 109.07/40.09 [And](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.09 109.07/40.09 [isAnd](x1) = [4] 109.07/40.09 109.07/40.09 [isConsTerm](x1, x2) = [4] 109.07/40.09 109.07/40.09 [True] = [0] 109.07/40.09 109.07/40.09 [disj](x1) = [4] 109.07/40.09 109.07/40.09 [Or](x1, x2) = [1] x1 + [1] x2 + [0] 109.07/40.09 109.07/40.09 [isOp](x1) = [4] 109.07/40.09 109.07/40.09 [getFirst](x1) = [1] x1 + [7] 109.07/40.09 109.07/40.09 [bool](x1) = [4] 109.07/40.09 109.07/40.09 [and](x1, x2) = [1] x1 + [1] x2 + [4] 109.07/40.09 109.07/40.09 [getSecond](x1) = [1] x1 + [7] 109.07/40.09 109.07/40.09 [T] = [0] 109.07/40.09 109.07/40.09 [disjconj](x1) = [1] x1 + [7] 109.07/40.09 109.07/40.09 [F] = [0] 109.07/40.09 109.07/40.09 [False] = [0] 109.07/40.09 109.07/40.09 The order satisfies the following ordering constraints: 109.07/40.09 109.07/40.09 [conj(And(t1, t2))] = [4] 109.07/40.09 ? [12] 109.07/40.09 = [and(disj(t1), conj(t1))] 109.07/40.09 109.07/40.09 [conj(Or(o1, o2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [conj(T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [conj(F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [isAnd(And(t1, t2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [isAnd(Or(t1, t2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isAnd(T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isAnd(F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(And(a1, a2), And(y1, y2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [isConsTerm(And(a1, a2), Or(x1, x2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(And(a1, a2), T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(And(a1, a2), F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(Or(o1, o2), And(y1, y2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(Or(o1, o2), Or(x1, x2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [isConsTerm(Or(o1, o2), T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(Or(o1, o2), F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(T(), And(y1, y2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(T(), Or(x1, x2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(T(), T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [isConsTerm(T(), F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(F(), And(y1, y2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(F(), Or(x1, x2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(F(), T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isConsTerm(F(), F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [disj(And(a1, a2))] = [4] 109.07/40.09 >= [4] 109.07/40.09 = [conj(And(a1, a2))] 109.07/40.09 109.07/40.09 [disj(Or(t1, t2))] = [4] 109.07/40.09 ? [12] 109.07/40.09 = [and(conj(t1), disj(t1))] 109.07/40.09 109.07/40.09 [disj(T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [disj(F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [isOp(And(t1, t2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [isOp(Or(t1, t2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [isOp(T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [isOp(F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [getFirst(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.09 > [1] t1 + [0] 109.07/40.09 = [t1] 109.07/40.09 109.07/40.09 [getFirst(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.09 > [1] t1 + [0] 109.07/40.09 = [t1] 109.07/40.09 109.07/40.09 [bool(And(a1, a2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [bool(Or(o1, o2))] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [bool(T())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [bool(F())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [and(True(), True())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [True()] 109.07/40.09 109.07/40.09 [and(True(), False())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [and(False(), True())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [and(False(), False())] = [4] 109.07/40.09 > [0] 109.07/40.09 = [False()] 109.07/40.09 109.07/40.09 [getSecond(And(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.09 > [1] t1 + [0] 109.07/40.09 = [t1] 109.07/40.09 109.07/40.09 [getSecond(Or(t1, t2))] = [1] t1 + [1] t2 + [7] 109.07/40.09 > [1] t1 + [0] 109.07/40.09 = [t1] 109.07/40.09 109.07/40.09 [disjconj(p)] = [1] p + [7] 109.07/40.09 > [4] 109.07/40.09 = [disj(p)] 109.07/40.09 109.07/40.09 109.07/40.09 Further, it can be verified that all rules not oriented are covered by the weightgap condition. 109.07/40.09 109.07/40.09 We are left with following problem, upon which TcT provides the 109.07/40.09 certificate MAYBE. 109.07/40.09 109.07/40.09 Strict Trs: 109.07/40.09 { conj(And(t1, t2)) -> and(disj(t1), conj(t1)) 109.07/40.09 , disj(Or(t1, t2)) -> and(conj(t1), disj(t1)) } 109.07/40.09 Weak Trs: 109.07/40.09 { conj(Or(o1, o2)) -> False() 109.07/40.09 , conj(T()) -> True() 109.07/40.09 , conj(F()) -> True() 109.07/40.09 , isAnd(And(t1, t2)) -> True() 109.07/40.09 , isAnd(Or(t1, t2)) -> False() 109.07/40.09 , isAnd(T()) -> False() 109.07/40.09 , isAnd(F()) -> False() 109.07/40.09 , isConsTerm(And(a1, a2), And(y1, y2)) -> True() 109.07/40.09 , isConsTerm(And(a1, a2), Or(x1, x2)) -> False() 109.07/40.09 , isConsTerm(And(a1, a2), T()) -> False() 109.07/40.09 , isConsTerm(And(a1, a2), F()) -> False() 109.07/40.09 , isConsTerm(Or(o1, o2), And(y1, y2)) -> False() 109.07/40.09 , isConsTerm(Or(o1, o2), Or(x1, x2)) -> True() 109.07/40.09 , isConsTerm(Or(o1, o2), T()) -> False() 109.07/40.09 , isConsTerm(Or(o1, o2), F()) -> False() 109.07/40.09 , isConsTerm(T(), And(y1, y2)) -> False() 109.07/40.09 , isConsTerm(T(), Or(x1, x2)) -> False() 109.07/40.09 , isConsTerm(T(), T()) -> True() 109.07/40.09 , isConsTerm(T(), F()) -> False() 109.07/40.09 , isConsTerm(F(), And(y1, y2)) -> False() 109.07/40.09 , isConsTerm(F(), Or(x1, x2)) -> False() 109.07/40.09 , isConsTerm(F(), T()) -> False() 109.07/40.09 , isConsTerm(F(), F()) -> True() 109.07/40.09 , disj(And(a1, a2)) -> conj(And(a1, a2)) 109.07/40.09 , disj(T()) -> True() 109.07/40.09 , disj(F()) -> True() 109.07/40.09 , isOp(And(t1, t2)) -> True() 109.07/40.09 , isOp(Or(t1, t2)) -> True() 109.07/40.09 , isOp(T()) -> False() 109.07/40.09 , isOp(F()) -> False() 109.07/40.09 , getFirst(And(t1, t2)) -> t1 109.07/40.09 , getFirst(Or(t1, t2)) -> t1 109.07/40.09 , bool(And(a1, a2)) -> False() 109.07/40.09 , bool(Or(o1, o2)) -> False() 109.07/40.09 , bool(T()) -> True() 109.07/40.09 , bool(F()) -> True() 109.07/40.09 , and(True(), True()) -> True() 109.07/40.09 , and(True(), False()) -> False() 109.07/40.09 , and(False(), True()) -> False() 109.07/40.09 , and(False(), False()) -> False() 109.07/40.09 , getSecond(And(t1, t2)) -> t1 109.07/40.09 , getSecond(Or(t1, t2)) -> t1 109.07/40.09 , disjconj(p) -> disj(p) } 109.07/40.09 Obligation: 109.07/40.09 innermost runtime complexity 109.07/40.09 Answer: 109.07/40.09 MAYBE 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'empty' failed due to the following reason: 109.07/40.09 109.07/40.09 Empty strict component of the problem is NOT empty. 109.07/40.09 109.07/40.09 2) 'With Problem ...' failed due to the following reason: 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'empty' failed due to the following reason: 109.07/40.09 109.07/40.09 Empty strict component of the problem is NOT empty. 109.07/40.09 109.07/40.09 2) 'Fastest' failed due to the following reason: 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'With Problem ...' failed due to the following reason: 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'empty' failed due to the following reason: 109.07/40.09 109.07/40.09 Empty strict component of the problem is NOT empty. 109.07/40.09 109.07/40.09 2) 'With Problem ...' failed due to the following reason: 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'empty' failed due to the following reason: 109.07/40.09 109.07/40.09 Empty strict component of the problem is NOT empty. 109.07/40.09 109.07/40.09 2) 'With Problem ...' failed due to the following reason: 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'empty' failed due to the following reason: 109.07/40.09 109.07/40.09 Empty strict component of the problem is NOT empty. 109.07/40.09 109.07/40.09 2) 'With Problem ...' failed due to the following reason: 109.07/40.09 109.07/40.09 Empty strict component of the problem is NOT empty. 109.07/40.09 109.07/40.09 109.07/40.09 109.07/40.09 109.07/40.09 2) 'With Problem ...' failed due to the following reason: 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'empty' failed due to the following reason: 109.07/40.09 109.07/40.09 Empty strict component of the problem is NOT empty. 109.07/40.09 109.07/40.09 2) 'With Problem ...' failed due to the following reason: 109.07/40.09 109.07/40.09 Empty strict component of the problem is NOT empty. 109.07/40.09 109.07/40.09 109.07/40.09 109.07/40.09 109.07/40.09 109.07/40.09 2) 'Best' failed due to the following reason: 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 109.07/40.09 following reason: 109.07/40.09 109.07/40.09 The input cannot be shown compatible 109.07/40.09 109.07/40.09 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 109.07/40.09 to the following reason: 109.07/40.09 109.07/40.09 The input cannot be shown compatible 109.07/40.09 109.07/40.09 109.07/40.09 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 109.07/40.09 failed due to the following reason: 109.07/40.09 109.07/40.09 None of the processors succeeded. 109.07/40.09 109.07/40.09 Details of failed attempt(s): 109.07/40.09 ----------------------------- 109.07/40.09 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 109.07/40.09 failed due to the following reason: 109.07/40.09 109.07/40.09 match-boundness of the problem could not be verified. 109.07/40.09 109.07/40.09 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 109.07/40.09 failed due to the following reason: 109.07/40.09 109.07/40.09 match-boundness of the problem could not be verified. 109.07/40.09 109.07/40.09 109.07/40.09 109.07/40.09 109.07/40.09 109.07/40.09 Arrrr.. 109.31/40.15 EOF