WORST_CASE(?,O(n^1))
proof of input_IZiDMPee7I.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 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), 928 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) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 82 ms]
(14) CdtProblem
(15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 54 ms]
(16) CdtProblem
(17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 32 ms]
(18) CdtProblem
(19) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
(20) BOUNDS(1, 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:
   E(Cons(B, Cons(z0, z1)), z2) -> c50
   EQUAL(F, A) -> c56
   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(T, Cons(A, z1))) -> c12
   E(Cons(T, Cons(z0, z1)), z2) -> c49
   P[ITE](False, z0, Cons(B, z1)) -> c35
   AND(False, True) -> c2
   EQUAL(F, B) -> c55
   R[ITE](False, z0, Cons(T, z1)) -> c28
   T'(z0, z1) -> c71(T[ITE](e(z0, z1), z0, z1), E(z0, z1))
   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, Cons(B, z1))) -> c11
   AND(True, False) -> c1
   EQUAL(B, A) -> c64
   AND(True, True) -> c3
   NOTEMPTY(Nil) -> c70
   E(Cons(A, Nil), z0) -> c47
   EQUAL(F, T) -> c54
   E(Cons(F, Cons(z0, z1)), z2) -> c48
   NOTEMPTY(Cons(z0, z1)) -> c69
   EQUAL(A, B) -> c67
   R[ITE](False, z0, Cons(B, z1)) -> c29
   Q[ITE](False, z0, Cons(F, Cons(B, z1))) -> c7
   P[ITE](False, z0, Cons(T, z1)) -> c34
   Q[ITE](False, z0, Cons(A, Cons(B, z1))) -> c19
   EQUAL(T, B) -> c59
   Q[ITE](False, z0, Cons(T, Cons(F, z1))) -> c9
   T[ITE](False, z0, z1) -> c41
   Q[ITE](True, z0, z1) -> c25
   E(Cons(T, Nil), z0) -> c45
   EQUAL(T, A) -> c60
   EQUAL(A, A) -> c68
   E(Cons(B, Nil), z0) -> c46
   P[ITE](False, z0, Cons(A, z1)) -> c36
   E(Cons(F, Nil), z0) -> c44
   R[ITE](False, z0, Cons(A, z1)) -> c30
   Q[ITE](False, z0, Cons(T, Cons(T, z1))) -> c10
   Q[ITE](False, z0, Cons(A, Cons(A, z1))) -> c20
   Q[ITE](False, z0, Cons(A, Cons(T, z1))) -> c18
   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(T, F) -> c57
   Q[ITE](False, z0, Cons(A, Cons(F, z1))) -> c17
   AND(False, False) -> c
   E(Nil, z0) -> c52
   Q[ITE](False, z0, Cons(B, Cons(F, z1))) -> c13
   EQUAL(B, T) -> c62
   R[ITE](True, z0, z1) -> c31
   EQUAL(B, F) -> c61
   EQUAL(F, F) -> c53
   E(Cons(A, Cons(z0, z1)), z2) -> c51
   Q[ITE](False, z0, Cons(B, Cons(B, z1))) -> c15
   Q[ITE](False, z0, Cons(B, Cons(A, z1))) -> c16
   EQUAL(T, T) -> c58
   Q[ITE](False, z0, Cons(F, Cons(A, z1))) -> c8
   EQUAL(A, T) -> c66
   Q[ITE](False, z0, Cons(F, Cons(T, z1))) -> c6
   Q[ITE][FALSE][ITE](False, z0, z1) -> c40
   HEAD(Cons(z0, z1)) -> c43
   EQUAL(A, F) -> c65
   EQUAL(B, B) -> c63
   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))
   T[ITE](True, z0, z1) -> c42
   Q[ITE](False, z0, Cons(B, Cons(T, z1))) -> c14
   P[ITE](True, z0, z1) -> c37

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

