Why do I keep running into contradictions in this problem (Knights and Knaves variation)? Edit: I've attempted to solve this another way and posted it as a possible answer. Hesitant to accept it, and would appreciate if anyone could go over it and confirm it's the way to go.
There is an island inhabited by two tribes, a tribe of Knaves (who always lie) and Spies (who lie to Knaves but tell the truth to other Spies).
\begin{align}
A \text{ says to } B &: F \text{ is a Spy, } C \text{ is a Knave.}\\
B \text{ says to } C &: \text{ If } D \text{ is a Knave, then so is }E\text{.}\\
C \text{ says to } D &: \text{ If } A \text{ is a Knave, then } F \text{ is a Spy.}\\
D \text{ says to } E &: \text{ Either } F \text{ is a Spy, or } A \text{ is a Knave.}\\
\end{align}
Determine which of the persons $A$, $B$, $C$, $D$ and $E$ are Spies, and which are Knaves.
Here is how I tried to tackle the problem:
For clarity, I write negation as $\bar p$, conjunction as $pq$, disjunction as $p+q$, exclusive disjunction as $p\oplus q$, implication as $p\implies q$ and contradiction as ↯.
If a person $x$ is a Knave, I denote it as $x=0$. Likewise if $x$ is a Spy, $x=1$.
The truthfullness of a statement $T$ ($0$ for false and $1$ for true) is a function of the person making the statement ($x$) and the person the statement is being made to ($y$). Obviously $T(x,y)=1$ iff $xy=1$.
First thing I did was write the statements thusly:
\begin{align}
AB&=F        \tag{1a}\\
AB&=\bar C          \tag{1b}\\
BC&=\bar D\implies \bar E  =       \\
        &=\bar D \bar E + D =      \\
        &=D+ \bar E     \tag{2}\\
CD&=\bar A\implies F   =       \\
        &=\bar AF +  A   =      \\
        &=A+ F       \tag{3}\\
DE&=F\oplus \bar A    =         \\
        &=\bar F \bar A + FA   \tag{4}\\
\end{align}
I made different assumptions about $A$ and $B$ (for all $4$ possible combinations) and based on them, calculating the values for $C$, $D$, $E$ and $F$. In all cases I ran into contradiction. I went over this lots of times, and simply can't see any flaw in my reasoning, so I'd appreciate any help. Also any advice about alternate (probably more elegant) approaches to this problem would be welcome.
Here is exactly what I did:
\begin{align}
\text{Assume}: A=0, B=0\tag{I}\\
\text{From (1a) and (1b)}: F=0, C=1\\
\text{From (2)}: D+\bar E=0\\
D=0, E=1\\
\text{From (3)}: A+F=0\\
\text{From (4)}: \bar F \bar A + FA=0 \\
1+0=0 ↯\\
\end{align}
\begin{align}
\text{Assume}: A&=0, B=1\tag{II}\\
\text{From (1a) and (1b)}: F&=0, C=1\\
\text{From (2)}: D+\bar E&=1\\
\text{Assume}: D&=0, E=0\tag{IIa}\\
\text{From (3)}: A&=0, F=0\\
\text{From (4)}: 1+0&=0 ↯\\
\text{Assume}: D&=1, E=1\tag{IIb}\\
\text{From (3)}: A+F&=1 ↯\\
\text{Assume}:D&=1, E=0\tag{IIc}\\
\text{From (3)}: A+F&=1 ↯\\
\end{align}
\begin{align}
\text{Assume}: A&=1, B=0\tag{III}\\
\text{From (1a) and (1b)}: F&=0, C=1\\
\text{From (2)}: D&=0, E=1\\
\text{From (3)}: A+F&=0 ↯\\
\end{align}
\begin{align}
\text{Assume}: A&=1, B=1\tag{IV}\\
\text{From (1a) and (1b)}: F&=1, C=0\\
\text{From (2)}: D&=0, E=1\\
\text{From (3)}: A+F&=0 ↯\\
\end{align}
 A: I translated your riddle into a Boolean circuit:
BC1.1

//  A says to B: F is a Spy, C is a Knave
S1 := F & !C;
//  if A is a Knave or B is a Spy
//  the statement of A is false
A1 := (!A | (A & !B)) => !S1;
//  if A and B are Spies, the statement is true
A2 := (A & B) => S1;

//  B says to C: If D is a Knave, then so is E
S2 := !D => !E;
B1 := (!B | (B & !C)) => !S2;
B2 := (B & C) => S2;

//  C says to D: If A is a Knave, then F is a Spy
S3 := !A => F;
C1 := (!C | (C & !D)) => !S3;
C2 := (C & D) => S3;

//  D says to E: Either F is a Spy, or A is a Knave
S4 := F ^ !A;
D1 := (!D | (D & E)) => !S4;
D2 := (D & E) => S4;

//  all variables must be true
ASSIGN A1, A2, B1, B2, C1, C2, D1, D2;

Using the tool bc2cnf, I converted the circuit into a Conjunctive Normal Form and ran two SAT Solvers Z3 and Cryptominisat to find a solution.
Both returned UNSAT, i.e. no solution exists, or there is some error in my circuit description.
A: A possible answer might be this. It doesn't give a unique solution, and I think it's a bit iffy, so I won't accept it yet, and would appreciate if anyone could look it over.
Let's see how the solution attempt changes if we treat the implication truth table as:
$$\begin{matrix}
  p&q&p\implies q&\overline{(p\implies q)}\\
  0&0&?&?\\
  0&1&?&?\\
  1&0&0&1\\
  1&1&1&0
