WORST_CASE(?,O(n^1))
proof of input_94TynTowWP.trs
# AProVE Commit ID: 5b976082cb74a395683ed8cc7acf94bd611ab29f fuhs 20230524 unpublished


The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 852 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 0 ms]
(4) CdtProblem
(5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
(6) CdtProblem
(7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CdtProblem
(9) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
(10) CdtProblem
(11) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
(12) CdtProblem
(13) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(14) CpxRelTRS
(15) RelTrsToWeightedTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(16) CpxWeightedTrs
(17) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(18) CpxTypedWeightedTrs
(19) CompletionProof [UPPER BOUND(ID), 0 ms]
(20) CpxTypedWeightedCompleteTrs
(21) NarrowingProof [BOTH BOUNDS(ID, ID), 0 ms]
(22) CpxTypedWeightedCompleteTrs
(23) CpxTypedWeightedTrsToRntsProof [UPPER BOUND(ID), 0 ms]
(24) CpxRNTS
(25) SimplificationProof [BOTH BOUNDS(ID, ID), 0 ms]
(26) CpxRNTS
(27) CpxRntsAnalysisOrderProof [BOTH BOUNDS(ID, ID), 0 ms]
(28) CpxRNTS
(29) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(30) CpxRNTS
(31) IntTrsBoundProof [UPPER BOUND(ID), 193 ms]
(32) CpxRNTS
(33) IntTrsBoundProof [UPPER BOUND(ID), 57 ms]
(34) CpxRNTS
(35) ResultPropagationProof [UPPER BOUND(ID), 0 ms]
(36) CpxRNTS
(37) IntTrsBoundProof [UPPER BOUND(ID), 10.2 s]
(38) CpxRNTS
(39) IntTrsBoundProof [UPPER BOUND(ID), 3467 ms]
(40) CpxRNTS
(41) FinalProof [FINISHED, 0 ms]
(42) BOUNDS(1, n^1)


----------------------------------------

(0)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   head(Cons(x, xs)) -> x
   e(Cons(F, Nil), b) -> False
   e(Cons(T, Nil), b) -> False
   e(Cons(B, Nil), b) -> False
   e(Cons(A, Nil), b) -> e[Match][Cons][Ite][True][Match](A, Nil, b)
   e(Cons(F, Cons(x, xs)), b) -> False
   e(Cons(T, Cons(x, xs)), b) -> False
   e(Cons(B, Cons(x, xs)), b) -> False
   e(Cons(A, Cons(x, xs)), b) -> False
   equal(F, F) -> True
   equal(F, T) -> False
   equal(F, B) -> False
   equal(F, A) -> False
   equal(T, F) -> False
   equal(T, T) -> True
   equal(T, B) -> False
   equal(T, A) -> False
   equal(B, F) -> False
   equal(B, T) -> False
   equal(B, B) -> True
   equal(B, A) -> False
   equal(A, F) -> False
   equal(A, T) -> False
   equal(A, B) -> False
   equal(A, A) -> True
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   e(Nil, b) -> False
   t(x, y) -> t[Ite](e(x, y), x, y)
   r(x, y) -> r[Ite](e(x, y), x, y)
   q(x, y) -> q[Ite](e(x, y), x, y)
   p(x, y) -> p[Ite](e(x, y), x, y)
   goal(x, y) -> q(x, y)

The (relative) TRS S consists of the following rules:

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   q[Ite](False, x', Cons(F, Cons(F, xs))) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs)))
   q[Ite](False, x, Cons(F, Cons(T, xs))) -> False
   q[Ite](False, x, Cons(F, Cons(B, xs))) -> False
   q[Ite](False, x, Cons(F, Cons(A, xs))) -> False
   q[Ite](False, x, Cons(T, Cons(F, xs))) -> False
   q[Ite](False, x, Cons(T, Cons(T, xs))) -> False
   q[Ite](False, x, Cons(T, Cons(B, xs))) -> False
   q[Ite](False, x, Cons(T, Cons(A, xs))) -> False
   q[Ite](False, x, Cons(B, Cons(F, xs))) -> False
   q[Ite](False, x, Cons(B, Cons(T, xs))) -> False
   q[Ite](False, x, Cons(B, Cons(B, xs))) -> False
   q[Ite](False, x, Cons(B, Cons(A, xs))) -> False
   q[Ite](False, x, Cons(A, Cons(F, xs))) -> False
   q[Ite](False, x, Cons(A, Cons(T, xs))) -> False
   q[Ite](False, x, Cons(A, Cons(B, xs))) -> False
   q[Ite](False, x, Cons(A, Cons(A, xs))) -> False
   q[Ite](False, x', Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))
   q[Ite](False, x', Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))
   q[Ite](False, x', Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))
   q[Ite](False, x', Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))
   r[Ite](False, x', Cons(F, xs)) -> r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs))
   r[Ite](False, x, Cons(T, xs)) -> False
   r[Ite](False, x, Cons(B, xs)) -> False
   r[Ite](False, x, Cons(A, xs)) -> False
   p[Ite](False, x', Cons(F, xs)) -> and(r(x', Cons(F, xs)), p(x', xs))
   p[Ite](False, x, Cons(T, xs)) -> False
   p[Ite](False, x, Cons(B, xs)) -> False
   p[Ite](False, x, Cons(A, xs)) -> False
   q[Ite][False][Ite](True, x', Cons(x, xs)) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs))
   t[Ite](False, x, y) -> True
   t[Ite](True, x, y) -> True
   r[Ite](True, x, y) -> True
   q[Ite](True, x, y) -> True
   q[Ite][False][Ite](False, x, y) -> False
   p[Ite](True, x, y) -> True

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(1) SInnermostTerminationProof (BOTH CONCRETE BOUNDS(ID, ID))
proved innermost termination of relative rules
----------------------------------------

(2)
Obligation:
The Runtime Complexity (parallel-innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   head(Cons(x, xs)) -> x
   e(Cons(F, Nil), b) -> False
   e(Cons(T, Nil), b) -> False
   e(Cons(B, Nil), b) -> False
   e(Cons(A, Nil), b) -> e[Match][Cons][Ite][True][Match](A, Nil, b)
   e(Cons(F, Cons(x, xs)), b) -> False
   e(Cons(T, Cons(x, xs)), b) -> False
   e(Cons(B, Cons(x, xs)), b) -> False
   e(Cons(A, Cons(x, xs)), b) -> False
   equal(F, F) -> True
   equal(F, T) -> False
   equal(F, B) -> False
   equal(F, A) -> False
   equal(T, F) -> False
   equal(T, T) -> True
   equal(T, B) -> False
   equal(T, A) -> False
   equal(B, F) -> False
   equal(B, T) -> False
   equal(B, B) -> True
   equal(B, A) -> False
   equal(A, F) -> False
   equal(A, T) -> False
   equal(A, B) -> False
   equal(A, A) -> True
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   e(Nil, b) -> False
   t(x, y) -> t[Ite](e(x, y), x, y)
   r(x, y) -> r[Ite](e(x, y), x, y)
   q(x, y) -> q[Ite](e(x, y), x, y)
   p(x, y) -> p[Ite](e(x, y), x, y)
   goal(x, y) -> q(x, y)

The (relative) TRS S consists of the following rules:

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   q[Ite](False, x', Cons(F, Cons(F, xs))) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(F, Cons(F, xs))), q(x', Cons(F, xs))), x', Cons(F, Cons(F, xs)))
   q[Ite](False, x, Cons(F, Cons(T, xs))) -> False
   q[Ite](False, x, Cons(F, Cons(B, xs))) -> False
   q[Ite](False, x, Cons(F, Cons(A, xs))) -> False
   q[Ite](False, x, Cons(T, Cons(F, xs))) -> False
   q[Ite](False, x, Cons(T, Cons(T, xs))) -> False
   q[Ite](False, x, Cons(T, Cons(B, xs))) -> False
   q[Ite](False, x, Cons(T, Cons(A, xs))) -> False
   q[Ite](False, x, Cons(B, Cons(F, xs))) -> False
   q[Ite](False, x, Cons(B, Cons(T, xs))) -> False
   q[Ite](False, x, Cons(B, Cons(B, xs))) -> False
   q[Ite](False, x, Cons(B, Cons(A, xs))) -> False
   q[Ite](False, x, Cons(A, Cons(F, xs))) -> False
   q[Ite](False, x, Cons(A, Cons(T, xs))) -> False
   q[Ite](False, x, Cons(A, Cons(B, xs))) -> False
   q[Ite](False, x, Cons(A, Cons(A, xs))) -> False
   q[Ite](False, x', Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), x', Cons(F, Nil))
   q[Ite](False, x', Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(T, Nil))
   q[Ite](False, x', Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(B, Nil))
   q[Ite](False, x', Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), x', Cons(A, Nil))
   r[Ite](False, x', Cons(F, xs)) -> r[Ite][False][Ite][True][Ite](and(q(x', xs), r(x', xs)), x', Cons(F, xs))
   r[Ite](False, x, Cons(T, xs)) -> False
   r[Ite](False, x, Cons(B, xs)) -> False
   r[Ite](False, x, Cons(A, xs)) -> False
   p[Ite](False, x', Cons(F, xs)) -> and(r(x', Cons(F, xs)), p(x', xs))
   p[Ite](False, x, Cons(T, xs)) -> False
   p[Ite](False, x, Cons(B, xs)) -> False
   p[Ite](False, x, Cons(A, xs)) -> False
   q[Ite][False][Ite](True, x', Cons(x, xs)) -> q[Ite][False][Ite][True][Ite](and(p(x', Cons(x, xs)), q(x', xs)), x', Cons(x, xs))
   t[Ite](False, x, y) -> True
   t[Ite](True, x, y) -> True
   r[Ite](True, x, y) -> True
   q[Ite](True, x, y) -> True
   q[Ite][False][Ite](False, x, y) -> False
   p[Ite](True, x, y) -> True

Rewrite Strategy: PARALLEL_INNERMOST
----------------------------------------

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1)))
   q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil))
   q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil))
   q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil))
   q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil))
   q[Ite](True, z0, z1) -> True
   r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1))
   r[Ite](False, z0, Cons(T, z1)) -> False
   r[Ite](False, z0, Cons(B, z1)) -> False
   r[Ite](False, z0, Cons(A, z1)) -> False
   r[Ite](True, z0, z1) -> True
   p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1))
   p[Ite](False, z0, Cons(T, z1)) -> False
   p[Ite](False, z0, Cons(B, z1)) -> False
   p[Ite](False, z0, Cons(A, z1)) -> False
   p[Ite](True, z0, z1) -> True
   q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2))
   q[Ite][False][Ite](False, z0, z1) -> False
   t[Ite](False, z0, z1) -> True
   t[Ite](True, z0, z1) -> True
   head(Cons(z0, z1)) -> z0
   e(Cons(F, Nil), z0) -> False
   e(Cons(T, Nil), z0) -> False
   e(Cons(B, Nil), z0) -> False
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0)
   e(Cons(F, Cons(z0, z1)), z2) -> False
   e(Cons(T, Cons(z0, z1)), z2) -> False
   e(Cons(B, Cons(z0, z1)), z2) -> False
   e(Cons(A, Cons(z0, z1)), z2) -> False
   e(Nil, z0) -> False
   equal(F, F) -> True
   equal(F, T) -> False
   equal(F, B) -> False
   equal(F, A) -> False
   equal(T, F) -> False
   equal(T, T) -> True
   equal(T, B) -> False
   equal(T, A) -> False
   equal(B, F) -> False
   equal(B, T) -> False
   equal(B, B) -> True
   equal(B, A) -> False
   equal(A, F) -> False
   equal(A, T) -> False
   equal(A, B) -> False
   equal(A, A) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   t(z0, z1) -> t[Ite](e(z0, z1), z0, z1)
   r(z0, z1) -> r[Ite](e(z0, z1), z0, z1)
   q(z0, z1) -> q[Ite](e(z0, z1), z0, z1)
   p(z0, z1) -> p[Ite](e(z0, z1), z0, z1)
   goal(z0, z1) -> q(z0, z1)
