============================== prooftrans (BV) =======================
Prover9 (64) version Aug-2007, Aug 2007.
Process 32341 was started by veroff on io,
Mon Jan 21 11:14:33 2008
The command was "prover9 -f 3.13.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: "(3.19)".
% Length of proof is 11.
% Level of proof is 4.
% Maximum clause weight is 9.
% Given clauses 51.

1 x => 0 = ~ x # label("(3.19)") # label(non_clause) # label(goal).  [goal].
15 ~ ~ x = x # label("(DN)").  [assumption].
16 ~ 1 = 0 # label("(2.2)").  [assumption].
38 1 => x = x # label("(BCK2)").  [assumption].
43 ~ x => ~ y = y => x # label("(3.12)").  [assumption].
54 ~ c1 != c1 => 0 # label("(3.19)") # answer("(3.19)").  [deny(1)].
55 c1 => 0 != ~ c1 # answer("(3.19)").  [copy(54),flip(a)].
600 ~ x => ~ 1 = x.  [para(38(a,1),43(a,2))].
829 ~ x => 0 = x.  [para(16(a,1),600(a,1,2))].
844 x => 0 = ~ x.  [para(15(a,1),829(a,1,1))].
845 $F # answer("(3.19)").  [resolve(844,a,55,a)].

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