Propositional logic problem : with Resolution

Question

I have given the following problem:

Family Smith plans to buy a car, a moped and a washing machine next year. However, if Mrs Smith fails to receive an incentive on top of her salary the Smiths cannot afford all three of them. The washing machine will be bought in any case. They need at least one motor vehicle, too. If they spend their holiday in Spain they cannot afford the car. If they do not spend their holiday in Spain theyneed to buy the moped in order to conciliate their spoilt son who is slightly mentally unstable.

Model the situation into a formula in propositional logic. Show by using the resolution method that family Smith will buy a moped and not a car if Mrs Smith fails to receive her inventive.

So far i tried the following:

C = Car , M = Moped, W = Wasching machine, S = Salary T = Travel Spain

F = $(\lnot S \rightarrow ((C \lor M)\lor(\lnot C \lor M))) \land((T\rightarrow \lnot C) \lor (\lnot T \rightarrow M))$

Since W will be bought in any case i decide to drop it from F.

So the following questions are: 1. Is this correct? If not what is wrong? 2. How should i proof it with the resolution method?

Answer 1

Hint on how to use Resolution.

With premises :

4) "If they spend their holiday in Spain they cannot afford the car", i.e. $T \to \lnot C$, and

5) "If they do not spend their holiday in Spain they need to buy the moped in order to conciliate their spoilt son who is slightly mentally unstable", i.e. $\lnot T \to M$,

we apply the Resolution rule to get :

6) $\lnot C \lor M$.

Using premise 3) "They need at least one motor vehicle, too", i.e. $C \lor M$, we apply again the rule to get :

7) $M$.

In addition we have premise 2) : "The washing machine will be bought in any case", i.e. $W$.

Up to now we have :

1) "if Mrs Smith fails to receive an incentive on top of her salary the Smiths cannot afford all three of them", i.e. $\lnot S \to \lnot (C \land M \land W)$ i.e.

1) $S \lor \lnot C \lor \lnot M \lor \lnot W$.

2) $W$

7) $M$

and the negation of the sought conclusion :

$\lnot [\lnot S \to (M \land \lnot C)]$,

that splits into :

8) $\lnot S$

and

9) $\lnot M \lor C$.

We have to apply Resolution to 1) with 9) to get :

10) $S \lor \lnot M \lor \lnot W$.

Now the result is straightforward.