Tuples:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(AND(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), P(z0, Cons(F, Cons(F, z1))))
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(AND(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), Q(z0, Cons(F, z1)))
   Q[ITE](False, z0, Cons(F, Cons(T, z1))) -> c6
   Q[ITE](False, z0, Cons(F, Cons(B, z1))) -> c7
   Q[ITE](False, z0, Cons(F, Cons(A, z1))) -> c8
   Q[ITE](False, z0, Cons(T, Cons(F, z1))) -> c9
   Q[ITE](False, z0, Cons(T, Cons(T, z1))) -> c10
   Q[ITE](False, z0, Cons(T, Cons(B, z1))) -> c11
   Q[ITE](False, z0, Cons(T, Cons(A, z1))) -> c12
   Q[ITE](False, z0, Cons(B, Cons(F, z1))) -> c13
   Q[ITE](False, z0, Cons(B, Cons(T, z1))) -> c14
   Q[ITE](False, z0, Cons(B, Cons(B, z1))) -> c15
   Q[ITE](False, z0, Cons(B, Cons(A, z1))) -> c16
   Q[ITE](False, z0, Cons(A, Cons(F, z1))) -> c17
   Q[ITE](False, z0, Cons(A, Cons(T, z1))) -> c18
   Q[ITE](False, z0, Cons(A, Cons(B, z1))) -> c19
   Q[ITE](False, z0, Cons(A, Cons(A, z1))) -> c20
   Q[ITE](False, z0, Cons(F, Nil)) -> c21(Q[ITE][FALSE][ITE](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)), AND(True, and(True, and(False, equal(head(Nil), F)))), AND(True, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil))
   Q[ITE](False, z0, Cons(T, Nil)) -> c22(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil))
   Q[ITE](False, z0, Cons(B, Nil)) -> c23(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil))
   Q[ITE](False, z0, Cons(A, Nil)) -> c24(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil))
   Q[ITE](True, z0, z1) -> c25
   R[ITE](False, z0, Cons(F, z1)) -> c26(AND(q(z0, z1), r(z0, z1)), Q(z0, z1))
   R[ITE](False, z0, Cons(F, z1)) -> c27(AND(q(z0, z1), r(z0, z1)), R(z0, z1))
   R[ITE](False, z0, Cons(T, z1)) -> c28
   R[ITE](False, z0, Cons(B, z1)) -> c29
   R[ITE](False, z0, Cons(A, z1)) -> c30
   R[ITE](True, z0, z1) -> c31
   P[ITE](False, z0, Cons(F, z1)) -> c32(AND(r(z0, Cons(F, z1)), p(z0, z1)), R(z0, Cons(F, z1)))
   P[ITE](False, z0, Cons(F, z1)) -> c33(AND(r(z0, Cons(F, z1)), p(z0, z1)), P(z0, z1))
   P[ITE](False, z0, Cons(T, z1)) -> c34
   P[ITE](False, z0, Cons(B, z1)) -> c35
   P[ITE](False, z0, Cons(A, z1)) -> c36
   P[ITE](True, z0, z1) -> c37
   Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c38(AND(p(z0, Cons(z1, z2)), q(z0, z2)), P(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c39(AND(p(z0, Cons(z1, z2)), q(z0, z2)), Q(z0, z2))
   Q[ITE][FALSE][ITE](False, z0, z1) -> c40
   T[ITE](False, z0, z1) -> c41
   T[ITE](True, z0, z1) -> c42
   HEAD(Cons(z0, z1)) -> c43
   E(Cons(F, Nil), z0) -> c44
   E(Cons(T, Nil), z0) -> c45
   E(Cons(B, Nil), z0) -> c46
   E(Cons(A, Nil), z0) -> c47
   E(Cons(F, Cons(z0, z1)), z2) -> c48
   E(Cons(T, Cons(z0, z1)), z2) -> c49
   E(Cons(B, Cons(z0, z1)), z2) -> c50
   E(Cons(A, Cons(z0, z1)), z2) -> c51
   E(Nil, z0) -> c52
   EQUAL(F, F) -> c53
   EQUAL(F, T) -> c54
   EQUAL(F, B) -> c55
   EQUAL(F, A) -> c56
   EQUAL(T, F) -> c57
   EQUAL(T, T) -> c58
   EQUAL(T, B) -> c59
   EQUAL(T, A) -> c60
   EQUAL(B, F) -> c61
   EQUAL(B, T) -> c62
   EQUAL(B, B) -> c63
   EQUAL(B, A) -> c64
   EQUAL(A, F) -> c65
   EQUAL(A, T) -> c66
   EQUAL(A, B) -> c67
   EQUAL(A, A) -> c68
   NOTEMPTY(Cons(z0, z1)) -> c69
   NOTEMPTY(Nil) -> c70
   T'(z0, z1) -> c71(T[ITE](e(z0, z1), z0, z1), E(z0, z1))
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1), E(z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1), E(z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1), E(z0, z1))
   GOAL(z0, z1) -> c75(Q(z0, z1))
S tuples:
   HEAD(Cons(z0, z1)) -> c43
   E(Cons(F, Nil), z0) -> c44
   E(Cons(T, Nil), z0) -> c45
   E(Cons(B, Nil), z0) -> c46
   E(Cons(A, Nil), z0) -> c47
   E(Cons(F, Cons(z0, z1)), z2) -> c48
   E(Cons(T, Cons(z0, z1)), z2) -> c49
   E(Cons(B, Cons(z0, z1)), z2) -> c50
   E(Cons(A, Cons(z0, z1)), z2) -> c51
   E(Nil, z0) -> c52
   EQUAL(F, F) -> c53
   EQUAL(F, T) -> c54
   EQUAL(F, B) -> c55
   EQUAL(F, A) -> c56
   EQUAL(T, F) -> c57
   EQUAL(T, T) -> c58
   EQUAL(T, B) -> c59
   EQUAL(T, A) -> c60
   EQUAL(B, F) -> c61
   EQUAL(B, T) -> c62
   EQUAL(B, B) -> c63
   EQUAL(B, A) -> c64
   EQUAL(A, F) -> c65
   EQUAL(A, T) -> c66
   EQUAL(A, B) -> c67
   EQUAL(A, A) -> c68
   NOTEMPTY(Cons(z0, z1)) -> c69
   NOTEMPTY(Nil) -> c70
   T'(z0, z1) -> c71(T[ITE](e(z0, z1), z0, z1), E(z0, z1))
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1), E(z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1), E(z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1), E(z0, z1))
   GOAL(z0, z1) -> c75(Q(z0, z1))
