(note TQG23)  ;; boolean version

;; Deep transitive reasoning.  Vampire typically requires about 75
;; steps to construct a proof.

(time 1200)

(instance Human23-1 Human)
(instance Human23-2 Human)
(instance Human23-3 Human)
(instance Human23-4 Human)
(instance Human23-5 Human)
(instance Human23-6 Human)
(instance Human23-7 Human)
(instance Human23-8 Human)
(instance Human23-9 Human)
(instance Human23-10 Human)
(instance Human23-11 Human)
(instance Human23-12 Human)
(instance Human23-13 Human)
(instance Human23-14 Human)
(instance Human23-15 Human)
(instance Human23-16 Human)
(ancestor Human23-1 Human23-2)
(ancestor Human23-2 Human23-3)
(ancestor Human23-3 Human23-4)
(ancestor Human23-4 Human23-5)
(ancestor Human23-5 Human23-6)
(ancestor Human23-6 Human23-7)
(ancestor Human23-7 Human23-8)
(ancestor Human23-8 Human23-9)
(ancestor Human23-9 Human23-10)
(ancestor Human23-10 Human23-11)
(ancestor Human23-11 Human23-12)
(ancestor Human23-12 Human23-13)
(ancestor Human23-13 Human23-14)
(ancestor Human23-14 Human23-15)
(ancestor Human23-14 Human23-16)

(query (and 
         (ancestor Human23-1 Human23-15) 
         (ancestor Human23-1 Human23-16)))

(answer yes)

;; Fails after 1200 seconds.

;; (solutionAxiom (subclass Human Organism))

;; (solutionAxiom
;;   (forall (?INST1 ?INST2 ?INST3) 
;;     (=> 
;;       (and 
;;         (instance ?INST2 Organism) 
;;         (instance ?INST1 Organism) 
;;         (instance ?INST3 Organism)) 
;;       (=> 
;;         (and 
;;           (ancestor ?INST1 ?INST2) 
;;           (ancestor ?INST2 ?INST3)) 
;;         (ancestor ?INST1 ?INST3)))))