* Step 1: Sum WORST_CASE(Omega(n^1),?)
    + 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:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
* Step 2: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + 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:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          conj(x){x -> And(x,y)} =
            conj(And(x,y)) ->^+ and(disj(x),conj(x))
              = C[conj(x) = conj(x){}]

WORST_CASE(Omega(n^1),?)