K tuples:none
Defined Rule Symbols:   head_1, e_2, equal_2, notEmpty_1, t_2, r_2, q_2, p_2, goal_2, and_2, q[Ite]_3, r[Ite]_3, p[Ite]_3, q[Ite][False][Ite]_3, t[Ite]_3

Defined Pair Symbols:   AND_2, Q[ITE]_3, R[ITE]_3, P[ITE]_3, Q[ITE][FALSE][ITE]_3, T[ITE]_3, HEAD_1, E_2, EQUAL_2, NOTEMPTY_1, T'_2, R_2, Q_2, P_2, GOAL_2

Compound Symbols:   c, c1, c2, c3, c4_2, c5_2, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21_6, c22_6, c23_6, c24_6, c25, c26_2, c27_2, c28, c29, c30, c31, c32_2, c33_2, c34, c35, c36, c37, c38_2, c39_2, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66, c67, c68, c69, c70, c71_2, c72_2, c73_2, c74_2, c75_1


----------------------------------------

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 1 leading nodes:
   GOAL(z0, z1) -> c75(Q(z0, z1))
Removed 64 trailing nodes:
   EQUAL(T, T) -> c58
   EQUAL(A, A) -> c68
   EQUAL(T, F) -> c57
   Q[ITE](False, z0, Cons(A, Cons(T, z1))) -> c18
   Q[ITE](False, z0, Cons(T, Cons(F, z1))) -> c9
   EQUAL(F, A) -> c56
   Q[ITE](False, z0, Cons(F, Nil)) -> c21(Q[ITE][FALSE][ITE](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil)), AND(True, and(True, and(False, equal(head(Nil), F)))), AND(True, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil))
   AND(True, True) -> c3
   Q[ITE](False, z0, Cons(F, Cons(A, z1))) -> c8
   R[ITE](False, z0, Cons(B, z1)) -> c29
   EQUAL(T, B) -> c59
   E(Cons(F, Cons(z0, z1)), z2) -> c48
   P[ITE](False, z0, Cons(T, z1)) -> c34
   E(Cons(B, Cons(z0, z1)), z2) -> c50
   E(Cons(T, Nil), z0) -> c45
   Q[ITE](False, z0, Cons(B, Cons(A, z1))) -> c16
   NOTEMPTY(Nil) -> c70
   E(Cons(B, Nil), z0) -> c46
   Q[ITE](False, z0, Cons(A, Nil)) -> c24(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil))
   EQUAL(B, F) -> c61
   AND(True, False) -> c1
   E(Cons(F, Nil), z0) -> c44
   R[ITE](False, z0, Cons(T, z1)) -> c28
   EQUAL(F, T) -> c54
   EQUAL(A, T) -> c66
   P[ITE](False, z0, Cons(B, z1)) -> c35
   Q[ITE](False, z0, Cons(F, Cons(T, z1))) -> c6
   EQUAL(B, B) -> c63
   EQUAL(A, B) -> c67
   Q[ITE](False, z0, Cons(A, Cons(F, z1))) -> c17
   E(Nil, z0) -> c52
   T[ITE](True, z0, z1) -> c42
   Q[ITE](False, z0, Cons(B, Cons(B, z1))) -> c15
   E(Cons(A, Nil), z0) -> c47
   Q[ITE](True, z0, z1) -> c25
   P[ITE](False, z0, Cons(A, z1)) -> c36
   Q[ITE](False, z0, Cons(T, Nil)) -> c22(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil))
   EQUAL(F, F) -> c53
   EQUAL(B, A) -> c64
   EQUAL(T, A) -> c60
   Q[ITE](False, z0, Cons(F, Cons(B, z1))) -> c7
   Q[ITE](False, z0, Cons(T, Cons(T, z1))) -> c10
   E(Cons(A, Cons(z0, z1)), z2) -> c51
   R[ITE](True, z0, z1) -> c31
   EQUAL(F, B) -> c55
   T[ITE](False, z0, z1) -> c41
   Q[ITE](False, z0, Cons(B, Cons(F, z1))) -> c13
   Q[ITE](False, z0, Cons(T, Cons(B, z1))) -> c11
   EQUAL(B, T) -> c62
   AND(False, True) -> c2
   E(Cons(T, Cons(z0, z1)), z2) -> c49
   Q[ITE](False, z0, Cons(A, Cons(B, z1))) -> c19
   Q[ITE](False, z0, Cons(T, Cons(A, z1))) -> c12
   Q[ITE][FALSE][ITE](False, z0, z1) -> c40
   Q[ITE](False, z0, Cons(A, Cons(A, z1))) -> c20
   NOTEMPTY(Cons(z0, z1)) -> c69
   AND(False, False) -> c
   HEAD(Cons(z0, z1)) -> c43
   T'(z0, z1) -> c71(T[ITE](e(z0, z1), z0, z1), E(z0, z1))
   Q[ITE](False, z0, Cons(B, Cons(T, z1))) -> c14
   P[ITE](True, z0, z1) -> c37
   EQUAL(A, F) -> c65
   R[ITE](False, z0, Cons(A, z1)) -> c30
   Q[ITE](False, z0, Cons(B, Nil)) -> c23(Q[ITE][FALSE][ITE](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil)), AND(True, and(False, and(False, equal(head(Nil), F)))), AND(False, and(False, equal(head(Nil), F))), AND(False, equal(head(Nil), F)), EQUAL(head(Nil), F), HEAD(Nil))

----------------------------------------

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1)))
   q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil))
   q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil))
   q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil))
   q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil))
   q[Ite](True, z0, z1) -> True
   r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1))
   r[Ite](False, z0, Cons(T, z1)) -> False
   r[Ite](False, z0, Cons(B, z1)) -> False
   r[Ite](False, z0, Cons(A, z1)) -> False
   r[Ite](True, z0, z1) -> True
   p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1))
   p[Ite](False, z0, Cons(T, z1)) -> False
   p[Ite](False, z0, Cons(B, z1)) -> False
   p[Ite](False, z0, Cons(A, z1)) -> False
   p[Ite](True, z0, z1) -> True
   q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2))
   q[Ite][False][Ite](False, z0, z1) -> False
   t[Ite](False, z0, z1) -> True
   t[Ite](True, z0, z1) -> True
   head(Cons(z0, z1)) -> z0
   e(Cons(F, Nil), z0) -> False
   e(Cons(T, Nil), z0) -> False
   e(Cons(B, Nil), z0) -> False
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0)
   e(Cons(F, Cons(z0, z1)), z2) -> False
   e(Cons(T, Cons(z0, z1)), z2) -> False
   e(Cons(B, Cons(z0, z1)), z2) -> False
   e(Cons(A, Cons(z0, z1)), z2) -> False
   e(Nil, z0) -> False
   equal(F, F) -> True
   equal(F, T) -> False
   equal(F, B) -> False
   equal(F, A) -> False
   equal(T, F) -> False
   equal(T, T) -> True
   equal(T, B) -> False
   equal(T, A) -> False
   equal(B, F) -> False
   equal(B, T) -> False
   equal(B, B) -> True
   equal(B, A) -> False
   equal(A, F) -> False
   equal(A, T) -> False
   equal(A, B) -> False
   equal(A, A) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   t(z0, z1) -> t[Ite](e(z0, z1), z0, z1)
   r(z0, z1) -> r[Ite](e(z0, z1), z0, z1)
   q(z0, z1) -> q[Ite](e(z0, z1), z0, z1)
   p(z0, z1) -> p[Ite](e(z0, z1), z0, z1)
   goal(z0, z1) -> q(z0, z1)
Tuples:
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(AND(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), P(z0, Cons(F, Cons(F, z1))))
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(AND(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), Q(z0, Cons(F, z1)))
   R[ITE](False, z0, Cons(F, z1)) -> c26(AND(q(z0, z1), r(z0, z1)), Q(z0, z1))
   R[ITE](False, z0, Cons(F, z1)) -> c27(AND(q(z0, z1), r(z0, z1)), R(z0, z1))
   P[ITE](False, z0, Cons(F, z1)) -> c32(AND(r(z0, Cons(F, z1)), p(z0, z1)), R(z0, Cons(F, z1)))
   P[ITE](False, z0, Cons(F, z1)) -> c33(AND(r(z0, Cons(F, z1)), p(z0, z1)), P(z0, z1))
   Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c38(AND(p(z0, Cons(z1, z2)), q(z0, z2)), P(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c39(AND(p(z0, Cons(z1, z2)), q(z0, z2)), Q(z0, z2))
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1), E(z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1), E(z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1), E(z0, z1))
S tuples:
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1), E(z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1), E(z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1), E(z0, z1))
K tuples:none
Defined Rule Symbols:   head_1, e_2, equal_2, notEmpty_1, t_2, r_2, q_2, p_2, goal_2, and_2, q[Ite]_3, r[Ite]_3, p[Ite]_3, q[Ite][False][Ite]_3, t[Ite]_3

