The law says that it is a crime for America to sell weapons to hostile nations.

Resolving the negated goal ¬Criminal(West) with the knowledge base gives the empty clause, so West is a criminal.

1. FOPL representation

1. It is a crime for an American to sell weapons to hostile nations:
   \(\forall x,y,z\ \mathrm{American}(x) \wedge \mathrm{Weapon}(y) \wedge \mathrm{Sells}(x,y,z) \wedge \mathrm{Hostile}(z) \rightarrow \mathrm{Criminal}(x)\)
2. Nono has some missiles: \(\exists x\ \mathrm{Owns}(Nono,x) \wedge \mathrm{Missile}(x)\)
3. All of its missiles were sold by West:
   \(\forall x\ \mathrm{Missile}(x) \wedge \mathrm{Owns}(Nono,x) \rightarrow \mathrm{Sells}(West,x,Nono)\)
4. Missiles are weapons: \(\forall x\ \mathrm{Missile}(x) \rightarrow \mathrm{Weapon}(x)\)
5. An enemy of America is hostile: \(\forall x\ \mathrm{Enemy}(x, America) \rightarrow \mathrm{Hostile}(x)\)
6. West is American: \(\mathrm{American}(West)\)
7. Nono is an enemy of America: \(\mathrm{Enemy}(Nono, America)\)

2. Clause form (implications removed; the existential in 2 is replaced by a Skolem constant \(M_1\)):

1. \(\neg\mathrm{American}(x) \vee \neg\mathrm{Weapon}(y) \vee \neg\mathrm{Sells}(x,y,z) \vee \neg\mathrm{Hostile}(z) \vee \mathrm{Criminal}(x)\)
2. \(\mathrm{Owns}(Nono, M_1)\)
3. \(\mathrm{Missile}(M_1)\)
4. \(\neg\mathrm{Missile}(u) \vee \neg\mathrm{Owns}(Nono,u) \vee \mathrm{Sells}(West,u,Nono)\)
5. \(\neg\mathrm{Missile}(v) \vee \mathrm{Weapon}(v)\)
6. \(\neg\mathrm{Enemy}(w, America) \vee \mathrm{Hostile}(w)\)
7. \(\mathrm{American}(West)\)
8. \(\mathrm{Enemy}(Nono, America)\)
9. Negated goal: \(\neg\mathrm{Criminal}(West)\)

3. Resolution proof

• (9) + (1), \(\{x/West\}\): \(\neg\mathrm{American}(West) \vee \neg\mathrm{Weapon}(y) \vee \neg\mathrm{Sells}(West,y,z) \vee \neg\mathrm{Hostile}(z)\)
• + (7): \(\neg\mathrm{Weapon}(y) \vee \neg\mathrm{Sells}(West,y,z) \vee \neg\mathrm{Hostile}(z)\)
• + (5), \(\{v/y\}\): \(\neg\mathrm{Missile}(y) \vee \neg\mathrm{Sells}(West,y,z) \vee \neg\mathrm{Hostile}(z)\)
• + (3), \(\{y/M_1\}\): \(\neg\mathrm{Sells}(West,M_1,z) \vee \neg\mathrm{Hostile}(z)\)
• + (4), \(\{u/M_1, z/Nono\}\): \(\neg\mathrm{Missile}(M_1) \vee \neg\mathrm{Owns}(Nono,M_1) \vee \neg\mathrm{Hostile}(Nono)\)
• + (3): \(\neg\mathrm{Owns}(Nono,M_1) \vee \neg\mathrm{Hostile}(Nono)\)
• + (2): \(\neg\mathrm{Hostile}(Nono)\)
• + (6), \(\{w/Nono\}\): \(\neg\mathrm{Enemy}(Nono, America)\)
• + (8): empty clause \(\square\)

Since assuming "West is not a criminal" leads to a contradiction, Criminal(West) is proved.