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

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

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

% -------- Comments from original proof --------
% Proof 1 at 0.03 (+ 0.01) seconds: "(N5)".
% Length of proof is 13.
% Level of proof is 8.
% Maximum clause weight is 17.
% Given clauses 48.

1 (x -> y) ^ (x -> z) = x -> (y ^ z) # label("(N5)") # label(non_clause) # label(goal).  [goal].
5 x ^ y = y ^ x # label("(D4)").  [assumption].
20 x -> y = x => (x => y) # label("(-> def)").  [assumption].
21 x => (x => y) = x -> y.  [copy(20),flip(a)].
37 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)").  [assumption].
48 (c1 -> c2) ^ (c1 -> c3) != c1 -> (c2 ^ c3) # label("(N5)") # answer("(N5)").  [deny(1)].
430 x => ((x => y) ^ z) = (x -> y) ^ (x => z).  [para(21(a,1),37(a,1,1)),flip(a)].
708 x => (y ^ (x => z)) = (x -> z) ^ (x => y).  [para(5(a,1),430(a,1,2))].
803 x => ((x => y) ^ (x => z)) = (x -> z) ^ (x -> y).  [para(21(a,1),708(a,2,2))].
908 x => (x => (y ^ z)) = (x -> z) ^ (x -> y).  [para(37(a,1),803(a,1,2))].
960 (x -> y) ^ (x -> z) = x -> (z ^ y).  [para(908(a,1),21(a,1))].
1011 (x -> y) ^ (x -> z) = x -> (y ^ z).  [para(960(a,1),5(a,1)),flip(a)].
1012 $F # answer("(N5)").  [resolve(1011,a,48,a)].

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