Defined Pair Symbols:   Q[ITE]_3, R[ITE]_3, P[ITE]_3, Q[ITE][FALSE][ITE]_3, R_2, Q_2, P_2

Compound Symbols:   c4_2, c5_2, c26_2, c27_2, c32_2, c33_2, c38_2, c39_2, c72_2, c73_2, c74_2


----------------------------------------

(7) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID))
Removed 11 trailing tuple parts
----------------------------------------

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1)))
   q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil))
   q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil))
   q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil))
   q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil))
   q[Ite](True, z0, z1) -> True
   r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1))
   r[Ite](False, z0, Cons(T, z1)) -> False
   r[Ite](False, z0, Cons(B, z1)) -> False
   r[Ite](False, z0, Cons(A, z1)) -> False
   r[Ite](True, z0, z1) -> True
   p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1))
   p[Ite](False, z0, Cons(T, z1)) -> False
   p[Ite](False, z0, Cons(B, z1)) -> False
   p[Ite](False, z0, Cons(A, z1)) -> False
   p[Ite](True, z0, z1) -> True
   q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2))
   q[Ite][False][Ite](False, z0, z1) -> False
   t[Ite](False, z0, z1) -> True
   t[Ite](True, z0, z1) -> True
   head(Cons(z0, z1)) -> z0
   e(Cons(F, Nil), z0) -> False
   e(Cons(T, Nil), z0) -> False
   e(Cons(B, Nil), z0) -> False
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0)
   e(Cons(F, Cons(z0, z1)), z2) -> False
   e(Cons(T, Cons(z0, z1)), z2) -> False
   e(Cons(B, Cons(z0, z1)), z2) -> False
   e(Cons(A, Cons(z0, z1)), z2) -> False
   e(Nil, z0) -> False
   equal(F, F) -> True
   equal(F, T) -> False
   equal(F, B) -> False
   equal(F, A) -> False
   equal(T, F) -> False
   equal(T, T) -> True
   equal(T, B) -> False
   equal(T, A) -> False
   equal(B, F) -> False
   equal(B, T) -> False
   equal(B, B) -> True
   equal(B, A) -> False
   equal(A, F) -> False
   equal(A, T) -> False
   equal(A, B) -> False
   equal(A, A) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   t(z0, z1) -> t[Ite](e(z0, z1), z0, z1)
   r(z0, z1) -> r[Ite](e(z0, z1), z0, z1)
   q(z0, z1) -> q[Ite](e(z0, z1), z0, z1)
   p(z0, z1) -> p[Ite](e(z0, z1), z0, z1)
   goal(z0, z1) -> q(z0, z1)
Tuples:
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1))))
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1)))
   R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1))
   R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1))
   P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1)))
   P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1))
   Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c38(P(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c39(Q(z0, z2))
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
S tuples:
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
K tuples:none
Defined Rule Symbols:   head_1, e_2, equal_2, notEmpty_1, t_2, r_2, q_2, p_2, goal_2, and_2, q[Ite]_3, r[Ite]_3, p[Ite]_3, q[Ite][False][Ite]_3, t[Ite]_3

Defined Pair Symbols:   Q[ITE]_3, R[ITE]_3, P[ITE]_3, Q[ITE][FALSE][ITE]_3, R_2, Q_2, P_2

Compound Symbols:   c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c38_1, c39_1, c72_1, c73_1, c74_1


----------------------------------------

(9) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 2 leading nodes:
   Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c38(P(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE](True, z0, Cons(z1, z2)) -> c39(Q(z0, z2))

----------------------------------------

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1)))
   q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil))
   q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil))
   q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil))
   q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil))
   q[Ite](True, z0, z1) -> True
   r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1))
   r[Ite](False, z0, Cons(T, z1)) -> False
   r[Ite](False, z0, Cons(B, z1)) -> False
   r[Ite](False, z0, Cons(A, z1)) -> False
   r[Ite](True, z0, z1) -> True
   p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1))
   p[Ite](False, z0, Cons(T, z1)) -> False
   p[Ite](False, z0, Cons(B, z1)) -> False
   p[Ite](False, z0, Cons(A, z1)) -> False
   p[Ite](True, z0, z1) -> True
   q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2))
   q[Ite][False][Ite](False, z0, z1) -> False
   t[Ite](False, z0, z1) -> True
   t[Ite](True, z0, z1) -> True
   head(Cons(z0, z1)) -> z0
   e(Cons(F, Nil), z0) -> False
   e(Cons(T, Nil), z0) -> False
   e(Cons(B, Nil), z0) -> False
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0)
   e(Cons(F, Cons(z0, z1)), z2) -> False
   e(Cons(T, Cons(z0, z1)), z2) -> False
   e(Cons(B, Cons(z0, z1)), z2) -> False
   e(Cons(A, Cons(z0, z1)), z2) -> False
   e(Nil, z0) -> False
   equal(F, F) -> True
   equal(F, T) -> False
   equal(F, B) -> False
   equal(F, A) -> False
   equal(T, F) -> False
   equal(T, T) -> True
   equal(T, B) -> False
   equal(T, A) -> False
   equal(B, F) -> False
   equal(B, T) -> False
   equal(B, B) -> True
   equal(B, A) -> False
   equal(A, F) -> False
   equal(A, T) -> False
   equal(A, B) -> False
   equal(A, A) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   t(z0, z1) -> t[Ite](e(z0, z1), z0, z1)
   r(z0, z1) -> r[Ite](e(z0, z1), z0, z1)
   q(z0, z1) -> q[Ite](e(z0, z1), z0, z1)
   p(z0, z1) -> p[Ite](e(z0, z1), z0, z1)
   goal(z0, z1) -> q(z0, z1)
Tuples:
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1))))
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1)))
   R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1))
   R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1))
   P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1)))
   P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1))
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
S tuples:
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
K tuples:none
Defined Rule Symbols:   head_1, e_2, equal_2, notEmpty_1, t_2, r_2, q_2, p_2, goal_2, and_2, q[Ite]_3, r[Ite]_3, p[Ite]_3, q[Ite][False][Ite]_3, t[Ite]_3

Defined Pair Symbols:   Q[ITE]_3, R[ITE]_3, P[ITE]_3, R_2, Q_2, P_2

Compound Symbols:   c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c72_1, c73_1, c74_1


----------------------------------------

(11) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   q[Ite](False, z0, Cons(F, Cons(F, z1))) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), z0, Cons(F, Cons(F, z1)))
   q[Ite](False, z0, Cons(F, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(F, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(T, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(B, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(F, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(T, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(B, z1))) -> False
   q[Ite](False, z0, Cons(A, Cons(A, z1))) -> False
   q[Ite](False, z0, Cons(F, Nil)) -> q[Ite][False][Ite](and(True, and(True, and(False, equal(head(Nil), F)))), z0, Cons(F, Nil))
   q[Ite](False, z0, Cons(T, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(T, Nil))
   q[Ite](False, z0, Cons(B, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(B, Nil))
   q[Ite](False, z0, Cons(A, Nil)) -> q[Ite][False][Ite](and(True, and(False, and(False, equal(head(Nil), F)))), z0, Cons(A, Nil))
   q[Ite](True, z0, z1) -> True
   r[Ite](False, z0, Cons(F, z1)) -> r[Ite][False][Ite][True][Ite](and(q(z0, z1), r(z0, z1)), z0, Cons(F, z1))
   r[Ite](False, z0, Cons(T, z1)) -> False
   r[Ite](False, z0, Cons(B, z1)) -> False
   r[Ite](False, z0, Cons(A, z1)) -> False
   r[Ite](True, z0, z1) -> True
   p[Ite](False, z0, Cons(F, z1)) -> and(r(z0, Cons(F, z1)), p(z0, z1))
   p[Ite](False, z0, Cons(T, z1)) -> False
   p[Ite](False, z0, Cons(B, z1)) -> False
   p[Ite](False, z0, Cons(A, z1)) -> False
   p[Ite](True, z0, z1) -> True
   q[Ite][False][Ite](True, z0, Cons(z1, z2)) -> q[Ite][False][Ite][True][Ite](and(p(z0, Cons(z1, z2)), q(z0, z2)), z0, Cons(z1, z2))
   q[Ite][False][Ite](False, z0, z1) -> False
   t[Ite](False, z0, z1) -> True
   t[Ite](True, z0, z1) -> True
   head(Cons(z0, z1)) -> z0
   equal(F, F) -> True
   equal(F, T) -> False
   equal(F, B) -> False
   equal(F, A) -> False
   equal(T, F) -> False
   equal(T, T) -> True
   equal(T, B) -> False
   equal(T, A) -> False
   equal(B, F) -> False
   equal(B, T) -> False
   equal(B, B) -> True
   equal(B, A) -> False
   equal(A, F) -> False
   equal(A, T) -> False
   equal(A, B) -> False
   equal(A, A) -> True
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   t(z0, z1) -> t[Ite](e(z0, z1), z0, z1)
   r(z0, z1) -> r[Ite](e(z0, z1), z0, z1)
   q(z0, z1) -> q[Ite](e(z0, z1), z0, z1)
   p(z0, z1) -> p[Ite](e(z0, z1), z0, z1)
   goal(z0, z1) -> q(z0, z1)

----------------------------------------

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   e(Cons(F, Nil), z0) -> False
   e(Cons(T, Nil), z0) -> False
   e(Cons(B, Nil), z0) -> False
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0)
   e(Cons(F, Cons(z0, z1)), z2) -> False
   e(Cons(T, Cons(z0, z1)), z2) -> False
   e(Cons(B, Cons(z0, z1)), z2) -> False
   e(Cons(A, Cons(z0, z1)), z2) -> False
   e(Nil, z0) -> False
Tuples:
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1))))
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1)))
   R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1))
   R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1))
   P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1)))
   P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1))
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
S tuples:
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
K tuples:none
Defined Rule Symbols:   e_2

