- removed duplicate resolvent check with self from OTTER Like theorem prover.

Author: ctjoreilly

src/aima/logic/fol/inference/FOLOTTERLikeTheoremProver.java

@@ -261,15 +261,9 @@ private InferenceResult otter(OTTERAnswerHandler ansHandler,
 	private Set<Clause> infer(Clause clause, Set<Clause> usable) {
 		Set<Clause> resultingClauses = new LinkedHashSet<Clause>();
 
-		// Remember to resolve with self
-		Set<Clause> resolvents = clause.binaryResolvents(clause);
-		for (Clause rc : resolvents) {
-			resultingClauses.add(rc);
-		}
-
 		// * resolve clause with each member of usable
 		for (Clause c : usable) {
-			resolvents = clause.binaryResolvents(c);
+			Set<Clause> resolvents = clause.binaryResolvents(c);
 			for (Clause rc : resolvents) {
 				resultingClauses.add(rc);
 			}