%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : LCL081-1 : TPTP v3.4.2. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art06.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:30 EDT 2009
% Result : Unsatisfiable 6.3s
% Output : Refutation 6.3s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 3
% Syntax : Number of formulae : 28 ( 19 unt; 0 def)
% Number of atoms : 39 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 24 ( 13 ~; 11 |; 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 : 2 ( 2 usr; 1 con; 0-2 aty)
% Number of variables : 79 ( 31 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(prove_ic_1,plain,
~ is_a_theorem(implies(a,a)),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL081-1.tptp',unknown),
[] ).
cnf(142580448,plain,
~ is_a_theorem(implies(a,a)),
inference(rewrite,[status(thm)],[prove_ic_1]),
[] ).
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/LCL081-1.tptp',unknown),
[] ).
cnf(142571680,plain,
( ~ is_a_theorem(implies(A,B))
| ~ is_a_theorem(A)
| is_a_theorem(B) ),
inference(rewrite,[status(thm)],[condensed_detachment]),
[] ).
fof(ic_JLukasiewicz,plain,
! [A,B,C,D] : is_a_theorem(implies(implies(implies(A,B),C),implies(implies(C,A),implies(D,A)))),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL081-1.tptp',unknown),
[] ).
cnf(142576504,plain,
is_a_theorem(implies(implies(implies(A,B),C),implies(implies(C,A),implies(D,A)))),
inference(rewrite,[status(thm)],[ic_JLukasiewicz]),
[] ).
cnf(150395648,plain,
( ~ is_a_theorem(implies(implies(implies(implies(B,C),D),implies(implies(D,B),implies(E,B))),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[142571680,142576504]),
[] ).
cnf(150376016,plain,
( ~ is_a_theorem(implies(implies(A,B),C))
| is_a_theorem(implies(implies(C,A),implies(D,A))) ),
inference(resolution,[status(thm)],[142571680,142576504]),
[] ).
cnf(150729672,plain,
is_a_theorem(implies(implies(implies(implies(A,C),implies(E,C)),implies(C,D)),implies(B,implies(C,D)))),
inference(resolution,[status(thm)],[150376016,142576504]),
[] ).
cnf(154418816,plain,
( ~ is_a_theorem(implies(implies(implies(implies(implies(A,C),implies(E,C)),implies(C,D)),implies(B,implies(C,D))),F))
| is_a_theorem(F) ),
inference(resolution,[status(thm)],[150729672,142571680]),
[] ).
cnf(155919160,plain,
is_a_theorem(implies(D,implies(implies(C,B),implies(B,implies(C,B))))),
inference(resolution,[status(thm)],[154418816,150729672]),
[] ).
cnf(155980736,plain,
is_a_theorem(implies(implies(G,F),implies(F,implies(G,F)))),
inference(resolution,[status(thm)],[150395648,155919160]),
[] ).
cnf(156017576,plain,
( ~ is_a_theorem(implies(implies(implies(H,G),implies(G,implies(H,G))),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[142571680,155980736]),
[] ).
cnf(156037536,plain,
is_a_theorem(implies(implies(implies(B,implies(A,B)),A),implies(C,A))),
inference(resolution,[status(thm)],[150376016,155980736]),
[] ).
cnf(156172368,plain,
is_a_theorem(implies(implies(implies(D,A),implies(C,implies(A,C))),implies(B,implies(C,implies(A,C))))),
inference(resolution,[status(thm)],[150376016,156037536]),
[] ).
cnf(157093104,plain,
is_a_theorem(implies(G,implies(F,implies(F,F)))),
inference(resolution,[status(thm)],[156017576,156172368]),
[] ).
cnf(157205800,plain,
is_a_theorem(implies(implies(implies(I,implies(I,I)),A),implies(C,A))),
inference(resolution,[status(thm)],[150376016,157093104]),
[] ).
cnf(157583752,plain,
( ~ is_a_theorem(implies(implies(implies(implies(J,implies(J,J)),B),implies(D,B)),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[142571680,157205800]),
[] ).
cnf(157749672,plain,
is_a_theorem(implies(H,implies(implies(G,G),implies(I,implies(G,G))))),
inference(resolution,[status(thm)],[157583752,150729672]),
[] ).
cnf(157836808,plain,
is_a_theorem(implies(implies(K,K),implies(L,implies(K,K)))),
inference(resolution,[status(thm)],[150395648,157749672]),
[] ).
cnf(157962192,plain,
( ~ is_a_theorem(implies(implies(implies(L,L),implies(M,implies(L,L))),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[142571680,157836808]),
[] ).
cnf(157982416,plain,
is_a_theorem(implies(implies(implies(M,implies(A,A)),A),implies(B,A))),
inference(resolution,[status(thm)],[150376016,157836808]),
[] ).
cnf(158332984,plain,
is_a_theorem(implies(implies(implies(C,A),implies(N,implies(A,A))),implies(B,implies(N,implies(A,A))))),
inference(resolution,[status(thm)],[150376016,157982416]),
[] ).
cnf(179191376,plain,
is_a_theorem(implies(M,implies(L,implies(K,K)))),
inference(resolution,[status(thm)],[157962192,158332984]),
[] ).
cnf(179471984,plain,
is_a_theorem(implies(P,implies(O,O))),
inference(resolution,[status(thm)],[150395648,179191376]),
[] ).
cnf(179749888,plain,
( ~ is_a_theorem(A)
| is_a_theorem(implies(P,P)) ),
inference(resolution,[status(thm)],[142571680,179471984]),
[] ).
cnf(179787328,plain,
is_a_theorem(implies(O,O)),
inference(resolution,[status(thm)],[179749888,142576504]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[142580448,179787328]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 6 seconds
% START OF PROOF SEQUENCE
% fof(prove_ic_1,plain,(~is_a_theorem(implies(a,a))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL081-1.tptp',unknown),[]).
%
% cnf(142580448,plain,(~is_a_theorem(implies(a,a))),inference(rewrite,[status(thm)],[prove_ic_1]),[]).
%
% 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/LCL081-1.tptp',unknown),[]).
%
% cnf(142571680,plain,(~is_a_theorem(implies(A,B))|~is_a_theorem(A)|is_a_theorem(B)),inference(rewrite,[status(thm)],[condensed_detachment]),[]).
%
% fof(ic_JLukasiewicz,plain,(is_a_theorem(implies(implies(implies(A,B),C),implies(implies(C,A),implies(D,A))))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL081-1.tptp',unknown),[]).
%
% cnf(142576504,plain,(is_a_theorem(implies(implies(implies(A,B),C),implies(implies(C,A),implies(D,A))))),inference(rewrite,[status(thm)],[ic_JLukasiewicz]),[]).
%
% cnf(150395648,plain,(~is_a_theorem(implies(implies(implies(implies(B,C),D),implies(implies(D,B),implies(E,B))),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[142571680,142576504]),[]).
%
% cnf(150376016,plain,(~is_a_theorem(implies(implies(A,B),C))|is_a_theorem(implies(implies(C,A),implies(D,A)))),inference(resolution,[status(thm)],[142571680,142576504]),[]).
%
% cnf(150729672,plain,(is_a_theorem(implies(implies(implies(implies(A,C),implies(E,C)),implies(C,D)),implies(B,implies(C,D))))),inference(resolution,[status(thm)],[150376016,142576504]),[]).
%
% cnf(154418816,plain,(~is_a_theorem(implies(implies(implies(implies(implies(A,C),implies(E,C)),implies(C,D)),implies(B,implies(C,D))),F))|is_a_theorem(F)),inference(resolution,[status(thm)],[150729672,142571680]),[]).
%
% cnf(155919160,plain,(is_a_theorem(implies(D,implies(implies(C,B),implies(B,implies(C,B)))))),inference(resolution,[status(thm)],[154418816,150729672]),[]).
%
% cnf(155980736,plain,(is_a_theorem(implies(implies(G,F),implies(F,implies(G,F))))),inference(resolution,[status(thm)],[150395648,155919160]),[]).
%
% cnf(156017576,plain,(~is_a_theorem(implies(implies(implies(H,G),implies(G,implies(H,G))),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[142571680,155980736]),[]).
%
% cnf(156037536,plain,(is_a_theorem(implies(implies(implies(B,implies(A,B)),A),implies(C,A)))),inference(resolution,[status(thm)],[150376016,155980736]),[]).
%
% cnf(156172368,plain,(is_a_theorem(implies(implies(implies(D,A),implies(C,implies(A,C))),implies(B,implies(C,implies(A,C)))))),inference(resolution,[status(thm)],[150376016,156037536]),[]).
%
% cnf(157093104,plain,(is_a_theorem(implies(G,implies(F,implies(F,F))))),inference(resolution,[status(thm)],[156017576,156172368]),[]).
%
% cnf(157205800,plain,(is_a_theorem(implies(implies(implies(I,implies(I,I)),A),implies(C,A)))),inference(resolution,[status(thm)],[150376016,157093104]),[]).
%
% cnf(157583752,plain,(~is_a_theorem(implies(implies(implies(implies(J,implies(J,J)),B),implies(D,B)),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[142571680,157205800]),[]).
%
% cnf(157749672,plain,(is_a_theorem(implies(H,implies(implies(G,G),implies(I,implies(G,G)))))),inference(resolution,[status(thm)],[157583752,150729672]),[]).
%
% cnf(157836808,plain,(is_a_theorem(implies(implies(K,K),implies(L,implies(K,K))))),inference(resolution,[status(thm)],[150395648,157749672]),[]).
%
% cnf(157962192,plain,(~is_a_theorem(implies(implies(implies(L,L),implies(M,implies(L,L))),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[142571680,157836808]),[]).
%
% cnf(157982416,plain,(is_a_theorem(implies(implies(implies(M,implies(A,A)),A),implies(B,A)))),inference(resolution,[status(thm)],[150376016,157836808]),[]).
%
% cnf(158332984,plain,(is_a_theorem(implies(implies(implies(C,A),implies(N,implies(A,A))),implies(B,implies(N,implies(A,A)))))),inference(resolution,[status(thm)],[150376016,157982416]),[]).
%
% cnf(179191376,plain,(is_a_theorem(implies(M,implies(L,implies(K,K))))),inference(resolution,[status(thm)],[157962192,158332984]),[]).
%
% cnf(179471984,plain,(is_a_theorem(implies(P,implies(O,O)))),inference(resolution,[status(thm)],[150395648,179191376]),[]).
%
% cnf(179749888,plain,(~is_a_theorem(A)|is_a_theorem(implies(P,P))),inference(resolution,[status(thm)],[142571680,179471984]),[]).
%
% cnf(179787328,plain,(is_a_theorem(implies(O,O))),inference(resolution,[status(thm)],[179749888,142576504]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[142580448,179787328]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------