%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : CSR050+1 : TPTP v3.4.2. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art09.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 11:42:17 EDT 2009
% Result : Theorem 0.1s
% Output : Refutation 0.1s
% Verified :
% SZS Type : Refutation
% Derivation depth : 6
% Number of leaves : 10
% Syntax : Number of formulae : 33 ( 20 unt; 0 def)
% Number of atoms : 48 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 35 ( 20 ~; 14 |; 1 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 11 con; 0-3 aty)
% Number of variables : 12 ( 0 sgn 6 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(just78,plain,
! [A,B] :
( ~ mtvisible(A)
| ~ genlmt(A,B)
| mtvisible(B) ),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(167186632,plain,
( ~ mtvisible(A)
| ~ genlmt(A,B)
| mtvisible(B) ),
inference(rewrite,[status(thm)],[just78]),
[] ).
fof(just7,plain,
genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(166551640,plain,
genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt),
inference(rewrite,[status(thm)],[just7]),
[] ).
cnf(179352264,plain,
( ~ mtvisible(c_ldscgeneralcollectormt)
| mtvisible(c_ldscdemonstrationspindleheadmt) ),
inference(resolution,[status(thm)],[167186632,166551640]),
[] ).
fof(query50,plain,
( mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32))
& ~ tptptypes_7_691(c_tptpcol_16_26939,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) ),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(167274512,plain,
mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32)),
inference(rewrite,[status(thm)],[query50]),
[] ).
fof(just4,plain,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32),c_machinelearningspindleheadmt),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(166534248,plain,
genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32),c_machinelearningspindleheadmt),
inference(rewrite,[status(thm)],[just4]),
[] ).
cnf(179405216,plain,
mtvisible(c_machinelearningspindleheadmt),
inference(forward_subsumption_resolution__resolution,[status(thm)],[167274512,167186632,166534248]),
[] ).
fof(just5,plain,
genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(166542960,plain,
genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt),
inference(rewrite,[status(thm)],[just5]),
[] ).
cnf(179337288,plain,
( ~ mtvisible(c_machinelearningspindleheadmt)
| mtvisible(c_miptdatabase19681997_termsmt) ),
inference(resolution,[status(thm)],[167186632,166542960]),
[] ).
fof(just6,plain,
genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(166511728,plain,
genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt),
inference(rewrite,[status(thm)],[just6]),
[] ).
cnf(178383104,plain,
( ~ mtvisible(c_miptdatabase19681997_termsmt)
| mtvisible(c_ldscgeneralcollectormt) ),
inference(resolution,[status(thm)],[167186632,166511728]),
[] ).
cnf(179545224,plain,
mtvisible(c_ldscgeneralcollectormt),
inference(forward_subsumption_resolution__resolution,[status(thm)],[179405216,179337288,178383104]),
[] ).
cnf(179591432,plain,
mtvisible(c_ldscdemonstrationspindleheadmt),
inference(resolution,[status(thm)],[179352264,179545224]),
[] ).
fof(just1,plain,
genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(166514280,plain,
genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric),
inference(rewrite,[status(thm)],[just1]),
[] ).
cnf(178273760,plain,
( ~ mtvisible(c_ldscdemonstrationspindleheadmt)
| mtvisible(c_currentworlddatacollectormt_nonhomocentric) ),
inference(resolution,[status(thm)],[167186632,166514280]),
[] ).
fof(just15,plain,
( ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939) ),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(166630048,plain,
( ~ mtvisible(c_currentworlddatacollectormt_nonhomocentric)
| tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939) ),
inference(rewrite,[status(thm)],[just15]),
[] ).
fof(just14,plain,
! [A,B] :
( ~ tptptypes_9_693(A,B)
| tptptypes_8_692(A,B) ),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(166617744,plain,
( ~ tptptypes_9_693(A,B)
| tptptypes_8_692(A,B) ),
inference(rewrite,[status(thm)],[just14]),
[] ).
fof(just12,plain,
! [A,B] :
( ~ tptptypes_8_692(A,B)
| tptptypes_7_691(B,A) ),
file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),
[] ).
cnf(166594104,plain,
( ~ tptptypes_8_692(A,B)
| tptptypes_7_691(B,A) ),
inference(rewrite,[status(thm)],[just12]),
[] ).
cnf(167261296,plain,
~ tptptypes_7_691(c_tptpcol_16_26939,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),
inference(rewrite,[status(thm)],[query50]),
[] ).
cnf(178852856,plain,
~ tptptypes_8_692(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939),
inference(resolution,[status(thm)],[166594104,167261296]),
[] ).
cnf(178878608,plain,
~ tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939),
inference(resolution,[status(thm)],[166617744,178852856]),
[] ).
cnf(178889272,plain,
~ mtvisible(c_currentworlddatacollectormt_nonhomocentric),
inference(resolution,[status(thm)],[166630048,178878608]),
[] ).
cnf(179450104,plain,
~ mtvisible(c_ldscdemonstrationspindleheadmt),
inference(resolution,[status(thm)],[178273760,178889272]),
[] ).
cnf(contradiction,plain,
$false,
inference(resolution,[status(thm)],[179591432,179450104]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(just78,plain,(~mtvisible(A)|~genlmt(A,B)|mtvisible(B)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(167186632,plain,(~mtvisible(A)|~genlmt(A,B)|mtvisible(B)),inference(rewrite,[status(thm)],[just78]),[]).
%
% fof(just7,plain,(genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(166551640,plain,(genlmt(c_ldscgeneralcollectormt,c_ldscdemonstrationspindleheadmt)),inference(rewrite,[status(thm)],[just7]),[]).
%
% cnf(179352264,plain,(~mtvisible(c_ldscgeneralcollectormt)|mtvisible(c_ldscdemonstrationspindleheadmt)),inference(resolution,[status(thm)],[167186632,166551640]),[]).
%
% fof(query50,plain,((mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32))&~tptptypes_7_691(c_tptpcol_16_26939,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(167274512,plain,(mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32))),inference(rewrite,[status(thm)],[query50]),[]).
%
% fof(just4,plain,(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32),c_machinelearningspindleheadmt)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(166534248,plain,(genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32),c_machinelearningspindleheadmt)),inference(rewrite,[status(thm)],[just4]),[]).
%
% cnf(179405216,plain,(mtvisible(c_machinelearningspindleheadmt)),inference(forward_subsumption_resolution__resolution,[status(thm)],[167274512,167186632,166534248]),[]).
%
% fof(just5,plain,(genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(166542960,plain,(genlmt(c_machinelearningspindleheadmt,c_miptdatabase19681997_termsmt)),inference(rewrite,[status(thm)],[just5]),[]).
%
% cnf(179337288,plain,(~mtvisible(c_machinelearningspindleheadmt)|mtvisible(c_miptdatabase19681997_termsmt)),inference(resolution,[status(thm)],[167186632,166542960]),[]).
%
% fof(just6,plain,(genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(166511728,plain,(genlmt(c_miptdatabase19681997_termsmt,c_ldscgeneralcollectormt)),inference(rewrite,[status(thm)],[just6]),[]).
%
% cnf(178383104,plain,(~mtvisible(c_miptdatabase19681997_termsmt)|mtvisible(c_ldscgeneralcollectormt)),inference(resolution,[status(thm)],[167186632,166511728]),[]).
%
% cnf(179545224,plain,(mtvisible(c_ldscgeneralcollectormt)),inference(forward_subsumption_resolution__resolution,[status(thm)],[179405216,179337288,178383104]),[]).
%
% cnf(179591432,plain,(mtvisible(c_ldscdemonstrationspindleheadmt)),inference(resolution,[status(thm)],[179352264,179545224]),[]).
%
% fof(just1,plain,(genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(166514280,plain,(genlmt(c_ldscdemonstrationspindleheadmt,c_currentworlddatacollectormt_nonhomocentric)),inference(rewrite,[status(thm)],[just1]),[]).
%
% cnf(178273760,plain,(~mtvisible(c_ldscdemonstrationspindleheadmt)|mtvisible(c_currentworlddatacollectormt_nonhomocentric)),inference(resolution,[status(thm)],[167186632,166514280]),[]).
%
% fof(just15,plain,(~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(166630048,plain,(~mtvisible(c_currentworlddatacollectormt_nonhomocentric)|tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939)),inference(rewrite,[status(thm)],[just15]),[]).
%
% fof(just14,plain,(~tptptypes_9_693(A,B)|tptptypes_8_692(A,B)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(166617744,plain,(~tptptypes_9_693(A,B)|tptptypes_8_692(A,B)),inference(rewrite,[status(thm)],[just14]),[]).
%
% fof(just12,plain,(~tptptypes_8_692(A,B)|tptptypes_7_691(B,A)),file('/tmp/SystemOnTPTP1837/CSR050+1.p',unknown),[]).
%
% cnf(166594104,plain,(~tptptypes_8_692(A,B)|tptptypes_7_691(B,A)),inference(rewrite,[status(thm)],[just12]),[]).
%
% cnf(167261296,plain,(~tptptypes_7_691(c_tptpcol_16_26939,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),inference(rewrite,[status(thm)],[query50]),[]).
%
% cnf(178852856,plain,(~tptptypes_8_692(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939)),inference(resolution,[status(thm)],[166594104,167261296]),[]).
%
% cnf(178878608,plain,(~tptptypes_9_693(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma),c_tptpcol_16_26939)),inference(resolution,[status(thm)],[166617744,178852856]),[]).
%
% cnf(178889272,plain,(~mtvisible(c_currentworlddatacollectormt_nonhomocentric)),inference(resolution,[status(thm)],[166630048,178878608]),[]).
%
% cnf(179450104,plain,(~mtvisible(c_ldscdemonstrationspindleheadmt)),inference(resolution,[status(thm)],[178273760,178889272]),[]).
%
% cnf(contradiction,plain,$false,inference(resolution,[status(thm)],[179591432,179450104]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------