WORST_CASE(Omega(n^1),?)
proof of input_pt0anHL6yQ.trs
# AProVE Commit ID: aff8ecad908e01718a4c36e68d2e55d5e0f16e15 fuhs 20220216 unpublished


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

(0) CpxRelTRS
(1) SInnermostTerminationProof [BOTH CONCRETE BOUNDS(ID, ID), 283 ms]
(2) CpxRelTRS
(3) CpxTrsToCdtProof [BOTH BOUNDS(ID, ID), 84 ms]
(4) CdtProblem
(5) CdtToCpxRelTrsProof [BOTH BOUNDS(ID, ID), 0 ms]
(6) CpxRelTRS
(7) RenamingProof [BOTH BOUNDS(ID, ID), 0 ms]
(8) CpxRelTRS
(9) TypeInferenceProof [BOTH BOUNDS(ID, ID), 0 ms]
(10) typed CpxTrs
(11) OrderProof [LOWER BOUND(ID), 39 ms]
(12) typed CpxTrs
(13) RewriteLemmaProof [LOWER BOUND(ID), 23.3 s]
(14) typed CpxTrs
(15) RewriteLemmaProof [LOWER BOUND(ID), 46.4 s]
(16) BEST
    (17) proven lower bound
        (18) LowerBoundPropagationProof [FINISHED, 0 ms]
        (19) BOUNDS(n^1, INF)
    (20) typed CpxTrs
        (21) RewriteLemmaProof [LOWER BOUND(ID), 102 ms]
        (22) typed CpxTrs


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

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


The TRS R consists of the following rules:

   colorof(node, Cons(CN(cl, N(name, adjs)), xs)) -> colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
   eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) -> and(True, eqColorList(cs1, cs2))
   eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) -> and(True, eqColorList(cs1, cs2))
   eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Red, cs1), Cons(Red, cs2)) -> and(True, eqColorList(cs1, cs2))
   eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) -> and(False, eqColorList(cs1, cs2))
   revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest))
   revapp(Nil, rest) -> rest
   possible(color, Cons(x, xs), colorednodes) -> possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
   possible(color, Nil, colorednodes) -> True
   colorrest(cs, ncs, colorednodes, Cons(x, xs)) -> colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
   colorrest(cs, ncs, colorednodes, Nil) -> colorednodes
   colorof(node, Nil) -> NoColor
   colornode(Cons(x, xs), N(n, ns), colorednodes) -> colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
   colornode(Nil, node, colorednodes) -> NotPossible
   graphcolour(Cons(x, xs), cs) -> reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
   eqColorList(Cons(c1, cs1), Nil) -> False
   eqColorList(Nil, Cons(c2, cs2)) -> False
   eqColorList(Nil, Nil) -> True
   eqColor(Yellow, NoColor) -> False
   eqColor(Yellow, Yellow) -> True
   eqColor(Yellow, Blue) -> False
   eqColor(Yellow, Red) -> False
   eqColor(Blue, NoColor) -> False
   eqColor(Blue, Yellow) -> False
   eqColor(Blue, Blue) -> True
   eqColor(Blue, Red) -> False
   eqColor(Red, NoColor) -> False
   eqColor(Red, Yellow) -> False
   eqColor(Red, Blue) -> False
   eqColor(Red, Red) -> True
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   isPossible(CN(cl, n)) -> True
   isPossible(NotPossible) -> False
   getNodeName(N(name, adjs)) -> name
   getNodeFromCN(CN(cl, n)) -> n
   getColorListFromCN(CN(cl, n)) -> cl
   getAdjs(N(n, ns)) -> ns
   eqColor(NoColor, b) -> False
   reverse(xs) -> revapp(xs, Nil)
   colorrestthetrick(cs1, cs, ncs, colorednodes, rest) -> colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

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

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) -> x
   colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) -> colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
   colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) -> colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
   possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) -> possible(color, xs, colorednodes)
   colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) -> colorrestthetrick(xs, cs, ncs, colorednodes, rest)
   colorof[Ite][True][Ite](False, node, Cons(x, xs)) -> colorof(node, xs)
   colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) -> colornode(xs, node, colorednodes)
   possible[Ite][True][Ite](True, color, adjs, colorednodes) -> False
   colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) -> colorrest(cs, cs1, colorednodes, rest)
   colornode[Ite][True][Ite](True, cs, node, colorednodes) -> CN(cs, node)

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

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

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


The TRS R consists of the following rules:

   colorof(node, Cons(CN(cl, N(name, adjs)), xs)) -> colorof[Ite][True][Ite](!EQ(name, node), node, Cons(CN(cl, N(name, adjs)), xs))
   eqColorList(Cons(Yellow, cs1), Cons(NoColor, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Yellow, cs1), Cons(Yellow, cs2)) -> and(True, eqColorList(cs1, cs2))
   eqColorList(Cons(Yellow, cs1), Cons(Blue, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Yellow, cs1), Cons(Red, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Blue, cs1), Cons(NoColor, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Blue, cs1), Cons(Yellow, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Blue, cs1), Cons(Blue, cs2)) -> and(True, eqColorList(cs1, cs2))
   eqColorList(Cons(Blue, cs1), Cons(Red, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Red, cs1), Cons(NoColor, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Red, cs1), Cons(Yellow, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Red, cs1), Cons(Blue, cs2)) -> and(False, eqColorList(cs1, cs2))
   eqColorList(Cons(Red, cs1), Cons(Red, cs2)) -> and(True, eqColorList(cs1, cs2))
   eqColorList(Cons(NoColor, cs1), Cons(b, cs2)) -> and(False, eqColorList(cs1, cs2))
   revapp(Cons(x, xs), rest) -> revapp(xs, Cons(x, rest))
   revapp(Nil, rest) -> rest
   possible(color, Cons(x, xs), colorednodes) -> possible[Ite][True][Ite](eqColor(color, colorof(x, colorednodes)), color, Cons(x, xs), colorednodes)
   possible(color, Nil, colorednodes) -> True
   colorrest(cs, ncs, colorednodes, Cons(x, xs)) -> colorrest[Ite][True][Let](cs, ncs, colorednodes, Cons(x, xs), colornode(ncs, x, colorednodes))
   colorrest(cs, ncs, colorednodes, Nil) -> colorednodes
   colorof(node, Nil) -> NoColor
   colornode(Cons(x, xs), N(n, ns), colorednodes) -> colornode[Ite][True][Ite](possible(x, ns, colorednodes), Cons(x, xs), N(n, ns), colorednodes)
   colornode(Nil, node, colorednodes) -> NotPossible
   graphcolour(Cons(x, xs), cs) -> reverse(colorrest(cs, cs, Cons(colornode(cs, x, Nil), Nil), xs))
   eqColorList(Cons(c1, cs1), Nil) -> False
   eqColorList(Nil, Cons(c2, cs2)) -> False
   eqColorList(Nil, Nil) -> True
   eqColor(Yellow, NoColor) -> False
   eqColor(Yellow, Yellow) -> True
   eqColor(Yellow, Blue) -> False
   eqColor(Yellow, Red) -> False
   eqColor(Blue, NoColor) -> False
   eqColor(Blue, Yellow) -> False
   eqColor(Blue, Blue) -> True
   eqColor(Blue, Red) -> False
   eqColor(Red, NoColor) -> False
   eqColor(Red, Yellow) -> False
   eqColor(Red, Blue) -> False
   eqColor(Red, Red) -> True
   notEmpty(Cons(x, xs)) -> True
   notEmpty(Nil) -> False
   isPossible(CN(cl, n)) -> True
   isPossible(NotPossible) -> False
   getNodeName(N(name, adjs)) -> name
   getNodeFromCN(CN(cl, n)) -> n
   getColorListFromCN(CN(cl, n)) -> cl
   getAdjs(N(n, ns)) -> ns
   eqColor(NoColor, b) -> False
   reverse(xs) -> revapp(xs, Nil)
   colorrestthetrick(cs1, cs, ncs, colorednodes, rest) -> colorrestthetrick[Ite](eqColorList(cs1, ncs), cs1, cs, ncs, colorednodes, rest)

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

   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(x), S(y)) -> !EQ(x, y)
   !EQ(0, S(y)) -> False
   !EQ(S(x), 0) -> False
   !EQ(0, 0) -> True
   colorof[Ite][True][Ite](True, node, Cons(CN(Cons(x, xs), n), xs')) -> x
   colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, CN(cl, n)) -> colorrest[Ite][True][Let][Ite](True, cs, ncs, colorednodes, rest, CN(cl, n))
   colorrest[Ite][True][Let](cs, ncs, colorednodes, rest, NotPossible) -> colorrest[Ite][True][Let][Ite](False, cs, ncs, colorednodes, rest, NotPossible)
   possible[Ite][True][Ite](False, color, Cons(x, xs), colorednodes) -> possible(color, xs, colorednodes)
   colorrestthetrick[Ite](False, Cons(x, xs), cs, ncs, colorednodes, rest) -> colorrestthetrick(xs, cs, ncs, colorednodes, rest)
   colorof[Ite][True][Ite](False, node, Cons(x, xs)) -> colorof(node, xs)
   colornode[Ite][True][Ite](False, Cons(x, xs), node, colorednodes) -> colornode(xs, node, colorednodes)
   possible[Ite][True][Ite](True, color, adjs, colorednodes) -> False
   colorrestthetrick[Ite](True, cs1, cs, ncs, colorednodes, rest) -> colorrest(cs, cs1, colorednodes, rest)
   colornode[Ite][True][Ite](True, cs, node, colorednodes) -> CN(cs, node)

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

(3) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID))
Converted Cpx (relative) TRS with rewrite strategy PARALLEL_INNERMOST to CDT
----------------------------------------

(4)
Obligation:
Complexity Dependency Tuples Problem

Rules:
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
   colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
   colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
   colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
   possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
   possible[Ite][True][Ite](True, z0, z1, z2) -> False
   colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
   colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
   colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
   colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
   colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
   colorof(z0, Nil) -> NoColor
   eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
   eqColorList(Cons(z0, z1), Nil) -> False
   eqColorList(Nil, Cons(z0, z1)) -> False
   eqColorList(Nil, Nil) -> True
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0
   possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
   possible(z0, Nil, z1) -> True
   colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
   colorrest(z0, z1, z2, Nil) -> z2
   colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
   colornode(Nil, z0, z1) -> NotPossible
   graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
   eqColor(Yellow, NoColor) -> False
   eqColor(Yellow, Yellow) -> True
   eqColor(Yellow, Blue) -> False
   eqColor(Yellow, Red) -> False
   eqColor(Blue, NoColor) -> False
   eqColor(Blue, Yellow) -> False
   eqColor(Blue, Blue) -> True
   eqColor(Blue, Red) -> False
   eqColor(Red, NoColor) -> False
   eqColor(Red, Yellow) -> False
   eqColor(Red, Blue) -> False
   eqColor(Red, Red) -> True
   eqColor(NoColor, z0) -> False
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   isPossible(CN(z0, z1)) -> True
   isPossible(NotPossible) -> False
   getNodeName(N(z0, z1)) -> z0
   getNodeFromCN(CN(z0, z1)) -> z1
   getColorListFromCN(CN(z0, z1)) -> z0
   getAdjs(N(z0, z1)) -> z1
   reverse(z0) -> revapp(z0, Nil)
   colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)