Defined Pair Symbols:   Q[ITE]_3, R[ITE]_3, P[ITE]_3, R_2, Q_2, P_2

Compound Symbols:   c4_1, c5_1, c26_1, c27_1, c32_1, c33_1, c72_1, c73_1, c74_1


----------------------------------------

(13) CdtToCpxRelTrsProof (BOTH BOUNDS(ID, ID))
Converted S to standard rules, and D \ S as well as R to relative rules.
----------------------------------------

(14)
Obligation:
The Runtime Complexity (innermost) of the given CpxRelTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))

The (relative) TRS S consists of the following rules:

   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1))))
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1)))
   R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1))
   R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1))
   P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1)))
   P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1))
   e(Cons(F, Nil), z0) -> False
   e(Cons(T, Nil), z0) -> False
   e(Cons(B, Nil), z0) -> False
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0)
   e(Cons(F, Cons(z0, z1)), z2) -> False
   e(Cons(T, Cons(z0, z1)), z2) -> False
   e(Cons(B, Cons(z0, z1)), z2) -> False
   e(Cons(A, Cons(z0, z1)), z2) -> False
   e(Nil, z0) -> False

Rewrite Strategy: INNERMOST
----------------------------------------

(15) RelTrsToWeightedTrsProof (BOTH BOUNDS(ID, ID))
Transformed relative TRS to weighted TRS
----------------------------------------

(16)
Obligation:
The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) [1]
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) [1]
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) [1]
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) [0]
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) [0]
   R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) [0]
   R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) [0]
   P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) [0]
   P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) [0]
   e(Cons(F, Nil), z0) -> False [0]
   e(Cons(T, Nil), z0) -> False [0]
   e(Cons(B, Nil), z0) -> False [0]
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) [0]
   e(Cons(F, Cons(z0, z1)), z2) -> False [0]
   e(Cons(T, Cons(z0, z1)), z2) -> False [0]
   e(Cons(B, Cons(z0, z1)), z2) -> False [0]
   e(Cons(A, Cons(z0, z1)), z2) -> False [0]
   e(Nil, z0) -> False [0]

Rewrite Strategy: INNERMOST
----------------------------------------

(17) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Infered types.
----------------------------------------

(18)
Obligation:
Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) [1]
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) [1]
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) [1]
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) [0]
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) [0]
   R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) [0]
   R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) [0]
   P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) [0]
   P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) [0]
   e(Cons(F, Nil), z0) -> False [0]
   e(Cons(T, Nil), z0) -> False [0]
   e(Cons(B, Nil), z0) -> False [0]
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) [0]
   e(Cons(F, Cons(z0, z1)), z2) -> False [0]
   e(Cons(T, Cons(z0, z1)), z2) -> False [0]
   e(Cons(B, Cons(z0, z1)), z2) -> False [0]
   e(Cons(A, Cons(z0, z1)), z2) -> False [0]
   e(Nil, z0) -> False [0]

The TRS has the following type information:
R :: Cons:Nil -> Cons:Nil -> c72
c72 :: c26:c27 -> c72
R[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c26:c27
e :: Cons:Nil -> Cons:Nil -> False:e[Match][Cons][Ite][True][Match]
Q :: Cons:Nil -> Cons:Nil -> c73
c73 :: c4:c5 -> c73
Q[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c4:c5
P :: Cons:Nil -> Cons:Nil -> c74
c74 :: c32:c33 -> c74
P[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c32:c33
False :: False:e[Match][Cons][Ite][True][Match]
Cons :: F:T:B:A -> Cons:Nil -> Cons:Nil
F :: F:T:B:A
c4 :: c74 -> c4:c5
c5 :: c73 -> c4:c5
c26 :: c73 -> c26:c27
c27 :: c72 -> c26:c27
c32 :: c72 -> c32:c33
c33 :: c74 -> c32:c33
Nil :: Cons:Nil
T :: F:T:B:A
B :: F:T:B:A
A :: F:T:B:A
e[Match][Cons][Ite][True][Match] :: F:T:B:A -> Cons:Nil -> Cons:Nil -> False:e[Match][Cons][Ite][True][Match]

Rewrite Strategy: INNERMOST
----------------------------------------

(19) CompletionProof (UPPER BOUND(ID))
The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

   R_2
   Q_2
   P_2

(c) The following functions are completely defined:

   Q[ITE]_3
   R[ITE]_3
   P[ITE]_3
   e_2

Due to the following rules being added:

   Q[ITE](v0, v1, v2) -> const3 [0]
   R[ITE](v0, v1, v2) -> const1 [0]
   P[ITE](v0, v1, v2) -> const5 [0]
   e(v0, v1) -> False [0]

And the following fresh constants:    const3, const1, const5, const, const2, const4

----------------------------------------

(20)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1)) [1]
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1)) [1]
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1)) [1]
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) [0]
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) [0]
   R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) [0]
   R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) [0]
   P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) [0]
   P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) [0]
   e(Cons(F, Nil), z0) -> False [0]
   e(Cons(T, Nil), z0) -> False [0]
   e(Cons(B, Nil), z0) -> False [0]
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) [0]
   e(Cons(F, Cons(z0, z1)), z2) -> False [0]
   e(Cons(T, Cons(z0, z1)), z2) -> False [0]
   e(Cons(B, Cons(z0, z1)), z2) -> False [0]
   e(Cons(A, Cons(z0, z1)), z2) -> False [0]
   e(Nil, z0) -> False [0]
   Q[ITE](v0, v1, v2) -> const3 [0]
   R[ITE](v0, v1, v2) -> const1 [0]
   P[ITE](v0, v1, v2) -> const5 [0]
   e(v0, v1) -> False [0]

