============================== prooftrans (BV) =======================
Prover9 (64) version Aug-2007, Aug 2007.
Process 26302 was started by veroff on titan,
Sat Jan 19 14:19:03 2008
The command was "prover9 -f 4.7.in".
============================== end of head ===========================
op(400,infix,[^,v,"->","=>",*]).
op(200,prefix,[~,-]).

============================== end of input ==========================

============================== PROOF =================================

% -------- Comments from original proof --------
% Proof 1 at 0.02 (+ 0.01) seconds: "(N3)".
% Length of proof is 12.
% Level of proof is 5.
% Maximum clause weight is 13.
% Given clauses 46.

1 (x -> y) ^ (~ x v y) = ~ x v y # label("(N3)") # label(non_clause) # label(goal).  [goal].
15 (x * y) => z = x => (y => z) # label("(P)").  [assumption].
20 x -> y = x => (x => y) # label("(-> def)").  [assumption].
21 x => (x => y) = x -> y.  [copy(20),flip(a)].
41 (x => y) ^ y = y # label("(3.13)").  [assumption].
46 x -> (~ x v y) = x -> y # label("(4.10)").  [assumption].
49 ~ c1 v c2 != (c1 -> c2) ^ (~ c1 v c2) # label("(N3)") # answer("(N3)").  [deny(1)].
50 (c1 -> c2) ^ (~ c1 v c2) != ~ c1 v c2 # answer("(N3)").  [copy(49),flip(a)].
143 (x * x) => y = x -> y.  [para(21(a,1),15(a,2))].
778 (x -> y) ^ y = y.  [para(143(a,1),41(a,1,1))].
795 (x -> y) ^ (~ x v y) = ~ x v y.  [para(46(a,1),778(a,1,1))].
796 $F # answer("(N3)").  [resolve(795,a,50,a)].

============================== end of proof ==========================