%------------------------------------------------------------------------------ % File : Etableau---0.67 % Problem : CSR070+5 : TPTP v8.1.0. Bugfixed v3.5.0. % Transfm : none % Format : tptp:raw % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % Computer : n028.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 : 600s % DateTime : Fri Jul 15 03:15:10 EDT 2022 % Result : Theorem 9.43s 9.62s % Output : CNFRefutation 9.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : CSR070+5 : TPTP v8.1.0. Bugfixed v3.5.0. % 0.11/0.12 % Command : etableau --auto --tsmdo --quicksat=10000 --tableau=1 --tableau-saturation=1 -s -p --tableau-cores=8 --cpu-limit=%d %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jun 10 17:42:04 EDT 2022 % 0.12/0.33 % CPUTime : % 8.53/8.75 # SinE strategy is gf500_h_gu_R04_F100_L20000 % 8.53/8.75 # Auto-Mode selected heuristic G_E___207_C18_F1_AE_CS_SP_PS_S0Y % 8.53/8.75 # and selection function SelectMaxLComplexAvoidPosPred. % 8.53/8.75 # % 8.53/8.75 # Presaturation interreduction done % 8.53/8.75 # Number of axioms: 1693 Number of unprocessed: 1493 % 8.53/8.75 # Tableaux proof search. % 8.53/8.75 # APR header successfully linked. % 8.53/8.75 # Hello from C++ % 8.97/9.14 # The folding up rule is enabled... % 8.97/9.14 # Local unification is enabled... % 8.97/9.14 # Any saturation attempts will use folding labels... % 8.97/9.14 # 1493 beginning clauses after preprocessing and clausification % 8.97/9.14 # Creating start rules for all 2 conjectures. % 8.97/9.14 # There are 2 start rule candidates: % 8.97/9.14 # Found 922 unit axioms. % 8.97/9.14 # Unsuccessfully attempted saturation on 1 start tableaux, moving on. % 8.97/9.14 # 2 start rule tableaux created. % 8.97/9.14 # 571 extension rule candidate clauses % 8.97/9.14 # 922 unit axiom clauses % 8.97/9.14 % 8.97/9.14 # Requested 8, 32 cores available to the main process. % 8.97/9.14 # There are not enough tableaux to fork, creating more from the initial 2 % 9.43/9.62 # There were 2 total branch saturation attempts. % 9.43/9.62 # There were 0 of these attempts blocked. % 9.43/9.62 # There were 0 deferred branch saturation attempts. % 9.43/9.62 # There were 0 free duplicated saturations. % 9.43/9.62 # There were 2 total successful branch saturations. % 9.43/9.62 # There were 0 successful branch saturations in interreduction. % 9.43/9.62 # There were 0 successful branch saturations on the branch. % 9.43/9.62 # There were 2 successful branch saturations after the branch. % 9.43/9.62 # SZS status Theorem for /export/starexec/sandbox/benchmark/theBenchmark.p % 9.43/9.62 # SZS output start for /export/starexec/sandbox/benchmark/theBenchmark.p % 9.43/9.62 # Begin clausification derivation % 9.43/9.62 % 9.43/9.62 # End clausification derivation % 9.43/9.62 # Begin listing active clauses obtained from FOF to CNF conversion % 9.43/9.62 cnf(i_0_2, negated_conjecture, (mtvisible(c_tptp_spindlecollectormt))). % 9.43/9.62 cnf(i_0_179, plain, (mtvisible(c_basekb))). % 9.43/9.62 cnf(i_0_321, plain, (firstordercollection(c_organization))). % 9.43/9.62 cnf(i_0_305, plain, (firstordercollection(c_situation))). % 9.43/9.62 cnf(i_0_201, plain, (firstordercollection(c_tptpcol_14_8433))). % 9.43/9.62 cnf(i_0_516, plain, (firstordercollection(c_tptpcol_16_9110))). % 9.43/9.62 cnf(i_0_1166, plain, (kbdependentcollection(c_inducedformulatemplate))). % 9.43/9.62 cnf(i_0_714, plain, (microtheory(c_tptpgeo_member5_mt))). % 9.43/9.62 cnf(i_0_713, plain, (microtheory(c_hpkbvocabmt))). % 9.43/9.62 cnf(i_0_715, plain, (microtheory(c_tptpgeo_member8_mt))). % 9.43/9.62 cnf(i_0_1660, plain, (existingobjecttype(c_stream))). % 9.43/9.62 cnf(i_0_569, plain, (existingobjecttype(c_footballteam))). % 9.43/9.62 cnf(i_0_1641, plain, (existingobjecttype(c_ditch))). % 9.43/9.62 cnf(i_0_797, plain, (atemporalnecessarilyessentialcollectiontype(c_positiveinteger))). % 9.43/9.62 cnf(i_0_799, plain, (atemporalnecessarilyessentialcollectiontype(c_genericquantity))). % 9.43/9.62 cnf(i_0_1603, plain, (existingstufftype(c_ediblestuff))). % 9.43/9.62 cnf(i_0_503, plain, (binarypredicate(c_tptp_6_72))). % 9.43/9.62 cnf(i_0_1083, plain, (reflexivebinarypredicate(c_genls))). % 9.43/9.62 cnf(i_0_1587, plain, (actorslot(c_wasteproducts))). % 9.43/9.62 cnf(i_0_1091, plain, (predicate(c_genls))). % 9.43/9.62 cnf(i_0_634, plain, (conceptnodesfortasktypefnintelligenceanalysistask_allotment(c_kidnappingsomeone))). % 9.43/9.62 cnf(i_0_1418, plain, (artifacttypebygenericcategory(c_weapon))). % 9.43/9.62 cnf(i_0_1554, plain, (coexistingobjectspredicate(c_eventoccursat))). % 9.43/9.62 cnf(i_0_1553, plain, (coexistingobjectspredicate(c_hasadministrators))). % 9.43/9.62 cnf(i_0_1557, plain, (coexistingobjectspredicate(c_wearsclothing))). % 9.43/9.62 cnf(i_0_1551, plain, (coexistingobjectspredicate(c_organizationhead))). % 9.43/9.62 cnf(i_0_448, plain, (coexistingobjectspredicate(c_fatherinlaw))). % 9.43/9.62 cnf(i_0_458, plain, (coexistingobjectspredicate(c_sisterinlaw))). % 9.43/9.62 cnf(i_0_1552, plain, (coexistingobjectspredicate(c_agricultureminister))). % 9.43/9.62 cnf(i_0_1555, plain, (coexistingobjectspredicate(c_teammates))). % 9.43/9.62 cnf(i_0_1111, plain, (durativeeventtype(c_selectingsomething))). % 9.43/9.62 cnf(i_0_1085, plain, (nonabduciblepredicate(c_genls))). % 9.43/9.62 cnf(i_0_1092, plain, (transitivebinarypredicate(c_genls))). % 9.43/9.62 cnf(i_0_1086, plain, (rulemacropredicate(c_genls))). % 9.43/9.62 cnf(i_0_1526, plain, (antisymmetricbinarypredicate(c_objectsides))). % 9.43/9.62 cnf(i_0_1528, plain, (antisymmetricbinarypredicate(c_constituents))). % 9.43/9.62 cnf(i_0_1527, plain, (antisymmetricbinarypredicate(c_subsituations))). % 9.43/9.62 cnf(i_0_1535, plain, (antisymmetricbinarypredicate(c_externalparts))). % 9.43/9.62 cnf(i_0_1534, plain, (antisymmetricbinarypredicate(c_quantitysubsumes))). % 9.43/9.62 cnf(i_0_1532, plain, (antisymmetricbinarypredicate(c_armedwithweapon))). % 9.43/9.62 cnf(i_0_1533, plain, (antisymmetricbinarypredicate(c_represents))). % 9.43/9.62 cnf(i_0_464, plain, (objectpredicate(c_tasteofobject))). % 9.43/9.62 cnf(i_0_1615, plain, (objectpredicate(c_specialtyofunit))). % 9.43/9.62 cnf(i_0_1089, plain, (defaultmonotonicpredicate(c_genls))). % 9.43/9.62 cnf(i_0_1595, plain, (personalassociationpredicate(c_hasassistants))). % 9.43/9.62 cnf(i_0_1594, plain, (personalassociationpredicate(c_grandmothers))). % 9.43/9.62 cnf(i_0_1592, plain, (personalassociationpredicate(c_grandchildren))). % 9.43/9.62 cnf(i_0_459, plain, (personalassociationpredicate(c_sisterinlaw))). % 9.43/9.62 cnf(i_0_1593, plain, (personalassociationpredicate(c_boss))). % 9.43/9.62 cnf(i_0_1610, plain, (clarifyingcollectiontype(c_taste))). % 9.43/9.62 cnf(i_0_26, plain, (genlmt(c_tptp_spindlecollectormt,c_basekb))). % 9.43/9.62 cnf(i_0_56, plain, (genlmt(c_tptp_spindlecollectormt,c_tptp_member2668_mt))). % 9.43/9.62 cnf(i_0_395, plain, (genls(c_geographicalregion,c_partiallytangible))). % 9.43/9.62 cnf(i_0_658, plain, (firstordercollection(f_planningfn(c_murder)))). % 9.43/9.62 cnf(i_0_1605, plain, (genls(c_ediblestuff,c_partiallytangible))). % 9.43/9.62 cnf(i_0_18, plain, (genls(f_groupfn(c_partiallytangible),c_partiallytangible))). % 9.43/9.62 cnf(i_0_267, plain, (individual(f_contextofpcwfn(c_lscomobjectandsituationontology)))). % 9.43/9.62 cnf(i_0_264, plain, (individual(f_the(c_situation)))). % 9.43/9.62 cnf(i_0_1320, plain, (individual(f_armyfn(c_albania)))). % 9.43/9.62 cnf(i_0_1372, plain, (individual(f_armedforcesfn(c_india)))). % 9.43/9.62 cnf(i_0_1327, plain, (individual(f_armedforcesfn(c_iran)))). % 9.43/9.62 cnf(i_0_1371, plain, (individual(f_armedforcesfn(c_saudiarabia)))). % 9.43/9.62 cnf(i_0_1368, plain, (individual(f_armedforcesfn(c_nepal)))). % 9.43/9.62 cnf(i_0_1167, plain, (kbdependentcollection(f_formulatemplateinductiontopictypefn(c_airport_physical)))). % 9.43/9.62 cnf(i_0_959, plain, (temporalstufftype(f_conveyfn(c_militaryperson)))). % 9.43/9.62 cnf(i_0_1016, plain, (spatiallydisjointobjecttype(f_freethingoftypefn(c_currency)))). % 9.43/9.62 cnf(i_0_1485, plain, (spatiallydisjointobjecttype(f_toyversionfn(c_automobile)))). % 9.43/9.62 cnf(i_0_1667, plain, (existingobjecttype(f_intermittentbodyofwaterfn(c_stream)))). % 9.43/9.62 cnf(i_0_277, plain, (atemporalnecessarilyessentialcollectiontype(f_setoftypefn(c_collection)))). % 9.43/9.62 cnf(i_0_145, plain, (collection(f_groupfn(c_homosapiens)))). % 9.43/9.62 cnf(i_0_300, plain, (collection(f_transportviafn(c_homosapiens)))). % 9.43/9.62 cnf(i_0_1340, plain, (collection(f_unitofmoneyofgeopoliticalentityfn(c_spain)))). % 9.43/9.62 cnf(i_0_725, plain, (collection(f_listoftypefn(c_set_mathematical)))). % 9.43/9.62 cnf(i_0_726, plain, (collection(f_listoftypefn(c_propernamestring)))). % 9.43/9.62 cnf(i_0_731, plain, (collection(f_listoftypefn(c_cyclsentence)))). % 9.43/9.62 cnf(i_0_655, plain, (collection(f_unsatisfactoryattempttofn(c_murder)))). % 9.43/9.62 cnf(i_0_621, plain, (collection(f_citizenfn(c_france)))). % 9.43/9.62 cnf(i_0_620, plain, (collection(f_citizenfn(c_turkey)))). % 9.43/9.62 cnf(i_0_1101, plain, (collection(f_programrepresentationfn(c_date)))). % 9.43/9.62 cnf(i_0_1435, plain, (collection(f_sharesinfundtypefn(c_hedgefund)))). % 9.43/9.62 cnf(i_0_542, plain, (setorcollection(f_makingavailablefn(c_humanresidence)))). % 9.43/9.62 cnf(i_0_859, plain, (skilledactivitytype(f_transportviafn(c_automobile)))). % 9.43/9.62 cnf(i_0_1184, plain, (skilledactivitytype(f_treatmentfn(c_ailmentcondition)))). % 9.43/9.62 cnf(i_0_1244, plain, (inducedformulatemplatetopictype(f_formulatemplateinductiontopictypefn(c_bodyofwater)))). % 9.43/9.62 cnf(i_0_1479, plain, (artifacttypebygenericcategory(f_toyversionfn(c_automobile)))). % 9.43/9.62 cnf(i_0_1414, plain, (cyclqueryspecification(f_literalbuilderqueryfn(c_hasbeliefsystems)))). % 9.43/9.62 cnf(i_0_1021, plain, (cyclqueryspecification(f_literalbuilderqueryfn(c_suborganizations)))). % 9.43/9.62 cnf(i_0_460, plain, (relation(f_presenttenseversionfn(c_eventoccursat)))). % 9.43/9.62 cnf(i_0_1443, plain, (firstordercollection(f_sharesinfundtypefn(X1)))). % 9.43/9.62 cnf(i_0_225, plain, (thing(X1))). % 9.43/9.62 cnf(i_0_252, plain, (individual(f_territoryfn(X1)))). % 9.43/9.62 cnf(i_0_1317, plain, (temporalstufftype(f_memberfn(X1)))). % 9.43/9.62 cnf(i_0_1204, plain, (temporalstufftype(f_exposureoforganismtoharmfulsubstancefn(X1)))). % 9.43/9.62 cnf(i_0_1191, plain, (temporalstufftype(f_treatmentfn(X1)))). % 9.43/9.62 cnf(i_0_269, plain, (microtheory(f_contextofpcwfn(X1)))). % 9.43/9.62 cnf(i_0_270, plain, (wordnetsynset(f_wordnetsynsetreifiedfn(X1)))). % 9.43/9.62 cnf(i_0_245, plain, (existingobjecttype(f_rightobjectofpairfn(X1)))). % 9.43/9.62 cnf(i_0_244, plain, (existingobjecttype(f_leftobjectofpairfn(X1)))). % 9.43/9.62 cnf(i_0_801, plain, (atemporalnecessarilyessentialcollectiontype(f_stringofmaximumlengthfn(X1)))). % 9.43/9.62 cnf(i_0_800, plain, (atemporalnecessarilyessentialcollectiontype(f_interagentsupporttypefn(X1)))). % 9.43/9.62 cnf(i_0_618, plain, (temporalobjecttype(f_endingfn(X1)))). % 9.43/9.62 cnf(i_0_617, plain, (temporalobjecttype(f_makingfn(X1)))). % 9.43/9.62 cnf(i_0_614, plain, (temporalobjecttype(f_buyingfn(X1)))). % 9.43/9.62 cnf(i_0_615, plain, (temporalobjecttype(f_playingfn(X1)))). % 9.43/9.62 cnf(i_0_850, plain, (existingstufftype(f_meatfn(X1)))). % 9.43/9.62 cnf(i_0_845, plain, (existingstufftype(f_stufffn(X1)))). % 9.43/9.62 cnf(i_0_848, plain, (existingstufftype(f_mobfn(X1)))). % 9.43/9.62 cnf(i_0_847, plain, (existingstufftype(f_woodfn(X1)))). % 9.43/9.62 cnf(i_0_739, plain, (collection(f_setoftypefn(X1)))). % 9.43/9.62 cnf(i_0_155, plain, (objecttype(f_groupfn(X1)))). % 9.43/9.62 cnf(i_0_262, plain, (objecttype(f_mapfn_individual(X1)))). % 9.43/9.62 cnf(i_0_318, plain, (objecttype(f_jobfn(X1)))). % 9.43/9.62 cnf(i_0_317, plain, (objecttype(f_freethingoftypefn(X1)))). % 9.43/9.62 cnf(i_0_316, plain, (objecttype(f_marketedproductofcwfn(X1)))). % 9.43/9.62 cnf(i_0_1014, plain, (manufacturedgoodstype(f_marketedproductofcwfn(X1)))). % 9.43/9.62 cnf(i_0_1558, plain, (coexistingobjectspredicate(f_presenttenseversionfn(X1)))). % 9.43/9.62 cnf(i_0_1496, plain, (scalarproperinterval(f_highamountfn(X1)))). % 9.43/9.62 cnf(i_0_1495, plain, (scalarquantity(f_highamountfn(X1)))). % 9.43/9.62 cnf(i_0_1497, plain, (genericquantity(f_highamountfn(X1)))). % 9.43/9.62 cnf(i_0_170, plain, (genlmt(c_englishmt,c_basekb))). % 9.43/9.62 cnf(i_0_174, plain, (genlmt(c_currentworlddatacollectormt_nonhomocentric,c_basekb))). % 9.43/9.62 cnf(i_0_169, plain, (genlmt(c_machinelearningspindleheadmt,c_basekb))). % 9.43/9.62 cnf(i_0_1686, plain, (genlmt(c_organizationdatamt,c_peopledatamt))). % 9.43/9.62 cnf(i_0_167, plain, (genlmt(c_generallexiconmt,c_basekb))). % 9.43/9.62 cnf(i_0_1687, plain, (genlmt(c_peopledatamt,c_basekb))). % 9.43/9.62 cnf(i_0_1689, plain, (genlmt(c_peopledatamt,c_organizationdatamt))). % 9.43/9.62 cnf(i_0_1691, plain, (genlmt(c_peopledatamt,c_literarypeopledatamt))). % 9.43/9.62 cnf(i_0_1549, plain, (genlmt(c_peopledatamt,c_humansociallifemt))). % 9.43/9.62 cnf(i_0_176, plain, (genlmt(c_cyclistsmt,c_basekb))). % 9.43/9.62 cnf(i_0_478, plain, (genlmt(c_cyclistsmt,c_peopledatamt))). % 9.43/9.62 cnf(i_0_177, plain, (genlmt(c_worldgeographymt,c_basekb))). % 9.43/9.62 cnf(i_0_532, plain, (genlmt(c_gafgatheringlogmt,c_basekb))). % 9.43/9.62 cnf(i_0_218, plain, (genlmt(c_gafgatheringlogmt,c_currentworlddatacollectormt_nonhomocentric))). % 9.43/9.62 cnf(i_0_533, plain, (genlmt(c_gafgatheringlogmt,c_cycnounlearnermt))). % 9.43/9.62 cnf(i_0_1693, plain, (genlmt(c_bookkeepingmt,c_basekb))). % 9.43/9.62 cnf(i_0_479, plain, (genlmt(c_bookkeepingmt,c_cyclistsmt))). % 9.43/9.62 cnf(i_0_1690, plain, (genlmt(c_massmediadatamt,c_peopledatamt))). % 9.43/9.62 cnf(i_0_178, plain, (genlmt(c_computersoftwaredatamt,c_basekb))). % 9.43/9.62 cnf(i_0_1253, plain, (genlmt(c_sensusmappingmt,c_basekb))). % 9.43/9.62 cnf(i_0_175, plain, (genlmt(c_tptp_spindleheadmt,c_basekb))). % 9.43/9.62 cnf(i_0_204, plain, (genlmt(c_tptp_spindleheadmt,c_cyclistsmt))). % 9.43/9.62 cnf(i_0_1695, plain, (genlmt(c_unitedstatesgeographymt,c_basekb))). % 9.43/9.62 cnf(i_0_480, plain, (genlmt(c_unitedstatesgeographymt,c_worldgeographymt))). % 9.43/9.62 cnf(i_0_1658, plain, (genlmt(c_topicmt,c_basekb))). % 9.43/9.62 cnf(i_0_1575, plain, (genlmt(c_productgmt,c_basekb))). % 9.43/9.62 cnf(i_0_1692, plain, (genlmt(c_ldscgeneralcollectormt,c_peopledatamt))). % 9.43/9.62 cnf(i_0_1688, plain, (genlmt(c_hpkbvocabmt,c_peopledatamt))). % 9.43/9.62 cnf(i_0_1543, plain, (genlmt(c_humansociallifemt,c_basekb))). % 9.43/9.62 cnf(i_0_1542, plain, (genlmt(c_humansociallifemt,c_humanactivitiesmt))). % 9.43/9.62 cnf(i_0_1507, plain, (genlmt(c_biologymt,c_basekb))). % 9.43/9.62 cnf(i_0_841, plain, (genlmt(c_geographicalregiongmt,c_basekb))). % 9.43/9.62 cnf(i_0_55, plain, (genlmt(c_tptp_member2668_mt,c_basekb))). % 9.43/9.62 cnf(i_0_319, plain, (genls(c_militaryorganization,c_organization))). % 9.43/9.62 cnf(i_0_380, plain, (genls(c_individual,c_thing))). % 9.43/9.62 cnf(i_0_1055, plain, (genls(c_artifact,c_artifact_generic))). % 9.43/9.62 cnf(i_0_413, plain, (genls(c_intelligentagent,c_agent_generic))). % 9.43/9.62 cnf(i_0_274, plain, (genls(c_collection,c_thing))). % 9.43/9.62 cnf(i_0_1233, plain, (genls(c_enduringthing_localized,c_spatialthing_localized))). % 9.43/9.62 cnf(i_0_1173, plain, (genls(c_microtheory,c_aspatialinformationstore))). % 9.43/9.62 cnf(i_0_399, plain, (genls(c_geographicalregion,c_place))). % 9.43/9.62 cnf(i_0_985, plain, (genls(c_adultfemalehuman,c_femalehuman))). % 9.43/9.62 cnf(i_0_180, plain, (genls(c_tptpcol_4_8195,c_tptpcol_3_3))). % 9.43/9.62 cnf(i_0_481, plain, (genls(c_tptpcol_3_3,c_tptpcol_2_2))). % 9.43/9.62 cnf(i_0_1404, plain, (genls(c_femalehuman,c_femaleanimal))). % 9.43/9.62 cnf(i_0_660, plain, (genls(c_contractmurder,c_murder))). % 9.43/9.62 cnf(i_0_1259, plain, (genls(c_place,c_enduringthing_localized))). % 9.43/9.62 cnf(i_0_1270, plain, (genls(c_place,c_location_underspecified))). % 9.43/9.62 cnf(i_0_1572, plain, (genls(c_buyingwhileonatrip,c_purposefulaction))). % 9.43/9.62 cnf(i_0_1128, plain, (genls(c_temporalthing,c_individual))). % 9.43/9.62 cnf(i_0_1052, plain, (genls(c_constructionartifact,c_artifact))). % 9.43/9.62 cnf(i_0_398, plain, (genls(c_ruralarea,c_geographicalregion))). % 9.43/9.62 cnf(i_0_942, plain, (genls(c_soldier,c_militaryperson))). % 9.43/9.62 cnf(i_0_1566, plain, (genls(c_sexualbehavior,c_purposefulaction))). % 9.43/9.62 cnf(i_0_1115, plain, (genls(c_selectingsomething,c_purposefulaction))). % 9.43/9.62 cnf(i_0_1113, plain, (genls(c_selectingsomething,c_humanactivity))). % 9.43/9.62 cnf(i_0_1258, plain, (genls(c_geographicalplace,c_place))). % 9.43/9.62 cnf(i_0_1155, plain, (genls(c_investing,c_buying))). % 9.43/9.62 cnf(i_0_1625, plain, (genls(c_drycreekbed,c_landtopographicalfeature))). % 9.43/9.62 cnf(i_0_1175, plain, (genls(c_propositionalinformationthing,c_microtheory))). % 9.43/9.62 cnf(i_0_1042, plain, (genls(c_crewmemberonship,c_personwithoccupation))). % 9.43/9.62 cnf(i_0_1607, plain, (genls(c_raw,c_ediblestuff))). % 9.43/9.62 cnf(i_0_1567, plain, (disjointwith(c_purposefulaction,c_accident))). % 9.43/9.62 cnf(i_0_273, plain, (disjointwith(c_collection,c_individual))). % 9.43/9.62 cnf(i_0_1241, plain, (disjointwith(c_bodyofwater,c_facility_construct))). % 9.43/9.62 cnf(i_0_397, plain, (disjointwith(c_geographicalregion,c_militaryorganization))). % 9.43/9.62 cnf(i_0_208, plain, (disjointwith(c_tptpcol_16_9110,c_tptpcol_16_9111))). % 9.43/9.62 cnf(i_0_1134, plain, (arg2isa(c_outputscreated,c_somethingexisting))). % 9.43/9.62 cnf(i_0_284, plain, (arg2isa(c_employees,c_person))). % 9.43/9.62 cnf(i_0_1271, plain, (arg2isa(c_residesinregion,c_place))). % 9.43/9.62 cnf(i_0_1082, plain, (arg2isa(c_genls,c_collection))). % 9.43/9.62 cnf(i_0_1075, plain, (arg2isa(c_grandchildren,c_animal))). % 9.43/9.62 cnf(i_0_184, plain, (arg2isa(c_tptp_8_625,c_tptpcol_4_8195))). % 9.43/9.62 cnf(i_0_215, plain, (hlprototypicalinstance(c_theprototypicaltptpcol_15_8510,c_tptpcol_15_8510))). % 9.43/9.62 cnf(i_0_386, plain, (arg1isa(c_objectfoundinlocation,c_spatialthing_localized))). % 9.43/9.62 cnf(i_0_1044, plain, (arg1isa(c_domainsofspecialization,c_personwithoccupation))). % 9.43/9.62 cnf(i_0_1081, plain, (arg1isa(c_genls,c_collection))). % 9.43/9.62 cnf(i_0_322, plain, (arg1isa(c_suborganizations,c_organization))). % 9.43/9.62 cnf(i_0_1170, plain, (arg1isa(c_objectactedon,c_event))). % 9.43/9.62 cnf(i_0_1078, plain, (arg1isa(c_grandchildren,c_animal))). % 9.43/9.62 cnf(i_0_1448, plain, (arg1isa(c_seller,c_monetaryexchangeofuserrights))). % 9.43/9.62 cnf(i_0_1122, plain, (arg1isa(c_groupmembers,c_group))). % 9.43/9.62 cnf(i_0_182, plain, (arg1isa(c_tptp_9_495,c_tptpcol_4_8195))). % 9.43/9.62 cnf(i_0_1133, plain, (genlpreds(c_outputscreated,c_possessiverelation))). % 9.43/9.62 cnf(i_0_1408, plain, (genlpreds(c_wife,c_spouse))). % 9.43/9.62 cnf(i_0_1020, plain, (genlpreds(c_suborganizations,c_affiliatedwith))). % 9.43/9.62 cnf(i_0_495, plain, (genlpreds(c_tptptypes_6_818,c_tptptypes_5_802))). % 9.43/9.62 cnf(i_0_496, plain, (genlpreds(c_tptptypes_7_819,c_tptptypes_6_818))). % 9.43/9.62 cnf(i_0_456, plain, (genlpreds(c_wasteproducts,c_byproducts))). % 9.43/9.62 cnf(i_0_686, plain, (arity(c_citizens,n_2))). % 9.43/9.62 cnf(i_0_1431, plain, (arity(c_armedwithweapontype,n_2))). % 9.43/9.62 cnf(i_0_1465, plain, (arity(c_seller,n_2))). % 9.43/9.62 cnf(i_0_504, plain, (arity(c_tptp_6_72,n_2))). % 9.43/9.62 cnf(i_0_1457, plain, (negationpreds(c_performedby,c_instrument_generic))). % 9.43/9.62 cnf(i_0_1458, plain, (negationpreds(c_lowamountof,c_hightoveryhighamountof))). % 9.43/9.62 cnf(i_0_435, plain, (negationpreds(c_buyer,c_seller))). % 9.43/9.62 cnf(i_0_1456, plain, (negationpreds(c_passengers,c_driveractor))). % 9.43/9.62 cnf(i_0_1094, plain, (typegenls(c_firstordercollection,c_individual))). % 9.43/9.62 cnf(i_0_1037, plain, (typegenls(c_persontypebyoccupation,c_personwithoccupation))). % 9.43/9.62 cnf(i_0_490, plain, (arg2genl(c_isa,c_thing))). % 9.43/9.62 cnf(i_0_489, plain, (arg2genl(c_ethnicity,c_person))). % 9.43/9.62 cnf(i_0_408, plain, (arg2genl(c_membertypes,c_agent_generic))). % 9.43/9.62 cnf(i_0_181, plain, (arg2genl(c_tptptypes_6_818,c_tptpcol_4_8195))). % 9.43/9.62 cnf(i_0_1499, plain, (arg2format(c_isa,c_settheformat))). % 9.43/9.62 cnf(i_0_1500, plain, (arg2format(c_objectcontrolled,c_settheformat))). % 9.43/9.62 cnf(i_0_1498, plain, (arg2format(c_conceptuallyrelated,c_settheformat))). % 9.43/9.62 cnf(i_0_1112, plain, (requiredarg1pred(c_selectingsomething,c_choices))). % 9.43/9.62 cnf(i_0_501, plain, (genlinverse(c_tptp_9_495,c_tptp_8_625))). % 9.43/9.62 cnf(i_0_236, plain, (isa(X1,c_thing))). % 9.43/9.62 cnf(i_0_1664, plain, (genls(f_groupfn(c_stream),c_partiallytangible))). % 9.43/9.62 cnf(i_0_1420, plain, (genls(f_groupfn(c_weapon),c_partiallytangible))). % 9.43/9.62 cnf(i_0_1621, plain, (genls(f_groupfn(c_drycreekbed),c_partiallytangible))). % 9.43/9.62 cnf(i_0_1666, plain, (genls(f_intermittentbodyofwaterfn(c_stream),c_partiallytangible))). % 9.43/9.62 cnf(i_0_633, plain, (isa(c_kidnappingsomeone,f_conceptnodesfortasktypefn(c_intelligenceanalysistask_allotment)))). % 9.43/9.62 cnf(i_0_502, plain, (arg1isa(c_tptp_6_72,f_endingfn(c_era)))). % 9.43/9.62 cnf(i_0_454, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_partiallytangible,c_byproducts,c_purposefulaction),c_partiallytangible))). % 9.43/9.62 cnf(i_0_268, plain, (genlmt(f_contextofpcwfn(c_lscomobjectandsituationontology),c_basekb))). % 9.43/9.62 cnf(i_0_265, plain, (genlmt(f_contextofpcwfn(c_motleyfoolukfoolishglossary),c_basekb))). % 9.43/9.62 cnf(i_0_1172, plain, (genlmt(f_the(c_microtheory),c_basekb))). % 9.43/9.62 cnf(i_0_1243, plain, (genls(f_formulatemplateinductiontopictypefn(c_bodyofwater),c_inducedformulatemplate))). % 9.43/9.62 cnf(i_0_149, plain, (genls(f_groupfn(c_thencmodifier),c_individual))). % 9.43/9.62 cnf(i_0_1140, plain, (genls(f_groupfn(c_communicationdevice),c_group))). % 9.43/9.62 cnf(i_0_1145, plain, (genls(f_groupfn(c_bill_currency),c_group))). % 9.43/9.62 cnf(i_0_1149, plain, (genls(f_groupfn(c_stoneobject_natural),c_group))). % 9.43/9.62 cnf(i_0_1147, plain, (genls(f_groupfn(c_protectiveattire),c_group))). % 9.43/9.62 cnf(i_0_1142, plain, (genls(f_groupfn(c_computeraccount),c_group))). % 9.43/9.62 cnf(i_0_1151, plain, (genls(f_groupfn(c_militaryequipment),c_group))). % 9.43/9.62 cnf(i_0_1148, plain, (genls(f_groupfn(c_populatedplace),c_group))). % 9.43/9.62 cnf(i_0_1144, plain, (genls(f_groupfn(c_island),c_group))). % 9.43/9.62 cnf(i_0_1146, plain, (genls(f_groupfn(c_electronicdevice),c_group))). % 9.43/9.62 cnf(i_0_1150, plain, (genls(f_groupfn(c_sudanperson),c_group))). % 9.43/9.62 cnf(i_0_1143, plain, (genls(f_groupfn(c_ballisticmissile),c_group))). % 9.43/9.62 cnf(i_0_1568, plain, (genls(f_killingbymeansoffn(c_gun),c_purposefulaction))). % 9.43/9.62 cnf(i_0_591, plain, (genls(f_residentfn(c_israel),c_individual))). % 9.43/9.62 cnf(i_0_1325, plain, (genls(f_residentfn(c_iran),c_individual))). % 9.43/9.62 cnf(i_0_1337, plain, (genls(f_residentfn(c_spain),c_individual))). % 9.43/9.62 cnf(i_0_552, plain, (genls(f_residentfn(c_unitedstatesofamerica),c_individual))). % 9.43/9.62 cnf(i_0_917, plain, (genls(f_residentfn(c_iraq),c_individual))). % 9.43/9.62 cnf(i_0_1350, plain, (genls(f_residentfn(c_turkey),c_individual))). % 9.43/9.62 cnf(i_0_724, plain, (genls(f_listoftypefn(c_thing),c_list))). % 9.43/9.62 cnf(i_0_733, plain, (genls(f_listoftypefn(c_realnumber),c_list))). % 9.43/9.62 cnf(i_0_728, plain, (genls(f_listoftypefn(c_setorcollection),c_list))). % 9.43/9.62 cnf(i_0_1156, plain, (genls(f_buyingfn(c_commercialorganization),c_buying))). % 9.43/9.62 cnf(i_0_1161, plain, (genls(f_buyingfn(c_house_modern),c_buying))). % 9.43/9.62 cnf(i_0_376, plain, (genls(f_exposureoforganismtoharmfulsubstancefn(c_thencmodifier),c_individual))). % 9.43/9.62 cnf(i_0_944, plain, (genls(f_conveyfn(c_militaryperson),c_conveyingmaterials))). % 9.43/9.62 cnf(i_0_366, plain, (genls(f_playingfn(c_thencmodifier),c_temporalthing))). % 9.43/9.62 cnf(i_0_1054, plain, (genls(f_accessoryfn_activity(c_climbing),c_artifact))). % 9.43/9.62 cnf(i_0_368, plain, (genls(f_treatmentfn(c_thencmodifier),c_individual))). % 9.43/9.62 cnf(i_0_1189, plain, (genls(f_treatmentfn(c_cancer),c_medicaltreatmentevent))). % 9.43/9.62 cnf(i_0_625, plain, (genls(f_citizenfn(c_canada),c_person))). % 9.43/9.62 cnf(i_0_1053, plain, (genls(f_accessoryfn_artifact(c_computer),c_artifact))). % 9.43/9.62 cnf(i_0_1056, plain, (genls(f_accessoryfn_artifact(c_telephone),c_artifact))). % 9.43/9.62 cnf(i_0_1441, plain, (genls(f_sharesinfundtypefn(c_unittrust),c_authorizedagreement))). % 9.43/9.62 cnf(i_0_1130, plain, (arg2isa(f_inversebinarypredicatefn(c_temporallysubsumes),c_temporalthing))). % 9.43/9.62 cnf(i_0_970, plain, (genlpreds(f_orgpositionslotfn(c_soldier),c_hasmembers))). % 9.43/9.62 cnf(i_0_1601, plain, (arity(f_presenttenseversionfn(c_doneby),n_2))). % 9.43/9.62 cnf(i_0_1047, plain, (arity(f_presenttenseversionfn(c_performedby),n_2))). % 9.43/9.62 cnf(i_0_488, plain, (arg2genl(f_inversebinarypredicatefn(c_genls),c_thing))). % 9.43/9.62 cnf(i_0_1087, plain, (genlinverse(f_inversebinarypredicatefn(c_genls),c_genls))). % 9.43/9.62 cnf(i_0_1417, plain, (firstordercollection(f_attemptingfn(f_smugglingfn(c_weapon))))). % 9.43/9.62 cnf(i_0_1223, plain, (individual(f_templatefromtestqueryfn(f_relationinstanceexistsbuilderqueryfn(c_operatesfacilities))))). % 9.43/9.62 cnf(i_0_1003, plain, (temporalstufftype(f_preventingfn(f_killingfn(c_civilian))))). % 9.43/9.62 cnf(i_0_1285, plain, (collection(f_memberfn(f_airforcefn(c_afghanistan))))). % 9.43/9.62 cnf(i_0_1283, plain, (collection(f_memberfn(f_armedforcesfn(c_albania))))). % 9.43/9.62 cnf(i_0_1284, plain, (collection(f_memberfn(f_armedforcesfn(c_italy))))). % 9.43/9.62 cnf(i_0_1304, plain, (collection(f_memberfn(f_armedforcesfn(c_afghanistan))))). % 9.43/9.62 cnf(i_0_1293, plain, (collection(f_memberfn(f_armedforcesfn(c_netherlands))))). % 9.43/9.62 cnf(i_0_1286, plain, (collection(f_memberfn(f_armedforcesfn(c_jordan_thenation))))). % 9.43/9.62 cnf(i_0_1301, plain, (collection(f_memberfn(f_armedforcesfn(c_unionofsovietsocialistrepublics))))). % 9.43/9.62 cnf(i_0_1312, plain, (collection(f_memberfn(f_navyfn(c_russia))))). % 9.43/9.62 cnf(i_0_1202, plain, (collection(f_exposureoforganismtoharmfulsubstancefn(f_liquidfn(c_cyanide))))). % 9.43/9.62 cnf(i_0_1106, plain, (inducedformulatemplatetopictype(f_formulatemplateinductiontopictypefn(f_specsfn(c_selectingsomething))))). % 9.43/9.62 cnf(i_0_1026, plain, (formulatemplate(f_templatefromtestqueryfn(f_literalbuilderqueryfn(c_membertypes))))). % 9.43/9.62 cnf(i_0_410, plain, (resultgenl(f_memberfn(X1),c_agent_generic))). % 9.43/9.62 cnf(i_0_1343, plain, (resultgenl(f_merchandiserelatedtofn(X1),c_manufacturedgoods))). % 9.43/9.62 cnf(i_0_644, plain, (firstordercollection(f_collectionintersection2fn(c_humanchild,c_israeliperson)))). % 9.43/9.62 cnf(i_0_641, plain, (firstordercollection(f_collectionintersection2fn(c_securityguard,c_israeliperson)))). % 9.43/9.62 cnf(i_0_763, plain, (individual(f_ncgenlsconstraintfn(c_thenchead,c_movement_translationevent)))). % 9.43/9.62 cnf(i_0_762, plain, (individual(f_ncgenlsconstraintfn(c_thenchead,c_informationtransferevent)))). % 9.43/9.62 cnf(i_0_771, plain, (individual(f_ncgenlsconstraintfn(c_thenchead,c_agent_partiallytangible)))). % 9.43/9.62 cnf(i_0_775, plain, (individual(f_ncgenlsconstraintfn(c_thenchead,c_temporallyexistingthing)))). % 9.43/9.62 cnf(i_0_153, plain, (termofunit(f_groupfn(c_agent_generic),f_groupfn(c_agent_generic)))). % 9.43/9.62 cnf(i_0_343, plain, (individual(f_ncgenlsconstraintfn(c_thencmodifier,c_firstordercollection)))). % 9.43/9.62 cnf(i_0_275, plain, (individual(f_ncgenlsconstraintfn(c_thencmodifier,c_collection)))). % 9.43/9.62 cnf(i_0_326, plain, (individual(f_ncgenlsconstraintfn(c_thencmodifier,c_computerprogram_cw)))). % 9.43/9.62 cnf(i_0_776, plain, (individual(f_ncgenlsconstraintfn(c_thencmodifier,c_textualmaterial)))). % 9.43/9.62 cnf(i_0_782, plain, (individual(f_ncgenlsconstraintfn(c_thencmodifier,c_educationalorganization)))). % 9.43/9.62 cnf(i_0_872, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_biologicallivingobject)))). % 9.43/9.62 cnf(i_0_154, plain, (termofunit(f_groupfn(c_intelligentagent),f_groupfn(c_intelligentagent)))). % 9.43/9.62 cnf(i_0_345, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_agent_generic)))). % 9.43/9.62 cnf(i_0_878, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_informationbearingthing)))). % 9.43/9.62 cnf(i_0_369, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_geopoliticalentity)))). % 9.43/9.62 cnf(i_0_353, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_group)))). % 9.43/9.62 cnf(i_0_356, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_buying)))). % 9.43/9.62 cnf(i_0_867, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_airtransportationdevice)))). % 9.43/9.62 cnf(i_0_146, plain, (termofunit(f_groupfn(c_situation),f_groupfn(c_situation)))). % 9.43/9.62 cnf(i_0_869, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_publishedmaterial)))). % 9.43/9.62 cnf(i_0_884, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_informationstore)))). % 9.43/9.62 cnf(i_0_350, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_temporalthing)))). % 9.43/9.62 cnf(i_0_333, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_organism_whole)))). % 9.43/9.62 cnf(i_0_370, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_existingobjecttype)))). % 9.43/9.62 cnf(i_0_882, plain, (individual(f_ncisaconstraintfn(c_thencmodifier,c_agent_partiallytangible)))). % 9.43/9.62 cnf(i_0_984, plain, (termofunit(f_groupfn(c_adultfemalehuman),f_groupfn(c_adultfemalehuman)))). % 9.43/9.62 cnf(i_0_898, plain, (temporalstufftype(f_artifacttypeforusertypefn(c_shirt,c_femalechild)))). % 9.43/9.62 cnf(i_0_907, plain, (spatiallydisjointobjecttype(f_artifacttypeforusertypefn(c_clothingitem,c_femalechild)))). % 9.43/9.62 cnf(i_0_905, plain, (existingobjecttype(f_artifacttypeforusertypefn(c_clothingitem,c_femalechild)))). % 9.43/9.62 cnf(i_0_1010, plain, (existingobjecttype(f_collectionintersection2fn(c_humanchild,c_civilian)))). % 9.43/9.62 cnf(i_0_967, plain, (existingobjecttype(f_collectionintersection2fn(c_soldier,c_frenchperson)))). % 9.43/9.62 cnf(i_0_969, plain, (existingobjecttype(f_collectionintersection2fn(c_soldier,c_britishperson)))). % 9.43/9.62 cnf(i_0_952, plain, (termofunit(f_groupfn(c_militaryperson),f_groupfn(c_militaryperson)))). % 9.43/9.62 cnf(i_0_1009, plain, (existingobjecttype(f_collectionintersection2fn(c_italianperson,c_civilian)))). % 9.43/9.62 cnf(i_0_257, plain, (collection(f_attacktypebytargettypefn(c_murder,c_israeliperson)))). % 9.43/9.62 cnf(i_0_653, plain, (collection(f_attacktypebytargettypefn(c_murder,c_militaryperson)))). % 9.43/9.62 cnf(i_0_1484, plain, (termofunit(f_the(c_automobile),f_the(c_automobile)))). % 9.43/9.62 cnf(i_0_1252, plain, (collection(f_meaninginsystemfn(c_sensus_information1997,s_decomposable_object)))). % 9.43/9.62 cnf(i_0_260, plain, (termofunit(f_mapfn_individual(c_virginia_state),f_mapfn_individual(c_virginia_state)))). % 9.43/9.62 cnf(i_0_315, plain, (objecttype(f_collectionintersection2fn(c_israeliperson,c_civilian)))). % 9.43/9.62 cnf(i_0_645, plain, (objecttype(f_collectionintersection2fn(c_israeliperson,c_diplomat)))). % 9.43/9.62 cnf(i_0_311, plain, (objecttype(f_collectionintersection2fn(c_israeliperson,c_soldier)))). % 9.43/9.62 cnf(i_0_931, plain, (objecttype(f_collectionintersection2fn(c_unitedstatesperson,c_ambassador)))). % 9.43/9.62 cnf(i_0_310, plain, (objecttype(f_collectionintersection2fn(c_militaryperson,c_unitedstatesperson)))). % 9.43/9.62 cnf(i_0_965, plain, (objecttype(f_collectionintersection2fn(c_soldier,c_russianperson)))). % 9.43/9.62 cnf(i_0_1355, plain, (termofunit(f_mapfn_individual(c_turkey),f_mapfn_individual(c_turkey)))). % 9.43/9.62 cnf(i_0_1008, plain, (objecttype(f_collectionintersection2fn(c_srilankanperson,c_civilian)))). % 9.43/9.62 cnf(i_0_640, plain, (setorcollection(f_attacktypebytargettypefn(c_kidnappingsomeone,c_civilian)))). % 9.43/9.62 cnf(i_0_901, plain, (artifacttypebygenericcategory(f_artifacttypeforusertypefn(c_sock,c_femalechild)))). % 9.43/9.62 cnf(i_0_1098, plain, (cyclqueryspecification(f_builderqueryforlogicalfieldtypeofsksfn(c_sageman_entityattribute_ks,c_date)))). % 9.43/9.62 cnf(i_0_1103, plain, (cyclqueryspecification(f_builderqueryforlogicalfieldtypeofsksfn(c_ali_baba_person_ks,c_date)))). % 9.43/9.62 cnf(i_0_851, plain, (termofunit(f_meatfn(c_tuna),f_meatfn(c_tuna)))). % 9.43/9.62 cnf(i_0_852, plain, (termofunit(f_meatfn(c_mammal),f_meatfn(c_mammal)))). % 9.43/9.62 cnf(i_0_856, plain, (termofunit(f_meatfn(c_chicken),f_meatfn(c_chicken)))). % 9.43/9.62 cnf(i_0_251, plain, (termofunit(f_territoryfn(c_israel),f_territoryfn(c_israel)))). % 9.43/9.62 cnf(i_0_1068, plain, (firstordercollection(f_subcollectionbyregionfn(X1,X2)))). % 9.43/9.62 cnf(i_0_1330, plain, (termofunit(f_territoryfn(c_iran),f_territoryfn(c_iran)))). % 9.43/9.62 cnf(i_0_1067, plain, (temporalstufftype(f_subcollectionbyregionfn(X1,X2)))). % 9.43/9.62 cnf(i_0_716, plain, (microtheory(f_contentmtofcdafromeventfn(X1,X2)))). % 9.43/9.62 cnf(i_0_571, plain, (existingobjecttype(f_parttypefn(X1,X2)))). % 9.43/9.62 cnf(i_0_572, plain, (existingobjecttype(f_jointtypebetweenfn(X1,X2)))). % 9.43/9.62 cnf(i_0_570, plain, (existingobjecttype(f_organismparttypefn(X1,X2)))). % 9.43/9.62 cnf(i_0_1473, plain, (existingobjecttype(f_prospectivewrtroleintypefn(X1,X2)))). % 9.43/9.62 cnf(i_0_710, plain, (termofunit(f_territoryfn(c_virginia_state),f_territoryfn(c_virginia_state)))). % 9.43/9.62 cnf(i_0_254, plain, (temporalobjecttype(f_attacktypebytargettypefn(X1,X2)))). % 9.43/9.62 cnf(i_0_119, plain, (collection(f_collectionintersection2fn(X1,X2)))). % 9.43/9.62 cnf(i_0_243, plain, (versionedsoftwareobject(f_softwareversionfn(X1,X2)))). % 9.43/9.62 cnf(i_0_794, plain, (nouncompoundruleconstraint_semantic(f_ncgenlsconstraintfn(X1,X2)))). % 9.43/9.62 cnf(i_0_990, plain, (termofunit(f_territoryfn(c_wisconsin_state),f_territoryfn(c_wisconsin_state)))). % 9.43/9.62 cnf(i_0_895, plain, (nouncompoundruleconstraint_semantic(f_ncisaconstraintfn(X1,X2)))). % 9.43/9.62 cnf(i_0_675, plain, (argisa(c_citizens,n_1,c_geopoliticalentity))). % 9.43/9.62 cnf(i_0_407, plain, (argisa(c_performedby,n_2,c_agent_generic))). % 9.43/9.62 cnf(i_0_672, plain, (argisa(c_annualdeathrate,n_1,c_geopoliticalentity))). % 9.43/9.62 cnf(i_0_1043, plain, (argisa(c_domainsofspecialization,n_1,c_personwithoccupation))). % 9.43/9.62 cnf(i_0_1192, plain, (argisa(c_armedwithweapontype,n_2,c_existingobjecttype))). % 9.43/9.62 cnf(i_0_1030, plain, (termofunit(f_thefn(c_computerprogram_cw),f_thefn(c_computerprogram_cw)))). % 9.43/9.62 cnf(i_0_426, plain, (argisa(c_hasbeliefsystems,n_1,c_intelligentagent))). % 9.43/9.62 cnf(i_0_1234, plain, (argisa(c_maincolorofobject,n_1,c_spatialthing_localized))). % 9.43/9.62 cnf(i_0_1129, plain, (argisa(c_temporallycoexist,n_1,c_temporalthing))). % 9.43/9.62 cnf(i_0_1171, plain, (argisa(c_objectactedon,n_1,c_event))). % 9.43/9.62 cnf(i_0_1028, plain, (argisa(c_programspecifications,n_1,c_computerprogram_cw))). % 9.43/9.62 cnf(i_0_183, plain, (argisa(c_tptp_6_72,n_2,c_tptpcol_4_8195))). % 9.43/9.62 cnf(i_0_1487, plain, (termofunit(f_highamountfn(c_monetaryvalue),f_highamountfn(c_monetaryvalue)))). % 9.43/9.62 cnf(i_0_1039, plain, (arggenl(c_approximatepay,n_1,c_personwithoccupation))). % 9.43/9.62 cnf(i_0_482, plain, (arggenl(c_tptptypes_6_388,n_1,c_tptpcol_3_3))). % 9.43/9.62 cnf(i_0_1205, plain, (argformat(c_parts,n_2,c_settheformat))). % 9.43/9.62 cnf(i_0_1538, plain, (argformat(c_directionoftranslation_throughout,n_1,c_openentryformatinargs))). % 9.43/9.62 cnf(i_0_1413, plain, (argformat(c_hasbeliefsystems,n_2,c_settheformat))). % 9.43/9.62 cnf(i_0_1506, plain, (argformat(c_conceptuallyrelated,n_1,c_settheformat))). % 9.43/9.62 cnf(i_0_1493, plain, (termofunit(f_highamountfn(c_beauty),f_highamountfn(c_beauty)))). % 9.43/9.62 cnf(i_0_1505, plain, (argformat(c_conceptuallyrelated,n_2,c_settheformat))). % 9.43/9.62 cnf(i_0_1084, plain, (transitiveviaarg(c_isa,c_genls,n_2))). % 9.43/9.62 cnf(i_0_854, plain, (genls(f_tastefn(f_meatfn(c_tuna)),c_partiallytangible))). % 9.43/9.62 cnf(i_0_320, plain, (firstordercollection(f_subcollectionofwithrelationfromtypefn(c_organization,c_suborganizations,c_organization)))). % 9.43/9.62 cnf(i_0_418, plain, (firstordercollection(f_subcollectionofwithrelationfromtypefn(c_agent_generic,c_considersasenemy,c_agent_generic)))). % 9.43/9.62 cnf(i_0_991, plain, (firstordercollection(f_subcollectionofwithrelationfromtypefn(c_transportationdevice_vehicle,c_owns,c_army_militaryechelon)))). % 9.43/9.62 cnf(i_0_361, plain, (kbdependentcollection(f_subcollectionofwithrelationfromtypefn(c_thenchead,c_physicalparts,c_thencmodifier)))). % 9.43/9.62 cnf(i_0_737, plain, (termofunit(f_setoftypefn(c_characterstring),f_setoftypefn(c_characterstring)))). % 9.43/9.62 cnf(i_0_1215, plain, (spatiallydisjointobjecttype(f_subcollectionofwithrelationfromtypefn(c_roadvehicle,c_owns,c_regionalgovernment)))). % 9.43/9.62 cnf(i_0_1217, plain, (spatiallydisjointobjecttype(f_subcollectionofwithrelationfromtypefn(c_officespace,c_operatesfacilities,c_regionalgovernment)))). % 9.43/9.62 cnf(i_0_392, plain, (spatiallydisjointobjecttype(f_subcollectionofwithrelationtotypefn(c_partiallytangible,c_objectfoundinlocation,c_bodyofwater)))). % 9.43/9.62 cnf(i_0_1661, plain, (existingobjecttype(f_subcollectionofwithrelationfromtypefn(c_stream,c_anabranches,c_stream)))). % 9.43/9.62 cnf(i_0_384, plain, (existingobjecttype(f_subcollectionofwithrelationfromtypefn(c_building,c_operatesfacilities,c_regionalgovernment)))). % 9.43/9.62 cnf(i_0_1445, plain, (existingobjecttype(f_subcollectionofwithrelationfromtypefn(c_socialbeing,c_seller,c_monetaryexchangeofuserrights)))). % 9.43/9.62 cnf(i_0_735, plain, (termofunit(f_setoftypefn(c_cyclassertion),f_setoftypefn(c_cyclassertion)))). % 9.43/9.62 cnf(i_0_428, plain, (existingobjecttype(f_subcollectionofwithrelationfromtypefn(c_femalehuman,c_wife,c_intelligentagent)))). % 9.43/9.62 cnf(i_0_1216, plain, (existingobjecttype(f_subcollectionofwithrelationfromtypefn(c_officespace,c_operatesfacilities,c_regionalgovernment)))). % 9.43/9.62 cnf(i_0_1624, plain, (existingobjecttype(f_subcollectionofwithrelationfromtypefn(c_flowterrain,c_subpaths,c_drycreekbed)))). % 9.43/9.62 cnf(i_0_1387, plain, (termofunit(f_cityincountryfn(c_india),f_cityincountryfn(c_india)))). % 9.43/9.62 cnf(i_0_1662, plain, (setorcollection(f_subcollectionofwithrelationfromtypefn(c_stream,c_anabranches,c_stream)))). % 9.43/9.62 cnf(i_0_1179, plain, (setorcollection(f_subcollectionofwithrelationfromtypefn(c_brain,c_doneby,c_creationevent)))). % 9.43/9.62 cnf(i_0_1029, plain, (setorcollection(f_subcollectionofwithrelationfromtypefn(c_specification,c_programspecifications,c_computerprogram_cw)))). % 9.43/9.62 cnf(i_0_16, plain, (collection(f_subcollectionofwithrelationfromtypefn(X1,X2,X3)))). % 9.43/9.62 cnf(i_0_389, plain, (genls(f_subcollectionofwithrelationtotypefn(c_partiallytangible,c_objectfoundinlocation,c_bodyofwater),c_partiallytangible))). % 9.43/9.62 cnf(i_0_242, plain, (termofunit(f_cityincountryfn(c_unitedstatesofamerica),f_cityincountryfn(c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_1599, plain, (termofunit(f_presenttenseversionfn(c_transportees),f_presenttenseversionfn(c_transportees)))). % 9.43/9.62 cnf(i_0_1319, plain, (termofunit(f_armyfn(c_saudiarabia),f_armyfn(c_saudiarabia)))). % 9.43/9.62 cnf(i_0_662, plain, (spatiallydisjointobjecttype(f_subcollectionofwithrelationtofn(c_partiallytangible,c_derivedfrom,f_somefn(c_partiallytangible))))). % 9.43/9.62 cnf(i_0_1163, plain, (termofunit(f_attemptingfn(c_buying),f_attemptingfn(c_buying)))). % 9.43/9.62 cnf(i_0_659, plain, (termofunit(f_unsuccessfulattempttofn(c_murder),f_unsuccessfulattempttofn(c_murder)))). % 9.43/9.62 cnf(i_0_1356, plain, (termofunit(f_nationalredcrosssocietyfn(c_turkey),f_nationalredcrosssocietyfn(c_turkey)))). % 9.43/9.62 cnf(i_0_860, plain, (termofunit(f_transportviafn(c_animal),f_transportviafn(c_animal)))). % 9.43/9.62 cnf(i_0_858, plain, (termofunit(f_transportviafn(c_automobile),f_transportviafn(c_automobile)))). % 9.43/9.62 cnf(i_0_1015, plain, (termofunit(f_freethingoftypefn(c_pornographicpicture),f_freethingoftypefn(c_pornographicpicture)))). % 9.43/9.62 cnf(i_0_664, plain, (genls(f_subcollectionofwithrelationtofn(c_partiallytangible,c_derivedfrom,f_somefn(c_partiallytangible)),c_partiallytangible))). % 9.43/9.62 cnf(i_0_1017, plain, (termofunit(f_freethingoftypefn(c_currency),f_freethingoftypefn(c_currency)))). % 9.43/9.62 cnf(i_0_1482, plain, (termofunit(f_makingfn(c_automobile),f_makingfn(c_automobile)))). % 9.43/9.62 cnf(i_0_271, plain, (termofunit(f_listoftypefn(c_collection),f_listoftypefn(c_collection)))). % 9.43/9.62 cnf(i_0_729, plain, (termofunit(f_listoftypefn(c_persontypebyoccupation),f_listoftypefn(c_persontypebyoccupation)))). % 9.43/9.62 cnf(i_0_730, plain, (termofunit(f_listoftypefn(c_predicate),f_listoftypefn(c_predicate)))). % 9.43/9.62 cnf(i_0_1370, plain, (termofunit(f_armedforcesfn(c_france),f_armedforcesfn(c_france)))). % 9.43/9.62 cnf(i_0_1369, plain, (termofunit(f_armedforcesfn(c_unionofsovietsocialistrepublics),f_armedforcesfn(c_unionofsovietsocialistrepublics)))). % 9.43/9.62 cnf(i_0_1476, plain, (termofunit(f_buyingfn(c_toxicsubstance),f_buyingfn(c_toxicsubstance)))). % 9.43/9.62 cnf(i_0_596, plain, (termofunit(f_nationalculturefn(c_israel),f_nationalculturefn(c_israel)))). % 9.43/9.62 cnf(i_0_556, plain, (termofunit(f_nationalculturefn(c_unitedstatesofamerica),f_nationalculturefn(c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_1351, plain, (termofunit(f_nationalculturefn(c_turkey),f_nationalculturefn(c_turkey)))). % 9.43/9.62 cnf(i_0_1354, plain, (termofunit(f_southernregionfn(c_turkey),f_southernregionfn(c_turkey)))). % 9.43/9.62 cnf(i_0_1421, plain, (termofunit(f_conveyfn(c_weapon),f_conveyfn(c_weapon)))). % 9.43/9.62 cnf(i_0_949, plain, (termofunit(f_conveyfn(c_militaryperson),f_conveyfn(c_militaryperson)))). % 9.43/9.62 cnf(i_0_1240, plain, (termofunit(f_repairingfn(c_ship),f_repairingfn(c_ship)))). % 9.43/9.62 cnf(i_0_992, plain, (termofunit(f_repairingfn(c_transportationdevice_vehicle),f_repairingfn(c_transportationdevice_vehicle)))). % 9.43/9.62 cnf(i_0_623, plain, (termofunit(f_citizenfn(c_norway),f_citizenfn(c_norway)))). % 9.43/9.62 cnf(i_0_622, plain, (termofunit(f_citizenfn(c_turkey),f_citizenfn(c_turkey)))). % 9.43/9.62 cnf(i_0_1224, plain, (termofunit(f_relationinstanceexistscountbuilderqueryfn(c_operatesfacilities),f_relationinstanceexistscountbuilderqueryfn(c_operatesfacilities)))). % 9.43/9.62 cnf(i_0_1423, plain, (termofunit(f_smugglingfn(c_weapon),f_smugglingfn(c_weapon)))). % 9.43/9.62 cnf(i_0_1403, plain, (genls(f_groupfn(c_femalehuman),f_groupfn(c_femaleanimal)))). % 9.43/9.62 cnf(i_0_900, plain, (genls(f_groupfn(c_femalechild),f_groupfn(c_person)))). % 9.43/9.62 cnf(i_0_1481, plain, (genls(f_groupfn(c_automobile),f_groupfn(c_transportationdevice)))). % 9.43/9.62 cnf(i_0_1198, plain, (genls(f_exposureoforganismtoharmfulsubstancefn(c_vx_nerveagent),f_exposureoforganismtoharmfulsubstancefn(c_cholinesteraseinhibitingsubstance)))). % 9.43/9.62 cnf(i_0_266, plain, (genlmt(f_contextofpcwfn(f_cycextendedsystemfn(c_lscomobjectandsituationontology)),c_basekb))). % 9.43/9.62 cnf(i_0_980, plain, (genls(f_groupfn(f_groupfn(c_adultfemalehuman)),c_group))). % 9.43/9.62 cnf(i_0_1152, plain, (genls(f_groupfn(f_intermittentbodyofwaterfn(c_pond)),c_group))). % 9.43/9.62 cnf(i_0_1307, plain, (genls(f_memberfn(f_airforcefn(c_pakistan)),c_agent_generic))). % 9.43/9.62 cnf(i_0_1291, plain, (genls(f_memberfn(f_armyfn(c_albania)),c_agent_generic))). % 9.43/9.62 cnf(i_0_406, plain, (genls(f_memberfn(f_armyfn(c_iran)),c_agent_generic))). % 9.43/9.62 cnf(i_0_409, plain, (genls(f_memberfn(f_armyfn(c_spain)),c_agent_generic))). % 9.43/9.62 cnf(i_0_411, plain, (genls(f_memberfn(f_armyfn(c_turkey)),c_agent_generic))). % 9.43/9.62 cnf(i_0_1299, plain, (genls(f_memberfn(f_armyfn(c_afghanistan)),c_agent_generic))). % 9.43/9.62 cnf(i_0_1296, plain, (genls(f_memberfn(f_armedforcesfn(c_germany)),c_agent_generic))). % 9.43/9.62 cnf(i_0_1315, plain, (genls(f_memberfn(f_armedforcesfn(c_italy)),c_agent_generic))). % 9.43/9.62 cnf(i_0_415, plain, (genls(f_memberfn(f_armedforcesfn(c_iraq)),c_agent_generic))). % 9.43/9.62 cnf(i_0_1367, plain, (genls(f_memberfn(f_armedforcesfn(c_portugal)),c_agent_generic))). % 9.43/9.62 cnf(i_0_1288, plain, (genls(f_memberfn(f_navyfn(c_unitedstatesofamerica)),c_agent_generic))). % 9.43/9.62 cnf(i_0_1604, plain, (genls(f_juicefn(f_fruitfn(c_tomatoplant)),c_ediblestuff))). % 9.43/9.62 cnf(i_0_1137, plain, (genls(f_preventingfn(f_productionoffn(c_opium)),c_action))). % 9.43/9.62 cnf(i_0_1439, plain, (genls(f_monitoringoffinancialassettypefn(f_sharesinfundtypefn(c_unittrust)),c_individual))). % 9.43/9.62 cnf(i_0_785, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,c_biologicallivingobject),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_787, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,c_purposefulaction),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_753, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,c_physicaldevice),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_758, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,c_textualmaterial),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_748, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,c_facility_generic),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_767, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,c_physicalpartofobject),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_747, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,c_informationtransferevent),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_1606, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,c_ediblestuff),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_774, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_biologicallivingobject),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_360, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_firstordercollection),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_740, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_stream),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_783, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_informationbearingthing),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_752, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_supportingsomething),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_781, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_facility_generic),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_745, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_solidtangiblething),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_751, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_weddingevent_generic),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_364, plain, (quotedisa(f_ncgenlsconstraintfn(c_thencmodifier,c_creationevent),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_671, plain, (quotedisa(f_ncisaconstraintfn(c_thenchead,c_geopoliticalentity),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_301, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_homosapiens),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_888, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_persontypebyactivity),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_357, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_thenchead),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_363, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_microtheory),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_876, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_textualmaterial),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_352, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_action),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_327, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_personwithoccupation),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_348, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_selectingsomething),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_883, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_informationtransferevent),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_875, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_educationalorganization),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_868, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_monetaryexchangeofuserrights),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_879, plain, (quotedisa(f_ncisaconstraintfn(c_thencmodifier,c_symbolicthing),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_255, plain, (genls(f_attacktypebytargettypefn(c_bombing,c_building),c_bombing))). % 9.43/9.62 cnf(i_0_609, plain, (genls(f_attacktypebytargettypefn(c_bombing,c_militaryperson),c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_1227, plain, (genls(f_attacktypebytargettypefn(c_murder,c_doctor_medical),c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_656, plain, (genls(f_attacktypebytargettypefn(c_murder,c_adultfemalehuman),c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_627, plain, (genls(f_attacktypebytargettypefn(c_kidnappingsomeone,c_humanchild),c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_630, plain, (genls(f_attacktypebytargettypefn(c_kidnappingsomeone,c_publicofficial),c_kidnappingsomeone))). % 9.43/9.62 cnf(i_0_637, plain, (genls(f_attacktypebytargettypefn(c_kidnappingsomeone,c_civilian),c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_631, plain, (genls(f_attacktypebytargettypefn(c_kidnappingsomeone,c_tourist),c_kidnappingsomeone))). % 9.43/9.62 cnf(i_0_635, plain, (genls(f_attacktypebytargettypefn(c_kidnappingsomeone,c_tourist),c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_638, plain, (genls(f_attacktypebytargettypefn(c_kidnappingsomeone,c_jewishperson),c_kidnappingsomeone))). % 9.43/9.62 cnf(i_0_954, plain, (genls(f_attacktypebytargettypefn(c_assassinatingsomeone,c_militaryperson),c_assassinatingsomeone))). % 9.43/9.62 cnf(i_0_957, plain, (genls(f_attacktypebytargettypefn(c_assassinatingsomeone,c_militaryperson),c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_1214, plain, (genls(f_attacktypebytargettypefn(c_terroristattack,c_regionalgovernment),c_terroristattack))). % 9.43/9.62 cnf(i_0_1250, plain, (genls(f_meaninginsystemfn(c_sensus_information1997,s_decomposable_object),c_thing))). % 9.43/9.62 cnf(i_0_1196, plain, (genls(f_exposureoforganismtoharmfulsubstancefn(f_liquidfn(c_vx_nerveagent)),f_exposureoforganismtoharmfulsubstancefn(c_vx_nerveagent)))). % 9.43/9.62 cnf(i_0_649, plain, (genls(f_collectionintersection2fn(c_israeliperson,c_officerinorganization),c_officerinorganization))). % 9.43/9.62 cnf(i_0_986, plain, (genls(f_collectionintersection2fn(c_adultfemalehuman,c_civilian),c_civilian))). % 9.43/9.62 cnf(i_0_936, plain, (genls(f_collectionintersection2fn(c_unitedstatesperson,c_tourist),c_unitedstatesperson))). % 9.43/9.62 cnf(i_0_938, plain, (genls(f_collectionintersection2fn(c_militaryperson,c_unitedstatesperson),c_militaryperson))). % 9.43/9.62 cnf(i_0_646, plain, (genls(f_collectionintersection2fn(c_humanteenager,c_israeliperson),c_israeliperson))). % 9.43/9.62 cnf(i_0_968, plain, (genls(f_collectionintersection2fn(c_soldier,c_russianperson),c_soldier))). % 9.43/9.62 cnf(i_0_973, plain, (genls(f_collectionintersection2fn(c_soldier,c_britishperson),c_britishperson))). % 9.43/9.62 cnf(i_0_947, plain, (genls(f_collectionintersection2fn(c_srilankanperson,c_militaryperson),c_militaryperson))). % 9.43/9.62 cnf(i_0_1002, plain, (genls(f_collectionintersection2fn(c_italianperson,c_civilian),c_italianperson))). % 9.43/9.62 cnf(i_0_1410, plain, (genls(f_subcollectionofusedfortypefn(c_clothing_generic,c_malehuman),c_clothing_generic))). % 9.43/9.62 cnf(i_0_1201, plain, (genls(f_exposureoforganismtoharmfulsubstancefn(f_liquidfn(c_cyanide)),f_exposureoforganismtoharmfulsubstancefn(c_cyanide)))). % 9.43/9.62 cnf(i_0_331, plain, (genls(f_subcollectionbyregionfn(c_thenchead,c_thencmodifier),c_individual))). % 9.43/9.62 cnf(i_0_256, plain, (collection(f_attacktypebytargettypefn(c_kidnappingsomeone,f_citizenfn(c_israel))))). % 9.43/9.62 cnf(i_0_1064, plain, (collection(f_subcollectionbyregionfn(c_muscle,f_somefn(c_centerofgeographicalregion))))). % 9.43/9.62 cnf(i_0_1051, plain, (objecttype(f_collectionintersection2fn(c_thenchead,f_groupfn(c_vaccinationevent))))). % 9.43/9.62 cnf(i_0_1469, plain, (resultgenl(f_prospectivewrtroleintypefn(X1,X2),c_individual))). % 9.43/9.62 cnf(i_0_1344, plain, (resultgenl(f_integerfromtofn(X1,X2),c_integer))). % 9.43/9.62 cnf(i_0_1470, plain, (natfunction(f_prospectivewrtroleintypefn(X1,X2),c_prospectivewrtroleintypefn))). % 9.43/9.62 cnf(i_0_1600, plain, (argformat(f_presenttenseversionfn(c_transportees),n_1,c_openentryformatinargs))). % 9.43/9.62 cnf(i_0_1540, plain, (argformat(f_presenttenseversionfn(c_doneby),n_2,c_openentryformatinargs))). % 9.43/9.62 cnf(i_0_105, plain, (natargument(f_namefn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_104, plain, (natargument(f_urlfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_103, plain, (natargument(f_urlreferentfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_100, plain, (natargument(f_formulatemplateinductiontopictypefn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_97, plain, (natargument(f_wordnetsynsetreifiedfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_91, plain, (natargument(f_groupfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_87, plain, (natargument(f_contextofpcwfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_86, plain, (natargument(f_the(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_82, plain, (natargument(f_liquidfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_81, plain, (natargument(f_mapfn_individual(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_78, plain, (natargument(f_yearfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_857, plain, (natargument(f_meatfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_75, plain, (natargument(f_territoryfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1494, plain, (natargument(f_highamountfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_64, plain, (natargument(f_rightobjectofpairfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1019, plain, (natargument(f_jobfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_63, plain, (natargument(f_leftobjectofpairfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_738, plain, (natargument(f_setoftypefn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_60, plain, (natargument(f_cityincountryfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1602, plain, (natargument(f_presenttenseversionfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1323, plain, (natargument(f_armyfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1316, plain, (natargument(f_memberfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_711, plain, (natargument(f_cycextendedsystemfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_59, plain, (natargument(f_specsfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_669, plain, (natargument(f_somefn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_861, plain, (natargument(f_transportviafn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1018, plain, (natargument(f_freethingoftypefn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_734, plain, (natargument(f_listoftypefn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1373, plain, (natargument(f_armedforcesfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1478, plain, (natargument(f_buyingfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1203, plain, (natargument(f_exposureoforganismtoharmfulsubstancefn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1183, plain, (natargument(f_playingfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1190, plain, (natargument(f_treatmentfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_626, plain, (natargument(f_citizenfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1013, plain, (natargument(f_marketedproductofcwfn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1442, plain, (natargument(f_sharesinfundtypefn(X1),n_1,X1))). % 9.43/9.62 cnf(i_0_1401, plain, (firstordercollection(f_subcollectionofwithrelationtotypefn(c_excreting,c_doneby,c_femalehuman)))). % 9.43/9.62 cnf(i_0_383, plain, (firstordercollection(f_subcollectionofwithrelationtotypefn(c_person,c_owns,c_building)))). % 9.43/9.62 cnf(i_0_1454, plain, (firstordercollection(f_subcollectionofwithrelationtotypefn(c_person,c_financialstate,c_wealthy)))). % 9.43/9.62 cnf(i_0_417, plain, (firstordercollection(f_subcollectionofwithrelationtotypefn(c_agent_generic,c_employees,c_person)))). % 9.43/9.62 cnf(i_0_272, plain, (termofunit(f_setoftypefn(f_listoftypefn(c_collection)),f_setoftypefn(f_listoftypefn(c_collection))))). % 9.43/9.62 cnf(i_0_1405, plain, (firstordercollection(f_subcollectionofwithrelationtotypefn(c_malehuman,c_wife,c_femalehuman)))). % 9.43/9.62 cnf(i_0_948, plain, (firstordercollection(f_subcollectionofwithrelationtotypefn(c_controllingsomething,c_objectcontrolled,c_militaryperson)))). % 9.43/9.62 cnf(i_0_1209, plain, (firstordercollection(f_subcollectionofwithrelationtotypefn(c_socialbeing,c_owns,c_somethingexisting)))). % 9.43/9.62 cnf(i_0_962, plain, (firstordercollection(f_subcollectionofwithrelationtotypefn(c_shootingaprojectileweapon,c_performedby,c_soldier)))). % 9.43/9.62 cnf(i_0_692, plain, (firstordercollection(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_colombia)))). % 9.43/9.62 cnf(i_0_681, plain, (firstordercollection(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_lebanon)))). % 9.43/9.62 cnf(i_0_682, plain, (firstordercollection(f_subcollectionofwithrelationfromfn(c_person,c_citizens,c_algeria)))). % 9.43/9.62 cnf(i_0_595, plain, (firstordercollection(f_subcollectionofwithrelationfromfn(c_militaryorganization,c_possessiverelation,c_israel)))). % 9.43/9.62 cnf(i_0_966, plain, (firstordercollection(f_subcollectionofwithrelationfromfn(c_soldier,c_employees,c_southlebanonarmy)))). % 9.43/9.62 cnf(i_0_1334, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terrorist,c_birthplace,c_spain)))). % 9.43/9.62 cnf(i_0_593, plain, (termofunit(f_memberfn(f_armyfn(c_israel)),f_memberfn(f_armyfn(c_israel))))). % 9.43/9.62 cnf(i_0_1352, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terrorist,c_birthplace,c_turkey)))). % 9.43/9.62 cnf(i_0_1274, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_spain)))). % 9.43/9.62 cnf(i_0_1385, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_india)))). % 9.43/9.62 cnf(i_0_1335, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_spain)))). % 9.43/9.62 cnf(i_0_1338, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_orgpresentinregion,c_spain)))). % 9.43/9.62 cnf(i_0_935, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_unitedstatesperson)))). % 9.43/9.62 cnf(i_0_1362, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_shootingattack_gun)))). % 9.43/9.62 cnf(i_0_1069, plain, (individual(f_relativegenericvaluefn(c_temperatureofobject,c_organism_whole,c_hightoveryhighamountof)))). % 9.43/9.62 cnf(i_0_1452, plain, (existingobjecttype(f_subcollectionofwithrelationtotypefn(c_person,c_financialstate,c_wealthy)))). % 9.43/9.62 cnf(i_0_680, plain, (existingobjecttype(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_indonesia_thenation)))). % 9.43/9.62 cnf(i_0_1311, plain, (termofunit(f_memberfn(f_armyfn(c_pakistan)),f_memberfn(f_armyfn(c_pakistan))))). % 9.43/9.62 cnf(i_0_702, plain, (existingobjecttype(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_russia)))). % 9.43/9.62 cnf(i_0_683, plain, (existingobjecttype(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_spain)))). % 9.43/9.62 cnf(i_0_684, plain, (existingobjecttype(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_turkey)))). % 9.43/9.62 cnf(i_0_592, plain, (existingobjecttype(f_subcollectionofwithrelationfromfn(c_militaryorganization,c_possessiverelation,c_israel)))). % 9.43/9.62 cnf(i_0_403, plain, (existingobjecttype(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_1022, plain, (existingobjecttype(f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_saudiperson)))). % 9.43/9.62 cnf(i_0_636, plain, (existingobjecttype(f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_kidnappingsomeone)))). % 9.43/9.62 cnf(i_0_1302, plain, (termofunit(f_memberfn(f_armyfn(c_nepal)),f_memberfn(f_armyfn(c_nepal))))). % 9.43/9.62 cnf(i_0_1310, plain, (termofunit(f_memberfn(f_armedforcesfn(c_germany)),f_memberfn(f_armedforcesfn(c_germany))))). % 9.43/9.62 cnf(i_0_1309, plain, (termofunit(f_memberfn(f_armedforcesfn(c_spain)),f_memberfn(f_armedforcesfn(c_spain))))). % 9.43/9.62 cnf(i_0_939, plain, (persontypebyoccupation(f_subcollectionofwithrelationtofn(c_person,c_retiredfromfield,c_militaryperson)))). % 9.43/9.62 cnf(i_0_1424, plain, (setorcollection(f_subcollectionofwithrelationtotypefn(c_manufacturing,c_productscreated,c_weapon)))). % 9.43/9.62 cnf(i_0_685, plain, (setorcollection(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_germany)))). % 9.43/9.62 cnf(i_0_687, plain, (setorcollection(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_malaysia)))). % 9.43/9.62 cnf(i_0_540, plain, (setorcollection(f_subcollectionofwithrelationfromfn(c_airplane,c_possessiverelation,c_israel)))). % 9.43/9.62 cnf(i_0_536, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terrorist,c_occupation,c_militaryperson)))). % 9.43/9.62 cnf(i_0_534, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terrorist,c_residesinregion,c_palestinianwestbankandgaza)))). % 9.43/9.62 cnf(i_0_541, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terrorist,c_residesinregion,c_israel)))). % 9.43/9.62 cnf(i_0_543, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terrorist,c_birthplace,c_israel)))). % 9.43/9.62 cnf(i_0_1300, plain, (termofunit(f_memberfn(f_armedforcesfn(c_afghanistan)),f_memberfn(f_armedforcesfn(c_afghanistan))))). % 9.43/9.62 cnf(i_0_404, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_1276, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_canada)))). % 9.43/9.62 cnf(i_0_1374, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_austria)))). % 9.43/9.62 cnf(i_0_1329, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_iran)))). % 9.43/9.62 cnf(i_0_544, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_orgpresentinregion,c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_1429, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_armedwithweapontype,c_bomb)))). % 9.43/9.62 cnf(i_0_537, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_soldier)))). % 9.43/9.62 cnf(i_0_535, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_murder)))). % 9.43/9.62 cnf(i_0_387, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))). % 9.43/9.62 cnf(i_0_1100, plain, (logicalfield(f_logicalfieldfn(c_edb_entityattribute_ls,c_date,n_1)))). % 9.43/9.62 cnf(i_0_699, plain, (termofunit(f_templatefromtestqueryfn(f_literalbuilderqueryfn(c_citizens)),f_templatefromtestqueryfn(f_literalbuilderqueryfn(c_citizens))))). % 9.43/9.62 cnf(i_0_1099, plain, (logicalfield(f_logicalfieldfn(c_edb_entityattribute_ls,c_date,n_2)))). % 9.43/9.62 cnf(i_0_1260, plain, (logicalfield(f_logicalfieldfn(c_edb_entityattribute_ls,c_place,n_1)))). % 9.43/9.62 cnf(i_0_582, plain, (firstordercollection(f_nthsubsituationtypeoftypefn(X1,X2,X3)))). % 9.43/9.62 cnf(i_0_139, plain, (collection(f_subcollectionofwithrelationtotypefn(X1,X2,X3)))). % 9.43/9.62 cnf(i_0_126, plain, (collection(f_subcollectionofwithrelationfromfn(X1,X2,X3)))). % 9.43/9.62 cnf(i_0_125, plain, (collection(f_subcollectionofwithrelationtofn(X1,X2,X3)))). % 9.43/9.62 cnf(i_0_110, plain, (collection(f_propersubcollectionnamedfn_ternary(X1,X2,X3)))). % 9.43/9.62 cnf(i_0_1377, plain, (termofunit(f_templatefromtestqueryfn(f_literalbuilderqueryfn(c_considersasenemy)),f_templatefromtestqueryfn(f_literalbuilderqueryfn(c_considersasenemy))))). % 9.43/9.62 cnf(i_0_1109, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_thing,c_chosenitem,c_selectingsomething),c_thing))). % 9.43/9.62 cnf(i_0_378, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_individual,c_parts,c_individual),c_individual))). % 9.43/9.62 cnf(i_0_677, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_realnumber,c_annualdeathrate,c_geopoliticalentity),c_realnumber))). % 9.43/9.62 cnf(i_0_1246, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_geographicalsubregions,c_stream),c_individual))). % 9.43/9.62 cnf(i_0_471, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_stream),c_individual))). % 9.43/9.62 cnf(i_0_1220, plain, (termofunit(f_templatefromtestqueryfn(f_relationinstanceexistsbuilderqueryfn(c_operatesfacilities)),f_templatefromtestqueryfn(f_relationinstanceexistsbuilderqueryfn(c_operatesfacilities))))). % 9.43/9.62 cnf(i_0_475, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_stream),c_bodyofwater))). % 9.43/9.62 cnf(i_0_477, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_ditch),c_individual))). % 9.43/9.62 cnf(i_0_466, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_geographicalregion,c_pathterminus,c_drycreekbed),c_geographicalregion))). % 9.43/9.62 cnf(i_0_1447, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_socialbeing,c_seller,c_monetaryexchangeofuserrights),c_socialbeing))). % 9.43/9.62 cnf(i_0_1400, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_femalehuman,c_wife,c_malehuman),c_femalehuman))). % 9.43/9.62 cnf(i_0_1159, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_monetaryvalue,c_discount,c_buying),c_monetaryvalue))). % 9.43/9.62 cnf(i_0_760, plain, (quotedisa(f_ncgenlsconstraintfn(c_thenchead,f_groupfn(c_transportationdevice)),c_termsuggestorexpertonlyterm))). % 9.43/9.62 cnf(i_0_1626, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_flowterrain,c_subpaths,c_drycreekbed),c_flowterrain))). % 9.43/9.62 cnf(i_0_1213, plain, (genls(f_subcollectionofwithrelationtotypefn(c_person,c_owns,c_confectionery),c_partiallytangible))). % 9.43/9.62 cnf(i_0_1397, plain, (genls(f_subcollectionofwithrelationfromfn(c_bus_roadvehicle,c_possessiverelation,c_israel),c_partiallytangible))). % 9.43/9.62 cnf(i_0_601, plain, (genls(f_subcollectionofwithrelationfromfn(c_airplane,c_possessiverelation,c_israel),c_partiallytangible))). % 9.43/9.62 cnf(i_0_1036, plain, (genls(f_subcollectionofwithrelationfromfn(c_personwithoccupation,c_performsinstancesaspartofjob,c_training),c_partiallytangible))). % 9.43/9.62 cnf(i_0_340, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_partiallytangible),f_ncisaconstraintfn(c_thencmodifier,c_partiallytangible)))). % 9.43/9.62 cnf(i_0_372, plain, (genls(f_collectionintersection2fn(c_thenchead,f_groupfn(c_thencmodifier)),c_individual))). % 9.43/9.62 cnf(i_0_1049, plain, (genls(f_collectionintersection2fn(c_thenchead,f_groupfn(c_vaccinationevent)),c_individual))). % 9.43/9.62 cnf(i_0_976, plain, (genls(f_collectionintersection2fn(c_soldier,f_memberfn(c_unitedstatesarmy)),c_soldier))). % 9.43/9.62 cnf(i_0_452, plain, (genls(f_subcollectionofwithrelationfromfn(c_partiallytangible,c_byproducts,f_somefn(c_physicalcreationordestructionevent)),c_partiallytangible))). % 9.43/9.62 cnf(i_0_437, plain, (genls(f_prospectivewrtroleintypefn(c_buyer,f_buyingfn(c_automobile)),c_individual))). % 9.43/9.62 cnf(i_0_359, plain, (genls(f_subcollectionbyregionfn(c_thenchead,f_somefn(c_thencmodifier)),c_individual))). % 9.43/9.62 cnf(i_0_559, plain, (firstordercollection(f_collectionintersection2fn(f_citizenfn(c_unitedstatesofamerica),f_citizenfn(c_israel))))). % 9.43/9.62 cnf(i_0_650, plain, (collection(f_attacktypebytargettypefn(c_shootingattack_gun,f_collectionintersection2fn(c_israeliperson,c_soldier))))). % 9.43/9.62 cnf(i_0_107, plain, (natargument(f_computervulnerabilityreportfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_108, plain, (natargument(f_computervulnerabilityreportfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_101, plain, (natargument(f_citynamedfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_102, plain, (natargument(f_citynamedfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_98, plain, (natargument(f_countynamedfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_99, plain, (natargument(f_countynamedfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_95, plain, (natargument(f_contentmtofcdafromeventfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_96, plain, (natargument(f_contentmtofcdafromeventfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_79, plain, (natargument(f_monthfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_80, plain, (natargument(f_monthfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_76, plain, (natargument(f_attacktypebytargettypefn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_77, plain, (natargument(f_attacktypebytargettypefn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_73, plain, (natargument(f_meaninginsystemfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_74, plain, (natargument(f_meaninginsystemfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_65, plain, (natargument(f_collectionintersection2fn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_66, plain, (natargument(f_collectionintersection2fn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_792, plain, (natargument(f_ncgenlsconstraintfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_793, plain, (natargument(f_ncgenlsconstraintfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_61, plain, (natargument(f_softwareversionfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_62, plain, (natargument(f_softwareversionfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_893, plain, (natargument(f_ncisaconstraintfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_894, plain, (natargument(f_ncisaconstraintfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_1471, plain, (natargument(f_prospectivewrtroleintypefn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_1097, plain, (termofunit(f_builderquerytemplateforlogicalfieldtypeofsksfn(c_sageman_entityattribute_ks,c_date),f_builderquerytemplateforlogicalfieldtypeofsksfn(c_sageman_entityattribute_ks,c_date)))). % 9.43/9.62 cnf(i_0_1472, plain, (natargument(f_prospectivewrtroleintypefn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_1065, plain, (natargument(f_subcollectionbyregionfn(X1,X2),n_1,X1))). % 9.43/9.62 cnf(i_0_1066, plain, (natargument(f_subcollectionbyregionfn(X1,X2),n_2,X2))). % 9.43/9.62 cnf(i_0_1211, plain, (genls(f_subcollectionofwithrelationtotypefn(c_person,c_owns,c_confectionery),c_individual))). % 9.43/9.62 cnf(i_0_996, plain, (genls(f_subcollectionofwithrelationtotypefn(c_arrivingataplace,c_transporter,c_transportationdevice_vehicle),c_transportationevent))). % 9.43/9.62 cnf(i_0_1416, plain, (genls(f_subcollectionofwithrelationtotypefn(c_manufacturing,c_productscreated,c_weapon),c_individual))). % 9.43/9.62 cnf(i_0_1262, plain, (termofunit(f_builderquerytemplateforlogicalfieldtypeofsksfn(c_usgs_gnis_ks,c_place),f_builderquerytemplateforlogicalfieldtypeofsksfn(c_usgs_gnis_ks,c_place)))). % 9.43/9.62 cnf(i_0_1256, plain, (genls(f_subcollectionofwithrelationtotypefn(c_lifeseeing,c_eventoccursat,c_ruralarea),c_lifeseeing))). % 9.43/9.62 cnf(i_0_972, plain, (genls(f_subcollectionofwithrelationtotypefn(c_shootingaprojectileweapon,c_performedby,c_soldier),c_action))). % 9.43/9.62 cnf(i_0_1119, plain, (genls(f_subcollectionofwithrelationtotypefn(c_policeorganization,c_groupmembers,c_ethnicgroupofblacks),c_policeorganization))). % 9.43/9.62 cnf(i_0_706, plain, (genls(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_indonesia_thenation),c_terrorist))). % 9.43/9.62 cnf(i_0_701, plain, (genls(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_brazil),c_terrorist))). % 9.43/9.62 cnf(i_0_695, plain, (genls(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_unitedkingdomofgreatbritainandnorthernireland),c_terrorist))). % 9.43/9.62 cnf(i_0_698, plain, (genls(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_saudiarabia),c_terrorist))). % 9.43/9.62 cnf(i_0_708, plain, (genls(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_algeria),c_terrorist))). % 9.43/9.62 cnf(i_0_690, plain, (genls(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_netherlands),c_terrorist))). % 9.43/9.62 cnf(i_0_1102, plain, (termofunit(f_builderquerytemplateforlogicalfieldtypeofsksfn(c_glassbox_citation_ks,c_date),f_builderquerytemplateforlogicalfieldtypeofsksfn(c_glassbox_citation_ks,c_date)))). % 9.43/9.62 cnf(i_0_704, plain, (genls(f_subcollectionofwithrelationfromfn(c_person,c_citizens,c_algeria),c_person))). % 9.43/9.62 cnf(i_0_1207, plain, (genls(f_subcollectionofwithrelationfromfn(c_individual,c_parts,c_edwood_moviedirector),c_individual))). % 9.43/9.62 cnf(i_0_1391, plain, (genls(f_subcollectionofwithrelationfromfn(c_individual,c_possessiverelation,c_edwood_moviedirector),c_individual))). % 9.43/9.62 cnf(i_0_1395, plain, (genls(f_subcollectionofwithrelationfromfn(c_bus_roadvehicle,c_possessiverelation,c_israel),c_individual))). % 9.43/9.62 cnf(i_0_1393, plain, (genls(f_subcollectionofwithrelationfromfn(c_bus_roadvehicle,c_possessiverelation,c_israel),c_bus_roadvehicle))). % 9.43/9.62 cnf(i_0_561, plain, (genls(f_subcollectionofwithrelationfromfn(c_adultfemalehuman,c_possessiverelation,c_unitedstatesofamerica),c_adultfemalehuman))). % 9.43/9.62 cnf(i_0_589, plain, (genls(f_subcollectionofwithrelationfromfn(c_airplane,c_possessiverelation,c_israel),c_individual))). % 9.43/9.62 cnf(i_0_563, plain, (genls(f_subcollectionofwithrelationfromfn(c_facility_construct,c_owns,c_unitedstatesofamerica),c_facility_construct))). % 9.43/9.62 cnf(i_0_1041, plain, (genls(f_subcollectionofwithrelationfromfn(c_personwithoccupation,c_performsinstancesaspartofjob,c_training),c_individual))). % 9.43/9.62 cnf(i_0_1076, plain, (genls(f_subcollectionofwithrelationtofn(c_terrorist,c_residesinregion,c_yemen),c_animal))). % 9.43/9.62 cnf(i_0_253, plain, (termofunit(f_attacktypebytargettypefn(c_bombing,c_airport_physical),f_attacktypebytargettypefn(c_bombing,c_airport_physical)))). % 9.43/9.62 cnf(i_0_1072, plain, (genls(f_subcollectionofwithrelationtofn(c_terrorist,c_residesinregion,c_australia),c_animal))). % 9.43/9.62 cnf(i_0_1077, plain, (genls(f_subcollectionofwithrelationtofn(c_terrorist,c_birthplace,c_sudan),c_animal))). % 9.43/9.62 cnf(i_0_1074, plain, (genls(f_subcollectionofwithrelationtofn(c_terrorist,c_birthplace,c_yemen),c_animal))). % 9.43/9.62 cnf(i_0_1038, plain, (genls(f_subcollectionofwithrelationtofn(c_person,c_retiredfromfield,c_lawenforcementofficer),c_personwithoccupation))). % 9.43/9.62 cnf(i_0_1281, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_india),c_terroristgroup))). % 9.43/9.62 cnf(i_0_1279, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_spain),c_terroristgroup))). % 9.43/9.62 cnf(i_0_405, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_unitedstatesofamerica),c_terroristgroup))). % 9.43/9.62 cnf(i_0_1280, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_canada),c_terroristgroup))). % 9.43/9.62 cnf(i_0_1379, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_india),c_terroristgroup))). % 9.43/9.62 cnf(i_0_419, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_india),c_agent_generic))). % 9.43/9.62 cnf(i_0_643, plain, (termofunit(f_attacktypebytargettypefn(c_terroristsuicidebombing,c_israeliperson),f_attacktypebytargettypefn(c_terroristsuicidebombing,c_israeliperson)))). % 9.43/9.62 cnf(i_0_557, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_unitedstatesofamerica),c_terroristgroup))). % 9.43/9.62 cnf(i_0_416, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_unitedstatesofamerica),c_agent_generic))). % 9.43/9.62 cnf(i_0_429, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_armedwithweapontype,c_weapon),c_intelligentagent))). % 9.43/9.62 cnf(i_0_933, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_unitedstatesperson),c_terroristgroup))). % 9.43/9.62 cnf(i_0_323, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_militaryperson),c_organization))). % 9.43/9.62 cnf(i_0_1025, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_saudiperson),c_terroristgroup))). % 9.43/9.62 cnf(i_0_412, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_murder),c_agent_generic))). % 9.43/9.62 cnf(i_0_1361, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_torture),c_terroristgroup))). % 9.43/9.62 cnf(i_0_1365, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_carbombing),c_agent_generic))). % 9.43/9.62 cnf(i_0_337, plain, (genls(f_subcollectionofwithrelationtofn(c_thenchead,c_genls,c_thencmodifier),c_collection))). % 9.43/9.62 cnf(i_0_628, plain, (termofunit(f_attacktypebytargettypefn(c_kidnappingsomeone,c_publicofficial),f_attacktypebytargettypefn(c_kidnappingsomeone,c_publicofficial)))). % 9.43/9.62 cnf(i_0_374, plain, (genls(f_subcollectionofwithrelationtofn(c_collection,c_genls,c_thencmodifier),c_collection))). % 9.43/9.62 cnf(i_0_1236, plain, (genls(f_subcollectionofwithrelationtofn(c_passport,c_originallyfromregion,c_guyana),c_spatialthing_localized))). % 9.43/9.62 cnf(i_0_964, plain, (genls(f_subcollectionofwithrelationtofn(c_soldier,c_isa,c_female),c_thing))). % 9.43/9.62 cnf(i_0_661, plain, (firstordercollection(f_subcollectionofwithrelationfromfn(c_spatialthing_localized,c_eventoccursat,f_somefn(c_event))))). % 9.43/9.62 cnf(i_0_599, plain, (firstordercollection(f_subcollectionofwithrelationfromfn(c_soldier,c_hasmembers,f_armyfn(c_israel))))). % 9.43/9.62 cnf(i_0_594, plain, (firstordercollection(f_subcollectionofwithrelationfromfn(c_soldier,c_employees,f_armyfn(c_israel))))). % 9.43/9.62 cnf(i_0_1383, plain, (firstordercollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,f_governmentfn(c_ethiopia))))). % 9.43/9.62 cnf(i_0_666, plain, (spatiallydisjointobjecttype(f_subcollectionofwithrelationfromfn(c_organism_whole,c_relatives,f_somefn(c_organism_whole))))). % 9.43/9.62 cnf(i_0_1321, plain, (existingobjecttype(f_subcollectionofwithrelationfromfn(c_militarypost,c_controls,f_armyfn(c_israel))))). % 9.43/9.62 cnf(i_0_665, plain, (existingobjecttype(f_subcollectionofwithrelationtofn(c_animal,c_residesinregion,f_somefn(c_geographicalthing))))). % 9.43/9.62 cnf(i_0_639, plain, (termofunit(f_attacktypebytargettypefn(c_kidnappingsomeone,c_militaryperson),f_attacktypebytargettypefn(c_kidnappingsomeone,c_militaryperson)))). % 9.43/9.62 cnf(i_0_1490, plain, (existingobjecttype(f_subcollectionofwithrelationtofn(c_femaleanimal,c_aestheticqualityofthing,f_highamountfn(c_beauty))))). % 9.43/9.62 cnf(i_0_562, plain, (setorcollection(f_subcollectionofwithrelationfromfn(c_militaryperson,c_hasmembers,f_armedforcesfn(c_unitedstatesofamerica))))). % 9.43/9.62 cnf(i_0_1382, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,f_governmentfn(c_egypt))))). % 9.43/9.62 cnf(i_0_1486, plain, (setorcollection(f_subcollectionofwithrelationtofn(c_femaleanimal,c_aestheticqualityofthing,f_highamountfn(c_beauty))))). % 9.43/9.62 cnf(i_0_1251, plain, (termofunit(f_meaninginsystemfn(c_sensus_information1997,s_decomposable_object),f_meaninginsystemfn(c_sensus_information1997,s_decomposable_object)))). % 9.43/9.62 cnf(i_0_1670, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_subpaths,f_intermittentbodyofwaterfn(c_stream)),c_individual))). % 9.43/9.62 cnf(i_0_443, plain, (genls(f_subcollectionofwithrelationtofn(c_homosapiens,c_hasphysicalattractiveness,f_highamountfn(c_physicalattractiveness)),c_partiallytangible))). % 9.43/9.62 cnf(i_0_439, plain, (genls(f_subcollectionofwithrelationtofn(c_person,c_hasphysicalattractiveness,f_highamountfn(c_physicalattractiveness)),c_partiallytangible))). % 9.43/9.62 cnf(i_0_441, plain, (genls(f_subcollectionofwithrelationtofn(c_malehuman,c_hasphysicalattractiveness,f_highamountfn(c_physicalattractiveness)),c_partiallytangible))). % 9.43/9.62 cnf(i_0_106, plain, (natargument(f_subcollectionofwithrelationfromtypefn(X1,X2,X3),n_3,X3))). % 9.43/9.62 cnf(i_0_910, plain, (termofunit(f_artifacttypeforusertypefn(c_shoe,c_femalechild),f_artifacttypeforusertypefn(c_shoe,c_femalechild)))). % 9.43/9.62 cnf(i_0_14, plain, (natargument(f_subcollectionofwithrelationfromtypefn(X1,X2,X3),n_1,X1))). % 9.43/9.62 cnf(i_0_15, plain, (natargument(f_subcollectionofwithrelationfromtypefn(X1,X2,X3),n_2,X2))). % 9.43/9.62 cnf(i_0_1061, plain, (genls(f_subcollectionbyregionfn(f_subcollectionofwithrelationfromtypefn(c_militarypost,c_controls,c_militaryorganization),c_israel),c_partiallytangible))). % 9.43/9.62 cnf(i_0_1125, plain, (persontypebyoccupation(f_subcollectionofwithrelationfromtypefn(c_person,c_employees,f_subcollectionofwithrelationfromtypefn(c_business,c_groupmembers,c_nuclearenergyindustry))))). % 9.43/9.62 cnf(i_0_908, plain, (termofunit(f_artifacttypeforusertypefn(c_costume,c_femalechild),f_artifacttypeforusertypefn(c_costume,c_femalechild)))). % 9.43/9.62 cnf(i_0_652, plain, (termofunit(f_collectionintersection2fn(c_israeliperson,c_diplomat),f_collectionintersection2fn(c_israeliperson,c_diplomat)))). % 9.43/9.62 cnf(i_0_648, plain, (termofunit(f_collectionintersection2fn(c_israeliperson,c_soldier),f_collectionintersection2fn(c_israeliperson,c_soldier)))). % 9.43/9.62 cnf(i_0_642, plain, (termofunit(f_collectionintersection2fn(c_student,c_israeliperson),f_collectionintersection2fn(c_student,c_israeliperson)))). % 9.43/9.62 cnf(i_0_1004, plain, (termofunit(f_collectionintersection2fn(c_turkishperson,c_civilian),f_collectionintersection2fn(c_turkishperson,c_civilian)))). % 9.43/9.62 cnf(i_0_1453, plain, (termofunit(f_collectionintersection2fn(c_famoushuman,c_wealthy),f_collectionintersection2fn(c_famoushuman,c_wealthy)))). % 9.43/9.62 cnf(i_0_777, plain, (termofunit(f_ncgenlsconstraintfn(c_thenchead,c_purposefulaction),f_ncgenlsconstraintfn(c_thenchead,c_purposefulaction)))). % 9.43/9.62 cnf(i_0_789, plain, (termofunit(f_ncgenlsconstraintfn(c_thenchead,c_animal),f_ncgenlsconstraintfn(c_thenchead,c_animal)))). % 9.43/9.62 cnf(i_0_768, plain, (termofunit(f_ncgenlsconstraintfn(c_thenchead,c_person),f_ncgenlsconstraintfn(c_thenchead,c_person)))). % 9.43/9.62 cnf(i_0_423, plain, (termofunit(f_ncgenlsconstraintfn(c_thenchead,c_intelligentagent),f_ncgenlsconstraintfn(c_thenchead,c_intelligentagent)))). % 9.43/9.62 cnf(i_0_741, plain, (termofunit(f_ncgenlsconstraintfn(c_thenchead,c_group),f_ncgenlsconstraintfn(c_thenchead,c_group)))). % 9.43/9.62 cnf(i_0_766, plain, (termofunit(f_ncgenlsconstraintfn(c_thenchead,c_informationtransferevent),f_ncgenlsconstraintfn(c_thenchead,c_informationtransferevent)))). % 9.43/9.62 cnf(i_0_354, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_thing),f_ncgenlsconstraintfn(c_thencmodifier,c_thing)))). % 9.43/9.62 cnf(i_0_347, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_date),f_ncgenlsconstraintfn(c_thencmodifier,c_date)))). % 9.43/9.62 cnf(i_0_334, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_animal),f_ncgenlsconstraintfn(c_thencmodifier,c_animal)))). % 9.43/9.62 cnf(i_0_329, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_artifact),f_ncgenlsconstraintfn(c_thencmodifier,c_artifact)))). % 9.43/9.62 cnf(i_0_346, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_thenchead),f_ncgenlsconstraintfn(c_thencmodifier,c_thenchead)))). % 9.43/9.62 cnf(i_0_304, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_situation),f_ncgenlsconstraintfn(c_thencmodifier,c_situation)))). % 9.43/9.62 cnf(i_0_338, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_computerprogram_cw),f_ncgenlsconstraintfn(c_thencmodifier,c_computerprogram_cw)))). % 9.43/9.62 cnf(i_0_750, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_food),f_ncgenlsconstraintfn(c_thencmodifier,c_food)))). % 9.43/9.62 cnf(i_0_773, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_textualmaterial),f_ncgenlsconstraintfn(c_thencmodifier,c_textualmaterial)))). % 9.43/9.62 cnf(i_0_344, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_unitedstatesperson),f_ncgenlsconstraintfn(c_thencmodifier,c_unitedstatesperson)))). % 9.43/9.62 cnf(i_0_759, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_solidtangiblething),f_ncgenlsconstraintfn(c_thencmodifier,c_solidtangiblething)))). % 9.43/9.62 cnf(i_0_754, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_perceptualagent_embodied),f_ncgenlsconstraintfn(c_thencmodifier,c_perceptualagent_embodied)))). % 9.43/9.62 cnf(i_0_335, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_transportationdevice_vehicle),f_ncgenlsconstraintfn(c_thencmodifier,c_transportationdevice_vehicle)))). % 9.43/9.62 cnf(i_0_742, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_evaluating),f_ncgenlsconstraintfn(c_thencmodifier,c_evaluating)))). % 9.43/9.62 cnf(i_0_779, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_commercialactivity),f_ncgenlsconstraintfn(c_thencmodifier,c_commercialactivity)))). % 9.43/9.62 cnf(i_0_764, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_exchangeofuserrights),f_ncgenlsconstraintfn(c_thencmodifier,c_exchangeofuserrights)))). % 9.43/9.62 cnf(i_0_749, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_transportationdevice),f_ncgenlsconstraintfn(c_thencmodifier,c_transportationdevice)))). % 9.43/9.62 cnf(i_0_780, plain, (termofunit(f_ncgenlsconstraintfn(c_thencmodifier,c_bacterium),f_ncgenlsconstraintfn(c_thencmodifier,c_bacterium)))). % 9.43/9.62 cnf(i_0_1328, plain, (termofunit(f_borderbetweenpolitiesfn(c_iran,c_armenia),f_borderbetweenpolitiesfn(c_iran,c_armenia)))). % 9.43/9.62 cnf(i_0_1332, plain, (termofunit(f_borderbetweenpolitiesfn(c_iran,c_azerbaijan),f_borderbetweenpolitiesfn(c_iran,c_azerbaijan)))). % 9.43/9.62 cnf(i_0_914, plain, (termofunit(f_borderbetweenpolitiesfn(c_iraq,c_iran),f_borderbetweenpolitiesfn(c_iraq,c_iran)))). % 9.43/9.62 cnf(i_0_924, plain, (termofunit(f_borderbetweenpolitiesfn(c_turkey,c_iraq),f_borderbetweenpolitiesfn(c_turkey,c_iraq)))). % 9.43/9.62 cnf(i_0_892, plain, (termofunit(f_ncisaconstraintfn(c_thenchead,c_collection),f_ncisaconstraintfn(c_thenchead,c_collection)))). % 9.43/9.62 cnf(i_0_874, plain, (termofunit(f_ncisaconstraintfn(c_thenchead,c_country),f_ncisaconstraintfn(c_thenchead,c_country)))). % 9.43/9.62 cnf(i_0_881, plain, (termofunit(f_ncisaconstraintfn(c_thenchead,c_binarypredicate),f_ncisaconstraintfn(c_thenchead,c_binarypredicate)))). % 9.43/9.62 cnf(i_0_877, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_persontypebyactivity),f_ncisaconstraintfn(c_thencmodifier,c_persontypebyactivity)))). % 9.43/9.62 cnf(i_0_870, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_competition),f_ncisaconstraintfn(c_thencmodifier,c_competition)))). % 9.43/9.62 cnf(i_0_332, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_thenchead),f_ncisaconstraintfn(c_thencmodifier,c_thenchead)))). % 9.43/9.62 cnf(i_0_862, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_chemicalreaction),f_ncisaconstraintfn(c_thencmodifier,c_chemicalreaction)))). % 9.43/9.62 cnf(i_0_355, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_geographicalregion),f_ncisaconstraintfn(c_thencmodifier,c_geographicalregion)))). % 9.43/9.62 cnf(i_0_863, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_textualmaterial),f_ncisaconstraintfn(c_thencmodifier,c_textualmaterial)))). % 9.43/9.62 cnf(i_0_891, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_legalgovernmentorganization),f_ncisaconstraintfn(c_thencmodifier,c_legalgovernmentorganization)))). % 9.43/9.62 cnf(i_0_865, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_state_geopolitical),f_ncisaconstraintfn(c_thencmodifier,c_state_geopolitical)))). % 9.43/9.62 cnf(i_0_886, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_educationalorganization),f_ncisaconstraintfn(c_thencmodifier,c_educationalorganization)))). % 9.43/9.62 cnf(i_0_885, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_property),f_ncisaconstraintfn(c_thencmodifier,c_property)))). % 9.43/9.62 cnf(i_0_866, plain, (termofunit(f_ncisaconstraintfn(c_thencmodifier,c_conflictevent),f_ncisaconstraintfn(c_thencmodifier,c_conflictevent)))). % 9.43/9.62 cnf(i_0_1409, plain, (termofunit(f_subcollectionofusedfortypefn(c_clothing_generic,c_malehuman),f_subcollectionofusedfortypefn(c_clothing_generic,c_malehuman)))). % 9.43/9.62 cnf(i_0_583, plain, (genlmt(f_instancewithrelationfromfn(c_mappingmicrotheory,c_informationstoremappingmt,f_cycextendedsystemfn(c_lscomobjectandsituationontology)),c_basekb))). % 9.43/9.62 cnf(i_0_151, plain, (genls(f_subcollectionofwithrelationtotypefn(c_geographicalregion,c_objectfoundinlocation,f_groupfn(c_building)),c_geographicalregion))). % 9.43/9.62 cnf(i_0_564, plain, (genls(f_subcollectionofwithrelationfromfn(c_militaryperson,c_hasmembers,f_armedforcesfn(c_unitedstatesofamerica)),c_militaryperson))). % 9.43/9.62 cnf(i_0_1492, plain, (genls(f_subcollectionofwithrelationtofn(c_thing,c_aestheticqualityofthing,f_highamountfn(c_beauty)),c_thing))). % 9.43/9.62 cnf(i_0_1381, plain, (genls(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,f_governmentfn(c_somalia)),c_terroristgroup))). % 9.43/9.62 cnf(i_0_1489, plain, (genls(f_subcollectionofwithrelationtofn(c_femaleanimal,c_aestheticqualityofthing,f_highamountfn(c_beauty)),c_thing))). % 9.43/9.62 cnf(i_0_566, plain, (genls(f_collectionintersection2fn(f_citizenfn(c_unitedstatesofamerica),f_citizenfn(c_israel)),f_citizenfn(c_israel)))). % 9.43/9.62 cnf(i_0_94, plain, (natargument(f_subcollectionofwithrelationtotypefn(X1,X2,X3),n_3,X3))). % 9.43/9.62 cnf(i_0_92, plain, (natargument(f_subcollectionofwithrelationtotypefn(X1,X2,X3),n_1,X1))). % 9.43/9.62 cnf(i_0_93, plain, (natargument(f_subcollectionofwithrelationtotypefn(X1,X2,X3),n_2,X2))). % 9.43/9.62 cnf(i_0_90, plain, (natargument(f_subcollectionofwithrelationfromfn(X1,X2,X3),n_3,X3))). % 9.43/9.62 cnf(i_0_88, plain, (natargument(f_subcollectionofwithrelationfromfn(X1,X2,X3),n_1,X1))). % 9.43/9.62 cnf(i_0_89, plain, (natargument(f_subcollectionofwithrelationfromfn(X1,X2,X3),n_2,X2))). % 9.43/9.62 cnf(i_0_85, plain, (natargument(f_subcollectionofwithrelationtofn(X1,X2,X3),n_3,X3))). % 9.43/9.62 cnf(i_0_83, plain, (natargument(f_subcollectionofwithrelationtofn(X1,X2,X3),n_1,X1))). % 9.43/9.62 cnf(i_0_84, plain, (natargument(f_subcollectionofwithrelationtofn(X1,X2,X3),n_2,X2))). % 9.43/9.62 cnf(i_0_72, plain, (natargument(f_propersubcollectionnamedfn_ternary(X1,X2,X3),n_3,X3))). % 9.43/9.62 cnf(i_0_554, plain, (genls(f_collectionintersection2fn(f_citizenfn(c_unitedstatesofamerica),f_citizenfn(c_israel)),f_citizenfn(c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_70, plain, (natargument(f_propersubcollectionnamedfn_ternary(X1,X2,X3),n_1,X1))). % 9.43/9.62 cnf(i_0_71, plain, (natargument(f_propersubcollectionnamedfn_ternary(X1,X2,X3),n_2,X2))). % 9.43/9.62 cnf(i_0_69, plain, (natargument(f_instancewithrelationtofn(X1,X2,X3),n_3,X3))). % 9.43/9.62 cnf(i_0_67, plain, (natargument(f_instancewithrelationtofn(X1,X2,X3),n_1,X1))). % 9.43/9.62 cnf(i_0_68, plain, (natargument(f_instancewithrelationtofn(X1,X2,X3),n_2,X2))). % 9.43/9.62 cnf(i_0_250, plain, (natargument(f_instancewithrelationfromfn(X1,X2,X3),n_3,X3))). % 9.43/9.62 cnf(i_0_585, plain, (natargument(f_instancewithrelationfromfn(X1,X2,X3),n_1,X1))). % 9.43/9.62 cnf(i_0_586, plain, (natargument(f_instancewithrelationfromfn(X1,X2,X3),n_2,X2))). % 9.43/9.62 cnf(i_0_249, plain, (natargument(f_nthsubsituationtypeoftypefn(X1,X2,X3),n_3,X3))). % 9.43/9.62 cnf(i_0_580, plain, (natargument(f_nthsubsituationtypeoftypefn(X1,X2,X3),n_1,X1))). % 9.43/9.62 cnf(i_0_581, plain, (natargument(f_nthsubsituationtypeoftypefn(X1,X2,X3),n_2,X2))). % 9.43/9.62 cnf(i_0_1123, plain, (collection(f_attacktypebytargettypefn(c_bombing,f_subcollectionofwithrelationtotypefn(c_policeorganization,c_groupmembers,c_ethnicgroupofblacks))))). % 9.43/9.62 cnf(i_0_598, plain, (genls(f_groupfn(f_subcollectionofwithrelationfromfn(c_airplane,c_possesses,f_governmentfn(c_israel))),c_partiallytangible))). % 9.43/9.62 cnf(i_0_422, plain, (firstordercollection(f_subcollectionofwithrelationfromtypefn(f_subcollectionofwithrelationtotypefn(c_malehuman,c_wife,c_femalehuman),c_possessiverelation,c_intelligentagent)))). % 9.43/9.62 cnf(i_0_1168, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_stairway,c_physicalparts,c_hotelbuilding),f_subcollectionofwithrelationfromtypefn(c_stairway,c_physicalparts,c_hotelbuilding)))). % 9.43/9.62 cnf(i_0_1114, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_thing,c_chosenitem,c_selectingsomething),f_subcollectionofwithrelationfromtypefn(c_thing,c_chosenitem,c_selectingsomething)))). % 9.43/9.62 cnf(i_0_1073, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_animal,c_children,c_animal),f_subcollectionofwithrelationfromtypefn(c_animal,c_children,c_animal)))). % 9.43/9.62 cnf(i_0_1659, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_stream,c_anabranches,c_stream),f_subcollectionofwithrelationfromtypefn(c_stream,c_anabranches,c_stream)))). % 9.43/9.62 cnf(i_0_379, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_individual,c_parts,c_individual),f_subcollectionofwithrelationfromtypefn(c_individual,c_parts,c_individual)))). % 9.43/9.62 cnf(i_0_469, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_ditch),f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_ditch)))). % 9.43/9.62 cnf(i_0_1160, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_monetaryvalue,c_salescommission,c_buying),f_subcollectionofwithrelationfromtypefn(c_monetaryvalue,c_salescommission,c_buying)))). % 9.43/9.62 cnf(i_0_667, plain, (termofunit(f_attacktypebytargettypefn(c_assassinatingsomeone,f_somefn(c_temporalstufftype)),f_attacktypebytargettypefn(c_assassinatingsomeone,f_somefn(c_temporalstufftype))))). % 9.43/9.62 cnf(i_0_1118, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_business,c_groupmembers,c_nuclearenergyindustry),f_subcollectionofwithrelationfromtypefn(c_business,c_groupmembers,c_nuclearenergyindustry)))). % 9.43/9.62 cnf(i_0_1392, plain, (genls(f_attacktypebytargettypefn(c_terroristsuicidebombing,f_subcollectionofwithrelationfromfn(c_bus_roadvehicle,c_possessiverelation,c_israel)),c_terroristsuicidebombing))). % 9.43/9.62 cnf(i_0_1225, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(c_officespace,c_operatesfacilities,c_politicalparty),f_subcollectionofwithrelationfromtypefn(c_officespace,c_operatesfacilities,c_politicalparty)))). % 9.43/9.62 cnf(i_0_1672, plain, (genls(f_subcollectionofwithrelationfromtypefn(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_geographicalsubregions,c_stream),c_eventoccursat,c_whirlingoffluid),c_individual))). % 9.43/9.62 cnf(i_0_929, plain, (genls(f_attacktypebytargettypefn(c_murder,f_subcollectionofwithrelationtotypefn(c_businessperson,c_affiliatedwith,c_unitedstatesperson)),c_murder))). % 9.43/9.62 cnf(i_0_602, plain, (setorcollection(f_subcollectionofwithrelationtotypefn(c_bombing,c_intendedattacktargets,f_subcollectionofwithrelationtofn(c_enduringthing_localized,c_inregion,c_unitedkingdomofgreatbritainandnorthernireland))))). % 9.43/9.62 cnf(i_0_247, plain, (natargument(f_relationexistsallfn(X1,X2,X3,X4),n_3,X3))). % 9.43/9.62 cnf(i_0_576, plain, (natargument(f_relationexistsallfn(X1,X2,X3,X4),n_1,X1))). % 9.43/9.62 cnf(i_0_577, plain, (natargument(f_relationexistsallfn(X1,X2,X3,X4),n_2,X2))). % 9.43/9.62 cnf(i_0_578, plain, (natargument(f_relationexistsallfn(X1,X2,X3,X4),n_4,X4))). % 9.43/9.62 cnf(i_0_248, plain, (natargument(f_relationallexistsfn(X1,X2,X3,X4),n_3,X3))). % 9.43/9.62 cnf(i_0_525, plain, (natargument(f_relationallexistsfn(X1,X2,X3,X4),n_1,X1))). % 9.43/9.62 cnf(i_0_1353, plain, (termofunit(f_borderbetweenfn(f_territoryfn(c_turkey),f_territoryfn(c_syria)),f_borderbetweenfn(f_territoryfn(c_turkey),f_territoryfn(c_syria))))). % 9.43/9.62 cnf(i_0_526, plain, (natargument(f_relationallexistsfn(X1,X2,X3,X4),n_2,X2))). % 9.43/9.62 cnf(i_0_527, plain, (natargument(f_relationallexistsfn(X1,X2,X3,X4),n_4,X4))). % 9.43/9.62 cnf(i_0_1585, plain, (isa(c_theprototypicalsubcollectionofwithrelationtotypefnliquidflowalongconduitprimaryobjectmovingsubcollectionofwithrelationfromtypefnwaterwasteproductspurposefulaction,f_subcollectionofwithrelationtotypefn(c_liquidflowalongconduit,c_primaryobjectmoving,f_subcollectionofwithrelationfromtypefn(c_water,c_wasteproducts,c_purposefulaction))))). % 9.43/9.62 cnf(i_0_1006, plain, (genls(f_subcollectionofwithrelationtotypefn(c_militaryattack,c_intendedattacktargets,f_subcollectionofwithrelationfromtypefn(c_somethingexisting,c_possesses,c_civilian)),c_individual))). % 9.43/9.62 cnf(i_0_1318, plain, (spatiallydisjointobjecttype(f_subcollectionofwithrelationfromtypefn(c_humanshelterconstruction,c_damages,f_subcollectionofwithrelationtofn(c_aerialattack,c_performedby,f_armyfn(c_israel)))))). % 9.43/9.62 cnf(i_0_913, plain, (termofunit(f_mapfn_individual(f_borderbetweenpolitiesfn(c_iraq,c_syria)),f_mapfn_individual(f_borderbetweenpolitiesfn(c_iraq,c_syria))))). % 9.43/9.62 cnf(i_0_351, plain, (termofunit(f_subcollectionofwithrelationtotypefn(c_thenchead,c_outputscreated,c_thencmodifier),f_subcollectionofwithrelationtotypefn(c_thenchead,c_outputscreated,c_thencmodifier)))). % 9.43/9.62 cnf(i_0_362, plain, (termofunit(f_subcollectionofwithrelationtotypefn(c_thenchead,c_objectactedon,c_thencmodifier),f_subcollectionofwithrelationtotypefn(c_thenchead,c_objectactedon,c_thencmodifier)))). % 9.43/9.62 cnf(i_0_349, plain, (termofunit(f_subcollectionofwithrelationtotypefn(c_thenchead,c_groupmembers,c_thencmodifier),f_subcollectionofwithrelationtotypefn(c_thenchead,c_groupmembers,c_thencmodifier)))). % 9.43/9.62 cnf(i_0_1107, plain, (termofunit(f_subcollectionofwithrelationtotypefn(c_selectingsomething,c_chosenitem,c_creditcard),f_subcollectionofwithrelationtotypefn(c_selectingsomething,c_chosenitem,c_creditcard)))). % 9.43/9.62 cnf(i_0_1110, plain, (termofunit(f_subcollectionofwithrelationtotypefn(c_selectingsomething,c_choices,c_weapon),f_subcollectionofwithrelationtotypefn(c_selectingsomething,c_choices,c_weapon)))). % 9.43/9.62 cnf(i_0_1121, plain, (termofunit(f_subcollectionofwithrelationtotypefn(c_division_militaryechelon,c_groupmembers,c_armypersonnel),f_subcollectionofwithrelationtotypefn(c_division_militaryechelon,c_groupmembers,c_armypersonnel)))). % 9.43/9.62 cnf(i_0_1141, plain, (termofunit(f_subcollectionofwithrelationtotypefn(c_transferofcontrol,c_objectofcontroltransfer,c_group),f_subcollectionofwithrelationtotypefn(c_transferofcontrol,c_objectofcontroltransfer,c_group)))). % 9.43/9.62 cnf(i_0_691, plain, (termofunit(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_colombia),f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_colombia)))). % 9.43/9.62 cnf(i_0_688, plain, (termofunit(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_sudan),f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_sudan)))). % 9.43/9.62 cnf(i_0_647, plain, (termofunit(f_attacktypebytargettypefn(c_terroristsuicidebombing,f_collectionintersection2fn(c_israeliperson,c_civilian)),f_attacktypebytargettypefn(c_terroristsuicidebombing,f_collectionintersection2fn(c_israeliperson,c_civilian))))). % 9.43/9.62 cnf(i_0_709, plain, (termofunit(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_turkey),f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_turkey)))). % 9.43/9.62 cnf(i_0_693, plain, (termofunit(f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_lebanon),f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_lebanon)))). % 9.43/9.62 cnf(i_0_997, plain, (termofunit(f_subcollectionofwithrelationfromfn(c_transportationdevice_vehicle,c_owns,c_unitednationsorganization),f_subcollectionofwithrelationfromfn(c_transportationdevice_vehicle,c_owns,c_unitednationsorganization)))). % 9.43/9.62 cnf(i_0_1033, plain, (termofunit(f_subcollectionofwithrelationfromfn(c_personwithoccupation,c_performsinstancesaspartofjob,c_training),f_subcollectionofwithrelationfromfn(c_personwithoccupation,c_performsinstancesaspartofjob,c_training)))). % 9.43/9.62 cnf(i_0_1124, plain, (termofunit(f_subcollectionofwithrelationfromfn(c_baseballteam,c_groupmembers,c_minorleaguebaseball),f_subcollectionofwithrelationfromfn(c_baseballteam,c_groupmembers,c_minorleaguebaseball)))). % 9.43/9.62 cnf(i_0_940, plain, (termofunit(f_subcollectionofwithrelationtofn(c_terrorist,c_occupation,c_militaryperson),f_subcollectionofwithrelationtofn(c_terrorist,c_occupation,c_militaryperson)))). % 9.43/9.62 cnf(i_0_1331, plain, (termofunit(f_subcollectionofwithrelationtofn(c_terrorist,c_birthplace,c_iran),f_subcollectionofwithrelationtofn(c_terrorist,c_birthplace,c_iran)))). % 9.43/9.62 cnf(i_0_1278, plain, (termofunit(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_spain),f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_spain)))). % 9.43/9.62 cnf(i_0_401, plain, (termofunit(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_unitedstatesofamerica),f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_925, plain, (termofunit(f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_iraq),f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_iraq)))). % 9.43/9.62 cnf(i_0_927, plain, (termofunit(f_attacktypebytargettypefn(c_shootingattack_gun,f_collectionintersection2fn(c_soldier,c_unitedstatesperson)),f_attacktypebytargettypefn(c_shootingattack_gun,f_collectionintersection2fn(c_soldier,c_unitedstatesperson))))). % 9.43/9.62 cnf(i_0_1333, plain, (termofunit(f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_iran),f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_iran)))). % 9.43/9.62 cnf(i_0_1430, plain, (termofunit(f_subcollectionofwithrelationtofn(c_terroristgroup,c_armedwithweapontype,c_bomb),f_subcollectionofwithrelationtofn(c_terroristgroup,c_armedwithweapontype,c_bomb)))). % 9.43/9.62 cnf(i_0_1023, plain, (termofunit(f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_saudiperson),f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_saudiperson)))). % 9.43/9.62 cnf(i_0_342, plain, (termofunit(f_subcollectionofwithrelationtofn(c_thenchead,c_performedby,c_thencmodifier),f_subcollectionofwithrelationtofn(c_thenchead,c_performedby,c_thencmodifier)))). % 9.43/9.62 cnf(i_0_1265, plain, (termofunit(f_logicalfieldfn(c_edb_entityattribute_ls,c_place,n_1),f_logicalfieldfn(c_edb_entityattribute_ls,c_place,n_1)))). % 9.43/9.62 cnf(i_0_1239, plain, (genls(f_subcollectionofwithrelationtotypefn(c_disembarkingfromatransportationdevice,c_fromlocation,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)),c_disembarkingfromatransportationdevice))). % 9.43/9.62 cnf(i_0_1235, plain, (genls(f_subcollectionofwithrelationtofn(c_facility_construct,c_primaryactivitytypeoflocation,f_subcollectionofwithrelationtotypefn(c_maintainingsomething,c_objecttakencareof,c_transformer_electric)),c_spatialthing_localized))). % 9.43/9.62 cnf(i_0_1232, plain, (genls(f_subcollectionofwithrelationtofn(c_oilpipeline,c_primaryactivitytypeoflocation,f_subcollectionofwithrelationtotypefn(c_maintainingsomething,c_objecttakencareof,c_subway)),c_spatialthing_localized))). % 9.43/9.62 cnf(i_0_1322, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_humanshelterconstruction,c_damages,f_subcollectionofwithrelationtofn(c_aerialattack,c_performedby,f_armyfn(c_israel))),c_humanshelterconstruction))). % 9.43/9.62 cnf(i_0_1675, plain, (genls(f_subcollectionofwithrelationfromtypefn(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_geographicalsubregions,c_stream),c_eventoccursat,c_whirlingoffluid),f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_eventoccursat,c_whirlingoffluid)))). % 9.43/9.62 cnf(i_0_1157, plain, (termofunit(f_subcollectionofwithrelationfromfn(c_monetaryvalue,c_salescommission,f_somefn(c_buying)),f_subcollectionofwithrelationfromfn(c_monetaryvalue,c_salescommission,f_somefn(c_buying))))). % 9.43/9.62 cnf(i_0_1222, plain, (genls(f_subcollectionofwithrelationtofn(f_subcollectionofwithrelationfromfn(c_facility_generic,c_operatesfacilities,c_unitedstatesfederalgovernment),c_objectfoundinlocation,f_territoryfn(c_panama)),c_spatialthing_nonsituational))). % 9.43/9.62 cnf(i_0_1433, plain, (genls(f_nthsubsituationtypeoftypefn(f_subcollectionofwithrelationtotypefn(c_investing,c_objectpaidfor,f_sharesinfundtypefn(c_hedgefund)),f_buyingfn(c_putoption),n_1),c_situation))). % 9.43/9.62 cnf(i_0_385, plain, (genls(f_attacktypebytargettypefn(c_bombing,f_subcollectionofwithrelationtofn(c_building,c_primaryactivitytypeoflocation,f_subcollectionofwithrelationtotypefn(c_maintainingsomething,c_objecttakencareof,c_militaryorganization))),c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_1437, plain, (genls(f_nthsubsituationtypeoftypefn(f_subcollectionofwithrelationtotypefn(c_investing,c_objectpaidfor,f_sharesinfundtypefn(c_hedgefund)),f_buyingfn(c_putoption),n_1),f_buyingfn(c_putoption)))). % 9.43/9.62 cnf(i_0_1012, plain, (firstordercollection(f_subcollectionofwithrelationtofn(f_subcollectionofwithrelationtotypefn(c_militaryattack,c_intendedattacktargets,f_subcollectionofwithrelationfromtypefn(c_somethingexisting,c_possesses,c_civilian)),c_eventoccursat,f_southernregionfn(c_lebanon))))). % 9.43/9.62 cnf(i_0_1117, plain, (genls(f_subcollectionofwithrelationtofn(f_subcollectionofwithrelationtotypefn(c_division_militaryechelon,c_groupmembers,c_armypersonnel),c_affiliatedwith,c_unitedstatesofamerica),f_subcollectionofwithrelationtotypefn(c_division_militaryechelon,c_groupmembers,c_armypersonnel)))). % 9.43/9.62 cnf(i_0_1668, plain, (termofunit(f_subcollectionofwithrelationfromtypefn(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_geographicalsubregions,c_stream),c_eventoccursat,c_whirlingoffluid),f_subcollectionofwithrelationfromtypefn(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_geographicalsubregions,c_stream),c_eventoccursat,c_whirlingoffluid)))). % 9.43/9.62 cnf(i_0_1001, plain, (genls(f_subcollectionofwithrelationtofn(f_subcollectionofwithrelationtotypefn(c_militaryattack,c_intendedattacktargets,f_subcollectionofwithrelationfromtypefn(c_somethingexisting,c_possesses,c_civilian)),c_eventoccursat,f_southernregionfn(c_lebanon)),c_individual))). % 9.43/9.62 cnf(i_0_928, plain, (termofunit(f_attacktypebytargettypefn(c_bombing,f_subcollectionofwithrelationtotypefn(c_administrator,c_affiliatedwith,c_unitedstatesperson)),f_attacktypebytargettypefn(c_bombing,f_subcollectionofwithrelationtotypefn(c_administrator,c_affiliatedwith,c_unitedstatesperson))))). % 9.43/9.62 cnf(i_0_993, plain, (termofunit(f_subcollectionofwithrelationfromfn(f_subcollectionofwithrelationfromtypefn(c_transportationdevice_vehicle,c_owns,c_army_militaryechelon),c_possessiverelation,c_israel),f_subcollectionofwithrelationfromfn(f_subcollectionofwithrelationfromtypefn(c_transportationdevice_vehicle,c_owns,c_army_militaryechelon),c_possessiverelation,c_israel)))). % 9.43/9.62 cnf(i_0_258, plain, (termofunit(f_attacktypebytargettypefn(c_murder,f_subcollectionofwithrelationfromfn(c_person,c_citizens,f_somefn(c_geopoliticalentity))),f_attacktypebytargettypefn(c_murder,f_subcollectionofwithrelationfromfn(c_person,c_citizens,f_somefn(c_geopoliticalentity)))))). % 9.43/9.62 cnf(i_0_941, plain, (termofunit(f_attacktypebytargettypefn(c_shootingattack_gun,f_subcollectionofwithrelationfromfn(c_militaryperson,c_hasmembers,f_armedforcesfn(c_unitedstatesofamerica))),f_attacktypebytargettypefn(c_shootingattack_gun,f_subcollectionofwithrelationfromfn(c_militaryperson,c_hasmembers,f_armedforcesfn(c_unitedstatesofamerica)))))). % 9.43/9.62 cnf(i_0_433, plain, (genls(f_subcollectionofwithrelationtotypefn(f_subcollectionofwithrelationtotypefn(c_monetaryexchangeofuserrights,c_buyer,f_sharesinfundtypefn(c_hedgefund)),c_performedby,f_subcollectionofwithrelationtotypefn(c_person,c_financialstate,c_wealthy)),f_subcollectionofwithrelationtotypefn(c_monetaryexchangeofuserrights,c_buyer,f_sharesinfundtypefn(c_hedgefund))))). % 9.43/9.62 cnf(i_0_434, plain, (termofunit(f_nthsubsituationtypeoftypefn(c_investinginahedgefund,f_subcollectionofwithrelationtotypefn(f_subcollectionofwithrelationtotypefn(c_monetaryexchangeofuserrights,c_buyer,f_sharesinfundtypefn(c_hedgefund)),c_performedby,f_subcollectionofwithrelationtotypefn(c_person,c_financialstate,c_wealthy)),n_1),f_nthsubsituationtypeoftypefn(c_investinginahedgefund,f_subcollectionofwithrelationtotypefn(f_subcollectionofwithrelationtotypefn(c_monetaryexchangeofuserrights,c_buyer,f_sharesinfundtypefn(c_hedgefund)),c_performedby,f_subcollectionofwithrelationtotypefn(c_person,c_financialstate,c_wealthy)),n_1)))). % 9.43/9.62 cnf(i_0_1, negated_conjecture, (~tptptypes_5_802(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886))). % 9.43/9.62 cnf(i_0_796, plain, (~atemporalnecessarilyessentialcollectiontype(c_partiallytangible))). % 9.43/9.62 cnf(i_0_400, plain, (~atemporalnecessarilyessentialcollectiontype(c_geographicalregion))). % 9.43/9.62 cnf(i_0_798, plain, (~atemporalnecessarilyessentialcollectiontype(c_university))). % 9.43/9.62 cnf(i_0_1531, plain, (~antisymmetricbinarypredicate(c_temporallysubsumes))). % 9.43/9.62 cnf(i_0_446, plain, (~antisymmetricbinarypredicate(c_sisters))). % 9.43/9.62 cnf(i_0_1529, plain, (~antisymmetricbinarypredicate(c_personrepresentingagent))). % 9.43/9.62 cnf(i_0_1422, plain, (~spatiallydisjointobjecttype(f_groupfn(c_weapon)))). % 9.43/9.62 cnf(i_0_427, plain, (~atemporalnecessarilyessentialcollectiontype(f_groupfn(c_intelligentagent)))). % 9.43/9.62 cnf(i_0_843, plain, (~borderson(X1,X1))). % 9.43/9.62 cnf(i_0_1462, plain, (~negationpreds(X1,X1))). % 9.43/9.62 cnf(i_0_21, plain, (relationalnounslot(c_orientation)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_112, plain, (~collection(X1)|~individual(X1))). % 9.43/9.62 cnf(i_0_538, plain, (~setorcollection(X1)|~individual(X1))). % 9.43/9.62 cnf(i_0_612, plain, (~temporalobjecttype(X1)|~temporalstufftype(X1))). % 9.43/9.62 cnf(i_0_897, plain, (~situation(X1)|~strategictarget(X1))). % 9.43/9.62 cnf(i_0_1676, plain, (~facility_construct(X1)|~bodyofwater(X1))). % 9.43/9.62 cnf(i_0_1677, plain, (~pathforwheeledvehicles(X1)|~bodyofwater(X1))). % 9.43/9.62 cnf(i_0_519, plain, (~tptpcol_16_9111(X1)|~tptpcol_16_9110(X1))). % 9.43/9.62 cnf(i_0_1182, plain, (individual(X1)|~temporalthing(X1))). % 9.43/9.62 cnf(i_0_712, plain, (microtheory(X1)|~webgatheredgafmicrotheory(X1))). % 9.43/9.62 cnf(i_0_802, plain, (binarypredicate(X1)|~binaryrolepredicate(X1))). % 9.43/9.62 cnf(i_0_795, plain, (collection(X1)|~atemporalnecessarilyessentialcollectiontype(X1))). % 9.43/9.62 cnf(i_0_10, plain, (tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_8886)|~mtvisible(c_tptp_member2668_mt))). % 9.43/9.62 cnf(i_0_288, plain, (geographicalregion(X1)|~geolevel_4(X1))). % 9.43/9.62 cnf(i_0_287, plain, (geographicalregion(X1)|~geopoliticalregion(X1))). % 9.43/9.62 cnf(i_0_142, plain, (partiallytangible(X1)|~geographicalregion(X1))). % 9.43/9.62 cnf(i_0_1525, plain, (uniqueanatomicalparttype(c_faceofanimal)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1515, plain, (uniqueanatomicalparttype(c_anus)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_674, plain, (conceptnodesfortasktypefnintelligenceanalysistask_allotment(c_geopoliticalentity)|~mtvisible(c_analystdatabasemt))). % 9.43/9.62 cnf(i_0_1522, plain, (keclarifyingcollectiontype(c_plant)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1509, plain, (keclarifyingcollectiontype(c_nonhumananimal)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1673, plain, (naturalfeaturetype(c_stream)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_164, plain, (relationalnounslot(c_eventoccursat)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_1389, plain, (agent_generic(X1)|~intelligentagent(X1))). % 9.43/9.62 cnf(i_0_567, plain, (versionedsoftwareobject(X1)|~versionedprogram(X1))). % 9.43/9.62 cnf(i_0_1530, plain, (antisymmetricbinarypredicate(X1)|~orderingpredicate(X1))). % 9.43/9.62 cnf(i_0_815, plain, (relation(X1)|~function_denotational(X1))). % 9.43/9.62 cnf(i_0_162, plain, (relationalnounslot(c_byproducts)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_160, plain, (relationalnounslot(c_affiliatedwith)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_156, plain, (relationalnounslot(c_buyer)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_159, plain, (relationalnounslot(c_motherinlaw)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_1617, plain, (objectpredicate(X1)|~orderingpredicate(X1))). % 9.43/9.62 cnf(i_0_1613, plain, (objectpredicate(X1)|~agentpredicate(X1))). % 9.43/9.62 cnf(i_0_1614, plain, (objectpredicate(X1)|~attackrolereplacement(X1))). % 9.43/9.62 cnf(i_0_1616, plain, (objectpredicate(X1)|~visualibtvisualfeaturepredicate(X1))). % 9.43/9.62 cnf(i_0_157, plain, (relationalnounslot(c_hasphysicalattractiveness)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_166, plain, (relationalnounslot(c_pathterminus)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_161, plain, (relationalnounslot(c_fatherinlaw)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_163, plain, (relationalnounslot(c_sisterinlaw)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_896, plain, (intangibleindividual(X1)|~situation(X1))). % 9.43/9.62 cnf(i_0_1636, plain, (cartographicfeaturetype(X1)|~naturalfeaturetype(X1))). % 9.43/9.62 cnf(i_0_1680, plain, (bodyofwater(X1)|~subcollectionofwithrelationfromtypefnbodyofwaterpathterminusstream(X1))). % 9.43/9.62 cnf(i_0_158, plain, (relationalnounslot(c_sisters)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_165, plain, (relationalnounslot(c_tasteofobject)|~mtvisible(c_generallexiconmt))). % 9.43/9.62 cnf(i_0_1269, plain, (cartographicfeaturetype(c_place)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1631, plain, (cartographicfeaturetype(c_channel_deeperwaterwaypart)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1628, plain, (cartographicfeaturetype(c_naturalelevation)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1632, plain, (cartographicfeaturetype(c_forestclearing)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1654, plain, (transportation_topic(c_ship)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1653, plain, (transportation_topic(c_helicopter)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1647, plain, (transportation_topic(c_street_generic)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1648, plain, (transportation_topic(c_train_transportationdevice)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1655, plain, (transportation_topic(c_transporter)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1646, plain, (transportation_topic(c_horse_domesticated)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_468, plain, (transportation_topic(c_pathterminus)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1650, plain, (transportation_topic(c_airtransportationevent)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1656, plain, (transportation_topic(c_trajectorypassesthrough)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1649, plain, (transportation_topic(c_landtransportationevent)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1651, plain, (transportation_topic(c_airportorganization)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1652, plain, (transportation_topic(c_pathartifact)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1657, plain, (transportation_topic(c_dock)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_1466, plain, (commercialactivities_financial_topic(c_seller)|~mtvisible(c_topicmt))). % 9.43/9.62 cnf(i_0_906, plain, (genls(c_femalechild,c_humanchild)|~mtvisible(c_biologyvocabularymt))). % 9.43/9.62 cnf(i_0_290, plain, (geographicalthing(X1)|~geographicalregion(X1))). % 9.43/9.62 cnf(i_0_505, plain, (tptpcol_3_3(X1)|~tptpcol_4_8195(X1))). % 9.43/9.62 cnf(i_0_1034, plain, (genls(c_officerinorganization,c_personwithoccupation)|~mtvisible(c_jobmt))). % 9.43/9.62 cnf(i_0_1263, plain, (genls(c_tree_theplant,c_place)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_20, plain, (isa(X1,c_partiallytangible)|~partiallytangible(X1))). % 9.43/9.62 cnf(i_0_25, plain, (isa(X1,c_orientationvector)|~orientationvector(X1))). % 9.43/9.62 cnf(i_0_1255, plain, (spatialthing_nonsituational(X1)|~subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(X1))). % 9.43/9.62 cnf(i_0_1556, plain, (cotemporalpredicate(X1)|~coexistingobjectspredicate(X1))). % 9.43/9.62 cnf(i_0_1679, plain, (topographicalfeature(X1)|~bodyofwater(X1))). % 9.43/9.62 cnf(i_0_27, plain, (firstordercollection(X1)|~tptptypes_6_803(X2,X1))). % 9.43/9.62 cnf(i_0_13, plain, (isa(X1,c_tptpcol_16_8886)|~tptpcol_16_8886(X1))). % 9.43/9.62 cnf(i_0_8, plain, (firstordercollection(X1)|~tptptypes_5_802(X2,X1))). % 9.43/9.62 cnf(i_0_9, plain, (firstordercollection(X1)|~tptptypes_5_802(X1,X2))). % 9.43/9.62 cnf(i_0_6, plain, (genls(X1,c_orientationvector)|~tptptypes_5_802(X1,X2))). % 9.43/9.62 cnf(i_0_33, plain, (firstordercollection(X1)|~tptptypes_6_818(X2,X1))). % 9.43/9.62 cnf(i_0_49, plain, (firstordercollection(X1)|~tptptypes_9_824(X2,X1))). % 9.43/9.62 cnf(i_0_206, plain, (firstordercollection(X1)|~tptptypes_8_823(X2,X1))). % 9.43/9.62 cnf(i_0_45, plain, (tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_14_8433)|~mtvisible(c_tptp_spindleheadmt))). % 9.43/9.62 cnf(i_0_47, plain, (tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_16_9111)|~mtvisible(c_tptp_spindleheadmt))). % 9.43/9.62 cnf(i_0_48, plain, (tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_15_8464)|~mtvisible(c_tptp_spindleheadmt))). % 9.43/9.62 cnf(i_0_50, plain, (tptptypes_9_824(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_15_8510)|~mtvisible(c_currentworlddatacollectormt_nonhomocentric))). % 9.43/9.62 cnf(i_0_192, plain, (firstordercollection(X1)|~tptptypes_7_819(X2,X1))). % 9.43/9.62 cnf(i_0_194, plain, (firstordercollection(X1)|~tptptypes_5_771(X2,X1))). % 9.43/9.62 cnf(i_0_36, plain, (firstordercollection(X1)|~tptptypes_4_770(X2,X1))). % 9.43/9.62 cnf(i_0_191, plain, (tptptypes_7_819(f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_12_12070)|~mtvisible(c_cyclistsmt))). % 9.43/9.62 cnf(i_0_23, plain, (isa(X1,f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible))|~subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(X1))). % 9.43/9.62 cnf(i_0_19, plain, (partiallytangible(X1)|~isa(X1,c_partiallytangible))). % 9.43/9.62 cnf(i_0_24, plain, (orientationvector(X1)|~isa(X1,c_orientationvector))). % 9.43/9.62 cnf(i_0_187, plain, (firstordercollection(X1)|~tptptypes_7_826(X2,X1))). % 9.43/9.62 cnf(i_0_28, plain, (firstordercollection(X1)|~tptptypes_6_803(X1,X2))). % 9.43/9.62 cnf(i_0_34, plain, (firstordercollection(X1)|~tptptypes_6_818(X1,X2))). % 9.43/9.62 cnf(i_0_54, plain, (firstordercollection(X1)|~tptptypes_9_824(X1,X2))). % 9.43/9.62 cnf(i_0_12, plain, (tptpcol_16_8886(X1)|~isa(X1,c_tptpcol_16_8886))). % 9.43/9.62 cnf(i_0_207, plain, (firstordercollection(X1)|~tptptypes_8_823(X1,X2))). % 9.43/9.62 cnf(i_0_193, plain, (firstordercollection(X1)|~tptptypes_7_819(X1,X2))). % 9.43/9.62 cnf(i_0_196, plain, (firstordercollection(X1)|~tptptypes_5_771(X1,X2))). % 9.43/9.62 cnf(i_0_37, plain, (firstordercollection(X1)|~tptptypes_4_770(X1,X2))). % 9.43/9.62 cnf(i_0_188, plain, (firstordercollection(X1)|~tptptypes_7_826(X1,X2))). % 9.43/9.62 cnf(i_0_115, plain, (collection(X1)|~disjointwith(X2,X1))). % 9.43/9.62 cnf(i_0_130, plain, (collection(X1)|~arg2isa(X2,X1))). % 9.43/9.62 cnf(i_0_128, plain, (collection(X1)|~hlprototypicalinstance(X2,X1))). % 9.43/9.62 cnf(i_0_124, plain, (collection(X1)|~arg1isa(X2,X1))). % 9.43/9.62 cnf(i_0_1345, plain, (collection(X1)|~resultgenl(X2,X1))). % 9.43/9.62 cnf(i_0_491, plain, (collection(X1)|~arg2genl(X2,X1))). % 9.43/9.62 cnf(i_0_132, plain, (collection(X1)|~disjointwith(X1,X2))). % 9.43/9.62 cnf(i_0_297, plain, (geographicalregion(X1)|~borderson(X2,X1))). % 9.43/9.62 cnf(i_0_291, plain, (geographicalregion(X1)|~geographicalsubregions(X2,X1))). % 9.43/9.62 cnf(i_0_298, plain, (geographicalregion(X1)|~borderson(X1,X2))). % 9.43/9.62 cnf(i_0_292, plain, (geographicalregion(X1)|~geographicalsubregions(X1,X2))). % 9.43/9.62 cnf(i_0_144, plain, (partiallytangible(X1)|~tptpofobject(X1,X2))). % 9.43/9.62 cnf(i_0_1504, plain, (predicate(X1)|~arg2format(X1,X2))). % 9.43/9.62 cnf(i_0_1561, plain, (predicate(X1)|~arg1format(X1,X2))). % 9.43/9.62 cnf(i_0_512, plain, (tptpcol_4_8195(X1)|~tptp_6_72(X2,X1))). % 9.43/9.62 cnf(i_0_507, plain, (tptpcol_4_8195(X1)|~tptp_8_625(X2,X1))). % 9.43/9.62 cnf(i_0_508, plain, (tptpcol_4_8195(X1)|~tptp_7_79(X2,X1))). % 9.43/9.62 cnf(i_0_513, plain, (tptpcol_4_8195(X1)|~tptp_7_537(X1,X2))). % 9.43/9.62 cnf(i_0_511, plain, (tptpcol_4_8195(X1)|~tptp_8_886(X1,X2))). % 9.43/9.62 cnf(i_0_506, plain, (tptpcol_4_8195(X1)|~tptp_9_495(X1,X2))). % 9.43/9.62 cnf(i_0_811, plain, (nonnegativeinteger(X1)|~aritymin(X2,X1))). % 9.43/9.62 cnf(i_0_810, plain, (nonnegativeinteger(X1)|~arity(X2,X1))). % 9.43/9.62 cnf(i_0_809, plain, (nonnegativeinteger(X1)|~aritymax(X2,X1))). % 9.43/9.62 cnf(i_0_831, plain, (relation(X1)|~arg2isa(X1,X2))). % 9.43/9.62 cnf(i_0_814, plain, (relation(X1)|~arg4isa(X1,X2))). % 9.43/9.62 cnf(i_0_828, plain, (relation(X1)|~arg1isa(X1,X2))). % 9.43/9.62 cnf(i_0_813, plain, (relation(X1)|~arg3isa(X1,X2))). % 9.43/9.62 cnf(i_0_826, plain, (relation(X1)|~arg1genl(X1,X2))). % 9.43/9.62 cnf(i_0_825, plain, (relation(X1)|~quotedargument(X1,X2))). % 9.43/9.62 cnf(i_0_824, plain, (relation(X1)|~resultgenl(X1,X2))). % 9.43/9.62 cnf(i_0_492, plain, (relation(X1)|~arg2genl(X1,X2))). % 9.43/9.62 cnf(i_0_823, plain, (relation(X1)|~resultisa(X1,X2))). % 9.43/9.62 cnf(i_0_822, plain, (relation(X1)|~argsisa(X1,X2))). % 9.43/9.62 cnf(i_0_817, plain, (relation(X1)|~arg3genl(X1,X2))). % 9.43/9.62 cnf(i_0_816, plain, (relation(X1)|~arg2quotedisa(X1,X2))). % 9.43/9.62 cnf(i_0_818, plain, (relation(X1)|~arg1quotedisa(X1,X2))). % 9.43/9.62 cnf(i_0_1559, plain, (intangibleindividual(X1)|~arg1format(X2,X1))). % 9.43/9.62 cnf(i_0_521, plain, (subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(X1)|~tptp_9_166(X1,X2))). % 9.43/9.62 cnf(i_0_1682, plain, (bodyofwater(X1)|~linkedbybodyofwater(X2,X1))). % 9.43/9.62 cnf(i_0_1681, plain, (bodyofwater(X1)|~flowsintoregion(X1,X2))). % 9.43/9.62 cnf(i_0_1683, plain, (bodyofwater(X1)|~linkedbybodyofwater(X1,X2))). % 9.43/9.62 cnf(i_0_1629, plain, (cartographicfeaturetype(X1)|~regiontypebyterrain(X1)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1105, plain, (isa(X1,c_date)|~date(X1))). % 9.43/9.62 cnf(i_0_22, plain, (subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible)))). % 9.43/9.62 cnf(i_0_1508, plain, (uniqueanatomicalparttype(f_rightobjectofpairfn(c_malar))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1096, plain, (isa(X1,c_firstordercollection)|~firstordercollection(X1))). % 9.43/9.62 cnf(i_0_1574, plain, (isa(X1,c_purposefulaction)|~purposefulaction(X1))). % 9.43/9.62 cnf(i_0_1080, plain, (isa(X1,c_animal)|~animal(X1))). % 9.43/9.62 cnf(i_0_303, plain, (isa(X1,c_homosapiens)|~homosapiens(X1))). % 9.43/9.62 cnf(i_0_172, plain, (mtvisible(X1)|~genlmt(X2,X1)|~mtvisible(X2))). % 9.43/9.62 cnf(i_0_325, plain, (isa(X1,c_organization)|~organization(X1))). % 9.43/9.62 cnf(i_0_421, plain, (isa(X1,c_agent_generic)|~agent_generic(X1))). % 9.43/9.62 cnf(i_0_1513, plain, (uniqueanatomicalparttype(f_rightobjectofpairfn(c_breast))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_382, plain, (isa(X1,c_individual)|~individual(X1))). % 9.43/9.62 cnf(i_0_1058, plain, (isa(X1,c_artifact)|~artifact(X1))). % 9.43/9.62 cnf(i_0_431, plain, (isa(X1,c_intelligentagent)|~intelligentagent(X1))). % 9.43/9.62 cnf(i_0_1412, plain, (isa(X1,c_malehuman)|~malehuman(X1))). % 9.43/9.62 cnf(i_0_121, plain, (isa(X1,c_collection)|~collection(X1))). % 9.43/9.62 cnf(i_0_307, plain, (isa(X1,c_situation)|~situation(X1))). % 9.43/9.62 cnf(i_0_1177, plain, (isa(X1,c_microtheory)|~microtheory(X1))). % 9.43/9.62 cnf(i_0_679, plain, (isa(X1,c_geopoliticalentity)|~geopoliticalentity(X1))). % 9.43/9.62 cnf(i_0_1517, plain, (uniqueanatomicalparttype(f_rightobjectofpairfn(c_radius_bone))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1685, plain, (isa(X1,c_bodyofwater)|~bodyofwater(X1))). % 9.43/9.62 cnf(i_0_1032, plain, (isa(X1,c_computerprogram_cw)|~computerprogram_cw(X1))). % 9.43/9.62 cnf(i_0_295, plain, (isa(X1,c_geographicalregion)|~geographicalregion(X1))). % 9.43/9.62 cnf(i_0_1154, plain, (isa(X1,c_group)|~group(X1))). % 9.43/9.62 cnf(i_0_546, plain, (isa(X1,c_setorcollection)|~setorcollection(X1))). % 9.43/9.62 cnf(i_0_1565, plain, (isa(X1,c_physicalcreationordestructionevent)|~physicalcreationordestructionevent(X1))). % 9.43/9.62 cnf(i_0_186, plain, (isa(X1,c_tptpcol_4_8195)|~tptpcol_4_8195(X1))). % 9.43/9.62 cnf(i_0_487, plain, (isa(X1,c_tptpcol_3_3)|~tptpcol_3_3(X1))). % 9.43/9.62 cnf(i_0_1514, plain, (uniqueanatomicalparttype(f_rightobjectofpairfn(c_trapezoidbone))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1407, plain, (isa(X1,c_femalehuman)|~femalehuman(X1))). % 9.43/9.62 cnf(i_0_1165, plain, (isa(X1,c_buying)|~buying(X1))). % 9.43/9.62 cnf(i_0_1427, plain, (isa(X1,c_weapon)|~weapon(X1))). % 9.43/9.62 cnf(i_0_808, plain, (isa(X1,c_nonnegativeinteger)|~nonnegativeinteger(X1))). % 9.43/9.62 cnf(i_0_1139, plain, (isa(X1,c_action)|~action(X1))). % 9.43/9.62 cnf(i_0_1273, plain, (isa(X1,c_place)|~place(X1))). % 9.43/9.62 cnf(i_0_961, plain, (isa(X1,c_militaryperson)|~militaryperson(X1))). % 9.43/9.62 cnf(i_0_820, plain, (isa(X1,c_relation)|~relation(X1))). % 9.43/9.62 cnf(i_0_1519, plain, (uniqueanatomicalparttype(f_rightobjectofpairfn(c_eighthrib))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1132, plain, (isa(X1,c_temporalthing)|~temporalthing(X1))). % 9.43/9.62 cnf(i_0_1238, plain, (isa(X1,c_spatialthing_localized)|~spatialthing_localized(X1))). % 9.43/9.62 cnf(i_0_1071, plain, (isa(X1,c_organism_whole)|~organism_whole(X1))). % 9.43/9.62 cnf(i_0_1194, plain, (isa(X1,c_existingobjecttype)|~existingobjecttype(X1))). % 9.43/9.62 cnf(i_0_1046, plain, (isa(X1,c_personwithoccupation)|~personwithoccupation(X1))). % 9.43/9.62 cnf(i_0_1230, plain, (isa(X1,c_hostilesocialaction)|~hostilesocialaction(X1))). % 9.43/9.62 cnf(i_0_203, plain, (isa(X1,c_tptpcol_14_8433)|~tptpcol_14_8433(X1))). % 9.43/9.62 cnf(i_0_1598, plain, (isa(X1,c_personalassociationpredicate)|~personalassociationpredicate(X1))). % 9.43/9.62 cnf(i_0_1512, plain, (uniqueanatomicalparttype(f_leftobjectofpairfn(c_ninthrib))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1645, plain, (isa(X1,c_ditch)|~ditch(X1))). % 9.43/9.62 cnf(i_0_1451, plain, (isa(X1,c_monetaryexchangeofuserrights)|~monetaryexchangeofuserrights(X1))). % 9.43/9.62 cnf(i_0_1612, plain, (isa(X1,c_taste)|~taste(X1))). % 9.43/9.62 cnf(i_0_1640, plain, (isa(X1,c_cartographicfeaturetype)|~cartographicfeaturetype(X1))). % 9.43/9.62 cnf(i_0_1181, plain, (isa(X1,c_creationevent)|~creationevent(X1))). % 9.43/9.62 cnf(i_0_1609, plain, (isa(X1,c_ediblestuff)|~ediblestuff(X1))). % 9.43/9.62 cnf(i_0_1619, plain, (isa(X1,c_objectpredicate)|~objectpredicate(X1))). % 9.43/9.62 cnf(i_0_1537, plain, (isa(X1,c_antisymmetricbinarypredicate)|~antisymmetricbinarypredicate(X1))). % 9.43/9.62 cnf(i_0_1523, plain, (uniqueanatomicalparttype(f_leftobjectofpairfn(c_eleventhrib))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_210, plain, (isa(X1,c_tptpcol_16_9111)|~tptpcol_16_9111(X1))). % 9.43/9.62 cnf(i_0_214, plain, (isa(X1,c_tptpcol_15_8464)|~tptpcol_15_8464(X1))). % 9.43/9.62 cnf(i_0_518, plain, (isa(X1,c_tptpcol_16_9110)|~tptpcol_16_9110(X1))). % 9.43/9.62 cnf(i_0_217, plain, (isa(X1,c_tptpcol_15_8510)|~tptpcol_15_8510(X1))). % 9.43/9.62 cnf(i_0_515, plain, (isa(X1,c_tptpcol_12_12070)|~tptpcol_12_12070(X1))). % 9.43/9.62 cnf(i_0_1095, plain, (firstordercollection(X1)|~isa(X1,c_firstordercollection))). % 9.43/9.62 cnf(i_0_381, plain, (individual(X1)|~isa(X1,c_individual))). % 9.43/9.62 cnf(i_0_1176, plain, (microtheory(X1)|~isa(X1,c_microtheory))). % 9.43/9.62 cnf(i_0_1524, plain, (uniqueanatomicalparttype(f_leftobjectofpairfn(c_fourthrib))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1104, plain, (date(X1)|~isa(X1,c_date))). % 9.43/9.62 cnf(i_0_1193, plain, (existingobjecttype(X1)|~isa(X1,c_existingobjecttype))). % 9.43/9.62 cnf(i_0_120, plain, (collection(X1)|~isa(X1,c_collection))). % 9.43/9.62 cnf(i_0_294, plain, (geographicalregion(X1)|~isa(X1,c_geographicalregion))). % 9.43/9.62 cnf(i_0_1057, plain, (artifact(X1)|~isa(X1,c_artifact))). % 9.43/9.62 cnf(i_0_545, plain, (setorcollection(X1)|~isa(X1,c_setorcollection))). % 9.43/9.62 cnf(i_0_420, plain, (agent_generic(X1)|~isa(X1,c_agent_generic))). % 9.43/9.62 cnf(i_0_1326, plain, (geographicalregion(f_northernregionfn(c_iran))|~mtvisible(c_worldpoliticalgeographydatavocabularymt))). % 9.43/9.62 cnf(i_0_1411, plain, (malehuman(X1)|~isa(X1,c_malehuman))). % 9.43/9.62 cnf(i_0_1153, plain, (group(X1)|~isa(X1,c_group))). % 9.43/9.62 cnf(i_0_185, plain, (tptpcol_4_8195(X1)|~isa(X1,c_tptpcol_4_8195))). % 9.43/9.62 cnf(i_0_486, plain, (tptpcol_3_3(X1)|~isa(X1,c_tptpcol_3_3))). % 9.43/9.62 cnf(i_0_1272, plain, (place(X1)|~isa(X1,c_place))). % 9.43/9.62 cnf(i_0_306, plain, (situation(X1)|~isa(X1,c_situation))). % 9.43/9.62 cnf(i_0_807, plain, (nonnegativeinteger(X1)|~isa(X1,c_nonnegativeinteger))). % 9.43/9.62 cnf(i_0_1426, plain, (weapon(X1)|~isa(X1,c_weapon))). % 9.43/9.62 cnf(i_0_836, plain, (geopoliticalregion(f_territoryfn(c_southdakota_state))|~mtvisible(c_unitedstatesgeographymt))). % 9.43/9.62 cnf(i_0_302, plain, (homosapiens(X1)|~isa(X1,c_homosapiens))). % 9.43/9.62 cnf(i_0_430, plain, (intelligentagent(X1)|~isa(X1,c_intelligentagent))). % 9.43/9.62 cnf(i_0_1406, plain, (femalehuman(X1)|~isa(X1,c_femalehuman))). % 9.43/9.62 cnf(i_0_1131, plain, (temporalthing(X1)|~isa(X1,c_temporalthing))). % 9.43/9.62 cnf(i_0_1079, plain, (animal(X1)|~isa(X1,c_animal))). % 9.43/9.62 cnf(i_0_1536, plain, (antisymmetricbinarypredicate(X1)|~isa(X1,c_antisymmetricbinarypredicate))). % 9.43/9.62 cnf(i_0_819, plain, (relation(X1)|~isa(X1,c_relation))). % 9.43/9.62 cnf(i_0_1618, plain, (objectpredicate(X1)|~isa(X1,c_objectpredicate))). % 9.43/9.62 cnf(i_0_834, plain, (geopoliticalregion(f_territoryfn(c_jammuandkashmir_stateindia))|~mtvisible(c_worldgeographymt))). % 9.43/9.62 cnf(i_0_324, plain, (organization(X1)|~isa(X1,c_organization))). % 9.43/9.62 cnf(i_0_678, plain, (geopoliticalentity(X1)|~isa(X1,c_geopoliticalentity))). % 9.43/9.62 cnf(i_0_1237, plain, (spatialthing_localized(X1)|~isa(X1,c_spatialthing_localized))). % 9.43/9.62 cnf(i_0_1031, plain, (computerprogram_cw(X1)|~isa(X1,c_computerprogram_cw))). % 9.43/9.62 cnf(i_0_1639, plain, (cartographicfeaturetype(X1)|~isa(X1,c_cartographicfeaturetype))). % 9.43/9.62 cnf(i_0_1644, plain, (ditch(X1)|~isa(X1,c_ditch))). % 9.43/9.62 cnf(i_0_1164, plain, (buying(X1)|~isa(X1,c_buying))). % 9.43/9.62 cnf(i_0_1070, plain, (organism_whole(X1)|~isa(X1,c_organism_whole))). % 9.43/9.62 cnf(i_0_833, plain, (geopoliticalregion(f_territoryfn(c_china_peoplesrepublic))|~mtvisible(c_worldpoliticalgeographydatavocabularymt))). % 9.43/9.62 cnf(i_0_1573, plain, (purposefulaction(X1)|~isa(X1,c_purposefulaction))). % 9.43/9.62 cnf(i_0_1138, plain, (action(X1)|~isa(X1,c_action))). % 9.43/9.62 cnf(i_0_1597, plain, (personalassociationpredicate(X1)|~isa(X1,c_personalassociationpredicate))). % 9.43/9.62 cnf(i_0_1684, plain, (bodyofwater(X1)|~isa(X1,c_bodyofwater))). % 9.43/9.62 cnf(i_0_1229, plain, (hostilesocialaction(X1)|~isa(X1,c_hostilesocialaction))). % 9.43/9.62 cnf(i_0_960, plain, (militaryperson(X1)|~isa(X1,c_militaryperson))). % 9.43/9.62 cnf(i_0_1045, plain, (personwithoccupation(X1)|~isa(X1,c_personwithoccupation))). % 9.43/9.62 cnf(i_0_1608, plain, (ediblestuff(X1)|~isa(X1,c_ediblestuff))). % 9.43/9.62 cnf(i_0_837, plain, (geopoliticalregion(f_territoryfn(c_northernireland))|~mtvisible(c_worldgeographymt))). % 9.43/9.62 cnf(i_0_1180, plain, (creationevent(X1)|~isa(X1,c_creationevent))). % 9.43/9.62 cnf(i_0_1611, plain, (taste(X1)|~isa(X1,c_taste))). % 9.43/9.62 cnf(i_0_517, plain, (tptpcol_16_9110(X1)|~isa(X1,c_tptpcol_16_9110))). % 9.43/9.62 cnf(i_0_209, plain, (tptpcol_16_9111(X1)|~isa(X1,c_tptpcol_16_9111))). % 9.43/9.62 cnf(i_0_1450, plain, (monetaryexchangeofuserrights(X1)|~isa(X1,c_monetaryexchangeofuserrights))). % 9.43/9.62 cnf(i_0_514, plain, (tptpcol_12_12070(X1)|~isa(X1,c_tptpcol_12_12070))). % 9.43/9.62 cnf(i_0_216, plain, (tptpcol_15_8510(X1)|~isa(X1,c_tptpcol_15_8510))). % 9.43/9.62 cnf(i_0_213, plain, (tptpcol_15_8464(X1)|~isa(X1,c_tptpcol_15_8464))). % 9.43/9.62 cnf(i_0_835, plain, (geopoliticalregion(f_territoryfn(c_greece))|~mtvisible(c_worldpoliticalgeographydatavocabularymt))). % 9.43/9.62 cnf(i_0_1564, plain, (physicalcreationordestructionevent(X1)|~isa(X1,c_physicalcreationordestructionevent))). % 9.43/9.62 cnf(i_0_202, plain, (tptpcol_14_8433(X1)|~isa(X1,c_tptpcol_14_8433))). % 9.43/9.62 cnf(i_0_148, plain, (individual(X1)|~isa(X1,f_groupfn(c_thencmodifier)))). % 9.43/9.62 cnf(i_0_590, plain, (individual(X1)|~isa(X1,f_residentfn(c_israel)))). % 9.43/9.62 cnf(i_0_17, plain, (partiallytangible(X1)|~isa(X1,f_groupfn(c_partiallytangible)))). % 9.43/9.62 cnf(i_0_3, plain, (tptptypes_5_802(X1,X2)|~tptptypes_6_803(X1,X2))). % 9.43/9.62 cnf(i_0_4, plain, (tptptypes_5_802(X1,X2)|~tptptypes_6_818(X1,X2))). % 9.43/9.62 cnf(i_0_832, plain, (geopoliticalregion(f_territoryfn(c_nebraska_state))|~mtvisible(c_unitedstatesgeographymt))). % 9.43/9.62 cnf(i_0_1324, plain, (individual(X1)|~isa(X1,f_residentfn(c_iran)))). % 9.43/9.62 cnf(i_0_1336, plain, (individual(X1)|~isa(X1,f_residentfn(c_spain)))). % 9.43/9.62 cnf(i_0_551, plain, (individual(X1)|~isa(X1,f_residentfn(c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_916, plain, (individual(X1)|~isa(X1,f_residentfn(c_iraq)))). % 9.43/9.62 cnf(i_0_1357, plain, (redcrosssociety_national(f_nationalredcrosssocietyfn(c_turkey))|~mtvisible(c_worldpoliticalgeographydatavocabularymt))). % 9.43/9.62 cnf(i_0_1185, plain, (keclarifyingcollectiontype(f_treatmentfn(c_anthraxinfection))|~mtvisible(c_modernwesternmedicinemt))). % 9.43/9.62 cnf(i_0_1186, plain, (keclarifyingcollectiontype(f_treatmentfn(c_psychologicalailment))|~mtvisible(c_modernwesternmedicinemt))). % 9.43/9.62 cnf(i_0_1342, plain, (persontypebynationality(f_citizenfn(c_spain))|~mtvisible(c_worldpoliticalgeographydatavocabularymt))). % 9.43/9.62 cnf(i_0_922, plain, (groupfnsocialbeing(f_armyfn(c_iraq))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_1349, plain, (individual(X1)|~isa(X1,f_residentfn(c_turkey)))). % 9.43/9.62 cnf(i_0_375, plain, (individual(X1)|~isa(X1,f_exposureoforganismtoharmfulsubstancefn(c_thencmodifier)))). % 9.43/9.62 cnf(i_0_367, plain, (individual(X1)|~isa(X1,f_treatmentfn(c_thencmodifier)))). % 9.43/9.62 cnf(i_0_723, plain, (list(X1)|~isa(X1,f_listoftypefn(c_thing)))). % 9.43/9.62 cnf(i_0_1637, plain, (cartographicfeaturetype(f_groupfn(c_stream))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1627, plain, (cartographicfeaturetype(f_groupfn(c_pond))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1635, plain, (cartographicfeaturetype(f_groupfn(c_lagoon))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1633, plain, (cartographicfeaturetype(f_groupfn(c_ridgeline_topographical))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1634, plain, (cartographicfeaturetype(f_intermittentbodyofwaterfn(c_lake))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_732, plain, (list(X1)|~isa(X1,f_listoftypefn(c_realnumber)))). % 9.43/9.62 cnf(i_0_727, plain, (list(X1)|~isa(X1,f_listoftypefn(c_setorcollection)))). % 9.43/9.62 cnf(i_0_550, plain, (map(X1)|~isa(X1,f_mapfn_individual(c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_1663, plain, (partiallytangible(X1)|~isa(X1,f_groupfn(c_stream)))). % 9.43/9.62 cnf(i_0_1630, plain, (cartographicfeaturetype(f_formerfn(c_inlet))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1358, plain, (militaryorganization(f_armedforcesfn(c_turkey))|~mtvisible(c_worldpoliticalgeographydatavocabularymt))). % 9.43/9.62 cnf(i_0_296, plain, (geographicalregion(f_territoryfn(X1))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1571, plain, (quotedisa(c_purposefulaction,c_wordnetworkflowconstant_notfullyreviewed)|~mtvisible(c_bookkeepingmt))). % 9.43/9.62 cnf(i_0_1419, plain, (partiallytangible(X1)|~isa(X1,f_groupfn(c_weapon)))). % 9.43/9.62 cnf(i_0_1620, plain, (partiallytangible(X1)|~isa(X1,f_groupfn(c_drycreekbed)))). % 9.43/9.62 cnf(i_0_1665, plain, (partiallytangible(X1)|~isa(X1,f_intermittentbodyofwaterfn(c_stream)))). % 9.43/9.62 cnf(i_0_624, plain, (person(X1)|~isa(X1,f_citizenfn(c_canada)))). % 9.43/9.62 cnf(i_0_994, plain, (disjointwith(c_transportationdevice_vehicle,c_factorybuildingcomplex)|~mtvisible(c_animalphysiologyvocabularymt))). % 9.43/9.62 cnf(i_0_1501, plain, (arg2format(c_mainconstituent,c_singleentry)|~mtvisible(c_naivephysicsmt))). % 9.43/9.62 cnf(i_0_449, plain, (arg2format(c_fatherinlaw,c_settheformat)|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_457, plain, (arg2format(c_sisterinlaw,c_settheformat)|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_1242, plain, (inducedformulatemplate(X1)|~isa(X1,f_formulatemplateinductiontopictypefn(c_bodyofwater)))). % 9.43/9.62 cnf(i_0_365, plain, (temporalthing(X1)|~isa(X1,f_playingfn(c_thencmodifier)))). % 9.43/9.62 cnf(i_0_736, plain, (set_mathematical(X1)|~isa(X1,f_setoftypefn(c_individual)))). % 9.43/9.62 cnf(i_0_1188, plain, (medicaltreatmentevent(X1)|~isa(X1,f_treatmentfn(c_cancer)))). % 9.43/9.62 cnf(i_0_445, plain, (arg2format(c_sisters,c_settheformat)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_461, plain, (arg2format(c_tasteofobject,c_settheformat)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_450, plain, (arg1format(c_fatherinlaw,c_settheformat)|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_1586, plain, (arg1format(c_wasteproducts,c_singleentry)|~mtvisible(c_productgmt))). % 9.43/9.62 cnf(i_0_1440, plain, (authorizedagreement(X1)|~isa(X1,f_sharesinfundtypefn(c_unittrust)))). % 9.43/9.62 cnf(i_0_803, plain, (binarypredicate(X1)|~relationexistsall(X1,X2,X3))). % 9.43/9.62 cnf(i_0_531, plain, (binarypredicate(X1)|~relationallexists(X1,X2,X3))). % 9.43/9.62 cnf(i_0_278, plain, (binarypredicate(X1)|~relationallinstance(X1,X2,X3))). % 9.43/9.62 cnf(i_0_1547, plain, (genls(f_groupfn(c_publicofficial),c_partiallytangible)|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_52, plain, (genls(X1,f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible))|~tptptypes_9_824(X1,X2))). % 9.43/9.62 cnf(i_0_453, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_partiallytangible,c_byproducts,c_purposefulaction)))). % 9.43/9.62 cnf(i_0_293, plain, (geographicalsubregions(X1,X1)|~geographicalregion(X1))). % 9.43/9.62 cnf(i_0_129, plain, (collection(X1)|~argisa(X2,X3,X1))). % 9.43/9.62 cnf(i_0_127, plain, (collection(X1)|~arggenl(X2,X3,X1))). % 9.43/9.62 cnf(i_0_529, plain, (collection(X1)|~relationallexists(X2,X3,X1))). % 9.43/9.62 cnf(i_0_530, plain, (collection(X1)|~relationallexists(X2,X1,X3))). % 9.43/9.62 cnf(i_0_212, plain, (relationallexists(c_tptp_9_166,f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_15_8464)|~mtvisible(c_tptp_spindleheadmt))). % 9.43/9.62 cnf(i_0_5, plain, (tptptypes_4_770(X1,X2)|~tptptypes_5_802(X1,X2))). % 9.43/9.62 cnf(i_0_123, plain, (collection(X1)|~relationallinstance(X2,X1,X3))). % 9.43/9.62 cnf(i_0_1539, plain, (predicate(X1)|~argformat(X1,X2,X3))). % 9.43/9.62 cnf(i_0_281, plain, (nonnegativeinteger(X1)|~arggenl(X2,X1,X3))). % 9.43/9.62 cnf(i_0_804, plain, (nonnegativeinteger(X1)|~argquotedisa(X2,X1,X3))). % 9.43/9.62 cnf(i_0_830, plain, (relation(X1)|~argisa(X1,X2,X3))). % 9.43/9.62 cnf(i_0_282, plain, (relation(X1)|~arggenl(X1,X2,X3))). % 9.43/9.62 cnf(i_0_821, plain, (relation(X1)|~argquotedisa(X1,X2,X3))). % 9.43/9.62 cnf(i_0_549, plain, (characterstring(X1)|~synonymousexternalconcept(X2,X3,X1))). % 9.43/9.62 cnf(i_0_1596, plain, (personalassociationpredicate(X1)|~agentsrelationship(X2,X3,X1))). % 9.43/9.62 cnf(i_0_717, plain, (microtheory(X1)|~genlmt(X2,X1))). % 9.43/9.62 cnf(i_0_719, plain, (microtheory(X1)|~genlmt(X1,X2))). % 9.43/9.62 cnf(i_0_111, plain, (collection(X1)|~genls(X2,X1))). % 9.43/9.62 cnf(i_0_140, plain, (collection(X1)|~isa(X2,X1))). % 9.43/9.62 cnf(i_0_109, plain, (collection(X1)|~genls(X1,X2))). % 9.43/9.62 cnf(i_0_1578, plain, (predicate(X1)|~genlpreds(X2,X1))). % 9.43/9.62 cnf(i_0_1459, plain, (predicate(X1)|~negationpreds(X2,X1))). % 9.43/9.62 cnf(i_0_1577, plain, (predicate(X1)|~genlpreds(X1,X2))). % 9.43/9.62 cnf(i_0_1460, plain, (predicate(X1)|~negationpreds(X1,X2))). % 9.43/9.62 cnf(i_0_1502, plain, (intangibleindividual(X1)|~arg2format(X2,X1))). % 9.43/9.62 cnf(i_0_1347, plain, (collectiondenotingfunction(X1)|~resultgenl(X1,X2))). % 9.43/9.62 cnf(i_0_520, plain, (tptpcol_7_8198(X1)|~tptp_9_166(X2,X1))). % 9.43/9.62 cnf(i_0_283, plain, (genls(X1,c_thing)|~arg2isa(X2,X1))). % 9.43/9.62 cnf(i_0_29, plain, (genls(X1,c_tptpcol_4_8195)|~tptptypes_6_818(X2,X1))). % 9.43/9.62 cnf(i_0_483, plain, (genls(X1,c_tptpcol_3_3)|~tptptypes_9_779(X2,X1))). % 9.43/9.62 cnf(i_0_485, plain, (genls(X1,c_tptpcol_3_3)|~tptptypes_6_772(X2,X1))). % 9.43/9.62 cnf(i_0_484, plain, (genls(X1,c_tptpcol_3_3)|~tptptypes_3_514(X2,X1))). % 9.43/9.62 cnf(i_0_31, plain, (tptptypes_6_818(X1,X2)|~tptptypes_7_819(X1,X2))). % 9.43/9.62 cnf(i_0_30, plain, (tptptypes_6_818(X1,X2)|~tptptypes_7_826(X1,X2))). % 9.43/9.62 cnf(i_0_189, plain, (tptptypes_7_819(X1,X2)|~tptptypes_8_823(X1,X2))). % 9.43/9.62 cnf(i_0_979, plain, (group(X1)|~isa(X1,f_groupfn(f_groupfn(c_adultfemalehuman))))). % 9.43/9.62 cnf(i_0_1247, plain, (meaninginsystemfnsensus_information1997separable_entity(X1)|~isa(X1,f_meaninginsystemfn(c_sensus_information1997,s_separable_entity)))). % 9.43/9.62 cnf(i_0_958, plain, (hostilesocialaction(X1)|~isa(X1,f_attacktypebytargettypefn(c_bombing,c_militaryperson)))). % 9.43/9.62 cnf(i_0_983, plain, (hostilesocialaction(X1)|~isa(X1,f_attacktypebytargettypefn(c_murder,c_adultfemalehuman)))). % 9.43/9.62 cnf(i_0_1007, plain, (hostilesocialaction(X1)|~isa(X1,f_attacktypebytargettypefn(c_kidnappingsomeone,c_civilian)))). % 9.43/9.62 cnf(i_0_956, plain, (hostilesocialaction(X1)|~isa(X1,f_attacktypebytargettypefn(c_assassinatingsomeone,c_militaryperson)))). % 9.43/9.62 cnf(i_0_937, plain, (militaryperson(X1)|~isa(X1,f_collectionintersection2fn(c_militaryperson,c_unitedstatesperson)))). % 9.43/9.62 cnf(i_0_946, plain, (militaryperson(X1)|~isa(X1,f_collectionintersection2fn(c_srilankanperson,c_militaryperson)))). % 9.43/9.62 cnf(i_0_1438, plain, (individual(X1)|~isa(X1,f_monitoringoffinancialassettypefn(f_sharesinfundtypefn(c_unittrust))))). % 9.43/9.62 cnf(i_0_853, plain, (partiallytangible(X1)|~isa(X1,f_tastefn(f_meatfn(c_tuna))))). % 9.43/9.62 cnf(i_0_1306, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_airforcefn(c_pakistan))))). % 9.43/9.62 cnf(i_0_1290, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armyfn(c_albania))))). % 9.43/9.62 cnf(i_0_1282, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armyfn(c_iran))))). % 9.43/9.62 cnf(i_0_1289, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armyfn(c_spain))))). % 9.43/9.62 cnf(i_0_1292, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armyfn(c_turkey))))). % 9.43/9.62 cnf(i_0_1298, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armyfn(c_afghanistan))))). % 9.43/9.62 cnf(i_0_1295, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armedforcesfn(c_germany))))). % 9.43/9.62 cnf(i_0_1314, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armedforcesfn(c_italy))))). % 9.43/9.62 cnf(i_0_920, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armedforcesfn(c_iraq))))). % 9.43/9.62 cnf(i_0_1366, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_armedforcesfn(c_portugal))))). % 9.43/9.62 cnf(i_0_1287, plain, (agent_generic(X1)|~isa(X1,f_memberfn(f_navyfn(c_unitedstatesofamerica))))). % 9.43/9.62 cnf(i_0_330, plain, (individual(X1)|~isa(X1,f_subcollectionbyregionfn(c_thenchead,c_thencmodifier)))). % 9.43/9.62 cnf(i_0_721, plain, (genlmt(X1,X1)|~microtheory(X1))). % 9.43/9.62 cnf(i_0_137, plain, (genls(X1,X1)|~collection(X1))). % 9.43/9.62 cnf(i_0_1583, plain, (genlpreds(X1,X1)|~predicate(X1))). % 9.43/9.62 cnf(i_0_1546, plain, (partiallytangible(X1)|~isa(X1,f_groupfn(c_publicofficial))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_918, plain, (person(X1)|~isa(X1,f_residentfn(c_iraq))|~mtvisible(c_worldgeographymt))). % 9.43/9.62 cnf(i_0_1341, plain, (unitofmoney(X1)|~isa(X1,f_unitofmoneyofgeopoliticalentityfn(c_spain))|~mtvisible(c_worldpoliticalgeographydatavocabularymt))). % 9.43/9.62 cnf(i_0_838, plain, (inregion(X1,X2)|~geographicalsubregions(X2,X1))). % 9.43/9.62 cnf(i_0_46, plain, (tptptypes_8_823(X1,X2)|~tptptypes_9_824(X1,X2))). % 9.43/9.62 cnf(i_0_35, plain, (tptptypes_4_770(X1,X2)|~tptptypes_5_771(X1,X2))). % 9.43/9.62 cnf(i_0_812, plain, (nonnegativeinteger(X1)|~argformat(X2,X1,X3))). % 9.43/9.62 cnf(i_0_805, plain, (nonnegativeinteger(X1)|~natargument(X2,X1,X3))). % 9.43/9.62 cnf(i_0_548, plain, (genls(X1,c_thing)|~relationexistsall(X2,X3,X1))). % 9.43/9.62 cnf(i_0_377, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_individual,c_parts,c_individual)))). % 9.43/9.62 cnf(i_0_1245, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_geographicalsubregions,c_stream)))). % 9.43/9.62 cnf(i_0_470, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_stream)))). % 9.43/9.62 cnf(i_0_476, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_ditch)))). % 9.43/9.62 cnf(i_0_1210, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_person,c_owns,c_confectionery)))). % 9.43/9.62 cnf(i_0_1415, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_manufacturing,c_productscreated,c_weapon)))). % 9.43/9.62 cnf(i_0_1206, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_individual,c_parts,c_edwood_moviedirector)))). % 9.43/9.62 cnf(i_0_1390, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_individual,c_possessiverelation,c_edwood_moviedirector)))). % 9.43/9.62 cnf(i_0_1394, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_bus_roadvehicle,c_possessiverelation,c_israel)))). % 9.43/9.62 cnf(i_0_588, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_airplane,c_possessiverelation,c_israel)))). % 9.43/9.62 cnf(i_0_1040, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_personwithoccupation,c_performsinstancesaspartofjob,c_training)))). % 9.43/9.62 cnf(i_0_705, plain, (terrorist(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_indonesia_thenation)))). % 9.43/9.62 cnf(i_0_465, plain, (geographicalregion(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_geographicalregion,c_pathterminus,c_drycreekbed)))). % 9.43/9.62 cnf(i_0_388, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_partiallytangible,c_objectfoundinlocation,c_bodyofwater)))). % 9.43/9.62 cnf(i_0_700, plain, (terrorist(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_brazil)))). % 9.43/9.62 cnf(i_0_694, plain, (terrorist(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_unitedkingdomofgreatbritainandnorthernireland)))). % 9.43/9.62 cnf(i_0_697, plain, (terrorist(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_saudiarabia)))). % 9.43/9.62 cnf(i_0_707, plain, (terrorist(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_algeria)))). % 9.43/9.62 cnf(i_0_1446, plain, (socialbeing(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_socialbeing,c_seller,c_monetaryexchangeofuserrights)))). % 9.43/9.62 cnf(i_0_1158, plain, (monetaryvalue(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_monetaryvalue,c_discount,c_buying)))). % 9.43/9.62 cnf(i_0_1399, plain, (femalehuman(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_femalehuman,c_wife,c_malehuman)))). % 9.43/9.62 cnf(i_0_474, plain, (bodyofwater(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_stream)))). % 9.43/9.62 cnf(i_0_689, plain, (terrorist(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_terrorist,c_citizens,c_netherlands)))). % 9.43/9.62 cnf(i_0_1212, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_person,c_owns,c_confectionery)))). % 9.43/9.62 cnf(i_0_1396, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_bus_roadvehicle,c_possessiverelation,c_israel)))). % 9.43/9.62 cnf(i_0_600, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_airplane,c_possessiverelation,c_israel)))). % 9.43/9.62 cnf(i_0_676, plain, (realnumber(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_realnumber,c_annualdeathrate,c_geopoliticalentity)))). % 9.43/9.62 cnf(i_0_1467, plain, (subcollectionofwithrelationfromtypefnsocialbeingsellermonetaryexchangeofuserrights(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_socialbeing,c_seller,c_monetaryexchangeofuserrights)))). % 9.43/9.62 cnf(i_0_1588, plain, (subcollectionofwithrelationfromtypefnwaterwasteproductspurposefulaction(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_water,c_wasteproducts,c_purposefulaction)))). % 9.43/9.62 cnf(i_0_1035, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_personwithoccupation,c_performsinstancesaspartofjob,c_training)))). % 9.43/9.62 cnf(i_0_1386, plain, (agent_generic(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_india)))). % 9.43/9.62 cnf(i_0_560, plain, (agent_generic(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_654, plain, (disjointwith(c_murder,f_unsuccessfulattempttofn(c_murder))|~mtvisible(c_agentgmt))). % 9.43/9.62 cnf(i_0_632, plain, (disjointwith(c_kidnappingsomeone,f_unsuccessfulattempttofn(c_kidnappingsomeone))|~mtvisible(c_agentgmt))). % 9.43/9.62 cnf(i_0_673, plain, (isa(c_geopoliticalentity,f_conceptnodesfortasktypefn(c_intelligenceanalysistask_allotment))|~mtvisible(c_analystdatabasemt))). % 9.43/9.62 cnf(i_0_1264, plain, (genls(f_groupfn(c_lake),c_place)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_657, plain, (agent_generic(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_murder)))). % 9.43/9.62 cnf(i_0_1364, plain, (agent_generic(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_carbombing)))). % 9.43/9.62 cnf(i_0_703, plain, (person(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_person,c_citizens,c_algeria)))). % 9.43/9.62 cnf(i_0_393, plain, (subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))). % 9.43/9.62 cnf(i_0_1261, plain, (genls(f_groupfn(c_hill),c_place)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_919, plain, (genls(f_residentfn(c_iraq),c_person)|~mtvisible(c_worldgeographymt))). % 9.43/9.62 cnf(i_0_1266, plain, (genls(f_mobfn(c_stoneobject_natural),c_place)|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1516, plain, (genls(f_femalefn(c_horse),c_horse)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1425, plain, (intelligentagent(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_armedwithweapontype,c_weapon)))). % 9.43/9.62 cnf(i_0_1388, plain, (terroristgroup(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_india)))). % 9.43/9.62 cnf(i_0_1339, plain, (terroristgroup(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_operatesinregion,c_spain)))). % 9.43/9.62 cnf(i_0_1378, plain, (terroristgroup(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_india)))). % 9.43/9.62 cnf(i_0_455, plain, (argformat(c_byproducts,n_1,c_singleentry)|~mtvisible(c_productgmt))). % 9.43/9.62 cnf(i_0_1511, plain, (argformat(c_biologicaloffspring,n_1,c_settheformat)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_1384, plain, (terroristgroup(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_932, plain, (terroristgroup(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_unitedstatesperson)))). % 9.43/9.62 cnf(i_0_1024, plain, (terroristgroup(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_saudiperson)))). % 9.43/9.62 cnf(i_0_1360, plain, (terroristgroup(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_performsactsoftype,c_torture)))). % 9.43/9.62 cnf(i_0_1520, plain, (argformat(c_biologicaloffspring,n_2,c_settheformat)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_447, plain, (argformat(c_motherinlaw,n_2,c_settheformat)|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_463, plain, (argformat(c_tasteofobject,n_2,c_settheformat)|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_988, plain, (genls(f_groupfn(f_groupfn(c_adultfemalehuman)),c_partiallytangible)|~mtvisible(c_cychistoricalpossibilitytheorymt))). % 9.43/9.62 cnf(i_0_1027, plain, (organization(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_orgpresentinregion,c_japan)))). % 9.43/9.62 cnf(i_0_950, plain, (organization(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_membertypes,c_militaryperson)))). % 9.43/9.62 cnf(i_0_971, plain, (action(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_shootingaprojectileweapon,c_performedby,c_soldier)))). % 9.43/9.62 cnf(i_0_1126, plain, (subcollectionofwithrelationfromfnbaseballteamgroupmembersminorleaguebaseball(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_baseballteam,c_groupmembers,c_minorleaguebaseball)))). % 9.43/9.62 cnf(i_0_982, plain, (genls(f_groupfn(f_groupfn(c_adultfemalehuman)),c_partiallytangible)|~mtvisible(c_biologyvocabularymt))). % 9.43/9.62 cnf(i_0_1169, plain, (firstordercollection(f_subcollectionofwithrelationfromtypefn(c_eukaryoticcell,c_physicalparts,c_rnamolecule))|~mtvisible(c_productgvocabularymt))). % 9.43/9.62 cnf(i_0_1622, plain, (naturalfeaturetype(f_subcollectionofwithrelationfromtypefn(c_flowterrain,c_subpaths,c_drycreekbed))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_472, plain, (cartographicfeaturetype(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_stream))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_995, plain, (transportationevent(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_arrivingataplace,c_transporter,c_transportationdevice_vehicle)))). % 9.43/9.62 cnf(i_0_1248, plain, (isa(X1,f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~meaninginsystemfnsensus_information1997separable_entity(X1))). % 9.43/9.62 cnf(i_0_987, plain, (partiallytangible(X1)|~isa(X1,f_groupfn(f_groupfn(c_adultfemalehuman)))|~mtvisible(c_cychistoricalpossibilitytheorymt))). % 9.43/9.62 cnf(i_0_981, plain, (partiallytangible(X1)|~isa(X1,f_groupfn(f_groupfn(c_adultfemalehuman)))|~mtvisible(c_biologyvocabularymt))). % 9.43/9.62 cnf(i_0_467, plain, (cartographicfeaturetype(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_ditch))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1562, plain, (subcollectionofwithrelationfromfnpartiallytangiblebyproductssomefnphysicalcreationordestructionevent(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_partiallytangible,c_byproducts,f_somefn(c_physicalcreationordestructionevent))))). % 9.43/9.62 cnf(i_0_1468, plain, (isa(X1,f_subcollectionofwithrelationfromtypefn(c_socialbeing,c_seller,c_monetaryexchangeofuserrights))|~subcollectionofwithrelationfromtypefnsocialbeingsellermonetaryexchangeofuserrights(X1))). % 9.43/9.62 cnf(i_0_1589, plain, (isa(X1,f_subcollectionofwithrelationfromtypefn(c_water,c_wasteproducts,c_purposefulaction))|~subcollectionofwithrelationfromtypefnwaterwasteproductspurposefulaction(X1))). % 9.43/9.62 cnf(i_0_371, plain, (individual(X1)|~isa(X1,f_collectionintersection2fn(c_thenchead,f_groupfn(c_thencmodifier))))). % 9.43/9.62 cnf(i_0_1048, plain, (individual(X1)|~isa(X1,f_collectionintersection2fn(c_thenchead,f_groupfn(c_vaccinationevent))))). % 9.43/9.62 cnf(i_0_436, plain, (individual(X1)|~isa(X1,f_prospectivewrtroleintypefn(c_buyer,f_buyingfn(c_automobile))))). % 9.43/9.62 cnf(i_0_358, plain, (individual(X1)|~isa(X1,f_subcollectionbyregionfn(c_thenchead,f_somefn(c_thencmodifier))))). % 9.43/9.62 cnf(i_0_663, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_partiallytangible,c_derivedfrom,f_somefn(c_partiallytangible))))). % 9.43/9.62 cnf(i_0_1474, plain, (prospectivewrtroleintypefnbuyerbuyingfnautomobile(X1)|~isa(X1,f_prospectivewrtroleintypefn(c_buyer,f_buyingfn(c_automobile))))). % 9.43/9.62 cnf(i_0_336, plain, (collection(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_thenchead,c_genls,c_thencmodifier)))). % 9.43/9.62 cnf(i_0_373, plain, (collection(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_collection,c_genls,c_thencmodifier)))). % 9.43/9.62 cnf(i_0_150, plain, (geographicalregion(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_geographicalregion,c_objectfoundinlocation,f_groupfn(c_building))))). % 9.43/9.62 cnf(i_0_955, plain, (militaryperson(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_militaryperson,c_hasmembers,f_armedforcesfn(c_unitedstatesofamerica))))). % 9.43/9.62 cnf(i_0_547, plain, (genls(X1,c_thing)|~isa(X2,X1))). % 9.43/9.62 cnf(i_0_199, plain, (disjointwith(X1,X2)|~disjointwith(X2,X1))). % 9.43/9.62 cnf(i_0_842, plain, (borderson(X1,X2)|~borderson(X2,X1))). % 9.43/9.62 cnf(i_0_1455, plain, (negationpreds(X1,X2)|~negationpreds(X2,X1))). % 9.43/9.62 cnf(i_0_197, plain, (~isa(X1,X2)|~isa(X1,X3)|~disjointwith(X3,X2))). % 9.43/9.62 cnf(i_0_606, plain, (genls(f_threateningtodofn(c_terroristsuicidebombing),f_threateningtodofn(c_bombing))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_899, plain, (isa(X1,f_groupfn(c_person))|~isa(X1,f_groupfn(c_femalechild)))). % 9.43/9.62 cnf(i_0_1669, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_subpaths,f_intermittentbodyofwaterfn(c_stream))))). % 9.43/9.62 cnf(i_0_451, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationfromfn(c_partiallytangible,c_byproducts,f_somefn(c_physicalcreationordestructionevent))))). % 9.43/9.62 cnf(i_0_442, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_homosapiens,c_hasphysicalattractiveness,f_highamountfn(c_physicalattractiveness))))). % 9.43/9.62 cnf(i_0_1550, plain, (genls(f_threateningtodofn(c_physicallyattackinganagent),f_threateningtodofn(c_physicallyattackinganagent))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_438, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_person,c_hasphysicalattractiveness,f_highamountfn(c_physicalattractiveness))))). % 9.43/9.62 cnf(i_0_440, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_malehuman,c_hasphysicalattractiveness,f_highamountfn(c_physicalattractiveness))))). % 9.43/9.62 cnf(i_0_943, plain, (isa(f_armyfn(c_sudan),f_groupfn(c_militaryperson))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_1380, plain, (terroristgroup(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_terroristgroup,c_considersasenemy,f_governmentfn(c_somalia))))). % 9.43/9.62 cnf(i_0_1678, plain, (bodyofwater(X1)|~isa(X1,f_subcollectionofwithrelationtofn(c_bodyofwater,c_sizeparameterofobject,f_lowamountfn(c_area))))). % 9.43/9.62 cnf(i_0_921, plain, (isa(f_armyfn(c_iraq),f_groupfn(c_socialbeing))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_945, plain, (isa(f_navyfn(c_algeria),f_groupfn(c_militaryperson))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_1570, plain, (genls(f_groupfn(f_gamefn(c_basketball_thegame)),f_groupfn(c_purposefulaction))|~mtvisible(c_sportsmt))). % 9.43/9.62 cnf(i_0_629, plain, (genls(f_attacktypebytargettypefn(c_kidnappingsomeone,c_militaryperson),c_kidnappingsomeone)|~mtvisible(c_cychistoricalpossibilitytheorymt))). % 9.43/9.62 cnf(i_0_909, plain, (genls(f_artifacttypeforusertypefn(c_shirt,c_femalechild),c_shirt)|~mtvisible(c_productgmt))). % 9.43/9.62 cnf(i_0_904, plain, (genls(f_artifacttypeforusertypefn(c_shortpants,c_femalechild),c_shortpants)|~mtvisible(c_productgmt))). % 9.43/9.62 cnf(i_0_1127, plain, (isa(X1,f_subcollectionofwithrelationfromfn(c_baseballteam,c_groupmembers,c_minorleaguebaseball))|~subcollectionofwithrelationfromfnbaseballteamgroupmembersminorleaguebaseball(X1))). % 9.43/9.62 cnf(i_0_394, plain, (isa(X1,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))|~subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(X1))). % 9.43/9.62 cnf(i_0_1590, plain, (subcollectionofwithrelationtotypefnliquidflowalongconduitprimaryobjectmovingsubcollectionofwithrelationfromtypefnwaterwasteproductspurposefulaction(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_liquidflowalongconduit,c_primaryobjectmoving,f_subcollectionofwithrelationfromtypefn(c_water,c_wasteproducts,c_purposefulaction))))). % 9.43/9.62 cnf(i_0_1195, plain, (isa(X1,f_exposureoforganismtoharmfulsubstancefn(c_vx_nerveagent))|~isa(X1,f_exposureoforganismtoharmfulsubstancefn(f_liquidfn(c_vx_nerveagent))))). % 9.43/9.62 cnf(i_0_1200, plain, (isa(X1,f_exposureoforganismtoharmfulsubstancefn(c_cyanide))|~isa(X1,f_exposureoforganismtoharmfulsubstancefn(f_liquidfn(c_cyanide))))). % 9.43/9.62 cnf(i_0_1402, plain, (isa(X1,f_groupfn(c_femaleanimal))|~isa(X1,f_groupfn(c_femalehuman)))). % 9.43/9.62 cnf(i_0_1480, plain, (isa(X1,f_groupfn(c_transportationdevice))|~isa(X1,f_groupfn(c_automobile)))). % 9.43/9.62 cnf(i_0_1197, plain, (isa(X1,f_exposureoforganismtoharmfulsubstancefn(c_cholinesteraseinhibitingsubstance))|~isa(X1,f_exposureoforganismtoharmfulsubstancefn(c_vx_nerveagent)))). % 9.43/9.62 cnf(i_0_605, plain, (isa(X1,f_threateningtodofn(c_bombing))|~isa(X1,f_threateningtodofn(c_terroristsuicidebombing))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_1060, plain, (partiallytangible(X1)|~isa(X1,f_subcollectionbyregionfn(f_subcollectionofwithrelationfromtypefn(c_militarypost,c_controls,c_militaryorganization),c_israel)))). % 9.43/9.62 cnf(i_0_597, plain, (partiallytangible(X1)|~isa(X1,f_groupfn(f_subcollectionofwithrelationfromfn(c_airplane,c_possesses,f_governmentfn(c_israel)))))). % 9.43/9.62 cnf(i_0_500, plain, (relationexistsall(c_tptp_9_495,c_tptpcol_11_12871,f_endingfn(c_era))|~mtvisible(c_tptp_member85_mt))). % 9.43/9.62 cnf(i_0_1257, plain, (place(f_thelogicalfieldvaluefn(c_edb_entityattribute_ls,c_place,n_1))|~mtvisible(c_sksimt))). % 9.43/9.62 cnf(i_0_1638, plain, (cartographicfeaturetype(f_subcollectionofwithrelationtotypefn(c_lake,c_in_contopen,c_crater))|~mtvisible(c_geographicalregiongmt))). % 9.43/9.62 cnf(i_0_1563, plain, (isa(X1,f_subcollectionofwithrelationfromfn(c_partiallytangible,c_byproducts,f_somefn(c_physicalcreationordestructionevent)))|~subcollectionofwithrelationfromfnpartiallytangiblebyproductssomefnphysicalcreationordestructionevent(X1))). % 9.43/9.62 cnf(i_0_1569, plain, (isa(X1,f_groupfn(c_purposefulaction))|~isa(X1,f_groupfn(f_gamefn(c_basketball_thegame)))|~mtvisible(c_sportsmt))). % 9.43/9.62 cnf(i_0_1545, plain, (firstordercollection(f_subcollectionofwithrelationfromtypefn(c_transportationevent,c_subevents,f_smugglingfn(c_nuclearrelatedmaterial)))|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_1005, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationtotypefn(c_militaryattack,c_intendedattacktargets,f_subcollectionofwithrelationfromtypefn(c_somethingexisting,c_possesses,c_civilian))))). % 9.43/9.62 cnf(i_0_1671, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationfromtypefn(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_geographicalsubregions,c_stream),c_eventoccursat,c_whirlingoffluid)))). % 9.43/9.62 cnf(i_0_44, plain, (quotedisa(X1,X2)|~genls(X3,X2)|~quotedisa(X1,X3))). % 9.43/9.62 cnf(i_0_173, plain, (genlmt(X1,X2)|~genlmt(X3,X2)|~genlmt(X1,X3))). % 9.43/9.62 cnf(i_0_1226, plain, (genls(f_attacktypebytargettypefn(c_killingperson,f_citizenfn(c_israel)),c_hostilesocialaction)|~mtvisible(c_unitedstatessociallifemt))). % 9.43/9.62 cnf(i_0_41, plain, (genls(X1,X2)|~genls(X1,X3)|~genls(X3,X2))). % 9.43/9.62 cnf(i_0_39, plain, (disjointwith(X1,X2)|~disjointwith(X3,X2)|~genls(X1,X3))). % 9.43/9.62 cnf(i_0_1475, plain, (isa(X1,f_prospectivewrtroleintypefn(c_buyer,f_buyingfn(c_automobile)))|~prospectivewrtroleintypefnbuyerbuyingfnautomobile(X1))). % 9.43/9.62 cnf(i_0_38, plain, (disjointwith(X1,X2)|~disjointwith(X1,X3)|~genls(X2,X3))). % 9.43/9.62 cnf(i_0_285, plain, (arg2isa(X1,X2)|~arg2isa(X1,X3)|~genls(X3,X2))). % 9.43/9.62 cnf(i_0_43, plain, (isa(X1,X2)|~isa(X1,X3)|~genls(X3,X2))). % 9.43/9.62 cnf(i_0_915, plain, (isa(f_industryofregionfn(f_productionindustrytypefn(c_weaponofmassdestruction),c_iraq),f_groupfn(c_business))|~mtvisible(c_medicalorganizationdatamt))). % 9.43/9.62 cnf(i_0_279, plain, (arg1isa(X1,X2)|~arg1isa(X1,X3)|~genls(X3,X2))). % 9.43/9.62 cnf(i_0_1582, plain, (genlpreds(X1,X2)|~genlpreds(X3,X2)|~genlpreds(X1,X3))). % 9.43/9.62 cnf(i_0_1463, plain, (negationpreds(X1,X2)|~negationpreds(X3,X2)|~genlpreds(X1,X3))). % 9.43/9.62 cnf(i_0_1464, plain, (negationpreds(X1,X2)|~negationpreds(X1,X3)|~genlpreds(X2,X3))). % 9.43/9.62 cnf(i_0_840, plain, (geographicalsubregions(X1,X2)|~geographicalsubregions(X3,X2)|~geographicalsubregions(X1,X3))). % 9.43/9.62 cnf(i_0_1348, plain, (resultgenl(X1,X2)|~resultgenl(X1,X3)|~genls(X3,X2))). % 9.43/9.62 cnf(i_0_493, plain, (arg2genl(X1,X2)|~arg2genl(X1,X3)|~genls(X3,X2))). % 9.43/9.62 cnf(i_0_565, plain, (isa(X1,f_citizenfn(c_israel))|~isa(X1,f_collectionintersection2fn(f_citizenfn(c_unitedstatesofamerica),f_citizenfn(c_israel))))). % 9.43/9.62 cnf(i_0_553, plain, (isa(X1,f_citizenfn(c_unitedstatesofamerica))|~isa(X1,f_collectionintersection2fn(f_citizenfn(c_unitedstatesofamerica),f_citizenfn(c_israel))))). % 9.43/9.62 cnf(i_0_1221, plain, (spatialthing_nonsituational(X1)|~isa(X1,f_subcollectionofwithrelationtofn(f_subcollectionofwithrelationfromfn(c_facility_generic,c_operatesfacilities,c_unitedstatesfederalgovernment),c_objectfoundinlocation,f_territoryfn(c_panama))))). % 9.43/9.62 cnf(i_0_902, plain, (isa(X1,f_artifacttypeforusertypefn(c_clothingitem,c_femalechild))|~isa(X1,f_artifacttypeforusertypefn(c_shirt,c_femalechild))|~mtvisible(c_productgvocabularymt))). % 9.43/9.62 cnf(i_0_911, plain, (isa(X1,f_artifacttypeforusertypefn(c_clothingitem,c_femalechild))|~isa(X1,f_artifacttypeforusertypefn(c_sock,c_femalechild))|~mtvisible(c_productgvocabularymt))). % 9.43/9.62 cnf(i_0_1642, plain, (tptpofobject(X1,f_tptpquantityfn_14(n_316))|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_ditch))|~mtvisible(c_currentworlddatacollectormt_nonhomocentric))). % 9.43/9.62 cnf(i_0_1591, plain, (isa(X1,f_subcollectionofwithrelationtotypefn(c_liquidflowalongconduit,c_primaryobjectmoving,f_subcollectionofwithrelationfromtypefn(c_water,c_wasteproducts,c_purposefulaction)))|~subcollectionofwithrelationtotypefnliquidflowalongconduitprimaryobjectmovingsubcollectionofwithrelationfromtypefnwaterwasteproductspurposefulaction(X1))). % 9.43/9.62 cnf(i_0_1432, plain, (situation(X1)|~isa(X1,f_nthsubsituationtypeoftypefn(f_subcollectionofwithrelationtotypefn(c_investing,c_objectpaidfor,f_sharesinfundtypefn(c_hedgefund)),f_buyingfn(c_putoption),n_1)))). % 9.43/9.62 cnf(i_0_903, plain, (genls(f_artifacttypeforusertypefn(c_shirt,c_femalechild),f_artifacttypeforusertypefn(c_clothingitem,c_femalechild))|~mtvisible(c_productgvocabularymt))). % 9.43/9.62 cnf(i_0_1267, plain, (isa(X1,f_meaninginsystemfn(c_sensus_information1997,s_decomposable_object))|~isa(X1,f_collectionintersection2fn(c_place,c_geographicalthing))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_912, plain, (genls(f_artifacttypeforusertypefn(c_sock,c_femalechild),f_artifacttypeforusertypefn(c_clothingitem,c_femalechild))|~mtvisible(c_productgvocabularymt))). % 9.43/9.62 cnf(i_0_1268, plain, (genls(f_collectionintersection2fn(c_place,c_geographicalthing),f_meaninginsystemfn(c_sensus_information1997,s_decomposable_object))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_978, plain, (genls(f_collectionintersection2fn(c_soldier,f_memberfn(c_unitedstatesarmy)),f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_977, plain, (isa(X1,f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~isa(X1,f_collectionintersection2fn(c_soldier,f_memberfn(c_unitedstatesarmy)))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_1178, plain, (genls(f_subcollectionofwithrelationtotypefn(c_massmanufacturing,c_outputscreated,f_mobfn(c_token_physical)),c_creationevent)|~mtvisible(c_cychistoricalpossibilitytheorymt))). % 9.43/9.62 cnf(i_0_424, plain, (isa(X1,f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_femalehuman,c_wife,c_intelligentagent))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_1135, plain, (isa(X1,f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_rnamolecule,c_outputscreated,c_transcription_dnatorna))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_1218, plain, (isa(X1,f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_roadvehicle,c_owns,c_regionalgovernment))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_390, plain, (isa(X1,f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~isa(X1,f_subcollectionofwithrelationtotypefn(c_partiallytangible,c_objectfoundinlocation,c_bodyofwater))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_1000, plain, (individual(X1)|~isa(X1,f_subcollectionofwithrelationtofn(f_subcollectionofwithrelationtotypefn(c_militaryattack,c_intendedattacktargets,f_subcollectionofwithrelationfromtypefn(c_somethingexisting,c_possesses,c_civilian)),c_eventoccursat,f_southernregionfn(c_lebanon))))). % 9.43/9.62 cnf(i_0_425, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_femalehuman,c_wife,c_intelligentagent),f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_1136, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_rnamolecule,c_outputscreated,c_transcription_dnatorna),f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_1219, plain, (genls(f_subcollectionofwithrelationfromtypefn(c_roadvehicle,c_owns,c_regionalgovernment),f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_1521, plain, (isa(f_the(f_organismparttypefn(c_homosapiens,c_nose)),f_organismparttypefn(c_homosapiens,c_nose))|~mtvisible(c_biologymt))). % 9.43/9.62 cnf(i_0_391, plain, (genls(f_subcollectionofwithrelationtotypefn(c_partiallytangible,c_objectfoundinlocation,c_bodyofwater),f_meaninginsystemfn(c_sensus_information1997,s_separable_entity))|~mtvisible(c_sensusmappingmt))). % 9.43/9.62 cnf(i_0_1643, plain, (relationallinstance(c_tptpofobject,f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_pathterminus,c_ditch),f_tptpquantityfn_14(n_316))|~mtvisible(c_currentworlddatacollectormt_nonhomocentric))). % 9.43/9.62 cnf(i_0_1436, plain, (isa(X1,f_buyingfn(c_putoption))|~isa(X1,f_nthsubsituationtypeoftypefn(f_subcollectionofwithrelationtotypefn(c_investing,c_objectpaidfor,f_sharesinfundtypefn(c_hedgefund)),f_buyingfn(c_putoption),n_1)))). % 9.43/9.62 cnf(i_0_1674, plain, (isa(X1,f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_eventoccursat,c_whirlingoffluid))|~isa(X1,f_subcollectionofwithrelationfromtypefn(f_subcollectionofwithrelationfromtypefn(c_bodyofwater,c_geographicalsubregions,c_stream),c_eventoccursat,c_whirlingoffluid)))). % 9.43/9.62 cnf(i_0_1116, plain, (isa(X1,f_subcollectionofwithrelationtotypefn(c_division_militaryechelon,c_groupmembers,c_armypersonnel))|~isa(X1,f_subcollectionofwithrelationtofn(f_subcollectionofwithrelationtotypefn(c_division_militaryechelon,c_groupmembers,c_armypersonnel),c_affiliatedwith,c_unitedstatesofamerica)))). % 9.43/9.62 cnf(i_0_211, plain, (tptp_9_166(X1,f_relationallexistsfn(X1,c_tptp_9_166,f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible),c_tptpcol_15_8464))|~isa(X1,f_subcollectionofwithrelationfromtypefn(c_orientationvector,c_orientation,c_partiallytangible))|~mtvisible(c_tptp_spindleheadmt))). % 9.43/9.62 cnf(i_0_1228, plain, (genls(f_attacktypebytargettypefn(c_ambushinganenemy,f_subcollectionofwithrelationfromfn(c_militaryorganization,c_possessiverelation,c_israel)),c_hostilesocialaction)|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_607, plain, (~isa(X1,f_unsuccessfulattempttofn(f_subcollectionofwithrelationtotypefn(c_bombing,c_intendedattacktargets,f_subcollectionofwithrelationtofn(c_enduringthing_localized,c_inregion,c_unitedkingdomofgreatbritainandnorthernireland))))|~isa(X1,f_subcollectionofwithrelationtotypefn(c_bombing,c_intendedattacktargets,f_subcollectionofwithrelationtofn(c_enduringthing_localized,c_inregion,c_unitedkingdomofgreatbritainandnorthernireland)))|~mtvisible(c_agentgmt))). % 9.43/9.62 cnf(i_0_951, plain, (genls(f_attacktypebytargettypefn(c_shootingattack_gun,f_subcollectionofwithrelationfromfn(c_militaryperson,c_hasmembers,f_armedforcesfn(c_unitedstatesofamerica))),c_shootingattack_gun)|~mtvisible(c_humansociallifemt))). % 9.43/9.62 cnf(i_0_499, plain, (tptp_9_495(f_relationexistsallfn(X1,c_tptp_9_495,c_tptpcol_11_12871,f_endingfn(c_era)),X1)|~isa(X1,f_endingfn(c_era))|~mtvisible(c_tptp_member85_mt))). % 9.43/9.62 cnf(i_0_573, plain, (isa(f_relationexistsallfn(X1,X2,X3,X4),X3)|~relationexistsall(X2,X3,X4)|~isa(X1,X4))). % 9.43/9.62 cnf(i_0_522, plain, (isa(f_relationallexistsfn(X1,X2,X3,X4),X4)|~relationallexists(X2,X3,X4)|~isa(X1,X3))). % 9.43/9.62 cnf(i_0_1062, plain, (isa(X1,f_subcollectionofwithrelationtofn(c_animal,c_residesinregion,f_somefn(c_geographicalthing)))|~isa(X1,f_subcollectionbyregionfn(f_subcollectionofwithrelationtofn(c_animal,c_residesinregion,f_somefn(c_geographicalthing)),f_somefn(c_island)))|~mtvisible(c_cychistoricalpossibilitytheorymt))). % 9.43/9.62 cnf(i_0_432, plain, (isa(X1,f_subcollectionofwithrelationtotypefn(c_monetaryexchangeofuserrights,c_buyer,f_sharesinfundtypefn(c_hedgefund)))|~isa(X1,f_subcollectionofwithrelationtotypefn(f_subcollectionofwithrelationtotypefn(c_monetaryexchangeofuserrights,c_buyer,f_sharesinfundtypefn(c_hedgefund)),c_performedby,f_subcollectionofwithrelationtotypefn(c_person,c_financialstate,c_wealthy))))). % 9.43/9.62 cnf(i_0_603, plain, (genls(f_attacktypebytargettypefn(c_bombing,f_subcollectionofwithrelationtofn(c_facility_construct,c_primaryactivitytypeoflocation,f_subcollectionofwithrelationtotypefn(c_maintainingsomething,c_objecttakencareof,c_regionalgovernment))),c_bombing)|~mtvisible(c_cychistoricalpossibilitytheorymt))). % 9.43/9.62 cnf(i_0_1063, plain, (genls(f_subcollectionbyregionfn(f_subcollectionofwithrelationtofn(c_animal,c_residesinregion,f_somefn(c_geographicalthing)),f_somefn(c_island)),f_subcollectionofwithrelationtofn(c_animal,c_residesinregion,f_somefn(c_geographicalthing)))|~mtvisible(c_cychistoricalpossibilitytheorymt))). % 9.43/9.62 cnf(i_0_608, plain, (disjointwith(f_subcollectionofwithrelationtotypefn(c_bombing,c_intendedattacktargets,f_subcollectionofwithrelationtofn(c_enduringthing_localized,c_inregion,c_unitedkingdomofgreatbritainandnorthernireland)),f_unsuccessfulattempttofn(f_subcollectionofwithrelationtotypefn(c_bombing,c_intendedattacktargets,f_subcollectionofwithrelationtofn(c_enduringthing_localized,c_inregion,c_unitedkingdomofgreatbritainandnorthernireland))))|~mtvisible(c_agentgmt))). % 9.43/9.62 # End listing active clauses. There is an equivalent clause to each of these in the clausification! % 9.43/9.62 # Begin printing tableau % 9.43/9.62 # Found 7 steps % 9.43/9.62 cnf(i_0_2, negated_conjecture, (mtvisible(c_tptp_spindlecollectormt)), inference(start_rule)). % 9.43/9.62 cnf(i_0_1698, plain, (mtvisible(c_tptp_spindlecollectormt)), inference(extension_rule, [i_0_172])). % 9.43/9.62 cnf(i_0_3182, plain, (~genlmt(c_tptp_spindlecollectormt,c_basekb)), inference(closure_rule, [i_0_26])). % 9.43/9.62 cnf(i_0_3181, plain, (mtvisible(c_basekb)), inference(extension_rule, [i_0_172])). % 9.43/9.62 cnf(i_0_4362, plain, (mtvisible(c_generallexiconmt)), inference(extension_rule, [i_0_21])). % 9.43/9.62 cnf(i_0_4363, plain, (~genlmt(c_basekb,c_generallexiconmt)), inference(etableau_closure_rule, [i_0_4363, ...])). % 9.43/9.62 cnf(i_0_5242, plain, (relationalnounslot(c_orientation)), inference(etableau_closure_rule, [i_0_5242, ...])). % 9.43/9.62 # End printing tableau % 9.43/9.62 # SZS output end % 9.43/9.62 # Branches closed with saturation will be marked with an "s" % 9.43/9.62 # Returning from population with 3 new_tableaux and 0 remaining starting tableaux. % 9.43/9.62 # We now have 3 tableaux to operate on % 9.43/9.62 # Found closed tableau during pool population. % 9.43/9.62 # Proof search is over... % 9.43/9.62 # Freeing feature tree %------------------------------------------------------------------------------