(VAR adjs b c1 c2 cl color colorednodes cs cs1 cs2 n name ncs node ns rest x xs xs' y )
(STRATEGY INNERMOST)
(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)
        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)
)