WORST_CASE(Omega(n^1),O(n^1)) * Step 1: Sum. WORST_CASE(Omega(n^1),O(n^1)) + Considered Problem: - Strict TRS: BOOL(And(z0,z1)) -> c16() BOOL(F()) -> c15() BOOL(Or(z0,z1)) -> c17() BOOL(T()) -> c14() CONJ(And(z0,z1)) -> c12(AND(disj(z0),conj(z0)),DISJ(z0)) CONJ(And(z0,z1)) -> c13(AND(disj(z0),conj(z0)),CONJ(z0)) CONJ(F()) -> c11() CONJ(Or(z0,z1)) -> c9() CONJ(T()) -> c10() DISJ(And(z0,z1)) -> c6(CONJ(And(z0,z1))) DISJ(F()) -> c5() DISJ(Or(z0,z1)) -> c7(AND(conj(z0),disj(z0)),CONJ(z0)) DISJ(Or(z0,z1)) -> c8(AND(conj(z0),disj(z0)),DISJ(z0)) DISJ(T()) -> c4() DISJCONJ(z0) -> c46(DISJ(z0)) GETFIRST(And(z0,z1)) -> c44() GETFIRST(Or(z0,z1)) -> c45() GETSECOND(And(z0,z1)) -> c42() GETSECOND(Or(z0,z1)) -> c43() ISAND(And(z0,z1)) -> c40() ISAND(F()) -> c39() ISAND(Or(z0,z1)) -> c41() ISAND(T()) -> c38() ISCONSTERM(And(z0,z1),And(z2,z3)) -> c28() ISCONSTERM(And(z0,z1),F()) -> c27() ISCONSTERM(And(z0,z1),Or(z2,z3)) -> c29() ISCONSTERM(And(z0,z1),T()) -> c26() ISCONSTERM(F(),And(z0,z1)) -> c24() ISCONSTERM(F(),F()) -> c23() ISCONSTERM(F(),Or(z0,z1)) -> c25() ISCONSTERM(F(),T()) -> c22() ISCONSTERM(Or(z0,z1),And(z2,z3)) -> c32() ISCONSTERM(Or(z0,z1),F()) -> c31() ISCONSTERM(Or(z0,z1),Or(z2,z3)) -> c33() ISCONSTERM(Or(z0,z1),T()) -> c30() ISCONSTERM(T(),And(z0,z1)) -> c20() ISCONSTERM(T(),F()) -> c19() ISCONSTERM(T(),Or(z0,z1)) -> c21() ISCONSTERM(T(),T()) -> c18() ISOP(And(z0,z1)) -> c36() ISOP(F()) -> c35() ISOP(Or(z0,z1)) -> c37() ISOP(T()) -> c34() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(z0,z1)) -> False() bool(F()) -> True() bool(Or(z0,z1)) -> False() bool(T()) -> True() conj(And(z0,z1)) -> and(disj(z0),conj(z0)) conj(F()) -> True() conj(Or(z0,z1)) -> False() conj(T()) -> True() disj(And(z0,z1)) -> conj(And(z0,z1)) disj(F()) -> True() disj(Or(z0,z1)) -> and(conj(z0),disj(z0)) disj(T()) -> True() disjconj(z0) -> disj(z0) getFirst(And(z0,z1)) -> z0 getFirst(Or(z0,z1)) -> z0 getSecond(And(z0,z1)) -> z0 getSecond(Or(z0,z1)) -> z0 isAnd(And(z0,z1)) -> True() isAnd(F()) -> False() isAnd(Or(z0,z1)) -> False() isAnd(T()) -> False() isConsTerm(And(z0,z1),And(z2,z3)) -> True() isConsTerm(And(z0,z1),F()) -> False() isConsTerm(And(z0,z1),Or(z2,z3)) -> False() isConsTerm(And(z0,z1),T()) -> False() isConsTerm(F(),And(z0,z1)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(z0,z1)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(z0,z1),And(z2,z3)) -> False() isConsTerm(Or(z0,z1),F()) -> False() isConsTerm(Or(z0,z1),Or(z2,z3)) -> True() isConsTerm(Or(z0,z1),T()) -> False() isConsTerm(T(),And(z0,z1)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(z0,z1)) -> False() isConsTerm(T(),T()) -> True() isOp(And(z0,z1)) -> True() isOp(F()) -> False() isOp(Or(z0,z1)) -> 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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0 ,c24/0,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0 ,c40/0,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,BOOL,CONJ,DISJ,DISJCONJ,GETFIRST,GETSECOND,ISAND ,ISCONSTERM,ISOP,and,bool,conj,disj,disjconj,getFirst,getSecond,isAnd,isConsTerm,isOp} and constructors {And ,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29 ,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: BOOL(And(z0,z1)) -> c16() BOOL(F()) -> c15() BOOL(Or(z0,z1)) -> c17() BOOL(T()) -> c14() CONJ(And(z0,z1)) -> c12(AND(disj(z0),conj(z0)),DISJ(z0)) CONJ(And(z0,z1)) -> c13(AND(disj(z0),conj(z0)),CONJ(z0)) CONJ(F()) -> c11() CONJ(Or(z0,z1)) -> c9() CONJ(T()) -> c10() DISJ(And(z0,z1)) -> c6(CONJ(And(z0,z1))) DISJ(F()) -> c5() DISJ(Or(z0,z1)) -> c7(AND(conj(z0),disj(z0)),CONJ(z0)) DISJ(Or(z0,z1)) -> c8(AND(conj(z0),disj(z0)),DISJ(z0)) DISJ(T()) -> c4() DISJCONJ(z0) -> c46(DISJ(z0)) GETFIRST(And(z0,z1)) -> c44() GETFIRST(Or(z0,z1)) -> c45() GETSECOND(And(z0,z1)) -> c42() GETSECOND(Or(z0,z1)) -> c43() ISAND(And(z0,z1)) -> c40() ISAND(F()) -> c39() ISAND(Or(z0,z1)) -> c41() ISAND(T()) -> c38() ISCONSTERM(And(z0,z1),And(z2,z3)) -> c28() ISCONSTERM(And(z0,z1),F()) -> c27() ISCONSTERM(And(z0,z1),Or(z2,z3)) -> c29() ISCONSTERM(And(z0,z1),T()) -> c26() ISCONSTERM(F(),And(z0,z1)) -> c24() ISCONSTERM(F(),F()) -> c23() ISCONSTERM(F(),Or(z0,z1)) -> c25() ISCONSTERM(F(),T()) -> c22() ISCONSTERM(Or(z0,z1),And(z2,z3)) -> c32() ISCONSTERM(Or(z0,z1),F()) -> c31() ISCONSTERM(Or(z0,z1),Or(z2,z3)) -> c33() ISCONSTERM(Or(z0,z1),T()) -> c30() ISCONSTERM(T(),And(z0,z1)) -> c20() ISCONSTERM(T(),F()) -> c19() ISCONSTERM(T(),Or(z0,z1)) -> c21() ISCONSTERM(T(),T()) -> c18() ISOP(And(z0,z1)) -> c36() ISOP(F()) -> c35() ISOP(Or(z0,z1)) -> c37() ISOP(T()) -> c34() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(z0,z1)) -> False() bool(F()) -> True() bool(Or(z0,z1)) -> False() bool(T()) -> True() conj(And(z0,z1)) -> and(disj(z0),conj(z0)) conj(F()) -> True() conj(Or(z0,z1)) -> False() conj(T()) -> True() disj(And(z0,z1)) -> conj(And(z0,z1)) disj(F()) -> True() disj(Or(z0,z1)) -> and(conj(z0),disj(z0)) disj(T()) -> True() disjconj(z0) -> disj(z0) getFirst(And(z0,z1)) -> z0 getFirst(Or(z0,z1)) -> z0 getSecond(And(z0,z1)) -> z0 getSecond(Or(z0,z1)) -> z0 isAnd(And(z0,z1)) -> True() isAnd(F()) -> False() isAnd(Or(z0,z1)) -> False() isAnd(T()) -> False() isConsTerm(And(z0,z1),And(z2,z3)) -> True() isConsTerm(And(z0,z1),F()) -> False() isConsTerm(And(z0,z1),Or(z2,z3)) -> False() isConsTerm(And(z0,z1),T()) -> False() isConsTerm(F(),And(z0,z1)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(z0,z1)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(z0,z1),And(z2,z3)) -> False() isConsTerm(Or(z0,z1),F()) -> False() isConsTerm(Or(z0,z1),Or(z2,z3)) -> True() isConsTerm(Or(z0,z1),T()) -> False() isConsTerm(T(),And(z0,z1)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(z0,z1)) -> False() isConsTerm(T(),T()) -> True() isOp(And(z0,z1)) -> True() isOp(F()) -> False() isOp(Or(z0,z1)) -> 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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0 ,c24/0,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0 ,c40/0,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,BOOL,CONJ,DISJ,DISJCONJ,GETFIRST,GETSECOND,ISAND ,ISCONSTERM,ISOP,and,bool,conj,disj,disjconj,getFirst,getSecond,isAnd,isConsTerm,isOp} and constructors {And ,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29 ,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6,c7,c8,c9} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () ** Step 1.a:2: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: BOOL(And(z0,z1)) -> c16() BOOL(F()) -> c15() BOOL(Or(z0,z1)) -> c17() BOOL(T()) -> c14() CONJ(And(z0,z1)) -> c12(AND(disj(z0),conj(z0)),DISJ(z0)) CONJ(And(z0,z1)) -> c13(AND(disj(z0),conj(z0)),CONJ(z0)) CONJ(F()) -> c11() CONJ(Or(z0,z1)) -> c9() CONJ(T()) -> c10() DISJ(And(z0,z1)) -> c6(CONJ(And(z0,z1))) DISJ(F()) -> c5() DISJ(Or(z0,z1)) -> c7(AND(conj(z0),disj(z0)),CONJ(z0)) DISJ(Or(z0,z1)) -> c8(AND(conj(z0),disj(z0)),DISJ(z0)) DISJ(T()) -> c4() DISJCONJ(z0) -> c46(DISJ(z0)) GETFIRST(And(z0,z1)) -> c44() GETFIRST(Or(z0,z1)) -> c45() GETSECOND(And(z0,z1)) -> c42() GETSECOND(Or(z0,z1)) -> c43() ISAND(And(z0,z1)) -> c40() ISAND(F()) -> c39() ISAND(Or(z0,z1)) -> c41() ISAND(T()) -> c38() ISCONSTERM(And(z0,z1),And(z2,z3)) -> c28() ISCONSTERM(And(z0,z1),F()) -> c27() ISCONSTERM(And(z0,z1),Or(z2,z3)) -> c29() ISCONSTERM(And(z0,z1),T()) -> c26() ISCONSTERM(F(),And(z0,z1)) -> c24() ISCONSTERM(F(),F()) -> c23() ISCONSTERM(F(),Or(z0,z1)) -> c25() ISCONSTERM(F(),T()) -> c22() ISCONSTERM(Or(z0,z1),And(z2,z3)) -> c32() ISCONSTERM(Or(z0,z1),F()) -> c31() ISCONSTERM(Or(z0,z1),Or(z2,z3)) -> c33() ISCONSTERM(Or(z0,z1),T()) -> c30() ISCONSTERM(T(),And(z0,z1)) -> c20() ISCONSTERM(T(),F()) -> c19() ISCONSTERM(T(),Or(z0,z1)) -> c21() ISCONSTERM(T(),T()) -> c18() ISOP(And(z0,z1)) -> c36() ISOP(F()) -> c35() ISOP(Or(z0,z1)) -> c37() ISOP(T()) -> c34() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(z0,z1)) -> False() bool(F()) -> True() bool(Or(z0,z1)) -> False() bool(T()) -> True() conj(And(z0,z1)) -> and(disj(z0),conj(z0)) conj(F()) -> True() conj(Or(z0,z1)) -> False() conj(T()) -> True() disj(And(z0,z1)) -> conj(And(z0,z1)) disj(F()) -> True() disj(Or(z0,z1)) -> and(conj(z0),disj(z0)) disj(T()) -> True() disjconj(z0) -> disj(z0) getFirst(And(z0,z1)) -> z0 getFirst(Or(z0,z1)) -> z0 getSecond(And(z0,z1)) -> z0 getSecond(Or(z0,z1)) -> z0 isAnd(And(z0,z1)) -> True() isAnd(F()) -> False() isAnd(Or(z0,z1)) -> False() isAnd(T()) -> False() isConsTerm(And(z0,z1),And(z2,z3)) -> True() isConsTerm(And(z0,z1),F()) -> False() isConsTerm(And(z0,z1),Or(z2,z3)) -> False() isConsTerm(And(z0,z1),T()) -> False() isConsTerm(F(),And(z0,z1)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(z0,z1)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(z0,z1),And(z2,z3)) -> False() isConsTerm(Or(z0,z1),F()) -> False() isConsTerm(Or(z0,z1),Or(z2,z3)) -> True() isConsTerm(Or(z0,z1),T()) -> False() isConsTerm(T(),And(z0,z1)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(z0,z1)) -> False() isConsTerm(T(),T()) -> True() isOp(And(z0,z1)) -> True() isOp(F()) -> False() isOp(Or(z0,z1)) -> 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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0 ,c24/0,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0 ,c40/0,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,BOOL,CONJ,DISJ,DISJCONJ,GETFIRST,GETSECOND,ISAND ,ISCONSTERM,ISOP,and,bool,conj,disj,disjconj,getFirst,getSecond,isAnd,isConsTerm,isOp} and constructors {And ,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29 ,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6,c7,c8,c9} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: CONJ(x){x -> And(x,y)} = CONJ(And(x,y)) ->^+ c13(AND(disj(x),conj(x)),CONJ(x)) = C[CONJ(x) = CONJ(x){}] ** Step 1.b:1: DependencyPairs. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: BOOL(And(z0,z1)) -> c16() BOOL(F()) -> c15() BOOL(Or(z0,z1)) -> c17() BOOL(T()) -> c14() CONJ(And(z0,z1)) -> c12(AND(disj(z0),conj(z0)),DISJ(z0)) CONJ(And(z0,z1)) -> c13(AND(disj(z0),conj(z0)),CONJ(z0)) CONJ(F()) -> c11() CONJ(Or(z0,z1)) -> c9() CONJ(T()) -> c10() DISJ(And(z0,z1)) -> c6(CONJ(And(z0,z1))) DISJ(F()) -> c5() DISJ(Or(z0,z1)) -> c7(AND(conj(z0),disj(z0)),CONJ(z0)) DISJ(Or(z0,z1)) -> c8(AND(conj(z0),disj(z0)),DISJ(z0)) DISJ(T()) -> c4() DISJCONJ(z0) -> c46(DISJ(z0)) GETFIRST(And(z0,z1)) -> c44() GETFIRST(Or(z0,z1)) -> c45() GETSECOND(And(z0,z1)) -> c42() GETSECOND(Or(z0,z1)) -> c43() ISAND(And(z0,z1)) -> c40() ISAND(F()) -> c39() ISAND(Or(z0,z1)) -> c41() ISAND(T()) -> c38() ISCONSTERM(And(z0,z1),And(z2,z3)) -> c28() ISCONSTERM(And(z0,z1),F()) -> c27() ISCONSTERM(And(z0,z1),Or(z2,z3)) -> c29() ISCONSTERM(And(z0,z1),T()) -> c26() ISCONSTERM(F(),And(z0,z1)) -> c24() ISCONSTERM(F(),F()) -> c23() ISCONSTERM(F(),Or(z0,z1)) -> c25() ISCONSTERM(F(),T()) -> c22() ISCONSTERM(Or(z0,z1),And(z2,z3)) -> c32() ISCONSTERM(Or(z0,z1),F()) -> c31() ISCONSTERM(Or(z0,z1),Or(z2,z3)) -> c33() ISCONSTERM(Or(z0,z1),T()) -> c30() ISCONSTERM(T(),And(z0,z1)) -> c20() ISCONSTERM(T(),F()) -> c19() ISCONSTERM(T(),Or(z0,z1)) -> c21() ISCONSTERM(T(),T()) -> c18() ISOP(And(z0,z1)) -> c36() ISOP(F()) -> c35() ISOP(Or(z0,z1)) -> c37() ISOP(T()) -> c34() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(z0,z1)) -> False() bool(F()) -> True() bool(Or(z0,z1)) -> False() bool(T()) -> True() conj(And(z0,z1)) -> and(disj(z0),conj(z0)) conj(F()) -> True() conj(Or(z0,z1)) -> False() conj(T()) -> True() disj(And(z0,z1)) -> conj(And(z0,z1)) disj(F()) -> True() disj(Or(z0,z1)) -> and(conj(z0),disj(z0)) disj(T()) -> True() disjconj(z0) -> disj(z0) getFirst(And(z0,z1)) -> z0 getFirst(Or(z0,z1)) -> z0 getSecond(And(z0,z1)) -> z0 getSecond(Or(z0,z1)) -> z0 isAnd(And(z0,z1)) -> True() isAnd(F()) -> False() isAnd(Or(z0,z1)) -> False() isAnd(T()) -> False() isConsTerm(And(z0,z1),And(z2,z3)) -> True() isConsTerm(And(z0,z1),F()) -> False() isConsTerm(And(z0,z1),Or(z2,z3)) -> False() isConsTerm(And(z0,z1),T()) -> False() isConsTerm(F(),And(z0,z1)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(z0,z1)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(z0,z1),And(z2,z3)) -> False() isConsTerm(Or(z0,z1),F()) -> False() isConsTerm(Or(z0,z1),Or(z2,z3)) -> True() isConsTerm(Or(z0,z1),T()) -> False() isConsTerm(T(),And(z0,z1)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(z0,z1)) -> False() isConsTerm(T(),T()) -> True() isOp(And(z0,z1)) -> True() isOp(F()) -> False() isOp(Or(z0,z1)) -> 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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0 ,c24/0,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0 ,c40/0,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND,BOOL,CONJ,DISJ,DISJCONJ,GETFIRST,GETSECOND,ISAND ,ISCONSTERM,ISOP,and,bool,conj,disj,disjconj,getFirst,getSecond,isAnd,isConsTerm,isOp} and constructors {And ,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29 ,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6,c7,c8,c9} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs BOOL#(And(z0,z1)) -> c_1() BOOL#(F()) -> c_2() BOOL#(Or(z0,z1)) -> c_3() BOOL#(T()) -> c_4() CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)) CONJ#(F()) -> c_7() CONJ#(Or(z0,z1)) -> c_8() CONJ#(T()) -> c_9() DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(F()) -> c_11() DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)) DISJ#(T()) -> c_14() DISJCONJ#(z0) -> c_15(DISJ#(z0)) GETFIRST#(And(z0,z1)) -> c_16() GETFIRST#(Or(z0,z1)) -> c_17() GETSECOND#(And(z0,z1)) -> c_18() GETSECOND#(Or(z0,z1)) -> c_19() ISAND#(And(z0,z1)) -> c_20() ISAND#(F()) -> c_21() ISAND#(Or(z0,z1)) -> c_22() ISAND#(T()) -> c_23() ISCONSTERM#(And(z0,z1),And(z2,z3)) -> c_24() ISCONSTERM#(And(z0,z1),F()) -> c_25() ISCONSTERM#(And(z0,z1),Or(z2,z3)) -> c_26() ISCONSTERM#(And(z0,z1),T()) -> c_27() ISCONSTERM#(F(),And(z0,z1)) -> c_28() ISCONSTERM#(F(),F()) -> c_29() ISCONSTERM#(F(),Or(z0,z1)) -> c_30() ISCONSTERM#(F(),T()) -> c_31() ISCONSTERM#(Or(z0,z1),And(z2,z3)) -> c_32() ISCONSTERM#(Or(z0,z1),F()) -> c_33() ISCONSTERM#(Or(z0,z1),Or(z2,z3)) -> c_34() ISCONSTERM#(Or(z0,z1),T()) -> c_35() ISCONSTERM#(T(),And(z0,z1)) -> c_36() ISCONSTERM#(T(),F()) -> c_37() ISCONSTERM#(T(),Or(z0,z1)) -> c_38() ISCONSTERM#(T(),T()) -> c_39() ISOP#(And(z0,z1)) -> c_40() ISOP#(F()) -> c_41() ISOP#(Or(z0,z1)) -> c_42() ISOP#(T()) -> c_43() Weak DPs AND#(False(),False()) -> c_44() AND#(False(),True()) -> c_45() AND#(True(),False()) -> c_46() AND#(True(),True()) -> c_47() and#(False(),False()) -> c_48() and#(False(),True()) -> c_49() and#(True(),False()) -> c_50() and#(True(),True()) -> c_51() bool#(And(z0,z1)) -> c_52() bool#(F()) -> c_53() bool#(Or(z0,z1)) -> c_54() bool#(T()) -> c_55() conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)) conj#(F()) -> c_57() conj#(Or(z0,z1)) -> c_58() conj#(T()) -> c_59() disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))) disj#(F()) -> c_61() disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)) disj#(T()) -> c_63() disjconj#(z0) -> c_64(disj#(z0)) getFirst#(And(z0,z1)) -> c_65() getFirst#(Or(z0,z1)) -> c_66() getSecond#(And(z0,z1)) -> c_67() getSecond#(Or(z0,z1)) -> c_68() isAnd#(And(z0,z1)) -> c_69() isAnd#(F()) -> c_70() isAnd#(Or(z0,z1)) -> c_71() isAnd#(T()) -> c_72() isConsTerm#(And(z0,z1),And(z2,z3)) -> c_73() isConsTerm#(And(z0,z1),F()) -> c_74() isConsTerm#(And(z0,z1),Or(z2,z3)) -> c_75() isConsTerm#(And(z0,z1),T()) -> c_76() isConsTerm#(F(),And(z0,z1)) -> c_77() isConsTerm#(F(),F()) -> c_78() isConsTerm#(F(),Or(z0,z1)) -> c_79() isConsTerm#(F(),T()) -> c_80() isConsTerm#(Or(z0,z1),And(z2,z3)) -> c_81() isConsTerm#(Or(z0,z1),F()) -> c_82() isConsTerm#(Or(z0,z1),Or(z2,z3)) -> c_83() isConsTerm#(Or(z0,z1),T()) -> c_84() isConsTerm#(T(),And(z0,z1)) -> c_85() isConsTerm#(T(),F()) -> c_86() isConsTerm#(T(),Or(z0,z1)) -> c_87() isConsTerm#(T(),T()) -> c_88() isOp#(And(z0,z1)) -> c_89() isOp#(F()) -> c_90() isOp#(Or(z0,z1)) -> c_91() isOp#(T()) -> c_92() and mark the set of starting terms. ** Step 1.b:2: PredecessorEstimation. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: BOOL#(And(z0,z1)) -> c_1() BOOL#(F()) -> c_2() BOOL#(Or(z0,z1)) -> c_3() BOOL#(T()) -> c_4() CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)) CONJ#(F()) -> c_7() CONJ#(Or(z0,z1)) -> c_8() CONJ#(T()) -> c_9() DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(F()) -> c_11() DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)) DISJ#(T()) -> c_14() DISJCONJ#(z0) -> c_15(DISJ#(z0)) GETFIRST#(And(z0,z1)) -> c_16() GETFIRST#(Or(z0,z1)) -> c_17() GETSECOND#(And(z0,z1)) -> c_18() GETSECOND#(Or(z0,z1)) -> c_19() ISAND#(And(z0,z1)) -> c_20() ISAND#(F()) -> c_21() ISAND#(Or(z0,z1)) -> c_22() ISAND#(T()) -> c_23() ISCONSTERM#(And(z0,z1),And(z2,z3)) -> c_24() ISCONSTERM#(And(z0,z1),F()) -> c_25() ISCONSTERM#(And(z0,z1),Or(z2,z3)) -> c_26() ISCONSTERM#(And(z0,z1),T()) -> c_27() ISCONSTERM#(F(),And(z0,z1)) -> c_28() ISCONSTERM#(F(),F()) -> c_29() ISCONSTERM#(F(),Or(z0,z1)) -> c_30() ISCONSTERM#(F(),T()) -> c_31() ISCONSTERM#(Or(z0,z1),And(z2,z3)) -> c_32() ISCONSTERM#(Or(z0,z1),F()) -> c_33() ISCONSTERM#(Or(z0,z1),Or(z2,z3)) -> c_34() ISCONSTERM#(Or(z0,z1),T()) -> c_35() ISCONSTERM#(T(),And(z0,z1)) -> c_36() ISCONSTERM#(T(),F()) -> c_37() ISCONSTERM#(T(),Or(z0,z1)) -> c_38() ISCONSTERM#(T(),T()) -> c_39() ISOP#(And(z0,z1)) -> c_40() ISOP#(F()) -> c_41() ISOP#(Or(z0,z1)) -> c_42() ISOP#(T()) -> c_43() - Weak DPs: AND#(False(),False()) -> c_44() AND#(False(),True()) -> c_45() AND#(True(),False()) -> c_46() AND#(True(),True()) -> c_47() and#(False(),False()) -> c_48() and#(False(),True()) -> c_49() and#(True(),False()) -> c_50() and#(True(),True()) -> c_51() bool#(And(z0,z1)) -> c_52() bool#(F()) -> c_53() bool#(Or(z0,z1)) -> c_54() bool#(T()) -> c_55() conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)) conj#(F()) -> c_57() conj#(Or(z0,z1)) -> c_58() conj#(T()) -> c_59() disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))) disj#(F()) -> c_61() disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)) disj#(T()) -> c_63() disjconj#(z0) -> c_64(disj#(z0)) getFirst#(And(z0,z1)) -> c_65() getFirst#(Or(z0,z1)) -> c_66() getSecond#(And(z0,z1)) -> c_67() getSecond#(Or(z0,z1)) -> c_68() isAnd#(And(z0,z1)) -> c_69() isAnd#(F()) -> c_70() isAnd#(Or(z0,z1)) -> c_71() isAnd#(T()) -> c_72() isConsTerm#(And(z0,z1),And(z2,z3)) -> c_73() isConsTerm#(And(z0,z1),F()) -> c_74() isConsTerm#(And(z0,z1),Or(z2,z3)) -> c_75() isConsTerm#(And(z0,z1),T()) -> c_76() isConsTerm#(F(),And(z0,z1)) -> c_77() isConsTerm#(F(),F()) -> c_78() isConsTerm#(F(),Or(z0,z1)) -> c_79() isConsTerm#(F(),T()) -> c_80() isConsTerm#(Or(z0,z1),And(z2,z3)) -> c_81() isConsTerm#(Or(z0,z1),F()) -> c_82() isConsTerm#(Or(z0,z1),Or(z2,z3)) -> c_83() isConsTerm#(Or(z0,z1),T()) -> c_84() isConsTerm#(T(),And(z0,z1)) -> c_85() isConsTerm#(T(),F()) -> c_86() isConsTerm#(T(),Or(z0,z1)) -> c_87() isConsTerm#(T(),T()) -> c_88() isOp#(And(z0,z1)) -> c_89() isOp#(F()) -> c_90() isOp#(Or(z0,z1)) -> c_91() isOp#(T()) -> c_92() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() BOOL(And(z0,z1)) -> c16() BOOL(F()) -> c15() BOOL(Or(z0,z1)) -> c17() BOOL(T()) -> c14() CONJ(And(z0,z1)) -> c12(AND(disj(z0),conj(z0)),DISJ(z0)) CONJ(And(z0,z1)) -> c13(AND(disj(z0),conj(z0)),CONJ(z0)) CONJ(F()) -> c11() CONJ(Or(z0,z1)) -> c9() CONJ(T()) -> c10() DISJ(And(z0,z1)) -> c6(CONJ(And(z0,z1))) DISJ(F()) -> c5() DISJ(Or(z0,z1)) -> c7(AND(conj(z0),disj(z0)),CONJ(z0)) DISJ(Or(z0,z1)) -> c8(AND(conj(z0),disj(z0)),DISJ(z0)) DISJ(T()) -> c4() DISJCONJ(z0) -> c46(DISJ(z0)) GETFIRST(And(z0,z1)) -> c44() GETFIRST(Or(z0,z1)) -> c45() GETSECOND(And(z0,z1)) -> c42() GETSECOND(Or(z0,z1)) -> c43() ISAND(And(z0,z1)) -> c40() ISAND(F()) -> c39() ISAND(Or(z0,z1)) -> c41() ISAND(T()) -> c38() ISCONSTERM(And(z0,z1),And(z2,z3)) -> c28() ISCONSTERM(And(z0,z1),F()) -> c27() ISCONSTERM(And(z0,z1),Or(z2,z3)) -> c29() ISCONSTERM(And(z0,z1),T()) -> c26() ISCONSTERM(F(),And(z0,z1)) -> c24() ISCONSTERM(F(),F()) -> c23() ISCONSTERM(F(),Or(z0,z1)) -> c25() ISCONSTERM(F(),T()) -> c22() ISCONSTERM(Or(z0,z1),And(z2,z3)) -> c32() ISCONSTERM(Or(z0,z1),F()) -> c31() ISCONSTERM(Or(z0,z1),Or(z2,z3)) -> c33() ISCONSTERM(Or(z0,z1),T()) -> c30() ISCONSTERM(T(),And(z0,z1)) -> c20() ISCONSTERM(T(),F()) -> c19() ISCONSTERM(T(),Or(z0,z1)) -> c21() ISCONSTERM(T(),T()) -> c18() ISOP(And(z0,z1)) -> c36() ISOP(F()) -> c35() ISOP(Or(z0,z1)) -> c37() ISOP(T()) -> c34() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(z0,z1)) -> False() bool(F()) -> True() bool(Or(z0,z1)) -> False() bool(T()) -> True() conj(And(z0,z1)) -> and(disj(z0),conj(z0)) conj(F()) -> True() conj(Or(z0,z1)) -> False() conj(T()) -> True() disj(And(z0,z1)) -> conj(And(z0,z1)) disj(F()) -> True() disj(Or(z0,z1)) -> and(conj(z0),disj(z0)) disj(T()) -> True() disjconj(z0) -> disj(z0) getFirst(And(z0,z1)) -> z0 getFirst(Or(z0,z1)) -> z0 getSecond(And(z0,z1)) -> z0 getSecond(Or(z0,z1)) -> z0 isAnd(And(z0,z1)) -> True() isAnd(F()) -> False() isAnd(Or(z0,z1)) -> False() isAnd(T()) -> False() isConsTerm(And(z0,z1),And(z2,z3)) -> True() isConsTerm(And(z0,z1),F()) -> False() isConsTerm(And(z0,z1),Or(z2,z3)) -> False() isConsTerm(And(z0,z1),T()) -> False() isConsTerm(F(),And(z0,z1)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(z0,z1)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(z0,z1),And(z2,z3)) -> False() isConsTerm(Or(z0,z1),F()) -> False() isConsTerm(Or(z0,z1),Or(z2,z3)) -> True() isConsTerm(Or(z0,z1),T()) -> False() isConsTerm(T(),And(z0,z1)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(z0,z1)) -> False() isConsTerm(T(),T()) -> True() isOp(And(z0,z1)) -> True() isOp(F()) -> False() isOp(Or(z0,z1)) -> 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,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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0,c40/0 ,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/4,c_6/4,c_7/0 ,c_8/0,c_9/0,c_10/1,c_11/0,c_12/4,c_13/4,c_14/0,c_15/1,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,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0 ,c_53/0,c_54/0,c_55/0,c_56/3,c_57/0,c_58/0,c_59/0,c_60/1,c_61/0,c_62/3,c_63/0,c_64/1,c_65/0,c_66/0,c_67/0 ,c_68/0,c_69/0,c_70/0,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/0,c_77/0,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0 ,c_83/0,c_84/0,c_85/0,c_86/0,c_87/0,c_88/0,c_89/0,c_90/0,c_91/0,c_92/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND# ,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm# ,isOp#} and constructors {And,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6 ,c7,c8,c9} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {1,2,3,4,7,8,9,11,14,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,42,43} by application of Pre({1,2,3,4,7,8,9,11,14,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,42 ,43}) = {5,6,12,13,15}. Here rules are labelled as follows: 1: BOOL#(And(z0,z1)) -> c_1() 2: BOOL#(F()) -> c_2() 3: BOOL#(Or(z0,z1)) -> c_3() 4: BOOL#(T()) -> c_4() 5: CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)) 6: CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)) 7: CONJ#(F()) -> c_7() 8: CONJ#(Or(z0,z1)) -> c_8() 9: CONJ#(T()) -> c_9() 10: DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) 11: DISJ#(F()) -> c_11() 12: DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)) 13: DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)) 14: DISJ#(T()) -> c_14() 15: DISJCONJ#(z0) -> c_15(DISJ#(z0)) 16: GETFIRST#(And(z0,z1)) -> c_16() 17: GETFIRST#(Or(z0,z1)) -> c_17() 18: GETSECOND#(And(z0,z1)) -> c_18() 19: GETSECOND#(Or(z0,z1)) -> c_19() 20: ISAND#(And(z0,z1)) -> c_20() 21: ISAND#(F()) -> c_21() 22: ISAND#(Or(z0,z1)) -> c_22() 23: ISAND#(T()) -> c_23() 24: ISCONSTERM#(And(z0,z1),And(z2,z3)) -> c_24() 25: ISCONSTERM#(And(z0,z1),F()) -> c_25() 26: ISCONSTERM#(And(z0,z1),Or(z2,z3)) -> c_26() 27: ISCONSTERM#(And(z0,z1),T()) -> c_27() 28: ISCONSTERM#(F(),And(z0,z1)) -> c_28() 29: ISCONSTERM#(F(),F()) -> c_29() 30: ISCONSTERM#(F(),Or(z0,z1)) -> c_30() 31: ISCONSTERM#(F(),T()) -> c_31() 32: ISCONSTERM#(Or(z0,z1),And(z2,z3)) -> c_32() 33: ISCONSTERM#(Or(z0,z1),F()) -> c_33() 34: ISCONSTERM#(Or(z0,z1),Or(z2,z3)) -> c_34() 35: ISCONSTERM#(Or(z0,z1),T()) -> c_35() 36: ISCONSTERM#(T(),And(z0,z1)) -> c_36() 37: ISCONSTERM#(T(),F()) -> c_37() 38: ISCONSTERM#(T(),Or(z0,z1)) -> c_38() 39: ISCONSTERM#(T(),T()) -> c_39() 40: ISOP#(And(z0,z1)) -> c_40() 41: ISOP#(F()) -> c_41() 42: ISOP#(Or(z0,z1)) -> c_42() 43: ISOP#(T()) -> c_43() 44: AND#(False(),False()) -> c_44() 45: AND#(False(),True()) -> c_45() 46: AND#(True(),False()) -> c_46() 47: AND#(True(),True()) -> c_47() 48: and#(False(),False()) -> c_48() 49: and#(False(),True()) -> c_49() 50: and#(True(),False()) -> c_50() 51: and#(True(),True()) -> c_51() 52: bool#(And(z0,z1)) -> c_52() 53: bool#(F()) -> c_53() 54: bool#(Or(z0,z1)) -> c_54() 55: bool#(T()) -> c_55() 56: conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)) 57: conj#(F()) -> c_57() 58: conj#(Or(z0,z1)) -> c_58() 59: conj#(T()) -> c_59() 60: disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))) 61: disj#(F()) -> c_61() 62: disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)) 63: disj#(T()) -> c_63() 64: disjconj#(z0) -> c_64(disj#(z0)) 65: getFirst#(And(z0,z1)) -> c_65() 66: getFirst#(Or(z0,z1)) -> c_66() 67: getSecond#(And(z0,z1)) -> c_67() 68: getSecond#(Or(z0,z1)) -> c_68() 69: isAnd#(And(z0,z1)) -> c_69() 70: isAnd#(F()) -> c_70() 71: isAnd#(Or(z0,z1)) -> c_71() 72: isAnd#(T()) -> c_72() 73: isConsTerm#(And(z0,z1),And(z2,z3)) -> c_73() 74: isConsTerm#(And(z0,z1),F()) -> c_74() 75: isConsTerm#(And(z0,z1),Or(z2,z3)) -> c_75() 76: isConsTerm#(And(z0,z1),T()) -> c_76() 77: isConsTerm#(F(),And(z0,z1)) -> c_77() 78: isConsTerm#(F(),F()) -> c_78() 79: isConsTerm#(F(),Or(z0,z1)) -> c_79() 80: isConsTerm#(F(),T()) -> c_80() 81: isConsTerm#(Or(z0,z1),And(z2,z3)) -> c_81() 82: isConsTerm#(Or(z0,z1),F()) -> c_82() 83: isConsTerm#(Or(z0,z1),Or(z2,z3)) -> c_83() 84: isConsTerm#(Or(z0,z1),T()) -> c_84() 85: isConsTerm#(T(),And(z0,z1)) -> c_85() 86: isConsTerm#(T(),F()) -> c_86() 87: isConsTerm#(T(),Or(z0,z1)) -> c_87() 88: isConsTerm#(T(),T()) -> c_88() 89: isOp#(And(z0,z1)) -> c_89() 90: isOp#(F()) -> c_90() 91: isOp#(Or(z0,z1)) -> c_91() 92: isOp#(T()) -> c_92() ** Step 1.b:3: RemoveWeakSuffixes. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)) DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)) DISJCONJ#(z0) -> c_15(DISJ#(z0)) - Weak DPs: AND#(False(),False()) -> c_44() AND#(False(),True()) -> c_45() AND#(True(),False()) -> c_46() AND#(True(),True()) -> c_47() BOOL#(And(z0,z1)) -> c_1() BOOL#(F()) -> c_2() BOOL#(Or(z0,z1)) -> c_3() BOOL#(T()) -> c_4() CONJ#(F()) -> c_7() CONJ#(Or(z0,z1)) -> c_8() CONJ#(T()) -> c_9() DISJ#(F()) -> c_11() DISJ#(T()) -> c_14() GETFIRST#(And(z0,z1)) -> c_16() GETFIRST#(Or(z0,z1)) -> c_17() GETSECOND#(And(z0,z1)) -> c_18() GETSECOND#(Or(z0,z1)) -> c_19() ISAND#(And(z0,z1)) -> c_20() ISAND#(F()) -> c_21() ISAND#(Or(z0,z1)) -> c_22() ISAND#(T()) -> c_23() ISCONSTERM#(And(z0,z1),And(z2,z3)) -> c_24() ISCONSTERM#(And(z0,z1),F()) -> c_25() ISCONSTERM#(And(z0,z1),Or(z2,z3)) -> c_26() ISCONSTERM#(And(z0,z1),T()) -> c_27() ISCONSTERM#(F(),And(z0,z1)) -> c_28() ISCONSTERM#(F(),F()) -> c_29() ISCONSTERM#(F(),Or(z0,z1)) -> c_30() ISCONSTERM#(F(),T()) -> c_31() ISCONSTERM#(Or(z0,z1),And(z2,z3)) -> c_32() ISCONSTERM#(Or(z0,z1),F()) -> c_33() ISCONSTERM#(Or(z0,z1),Or(z2,z3)) -> c_34() ISCONSTERM#(Or(z0,z1),T()) -> c_35() ISCONSTERM#(T(),And(z0,z1)) -> c_36() ISCONSTERM#(T(),F()) -> c_37() ISCONSTERM#(T(),Or(z0,z1)) -> c_38() ISCONSTERM#(T(),T()) -> c_39() ISOP#(And(z0,z1)) -> c_40() ISOP#(F()) -> c_41() ISOP#(Or(z0,z1)) -> c_42() ISOP#(T()) -> c_43() and#(False(),False()) -> c_48() and#(False(),True()) -> c_49() and#(True(),False()) -> c_50() and#(True(),True()) -> c_51() bool#(And(z0,z1)) -> c_52() bool#(F()) -> c_53() bool#(Or(z0,z1)) -> c_54() bool#(T()) -> c_55() conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)) conj#(F()) -> c_57() conj#(Or(z0,z1)) -> c_58() conj#(T()) -> c_59() disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))) disj#(F()) -> c_61() disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)) disj#(T()) -> c_63() disjconj#(z0) -> c_64(disj#(z0)) getFirst#(And(z0,z1)) -> c_65() getFirst#(Or(z0,z1)) -> c_66() getSecond#(And(z0,z1)) -> c_67() getSecond#(Or(z0,z1)) -> c_68() isAnd#(And(z0,z1)) -> c_69() isAnd#(F()) -> c_70() isAnd#(Or(z0,z1)) -> c_71() isAnd#(T()) -> c_72() isConsTerm#(And(z0,z1),And(z2,z3)) -> c_73() isConsTerm#(And(z0,z1),F()) -> c_74() isConsTerm#(And(z0,z1),Or(z2,z3)) -> c_75() isConsTerm#(And(z0,z1),T()) -> c_76() isConsTerm#(F(),And(z0,z1)) -> c_77() isConsTerm#(F(),F()) -> c_78() isConsTerm#(F(),Or(z0,z1)) -> c_79() isConsTerm#(F(),T()) -> c_80() isConsTerm#(Or(z0,z1),And(z2,z3)) -> c_81() isConsTerm#(Or(z0,z1),F()) -> c_82() isConsTerm#(Or(z0,z1),Or(z2,z3)) -> c_83() isConsTerm#(Or(z0,z1),T()) -> c_84() isConsTerm#(T(),And(z0,z1)) -> c_85() isConsTerm#(T(),F()) -> c_86() isConsTerm#(T(),Or(z0,z1)) -> c_87() isConsTerm#(T(),T()) -> c_88() isOp#(And(z0,z1)) -> c_89() isOp#(F()) -> c_90() isOp#(Or(z0,z1)) -> c_91() isOp#(T()) -> c_92() - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() BOOL(And(z0,z1)) -> c16() BOOL(F()) -> c15() BOOL(Or(z0,z1)) -> c17() BOOL(T()) -> c14() CONJ(And(z0,z1)) -> c12(AND(disj(z0),conj(z0)),DISJ(z0)) CONJ(And(z0,z1)) -> c13(AND(disj(z0),conj(z0)),CONJ(z0)) CONJ(F()) -> c11() CONJ(Or(z0,z1)) -> c9() CONJ(T()) -> c10() DISJ(And(z0,z1)) -> c6(CONJ(And(z0,z1))) DISJ(F()) -> c5() DISJ(Or(z0,z1)) -> c7(AND(conj(z0),disj(z0)),CONJ(z0)) DISJ(Or(z0,z1)) -> c8(AND(conj(z0),disj(z0)),DISJ(z0)) DISJ(T()) -> c4() DISJCONJ(z0) -> c46(DISJ(z0)) GETFIRST(And(z0,z1)) -> c44() GETFIRST(Or(z0,z1)) -> c45() GETSECOND(And(z0,z1)) -> c42() GETSECOND(Or(z0,z1)) -> c43() ISAND(And(z0,z1)) -> c40() ISAND(F()) -> c39() ISAND(Or(z0,z1)) -> c41() ISAND(T()) -> c38() ISCONSTERM(And(z0,z1),And(z2,z3)) -> c28() ISCONSTERM(And(z0,z1),F()) -> c27() ISCONSTERM(And(z0,z1),Or(z2,z3)) -> c29() ISCONSTERM(And(z0,z1),T()) -> c26() ISCONSTERM(F(),And(z0,z1)) -> c24() ISCONSTERM(F(),F()) -> c23() ISCONSTERM(F(),Or(z0,z1)) -> c25() ISCONSTERM(F(),T()) -> c22() ISCONSTERM(Or(z0,z1),And(z2,z3)) -> c32() ISCONSTERM(Or(z0,z1),F()) -> c31() ISCONSTERM(Or(z0,z1),Or(z2,z3)) -> c33() ISCONSTERM(Or(z0,z1),T()) -> c30() ISCONSTERM(T(),And(z0,z1)) -> c20() ISCONSTERM(T(),F()) -> c19() ISCONSTERM(T(),Or(z0,z1)) -> c21() ISCONSTERM(T(),T()) -> c18() ISOP(And(z0,z1)) -> c36() ISOP(F()) -> c35() ISOP(Or(z0,z1)) -> c37() ISOP(T()) -> c34() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(z0,z1)) -> False() bool(F()) -> True() bool(Or(z0,z1)) -> False() bool(T()) -> True() conj(And(z0,z1)) -> and(disj(z0),conj(z0)) conj(F()) -> True() conj(Or(z0,z1)) -> False() conj(T()) -> True() disj(And(z0,z1)) -> conj(And(z0,z1)) disj(F()) -> True() disj(Or(z0,z1)) -> and(conj(z0),disj(z0)) disj(T()) -> True() disjconj(z0) -> disj(z0) getFirst(And(z0,z1)) -> z0 getFirst(Or(z0,z1)) -> z0 getSecond(And(z0,z1)) -> z0 getSecond(Or(z0,z1)) -> z0 isAnd(And(z0,z1)) -> True() isAnd(F()) -> False() isAnd(Or(z0,z1)) -> False() isAnd(T()) -> False() isConsTerm(And(z0,z1),And(z2,z3)) -> True() isConsTerm(And(z0,z1),F()) -> False() isConsTerm(And(z0,z1),Or(z2,z3)) -> False() isConsTerm(And(z0,z1),T()) -> False() isConsTerm(F(),And(z0,z1)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(z0,z1)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(z0,z1),And(z2,z3)) -> False() isConsTerm(Or(z0,z1),F()) -> False() isConsTerm(Or(z0,z1),Or(z2,z3)) -> True() isConsTerm(Or(z0,z1),T()) -> False() isConsTerm(T(),And(z0,z1)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(z0,z1)) -> False() isConsTerm(T(),T()) -> True() isOp(And(z0,z1)) -> True() isOp(F()) -> False() isOp(Or(z0,z1)) -> 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,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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0,c40/0 ,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/4,c_6/4,c_7/0 ,c_8/0,c_9/0,c_10/1,c_11/0,c_12/4,c_13/4,c_14/0,c_15/1,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,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0 ,c_53/0,c_54/0,c_55/0,c_56/3,c_57/0,c_58/0,c_59/0,c_60/1,c_61/0,c_62/3,c_63/0,c_64/1,c_65/0,c_66/0,c_67/0 ,c_68/0,c_69/0,c_70/0,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/0,c_77/0,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0 ,c_83/0,c_84/0,c_85/0,c_86/0,c_87/0,c_88/0,c_89/0,c_90/0,c_91/0,c_92/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND# ,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm# ,isOp#} and constructors {And,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6 ,c7,c8,c9} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)) -->_2 disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)):62 -->_2 disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))):60 -->_3 conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)):56 -->_4 DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)):5 -->_4 DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)):4 -->_4 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 -->_2 disj#(T()) -> c_63():63 -->_2 disj#(F()) -> c_61():61 -->_3 conj#(T()) -> c_59():59 -->_3 conj#(Or(z0,z1)) -> c_58():58 -->_3 conj#(F()) -> c_57():57 -->_4 DISJ#(T()) -> c_14():19 -->_4 DISJ#(F()) -> c_11():18 -->_1 AND#(True(),True()) -> c_47():10 -->_1 AND#(True(),False()) -> c_46():9 -->_1 AND#(False(),True()) -> c_45():8 -->_1 AND#(False(),False()) -> c_44():7 2:S:CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)) -->_2 disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)):62 -->_2 disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))):60 -->_3 conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)):56 -->_2 disj#(T()) -> c_63():63 -->_2 disj#(F()) -> c_61():61 -->_3 conj#(T()) -> c_59():59 -->_3 conj#(Or(z0,z1)) -> c_58():58 -->_3 conj#(F()) -> c_57():57 -->_4 CONJ#(T()) -> c_9():17 -->_4 CONJ#(Or(z0,z1)) -> c_8():16 -->_4 CONJ#(F()) -> c_7():15 -->_1 AND#(True(),True()) -> c_47():10 -->_1 AND#(True(),False()) -> c_46():9 -->_1 AND#(False(),True()) -> c_45():8 -->_1 AND#(False(),False()) -> c_44():7 -->_4 CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)):2 -->_4 CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)):1 3:S:DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) -->_1 CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)):2 -->_1 CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)):1 4:S:DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)) -->_3 disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)):62 -->_3 disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))):60 -->_2 conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)):56 -->_3 disj#(T()) -> c_63():63 -->_3 disj#(F()) -> c_61():61 -->_2 conj#(T()) -> c_59():59 -->_2 conj#(Or(z0,z1)) -> c_58():58 -->_2 conj#(F()) -> c_57():57 -->_4 CONJ#(T()) -> c_9():17 -->_4 CONJ#(Or(z0,z1)) -> c_8():16 -->_4 CONJ#(F()) -> c_7():15 -->_1 AND#(True(),True()) -> c_47():10 -->_1 AND#(True(),False()) -> c_46():9 -->_1 AND#(False(),True()) -> c_45():8 -->_1 AND#(False(),False()) -> c_44():7 -->_4 CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)):2 -->_4 CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)):1 5:S:DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)) -->_3 disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)):62 -->_3 disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))):60 -->_2 conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)):56 -->_3 disj#(T()) -> c_63():63 -->_3 disj#(F()) -> c_61():61 -->_2 conj#(T()) -> c_59():59 -->_2 conj#(Or(z0,z1)) -> c_58():58 -->_2 conj#(F()) -> c_57():57 -->_4 DISJ#(T()) -> c_14():19 -->_4 DISJ#(F()) -> c_11():18 -->_1 AND#(True(),True()) -> c_47():10 -->_1 AND#(True(),False()) -> c_46():9 -->_1 AND#(False(),True()) -> c_45():8 -->_1 AND#(False(),False()) -> c_44():7 -->_4 DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)):5 -->_4 DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)):4 -->_4 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 6:S:DISJCONJ#(z0) -> c_15(DISJ#(z0)) -->_1 DISJ#(T()) -> c_14():19 -->_1 DISJ#(F()) -> c_11():18 -->_1 DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)):5 -->_1 DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)):4 -->_1 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 7:W:AND#(False(),False()) -> c_44() 8:W:AND#(False(),True()) -> c_45() 9:W:AND#(True(),False()) -> c_46() 10:W:AND#(True(),True()) -> c_47() 11:W:BOOL#(And(z0,z1)) -> c_1() 12:W:BOOL#(F()) -> c_2() 13:W:BOOL#(Or(z0,z1)) -> c_3() 14:W:BOOL#(T()) -> c_4() 15:W:CONJ#(F()) -> c_7() 16:W:CONJ#(Or(z0,z1)) -> c_8() 17:W:CONJ#(T()) -> c_9() 18:W:DISJ#(F()) -> c_11() 19:W:DISJ#(T()) -> c_14() 20:W:GETFIRST#(And(z0,z1)) -> c_16() 21:W:GETFIRST#(Or(z0,z1)) -> c_17() 22:W:GETSECOND#(And(z0,z1)) -> c_18() 23:W:GETSECOND#(Or(z0,z1)) -> c_19() 24:W:ISAND#(And(z0,z1)) -> c_20() 25:W:ISAND#(F()) -> c_21() 26:W:ISAND#(Or(z0,z1)) -> c_22() 27:W:ISAND#(T()) -> c_23() 28:W:ISCONSTERM#(And(z0,z1),And(z2,z3)) -> c_24() 29:W:ISCONSTERM#(And(z0,z1),F()) -> c_25() 30:W:ISCONSTERM#(And(z0,z1),Or(z2,z3)) -> c_26() 31:W:ISCONSTERM#(And(z0,z1),T()) -> c_27() 32:W:ISCONSTERM#(F(),And(z0,z1)) -> c_28() 33:W:ISCONSTERM#(F(),F()) -> c_29() 34:W:ISCONSTERM#(F(),Or(z0,z1)) -> c_30() 35:W:ISCONSTERM#(F(),T()) -> c_31() 36:W:ISCONSTERM#(Or(z0,z1),And(z2,z3)) -> c_32() 37:W:ISCONSTERM#(Or(z0,z1),F()) -> c_33() 38:W:ISCONSTERM#(Or(z0,z1),Or(z2,z3)) -> c_34() 39:W:ISCONSTERM#(Or(z0,z1),T()) -> c_35() 40:W:ISCONSTERM#(T(),And(z0,z1)) -> c_36() 41:W:ISCONSTERM#(T(),F()) -> c_37() 42:W:ISCONSTERM#(T(),Or(z0,z1)) -> c_38() 43:W:ISCONSTERM#(T(),T()) -> c_39() 44:W:ISOP#(And(z0,z1)) -> c_40() 45:W:ISOP#(F()) -> c_41() 46:W:ISOP#(Or(z0,z1)) -> c_42() 47:W:ISOP#(T()) -> c_43() 48:W:and#(False(),False()) -> c_48() 49:W:and#(False(),True()) -> c_49() 50:W:and#(True(),False()) -> c_50() 51:W:and#(True(),True()) -> c_51() 52:W:bool#(And(z0,z1)) -> c_52() 53:W:bool#(F()) -> c_53() 54:W:bool#(Or(z0,z1)) -> c_54() 55:W:bool#(T()) -> c_55() 56:W:conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)) -->_2 disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)):62 -->_2 disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))):60 -->_2 disj#(T()) -> c_63():63 -->_2 disj#(F()) -> c_61():61 -->_3 conj#(T()) -> c_59():59 -->_3 conj#(Or(z0,z1)) -> c_58():58 -->_3 conj#(F()) -> c_57():57 -->_3 conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)):56 -->_1 and#(True(),True()) -> c_51():51 -->_1 and#(True(),False()) -> c_50():50 -->_1 and#(False(),True()) -> c_49():49 -->_1 and#(False(),False()) -> c_48():48 57:W:conj#(F()) -> c_57() 58:W:conj#(Or(z0,z1)) -> c_58() 59:W:conj#(T()) -> c_59() 60:W:disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))) -->_1 conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)):56 61:W:disj#(F()) -> c_61() 62:W:disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)) -->_3 disj#(T()) -> c_63():63 -->_3 disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)):62 -->_3 disj#(F()) -> c_61():61 -->_3 disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))):60 -->_2 conj#(T()) -> c_59():59 -->_2 conj#(Or(z0,z1)) -> c_58():58 -->_2 conj#(F()) -> c_57():57 -->_2 conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)):56 -->_1 and#(True(),True()) -> c_51():51 -->_1 and#(True(),False()) -> c_50():50 -->_1 and#(False(),True()) -> c_49():49 -->_1 and#(False(),False()) -> c_48():48 63:W:disj#(T()) -> c_63() 64:W:disjconj#(z0) -> c_64(disj#(z0)) -->_1 disj#(T()) -> c_63():63 -->_1 disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)):62 -->_1 disj#(F()) -> c_61():61 -->_1 disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))):60 65:W:getFirst#(And(z0,z1)) -> c_65() 66:W:getFirst#(Or(z0,z1)) -> c_66() 67:W:getSecond#(And(z0,z1)) -> c_67() 68:W:getSecond#(Or(z0,z1)) -> c_68() 69:W:isAnd#(And(z0,z1)) -> c_69() 70:W:isAnd#(F()) -> c_70() 71:W:isAnd#(Or(z0,z1)) -> c_71() 72:W:isAnd#(T()) -> c_72() 73:W:isConsTerm#(And(z0,z1),And(z2,z3)) -> c_73() 74:W:isConsTerm#(And(z0,z1),F()) -> c_74() 75:W:isConsTerm#(And(z0,z1),Or(z2,z3)) -> c_75() 76:W:isConsTerm#(And(z0,z1),T()) -> c_76() 77:W:isConsTerm#(F(),And(z0,z1)) -> c_77() 78:W:isConsTerm#(F(),F()) -> c_78() 79:W:isConsTerm#(F(),Or(z0,z1)) -> c_79() 80:W:isConsTerm#(F(),T()) -> c_80() 81:W:isConsTerm#(Or(z0,z1),And(z2,z3)) -> c_81() 82:W:isConsTerm#(Or(z0,z1),F()) -> c_82() 83:W:isConsTerm#(Or(z0,z1),Or(z2,z3)) -> c_83() 84:W:isConsTerm#(Or(z0,z1),T()) -> c_84() 85:W:isConsTerm#(T(),And(z0,z1)) -> c_85() 86:W:isConsTerm#(T(),F()) -> c_86() 87:W:isConsTerm#(T(),Or(z0,z1)) -> c_87() 88:W:isConsTerm#(T(),T()) -> c_88() 89:W:isOp#(And(z0,z1)) -> c_89() 90:W:isOp#(F()) -> c_90() 91:W:isOp#(Or(z0,z1)) -> c_91() 92:W:isOp#(T()) -> c_92() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 92: isOp#(T()) -> c_92() 91: isOp#(Or(z0,z1)) -> c_91() 90: isOp#(F()) -> c_90() 89: isOp#(And(z0,z1)) -> c_89() 88: isConsTerm#(T(),T()) -> c_88() 87: isConsTerm#(T(),Or(z0,z1)) -> c_87() 86: isConsTerm#(T(),F()) -> c_86() 85: isConsTerm#(T(),And(z0,z1)) -> c_85() 84: isConsTerm#(Or(z0,z1),T()) -> c_84() 83: isConsTerm#(Or(z0,z1),Or(z2,z3)) -> c_83() 82: isConsTerm#(Or(z0,z1),F()) -> c_82() 81: isConsTerm#(Or(z0,z1),And(z2,z3)) -> c_81() 80: isConsTerm#(F(),T()) -> c_80() 79: isConsTerm#(F(),Or(z0,z1)) -> c_79() 78: isConsTerm#(F(),F()) -> c_78() 77: isConsTerm#(F(),And(z0,z1)) -> c_77() 76: isConsTerm#(And(z0,z1),T()) -> c_76() 75: isConsTerm#(And(z0,z1),Or(z2,z3)) -> c_75() 74: isConsTerm#(And(z0,z1),F()) -> c_74() 73: isConsTerm#(And(z0,z1),And(z2,z3)) -> c_73() 72: isAnd#(T()) -> c_72() 71: isAnd#(Or(z0,z1)) -> c_71() 70: isAnd#(F()) -> c_70() 69: isAnd#(And(z0,z1)) -> c_69() 68: getSecond#(Or(z0,z1)) -> c_68() 67: getSecond#(And(z0,z1)) -> c_67() 66: getFirst#(Or(z0,z1)) -> c_66() 65: getFirst#(And(z0,z1)) -> c_65() 64: disjconj#(z0) -> c_64(disj#(z0)) 55: bool#(T()) -> c_55() 54: bool#(Or(z0,z1)) -> c_54() 53: bool#(F()) -> c_53() 52: bool#(And(z0,z1)) -> c_52() 47: ISOP#(T()) -> c_43() 46: ISOP#(Or(z0,z1)) -> c_42() 45: ISOP#(F()) -> c_41() 44: ISOP#(And(z0,z1)) -> c_40() 43: ISCONSTERM#(T(),T()) -> c_39() 42: ISCONSTERM#(T(),Or(z0,z1)) -> c_38() 41: ISCONSTERM#(T(),F()) -> c_37() 40: ISCONSTERM#(T(),And(z0,z1)) -> c_36() 39: ISCONSTERM#(Or(z0,z1),T()) -> c_35() 38: ISCONSTERM#(Or(z0,z1),Or(z2,z3)) -> c_34() 37: ISCONSTERM#(Or(z0,z1),F()) -> c_33() 36: ISCONSTERM#(Or(z0,z1),And(z2,z3)) -> c_32() 35: ISCONSTERM#(F(),T()) -> c_31() 34: ISCONSTERM#(F(),Or(z0,z1)) -> c_30() 33: ISCONSTERM#(F(),F()) -> c_29() 32: ISCONSTERM#(F(),And(z0,z1)) -> c_28() 31: ISCONSTERM#(And(z0,z1),T()) -> c_27() 30: ISCONSTERM#(And(z0,z1),Or(z2,z3)) -> c_26() 29: ISCONSTERM#(And(z0,z1),F()) -> c_25() 28: ISCONSTERM#(And(z0,z1),And(z2,z3)) -> c_24() 27: ISAND#(T()) -> c_23() 26: ISAND#(Or(z0,z1)) -> c_22() 25: ISAND#(F()) -> c_21() 24: ISAND#(And(z0,z1)) -> c_20() 23: GETSECOND#(Or(z0,z1)) -> c_19() 22: GETSECOND#(And(z0,z1)) -> c_18() 21: GETFIRST#(Or(z0,z1)) -> c_17() 20: GETFIRST#(And(z0,z1)) -> c_16() 14: BOOL#(T()) -> c_4() 13: BOOL#(Or(z0,z1)) -> c_3() 12: BOOL#(F()) -> c_2() 11: BOOL#(And(z0,z1)) -> c_1() 15: CONJ#(F()) -> c_7() 16: CONJ#(Or(z0,z1)) -> c_8() 17: CONJ#(T()) -> c_9() 7: AND#(False(),False()) -> c_44() 8: AND#(False(),True()) -> c_45() 9: AND#(True(),False()) -> c_46() 10: AND#(True(),True()) -> c_47() 18: DISJ#(F()) -> c_11() 19: DISJ#(T()) -> c_14() 62: disj#(Or(z0,z1)) -> c_62(and#(conj(z0),disj(z0)),conj#(z0),disj#(z0)) 56: conj#(And(z0,z1)) -> c_56(and#(disj(z0),conj(z0)),disj#(z0),conj#(z0)) 60: disj#(And(z0,z1)) -> c_60(conj#(And(z0,z1))) 48: and#(False(),False()) -> c_48() 49: and#(False(),True()) -> c_49() 50: and#(True(),False()) -> c_50() 51: and#(True(),True()) -> c_51() 57: conj#(F()) -> c_57() 58: conj#(Or(z0,z1)) -> c_58() 59: conj#(T()) -> c_59() 61: disj#(F()) -> c_61() 63: disj#(T()) -> c_63() ** Step 1.b:4: SimplifyRHS. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)) DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)) DISJCONJ#(z0) -> c_15(DISJ#(z0)) - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() BOOL(And(z0,z1)) -> c16() BOOL(F()) -> c15() BOOL(Or(z0,z1)) -> c17() BOOL(T()) -> c14() CONJ(And(z0,z1)) -> c12(AND(disj(z0),conj(z0)),DISJ(z0)) CONJ(And(z0,z1)) -> c13(AND(disj(z0),conj(z0)),CONJ(z0)) CONJ(F()) -> c11() CONJ(Or(z0,z1)) -> c9() CONJ(T()) -> c10() DISJ(And(z0,z1)) -> c6(CONJ(And(z0,z1))) DISJ(F()) -> c5() DISJ(Or(z0,z1)) -> c7(AND(conj(z0),disj(z0)),CONJ(z0)) DISJ(Or(z0,z1)) -> c8(AND(conj(z0),disj(z0)),DISJ(z0)) DISJ(T()) -> c4() DISJCONJ(z0) -> c46(DISJ(z0)) GETFIRST(And(z0,z1)) -> c44() GETFIRST(Or(z0,z1)) -> c45() GETSECOND(And(z0,z1)) -> c42() GETSECOND(Or(z0,z1)) -> c43() ISAND(And(z0,z1)) -> c40() ISAND(F()) -> c39() ISAND(Or(z0,z1)) -> c41() ISAND(T()) -> c38() ISCONSTERM(And(z0,z1),And(z2,z3)) -> c28() ISCONSTERM(And(z0,z1),F()) -> c27() ISCONSTERM(And(z0,z1),Or(z2,z3)) -> c29() ISCONSTERM(And(z0,z1),T()) -> c26() ISCONSTERM(F(),And(z0,z1)) -> c24() ISCONSTERM(F(),F()) -> c23() ISCONSTERM(F(),Or(z0,z1)) -> c25() ISCONSTERM(F(),T()) -> c22() ISCONSTERM(Or(z0,z1),And(z2,z3)) -> c32() ISCONSTERM(Or(z0,z1),F()) -> c31() ISCONSTERM(Or(z0,z1),Or(z2,z3)) -> c33() ISCONSTERM(Or(z0,z1),T()) -> c30() ISCONSTERM(T(),And(z0,z1)) -> c20() ISCONSTERM(T(),F()) -> c19() ISCONSTERM(T(),Or(z0,z1)) -> c21() ISCONSTERM(T(),T()) -> c18() ISOP(And(z0,z1)) -> c36() ISOP(F()) -> c35() ISOP(Or(z0,z1)) -> c37() ISOP(T()) -> c34() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(z0,z1)) -> False() bool(F()) -> True() bool(Or(z0,z1)) -> False() bool(T()) -> True() conj(And(z0,z1)) -> and(disj(z0),conj(z0)) conj(F()) -> True() conj(Or(z0,z1)) -> False() conj(T()) -> True() disj(And(z0,z1)) -> conj(And(z0,z1)) disj(F()) -> True() disj(Or(z0,z1)) -> and(conj(z0),disj(z0)) disj(T()) -> True() disjconj(z0) -> disj(z0) getFirst(And(z0,z1)) -> z0 getFirst(Or(z0,z1)) -> z0 getSecond(And(z0,z1)) -> z0 getSecond(Or(z0,z1)) -> z0 isAnd(And(z0,z1)) -> True() isAnd(F()) -> False() isAnd(Or(z0,z1)) -> False() isAnd(T()) -> False() isConsTerm(And(z0,z1),And(z2,z3)) -> True() isConsTerm(And(z0,z1),F()) -> False() isConsTerm(And(z0,z1),Or(z2,z3)) -> False() isConsTerm(And(z0,z1),T()) -> False() isConsTerm(F(),And(z0,z1)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(z0,z1)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(z0,z1),And(z2,z3)) -> False() isConsTerm(Or(z0,z1),F()) -> False() isConsTerm(Or(z0,z1),Or(z2,z3)) -> True() isConsTerm(Or(z0,z1),T()) -> False() isConsTerm(T(),And(z0,z1)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(z0,z1)) -> False() isConsTerm(T(),T()) -> True() isOp(And(z0,z1)) -> True() isOp(F()) -> False() isOp(Or(z0,z1)) -> 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,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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0,c40/0 ,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/4,c_6/4,c_7/0 ,c_8/0,c_9/0,c_10/1,c_11/0,c_12/4,c_13/4,c_14/0,c_15/1,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,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0 ,c_53/0,c_54/0,c_55/0,c_56/3,c_57/0,c_58/0,c_59/0,c_60/1,c_61/0,c_62/3,c_63/0,c_64/1,c_65/0,c_66/0,c_67/0 ,c_68/0,c_69/0,c_70/0,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/0,c_77/0,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0 ,c_83/0,c_84/0,c_85/0,c_86/0,c_87/0,c_88/0,c_89/0,c_90/0,c_91/0,c_92/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND# ,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm# ,isOp#} and constructors {And,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6 ,c7,c8,c9} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)) -->_4 DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)):5 -->_4 DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)):4 -->_4 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 2:S:CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)) -->_4 CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)):2 -->_4 CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)):1 3:S:DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) -->_1 CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)):2 -->_1 CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)):1 4:S:DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)) -->_4 CONJ#(And(z0,z1)) -> c_6(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),CONJ#(z0)):2 -->_4 CONJ#(And(z0,z1)) -> c_5(AND#(disj(z0),conj(z0)),disj#(z0),conj#(z0),DISJ#(z0)):1 5:S:DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)) -->_4 DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)):5 -->_4 DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)):4 -->_4 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 6:S:DISJCONJ#(z0) -> c_15(DISJ#(z0)) -->_1 DISJ#(Or(z0,z1)) -> c_13(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),DISJ#(z0)):5 -->_1 DISJ#(Or(z0,z1)) -> c_12(AND#(conj(z0),disj(z0)),conj#(z0),disj#(z0),CONJ#(z0)):4 -->_1 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)) ** Step 1.b:5: UsableRules. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)) DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)) DISJCONJ#(z0) -> c_15(DISJ#(z0)) - Weak TRS: AND(False(),False()) -> c() AND(False(),True()) -> c2() AND(True(),False()) -> c1() AND(True(),True()) -> c3() BOOL(And(z0,z1)) -> c16() BOOL(F()) -> c15() BOOL(Or(z0,z1)) -> c17() BOOL(T()) -> c14() CONJ(And(z0,z1)) -> c12(AND(disj(z0),conj(z0)),DISJ(z0)) CONJ(And(z0,z1)) -> c13(AND(disj(z0),conj(z0)),CONJ(z0)) CONJ(F()) -> c11() CONJ(Or(z0,z1)) -> c9() CONJ(T()) -> c10() DISJ(And(z0,z1)) -> c6(CONJ(And(z0,z1))) DISJ(F()) -> c5() DISJ(Or(z0,z1)) -> c7(AND(conj(z0),disj(z0)),CONJ(z0)) DISJ(Or(z0,z1)) -> c8(AND(conj(z0),disj(z0)),DISJ(z0)) DISJ(T()) -> c4() DISJCONJ(z0) -> c46(DISJ(z0)) GETFIRST(And(z0,z1)) -> c44() GETFIRST(Or(z0,z1)) -> c45() GETSECOND(And(z0,z1)) -> c42() GETSECOND(Or(z0,z1)) -> c43() ISAND(And(z0,z1)) -> c40() ISAND(F()) -> c39() ISAND(Or(z0,z1)) -> c41() ISAND(T()) -> c38() ISCONSTERM(And(z0,z1),And(z2,z3)) -> c28() ISCONSTERM(And(z0,z1),F()) -> c27() ISCONSTERM(And(z0,z1),Or(z2,z3)) -> c29() ISCONSTERM(And(z0,z1),T()) -> c26() ISCONSTERM(F(),And(z0,z1)) -> c24() ISCONSTERM(F(),F()) -> c23() ISCONSTERM(F(),Or(z0,z1)) -> c25() ISCONSTERM(F(),T()) -> c22() ISCONSTERM(Or(z0,z1),And(z2,z3)) -> c32() ISCONSTERM(Or(z0,z1),F()) -> c31() ISCONSTERM(Or(z0,z1),Or(z2,z3)) -> c33() ISCONSTERM(Or(z0,z1),T()) -> c30() ISCONSTERM(T(),And(z0,z1)) -> c20() ISCONSTERM(T(),F()) -> c19() ISCONSTERM(T(),Or(z0,z1)) -> c21() ISCONSTERM(T(),T()) -> c18() ISOP(And(z0,z1)) -> c36() ISOP(F()) -> c35() ISOP(Or(z0,z1)) -> c37() ISOP(T()) -> c34() and(False(),False()) -> False() and(False(),True()) -> False() and(True(),False()) -> False() and(True(),True()) -> True() bool(And(z0,z1)) -> False() bool(F()) -> True() bool(Or(z0,z1)) -> False() bool(T()) -> True() conj(And(z0,z1)) -> and(disj(z0),conj(z0)) conj(F()) -> True() conj(Or(z0,z1)) -> False() conj(T()) -> True() disj(And(z0,z1)) -> conj(And(z0,z1)) disj(F()) -> True() disj(Or(z0,z1)) -> and(conj(z0),disj(z0)) disj(T()) -> True() disjconj(z0) -> disj(z0) getFirst(And(z0,z1)) -> z0 getFirst(Or(z0,z1)) -> z0 getSecond(And(z0,z1)) -> z0 getSecond(Or(z0,z1)) -> z0 isAnd(And(z0,z1)) -> True() isAnd(F()) -> False() isAnd(Or(z0,z1)) -> False() isAnd(T()) -> False() isConsTerm(And(z0,z1),And(z2,z3)) -> True() isConsTerm(And(z0,z1),F()) -> False() isConsTerm(And(z0,z1),Or(z2,z3)) -> False() isConsTerm(And(z0,z1),T()) -> False() isConsTerm(F(),And(z0,z1)) -> False() isConsTerm(F(),F()) -> True() isConsTerm(F(),Or(z0,z1)) -> False() isConsTerm(F(),T()) -> False() isConsTerm(Or(z0,z1),And(z2,z3)) -> False() isConsTerm(Or(z0,z1),F()) -> False() isConsTerm(Or(z0,z1),Or(z2,z3)) -> True() isConsTerm(Or(z0,z1),T()) -> False() isConsTerm(T(),And(z0,z1)) -> False() isConsTerm(T(),F()) -> False() isConsTerm(T(),Or(z0,z1)) -> False() isConsTerm(T(),T()) -> True() isOp(And(z0,z1)) -> True() isOp(F()) -> False() isOp(Or(z0,z1)) -> 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,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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0,c40/0 ,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,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,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0 ,c_53/0,c_54/0,c_55/0,c_56/3,c_57/0,c_58/0,c_59/0,c_60/1,c_61/0,c_62/3,c_63/0,c_64/1,c_65/0,c_66/0,c_67/0 ,c_68/0,c_69/0,c_70/0,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/0,c_77/0,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0 ,c_83/0,c_84/0,c_85/0,c_86/0,c_87/0,c_88/0,c_89/0,c_90/0,c_91/0,c_92/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND# ,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm# ,isOp#} and constructors {And,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6 ,c7,c8,c9} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)) DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)) DISJCONJ#(z0) -> c_15(DISJ#(z0)) ** Step 1.b:6: RemoveHeads. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)) DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)) DISJCONJ#(z0) -> c_15(DISJ#(z0)) - 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,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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0,c40/0 ,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,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,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0 ,c_53/0,c_54/0,c_55/0,c_56/3,c_57/0,c_58/0,c_59/0,c_60/1,c_61/0,c_62/3,c_63/0,c_64/1,c_65/0,c_66/0,c_67/0 ,c_68/0,c_69/0,c_70/0,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/0,c_77/0,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0 ,c_83/0,c_84/0,c_85/0,c_86/0,c_87/0,c_88/0,c_89/0,c_90/0,c_91/0,c_92/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND# ,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm# ,isOp#} and constructors {And,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6 ,c7,c8,c9} + Applied Processor: RemoveHeads + Details: Consider the dependency graph 1:S:CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)) -->_1 DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)):5 -->_1 DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)):4 -->_1 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 2:S:CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)) -->_1 CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)):2 -->_1 CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)):1 3:S:DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) -->_1 CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)):2 -->_1 CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)):1 4:S:DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)) -->_1 CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)):2 -->_1 CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)):1 5:S:DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)) -->_1 DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)):5 -->_1 DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)):4 -->_1 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 6:S:DISJCONJ#(z0) -> c_15(DISJ#(z0)) -->_1 DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)):5 -->_1 DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)):4 -->_1 DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))):3 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). [(6,DISJCONJ#(z0) -> c_15(DISJ#(z0)))] ** Step 1.b:7: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)) DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)) - 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,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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0,c40/0 ,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,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,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0 ,c_53/0,c_54/0,c_55/0,c_56/3,c_57/0,c_58/0,c_59/0,c_60/1,c_61/0,c_62/3,c_63/0,c_64/1,c_65/0,c_66/0,c_67/0 ,c_68/0,c_69/0,c_70/0,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/0,c_77/0,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0 ,c_83/0,c_84/0,c_85/0,c_86/0,c_87/0,c_88/0,c_89/0,c_90/0,c_91/0,c_92/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND# ,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm# ,isOp#} and constructors {And,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6 ,c7,c8,c9} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_10) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1} Following symbols are considered usable: {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND#,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj# ,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm#,isOp#} TcT has computed the following interpretation: p(AND) = [0] p(And) = [1] x1 + [1] x2 + [12] p(BOOL) = [0] p(CONJ) = [0] p(DISJ) = [0] p(DISJCONJ) = [0] p(F) = [0] p(False) = [0] p(GETFIRST) = [0] p(GETSECOND) = [0] p(ISAND) = [0] p(ISCONSTERM) = [0] p(ISOP) = [0] p(Or) = [1] x1 + [1] x2 + [1] p(T) = [0] p(True) = [0] p(and) = [0] p(bool) = [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [1] x2 + [0] p(c13) = [1] x1 + [1] x2 + [0] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [0] p(c19) = [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c26) = [0] p(c27) = [0] p(c28) = [0] p(c29) = [0] p(c3) = [0] p(c30) = [0] p(c31) = [0] p(c32) = [0] p(c33) = [0] p(c34) = [0] p(c35) = [0] p(c36) = [0] p(c37) = [0] p(c38) = [0] p(c39) = [0] p(c4) = [0] p(c40) = [0] p(c41) = [0] p(c42) = [0] p(c43) = [0] p(c44) = [0] p(c45) = [0] p(c46) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [1] x1 + [1] x2 + [0] p(c9) = [0] p(conj) = [8] p(disj) = [1] p(disjconj) = [2] x1 + [1] p(getFirst) = [0] p(getSecond) = [1] p(isAnd) = [2] x1 + [8] p(isConsTerm) = [2] x1 + [1] p(isOp) = [0] p(AND#) = [0] p(BOOL#) = [1] p(CONJ#) = [1] x1 + [0] p(DISJ#) = [1] x1 + [4] p(DISJCONJ#) = [1] p(GETFIRST#) = [0] p(GETSECOND#) = [1] x1 + [0] p(ISAND#) = [1] p(ISCONSTERM#) = [1] p(ISOP#) = [1] p(and#) = [1] p(bool#) = [0] p(conj#) = [8] p(disj#) = [8] x1 + [8] p(disjconj#) = [0] p(getFirst#) = [4] x1 + [0] p(getSecond#) = [1] p(isAnd#) = [8] x1 + [4] p(isConsTerm#) = [0] p(isOp#) = [1] x1 + [0] p(c_1) = [0] p(c_2) = [1] p(c_3) = [2] p(c_4) = [1] p(c_5) = [1] x1 + [7] p(c_6) = [1] x1 + [7] p(c_7) = [0] p(c_8) = [0] p(c_9) = [2] p(c_10) = [1] x1 + [4] p(c_11) = [8] p(c_12) = [1] x1 + [0] p(c_13) = [1] x1 + [0] p(c_14) = [0] p(c_15) = [2] p(c_16) = [1] p(c_17) = [1] p(c_18) = [0] p(c_19) = [8] p(c_20) = [0] p(c_21) = [2] p(c_22) = [2] p(c_23) = [1] p(c_24) = [2] p(c_25) = [2] p(c_26) = [0] p(c_27) = [0] p(c_28) = [2] p(c_29) = [0] p(c_30) = [0] p(c_31) = [4] p(c_32) = [1] p(c_33) = [1] p(c_34) = [2] p(c_35) = [0] p(c_36) = [1] p(c_37) = [2] p(c_38) = [2] p(c_39) = [1] p(c_40) = [1] p(c_41) = [1] p(c_42) = [1] p(c_43) = [1] p(c_44) = [8] p(c_45) = [1] p(c_46) = [1] p(c_47) = [1] p(c_48) = [1] p(c_49) = [1] p(c_50) = [1] p(c_51) = [1] p(c_52) = [1] p(c_53) = [2] p(c_54) = [1] p(c_55) = [1] p(c_56) = [2] x1 + [1] x2 + [2] p(c_57) = [1] p(c_58) = [4] p(c_59) = [0] p(c_60) = [1] x1 + [0] p(c_61) = [2] p(c_62) = [1] x1 + [1] p(c_63) = [1] p(c_64) = [1] p(c_65) = [2] p(c_66) = [1] p(c_67) = [8] p(c_68) = [1] p(c_69) = [0] p(c_70) = [1] p(c_71) = [0] p(c_72) = [1] p(c_73) = [1] p(c_74) = [2] p(c_75) = [1] p(c_76) = [8] p(c_77) = [1] p(c_78) = [1] p(c_79) = [1] p(c_80) = [1] p(c_81) = [0] p(c_82) = [1] p(c_83) = [8] p(c_84) = [1] p(c_85) = [0] p(c_86) = [1] p(c_87) = [2] p(c_88) = [0] p(c_89) = [1] p(c_90) = [1] p(c_91) = [0] p(c_92) = [1] Following rules are strictly oriented: CONJ#(And(z0,z1)) = [1] z0 + [1] z1 + [12] > [1] z0 + [11] = c_5(DISJ#(z0)) CONJ#(And(z0,z1)) = [1] z0 + [1] z1 + [12] > [1] z0 + [7] = c_6(CONJ#(z0)) DISJ#(Or(z0,z1)) = [1] z0 + [1] z1 + [5] > [1] z0 + [0] = c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) = [1] z0 + [1] z1 + [5] > [1] z0 + [4] = c_13(DISJ#(z0)) Following rules are (at-least) weakly oriented: DISJ#(And(z0,z1)) = [1] z0 + [1] z1 + [16] >= [1] z0 + [1] z1 + [16] = c_10(CONJ#(And(z0,z1))) ** Step 1.b:8: NaturalMI. WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) - Weak DPs: CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)) - 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,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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0,c40/0 ,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,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,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0 ,c_53/0,c_54/0,c_55/0,c_56/3,c_57/0,c_58/0,c_59/0,c_60/1,c_61/0,c_62/3,c_63/0,c_64/1,c_65/0,c_66/0,c_67/0 ,c_68/0,c_69/0,c_70/0,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/0,c_77/0,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0 ,c_83/0,c_84/0,c_85/0,c_86/0,c_87/0,c_88/0,c_89/0,c_90/0,c_91/0,c_92/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND# ,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm# ,isOp#} and constructors {And,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6 ,c7,c8,c9} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1}, uargs(c_6) = {1}, uargs(c_10) = {1}, uargs(c_12) = {1}, uargs(c_13) = {1} Following symbols are considered usable: {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND#,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj# ,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm#,isOp#} TcT has computed the following interpretation: p(AND) = [1] x2 + [1] p(And) = [1] x1 + [2] p(BOOL) = [1] x1 + [1] p(CONJ) = [0] p(DISJ) = [0] p(DISJCONJ) = [0] p(F) = [0] p(False) = [0] p(GETFIRST) = [0] p(GETSECOND) = [0] p(ISAND) = [0] p(ISCONSTERM) = [0] p(ISOP) = [0] p(Or) = [1] x1 + [1] x2 + [1] p(T) = [0] p(True) = [0] p(and) = [0] p(bool) = [0] p(c) = [0] p(c1) = [0] p(c10) = [0] p(c11) = [0] p(c12) = [1] x1 + [1] x2 + [0] p(c13) = [1] x1 + [1] x2 + [0] p(c14) = [0] p(c15) = [0] p(c16) = [0] p(c17) = [0] p(c18) = [0] p(c19) = [0] p(c2) = [0] p(c20) = [0] p(c21) = [0] p(c22) = [0] p(c23) = [0] p(c24) = [0] p(c25) = [0] p(c26) = [0] p(c27) = [0] p(c28) = [0] p(c29) = [0] p(c3) = [0] p(c30) = [0] p(c31) = [0] p(c32) = [0] p(c33) = [0] p(c34) = [0] p(c35) = [0] p(c36) = [0] p(c37) = [0] p(c38) = [0] p(c39) = [0] p(c4) = [0] p(c40) = [2] p(c41) = [0] p(c42) = [0] p(c43) = [0] p(c44) = [0] p(c45) = [0] p(c46) = [1] x1 + [0] p(c5) = [0] p(c6) = [1] x1 + [0] p(c7) = [1] x1 + [1] x2 + [0] p(c8) = [1] x1 + [1] x2 + [0] p(c9) = [0] p(conj) = [0] p(disj) = [0] p(disjconj) = [0] p(getFirst) = [0] p(getSecond) = [0] p(isAnd) = [0] p(isConsTerm) = [0] p(isOp) = [0] p(AND#) = [0] p(BOOL#) = [0] p(CONJ#) = [8] x1 + [0] p(DISJ#) = [8] x1 + [1] p(DISJCONJ#) = [0] p(GETFIRST#) = [0] p(GETSECOND#) = [0] p(ISAND#) = [0] p(ISCONSTERM#) = [0] p(ISOP#) = [0] p(and#) = [0] p(bool#) = [0] p(conj#) = [0] p(disj#) = [0] p(disjconj#) = [0] p(getFirst#) = [0] p(getSecond#) = [0] p(isAnd#) = [0] p(isConsTerm#) = [0] p(isOp#) = [2] x1 + [0] p(c_1) = [2] p(c_2) = [2] p(c_3) = [0] p(c_4) = [1] p(c_5) = [1] x1 + [15] p(c_6) = [1] x1 + [0] p(c_7) = [1] p(c_8) = [4] p(c_9) = [0] p(c_10) = [1] x1 + [0] p(c_11) = [0] p(c_12) = [1] x1 + [9] p(c_13) = [1] x1 + [1] p(c_14) = [0] p(c_15) = [2] x1 + [0] p(c_16) = [0] p(c_17) = [0] p(c_18) = [8] p(c_19) = [1] p(c_20) = [0] p(c_21) = [1] p(c_22) = [0] p(c_23) = [0] p(c_24) = [0] p(c_25) = [2] p(c_26) = [1] p(c_27) = [1] p(c_28) = [1] p(c_29) = [1] p(c_30) = [1] p(c_31) = [2] p(c_32) = [8] p(c_33) = [0] p(c_34) = [2] p(c_35) = [2] p(c_36) = [1] p(c_37) = [0] p(c_38) = [0] p(c_39) = [2] p(c_40) = [2] p(c_41) = [0] p(c_42) = [1] p(c_43) = [2] p(c_44) = [1] p(c_45) = [4] p(c_46) = [0] p(c_47) = [0] p(c_48) = [8] p(c_49) = [1] p(c_50) = [1] p(c_51) = [0] p(c_52) = [1] p(c_53) = [0] p(c_54) = [0] p(c_55) = [1] p(c_56) = [1] x2 + [2] p(c_57) = [1] p(c_58) = [2] p(c_59) = [1] p(c_60) = [1] x1 + [4] p(c_61) = [1] p(c_62) = [1] x2 + [1] x3 + [1] p(c_63) = [0] p(c_64) = [1] p(c_65) = [0] p(c_66) = [0] p(c_67) = [1] p(c_68) = [1] p(c_69) = [0] p(c_70) = [1] p(c_71) = [1] p(c_72) = [1] p(c_73) = [0] p(c_74) = [1] p(c_75) = [1] p(c_76) = [1] p(c_77) = [1] p(c_78) = [1] p(c_79) = [1] p(c_80) = [2] p(c_81) = [2] p(c_82) = [0] p(c_83) = [0] p(c_84) = [8] p(c_85) = [8] p(c_86) = [0] p(c_87) = [0] p(c_88) = [1] p(c_89) = [0] p(c_90) = [2] p(c_91) = [1] p(c_92) = [1] Following rules are strictly oriented: DISJ#(And(z0,z1)) = [8] z0 + [17] > [8] z0 + [16] = c_10(CONJ#(And(z0,z1))) Following rules are (at-least) weakly oriented: CONJ#(And(z0,z1)) = [8] z0 + [16] >= [8] z0 + [16] = c_5(DISJ#(z0)) CONJ#(And(z0,z1)) = [8] z0 + [16] >= [8] z0 + [0] = c_6(CONJ#(z0)) DISJ#(Or(z0,z1)) = [8] z0 + [8] z1 + [9] >= [8] z0 + [9] = c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) = [8] z0 + [8] z1 + [9] >= [8] z0 + [2] = c_13(DISJ#(z0)) ** Step 1.b:9: EmptyProcessor. WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: CONJ#(And(z0,z1)) -> c_5(DISJ#(z0)) CONJ#(And(z0,z1)) -> c_6(CONJ#(z0)) DISJ#(And(z0,z1)) -> c_10(CONJ#(And(z0,z1))) DISJ#(Or(z0,z1)) -> c_12(CONJ#(z0)) DISJ#(Or(z0,z1)) -> c_13(DISJ#(z0)) - 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,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/0,c1/0,c10/0,c11/0,c12/2,c13/2,c14/0,c15/0,c16/0,c17/0,c18/0,c19/0,c2/0,c20/0,c21/0,c22/0,c23/0,c24/0 ,c25/0,c26/0,c27/0,c28/0,c29/0,c3/0,c30/0,c31/0,c32/0,c33/0,c34/0,c35/0,c36/0,c37/0,c38/0,c39/0,c4/0,c40/0 ,c41/0,c42/0,c43/0,c44/0,c45/0,c46/1,c5/0,c6/1,c7/2,c8/2,c9/0,c_1/0,c_2/0,c_3/0,c_4/0,c_5/1,c_6/1,c_7/0 ,c_8/0,c_9/0,c_10/1,c_11/0,c_12/1,c_13/1,c_14/0,c_15/1,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,c_46/0,c_47/0,c_48/0,c_49/0,c_50/0,c_51/0,c_52/0 ,c_53/0,c_54/0,c_55/0,c_56/3,c_57/0,c_58/0,c_59/0,c_60/1,c_61/0,c_62/3,c_63/0,c_64/1,c_65/0,c_66/0,c_67/0 ,c_68/0,c_69/0,c_70/0,c_71/0,c_72/0,c_73/0,c_74/0,c_75/0,c_76/0,c_77/0,c_78/0,c_79/0,c_80/0,c_81/0,c_82/0 ,c_83/0,c_84/0,c_85/0,c_86/0,c_87/0,c_88/0,c_89/0,c_90/0,c_91/0,c_92/0} - Obligation: innermost runtime complexity wrt. defined symbols {AND#,BOOL#,CONJ#,DISJ#,DISJCONJ#,GETFIRST#,GETSECOND# ,ISAND#,ISCONSTERM#,ISOP#,and#,bool#,conj#,disj#,disjconj#,getFirst#,getSecond#,isAnd#,isConsTerm# ,isOp#} and constructors {And,F,False,Or,T,True,c,c1,c10,c11,c12,c13,c14,c15,c16,c17,c18,c19,c2,c20,c21,c22 ,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41,c42,c43,c44,c45,c46,c5,c6 ,c7,c8,c9} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(Omega(n^1),O(n^1))