WORST_CASE(Omega(n^1),O(n^1))
proof of /export/starexec/sandbox/benchmark/theBenchmark.trs
# AProVE Commit ID: c69e44bd14796315568835c1ffa2502984884775 mhark 20210624 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 2963 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [UPPER BOUND(ID), 36 ms]
(4) CdtProblem
    (5) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (6) CdtProblem
    (7) CdtRhsSimplificationProcessorProof [BOTH BOUNDS(ID, ID), 0 ms]
    (8) CdtProblem
    (9) CdtGraphSplitRhsProof [BOTH BOUNDS(ID, ID), 0 ms]
    (10) CdtProblem
    (11) CdtLeafRemovalProof [ComplexityIfPolyImplication, 0 ms]
    (12) CdtProblem
    (13) CdtUsableRulesProof [BOTH BOUNDS(ID, ID), 0 ms]
    (14) CdtProblem
    (15) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 141 ms]
    (16) CdtProblem
    (17) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 42 ms]
    (18) CdtProblem
    (19) CdtRuleRemovalProof [UPPER BOUND(ADD(n^1)), 41 ms]
    (20) CdtProblem
    (21) SIsEmptyProof [BOTH BOUNDS(ID, ID), 0 ms]
    (22) BOUNDS(1, 1)
(23) RelTrsToDecreasingLoopProblemProof [LOWER BOUND(ID), 0 ms]
(24) TRS for Loop Detection
    (25) DecreasingLoopProof [LOWER BOUND(ID), 1274 ms]
    (26) BEST
        (27) proven lower bound
            (28) LowerBoundPropagationProof [FINISHED, 0 ms]
            (29) BOUNDS(n^1, INF)
        (30) TRS for Loop Detection


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

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


The TRS R consists of the following rules:

   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))

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

   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
   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)

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

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

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


The TRS R consists of the following rules:

   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))

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

   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
   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)

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

(3) CpxTrsToCdtProof (UPPER BOUND(ID))
Converted Cpx (relative) TRS to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   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
   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)
   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))