Tuples:
   AND(False, False) -> c
   AND(True, False) -> c1
   AND(False, True) -> c2
   AND(True, True) -> c3
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c5
   !EQ'(S(z0), 0) -> c6
   !EQ'(0, 0) -> c7
   COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
   COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
   COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
   COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
   POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
   POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
   COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
   COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
   COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
   COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
   COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
   COLOROF(z0, Nil) -> c19
   EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
   EQCOLORLIST(Cons(z0, z1), Nil) -> c33
   EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
   EQCOLORLIST(Nil, Nil) -> c35
   REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c37
   POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
   POSSIBLE(z0, Nil, z1) -> c39
   COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
   COLORREST(z0, z1, z2, Nil) -> c41
   COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
   COLORNODE(Nil, z0, z1) -> c43
   GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
   EQCOLOR(Yellow, NoColor) -> c45
   EQCOLOR(Yellow, Yellow) -> c46
   EQCOLOR(Yellow, Blue) -> c47
   EQCOLOR(Yellow, Red) -> c48
   EQCOLOR(Blue, NoColor) -> c49
   EQCOLOR(Blue, Yellow) -> c50
   EQCOLOR(Blue, Blue) -> c51
   EQCOLOR(Blue, Red) -> c52
   EQCOLOR(Red, NoColor) -> c53
   EQCOLOR(Red, Yellow) -> c54
   EQCOLOR(Red, Blue) -> c55
   EQCOLOR(Red, Red) -> c56
   EQCOLOR(NoColor, z0) -> c57
   NOTEMPTY(Cons(z0, z1)) -> c58
   NOTEMPTY(Nil) -> c59
   ISPOSSIBLE(CN(z0, z1)) -> c60
   ISPOSSIBLE(NotPossible) -> c61
   GETNODENAME(N(z0, z1)) -> c62
   GETNODEFROMCN(CN(z0, z1)) -> c63
   GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
   GETADJS(N(z0, z1)) -> c65
   REVERSE(z0) -> c66(REVAPP(z0, Nil))
   COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))
S tuples:
   COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
   COLOROF(z0, Nil) -> c19
   EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
   EQCOLORLIST(Cons(z0, z1), Nil) -> c33
   EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
   EQCOLORLIST(Nil, Nil) -> c35
   REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c37
   POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
   POSSIBLE(z0, Nil, z1) -> c39
   COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
   COLORREST(z0, z1, z2, Nil) -> c41
   COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
   COLORNODE(Nil, z0, z1) -> c43
   GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
   EQCOLOR(Yellow, NoColor) -> c45
   EQCOLOR(Yellow, Yellow) -> c46
   EQCOLOR(Yellow, Blue) -> c47
   EQCOLOR(Yellow, Red) -> c48
   EQCOLOR(Blue, NoColor) -> c49
   EQCOLOR(Blue, Yellow) -> c50
   EQCOLOR(Blue, Blue) -> c51
   EQCOLOR(Blue, Red) -> c52
   EQCOLOR(Red, NoColor) -> c53
   EQCOLOR(Red, Yellow) -> c54
   EQCOLOR(Red, Blue) -> c55
   EQCOLOR(Red, Red) -> c56
   EQCOLOR(NoColor, z0) -> c57
   NOTEMPTY(Cons(z0, z1)) -> c58
   NOTEMPTY(Nil) -> c59
   ISPOSSIBLE(CN(z0, z1)) -> c60
   ISPOSSIBLE(NotPossible) -> c61
   GETNODENAME(N(z0, z1)) -> c62
   GETNODEFROMCN(CN(z0, z1)) -> c63
   GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
   GETADJS(N(z0, z1)) -> c65
   REVERSE(z0) -> c66(REVAPP(z0, Nil))
   COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))
K tuples:none
Defined Rule Symbols:   colorof_2, eqColorList_2, revapp_2, possible_3, colorrest_4, colornode_3, graphcolour_2, eqColor_2, notEmpty_1, isPossible_1, getNodeName_1, getNodeFromCN_1, getColorListFromCN_1, getAdjs_1, reverse_1, colorrestthetrick_5, and_2, !EQ_2, colorof[Ite][True][Ite]_3, colorrest[Ite][True][Let]_5, possible[Ite][True][Ite]_4, colorrestthetrick[Ite]_6, colornode[Ite][True][Ite]_4

Defined Pair Symbols:   AND_2, !EQ'_2, COLOROF[ITE][TRUE][ITE]_3, COLORREST[ITE][TRUE][LET]_5, POSSIBLE[ITE][TRUE][ITE]_4, COLORRESTTHETRICK[ITE]_6, COLORNODE[ITE][TRUE][ITE]_4, COLOROF_2, EQCOLORLIST_2, REVAPP_2, POSSIBLE_3, COLORREST_4, COLORNODE_3, GRAPHCOLOUR_2, EQCOLOR_2, NOTEMPTY_1, ISPOSSIBLE_1, GETNODENAME_1, GETNODEFROMCN_1, GETCOLORLISTFROMCN_1, GETADJS_1, REVERSE_1, COLORRESTTHETRICK_5

Compound Symbols:   c, c1, c2, c3, c4_1, c5, c6, c7, c8, c9_1, c10, c11, c12_1, c13, c14_1, c15_1, c16_1, c17, c18_2, c19, c20_2, c21_2, c22_2, c23_2, c24_2, c25_2, c26_2, c27_2, c28_2, c29_2, c30_2, c31_2, c32_2, c33, c34, c35, c36_1, c37, c38_3, c39, c40_2, c41, c42_2, c43, c44_3, c45, c46, c47, c48, c49, c50, c51, c52, c53, c54, c55, c56, c57, c58, c59, c60, c61, c62, c63, c64, c65, c66_1, c67_2


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

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

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


The TRS R consists of the following rules:

   COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
   COLOROF(z0, Nil) -> c19
   EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
   EQCOLORLIST(Cons(z0, z1), Nil) -> c33
   EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
   EQCOLORLIST(Nil, Nil) -> c35
   REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c37
   POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
   POSSIBLE(z0, Nil, z1) -> c39
   COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
   COLORREST(z0, z1, z2, Nil) -> c41
   COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
   COLORNODE(Nil, z0, z1) -> c43
   GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
   EQCOLOR(Yellow, NoColor) -> c45
   EQCOLOR(Yellow, Yellow) -> c46
   EQCOLOR(Yellow, Blue) -> c47
   EQCOLOR(Yellow, Red) -> c48
   EQCOLOR(Blue, NoColor) -> c49
   EQCOLOR(Blue, Yellow) -> c50
   EQCOLOR(Blue, Blue) -> c51
   EQCOLOR(Blue, Red) -> c52
   EQCOLOR(Red, NoColor) -> c53
   EQCOLOR(Red, Yellow) -> c54
   EQCOLOR(Red, Blue) -> c55
   EQCOLOR(Red, Red) -> c56
   EQCOLOR(NoColor, z0) -> c57
   NOTEMPTY(Cons(z0, z1)) -> c58
   NOTEMPTY(Nil) -> c59
   ISPOSSIBLE(CN(z0, z1)) -> c60
   ISPOSSIBLE(NotPossible) -> c61
   GETNODENAME(N(z0, z1)) -> c62
   GETNODEFROMCN(CN(z0, z1)) -> c63
   GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
   GETADJS(N(z0, z1)) -> c65
   REVERSE(z0) -> c66(REVAPP(z0, Nil))
   COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))

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
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   !EQ'(0, S(z0)) -> c5
   !EQ'(S(z0), 0) -> c6
   !EQ'(0, 0) -> c7
   COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
   COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
   COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
   COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
   POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
   POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
   COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
   COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
   COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
   COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0, S(z0)) -> False
   !EQ(S(z0), 0) -> False
   !EQ(0, 0) -> True
   colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
   colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
   colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
   colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
   possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
   possible[Ite][True][Ite](True, z0, z1, z2) -> False
   colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
   colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
   colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
   colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
   colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
   colorof(z0, Nil) -> NoColor
   eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
   eqColorList(Cons(z0, z1), Nil) -> False
   eqColorList(Nil, Cons(z0, z1)) -> False
   eqColorList(Nil, Nil) -> True
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0
   possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
   possible(z0, Nil, z1) -> True
   colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
   colorrest(z0, z1, z2, Nil) -> z2
   colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
   colornode(Nil, z0, z1) -> NotPossible
   graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
   eqColor(Yellow, NoColor) -> False
   eqColor(Yellow, Yellow) -> True
   eqColor(Yellow, Blue) -> False
   eqColor(Yellow, Red) -> False
   eqColor(Blue, NoColor) -> False
   eqColor(Blue, Yellow) -> False
   eqColor(Blue, Blue) -> True
   eqColor(Blue, Red) -> False
   eqColor(Red, NoColor) -> False
   eqColor(Red, Yellow) -> False
   eqColor(Red, Blue) -> False
   eqColor(Red, Red) -> True
   eqColor(NoColor, z0) -> False
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   isPossible(CN(z0, z1)) -> True
   isPossible(NotPossible) -> False
   getNodeName(N(z0, z1)) -> z0
   getNodeFromCN(CN(z0, z1)) -> z1
   getColorListFromCN(CN(z0, z1)) -> z0
   getAdjs(N(z0, z1)) -> z1
   reverse(z0) -> revapp(z0, Nil)
   colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)

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

(7) RenamingProof (BOTH BOUNDS(ID, ID))
Renamed function symbols to avoid clashes with predefined symbol.
----------------------------------------

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


