%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : LCL086-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:44 EDT 2009
% Result : Unsatisfiable 0.6s
% Output : Refutation 0.6s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 3
% Syntax : Number of formulae : 29 ( 17 unt; 0 def)
% Number of atoms : 44 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 32 ( 17 ~; 15 |; 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 : 81 ( 30 sgn 7 !; 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/LCL086-1.tptp',unknown),
[] ).
cnf(145914168,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/LCL086-1.tptp',unknown),
[] ).
cnf(145905264,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/LCL086-1.tptp',unknown),
[] ).
cnf(145910216,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(153739880,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)],[145905264,145910216]),
[] ).
cnf(153720208,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)],[145905264,145910216]),
[] ).
cnf(154148912,plain,
( ~ is_a_theorem(implies(implies(A,B),implies(C,D)))
| ~ is_a_theorem(E)
| is_a_theorem(implies(implies(D,A),implies(C,A))) ),
inference(resolution,[status(thm)],[153720208,145905264]),
[] ).
cnf(156223912,plain,
is_a_theorem(implies(implies(implies(implies(E,B),implies(D,B)),implies(B,C)),implies(A,implies(B,C)))),
inference(resolution,[status(thm)],[154148912,145910216]),
[] ).
cnf(158018344,plain,
( ~ is_a_theorem(implies(implies(implies(E,B),implies(D,B)),implies(B,C)))
| is_a_theorem(implies(A,implies(B,C))) ),
inference(resolution,[status(thm)],[145905264,156223912]),
[] ).
cnf(158093064,plain,
is_a_theorem(implies(A,implies(implies(C,B),implies(B,implies(C,B))))),
inference(resolution,[status(thm)],[158018344,156223912]),
[] ).
cnf(158424440,plain,
is_a_theorem(implies(implies(G,F),implies(F,implies(G,F)))),
inference(resolution,[status(thm)],[153739880,158093064]),
[] ).
cnf(158509128,plain,
is_a_theorem(implies(C,implies(implies(implies(A,B),A),implies(B,A)))),
inference(resolution,[status(thm)],[153720208,158424440]),
[] ).
cnf(158705376,plain,
is_a_theorem(implies(implies(implies(F,G),F),implies(G,F))),
inference(resolution,[status(thm)],[153739880,158509128]),
[] ).
cnf(158754960,plain,
( ~ is_a_theorem(implies(implies(F,G),F))
| is_a_theorem(implies(G,F)) ),
inference(resolution,[status(thm)],[145905264,158705376]),
[] ).
cnf(158855880,plain,
is_a_theorem(implies(F,implies(F,F))),
inference(resolution,[status(thm)],[158754960,158705376]),
[] ).
cnf(158940896,plain,
( ~ is_a_theorem(implies(implies(G,implies(G,G)),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[145905264,158855880]),
[] ).
cnf(158773328,plain,
( ~ is_a_theorem(implies(implies(implies(implies(G,H),G),implies(H,G)),A))
| is_a_theorem(A) ),
inference(resolution,[status(thm)],[145905264,158705376]),
[] ).
cnf(158907576,plain,
is_a_theorem(implies(G,implies(F,implies(H,F)))),
inference(resolution,[status(thm)],[158773328,156223912]),
[] ).
cnf(159080232,plain,
( ~ is_a_theorem(A)
| is_a_theorem(implies(G,implies(H,G))) ),
inference(resolution,[status(thm)],[145905264,158907576]),
[] ).
cnf(159121328,plain,
is_a_theorem(implies(F,implies(G,F))),
inference(resolution,[status(thm)],[159080232,158855880]),
[] ).
cnf(159335304,plain,
is_a_theorem(implies(D,implies(implies(implies(A,B),A),implies(C,A)))),
inference(resolution,[status(thm)],[153720208,159121328]),
[] ).
cnf(161537504,plain,
is_a_theorem(implies(implies(implies(G,H),G),implies(I,G))),
inference(resolution,[status(thm)],[158940896,159335304]),
[] ).
cnf(161634728,plain,
( ~ is_a_theorem(implies(implies(G,H),G))
| is_a_theorem(implies(I,G)) ),
inference(resolution,[status(thm)],[145905264,161537504]),
[] ).
cnf(161716088,plain,
is_a_theorem(implies(H,implies(G,G))),
inference(resolution,[status(thm)],[161634728,158705376]),
[] ).
cnf(161794488,plain,
( ~ is_a_theorem(A)
| is_a_theorem(implies(H,H)) ),
inference(resolution,[status(thm)],[145905264,161716088]),
[] ).
cnf(161852040,plain,
is_a_theorem(implies(G,G)),
inference(resolution,[status(thm)],[161794488,158855880]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[145914168,161852040]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 1 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/LCL086-1.tptp',unknown),[]).
%
% cnf(145914168,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/LCL086-1.tptp',unknown),[]).
%
% cnf(145905264,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/LCL086-1.tptp',unknown),[]).
%
% cnf(145910216,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(153739880,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)],[145905264,145910216]),[]).
%
% cnf(153720208,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)],[145905264,145910216]),[]).
%
% cnf(154148912,plain,(~is_a_theorem(implies(implies(A,B),implies(C,D)))|~is_a_theorem(E)|is_a_theorem(implies(implies(D,A),implies(C,A)))),inference(resolution,[status(thm)],[153720208,145905264]),[]).
%
% cnf(156223912,plain,(is_a_theorem(implies(implies(implies(implies(E,B),implies(D,B)),implies(B,C)),implies(A,implies(B,C))))),inference(resolution,[status(thm)],[154148912,145910216]),[]).
%
% cnf(158018344,plain,(~is_a_theorem(implies(implies(implies(E,B),implies(D,B)),implies(B,C)))|is_a_theorem(implies(A,implies(B,C)))),inference(resolution,[status(thm)],[145905264,156223912]),[]).
%
% cnf(158093064,plain,(is_a_theorem(implies(A,implies(implies(C,B),implies(B,implies(C,B)))))),inference(resolution,[status(thm)],[158018344,156223912]),[]).
%
% cnf(158424440,plain,(is_a_theorem(implies(implies(G,F),implies(F,implies(G,F))))),inference(resolution,[status(thm)],[153739880,158093064]),[]).
%
% cnf(158509128,plain,(is_a_theorem(implies(C,implies(implies(implies(A,B),A),implies(B,A))))),inference(resolution,[status(thm)],[153720208,158424440]),[]).
%
% cnf(158705376,plain,(is_a_theorem(implies(implies(implies(F,G),F),implies(G,F)))),inference(resolution,[status(thm)],[153739880,158509128]),[]).
%
% cnf(158754960,plain,(~is_a_theorem(implies(implies(F,G),F))|is_a_theorem(implies(G,F))),inference(resolution,[status(thm)],[145905264,158705376]),[]).
%
% cnf(158855880,plain,(is_a_theorem(implies(F,implies(F,F)))),inference(resolution,[status(thm)],[158754960,158705376]),[]).
%
% cnf(158940896,plain,(~is_a_theorem(implies(implies(G,implies(G,G)),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[145905264,158855880]),[]).
%
% cnf(158773328,plain,(~is_a_theorem(implies(implies(implies(implies(G,H),G),implies(H,G)),A))|is_a_theorem(A)),inference(resolution,[status(thm)],[145905264,158705376]),[]).
%
% cnf(158907576,plain,(is_a_theorem(implies(G,implies(F,implies(H,F))))),inference(resolution,[status(thm)],[158773328,156223912]),[]).
%
% cnf(159080232,plain,(~is_a_theorem(A)|is_a_theorem(implies(G,implies(H,G)))),inference(resolution,[status(thm)],[145905264,158907576]),[]).
%
% cnf(159121328,plain,(is_a_theorem(implies(F,implies(G,F)))),inference(resolution,[status(thm)],[159080232,158855880]),[]).
%
% cnf(159335304,plain,(is_a_theorem(implies(D,implies(implies(implies(A,B),A),implies(C,A))))),inference(resolution,[status(thm)],[153720208,159121328]),[]).
%
% cnf(161537504,plain,(is_a_theorem(implies(implies(implies(G,H),G),implies(I,G)))),inference(resolution,[status(thm)],[158940896,159335304]),[]).
%
% cnf(161634728,plain,(~is_a_theorem(implies(implies(G,H),G))|is_a_theorem(implies(I,G))),inference(resolution,[status(thm)],[145905264,161537504]),[]).
%
% cnf(161716088,plain,(is_a_theorem(implies(H,implies(G,G)))),inference(resolution,[status(thm)],[161634728,158705376]),[]).
%
% cnf(161794488,plain,(~is_a_theorem(A)|is_a_theorem(implies(H,H))),inference(resolution,[status(thm)],[145905264,161716088]),[]).
%
% cnf(161852040,plain,(is_a_theorem(implies(G,G))),inference(resolution,[status(thm)],[161794488,158855880]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[145914168,161852040]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------