Tuples:
   AND'(False, False) -> c76
   AND'(True, False) -> c77
   AND'(False, True) -> c78
   AND'(True, True) -> c79
   Q[ITE]'(False, z0, Cons(F, Cons(F, z1))) -> c80(AND'(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), 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))) -> c81(AND'(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), 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))) -> c82
   Q[ITE]'(False, z0, Cons(F, Cons(B, z1))) -> c83
   Q[ITE]'(False, z0, Cons(F, Cons(A, z1))) -> c84
   Q[ITE]'(False, z0, Cons(T, Cons(F, z1))) -> c85
   Q[ITE]'(False, z0, Cons(T, Cons(T, z1))) -> c86
   Q[ITE]'(False, z0, Cons(T, Cons(B, z1))) -> c87
   Q[ITE]'(False, z0, Cons(T, Cons(A, z1))) -> c88
   Q[ITE]'(False, z0, Cons(B, Cons(F, z1))) -> c89
   Q[ITE]'(False, z0, Cons(B, Cons(T, z1))) -> c90
   Q[ITE]'(False, z0, Cons(B, Cons(B, z1))) -> c91
   Q[ITE]'(False, z0, Cons(B, Cons(A, z1))) -> c92
   Q[ITE]'(False, z0, Cons(A, Cons(F, z1))) -> c93
   Q[ITE]'(False, z0, Cons(A, Cons(T, z1))) -> c94
   Q[ITE]'(False, z0, Cons(A, Cons(B, z1))) -> c95
   Q[ITE]'(False, z0, Cons(A, Cons(A, z1))) -> c96
   Q[ITE]'(False, z0, Cons(F, Nil)) -> c97(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, 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, and(False, equal(head(Nil), F))), AND''(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), AND'(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), EQUAL''(head(Nil), F), HEAD'(Nil), HEAD''(Nil))
   Q[ITE]'(False, z0, Cons(T, Nil)) -> c98(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), 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), AND'(False, and(False, equal(head(Nil), F))), AND''(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), AND'(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), EQUAL''(head(Nil), F), HEAD'(Nil), HEAD''(Nil))
   Q[ITE]'(False, z0, Cons(B, Nil)) -> c99(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), 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), AND'(False, and(False, equal(head(Nil), F))), AND''(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), AND'(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), EQUAL''(head(Nil), F), HEAD'(Nil), HEAD''(Nil))
   Q[ITE]'(False, z0, Cons(A, Nil)) -> c100(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), 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), AND'(False, and(False, equal(head(Nil), F))), AND''(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), AND'(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), EQUAL''(head(Nil), F), HEAD'(Nil), HEAD''(Nil))
   Q[ITE]'(True, z0, z1) -> c101
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(AND'(q(z0, z1), r(z0, z1)), Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(AND'(q(z0, z1), r(z0, z1)), Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   R[ITE]'(False, z0, Cons(T, z1)) -> c104
   R[ITE]'(False, z0, Cons(B, z1)) -> c105
   R[ITE]'(False, z0, Cons(A, z1)) -> c106
   R[ITE]'(True, z0, z1) -> c107
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(AND'(r(z0, Cons(F, z1)), p(z0, z1)), R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(AND'(r(z0, Cons(F, z1)), p(z0, z1)), R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   P[ITE]'(False, z0, Cons(T, z1)) -> c110
   P[ITE]'(False, z0, Cons(B, z1)) -> c111
   P[ITE]'(False, z0, Cons(A, z1)) -> c112
   P[ITE]'(True, z0, z1) -> c113
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c114(AND'(p(z0, Cons(z1, z2)), q(z0, z2)), P'(z0, Cons(z1, z2)), Q'(z0, z2), P''(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c115(AND'(p(z0, Cons(z1, z2)), q(z0, z2)), P'(z0, Cons(z1, z2)), Q'(z0, z2), Q''(z0, z2))
   Q[ITE][FALSE][ITE]'(False, z0, z1) -> c116
   T[ITE]'(False, z0, z1) -> c117
   T[ITE]'(True, z0, z1) -> c118
   AND''(False, False) -> c119
   AND''(True, False) -> c120
   AND''(False, True) -> c121
   AND''(True, True) -> c122
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(AND''(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   Q[ITE]''(False, z0, Cons(F, Cons(T, z1))) -> c124
   Q[ITE]''(False, z0, Cons(F, Cons(B, z1))) -> c125
   Q[ITE]''(False, z0, Cons(F, Cons(A, z1))) -> c126
   Q[ITE]''(False, z0, Cons(T, Cons(F, z1))) -> c127
   Q[ITE]''(False, z0, Cons(T, Cons(T, z1))) -> c128
   Q[ITE]''(False, z0, Cons(T, Cons(B, z1))) -> c129
   Q[ITE]''(False, z0, Cons(T, Cons(A, z1))) -> c130
   Q[ITE]''(False, z0, Cons(B, Cons(F, z1))) -> c131
   Q[ITE]''(False, z0, Cons(B, Cons(T, z1))) -> c132
   Q[ITE]''(False, z0, Cons(B, Cons(B, z1))) -> c133
   Q[ITE]''(False, z0, Cons(B, Cons(A, z1))) -> c134
   Q[ITE]''(False, z0, Cons(A, Cons(F, z1))) -> c135
   Q[ITE]''(False, z0, Cons(A, Cons(T, z1))) -> c136
   Q[ITE]''(False, z0, Cons(A, Cons(B, z1))) -> c137
   Q[ITE]''(False, z0, Cons(A, Cons(A, z1))) -> c138
   Q[ITE]''(False, z0, Cons(F, Nil)) -> c139(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)) -> c140(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)) -> c141(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)) -> c142(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) -> c143
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(AND''(q(z0, z1), r(z0, z1)), Q'(z0, z1), R'(z0, z1))
   R[ITE]''(False, z0, Cons(T, z1)) -> c145
   R[ITE]''(False, z0, Cons(B, z1)) -> c146
   R[ITE]''(False, z0, Cons(A, z1)) -> c147
   R[ITE]''(True, z0, z1) -> c148
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(AND''(r(z0, Cons(F, z1)), p(z0, z1)), R'(z0, Cons(F, z1)), P'(z0, z1))
   P[ITE]''(False, z0, Cons(T, z1)) -> c150
   P[ITE]''(False, z0, Cons(B, z1)) -> c151
   P[ITE]''(False, z0, Cons(A, z1)) -> c152
   P[ITE]''(True, z0, z1) -> c153
   Q[ITE][FALSE][ITE]''(True, z0, Cons(z1, z2)) -> c154(AND''(p(z0, Cons(z1, z2)), q(z0, z2)), P'(z0, Cons(z1, z2)), Q'(z0, z2))
   Q[ITE][FALSE][ITE]''(False, z0, z1) -> c155
   T[ITE]''(False, z0, z1) -> c156
   T[ITE]''(True, z0, z1) -> c157
   HEAD'(Cons(z0, z1)) -> c158
   E'(Cons(F, Nil), z0) -> c159
   E'(Cons(T, Nil), z0) -> c160
   E'(Cons(B, Nil), z0) -> c161
   E'(Cons(A, Nil), z0) -> c162
   E'(Cons(F, Cons(z0, z1)), z2) -> c163
   E'(Cons(T, Cons(z0, z1)), z2) -> c164
   E'(Cons(B, Cons(z0, z1)), z2) -> c165
   E'(Cons(A, Cons(z0, z1)), z2) -> c166
   E'(Nil, z0) -> c167
   EQUAL'(F, F) -> c168
   EQUAL'(F, T) -> c169
   EQUAL'(F, B) -> c170
   EQUAL'(F, A) -> c171
   EQUAL'(T, F) -> c172
   EQUAL'(T, T) -> c173
   EQUAL'(T, B) -> c174
   EQUAL'(T, A) -> c175
   EQUAL'(B, F) -> c176
   EQUAL'(B, T) -> c177
   EQUAL'(B, B) -> c178
   EQUAL'(B, A) -> c179
   EQUAL'(A, F) -> c180
   EQUAL'(A, T) -> c181
   EQUAL'(A, B) -> c182
   EQUAL'(A, A) -> c183
   NOTEMPTY'(Cons(z0, z1)) -> c184
   NOTEMPTY'(Nil) -> c185
   T''(z0, z1) -> c186(T[ITE]''(e(z0, z1), z0, z1), E'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1), E'(z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1), E'(z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1), E'(z0, z1))
   GOAL'(z0, z1) -> c190(Q'(z0, z1))
   HEAD''(Cons(z0, z1)) -> c191
   E''(Cons(F, Nil), z0) -> c192
   E''(Cons(T, Nil), z0) -> c193
   E''(Cons(B, Nil), z0) -> c194
   E''(Cons(A, Nil), z0) -> c195
   E''(Cons(F, Cons(z0, z1)), z2) -> c196
   E''(Cons(T, Cons(z0, z1)), z2) -> c197
   E''(Cons(B, Cons(z0, z1)), z2) -> c198
   E''(Cons(A, Cons(z0, z1)), z2) -> c199
   E''(Nil, z0) -> c200
   EQUAL''(F, F) -> c201
   EQUAL''(F, T) -> c202
   EQUAL''(F, B) -> c203
   EQUAL''(F, A) -> c204
   EQUAL''(T, F) -> c205
   EQUAL''(T, T) -> c206
   EQUAL''(T, B) -> c207
   EQUAL''(T, A) -> c208
   EQUAL''(B, F) -> c209
   EQUAL''(B, T) -> c210
   EQUAL''(B, B) -> c211
   EQUAL''(B, A) -> c212
   EQUAL''(A, F) -> c213
   EQUAL''(A, T) -> c214
   EQUAL''(A, B) -> c215
   EQUAL''(A, A) -> c216
   NOTEMPTY''(Cons(z0, z1)) -> c217
   NOTEMPTY''(Nil) -> c218
   T'''(z0, z1) -> c219(T[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   GOAL''(z0, z1) -> c223(Q''(z0, z1))
S tuples:
   HEAD''(Cons(z0, z1)) -> c191
   E''(Cons(F, Nil), z0) -> c192
   E''(Cons(T, Nil), z0) -> c193
   E''(Cons(B, Nil), z0) -> c194
   E''(Cons(A, Nil), z0) -> c195
   E''(Cons(F, Cons(z0, z1)), z2) -> c196
   E''(Cons(T, Cons(z0, z1)), z2) -> c197
   E''(Cons(B, Cons(z0, z1)), z2) -> c198
   E''(Cons(A, Cons(z0, z1)), z2) -> c199
   E''(Nil, z0) -> c200
   EQUAL''(F, F) -> c201
   EQUAL''(F, T) -> c202
   EQUAL''(F, B) -> c203
   EQUAL''(F, A) -> c204
   EQUAL''(T, F) -> c205
   EQUAL''(T, T) -> c206
   EQUAL''(T, B) -> c207
   EQUAL''(T, A) -> c208
   EQUAL''(B, F) -> c209
   EQUAL''(B, T) -> c210
   EQUAL''(B, B) -> c211
   EQUAL''(B, A) -> c212
   EQUAL''(A, F) -> c213
   EQUAL''(A, T) -> c214
   EQUAL''(A, B) -> c215
   EQUAL''(A, A) -> c216
   NOTEMPTY''(Cons(z0, z1)) -> c217
   NOTEMPTY''(Nil) -> c218
   T'''(z0, z1) -> c219(T[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   GOAL''(z0, z1) -> c223(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, 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

Defined Pair Symbols:   AND'_2, Q[ITE]'_3, R[ITE]'_3, P[ITE]'_3, Q[ITE][FALSE][ITE]'_3, T[ITE]'_3, 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, HEAD''_1, E''_2, EQUAL''_2, NOTEMPTY''_1, T'''_2, R''_2, Q''_2, P''_2, GOAL''_2

Compound Symbols:   c76, c77, c78, c79, c80_4, c81_4, c82, c83, c84, c85, c86, c87, c88, c89, c90, c91, c92, c93, c94, c95, c96, c97_21, c98_21, c99_21, c100_21, c101, c102_4, c103_4, c104, c105, c106, c107, c108_4, c109_4, c110, c111, c112, c113, c114_4, c115_4, c116, c117, c118, c119, c120, c121, c122, c123_3, c124, c125, c126, c127, c128, c129, c130, c131, c132, c133, c134, c135, c136, c137, c138, c139_6, c140_6, c141_6, c142_6, c143, c144_3, c145, c146, c147, c148, c149_3, c150, c151, c152, c153, c154_3, c155, c156, c157, c158, c159, c160, c161, c162, c163, c164, c165, c166, c167, c168, c169, c170, c171, c172, c173, c174, c175, c176, c177, c178, c179, c180, c181, c182, c183, c184, c185, c186_2, c187_2, c188_2, c189_2, c190_1, c191, c192, c193, c194, c195, c196, c197, c198, c199, c200, c201, c202, c203, c204, c205, c206, c207, c208, c209, c210, c211, c212, c213, c214, c215, c216, c217, c218, c219_3, c220_3, c221_3, c222_3, c223_1


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

(5) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 2 leading nodes:
   GOAL''(z0, z1) -> c223(Q''(z0, z1))
   GOAL'(z0, z1) -> c190(Q'(z0, z1))
Removed 128 trailing nodes:
   Q[ITE]'(False, z0, Cons(B, Cons(T, z1))) -> c90
   E'(Cons(F, Nil), z0) -> c159
   Q[ITE]''(False, z0, Cons(T, Nil)) -> c140(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(F, Cons(T, z1))) -> c82
   AND'(True, True) -> c79
   Q[ITE]''(False, z0, Cons(B, Cons(F, z1))) -> c131
   EQUAL'(B, F) -> c176
   EQUAL'(T, B) -> c174
   Q[ITE]''(False, z0, Cons(B, Cons(A, z1))) -> c134
   NOTEMPTY'(Cons(z0, z1)) -> c184
   Q[ITE]'(False, z0, Cons(A, Cons(F, z1))) -> c93
   EQUAL'(A, F) -> c180
   Q[ITE]''(False, z0, Cons(F, Cons(T, z1))) -> c124
   R[ITE]'(False, z0, Cons(A, z1)) -> c106
   E'(Cons(T, Nil), z0) -> c160
   Q[ITE]''(False, z0, Cons(A, Nil)) -> c142(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))
   T'''(z0, z1) -> c219(T[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   E''(Cons(B, Cons(z0, z1)), z2) -> c198
   Q[ITE]'(False, z0, Cons(B, Nil)) -> c99(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), 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), AND'(False, and(False, equal(head(Nil), F))), AND''(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), AND'(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), EQUAL''(head(Nil), F), HEAD'(Nil), HEAD''(Nil))
   EQUAL'(T, A) -> c175
   EQUAL''(F, T) -> c202
   Q[ITE]''(False, z0, Cons(B, Cons(B, z1))) -> c133
   AND'(False, False) -> c76
   EQUAL'(A, B) -> c182
   AND''(False, False) -> c119
   Q[ITE]'(True, z0, z1) -> c101
   T[ITE]''(False, z0, z1) -> c156
   Q[ITE]'(False, z0, Cons(T, Cons(F, z1))) -> c85
   Q[ITE]''(False, z0, Cons(B, Cons(T, z1))) -> c132
   Q[ITE]''(False, z0, Cons(T, Cons(F, z1))) -> c127
   P[ITE]'(False, z0, Cons(A, z1)) -> c112
   R[ITE]''(False, z0, Cons(T, z1)) -> c145
   Q[ITE]'(False, z0, Cons(B, Cons(B, z1))) -> c91
   E'(Nil, z0) -> c167
   Q[ITE]'(False, z0, Cons(F, Nil)) -> c97(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, 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, and(False, equal(head(Nil), F))), AND''(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), AND'(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), EQUAL''(head(Nil), F), HEAD'(Nil), HEAD''(Nil))
   E'(Cons(A, Nil), z0) -> c162
   AND''(True, True) -> c122
   P[ITE]'(False, z0, Cons(B, z1)) -> c111
   EQUAL''(F, A) -> c204
   EQUAL'(T, T) -> c173
   Q[ITE]''(False, z0, Cons(T, Cons(B, z1))) -> c129
   Q[ITE]'(False, z0, Cons(F, Cons(A, z1))) -> c84
   AND'(False, True) -> c78
   Q[ITE]''(False, z0, Cons(A, Cons(F, z1))) -> c135
   Q[ITE]'(False, z0, Cons(A, Nil)) -> c100(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), 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), AND'(False, and(False, equal(head(Nil), F))), AND''(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), AND'(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), EQUAL''(head(Nil), F), HEAD'(Nil), HEAD''(Nil))
   EQUAL''(F, F) -> c201
   R[ITE]''(False, z0, Cons(B, z1)) -> c146
   AND'(True, False) -> c77
   E'(Cons(A, Cons(z0, z1)), z2) -> c166
   E'(Cons(B, Cons(z0, z1)), z2) -> c165
   P[ITE]''(False, z0, Cons(A, z1)) -> c152
   R[ITE]''(False, z0, Cons(A, z1)) -> c147
   T[ITE]'(True, z0, z1) -> c118
   NOTEMPTY''(Cons(z0, z1)) -> c217
   E''(Cons(F, Nil), z0) -> c192
   Q[ITE]'(False, z0, Cons(T, Cons(A, z1))) -> c88
   EQUAL''(T, B) -> c207
   EQUAL'(F, T) -> c169
   EQUAL''(A, B) -> c215
   HEAD'(Cons(z0, z1)) -> c158
   AND''(False, True) -> c121
   Q[ITE]'(False, z0, Cons(A, Cons(A, z1))) -> c96
   E''(Cons(T, Nil), z0) -> c193
   Q[ITE]''(False, z0, Cons(F, Cons(B, z1))) -> c125
   E''(Cons(B, Nil), z0) -> c194
   Q[ITE]'(False, z0, Cons(T, Cons(T, z1))) -> c86
   EQUAL''(B, B) -> c211
   Q[ITE]''(False, z0, Cons(F, Cons(A, z1))) -> c126
   EQUAL'(A, A) -> c183
   EQUAL'(F, A) -> c171
   Q[ITE][FALSE][ITE]'(False, z0, z1) -> c116
   Q[ITE]''(False, z0, Cons(F, Nil)) -> c139(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))
   EQUAL''(T, A) -> c208
   T[ITE]'(False, z0, z1) -> c117
   R[ITE]'(False, z0, Cons(B, z1)) -> c105
   Q[ITE]'(False, z0, Cons(A, Cons(B, z1))) -> c95
   P[ITE]'(False, z0, Cons(T, z1)) -> c110
   EQUAL''(B, T) -> c210
   E''(Cons(A, Nil), z0) -> c195
   E''(Cons(T, Cons(z0, z1)), z2) -> c197
   E'(Cons(B, Nil), z0) -> c161
   EQUAL''(A, A) -> c216
   T[ITE]''(True, z0, z1) -> c157
   Q[ITE][FALSE][ITE]''(False, z0, z1) -> c155
   EQUAL'(F, B) -> c170
   E'(Cons(F, Cons(z0, z1)), z2) -> c163
   EQUAL''(F, B) -> c203
   EQUAL'(B, A) -> c179
   E'(Cons(T, Cons(z0, z1)), z2) -> c164
   EQUAL''(A, F) -> c213
   E''(Cons(A, Cons(z0, z1)), z2) -> c199
   Q[ITE]''(True, z0, z1) -> c143
   HEAD''(Cons(z0, z1)) -> c191
   NOTEMPTY'(Nil) -> c185
   Q[ITE]'(False, z0, Cons(T, Nil)) -> c98(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), 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), AND'(False, and(False, equal(head(Nil), F))), AND''(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), AND'(False, equal(head(Nil), F)), EQUAL'(head(Nil), F), HEAD'(Nil), EQUAL''(head(Nil), F), HEAD'(Nil), HEAD''(Nil))
   EQUAL''(B, A) -> c212
   Q[ITE]''(False, z0, Cons(A, Cons(B, z1))) -> c137
   Q[ITE]'(False, z0, Cons(F, Cons(B, z1))) -> c83
   Q[ITE]'(False, z0, Cons(B, Cons(A, z1))) -> c92
   EQUAL'(A, T) -> c181
   EQUAL'(B, T) -> c177
   P[ITE]''(False, z0, Cons(T, z1)) -> c150
   Q[ITE]'(False, z0, Cons(B, Cons(F, z1))) -> c89
   EQUAL''(B, F) -> c209
   EQUAL''(T, T) -> c206
   Q[ITE]''(False, z0, Cons(B, Nil)) -> c141(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))
   R[ITE]'(False, z0, Cons(T, z1)) -> c104
   EQUAL'(B, B) -> c178
   T''(z0, z1) -> c186(T[ITE]''(e(z0, z1), z0, z1), E'(z0, z1))
   EQUAL''(A, T) -> c214
   Q[ITE]'(False, z0, Cons(T, Cons(B, z1))) -> c87
   Q[ITE]''(False, z0, Cons(A, Cons(A, z1))) -> c138
   EQUAL''(T, F) -> c205
   Q[ITE]''(False, z0, Cons(T, Cons(A, z1))) -> c130
   Q[ITE]''(False, z0, Cons(T, Cons(T, z1))) -> c128
   AND''(True, False) -> c120
   E''(Nil, z0) -> c200
   EQUAL'(T, F) -> c172
   P[ITE]''(False, z0, Cons(B, z1)) -> c151
   R[ITE]''(True, z0, z1) -> c148
   Q[ITE]''(False, z0, Cons(A, Cons(T, z1))) -> c136
   P[ITE]'(True, z0, z1) -> c113
   E''(Cons(F, Cons(z0, z1)), z2) -> c196
   Q[ITE]'(False, z0, Cons(A, Cons(T, z1))) -> c94
   R[ITE]'(True, z0, z1) -> c107
   NOTEMPTY''(Nil) -> c218
   EQUAL'(F, F) -> c168
   P[ITE]''(True, z0, z1) -> c153

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

(6)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   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
   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)
   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))
Tuples:
   Q[ITE]'(False, z0, Cons(F, Cons(F, z1))) -> c80(AND'(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), 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))) -> c81(AND'(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(AND'(q(z0, z1), r(z0, z1)), Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(AND'(q(z0, z1), r(z0, z1)), Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(AND'(r(z0, Cons(F, z1)), p(z0, z1)), R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(AND'(r(z0, Cons(F, z1)), p(z0, z1)), R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c114(AND'(p(z0, Cons(z1, z2)), q(z0, z2)), P'(z0, Cons(z1, z2)), Q'(z0, z2), P''(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c115(AND'(p(z0, Cons(z1, z2)), q(z0, z2)), P'(z0, Cons(z1, z2)), Q'(z0, z2), Q''(z0, z2))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(AND''(p(z0, Cons(F, Cons(F, z1))), q(z0, Cons(F, z1))), P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(AND''(q(z0, z1), r(z0, z1)), Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(AND''(r(z0, Cons(F, z1)), p(z0, z1)), R'(z0, Cons(F, z1)), P'(z0, z1))
   Q[ITE][FALSE][ITE]''(True, z0, Cons(z1, z2)) -> c154(AND''(p(z0, Cons(z1, z2)), q(z0, z2)), P'(z0, Cons(z1, z2)), Q'(z0, z2))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1), E'(z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1), E'(z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1), E'(z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
S tuples:
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1), E'(z0, z1), E''(z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1), E'(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, 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

Defined Pair Symbols:   Q[ITE]'_3, R[ITE]'_3, P[ITE]'_3, Q[ITE][FALSE][ITE]'_3, Q[ITE]''_3, R[ITE]''_3, P[ITE]''_3, Q[ITE][FALSE][ITE]''_3, R'_2, Q'_2, P'_2, R''_2, Q''_2, P''_2

Compound Symbols:   c80_4, c81_4, c102_4, c103_4, c108_4, c109_4, c114_4, c115_4, c123_3, c144_3, c149_3, c154_3, c187_2, c188_2, c189_2, c220_3, c221_3, c222_3


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

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

(8)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   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
   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)
   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))
Tuples:
   Q[ITE]'(False, z0, Cons(F, Cons(F, z1))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c114(P'(z0, Cons(z1, z2)), Q'(z0, z2), P''(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c115(P'(z0, Cons(z1, z2)), Q'(z0, z2), Q''(z0, z2))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   Q[ITE][FALSE][ITE]''(True, z0, Cons(z1, z2)) -> c154(P'(z0, Cons(z1, z2)), Q'(z0, z2))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
S tuples:
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(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, 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

Defined Pair Symbols:   Q[ITE]'_3, R[ITE]'_3, P[ITE]'_3, Q[ITE][FALSE][ITE]'_3, Q[ITE]''_3, R[ITE]''_3, P[ITE]''_3, Q[ITE][FALSE][ITE]''_3, R'_2, Q'_2, P'_2, R''_2, Q''_2, P''_2

Compound Symbols:   c80_3, c81_3, c102_3, c103_3, c108_3, c109_3, c114_3, c115_3, c123_2, c144_2, c149_2, c154_2, c187_1, c188_1, c189_1, c220_1, c221_1, c222_1


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

(9) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID))
Split RHS of tuples not part of any SCC
----------------------------------------

(10)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   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
   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)
   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))
Tuples:
   Q[ITE]'(False, z0, Cons(F, Cons(F, z1))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c76(P'(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c76(Q'(z0, z2))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c76(P''(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c76(Q''(z0, z2))
   Q[ITE][FALSE][ITE]''(True, z0, Cons(z1, z2)) -> c76(P'(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]''(True, z0, Cons(z1, z2)) -> c76(Q'(z0, z2))
S tuples:
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(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, 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

Defined Pair Symbols:   Q[ITE]'_3, R[ITE]'_3, P[ITE]'_3, Q[ITE]''_3, R[ITE]''_3, P[ITE]''_3, R'_2, Q'_2, P'_2, R''_2, Q''_2, P''_2, Q[ITE][FALSE][ITE]'_3, Q[ITE][FALSE][ITE]''_3

Compound Symbols:   c80_3, c81_3, c102_3, c103_3, c108_3, c109_3, c123_2, c144_2, c149_2, c187_1, c188_1, c189_1, c220_1, c221_1, c222_1, c76_1


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

(11) CdtLeafRemovalProof (ComplexityIfPolyImplication)
Removed 6 leading nodes:
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c76(P''(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c76(Q''(z0, z2))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c76(P'(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]''(True, z0, Cons(z1, z2)) -> c76(P'(z0, Cons(z1, z2)))
   Q[ITE][FALSE][ITE]'(True, z0, Cons(z1, z2)) -> c76(Q'(z0, z2))
   Q[ITE][FALSE][ITE]''(True, z0, Cons(z1, z2)) -> c76(Q'(z0, z2))

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

(12)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   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
   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)
   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))
Tuples:
   Q[ITE]'(False, z0, Cons(F, Cons(F, z1))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
S tuples:
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(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, 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

Defined Pair Symbols:   Q[ITE]'_3, R[ITE]'_3, P[ITE]'_3, Q[ITE]''_3, R[ITE]''_3, P[ITE]''_3, R'_2, Q'_2, P'_2, R''_2, Q''_2, P''_2

Compound Symbols:   c80_3, c81_3, c102_3, c103_3, c108_3, c109_3, c123_2, c144_2, c149_2, c187_1, c188_1, c189_1, c220_1, c221_1, c222_1


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

(13) CdtUsableRulesProof (BOTH BOUNDS(ID, ID))
The following rules are not usable and were removed:
   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
   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)
   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))

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