(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) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
We considered the (Usable) Rules:none
And the 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))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(A) = [3]
   POL(B) = [3]
   POL(Cons(x_1, x_2)) = [1] + x_2
   POL(F) = 0
   POL(False) = 0
   POL(Nil) = 0
   POL(P(x_1, x_2)) = x_2
   POL(P[ITE](x_1, x_2, x_3)) = x_3
   POL(Q(x_1, x_2)) = [1] + x_2
   POL(Q[ITE](x_1, x_2, x_3)) = x_3
   POL(R(x_1, x_2)) = x_2
   POL(R[ITE](x_1, x_2, x_3)) = x_3
   POL(T) = [3]
   POL(c26(x_1)) = x_1
   POL(c27(x_1)) = x_1
   POL(c32(x_1)) = x_1
   POL(c33(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c5(x_1)) = x_1
   POL(c72(x_1)) = x_1
   POL(c73(x_1)) = x_1
   POL(c74(x_1)) = x_1
   POL(e(x_1, x_2)) = [3]x_1 + [3]x_2
   POL(e[Match][Cons][Ite][True][Match](x_1, x_2, x_3)) = [3] + x_1 + x_2 + x_3

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

(14)
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))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
K tuples:
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
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


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

(15) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
We considered the (Usable) Rules:none
And the 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))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(A) = [3]
   POL(B) = [3]
   POL(Cons(x_1, x_2)) = [2] + x_2
   POL(F) = 0
   POL(False) = 0
   POL(Nil) = 0
   POL(P(x_1, x_2)) = [1] + [2]x_2
   POL(P[ITE](x_1, x_2, x_3)) = [2]x_3
   POL(Q(x_1, x_2)) = [1] + [2]x_2
   POL(Q[ITE](x_1, x_2, x_3)) = [1] + [2]x_3
   POL(R(x_1, x_2)) = [2]x_2
   POL(R[ITE](x_1, x_2, x_3)) = [2]x_3
   POL(T) = [3]
   POL(c26(x_1)) = x_1
   POL(c27(x_1)) = x_1
   POL(c32(x_1)) = x_1
   POL(c33(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c5(x_1)) = x_1
   POL(c72(x_1)) = x_1
   POL(c73(x_1)) = x_1
   POL(c74(x_1)) = x_1
   POL(e(x_1, x_2)) = [3]x_1 + [3]x_2
   POL(e[Match][Cons][Ite][True][Match](x_1, x_2, x_3)) = [3] + x_1 + x_2 + x_3

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

(16)
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))
K tuples:
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
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


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

(17) CdtRuleRemovalProof (UPPER BOUND(ADD(n^1)))
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
We considered the (Usable) Rules:none
And the 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))
The order we found is given by the following interpretation:

Polynomial interpretation :

   POL(A) = [1]
   POL(B) = [1]
   POL(Cons(x_1, x_2)) = x_1 + x_2
   POL(F) = [1]
   POL(False) = [1]
   POL(Nil) = [1]
   POL(P(x_1, x_2)) = [1] + x_1 + x_2
   POL(P[ITE](x_1, x_2, x_3)) = [1] + x_2 + x_3
   POL(Q(x_1, x_2)) = [1] + x_1 + x_2
   POL(Q[ITE](x_1, x_2, x_3)) = [1] + x_2 + x_3
   POL(R(x_1, x_2)) = [1] + x_1 + x_2
   POL(R[ITE](x_1, x_2, x_3)) = x_2 + x_3
   POL(T) = [1]
   POL(c26(x_1)) = x_1
   POL(c27(x_1)) = x_1
   POL(c32(x_1)) = x_1
   POL(c33(x_1)) = x_1
   POL(c4(x_1)) = x_1
   POL(c5(x_1)) = x_1
   POL(c72(x_1)) = x_1
   POL(c73(x_1)) = x_1
   POL(c74(x_1)) = x_1
   POL(e(x_1, x_2)) = [1] + x_1 + x_2
   POL(e[Match][Cons][Ite][True][Match](x_1, x_2, x_3)) = [1] + x_1 + x_3

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

(18)
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:none
K tuples:
   Q(z0, z1) -> c73(Q[ITE](e(z0, z1), z0, z1))
   P(z0, z1) -> c74(P[ITE](e(z0, z1), z0, z1))
   R(z0, z1) -> c72(R[ITE](e(z0, z1), z0, z1))
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


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

(19) SIsEmptyProof (BOTH BOUNDS(ID, ID))
The set S is empty
----------------------------------------

(20)
BOUNDS(1, 1)