MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: bool(And(a1,a2)) -> False() bool(F()) -> True() bool(Or(o1,o2)) -> False() bool(T()) -> True() conj(And(t1,t2)) -> and(disj(t1),conj(t1)) conj(F()) -> True() conj(Or(o1,o2)) -> False() conj(T()) -> True() disj(And(a1,a2)) -> conj(And(a1,a2)) disj(F()) -> True() disj(Or(t1,t2)) -> and(conj(t1),disj(t1)) disj(T()) -> True() disjconj(p) -> disj(p) getFirst(And(t1,t2)) -> t1 getFirst(Or(t1,t2)) -> t1 getSecond(And(t1,t2)) -> t1 getSecond(Or(t1,t2)) -> t1 isAnd(And(t1,t2)) -> True() isAnd(F()) -> False() isAnd(Or(t1,t2)) -> False() isAnd(T()) -> False() isConsTerm(And(a1,a2),And(y1,y2)) -> True() isConsTerm(And(a1,a2),F()) -> False() isConsTerm(And(a1,a2),Or(x1,x2)) -> False() isConsTerm(And(a1,a2),T()) -> False() isConsTerm(F(),And(y1,y2)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(x1,x2)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(o1,o2),And(y1,y2)) -> False() isConsTerm(Or(o1,o2),F()) -> False() isConsTerm(Or(o1,o2),Or(x1,x2)) -> True() isConsTerm(Or(o1,o2),T()) -> False() isConsTerm(T(),And(y1,y2)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(x1,x2)) -> False() isConsTerm(T(),T()) -> True() isOp(And(t1,t2)) -> True() isOp(F()) -> False() isOp(Or(t1,t2)) -> True() isOp(T()) -> False() - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1} / {And/2,F/0 ,False/0,Or/2,T/0,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {and,bool,conj,disj,disjconj,getFirst,getSecond,isAnd ,isConsTerm,isOp} and constructors {And,F,False,Or,T,True} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs bool#(And(a1,a2)) -> c_1() bool#(F()) -> c_2() bool#(Or(o1,o2)) -> c_3() bool#(T()) -> c_4() conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) conj#(F()) -> c_6() conj#(Or(o1,o2)) -> c_7() conj#(T()) -> c_8() disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(F()) -> c_10() disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) disj#(T()) -> c_12() disjconj#(p) -> c_13(disj#(p)) getFirst#(And(t1,t2)) -> c_14() getFirst#(Or(t1,t2)) -> c_15() getSecond#(And(t1,t2)) -> c_16() getSecond#(Or(t1,t2)) -> c_17() isAnd#(And(t1,t2)) -> c_18() isAnd#(F()) -> c_19() isAnd#(Or(t1,t2)) -> c_20() isAnd#(T()) -> c_21() isConsTerm#(And(a1,a2),And(y1,y2)) -> c_22() isConsTerm#(And(a1,a2),F()) -> c_23() isConsTerm#(And(a1,a2),Or(x1,x2)) -> c_24() isConsTerm#(And(a1,a2),T()) -> c_25() isConsTerm#(F(),And(y1,y2)) -> c_26() isConsTerm#(F(),F()) -> c_27() isConsTerm#(F(),Or(x1,x2)) -> c_28() isConsTerm#(F(),T()) -> c_29() isConsTerm#(Or(o1,o2),And(y1,y2)) -> c_30() isConsTerm#(Or(o1,o2),F()) -> c_31() isConsTerm#(Or(o1,o2),Or(x1,x2)) -> c_32() isConsTerm#(Or(o1,o2),T()) -> c_33() isConsTerm#(T(),And(y1,y2)) -> c_34() isConsTerm#(T(),F()) -> c_35() isConsTerm#(T(),Or(x1,x2)) -> c_36() isConsTerm#(T(),T()) -> c_37() isOp#(And(t1,t2)) -> c_38() isOp#(F()) -> c_39() isOp#(Or(t1,t2)) -> c_40() isOp#(T()) -> c_41() Weak DPs and#(False(),False()) -> c_42() and#(False(),True()) -> c_43() and#(True(),False()) -> c_44() and#(True(),True()) -> c_45() and mark the set of starting terms. * Step 2: UsableRules MAYBE + Considered Problem: - Strict DPs: bool#(And(a1,a2)) -> c_1() bool#(F()) -> c_2() bool#(Or(o1,o2)) -> c_3() bool#(T()) -> c_4() conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) conj#(F()) -> c_6() conj#(Or(o1,o2)) -> c_7() conj#(T()) -> c_8() disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(F()) -> c_10() disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) disj#(T()) -> c_12() disjconj#(p) -> c_13(disj#(p)) getFirst#(And(t1,t2)) -> c_14() getFirst#(Or(t1,t2)) -> c_15() getSecond#(And(t1,t2)) -> c_16() getSecond#(Or(t1,t2)) -> c_17() isAnd#(And(t1,t2)) -> c_18() isAnd#(F()) -> c_19() isAnd#(Or(t1,t2)) -> c_20() isAnd#(T()) -> c_21() isConsTerm#(And(a1,a2),And(y1,y2)) -> c_22() isConsTerm#(And(a1,a2),F()) -> c_23() isConsTerm#(And(a1,a2),Or(x1,x2)) -> c_24() isConsTerm#(And(a1,a2),T()) -> c_25() isConsTerm#(F(),And(y1,y2)) -> c_26() isConsTerm#(F(),F()) -> c_27() isConsTerm#(F(),Or(x1,x2)) -> c_28() isConsTerm#(F(),T()) -> c_29() isConsTerm#(Or(o1,o2),And(y1,y2)) -> c_30() isConsTerm#(Or(o1,o2),F()) -> c_31() isConsTerm#(Or(o1,o2),Or(x1,x2)) -> c_32() isConsTerm#(Or(o1,o2),T()) -> c_33() isConsTerm#(T(),And(y1,y2)) -> c_34() isConsTerm#(T(),F()) -> c_35() isConsTerm#(T(),Or(x1,x2)) -> c_36() isConsTerm#(T(),T()) -> c_37() isOp#(And(t1,t2)) -> c_38() isOp#(F()) -> c_39() isOp#(Or(t1,t2)) -> c_40() isOp#(T()) -> c_41() - Weak DPs: and#(False(),False()) -> c_42() and#(False(),True()) -> c_43() and#(True(),False()) -> c_44() and#(True(),True()) -> c_45() - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(a1,a2)) -> False() bool(F()) -> True() bool(Or(o1,o2)) -> False() bool(T()) -> True() conj(And(t1,t2)) -> and(disj(t1),conj(t1)) conj(F()) -> True() conj(Or(o1,o2)) -> False() conj(T()) -> True() disj(And(a1,a2)) -> conj(And(a1,a2)) disj(F()) -> True() disj(Or(t1,t2)) -> and(conj(t1),disj(t1)) disj(T()) -> True() disjconj(p) -> disj(p) getFirst(And(t1,t2)) -> t1 getFirst(Or(t1,t2)) -> t1 getSecond(And(t1,t2)) -> t1 getSecond(Or(t1,t2)) -> t1 isAnd(And(t1,t2)) -> True() isAnd(F()) -> False() isAnd(Or(t1,t2)) -> False() isAnd(T()) -> False() isConsTerm(And(a1,a2),And(y1,y2)) -> True() isConsTerm(And(a1,a2),F()) -> False() isConsTerm(And(a1,a2),Or(x1,x2)) -> False() isConsTerm(And(a1,a2),T()) -> False() isConsTerm(F(),And(y1,y2)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(x1,x2)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(o1,o2),And(y1,y2)) -> False() isConsTerm(Or(o1,o2),F()) -> False() isConsTerm(Or(o1,o2),Or(x1,x2)) -> True() isConsTerm(Or(o1,o2),T()) -> False() isConsTerm(T(),And(y1,y2)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(x1,x2)) -> False() isConsTerm(T(),T()) -> True() isOp(And(t1,t2)) -> True() isOp(F()) -> False() isOp(Or(t1,t2)) -> True() isOp(T()) -> False() - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1,and#/2,bool#/1 ,conj#/1,disj#/1,disjconj#/1,getFirst#/1,getSecond#/1,isAnd#/1,isConsTerm#/2,isOp#/1} / {And/2,F/0,False/0 ,Or/2,T/0,True/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/3,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/3,c_12/0,c_13/1,c_14/0 ,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0 ,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0 ,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond# ,isAnd#,isConsTerm#,isOp#} and constructors {And,F,False,Or,T,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() conj(And(t1,t2)) -> and(disj(t1),conj(t1)) conj(F()) -> True() conj(Or(o1,o2)) -> False() conj(T()) -> True() disj(And(a1,a2)) -> conj(And(a1,a2)) disj(F()) -> True() disj(Or(t1,t2)) -> and(conj(t1),disj(t1)) disj(T()) -> True() and#(False(),False()) -> c_42() and#(False(),True()) -> c_43() and#(True(),False()) -> c_44() and#(True(),True()) -> c_45() bool#(And(a1,a2)) -> c_1() bool#(F()) -> c_2() bool#(Or(o1,o2)) -> c_3() bool#(T()) -> c_4() conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) conj#(F()) -> c_6() conj#(Or(o1,o2)) -> c_7() conj#(T()) -> c_8() disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(F()) -> c_10() disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) disj#(T()) -> c_12() disjconj#(p) -> c_13(disj#(p)) getFirst#(And(t1,t2)) -> c_14() getFirst#(Or(t1,t2)) -> c_15() getSecond#(And(t1,t2)) -> c_16() getSecond#(Or(t1,t2)) -> c_17() isAnd#(And(t1,t2)) -> c_18() isAnd#(F()) -> c_19() isAnd#(Or(t1,t2)) -> c_20() isAnd#(T()) -> c_21() isConsTerm#(And(a1,a2),And(y1,y2)) -> c_22() isConsTerm#(And(a1,a2),F()) -> c_23() isConsTerm#(And(a1,a2),Or(x1,x2)) -> c_24() isConsTerm#(And(a1,a2),T()) -> c_25() isConsTerm#(F(),And(y1,y2)) -> c_26() isConsTerm#(F(),F()) -> c_27() isConsTerm#(F(),Or(x1,x2)) -> c_28() isConsTerm#(F(),T()) -> c_29() isConsTerm#(Or(o1,o2),And(y1,y2)) -> c_30() isConsTerm#(Or(o1,o2),F()) -> c_31() isConsTerm#(Or(o1,o2),Or(x1,x2)) -> c_32() isConsTerm#(Or(o1,o2),T()) -> c_33() isConsTerm#(T(),And(y1,y2)) -> c_34() isConsTerm#(T(),F()) -> c_35() isConsTerm#(T(),Or(x1,x2)) -> c_36() isConsTerm#(T(),T()) -> c_37() isOp#(And(t1,t2)) -> c_38() isOp#(F()) -> c_39() isOp#(Or(t1,t2)) -> c_40() isOp#(T()) -> c_41() * Step 3: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: bool#(And(a1,a2)) -> c_1() bool#(F()) -> c_2() bool#(Or(o1,o2)) -> c_3() bool#(T()) -> c_4() conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) conj#(F()) -> c_6() conj#(Or(o1,o2)) -> c_7() conj#(T()) -> c_8() disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(F()) -> c_10() disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) disj#(T()) -> c_12() disjconj#(p) -> c_13(disj#(p)) getFirst#(And(t1,t2)) -> c_14() getFirst#(Or(t1,t2)) -> c_15() getSecond#(And(t1,t2)) -> c_16() getSecond#(Or(t1,t2)) -> c_17() isAnd#(And(t1,t2)) -> c_18() isAnd#(F()) -> c_19() isAnd#(Or(t1,t2)) -> c_20() isAnd#(T()) -> c_21() isConsTerm#(And(a1,a2),And(y1,y2)) -> c_22() isConsTerm#(And(a1,a2),F()) -> c_23() isConsTerm#(And(a1,a2),Or(x1,x2)) -> c_24() isConsTerm#(And(a1,a2),T()) -> c_25() isConsTerm#(F(),And(y1,y2)) -> c_26() isConsTerm#(F(),F()) -> c_27() isConsTerm#(F(),Or(x1,x2)) -> c_28() isConsTerm#(F(),T()) -> c_29() isConsTerm#(Or(o1,o2),And(y1,y2)) -> c_30() isConsTerm#(Or(o1,o2),F()) -> c_31() isConsTerm#(Or(o1,o2),Or(x1,x2)) -> c_32() isConsTerm#(Or(o1,o2),T()) -> c_33() isConsTerm#(T(),And(y1,y2)) -> c_34() isConsTerm#(T(),F()) -> c_35() isConsTerm#(T(),Or(x1,x2)) -> c_36() isConsTerm#(T(),T()) -> c_37() isOp#(And(t1,t2)) -> c_38() isOp#(F()) -> c_39() isOp#(Or(t1,t2)) -> c_40() isOp#(T()) -> c_41() - Weak DPs: and#(False(),False()) -> c_42() and#(False(),True()) -> c_43() and#(True(),False()) -> c_44() and#(True(),True()) -> c_45() - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() conj(And(t1,t2)) -> and(disj(t1),conj(t1)) conj(F()) -> True() conj(Or(o1,o2)) -> False() conj(T()) -> True() disj(And(a1,a2)) -> conj(And(a1,a2)) disj(F()) -> True() disj(Or(t1,t2)) -> and(conj(t1),disj(t1)) disj(T()) -> True() - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1,and#/2,bool#/1 ,conj#/1,disj#/1,disjconj#/1,getFirst#/1,getSecond#/1,isAnd#/1,isConsTerm#/2,isOp#/1} / {And/2,F/0,False/0 ,Or/2,T/0,True/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/3,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/3,c_12/0,c_13/1,c_14/0 ,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0 ,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0 ,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond# ,isAnd#,isConsTerm#,isOp#} and constructors {And,F,False,Or,T,True} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,6,7,8,10,12,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,41} by application of Pre({1,2,3,4,6,7,8,10,12,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 ,41}) = {5,11,13}. Here rules are labelled as follows: 1: bool#(And(a1,a2)) -> c_1() 2: bool#(F()) -> c_2() 3: bool#(Or(o1,o2)) -> c_3() 4: bool#(T()) -> c_4() 5: conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) 6: conj#(F()) -> c_6() 7: conj#(Or(o1,o2)) -> c_7() 8: conj#(T()) -> c_8() 9: disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) 10: disj#(F()) -> c_10() 11: disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) 12: disj#(T()) -> c_12() 13: disjconj#(p) -> c_13(disj#(p)) 14: getFirst#(And(t1,t2)) -> c_14() 15: getFirst#(Or(t1,t2)) -> c_15() 16: getSecond#(And(t1,t2)) -> c_16() 17: getSecond#(Or(t1,t2)) -> c_17() 18: isAnd#(And(t1,t2)) -> c_18() 19: isAnd#(F()) -> c_19() 20: isAnd#(Or(t1,t2)) -> c_20() 21: isAnd#(T()) -> c_21() 22: isConsTerm#(And(a1,a2),And(y1,y2)) -> c_22() 23: isConsTerm#(And(a1,a2),F()) -> c_23() 24: isConsTerm#(And(a1,a2),Or(x1,x2)) -> c_24() 25: isConsTerm#(And(a1,a2),T()) -> c_25() 26: isConsTerm#(F(),And(y1,y2)) -> c_26() 27: isConsTerm#(F(),F()) -> c_27() 28: isConsTerm#(F(),Or(x1,x2)) -> c_28() 29: isConsTerm#(F(),T()) -> c_29() 30: isConsTerm#(Or(o1,o2),And(y1,y2)) -> c_30() 31: isConsTerm#(Or(o1,o2),F()) -> c_31() 32: isConsTerm#(Or(o1,o2),Or(x1,x2)) -> c_32() 33: isConsTerm#(Or(o1,o2),T()) -> c_33() 34: isConsTerm#(T(),And(y1,y2)) -> c_34() 35: isConsTerm#(T(),F()) -> c_35() 36: isConsTerm#(T(),Or(x1,x2)) -> c_36() 37: isConsTerm#(T(),T()) -> c_37() 38: isOp#(And(t1,t2)) -> c_38() 39: isOp#(F()) -> c_39() 40: isOp#(Or(t1,t2)) -> c_40() 41: isOp#(T()) -> c_41() 42: and#(False(),False()) -> c_42() 43: and#(False(),True()) -> c_43() 44: and#(True(),False()) -> c_44() 45: and#(True(),True()) -> c_45() * Step 4: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) disjconj#(p) -> c_13(disj#(p)) - Weak DPs: and#(False(),False()) -> c_42() and#(False(),True()) -> c_43() and#(True(),False()) -> c_44() and#(True(),True()) -> c_45() bool#(And(a1,a2)) -> c_1() bool#(F()) -> c_2() bool#(Or(o1,o2)) -> c_3() bool#(T()) -> c_4() conj#(F()) -> c_6() conj#(Or(o1,o2)) -> c_7() conj#(T()) -> c_8() disj#(F()) -> c_10() disj#(T()) -> c_12() getFirst#(And(t1,t2)) -> c_14() getFirst#(Or(t1,t2)) -> c_15() getSecond#(And(t1,t2)) -> c_16() getSecond#(Or(t1,t2)) -> c_17() isAnd#(And(t1,t2)) -> c_18() isAnd#(F()) -> c_19() isAnd#(Or(t1,t2)) -> c_20() isAnd#(T()) -> c_21() isConsTerm#(And(a1,a2),And(y1,y2)) -> c_22() isConsTerm#(And(a1,a2),F()) -> c_23() isConsTerm#(And(a1,a2),Or(x1,x2)) -> c_24() isConsTerm#(And(a1,a2),T()) -> c_25() isConsTerm#(F(),And(y1,y2)) -> c_26() isConsTerm#(F(),F()) -> c_27() isConsTerm#(F(),Or(x1,x2)) -> c_28() isConsTerm#(F(),T()) -> c_29() isConsTerm#(Or(o1,o2),And(y1,y2)) -> c_30() isConsTerm#(Or(o1,o2),F()) -> c_31() isConsTerm#(Or(o1,o2),Or(x1,x2)) -> c_32() isConsTerm#(Or(o1,o2),T()) -> c_33() isConsTerm#(T(),And(y1,y2)) -> c_34() isConsTerm#(T(),F()) -> c_35() isConsTerm#(T(),Or(x1,x2)) -> c_36() isConsTerm#(T(),T()) -> c_37() isOp#(And(t1,t2)) -> c_38() isOp#(F()) -> c_39() isOp#(Or(t1,t2)) -> c_40() isOp#(T()) -> c_41() - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() conj(And(t1,t2)) -> and(disj(t1),conj(t1)) conj(F()) -> True() conj(Or(o1,o2)) -> False() conj(T()) -> True() disj(And(a1,a2)) -> conj(And(a1,a2)) disj(F()) -> True() disj(Or(t1,t2)) -> and(conj(t1),disj(t1)) disj(T()) -> True() - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1,and#/2,bool#/1 ,conj#/1,disj#/1,disjconj#/1,getFirst#/1,getSecond#/1,isAnd#/1,isConsTerm#/2,isOp#/1} / {And/2,F/0,False/0 ,Or/2,T/0,True/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/3,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/3,c_12/0,c_13/1,c_14/0 ,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0 ,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0 ,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond# ,isAnd#,isConsTerm#,isOp#} and constructors {And,F,False,Or,T,True} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) -->_2 disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)):3 -->_2 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 -->_2 disj#(T()) -> c_12():17 -->_2 disj#(F()) -> c_10():16 -->_3 conj#(T()) -> c_8():15 -->_3 conj#(Or(o1,o2)) -> c_7():14 -->_3 conj#(F()) -> c_6():13 -->_1 and#(True(),True()) -> c_45():8 -->_1 and#(True(),False()) -> c_44():7 -->_1 and#(False(),True()) -> c_43():6 -->_1 and#(False(),False()) -> c_42():5 -->_3 conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)):1 2:S:disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) -->_1 conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)):1 3:S:disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) -->_3 disj#(T()) -> c_12():17 -->_3 disj#(F()) -> c_10():16 -->_2 conj#(T()) -> c_8():15 -->_2 conj#(Or(o1,o2)) -> c_7():14 -->_2 conj#(F()) -> c_6():13 -->_1 and#(True(),True()) -> c_45():8 -->_1 and#(True(),False()) -> c_44():7 -->_1 and#(False(),True()) -> c_43():6 -->_1 and#(False(),False()) -> c_42():5 -->_3 disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)):3 -->_3 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 -->_2 conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)):1 4:S:disjconj#(p) -> c_13(disj#(p)) -->_1 disj#(T()) -> c_12():17 -->_1 disj#(F()) -> c_10():16 -->_1 disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)):3 -->_1 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 5:W:and#(False(),False()) -> c_42() 6:W:and#(False(),True()) -> c_43() 7:W:and#(True(),False()) -> c_44() 8:W:and#(True(),True()) -> c_45() 9:W:bool#(And(a1,a2)) -> c_1() 10:W:bool#(F()) -> c_2() 11:W:bool#(Or(o1,o2)) -> c_3() 12:W:bool#(T()) -> c_4() 13:W:conj#(F()) -> c_6() 14:W:conj#(Or(o1,o2)) -> c_7() 15:W:conj#(T()) -> c_8() 16:W:disj#(F()) -> c_10() 17:W:disj#(T()) -> c_12() 18:W:getFirst#(And(t1,t2)) -> c_14() 19:W:getFirst#(Or(t1,t2)) -> c_15() 20:W:getSecond#(And(t1,t2)) -> c_16() 21:W:getSecond#(Or(t1,t2)) -> c_17() 22:W:isAnd#(And(t1,t2)) -> c_18() 23:W:isAnd#(F()) -> c_19() 24:W:isAnd#(Or(t1,t2)) -> c_20() 25:W:isAnd#(T()) -> c_21() 26:W:isConsTerm#(And(a1,a2),And(y1,y2)) -> c_22() 27:W:isConsTerm#(And(a1,a2),F()) -> c_23() 28:W:isConsTerm#(And(a1,a2),Or(x1,x2)) -> c_24() 29:W:isConsTerm#(And(a1,a2),T()) -> c_25() 30:W:isConsTerm#(F(),And(y1,y2)) -> c_26() 31:W:isConsTerm#(F(),F()) -> c_27() 32:W:isConsTerm#(F(),Or(x1,x2)) -> c_28() 33:W:isConsTerm#(F(),T()) -> c_29() 34:W:isConsTerm#(Or(o1,o2),And(y1,y2)) -> c_30() 35:W:isConsTerm#(Or(o1,o2),F()) -> c_31() 36:W:isConsTerm#(Or(o1,o2),Or(x1,x2)) -> c_32() 37:W:isConsTerm#(Or(o1,o2),T()) -> c_33() 38:W:isConsTerm#(T(),And(y1,y2)) -> c_34() 39:W:isConsTerm#(T(),F()) -> c_35() 40:W:isConsTerm#(T(),Or(x1,x2)) -> c_36() 41:W:isConsTerm#(T(),T()) -> c_37() 42:W:isOp#(And(t1,t2)) -> c_38() 43:W:isOp#(F()) -> c_39() 44:W:isOp#(Or(t1,t2)) -> c_40() 45:W:isOp#(T()) -> c_41() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 45: isOp#(T()) -> c_41() 44: isOp#(Or(t1,t2)) -> c_40() 43: isOp#(F()) -> c_39() 42: isOp#(And(t1,t2)) -> c_38() 41: isConsTerm#(T(),T()) -> c_37() 40: isConsTerm#(T(),Or(x1,x2)) -> c_36() 39: isConsTerm#(T(),F()) -> c_35() 38: isConsTerm#(T(),And(y1,y2)) -> c_34() 37: isConsTerm#(Or(o1,o2),T()) -> c_33() 36: isConsTerm#(Or(o1,o2),Or(x1,x2)) -> c_32() 35: isConsTerm#(Or(o1,o2),F()) -> c_31() 34: isConsTerm#(Or(o1,o2),And(y1,y2)) -> c_30() 33: isConsTerm#(F(),T()) -> c_29() 32: isConsTerm#(F(),Or(x1,x2)) -> c_28() 31: isConsTerm#(F(),F()) -> c_27() 30: isConsTerm#(F(),And(y1,y2)) -> c_26() 29: isConsTerm#(And(a1,a2),T()) -> c_25() 28: isConsTerm#(And(a1,a2),Or(x1,x2)) -> c_24() 27: isConsTerm#(And(a1,a2),F()) -> c_23() 26: isConsTerm#(And(a1,a2),And(y1,y2)) -> c_22() 25: isAnd#(T()) -> c_21() 24: isAnd#(Or(t1,t2)) -> c_20() 23: isAnd#(F()) -> c_19() 22: isAnd#(And(t1,t2)) -> c_18() 21: getSecond#(Or(t1,t2)) -> c_17() 20: getSecond#(And(t1,t2)) -> c_16() 19: getFirst#(Or(t1,t2)) -> c_15() 18: getFirst#(And(t1,t2)) -> c_14() 12: bool#(T()) -> c_4() 11: bool#(Or(o1,o2)) -> c_3() 10: bool#(F()) -> c_2() 9: bool#(And(a1,a2)) -> c_1() 5: and#(False(),False()) -> c_42() 6: and#(False(),True()) -> c_43() 7: and#(True(),False()) -> c_44() 8: and#(True(),True()) -> c_45() 13: conj#(F()) -> c_6() 14: conj#(Or(o1,o2)) -> c_7() 15: conj#(T()) -> c_8() 16: disj#(F()) -> c_10() 17: disj#(T()) -> c_12() * Step 5: SimplifyRHS MAYBE + Considered Problem: - Strict DPs: conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) disjconj#(p) -> c_13(disj#(p)) - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() conj(And(t1,t2)) -> and(disj(t1),conj(t1)) conj(F()) -> True() conj(Or(o1,o2)) -> False() conj(T()) -> True() disj(And(a1,a2)) -> conj(And(a1,a2)) disj(F()) -> True() disj(Or(t1,t2)) -> and(conj(t1),disj(t1)) disj(T()) -> True() - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1,and#/2,bool#/1 ,conj#/1,disj#/1,disjconj#/1,getFirst#/1,getSecond#/1,isAnd#/1,isConsTerm#/2,isOp#/1} / {And/2,F/0,False/0 ,Or/2,T/0,True/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/3,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/3,c_12/0,c_13/1,c_14/0 ,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0 ,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0 ,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond# ,isAnd#,isConsTerm#,isOp#} and constructors {And,F,False,Or,T,True} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)) -->_2 disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)):3 -->_2 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 -->_3 conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)):1 2:S:disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) -->_1 conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)):1 3:S:disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)) -->_3 disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)):3 -->_3 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 -->_2 conj#(And(t1,t2)) -> c_5(and#(disj(t1),conj(t1)),disj#(t1),conj#(t1)):1 4:S:disjconj#(p) -> c_13(disj#(p)) -->_1 disj#(Or(t1,t2)) -> c_11(and#(conj(t1),disj(t1)),conj#(t1),disj#(t1)):3 -->_1 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)) disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)) * Step 6: UsableRules MAYBE + Considered Problem: - Strict DPs: conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)) disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)) disjconj#(p) -> c_13(disj#(p)) - Weak TRS: and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() conj(And(t1,t2)) -> and(disj(t1),conj(t1)) conj(F()) -> True() conj(Or(o1,o2)) -> False() conj(T()) -> True() disj(And(a1,a2)) -> conj(And(a1,a2)) disj(F()) -> True() disj(Or(t1,t2)) -> and(conj(t1),disj(t1)) disj(T()) -> True() - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1,and#/2,bool#/1 ,conj#/1,disj#/1,disjconj#/1,getFirst#/1,getSecond#/1,isAnd#/1,isConsTerm#/2,isOp#/1} / {And/2,F/0,False/0 ,Or/2,T/0,True/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/0,c_13/1,c_14/0 ,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0 ,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0 ,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond# ,isAnd#,isConsTerm#,isOp#} and constructors {And,F,False,Or,T,True} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)) disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)) disjconj#(p) -> c_13(disj#(p)) * Step 7: RemoveHeads MAYBE + Considered Problem: - Strict DPs: conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)) disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)) disjconj#(p) -> c_13(disj#(p)) - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1,and#/2,bool#/1 ,conj#/1,disj#/1,disjconj#/1,getFirst#/1,getSecond#/1,isAnd#/1,isConsTerm#/2,isOp#/1} / {And/2,F/0,False/0 ,Or/2,T/0,True/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/0,c_13/1,c_14/0 ,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0 ,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0 ,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond# ,isAnd#,isConsTerm#,isOp#} and constructors {And,F,False,Or,T,True} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)) -->_1 disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)):3 -->_1 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 -->_2 conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)):1 2:S:disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) -->_1 conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)):1 3:S:disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)) -->_2 disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)):3 -->_2 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 -->_1 conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)):1 4:S:disjconj#(p) -> c_13(disj#(p)) -->_1 disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)):3 -->_1 disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))):2 Following roots of the dependency graph are removed, as the considered set of starting terms is closed under reduction with respect to these rules (modulo compound contexts). [(4,disjconj#(p) -> c_13(disj#(p)))] * Step 8: WeightGap MAYBE + Considered Problem: - Strict DPs: conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)) disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)) - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1,and#/2,bool#/1 ,conj#/1,disj#/1,disjconj#/1,getFirst#/1,getSecond#/1,isAnd#/1,isConsTerm#/2,isOp#/1} / {And/2,F/0,False/0 ,Or/2,T/0,True/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/0,c_13/1,c_14/0 ,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0 ,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0 ,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond# ,isAnd#,isConsTerm#,isOp#} and constructors {And,F,False,Or,T,True} + Applied Processor: WeightGap {wgDimension = 1, wgDegree = 0, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny} + Details: The weightgap principle applies using the following constant growth matrix-interpretation: We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 0 non-zero interpretation-entries in the diagonal of the component-wise maxima): The following argument positions are considered usable: uargs(c_5) = {1,2}, uargs(c_9) = {1}, uargs(c_11) = {1,2} Following symbols are considered usable: all TcT has computed the following interpretation: p(And) = [1] p(F) = [0] p(False) = [0] p(Or) = [0] p(T) = [0] p(True) = [0] p(and) = [0] p(bool) = [0] p(conj) = [0] p(disj) = [1] x1 + [0] p(disjconj) = [0] p(getFirst) = [1] x1 + [8] p(getSecond) = [1] x1 + [4] p(isAnd) = [1] x1 + [8] p(isConsTerm) = [2] x2 + [0] p(isOp) = [2] x1 + [1] p(and#) = [4] p(bool#) = [0] p(conj#) = [0] p(disj#) = [9] p(disjconj#) = [0] p(getFirst#) = [0] p(getSecond#) = [0] p(isAnd#) = [0] p(isConsTerm#) = [0] p(isOp#) = [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [1] x1 + [1] x2 + [7] p(c_6) = [0] p(c_7) = [8] p(c_8) = [1] p(c_9) = [1] x1 + [1] p(c_10) = [4] p(c_11) = [1] x1 + [1] x2 + [4] p(c_12) = [0] p(c_13) = [0] p(c_14) = [0] p(c_15) = [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [0] p(c_19) = [0] p(c_20) = [0] p(c_21) = [0] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [0] p(c_26) = [0] p(c_27) = [0] p(c_28) = [1] p(c_29) = [8] p(c_30) = [0] p(c_31) = [1] p(c_32) = [0] p(c_33) = [1] p(c_34) = [1] p(c_35) = [1] p(c_36) = [1] p(c_37) = [0] p(c_38) = [4] p(c_39) = [2] p(c_40) = [8] p(c_41) = [0] p(c_42) = [0] p(c_43) = [0] p(c_44) = [2] p(c_45) = [1] Following rules are strictly oriented: disj#(And(a1,a2)) = [9] > [1] = c_9(conj#(And(a1,a2))) Following rules are (at-least) weakly oriented: conj#(And(t1,t2)) = [0] >= [16] = c_5(disj#(t1),conj#(t1)) disj#(Or(t1,t2)) = [9] >= [13] = c_11(conj#(t1),disj#(t1)) Further, it can be verified that all rules not oriented are covered by the weightgap condition. * Step 9: Failure MAYBE + Considered Problem: - Strict DPs: conj#(And(t1,t2)) -> c_5(disj#(t1),conj#(t1)) disj#(Or(t1,t2)) -> c_11(conj#(t1),disj#(t1)) - Weak DPs: disj#(And(a1,a2)) -> c_9(conj#(And(a1,a2))) - Signature: {and/2,bool/1,conj/1,disj/1,disjconj/1,getFirst/1,getSecond/1,isAnd/1,isConsTerm/2,isOp/1,and#/2,bool#/1 ,conj#/1,disj#/1,disjconj#/1,getFirst#/1,getSecond#/1,isAnd#/1,isConsTerm#/2,isOp#/1} / {And/2,F/0,False/0 ,Or/2,T/0,True/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/2,c_6/0,c_7/0,c_8/0,c_9/1,c_10/0,c_11/2,c_12/0,c_13/1,c_14/0 ,c_15/0,c_16/0,c_17/0,c_18/0,c_19/0,c_20/0,c_21/0,c_22/0,c_23/0,c_24/0,c_25/0,c_26/0,c_27/0,c_28/0,c_29/0 ,c_30/0,c_31/0,c_32/0,c_33/0,c_34/0,c_35/0,c_36/0,c_37/0,c_38/0,c_39/0,c_40/0,c_41/0,c_42/0,c_43/0,c_44/0 ,c_45/0} - Obligation: innermost runtime complexity wrt. defined symbols {and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond# ,isAnd#,isConsTerm#,isOp#} and constructors {And,F,False,Or,T,True} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE