%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : LCL091-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:53 EDT 2009
% Result : Unsatisfiable 9.6s
% Output : Refutation 9.6s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 3
% Syntax : Number of formulae : 32 ( 23 unt; 0 def)
% Number of atoms : 43 ( 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 : 3 ( 3 usr; 2 con; 0-2 aty)
% Number of variables : 113 ( 60 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/LCL091-1.tptp',unknown),
[] ).
cnf(157253688,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/LCL091-1.tptp',unknown),
[] ).
cnf(157244704,plain,
( ~ is_a_theorem(implies(A,B))
| ~ is_a_theorem(A)
| is_a_theorem(B) ),
inference(rewrite,[status(thm)],[condensed_detachment]),
[] ).
fof(ic_JLukasiewicz_5,plain,
! [A,B,C,D,E] : is_a_theorem(implies(implies(implies(A,B),implies(C,D)),implies(implies(D,A),implies(E,implies(C,A))))),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL091-1.tptp',unknown),
[] ).
cnf(157249688,plain,
is_a_theorem(implies(implies(implies(A,B),implies(C,D)),implies(implies(D,A),implies(E,implies(C,A))))),
inference(rewrite,[status(thm)],[ic_JLukasiewicz_5]),
[] ).
cnf(165082136,plain,
( ~ is_a_theorem(implies(implies(implies(implies(B,C),implies(D,E)),implies(implies(E,B),implies(F,implies(D,B)))),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[157244704,157249688]),
[] ).
cnf(165062464,plain,
( ~ is_a_theorem(implies(implies(A,B),implies(C,D)))
| is_a_theorem(implies(implies(D,A),implies(E,implies(C,A)))) ),
inference(resolution,[status(thm)],[157244704,157249688]),
[] ).
cnf(165866680,plain,
is_a_theorem(implies(implies(implies(F,implies(D,B)),implies(B,C)),implies(A,implies(implies(E,B),implies(B,C))))),
inference(resolution,[status(thm)],[165062464,157249688]),
[] ).
cnf(167744424,plain,
( ~ is_a_theorem(implies(implies(F,implies(D,B)),implies(B,C)))
| is_a_theorem(implies(A,implies(implies(E,B),implies(B,C)))) ),
inference(resolution,[status(thm)],[157244704,165866680]),
[] ).
cnf(167833128,plain,
is_a_theorem(implies(A,implies(implies(D,B),implies(B,implies(implies(F,C),implies(C,B)))))),
inference(resolution,[status(thm)],[167744424,165866680]),
[] ).
cnf(167927920,plain,
is_a_theorem(implies(implies(H,F),implies(F,implies(implies(J,G),implies(G,F))))),
inference(resolution,[status(thm)],[165082136,167833128]),
[] ).
cnf(168022600,plain,
is_a_theorem(implies(implies(implies(implies(K,I),implies(I,B)),A),implies(C,implies(B,A)))),
inference(resolution,[status(thm)],[165062464,167927920]),
[] ).
cnf(168357584,plain,
is_a_theorem(implies(A,implies(implies(D,B),implies(B,implies(E,implies(C,B)))))),
inference(resolution,[status(thm)],[167744424,168022600]),
[] ).
cnf(169550264,plain,
is_a_theorem(implies(implies(H,F),implies(F,implies(I,implies(G,F))))),
inference(resolution,[status(thm)],[165082136,168357584]),
[] ).
cnf(169703416,plain,
is_a_theorem(implies(implies(implies(J,implies(I,B)),A),implies(C,implies(B,A)))),
inference(resolution,[status(thm)],[165062464,169550264]),
[] ).
cnf(170026312,plain,
is_a_theorem(implies(implies(implies(D,A),implies(K,implies(J,D))),implies(C,implies(B,implies(K,implies(J,D)))))),
inference(resolution,[status(thm)],[165062464,169703416]),
[] ).
cnf(191264632,plain,
is_a_theorem(implies(E,implies(D,implies(implies(B,A),implies(C,implies(A,A)))))),
inference(resolution,[status(thm)],[165082136,170026312]),
[] ).
cnf(193294520,plain,
is_a_theorem(implies(I,implies(implies(G,F),implies(H,implies(F,F))))),
inference(resolution,[status(thm)],[165082136,191264632]),
[] ).
cnf(193897856,plain,
is_a_theorem(implies(implies(L,K),implies(M,implies(K,K)))),
inference(resolution,[status(thm)],[165082136,193294520]),
[] ).
cnf(194172176,plain,
( ~ is_a_theorem(implies(implies(implies(M,L),implies(N,implies(L,L))),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[157244704,193897856]),
[] ).
cnf(194470472,plain,
is_a_theorem(implies(N,implies(M,implies(L,implies(K,K))))),
inference(resolution,[status(thm)],[194172176,170026312]),
[] ).
cnf(194619608,plain,
is_a_theorem(implies(R,implies(Q,implies(P,P)))),
inference(resolution,[status(thm)],[165082136,194470472]),
[] ).
cnf(195117696,plain,
( ~ is_a_theorem(A)
| is_a_theorem(implies(R,implies(Q,Q))) ),
inference(resolution,[status(thm)],[157244704,194619608]),
[] ).
cnf(195143760,plain,
is_a_theorem(implies(Q,implies(P,P))),
inference(resolution,[status(thm)],[195117696,157249688]),
[] ).
cnf(195417136,plain,
( ~ is_a_theorem(A)
| is_a_theorem(implies(Q,Q)) ),
inference(resolution,[status(thm)],[157244704,195143760]),
[] ).
cnf(195439120,plain,
is_a_theorem(implies(P,P)),
inference(resolution,[status(thm)],[195417136,195143760]),
[] ).
cnf(195746400,plain,
( ~ is_a_theorem(implies(implies(Q,Q),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[157244704,195439120]),
[] ).
cnf(195908824,plain,
is_a_theorem(implies(Q,implies(P,implies(R,implies(X,R))))),
inference(resolution,[status(thm)],[195746400,170026312]),
[] ).
cnf(197359128,plain,
is_a_theorem(implies(Bf,implies(Bg,implies(Bm,Bg)))),
inference(resolution,[status(thm)],[195746400,195908824]),
[] ).
cnf(197892640,plain,
is_a_theorem(implies(Bv,implies(Cb,Bv))),
inference(resolution,[status(thm)],[195746400,197359128]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[157253688,197892640]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 9 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/LCL091-1.tptp',unknown),[]).
%
% cnf(157253688,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/LCL091-1.tptp',unknown),[]).
%
% cnf(157244704,plain,(~is_a_theorem(implies(A,B))|~is_a_theorem(A)|is_a_theorem(B)),inference(rewrite,[status(thm)],[condensed_detachment]),[]).
%
% fof(ic_JLukasiewicz_5,plain,(is_a_theorem(implies(implies(implies(A,B),implies(C,D)),implies(implies(D,A),implies(E,implies(C,A)))))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/LCL/LCL091-1.tptp',unknown),[]).
%
% cnf(157249688,plain,(is_a_theorem(implies(implies(implies(A,B),implies(C,D)),implies(implies(D,A),implies(E,implies(C,A)))))),inference(rewrite,[status(thm)],[ic_JLukasiewicz_5]),[]).
%
% cnf(165082136,plain,(~is_a_theorem(implies(implies(implies(implies(B,C),implies(D,E)),implies(implies(E,B),implies(F,implies(D,B)))),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[157244704,157249688]),[]).
%
% cnf(165062464,plain,(~is_a_theorem(implies(implies(A,B),implies(C,D)))|is_a_theorem(implies(implies(D,A),implies(E,implies(C,A))))),inference(resolution,[status(thm)],[157244704,157249688]),[]).
%
% cnf(165866680,plain,(is_a_theorem(implies(implies(implies(F,implies(D,B)),implies(B,C)),implies(A,implies(implies(E,B),implies(B,C)))))),inference(resolution,[status(thm)],[165062464,157249688]),[]).
%
% cnf(167744424,plain,(~is_a_theorem(implies(implies(F,implies(D,B)),implies(B,C)))|is_a_theorem(implies(A,implies(implies(E,B),implies(B,C))))),inference(resolution,[status(thm)],[157244704,165866680]),[]).
%
% cnf(167833128,plain,(is_a_theorem(implies(A,implies(implies(D,B),implies(B,implies(implies(F,C),implies(C,B))))))),inference(resolution,[status(thm)],[167744424,165866680]),[]).
%
% cnf(167927920,plain,(is_a_theorem(implies(implies(H,F),implies(F,implies(implies(J,G),implies(G,F)))))),inference(resolution,[status(thm)],[165082136,167833128]),[]).
%
% cnf(168022600,plain,(is_a_theorem(implies(implies(implies(implies(K,I),implies(I,B)),A),implies(C,implies(B,A))))),inference(resolution,[status(thm)],[165062464,167927920]),[]).
%
% cnf(168357584,plain,(is_a_theorem(implies(A,implies(implies(D,B),implies(B,implies(E,implies(C,B))))))),inference(resolution,[status(thm)],[167744424,168022600]),[]).
%
% cnf(169550264,plain,(is_a_theorem(implies(implies(H,F),implies(F,implies(I,implies(G,F)))))),inference(resolution,[status(thm)],[165082136,168357584]),[]).
%
% cnf(169703416,plain,(is_a_theorem(implies(implies(implies(J,implies(I,B)),A),implies(C,implies(B,A))))),inference(resolution,[status(thm)],[165062464,169550264]),[]).
%
% cnf(170026312,plain,(is_a_theorem(implies(implies(implies(D,A),implies(K,implies(J,D))),implies(C,implies(B,implies(K,implies(J,D))))))),inference(resolution,[status(thm)],[165062464,169703416]),[]).
%
% cnf(191264632,plain,(is_a_theorem(implies(E,implies(D,implies(implies(B,A),implies(C,implies(A,A))))))),inference(resolution,[status(thm)],[165082136,170026312]),[]).
%
% cnf(193294520,plain,(is_a_theorem(implies(I,implies(implies(G,F),implies(H,implies(F,F)))))),inference(resolution,[status(thm)],[165082136,191264632]),[]).
%
% cnf(193897856,plain,(is_a_theorem(implies(implies(L,K),implies(M,implies(K,K))))),inference(resolution,[status(thm)],[165082136,193294520]),[]).
%
% cnf(194172176,plain,(~is_a_theorem(implies(implies(implies(M,L),implies(N,implies(L,L))),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[157244704,193897856]),[]).
%
% cnf(194470472,plain,(is_a_theorem(implies(N,implies(M,implies(L,implies(K,K)))))),inference(resolution,[status(thm)],[194172176,170026312]),[]).
%
% cnf(194619608,plain,(is_a_theorem(implies(R,implies(Q,implies(P,P))))),inference(resolution,[status(thm)],[165082136,194470472]),[]).
%
% cnf(195117696,plain,(~is_a_theorem(A)|is_a_theorem(implies(R,implies(Q,Q)))),inference(resolution,[status(thm)],[157244704,194619608]),[]).
%
% cnf(195143760,plain,(is_a_theorem(implies(Q,implies(P,P)))),inference(resolution,[status(thm)],[195117696,157249688]),[]).
%
% cnf(195417136,plain,(~is_a_theorem(A)|is_a_theorem(implies(Q,Q))),inference(resolution,[status(thm)],[157244704,195143760]),[]).
%
% cnf(195439120,plain,(is_a_theorem(implies(P,P))),inference(resolution,[status(thm)],[195417136,195143760]),[]).
%
% cnf(195746400,plain,(~is_a_theorem(implies(implies(Q,Q),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[157244704,195439120]),[]).
%
% cnf(195908824,plain,(is_a_theorem(implies(Q,implies(P,implies(R,implies(X,R)))))),inference(resolution,[status(thm)],[195746400,170026312]),[]).
%
% cnf(197359128,plain,(is_a_theorem(implies(Bf,implies(Bg,implies(Bm,Bg))))),inference(resolution,[status(thm)],[195746400,195908824]),[]).
%
% cnf(197892640,plain,(is_a_theorem(implies(Bv,implies(Cb,Bv)))),inference(resolution,[status(thm)],[195746400,197359128]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[157253688,197892640]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------