;; ============================== prooftrans ============================ ;; Prover9 (32) version June-2007, June 2007. ;; Process 26909 was started by mccune on rhea, ;; Thu Jun 14 14:03:55 2007 ;; The command was "prover9 -f example.in". ;; ============================== end of head =========================== ;; BEGINNING OF PROOF OBJECT ( (3 (input) (p (a)) NIL) (4 (input) (or (not (p v0)) (q v0)) NIL) (8 (instantiate 4 ((v0 . (a)))) (or (not (p (a))) (q (a))) NIL) (5 (resolve 3 () 8 (1)) (q (a)) NIL) (6 (input) (not (q (a))) NIL) (7 (resolve 5 () 6 ()) false NIL) ) ;; END OF PROOF OBJECT