```* Step 1: MI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
implies(x,or(y,z)) -> or(y,implies(x,z))
implies(not(x),y) -> or(x,y)
implies(not(x),or(y,z)) -> implies(y,or(x,z))
- Signature:
{implies/2} / {not/1,or/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {implies} and constructors {not,or}
+ Applied Processor:
MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity Nothing)), miDimension = 1, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
+ Details:
We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity Nothing)):

The following argument positions are considered usable:
uargs(or) = {2}

Following symbols are considered usable:
{implies}
TcT has computed the following interpretation:
p(implies) =  x_2 + 
p(not) = 
p(or) =  x_2 + 

Following rules are strictly oriented:
implies(x,or(y,z)) =  z + 
>  z + 
= or(y,implies(x,z))

Following rules are (at-least) weakly oriented:
implies(not(x),y) =   y + 
>=  y + 
=  or(x,y)

implies(not(x),or(y,z)) =   z + 
>=  z + 
=  implies(y,or(x,z))

* Step 2: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
implies(not(x),y) -> or(x,y)
implies(not(x),or(y,z)) -> implies(y,or(x,z))
- Weak TRS:
implies(x,or(y,z)) -> or(y,implies(x,z))
- Signature:
{implies/2} / {not/1,or/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {implies} and constructors {not,or}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(or) = {2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(implies) =  x2 + 
p(not) =  x1 + 
p(or) =  x2 + 

Following rules are strictly oriented:
implies(not(x),y) =  y + 
>  y + 
= or(x,y)

Following rules are (at-least) weakly oriented:
implies(x,or(y,z)) =   z + 
>=  z + 
=  or(y,implies(x,z))

implies(not(x),or(y,z)) =   z + 
>=  z + 
=  implies(y,or(x,z))

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
implies(not(x),or(y,z)) -> implies(y,or(x,z))
- Weak TRS:
implies(x,or(y,z)) -> or(y,implies(x,z))
implies(not(x),y) -> or(x,y)
- Signature:
{implies/2} / {not/1,or/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {implies} and constructors {not,or}
+ Applied Processor:
WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
+ Details:
The weightgap principle applies using the following nonconstant growth matrix-interpretation:
We apply a matrix interpretation of kind constructor based matrix interpretation:
The following argument positions are considered usable:
uargs(or) = {2}

Following symbols are considered usable:
all
TcT has computed the following interpretation:
p(implies) =  x1 +  x2 + 
p(not) =  x1 + 
p(or) =  x1 +  x2 + 

Following rules are strictly oriented:
implies(not(x),or(y,z)) =  x +  y +  z + 
>  x +  y +  z + 
= implies(y,or(x,z))

Following rules are (at-least) weakly oriented:
implies(x,or(y,z)) =   x +  y +  z + 
>=  x +  y +  z + 
=  or(y,implies(x,z))

implies(not(x),y) =   x +  y + 
>=  x +  y + 
=  or(x,y)

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
implies(x,or(y,z)) -> or(y,implies(x,z))
implies(not(x),y) -> or(x,y)
implies(not(x),or(y,z)) -> implies(y,or(x,z))
- Signature:
{implies/2} / {not/1,or/2}
- Obligation:
innermost runtime complexity wrt. defined symbols {implies} and constructors {not,or}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))
```