The TRS R consists of the following rules:

   COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
   COLOROF(z0, Nil) -> c19
   EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
   EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
   EQCOLORLIST(Cons(z0, z1), Nil) -> c33
   EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
   EQCOLORLIST(Nil, Nil) -> c35
   REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
   REVAPP(Nil, z0) -> c37
   POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
   POSSIBLE(z0, Nil, z1) -> c39
   COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
   COLORREST(z0, z1, z2, Nil) -> c41
   COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
   COLORNODE(Nil, z0, z1) -> c43
   GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
   EQCOLOR(Yellow, NoColor) -> c45
   EQCOLOR(Yellow, Yellow) -> c46
   EQCOLOR(Yellow, Blue) -> c47
   EQCOLOR(Yellow, Red) -> c48
   EQCOLOR(Blue, NoColor) -> c49
   EQCOLOR(Blue, Yellow) -> c50
   EQCOLOR(Blue, Blue) -> c51
   EQCOLOR(Blue, Red) -> c52
   EQCOLOR(Red, NoColor) -> c53
   EQCOLOR(Red, Yellow) -> c54
   EQCOLOR(Red, Blue) -> c55
   EQCOLOR(Red, Red) -> c56
   EQCOLOR(NoColor, z0) -> c57
   NOTEMPTY(Cons(z0, z1)) -> c58
   NOTEMPTY(Nil) -> c59
   ISPOSSIBLE(CN(z0, z1)) -> c60
   ISPOSSIBLE(NotPossible) -> c61
   GETNODENAME(N(z0, z1)) -> c62
   GETNODEFROMCN(CN(z0, z1)) -> c63
   GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
   GETADJS(N(z0, z1)) -> c65
   REVERSE(z0) -> c66(REVAPP(z0, Nil))
   COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))

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
   !EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
   !EQ'(0', S(z0)) -> c5
   !EQ'(S(z0), 0') -> c6
   !EQ'(0', 0') -> c7
   COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
   COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
   COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
   COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
   POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
   POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
   COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
   COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
   COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
   COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
   and(False, False) -> False
   and(True, False) -> False
   and(False, True) -> False
   and(True, True) -> True
   !EQ(S(z0), S(z1)) -> !EQ(z0, z1)
   !EQ(0', S(z0)) -> False
   !EQ(S(z0), 0') -> False
   !EQ(0', 0') -> True
   colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
   colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
   colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
   colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
   possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
   possible[Ite][True][Ite](True, z0, z1, z2) -> False
   colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
   colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
   colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
   colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
   colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
   colorof(z0, Nil) -> NoColor
   eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
   eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
   eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
   eqColorList(Cons(z0, z1), Nil) -> False
   eqColorList(Nil, Cons(z0, z1)) -> False
   eqColorList(Nil, Nil) -> True
   revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
   revapp(Nil, z0) -> z0
   possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
   possible(z0, Nil, z1) -> True
   colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
   colorrest(z0, z1, z2, Nil) -> z2
   colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
   colornode(Nil, z0, z1) -> NotPossible
   graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
   eqColor(Yellow, NoColor) -> False
   eqColor(Yellow, Yellow) -> True
   eqColor(Yellow, Blue) -> False
   eqColor(Yellow, Red) -> False
   eqColor(Blue, NoColor) -> False
   eqColor(Blue, Yellow) -> False
   eqColor(Blue, Blue) -> True
   eqColor(Blue, Red) -> False
   eqColor(Red, NoColor) -> False
   eqColor(Red, Yellow) -> False
   eqColor(Red, Blue) -> False
   eqColor(Red, Red) -> True
   eqColor(NoColor, z0) -> False
   notEmpty(Cons(z0, z1)) -> True
   notEmpty(Nil) -> False
   isPossible(CN(z0, z1)) -> True
   isPossible(NotPossible) -> False
   getNodeName(N(z0, z1)) -> z0
   getNodeFromCN(CN(z0, z1)) -> z1
   getColorListFromCN(CN(z0, z1)) -> z0
   getAdjs(N(z0, z1)) -> z1
   reverse(z0) -> revapp(z0, Nil)
   colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)

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

(9) TypeInferenceProof (BOTH BOUNDS(ID, ID))
Inferred types.
----------------------------------------

(10)
Obligation:
Innermost TRS:
Rules:
COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
COLOROF(z0, Nil) -> c19
EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
EQCOLORLIST(Cons(z0, z1), Nil) -> c33
EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
EQCOLORLIST(Nil, Nil) -> c35
REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
REVAPP(Nil, z0) -> c37
POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
POSSIBLE(z0, Nil, z1) -> c39
COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
COLORREST(z0, z1, z2, Nil) -> c41
COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
COLORNODE(Nil, z0, z1) -> c43
GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
EQCOLOR(Yellow, NoColor) -> c45
EQCOLOR(Yellow, Yellow) -> c46
EQCOLOR(Yellow, Blue) -> c47
EQCOLOR(Yellow, Red) -> c48
EQCOLOR(Blue, NoColor) -> c49
EQCOLOR(Blue, Yellow) -> c50
EQCOLOR(Blue, Blue) -> c51
EQCOLOR(Blue, Red) -> c52
EQCOLOR(Red, NoColor) -> c53
EQCOLOR(Red, Yellow) -> c54
EQCOLOR(Red, Blue) -> c55
EQCOLOR(Red, Red) -> c56
EQCOLOR(NoColor, z0) -> c57
NOTEMPTY(Cons(z0, z1)) -> c58
NOTEMPTY(Nil) -> c59
ISPOSSIBLE(CN(z0, z1)) -> c60
ISPOSSIBLE(NotPossible) -> c61
GETNODENAME(N(z0, z1)) -> c62
GETNODEFROMCN(CN(z0, z1)) -> c63
GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
GETADJS(N(z0, z1)) -> c65
REVERSE(z0) -> c66(REVAPP(z0, Nil))
COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
!EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c5
!EQ'(S(z0), 0') -> c6
!EQ'(0', 0') -> c7
COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
possible[Ite][True][Ite](True, z0, z1, z2) -> False
colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
colorof(z0, Nil) -> NoColor
eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
eqColorList(Cons(z0, z1), Nil) -> False
eqColorList(Nil, Cons(z0, z1)) -> False
eqColorList(Nil, Nil) -> True
revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
revapp(Nil, z0) -> z0
possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
possible(z0, Nil, z1) -> True
colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
colorrest(z0, z1, z2, Nil) -> z2
colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
colornode(Nil, z0, z1) -> NotPossible
graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
eqColor(Yellow, NoColor) -> False
eqColor(Yellow, Yellow) -> True
eqColor(Yellow, Blue) -> False
eqColor(Yellow, Red) -> False
eqColor(Blue, NoColor) -> False
eqColor(Blue, Yellow) -> False
eqColor(Blue, Blue) -> True
eqColor(Blue, Red) -> False
eqColor(Red, NoColor) -> False
eqColor(Red, Yellow) -> False
eqColor(Red, Blue) -> False
eqColor(Red, Red) -> True
eqColor(NoColor, z0) -> False
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
isPossible(CN(z0, z1)) -> True
isPossible(NotPossible) -> False
getNodeName(N(z0, z1)) -> z0
getNodeFromCN(CN(z0, z1)) -> z1
getColorListFromCN(CN(z0, z1)) -> z0
getAdjs(N(z0, z1)) -> z1
reverse(z0) -> revapp(z0, Nil)
colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)

Types:
COLOROF :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c18:c19
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c18 :: c8:c9 -> c4:c5:c6:c7 -> c18:c19
COLOROF[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c8:c9
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
!EQ' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c4:c5:c6:c7
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
c19 :: c18:c19
EQCOLORLIST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c20 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
AND :: False:True -> False:True -> c:c1:c2:c3
False :: False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c21 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c22 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c23 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c24 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c25 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c26 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c27 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c28 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c29 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c30 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c31 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c32 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c33 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c34 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c35 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
REVAPP :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c36:c37
c36 :: c36:c37 -> c36:c37
c37 :: c36:c37
POSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c38:c39
c38 :: c12:c13 -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57 -> c18:c19 -> c38:c39
POSSIBLE[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c12:c13
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
EQCOLOR :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c39 :: c38:c39
COLORREST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c40:c41
c40 :: c10:c11 -> c42:c43 -> c40:c41
COLORREST[ITE][TRUE][LET] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c10:c11
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
COLORNODE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c42:c43
c41 :: c40:c41
c42 :: c16:c17 -> c38:c39 -> c42:c43
COLORNODE[ITE][TRUE][ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c16:c17
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c43 :: c42:c43
GRAPHCOLOUR :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c44
c44 :: c66 -> c40:c41 -> c42:c43 -> c44
REVERSE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c66
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
c45 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c46 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c47 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c48 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c49 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c50 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c51 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c52 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c53 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c54 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c55 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c56 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c57 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
NOTEMPTY :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c58:c59
c58 :: c58:c59
c59 :: c58:c59
ISPOSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c60:c61
c60 :: c60:c61
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c61 :: c60:c61
GETNODENAME :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c62
c62 :: c62
GETNODEFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c63
c63 :: c63
GETCOLORLISTFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c64
c64 :: c64
GETADJS :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c65
c65 :: c65
c66 :: c36:c37 -> c66
COLORRESTTHETRICK :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c67
c67 :: c14:c15 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c67
COLORRESTTHETRICK[ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c14:c15
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c4 :: c4:c5:c6:c7 -> c4:c5:c6:c7
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c8:c9
c9 :: c18:c19 -> c8:c9
c10 :: c10:c11
c11 :: c10:c11
c12 :: c38:c39 -> c12:c13
c13 :: c12:c13
c14 :: c67 -> c14:c15
c15 :: c40:c41 -> c14:c15
c16 :: c42:c43 -> c16:c17
c17 :: c16:c17
and :: False:True -> False:True -> False:True
colorof[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
possible[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
colorrestthetrick[Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode[Ite][True][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c18:c191_68 :: c18:c19
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'2_68 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]3_68 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c8:c94_68 :: c8:c9
hole_c4:c5:c6:c75_68 :: c4:c5:c6:c7
hole_False:True6_68 :: False:True
hole_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c357_68 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
hole_c:c1:c2:c38_68 :: c:c1:c2:c3
hole_c36:c379_68 :: c36:c37
hole_c38:c3910_68 :: c38:c39
hole_c12:c1311_68 :: c12:c13
hole_c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c5712_68 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
hole_c40:c4113_68 :: c40:c41
hole_c10:c1114_68 :: c10:c11
hole_c42:c4315_68 :: c42:c43
hole_c16:c1716_68 :: c16:c17
hole_c4417_68 :: c44
hole_c6618_68 :: c66
hole_c58:c5919_68 :: c58:c59
hole_c60:c6120_68 :: c60:c61
hole_c6221_68 :: c62
hole_c6322_68 :: c63
hole_c6423_68 :: c64
hole_c6524_68 :: c65
hole_c6725_68 :: c67
hole_c14:c1526_68 :: c14:c15
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68 :: Nat -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68 :: Nat -> Cons:Nil:colorrest[Ite][True][Let][Ite]
gen_c4:c5:c6:c729_68 :: Nat -> c4:c5:c6:c7
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68 :: Nat -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
gen_c36:c3731_68 :: Nat -> c36:c37

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

(11) OrderProof (LOWER BOUND(ID))
Heuristically decided to analyse the following defined symbols:
COLOROF, !EQ, !EQ', EQCOLORLIST, eqColorList, REVAPP, POSSIBLE, colorof, colornode, COLORNODE, possible, COLORRESTTHETRICK, colorrestthetrick, revapp

They will be analysed ascendingly in the following order:
!EQ < COLOROF
!EQ' < COLOROF
COLOROF < POSSIBLE
!EQ < colorof
eqColorList < EQCOLORLIST
EQCOLORLIST < COLORRESTTHETRICK
eqColorList < COLORRESTTHETRICK
eqColorList < colorrestthetrick
colorof < POSSIBLE
POSSIBLE < COLORNODE
colorof < possible
possible < colornode
possible < COLORNODE

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

(12)
Obligation:
Innermost TRS:
Rules:
COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
COLOROF(z0, Nil) -> c19
EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
EQCOLORLIST(Cons(z0, z1), Nil) -> c33
EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
EQCOLORLIST(Nil, Nil) -> c35
REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
REVAPP(Nil, z0) -> c37
POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
POSSIBLE(z0, Nil, z1) -> c39
COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
COLORREST(z0, z1, z2, Nil) -> c41
COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
COLORNODE(Nil, z0, z1) -> c43
GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
EQCOLOR(Yellow, NoColor) -> c45
EQCOLOR(Yellow, Yellow) -> c46
EQCOLOR(Yellow, Blue) -> c47
EQCOLOR(Yellow, Red) -> c48
EQCOLOR(Blue, NoColor) -> c49
EQCOLOR(Blue, Yellow) -> c50
EQCOLOR(Blue, Blue) -> c51
EQCOLOR(Blue, Red) -> c52
EQCOLOR(Red, NoColor) -> c53
EQCOLOR(Red, Yellow) -> c54
EQCOLOR(Red, Blue) -> c55
EQCOLOR(Red, Red) -> c56
EQCOLOR(NoColor, z0) -> c57
NOTEMPTY(Cons(z0, z1)) -> c58
NOTEMPTY(Nil) -> c59
ISPOSSIBLE(CN(z0, z1)) -> c60
ISPOSSIBLE(NotPossible) -> c61
GETNODENAME(N(z0, z1)) -> c62
GETNODEFROMCN(CN(z0, z1)) -> c63
GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
GETADJS(N(z0, z1)) -> c65
REVERSE(z0) -> c66(REVAPP(z0, Nil))
COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
!EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c5
!EQ'(S(z0), 0') -> c6
!EQ'(0', 0') -> c7
COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
possible[Ite][True][Ite](True, z0, z1, z2) -> False
colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
colorof(z0, Nil) -> NoColor
eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
eqColorList(Cons(z0, z1), Nil) -> False
eqColorList(Nil, Cons(z0, z1)) -> False
eqColorList(Nil, Nil) -> True
revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
revapp(Nil, z0) -> z0
possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
possible(z0, Nil, z1) -> True
colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
colorrest(z0, z1, z2, Nil) -> z2
colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
colornode(Nil, z0, z1) -> NotPossible
graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
eqColor(Yellow, NoColor) -> False
eqColor(Yellow, Yellow) -> True
eqColor(Yellow, Blue) -> False
eqColor(Yellow, Red) -> False
eqColor(Blue, NoColor) -> False
eqColor(Blue, Yellow) -> False
eqColor(Blue, Blue) -> True
eqColor(Blue, Red) -> False
eqColor(Red, NoColor) -> False
eqColor(Red, Yellow) -> False
eqColor(Red, Blue) -> False
eqColor(Red, Red) -> True
eqColor(NoColor, z0) -> False
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
isPossible(CN(z0, z1)) -> True
isPossible(NotPossible) -> False
getNodeName(N(z0, z1)) -> z0
getNodeFromCN(CN(z0, z1)) -> z1
getColorListFromCN(CN(z0, z1)) -> z0
getAdjs(N(z0, z1)) -> z1
reverse(z0) -> revapp(z0, Nil)
colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)

Types:
COLOROF :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c18:c19
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c18 :: c8:c9 -> c4:c5:c6:c7 -> c18:c19
COLOROF[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c8:c9
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
!EQ' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c4:c5:c6:c7
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
c19 :: c18:c19
EQCOLORLIST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c20 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
AND :: False:True -> False:True -> c:c1:c2:c3
False :: False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c21 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c22 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c23 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c24 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c25 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c26 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c27 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c28 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c29 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c30 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c31 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c32 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c33 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c34 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c35 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
REVAPP :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c36:c37
c36 :: c36:c37 -> c36:c37
c37 :: c36:c37
POSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c38:c39
c38 :: c12:c13 -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57 -> c18:c19 -> c38:c39
POSSIBLE[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c12:c13
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
EQCOLOR :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c39 :: c38:c39
COLORREST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c40:c41
c40 :: c10:c11 -> c42:c43 -> c40:c41
COLORREST[ITE][TRUE][LET] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c10:c11
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
COLORNODE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c42:c43
c41 :: c40:c41
c42 :: c16:c17 -> c38:c39 -> c42:c43
COLORNODE[ITE][TRUE][ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c16:c17
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c43 :: c42:c43
GRAPHCOLOUR :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c44
c44 :: c66 -> c40:c41 -> c42:c43 -> c44
REVERSE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c66
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
c45 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c46 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c47 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c48 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c49 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c50 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c51 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c52 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c53 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c54 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c55 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c56 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c57 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
NOTEMPTY :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c58:c59
c58 :: c58:c59
c59 :: c58:c59
ISPOSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c60:c61
c60 :: c60:c61
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c61 :: c60:c61
GETNODENAME :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c62
c62 :: c62
GETNODEFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c63
c63 :: c63
GETCOLORLISTFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c64
c64 :: c64
GETADJS :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c65
c65 :: c65
c66 :: c36:c37 -> c66
COLORRESTTHETRICK :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c67
c67 :: c14:c15 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c67
COLORRESTTHETRICK[ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c14:c15
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c4 :: c4:c5:c6:c7 -> c4:c5:c6:c7
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c8:c9
c9 :: c18:c19 -> c8:c9
c10 :: c10:c11
c11 :: c10:c11
c12 :: c38:c39 -> c12:c13
c13 :: c12:c13
c14 :: c67 -> c14:c15
c15 :: c40:c41 -> c14:c15
c16 :: c42:c43 -> c16:c17
c17 :: c16:c17
and :: False:True -> False:True -> False:True
colorof[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
possible[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
colorrestthetrick[Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode[Ite][True][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c18:c191_68 :: c18:c19
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'2_68 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]3_68 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c8:c94_68 :: c8:c9
hole_c4:c5:c6:c75_68 :: c4:c5:c6:c7
hole_False:True6_68 :: False:True
hole_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c357_68 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
hole_c:c1:c2:c38_68 :: c:c1:c2:c3
hole_c36:c379_68 :: c36:c37
hole_c38:c3910_68 :: c38:c39
hole_c12:c1311_68 :: c12:c13
hole_c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c5712_68 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
hole_c40:c4113_68 :: c40:c41
hole_c10:c1114_68 :: c10:c11
hole_c42:c4315_68 :: c42:c43
hole_c16:c1716_68 :: c16:c17
hole_c4417_68 :: c44
hole_c6618_68 :: c66
hole_c58:c5919_68 :: c58:c59
hole_c60:c6120_68 :: c60:c61
hole_c6221_68 :: c62
hole_c6322_68 :: c63
hole_c6423_68 :: c64
hole_c6524_68 :: c65
hole_c6725_68 :: c67
hole_c14:c1526_68 :: c14:c15
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68 :: Nat -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68 :: Nat -> Cons:Nil:colorrest[Ite][True][Let][Ite]
gen_c4:c5:c6:c729_68 :: Nat -> c4:c5:c6:c7
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68 :: Nat -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
gen_c36:c3731_68 :: Nat -> c36:c37


Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(0) <=> Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(+(x, 1)) <=> CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(0) <=> Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(x, 1)) <=> Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(x))
gen_c4:c5:c6:c729_68(0) <=> c5
gen_c4:c5:c6:c729_68(+(x, 1)) <=> c4(gen_c4:c5:c6:c729_68(x))
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(0) <=> c33
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(+(x, 1)) <=> c20(c, gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(x))
gen_c36:c3731_68(0) <=> c37
gen_c36:c3731_68(+(x, 1)) <=> c36(gen_c36:c3731_68(x))


The following defined symbols remain to be analysed:
!EQ, COLOROF, !EQ', EQCOLORLIST, eqColorList, REVAPP, POSSIBLE, colorof, colornode, COLORNODE, possible, COLORRESTTHETRICK, colorrestthetrick, revapp

They will be analysed ascendingly in the following order:
!EQ < COLOROF
!EQ' < COLOROF
COLOROF < POSSIBLE
!EQ < colorof
eqColorList < EQCOLORLIST
EQCOLORLIST < COLORRESTTHETRICK
eqColorList < COLORRESTTHETRICK
eqColorList < colorrestthetrick
colorof < POSSIBLE
POSSIBLE < COLORNODE
colorof < possible
possible < colornode
possible < COLORNODE

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

(13) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n74_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n74_68)) -> False, rt in Omega(0)

Induction Base:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, 0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(0)) ->_R^Omega(0)
False

Induction Step:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, +(n74_68, 1))), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(n74_68, 1))) ->_R^Omega(0)
and(True, eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n74_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n74_68))) ->_IH
and(True, False) ->_R^Omega(0)
False

We have rt in Omega(1) and sz in O(n). Thus, we have irc_R in Omega(n^0).
----------------------------------------

(14)
Obligation:
Innermost TRS:
Rules:
COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
COLOROF(z0, Nil) -> c19
EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
EQCOLORLIST(Cons(z0, z1), Nil) -> c33
EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
EQCOLORLIST(Nil, Nil) -> c35
REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
REVAPP(Nil, z0) -> c37
POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
POSSIBLE(z0, Nil, z1) -> c39
COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
COLORREST(z0, z1, z2, Nil) -> c41
COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
COLORNODE(Nil, z0, z1) -> c43
GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
EQCOLOR(Yellow, NoColor) -> c45
EQCOLOR(Yellow, Yellow) -> c46
EQCOLOR(Yellow, Blue) -> c47
EQCOLOR(Yellow, Red) -> c48
EQCOLOR(Blue, NoColor) -> c49
EQCOLOR(Blue, Yellow) -> c50
EQCOLOR(Blue, Blue) -> c51
EQCOLOR(Blue, Red) -> c52
EQCOLOR(Red, NoColor) -> c53
EQCOLOR(Red, Yellow) -> c54
EQCOLOR(Red, Blue) -> c55
EQCOLOR(Red, Red) -> c56
EQCOLOR(NoColor, z0) -> c57
NOTEMPTY(Cons(z0, z1)) -> c58
NOTEMPTY(Nil) -> c59
ISPOSSIBLE(CN(z0, z1)) -> c60
ISPOSSIBLE(NotPossible) -> c61
GETNODENAME(N(z0, z1)) -> c62
GETNODEFROMCN(CN(z0, z1)) -> c63
GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
GETADJS(N(z0, z1)) -> c65
REVERSE(z0) -> c66(REVAPP(z0, Nil))
COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
!EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c5
!EQ'(S(z0), 0') -> c6
!EQ'(0', 0') -> c7
COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
possible[Ite][True][Ite](True, z0, z1, z2) -> False
colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
colorof(z0, Nil) -> NoColor
eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
eqColorList(Cons(z0, z1), Nil) -> False
eqColorList(Nil, Cons(z0, z1)) -> False
eqColorList(Nil, Nil) -> True
revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
revapp(Nil, z0) -> z0
possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
possible(z0, Nil, z1) -> True
colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
colorrest(z0, z1, z2, Nil) -> z2
colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
colornode(Nil, z0, z1) -> NotPossible
graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
eqColor(Yellow, NoColor) -> False
eqColor(Yellow, Yellow) -> True
eqColor(Yellow, Blue) -> False
eqColor(Yellow, Red) -> False
eqColor(Blue, NoColor) -> False
eqColor(Blue, Yellow) -> False
eqColor(Blue, Blue) -> True
eqColor(Blue, Red) -> False
eqColor(Red, NoColor) -> False
eqColor(Red, Yellow) -> False
eqColor(Red, Blue) -> False
eqColor(Red, Red) -> True
eqColor(NoColor, z0) -> False
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
isPossible(CN(z0, z1)) -> True
isPossible(NotPossible) -> False
getNodeName(N(z0, z1)) -> z0
getNodeFromCN(CN(z0, z1)) -> z1
getColorListFromCN(CN(z0, z1)) -> z0
getAdjs(N(z0, z1)) -> z1
reverse(z0) -> revapp(z0, Nil)
colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)

Types:
COLOROF :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c18:c19
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c18 :: c8:c9 -> c4:c5:c6:c7 -> c18:c19
COLOROF[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c8:c9
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
!EQ' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c4:c5:c6:c7
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
c19 :: c18:c19
EQCOLORLIST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c20 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
AND :: False:True -> False:True -> c:c1:c2:c3
False :: False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c21 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c22 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c23 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c24 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c25 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c26 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c27 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c28 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c29 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c30 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c31 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c32 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c33 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c34 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c35 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
REVAPP :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c36:c37
c36 :: c36:c37 -> c36:c37
c37 :: c36:c37
POSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c38:c39
c38 :: c12:c13 -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57 -> c18:c19 -> c38:c39
POSSIBLE[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c12:c13
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
EQCOLOR :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c39 :: c38:c39
COLORREST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c40:c41
c40 :: c10:c11 -> c42:c43 -> c40:c41
COLORREST[ITE][TRUE][LET] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c10:c11
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
COLORNODE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c42:c43
c41 :: c40:c41
c42 :: c16:c17 -> c38:c39 -> c42:c43
COLORNODE[ITE][TRUE][ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c16:c17
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c43 :: c42:c43
GRAPHCOLOUR :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c44
c44 :: c66 -> c40:c41 -> c42:c43 -> c44
REVERSE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c66
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
c45 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c46 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c47 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c48 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c49 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c50 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c51 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c52 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c53 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c54 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c55 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c56 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c57 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
NOTEMPTY :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c58:c59
c58 :: c58:c59
c59 :: c58:c59
ISPOSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c60:c61
c60 :: c60:c61
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c61 :: c60:c61
GETNODENAME :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c62
c62 :: c62
GETNODEFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c63
c63 :: c63
GETCOLORLISTFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c64
c64 :: c64
GETADJS :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c65
c65 :: c65
c66 :: c36:c37 -> c66
COLORRESTTHETRICK :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c67
c67 :: c14:c15 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c67
COLORRESTTHETRICK[ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c14:c15
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c4 :: c4:c5:c6:c7 -> c4:c5:c6:c7
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c8:c9
c9 :: c18:c19 -> c8:c9
c10 :: c10:c11
c11 :: c10:c11
c12 :: c38:c39 -> c12:c13
c13 :: c12:c13
c14 :: c67 -> c14:c15
c15 :: c40:c41 -> c14:c15
c16 :: c42:c43 -> c16:c17
c17 :: c16:c17
and :: False:True -> False:True -> False:True
colorof[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
possible[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
colorrestthetrick[Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode[Ite][True][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c18:c191_68 :: c18:c19
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'2_68 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]3_68 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c8:c94_68 :: c8:c9
hole_c4:c5:c6:c75_68 :: c4:c5:c6:c7
hole_False:True6_68 :: False:True
hole_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c357_68 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
hole_c:c1:c2:c38_68 :: c:c1:c2:c3
hole_c36:c379_68 :: c36:c37
hole_c38:c3910_68 :: c38:c39
hole_c12:c1311_68 :: c12:c13
hole_c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c5712_68 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
hole_c40:c4113_68 :: c40:c41
hole_c10:c1114_68 :: c10:c11
hole_c42:c4315_68 :: c42:c43
hole_c16:c1716_68 :: c16:c17
hole_c4417_68 :: c44
hole_c6618_68 :: c66
hole_c58:c5919_68 :: c58:c59
hole_c60:c6120_68 :: c60:c61
hole_c6221_68 :: c62
hole_c6322_68 :: c63
hole_c6423_68 :: c64
hole_c6524_68 :: c65
hole_c6725_68 :: c67
hole_c14:c1526_68 :: c14:c15
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68 :: Nat -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68 :: Nat -> Cons:Nil:colorrest[Ite][True][Let][Ite]
gen_c4:c5:c6:c729_68 :: Nat -> c4:c5:c6:c7
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68 :: Nat -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
gen_c36:c3731_68 :: Nat -> c36:c37


Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n74_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n74_68)) -> False, rt in Omega(0)


Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(0) <=> Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(+(x, 1)) <=> CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(0) <=> Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(x, 1)) <=> Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(x))
gen_c4:c5:c6:c729_68(0) <=> c5
gen_c4:c5:c6:c729_68(+(x, 1)) <=> c4(gen_c4:c5:c6:c729_68(x))
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(0) <=> c33
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(+(x, 1)) <=> c20(c, gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(x))
gen_c36:c3731_68(0) <=> c37
gen_c36:c3731_68(+(x, 1)) <=> c36(gen_c36:c3731_68(x))


The following defined symbols remain to be analysed:
EQCOLORLIST, REVAPP, POSSIBLE, colorof, colornode, COLORNODE, possible, COLORRESTTHETRICK, colorrestthetrick, revapp

They will be analysed ascendingly in the following order:
EQCOLORLIST < COLORRESTTHETRICK
colorof < POSSIBLE
POSSIBLE < COLORNODE
colorof < possible
possible < colornode
possible < COLORNODE

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

(15) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
EQCOLORLIST(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, n4056601_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n4056601_68))) -> *32_68, rt in Omega(n4056601_68)

Induction Base:
EQCOLORLIST(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, 0)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, 0)))

Induction Step:
EQCOLORLIST(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, +(n4056601_68, 1))), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, +(n4056601_68, 1)))) ->_R^Omega(1)
c21(AND(True, eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, n4056601_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n4056601_68)))), EQCOLORLIST(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, n4056601_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n4056601_68)))) ->_L^Omega(0)
c21(AND(True, False), EQCOLORLIST(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, n4056601_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n4056601_68)))) ->_R^Omega(0)
c21(c1, EQCOLORLIST(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, n4056601_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n4056601_68)))) ->_IH
c21(c1, *32_68)

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(16)
Complex Obligation (BEST)

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

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

Innermost TRS:
Rules:
COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
COLOROF(z0, Nil) -> c19
EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
EQCOLORLIST(Cons(z0, z1), Nil) -> c33
EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
EQCOLORLIST(Nil, Nil) -> c35
REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
REVAPP(Nil, z0) -> c37
POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
POSSIBLE(z0, Nil, z1) -> c39
COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
COLORREST(z0, z1, z2, Nil) -> c41
COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
COLORNODE(Nil, z0, z1) -> c43
GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
EQCOLOR(Yellow, NoColor) -> c45
EQCOLOR(Yellow, Yellow) -> c46
EQCOLOR(Yellow, Blue) -> c47
EQCOLOR(Yellow, Red) -> c48
EQCOLOR(Blue, NoColor) -> c49
EQCOLOR(Blue, Yellow) -> c50
EQCOLOR(Blue, Blue) -> c51
EQCOLOR(Blue, Red) -> c52
EQCOLOR(Red, NoColor) -> c53
EQCOLOR(Red, Yellow) -> c54
EQCOLOR(Red, Blue) -> c55
EQCOLOR(Red, Red) -> c56
EQCOLOR(NoColor, z0) -> c57
NOTEMPTY(Cons(z0, z1)) -> c58
NOTEMPTY(Nil) -> c59
ISPOSSIBLE(CN(z0, z1)) -> c60
ISPOSSIBLE(NotPossible) -> c61
GETNODENAME(N(z0, z1)) -> c62
GETNODEFROMCN(CN(z0, z1)) -> c63
GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
GETADJS(N(z0, z1)) -> c65
REVERSE(z0) -> c66(REVAPP(z0, Nil))
COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
!EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c5
!EQ'(S(z0), 0') -> c6
!EQ'(0', 0') -> c7
COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
possible[Ite][True][Ite](True, z0, z1, z2) -> False
colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
colorof(z0, Nil) -> NoColor
eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
eqColorList(Cons(z0, z1), Nil) -> False
eqColorList(Nil, Cons(z0, z1)) -> False
eqColorList(Nil, Nil) -> True
revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
revapp(Nil, z0) -> z0
possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
possible(z0, Nil, z1) -> True
colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
colorrest(z0, z1, z2, Nil) -> z2
colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
colornode(Nil, z0, z1) -> NotPossible
graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
eqColor(Yellow, NoColor) -> False
eqColor(Yellow, Yellow) -> True
eqColor(Yellow, Blue) -> False
eqColor(Yellow, Red) -> False
eqColor(Blue, NoColor) -> False
eqColor(Blue, Yellow) -> False
eqColor(Blue, Blue) -> True
eqColor(Blue, Red) -> False
eqColor(Red, NoColor) -> False
eqColor(Red, Yellow) -> False
eqColor(Red, Blue) -> False
eqColor(Red, Red) -> True
eqColor(NoColor, z0) -> False
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
isPossible(CN(z0, z1)) -> True
isPossible(NotPossible) -> False
getNodeName(N(z0, z1)) -> z0
getNodeFromCN(CN(z0, z1)) -> z1
getColorListFromCN(CN(z0, z1)) -> z0
getAdjs(N(z0, z1)) -> z1
reverse(z0) -> revapp(z0, Nil)
colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)

