1. A ∨ B
2. A → (C ∨ D)
3. (A ∧ D) → C
4. (A ∧ ¬D) → E
5. B → (D ∨ E)
6. ¬(C ∧ D)
7. (C ∨ ¬D) → E
8. E → D
I'll show step 1 for sentence 7.
(C ∨ ¬D) → E, Replace →.
¬(C ∨ ¬D) ∨ E. Move ¬ inside.
(¬C ∧ ¬¬D) ∨ E. Move ¬ inside.
(¬C ∧ D) ∨ E. Distribute ∨ over ∧.
(¬C ∨ E) ∧ (D ∨ E) . Break into two clauses.
{ ¬C ∨ E, D ∨ E} .
Output of step 1:
1. A V B 2. ~A V C V D 3. ~A V ~D V C 4. ~A V D V E 5. ~B V D V E 6. ~C V ~D 7A. ~C V E 7B. D V E 8. ~E V D
Set S0:
1. A V B
2. ~A V C V D
3. ~A V ~D V C
4. ~A V D V E
5. ~B V D V E
6. ~C V ~D
7A. ~C V E
7B. D V E
8. ~E V D
No easy cases. Try A=T. Delete 1. Delete ~A from 2, 3, 4.
Set S1
2. C V D
3. ~D V C
4. D V E
5. ~B V D V E
6. ~C V ~D
7A. ~C V E
7B. D V E
8. ~E V D
B is a pure literal. Set B=F. Delete 5.
2. C V D
3. ~D V C
4. D V E
6. ~C V ~D
7A. ~C V E
7B. D V E
8. ~E V D
No easy cases. Try C=T. Delete 2, 3, delete ~C from 6 and 7A.
Set S2
4. D V E
6. ~D
7A. E
7B. D V E
8. ~E V D
6 and 7 are singleton clauses. Set D=F, E=T. delete 4, 6, 7A, 7B. Delete
~E and D from 8.
8 is the null clause. Backtrack to S1.
Try C=F. Delete 6 and 7A. Delete C from 2 and 3.
Set S3
2. D
3. ~D
4. D V E
7B. D V E
8. ~E V D
2 is a singleton clause. Set D=T. Delete 2, 5, 7B, 8. Delete ~D from 3.
3 is the null clause. Back track to S0.
Try A=F. Delete 2, 3, 4. Delete A from 1.
Set S0:
1. B
5. ~B V D V E
6. ~C V ~D
7A. ~C V E
7B. D V E
8. ~E V D
1 is a singleton clause. Set B=T. Delete ~B from 5.
5. D V E
6. ~C V ~D
7A. ~C V E
7B. D V E
8. ~E V D
~C is a pure literal. Set C=F. Delete 6, 7.
`
5. D V E
7B. D V E
8. ~E V D
D is a pure literal. Set D=T. Delete 5, 7B, 8. Success!
Return: A=F, B=T, C=F, D=T, E is arbitrary.