The TRS has the following type information:
R :: Cons:Nil -> Cons:Nil -> c72
c72 :: c26:c27:const1 -> c72
R[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c26:c27:const1
e :: Cons:Nil -> Cons:Nil -> False:e[Match][Cons][Ite][True][Match]
Q :: Cons:Nil -> Cons:Nil -> c73
c73 :: c4:c5:const3 -> c73
Q[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c4:c5:const3
P :: Cons:Nil -> Cons:Nil -> c74
c74 :: c32:c33:const5 -> c74
P[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c32:c33:const5
False :: False:e[Match][Cons][Ite][True][Match]
Cons :: F:T:B:A -> Cons:Nil -> Cons:Nil
F :: F:T:B:A
c4 :: c74 -> c4:c5:const3
c5 :: c73 -> c4:c5:const3
c26 :: c73 -> c26:c27:const1
c27 :: c72 -> c26:c27:const1
c32 :: c72 -> c32:c33:const5
c33 :: c74 -> c32:c33:const5
Nil :: Cons:Nil
T :: F:T:B:A
B :: F:T:B:A
A :: F:T:B:A
e[Match][Cons][Ite][True][Match] :: F:T:B:A -> Cons:Nil -> Cons:Nil -> False:e[Match][Cons][Ite][True][Match]
const3 :: c4:c5:const3
const1 :: c26:c27:const1
const5 :: c32:c33:const5
const :: c72
const2 :: c73
const4 :: c74

Rewrite Strategy: INNERMOST
----------------------------------------

(21) NarrowingProof (BOTH BOUNDS(ID, ID))
Narrowed the inner basic terms of all right-hand sides by a single narrowing step.
----------------------------------------

(22)
Obligation:
Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

   R(Cons(F, Nil), z1) -> c72(R[ITE](False, Cons(F, Nil), z1)) [1]
   R(Cons(T, Nil), z1) -> c72(R[ITE](False, Cons(T, Nil), z1)) [1]
   R(Cons(B, Nil), z1) -> c72(R[ITE](False, Cons(B, Nil), z1)) [1]
   R(Cons(A, Nil), z1) -> c72(R[ITE](e[Match][Cons][Ite][True][Match](A, Nil, z1), Cons(A, Nil), z1)) [1]
   R(Cons(F, Cons(z0', z1')), z1) -> c72(R[ITE](False, Cons(F, Cons(z0', z1')), z1)) [1]
   R(Cons(T, Cons(z0'', z1'')), z1) -> c72(R[ITE](False, Cons(T, Cons(z0'', z1'')), z1)) [1]
   R(Cons(B, Cons(z01, z11)), z1) -> c72(R[ITE](False, Cons(B, Cons(z01, z11)), z1)) [1]
   R(Cons(A, Cons(z02, z12)), z1) -> c72(R[ITE](False, Cons(A, Cons(z02, z12)), z1)) [1]
   R(Nil, z1) -> c72(R[ITE](False, Nil, z1)) [1]
   R(z0, z1) -> c72(R[ITE](False, z0, z1)) [1]
   Q(Cons(F, Nil), z1) -> c73(Q[ITE](False, Cons(F, Nil), z1)) [1]
   Q(Cons(T, Nil), z1) -> c73(Q[ITE](False, Cons(T, Nil), z1)) [1]
   Q(Cons(B, Nil), z1) -> c73(Q[ITE](False, Cons(B, Nil), z1)) [1]
   Q(Cons(A, Nil), z1) -> c73(Q[ITE](e[Match][Cons][Ite][True][Match](A, Nil, z1), Cons(A, Nil), z1)) [1]
   Q(Cons(F, Cons(z03, z13)), z1) -> c73(Q[ITE](False, Cons(F, Cons(z03, z13)), z1)) [1]
   Q(Cons(T, Cons(z04, z14)), z1) -> c73(Q[ITE](False, Cons(T, Cons(z04, z14)), z1)) [1]
   Q(Cons(B, Cons(z05, z15)), z1) -> c73(Q[ITE](False, Cons(B, Cons(z05, z15)), z1)) [1]
   Q(Cons(A, Cons(z06, z16)), z1) -> c73(Q[ITE](False, Cons(A, Cons(z06, z16)), z1)) [1]
   Q(Nil, z1) -> c73(Q[ITE](False, Nil, z1)) [1]
   Q(z0, z1) -> c73(Q[ITE](False, z0, z1)) [1]
   P(Cons(F, Nil), z1) -> c74(P[ITE](False, Cons(F, Nil), z1)) [1]
   P(Cons(T, Nil), z1) -> c74(P[ITE](False, Cons(T, Nil), z1)) [1]
   P(Cons(B, Nil), z1) -> c74(P[ITE](False, Cons(B, Nil), z1)) [1]
   P(Cons(A, Nil), z1) -> c74(P[ITE](e[Match][Cons][Ite][True][Match](A, Nil, z1), Cons(A, Nil), z1)) [1]
   P(Cons(F, Cons(z07, z17)), z1) -> c74(P[ITE](False, Cons(F, Cons(z07, z17)), z1)) [1]
   P(Cons(T, Cons(z08, z18)), z1) -> c74(P[ITE](False, Cons(T, Cons(z08, z18)), z1)) [1]
   P(Cons(B, Cons(z09, z19)), z1) -> c74(P[ITE](False, Cons(B, Cons(z09, z19)), z1)) [1]
   P(Cons(A, Cons(z010, z110)), z1) -> c74(P[ITE](False, Cons(A, Cons(z010, z110)), z1)) [1]
   P(Nil, z1) -> c74(P[ITE](False, Nil, z1)) [1]
   P(z0, z1) -> c74(P[ITE](False, z0, z1)) [1]
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c4(P(z0, Cons(F, Cons(F, z1)))) [0]
   Q[ITE](False, z0, Cons(F, Cons(F, z1))) -> c5(Q(z0, Cons(F, z1))) [0]
   R[ITE](False, z0, Cons(F, z1)) -> c26(Q(z0, z1)) [0]
   R[ITE](False, z0, Cons(F, z1)) -> c27(R(z0, z1)) [0]
   P[ITE](False, z0, Cons(F, z1)) -> c32(R(z0, Cons(F, z1))) [0]
   P[ITE](False, z0, Cons(F, z1)) -> c33(P(z0, z1)) [0]
   e(Cons(F, Nil), z0) -> False [0]
   e(Cons(T, Nil), z0) -> False [0]
   e(Cons(B, Nil), z0) -> False [0]
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0) [0]
   e(Cons(F, Cons(z0, z1)), z2) -> False [0]
   e(Cons(T, Cons(z0, z1)), z2) -> False [0]
   e(Cons(B, Cons(z0, z1)), z2) -> False [0]
   e(Cons(A, Cons(z0, z1)), z2) -> False [0]
   e(Nil, z0) -> False [0]
   Q[ITE](v0, v1, v2) -> const3 [0]
   R[ITE](v0, v1, v2) -> const1 [0]
   P[ITE](v0, v1, v2) -> const5 [0]
   e(v0, v1) -> False [0]

The TRS has the following type information:
R :: Cons:Nil -> Cons:Nil -> c72
c72 :: c26:c27:const1 -> c72
R[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c26:c27:const1
e :: Cons:Nil -> Cons:Nil -> False:e[Match][Cons][Ite][True][Match]
Q :: Cons:Nil -> Cons:Nil -> c73
c73 :: c4:c5:const3 -> c73
Q[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c4:c5:const3
P :: Cons:Nil -> Cons:Nil -> c74
c74 :: c32:c33:const5 -> c74
P[ITE] :: False:e[Match][Cons][Ite][True][Match] -> Cons:Nil -> Cons:Nil -> c32:c33:const5
False :: False:e[Match][Cons][Ite][True][Match]
Cons :: F:T:B:A -> Cons:Nil -> Cons:Nil
F :: F:T:B:A
c4 :: c74 -> c4:c5:const3
c5 :: c73 -> c4:c5:const3
c26 :: c73 -> c26:c27:const1
c27 :: c72 -> c26:c27:const1
c32 :: c72 -> c32:c33:const5
c33 :: c74 -> c32:c33:const5
Nil :: Cons:Nil
T :: F:T:B:A
B :: F:T:B:A
A :: F:T:B:A
e[Match][Cons][Ite][True][Match] :: F:T:B:A -> Cons:Nil -> Cons:Nil -> False:e[Match][Cons][Ite][True][Match]
const3 :: c4:c5:const3
const1 :: c26:c27:const1
const5 :: c32:c33:const5
const :: c72
const2 :: c73
const4 :: c74

Rewrite Strategy: INNERMOST
----------------------------------------

(23) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID))
Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

   False => 0
   F => 2
   Nil => 0
   T => 3
   B => 1
   A => 0
   const3 => 0
   const1 => 0
   const5 => 0
   const => 0
   const2 => 0
   const4 => 0

----------------------------------------

(24)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z1) :|: z1 >= 0, z' = z1, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z1) :|: z1 >= 0, z' = z1, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z1) :|: z08 >= 0, z18 >= 0, z1 >= 0, z = 1 + 3 + (1 + z08 + z18), z' = z1
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z1) :|: z1 >= 0, z = 1 + 2 + 0, z' = z1
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z1) :|: z1 >= 0, z07 >= 0, z17 >= 0, z' = z1, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z1) :|: z = 1 + 1 + 0, z1 >= 0, z' = z1
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z1) :|: z1 >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z' = z1, z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z1) :|: z110 >= 0, z1 >= 0, z = 1 + 0 + (1 + z010 + z110), z' = z1, z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z1, 1 + 0 + 0, z1) :|: z = 1 + 0 + 0, z1 >= 0, z' = z1
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z0, 1 + 2 + z1) :|: z1 >= 0, z0 >= 0, z = 0, z'' = 1 + 2 + z1, z' = z0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z0, z1) :|: z1 >= 0, z0 >= 0, z = 0, z'' = 1 + 2 + z1, z' = z0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z1) :|: z1 >= 0, z' = z1, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z1) :|: z1 >= 0, z' = z1, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z1) :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z1 >= 0, z' = z1, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z1) :|: z1 >= 0, z = 1 + 2 + 0, z' = z1
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z1) :|: z1 >= 0, z = 1 + 2 + (1 + z03 + z13), z' = z1, z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z1) :|: z = 1 + 1 + 0, z1 >= 0, z' = z1
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z1) :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z1 >= 0, z' = z1, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z1) :|: z1 >= 0, z06 >= 0, z' = z1, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z1, 1 + 0 + 0, z1) :|: z = 1 + 0 + 0, z1 >= 0, z' = z1
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z0, 1 + 2 + z1) :|: z1 >= 0, z'' = 1 + 2 + (1 + 2 + z1), z0 >= 0, z = 0, z' = z0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z0, 1 + 2 + (1 + 2 + z1)) :|: z1 >= 0, z'' = 1 + 2 + (1 + 2 + z1), z0 >= 0, z = 0, z' = z0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z0, z1) :|: z = z0, z1 >= 0, z' = z1, z0 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z1) :|: z1 >= 0, z' = z1, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z1) :|: z1 >= 0, z' = z1, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z1) :|: z1 >= 0, z' = z1, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z1) :|: z1 >= 0, z = 1 + 2 + 0, z' = z1
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z1) :|: z1 >= 0, z0' >= 0, z1' >= 0, z' = z1, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z1) :|: z = 1 + 1 + 0, z1 >= 0, z' = z1
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z1) :|: z11 >= 0, z1 >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11), z' = z1
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z1) :|: z1 >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z' = z1, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z1, 1 + 0 + 0, z1) :|: z = 1 + 0 + 0, z1 >= 0, z' = z1
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: v0 >= 0, z'' = v2, v1 >= 0, z = v0, z' = v1, v2 >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z0, z1) :|: z1 >= 0, z0 >= 0, z = 0, z'' = 1 + 2 + z1, z' = z0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z0, z1) :|: z1 >= 0, z0 >= 0, z = 0, z'' = 1 + 2 + z1, z' = z0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z0 >= 0, z' = z0
   e(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 1 + 3 + 0, z' = z0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z0 >= 0, z' = z0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z' = z2, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z2 >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z' = z2, z0 >= 0, z2 >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z' = z2, z0 >= 0, z2 >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z' = z2, z0 >= 0, z2 >= 0
   e(z, z') -{ 0 }-> 0 :|: z0 >= 0, z = 0, z' = z0
   e(z, z') -{ 0 }-> 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z0 :|: z = 1 + 0 + 0, z0 >= 0, z' = z0


----------------------------------------

(25) SimplificationProof (BOTH BOUNDS(ID, ID))
Simplified the RNTS by moving equalities from the constraints into the right-hand sides.
----------------------------------------

(26)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z, z') :|: z' >= 0, z >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z') :|: z' >= 0, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z') :|: z08 >= 0, z18 >= 0, z' >= 0, z = 1 + 3 + (1 + z08 + z18)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z') :|: z' >= 0, z07 >= 0, z17 >= 0, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z') :|: z' >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z') :|: z110 >= 0, z' >= 0, z = 1 + 0 + (1 + z010 + z110), z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z', 1 + 2 + (z'' - 3)) :|: z'' - 3 >= 0, z' >= 0, z = 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z, z') :|: z' >= 0, z >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z') :|: z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z') :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z' >= 0, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z') :|: z' >= 0, z = 1 + 2 + (1 + z03 + z13), z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z') :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z' >= 0, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z') :|: z' >= 0, z06 >= 0, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', 1 + 2 + (z'' - 6)) :|: z'' - 6 >= 0, z' >= 0, z = 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z', 1 + 2 + (1 + 2 + (z'' - 6))) :|: z'' - 6 >= 0, z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z, z') :|: z' >= 0, z >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z') :|: z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z') :|: z' >= 0, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z') :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z') :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11)
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z') :|: z' >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 1 + 3 + 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z' :|: z = 1 + 0 + 0, z' >= 0