\end{matrix}$$
instead of:
$$\begin{matrix}
  p&q&p\implies q&\overline{(p\implies q)}\\
  0&0&1&0\\
  0&1&1&0\\
  1&0&0&1\\
  1&1&1&0
\end{matrix}$$
We do this because when $p=0$, we can have no confirmation about whether the rule (if $p$ then $q$) holds, so we can't infer anything about the Spy/Knave status of the statement maker and the statement hearer.


*

*Assume $A=1$ and $B=1$

*From (1a) and (1b): $F=1$ and $C=0$

*From (2): $\overline{D} \implies E$

*(3) is irrelevant as $A=1$

*Assume $D=0$ then $E=1$

*From (4): $0=1+0$ is a contradiction

*Assume instead $D=1$ then $E=0$ or $E=1$

*If $E=0$, (4) leads to contradiction again, so assume $E=1$

*From (4): $1=1+0$


This gets us a solution. $A$, $B$, $D$, $E$ and $F$ are the spies and $C$ is the Knave.
Now we try for other values of $A$ and $B$:


*

*Assume $A=0$ and $B=0$

*From (1a) and (1b): $F=0$ and $C=1$

*From (2): $\overline{D}\implies E$

*Assume $D=0$ then $E=1$

*From (3): $\overline{A}\implies \overline{F}$, $F=0$ which is correct

*From (4): $0 = 0 + 1$ is a contradiction

*Assume instead $D=1$ then $E=0$ or $E=1$

*From (3): $F=1$ which is a contradiction, regardless of $E$





*

*Assume $A=0$ and $B=1$

*From (1a) and (1b): $F=0$ and $C=1$

*From (2): $\overline{D}\implies \overline{E}$

*Assume $D=0$ then $E=0$

*From (3): $\overline{A}\implies \overline{F}$, $F=0$ correct

*(4) leads to contradiction.

*Assume instead $D=1$ then $E=0$ or $E=1$

*From (3): $F=1$ which is a contradiction, regardless of $E$


And finally


*

*Assume $A=1$ and $B=0$

*From (1a) and (1b): $F=0$ and $C=1$

*From (2): $\overline{D}\implies E$

*Assume $D=0$ then $E=1$

*(3) is irrelevant here because $A=1$

*From (4): $0 = 0 + 0$


Which gives us another solution. Spies: $A$, $C$ and $E$. Knaves: $B$, $D$, and $F$.


*

*Assume $D=1$ then $E=0$ or $E=1$

*For $E=1$, (4) leads to contradiction, but for $E=0$ we get another solution


Spies: $A$, $C$ and $D$. Knaves: $B$, $E$ and $F$.
All 3 solutions seem to fit the statements.
A: A couple of things about your original translations.
The situation where $A$ says to $B$ that '$F$ is a spy and $C$ is a knave' is different from the situation where $A$ says to $B$ that '$F$ is a spy' and where (on a separate occasion) $A$ says to $B$ that '$C$ is a knave.
That is: $AB = (F \land C')$ is not equivalent to $(AB = F) \land (AB = C')$
So, which one should we use? Interestingly, you write:

$A \text{ says to } B : F \text{ is a Spy, } C \text{ is a Knave.}$

.. which still leaves it a bit ambiguous: what does the comma represent?  That this is one statement by $A$ to $B$, or that there were two occasions here? Let's go with the former, i.e. let's suppose we have:
$AB = FC'$  I note that Alex in his answer used this interpretation as well.
Second, 'either ... or ...' statements certainly feel like exclusive or statements, but there are plenty of occasions where in English we use an 'either ... or ...' statement when we mean an inclusive disjunction, e.g. when I say 'I want to be either rich or happy', I won't complain when I become both rich and happy!
So, what is meant here?  Given that I followed Alex's interpretation on the first statement, and given that he could not find a solution when interpretating this statement as an inclusive or (if you look at his symbolization you'll see that's what he did), I'll agree with you this time and take the exclusive or interpretation, i.e:
$DE = FA + F'A'$
OK, so we have:
$AB = FC'$
$BC = D + E'$
$CD = A+F$
$DE = FA + F'A'$
Now, I'll use a Davis-Putnam like method to see if there are any models for this:
I. Suppose $A=1$.  Then the equations reduce to:
$B = FC'$
$BC = D + E'$
$CD = 1$
$DE = F$
Clearly this means $C=1$ and $D=1$, so reducing with that:
$B = 0$
$BC = 1$
$E = F$
And so $B=0$ and $B=1$. Contradiction.
So, $A=0$. Reduce:
$0 = FC'$
$BC = D + E'$
$CD = F$
$DE = F'$
OK, let's try $F=1$:
$0 = C'$
$BC = D + E'$
$CD = 1$
$DE = 0$
So, $C=1$ and $D=1$:
$B = 1$
$E = 0$
Score! $A=0$, $B = 1$, $C=1$, $D=1$, $E = 0$, and $F=1$
Is it unique? Let's try $F=0$:
$0 = 0$
$BC = D + E'$
$CD = 0$
$DE = 1$
OK, so $D=1$ and $E=1$:
$BC = 1$
$C = 0$
and so $C=1$ and $C=0$. Contradiction.
So yes, we now get a unique solution:
$A$ and $E$ are knaves, and all others are spies.
