============================== prooftrans ============================
Prover9 (64) version 2008-06A, June 2008.
Process 23428 was started by veroff on pengy,
Tue Jul  8 08:19:51 2008
The command was "prover9 -f 5.5.in".
============================== end of head ===========================
op(400,infix,[^,v,"->","=>",*]).
op(200,prefix,[~]).

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

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

% -------- Comments from original proof --------
% Proof 1 at 0.17 (+ 0.01) seconds: "N".
% Length of proof is 34.
% Level of proof is 14.
% Maximum clause weight is 20.
% Given clauses 52.

1 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y # label("N") # label(non_clause) # label(goal).  [goal].
4 x v y = y v x # label("(D3)").  [assumption].
12 x * 1 = x # label("(M1)").  [assumption].
20 ~ x = x => 0 # label("(~ def)").  [assumption].
21 x => 0 = ~ x.  [copy(20),flip(a)].
25 ~ ~ x = x # label("(DN)").  [assumption].
26 ((x => (x => y)) ^ (~ y => (~ y => ~ x))) => (x => y) = 1 # label("(5.6)").  [assumption].
30 x => (y => x) = 1 # label("(3.17)").  [assumption].
31 x => (y => z) = y => (x => z) # label("(3.18)").  [assumption].
33 (x => y) ^ (x => z) = x => (y ^ z) # label("(4.2)").  [assumption].
34 (x * (x => y)) v y = y # label("(4.3)").  [assumption].
35 (x => y) ^ (z => y) = (x v z) => y # label("(4.4)").  [assumption].
37 c1 => c2 != (c1 => (c1 => c2)) ^ (~ c2 => (~ c2 => ~ c1)) # label("N") # answer("N").  [deny(1)].
38 (c1 => (c1 => c2)) ^ (~ c2 => (~ c2 => ~ c1)) != c1 => c2 # answer("N").  [copy(37),flip(a)].
959 x => (y => 0) = y => ~ x.  [para(21(a,1),31(a,1,2)),flip(a)].
967 x => (((x => (x => y)) ^ (~ y => (~ y => ~ x))) => y) = 1.  [para(31(a,1),26(a,1))].
1137 x v (y * (y => x)) = x.  [para(34(a,1),4(a,1)),flip(a)].
1609 (x => y) v (y * 1) = x => y.  [para(30(a,1),1137(a,1,2,2))].
1612 (x => y) v (z * (x => (z => y))) = x => y.  [para(31(a,1),1137(a,1,2,2))].
1691 x => ~ y = y => ~ x.  [para(21(a,1),959(a,1,2))].
1766 ~ x => ~ y = y => x.  [para(25(a,1),1691(a,1,2)),flip(a)].
1912 (x => y) v y = x => y.  [para(12(a,1),1609(a,1,2))].
2020 x v (y => x) = y => x.  [para(1912(a,1),4(a,1)),flip(a)].
2181 (x => y) v (x => (z => y)) = z => (x => y).  [para(31(a,1),2020(a,1,2))].
2752 x => (((x => (x => y)) ^ (~ y => (x => y))) => y) = 1.  [para(1766(a,1),967(a,1,2,1,2,2))].
2911 x => (((x => (x => y)) ^ (x => (~ y => y))) => y) = 1.  [para(31(a,1),2752(a,1,2,1,2))].
3122 x => ((x => ((x => y) ^ (~ y => y))) => y) = 1.  [para(33(a,1),2911(a,1,2,1))].
3330 x => ((x => ((x v ~ y) => y)) => y) = 1.  [para(35(a,1),3122(a,1,2,1,2))].
3539 (x => y) v ((x => ((x v ~ y) => y)) * 1) = x => y.  [para(3330(a,1),1612(a,1,2,2))].
3602 (x => y) v (x => ((x v ~ y) => y)) = x => y.  [para(12(a,1),3539(a,1,2))].
3999 (x v ~ y) => (x => y) = x => y.  [para(3602(a,1),2181(a,1)),flip(a)].
4142 (x => (x => y)) ^ (~ y => (x => y)) = x => y.  [para(3999(a,1),35(a,2))].
4417 (x => (x => y)) ^ (~ y => (~ y => ~ x)) = x => y.  [para(1766(a,2),4142(a,1,2,2))].
4418 $F # answer("N").  [resolve(4417,a,38,a)].

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