%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR065+2 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n004.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 : 300s
% DateTime : Thu May 7 07:20:04 PM UTC 2026
% Result : Theorem 33.86s 7.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.10 % Problem : CSR065+2 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.12/0.30 % Computer : n004.cluster.edu
% 0.12/0.30 % Model : x86_64 x86_64
% 0.12/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.30 % Memory : 8042.1875MB
% 0.12/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.30 % CPULimit : 300
% 0.12/0.30 % WCLimit : 300
% 0.12/0.30 % DateTime : Thu May 7 11:40:41 EDT 2026
% 0.12/0.31 % CPUTime :
% 0.12/0.31 SPASS-SCL-FOL version:
% 0.18/0.40 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 33.86/7.26 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.86/7.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.86/7.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.86/7.26 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.86/7.26 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.86/7.26 Execution resolution_1 ended with status: unsatisfiable
% 33.86/7.26 Used heuristic: resolution_1
% 33.86/7.26
% 33.86/7.26 Input Clauses:
% 33.86/7.26
% 33.86/7.26 Predicates: genlmt disjointwith intangible partiallytangible genls tptpcol_15_40430 tptpcol_14_40429 tptpcol_10_72710 tptpcol_9_72709 inanimateobject microtheory genlinverse genlpreds subsetof most tptpcol_7_93186 tptpcol_6_92162 tptpcol_13_40421 tptpcol_12_40420 mtvisible geographicalsubregions transitivebinarypredicate tptpcol_9_22021 tptpcol_8_22020 tptpcol_5_16388 tptpcol_4_16387 ridgeline_topographical tptpcol_14_72792 tptpcol_13_72791 tptpcol_5_20483 tptpcol_11_22023 tptpcol_10_22022 partiallyintangibleindividual individual trajector_underspecified location_underspecified enduringthing_localized artsupplies tptpcol_3_81921 tptpcol_2_65537 tptpcol_10_18567 tptpcol_9_18439 orderingpredicate tptpcol_11_92230 tptpcol_10_92166 tptpcol_2_98304 tptpcol_1_65536 marriagelicensedocument tptpcol_11_40388 tptptypes_9_693 tptptypes_8_692 tptptypes_8_390 tptptypes_7_389 isa relationexistsall resultisaarg tptpcol_4_106497 tptpcol_3_98305 tptpcol_5_114690 tptpcol_4_114689 tptpcol_12_93765 tptpcol_11_93764 tptpcol_8_72708 tptpcol_7_72707 tptpcol_10_40324 tptpcol_9_40196 tptpcol_13_93766 furpelt tptpofobject relationallinstance inregion applicationcontext computerdataartifact thing tptpcol_12_92262 navypersonnel executionbyfiringsquad tptpcol_10_109061 tptpcol_9_109060 shavingrazor_manual tptptypes_6_388 tptptypes_5_387 tptpcol_6_116738 tptpcol_15_92268 tptpcol_14_92264 borderson tptptypes_9_401 tptptypes_8_400 tptpcol_12_18663 tptpcol_11_18631 setorcollection mathematicalthing tptpcol_13_109173 tptpcol_12_109157 tptpcol_5_106498 tptpcol_5_24579 tptpcol_4_24578 geolevel_3 tptpcol_0_0 prettystring tptpcol_11_118084 tptpcol_10_118020 mathematicalorcomputationalthing subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription tptptypes_7_819 tptptypes_6_818 tptpcol_12_26919 tptpcol_11_26887 tptptypes_7_691 tptpcol_2_2 tptpcol_1_1 tptpcol_9_92165 tptpcol_8_92164 fixedordercollection collection aspatialinformationstore tptp_8_875 relationallexists tptpcol_9_118019 runningshorts tptp_9_720 tptpcol_12_22055 tptptypes_7_396 tptptypes_9_824 tptpcol_15_93775 tptpcol_14_93774 tptpcol_8_109059 tptpcol_7_108547 tptpcol_14_22072 tptpcol_13_22071 inanimateobject_nonnatural supplies firstordercollection tptpcol_13_18664 artifact tptpcol_7_113665 tptpcol_6_112641 geographicalregion no tptpcol_3_16386 tptpcol_5_69635 tptpcol_4_65539 subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma arg1isa tptpcol_3_114688 tptpcol_8_26629 tptpcol_7_26628 tptp_8_968 physicalorderingpredicate tptpcol_14_109181 tptpcol_16_30972 tptpcol_15_30970 tptpcol_8_18438 tptpcol_12_118116 tptpcol_6_26627 tptpcol_15_109185 tptpcol_16_92269 tptptypes_8_823 tptpcol_10_26886 tptpcol_9_26885 tptpcol_15_72793 militaryperson spatialthing_nonsituational geolevel_1 arg2isa state_geopolitical hpkb_subnationalagent tptpcol_7_21508 reflexivebinarypredicate tptp_9_51 tptpcol_3_65538 tptpcol_14_26921 tptpcol_13_26920 subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent intangibleindividual tptpcol_16_130924 tptpcol_15_130923 tptpcol_7_92163 tptpcol_16_130933 tptpcol_15_130931 few tptpcol_6_20484 tptpcol_6_108546 tptpcol_11_109125 tptpcol_8_93698 tptpcol_6_18436 tptpcol_7_18437 tptpcol_8_117763 tptpcol_7_117762 aspatialthing tptpcol_9_93699 tptpcol_10_93700 tptpcol_4_90113 tptp_8_271 tptpcol_5_110593 tptpcol_12_72775 tptpcol_11_72774 tptpcol_6_71683 tptpcol_16_50958 tptpcol_15_50957 tptpcol_8_114177 tptpcol_16_72795 tptptypes_5_802 tptpcol_5_90114 tptpcol_13_118117 tptpcol_16_26926 tptpcol_15_26925 tptpcol_8_39940 tptpcol_7_39939 tptpcol_15_22076 geolevel_4 tptpcol_13_92263 tptpcol_14_118118 natfunction natargument tptpquantity tptpcol_16_26939 tptpcol_16_62187 tptpcol_15_4027 pushingwithfingers affiliatedwith agent_generic footballteam tptpcol_16_4451 pushingwithopenhand tptpcol_16_25972 razor city tptpcol_16_27189 relation tptpcol_16_7738 tptpcol_7_7172 binarypredicate objectfoundinlocation spatialthing_localized geopoliticalsubdivision geographicallysubsumes subregions ship airporthasiatacode stringoflengthfn3 airport_physical tptpcol_16_8886 orientation orientationvector subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible tptpcol_16_29490 tptpcol_5_28674 tptpcol_16_31868 movement_translationevent directionoftranslation_throughout unitvectorinterval subevents tptpcol_16_10258 pushingababycarriage correctivelensprescription products creationordestructionevent issuingaprescription terroristgroup hasmembers organization terrorist subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup controlcharacterfreestring positiveinteger function_denotational predicate uniformresourcelocator
% 33.86/7.26 Fol Constants: c_tptpgeo_member8_mt c_tptpgeo_spindleheadmt c_intangible c_partiallytangible c_tptpcol_15_40430 c_tptpcol_14_40429 c_tptpcol_10_72710 c_tptpcol_9_72709 c_inanimateobject s_http_wwwinformationblastcomtechnical_university_of_munichhtml c_translation_3 c_subsetof c_most c_tptpcol_7_93186 c_tptpcol_6_92162 c_tptpcol_13_40421 c_tptpcol_12_40420 c_tptpgeo_member2_mt c_georegion_l1_x2_y0 c_georegion_l2_x8_y2 c_genls c_tptp_spindlecollectormt c_tptp_member2610_mt c_tptpcol_9_22021 c_tptpcol_8_22020 c_tptpcol_5_16388 c_tptpcol_4_16387 c_cyclistsmt c_tptpridgeline_topographical c_tptpcol_14_72792 c_tptpcol_13_72791 c_tptpcol_5_20483 c_tptpcol_11_22023 c_tptpcol_10_22022 c_partiallyintangibleindividual c_individual c_tptp_member3205_mt c_tptp_spindleheadmt c_peopledatamt c_unitedstatessociallifemt c_trajector_underspecified c_location_underspecified c_enduringthing_localized c_tptpartsupplies c_tptpcol_3_81921 c_tptpcol_2_65537 c_tptpcol_10_18567 c_tptpcol_9_18439 c_orderingpredicate c_transitivebinarypredicate c_tptpcol_11_92230 c_tptpcol_10_92166 c_tptpcol_2_98304 c_tptpcol_1_65536 c_tptp_member3356_mt c_tptpmarriagelicensedocument c_miptdatabase19681997_termsmt c_ldscgeneralcollectormt c_ethnicgroupsmt c_ethnicgroupsvocabularymt c_tptpcol_11_40388 c_tptptypes_9_693 c_tptptypes_8_692 c_machinelearningspindleheadmt c_ldscdemonstrationspindleheadmt c_currentworlddatacollectormt_nonhomocentric c_tptptypes_8_390 c_tptptypes_7_389 s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml c_translation_33 c_tptpgeo_member7_mt c_relationexistsallfn n_3 c_nooescapearchitecturemt c_organizationdatamt s_http_wwwfuntriviacomplayquizcfmqid60926origin c_translation_0_885 c_tptpcol_4_106497 c_tptpcol_3_98305 c_tptpcol_5_114690 c_tptpcol_4_114689 c_tptpcol_12_93765 c_tptpcol_11_93764 c_tptpcol_8_72708 c_tptpcol_7_72707 c_tptpcol_10_40324 c_tptpcol_9_40196 c_tptpcol_13_93766 n_328 c_tptpofobject c_furpelt c_geolocation_x53_y74 c_georegion_l4_x53_y74 c_wamt_evalinitial_p14 s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf c_thing c_patterndetectormt c_basekb c_tptpcol_12_92262 c_tptp_member1672_mt c_tptpnavypersonnel_3 c_universalvocabularymt c_corecyclmt c_tptp_member2831_mt c_tptpexecutionbyfiringsquad_90 c_tptpcol_10_109061 c_tptpcol_9_109060 c_theprototypicalshavingrazor_manual c_tptptypes_6_388 c_tptptypes_5_387 c_tptpcol_6_116738 c_tptpcol_15_92268 c_tptpcol_14_92264 c_tptpgeo_member5_mt c_georegion_l4_x56_y47 c_georegion_l4_x57_y47 c_tptp_member235_mt n_468 c_ridgeline_topographical c_tptptypes_9_401 c_tptptypes_8_400 c_tptpcol_12_18663 c_tptpcol_11_18631 c_setorcollection c_mathematicalthing c_tptpcol_13_109173 c_tptpcol_12_109157 c_calendarsmt c_tptpcol_5_106498 c_tptpcol_5_24579 c_tptpcol_4_24578 c_genlpreds c_worldgeographymt c_georegion_l3_x4_y13 c_georegion_l4_x27_y64 c_georegion_l4_x27_y65 c_tptpcol_0_0 c_hpkbvocabmt c_englishmt c_terrorist c_hasmembers c_terroristgroup s_terroristthathasbeenamemberofaterroristorganization c_geographicalsubregions c_inregion c_tptpcol_11_118084 c_tptpcol_10_118020 c_mathematicalorcomputationalthing c_tptp_member3393_mt c_tptpnsubcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription_2804 c_issuingaprescription c_products c_correctivelensprescription c_generictemporalmt c_worldgeographydualistmt c_tptptypes_7_819 c_tptptypes_6_818 c_tptpgeo_spindlecollectormt c_tptpgeo_member1_mt c_tptpcol_12_26919 c_tptpcol_11_26887 c_tptptypes_7_691 c_tptpcol_2_2 c_tptpcol_1_1 c_tptp_member3515_mt c_tptpcol_9_92165 c_tptpcol_8_92164 c_fixedordercollection c_collection c_geographymt c_microtheory c_aspatialinformationstore c_tptp_member237_mt c_pushingababycarriage c_tptpcol_16_10258 c_unitvectorinterval c_directionoftranslation_throughout c_movement_translationevent c_tptp_8_875 c_tptpcol_16_31868 c_tptpcol_9_118019 c_calendarsvocabularymt c_tptprunningshorts c_tptp_9_720 c_executionbyfiringsquad c_tptpcol_16_29490 c_tptpcol_12_22055 c_applicationcontext c_tptp_member2089_mt c_tptptypes_7_396 c_cycnounlearnermt c_tptp_member2668_mt c_orientationvector c_orientation c_tptpcol_16_8886 s_http_wwwthedailybulletincompostcardsmar9chtm c_translation_14 c_tptpcol_15_93775 c_tptpcol_14_93774 c_tptpcol_8_109059 c_tptpcol_7_108547 c_georegion_l3_x15_y24 c_georegion_l4_x45_y72 c_tptpcol_14_22072 c_tptpcol_13_22071 c_inanimateobject_nonnatural c_xskijump_thegame n_232 c_supplies c_firstordercollection c_georegion_l4_x45_y9 c_georegion_l4_x45_y10 c_tptpcol_13_18664 c_artifact c_tptpgeo_member3_mt c_genlmt c_timehasnoendmt c_tptpcol_7_113665 c_tptpcol_6_112641 c_airport_physical c_airporthasiatacode s_tlh n_170 c_geographicalregion c_disjointwith c_no c_tptpcol_3_16386 c_tptpcol_5_69635 c_tptpcol_4_65539 c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 c_ship c_objectfoundinlocation c_cityofbostonma c_ap_martha_stewart_omnimedia_names_chairman c_massmediadatamt c_tptpcol_3_114688 c_artsupplies c_tptpcol_8_26629 c_tptpcol_7_26628 c_tptp_member3633_mt c_tptp_8_968 c_tptpcol_16_7738 s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988 c_tptp_member974_mt c_georegion_l3_x11_y2 c_georegion_l4_x35_y7 c_tptpcol_14_109181 c_tptpcol_16_30972 c_tptpcol_15_30970 c_tptpcol_8_18438 c_keinteractionresourcetestmt c_testvocabularymt c_tptpcol_12_118116 c_theprototypicalfurpelt c_tptpcol_6_26627 c_tptpcol_15_109185 c_tptpcol_16_92269 c_cycorpproductsmt c_tptptypes_8_823 c_humansociallifemt c_knowledgefragmentd3mt c_georegion_l2_x5_y8 c_tptpcol_10_26886 c_tptpcol_9_26885 c_tptp_member3717_mt c_tptpcol_15_72793 c_geolocation_x14_y39 c_georegion_l4_x14_y39 c_navypersonnel c_militaryperson c_spatialthing_nonsituational c_georegion_l3_x25_y7 c_physicalorderingpredicate c_relationallexistsfn n_4 c_tptptptpcol_16_25985 c_georegion_l4_x76_y23 c_state_geopolitical c_hpkb_subnationalagent c_tptpcol_7_21508 c_tptp_9_51 c_tptpcol_16_27189 c_tptpcol_3_65538 c_tptpcol_14_26921 c_tptpcol_13_26920 c_tptp_member3993_mt c_tptpnsubcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent_786 s_agen c_france c_intangibleindividual c_wanica_districtsuriname c_tptpcol_16_130924 c_tptpcol_15_130923 c_tptpcol_7_92163 c_tptpcol_16_130933 c_tptpcol_15_130931 c_few c_reasoningaboutpossibleantecedentsmt c_tptpcol_6_20484 s_http_memberstripodcomindygalfordtriviahtm c_translation_32 c_worldcompletedualistgeographymt c_unitedstatesgeographydualistmt c_tptpcol_6_108546 c_tptpcol_11_109125 c_tptp_member2701_mt c_tptpcol_8_93698 s_http_wwwpoweripodsearchinfobrown_ipodhtml c_translation_7 c_tptpcol_6_18436 c_tptpcol_7_18437 c_geolocation_x76_y23 c_tptpcol_8_117763 c_tptpcol_7_117762 c_logicaltruthmt c_aspatialthing s_http_wwwarthritis_symptomcoma_cbursitishtm c_tptpcol_9_93699 c_tptpcol_10_93700 c_tptpcol_4_90113 c_tptpgeo_member4_mt c_georegion_l4_x36_y50 c_georegion_l4_x37_y50 c_unitedstatesgeographypeoplemt c_tptp_8_271 c_tptpcol_16_25972 c_shavingrazor_manual c_tptpcol_5_110593 c_tptpcol_12_72775 c_tptpcol_11_72774 c_tptpcol_6_71683 c_tptpcol_16_50958 c_tptpcol_15_50957 c_tptpcol_8_114177 c_tptpcol_16_72795 c_gregoriancalendarmt c_tptptypes_5_802 c_tptpcol_5_90114 c_tptpcol_13_118117 c_tptptypes_9_824 s_http_wwwahwatukeecomafnentertainmentarticles030423ahtml c_tptpcol_16_26926 c_tptpcol_15_26925 s_http_webnjiteducjohnsontreebiochhtm c_translation_21 c_tptpcol_8_39940 c_tptpcol_7_39939 n_756 c_runningshorts c_tptpcol_15_22076 c_tptp_member2356_mt c_tptptptpcol_16_8398 c_tptp_member698_mt c_pushingwithopenhand c_tptpcol_16_4451 c_footballteam c_affiliatedwith c_beloitcollege s_thefootballteamwhohasbeenaffiliatedwithbeloitcollege c_pushingwithfingers c_tptpcol_15_4027 c_geolevel_4 c_georegion_l4_x38_y24 c_georegion_l4_x39_y24 c_georegion_l4_x75_y75 c_tptpcol_13_92263 c_georegion_l3_x17_y24 c_tptpcol_16_62187 c_tptp_member2862_mt c_tptpcol_16_26939 c_georegion_l4_x29_y75 c_georegion_l4_x29_y76 c_computerdataartifact n_414 c_tptpcol_14_118118 c_tptpquantityfn_6 n_1 c_tptpquantityfn_2 c_citynamedfn n_2 c_reflexivebinarypredicate c_geolevel_1 c_contextofpcwfn c_subcollectionofwithrelationtofn c_tptpquantityfn_21 c_instancewithrelationtofn c_tptpquantityfn_14 c_subcollectionofwithrelationtotypefn c_subcollectionofwithrelationfromtypefn c_geolevel_3 c_tptpquantityfn_13 c_tptpquantityfn_1 c_marriagelicensedocument c_urlfn c_urlreferentfn c_contentmtofcdafromeventfn
% 33.86/7.26 Fol Functions: f_urlfn f_urlreferentfn f_contentmtofcdafromeventfn f_relationexistsallfn f_tptpquantityfn_1 f_tptpquantityfn_13 f_subcollectionofwithrelationfromtypefn f_subcollectionofwithrelationtotypefn f_relationallexistsfn f_tptpquantityfn_14 f_instancewithrelationtofn f_tptpquantityfn_21 f_subcollectionofwithrelationtofn f_contextofpcwfn f_citynamedfn f_tptpquantityfn_2 f_tptpquantityfn_6
% 33.86/7.26 Problem Properties:
% 33.86/7.26 This is a full first-order problem without equality.
% 33.86/7.26
% 33.86/7.26 After reduction: Problem Properties:
% 33.86/7.26 This is a full first-order problem without equality.
% 33.86/7.26
% 33.86/7.26
% 33.86/7.26 Reduced Input Clauses:
% 33.86/7.26
% 33.86/7.26 Most General Atoms: intangible(x0) partiallytangible(x0) tptpcol_15_40430(x0) tptpcol_14_40429(x0) tptpcol_10_72710(x0) tptpcol_9_72709(x0) inanimateobject(x0) tptpcol_7_93186(x0) tptpcol_6_92162(x0) tptpcol_13_40421(x0) tptpcol_12_40420(x0) tptpcol_9_22021(x0) tptpcol_8_22020(x0) tptpcol_5_16388(x0) tptpcol_4_16387(x0) tptpcol_14_72792(x0) tptpcol_13_72791(x0) tptpcol_5_20483(x0) tptpcol_11_22023(x0) tptpcol_10_22022(x0) partiallyintangibleindividual(x0) individual(x0) trajector_underspecified(x0) location_underspecified(x0) enduringthing_localized(x0) tptpcol_3_81921(x0) tptpcol_2_65537(x0) tptpcol_10_18567(x0) tptpcol_9_18439(x0) orderingpredicate(x0) transitivebinarypredicate(x0) tptpcol_11_92230(x0) tptpcol_10_92166(x0) tptpcol_2_98304(x0) tptpcol_1_65536(x0) tptpcol_11_40388(x0) tptptypes_9_693(x0,x1) tptptypes_8_692(x0,x1) tptptypes_8_390(x0,x1) tptptypes_7_389(x0,x1) tptpcol_4_106497(x0) tptpcol_3_98305(x0) tptpcol_5_114690(x0) tptpcol_4_114689(x0) tptpcol_12_93765(x0) tptpcol_11_93764(x0) tptpcol_8_72708(x0) tptpcol_7_72707(x0) tptpcol_10_40324(x0) tptpcol_9_40196(x0) tptpcol_13_93766(x0) furpelt(x0) tptpcol_12_92262(x0) tptpcol_10_109061(x0) tptpcol_9_109060(x0) tptptypes_5_387(x0,x1) tptpcol_6_116738(x0) tptpcol_15_92268(x0) tptpcol_14_92264(x0) ridgeline_topographical(x0) tptptypes_9_401(x0,x1) tptpcol_12_18663(x0) tptpcol_11_18631(x0) mathematicalthing(x0) tptpcol_13_109173(x0) tptpcol_12_109157(x0) tptpcol_5_106498(x0) tptpcol_5_24579(x0) tptpcol_0_0(x0) tptpcol_11_118084(x0) tptpcol_10_118020(x0) mathematicalorcomputationalthing(x0) tptptypes_7_819(x0,x1) tptptypes_6_818(x0,x1) tptpcol_12_26919(x0) tptpcol_11_26887(x0) tptpcol_2_2(x0) tptpcol_1_1(x0) tptpcol_9_92165(x0) tptpcol_8_92164(x0) fixedordercollection(x0) aspatialinformationstore(x0) tptpcol_9_118019(x0) executionbyfiringsquad(x0) tptpcol_12_22055(x0) applicationcontext(x0) tptptypes_8_400(x0,x1) tptptypes_7_396(x0,x1) tptpcol_15_93775(x0) tptpcol_14_93774(x0) tptpcol_8_109059(x0) tptpcol_7_108547(x0) tptpcol_14_22072(x0) tptpcol_13_22071(x0) inanimateobject_nonnatural(x0) supplies(x0) tptpcol_13_18664(x0) tptpcol_7_113665(x0) tptpcol_6_112641(x0) tptpcol_3_16386(x0) tptpcol_5_69635(x0) tptpcol_4_65539(x0) tptpcol_3_114688(x0) artsupplies(x0) tptpcol_8_26629(x0) tptpcol_7_26628(x0) tptpcol_14_109181(x0) tptpcol_16_30972(x0) tptpcol_15_30970(x0) tptpcol_8_18438(x0) tptpcol_12_118116(x0) tptpcol_6_26627(x0) tptpcol_15_109185(x0) tptpcol_16_92269(x0) tptptypes_8_823(x0,x1) tptpcol_10_26886(x0) tptpcol_9_26885(x0) tptpcol_15_72793(x0) navypersonnel(x0) militaryperson(x0) physicalorderingpredicate(x0) genlmt(x0,x2) tptptypes_6_388(x1,x0) state_geopolitical(x0) hpkb_subnationalagent(x0) tptpcol_7_21508(x0) tptpcol_3_65538(x0) tptpcol_14_26921(x0) tptpcol_13_26920(x0) intangibleindividual(x0) tptpcol_16_130924(x0) tptpcol_15_130923(x0) tptpcol_7_92163(x0) tptpcol_16_130933(x0) tptpcol_15_130931(x0) tptpcol_6_20484(x0) tptpcol_6_108546(x0) tptpcol_11_109125(x0) tptpcol_8_93698(x0) tptpcol_6_18436(x0) tptpcol_7_18437(x0) tptpcol_8_117763(x0) tptpcol_7_117762(x0) isa(x0,x2) aspatialthing(x0) tptpcol_9_93699(x0) tptpcol_10_93700(x0) tptpcol_4_90113(x0) shavingrazor_manual(x0) tptpcol_5_110593(x0) tptpcol_12_72775(x0) tptpcol_11_72774(x0) tptpcol_6_71683(x0) tptpcol_16_50958(x0) tptpcol_15_50957(x0) tptpcol_8_114177(x0) tptpcol_16_72795(x0) tptptypes_5_802(x0,x1) tptpcol_5_90114(x0) tptpcol_13_118117(x0) tptptypes_9_824(x0,x1) tptpcol_16_26926(x0) tptpcol_15_26925(x0) tptpcol_8_39940(x0) tptpcol_7_39939(x0) runningshorts(x0) tptpcol_15_22076(x0) geolevel_4(x0) tptpcol_13_92263(x0) computerdataartifact(x0) tptpcol_14_118118(x0) natfunction(f_tptpquantityfn_6(x0),c_tptpquantityfn_6) natargument(f_tptpquantityfn_6(x0),n_1,x0) tptpcol_16_26939(x0) tptpcol_16_62187(x0) tptpcol_15_4027(x0) pushingwithfingers(x0) agent_generic(x0) affiliatedwith(x1,x0) footballteam(x0) tptpcol_16_4451(x0) pushingwithopenhand(x0) natfunction(f_tptpquantityfn_2(x0),c_tptpquantityfn_2) natargument(f_tptpquantityfn_2(x0),n_1,x0) firstordercollection(x1) tptpcol_16_25972(x0) tptp_8_271(x0,x1) razor(x1) microtheory(x1) setorcollection(x1) mtvisible(x1) few(x0,x2) natfunction(f_citynamedfn(x0,x1),c_citynamedfn) natargument(f_citynamedfn(x0,x1),n_1,x0) natargument(f_citynamedfn(x0,x1),n_2,x1) city(f_citynamedfn(x0,x1)) tptpcol_16_27189(x0) tptp_9_51(x0,x1) reflexivebinarypredicate(x0) natfunction(f_relationallexistsfn(x0,x1,x2,x3),c_relationallexistsfn) natargument(f_relationallexistsfn(x0,x1,x2,x3),n_1,x0) natargument(f_relationallexistsfn(x0,x1,x2,x3),n_2,x1) natargument(f_relationallexistsfn(x0,x1,x2,x3),n_3,x2) natargument(f_relationallexistsfn(x0,x1,x2,x3),n_4,x3) relation(x0) arg2isa(x0,x2) geolevel_1(x0) tptpcol_16_7738(x0) tptp_8_968(x0,x1) tptpcol_7_7172(x0) relationexistsall(x0,x1,x2) collection(x2) natfunction(f_contextofpcwfn(x0),c_contextofpcwfn) natargument(f_contextofpcwfn(x0),n_1,x0) arg1isa(x0,x2) spatialthing_nonsituational(x1) spatialthing_localized(x0) objectfoundinlocation(x0,x2) geopoliticalsubdivision(x2,x1) geographicallysubsumes(x2,x1) subregions(x2,x1) ship(x0) natfunction(f_subcollectionofwithrelationtofn(x0,x1,x2),c_subcollectionofwithrelationtofn) natargument(f_subcollectionofwithrelationtofn(x0,x1,x2),n_1,x0) natargument(f_subcollectionofwithrelationtofn(x0,x1,x2),n_2,x1) natargument(f_subcollectionofwithrelationtofn(x0,x1,x2),n_3,x2) subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(x0) disjointwith(x1,x0) no(x0,x2) natfunction(f_tptpquantityfn_21(x0),c_tptpquantityfn_21) natargument(f_tptpquantityfn_21(x0),n_1,x0) airporthasiatacode(x0,x1) stringoflengthfn3(x1) airport_physical(x0) natfunction(f_instancewithrelationtofn(x0,x1,x2),c_instancewithrelationtofn) natargument(f_instancewithrelationtofn(x0,x1,x2),n_1,x0) natargument(f_instancewithrelationtofn(x0,x1,x2),n_2,x1) natargument(f_instancewithrelationtofn(x0,x1,x2),n_3,x2) natfunction(f_tptpquantityfn_14(x0),c_tptpquantityfn_14) natargument(f_tptpquantityfn_14(x0),n_1,x0) tptpcol_16_8886(x0) orientation(x0,x1) orientationvector(x0) subcollectionofwithrelationfromtypefnorientationvectororientationpartiallytangible(x0) tptpcol_16_29490(x0) tptp_9_720(x0,x1) tptpcol_5_28674(x1) tptpcol_16_31868(x0) movement_translationevent(x0) subevents(x0,x2) directionoftranslation_throughout(x2,x1) unitvectorinterval(x0) subcollectionofwithrelationfromtypefnunitvectorintervaldirectionoftranslation_throughoutmovement_translationevent(x0) tptp_8_875(x0,x1) tptpcol_4_24578(x1) relationallexists(x0,x1,x2) tptpcol_16_10258(x0) pushingababycarriage(x0) tptptypes_7_691(x0,x1) correctivelensprescription(x0) products(x0,x1) artifact(x1) creationordestructionevent(x0) issuingaprescription(x0) natfunction(f_subcollectionofwithrelationtotypefn(x0,x1,x2),c_subcollectionofwithrelationtotypefn) natargument(f_subcollectionofwithrelationtotypefn(x0,x1,x2),n_1,x0) natargument(f_subcollectionofwithrelationtotypefn(x0,x1,x2),n_2,x1) natargument(f_subcollectionofwithrelationtotypefn(x0,x1,x2),n_3,x2) subcollectionofwithrelationtotypefnissuingaprescriptionproductscorrectivelensprescription(x0) terroristgroup(x0) hasmembers(x0,x1) organization(x0) terrorist(x0) natfunction(f_subcollectionofwithrelationfromtypefn(x0,x1,x2),c_subcollectionofwithrelationfromtypefn) natargument(f_subcollectionofwithrelationfromtypefn(x0,x1,x2),n_1,x0) natargument(f_subcollectionofwithrelationfromtypefn(x0,x1,x2),n_2,x1) natargument(f_subcollectionofwithrelationfromtypefn(x0,x1,x2),n_3,x2) subcollectionofwithrelationfromtypefnterroristhasmembersterroristgroup(x0) prettystring(x0,x1) controlcharacterfreestring(x1) geolevel_3(x0) natfunction(f_tptpquantityfn_13(x0),c_tptpquantityfn_13) natargument(f_tptpquantityfn_13(x0),n_1,x0) geographicalregion(x1) borderson(x1,x0) inregion(x0,x2) natfunction(f_tptpquantityfn_1(x0),c_tptpquantityfn_1) natargument(f_tptpquantityfn_1(x0),n_1,x0) tptpofobject(x0,x1) tptpquantity(x1) relationallinstance(x0,x1,x2) thing(x2) natfunction(f_relationexistsallfn(x0,x1,x2,x3),c_relationexistsallfn) natargument(f_relationexistsallfn(x0,x1,x2,x3),n_1,x0) natargument(f_relationexistsallfn(x0,x1,x2,x3),n_2,x1) natargument(f_relationexistsallfn(x0,x1,x2,x3),n_3,x2) natargument(f_relationexistsallfn(x0,x1,x2,x3),n_4,x3) resultisaarg(x0,x1) positiveinteger(x1) function_denotational(x0) marriagelicensedocument(x0) geographicalsubregions(x0,x2) most(x0,x2) genls(x0,x2) subsetof(x0,x2) predicate(x0) binarypredicate(x1) genlpreds(x2,x0) genlinverse(x0,x2) natfunction(f_urlfn(x0),c_urlfn) natargument(f_urlfn(x0),n_1,x0) uniformresourcelocator(f_urlfn(x0)) natfunction(f_urlreferentfn(x0),c_urlreferentfn) natargument(f_urlreferentfn(x0),n_1,x0) natfunction(f_contentmtofcdafromeventfn(x0,x1),c_contentmtofcdafromeventfn) natargument(f_contentmtofcdafromeventfn(x0,x1),n_1,x0) natargument(f_contentmtofcdafromeventfn(x0,x1),n_2,x1)
% 33.86/7.26
% 33.86/7.26 === Starting SPASS-SCL-FOL A Little Less Naive, considering 164 atoms initially, heuristics mode: resolution_1 ===
% 33.86/7.26
% 33.86/7.26 === Backtracking. Learning clause 1134:2:1:[31.2,194.1]:Top: tptpcol_11_22023(x0) -> tptpcol_9_22021(x0)
% 33.86/7.26 === Backtracking. Learning clause 1135:2:1:[69.2,234.1]:Top: tptpcol_4_106497(x0) -> tptpcol_2_98304(x0)
% 33.86/7.26 === Backtracking. Learning clause 1136:1:0:[171.1,83.1]:: -> microtheory(c_wamt_evalinitial_p14)
% 33.86/7.26 === Backtracking. Learning clause 1137:2:1:[110.2,176.1]:Top: tptpcol_12_18663(x0) -> tptpcol_10_18567(x0)
% 33.86/7.26 === Backtracking. Learning clause 1138:2:1:[180.2,132.1]:Top: mathematicalthing(x0) -> intangible(x0)
% 33.86/7.26 === Backtracking. Learning clause 1139:2:1:[146.2,153.1]:Top: tptpcol_2_2(x0),tptpcol_1_65536(x0) ->
% 33.86/7.26 === Backtracking. Learning clause 1140:2:1:[151.2,289.1]:Top: fixedordercollection(x0),individual(x0) ->
% 33.86/7.26 === Backtracking. Learning clause 1141:2:1:[183.2,192.1]:Top: tptpcol_15_93775(x0) -> tptpcol_13_93766(x0)
% 33.86/7.26 === Backtracking. Learning clause 1142:2:1:[190.2,231.1]:Top: tptpcol_14_22072(x0) -> tptpcol_12_22055(x0)
% 33.86/7.26 === Backtracking. Learning clause 1143:1:0:[294.1,246.1]:: -> orderingpredicate(c_geographicalsubregions)
% 33.86/7.26 === Backtracking. Learning clause 1144:2:1:[1128.2,20.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2610_mt)
% 33.86/7.26 === Backtracking. Learning clause 1145:2:1:[1128.2,198.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member237_mt)
% 33.86/7.26 === Backtracking. Learning clause 1146:2:1:[1128.2,115.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_calendarsmt)
% 33.86/7.26 === Backtracking. Learning clause 1147:2:1:[1128.2,125.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_hpkbvocabmt)
% 33.86/7.26 === Backtracking. Learning clause 1148:2:1:[1128.2,34.1]:Top: genlmt(x0,c_tptp_member3205_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1149:2:1:[1128.2,35.1]:Top: genlmt(x0,c_peopledatamt) -> genlmt(x0,c_unitedstatessociallifemt)
% 33.86/7.26 === Backtracking. Learning clause 1150:2:1:[1128.2,52.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> genlmt(x0,c_ldscgeneralcollectormt)
% 33.86/7.26 === Backtracking. Learning clause 1151:2:1:[1128.2,53.1]:Top: genlmt(x0,c_ethnicgroupsmt) -> genlmt(x0,c_ethnicgroupsvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1152:2:1:[1128.1,58.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> genlmt(c_machinelearningspindleheadmt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1153:2:1:[1128.2,177.1]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> genlmt(x0,c_cycnounlearnermt)
% 33.86/7.26 === Backtracking. Learning clause 1154:2:1:[1128.2,59.1]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt) -> genlmt(x0,c_currentworlddatacollectormt_nonhomocentric)
% 33.86/7.26 === Backtracking. Learning clause 1155:2:1:[1128.1,63.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member7_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1156:2:1:[1128.2,66.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_organizationdatamt)
% 33.86/7.26 === Backtracking. Learning clause 1157:2:1:[1128.2,88.1]:Top: genlmt(x0,c_patterndetectormt) -> genlmt(x0,c_basekb)
% 33.86/7.26 === Backtracking. Learning clause 1158:2:1:[1128.1,206.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_universalvocabularymt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1159:2:1:[1128.2,92.1]:Top: genlmt(x0,c_universalvocabularymt) -> genlmt(x0,c_corecyclmt)
% 33.86/7.26 === Backtracking. Learning clause 1160:2:1:[1128.1,93.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2831_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1161:2:1:[1128.1,133.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3393_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1162:2:1:[1128.1,136.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_generictemporalmt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1163:2:1:[1128.1,137.1]:Top: genlmt(c_worldgeographymt,x0) -> genlmt(c_worldgeographydualistmt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1164:2:1:[1128.2,137.1]:Top: genlmt(x0,c_worldgeographydualistmt) -> genlmt(x0,c_worldgeographymt)
% 33.86/7.26 === Backtracking. Learning clause 1165:2:1:[1128.2,273.1]:Top: genlmt(x0,c_tptpgeo_spindlecollectormt) -> genlmt(x0,c_tptpgeo_member2_mt)
% 33.86/7.26 === Backtracking. Learning clause 1166:2:1:[1128.1,147.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3515_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1167:2:1:[1128.1,154.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_geographymt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1168:2:1:[1128.1,162.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_calendarsvocabularymt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1169:2:1:[1128.1,172.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2089_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1170:2:1:[1128.2,269.1]:Top: genlmt(x0,c_cycnounlearnermt) -> genlmt(x0,c_cycorpproductsmt)
% 33.86/7.26 === Backtracking. Learning clause 1171:2:1:[1128.1,212.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member3_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1172:2:1:[1128.1,214.1]:Top: genlmt(c_generictemporalmt,x0) -> genlmt(c_timehasnoendmt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1173:2:1:[1128.1,243.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3633_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1174:2:1:[1128.1,248.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member974_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1176:2:1:[1128.1,275.1]:Top: genlmt(c_nooescapearchitecturemt,x0) -> genlmt(c_testvocabularymt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1177:2:1:[1128.1,272.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_humansociallifemt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1178:2:1:[1128.1,274.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_knowledgefragmentd3mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1179:2:1:[1128.1,279.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3717_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1180:2:1:[1128.1,232.1]:Top: genlmt(c_massmediadatamt,x0) -> genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),x0)
% 33.86/7.26 === Backtracking. Learning clause 1181:2:1:[1128.2,232.1]:Top: genlmt(x0,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) -> genlmt(x0,c_massmediadatamt)
% 33.86/7.26 === Backtracking. Learning clause 1182:2:0:[105.3,1133.1]:: mtvisible(c_tptp_member235_mt),ridgeline_topographical(c_tptpridgeline_topographical) ->
% 33.86/7.26 === Backtracking. Learning clause 1183:2:1:[1128.1,62.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33),x0)
% 33.86/7.26 === Backtracking. Learning clause 1184:2:1:[1128.1,67.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwfuntriviacomplayquizcfmqid60926origin)),c_translation_0_885),x0)
% 33.86/7.26 === Backtracking. Learning clause 1185:2:1:[1128.1,181.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14),x0)
% 33.86/7.26 === Backtracking. Learning clause 1186:2:1:[1128.1,247.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),x0)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 228
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1187:1:0:[1127.1,1.1]:: -> microtheory(c_tptpgeo_member8_mt)
% 33.86/7.26 === Backtracking. Learning clause 1188:2:1:[1128.2,326.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_worldgeographymt)
% 33.86/7.26 === Backtracking. Learning clause 1189:2:1:[1128.2,367.1]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> genlmt(x0,c_worldcompletedualistgeographymt)
% 33.86/7.26 === Backtracking. Learning clause 1190:2:1:[1128.2,378.1]:Top: genlmt(x0,c_calendarsmt) -> genlmt(x0,c_calendarsvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1191:2:1:[1128.2,334.1]:Top: genlmt(x0,c_worldgeographymt) -> genlmt(x0,c_geographymt)
% 33.86/7.26 === Backtracking. Learning clause 1192:3:2:[1128.2,1167.2,334.1,1128.2]:TopTop: genlmt(c_basekb,x0),genlmt(x1,c_worldgeographymt) -> genlmt(x1,x0)
% 33.86/7.26 === Backtracking. Learning clause 1193:2:1:[1128.1,338.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32),x0)
% 33.86/7.26 === Backtracking. Learning clause 1194:2:1:[1128.1,368.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),c_translation_0_885),x0)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 317
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1195:2:1:[262.2,375.1,240.2]:Top: tptpcol_8_26629(x0) -> tptpcol_5_24579(x0)
% 33.86/7.26 === Backtracking. Learning clause 1196:2:1:[278.2,411.1]:Top: tptpcol_10_26886(x0) -> tptpcol_8_26629(x0)
% 33.86/7.26 === Backtracking. Learning clause 1197:2:1:[360.2,343.1]:Top: tptpcol_12_109157(x0) -> tptpcol_10_109061(x0)
% 33.86/7.26 === Backtracking. Learning clause 1198:2:1:[380.1,373.2]:Top: tptpcol_11_93764(x0) -> tptpcol_9_93699(x0)
% 33.86/7.26 === Conflict found: 1188:2:1:[1128.2,326.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_worldgeographymt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1199:1:0:[1188.2,1125.1,1.1]:: -> microtheory(c_worldgeographymt)
% 33.86/7.26 === Conflict found: 1191:2:1:[1128.2,334.1]:Top: genlmt(x0,c_worldgeographymt) -> genlmt(x0,c_geographymt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1200:1:0:[1191.2,1125.1,1188.2,1.1]:: -> microtheory(c_geographymt)
% 33.86/7.26 === Backtracking. Learning clause 1201:1:0:[1127.1,20.1]:: -> microtheory(c_tptp_spindlecollectormt)
% 33.86/7.26 === Backtracking. Learning clause 1202:1:0:[1125.1,364.1]:: -> microtheory(c_tptp_member3993_mt)
% 33.86/7.26 === Backtracking. Learning clause 1203:1:0:[1127.1,34.1]:: -> microtheory(c_tptp_member3205_mt)
% 33.86/7.26 === Conflict found: 1148:2:1:[1128.2,34.1]:Top: genlmt(x0,c_tptp_member3205_mt) -> genlmt(x0,c_tptp_spindleheadmt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1204:2:1:[1148.2,1125.1]:Top: genlmt(x0,c_tptp_member3205_mt) -> microtheory(c_tptp_spindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1205:1:0:[1125.1,34.1]:: -> microtheory(c_tptp_spindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1206:2:1:[1128.2,254.1,1148.2]:Top: genlmt(x0,c_tptp_member3205_mt) -> genlmt(x0,c_cyclistsmt)
% 33.86/7.26 === Backtracking. Learning clause 1207:1:0:[1127.1,35.1]:: -> microtheory(c_peopledatamt)
% 33.86/7.26 === Backtracking. Learning clause 1208:1:0:[1125.1,367.1]:: -> microtheory(c_worldcompletedualistgeographymt)
% 33.86/7.26 === Backtracking. Learning clause 1209:1:0:[1127.1,58.1]:: -> microtheory(c_machinelearningspindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1210:1:0:[1125.1,177.1]:: -> microtheory(c_cycnounlearnermt)
% 33.86/7.26 === Backtracking. Learning clause 1211:1:0:[1127.1,63.1]:: -> microtheory(c_tptpgeo_member7_mt)
% 33.86/7.26 === Conflict found: 1160:2:1:[1128.1,93.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2831_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1212:2:1:[1160.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member2831_mt)
% 33.86/7.26 === Backtracking. Learning clause 1213:2:1:[1128.1,254.1,1212.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2831_mt)
% 33.86/7.26 === Conflict found: 1213:2:1:[1128.1,254.1,1212.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2831_mt) {x0 -> c_calendarsmt}
% 33.86/7.26 === Backtracking. Learning clause 1214:1:0:[1213.1,115.1]:: -> microtheory(c_tptp_member2831_mt)
% 33.86/7.26 === Backtracking. Learning clause 1215:2:1:[1128.2,93.1]:Top: genlmt(x0,c_tptp_member2831_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 33.86/7.26 === Conflict found: 1161:2:1:[1128.1,133.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3393_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1216:2:1:[1161.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3393_mt)
% 33.86/7.26 === Backtracking. Learning clause 1217:2:1:[1128.1,254.1,1216.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3393_mt)
% 33.86/7.26 === Conflict found: 1217:2:1:[1128.1,254.1,1216.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3393_mt) {x0 -> c_calendarsmt}
% 33.86/7.26 === Backtracking. Learning clause 1218:1:0:[1217.1,115.1]:: -> microtheory(c_tptp_member3393_mt)
% 33.86/7.26 === Backtracking. Learning clause 1219:1:0:[1127.1,137.1]:: -> microtheory(c_worldgeographydualistmt)
% 33.86/7.26 === Backtracking. Learning clause 1220:1:0:[1127.1,369.1]:: -> microtheory(c_tptpgeo_spindlecollectormt)
% 33.86/7.26 === Backtracking. Learning clause 1221:2:1:[1128.2,140.1]:Top: genlmt(x0,c_tptpgeo_spindlecollectormt) -> genlmt(x0,c_tptpgeo_member1_mt)
% 33.86/7.26 === Conflict found: 1166:2:1:[1128.1,147.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3515_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1222:2:1:[1166.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3515_mt)
% 33.86/7.26 === Backtracking. Learning clause 1223:2:1:[1128.1,254.1,1222.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3515_mt)
% 33.86/7.26 === Conflict found: 1223:2:1:[1128.1,254.1,1222.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3515_mt) {x0 -> c_calendarsmt}
% 33.86/7.26 === Backtracking. Learning clause 1224:1:0:[1223.1,115.1]:: -> microtheory(c_tptp_member3515_mt)
% 33.86/7.26 === Backtracking. Learning clause 1225:2:1:[1128.2,147.1]:Top: genlmt(x0,c_tptp_member3515_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 33.86/7.26 === Conflict found: 1169:2:1:[1128.1,172.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2089_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1226:2:1:[1169.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member2089_mt)
% 33.86/7.26 === Backtracking. Learning clause 1227:2:1:[1128.1,254.1,1226.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2089_mt)
% 33.86/7.26 === Conflict found: 1227:2:1:[1128.1,254.1,1226.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2089_mt) {x0 -> c_calendarsmt}
% 33.86/7.26 === Backtracking. Learning clause 1228:1:0:[1227.1,115.1]:: -> microtheory(c_tptp_member2089_mt)
% 33.86/7.26 === Backtracking. Learning clause 1229:2:1:[1128.2,172.1]:Top: genlmt(x0,c_tptp_member2089_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1230:1:0:[1127.1,212.1]:: -> microtheory(c_tptpgeo_member3_mt)
% 33.86/7.26 === Backtracking. Learning clause 1231:1:0:[1127.1,214.1]:: -> microtheory(c_timehasnoendmt)
% 33.86/7.26 === Backtracking. Learning clause 1232:2:1:[1128.2,329.1]:Top: genlmt(x0,c_massmediadatamt) -> genlmt(x0,c_ethnicgroupsmt)
% 33.86/7.26 === Conflict found: 1173:2:1:[1128.1,243.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3633_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1233:2:1:[1173.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3633_mt)
% 33.86/7.26 === Backtracking. Learning clause 1234:2:1:[1128.1,254.1,1233.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3633_mt)
% 33.86/7.26 === Conflict found: 1234:2:1:[1128.1,254.1,1233.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3633_mt) {x0 -> c_calendarsmt}
% 33.86/7.26 === Backtracking. Learning clause 1235:1:0:[1234.1,115.1]:: -> microtheory(c_tptp_member3633_mt)
% 33.86/7.26 === Backtracking. Learning clause 1236:2:1:[1128.2,243.1]:Top: genlmt(x0,c_tptp_member3633_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 33.86/7.26 === Conflict found: 1174:2:1:[1128.1,248.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member974_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1237:2:1:[1174.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member974_mt)
% 33.86/7.26 === Backtracking. Learning clause 1238:2:1:[1128.1,254.1,1237.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member974_mt)
% 33.86/7.26 === Conflict found: 1238:2:1:[1128.1,254.1,1237.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member974_mt) {x0 -> c_calendarsmt}
% 33.86/7.26 === Backtracking. Learning clause 1239:1:0:[1238.1,115.1]:: -> microtheory(c_tptp_member974_mt)
% 33.86/7.26 === Backtracking. Learning clause 1240:2:1:[1128.2,275.1,1175.2]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_nooescapearchitecturemt)
% 33.86/7.26 === Backtracking. Learning clause 1241:2:1:[1128.2,275.1]:Top: genlmt(x0,c_testvocabularymt) -> genlmt(x0,c_nooescapearchitecturemt)
% 33.86/7.26 === Backtracking. Learning clause 1242:1:0:[1127.1,272.1]:: -> microtheory(c_humansociallifemt)
% 33.86/7.26 === Backtracking. Learning clause 1243:1:0:[1127.1,274.1]:: -> microtheory(c_knowledgefragmentd3mt)
% 33.86/7.26 === Conflict found: 1179:2:1:[1128.1,279.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3717_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1244:2:1:[1179.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3717_mt)
% 33.86/7.26 === Backtracking. Learning clause 1245:2:1:[1128.1,254.1,1244.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3717_mt)
% 33.86/7.26 === Conflict found: 1245:2:1:[1128.1,254.1,1244.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3717_mt) {x0 -> c_calendarsmt}
% 33.86/7.26 === Backtracking. Learning clause 1246:1:0:[1245.1,115.1]:: -> microtheory(c_tptp_member3717_mt)
% 33.86/7.26 === Backtracking. Learning clause 1247:2:1:[1128.2,315.1]:Top: genlmt(x0,c_tptp_member3993_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1248:2:1:[1128.2,333.1]:Top: genlmt(x0,c_reasoningaboutpossibleantecedentsmt) -> genlmt(x0,c_humansociallifemt)
% 33.86/7.26 === Backtracking. Learning clause 1249:2:1:[1128.1,333.1]:Top: genlmt(c_humansociallifemt,x0) -> genlmt(c_reasoningaboutpossibleantecedentsmt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1250:2:1:[1128.2,384.1]:Top: genlmt(x0,c_unitedstatesgeographypeoplemt) -> genlmt(x0,c_peopledatamt)
% 33.86/7.26 === Backtracking. Learning clause 1251:2:2:[427.2,271.1]:TopTop: tptptypes_9_824(x0,x1) -> tptptypes_7_819(x0,x1)
% 33.86/7.26 === Backtracking. Learning clause 1252:2:1:[1128.2,338.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1253:2:1:[1128.2,433.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 383
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1254:2:1:[386.1,223.2,1139.1]:Top: tptpcol_4_24578(x0),tptpcol_1_65536(x0) ->
% 33.86/7.26 === Backtracking. Learning clause 1255:2:1:[262.2,375.1]:Top: tptpcol_7_26628(x0) -> tptpcol_5_24579(x0)
% 33.86/7.26 === Backtracking. Learning clause 1256:2:1:[437.2,312.1]:Top: tptpcol_4_65539(x0) -> tptpcol_2_65537(x0)
% 33.86/7.26 === Conflict found: 1156:2:1:[1128.2,66.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_organizationdatamt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1257:2:1:[1156.2,1125.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> microtheory(c_organizationdatamt)
% 33.86/7.26 === Backtracking. Learning clause 1258:2:1:[1128.2,350.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2668_mt)
% 33.86/7.26 === Backtracking. Learning clause 1259:2:1:[1128.2,344.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2701_mt)
% 33.86/7.26 === Backtracking. Learning clause 1260:2:1:[1128.2,448.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member698_mt)
% 33.86/7.26 === Backtracking. Learning clause 1261:1:0:[1125.1,115.1]:: -> microtheory(c_calendarsmt)
% 33.86/7.26 === Conflict found: 1190:2:1:[1128.2,378.1]:Top: genlmt(x0,c_calendarsmt) -> genlmt(x0,c_calendarsvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1262:2:1:[1190.2,1125.1]:Top: genlmt(x0,c_calendarsmt) -> microtheory(c_calendarsvocabularymt)
% 33.86/7.26 === Conflict found: 1262:2:1:[1190.2,1125.1]:Top: genlmt(x0,c_calendarsmt) -> microtheory(c_calendarsvocabularymt) {x0 -> c_cyclistsmt}
% 33.86/7.26 === Backtracking. Learning clause 1263:1:0:[1262.1,115.1]:: -> microtheory(c_calendarsvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1264:1:0:[1125.1,310.1]:: -> microtheory(c_keinteractionresourcetestmt)
% 33.86/7.26 === Backtracking. Learning clause 1265:2:1:[1128.2,254.1]:Top: genlmt(x0,c_tptp_spindleheadmt) -> genlmt(x0,c_cyclistsmt)
% 33.86/7.26 === Backtracking. Learning clause 1266:2:1:[1128.2,364.1,1247.1,1265.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_cyclistsmt)
% 33.86/7.26 === Backtracking. Learning clause 1267:2:1:[1128.2,310.1,1240.1,1257.1,1266.2]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_organizationdatamt)
% 33.86/7.26 === Backtracking. Learning clause 1268:2:1:[1128.2,414.1,1125.1,1149.2]:Top: genlmt(x0,c_peopledatamt) -> microtheory(c_gregoriancalendarmt)
% 33.86/7.26 === Backtracking. Learning clause 1269:2:1:[1128.2,414.1,1125.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> microtheory(c_gregoriancalendarmt)
% 33.86/7.26 === Conflict found: 1269:2:1:[1128.2,414.1,1125.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> microtheory(c_gregoriancalendarmt) {x0 -> c_peopledatamt}
% 33.86/7.26 === Backtracking. Learning clause 1270:1:0:[1269.1,35.1]:: -> microtheory(c_gregoriancalendarmt)
% 33.86/7.26 === Backtracking. Learning clause 1271:2:1:[1128.2,414.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> genlmt(x0,c_gregoriancalendarmt)
% 33.86/7.26 === Backtracking. Learning clause 1272:2:1:[1128.2,87.1,1125.1,1150.2]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> microtheory(c_ldscdemonstrationspindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1273:1:0:[1125.1,87.1]:: -> microtheory(c_ldscdemonstrationspindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1274:2:1:[1128.2,87.1]:Top: genlmt(x0,c_ldscgeneralcollectormt) -> genlmt(x0,c_ldscdemonstrationspindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1275:1:0:[1127.1,53.1]:: -> microtheory(c_ethnicgroupsmt)
% 33.86/7.26 === Backtracking. Learning clause 1276:1:0:[1125.1,53.1]:: -> microtheory(c_ethnicgroupsvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1277:1:0:[1125.1,66.1]:: -> microtheory(c_organizationdatamt)
% 33.86/7.26 === Backtracking. Learning clause 1278:2:1:[1128.2,310.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_keinteractionresourcetestmt)
% 33.86/7.26 === Conflict found: 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1279:2:1:[1175.2,1125.1,1278.2,1266.2]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_testvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1280:1:0:[1127.1,88.1]:: -> microtheory(c_patterndetectormt)
% 33.86/7.26 === Backtracking. Learning clause 1281:1:0:[1125.1,88.1]:: -> microtheory(c_basekb)
% 33.86/7.26 === Backtracking. Learning clause 1282:2:1:[1128.2,133.1]:Top: genlmt(x0,c_tptp_member3393_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1283:1:0:[1127.1,136.1]:: -> microtheory(c_generictemporalmt)
% 33.86/7.26 === Backtracking. Learning clause 1284:2:1:[1128.2,407.1]:Top: genlmt(x0,c_tptpgeo_spindlecollectormt) -> genlmt(x0,c_tptpgeo_member5_mt)
% 33.86/7.26 === Backtracking. Learning clause 1285:1:0:[1125.1,269.1]:: -> microtheory(c_cycorpproductsmt)
% 33.86/7.26 === Backtracking. Learning clause 1286:2:1:[1128.2,214.1]:Top: genlmt(x0,c_timehasnoendmt) -> genlmt(x0,c_generictemporalmt)
% 33.86/7.26 === Backtracking. Learning clause 1287:1:0:[1127.1,329.1]:: -> microtheory(c_massmediadatamt)
% 33.86/7.26 === Backtracking. Learning clause 1288:1:0:[1125.1,257.1]:: -> microtheory(c_testvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1289:2:1:[1128.1,315.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3993_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1290:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt)
% 33.86/7.26 === Backtracking. Learning clause 1291:2:1:[1128.2,454.1,1290.2,1189.2]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> genlmt(x0,c_worldgeographydualistmt)
% 33.86/7.26 === Backtracking. Learning clause 1292:1:0:[1127.1,384.1]:: -> microtheory(c_unitedstatesgeographypeoplemt)
% 33.86/7.26 === Backtracking. Learning clause 1293:1:0:[1127.1,446.1]:: -> microtheory(c_tptp_member2356_mt)
% 33.86/7.26 === Backtracking. Learning clause 1294:2:1:[1128.2,486.1,1181.1,1232.1,1156.2]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_ethnicgroupsmt)
% 33.86/7.26 === Conflict found: 1240:2:1:[1128.2,275.1,1175.2]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_nooescapearchitecturemt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1295:2:1:[1240.1,1278.2,1294.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_ethnicgroupsmt)
% 33.86/7.26 === Backtracking. Learning clause 1296:2:1:[1128.2,486.1,1181.1]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,c_massmediadatamt)
% 33.86/7.26 === Backtracking. Learning clause 1297:2:1:[1128.2,486.1]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))
% 33.86/7.26 === Backtracking. Learning clause 1298:2:1:[1128.2,67.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwfuntriviacomplayquizcfmqid60926origin)),c_translation_0_885)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1299:2:1:[1128.2,247.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1300:2:1:[1128.2,368.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),c_translation_0_885)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 448
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1301:2:1:[119.2,1254.1]:Top: tptpcol_5_24579(x0),tptpcol_1_65536(x0) ->
% 33.86/7.26 === Backtracking. Learning clause 1302:2:1:[386.1,286.2,1139.1,349.2]:Top: tptpcol_4_16387(x0),tptpcol_2_65537(x0) ->
% 33.86/7.26 === Backtracking. Learning clause 1303:2:1:[386.1,286.2,1139.1]:Top: tptpcol_4_16387(x0),tptpcol_1_65536(x0) ->
% 33.86/7.26 === Backtracking. Learning clause 1304:2:1:[386.1,286.2]:Top: tptpcol_4_16387(x0) -> tptpcol_2_2(x0)
% 33.86/7.26 === Backtracking. Learning clause 1305:2:1:[225.2,1256.1]:Top: tptpcol_5_69635(x0) -> tptpcol_2_65537(x0)
% 33.86/7.26 === Backtracking. Learning clause 1306:2:1:[341.2,459.1]:Top: tptpcol_7_108547(x0) -> tptpcol_5_106498(x0)
% 33.86/7.26 === Backtracking. Learning clause 1307:2:1:[477.1,418.2]:Top: tptpcol_6_92162(x0) -> tptpcol_4_90113(x0)
% 33.86/7.26 === Backtracking. Learning clause 1308:1:0:[1125.1,1.1]:: -> microtheory(c_tptpgeo_spindleheadmt)
% 33.86/7.26 === Conflict found: 1266:2:1:[1128.2,364.1,1247.1,1265.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_cyclistsmt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1309:2:1:[1266.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_cyclistsmt)
% 33.86/7.26 === Backtracking. Learning clause 1310:1:0:[1127.1,115.1]:: -> microtheory(c_cyclistsmt)
% 33.86/7.26 === Conflict found: 1240:2:1:[1128.2,275.1,1175.2]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_nooescapearchitecturemt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1311:2:1:[1240.1,1278.2]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_nooescapearchitecturemt)
% 33.86/7.26 === Backtracking. Learning clause 1312:2:1:[1128.2,419.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member235_mt)
% 33.86/7.26 === Backtracking. Learning clause 1313:1:0:[1127.1,52.1]:: -> microtheory(c_miptdatabase19681997_termsmt)
% 33.86/7.26 === Backtracking. Learning clause 1314:1:0:[1125.1,455.1]:: -> microtheory(c_universalvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1315:2:1:[1128.2,455.1]:Top: genlmt(x0,c_basekb) -> genlmt(x0,c_universalvocabularymt)
% 33.86/7.26 === Backtracking. Learning clause 1316:2:1:[1128.2,358.1]:Top: genlmt(x0,c_corecyclmt) -> genlmt(x0,c_logicaltruthmt)
% 33.86/7.26 === Backtracking. Learning clause 1317:2:1:[1128.1,446.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2356_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1318:1:0:[1127.1,479.1]:: -> microtheory(c_tptp_member2862_mt)
% 33.86/7.26 === Backtracking. Learning clause 1319:2:1:[1128.1,347.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7),x0)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 514
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1320:2:1:[236.2,488.2]:Top: tptpcol_4_114689(x0),tptpcol_3_98305(x0) ->
% 33.86/7.26 === Backtracking. Learning clause 1321:2:1:[382.2,320.1,156.2]:Top: microtheory(x0) -> partiallyintangibleindividual(x0)
% 33.86/7.26 === Backtracking. Learning clause 1322:2:1:[457.2,336.1]:Top: tptpcol_7_21508(x0) -> tptpcol_5_20483(x0)
% 33.86/7.26 === Backtracking. Learning clause 1323:2:1:[484.1,354.2]:Top: tptpcol_8_18438(x0) -> tptpcol_6_18436(x0)
% 33.86/7.26 === Backtracking. Learning clause 1324:2:1:[432.2,481.1]:Top: tptpcol_16_26926(x0) -> tptpcol_14_26921(x0)
% 33.86/7.26 === Conflict found: 1159:2:1:[1128.2,92.1]:Top: genlmt(x0,c_universalvocabularymt) -> genlmt(x0,c_corecyclmt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1325:2:1:[1159.2,1125.1,1315.2]:Top: genlmt(x0,c_basekb) -> microtheory(c_corecyclmt)
% 33.86/7.26 === Conflict found: 1159:2:1:[1128.2,92.1]:Top: genlmt(x0,c_universalvocabularymt) -> genlmt(x0,c_corecyclmt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1326:2:1:[1159.2,1125.1]:Top: genlmt(x0,c_universalvocabularymt) -> microtheory(c_corecyclmt)
% 33.86/7.26 === Conflict found: 1290:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1327:2:1:[1290.2,1125.1,1189.2,1151.2]:Top: genlmt(x0,c_ethnicgroupsmt) -> microtheory(c_unitedstatesgeographydualistmt)
% 33.86/7.26 === Conflict found: 1290:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1328:2:1:[1290.2,1125.1,1189.2]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> microtheory(c_unitedstatesgeographydualistmt)
% 33.86/7.26 === Conflict found: 1328:2:1:[1290.2,1125.1,1189.2]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> microtheory(c_unitedstatesgeographydualistmt) {x0 -> c_ethnicgroupsmt}
% 33.86/7.26 === Backtracking. Learning clause 1329:1:0:[1328.1,53.1]:: -> microtheory(c_unitedstatesgeographydualistmt)
% 33.86/7.26 === Backtracking. Learning clause 1330:2:1:[1128.2,58.1]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> genlmt(x0,c_miptdatabase19681997_termsmt)
% 33.86/7.26 === Backtracking. Learning clause 1331:1:0:[1127.1,66.1]:: -> microtheory(c_nooescapearchitecturemt)
% 33.86/7.26 === Conflict found: 1325:2:1:[1159.2,1125.1,1315.2]:Top: genlmt(x0,c_basekb) -> microtheory(c_corecyclmt) {x0 -> c_patterndetectormt}
% 33.86/7.26 === Backtracking. Learning clause 1332:1:0:[1325.1,88.1]:: -> microtheory(c_corecyclmt)
% 33.86/7.26 === Backtracking. Learning clause 1333:1:0:[1127.1,333.1]:: -> microtheory(c_reasoningaboutpossibleantecedentsmt)
% 33.86/7.26 === Backtracking. Learning clause 1334:2:1:[1128.1,454.1]:Top: genlmt(c_worldgeographydualistmt,x0) -> genlmt(c_unitedstatesgeographydualistmt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1335:2:1:[1128.1,479.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2862_mt,x0)
% 33.86/7.26 === Backtracking. Learning clause 1336:2:2:[174.2,409.1]:TopTop: tptptypes_8_400(x0,x1) -> tptptypes_6_388(x0,x1)
% 33.86/7.26 === Backtracking. Learning clause 1337:2:1:[1128.2,347.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1338:2:1:[1128.1,433.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21),x0)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 578
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1339:2:1:[314.2,466.1]:Top: tptpcol_14_26921(x0) -> tptpcol_12_26919(x0)
% 33.86/7.26 === Backtracking. Learning clause 1340:1:0:[1125.1,35.1]:: -> microtheory(c_unitedstatessociallifemt)
% 33.86/7.26 === Backtracking. Learning clause 1341:2:1:[1128.1,384.1]:Top: genlmt(c_peopledatamt,x0) -> genlmt(c_unitedstatesgeographypeoplemt,x0)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 644
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1342:1:0:[205.1,475.1]:: -> fixedordercollection(c_tptpcol_16_62187)
% 33.86/7.26 === Backtracking. Learning clause 1343:2:1:[406.1,398.2]:Top: tptpcol_7_72707(x0) -> tptpcol_5_69635(x0)
% 33.86/7.26 === Conflict found: 1150:2:1:[1128.2,52.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> genlmt(x0,c_ldscgeneralcollectormt) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1344:2:1:[1150.2,1125.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> microtheory(c_ldscgeneralcollectormt)
% 33.86/7.26 === Backtracking. Learning clause 1345:2:1:[1128.2,364.1,1247.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_spindleheadmt)
% 33.86/7.26 === Backtracking. Learning clause 1346:1:0:[1125.1,52.1]:: -> microtheory(c_ldscgeneralcollectormt)
% 33.86/7.26 === Backtracking. Learning clause 1347:2:1:[1128.2,181.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 708
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1348:2:1:[421.2,325.1]:Top: tptpcol_8_92164(x0) -> tptpcol_6_92162(x0)
% 33.86/7.26 === Backtracking. Learning clause 1349:2:1:[394.2,490.1]:Top: tptpcol_6_112641(x0) -> tptpcol_4_106497(x0)
% 33.86/7.26 === Backtracking. Learning clause 1350:2:1:[1128.2,453.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member1672_mt)
% 33.86/7.26 === Backtracking. Learning clause 1351:2:1:[1128.2,364.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member3993_mt)
% 33.86/7.26 === Backtracking. Learning clause 1352:2:1:[1128.1,329.1]:Top: genlmt(c_ethnicgroupsmt,x0) -> genlmt(c_massmediadatamt,x0)
% 33.86/7.26 === Clause set with instances from active satisfied. Growing active. New size: 836
% 33.86/7.26 === Restarting.
% 33.86/7.26 === Backtracking. Learning clause 1353:2:1:[50.2,1303.2]:Top: tptpcol_2_98304(x0),tptpcol_4_16387(x0) ->
% 33.86/7.26 === Backtracking. Learning clause 1354:2:1:[211.1,494.2]:Top: computerdataartifact(x0) -> inanimateobject_nonnatural(x0)
% 33.86/7.26 === Conflict found: 1343:2:1:[406.1,398.2]:Top: tptpcol_7_72707(x0) -> tptpcol_5_69635(x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.26 === Backtracking. Learning clause 1355:2:1:[1343.2,1305.1]:Top: tptpcol_7_72707(x0) -> tptpcol_2_65537(x0)
% 33.86/7.26 === Backtracking. Learning clause 1356:2:1:[468.2,474.1]:Top: tptpcol_14_92264(x0) -> tptpcol_12_92262(x0)
% 33.86/7.26 === Backtracking. Learning clause 1357:2:0:[1123.2,326.1]:: mtvisible(c_tptpgeo_spindleheadmt) -> mtvisible(c_worldgeographymt)
% 33.86/7.27 === Backtracking. Learning clause 1358:2:0:[462.1,464.2]:: mtvisible(c_worldgeographymt) -> geographicalregion(c_georegion_l4_x75_y75)
% 33.86/7.27 === Backtracking. Learning clause 1360:1:0:[1132.0,1359.0,1123.2,20.1]:: -> mtvisible(c_tptp_member2610_mt)
% 33.86/7.27 === Backtracking. Learning clause 1361:1:0:[1125.1,20.1]:: -> microtheory(c_tptp_member2610_mt)
% 33.86/7.27 === Backtracking. Learning clause 1363:1:0:[1132.0,1362.0,1123.2,453.1]:: -> mtvisible(c_tptp_member1672_mt)
% 33.86/7.27 === Backtracking. Learning clause 1365:1:0:[1132.0,1364.0,1123.2,419.1]:: -> mtvisible(c_tptp_member235_mt)
% 33.86/7.27 === Backtracking. Learning clause 1367:1:0:[1132.0,1366.0,1123.2,198.1]:: -> mtvisible(c_tptp_member237_mt)
% 33.86/7.27 === Backtracking. Learning clause 1368:1:0:[1125.1,198.1]:: -> microtheory(c_tptp_member237_mt)
% 33.86/7.27 === Backtracking. Learning clause 1370:1:0:[1132.0,1369.0,1123.2,350.1]:: -> mtvisible(c_tptp_member2668_mt)
% 33.86/7.27 === Backtracking. Learning clause 1371:1:0:[1125.1,350.1]:: -> microtheory(c_tptp_member2668_mt)
% 33.86/7.27 === Backtracking. Learning clause 1373:1:0:[1132.0,1372.0,1123.2,364.1]:: -> mtvisible(c_tptp_member3993_mt)
% 33.86/7.27 === Backtracking. Learning clause 1374:1:0:[1125.1,344.1]:: -> microtheory(c_tptp_member2701_mt)
% 33.86/7.27 === Backtracking. Learning clause 1375:2:0:[1123.2,34.1]:: mtvisible(c_tptp_member3205_mt) -> mtvisible(c_tptp_spindleheadmt)
% 33.86/7.27 === Backtracking. Learning clause 1376:2:0:[1123.2,254.1,1375.2]:: mtvisible(c_tptp_member3205_mt) -> mtvisible(c_cyclistsmt)
% 33.86/7.27 === Backtracking. Learning clause 1377:2:0:[1123.2,53.1]:: mtvisible(c_ethnicgroupsmt) -> mtvisible(c_ethnicgroupsvocabularymt)
% 33.86/7.27 === Backtracking. Learning clause 1378:2:0:[1123.2,367.1]:: mtvisible(c_ethnicgroupsvocabularymt) -> mtvisible(c_worldcompletedualistgeographymt)
% 33.86/7.27 === Conflict found: 1152:2:1:[1128.1,58.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> genlmt(c_machinelearningspindleheadmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.27 === Backtracking. Learning clause 1379:3:1:[1152.2,1123.2]:Top: genlmt(c_miptdatabase19681997_termsmt,x0),mtvisible(c_machinelearningspindleheadmt) -> mtvisible(x0)
% 33.86/7.27 === Conflict found: 1379:3:1:[1152.2,1123.2]:Top: genlmt(c_miptdatabase19681997_termsmt,x0),mtvisible(c_machinelearningspindleheadmt) -> mtvisible(x0) {x0 -> c_ldscgeneralcollectormt}
% 33.86/7.27 === Backtracking. Learning clause 1380:2:0:[1379.1,52.1]:: mtvisible(c_machinelearningspindleheadmt) -> mtvisible(c_ldscgeneralcollectormt)
% 33.86/7.27 === Backtracking. Learning clause 1381:2:0:[1123.2,334.1]:: mtvisible(c_worldgeographymt) -> mtvisible(c_geographymt)
% 33.86/7.27 === Backtracking. Learning clause 1382:2:0:[1123.2,369.1]:: mtvisible(c_tptpgeo_spindlecollectormt) -> mtvisible(c_tptpgeo_member8_mt)
% 33.86/7.27 === Backtracking. Learning clause 1383:1:0:[1125.1,273.1]:: -> microtheory(c_tptpgeo_member2_mt)
% 33.86/7.27 === Backtracking. Learning clause 1384:1:0:[1125.1,407.1]:: -> microtheory(c_tptpgeo_member5_mt)
% 33.86/7.27 === Backtracking. Learning clause 1385:1:0:[1125.1,140.1]:: -> microtheory(c_tptpgeo_member1_mt)
% 33.86/7.27 === Backtracking. Learning clause 1386:2:0:[1123.2,147.1]:: mtvisible(c_tptp_member3515_mt) -> mtvisible(c_tptp_spindleheadmt)
% 33.86/7.27 === Backtracking. Learning clause 1387:2:0:[1123.2,172.1]:: mtvisible(c_tptp_member2089_mt) -> mtvisible(c_tptp_spindleheadmt)
% 33.86/7.27 === Backtracking. Learning clause 1388:2:0:[1123.2,269.1]:: mtvisible(c_cycnounlearnermt) -> mtvisible(c_cycorpproductsmt)
% 33.86/7.27 === Backtracking. Learning clause 1389:2:0:[1123.2,243.1]:: mtvisible(c_tptp_member3633_mt) -> mtvisible(c_tptp_spindleheadmt)
% 33.86/7.27 === Backtracking. Learning clause 1390:2:0:[1123.2,257.1]:: mtvisible(c_keinteractionresourcetestmt) -> mtvisible(c_testvocabularymt)
% 33.86/7.27 === Conflict found: 1176:2:1:[1128.1,275.1]:Top: genlmt(c_nooescapearchitecturemt,x0) -> genlmt(c_testvocabularymt,x0) {x0 -> c_tptpgeo_member8_mt}
% 33.86/7.27 === Backtracking. Learning clause 1391:3:1:[1176.2,1123.2]:Top: genlmt(c_nooescapearchitecturemt,x0),mtvisible(c_testvocabularymt) -> mtvisible(x0)
% 33.86/7.27 === Conflict found: 1391:3:1:[1176.2,1123.2]:Top: genlmt(c_nooescapearchitecturemt,x0),mtvisible(c_testvocabularymt) -> mtvisible(x0) {x0 -> c_organizationdatamt}
% 33.86/7.27 === Backtracking. Learning clause 1392:2:0:[1391.1,66.1,1390.2]:: mtvisible(c_keinteractionresourcetestmt) -> mtvisible(c_organizationdatamt)
% 33.86/7.27 === Backtracking. Learning clause 1393:2:0:[1123.2,279.1]:: mtvisible(c_tptp_member3717_mt) -> mtvisible(c_tptp_spindleheadmt)
% 33.86/7.27 === Backtracking. Learning clause 1394:1:0:[1123.2,315.1,1373.1]:: -> mtvisible(c_tptp_spindleheadmt)
% 33.86/7.27 === Backtracking. Learning clause 1395:1:0:[1123.2,254.1,1394.1]:: -> mtvisible(c_cyclistsmt)
% 33.86/7.27 === Conflict found: 1182:2:0:[105.3,1133.1]:: mtvisible(c_tptp_member235_mt),ridgeline_topographical(c_tptpridgeline_topographical) -> {}
% 33.86/7.27
% 33.86/7.27 SZS status Unsatisfiable
% 33.86/7.27
% 33.86/7.27 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.86/7.27
% 33.86/7.27 SPASS-SCL-FOL Statistics:
% 33.86/7.27 Number of learned clauses: 256
% 33.86/7.27 Number of propagations: 23056
% 33.86/7.27 Number of decisions: 17234
% 33.86/7.27 Number of resolutions: 307
% 33.86/7.27 Number of condensations: 0
% 33.86/7.27 Number of sub resolutions: 6
% 33.86/7.27 Number of input literals (deduplicated): 891
% 33.86/7.27 Number of grows: 9
% 33.86/7.27 Number of considered ground atoms: 836
% 33.86/7.27
% 33.86/7.27 Needed: 0:00:06.72
% 33.86/7.27
%------------------------------------------------------------------------------