----------------------------------------

(27) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID))
Found the following analysis order by SCC decomposition:

   { e }
   { Q, Q[ITE], R[ITE], P[ITE], P, R }

----------------------------------------

(28)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z, z') :|: z' >= 0, z >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z') :|: z' >= 0, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z') :|: z08 >= 0, z18 >= 0, z' >= 0, z = 1 + 3 + (1 + z08 + z18)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z') :|: z' >= 0, z07 >= 0, z17 >= 0, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z') :|: z' >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z') :|: z110 >= 0, z' >= 0, z = 1 + 0 + (1 + z010 + z110), z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z', 1 + 2 + (z'' - 3)) :|: z'' - 3 >= 0, z' >= 0, z = 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z, z') :|: z' >= 0, z >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z') :|: z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z') :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z' >= 0, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z') :|: z' >= 0, z = 1 + 2 + (1 + z03 + z13), z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z') :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z' >= 0, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z') :|: z' >= 0, z06 >= 0, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', 1 + 2 + (z'' - 6)) :|: z'' - 6 >= 0, z' >= 0, z = 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z', 1 + 2 + (1 + 2 + (z'' - 6))) :|: z'' - 6 >= 0, z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z, z') :|: z' >= 0, z >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z') :|: z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z') :|: z' >= 0, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z') :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z') :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11)
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z') :|: z' >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 1 + 3 + 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z' :|: z = 1 + 0 + 0, z' >= 0

Function symbols to be analyzed: {e}, {Q,Q[ITE],R[ITE],P[ITE],P,R}

----------------------------------------

(29) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(30)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z, z') :|: z' >= 0, z >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z') :|: z' >= 0, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z') :|: z08 >= 0, z18 >= 0, z' >= 0, z = 1 + 3 + (1 + z08 + z18)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z') :|: z' >= 0, z07 >= 0, z17 >= 0, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z') :|: z' >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z') :|: z110 >= 0, z' >= 0, z = 1 + 0 + (1 + z010 + z110), z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z', 1 + 2 + (z'' - 3)) :|: z'' - 3 >= 0, z' >= 0, z = 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z, z') :|: z' >= 0, z >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z') :|: z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z') :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z' >= 0, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z') :|: z' >= 0, z = 1 + 2 + (1 + z03 + z13), z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z') :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z' >= 0, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z') :|: z' >= 0, z06 >= 0, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', 1 + 2 + (z'' - 6)) :|: z'' - 6 >= 0, z' >= 0, z = 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z', 1 + 2 + (1 + 2 + (z'' - 6))) :|: z'' - 6 >= 0, z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z, z') :|: z' >= 0, z >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z') :|: z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z') :|: z' >= 0, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z') :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z') :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11)
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z') :|: z' >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 1 + 3 + 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z' :|: z = 1 + 0 + 0, z' >= 0

Function symbols to be analyzed: {e}, {Q,Q[ITE],R[ITE],P[ITE],P,R}

----------------------------------------

(31) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using CoFloCo for: e
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + z'

----------------------------------------

(32)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z, z') :|: z' >= 0, z >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z') :|: z' >= 0, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z') :|: z08 >= 0, z18 >= 0, z' >= 0, z = 1 + 3 + (1 + z08 + z18)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z') :|: z' >= 0, z07 >= 0, z17 >= 0, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z') :|: z' >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z') :|: z110 >= 0, z' >= 0, z = 1 + 0 + (1 + z010 + z110), z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z', 1 + 2 + (z'' - 3)) :|: z'' - 3 >= 0, z' >= 0, z = 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z, z') :|: z' >= 0, z >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z') :|: z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z') :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z' >= 0, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z') :|: z' >= 0, z = 1 + 2 + (1 + z03 + z13), z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z') :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z' >= 0, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z') :|: z' >= 0, z06 >= 0, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', 1 + 2 + (z'' - 6)) :|: z'' - 6 >= 0, z' >= 0, z = 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z', 1 + 2 + (1 + 2 + (z'' - 6))) :|: z'' - 6 >= 0, z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z, z') :|: z' >= 0, z >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z') :|: z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z') :|: z' >= 0, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z') :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z') :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11)
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z') :|: z' >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 1 + 3 + 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z' :|: z = 1 + 0 + 0, z' >= 0

Function symbols to be analyzed: {e}, {Q,Q[ITE],R[ITE],P[ITE],P,R}
Previous analysis results are:
  e: runtime: ?, size: O(n^1) [1 + z']

----------------------------------------

(33) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using CoFloCo for: e
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

----------------------------------------

(34)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z, z') :|: z' >= 0, z >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z') :|: z' >= 0, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z') :|: z08 >= 0, z18 >= 0, z' >= 0, z = 1 + 3 + (1 + z08 + z18)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z') :|: z' >= 0, z07 >= 0, z17 >= 0, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z') :|: z' >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z') :|: z110 >= 0, z' >= 0, z = 1 + 0 + (1 + z010 + z110), z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z', 1 + 2 + (z'' - 3)) :|: z'' - 3 >= 0, z' >= 0, z = 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z, z') :|: z' >= 0, z >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z') :|: z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z') :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z' >= 0, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z') :|: z' >= 0, z = 1 + 2 + (1 + z03 + z13), z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z') :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z' >= 0, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z') :|: z' >= 0, z06 >= 0, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', 1 + 2 + (z'' - 6)) :|: z'' - 6 >= 0, z' >= 0, z = 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z', 1 + 2 + (1 + 2 + (z'' - 6))) :|: z'' - 6 >= 0, z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z, z') :|: z' >= 0, z >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z') :|: z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z') :|: z' >= 0, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z') :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z') :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11)
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z') :|: z' >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 1 + 3 + 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z' :|: z = 1 + 0 + 0, z' >= 0

Function symbols to be analyzed: {Q,Q[ITE],R[ITE],P[ITE],P,R}
Previous analysis results are:
  e: runtime: O(1) [0], size: O(n^1) [1 + z']

----------------------------------------

(35) ResultPropagationProof (UPPER BOUND(ID))
Applied inner abstraction using the recently inferred runtime/size bounds where possible.
----------------------------------------

(36)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z, z') :|: z' >= 0, z >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z') :|: z' >= 0, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z') :|: z08 >= 0, z18 >= 0, z' >= 0, z = 1 + 3 + (1 + z08 + z18)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z') :|: z' >= 0, z07 >= 0, z17 >= 0, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z') :|: z' >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z') :|: z110 >= 0, z' >= 0, z = 1 + 0 + (1 + z010 + z110), z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z', 1 + 2 + (z'' - 3)) :|: z'' - 3 >= 0, z' >= 0, z = 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z, z') :|: z' >= 0, z >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z') :|: z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z') :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z' >= 0, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z') :|: z' >= 0, z = 1 + 2 + (1 + z03 + z13), z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z') :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z' >= 0, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z') :|: z' >= 0, z06 >= 0, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', 1 + 2 + (z'' - 6)) :|: z'' - 6 >= 0, z' >= 0, z = 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z', 1 + 2 + (1 + 2 + (z'' - 6))) :|: z'' - 6 >= 0, z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z, z') :|: z' >= 0, z >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z') :|: z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z') :|: z' >= 0, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z') :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z') :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11)
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z') :|: z' >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 1 + 3 + 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z' :|: z = 1 + 0 + 0, z' >= 0

