A tough logic puzzle I took a course on logic a few semesters ago so am having trouble remembering certian concepts. I came across another problem in one of my classes yesterday and am not sure how to solve it exactly. Could I use resolution to solve the following
A, B, C, D, and E all live in a house together.


*

*If A is at home then so is B

*Either D or E, or both are at home

*Either B or C, but not both are home

*D and C are either both at home or both not at home

*If E is at home then A and D are also at home


The question asks, who's at home and who isn't?
If I remember correctly, resolution is used when we want to determine if an argument is valid. If the conjunction of the premises and negated conclusion leads to a contradiction (an empty set), then the argument is valid. However, this isn't that type of question. I tried using it and ended up with the following clauses
$$D \vee \neg E$$
$$B \vee D$$
This can't be resolved further. So either I made a mistake or we can't use resolution here. How else could this problem be solved?
Thanks for the help
EDIT
Here's what my resolution looked like
I converted the statements into clauses
$$\neg A \vee B$$
$$D \vee E$$
$$B \vee C$$
$$\neg B \vee \neg C$$
$$\neg D \vee C$$
$$\neg C \vee D$$
$$\neg E \vee A$$
$$\neg E \vee D$$
 A: Either $E$ or $\neg E$. If $E$ then $A\land D$, hence $B\land C$, a contradiction. On the other hand $\neg E$ implies $D$, then $C$, then $\neg B$, then $\neg A$. Since this truth assignment for $A,B,C,D,E$ is compatible with the givens it follows that only $C$ and $D$ are at home.
A: You must have made an oversight.  We can show D is home.  If E is home, by 5 so is D.  If E is not home, by 2 D is.  Then 4 tells us C is home.  3 tells us B is not.  1 tells us A is not.  Then 5 tells us E is not.  
A mechanical approach would be a truth table, though it has $32$ lines.  Make one and see which of your clues come out true for each line.  There should be only one line where they all come out true.  If there is more than one, you can cite that to show the puzzle is flawed.  
Edit:  it appears you missed the inference that $(D \vee \lnot E) \wedge (D \vee E)\implies D\vee (E \wedge \lnot E) \implies D$
A: I use Polish notation.  The clauses now read as follows:


*

*ANab

*Ade

*Abc

*ANbNc

*ANdc

*ANcd

*ANea

*ANed


To prove any member of {a, Na, b, Nb, c, Nc, d, Nd, e, Ne} we can assume it's complement C.  Then if we deduce a contradiction by resolution, the complement of C will have gotten proved.
To show that we can't deduce any member of the above set with 8 members requires more work.  We can basically show that we can only deduce a certain number of formulas by resolution and then indicate that such a set of formulas doesn't have any instance of $\alpha$ and N$\alpha$.  Consequently, that formula can't get deduced.
For an example of the latter, let's assume that Na holds.
Assumption 9 Na

Only 7 has 'a' as one of it's disjuncts, and thus we can only deduce 'Ne' so far.
9, 7      10 Ne

Now only 2 has 'e' as one of it's disjuncts, and thus the only new formula we can deduce is 'd'.
10, 2     11 d

Only 5 has 'Nd' as one of it's disjuncts, and thus the only new formula we can deduce is 'c'.
11, 5     12 c

Now both 4 and 6 have 'Nc' as one of their disjuncts.  But 12, 6 yields 'd' which we have in our set of derived formulas so far.  But, we can derive 'Nb' as a new formula.
12, 4     13 Nb

Now, 1, and 3 have 'b' as one of their disjuncts.  But, 13, 1 as well as 13, 3 yield a formula already in our set of derived formulas.  Thus, given Na, we can only derive formulas in the set {Na, Ne, d, c, Nb}.  We don't have a literal and it's complement there, and thus we can't deduce a contradiction.  Therefore, 'a' is not provable here.
Here's an example of proving one of the eight formulas.
assumption 14 a
1, 14      15 b
4, 15      16 Nc
5, 16      17 Nd
17, 2      18 e
17, 8      19 Ne
18, 19     20 {}

Thus, since 'a' leads to a contradiction, 'Na' holds true.  And we have a bonus of sorts.  Since 'Na' holds true, the above disproof of 'a' as true tells us all five formulas which hold here.
In other words, A is not at home, E is not at home, d is at home, c is at home, and B is not at home.
A: You have 5 variables to start with, however,

3. Either B or C, but not both are home
4. D and C are either both at home or both not at home


These allow you to assume $B = \lnot C$ and $D = C$, so you can reduce the problem to 3 variables, $A, C, E$.

1. If A is at home then so is B
2. Either D or E, or both are at home
5. If E is at home then A and D are also at home


$$(A \implies B) \land (D \lor E) \land (E \implies (A \land D))$$
Becomes
$$(A \implies \lnot C) \land (C \lor E) \land (E \implies (A \land C))$$
Now there are only 8 cases left over.  For this formula it is easier to exclude cases 1 clause at a time:
$(A \implies \lnot C)$ excludes $\{T, T, T\}$ and $\{T, T, F\}$.
$(C \lor E)$ excludes $\{T, F, F\}$ and $\{F, F, F\}$.
$E \implies (A \land C)$ excludes $\{T, F, T\}$ and $\{F, T, T\}$ and $\{F, F, T\}$.
That excludes 7 cases, the only remaining case is $\{F, T, F\}$, so

$$A = \text{False}, B = \lnot C, C = \text{True}, D = C, E = \text{False}$$

However, this was a special case of proposition that can be reduced from 5 variables to 3 variables.  In general, there is no known technique for checking propositions faster than just checking every single case.
