%------------------------------------------------------------------------------
% File : Faust---1.0
% Problem : CSR074+1 : TPTP v3.4.2. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : faust %s
% Computer : art04.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:46:33 EDT 2009
% Result : Theorem 0.1s
% Output : Refutation 0.1s
% Verified :
% SZS Type : Refutation
% Derivation depth : 4
% Number of leaves : 9
% Syntax : Number of formulae : 28 ( 11 unt; 0 def)
% Number of atoms : 55 ( 0 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 54 ( 27 ~; 24 |; 3 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 6 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 6 con; 0-0 aty)
% Number of variables : 15 ( 0 sgn 7 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Faust---1.0 format not known, defaulting to TPTP
fof(just5,plain,
! [A,B] :
( ~ geographicalsubregions(A,B)
| inregion(B,A) ),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150271240,plain,
( ~ geographicalsubregions(A,B)
| inregion(B,A) ),
inference(rewrite,[status(thm)],[just5]),
[] ).
fof(just11,plain,
( ~ mtvisible(c_tptpgeo_member7_mt)
| geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74) ),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150309488,plain,
( ~ mtvisible(c_tptpgeo_member7_mt)
| geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74) ),
inference(rewrite,[status(thm)],[just11]),
[] ).
fof(query74,plain,
( ( mtvisible(c_tptpgeo_member7_mt)
| ~ geolevel_3(c_georegion_l3_x17_y24) )
& ( ~ inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)
| ~ geolevel_3(c_georegion_l3_x17_y24) )
& ( mtvisible(c_tptpgeo_member7_mt)
| mtvisible(c_tptpgeo_member7_mt) )
& ( ~ inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)
| mtvisible(c_tptpgeo_member7_mt) ) ),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150674992,plain,
mtvisible(c_tptpgeo_member7_mt),
inference(rewrite,[status(thm)],[query74]),
[] ).
cnf(164407288,plain,
geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74),
inference(resolution,[status(thm)],[150309488,150674992]),
[] ).
cnf(164780264,plain,
inregion(c_georegion_l4_x53_y74,c_georegion_l3_x17_y24),
inference(resolution,[status(thm)],[150271240,164407288]),
[] ).
fof(just41,plain,
! [A,B,C] :
( ~ inregion(A,B)
| ~ inregion(B,C)
| inregion(A,C) ),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150530784,plain,
( ~ inregion(A,B)
| ~ inregion(B,C)
| inregion(A,C) ),
inference(rewrite,[status(thm)],[just41]),
[] ).
fof(just12,plain,
( ~ mtvisible(c_tptpgeo_member7_mt)
| inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74) ),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150319384,plain,
( ~ mtvisible(c_tptpgeo_member7_mt)
| inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74) ),
inference(rewrite,[status(thm)],[just12]),
[] ).
cnf(164417680,plain,
inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74),
inference(resolution,[status(thm)],[150319384,150674992]),
[] ).
cnf(166671024,plain,
( ~ inregion(c_georegion_l4_x53_y74,A)
| inregion(c_geolocation_x53_y74,A) ),
inference(resolution,[status(thm)],[150530784,164417680]),
[] ).
fof(just49,plain,
! [A,B] :
( ~ mtvisible(A)
| ~ genlmt(A,B)
| mtvisible(B) ),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150578880,plain,
( ~ mtvisible(A)
| ~ genlmt(A,B)
| mtvisible(B) ),
inference(rewrite,[status(thm)],[just49]),
[] ).
fof(just9,plain,
genlmt(c_tptpgeo_member7_mt,c_tptpgeo_spindleheadmt),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150296488,plain,
genlmt(c_tptpgeo_member7_mt,c_tptpgeo_spindleheadmt),
inference(rewrite,[status(thm)],[just9]),
[] ).
cnf(165128560,plain,
mtvisible(c_tptpgeo_spindleheadmt),
inference(forward_subsumption_resolution__resolution,[status(thm)],[150674992,150578880,150296488]),
[] ).
fof(just8,plain,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150288416,plain,
genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt),
inference(rewrite,[status(thm)],[just8]),
[] ).
cnf(165123832,plain,
( ~ mtvisible(c_tptpgeo_spindleheadmt)
| mtvisible(c_worldgeographymt) ),
inference(resolution,[status(thm)],[150578880,150288416]),
[] ).
cnf(150679520,plain,
( ~ inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)
| ~ geolevel_3(c_georegion_l3_x17_y24) ),
inference(rewrite,[status(thm)],[query74]),
[] ).
fof(just10,plain,
( ~ mtvisible(c_worldgeographymt)
| geolevel_3(c_georegion_l3_x17_y24) ),
file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),
[] ).
cnf(150241016,plain,
( ~ mtvisible(c_worldgeographymt)
| geolevel_3(c_georegion_l3_x17_y24) ),
inference(rewrite,[status(thm)],[just10]),
[] ).
cnf(164879032,plain,
( ~ inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)
| ~ mtvisible(c_worldgeographymt) ),
inference(resolution,[status(thm)],[150679520,150241016]),
[] ).
cnf(165302936,plain,
~ inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24),
inference(forward_subsumption_resolution__resolution,[status(thm)],[165128560,165123832,164879032]),
[] ).
cnf(contradiction,plain,
$false,
inference(forward_subsumption_resolution__resolution,[status(thm)],[164780264,166671024,165302936]),
[] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Proof found in: 0 seconds
% START OF PROOF SEQUENCE
% fof(just5,plain,(~geographicalsubregions(A,B)|inregion(B,A)),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150271240,plain,(~geographicalsubregions(A,B)|inregion(B,A)),inference(rewrite,[status(thm)],[just5]),[]).
%
% fof(just11,plain,(~mtvisible(c_tptpgeo_member7_mt)|geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74)),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150309488,plain,(~mtvisible(c_tptpgeo_member7_mt)|geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74)),inference(rewrite,[status(thm)],[just11]),[]).
%
% fof(query74,plain,(((mtvisible(c_tptpgeo_member7_mt)|~geolevel_3(c_georegion_l3_x17_y24))&(~inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)|~geolevel_3(c_georegion_l3_x17_y24))&(mtvisible(c_tptpgeo_member7_mt)|mtvisible(c_tptpgeo_member7_mt))&(~inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)|mtvisible(c_tptpgeo_member7_mt)))),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150674992,plain,(mtvisible(c_tptpgeo_member7_mt)),inference(rewrite,[status(thm)],[query74]),[]).
%
% cnf(164407288,plain,(geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74)),inference(resolution,[status(thm)],[150309488,150674992]),[]).
%
% cnf(164780264,plain,(inregion(c_georegion_l4_x53_y74,c_georegion_l3_x17_y24)),inference(resolution,[status(thm)],[150271240,164407288]),[]).
%
% fof(just41,plain,(~inregion(A,B)|~inregion(B,C)|inregion(A,C)),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150530784,plain,(~inregion(A,B)|~inregion(B,C)|inregion(A,C)),inference(rewrite,[status(thm)],[just41]),[]).
%
% fof(just12,plain,(~mtvisible(c_tptpgeo_member7_mt)|inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74)),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150319384,plain,(~mtvisible(c_tptpgeo_member7_mt)|inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74)),inference(rewrite,[status(thm)],[just12]),[]).
%
% cnf(164417680,plain,(inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74)),inference(resolution,[status(thm)],[150319384,150674992]),[]).
%
% cnf(166671024,plain,(~inregion(c_georegion_l4_x53_y74,A)|inregion(c_geolocation_x53_y74,A)),inference(resolution,[status(thm)],[150530784,164417680]),[]).
%
% fof(just49,plain,(~mtvisible(A)|~genlmt(A,B)|mtvisible(B)),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150578880,plain,(~mtvisible(A)|~genlmt(A,B)|mtvisible(B)),inference(rewrite,[status(thm)],[just49]),[]).
%
% fof(just9,plain,(genlmt(c_tptpgeo_member7_mt,c_tptpgeo_spindleheadmt)),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150296488,plain,(genlmt(c_tptpgeo_member7_mt,c_tptpgeo_spindleheadmt)),inference(rewrite,[status(thm)],[just9]),[]).
%
% cnf(165128560,plain,(mtvisible(c_tptpgeo_spindleheadmt)),inference(forward_subsumption_resolution__resolution,[status(thm)],[150674992,150578880,150296488]),[]).
%
% fof(just8,plain,(genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt)),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150288416,plain,(genlmt(c_tptpgeo_spindleheadmt,c_worldgeographymt)),inference(rewrite,[status(thm)],[just8]),[]).
%
% cnf(165123832,plain,(~mtvisible(c_tptpgeo_spindleheadmt)|mtvisible(c_worldgeographymt)),inference(resolution,[status(thm)],[150578880,150288416]),[]).
%
% cnf(150679520,plain,(~inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)|~geolevel_3(c_georegion_l3_x17_y24)),inference(rewrite,[status(thm)],[query74]),[]).
%
% fof(just10,plain,(~mtvisible(c_worldgeographymt)|geolevel_3(c_georegion_l3_x17_y24)),file('/tmp/SystemOnTPTP10177/CSR074+1.p',unknown),[]).
%
% cnf(150241016,plain,(~mtvisible(c_worldgeographymt)|geolevel_3(c_georegion_l3_x17_y24)),inference(rewrite,[status(thm)],[just10]),[]).
%
% cnf(164879032,plain,(~inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)|~mtvisible(c_worldgeographymt)),inference(resolution,[status(thm)],[150679520,150241016]),[]).
%
% cnf(165302936,plain,(~inregion(c_geolocation_x53_y74,c_georegion_l3_x17_y24)),inference(forward_subsumption_resolution__resolution,[status(thm)],[165128560,165123832,164879032]),[]).
%
% cnf(contradiction,plain,$false,inference(forward_subsumption_resolution__resolution,[status(thm)],[164780264,166671024,165302936]),[]).
%
% END OF PROOF SEQUENCE
%
%------------------------------------------------------------------------------