Function symbols to be analyzed: {Q,Q[ITE],R[ITE],P[ITE],P,R}
Previous analysis results are:
  e: runtime: O(1) [0], size: O(n^1) [1 + z']

----------------------------------------

(37) IntTrsBoundProof (UPPER BOUND(ID))

Computed SIZE bound using KoAT for: Q
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 5 + 2*z'

Computed SIZE bound using CoFloCo for: Q[ITE]
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 4 + 2*z''

Computed SIZE bound using KoAT for: R[ITE]
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 2*z''

Computed SIZE bound using KoAT for: P[ITE]
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 2 + 2*z''

Computed SIZE bound using CoFloCo for: P
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 3 + 2*z'

Computed SIZE bound using CoFloCo for: R
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + 2*z'

----------------------------------------

(38)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z, z') :|: z' >= 0, z >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z') :|: z' >= 0, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z') :|: z08 >= 0, z18 >= 0, z' >= 0, z = 1 + 3 + (1 + z08 + z18)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z') :|: z' >= 0, z07 >= 0, z17 >= 0, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z') :|: z' >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z') :|: z110 >= 0, z' >= 0, z = 1 + 0 + (1 + z010 + z110), z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z', 1 + 2 + (z'' - 3)) :|: z'' - 3 >= 0, z' >= 0, z = 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z, z') :|: z' >= 0, z >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z') :|: z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z') :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z' >= 0, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z') :|: z' >= 0, z = 1 + 2 + (1 + z03 + z13), z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z') :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z' >= 0, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z') :|: z' >= 0, z06 >= 0, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', 1 + 2 + (z'' - 6)) :|: z'' - 6 >= 0, z' >= 0, z = 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z', 1 + 2 + (1 + 2 + (z'' - 6))) :|: z'' - 6 >= 0, z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z, z') :|: z' >= 0, z >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z') :|: z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z') :|: z' >= 0, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z') :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z') :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11)
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z') :|: z' >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 1 + 3 + 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z' :|: z = 1 + 0 + 0, z' >= 0

Function symbols to be analyzed: {Q,Q[ITE],R[ITE],P[ITE],P,R}
Previous analysis results are:
  e: runtime: O(1) [0], size: O(n^1) [1 + z']
  Q: runtime: ?, size: O(n^1) [5 + 2*z']
  Q[ITE]: runtime: ?, size: O(n^1) [4 + 2*z'']
  R[ITE]: runtime: ?, size: O(n^1) [2*z'']
  P[ITE]: runtime: ?, size: O(n^1) [2 + 2*z'']
  P: runtime: ?, size: O(n^1) [3 + 2*z']
  R: runtime: ?, size: O(n^1) [1 + 2*z']

----------------------------------------

(39) IntTrsBoundProof (UPPER BOUND(ID))

Computed RUNTIME bound using KoAT for: Q
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 150 + 60*z'

Computed RUNTIME bound using CoFloCo for: Q[ITE]
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 32 + 60*z''

Computed RUNTIME bound using KoAT for: R[ITE]
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 80*z''

Computed RUNTIME bound using CoFloCo for: P[ITE]
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 4 + 80*z''

Computed RUNTIME bound using CoFloCo for: P
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 5 + 80*z'

Computed RUNTIME bound using CoFloCo for: R
after applying outer abstraction to obtain an ITS,
resulting in: O(n^1) with polynomial bound: 1 + 80*z'

----------------------------------------

(40)
Obligation:
Complexity RNTS consisting of the following rules:

   P(z, z') -{ 1 }-> 1 + P[ITE](0, z, z') :|: z' >= 0, z >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 0, z') :|: z' >= 0, z = 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 3 + (1 + z08 + z18), z') :|: z08 >= 0, z18 >= 0, z' >= 0, z = 1 + 3 + (1 + z08 + z18)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 2 + (1 + z07 + z17), z') :|: z' >= 0, z07 >= 0, z17 >= 0, z = 1 + 2 + (1 + z07 + z17)
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 1 + (1 + z09 + z19), z') :|: z' >= 0, z19 >= 0, z = 1 + 1 + (1 + z09 + z19), z09 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](0, 1 + 0 + (1 + z010 + z110), z') :|: z110 >= 0, z' >= 0, z = 1 + 0 + (1 + z010 + z110), z010 >= 0
   P(z, z') -{ 1 }-> 1 + P[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + R(z', 1 + 2 + (z'' - 3)) :|: z'' - 3 >= 0, z' >= 0, z = 0
   P[ITE](z, z', z'') -{ 0 }-> 1 + P(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, z, z') :|: z' >= 0, z >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 0, z') :|: z' >= 0, z = 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 3 + (1 + z04 + z14), z') :|: z04 >= 0, z = 1 + 3 + (1 + z04 + z14), z' >= 0, z14 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 2 + (1 + z03 + z13), z') :|: z' >= 0, z = 1 + 2 + (1 + z03 + z13), z03 >= 0, z13 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 1 + (1 + z05 + z15), z') :|: z = 1 + 1 + (1 + z05 + z15), z15 >= 0, z' >= 0, z05 >= 0
   Q(z, z') -{ 1 }-> 1 + Q[ITE](0, 1 + 0 + (1 + z06 + z16), z') :|: z' >= 0, z06 >= 0, z16 >= 0, z = 1 + 0 + (1 + z06 + z16)
   Q(z, z') -{ 1 }-> 1 + Q[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', 1 + 2 + (z'' - 6)) :|: z'' - 6 >= 0, z' >= 0, z = 0
   Q[ITE](z, z', z'') -{ 0 }-> 1 + P(z', 1 + 2 + (1 + 2 + (z'' - 6))) :|: z'' - 6 >= 0, z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, z, z') :|: z' >= 0, z >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 0, z') :|: z' >= 0, z = 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + 0, z') :|: z' >= 0, z = 1 + 3 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 3 + (1 + z0'' + z1''), z') :|: z' >= 0, z0'' >= 0, z = 1 + 3 + (1 + z0'' + z1''), z1'' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + 0, z') :|: z' >= 0, z = 1 + 2 + 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 2 + (1 + z0' + z1'), z') :|: z' >= 0, z0' >= 0, z1' >= 0, z = 1 + 2 + (1 + z0' + z1')
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + 0, z') :|: z = 1 + 1 + 0, z' >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 1 + (1 + z01 + z11), z') :|: z11 >= 0, z' >= 0, z01 >= 0, z = 1 + 1 + (1 + z01 + z11)
   R(z, z') -{ 1 }-> 1 + R[ITE](0, 1 + 0 + (1 + z02 + z12), z') :|: z' >= 0, z = 1 + 0 + (1 + z02 + z12), z02 >= 0, z12 >= 0
   R(z, z') -{ 1 }-> 1 + R[ITE](1 + 0 + 0 + z', 1 + 0 + 0, z') :|: z = 1 + 0 + 0, z' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 0 :|: z >= 0, z' >= 0, z'' >= 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + R(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   R[ITE](z, z', z'') -{ 0 }-> 1 + Q(z', z'' - 3) :|: z'' - 3 >= 0, z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 2 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 1 + 3 + 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 1 + 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z0 >= 0, z = 1 + 2 + (1 + z0 + z1), z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 3 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z1 >= 0, z = 1 + 1 + (1 + z0 + z1), z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z = 1 + 0 + (1 + z0 + z1), z1 >= 0, z0 >= 0, z' >= 0
   e(z, z') -{ 0 }-> 0 :|: z' >= 0, z = 0
   e(z, z') -{ 0 }-> 0 :|: z >= 0, z' >= 0
   e(z, z') -{ 0 }-> 1 + 0 + 0 + z' :|: z = 1 + 0 + 0, z' >= 0

Function symbols to be analyzed: 
Previous analysis results are:
  e: runtime: O(1) [0], size: O(n^1) [1 + z']
  Q: runtime: O(n^1) [150 + 60*z'], size: O(n^1) [5 + 2*z']
  Q[ITE]: runtime: O(n^1) [32 + 60*z''], size: O(n^1) [4 + 2*z'']
  R[ITE]: runtime: O(n^1) [80*z''], size: O(n^1) [2*z'']
  P[ITE]: runtime: O(n^1) [4 + 80*z''], size: O(n^1) [2 + 2*z'']
  P: runtime: O(n^1) [5 + 80*z'], size: O(n^1) [3 + 2*z']
  R: runtime: O(n^1) [1 + 80*z'], size: O(n^1) [1 + 2*z']

----------------------------------------

(41) FinalProof (FINISHED)
Computed overall runtime complexity
----------------------------------------

(42)
BOUNDS(1, n^1)