%------------------------------------------------------------------------------
% File : DarwinFM---1.4.5
% Problem : CSR111+2 : TPTP v8.1.0. Released v3.5.0.
% Transfm : none
% Format : tptp:raw
% Command : darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s
% Computer : n023.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 0s
% DateTime : Fri Jul 15 02:34:41 EDT 2022
% Result : Satisfiable 9.10s 9.26s
% Output : FiniteModel 9.10s
% Verified :
% SZS Type : FiniteModel
% Domain size : 5
% Comments :
%------------------------------------------------------------------------------
fof(interpretation_domain,fi_domain,
! [X] :
( X = e1
| X = e2
| X = e3
| X = e4
| X = e5 ) ).
fof(interpretation_domain_distinct,fi_domain,
( e1 != e2
& e1 != e3
& e1 != e4
& e1 != e5
& e2 != e3
& e2 != e4
& e2 != e5
& e3 != e4
& e3 != e5
& e4 != e5 ) ).
fof(interpretation_terms,fi_functors,
( c_affiliatedwith = e1
& c_airport_physical = e1
& c_airporthasiatacode = e1
& c_ap_martha_stewart_omnimedia_names_chairman = e1
& c_applicationcontext = e1
& c_artifact = e1
& c_artsupplies = e1
& c_aspatialinformationstore = e1
& c_aspatialthing = e1
& c_basekb = e2
& c_beloitcollege = e1
& c_calendarsmt = e2
& c_calendarsvocabularymt = e2
& c_citynamedfn = e1
& c_cityofbostonma = e1
& c_collection = e3
& c_computerdataartifact = e1
& c_contentmtofcdafromeventfn = e1
& c_contextofpcwfn = e1
& c_corecyclmt = e2
& c_correctivelensprescription = e1
& c_currentworlddatacollectormt_nonhomocentric = e2
& c_cyclistsmt = e2
& c_cycnounlearnermt = e2
& c_cycorpproductsmt = e2
& c_directionoftranslation_throughout = e1
& c_disjointwith = e1
& c_enduringthing_localized = e1
& c_englishmt = e1
& c_ethnicgroupsmt = e2
& c_ethnicgroupsvocabularymt = e2
& c_executionbyfiringsquad = e1
& c_few = e1
& c_firstordercollection = e3
& c_fixedordercollection = e3
& c_footballteam = e1
& c_france = e1
& c_furpelt = e1
& c_generictemporalmt = e2
& c_genlmt = e1
& c_genlpreds = e1
& c_genls = e1
& c_geographicalregion = e1
& c_geographicalsubregions = e1
& c_geographymt = e2
& c_geolevel_1 = e1
& c_geolevel_3 = e4
& c_geolevel_4 = e1
& c_geolocation_x14_y39 = e2
& c_geolocation_x53_y74 = e2
& c_geolocation_x76_y23 = e2
& c_georegion_l1_x2_y0 = e2
& c_georegion_l2_x5_y8 = e2
& c_georegion_l2_x8_y2 = e2
& c_georegion_l3_x11_y2 = e2
& c_georegion_l3_x15_y24 = e2
& c_georegion_l3_x17_y24 = e2
& c_georegion_l3_x25_y7 = e2
& c_georegion_l3_x4_y13 = e2
& c_georegion_l4_x14_y39 = e2
& c_georegion_l4_x27_y64 = e2
& c_georegion_l4_x27_y65 = e5
& c_georegion_l4_x29_y75 = e2
& c_georegion_l4_x29_y76 = e5
& c_georegion_l4_x35_y7 = e2
& c_georegion_l4_x36_y50 = e1
& c_georegion_l4_x37_y50 = e1
& c_georegion_l4_x38_y24 = e2
& c_georegion_l4_x39_y24 = e5
& c_georegion_l4_x45_y10 = e2
& c_georegion_l4_x45_y72 = e2
& c_georegion_l4_x45_y9 = e5
& c_georegion_l4_x53_y74 = e2
& c_georegion_l4_x56_y47 = e2
& c_georegion_l4_x57_y47 = e5
& c_georegion_l4_x75_y75 = e2
& c_georegion_l4_x76_y23 = e2
& c_gregoriancalendarmt = e2
& c_hasmembers = e1
& c_hpkb_subnationalagent = e1
& c_hpkbvocabmt = e2
& c_humansociallifemt = e2
& c_inanimateobject = e1
& c_inanimateobject_nonnatural = e1
& c_individual = e1
& c_inregion = e1
& c_instancewithrelationtofn = e1
& c_intangible = e3
& c_intangibleindividual = e1
& c_issuingaprescription = e1
& c_keinteractionresourcetestmt = e2
& c_knowledgefragmentd3mt = e2
& c_ldscdemonstrationspindleheadmt = e2
& c_ldscgeneralcollectormt = e2
& c_location_underspecified = e1
& c_logicaltruthmt = e2
& c_machinelearningspindleheadmt = e2
& c_marriagelicensedocument = e1
& c_massmediadatamt = e2
& c_mathematicalorcomputationalthing = e3
& c_mathematicalthing = e3
& c_microtheory = e1
& c_militaryperson = e1
& c_miptdatabase19681997_termsmt = e2
& c_most = e1
& c_movement_translationevent = e1
& c_navypersonnel = e1
& c_no = e1
& c_nooescapearchitecturemt = e2
& c_objectfoundinlocation = e1
& c_orderingpredicate = e3
& c_organizationdatamt = e2
& c_orientation = e1
& c_orientationvector = e1
& c_partiallyintangibleindividual = e1
& c_partiallytangible = e1
& c_patterndetectormt = e2
& c_peopledatamt = e2
& c_physicalorderingpredicate = e3
& c_products = e1
& c_pushingababycarriage = e1
& c_pushingwithfingers = e1
& c_pushingwithopenhand = e1
& c_reasoningaboutpossibleantecedentsmt = e2
& c_reflexivebinarypredicate = e3
& c_relationallexistsfn = e1
& c_relationexistsallfn = e1
& c_ridgeline_topographical = e1
& c_runningshorts = e1
& c_setorcollection = e3
& c_shavingrazor_manual = e1
& c_ship = e1
& c_spatialthing_nonsituational = e1
& c_state_geopolitical = e1
& c_subcollectionofwithrelationfromtypefn = e1
& c_subcollectionofwithrelationtofn = e1
& c_subcollectionofwithrelationtotypefn = e1
& c_subsetof = e1
& c_supplies = e1
& c_terrorist = e1
& c_terroristgroup = e1
& c_testvocabularymt = e2
& c_theprototypicalfurpelt = e2
& c_theprototypicalshavingrazor_manual = e2
& c_thing = e4
& c_timehasnoendmt = e2
& c_tptp_8_271 = e1
& c_tptp_8_875 = e1
& c_tptp_8_968 = e1
& c_tptp_9_51 = e1
& c_tptp_9_720 = e1
& c_tptp_member1672_mt = e2
& c_tptp_member2089_mt = e2
& c_tptp_member2356_mt = e2
& c_tptp_member235_mt = e2
& c_tptp_member237_mt = e2
& c_tptp_member2610_mt = e2
& c_tptp_member2668_mt = e2
& c_tptp_member2701_mt = e2
& c_tptp_member2831_mt = e2
& c_tptp_member2862_mt = e2
& c_tptp_member3205_mt = e2
& c_tptp_member3356_mt = e1
& c_tptp_member3393_mt = e2
& c_tptp_member3515_mt = e2
& c_tptp_member3633_mt = e2
& c_tptp_member3717_mt = e2
& c_tptp_member3993_mt = e2
& c_tptp_member698_mt = e2
& c_tptp_member974_mt = e2
& c_tptp_spindlecollectormt = e2
& c_tptp_spindleheadmt = e2
& c_tptpartsupplies = e2
& c_tptpcol_0_0 = e1
& c_tptpcol_10_109061 = e1
& c_tptpcol_10_118020 = e3
& c_tptpcol_10_18567 = e3
& c_tptpcol_10_22022 = e3
& c_tptpcol_10_26886 = e3
& c_tptpcol_10_40324 = e1
& c_tptpcol_10_72710 = e1
& c_tptpcol_10_92166 = e1
& c_tptpcol_10_93700 = e1
& c_tptpcol_11_109125 = e1
& c_tptpcol_11_118084 = e3
& c_tptpcol_11_18631 = e3
& c_tptpcol_11_22023 = e3
& c_tptpcol_11_26887 = e3
& c_tptpcol_11_40388 = e1
& c_tptpcol_11_72774 = e1
& c_tptpcol_11_92230 = e1
& c_tptpcol_11_93764 = e1
& c_tptpcol_12_109157 = e1
& c_tptpcol_12_118116 = e3
& c_tptpcol_12_18663 = e3
& c_tptpcol_12_22055 = e3
& c_tptpcol_12_26919 = e3
& c_tptpcol_12_40420 = e1
& c_tptpcol_12_72775 = e1
& c_tptpcol_12_92262 = e1
& c_tptpcol_12_93765 = e1
& c_tptpcol_13_109173 = e1
& c_tptpcol_13_118117 = e3
& c_tptpcol_13_18664 = e3
& c_tptpcol_13_22071 = e3
& c_tptpcol_13_26920 = e3
& c_tptpcol_13_40421 = e1
& c_tptpcol_13_72791 = e1
& c_tptpcol_13_92263 = e1
& c_tptpcol_13_93766 = e1
& c_tptpcol_14_109181 = e1
& c_tptpcol_14_118118 = e3
& c_tptpcol_14_22072 = e3
& c_tptpcol_14_26921 = e3
& c_tptpcol_14_40429 = e1
& c_tptpcol_14_72792 = e1
& c_tptpcol_14_92264 = e1
& c_tptpcol_14_93774 = e1
& c_tptpcol_15_109185 = e1
& c_tptpcol_15_130923 = e1
& c_tptpcol_15_130931 = e1
& c_tptpcol_15_22076 = e3
& c_tptpcol_15_26925 = e3
& c_tptpcol_15_30970 = e1
& c_tptpcol_15_4027 = e1
& c_tptpcol_15_40430 = e1
& c_tptpcol_15_50957 = e1
& c_tptpcol_15_72793 = e1
& c_tptpcol_15_92268 = e1
& c_tptpcol_15_93775 = e1
& c_tptpcol_16_10258 = e1
& c_tptpcol_16_130924 = e1
& c_tptpcol_16_130933 = e1
& c_tptpcol_16_25972 = e3
& c_tptpcol_16_26926 = e3
& c_tptpcol_16_26939 = e1
& c_tptpcol_16_27189 = e3
& c_tptpcol_16_29490 = e1
& c_tptpcol_16_30972 = e1
& c_tptpcol_16_31868 = e3
& c_tptpcol_16_4451 = e1
& c_tptpcol_16_50958 = e1
& c_tptpcol_16_62187 = e1
& c_tptpcol_16_72795 = e1
& c_tptpcol_16_7738 = e1
& c_tptpcol_16_8886 = e1
& c_tptpcol_16_92269 = e1
& c_tptpcol_1_1 = e3
& c_tptpcol_1_65536 = e1
& c_tptpcol_2_2 = e3
& c_tptpcol_2_65537 = e1
& c_tptpcol_2_98304 = e1
& c_tptpcol_3_114688 = e3
& c_tptpcol_3_16386 = e3
& c_tptpcol_3_65538 = e1
& c_tptpcol_3_81921 = e1
& c_tptpcol_3_98305 = e1
& c_tptpcol_4_106497 = e1
& c_tptpcol_4_114689 = e3
& c_tptpcol_4_16387 = e3
& c_tptpcol_4_24578 = e3
& c_tptpcol_4_65539 = e1
& c_tptpcol_4_90113 = e1
& c_tptpcol_5_106498 = e1
& c_tptpcol_5_110593 = e1
& c_tptpcol_5_114690 = e3
& c_tptpcol_5_16388 = e3
& c_tptpcol_5_20483 = e3
& c_tptpcol_5_24579 = e3
& c_tptpcol_5_69635 = e1
& c_tptpcol_5_90114 = e1
& c_tptpcol_6_108546 = e1
& c_tptpcol_6_112641 = e1
& c_tptpcol_6_116738 = e3
& c_tptpcol_6_18436 = e3
& c_tptpcol_6_20484 = e3
& c_tptpcol_6_26627 = e3
& c_tptpcol_6_71683 = e1
& c_tptpcol_6_92162 = e1
& c_tptpcol_7_108547 = e1
& c_tptpcol_7_113665 = e1
& c_tptpcol_7_117762 = e3
& c_tptpcol_7_18437 = e3
& c_tptpcol_7_21508 = e3
& c_tptpcol_7_26628 = e3
& c_tptpcol_7_39939 = e1
& c_tptpcol_7_72707 = e1
& c_tptpcol_7_92163 = e1
& c_tptpcol_7_93186 = e1
& c_tptpcol_8_109059 = e1
& c_tptpcol_8_114177 = e1
& c_tptpcol_8_117763 = e3
& c_tptpcol_8_18438 = e3
& c_tptpcol_8_22020 = e3
& c_tptpcol_8_26629 = e3
& c_tptpcol_8_39940 = e1
& c_tptpcol_8_72708 = e1
& c_tptpcol_8_92164 = e1
& c_tptpcol_8_93698 = e1
& c_tptpcol_9_109060 = e1
& c_tptpcol_9_118019 = e3
& c_tptpcol_9_18439 = e3
& c_tptpcol_9_22021 = e3
& c_tptpcol_9_26885 = e3
& c_tptpcol_9_40196 = e1
& c_tptpcol_9_72709 = e1
& c_tptpcol_9_92165 = e1
& c_tptpcol_9_93699 = e1
& c_tptpexecutionbyfiringsquad_90 = e2
& c_tptpgeo_member1_mt = e2
& c_tptpgeo_member2_mt = e2
& c_tptpgeo_member3_mt = e2
& c_tptpgeo_member4_mt = e1
& c_tptpgeo_member5_mt = e2
& c_tptpgeo_member7_mt = e2
& c_tptpgeo_member8_mt = e2
& c_tptpgeo_spindlecollectormt = e2
& c_tptpgeo_spindleheadmt = e2
& c_tptpmarriagelicensedocument = e1
& c_tptpnavypersonnel_3 = e2
& c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 = e2
& c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 = e2
& c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 = e2
& c_tptpofobject = e1
& c_tptpquantityfn_1 = e1
& c_tptpquantityfn_13 = e1
& c_tptpquantityfn_14 = e1
& c_tptpquantityfn_2 = e1
& c_tptpquantityfn_21 = e1
& c_tptpquantityfn_6 = e1
& c_tptpridgeline_topographical = e2
& c_tptprunningshorts = e2
& c_tptptptpcol_16_25985 = e2
& c_tptptptpcol_16_8398 = e2
& c_tptptypes_5_387 = e1
& c_tptptypes_5_802 = e1
& c_tptptypes_6_388 = e1
& c_tptptypes_6_818 = e1
& c_tptptypes_7_389 = e1
& c_tptptypes_7_396 = e1
& c_tptptypes_7_691 = e1
& c_tptptypes_7_819 = e1
& c_tptptypes_8_390 = e1
& c_tptptypes_8_400 = e1
& c_tptptypes_8_692 = e1
& c_tptptypes_8_823 = e1
& c_tptptypes_9_401 = e1
& c_tptptypes_9_693 = e1
& c_tptptypes_9_824 = e1
& c_trajector_underspecified = e1
& c_transitivebinarypredicate = e3
& c_translation_0_885 = e1
& c_translation_14 = e1
& c_translation_21 = e1
& c_translation_3 = e1
& c_translation_32 = e1
& c_translation_33 = e1
& c_translation_7 = e1
& c_unitedstatesgeographydualistmt = e2
& c_unitedstatesgeographypeoplemt = e2
& c_unitedstatessociallifemt = e2
& c_unitvectorinterval = e1
& c_universalvocabularymt = e2
& c_urlfn = e1
& c_urlreferentfn = e1
& c_wamt_evalinitial_p14 = e2
& c_wanica_districtsuriname = e2
& c_worldcompletedualistgeographymt = e2
& c_worldgeographydualistmt = e2
& c_worldgeographymt = e2
& c_xskijump_thegame = e2
& ! [X0,X1,X2] :
( f_citynamedfn(X0,X1) = X2
<=> ( ( X2 = e1
& ~ ( X0 = e1
& X1 = e1 ) )
| ( X0 = e1
& X1 = e1
& X2 = e2 ) ) )
& ! [X0,X1] : f_contentmtofcdafromeventfn(X0,X1) = e2
& ! [X0] : f_contextofpcwfn(X0) = e2
& ! [X0,X1,X2,X3] :
( f_instancewithrelationtofn(X0,X1,X2) = X3
<=> ( ( X3 = e1
& ~ ( X0 = e1
& X1 = e1
& X2 = e1 ) )
| ( X0 = e1
& X1 = e1
& X2 = e1
& X3 = e2 ) ) )
& ! [X0,X1,X2,X3,X4] :
( f_relationallexistsfn(X0,X1,X2,X3) = X4
<=> ( ( X0 = e5
& X1 = e1
& X2 = e1
& X3 = e1
& X4 = e2 )
| ( X4 = e1
& ~ ( X0 = e5
& X1 = e1
& X2 = e1
& X3 = e1 )
& ~ ( X0 = e2
& X1 = e1
& X2 = e1
& X3 = e1 ) )
| ( X0 = e2
& X1 = e1
& X2 = e1
& X3 = e1
& X4 = e2 ) ) )
& ! [X0,X1,X2,X3,X4] :
( f_relationexistsallfn(X0,X1,X2,X3) = X4
<=> ( ( X0 = e5
& X1 = e1
& X2 = e1
& X3 = e1
& X4 = e2 )
| ( X4 = e1
& ~ ( X0 = e5
& X1 = e1
& X2 = e1
& X3 = e1 )
& ~ ( X0 = e2
& X1 = e1
& X2 = e1
& X3 = e1 ) )
| ( X0 = e2
& X1 = e1
& X2 = e1
& X3 = e1
& X4 = e2 ) ) )
& ! [X0,X1,X2] : f_subcollectionofwithrelationfromtypefn(X0,X1,X2) = e1
& ! [X0,X1,X2] : f_subcollectionofwithrelationtofn(X0,X1,X2) = e1
& ! [X0,X1,X2] : f_subcollectionofwithrelationtotypefn(X0,X1,X2) = e1
& ! [X0] : f_tptpquantityfn_1(X0) = e1
& ! [X0] : f_tptpquantityfn_13(X0) = e1
& ! [X0] : f_tptpquantityfn_14(X0) = e1
& ! [X0] : f_tptpquantityfn_2(X0) = e1
& ! [X0] : f_tptpquantityfn_21(X0) = e1
& ! [X0] : f_tptpquantityfn_6(X0) = e1
& ! [X0,X1] :
( f_urlfn(X0) = X1
<=> ( ( X1 = e1
& X0 != e2
& X0 != e1 )
| ( X0 = e1
& X1 = e2 )
| ( X0 = e2
& X1 = e2 ) ) )
& ! [X0] : f_urlreferentfn(X0) = e2
& n_1 = e1
& n_170 = e1
& n_2 = e1
& n_232 = e1
& n_3 = e1
& n_328 = e1
& n_4 = e1
& n_414 = e1
& n_468 = e1
& n_756 = e1
& s_agen = e1
& s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf = e1
& s_http_memberstripodcomindygalfordtriviahtm = e1
& s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml = e1
& s_http_webnjiteducjohnsontreebiochhtm = e1
& s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml = e1
& s_http_wwwarthritis_symptomcoma_cbursitishtm = e1
& s_http_wwwfuntriviacomplayquizcfmqid60926origin = e1
& s_http_wwwinformationblastcomtechnical_university_of_munichhtml = e1
& s_http_wwwpoweripodsearchinfobrown_ipodhtml = e1
& s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988 = e1
& s_http_wwwthedailybulletincompostcardsmar9chtm = e1
& s_terroristthathasbeenamemberofaterroristorganization = e1
& s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege = e1
& s_tlh = e1 ) ).
fof(interpretation_atoms,fi_predicates,
( ! [X0,X1] :
( affiliatedwith(X0,X1)
<=> $false )
& ! [X0] : agent_generic(X0)
& ! [X0] :
( airport_physical(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( airporthasiatacode(X0,X1)
<=> $false )
& ! [X0] :
( applicationcontext(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( arg1isa(X0,X1)
<=> ( X0 = e1
& X1 = e3 ) )
& ! [X0,X1] :
( arg2isa(X0,X1)
<=> ( X0 = e1
& X1 = e3 ) )
& ! [X0] :
( artifact(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( artsupplies(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( aspatialinformationstore(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( aspatialthing(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] : binarypredicate(X0)
& ! [X0,X1] :
( borderson(X0,X1)
<=> ( ( X0 = e2
& X1 = e5 )
| ( X0 = e5
& X1 = e2 ) ) )
& ! [X0] : city(X0)
& ! [X0] :
( collection(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( computerdataartifact(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] : controlcharacterfreestring(X0)
& ! [X0] :
( correctivelensprescription(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] : creationordestructionevent(X0)
& ! [X0,X1] :
( directionoftranslation_throughout(X0,X1)
<=> $false )
& ! [X0,X1] :
( disjointwith(X0,X1)
<=> ( ( X0 = e1
& X1 = e3 )
| ( X0 = e3
& X1 = e1 ) ) )
& ! [X0] :
( enduringthing_localized(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( executionbyfiringsquad(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( few(X0,X1)
<=> ( ( X0 = e1
& X1 = e3 )
| ( X0 = e3
& X1 = e1 ) ) )
& ! [X0] :
( firstordercollection(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( fixedordercollection(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( footballteam(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] : function_denotational(X0)
& ! [X0] :
( furpelt(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( genlinverse(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( genlmt(X0,X1)
<=> ( ( X0 = e2
& X1 = e2 )
| ( X0 = e5
& X1 = e5 ) ) )
& ! [X0,X1] :
( genlpreds(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( genls(X0,X1)
<=> ( ( X0 = e4
& X1 = e4 )
| ( X0 = e1
& X1 = e4 )
| ( X0 = e1
& X1 = e1 )
| ( X0 = e3
& X1 = e3 ) ) )
& ! [X0,X1] :
( geographicallysubsumes(X0,X1)
<=> $false )
& ! [X0] :
( geographicalregion(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( geographicalsubregions(X0,X1)
<=> ( ( X0 = e2
& X1 = e2 )
| ( X0 = e5
& X1 = e5 ) ) )
& ! [X0] :
( geolevel_1(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( geolevel_3(X0)
<=> ( X0 = e4
| X0 = e2
| X0 = e1
| X0 = e5
| X0 = e3 ) )
& ! [X0] :
( geolevel_4(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( geopoliticalsubdivision(X0,X1)
<=> $false )
& ! [X0] :
( hpkb_subnationalagent(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( inanimateobject(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( inanimateobject_nonnatural(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( individual(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( inregion(X0,X1)
<=> ( ( X0 = e2
& X1 = e2 )
| ( X0 = e5
& X1 = e5 ) ) )
& ! [X0] :
( intangible(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( intangibleindividual(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( isa(X0,X1)
<=> ( ( X0 = e4
& X1 = e4 )
| ( X0 = e4
& X1 = e3 )
| ( X0 = e2
& X1 = e4 )
| ( X0 = e2
& X1 = e1 )
| ( X0 = e1
& X1 = e4 )
| ( X0 = e1
& X1 = e3 )
| ( X0 = e5
& X1 = e4 )
| ( X0 = e5
& X1 = e1 )
| ( X0 = e3
& X1 = e4 )
| ( X0 = e3
& X1 = e3 ) ) )
& ! [X0] :
( issuingaprescription(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( location_underspecified(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( marriagelicensedocument(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( mathematicalorcomputationalthing(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( mathematicalthing(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( microtheory(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( militaryperson(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( most(X0,X1)
<=> ( ( X0 = e4
& X1 = e4 )
| ( X0 = e1
& X1 = e4 )
| ( X0 = e1
& X1 = e1 )
| ( X0 = e3
& X1 = e3 ) ) )
& ! [X0] :
( movement_translationevent(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( mtvisible(X0)
<=> X0 = e2 )
& ! [X0,X1,X2] : natargument(X0,X1,X2)
& ! [X0,X1] : natfunction(X0,X1)
& ! [X0] :
( navypersonnel(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( no(X0,X1)
<=> ( ( X0 = e1
& X1 = e3 )
| ( X0 = e3
& X1 = e1 ) ) )
& ! [X0,X1] :
( objectfoundinlocation(X0,X1)
<=> $false )
& ! [X0] :
( orderingpredicate(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] : organization(X0)
& ! [X0,X1] :
( orientation(X0,X1)
<=> $false )
& ! [X0] :
( orientationvector(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( partiallyintangibleindividual(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( partiallytangible(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( physicalorderingpredicate(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] : positiveinteger(X0)
& ! [X0] :
( predicate(X0)
<=> X0 = e1 )
& ! [X0,X1] :
( prettystring(X0,X1)
<=> $false )
& ! [X0,X1] :
( products(X0,X1)
<=> $false )
& ! [X0] :
( pushingababycarriage(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( pushingwithfingers(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( pushingwithopenhand(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] : razor(X0)
& ! [X0] :
( reflexivebinarypredicate(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] : relation(X0)
& ! [X0,X1,X2] :
( relationallexists(X0,X1,X2)
<=> ( ( X0 = e1
& X1 = e1
& X2 = e1 )
| ( X0 = e1
& X1 = e1
& X2 = e3 ) ) )
& ! [X0,X1,X2] :
( relationallinstance(X0,X1,X2)
<=> ( X0 = e1
& X1 = e1
& X2 = e1 ) )
& ! [X0,X1,X2] :
( relationexistsall(X0,X1,X2)
<=> ( ( X0 = e1
& X1 = e1
& X2 = e1 )
| ( X0 = e1
& X1 = e3
& X2 = e1 ) ) )
& ! [X0,X1] :
( resultisaarg(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0] :
( ridgeline_topographical(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( runningshorts(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( setorcollection(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( shavingrazor_manual(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( ship(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] : spatialthing_localized(X0)
& ! [X0] :
( spatialthing_nonsituational(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( state_geopolitical(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] : stringoflengthfn3(X0)
& ! [X0] :
( subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( subregions(X0,X1)
<=> $false )
& ! [X0,X1] :
( subsetof(X0,X1)
<=> ( ( X0 = e4
& X1 = e4 )
| ( X0 = e1
& X1 = e4 )
| ( X0 = e1
& X1 = e1 )
| ( X0 = e3
& X1 = e3 ) ) )
& ! [X0] :
( supplies(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( terrorist(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( terroristgroup(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( thing(X0)
<=> ( X0 = e4
| X0 = e2
| X0 = e1
| X0 = e5
| X0 = e3 ) )
& ! [X0,X1] :
( tptp_8_271(X0,X1)
<=> ( ( X0 = e1
& X1 = e2 )
| ( X0 = e1
& X1 = e5 ) ) )
& ! [X0,X1] :
( tptp_8_875(X0,X1)
<=> ( ( X0 = e2
& X1 = e1 )
| ( X0 = e5
& X1 = e1 ) ) )
& ! [X0,X1] :
( tptp_8_968(X0,X1)
<=> ( ( X0 = e2
& X1 = e2 )
| ( X0 = e2
& X1 = e5 ) ) )
& ! [X0,X1] :
( tptp_9_51(X0,X1)
<=> ( ( X0 = e1
& X1 = e2 )
| ( X0 = e1
& X1 = e5 ) ) )
& ! [X0,X1] :
( tptp_9_720(X0,X1)
<=> ( ( X0 = e2
& X1 = e2 )
| ( X0 = e5
& X1 = e2 ) ) )
& ! [X0] :
( tptpcol_0_0(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_10_109061(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_10_118020(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_10_18567(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_10_22022(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_10_26886(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_10_40324(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_10_72710(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_10_92166(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_10_93700(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_11_109125(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_11_118084(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_11_18631(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_11_22023(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_11_26887(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_11_40388(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_11_72774(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_11_92230(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_11_93764(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_12_109157(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_12_118116(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_12_18663(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_12_22055(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_12_26919(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_12_40420(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_12_72775(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_12_92262(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_12_93765(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_13_109173(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_13_118117(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_13_18664(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_13_22071(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_13_26920(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_13_40421(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_13_72791(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_13_92263(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_13_93766(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_14_109181(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_14_118118(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_14_22072(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_14_26921(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_14_40429(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_14_72792(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_14_92264(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_14_93774(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_109185(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_130923(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_130931(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_22076(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_15_26925(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_15_30970(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_4027(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_40430(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_50957(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_72793(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_92268(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_15_93775(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_10258(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_130924(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_130933(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_25972(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_16_26926(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_16_26939(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_27189(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_16_29490(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_30972(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_31868(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_16_4451(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_50958(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_62187(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_72795(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_7738(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_8886(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_16_92269(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_1_1(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_1_65536(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_2_2(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_2_65537(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_2_98304(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_3_114688(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_3_16386(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_3_65538(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_3_81921(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_3_98305(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_4_106497(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_4_114689(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_4_16387(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_4_24578(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_4_65539(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_4_90113(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_5_106498(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_5_110593(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_5_114690(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_5_16388(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_5_20483(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_5_24579(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] : tptpcol_5_28674(X0)
& ! [X0] :
( tptpcol_5_69635(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_5_90114(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_6_108546(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_6_112641(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_6_116738(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_6_18436(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_6_20484(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_6_26627(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_6_71683(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_6_92162(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_7_108547(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_7_113665(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_7_117762(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_7_18437(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_7_21508(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_7_26628(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_7_39939(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] : tptpcol_7_7172(X0)
& ! [X0] :
( tptpcol_7_72707(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_7_92163(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_7_93186(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_8_109059(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_8_114177(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_8_117763(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_8_18438(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_8_22020(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_8_26629(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_8_39940(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_8_72708(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_8_92164(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_8_93698(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_9_109060(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_9_118019(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_9_18439(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_9_22021(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_9_26885(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] :
( tptpcol_9_40196(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_9_72709(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_9_92165(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( tptpcol_9_93699(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0,X1] :
( tptpofobject(X0,X1)
<=> ( ( X0 = e2
& X1 = e1 )
| ( X0 = e5
& X1 = e1 ) ) )
& ! [X0] : tptpquantity(X0)
& ! [X0,X1] :
( tptptypes_5_387(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_5_802(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_6_388(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_6_818(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_7_389(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_7_396(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_7_691(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_7_819(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_8_390(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_8_400(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_8_692(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_8_823(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_9_401(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_9_693(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0,X1] :
( tptptypes_9_824(X0,X1)
<=> ( X0 = e1
& X1 = e1 ) )
& ! [X0] :
( trajector_underspecified(X0)
<=> ( X0 = e2
| X0 = e5 ) )
& ! [X0] :
( transitivebinarypredicate(X0)
<=> ( X0 = e4
| X0 = e1
| X0 = e3 ) )
& ! [X0] : uniformresourcelocator(X0)
& ! [X0] :
( unitvectorinterval(X0)
<=> ( X0 = e2
| X0 = e5 ) ) ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : CSR111+2 : TPTP v8.1.0. Released v3.5.0.
% 0.07/0.13 % Command : darwin -fd true -ppp true -pl 0 -to %d -pmtptp true %s
% 0.13/0.34 % Computer : n023.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % DateTime : Sat Jun 11 14:53:07 EDT 2022
% 0.13/0.34 % CPUTime :
% 0.13/0.34 Defaulting to tptp format.
% 9.10/9.26 SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.10/9.26
% 9.10/9.26 MODEL (TPTP):
% 9.10/9.26 SZS output start FiniteModel for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------