;;;; Rules and problems based on the Logic theorist


(index-brules '((<- (theorem (or (not (or ?a ?a)) ?a)))
		(<- (theorem (or (not ?a) (or ?b ?a))))
		(<- (theorem (or (not (or ?a ?b)) (or ?b ?a))))
		(<- (theorem (or (not (or ?a (or ?b ?c)))(or ?b (or ?a ?c)))))
		(<- (theorem (or (not (or (not ?a) ?b)) (or (not (or ?c ?a))(or ?c ?b)))))
		(<- (theorem ?x) (theorem (or (not ?y) ?x)) (theorem ?y))
		(<- (theorem (or (not ?x) ?z))
		    (theorem (or (not ?y) ?z)) (theorem (or (not ?x) ?y)))))

(defun replace-implies (a)
  (cond ((not (consp a)) a)
	((eq (first a) 'implies)
	 `(or (not ,(replace-implies (second a))) ,(replace-implies (third a))))
	(T (cons (replace-implies (first a))
		 (replace-implies (rest a))))))
(setf lt-problems
      '((implies (implies p (not p)) (not p))
	(implies q (implies p q))
	(implies (implies p (not q))(implies q (not p)))
	(implies (implies p (implies q r))(implies q (implies p r)))
	(implies (implies q r)(implies (implies p q)(implies p r)))
	(implies (implies p q) (implies (implies q r)(implies p r)))
	(implies p (or p p))
	(implies p p)
	(or (not p) p)
	(or p (not p))
	(implies p (not (not p)))
	(or p (not (not (not p))))
	(implies (not (not p)) p)
	(implies (implies (not p) q)(implies (not q) p))
	(implies (implies p q)(implies (not q)(not p)))
	(implies (implies (not q)(not p))(implies p q))
	(implies (implies (not p) p) p)
	(implies p (or p q))
	(implies (not p) (implies p q))
	(implies p (implies (not p) q))
	(or p (implies (or p q) q))
	(or (not p) (implies (implies p q) q))
	(implies p (implies (implies p q) q))
	(implies (or p (or q r))(or p (or r q)))
	(implies (or p (or q r))(or (or p q) r))
	(implies (or (or p q) r)(or p (or q r)))
	(implies (implies q r)(implies (or p q)(or r p)))
	(implies (implies q r)(implies (or q p)(or p r)))
	(implies (implies q r)(implies (or q p)(or r p)))
	(implies (or p (or p q)) (or p q))
	(implies (or q (or p q)) (or p q))
	(implies (or (not p)(implies p q)) (implies p q))
	(implies (implies p (implies p q)) (implies p q))
	(implies (not (or p q))(not p))
	(implies (not (or p q))(not q))
	(implies (not (or p q))(or (not p) q))
	(implies (not (or p q))(or p (not q)))
	(implies (not (or p q))(or (not p) (not q)))
	(implies (not (implies p q))(implies (not p) q))
	(implies (not (implies p q))(implies p (not q)))
	(implies (not (implies p q))(implies (not p)(not q)))
	(implies (not (implies p q))(implies q p))
	(implies (or p q)(implies (not p) q))
	(implies (implies (not p) q) (or p q))
	(implies (not p) (implies (or p q) q))
	(implies (not q) (implies (or p q) p))
	(implies (not p)(implies q (implies (implies p q) q)))
	(implies (implies p q)(implies (implies (not p) q) q))
	(implies (or p q)(implies (implies p q) q))
	(implies (implies p q)(implies (or p q) q))
	(implies (or p q) (implies (or (not p) q) q))
	(implies (or p q)(implies (or p (not q)) p))))

(setf lt-problems (mapcar #'(lambda (problem) (list 'theorem (replace-implies problem)))
			  lt-problems))

; Thirty problems solvable within a depth limit of 3 on chaining rules together
(setf lt-problems-depth3 (mapcar #'(lambda (i) (elt lt-problems (1- i)))
			   '(1 2 3 4 5 6 7 8 9 10 11 18 19 20 21 22 23 24 25 26 27 28 31 44 46 47 48 49 51 52)))