MAYBE * Step 1: DependencyPairs MAYBE + Considered Problem: - Strict TRS: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) not(not(x)) -> x not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) - Signature: {not/1} / {and/2,or/2} - Obligation: innermost runtime complexity wrt. defined symbols {not} and constructors {and,or} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs not#(and(x,y)) -> c_1(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) not#(not(x)) -> c_2() not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) Weak DPs and mark the set of starting terms. * Step 2: PredecessorEstimation MAYBE + Considered Problem: - Strict DPs: not#(and(x,y)) -> c_1(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) not#(not(x)) -> c_2() not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) - Weak TRS: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) not(not(x)) -> x not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) - Signature: {not/1,not#/1} / {and/2,or/2,c_1/6,c_2/0,c_3/6} - Obligation: innermost runtime complexity wrt. defined symbols {not#} and constructors {and,or} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {2} by application of Pre({2}) = {1,3}. Here rules are labelled as follows: 1: not#(and(x,y)) -> c_1(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) 2: not#(not(x)) -> c_2() 3: not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) * Step 3: RemoveWeakSuffixes MAYBE + Considered Problem: - Strict DPs: not#(and(x,y)) -> c_1(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) - Weak DPs: not#(not(x)) -> c_2() - Weak TRS: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) not(not(x)) -> x not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) - Signature: {not/1,not#/1} / {and/2,or/2,c_1/6,c_2/0,c_3/6} - Obligation: innermost runtime complexity wrt. defined symbols {not#} and constructors {and,or} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:not#(and(x,y)) -> c_1(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) -->_6 not#(or(x,y)) -> c_3(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):2 -->_5 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_4 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_3 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_2 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_1 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_6 not#(not(x)) -> c_2():3 -->_5 not#(not(x)) -> c_2():3 -->_4 not#(not(x)) -> c_2():3 -->_3 not#(not(x)) -> c_2():3 -->_2 not#(not(x)) -> c_2():3 -->_1 not#(not(x)) -> c_2():3 -->_6 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_5 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_4 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_3 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_2 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_1 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 2:S:not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) -->_6 not#(not(x)) -> c_2():3 -->_5 not#(not(x)) -> c_2():3 -->_4 not#(not(x)) -> c_2():3 -->_3 not#(not(x)) -> c_2():3 -->_2 not#(not(x)) -> c_2():3 -->_1 not#(not(x)) -> c_2():3 -->_6 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_5 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_4 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_3 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_2 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_1 not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)):2 -->_6 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_5 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_4 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_3 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_2 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 -->_1 not#(and(x,y)) -> c_1(not#(not(not(x))) ,not#(not(x)) ,not#(x) ,not#(not(not(y))) ,not#(not(y)) ,not#(y)):1 3:W:not#(not(x)) -> c_2() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 3: not#(not(x)) -> c_2() * Step 4: Failure MAYBE + Considered Problem: - Strict DPs: not#(and(x,y)) -> c_1(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) not#(or(x,y)) -> c_3(not#(not(not(x))),not#(not(x)),not#(x),not#(not(not(y))),not#(not(y)),not#(y)) - Weak TRS: not(and(x,y)) -> or(not(not(not(x))),not(not(not(y)))) not(not(x)) -> x not(or(x,y)) -> and(not(not(not(x))),not(not(not(y)))) - Signature: {not/1,not#/1} / {and/2,or/2,c_1/6,c_2/0,c_3/6} - Obligation: innermost runtime complexity wrt. defined symbols {not#} and constructors {and,or} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE