%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : NLP145-1 : TPTP v3.4.2. Released v2.4.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 14:43:21 EDT 2009
% Result : Unsatisfiable 6.9s
% Output : Refutation 6.9s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 15
% Syntax : Number of formulae : 45 ( 16 unt; 0 def)
% Number of atoms : 74 ( 0 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 61 ( 32 ~; 29 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 1 prp; 0-4 aty)
% Number of functors : 5 ( 5 usr; 2 con; 0-2 aty)
% Number of variables : 66 ( 12 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(clause88,plain,
! [A] :
( ~ member(skc7,A,skc8)
| fellow(skc7,A) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(165530544,plain,
( ~ member(skc7,A,skc8)
| fellow(skc7,A) ),
inference(rewrite,[status(thm)],[clause88]),
[] ).
fof(clause60,plain,
! [A,B] :
( ~ two(A,B)
| member(A,skf10(B,A),B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(165137880,plain,
( ~ two(A,B)
| member(A,skf10(B,A),B) ),
inference(rewrite,[status(thm)],[clause60]),
[] ).
fof(clause74,plain,
two(skc7,skc8),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(165359424,plain,
two(skc7,skc8),
inference(rewrite,[status(thm)],[clause74]),
[] ).
cnf(241736168,plain,
member(skc7,skf10(skc8,skc7),skc8),
inference(resolution,[status(thm)],[165137880,165359424]),
[] ).
cnf(242861904,plain,
fellow(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[165530544,241736168]),
[] ).
fof(clause14,plain,
! [A,B] :
( ~ man(A,B)
| male(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(164497992,plain,
( ~ man(A,B)
| male(A,B) ),
inference(rewrite,[status(thm)],[clause14]),
[] ).
fof(clause2,plain,
! [A,B] :
( ~ fellow(A,B)
| man(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(164337688,plain,
( ~ fellow(A,B)
| man(A,B) ),
inference(rewrite,[status(thm)],[clause2]),
[] ).
cnf(243191416,plain,
( male(A,B)
| ~ fellow(A,B) ),
inference(resolution,[status(thm)],[164497992,164337688]),
[] ).
cnf(255758976,plain,
male(skc7,skf10(skc8,skc7)),
inference(resolution,[status(thm)],[242861904,243191416]),
[] ).
fof(clause59,plain,
! [A,B,C,D] :
( ~ be(A,B,C,D)
| $equal(D,C) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(165120872,plain,
( ~ be(A,B,C,D)
| $equal(D,C) ),
inference(rewrite,[status(thm)],[clause59]),
[] ).
fof(clause92,plain,
! [A] :
( ~ member(skc7,A,skc8)
| be(skc7,skf6(A),A,skf5(A)) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(165591000,plain,
( ~ member(skc7,A,skc8)
| be(skc7,skf6(A),A,skf5(A)) ),
inference(rewrite,[status(thm)],[clause92]),
[] ).
cnf(242915904,plain,
be(skc7,skf6(skf10(skc8,skc7)),skf10(skc8,skc7),skf5(skf10(skc8,skc7))),
inference(resolution,[status(thm)],[165591000,241736168]),
[] ).
cnf(243013592,plain,
$equal(skf5(skf10(skc8,skc7)),skf10(skc8,skc7)),
inference(resolution,[status(thm)],[165120872,242915904]),
[] ).
fof(clause52,plain,
! [A,B] :
( ~ male(A,B)
| ~ unisex(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(165018776,plain,
( ~ male(A,B)
| ~ unisex(A,B) ),
inference(rewrite,[status(thm)],[clause52]),
[] ).
fof(clause50,plain,
! [A,B] :
( ~ furniture(A,B)
| instrumentality(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(164991976,plain,
( ~ furniture(A,B)
| instrumentality(A,B) ),
inference(rewrite,[status(thm)],[clause50]),
[] ).
fof(clause49,plain,
! [A,B] :
( ~ seat(A,B)
| furniture(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(164974048,plain,
( ~ seat(A,B)
| furniture(A,B) ),
inference(rewrite,[status(thm)],[clause49]),
[] ).
fof(clause48,plain,
! [A,B] :
( ~ frontseat(A,B)
| seat(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(164960144,plain,
( ~ frontseat(A,B)
| seat(A,B) ),
inference(rewrite,[status(thm)],[clause48]),
[] ).
fof(clause89,plain,
! [A,B] :
( ~ member(skc7,A,skc8)
| frontseat(skc7,skf5(B)) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(165546448,plain,
( ~ member(skc7,A,skc8)
| frontseat(skc7,skf5(B)) ),
inference(rewrite,[status(thm)],[clause89]),
[] ).
cnf(242873832,plain,
frontseat(skc7,skf5(A)),
inference(resolution,[status(thm)],[165546448,241736168]),
[] ).
cnf(242938968,plain,
seat(skc7,skf5(A)),
inference(resolution,[status(thm)],[164960144,242873832]),
[] ).
cnf(242962272,plain,
furniture(skc7,skf5(A)),
inference(resolution,[status(thm)],[164974048,242938968]),
[] ).
cnf(242976832,plain,
instrumentality(skc7,skf5(A)),
inference(resolution,[status(thm)],[164991976,242962272]),
[] ).
fof(clause30,plain,
! [A,B] :
( ~ instrumentality(A,B)
| artifact(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(164716000,plain,
( ~ instrumentality(A,B)
| artifact(A,B) ),
inference(rewrite,[status(thm)],[clause30]),
[] ).
cnf(244022848,plain,
artifact(skc7,skf5(A)),
inference(resolution,[status(thm)],[242976832,164716000]),
[] ).
fof(clause31,plain,
! [A,B] :
( ~ artifact(A,B)
| object(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(164734376,plain,
( ~ artifact(A,B)
| object(A,B) ),
inference(rewrite,[status(thm)],[clause31]),
[] ).
cnf(244031584,plain,
object(skc7,skf5(A)),
inference(resolution,[status(thm)],[244022848,164734376]),
[] ).
fof(clause35,plain,
! [A,B] :
( ~ object(A,B)
| unisex(A,B) ),
file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),
[] ).
cnf(164782920,plain,
( ~ object(A,B)
| unisex(A,B) ),
inference(rewrite,[status(thm)],[clause35]),
[] ).
cnf(244072184,plain,
unisex(skc7,skf5(A)),
inference(resolution,[status(thm)],[244031584,164782920]),
[] ).
cnf(245147344,plain,
~ male(skc7,skf5(A)),
inference(resolution,[status(thm)],[165018776,244072184]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__paramodulation,[status(thm)],[255758976,243013592,245147344,theory(equality)]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 7 seconds
% START OF PROOF SEQUENCE
% fof(clause88,plain,(~member(skc7,A,skc8)|fellow(skc7,A)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(165530544,plain,(~member(skc7,A,skc8)|fellow(skc7,A)),inference(rewrite,[status(thm)],[clause88]),[]).
%
% fof(clause60,plain,(~two(A,B)|member(A,skf10(B,A),B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(165137880,plain,(~two(A,B)|member(A,skf10(B,A),B)),inference(rewrite,[status(thm)],[clause60]),[]).
%
% fof(clause74,plain,(two(skc7,skc8)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(165359424,plain,(two(skc7,skc8)),inference(rewrite,[status(thm)],[clause74]),[]).
%
% cnf(241736168,plain,(member(skc7,skf10(skc8,skc7),skc8)),inference(resolution,[status(thm)],[165137880,165359424]),[]).
%
% cnf(242861904,plain,(fellow(skc7,skf10(skc8,skc7))),inference(resolution,[status(thm)],[165530544,241736168]),[]).
%
% fof(clause14,plain,(~man(A,B)|male(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(164497992,plain,(~man(A,B)|male(A,B)),inference(rewrite,[status(thm)],[clause14]),[]).
%
% fof(clause2,plain,(~fellow(A,B)|man(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(164337688,plain,(~fellow(A,B)|man(A,B)),inference(rewrite,[status(thm)],[clause2]),[]).
%
% cnf(243191416,plain,(male(A,B)|~fellow(A,B)),inference(resolution,[status(thm)],[164497992,164337688]),[]).
%
% cnf(255758976,plain,(male(skc7,skf10(skc8,skc7))),inference(resolution,[status(thm)],[242861904,243191416]),[]).
%
% fof(clause59,plain,(~be(A,B,C,D)|$equal(D,C)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(165120872,plain,(~be(A,B,C,D)|$equal(D,C)),inference(rewrite,[status(thm)],[clause59]),[]).
%
% fof(clause92,plain,(~member(skc7,A,skc8)|be(skc7,skf6(A),A,skf5(A))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(165591000,plain,(~member(skc7,A,skc8)|be(skc7,skf6(A),A,skf5(A))),inference(rewrite,[status(thm)],[clause92]),[]).
%
% cnf(242915904,plain,(be(skc7,skf6(skf10(skc8,skc7)),skf10(skc8,skc7),skf5(skf10(skc8,skc7)))),inference(resolution,[status(thm)],[165591000,241736168]),[]).
%
% cnf(243013592,plain,($equal(skf5(skf10(skc8,skc7)),skf10(skc8,skc7))),inference(resolution,[status(thm)],[165120872,242915904]),[]).
%
% fof(clause52,plain,(~male(A,B)|~unisex(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(165018776,plain,(~male(A,B)|~unisex(A,B)),inference(rewrite,[status(thm)],[clause52]),[]).
%
% fof(clause50,plain,(~furniture(A,B)|instrumentality(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(164991976,plain,(~furniture(A,B)|instrumentality(A,B)),inference(rewrite,[status(thm)],[clause50]),[]).
%
% fof(clause49,plain,(~seat(A,B)|furniture(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(164974048,plain,(~seat(A,B)|furniture(A,B)),inference(rewrite,[status(thm)],[clause49]),[]).
%
% fof(clause48,plain,(~frontseat(A,B)|seat(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(164960144,plain,(~frontseat(A,B)|seat(A,B)),inference(rewrite,[status(thm)],[clause48]),[]).
%
% fof(clause89,plain,(~member(skc7,A,skc8)|frontseat(skc7,skf5(B))),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(165546448,plain,(~member(skc7,A,skc8)|frontseat(skc7,skf5(B))),inference(rewrite,[status(thm)],[clause89]),[]).
%
% cnf(242873832,plain,(frontseat(skc7,skf5(A))),inference(resolution,[status(thm)],[165546448,241736168]),[]).
%
% cnf(242938968,plain,(seat(skc7,skf5(A))),inference(resolution,[status(thm)],[164960144,242873832]),[]).
%
% cnf(242962272,plain,(furniture(skc7,skf5(A))),inference(resolution,[status(thm)],[164974048,242938968]),[]).
%
% cnf(242976832,plain,(instrumentality(skc7,skf5(A))),inference(resolution,[status(thm)],[164991976,242962272]),[]).
%
% fof(clause30,plain,(~instrumentality(A,B)|artifact(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(164716000,plain,(~instrumentality(A,B)|artifact(A,B)),inference(rewrite,[status(thm)],[clause30]),[]).
%
% cnf(244022848,plain,(artifact(skc7,skf5(A))),inference(resolution,[status(thm)],[242976832,164716000]),[]).
%
% fof(clause31,plain,(~artifact(A,B)|object(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(164734376,plain,(~artifact(A,B)|object(A,B)),inference(rewrite,[status(thm)],[clause31]),[]).
%
% cnf(244031584,plain,(object(skc7,skf5(A))),inference(resolution,[status(thm)],[244022848,164734376]),[]).
%
% fof(clause35,plain,(~object(A,B)|unisex(A,B)),file('/home/graph/tptp/TSTP/PreparedTPTP/tptp---none/NLP/NLP145-1.tptp',unknown),[]).
%
% cnf(164782920,plain,(~object(A,B)|unisex(A,B)),inference(rewrite,[status(thm)],[clause35]),[]).
%
% cnf(244072184,plain,(unisex(skc7,skf5(A))),inference(resolution,[status(thm)],[244031584,164782920]),[]).
%
% cnf(245147344,plain,(~male(skc7,skf5(A))),inference(resolution,[status(thm)],[165018776,244072184]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__paramodulation,[status(thm)],[255758976,243013592,245147344,theory(equality)]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------