 Let C1and C2 be two clauses. Then, a resolvent obtained by resolution from C1 and C2 is defined as: (a) a binary resolvent of C1 and C2; (b) a binary resolvent of C1 and a factor of C2; (c) a binary resolvent of a factor of C1 and C2; or, (d) a binary resolvent of a factor of C1 and a factor of C2. 