============================== prooftrans (BV) =======================
Prover9 (64) version Aug-2007, Aug 2007.
Process 32412 was started by veroff on io,
Mon Jan 21 11:14:54 2008
The command was "prover9 -f 3.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.00) seconds: "(E2)".
% Length of proof is 12.
% Level of proof is 4.
% Maximum clause weight is 13.
% Given clauses 53.

1 x => (x => (x => y)) = x => (x => y) # label("(E2)") # label(non_clause) # label(goal).  [goal].
33 x -> (x -> y) = x -> y # label("(3.5)").  [assumption].
40 x => y != 1 | y => x != 1 | x = y # label("(BCK4)").  [assumption].
46 x => (x => y) = x -> y # label("(3.15)").  [assumption].
50 x => (y => x) = 1 # label("(3.17)").  [assumption].
52 c1 => (c1 => (c1 => c2)) != c1 => (c1 => c2) # label("(E2)") # answer("(E2)").  [deny(1)].
711 (x => y) => (x -> y) = 1.  [para(46(a,1),50(a,1,2))].
744 c1 => (c1 -> c2) != c1 => (c1 => c2) # answer("(E2)").  [para(46(a,1),52(a,1,2))].
752 (x => (x -> y)) => (x -> y) = 1.  [para(33(a,1),711(a,1,2))].
775 x => (x -> y) = x -> y.  [hyper(40,a,50,a,b,752,a),flip(a)].
871 c1 => (c1 -> c2) != c1 -> c2 # answer("(E2)").  [para(46(a,1),744(a,2))].
872 $F # answer("(E2)").  [resolve(871,a,775,a)].

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