%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : LCL082-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:35 EDT 2009
% Result : Unsatisfiable 11.0s
% Output : Refutation 11.0s
% Verified :
% SZS Type : Refutation
% Derivation depth : 22
% Number of leaves : 3
% Syntax : Number of formulae : 30 ( 21 unt; 0 def)
% Number of atoms : 41 ( 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 : 88 ( 35 sgn 6 !; 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/LCL082-1.tptp',unknown),
[] ).
cnf(156496360,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/LCL082-1.tptp',unknown),
[] ).
cnf(156487512,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/LCL082-1.tptp',unknown),
[] ).
cnf(156492368,plain,
is_a_theorem(implies(implies(implies(A,B),C),implies(implies(C,A),implies(D,A)))),
inference(rewrite,[status(thm)],[ic_JLukasiewicz]),
[] ).
cnf(164316488,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)],[156487512,156492368]),
[] ).
cnf(164296824,plain,
( ~ is_a_theorem(implies(implies(A,B),C))
| is_a_theorem(implies(implies(C,A),implies(D,A))) ),
inference(resolution,[status(thm)],[156487512,156492368]),
[] ).
cnf(164676352,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)],[164296824,156492368]),
[] ).
cnf(167598088,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)],[164676352,156487512]),
[] ).
cnf(168548120,plain,
is_a_theorem(implies(D,implies(implies(C,B),implies(B,implies(C,B))))),
inference(resolution,[status(thm)],[167598088,164676352]),
[] ).
cnf(168609680,plain,
is_a_theorem(implies(implies(G,F),implies(F,implies(G,F)))),
inference(resolution,[status(thm)],[164316488,168548120]),
[] ).
cnf(168651456,plain,
( ~ is_a_theorem(implies(implies(implies(H,G),implies(G,implies(H,G))),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[156487512,168609680]),
[] ).
cnf(168671432,plain,
is_a_theorem(implies(implies(implies(B,implies(A,B)),A),implies(C,A))),
inference(resolution,[status(thm)],[164296824,168609680]),
[] ).
cnf(168806888,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)],[164296824,168671432]),
[] ).
cnf(169734280,plain,
is_a_theorem(implies(G,implies(F,implies(F,F)))),
inference(resolution,[status(thm)],[168651456,168806888]),
[] ).
cnf(169860904,plain,
is_a_theorem(implies(implies(implies(I,implies(I,I)),A),implies(C,A))),
inference(resolution,[status(thm)],[164296824,169734280]),
[] ).
cnf(170234736,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)],[156487512,169860904]),
[] ).
cnf(170406336,plain,
is_a_theorem(implies(H,implies(implies(G,G),implies(I,implies(G,G))))),
inference(resolution,[status(thm)],[170234736,164676352]),
[] ).
cnf(170502288,plain,
is_a_theorem(implies(implies(K,K),implies(L,implies(K,K)))),
inference(resolution,[status(thm)],[164316488,170406336]),
[] ).
cnf(170614800,plain,
( ~ is_a_theorem(implies(implies(implies(L,L),implies(M,implies(L,L))),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[156487512,170502288]),
[] ).
cnf(170635816,plain,
is_a_theorem(implies(implies(implies(M,implies(A,A)),A),implies(B,A))),
inference(resolution,[status(thm)],[164296824,170502288]),
[] ).
cnf(170998976,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)],[164296824,170635816]),
[] ).
cnf(189618192,plain,
is_a_theorem(implies(M,implies(L,implies(K,K)))),
inference(resolution,[status(thm)],[170614800,170998976]),
[] ).
cnf(189883080,plain,
is_a_theorem(implies(P,implies(O,O))),
inference(resolution,[status(thm)],[164316488,189618192]),
[] ).
cnf(190176816,plain,
is_a_theorem(implies(implies(implies(R,R),A),implies(C,A))),
inference(resolution,[status(thm)],[164296824,189883080]),
[] ).
cnf(190967144,plain,
( ~ is_a_theorem(implies(implies(implies(implies(S,S),B),implies(D,B)),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[156487512,190176816]),
[] ).
cnf(191146496,plain,
is_a_theorem(implies(Q,implies(B,implies(R,B)))),
inference(resolution,[status(thm)],[190967144,164676352]),
[] ).
cnf(191326344,plain,
is_a_theorem(implies(F,implies(U,F))),
inference(resolution,[status(thm)],[164316488,191146496]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[156496360,191326344]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 10 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/LCL082-1.tptp',unknown),[]).
%
% cnf(156496360,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/LCL082-1.tptp',unknown),[]).
%
% cnf(156487512,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/LCL082-1.tptp',unknown),[]).
%
% cnf(156492368,plain,(is_a_theorem(implies(implies(implies(A,B),C),implies(implies(C,A),implies(D,A))))),inference(rewrite,[status(thm)],[ic_JLukasiewicz]),[]).
%
% cnf(164316488,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)],[156487512,156492368]),[]).
%
% cnf(164296824,plain,(~is_a_theorem(implies(implies(A,B),C))|is_a_theorem(implies(implies(C,A),implies(D,A)))),inference(resolution,[status(thm)],[156487512,156492368]),[]).
%
% cnf(164676352,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)],[164296824,156492368]),[]).
%
% cnf(167598088,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)],[164676352,156487512]),[]).
%
% cnf(168548120,plain,(is_a_theorem(implies(D,implies(implies(C,B),implies(B,implies(C,B)))))),inference(resolution,[status(thm)],[167598088,164676352]),[]).
%
% cnf(168609680,plain,(is_a_theorem(implies(implies(G,F),implies(F,implies(G,F))))),inference(resolution,[status(thm)],[164316488,168548120]),[]).
%
% cnf(168651456,plain,(~is_a_theorem(implies(implies(implies(H,G),implies(G,implies(H,G))),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[156487512,168609680]),[]).
%
% cnf(168671432,plain,(is_a_theorem(implies(implies(implies(B,implies(A,B)),A),implies(C,A)))),inference(resolution,[status(thm)],[164296824,168609680]),[]).
%
% cnf(168806888,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)],[164296824,168671432]),[]).
%
% cnf(169734280,plain,(is_a_theorem(implies(G,implies(F,implies(F,F))))),inference(resolution,[status(thm)],[168651456,168806888]),[]).
%
% cnf(169860904,plain,(is_a_theorem(implies(implies(implies(I,implies(I,I)),A),implies(C,A)))),inference(resolution,[status(thm)],[164296824,169734280]),[]).
%
% cnf(170234736,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)],[156487512,169860904]),[]).
%
% cnf(170406336,plain,(is_a_theorem(implies(H,implies(implies(G,G),implies(I,implies(G,G)))))),inference(resolution,[status(thm)],[170234736,164676352]),[]).
%
% cnf(170502288,plain,(is_a_theorem(implies(implies(K,K),implies(L,implies(K,K))))),inference(resolution,[status(thm)],[164316488,170406336]),[]).
%
% cnf(170614800,plain,(~is_a_theorem(implies(implies(implies(L,L),implies(M,implies(L,L))),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[156487512,170502288]),[]).
%
% cnf(170635816,plain,(is_a_theorem(implies(implies(implies(M,implies(A,A)),A),implies(B,A)))),inference(resolution,[status(thm)],[164296824,170502288]),[]).
%
% cnf(170998976,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)],[164296824,170635816]),[]).
%
% cnf(189618192,plain,(is_a_theorem(implies(M,implies(L,implies(K,K))))),inference(resolution,[status(thm)],[170614800,170998976]),[]).
%
% cnf(189883080,plain,(is_a_theorem(implies(P,implies(O,O)))),inference(resolution,[status(thm)],[164316488,189618192]),[]).
%
% cnf(190176816,plain,(is_a_theorem(implies(implies(implies(R,R),A),implies(C,A)))),inference(resolution,[status(thm)],[164296824,189883080]),[]).
%
% cnf(190967144,plain,(~is_a_theorem(implies(implies(implies(implies(S,S),B),implies(D,B)),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[156487512,190176816]),[]).
%
% cnf(191146496,plain,(is_a_theorem(implies(Q,implies(B,implies(R,B))))),inference(resolution,[status(thm)],[190967144,164676352]),[]).
%
% cnf(191326344,plain,(is_a_theorem(implies(F,implies(U,F)))),inference(resolution,[status(thm)],[164316488,191146496]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[156496360,191326344]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------