%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : SYN015-2 : TPTP v3.4.2. Released v1.0.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art10.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 16:37:58 EDT 2009
% Result : Unsatisfiable 1.7s
% Output : Refutation 1.7s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 14
% Syntax : Number of formulae : 53 ( 22 unt; 0 def)
% Number of atoms : 112 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 107 ( 48 ~; 59 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 3 con; 0-1 aty)
% Number of variables : 38 ( 0 sgn 17 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(c_23,plain,
equalish(m,k),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(148105024,plain,
equalish(m,k),
inference(rewrite,[status(thm)],[c_23]),
[] ).
fof(element_substitution1,plain,
! [A,B,C] :
( ~ equalish(A,B)
| ~ element(C,A)
| element(C,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147934176,plain,
( ~ equalish(A,B)
| ~ element(C,A)
| element(C,B) ),
inference(rewrite,[status(thm)],[element_substitution1]),
[] ).
fof(c_8,plain,
! [A] :
( element(f(A),A)
| ~ element(A,m)
| equalish(A,m) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147995032,plain,
( element(f(A),A)
| ~ element(A,m)
| equalish(A,m) ),
inference(rewrite,[status(thm)],[c_8]),
[] ).
fof(symmetry,plain,
! [A,B] :
( ~ equalish(A,B)
| equalish(B,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147921120,plain,
( ~ equalish(A,B)
| equalish(B,A) ),
inference(rewrite,[status(thm)],[symmetry]),
[] ).
cnf(208433360,plain,
equalish(k,m),
inference(resolution,[status(thm)],[147921120,148105024]),
[] ).
cnf(210879208,plain,
( ~ element(A,k)
| element(A,m) ),
inference(resolution,[status(thm)],[147934176,208433360]),
[] ).
fof(c_16,plain,
! [A] :
( ~ equalish(A,n)
| element(A,k)
| equalish(A,k) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(148069144,plain,
( ~ equalish(A,n)
| element(A,k)
| equalish(A,k) ),
inference(rewrite,[status(thm)],[c_16]),
[] ).
fof(reflexivity,plain,
! [A] : equalish(A,A),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147914560,plain,
equalish(A,A),
inference(rewrite,[status(thm)],[reflexivity]),
[] ).
cnf(208418296,plain,
( element(n,k)
| equalish(n,k) ),
inference(resolution,[status(thm)],[148069144,147914560]),
[] ).
fof(c_20,plain,
~ equalish(n,k),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147911936,plain,
~ equalish(n,k),
inference(rewrite,[status(thm)],[c_20]),
[] ).
cnf(209348248,plain,
element(n,k),
inference(resolution,[status(thm)],[208418296,147911936]),
[] ).
cnf(211304936,plain,
element(n,m),
inference(resolution,[status(thm)],[210879208,209348248]),
[] ).
cnf(213596288,plain,
( element(f(n),n)
| equalish(n,m) ),
inference(resolution,[status(thm)],[147995032,211304936]),
[] ).
fof(c_7,plain,
! [A] :
( element(A,f(A))
| ~ element(A,m)
| equalish(A,m) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147983584,plain,
( element(A,f(A))
| ~ element(A,m)
| equalish(A,m) ),
inference(rewrite,[status(thm)],[c_7]),
[] ).
cnf(211921152,plain,
( element(n,f(n))
| equalish(n,m) ),
inference(resolution,[status(thm)],[147983584,211304936]),
[] ).
fof(c_9,plain,
! [A,B] :
( ~ element(A,B)
| ~ element(B,A)
| equalish(A,B)
| equalish(A,m)
| element(B,m)
| equalish(B,m) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(148006320,plain,
( ~ element(A,B)
| ~ element(B,A)
| equalish(A,B)
| equalish(A,m)
| element(B,m)
| equalish(B,m) ),
inference(rewrite,[status(thm)],[c_9]),
[] ).
fof(c_6,plain,
! [A] :
( ~ equalish(f(A),A)
| ~ element(A,m)
| equalish(A,m) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147975760,plain,
( ~ equalish(f(A),A)
| ~ element(A,m)
| equalish(A,m) ),
inference(rewrite,[status(thm)],[c_6]),
[] ).
fof(c_19,plain,
~ equalish(m,n),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(148085632,plain,
~ equalish(m,n),
inference(rewrite,[status(thm)],[c_19]),
[] ).
cnf(208626912,plain,
~ equalish(n,m),
inference(resolution,[status(thm)],[147921120,148085632]),
[] ).
cnf(216349464,plain,
~ equalish(f(n),n),
inference(forward_subsumption_resolution__resolution,[status(thm)],[211304936,147975760,208626912]),
[] ).
cnf(217071280,plain,
~ equalish(n,f(n)),
inference(resolution,[status(thm)],[147921120,216349464]),
[] ).
cnf(217426864,plain,
( equalish(n,m)
| element(f(n),m)
| equalish(f(n),m) ),
inference(forward_subsumption_resolution__resolution,[status(thm)],[213596288,211921152,148006320,217071280]),
[] ).
cnf(211925776,plain,
element(n,f(n)),
inference(forward_subsumption_resolution__resolution,[status(thm)],[211304936,147983584,208626912]),
[] ).
cnf(212162104,plain,
( ~ equalish(f(n),A)
| element(n,A) ),
inference(resolution,[status(thm)],[211925776,147934176]),
[] ).
fof(c_5,plain,
! [A] :
( ~ equalish(f(A),m)
| ~ element(A,m)
| equalish(A,m) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147968216,plain,
( ~ equalish(f(A),m)
| ~ element(A,m)
| equalish(A,m) ),
inference(rewrite,[status(thm)],[c_5]),
[] ).
cnf(216337432,plain,
~ equalish(f(n),m),
inference(forward_subsumption_resolution__resolution,[status(thm)],[212162104,147968216,208626912]),
[] ).
cnf(217453512,plain,
( equalish(n,m)
| element(f(n),m) ),
inference(resolution,[status(thm)],[217426864,216337432]),
[] ).
cnf(217464512,plain,
element(f(n),m),
inference(resolution,[status(thm)],[217453512,208626912]),
[] ).
cnf(219340640,plain,
( ~ equalish(m,A)
| element(f(n),A) ),
inference(resolution,[status(thm)],[147934176,217464512]),
[] ).
fof(c_17,plain,
! [A] :
( ~ element(A,k)
| equalish(A,n)
| equalish(A,m)
| equalish(A,k) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(148077896,plain,
( ~ element(A,k)
| equalish(A,n)
| equalish(A,m)
| equalish(A,k) ),
inference(rewrite,[status(thm)],[c_17]),
[] ).
cnf(216863400,plain,
( ~ element(f(n),k)
| equalish(f(n),n)
| equalish(f(n),k) ),
inference(resolution,[status(thm)],[148077896,216337432]),
[] ).
cnf(217103080,plain,
( ~ element(f(n),k)
| equalish(f(n),k) ),
inference(resolution,[status(thm)],[216863400,216349464]),
[] ).
fof(transitivity,plain,
! [A,B,C] :
( ~ equalish(A,B)
| ~ equalish(B,C)
| equalish(A,C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),
[] ).
cnf(147927792,plain,
( ~ equalish(A,B)
| ~ equalish(B,C)
| equalish(A,C) ),
inference(rewrite,[status(thm)],[transitivity]),
[] ).
cnf(208466000,plain,
( ~ equalish(k,A)
| equalish(m,A) ),
inference(resolution,[status(thm)],[147927792,148105024]),
[] ).
cnf(216768288,plain,
~ equalish(m,f(n)),
inference(resolution,[status(thm)],[147921120,216337432]),
[] ).
cnf(217625112,plain,
~ equalish(k,f(n)),
inference(resolution,[status(thm)],[208466000,216768288]),
[] ).
cnf(217861472,plain,
~ equalish(f(n),k),
inference(resolution,[status(thm)],[147921120,217625112]),
[] ).
cnf(218019896,plain,
~ element(f(n),k),
inference(resolution,[status(thm)],[217103080,217861472]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[148105024,219340640,218019896]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 2 seconds
% START OF PROOF SEQUENCE
% fof(c_23,plain,(equalish(m,k)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(148105024,plain,(equalish(m,k)),inference(rewrite,[status(thm)],[c_23]),[]).
%
% fof(element_substitution1,plain,(~equalish(A,B)|~element(C,A)|element(C,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147934176,plain,(~equalish(A,B)|~element(C,A)|element(C,B)),inference(rewrite,[status(thm)],[element_substitution1]),[]).
%
% fof(c_8,plain,(element(f(A),A)|~element(A,m)|equalish(A,m)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147995032,plain,(element(f(A),A)|~element(A,m)|equalish(A,m)),inference(rewrite,[status(thm)],[c_8]),[]).
%
% fof(symmetry,plain,(~equalish(A,B)|equalish(B,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147921120,plain,(~equalish(A,B)|equalish(B,A)),inference(rewrite,[status(thm)],[symmetry]),[]).
%
% cnf(208433360,plain,(equalish(k,m)),inference(resolution,[status(thm)],[147921120,148105024]),[]).
%
% cnf(210879208,plain,(~element(A,k)|element(A,m)),inference(resolution,[status(thm)],[147934176,208433360]),[]).
%
% fof(c_16,plain,(~equalish(A,n)|element(A,k)|equalish(A,k)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(148069144,plain,(~equalish(A,n)|element(A,k)|equalish(A,k)),inference(rewrite,[status(thm)],[c_16]),[]).
%
% fof(reflexivity,plain,(equalish(A,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147914560,plain,(equalish(A,A)),inference(rewrite,[status(thm)],[reflexivity]),[]).
%
% cnf(208418296,plain,(element(n,k)|equalish(n,k)),inference(resolution,[status(thm)],[148069144,147914560]),[]).
%
% fof(c_20,plain,(~equalish(n,k)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147911936,plain,(~equalish(n,k)),inference(rewrite,[status(thm)],[c_20]),[]).
%
% cnf(209348248,plain,(element(n,k)),inference(resolution,[status(thm)],[208418296,147911936]),[]).
%
% cnf(211304936,plain,(element(n,m)),inference(resolution,[status(thm)],[210879208,209348248]),[]).
%
% cnf(213596288,plain,(element(f(n),n)|equalish(n,m)),inference(resolution,[status(thm)],[147995032,211304936]),[]).
%
% fof(c_7,plain,(element(A,f(A))|~element(A,m)|equalish(A,m)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147983584,plain,(element(A,f(A))|~element(A,m)|equalish(A,m)),inference(rewrite,[status(thm)],[c_7]),[]).
%
% cnf(211921152,plain,(element(n,f(n))|equalish(n,m)),inference(resolution,[status(thm)],[147983584,211304936]),[]).
%
% fof(c_9,plain,(~element(A,B)|~element(B,A)|equalish(A,B)|equalish(A,m)|element(B,m)|equalish(B,m)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(148006320,plain,(~element(A,B)|~element(B,A)|equalish(A,B)|equalish(A,m)|element(B,m)|equalish(B,m)),inference(rewrite,[status(thm)],[c_9]),[]).
%
% fof(c_6,plain,(~equalish(f(A),A)|~element(A,m)|equalish(A,m)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147975760,plain,(~equalish(f(A),A)|~element(A,m)|equalish(A,m)),inference(rewrite,[status(thm)],[c_6]),[]).
%
% fof(c_19,plain,(~equalish(m,n)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(148085632,plain,(~equalish(m,n)),inference(rewrite,[status(thm)],[c_19]),[]).
%
% cnf(208626912,plain,(~equalish(n,m)),inference(resolution,[status(thm)],[147921120,148085632]),[]).
%
% cnf(216349464,plain,(~equalish(f(n),n)),inference(forward_subsumption_resolution__resolution,[status(thm)],[211304936,147975760,208626912]),[]).
%
% cnf(217071280,plain,(~equalish(n,f(n))),inference(resolution,[status(thm)],[147921120,216349464]),[]).
%
% cnf(217426864,plain,(equalish(n,m)|element(f(n),m)|equalish(f(n),m)),inference(forward_subsumption_resolution__resolution,[status(thm)],[213596288,211921152,148006320,217071280]),[]).
%
% cnf(211925776,plain,(element(n,f(n))),inference(forward_subsumption_resolution__resolution,[status(thm)],[211304936,147983584,208626912]),[]).
%
% cnf(212162104,plain,(~equalish(f(n),A)|element(n,A)),inference(resolution,[status(thm)],[211925776,147934176]),[]).
%
% fof(c_5,plain,(~equalish(f(A),m)|~element(A,m)|equalish(A,m)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147968216,plain,(~equalish(f(A),m)|~element(A,m)|equalish(A,m)),inference(rewrite,[status(thm)],[c_5]),[]).
%
% cnf(216337432,plain,(~equalish(f(n),m)),inference(forward_subsumption_resolution__resolution,[status(thm)],[212162104,147968216,208626912]),[]).
%
% cnf(217453512,plain,(equalish(n,m)|element(f(n),m)),inference(resolution,[status(thm)],[217426864,216337432]),[]).
%
% cnf(217464512,plain,(element(f(n),m)),inference(resolution,[status(thm)],[217453512,208626912]),[]).
%
% cnf(219340640,plain,(~equalish(m,A)|element(f(n),A)),inference(resolution,[status(thm)],[147934176,217464512]),[]).
%
% fof(c_17,plain,(~element(A,k)|equalish(A,n)|equalish(A,m)|equalish(A,k)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(148077896,plain,(~element(A,k)|equalish(A,n)|equalish(A,m)|equalish(A,k)),inference(rewrite,[status(thm)],[c_17]),[]).
%
% cnf(216863400,plain,(~element(f(n),k)|equalish(f(n),n)|equalish(f(n),k)),inference(resolution,[status(thm)],[148077896,216337432]),[]).
%
% cnf(217103080,plain,(~element(f(n),k)|equalish(f(n),k)),inference(resolution,[status(thm)],[216863400,216349464]),[]).
%
% fof(transitivity,plain,(~equalish(A,B)|~equalish(B,C)|equalish(A,C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/SYN/SYN015-2.tptp',unknown),[]).
%
% cnf(147927792,plain,(~equalish(A,B)|~equalish(B,C)|equalish(A,C)),inference(rewrite,[status(thm)],[transitivity]),[]).
%
% cnf(208466000,plain,(~equalish(k,A)|equalish(m,A)),inference(resolution,[status(thm)],[147927792,148105024]),[]).
%
% cnf(216768288,plain,(~equalish(m,f(n))),inference(resolution,[status(thm)],[147921120,216337432]),[]).
%
% cnf(217625112,plain,(~equalish(k,f(n))),inference(resolution,[status(thm)],[208466000,216768288]),[]).
%
% cnf(217861472,plain,(~equalish(f(n),k)),inference(resolution,[status(thm)],[147921120,217625112]),[]).
%
% cnf(218019896,plain,(~element(f(n),k)),inference(resolution,[status(thm)],[217103080,217861472]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[148105024,219340640,218019896]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------