============================== prooftrans (BV) =======================
Prover9 (64) version Aug-2007, Aug 2007.
Process 32425 was started by veroff on io,
Mon Jan 21 11:14:57 2008
The command was "prover9 -f 3.9.in".
============================== end of head ===========================
op(400,infix,[^,v,"->","=>",*]).
op(200,prefix,[~,-]).

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

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

% -------- Comments from original proof --------
% Proof 1 at 0.04 (+ 0.00) seconds: "(P)".
% Length of proof is 18.
% Level of proof is 6.
% Maximum clause weight is 15.
% Given clauses 54.

1 (x * y) => z = x => (y => z) # label("(P)") # label(non_clause) # label(goal).  [goal].
13 ~ x v ~ y = ~ (x ^ y) # label("(DM1)").  [assumption].
15 ~ ~ x = x # label("(DN)").  [assumption].
25 x * y = ~ (x -> ~ y) v ~ (y -> ~ x) # label("(* def)").  [assumption].
26 ~ (x -> ~ y) v ~ (y -> ~ x) = x * y.  [copy(25),flip(a)].
27 x => y = (x -> y) ^ (~ y -> ~ x) # label("(=> def)").  [assumption].
28 (x -> y) ^ (~ y -> ~ x) = x => y.  [copy(27),flip(a)].
43 ~ x => ~ y = y => x # label("(3.12)").  [assumption].
51 x => (y => z) = y => (x => z) # label("(3.18)").  [assumption].
53 (c1 * c2) => c3 != c1 => (c2 => c3) # label("(P)") # answer("(P)").  [deny(1)].
288 ~ ((x -> ~ y) ^ (y -> ~ x)) = x * y.  [para(26(a,1),13(a,1)),flip(a)].
309 (x -> ~ y) ^ (y -> ~ x) = x => ~ y.  [para(15(a,1),28(a,1,2,1))].
593 ~ x => y = ~ y => x.  [para(15(a,1),43(a,1,2))].
725 ~ x => (y => ~ z) = y => (z => x).  [para(43(a,1),51(a,1,2)),flip(a)].
931 ~ (x => ~ y) = x * y.  [para(309(a,1),288(a,1,1))].
960 ~ x => (y => ~ z) = (y * z) => x.  [para(931(a,1),593(a,1,1)),flip(a)].
1007 (x * y) => z = x => (y => z).  [para(960(a,1),725(a,1))].
1008 $F # answer("(P)").  [resolve(1007,a,53,a)].

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