Types:
COLOROF :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c18:c19
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c18 :: c8:c9 -> c4:c5:c6:c7 -> c18:c19
COLOROF[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c8:c9
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
!EQ' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c4:c5:c6:c7
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
c19 :: c18:c19
EQCOLORLIST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c20 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
AND :: False:True -> False:True -> c:c1:c2:c3
False :: False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c21 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c22 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c23 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c24 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c25 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c26 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c27 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c28 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c29 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c30 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c31 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c32 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c33 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c34 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c35 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
REVAPP :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c36:c37
c36 :: c36:c37 -> c36:c37
c37 :: c36:c37
POSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c38:c39
c38 :: c12:c13 -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57 -> c18:c19 -> c38:c39
POSSIBLE[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c12:c13
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
EQCOLOR :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c39 :: c38:c39
COLORREST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c40:c41
c40 :: c10:c11 -> c42:c43 -> c40:c41
COLORREST[ITE][TRUE][LET] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c10:c11
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
COLORNODE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c42:c43
c41 :: c40:c41
c42 :: c16:c17 -> c38:c39 -> c42:c43
COLORNODE[ITE][TRUE][ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c16:c17
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c43 :: c42:c43
GRAPHCOLOUR :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c44
c44 :: c66 -> c40:c41 -> c42:c43 -> c44
REVERSE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c66
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
c45 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c46 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c47 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c48 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c49 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c50 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c51 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c52 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c53 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c54 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c55 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c56 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c57 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
NOTEMPTY :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c58:c59
c58 :: c58:c59
c59 :: c58:c59
ISPOSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c60:c61
c60 :: c60:c61
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c61 :: c60:c61
GETNODENAME :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c62
c62 :: c62
GETNODEFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c63
c63 :: c63
GETCOLORLISTFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c64
c64 :: c64
GETADJS :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c65
c65 :: c65
c66 :: c36:c37 -> c66
COLORRESTTHETRICK :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c67
c67 :: c14:c15 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c67
COLORRESTTHETRICK[ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c14:c15
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c4 :: c4:c5:c6:c7 -> c4:c5:c6:c7
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c8:c9
c9 :: c18:c19 -> c8:c9
c10 :: c10:c11
c11 :: c10:c11
c12 :: c38:c39 -> c12:c13
c13 :: c12:c13
c14 :: c67 -> c14:c15
c15 :: c40:c41 -> c14:c15
c16 :: c42:c43 -> c16:c17
c17 :: c16:c17
and :: False:True -> False:True -> False:True
colorof[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
possible[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
colorrestthetrick[Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode[Ite][True][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c18:c191_68 :: c18:c19
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'2_68 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]3_68 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c8:c94_68 :: c8:c9
hole_c4:c5:c6:c75_68 :: c4:c5:c6:c7
hole_False:True6_68 :: False:True
hole_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c357_68 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
hole_c:c1:c2:c38_68 :: c:c1:c2:c3
hole_c36:c379_68 :: c36:c37
hole_c38:c3910_68 :: c38:c39
hole_c12:c1311_68 :: c12:c13
hole_c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c5712_68 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
hole_c40:c4113_68 :: c40:c41
hole_c10:c1114_68 :: c10:c11
hole_c42:c4315_68 :: c42:c43
hole_c16:c1716_68 :: c16:c17
hole_c4417_68 :: c44
hole_c6618_68 :: c66
hole_c58:c5919_68 :: c58:c59
hole_c60:c6120_68 :: c60:c61
hole_c6221_68 :: c62
hole_c6322_68 :: c63
hole_c6423_68 :: c64
hole_c6524_68 :: c65
hole_c6725_68 :: c67
hole_c14:c1526_68 :: c14:c15
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68 :: Nat -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68 :: Nat -> Cons:Nil:colorrest[Ite][True][Let][Ite]
gen_c4:c5:c6:c729_68 :: Nat -> c4:c5:c6:c7
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68 :: Nat -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
gen_c36:c3731_68 :: Nat -> c36:c37


Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n74_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n74_68)) -> False, rt in Omega(0)


Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(0) <=> Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(+(x, 1)) <=> CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(0) <=> Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(x, 1)) <=> Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(x))
gen_c4:c5:c6:c729_68(0) <=> c5
gen_c4:c5:c6:c729_68(+(x, 1)) <=> c4(gen_c4:c5:c6:c729_68(x))
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(0) <=> c33
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(+(x, 1)) <=> c20(c, gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(x))
gen_c36:c3731_68(0) <=> c37
gen_c36:c3731_68(+(x, 1)) <=> c36(gen_c36:c3731_68(x))


The following defined symbols remain to be analysed:
EQCOLORLIST, REVAPP, POSSIBLE, colorof, colornode, COLORNODE, possible, COLORRESTTHETRICK, colorrestthetrick, revapp

They will be analysed ascendingly in the following order:
EQCOLORLIST < COLORRESTTHETRICK
colorof < POSSIBLE
POSSIBLE < COLORNODE
colorof < possible
possible < colornode
possible < COLORNODE

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

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

(19)
BOUNDS(n^1, INF)

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

(20)
Obligation:
Innermost TRS:
Rules:
COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
COLOROF(z0, Nil) -> c19
EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
EQCOLORLIST(Cons(z0, z1), Nil) -> c33
EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
EQCOLORLIST(Nil, Nil) -> c35
REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
REVAPP(Nil, z0) -> c37
POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
POSSIBLE(z0, Nil, z1) -> c39
COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
COLORREST(z0, z1, z2, Nil) -> c41
COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
COLORNODE(Nil, z0, z1) -> c43
GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
EQCOLOR(Yellow, NoColor) -> c45
EQCOLOR(Yellow, Yellow) -> c46
EQCOLOR(Yellow, Blue) -> c47
EQCOLOR(Yellow, Red) -> c48
EQCOLOR(Blue, NoColor) -> c49
EQCOLOR(Blue, Yellow) -> c50
EQCOLOR(Blue, Blue) -> c51
EQCOLOR(Blue, Red) -> c52
EQCOLOR(Red, NoColor) -> c53
EQCOLOR(Red, Yellow) -> c54
EQCOLOR(Red, Blue) -> c55
EQCOLOR(Red, Red) -> c56
EQCOLOR(NoColor, z0) -> c57
NOTEMPTY(Cons(z0, z1)) -> c58
NOTEMPTY(Nil) -> c59
ISPOSSIBLE(CN(z0, z1)) -> c60
ISPOSSIBLE(NotPossible) -> c61
GETNODENAME(N(z0, z1)) -> c62
GETNODEFROMCN(CN(z0, z1)) -> c63
GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
GETADJS(N(z0, z1)) -> c65
REVERSE(z0) -> c66(REVAPP(z0, Nil))
COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
!EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c5
!EQ'(S(z0), 0') -> c6
!EQ'(0', 0') -> c7
COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
possible[Ite][True][Ite](True, z0, z1, z2) -> False
colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
colorof(z0, Nil) -> NoColor
eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
eqColorList(Cons(z0, z1), Nil) -> False
eqColorList(Nil, Cons(z0, z1)) -> False
eqColorList(Nil, Nil) -> True
revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
revapp(Nil, z0) -> z0
possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
possible(z0, Nil, z1) -> True
colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
colorrest(z0, z1, z2, Nil) -> z2
colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
colornode(Nil, z0, z1) -> NotPossible
graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
eqColor(Yellow, NoColor) -> False
eqColor(Yellow, Yellow) -> True
eqColor(Yellow, Blue) -> False
eqColor(Yellow, Red) -> False
eqColor(Blue, NoColor) -> False
eqColor(Blue, Yellow) -> False
eqColor(Blue, Blue) -> True
eqColor(Blue, Red) -> False
eqColor(Red, NoColor) -> False
eqColor(Red, Yellow) -> False
eqColor(Red, Blue) -> False
eqColor(Red, Red) -> True
eqColor(NoColor, z0) -> False
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
isPossible(CN(z0, z1)) -> True
isPossible(NotPossible) -> False
getNodeName(N(z0, z1)) -> z0
getNodeFromCN(CN(z0, z1)) -> z1
getColorListFromCN(CN(z0, z1)) -> z0
getAdjs(N(z0, z1)) -> z1
reverse(z0) -> revapp(z0, Nil)
colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)

Types:
COLOROF :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c18:c19
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c18 :: c8:c9 -> c4:c5:c6:c7 -> c18:c19
COLOROF[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c8:c9
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
!EQ' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c4:c5:c6:c7
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
c19 :: c18:c19
EQCOLORLIST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c20 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
AND :: False:True -> False:True -> c:c1:c2:c3
False :: False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c21 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c22 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c23 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c24 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c25 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c26 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c27 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c28 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c29 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c30 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c31 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c32 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c33 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c34 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c35 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
REVAPP :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c36:c37
c36 :: c36:c37 -> c36:c37
c37 :: c36:c37
POSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c38:c39
c38 :: c12:c13 -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57 -> c18:c19 -> c38:c39
POSSIBLE[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c12:c13
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
EQCOLOR :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c39 :: c38:c39
COLORREST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c40:c41
c40 :: c10:c11 -> c42:c43 -> c40:c41
COLORREST[ITE][TRUE][LET] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c10:c11
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
COLORNODE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c42:c43
c41 :: c40:c41
c42 :: c16:c17 -> c38:c39 -> c42:c43
COLORNODE[ITE][TRUE][ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c16:c17
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c43 :: c42:c43
GRAPHCOLOUR :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c44
c44 :: c66 -> c40:c41 -> c42:c43 -> c44
REVERSE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c66
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
c45 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c46 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c47 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c48 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c49 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c50 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c51 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c52 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c53 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c54 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c55 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c56 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c57 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
NOTEMPTY :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c58:c59
c58 :: c58:c59
c59 :: c58:c59
ISPOSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c60:c61
c60 :: c60:c61
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c61 :: c60:c61
GETNODENAME :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c62
c62 :: c62
GETNODEFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c63
c63 :: c63
GETCOLORLISTFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c64
c64 :: c64
GETADJS :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c65
c65 :: c65
c66 :: c36:c37 -> c66
COLORRESTTHETRICK :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c67
c67 :: c14:c15 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c67
COLORRESTTHETRICK[ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c14:c15
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c4 :: c4:c5:c6:c7 -> c4:c5:c6:c7
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c8:c9
c9 :: c18:c19 -> c8:c9
c10 :: c10:c11
c11 :: c10:c11
c12 :: c38:c39 -> c12:c13
c13 :: c12:c13
c14 :: c67 -> c14:c15
c15 :: c40:c41 -> c14:c15
c16 :: c42:c43 -> c16:c17
c17 :: c16:c17
and :: False:True -> False:True -> False:True
colorof[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
possible[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
colorrestthetrick[Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode[Ite][True][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c18:c191_68 :: c18:c19
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'2_68 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]3_68 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c8:c94_68 :: c8:c9
hole_c4:c5:c6:c75_68 :: c4:c5:c6:c7
hole_False:True6_68 :: False:True
hole_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c357_68 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
hole_c:c1:c2:c38_68 :: c:c1:c2:c3
hole_c36:c379_68 :: c36:c37
hole_c38:c3910_68 :: c38:c39
hole_c12:c1311_68 :: c12:c13
hole_c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c5712_68 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
hole_c40:c4113_68 :: c40:c41
hole_c10:c1114_68 :: c10:c11
hole_c42:c4315_68 :: c42:c43
hole_c16:c1716_68 :: c16:c17
hole_c4417_68 :: c44
hole_c6618_68 :: c66
hole_c58:c5919_68 :: c58:c59
hole_c60:c6120_68 :: c60:c61
hole_c6221_68 :: c62
hole_c6322_68 :: c63
hole_c6423_68 :: c64
hole_c6524_68 :: c65
hole_c6725_68 :: c67
hole_c14:c1526_68 :: c14:c15
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68 :: Nat -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68 :: Nat -> Cons:Nil:colorrest[Ite][True][Let][Ite]
gen_c4:c5:c6:c729_68 :: Nat -> c4:c5:c6:c7
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68 :: Nat -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
gen_c36:c3731_68 :: Nat -> c36:c37


Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n74_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n74_68)) -> False, rt in Omega(0)
EQCOLORLIST(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, n4056601_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n4056601_68))) -> *32_68, rt in Omega(n4056601_68)


Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(0) <=> Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(+(x, 1)) <=> CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(0) <=> Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(x, 1)) <=> Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(x))
gen_c4:c5:c6:c729_68(0) <=> c5
gen_c4:c5:c6:c729_68(+(x, 1)) <=> c4(gen_c4:c5:c6:c729_68(x))
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(0) <=> c33
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(+(x, 1)) <=> c20(c, gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(x))
gen_c36:c3731_68(0) <=> c37
gen_c36:c3731_68(+(x, 1)) <=> c36(gen_c36:c3731_68(x))


The following defined symbols remain to be analysed:
REVAPP, POSSIBLE, colorof, colornode, COLORNODE, possible, COLORRESTTHETRICK, colorrestthetrick, revapp

They will be analysed ascendingly in the following order:
colorof < POSSIBLE
POSSIBLE < COLORNODE
colorof < possible
possible < colornode
possible < COLORNODE

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

(21) RewriteLemmaProof (LOWER BOUND(ID))
Proved the following rewrite lemma:
REVAPP(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n11721368_68), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(b)) -> gen_c36:c3731_68(n11721368_68), rt in Omega(1 + n11721368_68)

Induction Base:
REVAPP(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(0), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(b)) ->_R^Omega(1)
c37

Induction Step:
REVAPP(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(n11721368_68, 1)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(b)) ->_R^Omega(1)
c36(REVAPP(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n11721368_68), Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(b)))) ->_IH
c36(gen_c36:c3731_68(c11721369_68))

We have rt in Omega(n^1) and sz in O(n). Thus, we have irc_R in Omega(n).
----------------------------------------

(22)
Obligation:
Innermost TRS:
Rules:
COLOROF(z0, Cons(CN(z1, N(z2, z3)), z4)) -> c18(COLOROF[ITE][TRUE][ITE](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4)), !EQ'(z2, z0))
COLOROF(z0, Nil) -> c19
EQCOLORLIST(Cons(Yellow, z0), Cons(NoColor, z1)) -> c20(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Yellow, z1)) -> c21(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Blue, z1)) -> c22(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Yellow, z0), Cons(Red, z1)) -> c23(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(NoColor, z1)) -> c24(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Yellow, z1)) -> c25(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Blue, z1)) -> c26(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Blue, z0), Cons(Red, z1)) -> c27(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(NoColor, z1)) -> c28(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Yellow, z1)) -> c29(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Blue, z1)) -> c30(AND(False, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(Red, z0), Cons(Red, z1)) -> c31(AND(True, eqColorList(z0, z1)), EQCOLORLIST(z0, z1))
EQCOLORLIST(Cons(NoColor, z0), Cons(z1, z2)) -> c32(AND(False, eqColorList(z0, z2)), EQCOLORLIST(z0, z2))
EQCOLORLIST(Cons(z0, z1), Nil) -> c33
EQCOLORLIST(Nil, Cons(z0, z1)) -> c34
EQCOLORLIST(Nil, Nil) -> c35
REVAPP(Cons(z0, z1), z2) -> c36(REVAPP(z1, Cons(z0, z2)))
REVAPP(Nil, z0) -> c37
POSSIBLE(z0, Cons(z1, z2), z3) -> c38(POSSIBLE[ITE][TRUE][ITE](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3), EQCOLOR(z0, colorof(z1, z3)), COLOROF(z1, z3))
POSSIBLE(z0, Nil, z1) -> c39
COLORREST(z0, z1, z2, Cons(z3, z4)) -> c40(COLORREST[ITE][TRUE][LET](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2)), COLORNODE(z1, z3, z2))
COLORREST(z0, z1, z2, Nil) -> c41
COLORNODE(Cons(z0, z1), N(z2, z3), z4) -> c42(COLORNODE[ITE][TRUE][ITE](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4), POSSIBLE(z0, z3, z4))
COLORNODE(Nil, z0, z1) -> c43
GRAPHCOLOUR(Cons(z0, z1), z2) -> c44(REVERSE(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1)), COLORREST(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1), COLORNODE(z2, z0, Nil))
EQCOLOR(Yellow, NoColor) -> c45
EQCOLOR(Yellow, Yellow) -> c46
EQCOLOR(Yellow, Blue) -> c47
EQCOLOR(Yellow, Red) -> c48
EQCOLOR(Blue, NoColor) -> c49
EQCOLOR(Blue, Yellow) -> c50
EQCOLOR(Blue, Blue) -> c51
EQCOLOR(Blue, Red) -> c52
EQCOLOR(Red, NoColor) -> c53
EQCOLOR(Red, Yellow) -> c54
EQCOLOR(Red, Blue) -> c55
EQCOLOR(Red, Red) -> c56
EQCOLOR(NoColor, z0) -> c57
NOTEMPTY(Cons(z0, z1)) -> c58
NOTEMPTY(Nil) -> c59
ISPOSSIBLE(CN(z0, z1)) -> c60
ISPOSSIBLE(NotPossible) -> c61
GETNODENAME(N(z0, z1)) -> c62
GETNODEFROMCN(CN(z0, z1)) -> c63
GETCOLORLISTFROMCN(CN(z0, z1)) -> c64
GETADJS(N(z0, z1)) -> c65
REVERSE(z0) -> c66(REVAPP(z0, Nil))
COLORRESTTHETRICK(z0, z1, z2, z3, z4) -> c67(COLORRESTTHETRICK[ITE](eqColorList(z0, z2), z0, z1, z2, z3, z4), EQCOLORLIST(z0, z2))
AND(False, False) -> c
AND(True, False) -> c1
AND(False, True) -> c2
AND(True, True) -> c3
!EQ'(S(z0), S(z1)) -> c4(!EQ'(z0, z1))
!EQ'(0', S(z0)) -> c5
!EQ'(S(z0), 0') -> c6
!EQ'(0', 0') -> c7
COLOROF[ITE][TRUE][ITE](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> c8
COLOROF[ITE][TRUE][ITE](False, z0, Cons(z1, z2)) -> c9(COLOROF(z0, z2))
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, CN(z4, z5)) -> c10
COLORREST[ITE][TRUE][LET](z0, z1, z2, z3, NotPossible) -> c11
POSSIBLE[ITE][TRUE][ITE](False, z0, Cons(z1, z2), z3) -> c12(POSSIBLE(z0, z2, z3))
POSSIBLE[ITE][TRUE][ITE](True, z0, z1, z2) -> c13
COLORRESTTHETRICK[ITE](False, Cons(z0, z1), z2, z3, z4, z5) -> c14(COLORRESTTHETRICK(z1, z2, z3, z4, z5))
COLORRESTTHETRICK[ITE](True, z0, z1, z2, z3, z4) -> c15(COLORREST(z1, z0, z3, z4))
COLORNODE[ITE][TRUE][ITE](False, Cons(z0, z1), z2, z3) -> c16(COLORNODE(z1, z2, z3))
COLORNODE[ITE][TRUE][ITE](True, z0, z1, z2) -> c17
and(False, False) -> False
and(True, False) -> False
and(False, True) -> False
and(True, True) -> True
!EQ(S(z0), S(z1)) -> !EQ(z0, z1)
!EQ(0', S(z0)) -> False
!EQ(S(z0), 0') -> False
!EQ(0', 0') -> True
colorof[Ite][True][Ite](True, z0, Cons(CN(Cons(z1, z2), z3), z4)) -> z1
colorof[Ite][True][Ite](False, z0, Cons(z1, z2)) -> colorof(z0, z2)
colorrest[Ite][True][Let](z0, z1, z2, z3, CN(z4, z5)) -> colorrest[Ite][True][Let][Ite](True, z0, z1, z2, z3, CN(z4, z5))
colorrest[Ite][True][Let](z0, z1, z2, z3, NotPossible) -> colorrest[Ite][True][Let][Ite](False, z0, z1, z2, z3, NotPossible)
possible[Ite][True][Ite](False, z0, Cons(z1, z2), z3) -> possible(z0, z2, z3)
possible[Ite][True][Ite](True, z0, z1, z2) -> False
colorrestthetrick[Ite](False, Cons(z0, z1), z2, z3, z4, z5) -> colorrestthetrick(z1, z2, z3, z4, z5)
colorrestthetrick[Ite](True, z0, z1, z2, z3, z4) -> colorrest(z1, z0, z3, z4)
colornode[Ite][True][Ite](False, Cons(z0, z1), z2, z3) -> colornode(z1, z2, z3)
colornode[Ite][True][Ite](True, z0, z1, z2) -> CN(z0, z1)
colorof(z0, Cons(CN(z1, N(z2, z3)), z4)) -> colorof[Ite][True][Ite](!EQ(z2, z0), z0, Cons(CN(z1, N(z2, z3)), z4))
colorof(z0, Nil) -> NoColor
eqColorList(Cons(Yellow, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Yellow, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Yellow, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Blue, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(Blue, z0), Cons(Red, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(NoColor, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Yellow, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Blue, z1)) -> and(False, eqColorList(z0, z1))
eqColorList(Cons(Red, z0), Cons(Red, z1)) -> and(True, eqColorList(z0, z1))
eqColorList(Cons(NoColor, z0), Cons(z1, z2)) -> and(False, eqColorList(z0, z2))
eqColorList(Cons(z0, z1), Nil) -> False
eqColorList(Nil, Cons(z0, z1)) -> False
eqColorList(Nil, Nil) -> True
revapp(Cons(z0, z1), z2) -> revapp(z1, Cons(z0, z2))
revapp(Nil, z0) -> z0
possible(z0, Cons(z1, z2), z3) -> possible[Ite][True][Ite](eqColor(z0, colorof(z1, z3)), z0, Cons(z1, z2), z3)
possible(z0, Nil, z1) -> True
colorrest(z0, z1, z2, Cons(z3, z4)) -> colorrest[Ite][True][Let](z0, z1, z2, Cons(z3, z4), colornode(z1, z3, z2))
colorrest(z0, z1, z2, Nil) -> z2
colornode(Cons(z0, z1), N(z2, z3), z4) -> colornode[Ite][True][Ite](possible(z0, z3, z4), Cons(z0, z1), N(z2, z3), z4)
colornode(Nil, z0, z1) -> NotPossible
graphcolour(Cons(z0, z1), z2) -> reverse(colorrest(z2, z2, Cons(colornode(z2, z0, Nil), Nil), z1))
eqColor(Yellow, NoColor) -> False
eqColor(Yellow, Yellow) -> True
eqColor(Yellow, Blue) -> False
eqColor(Yellow, Red) -> False
eqColor(Blue, NoColor) -> False
eqColor(Blue, Yellow) -> False
eqColor(Blue, Blue) -> True
eqColor(Blue, Red) -> False
eqColor(Red, NoColor) -> False
eqColor(Red, Yellow) -> False
eqColor(Red, Blue) -> False
eqColor(Red, Red) -> True
eqColor(NoColor, z0) -> False
notEmpty(Cons(z0, z1)) -> True
notEmpty(Nil) -> False
isPossible(CN(z0, z1)) -> True
isPossible(NotPossible) -> False
getNodeName(N(z0, z1)) -> z0
getNodeFromCN(CN(z0, z1)) -> z1
getColorListFromCN(CN(z0, z1)) -> z0
getAdjs(N(z0, z1)) -> z1
reverse(z0) -> revapp(z0, Nil)
colorrestthetrick(z0, z1, z2, z3, z4) -> colorrestthetrick[Ite](eqColorList(z0, z2), z0, z1, z2, z3, z4)

Types:
COLOROF :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c18:c19
Cons :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
CN :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
N :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c18 :: c8:c9 -> c4:c5:c6:c7 -> c18:c19
COLOROF[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c8:c9
!EQ :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
!EQ' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c4:c5:c6:c7
Nil :: Cons:Nil:colorrest[Ite][True][Let][Ite]
c19 :: c18:c19
EQCOLORLIST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Yellow :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
NoColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c20 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
AND :: False:True -> False:True -> c:c1:c2:c3
False :: False:True
eqColorList :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c21 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
True :: False:True
Blue :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c22 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
Red :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c23 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c24 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c25 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c26 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c27 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c28 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c29 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c30 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c31 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c32 :: c:c1:c2:c3 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c33 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c34 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
c35 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
REVAPP :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c36:c37
c36 :: c36:c37 -> c36:c37
c37 :: c36:c37
POSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c38:c39
c38 :: c12:c13 -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57 -> c18:c19 -> c38:c39
POSSIBLE[ITE][TRUE][ITE] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c12:c13
eqColor :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
colorof :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
EQCOLOR :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c39 :: c38:c39
COLORREST :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c40:c41
c40 :: c10:c11 -> c42:c43 -> c40:c41
COLORREST[ITE][TRUE][LET] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c10:c11
colornode :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
COLORNODE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c42:c43
c41 :: c40:c41
c42 :: c16:c17 -> c38:c39 -> c42:c43
COLORNODE[ITE][TRUE][ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c16:c17
possible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
c43 :: c42:c43
GRAPHCOLOUR :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c44
c44 :: c66 -> c40:c41 -> c42:c43 -> c44
REVERSE :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c66
colorrest :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
c45 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c46 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c47 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c48 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c49 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c50 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c51 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c52 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c53 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c54 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c55 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c56 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
c57 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
NOTEMPTY :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> c58:c59
c58 :: c58:c59
c59 :: c58:c59
ISPOSSIBLE :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c60:c61
c60 :: c60:c61
NotPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c61 :: c60:c61
GETNODENAME :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c62
c62 :: c62
GETNODEFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c63
c63 :: c63
GETCOLORLISTFROMCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c64
c64 :: c64
GETADJS :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> c65
c65 :: c65
c66 :: c36:c37 -> c66
COLORRESTTHETRICK :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c67
c67 :: c14:c15 -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35 -> c67
COLORRESTTHETRICK[ITE] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> c14:c15
c :: c:c1:c2:c3
c1 :: c:c1:c2:c3
c2 :: c:c1:c2:c3
c3 :: c:c1:c2:c3
S :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c4 :: c4:c5:c6:c7 -> c4:c5:c6:c7
0' :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
c5 :: c4:c5:c6:c7
c6 :: c4:c5:c6:c7
c7 :: c4:c5:c6:c7
c8 :: c8:c9
c9 :: c18:c19 -> c8:c9
c10 :: c10:c11
c11 :: c10:c11
c12 :: c38:c39 -> c12:c13
c13 :: c12:c13
c14 :: c67 -> c14:c15
c15 :: c40:c41 -> c14:c15
c16 :: c42:c43 -> c16:c17
c17 :: c16:c17
and :: False:True -> False:True -> False:True
colorof[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
colorrest[Ite][True][Let] :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrest[Ite][True][Let][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
possible[Ite][True][Ite] :: False:True -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
colorrestthetrick[Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colorrestthetrick :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
colornode[Ite][True][Ite] :: False:True -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
revapp :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
graphcolour :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
reverse :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> Cons:Nil:colorrest[Ite][True][Let][Ite]
notEmpty :: Cons:Nil:colorrest[Ite][True][Let][Ite] -> False:True
isPossible :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> False:True
getNodeName :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getNodeFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
getColorListFromCN :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
getAdjs :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0' -> Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c18:c191_68 :: c18:c19
hole_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'2_68 :: N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
hole_Cons:Nil:colorrest[Ite][True][Let][Ite]3_68 :: Cons:Nil:colorrest[Ite][True][Let][Ite]
hole_c8:c94_68 :: c8:c9
hole_c4:c5:c6:c75_68 :: c4:c5:c6:c7
hole_False:True6_68 :: False:True
hole_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c357_68 :: c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
hole_c:c1:c2:c38_68 :: c:c1:c2:c3
hole_c36:c379_68 :: c36:c37
hole_c38:c3910_68 :: c38:c39
hole_c12:c1311_68 :: c12:c13
hole_c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c5712_68 :: c45:c46:c47:c48:c49:c50:c51:c52:c53:c54:c55:c56:c57
hole_c40:c4113_68 :: c40:c41
hole_c10:c1114_68 :: c10:c11
hole_c42:c4315_68 :: c42:c43
hole_c16:c1716_68 :: c16:c17
hole_c4417_68 :: c44
hole_c6618_68 :: c66
hole_c58:c5919_68 :: c58:c59
hole_c60:c6120_68 :: c60:c61
hole_c6221_68 :: c62
hole_c6322_68 :: c63
hole_c6423_68 :: c64
hole_c6524_68 :: c65
hole_c6725_68 :: c67
hole_c14:c1526_68 :: c14:c15
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68 :: Nat -> N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68 :: Nat -> Cons:Nil:colorrest[Ite][True][Let][Ite]
gen_c4:c5:c6:c729_68 :: Nat -> c4:c5:c6:c7
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68 :: Nat -> c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c35
gen_c36:c3731_68 :: Nat -> c36:c37


Lemmas:
eqColorList(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n74_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n74_68)) -> False, rt in Omega(0)
EQCOLORLIST(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(2, n4056601_68)), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(1, n4056601_68))) -> *32_68, rt in Omega(n4056601_68)
REVAPP(gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(n11721368_68), gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(b)) -> gen_c36:c3731_68(n11721368_68), rt in Omega(1 + n11721368_68)


Generator Equations:
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(0) <=> Yellow
gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(+(x, 1)) <=> CN(Nil, gen_N:CN:Yellow:NoColor:Blue:Red:NotPossible:S:0'27_68(x))
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(0) <=> Nil
gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(+(x, 1)) <=> Cons(Yellow, gen_Cons:Nil:colorrest[Ite][True][Let][Ite]28_68(x))
gen_c4:c5:c6:c729_68(0) <=> c5
gen_c4:c5:c6:c729_68(+(x, 1)) <=> c4(gen_c4:c5:c6:c729_68(x))
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(0) <=> c33
gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(+(x, 1)) <=> c20(c, gen_c20:c21:c22:c23:c24:c25:c26:c27:c28:c29:c30:c31:c32:c33:c34:c3530_68(x))
gen_c36:c3731_68(0) <=> c37
gen_c36:c3731_68(+(x, 1)) <=> c36(gen_c36:c3731_68(x))


The following defined symbols remain to be analysed:
colorof, POSSIBLE, colornode, COLORNODE, possible, COLORRESTTHETRICK, colorrestthetrick, revapp

They will be analysed ascendingly in the following order:
colorof < POSSIBLE
POSSIBLE < COLORNODE
colorof < possible
possible < colornode
possible < COLORNODE