%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR057+2 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n031.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:19:57 PM UTC 2026
% Result : Theorem 226.35s 45.76s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : CSR057+2 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n031.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 11:40:55 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.39 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 226.35/45.75 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 226.35/45.75 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 226.35/45.75 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 226.35/45.75 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 226.35/45.75 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 226.35/45.75 Execution resolution_1 ended with status: unsatisfiable
% 226.35/45.75 Used heuristic: resolution_1
% 226.35/45.75
% 226.35/45.75 Input Clauses:
% 226.35/45.75
% 226.35/45.75 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
% 226.35/45.75 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
% 226.35/45.75 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
% 226.35/45.75 Problem Properties:
% 226.35/45.75 This is a full first-order problem without equality.
% 226.35/45.75
% 226.35/45.75 After reduction: Problem Properties:
% 226.35/45.75 This is a full first-order problem without equality.
% 226.35/45.75
% 226.35/45.75
% 226.35/45.75 Reduced Input Clauses:
% 226.35/45.76
% 226.35/45.76 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)
% 226.35/45.76
% 226.35/45.76 === Starting SPASS-SCL-FOL A Little Less Naive, considering 163 atoms initially, heuristics mode: resolution_1 ===
% 226.35/45.76
% 226.35/45.76 === Backtracking. Learning clause 1134:2:1:[31.2,194.1]:Top: tptpcol_11_22023(x0) -> tptpcol_9_22021(x0)
% 226.35/45.76 === Backtracking. Learning clause 1135:2:1:[69.2,234.1]:Top: tptpcol_4_106497(x0) -> tptpcol_2_98304(x0)
% 226.35/45.76 === Backtracking. Learning clause 1136:1:0:[171.1,83.1]:: -> microtheory(c_wamt_evalinitial_p14)
% 226.35/45.76 === Backtracking. Learning clause 1137:2:1:[110.2,176.1]:Top: tptpcol_12_18663(x0) -> tptpcol_10_18567(x0)
% 226.35/45.76 === Backtracking. Learning clause 1138:2:1:[180.2,132.1]:Top: mathematicalthing(x0) -> intangible(x0)
% 226.35/45.76 === Backtracking. Learning clause 1139:2:1:[146.2,153.1]:Top: tptpcol_2_2(x0),tptpcol_1_65536(x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1140:2:1:[151.2,289.1]:Top: fixedordercollection(x0),individual(x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1141:2:1:[183.2,192.1]:Top: tptpcol_15_93775(x0) -> tptpcol_13_93766(x0)
% 226.35/45.76 === Backtracking. Learning clause 1142:2:1:[190.2,231.1]:Top: tptpcol_14_22072(x0) -> tptpcol_12_22055(x0)
% 226.35/45.76 === Backtracking. Learning clause 1143:1:0:[294.1,246.1]:: -> orderingpredicate(c_geographicalsubregions)
% 226.35/45.76 === Backtracking. Learning clause 1144:2:1:[1128.2,20.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2610_mt)
% 226.35/45.76 === Backtracking. Learning clause 1145:2:1:[1128.2,198.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member237_mt)
% 226.35/45.76 === Backtracking. Learning clause 1146:2:1:[1128.2,115.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_calendarsmt)
% 226.35/45.76 === Backtracking. Learning clause 1147:2:1:[1128.2,125.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_hpkbvocabmt)
% 226.35/45.76 === Backtracking. Learning clause 1148:2:1:[1128.2,34.1]:Top: genlmt(x0,c_tptp_member3205_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1149:2:1:[1128.2,35.1]:Top: genlmt(x0,c_peopledatamt) -> genlmt(x0,c_unitedstatessociallifemt)
% 226.35/45.76 === Backtracking. Learning clause 1150:2:1:[1128.2,52.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> genlmt(x0,c_ldscgeneralcollectormt)
% 226.35/45.76 === Backtracking. Learning clause 1151:2:1:[1128.2,53.1]:Top: genlmt(x0,c_ethnicgroupsmt) -> genlmt(x0,c_ethnicgroupsvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1152:2:1:[1128.1,58.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> genlmt(c_machinelearningspindleheadmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1153:2:1:[1128.2,177.1]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> genlmt(x0,c_cycnounlearnermt)
% 226.35/45.76 === Backtracking. Learning clause 1154:2:1:[1128.2,59.1]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt) -> genlmt(x0,c_currentworlddatacollectormt_nonhomocentric)
% 226.35/45.76 === Backtracking. Learning clause 1155:2:1:[1128.1,63.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member7_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1156:2:1:[1128.2,66.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_organizationdatamt)
% 226.35/45.76 === Backtracking. Learning clause 1157:2:1:[1128.2,88.1]:Top: genlmt(x0,c_patterndetectormt) -> genlmt(x0,c_basekb)
% 226.35/45.76 === Backtracking. Learning clause 1158:2:1:[1128.1,206.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_universalvocabularymt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1159:2:1:[1128.2,92.1]:Top: genlmt(x0,c_universalvocabularymt) -> genlmt(x0,c_corecyclmt)
% 226.35/45.76 === Backtracking. Learning clause 1160:2:1:[1128.1,93.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2831_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1161:2:1:[1128.1,133.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3393_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1162:2:1:[1128.1,136.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_generictemporalmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1163:2:1:[1128.1,137.1]:Top: genlmt(c_worldgeographymt,x0) -> genlmt(c_worldgeographydualistmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1164:2:1:[1128.2,137.1]:Top: genlmt(x0,c_worldgeographydualistmt) -> genlmt(x0,c_worldgeographymt)
% 226.35/45.76 === Backtracking. Learning clause 1165:2:1:[1128.2,273.1]:Top: genlmt(x0,c_tptpgeo_spindlecollectormt) -> genlmt(x0,c_tptpgeo_member2_mt)
% 226.35/45.76 === Backtracking. Learning clause 1166:2:1:[1128.1,147.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3515_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1167:2:1:[1128.1,154.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_geographymt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1168:2:1:[1128.1,162.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_calendarsvocabularymt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1169:2:1:[1128.1,172.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2089_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1170:2:1:[1128.2,269.1]:Top: genlmt(x0,c_cycnounlearnermt) -> genlmt(x0,c_cycorpproductsmt)
% 226.35/45.76 === Backtracking. Learning clause 1171:2:1:[1128.1,212.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member3_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1172:2:1:[1128.1,214.1]:Top: genlmt(c_generictemporalmt,x0) -> genlmt(c_timehasnoendmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1173:2:1:[1128.1,243.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3633_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1174:2:1:[1128.1,248.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member974_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1176:2:1:[1128.1,275.1]:Top: genlmt(c_nooescapearchitecturemt,x0) -> genlmt(c_testvocabularymt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1177:2:1:[1128.1,272.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_humansociallifemt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1178:2:1:[1128.1,274.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_knowledgefragmentd3mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1179:2:1:[1128.1,279.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3717_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1180:1:1:[128.2,1133.1]:Top: geographicalsubregions(c_georegion_l4_x75_y75,x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1181:2:1:[1128.1,232.1]:Top: genlmt(c_massmediadatamt,x0) -> genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),x0)
% 226.35/45.76 === Backtracking. Learning clause 1182:2:1:[1128.2,232.1]:Top: genlmt(x0,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) -> genlmt(x0,c_massmediadatamt)
% 226.35/45.76 === 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)
% 226.35/45.76 === 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)
% 226.35/45.76 === 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)
% 226.35/45.76 === 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)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 227
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1187:1:0:[1127.1,1.1]:: -> microtheory(c_tptpgeo_member8_mt)
% 226.35/45.76 === Backtracking. Learning clause 1188:2:1:[1128.2,350.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2668_mt)
% 226.35/45.76 === Backtracking. Learning clause 1189:2:1:[1128.2,364.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member3993_mt)
% 226.35/45.76 === Backtracking. Learning clause 1190:2:1:[1128.2,344.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2701_mt)
% 226.35/45.76 === Backtracking. Learning clause 1191:2:1:[1128.2,310.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_keinteractionresourcetestmt)
% 226.35/45.76 === 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)
% 226.35/45.76 === Backtracking. Learning clause 1193:2:1:[1128.2,154.1]:Top: genlmt(x0,c_geographymt) -> genlmt(x0,c_basekb)
% 226.35/45.76 === Backtracking. Learning clause 1194:2:1:[1128.2,334.1,1193.1]:Top: genlmt(x0,c_worldgeographymt) -> genlmt(x0,c_basekb)
% 226.35/45.76 === Backtracking. Learning clause 1195:2:1:[1128.2,326.1,1194.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_basekb)
% 226.35/45.76 === Backtracking. Learning clause 1196:2:1:[1128.2,214.1]:Top: genlmt(x0,c_timehasnoendmt) -> genlmt(x0,c_generictemporalmt)
% 226.35/45.76 === Backtracking. Learning clause 1197:2:1:[1128.1,333.1]:Top: genlmt(c_humansociallifemt,x0) -> genlmt(c_reasoningaboutpossibleantecedentsmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1198:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1199: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)
% 226.35/45.76 === Backtracking. Learning clause 1200: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)
% 226.35/45.76 === Backtracking. Learning clause 1201: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)
% 226.35/45.76 === Backtracking. Learning clause 1202: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)
% 226.35/45.76 === Backtracking. Learning clause 1203: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)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 316
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1204:2:1:[262.2,375.1,240.2]:Top: tptpcol_8_26629(x0) -> tptpcol_5_24579(x0)
% 226.35/45.76 === Backtracking. Learning clause 1205:2:1:[278.2,411.1]:Top: tptpcol_10_26886(x0) -> tptpcol_8_26629(x0)
% 226.35/45.76 === Backtracking. Learning clause 1206:2:1:[360.2,343.1]:Top: tptpcol_12_109157(x0) -> tptpcol_10_109061(x0)
% 226.35/45.76 === Backtracking. Learning clause 1207:2:1:[380.1,373.2]:Top: tptpcol_11_93764(x0) -> tptpcol_9_93699(x0)
% 226.35/45.76 === Backtracking. Learning clause 1208:1:0:[1125.1,1.1]:: -> microtheory(c_tptpgeo_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1209:1:0:[1125.1,326.1]:: -> microtheory(c_worldgeographymt)
% 226.35/45.76 === Backtracking. Learning clause 1210:2:1:[1128.2,326.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_worldgeographymt)
% 226.35/45.76 === Backtracking. Learning clause 1211:1:0:[1127.1,115.1]:: -> microtheory(c_cyclistsmt)
% 226.35/45.76 === Backtracking. Learning clause 1212:1:0:[1125.1,115.1]:: -> microtheory(c_calendarsmt)
% 226.35/45.76 === Backtracking. Learning clause 1213:1:0:[1127.1,34.1]:: -> microtheory(c_tptp_member3205_mt)
% 226.35/45.76 === 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}
% 226.35/45.76 === Backtracking. Learning clause 1214:2:1:[1148.2,1125.1]:Top: genlmt(x0,c_tptp_member3205_mt) -> microtheory(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1215:1:0:[1125.1,34.1]:: -> microtheory(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1216:2:1:[1128.2,254.1,1148.2]:Top: genlmt(x0,c_tptp_member3205_mt) -> genlmt(x0,c_cyclistsmt)
% 226.35/45.76 === Backtracking. Learning clause 1217:2:1:[1128.2,87.1,1125.1]:Top: genlmt(x0,c_ldscgeneralcollectormt) -> microtheory(c_ldscdemonstrationspindleheadmt)
% 226.35/45.76 === Conflict found: 1217:2:1:[1128.2,87.1,1125.1]:Top: genlmt(x0,c_ldscgeneralcollectormt) -> microtheory(c_ldscdemonstrationspindleheadmt) {x0 -> c_miptdatabase19681997_termsmt}
% 226.35/45.76 === Backtracking. Learning clause 1218:1:0:[1217.1,52.1]:: -> microtheory(c_ldscdemonstrationspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1219:2:1:[1128.2,87.1]:Top: genlmt(x0,c_ldscgeneralcollectormt) -> genlmt(x0,c_ldscdemonstrationspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1220:1:0:[1125.1,53.1]:: -> microtheory(c_ethnicgroupsvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1221:1:0:[1125.1,177.1]:: -> microtheory(c_cycnounlearnermt)
% 226.35/45.76 === Backtracking. Learning clause 1222:1:0:[1125.1,92.1]:: -> microtheory(c_corecyclmt)
% 226.35/45.76 === Backtracking. Learning clause 1223:2:1:[1128.2,93.1]:Top: genlmt(x0,c_tptp_member2831_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1224:2:1:[1128.2,378.1,1125.1]:Top: genlmt(x0,c_calendarsmt) -> microtheory(c_calendarsvocabularymt)
% 226.35/45.76 === Conflict found: 1224:2:1:[1128.2,378.1,1125.1]:Top: genlmt(x0,c_calendarsmt) -> microtheory(c_calendarsvocabularymt) {x0 -> c_cyclistsmt}
% 226.35/45.76 === Backtracking. Learning clause 1225:1:0:[1224.1,115.1]:: -> microtheory(c_calendarsvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1226:2:1:[1128.2,334.1]:Top: genlmt(x0,c_worldgeographymt) -> genlmt(x0,c_geographymt)
% 226.35/45.76 === Conflict found: 1162:2:1:[1128.1,136.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_generictemporalmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1227:2:1:[1162.2,1127.1]:Top: genlmt(c_basekb,x0) -> microtheory(c_generictemporalmt)
% 226.35/45.76 === Backtracking. Learning clause 1228:1:0:[1127.1,136.1]:: -> microtheory(c_generictemporalmt)
% 226.35/45.76 === Conflict found: 1192:3:2:[1128.2,1167.2,334.1,1128.2]:TopTop: genlmt(c_basekb,x0),genlmt(x1,c_worldgeographymt) -> genlmt(x1,x0) {x0 -> c_tptpgeo_member8_mt, x1 -> c_worldgeographydualistmt}
% 226.35/45.76 === Backtracking. Learning clause 1229:2:1:[1192.2,137.1,1127.1]:Top: genlmt(c_basekb,x0) -> microtheory(c_worldgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1230:1:0:[1127.1,137.1]:: -> microtheory(c_worldgeographydualistmt)
% 226.35/45.76 === Conflict found: 1192:3:2:[1128.2,1167.2,334.1,1128.2]:TopTop: genlmt(c_basekb,x0),genlmt(x1,c_worldgeographymt) -> genlmt(x1,x0) {x0 -> c_tptpgeo_member8_mt, x1 -> c_worldgeographydualistmt}
% 226.35/45.76 === Backtracking. Learning clause 1231:2:1:[1192.2,137.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_worldgeographydualistmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1232:1:0:[1127.1,369.1]:: -> microtheory(c_tptpgeo_spindlecollectormt)
% 226.35/45.76 === 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}
% 226.35/45.76 === Backtracking. Learning clause 1233:2:1:[1166.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3515_mt)
% 226.35/45.76 === Backtracking. Learning clause 1234:2:1:[1128.1,254.1,1233.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3515_mt)
% 226.35/45.76 === Conflict found: 1234:2:1:[1128.1,254.1,1233.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3515_mt) {x0 -> c_calendarsmt}
% 226.35/45.76 === Backtracking. Learning clause 1235:1:0:[1234.1,115.1]:: -> microtheory(c_tptp_member3515_mt)
% 226.35/45.76 === Backtracking. Learning clause 1236:2:1:[1128.2,147.1]:Top: genlmt(x0,c_tptp_member3515_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1237:2:1:[1128.2,1167.2,334.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_worldgeographymt,x0)
% 226.35/45.76 === 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}
% 226.35/45.76 === Backtracking. Learning clause 1238:2:1:[1169.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member2089_mt)
% 226.35/45.76 === Backtracking. Learning clause 1239:2:1:[1128.1,254.1,1238.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2089_mt)
% 226.35/45.76 === Conflict found: 1239:2:1:[1128.1,254.1,1238.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2089_mt) {x0 -> c_calendarsmt}
% 226.35/45.76 === Backtracking. Learning clause 1240:1:0:[1239.1,115.1]:: -> microtheory(c_tptp_member2089_mt)
% 226.35/45.76 === Backtracking. Learning clause 1241:2:1:[1128.2,172.1]:Top: genlmt(x0,c_tptp_member2089_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1242:1:0:[1125.1,269.1]:: -> microtheory(c_cycorpproductsmt)
% 226.35/45.76 === Conflict found: 1171:2:1:[1128.1,212.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member3_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1243:2:1:[1171.2,1127.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> microtheory(c_tptpgeo_member3_mt)
% 226.35/45.76 === Conflict found: 1243:2:1:[1171.2,1127.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> microtheory(c_tptpgeo_member3_mt) {x0 -> c_worldgeographymt}
% 226.35/45.76 === Backtracking. Learning clause 1244:1:0:[1243.1,326.1]:: -> microtheory(c_tptpgeo_member3_mt)
% 226.35/45.76 === Backtracking. Learning clause 1245:1:0:[1127.1,329.1]:: -> microtheory(c_massmediadatamt)
% 226.35/45.76 === 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}
% 226.35/45.76 === Backtracking. Learning clause 1246:2:1:[1173.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3633_mt)
% 226.35/45.76 === Backtracking. Learning clause 1247:2:1:[1128.1,254.1,1246.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3633_mt)
% 226.35/45.76 === Conflict found: 1247:2:1:[1128.1,254.1,1246.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3633_mt) {x0 -> c_calendarsmt}
% 226.35/45.76 === Backtracking. Learning clause 1248:1:0:[1247.1,115.1]:: -> microtheory(c_tptp_member3633_mt)
% 226.35/45.76 === Conflict found: 1177:2:1:[1128.1,272.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_humansociallifemt,x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1249:2:1:[1177.2,1127.1]:Top: genlmt(c_basekb,x0) -> microtheory(c_humansociallifemt)
% 226.35/45.76 === Backtracking. Learning clause 1250:1:0:[1127.1,272.1]:: -> microtheory(c_humansociallifemt)
% 226.35/45.76 === Conflict found: 1178:2:1:[1128.1,274.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_knowledgefragmentd3mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1251:2:1:[1178.2,1127.1]:Top: genlmt(c_basekb,x0) -> microtheory(c_knowledgefragmentd3mt)
% 226.35/45.76 === Backtracking. Learning clause 1252:1:0:[1127.1,274.1]:: -> microtheory(c_knowledgefragmentd3mt)
% 226.35/45.76 === 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}
% 226.35/45.76 === Backtracking. Learning clause 1253:2:1:[1179.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3717_mt)
% 226.35/45.76 === Backtracking. Learning clause 1254:2:1:[1128.1,254.1,1253.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3717_mt)
% 226.35/45.76 === Conflict found: 1254:2:1:[1128.1,254.1,1253.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3717_mt) {x0 -> c_calendarsmt}
% 226.35/45.76 === Backtracking. Learning clause 1255:1:0:[1254.1,115.1]:: -> microtheory(c_tptp_member3717_mt)
% 226.35/45.76 === Backtracking. Learning clause 1256:2:1:[1128.2,315.1]:Top: genlmt(x0,c_tptp_member3993_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Conflict found: 1197:2:1:[1128.1,333.1]:Top: genlmt(c_humansociallifemt,x0) -> genlmt(c_reasoningaboutpossibleantecedentsmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1257:2:1:[1197.2,1127.1,1177.2]:Top: genlmt(c_basekb,x0) -> microtheory(c_reasoningaboutpossibleantecedentsmt)
% 226.35/45.76 === Conflict found: 1197:2:1:[1128.1,333.1]:Top: genlmt(c_humansociallifemt,x0) -> genlmt(c_reasoningaboutpossibleantecedentsmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1258:2:1:[1197.2,1127.1]:Top: genlmt(c_humansociallifemt,x0) -> microtheory(c_reasoningaboutpossibleantecedentsmt)
% 226.35/45.76 === Conflict found: 1258:2:1:[1197.2,1127.1]:Top: genlmt(c_humansociallifemt,x0) -> microtheory(c_reasoningaboutpossibleantecedentsmt) {x0 -> c_basekb}
% 226.35/45.76 === Backtracking. Learning clause 1259:1:0:[1258.1,272.1]:: -> microtheory(c_reasoningaboutpossibleantecedentsmt)
% 226.35/45.76 === Backtracking. Learning clause 1260:2:1:[1128.2,333.1]:Top: genlmt(x0,c_reasoningaboutpossibleantecedentsmt) -> genlmt(x0,c_humansociallifemt)
% 226.35/45.76 === Backtracking. Learning clause 1261:2:1:[1128.2,62.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1262: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)
% 226.35/45.76 === Backtracking. Learning clause 1263: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)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 382
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1264:2:1:[437.2,312.1,225.2]:Top: tptpcol_5_69635(x0) -> tptpcol_2_65537(x0)
% 226.35/45.76 === Backtracking. Learning clause 1265:2:1:[357.2,362.1]:Top: tptpcol_8_117763(x0) -> tptpcol_6_116738(x0)
% 226.35/45.76 === Backtracking. Learning clause 1266:2:1:[394.2,490.1]:Top: tptpcol_6_112641(x0) -> tptpcol_4_106497(x0)
% 226.35/45.76 === Backtracking. Learning clause 1267:2:1:[396.2,450.1]:Top: tptpcol_12_72775(x0) -> tptpcol_10_72710(x0)
% 226.35/45.76 === Backtracking. Learning clause 1268:2:1:[406.1,398.2,1264.1]:Top: tptpcol_7_72707(x0) -> tptpcol_2_65537(x0)
% 226.35/45.76 === Conflict found: 1195:2:1:[1128.2,326.1,1194.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_basekb) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1269:1:0:[1195.2,1125.1,1.1]:: -> microtheory(c_basekb)
% 226.35/45.76 === Conflict found: 1226:2:1:[1128.2,334.1]:Top: genlmt(x0,c_worldgeographymt) -> genlmt(x0,c_geographymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1270:1:0:[1226.2,1125.1,1210.2,1.1]:: -> microtheory(c_geographymt)
% 226.35/45.76 === Conflict found: 1189:2:1:[1128.2,364.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member3993_mt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1271:2:1:[1189.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member3993_mt)
% 226.35/45.76 === Backtracking. Learning clause 1272:1:0:[1125.1,364.1]:: -> microtheory(c_tptp_member3993_mt)
% 226.35/45.76 === Backtracking. Learning clause 1273:2:1:[1128.2,254.1]:Top: genlmt(x0,c_tptp_spindleheadmt) -> genlmt(x0,c_cyclistsmt)
% 226.35/45.76 === Conflict found: 1256:2:1:[1128.2,315.1]:Top: genlmt(x0,c_tptp_member3993_mt) -> genlmt(x0,c_tptp_spindleheadmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1274:2:1:[1256.1,1189.2,1273.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_cyclistsmt)
% 226.35/45.76 === Conflict found: 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1275:2:1:[1175.2,1125.1,1191.2,1274.2]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_testvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1276:2:1:[1128.1,254.1]:Top: genlmt(c_cyclistsmt,x0) -> genlmt(c_tptp_spindleheadmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1277:2:1:[1128.2,414.1,1125.1,1149.2]:Top: genlmt(x0,c_peopledatamt) -> microtheory(c_gregoriancalendarmt)
% 226.35/45.76 === Backtracking. Learning clause 1278:1:0:[1125.1,414.1]:: -> microtheory(c_gregoriancalendarmt)
% 226.35/45.76 === Backtracking. Learning clause 1279:2:1:[1128.2,367.1,1125.1,1151.2]:Top: genlmt(x0,c_ethnicgroupsmt) -> microtheory(c_worldcompletedualistgeographymt)
% 226.35/45.76 === Backtracking. Learning clause 1280:2:1:[1128.2,367.1,1125.1]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> microtheory(c_worldcompletedualistgeographymt)
% 226.35/45.76 === Conflict found: 1280:2:1:[1128.2,367.1,1125.1]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> microtheory(c_worldcompletedualistgeographymt) {x0 -> c_ethnicgroupsmt}
% 226.35/45.76 === Backtracking. Learning clause 1281:1:0:[1280.1,53.1]:: -> microtheory(c_worldcompletedualistgeographymt)
% 226.35/45.76 === Conflict found: 1198:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1282:2:1:[1198.2,1125.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> microtheory(c_unitedstatesgeographydualistmt)
% 226.35/45.76 === Conflict found: 1282:2:1:[1198.2,1125.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> microtheory(c_unitedstatesgeographydualistmt) {x0 -> c_ethnicgroupsvocabularymt}
% 226.35/45.76 === Backtracking. Learning clause 1283:1:0:[1282.1,367.1]:: -> microtheory(c_unitedstatesgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1284:2:1:[1128.2,58.1]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> genlmt(x0,c_miptdatabase19681997_termsmt)
% 226.35/45.76 === Backtracking. Learning clause 1285:1:0:[1127.1,88.1]:: -> microtheory(c_patterndetectormt)
% 226.35/45.76 === Backtracking. Learning clause 1286:1:0:[1125.1,455.1]:: -> microtheory(c_universalvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1287:2:1:[1128.2,358.1]:Top: genlmt(x0,c_corecyclmt) -> genlmt(x0,c_logicaltruthmt)
% 226.35/45.76 === Backtracking. Learning clause 1288:2:1:[1128.2,378.1]:Top: genlmt(x0,c_calendarsmt) -> genlmt(x0,c_calendarsvocabularymt)
% 226.35/45.76 === 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}
% 226.35/45.76 === Backtracking. Learning clause 1289:2:1:[1161.2,1127.1,1276.2]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3393_mt)
% 226.35/45.76 === Conflict found: 1289:2:1:[1161.2,1127.1,1276.2]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3393_mt) {x0 -> c_calendarsmt}
% 226.35/45.76 === Backtracking. Learning clause 1290:1:0:[1289.1,115.1]:: -> microtheory(c_tptp_member3393_mt)
% 226.35/45.76 === Backtracking. Learning clause 1291:1:0:[1127.1,214.1]:: -> microtheory(c_timehasnoendmt)
% 226.35/45.76 === Backtracking. Learning clause 1292:1:0:[1125.1,257.1]:: -> microtheory(c_testvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1293:2:1:[1128.1,315.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3993_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1294:2:1:[1128.2,454.1,1198.2]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_worldgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1295:2:1:[1128.2,367.1,1294.1]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> genlmt(x0,c_worldgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1296:2:1:[1128.1,384.1,1127.1]:Top: genlmt(c_peopledatamt,x0) -> microtheory(c_unitedstatesgeographypeoplemt)
% 226.35/45.76 === Conflict found: 1296:2:1:[1128.1,384.1,1127.1]:Top: genlmt(c_peopledatamt,x0) -> microtheory(c_unitedstatesgeographypeoplemt) {x0 -> c_unitedstatessociallifemt}
% 226.35/45.76 === Backtracking. Learning clause 1297:1:0:[1296.1,35.1]:: -> microtheory(c_unitedstatesgeographypeoplemt)
% 226.35/45.76 === Backtracking. Learning clause 1298:2:1:[1128.1,384.1]:Top: genlmt(c_peopledatamt,x0) -> genlmt(c_unitedstatesgeographypeoplemt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1299:1:0:[1127.1,446.1]:: -> microtheory(c_tptp_member2356_mt)
% 226.35/45.76 === Backtracking. Learning clause 1300:2:1:[1128.1,446.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2356_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1301:2:1:[1128.2,486.1]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))
% 226.35/45.76 === Backtracking. Learning clause 1302: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)
% 226.35/45.76 === Backtracking. Learning clause 1303: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)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 447
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1304:2:1:[211.1,494.2]:Top: computerdataartifact(x0) -> inanimateobject_nonnatural(x0)
% 226.35/45.76 === Backtracking. Learning clause 1305:2:1:[386.1,223.2,1139.1,119.2]:Top: tptpcol_1_65536(x0),tptpcol_5_24579(x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1306:2:1:[236.2,488.2]:Top: tptpcol_4_114689(x0),tptpcol_3_98305(x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1307:2:1:[382.2,320.1,156.2]:Top: microtheory(x0) -> partiallyintangibleindividual(x0)
% 226.35/45.76 === Backtracking. Learning clause 1308:2:1:[477.1,418.2]:Top: tptpcol_6_92162(x0) -> tptpcol_4_90113(x0)
% 226.35/45.76 === Backtracking. Learning clause 1309:2:1:[468.2,474.1]:Top: tptpcol_14_92264(x0) -> tptpcol_12_92262(x0)
% 226.35/45.76 === Backtracking. Learning clause 1310:1:0:[1127.1,20.1]:: -> microtheory(c_tptp_spindlecollectormt)
% 226.35/45.76 === Backtracking. Learning clause 1311:2:1:[1128.2,448.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member698_mt)
% 226.35/45.76 === Backtracking. Learning clause 1312:1:0:[1127.1,35.1]:: -> microtheory(c_peopledatamt)
% 226.35/45.76 === Conflict found: 1149:2:1:[1128.2,35.1]:Top: genlmt(x0,c_peopledatamt) -> genlmt(x0,c_unitedstatessociallifemt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1313:2:1:[1149.2,1125.1]:Top: genlmt(x0,c_peopledatamt) -> microtheory(c_unitedstatessociallifemt)
% 226.35/45.76 === Backtracking. Learning clause 1314:1:0:[1125.1,35.1]:: -> microtheory(c_unitedstatessociallifemt)
% 226.35/45.76 === Backtracking. Learning clause 1315:2:1:[1128.2,414.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> genlmt(x0,c_gregoriancalendarmt)
% 226.35/45.76 === Backtracking. Learning clause 1316:1:0:[1127.1,52.1]:: -> microtheory(c_miptdatabase19681997_termsmt)
% 226.35/45.76 === Conflict found: 1155:2:1:[1128.1,63.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member7_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1317:2:1:[1155.2,1127.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> microtheory(c_tptpgeo_member7_mt)
% 226.35/45.76 === Conflict found: 1317:2:1:[1155.2,1127.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> microtheory(c_tptpgeo_member7_mt) {x0 -> c_worldgeographymt}
% 226.35/45.76 === Backtracking. Learning clause 1318:1:0:[1317.1,326.1]:: -> microtheory(c_tptpgeo_member7_mt)
% 226.35/45.76 === Backtracking. Learning clause 1319:1:0:[1125.1,66.1]:: -> microtheory(c_organizationdatamt)
% 226.35/45.76 === Conflict found: 1192:3:2:[1128.2,1167.2,334.1,1128.2]:TopTop: genlmt(c_basekb,x0),genlmt(x1,c_worldgeographymt) -> genlmt(x1,x0) {x0 -> c_universalvocabularymt, x1 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1320:2:1:[1192.1,455.1,1210.2]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_universalvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1321:2:1:[1128.1,329.1]:Top: genlmt(c_ethnicgroupsmt,x0) -> genlmt(c_massmediadatamt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1322:2:1:[1128.2,329.1]:Top: genlmt(x0,c_massmediadatamt) -> genlmt(x0,c_ethnicgroupsmt)
% 226.35/45.76 === Backtracking. Learning clause 1323:1:0:[1127.1,248.1]:: -> microtheory(c_tptp_member974_mt)
% 226.35/45.76 === Backtracking. Learning clause 1324:2:1:[1128.2,275.1,1175.2,1191.2]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_nooescapearchitecturemt)
% 226.35/45.76 === Backtracking. Learning clause 1325:2:1:[1128.2,454.1]:Top: genlmt(x0,c_unitedstatesgeographydualistmt) -> genlmt(x0,c_worldgeographydualistmt)
% 226.35/45.76 === Conflict found: 1182:2:1:[1128.2,232.1]:Top: genlmt(x0,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) -> genlmt(x0,c_massmediadatamt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1326:2:1:[1182.1,1301.2,1322.1,1156.2,1324.2]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_ethnicgroupsmt)
% 226.35/45.76 === Backtracking. Learning clause 1327:2:1:[1128.2,367.1]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> genlmt(x0,c_worldcompletedualistgeographymt)
% 226.35/45.76 === Backtracking. Learning clause 1328: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)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 513
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1329:2:1:[386.1,286.2,1139.1,349.2]:Top: tptpcol_4_16387(x0),tptpcol_2_65537(x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1330:2:1:[386.1,286.2,1139.1,50.2]:Top: tptpcol_4_16387(x0),tptpcol_2_98304(x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1331:2:1:[386.1,286.2,1139.1]:Top: tptpcol_4_16387(x0),tptpcol_1_65536(x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1332:2:1:[386.1,286.2]:Top: tptpcol_4_16387(x0) -> tptpcol_2_2(x0)
% 226.35/45.76 === Backtracking. Learning clause 1333:2:1:[262.2,375.1]:Top: tptpcol_7_26628(x0) -> tptpcol_5_24579(x0)
% 226.35/45.76 === Backtracking. Learning clause 1334:2:1:[437.2,312.1]:Top: tptpcol_4_65539(x0) -> tptpcol_2_65537(x0)
% 226.35/45.76 === Backtracking. Learning clause 1335:2:1:[421.2,325.1]:Top: tptpcol_8_92164(x0) -> tptpcol_6_92162(x0)
% 226.35/45.76 === Backtracking. Learning clause 1336:2:1:[484.1,354.2]:Top: tptpcol_8_18438(x0) -> tptpcol_6_18436(x0)
% 226.35/45.76 === Backtracking. Learning clause 1337:2:1:[432.2,481.1]:Top: tptpcol_16_26926(x0) -> tptpcol_14_26921(x0)
% 226.35/45.76 === Conflict found: 1324:2:1:[1128.2,275.1,1175.2,1191.2]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_nooescapearchitecturemt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1338:2:1:[1324.2,1125.1,1274.2]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_nooescapearchitecturemt)
% 226.35/45.76 === Conflict found: 1324:2:1:[1128.2,275.1,1175.2,1191.2]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_nooescapearchitecturemt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1339:2:1:[1324.2,1125.1]:Top: genlmt(x0,c_cyclistsmt) -> microtheory(c_nooescapearchitecturemt)
% 226.35/45.76 === Backtracking. Learning clause 1340:1:0:[1125.1,310.1]:: -> microtheory(c_keinteractionresourcetestmt)
% 226.35/45.76 === Conflict found: 1339:2:1:[1324.2,1125.1]:Top: genlmt(x0,c_cyclistsmt) -> microtheory(c_nooescapearchitecturemt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1341:1:0:[1339.1,254.1]:: -> microtheory(c_nooescapearchitecturemt)
% 226.35/45.76 === Backtracking. Learning clause 1342:2:1:[1128.2,453.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member1672_mt)
% 226.35/45.76 === Backtracking. Learning clause 1343:2:1:[1128.2,419.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member235_mt)
% 226.35/45.76 === Conflict found: 1152:2:1:[1128.1,58.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> genlmt(c_machinelearningspindleheadmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1344:2:1:[1152.2,1127.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> microtheory(c_machinelearningspindleheadmt)
% 226.35/45.76 === Conflict found: 1344:2:1:[1152.2,1127.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> microtheory(c_machinelearningspindleheadmt) {x0 -> c_ldscgeneralcollectormt}
% 226.35/45.76 === Backtracking. Learning clause 1345:1:0:[1344.1,52.1]:: -> microtheory(c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1346:2:1:[1128.1,332.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_cycorpproductsmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1347:2:1:[1128.2,384.1]:Top: genlmt(x0,c_unitedstatesgeographypeoplemt) -> genlmt(x0,c_peopledatamt)
% 226.35/45.76 === Backtracking. Learning clause 1348:2:1:[1128.1,469.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_gregoriancalendarmt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1349:2:2:[427.2,271.1]:TopTop: tptptypes_9_824(x0,x1) -> tptptypes_7_819(x0,x1)
% 226.35/45.76 === Backtracking. Learning clause 1350: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)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 577
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1351:1:0:[205.1,475.1]:: -> fixedordercollection(c_tptpcol_16_62187)
% 226.35/45.76 === Backtracking. Learning clause 1352:2:1:[341.2,459.1]:Top: tptpcol_7_108547(x0) -> tptpcol_5_106498(x0)
% 226.35/45.76 === Backtracking. Learning clause 1353:2:1:[406.1,398.2]:Top: tptpcol_7_72707(x0) -> tptpcol_5_69635(x0)
% 226.35/45.76 === Backtracking. Learning clause 1354:1:0:[1125.1,52.1]:: -> microtheory(c_ldscgeneralcollectormt)
% 226.35/45.76 === 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}
% 226.35/45.76 === Backtracking. Learning clause 1355:2:1:[1160.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member2831_mt)
% 226.35/45.76 === Conflict found: 1355:2:1:[1160.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member2831_mt) {x0 -> c_cyclistsmt}
% 226.35/45.76 === Backtracking. Learning clause 1356:1:0:[1355.1,254.1]:: -> microtheory(c_tptp_member2831_mt)
% 226.35/45.76 === Backtracking. Learning clause 1357:2:1:[1128.2,248.1]:Top: genlmt(x0,c_tptp_member974_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1358:2:1:[1128.2,275.1,1175.2]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_nooescapearchitecturemt)
% 226.35/45.76 === Backtracking. Learning clause 1359:2:1:[1128.2,279.1]:Top: genlmt(x0,c_tptp_member3717_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1360:2:1:[1128.2,446.1]:Top: genlmt(x0,c_tptp_member2356_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 643
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1361:2:0:[462.1,464.2]:: mtvisible(c_worldgeographymt) -> geographicalregion(c_georegion_l4_x75_y75)
% 226.35/45.76 === Backtracking. Learning clause 1362:1:0:[1127.1,479.1]:: -> microtheory(c_tptp_member2862_mt)
% 226.35/45.76 === Conflict found: 1182:2:1:[1128.2,232.1]:Top: genlmt(x0,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) -> genlmt(x0,c_massmediadatamt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1363:2:1:[1182.1,1301.2,1322.1,1156.2]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_ethnicgroupsmt)
% 226.35/45.76 === Backtracking. Learning clause 1364:2:1:[1128.2,275.1]:Top: genlmt(x0,c_testvocabularymt) -> genlmt(x0,c_nooescapearchitecturemt)
% 226.35/45.76 === Backtracking. Learning clause 1365:2:1:[566.1,391.2]:Top: shavingrazor_manual(x0) -> tptpcol_5_24579(f_relationexistsallfn(x0,c_tptp_8_271,c_tptpcol_16_25972,c_shavingrazor_manual))
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 707
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1366:1:0:[1127.1,53.1]:: -> microtheory(c_ethnicgroupsmt)
% 226.35/45.76 === Backtracking. Learning clause 1367:2:1:[1128.2,133.1]:Top: genlmt(x0,c_tptp_member3393_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1368:2:1:[1128.2,243.1]:Top: genlmt(x0,c_tptp_member3633_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1369:2:1:[1128.2,479.1]:Top: genlmt(x0,c_tptp_member2862_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 836
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1370:2:1:[386.1,223.2,1139.1]:Top: tptpcol_4_24578(x0),tptpcol_1_65536(x0) ->
% 226.35/45.76 === Backtracking. Learning clause 1371:2:1:[457.2,336.1]:Top: tptpcol_7_21508(x0) -> tptpcol_5_20483(x0)
% 226.35/45.76 === Backtracking. Learning clause 1372:2:1:[371.1,1207.2]:Top: tptpcol_11_93764(x0) -> tptpcol_8_93698(x0)
% 226.35/45.76 === Conflict found: 1154:2:1:[1128.2,59.1]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt) -> genlmt(x0,c_currentworlddatacollectormt_nonhomocentric) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1373:3:1:[1154.2,1123.2]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt),mtvisible(x0) -> mtvisible(c_currentworlddatacollectormt_nonhomocentric)
% 226.35/45.76 === Conflict found: 1210:2:1:[1128.2,326.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_worldgeographymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1375:1:0:[1132.0,1374.0,1210.2,1123.2,1.1]:: -> mtvisible(c_worldgeographymt)
% 226.35/45.76 === Conflict found: 1315:2:1:[1128.2,414.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> genlmt(x0,c_gregoriancalendarmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1376:3:1:[1315.2,1123.2,1149.2]:Top: mtvisible(x0),genlmt(x0,c_peopledatamt) -> mtvisible(c_gregoriancalendarmt)
% 226.35/45.76 === Conflict found: 1315:2:1:[1128.2,414.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> genlmt(x0,c_gregoriancalendarmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1377:3:1:[1315.2,1123.2]:Top: genlmt(x0,c_unitedstatessociallifemt),mtvisible(x0) -> mtvisible(c_gregoriancalendarmt)
% 226.35/45.76 === Backtracking. Learning clause 1378:1:0:[1125.1,419.1]:: -> microtheory(c_tptp_member235_mt)
% 226.35/45.76 === Backtracking. Learning clause 1379:1:0:[1125.1,350.1]:: -> microtheory(c_tptp_member2668_mt)
% 226.35/45.76 === Backtracking. Learning clause 1380:1:0:[1125.1,344.1]:: -> microtheory(c_tptp_member2701_mt)
% 226.35/45.76 === Backtracking. Learning clause 1381:1:0:[1125.1,125.1]:: -> microtheory(c_hpkbvocabmt)
% 226.35/45.76 === Backtracking. Learning clause 1382:2:0:[1123.2,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_cyclistsmt)
% 226.35/45.76 === Conflict found: 1377:3:1:[1315.2,1123.2]:Top: genlmt(x0,c_unitedstatessociallifemt),mtvisible(x0) -> mtvisible(c_gregoriancalendarmt) {x0 -> c_peopledatamt}
% 226.35/45.76 === Backtracking. Learning clause 1383:2:0:[1377.1,35.1]:: mtvisible(c_peopledatamt) -> mtvisible(c_gregoriancalendarmt)
% 226.35/45.76 === Conflict found: 1373:3:1:[1154.2,1123.2]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt),mtvisible(x0) -> mtvisible(c_currentworlddatacollectormt_nonhomocentric) {x0 -> c_ldscgeneralcollectormt}
% 226.35/45.76 === Backtracking. Learning clause 1384:2:0:[1373.1,87.1]:: mtvisible(c_ldscgeneralcollectormt) -> mtvisible(c_currentworlddatacollectormt_nonhomocentric)
% 226.35/45.76 === Backtracking. Learning clause 1385:2:0:[1123.2,329.1]:: mtvisible(c_massmediadatamt) -> mtvisible(c_ethnicgroupsmt)
% 226.35/45.76 === Backtracking. Learning clause 1386:2:0:[1123.2,275.1]:: mtvisible(c_testvocabularymt) -> mtvisible(c_nooescapearchitecturemt)
% 226.35/45.76 === Backtracking. Learning clause 1387:2:0:[1123.2,257.1,1386.1]:: mtvisible(c_keinteractionresourcetestmt) -> mtvisible(c_nooescapearchitecturemt)
% 226.35/45.76 === Backtracking. Learning clause 1388:2:0:[1123.2,333.1]:: mtvisible(c_reasoningaboutpossibleantecedentsmt) -> mtvisible(c_humansociallifemt)
% 226.35/45.76 === Backtracking. Learning clause 1389:2:0:[1123.2,454.1]:: mtvisible(c_unitedstatesgeographydualistmt) -> mtvisible(c_worldgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1390:2:0:[1123.2,446.1]:: mtvisible(c_tptp_member2356_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1391:2:0:[1123.2,62.1]:: mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_ukencartamsncomencyclopedia_761573010_4united_states_of_americahtml)),c_translation_33)) -> mtvisible(c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1392:2:0:[1123.2,67.1]:: mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwfuntriviacomplayquizcfmqid60926origin)),c_translation_0_885)) -> mtvisible(c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1393:2:0:[1123.2,347.1]:: mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwpoweripodsearchinfobrown_ipodhtml)),c_translation_7)) -> mtvisible(c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1394:2:1:[565.1,391.2]:Top: shavingrazor_manual(x0) -> razor(x0)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 901
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1149:2:1:[1128.2,35.1]:Top: genlmt(x0,c_peopledatamt) -> genlmt(x0,c_unitedstatessociallifemt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1395:3:1:[1149.2,1123.2]:Top: genlmt(x0,c_peopledatamt),mtvisible(x0) -> mtvisible(c_unitedstatessociallifemt)
% 226.35/45.76 === Conflict found: 1151:2:1:[1128.2,53.1]:Top: genlmt(x0,c_ethnicgroupsmt) -> genlmt(x0,c_ethnicgroupsvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1396:3:1:[1151.2,1123.2,1326.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_ethnicgroupsvocabularymt)
% 226.35/45.76 === Conflict found: 1219:2:1:[1128.2,87.1]:Top: genlmt(x0,c_ldscgeneralcollectormt) -> genlmt(x0,c_ldscdemonstrationspindleheadmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1397:3:1:[1219.2,1123.2,1150.2]:Top: mtvisible(x0),genlmt(x0,c_miptdatabase19681997_termsmt) -> mtvisible(c_ldscdemonstrationspindleheadmt)
% 226.35/45.76 === Conflict found: 1219:2:1:[1128.2,87.1]:Top: genlmt(x0,c_ldscgeneralcollectormt) -> genlmt(x0,c_ldscdemonstrationspindleheadmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1398:3:1:[1219.2,1123.2]:Top: genlmt(x0,c_ldscgeneralcollectormt),mtvisible(x0) -> mtvisible(c_ldscdemonstrationspindleheadmt)
% 226.35/45.76 === Conflict found: 1226:2:1:[1128.2,334.1]:Top: genlmt(x0,c_worldgeographymt) -> genlmt(x0,c_geographymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1400:1:0:[1132.0,1399.0,1226.2,1123.2,1210.2,1.1]:: -> mtvisible(c_geographymt)
% 226.35/45.76 === Backtracking. Learning clause 1401:2:0:[1123.2,20.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member2610_mt)
% 226.35/45.76 === Backtracking. Learning clause 1402:1:0:[1125.1,20.1]:: -> microtheory(c_tptp_member2610_mt)
% 226.35/45.76 === Backtracking. Learning clause 1403:2:0:[1123.2,453.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member1672_mt)
% 226.35/45.76 === Backtracking. Learning clause 1404:2:0:[1123.2,198.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member237_mt)
% 226.35/45.76 === Backtracking. Learning clause 1405:1:0:[1125.1,198.1]:: -> microtheory(c_tptp_member237_mt)
% 226.35/45.76 === Backtracking. Learning clause 1406:2:0:[1123.2,344.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member2701_mt)
% 226.35/45.76 === Backtracking. Learning clause 1407:1:0:[1125.1,448.1]:: -> microtheory(c_tptp_member698_mt)
% 226.35/45.76 === Backtracking. Learning clause 1408:2:0:[1123.2,310.1,1387.1]:: mtvisible(c_cyclistsmt) -> mtvisible(c_nooescapearchitecturemt)
% 226.35/45.76 === Backtracking. Learning clause 1409:2:0:[1123.2,310.1]:: mtvisible(c_cyclistsmt) -> mtvisible(c_keinteractionresourcetestmt)
% 226.35/45.76 === Conflict found: 1396:3:1:[1151.2,1123.2,1326.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_ethnicgroupsvocabularymt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1410:2:0:[1396.2,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_ethnicgroupsvocabularymt)
% 226.35/45.76 === Conflict found: 1156:2:1:[1128.2,66.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_organizationdatamt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1411:3:1:[1156.2,1123.2,1324.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_organizationdatamt)
% 226.35/45.76 === Conflict found: 1327:2:1:[1128.2,367.1]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> genlmt(x0,c_worldcompletedualistgeographymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1412:3:1:[1327.2,1123.2]:Top: genlmt(x0,c_ethnicgroupsvocabularymt),mtvisible(x0) -> mtvisible(c_worldcompletedualistgeographymt)
% 226.35/45.76 === Conflict found: 1411:3:1:[1156.2,1123.2,1324.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_organizationdatamt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1413:2:0:[1411.2,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_organizationdatamt)
% 226.35/45.76 === Conflict found: 1151:2:1:[1128.2,53.1]:Top: genlmt(x0,c_ethnicgroupsmt) -> genlmt(x0,c_ethnicgroupsvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1414:3:1:[1151.2,1412.1,1326.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_worldcompletedualistgeographymt)
% 226.35/45.76 === Conflict found: 1414:3:1:[1151.2,1412.1,1326.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_worldcompletedualistgeographymt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1415:2:0:[1414.2,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_worldcompletedualistgeographymt)
% 226.35/45.76 === Backtracking. Learning clause 1416:2:0:[1123.2,35.1]:: mtvisible(c_peopledatamt) -> mtvisible(c_unitedstatessociallifemt)
% 226.35/45.76 === Conflict found: 1398:3:1:[1219.2,1123.2]:Top: genlmt(x0,c_ldscgeneralcollectormt),mtvisible(x0) -> mtvisible(c_ldscdemonstrationspindleheadmt) {x0 -> c_miptdatabase19681997_termsmt}
% 226.35/45.76 === Backtracking. Learning clause 1417:2:0:[1398.1,52.1]:: mtvisible(c_miptdatabase19681997_termsmt) -> mtvisible(c_ldscdemonstrationspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1418:1:0:[1125.1,273.1]:: -> microtheory(c_tptpgeo_member2_mt)
% 226.35/45.76 === Backtracking. Learning clause 1419:2:0:[1123.2,407.1]:: mtvisible(c_tptpgeo_spindlecollectormt) -> mtvisible(c_tptpgeo_member5_mt)
% 226.35/45.76 === Backtracking. Learning clause 1420:1:0:[1125.1,407.1]:: -> microtheory(c_tptpgeo_member5_mt)
% 226.35/45.76 === Backtracking. Learning clause 1421:1:0:[1125.1,140.1]:: -> microtheory(c_tptpgeo_member1_mt)
% 226.35/45.76 === Backtracking. Learning clause 1422:2:0:[1123.2,181.1]:: mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwthedailybulletincompostcardsmar9chtm)),c_translation_14)) -> mtvisible(c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1423:2:0:[1123.2,338.1]:: mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_memberstripodcomindygalfordtriviahtm)),c_translation_32)) -> mtvisible(c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1424:2:0:[1123.2,368.1]:: mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwarthritis_symptomcoma_cbursitishtm)),c_translation_0_885)) -> mtvisible(c_machinelearningspindleheadmt)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 965
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1425:2:1:[314.2,466.1]:Top: tptpcol_14_26921(x0) -> tptpcol_12_26919(x0)
% 226.35/45.76 === Backtracking. Learning clause 1427:1:0:[1132.0,1426.0,1123.2,1.1]:: -> mtvisible(c_tptpgeo_spindleheadmt)
% 226.35/45.76 === Conflict found: 1274:2:1:[1256.1,1189.2,1273.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_cyclistsmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1428:3:1:[1274.2,1123.2]:Top: genlmt(x0,c_tptp_spindlecollectormt),mtvisible(x0) -> mtvisible(c_cyclistsmt)
% 226.35/45.76 === Conflict found: 1287:2:1:[1128.2,358.1]:Top: genlmt(x0,c_corecyclmt) -> genlmt(x0,c_logicaltruthmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1429:1:0:[1287.2,1125.1,1159.2,1320.2,1.1]:: -> microtheory(c_logicaltruthmt)
% 226.35/45.76 === Backtracking. Learning clause 1430:2:0:[1123.2,350.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member2668_mt)
% 226.35/45.76 === Backtracking. Learning clause 1431:2:0:[1123.2,448.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member698_mt)
% 226.35/45.76 === Backtracking. Learning clause 1432:1:0:[1125.1,59.1]:: -> microtheory(c_currentworlddatacollectormt_nonhomocentric)
% 226.35/45.76 === Backtracking. Learning clause 1433:2:0:[1123.2,93.1]:: mtvisible(c_tptp_member2831_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1434:2:0:[1123.2,140.1]:: mtvisible(c_tptpgeo_spindlecollectormt) -> mtvisible(c_tptpgeo_member1_mt)
% 226.35/45.76 === Backtracking. Learning clause 1435:2:0:[1123.2,214.1]:: mtvisible(c_timehasnoendmt) -> mtvisible(c_generictemporalmt)
% 226.35/45.76 === Backtracking. Learning clause 1436:2:0:[1123.2,248.1]:: mtvisible(c_tptp_member974_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1437:2:0:[1123.2,315.1]:: mtvisible(c_tptp_member3993_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1438:2:0:[1123.2,364.1,1437.1,1382.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_cyclistsmt)
% 226.35/45.76 === Conflict found: 1146:2:1:[1128.2,115.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_calendarsmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1439:3:1:[1146.2,1123.2,1274.2]:Top: mtvisible(x0),genlmt(x0,c_tptp_spindlecollectormt) -> mtvisible(c_calendarsmt)
% 226.35/45.76 === Conflict found: 1146:2:1:[1128.2,115.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_calendarsmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1440:3:1:[1146.2,1123.2]:Top: genlmt(x0,c_cyclistsmt),mtvisible(x0) -> mtvisible(c_calendarsmt)
% 226.35/45.76 === Backtracking. Learning clause 1441:2:0:[1123.2,364.1,1437.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1442:2:0:[1123.2,115.1]:: mtvisible(c_cyclistsmt) -> mtvisible(c_calendarsmt)
% 226.35/45.76 === Conflict found: 1147:2:1:[1128.2,125.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_hpkbvocabmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1443:3:1:[1147.2,1123.2,1274.2]:Top: mtvisible(x0),genlmt(x0,c_tptp_spindlecollectormt) -> mtvisible(c_hpkbvocabmt)
% 226.35/45.76 === Conflict found: 1147:2:1:[1128.2,125.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_hpkbvocabmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1444:3:1:[1147.2,1123.2]:Top: genlmt(x0,c_cyclistsmt),mtvisible(x0) -> mtvisible(c_hpkbvocabmt)
% 226.35/45.76 === Backtracking. Learning clause 1445:2:0:[1123.2,125.1]:: mtvisible(c_cyclistsmt) -> mtvisible(c_hpkbvocabmt)
% 226.35/45.76 === Conflict found: 1295:2:1:[1128.2,367.1,1294.1]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> genlmt(x0,c_worldgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1446:3:1:[1295.2,1123.2,1151.2,1326.2,1274.2]:Top: mtvisible(x0),genlmt(x0,c_tptp_spindlecollectormt) -> mtvisible(c_worldgeographydualistmt)
% 226.35/45.76 === Conflict found: 1295:2:1:[1128.2,367.1,1294.1]:Top: genlmt(x0,c_ethnicgroupsvocabularymt) -> genlmt(x0,c_worldgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1447:3:1:[1295.2,1123.2,1151.2,1326.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_worldgeographydualistmt)
% 226.35/45.76 === Conflict found: 1447:3:1:[1295.2,1123.2,1151.2,1326.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_worldgeographydualistmt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1448:2:0:[1447.2,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_worldgeographydualistmt)
% 226.35/45.76 === Conflict found: 1198:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1449:3:1:[1198.2,1123.2,1327.2,1151.2,1326.2,1274.2]:Top: mtvisible(x0),genlmt(x0,c_tptp_spindlecollectormt) -> mtvisible(c_unitedstatesgeographydualistmt)
% 226.35/45.76 === Conflict found: 1198:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1450:3:1:[1198.2,1123.2,1327.2,1151.2,1326.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_unitedstatesgeographydualistmt)
% 226.35/45.76 === Conflict found: 1450:3:1:[1198.2,1123.2,1327.2,1151.2,1326.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_unitedstatesgeographydualistmt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1451:2:0:[1450.2,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_unitedstatesgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1452:2:1:[1128.1,454.1]:Top: genlmt(c_worldgeographydualistmt,x0) -> genlmt(c_unitedstatesgeographydualistmt,x0)
% 226.35/45.76 === Conflict found: 1182:2:1:[1128.2,232.1]:Top: genlmt(x0,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) -> genlmt(x0,c_massmediadatamt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1453:2:1:[1182.1,1301.2]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,c_massmediadatamt)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1242
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1326:2:1:[1182.1,1301.2,1322.1,1156.2,1324.2]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_ethnicgroupsmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1454:3:1:[1326.2,1123.2,1274.2]:Top: mtvisible(x0),genlmt(x0,c_tptp_spindlecollectormt) -> mtvisible(c_ethnicgroupsmt)
% 226.35/45.76 === Conflict found: 1326:2:1:[1182.1,1301.2,1322.1,1156.2,1324.2]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_ethnicgroupsmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1455:3:1:[1326.2,1123.2]:Top: genlmt(x0,c_cyclistsmt),mtvisible(x0) -> mtvisible(c_ethnicgroupsmt)
% 226.35/45.76 === Conflict found: 1453:2:1:[1182.1,1301.2]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,c_massmediadatamt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1456:3:1:[1453.2,1123.2]:Top: genlmt(x0,c_organizationdatamt),mtvisible(x0) -> mtvisible(c_massmediadatamt)
% 226.35/45.76 === Backtracking. Learning clause 1457:2:0:[1123.2,364.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member3993_mt)
% 226.35/45.76 === Conflict found: 1455:3:1:[1326.2,1123.2]:Top: genlmt(x0,c_cyclistsmt),mtvisible(x0) -> mtvisible(c_ethnicgroupsmt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1458:2:0:[1455.1,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_ethnicgroupsmt)
% 226.35/45.76 === Conflict found: 1288:2:1:[1128.2,378.1]:Top: genlmt(x0,c_calendarsmt) -> genlmt(x0,c_calendarsvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1459:3:1:[1288.2,1123.2,1146.2,1274.2]:Top: mtvisible(x0),genlmt(x0,c_tptp_spindlecollectormt) -> mtvisible(c_calendarsvocabularymt)
% 226.35/45.76 === Conflict found: 1288:2:1:[1128.2,378.1]:Top: genlmt(x0,c_calendarsmt) -> genlmt(x0,c_calendarsvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1460:3:1:[1288.2,1123.2,1146.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_calendarsvocabularymt)
% 226.35/45.76 === Conflict found: 1460:3:1:[1288.2,1123.2,1146.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_calendarsvocabularymt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1461:2:0:[1460.2,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_calendarsvocabularymt)
% 226.35/45.76 === Conflict found: 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1462:3:1:[1175.2,1123.2,1191.2,1274.2]:Top: mtvisible(x0),genlmt(x0,c_tptp_spindlecollectormt) -> mtvisible(c_testvocabularymt)
% 226.35/45.76 === Conflict found: 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1463:3:1:[1175.2,1123.2,1191.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_testvocabularymt)
% 226.35/45.76 === Conflict found: 1463:3:1:[1175.2,1123.2,1191.2]:Top: mtvisible(x0),genlmt(x0,c_cyclistsmt) -> mtvisible(c_testvocabularymt) {x0 -> c_tptp_spindleheadmt}
% 226.35/45.76 === Backtracking. Learning clause 1464:2:0:[1463.2,254.1]:: mtvisible(c_tptp_spindleheadmt) -> mtvisible(c_testvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1465:2:1:[1128.1,479.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2862_mt,x0)
% 226.35/45.76 === Backtracking. Learning clause 1466:1:0:[1108.1,111.1]:: -> collection(c_setorcollection)
% 226.35/45.76 === Backtracking. Learning clause 1467:1:0:[1106.1,150.1]:: -> collection(c_collection)
% 226.35/45.76 === Backtracking. Learning clause 1468:1:0:[637.1,295.1]:: -> relation(c_disjointwith)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1308
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1288:2:1:[1128.2,378.1]:Top: genlmt(x0,c_calendarsmt) -> genlmt(x0,c_calendarsvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1469:3:1:[1288.2,1123.2]:Top: genlmt(x0,c_calendarsmt),mtvisible(x0) -> mtvisible(c_calendarsvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1470:1:0:[1125.1,453.1]:: -> microtheory(c_tptp_member1672_mt)
% 226.35/45.76 === Backtracking. Learning clause 1471:2:0:[1123.2,34.1,1382.1]:: mtvisible(c_tptp_member3205_mt) -> mtvisible(c_cyclistsmt)
% 226.35/45.76 === Backtracking. Learning clause 1472:2:0:[1123.2,378.1]:: mtvisible(c_calendarsmt) -> mtvisible(c_calendarsvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1473:2:0:[1123.2,172.1]:: mtvisible(c_tptp_member2089_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1474:2:0:[1123.2,279.1]:: mtvisible(c_tptp_member3717_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1475:2:0:[1123.2,479.1]:: mtvisible(c_tptp_member2862_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1476:2:0:[1123.2,232.1]:: mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) -> mtvisible(c_massmediadatamt)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1372
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1477:2:0:[1123.2,87.1]:: mtvisible(c_ldscgeneralcollectormt) -> mtvisible(c_ldscdemonstrationspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1478:2:0:[1123.2,58.1]:: mtvisible(c_machinelearningspindleheadmt) -> mtvisible(c_miptdatabase19681997_termsmt)
% 226.35/45.76 === Conflict found: 1456:3:1:[1453.2,1123.2]:Top: genlmt(x0,c_organizationdatamt),mtvisible(x0) -> mtvisible(c_massmediadatamt) {x0 -> c_nooescapearchitecturemt}
% 226.35/45.76 === Backtracking. Learning clause 1479:2:0:[1456.1,66.1]:: mtvisible(c_nooescapearchitecturemt) -> mtvisible(c_massmediadatamt)
% 226.35/45.76 === Conflict found: 1453:2:1:[1182.1,1301.2]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,c_massmediadatamt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1480:2:1:[1453.2,1322.1]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,c_ethnicgroupsmt)
% 226.35/45.76 === Backtracking. Learning clause 1481:2:0:[1123.2,273.1]:: mtvisible(c_tptpgeo_spindlecollectormt) -> mtvisible(c_tptpgeo_member2_mt)
% 226.35/45.76 === Backtracking. Learning clause 1482:2:0:[1123.2,384.1]:: mtvisible(c_unitedstatesgeographypeoplemt) -> mtvisible(c_peopledatamt)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1535
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1170:2:1:[1128.2,269.1]:Top: genlmt(x0,c_cycnounlearnermt) -> genlmt(x0,c_cycorpproductsmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1483:3:1:[1170.2,1123.2,1153.2]:Top: mtvisible(x0),genlmt(x0,c_machinelearningspindleheadmt) -> mtvisible(c_cycorpproductsmt)
% 226.35/45.76 === Backtracking. Learning clause 1484:2:1:[1128.2,407.1]:Top: genlmt(x0,c_tptpgeo_spindlecollectormt) -> genlmt(x0,c_tptpgeo_member5_mt)
% 226.35/45.76 === Backtracking. Learning clause 1485:2:0:[1123.2,269.1]:: mtvisible(c_cycnounlearnermt) -> mtvisible(c_cycorpproductsmt)
% 226.35/45.76 === Backtracking. Learning clause 1486:1:0:[690.1,263.1]:: -> relation(c_most)
% 226.35/45.76 === Backtracking. Learning clause 1487:1:0:[690.1,228.1]:: -> relation(c_genls)
% 226.35/45.76 === Backtracking. Learning clause 1488:1:0:[637.1,434.1]:: -> relation(c_few)
% 226.35/45.76 === Backtracking. Learning clause 1489:1:0:[678.1,392.1]:: -> collection(c_tptpcol_16_25972)
% 226.35/45.76 === Backtracking. Learning clause 1490:2:0:[679.1,309.2]:: mtvisible(c_currentworlddatacollectormt_nonhomocentric) -> binarypredicate(c_tptp_9_51)
% 226.35/45.76 === Backtracking. Learning clause 1491:2:1:[676.1,244.2]:Top: isa(x0,f_subcollectionofwithrelationtotypefn(c_issuingaprescription,c_products,c_correctivelensprescription)) -> tptpcol_7_7172(f_relationexistsallfn(x0,c_tptp_8_968,c_tptpcol_16_7738,f_subcollectionofwithrelationtotypefn(c_issuingaprescription,c_products,c_correctivelensprescription)))
% 226.35/45.76 === Backtracking. Learning clause 1492:3:1:[621.1,308.3]:Top: mtvisible(c_currentworlddatacollectormt_nonhomocentric),isa(x0,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)) -> tptpcol_7_26628(f_relationexistsallfn(x0,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma)))
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1599
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1412:3:1:[1327.2,1123.2]:Top: genlmt(x0,c_ethnicgroupsvocabularymt),mtvisible(x0) -> mtvisible(c_worldcompletedualistgeographymt) {x0 -> c_ethnicgroupsmt}
% 226.35/45.76 === Backtracking. Learning clause 1493:2:0:[1412.1,53.1]:: mtvisible(c_ethnicgroupsmt) -> mtvisible(c_worldcompletedualistgeographymt)
% 226.35/45.76 === Backtracking. Learning clause 1494:2:0:[1123.2,177.1]:: mtvisible(c_machinelearningspindleheadmt) -> mtvisible(c_cycnounlearnermt)
% 226.35/45.76 === Backtracking. Learning clause 1495:2:0:[1123.2,243.1]:: mtvisible(c_tptp_member3633_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1496:2:0:[1123.2,339.1,1389.1,1493.2]:: mtvisible(c_ethnicgroupsmt) -> mtvisible(c_worldgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1497:1:0:[1119.1,152.1]:: -> collection(c_tptpcol_1_1)
% 226.35/45.76 === Backtracking. Learning clause 1498:1:0:[1120.1,290.1]:: -> disjointwith(c_individual,c_collection)
% 226.35/45.76 === Backtracking. Learning clause 1499:2:1:[619.2,1091.1]:Top: tptpcol_16_27189(x0) -> collection(c_tptpcol_16_27189)
% 226.35/45.76 === Backtracking. Learning clause 1500:2:0:[1123.2,486.1,1476.1]:: mtvisible(c_organizationdatamt) -> mtvisible(c_massmediadatamt)
% 226.35/45.76 === Backtracking. Learning clause 1501:1:0:[677.1,392.1]:: -> collection(c_shavingrazor_manual)
% 226.35/45.76 === Backtracking. Learning clause 1502:1:0:[679.1,392.1]:: -> binarypredicate(c_tptp_8_271)
% 226.35/45.76 === Backtracking. Learning clause 1503:1:3:[289.1,708.1]:TopTopTop: individual(f_subcollectionofwithrelationtofn(x0,x1,x2)) ->
% 226.35/45.76 === Backtracking. Learning clause 1504:1:0:[679.1,245.1]:: -> binarypredicate(c_tptp_8_968)
% 226.35/45.76 === Backtracking. Learning clause 1505:2:0:[678.1,309.2]:: mtvisible(c_currentworlddatacollectormt_nonhomocentric) -> collection(c_tptpcol_16_27189)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1667
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1343:2:1:[1128.2,419.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member235_mt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1506:3:1:[1343.2,1123.2]:Top: genlmt(x0,c_tptp_spindlecollectormt),mtvisible(x0) -> mtvisible(c_tptp_member235_mt)
% 226.35/45.76 === Backtracking. Learning clause 1507:2:0:[1123.2,419.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member235_mt)
% 226.35/45.76 === Conflict found: 1256:2:1:[1128.2,315.1]:Top: genlmt(x0,c_tptp_member3993_mt) -> genlmt(x0,c_tptp_spindleheadmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1508:2:1:[1256.1,1189.2]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1509:1:0:[1119.1,2.1]:: -> collection(c_intangible)
% 226.35/45.76 === Backtracking. Learning clause 1510:1:0:[1119.1,487.1]:: -> collection(c_tptpcol_3_98305)
% 226.35/45.76 === Backtracking. Learning clause 1511:1:0:[1120.1,152.1]:: -> disjointwith(c_tptpcol_1_65536,c_tptpcol_1_1)
% 226.35/45.76 === Backtracking. Learning clause 1512:2:0:[1123.2,247.1]:: mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885)) -> mtvisible(c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1513:2:0:[1123.2,433.1]:: mtvisible(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_webnjiteducjohnsontreebiochhtm)),c_translation_21)) -> mtvisible(c_machinelearningspindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1514:1:0:[678.1,245.1]:: -> collection(c_tptpcol_16_7738)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1734
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1479:2:0:[1456.1,66.1]:: mtvisible(c_nooescapearchitecturemt) -> mtvisible(c_massmediadatamt) {}
% 226.35/45.76 === Backtracking. Learning clause 1515:2:0:[1479.2,1385.1,1408.2]:: mtvisible(c_cyclistsmt) -> mtvisible(c_ethnicgroupsmt)
% 226.35/45.76 === Backtracking. Learning clause 1516:2:1:[185.2,1352.1]:Top: tptpcol_8_109059(x0) -> tptpcol_5_106498(x0)
% 226.35/45.76 === Conflict found: 1198:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1517:3:1:[1198.2,1123.2]:Top: genlmt(x0,c_worldcompletedualistgeographymt),mtvisible(x0) -> mtvisible(c_unitedstatesgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1518:2:0:[1123.2,53.1]:: mtvisible(c_ethnicgroupsmt) -> mtvisible(c_ethnicgroupsvocabularymt)
% 226.35/45.76 === Conflict found: 1517:3:1:[1198.2,1123.2]:Top: genlmt(x0,c_worldcompletedualistgeographymt),mtvisible(x0) -> mtvisible(c_unitedstatesgeographydualistmt) {x0 -> c_ethnicgroupsvocabularymt}
% 226.35/45.76 === Backtracking. Learning clause 1519:2:0:[1517.1,367.1]:: mtvisible(c_ethnicgroupsvocabularymt) -> mtvisible(c_unitedstatesgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1520:2:0:[1123.2,66.1]:: mtvisible(c_nooescapearchitecturemt) -> mtvisible(c_organizationdatamt)
% 226.35/45.76 === Backtracking. Learning clause 1521:2:0:[1123.2,147.1]:: mtvisible(c_tptp_member3515_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1522:2:0:[1123.2,257.1]:: mtvisible(c_keinteractionresourcetestmt) -> mtvisible(c_testvocabularymt)
% 226.35/45.76 === Backtracking. Learning clause 1523:1:0:[1119.1,166.1]:: -> collection(c_individual)
% 226.35/45.76 === Backtracking. Learning clause 1524:3:1:[1123.2,1301.2]:Top: mtvisible(x0),genlmt(x0,c_organizationdatamt) -> mtvisible(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman))
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1801
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1500:2:0:[1123.2,486.1,1476.1]:: mtvisible(c_organizationdatamt) -> mtvisible(c_massmediadatamt) {}
% 226.35/45.76 === Backtracking. Learning clause 1525:2:0:[1500.2,1385.1,1520.2]:: mtvisible(c_nooescapearchitecturemt) -> mtvisible(c_ethnicgroupsmt)
% 226.35/45.76 === Conflict found: 1389:2:0:[1123.2,454.1]:: mtvisible(c_unitedstatesgeographydualistmt) -> mtvisible(c_worldgeographydualistmt) {}
% 226.35/45.76 === Backtracking. Learning clause 1526:2:0:[1389.1,1519.2]:: mtvisible(c_ethnicgroupsvocabularymt) -> mtvisible(c_worldgeographydualistmt)
% 226.35/45.76 === Backtracking. Learning clause 1527:2:1:[216.2,1266.1]:Top: tptpcol_7_113665(x0) -> tptpcol_4_106497(x0)
% 226.35/45.76 === Backtracking. Learning clause 1528:2:0:[1123.2,133.1]:: mtvisible(c_tptp_member3393_mt) -> mtvisible(c_tptp_spindleheadmt)
% 226.35/45.76 === Backtracking. Learning clause 1529:2:0:[777.1,178.2]:: mtvisible(c_tptp_member2668_mt) -> firstordercollection(c_tptpcol_16_8886)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1865
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1931
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1530:2:1:[792.2,1091.1]:Top: tptpcol_16_31868(x0) -> collection(c_tptpcol_16_31868)
% 226.35/45.76 === Backtracking. Learning clause 1531:2:0:[804.1,159.2]:: mtvisible(c_tptp_member2610_mt) -> collection(c_tptpcol_16_31868)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 1995
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1532:2:1:[388.2,1265.1,161.2,130.2]:Top: tptpcol_11_118084(x0) -> tptpcol_6_116738(x0)
% 226.35/45.76 === Backtracking. Learning clause 1533:2:1:[388.2,1265.1,161.2]:Top: tptpcol_10_118020(x0) -> tptpcol_6_116738(x0)
% 226.35/45.76 === Backtracking. Learning clause 1534:2:0:[1123.2,414.1]:: mtvisible(c_unitedstatessociallifemt) -> mtvisible(c_gregoriancalendarmt)
% 226.35/45.76 === Backtracking. Learning clause 1535:1:3:[289.1,864.1]:TopTopTop: individual(f_subcollectionofwithrelationfromtypefn(x0,x1,x2)) ->
% 226.35/45.76 === Backtracking. Learning clause 1536:2:0:[806.1,159.2]:: mtvisible(c_tptp_member2610_mt) -> binarypredicate(c_tptp_8_875)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 2061
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1537:2:1:[114.2,1206.1]:Top: tptpcol_13_109173(x0) -> tptpcol_10_109061(x0)
% 226.35/45.76 === Backtracking. Learning clause 1538:2:1:[388.2,1265.1]:Top: tptpcol_9_118019(x0) -> tptpcol_6_116738(x0)
% 226.35/45.76 === Backtracking. Learning clause 1539:2:0:[804.1,165.2]:: mtvisible(c_cyclistsmt) -> collection(c_tptpcol_16_29490)
% 226.35/45.76 === Backtracking. Learning clause 1540:2:0:[805.1,165.2]:: mtvisible(c_cyclistsmt) -> collection(c_executionbyfiringsquad)
% 226.35/45.76 === Backtracking. Learning clause 1541:3:1:[785.1,164.3]:Top: mtvisible(c_cyclistsmt),executionbyfiringsquad(x0) -> tptpcol_5_28674(f_relationallexistsfn(x0,c_tptp_9_720,c_executionbyfiringsquad,c_tptpcol_16_29490))
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 2128
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1205:2:1:[278.2,411.1]:Top: tptpcol_10_26886(x0) -> tptpcol_8_26629(x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1542:2:1:[1205.1,430.2,1204.1,142.2]:Top: tptpcol_12_26919(x0) -> tptpcol_5_24579(x0)
% 226.35/45.76 === Conflict found: 1150:2:1:[1128.2,52.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> genlmt(x0,c_ldscgeneralcollectormt) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1543:3:1:[1150.2,1123.2]:Top: genlmt(x0,c_miptdatabase19681997_termsmt),mtvisible(x0) -> mtvisible(c_ldscgeneralcollectormt)
% 226.35/45.76 === Backtracking. Learning clause 1544:2:0:[1123.2,52.1]:: mtvisible(c_miptdatabase19681997_termsmt) -> mtvisible(c_ldscgeneralcollectormt)
% 226.35/45.76 === Backtracking. Learning clause 1545:2:0:[898.1,104.2]:: mtvisible(c_tptpgeo_member5_mt) -> geographicalregion(c_georegion_l4_x57_y47)
% 226.35/45.76 === Backtracking. Learning clause 1546:2:0:[899.1,104.2]:: mtvisible(c_tptpgeo_member5_mt) -> geographicalregion(c_georegion_l4_x56_y47)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 2197
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Backtracking. Learning clause 1547:2:1:[149.2,1335.1]:Top: tptpcol_9_92165(x0) -> tptpcol_6_92162(x0)
% 226.35/45.76 === Conflict found: 1516:2:1:[185.2,1352.1]:Top: tptpcol_8_109059(x0) -> tptpcol_5_106498(x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1548:2:1:[1516.1,242.2,117.1,96.2]:Top: tptpcol_10_109061(x0) -> tptpcol_4_106497(x0)
% 226.35/45.76 === Conflict found: 1205:2:1:[278.2,411.1]:Top: tptpcol_10_26886(x0) -> tptpcol_8_26629(x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1549:2:1:[1205.1,430.2]:Top: tptpcol_11_26887(x0) -> tptpcol_8_26629(x0)
% 226.35/45.76 === Backtracking. Learning clause 1550:1:0:[1118.1,2.1]:: -> collection(c_partiallytangible)
% 226.35/45.76 === Backtracking. Learning clause 1551:1:0:[1119.1,1511.1]:: -> collection(c_tptpcol_1_65536)
% 226.35/45.76 === Backtracking. Learning clause 1552:1:0:[1118.1,487.1]:: -> collection(c_tptpcol_3_114688)
% 226.35/45.76 === Backtracking. Learning clause 1553:2:1:[924.2,1093.1]:Top: tptpcol_12_92262(x0) -> thing(x0)
% 226.35/45.76 === Backtracking. Learning clause 1554:2:1:[907.2,1093.1]:Top: tptpcol_6_116738(x0) -> thing(x0)
% 226.35/45.76 === Backtracking. Learning clause 1555:2:1:[888.2,1093.1]:Top: tptpcol_11_18631(x0) -> thing(x0)
% 226.35/45.76 === Backtracking. Learning clause 1556:2:1:[876.2,1093.1]:Top: tptpcol_5_24579(x0) -> thing(x0)
% 226.35/45.76 === Backtracking. Learning clause 1557:2:1:[874.2,1093.1]:Top: tptpcol_4_24578(x0) -> thing(x0)
% 226.35/45.76 === Backtracking. Learning clause 1558:2:1:[855.2,1093.1]:Top: terroristgroup(x0) -> thing(x0)
% 226.35/45.76 === Backtracking. Learning clause 1559:2:1:[824.2,1093.1,1332.2]:Top: tptpcol_4_16387(x0) -> thing(x0)
% 226.35/45.76 === Backtracking. Learning clause 1560:2:1:[1091.1,919.2]:Top: executionbyfiringsquad(x0) -> collection(c_executionbyfiringsquad)
% 226.35/45.76 === Backtracking. Learning clause 1561:2:0:[898.1,485.2]:: mtvisible(c_tptpgeo_member7_mt) -> geographicalregion(c_georegion_l4_x29_y76)
% 226.35/45.76 === Backtracking. Learning clause 1562:2:0:[894.1,157.2]:: mtvisible(c_tptp_member237_mt) -> firstordercollection(c_pushingababycarriage)
% 226.35/45.76 === Clause set with instances from active satisfied. Growing active. New size: 2261
% 226.35/45.76 === Restarting.
% 226.35/45.76 === Conflict found: 1516:2:1:[185.2,1352.1]:Top: tptpcol_8_109059(x0) -> tptpcol_5_106498(x0) {x0 -> c_tptpgeo_member8_mt}
% 226.35/45.76 === Backtracking. Learning clause 1563:2:1:[1516.1,242.2,117.1]:Top: tptpcol_9_109060(x0) -> tptpcol_4_106497(x0)
% 226.35/45.76 === Backtracking. Learning clause 1564:2:1:[1091.1,939.2]:Top: furpelt(x0) -> collection(c_furpelt)
% 226.35/45.76 === Backtracking. Learning clause 1565:2:1:[128.2,931.1,1042.2]:Top: geographicalregion(x0) -> spatialthing_nonsituational(x0)
% 226.35/45.76 === Backtracking. Learning clause 1566:2:0:[931.1,82.2]:: mtvisible(c_tptpgeo_member7_mt) -> spatialthing_nonsituational(c_georegion_l4_x53_y74)
% 226.35/45.76 === Backtracking. Learning clause 1567:2:0:[932.1,82.2]:: mtvisible(c_tptpgeo_member7_mt) -> spatialthing_nonsituational(c_geolocation_x53_y74)
% 226.35/45.76 === Backtracking. Learning clause 1568:2:0:[931.1,282.2]:: mtvisible(c_tptpgeo_member3_mt) -> spatialthing_nonsituational(c_georegion_l4_x14_y39)
% 226.35/45.76
% 226.35/45.76 SZS status Unsatisfiable
% 226.35/45.76
% 226.35/45.76 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 226.35/45.76
% 226.35/45.76 SPASS-SCL-FOL Statistics:
% 226.35/45.76 Number of learned clauses: 432
% 226.35/45.76 Number of propagations: 112359
% 226.35/45.76 Number of decisions: 42694
% 226.35/45.76 Number of resolutions: 541
% 226.35/45.76 Number of condensations: 0
% 226.35/45.76 Number of sub resolutions: 3
% 226.35/45.76 Number of input literals (deduplicated): 891
% 226.35/45.76 Number of grows: 26
% 226.35/45.76 Number of considered ground atoms: 2261
% 226.35/45.76
% 226.35/45.76 Needed: 0:0:45.23
% 226.35/45.76
%------------------------------------------------------------------------------