```* Step 1: ToInnermost 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:
runtime complexity wrt. defined symbols {implies} and constructors {not,or}
+ Applied Processor:
ToInnermost
+ Details:
switch to innermost, as the system is overlay and right linear and does not contain weak rules
* Step 2: 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) = [2] x_2 + [10]
p(not) = [0]
p(or) = [1] x_2 + [10]

Following rules are strictly oriented:
implies(x,or(y,z)) = [2] z + [30]
> [2] z + [20]
= or(y,implies(x,z))

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

implies(not(x),or(y,z)) =  [2] z + [30]
>= [2] z + [30]
=  implies(y,or(x,z))

* Step 3: 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) = [2] x2 + [1]
p(not) = [1] x1 + [0]
p(or) = [1] x2 + [0]

Following rules are strictly oriented:
implies(not(x),y) = [2] y + [1]
> [1] y + [0]
= or(x,y)

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

implies(not(x),or(y,z)) =  [2] z + [1]
>= [2] z + [1]
=  implies(y,or(x,z))

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: 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) = [1] x1 + [1] x2 + [0]
p(not) = [1] x1 + [2]
p(or) = [1] x1 + [1] x2 + [1]

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

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

implies(not(x),y) =  [1] x + [1] y + [2]
>= [1] x + [1] y + [1]
=  or(x,y)

Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: 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))
```