(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))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
S tuples:
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(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, Q[ITE]''_3, R[ITE]''_3, P[ITE]''_3, R'_2, Q'_2, P'_2, R''_2, Q''_2, P''_2

Compound Symbols:   c80_3, c81_3, c102_3, c103_3, c108_3, c109_3, c123_2, c144_2, c149_2, c187_1, c188_1, c189_1, c220_1, c221_1, c222_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.
   Q''(z0, z1) -> c221(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))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(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)) = x_1 + x_2
   POL(F) = [1]
   POL(False) = 0
   POL(Nil) = 0
   POL(P'(x_1, x_2)) = 0
   POL(P''(x_1, x_2)) = x_2
   POL(P[ITE]'(x_1, x_2, x_3)) = x_3
   POL(P[ITE]''(x_1, x_2, x_3)) = 0
   POL(Q'(x_1, x_2)) = 0
   POL(Q''(x_1, x_2)) = [1] + x_2
   POL(Q[ITE]'(x_1, x_2, x_3)) = x_3
   POL(Q[ITE]''(x_1, x_2, x_3)) = 0
   POL(R'(x_1, x_2)) = 0
   POL(R''(x_1, x_2)) = x_2
   POL(R[ITE]'(x_1, x_2, x_3)) = x_3
   POL(R[ITE]''(x_1, x_2, x_3)) = 0
   POL(T) = [3]
   POL(c102(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c103(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c108(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c109(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c123(x_1, x_2)) = x_1 + x_2
   POL(c144(x_1, x_2)) = x_1 + x_2
   POL(c149(x_1, x_2)) = x_1 + x_2
   POL(c187(x_1)) = x_1
   POL(c188(x_1)) = x_1
   POL(c189(x_1)) = x_1
   POL(c220(x_1)) = x_1
   POL(c221(x_1)) = x_1
   POL(c222(x_1)) = x_1
   POL(c80(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c81(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   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))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
S tuples:
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
K tuples:
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
Defined Rule Symbols:   e_2

Defined Pair Symbols:   Q[ITE]'_3, R[ITE]'_3, P[ITE]'_3, Q[ITE]''_3, R[ITE]''_3, P[ITE]''_3, R'_2, Q'_2, P'_2, R''_2, Q''_2, P''_2

Compound Symbols:   c80_3, c81_3, c102_3, c103_3, c108_3, c109_3, c123_2, c144_2, c149_2, c187_1, c188_1, c189_1, c220_1, c221_1, c222_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.
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
We considered the (Usable) Rules:
   e(Cons(F, Cons(z0, z1)), z2) -> False
   e(Cons(B, Cons(z0, z1)), z2) -> False
   e(Cons(B, Nil), z0) -> False
   e(Cons(A, Nil), z0) -> e[Match][Cons][Ite][True][Match](A, Nil, z0)
   e(Cons(T, Nil), z0) -> False
   e(Cons(F, Nil), z0) -> False
   e(Nil, z0) -> False
   e(Cons(T, Cons(z0, z1)), z2) -> False
   e(Cons(A, Cons(z0, z1)), z2) -> False
And the Tuples:
   Q[ITE]'(False, z0, Cons(F, Cons(F, z1))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(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)) = 0
   POL(P''(x_1, x_2)) = [1] + x_1 + x_2
   POL(P[ITE]'(x_1, x_2, x_3)) = x_2 + x_3
   POL(P[ITE]''(x_1, x_2, x_3)) = 0
   POL(Q'(x_1, x_2)) = 0
   POL(Q''(x_1, x_2)) = [1] + x_1 + x_2
   POL(Q[ITE]'(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(Q[ITE]''(x_1, x_2, x_3)) = 0
   POL(R'(x_1, x_2)) = 0
   POL(R''(x_1, x_2)) = x_1 + x_2
   POL(R[ITE]'(x_1, x_2, x_3)) = x_2 + x_3
   POL(R[ITE]''(x_1, x_2, x_3)) = 0
   POL(T) = [1]
   POL(c102(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c103(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c108(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c109(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c123(x_1, x_2)) = x_1 + x_2
   POL(c144(x_1, x_2)) = x_1 + x_2
   POL(c149(x_1, x_2)) = x_1 + x_2
   POL(c187(x_1)) = x_1
   POL(c188(x_1)) = x_1
   POL(c189(x_1)) = x_1
   POL(c220(x_1)) = x_1
   POL(c221(x_1)) = x_1
   POL(c222(x_1)) = x_1
   POL(c80(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c81(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(e(x_1, x_2)) = [1]
   POL(e[Match][Cons][Ite][True][Match](x_1, x_2, x_3)) = x_2

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

(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))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
S tuples:
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
K tuples:
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
Defined Rule Symbols:   e_2

Defined Pair Symbols:   Q[ITE]'_3, R[ITE]'_3, P[ITE]'_3, Q[ITE]''_3, R[ITE]''_3, P[ITE]''_3, R'_2, Q'_2, P'_2, R''_2, Q''_2, P''_2

Compound Symbols:   c80_3, c81_3, c102_3, c103_3, c108_3, c109_3, c123_2, c144_2, c149_2, c187_1, c188_1, c189_1, c220_1, c221_1, c222_1


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

(19) 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) -> c220(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))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(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)) = 0
   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(P[ITE]''(x_1, x_2, x_3)) = 0
   POL(Q'(x_1, x_2)) = 0
   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(Q[ITE]''(x_1, x_2, x_3)) = 0
   POL(R'(x_1, x_2)) = 0
   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(R[ITE]''(x_1, x_2, x_3)) = 0
   POL(T) = [1]
   POL(c102(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c103(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c108(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c109(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c123(x_1, x_2)) = x_1 + x_2
   POL(c144(x_1, x_2)) = x_1 + x_2
   POL(c149(x_1, x_2)) = x_1 + x_2
   POL(c187(x_1)) = x_1
   POL(c188(x_1)) = x_1
   POL(c189(x_1)) = x_1
   POL(c220(x_1)) = x_1
   POL(c221(x_1)) = x_1
   POL(c222(x_1)) = x_1
   POL(c80(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   POL(c81(x_1, x_2, x_3)) = x_1 + x_2 + x_3
   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_2 + x_3

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

(20)
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))) -> c80(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))) -> c81(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)), Q''(z0, Cons(F, z1)))
   R[ITE]'(False, z0, Cons(F, z1)) -> c102(Q'(z0, z1), R'(z0, z1), Q''(z0, z1))
   R[ITE]'(False, z0, Cons(F, z1)) -> c103(Q'(z0, z1), R'(z0, z1), R''(z0, z1))
   P[ITE]'(False, z0, Cons(F, z1)) -> c108(R'(z0, Cons(F, z1)), P'(z0, z1), R''(z0, Cons(F, z1)))
   P[ITE]'(False, z0, Cons(F, z1)) -> c109(R'(z0, Cons(F, z1)), P'(z0, z1), P''(z0, z1))
   Q[ITE]''(False, z0, Cons(F, Cons(F, z1))) -> c123(P'(z0, Cons(F, Cons(F, z1))), Q'(z0, Cons(F, z1)))
   R[ITE]''(False, z0, Cons(F, z1)) -> c144(Q'(z0, z1), R'(z0, z1))
   P[ITE]''(False, z0, Cons(F, z1)) -> c149(R'(z0, Cons(F, z1)), P'(z0, z1))
   R'(z0, z1) -> c187(R[ITE]''(e(z0, z1), z0, z1))
   Q'(z0, z1) -> c188(Q[ITE]''(e(z0, z1), z0, z1))
   P'(z0, z1) -> c189(P[ITE]''(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
S tuples:none
K tuples:
   Q''(z0, z1) -> c221(Q[ITE]'(e(z0, z1), z0, z1))
   P''(z0, z1) -> c222(P[ITE]'(e(z0, z1), z0, z1))
   R''(z0, z1) -> c220(R[ITE]'(e(z0, z1), z0, z1))
Defined Rule Symbols:   e_2

Defined Pair Symbols:   Q[ITE]'_3, R[ITE]'_3, P[ITE]'_3, Q[ITE]''_3, R[ITE]''_3, P[ITE]''_3, R'_2, Q'_2, P'_2, R''_2, Q''_2, P''_2

Compound Symbols:   c80_3, c81_3, c102_3, c103_3, c108_3, c109_3, c123_2, c144_2, c149_2, c187_1, c188_1, c189_1, c220_1, c221_1, c222_1


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

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

(22)
BOUNDS(1, 1)

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

(23) RelTrsToDecreasingLoopProblemProof (LOWER BOUND(ID))
Transformed a relative TRS into a decreasing-loop problem.
----------------------------------------

(24)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   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))

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

   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
   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)

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

(25) DecreasingLoopProof (LOWER BOUND(ID))
The following loop(s) give(s) rise to the lower bound Omega(n^1):

The rewrite sequence

Q(Cons(T, Nil), Cons(F, Cons(F, z12_0))) ->^+ c73(c5(AND(p(Cons(T, Nil), Cons(F, Cons(F, z12_0))), q(Cons(T, Nil), Cons(F, z12_0))), Q(Cons(T, Nil), Cons(F, z12_0))), E(Cons(T, Nil), Cons(F, Cons(F, z12_0))))

gives rise to a decreasing loop by considering the right hand sides subterm at position [0,1].

The pumping substitution is [z12_0 / Cons(F, z12_0)].

The result substitution is [ ].




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

(26)
Complex Obligation (BEST)

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

(27)
Obligation:
Proved the lower bound n^1 for the following obligation:

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


The TRS R consists of the following rules:

   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))

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

   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
   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)

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

(28) LowerBoundPropagationProof (FINISHED)
Propagated lower bound.
----------------------------------------

(29)
BOUNDS(n^1, INF)

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

(30)
Obligation:
Analyzing the following TRS for decreasing loops:

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


The TRS R consists of the following rules:

   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))

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

   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
   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)

Rewrite Strategy: INNERMOST