%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : LCL087-1 : TPTP v3.4.2. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art03.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 1003MB
% OS : Linux 2.6.17-1.2142_FC4
% CPULimit : 600s
% DateTime : Wed May 6 13:41:45 EDT 2009
% Result : Unsatisfiable 2.0s
% Output : Refutation 2.0s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 3
% Syntax : Number of formulae : 24 ( 14 unt; 0 def)
% Number of atoms : 36 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 26 ( 14 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 1 usr; 1 prp; 0-1 aty)
% Number of functors : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 71 ( 25 sgn 7 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(prove_ic_2,plain,
~ is_a_theorem(implies(a,implies(b,a))),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL087-1.tptp',unknown),
[] ).
cnf(141406272,plain,
~ is_a_theorem(implies(a,implies(b,a))),
inference(rewrite,[status(thm)],[prove_ic_2]),
[] ).
fof(condensed_detachment,plain,
! [A,B] :
( ~ is_a_theorem(implies(A,B))
| ~ is_a_theorem(A)
| is_a_theorem(B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL087-1.tptp',unknown),
[] ).
cnf(141397288,plain,
( ~ is_a_theorem(implies(A,B))
| ~ is_a_theorem(A)
| is_a_theorem(B) ),
inference(rewrite,[status(thm)],[condensed_detachment]),
[] ).
fof(ic_JLukasiewicz_4,plain,
! [A,B,C,D,E] : is_a_theorem(implies(implies(implies(A,B),implies(C,D)),implies(E,implies(implies(D,A),implies(C,A))))),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL087-1.tptp',unknown),
[] ).
cnf(141402272,plain,
is_a_theorem(implies(implies(implies(A,B),implies(C,D)),implies(E,implies(implies(D,A),implies(C,A))))),
inference(rewrite,[status(thm)],[ic_JLukasiewicz_4]),
[] ).
cnf(149221592,plain,
( ~ is_a_theorem(implies(implies(A,B),implies(C,D)))
| is_a_theorem(implies(E,implies(implies(D,A),implies(C,A)))) ),
inference(resolution,[status(thm)],[141397288,141402272]),
[] ).
cnf(149241296,plain,
( ~ is_a_theorem(implies(implies(implies(implies(B,C),implies(D,E)),implies(F,implies(implies(E,B),implies(D,B)))),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[141397288,141402272]),
[] ).
cnf(149993384,plain,
is_a_theorem(implies(B,implies(implies(implies(implies(F,C),implies(E,C)),implies(C,D)),implies(A,implies(C,D))))),
inference(resolution,[status(thm)],[149221592,141402272]),
[] ).
cnf(151563216,plain,
is_a_theorem(implies(implies(implies(implies(J,G),implies(I,G)),implies(G,H)),implies(F,implies(G,H)))),
inference(resolution,[status(thm)],[149241296,149993384]),
[] ).
cnf(151582144,plain,
( ~ is_a_theorem(implies(implies(implies(J,G),implies(I,G)),implies(G,H)))
| is_a_theorem(implies(F,implies(G,H))) ),
inference(resolution,[status(thm)],[141397288,151563216]),
[] ).
cnf(151677408,plain,
is_a_theorem(implies(F,implies(implies(M,G),implies(G,implies(M,G))))),
inference(resolution,[status(thm)],[151582144,151563216]),
[] ).
cnf(151944224,plain,
( ~ is_a_theorem(A)
| is_a_theorem(implies(implies(M,G),implies(G,implies(M,G)))) ),
inference(resolution,[status(thm)],[141397288,151677408]),
[] ).
cnf(152021400,plain,
is_a_theorem(implies(implies(L,F),implies(F,implies(L,F)))),
inference(resolution,[status(thm)],[151944224,141402272]),
[] ).
cnf(152096680,plain,
is_a_theorem(implies(C,implies(implies(implies(A,B),A),implies(B,A)))),
inference(resolution,[status(thm)],[149221592,152021400]),
[] ).
cnf(152227976,plain,
( ~ is_a_theorem(A)
| is_a_theorem(implies(implies(implies(B,C),B),implies(C,B))) ),
inference(resolution,[status(thm)],[141397288,152096680]),
[] ).
cnf(152321864,plain,
is_a_theorem(implies(implies(implies(A,B),A),implies(B,A))),
inference(resolution,[status(thm)],[152227976,141402272]),
[] ).
cnf(152371184,plain,
( ~ is_a_theorem(implies(implies(implies(implies(B,C),B),implies(C,B)),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[141397288,152321864]),
[] ).
cnf(152501360,plain,
is_a_theorem(implies(G,implies(A,implies(H,A)))),
inference(resolution,[status(thm)],[152371184,151563216]),
[] ).
cnf(152676352,plain,
( ~ is_a_theorem(A)
| is_a_theorem(implies(B,implies(H,B))) ),
inference(resolution,[status(thm)],[141397288,152501360]),
[] ).
cnf(152352800,plain,
( ~ is_a_theorem(implies(implies(A,B),A))
| is_a_theorem(implies(B,A)) ),
inference(resolution,[status(thm)],[141397288,152321864]),
[] ).
cnf(152453728,plain,
is_a_theorem(implies(A,implies(A,A))),
inference(resolution,[status(thm)],[152352800,152321864]),
[] ).
cnf(152717352,plain,
is_a_theorem(implies(A,implies(G,A))),
inference(resolution,[status(thm)],[152676352,152453728]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[141406272,152717352]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 2 seconds
% START OF PROOF SEQUENCE
% fof(prove_ic_2,plain,(~is_a_theorem(implies(a,implies(b,a)))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL087-1.tptp',unknown),[]).
%
% cnf(141406272,plain,(~is_a_theorem(implies(a,implies(b,a)))),inference(rewrite,[status(thm)],[prove_ic_2]),[]).
%
% fof(condensed_detachment,plain,(~is_a_theorem(implies(A,B))|~is_a_theorem(A)|is_a_theorem(B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL087-1.tptp',unknown),[]).
%
% cnf(141397288,plain,(~is_a_theorem(implies(A,B))|~is_a_theorem(A)|is_a_theorem(B)),inference(rewrite,[status(thm)],[condensed_detachment]),[]).
%
% fof(ic_JLukasiewicz_4,plain,(is_a_theorem(implies(implies(implies(A,B),implies(C,D)),implies(E,implies(implies(D,A),implies(C,A)))))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL087-1.tptp',unknown),[]).
%
% cnf(141402272,plain,(is_a_theorem(implies(implies(implies(A,B),implies(C,D)),implies(E,implies(implies(D,A),implies(C,A)))))),inference(rewrite,[status(thm)],[ic_JLukasiewicz_4]),[]).
%
% cnf(149221592,plain,(~is_a_theorem(implies(implies(A,B),implies(C,D)))|is_a_theorem(implies(E,implies(implies(D,A),implies(C,A))))),inference(resolution,[status(thm)],[141397288,141402272]),[]).
%
% cnf(149241296,plain,(~is_a_theorem(implies(implies(implies(implies(B,C),implies(D,E)),implies(F,implies(implies(E,B),implies(D,B)))),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[141397288,141402272]),[]).
%
% cnf(149993384,plain,(is_a_theorem(implies(B,implies(implies(implies(implies(F,C),implies(E,C)),implies(C,D)),implies(A,implies(C,D)))))),inference(resolution,[status(thm)],[149221592,141402272]),[]).
%
% cnf(151563216,plain,(is_a_theorem(implies(implies(implies(implies(J,G),implies(I,G)),implies(G,H)),implies(F,implies(G,H))))),inference(resolution,[status(thm)],[149241296,149993384]),[]).
%
% cnf(151582144,plain,(~is_a_theorem(implies(implies(implies(J,G),implies(I,G)),implies(G,H)))|is_a_theorem(implies(F,implies(G,H)))),inference(resolution,[status(thm)],[141397288,151563216]),[]).
%
% cnf(151677408,plain,(is_a_theorem(implies(F,implies(implies(M,G),implies(G,implies(M,G)))))),inference(resolution,[status(thm)],[151582144,151563216]),[]).
%
% cnf(151944224,plain,(~is_a_theorem(A)|is_a_theorem(implies(implies(M,G),implies(G,implies(M,G))))),inference(resolution,[status(thm)],[141397288,151677408]),[]).
%
% cnf(152021400,plain,(is_a_theorem(implies(implies(L,F),implies(F,implies(L,F))))),inference(resolution,[status(thm)],[151944224,141402272]),[]).
%
% cnf(152096680,plain,(is_a_theorem(implies(C,implies(implies(implies(A,B),A),implies(B,A))))),inference(resolution,[status(thm)],[149221592,152021400]),[]).
%
% cnf(152227976,plain,(~is_a_theorem(A)|is_a_theorem(implies(implies(implies(B,C),B),implies(C,B)))),inference(resolution,[status(thm)],[141397288,152096680]),[]).
%
% cnf(152321864,plain,(is_a_theorem(implies(implies(implies(A,B),A),implies(B,A)))),inference(resolution,[status(thm)],[152227976,141402272]),[]).
%
% cnf(152371184,plain,(~is_a_theorem(implies(implies(implies(implies(B,C),B),implies(C,B)),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[141397288,152321864]),[]).
%
% cnf(152501360,plain,(is_a_theorem(implies(G,implies(A,implies(H,A))))),inference(resolution,[status(thm)],[152371184,151563216]),[]).
%
% cnf(152676352,plain,(~is_a_theorem(A)|is_a_theorem(implies(B,implies(H,B)))),inference(resolution,[status(thm)],[141397288,152501360]),[]).
%
% cnf(152352800,plain,(~is_a_theorem(implies(implies(A,B),A))|is_a_theorem(implies(B,A))),inference(resolution,[status(thm)],[141397288,152321864]),[]).
%
% cnf(152453728,plain,(is_a_theorem(implies(A,implies(A,A)))),inference(resolution,[status(thm)],[152352800,152321864]),[]).
%
% cnf(152717352,plain,(is_a_theorem(implies(A,implies(G,A)))),inference(resolution,[status(thm)],[152676352,152453728]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[141406272,152717352]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------