%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR034+2 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu May 7 07:19:36 PM UTC 2026
% Result : Theorem 56.33s 14.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : CSR034+2 : TPTP v9.2.1. Released v3.4.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.13/0.31 % Computer : n028.cluster.edu
% 0.13/0.31 % Model : x86_64 x86_64
% 0.13/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.31 % Memory : 8042.1875MB
% 0.13/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.31 % CPULimit : 300
% 0.13/0.31 % WCLimit : 300
% 0.13/0.31 % DateTime : Thu May 7 11:38:38 EDT 2026
% 0.13/0.32 % CPUTime :
% 0.13/0.32 SPASS-SCL-FOL version:
% 0.19/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 56.33/14.54 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.33/14.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.33/14.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.33/14.54 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.33/14.54 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.33/14.54 Execution resolution_3 ended with status: unsatisfiable
% 56.33/14.54 Used heuristic: resolution_3
% 56.33/14.54
% 56.33/14.54 Input Clauses:
% 56.33/14.54
% 56.33/14.54 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
% 56.33/14.54 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
% 56.33/14.54 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
% 56.33/14.54 Problem Properties:
% 56.33/14.54 This is a full first-order problem without equality.
% 56.33/14.54
% 56.33/14.54 After reduction: Problem Properties:
% 56.33/14.54 This is a full first-order problem without equality.
% 56.33/14.54
% 56.33/14.54
% 56.33/14.54 Reduced Input Clauses:
% 56.33/14.54
% 56.33/14.54 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)
% 56.33/14.54
% 56.33/14.54 === Starting SPASS-SCL-FOL A Little Less Naive, considering 161 atoms initially, heuristics mode: resolution_3 ===
% 56.33/14.54
% 56.33/14.54 === Backtracking. Learning clause 1134:2:1:[31.2,194.1]:Top: tptpcol_11_22023(x0) -> tptpcol_9_22021(x0)
% 56.33/14.54 === Backtracking. Learning clause 1135:2:1:[69.2,234.1]:Top: tptpcol_4_106497(x0) -> tptpcol_2_98304(x0)
% 56.33/14.54 === Backtracking. Learning clause 1136:1:0:[171.1,83.1]:: -> microtheory(c_wamt_evalinitial_p14)
% 56.33/14.54 === Backtracking. Learning clause 1137:2:1:[110.2,176.1]:Top: tptpcol_12_18663(x0) -> tptpcol_10_18567(x0)
% 56.33/14.54 === Backtracking. Learning clause 1138:2:1:[180.2,132.1]:Top: mathematicalthing(x0) -> intangible(x0)
% 56.33/14.54 === Backtracking. Learning clause 1139:2:1:[146.2,153.1]:Top: tptpcol_2_2(x0),tptpcol_1_65536(x0) ->
% 56.33/14.54 === Backtracking. Learning clause 1140:2:1:[151.2,289.1]:Top: fixedordercollection(x0),individual(x0) ->
% 56.33/14.54 === Backtracking. Learning clause 1141:2:1:[183.2,192.1]:Top: tptpcol_15_93775(x0) -> tptpcol_13_93766(x0)
% 56.33/14.54 === Backtracking. Learning clause 1142:2:1:[190.2,231.1]:Top: tptpcol_14_22072(x0) -> tptpcol_12_22055(x0)
% 56.33/14.54 === Backtracking. Learning clause 1143:1:0:[294.1,246.1]:: -> orderingpredicate(c_geographicalsubregions)
% 56.33/14.54 === Backtracking. Learning clause 1144:2:1:[1128.2,20.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2610_mt)
% 56.33/14.54 === Backtracking. Learning clause 1145:2:1:[1128.2,198.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member237_mt)
% 56.33/14.54 === Backtracking. Learning clause 1146:2:1:[1128.2,115.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_calendarsmt)
% 56.33/14.54 === Backtracking. Learning clause 1147:2:1:[1128.2,125.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_hpkbvocabmt)
% 56.33/14.54 === Backtracking. Learning clause 1148:2:1:[1128.2,34.1]:Top: genlmt(x0,c_tptp_member3205_mt) -> genlmt(x0,c_tptp_spindleheadmt)
% 56.33/14.54 === Backtracking. Learning clause 1149:2:1:[1128.2,35.1]:Top: genlmt(x0,c_peopledatamt) -> genlmt(x0,c_unitedstatessociallifemt)
% 56.33/14.54 === Backtracking. Learning clause 1150:2:1:[1128.2,52.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> genlmt(x0,c_ldscgeneralcollectormt)
% 56.33/14.54 === Backtracking. Learning clause 1151:2:1:[1128.2,53.1]:Top: genlmt(x0,c_ethnicgroupsmt) -> genlmt(x0,c_ethnicgroupsvocabularymt)
% 56.33/14.54 === Backtracking. Learning clause 1152:2:1:[1128.1,58.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> genlmt(c_machinelearningspindleheadmt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1153:2:1:[1128.2,177.1]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> genlmt(x0,c_cycnounlearnermt)
% 56.33/14.54 === Backtracking. Learning clause 1154:2:1:[1128.2,59.1]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt) -> genlmt(x0,c_currentworlddatacollectormt_nonhomocentric)
% 56.33/14.54 === Backtracking. Learning clause 1155:2:1:[1128.1,63.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member7_mt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1156:2:1:[1128.2,66.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_organizationdatamt)
% 56.33/14.54 === Backtracking. Learning clause 1157:2:1:[1128.2,88.1]:Top: genlmt(x0,c_patterndetectormt) -> genlmt(x0,c_basekb)
% 56.33/14.54 === Backtracking. Learning clause 1158:2:1:[1128.1,206.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_universalvocabularymt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1159:2:1:[1128.2,92.1]:Top: genlmt(x0,c_universalvocabularymt) -> genlmt(x0,c_corecyclmt)
% 56.33/14.54 === Backtracking. Learning clause 1160:2:1:[1128.1,93.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2831_mt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1161:2:1:[1128.1,133.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3393_mt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1162:2:1:[1128.1,136.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_generictemporalmt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1163:2:1:[1128.1,137.1]:Top: genlmt(c_worldgeographymt,x0) -> genlmt(c_worldgeographydualistmt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1164:2:1:[1128.2,137.1]:Top: genlmt(x0,c_worldgeographydualistmt) -> genlmt(x0,c_worldgeographymt)
% 56.33/14.54 === Backtracking. Learning clause 1165:2:1:[1128.2,273.1]:Top: genlmt(x0,c_tptpgeo_spindlecollectormt) -> genlmt(x0,c_tptpgeo_member2_mt)
% 56.33/14.54 === Backtracking. Learning clause 1166:2:1:[1128.1,147.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3515_mt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1167:2:1:[1128.1,154.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_geographymt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1168:2:1:[1128.1,162.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_calendarsvocabularymt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1169:2:1:[1128.1,172.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2089_mt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1170:2:1:[1128.2,269.1]:Top: genlmt(x0,c_cycnounlearnermt) -> genlmt(x0,c_cycorpproductsmt)
% 56.33/14.54 === Backtracking. Learning clause 1171:2:1:[1128.1,212.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member3_mt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1172:2:1:[1128.1,214.1]:Top: genlmt(c_generictemporalmt,x0) -> genlmt(c_timehasnoendmt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1173:2:1:[1128.1,243.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3633_mt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1174:2:1:[1128.1,248.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member974_mt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt)
% 56.33/14.54 === Backtracking. Learning clause 1176:2:1:[1128.1,275.1]:Top: genlmt(c_nooescapearchitecturemt,x0) -> genlmt(c_testvocabularymt,x0)
% 56.33/14.54 === Backtracking. Learning clause 1177:2:1:[1128.1,272.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_humansociallifemt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1178:2:1:[1128.1,274.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_knowledgefragmentd3mt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1179:2:1:[1128.1,279.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3717_mt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1180:2:1:[1128.1,232.1]:Top: genlmt(c_massmediadatamt,x0) -> genlmt(f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman),x0)
% 56.33/14.55 === Backtracking. Learning clause 1181:2:1:[1128.2,232.1]:Top: genlmt(x0,f_contextofpcwfn(c_ap_martha_stewart_omnimedia_names_chairman)) -> genlmt(x0,c_massmediadatamt)
% 56.33/14.55 === Backtracking. Learning clause 1182: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)
% 56.33/14.55 === Backtracking. Learning clause 1183: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)
% 56.33/14.55 === Backtracking. Learning clause 1184: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)
% 56.33/14.55 === Backtracking. Learning clause 1185: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)
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 225
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1186:2:1:[262.2,375.1]:Top: tptpcol_7_26628(x0) -> tptpcol_5_24579(x0)
% 56.33/14.55 === Backtracking. Learning clause 1187:2:1:[360.2,343.1]:Top: tptpcol_12_109157(x0) -> tptpcol_10_109061(x0)
% 56.33/14.55 === Backtracking. Learning clause 1188:2:1:[357.2,362.1]:Top: tptpcol_8_117763(x0) -> tptpcol_6_116738(x0)
% 56.33/14.55 === Backtracking. Learning clause 1189:2:1:[380.1,373.2]:Top: tptpcol_11_93764(x0) -> tptpcol_9_93699(x0)
% 56.33/14.55 === Backtracking. Learning clause 1190:2:1:[1128.2,326.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_worldgeographymt)
% 56.33/14.55 === Backtracking. Learning clause 1191:2:1:[1128.2,350.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2668_mt)
% 56.33/14.55 === Backtracking. Learning clause 1192:2:1:[1128.2,344.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2701_mt)
% 56.33/14.55 === Backtracking. Learning clause 1193:2:1:[1128.2,358.1]:Top: genlmt(x0,c_corecyclmt) -> genlmt(x0,c_logicaltruthmt)
% 56.33/14.55 === Backtracking. Learning clause 1194:2:1:[1128.1,332.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_cycorpproductsmt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1195:2:1:[1128.1,315.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member3993_mt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1196:2:1:[1128.1,333.1]:Top: genlmt(c_humansociallifemt,x0) -> genlmt(c_reasoningaboutpossibleantecedentsmt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1197:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt)
% 56.33/14.55 === Backtracking. Learning clause 1198: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)
% 56.33/14.55 === Backtracking. Learning clause 1199: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)
% 56.33/14.55 === Backtracking. Learning clause 1200: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)
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 314
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1201:2:1:[386.1,286.2,1139.1]:Top: tptpcol_4_16387(x0),tptpcol_1_65536(x0) ->
% 56.33/14.55 === Backtracking. Learning clause 1202:2:1:[278.2,411.1]:Top: tptpcol_10_26886(x0) -> tptpcol_8_26629(x0)
% 56.33/14.55 === Backtracking. Learning clause 1203:2:1:[382.2,320.1,156.2]:Top: microtheory(x0) -> partiallyintangibleindividual(x0)
% 56.33/14.55 === Backtracking. Learning clause 1204:2:1:[421.2,325.1]:Top: tptpcol_8_92164(x0) -> tptpcol_6_92162(x0)
% 56.33/14.55 === Backtracking. Learning clause 1205:2:1:[406.1,398.2]:Top: tptpcol_7_72707(x0) -> tptpcol_5_69635(x0)
% 56.33/14.55 === Backtracking. Learning clause 1206:1:0:[1125.1,1.1]:: -> microtheory(c_tptpgeo_spindleheadmt)
% 56.33/14.55 === Conflict found: 1190:2:1:[1128.2,326.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_worldgeographymt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1207:1:0:[1190.2,1125.1,1.1]:: -> microtheory(c_worldgeographymt)
% 56.33/14.55 === Backtracking. Learning clause 1208:1:0:[1127.1,20.1]:: -> microtheory(c_tptp_spindlecollectormt)
% 56.33/14.55 === Backtracking. Learning clause 1209:2:1:[1128.2,419.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member235_mt)
% 56.33/14.55 === Backtracking. Learning clause 1210:2:1:[1128.2,364.1,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member3993_mt)
% 56.33/14.55 === Backtracking. Learning clause 1211:1:0:[1125.1,364.1]:: -> microtheory(c_tptp_member3993_mt)
% 56.33/14.55 === Backtracking. Learning clause 1212:1:0:[1127.1,115.1]:: -> microtheory(c_cyclistsmt)
% 56.33/14.55 === Conflict found: 1146:2:1:[1128.2,115.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_calendarsmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1213:2:1:[1146.2,1125.1]:Top: genlmt(x0,c_cyclistsmt) -> microtheory(c_calendarsmt)
% 56.33/14.55 === Backtracking. Learning clause 1214:1:0:[1125.1,115.1]:: -> microtheory(c_calendarsmt)
% 56.33/14.55 === Backtracking. Learning clause 1215:2:1:[1128.2,310.1,1125.1]:Top: genlmt(x0,c_cyclistsmt) -> microtheory(c_keinteractionresourcetestmt)
% 56.33/14.55 === Backtracking. Learning clause 1216:1:0:[1125.1,310.1]:: -> microtheory(c_keinteractionresourcetestmt)
% 56.33/14.55 === Conflict found: 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1217:2:1:[1175.2,1125.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> microtheory(c_testvocabularymt)
% 56.33/14.55 === Conflict found: 1217:2:1:[1175.2,1125.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> microtheory(c_testvocabularymt) {x0 -> c_cyclistsmt}
% 56.33/14.55 === Backtracking. Learning clause 1218:1:0:[1217.1,310.1]:: -> microtheory(c_testvocabularymt)
% 56.33/14.55 === Backtracking. Learning clause 1219:1:0:[1127.1,34.1]:: -> microtheory(c_tptp_member3205_mt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1220:2:1:[1148.2,1125.1]:Top: genlmt(x0,c_tptp_member3205_mt) -> microtheory(c_tptp_spindleheadmt)
% 56.33/14.55 === Backtracking. Learning clause 1221:1:0:[1125.1,34.1]:: -> microtheory(c_tptp_spindleheadmt)
% 56.33/14.55 === Backtracking. Learning clause 1222:1:0:[1127.1,35.1]:: -> microtheory(c_peopledatamt)
% 56.33/14.55 === Conflict found: 1149:2:1:[1128.2,35.1]:Top: genlmt(x0,c_peopledatamt) -> genlmt(x0,c_unitedstatessociallifemt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1223:2:1:[1149.2,1125.1]:Top: genlmt(x0,c_peopledatamt) -> microtheory(c_unitedstatessociallifemt)
% 56.33/14.55 === Backtracking. Learning clause 1224:1:0:[1125.1,35.1]:: -> microtheory(c_unitedstatessociallifemt)
% 56.33/14.55 === Backtracking. Learning clause 1225:2:1:[1128.2,414.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> genlmt(x0,c_gregoriancalendarmt)
% 56.33/14.55 === Backtracking. Learning clause 1226:1:0:[1127.1,52.1]:: -> microtheory(c_miptdatabase19681997_termsmt)
% 56.33/14.55 === Conflict found: 1150:2:1:[1128.2,52.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> genlmt(x0,c_ldscgeneralcollectormt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1227:2:1:[1150.2,1125.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> microtheory(c_ldscgeneralcollectormt)
% 56.33/14.55 === Backtracking. Learning clause 1228:1:0:[1125.1,52.1]:: -> microtheory(c_ldscgeneralcollectormt)
% 56.33/14.55 === Backtracking. Learning clause 1229:2:1:[1128.2,87.1,1125.1,1150.2]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> microtheory(c_ldscdemonstrationspindleheadmt)
% 56.33/14.55 === Backtracking. Learning clause 1230:1:0:[1125.1,87.1]:: -> microtheory(c_ldscdemonstrationspindleheadmt)
% 56.33/14.55 === Backtracking. Learning clause 1231:1:0:[1127.1,53.1]:: -> microtheory(c_ethnicgroupsmt)
% 56.33/14.55 === Conflict found: 1151:2:1:[1128.2,53.1]:Top: genlmt(x0,c_ethnicgroupsmt) -> genlmt(x0,c_ethnicgroupsvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1232:2:1:[1151.2,1125.1]:Top: genlmt(x0,c_ethnicgroupsmt) -> microtheory(c_ethnicgroupsvocabularymt)
% 56.33/14.55 === Backtracking. Learning clause 1233:1:0:[1125.1,53.1]:: -> microtheory(c_ethnicgroupsvocabularymt)
% 56.33/14.55 === Backtracking. Learning clause 1234:2:1:[1128.2,367.1,1125.1,1151.2]:Top: genlmt(x0,c_ethnicgroupsmt) -> microtheory(c_worldcompletedualistgeographymt)
% 56.33/14.55 === Backtracking. Learning clause 1235:1:0:[1125.1,367.1]:: -> microtheory(c_worldcompletedualistgeographymt)
% 56.33/14.55 === Conflict found: 1152:2:1:[1128.1,58.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> genlmt(c_machinelearningspindleheadmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1236:2:1:[1152.2,1127.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> microtheory(c_machinelearningspindleheadmt)
% 56.33/14.55 === Conflict found: 1236:2:1:[1152.2,1127.1]:Top: genlmt(c_miptdatabase19681997_termsmt,x0) -> microtheory(c_machinelearningspindleheadmt) {x0 -> c_ldscgeneralcollectormt}
% 56.33/14.55 === Backtracking. Learning clause 1237:1:0:[1236.1,52.1]:: -> microtheory(c_machinelearningspindleheadmt)
% 56.33/14.55 === Conflict found: 1153:2:1:[1128.2,177.1]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> genlmt(x0,c_cycnounlearnermt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1238:2:1:[1153.2,1125.1]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> microtheory(c_cycnounlearnermt)
% 56.33/14.55 === Backtracking. Learning clause 1239:1:0:[1125.1,177.1]:: -> microtheory(c_cycnounlearnermt)
% 56.33/14.55 === Conflict found: 1170:2:1:[1128.2,269.1]:Top: genlmt(x0,c_cycnounlearnermt) -> genlmt(x0,c_cycorpproductsmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1240:2:1:[1170.2,1125.1,1153.2]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> microtheory(c_cycorpproductsmt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1241:2:1:[1155.2,1127.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> microtheory(c_tptpgeo_member7_mt)
% 56.33/14.55 === Conflict found: 1241:2:1:[1155.2,1127.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> microtheory(c_tptpgeo_member7_mt) {x0 -> c_worldgeographymt}
% 56.33/14.55 === Backtracking. Learning clause 1242:1:0:[1241.1,326.1]:: -> microtheory(c_tptpgeo_member7_mt)
% 56.33/14.55 === Backtracking. Learning clause 1243:1:0:[1127.1,66.1]:: -> microtheory(c_nooescapearchitecturemt)
% 56.33/14.55 === Backtracking. Learning clause 1244:1:0:[1127.1,88.1]:: -> microtheory(c_patterndetectormt)
% 56.33/14.55 === Conflict found: 1158:2:1:[1128.1,206.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_universalvocabularymt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1245:2:1:[1158.2,1127.1]:Top: genlmt(c_basekb,x0) -> microtheory(c_universalvocabularymt)
% 56.33/14.55 === Backtracking. Learning clause 1246:1:0:[1127.1,206.1]:: -> microtheory(c_universalvocabularymt)
% 56.33/14.55 === Conflict found: 1159:2:1:[1128.2,92.1]:Top: genlmt(x0,c_universalvocabularymt) -> genlmt(x0,c_corecyclmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1247:2:1:[1159.2,1125.1]:Top: genlmt(x0,c_universalvocabularymt) -> microtheory(c_corecyclmt)
% 56.33/14.55 === Backtracking. Learning clause 1248:1:0:[1125.1,92.1]:: -> microtheory(c_corecyclmt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1249:2:1:[1160.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member2831_mt)
% 56.33/14.55 === Backtracking. Learning clause 1250:2:1:[1128.1,254.1,1249.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2831_mt)
% 56.33/14.55 === Conflict found: 1250:2:1:[1128.1,254.1,1249.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2831_mt) {x0 -> c_calendarsmt}
% 56.33/14.55 === Backtracking. Learning clause 1251:1:0:[1250.1,115.1]:: -> microtheory(c_tptp_member2831_mt)
% 56.33/14.55 === Backtracking. Learning clause 1252:2:1:[1128.2,378.1,1125.1,1146.2]:Top: genlmt(x0,c_cyclistsmt) -> microtheory(c_calendarsvocabularymt)
% 56.33/14.55 === Conflict found: 1252:2:1:[1128.2,378.1,1125.1,1146.2]:Top: genlmt(x0,c_cyclistsmt) -> microtheory(c_calendarsvocabularymt) {x0 -> c_tptp_spindleheadmt}
% 56.33/14.55 === Backtracking. Learning clause 1253:1:0:[1252.1,254.1]:: -> microtheory(c_calendarsvocabularymt)
% 56.33/14.55 === Backtracking. Learning clause 1254:1:0:[1128.2,334.1,1125.1,1190.2,1.1]:: -> microtheory(c_geographymt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1255:2:1:[1161.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3393_mt)
% 56.33/14.55 === Backtracking. Learning clause 1256:2:1:[1128.1,254.1,1255.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3393_mt)
% 56.33/14.55 === Conflict found: 1256:2:1:[1128.1,254.1,1255.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3393_mt) {x0 -> c_calendarsmt}
% 56.33/14.55 === Backtracking. Learning clause 1257:1:0:[1256.1,115.1]:: -> microtheory(c_tptp_member3393_mt)
% 56.33/14.55 === Conflict found: 1162:2:1:[1128.1,136.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_generictemporalmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1258:2:1:[1162.2,1127.1]:Top: genlmt(c_basekb,x0) -> microtheory(c_generictemporalmt)
% 56.33/14.55 === Backtracking. Learning clause 1259:1:0:[1127.1,136.1]:: -> microtheory(c_generictemporalmt)
% 56.33/14.55 === Conflict found: 1163:2:1:[1128.1,137.1]:Top: genlmt(c_worldgeographymt,x0) -> genlmt(c_worldgeographydualistmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1260:2:1:[1163.2,1127.1]:Top: genlmt(c_worldgeographymt,x0) -> microtheory(c_worldgeographydualistmt)
% 56.33/14.55 === Conflict found: 1260:2:1:[1163.2,1127.1]:Top: genlmt(c_worldgeographymt,x0) -> microtheory(c_worldgeographydualistmt) {x0 -> c_geographymt}
% 56.33/14.55 === Backtracking. Learning clause 1261:1:0:[1260.1,334.1]:: -> microtheory(c_worldgeographydualistmt)
% 56.33/14.55 === Backtracking. Learning clause 1262:1:0:[1127.1,369.1]:: -> microtheory(c_tptpgeo_spindlecollectormt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1263:2:1:[1166.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3515_mt)
% 56.33/14.55 === Backtracking. Learning clause 1264:2:1:[1128.1,254.1,1263.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3515_mt)
% 56.33/14.55 === Conflict found: 1264:2:1:[1128.1,254.1,1263.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3515_mt) {x0 -> c_calendarsmt}
% 56.33/14.55 === Backtracking. Learning clause 1265:1:0:[1264.1,115.1]:: -> microtheory(c_tptp_member3515_mt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1266:2:1:[1169.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member2089_mt)
% 56.33/14.55 === Backtracking. Learning clause 1267:2:1:[1128.1,254.1,1266.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2089_mt)
% 56.33/14.55 === Conflict found: 1267:2:1:[1128.1,254.1,1266.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member2089_mt) {x0 -> c_calendarsmt}
% 56.33/14.55 === Backtracking. Learning clause 1268:1:0:[1267.1,115.1]:: -> microtheory(c_tptp_member2089_mt)
% 56.33/14.55 === Backtracking. Learning clause 1269:1:0:[1125.1,269.1]:: -> microtheory(c_cycorpproductsmt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1270:2:1:[1171.2,1127.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> microtheory(c_tptpgeo_member3_mt)
% 56.33/14.55 === Conflict found: 1270:2:1:[1171.2,1127.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> microtheory(c_tptpgeo_member3_mt) {x0 -> c_worldgeographymt}
% 56.33/14.55 === Backtracking. Learning clause 1271:1:0:[1270.1,326.1]:: -> microtheory(c_tptpgeo_member3_mt)
% 56.33/14.55 === Conflict found: 1172:2:1:[1128.1,214.1]:Top: genlmt(c_generictemporalmt,x0) -> genlmt(c_timehasnoendmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1272:2:1:[1172.2,1127.1,1162.2]:Top: genlmt(c_basekb,x0) -> microtheory(c_timehasnoendmt)
% 56.33/14.55 === Backtracking. Learning clause 1273:1:0:[1127.1,214.1]:: -> microtheory(c_timehasnoendmt)
% 56.33/14.55 === Backtracking. Learning clause 1274:1:0:[1127.1,329.1]:: -> microtheory(c_massmediadatamt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1275:2:1:[1173.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3633_mt)
% 56.33/14.55 === Backtracking. Learning clause 1276:2:1:[1128.1,254.1,1275.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3633_mt)
% 56.33/14.55 === Conflict found: 1276:2:1:[1128.1,254.1,1275.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3633_mt) {x0 -> c_calendarsmt}
% 56.33/14.55 === Backtracking. Learning clause 1277:1:0:[1276.1,115.1]:: -> microtheory(c_tptp_member3633_mt)
% 56.33/14.55 === Conflict found: 1174:2:1:[1128.1,248.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member974_mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1278:2:1:[1174.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member974_mt)
% 56.33/14.55 === Backtracking. Learning clause 1279:2:1:[1128.1,254.1,1278.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member974_mt)
% 56.33/14.55 === Conflict found: 1279:2:1:[1128.1,254.1,1278.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member974_mt) {x0 -> c_calendarsmt}
% 56.33/14.55 === Backtracking. Learning clause 1280:1:0:[1279.1,115.1]:: -> microtheory(c_tptp_member974_mt)
% 56.33/14.55 === Conflict found: 1177:2:1:[1128.1,272.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_humansociallifemt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1281:2:1:[1177.2,1127.1]:Top: genlmt(c_basekb,x0) -> microtheory(c_humansociallifemt)
% 56.33/14.55 === Backtracking. Learning clause 1282:1:0:[1127.1,272.1]:: -> microtheory(c_humansociallifemt)
% 56.33/14.55 === Conflict found: 1178:2:1:[1128.1,274.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_knowledgefragmentd3mt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1283:2:1:[1178.2,1127.1]:Top: genlmt(c_basekb,x0) -> microtheory(c_knowledgefragmentd3mt)
% 56.33/14.55 === Backtracking. Learning clause 1284:1:0:[1127.1,274.1]:: -> microtheory(c_knowledgefragmentd3mt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1285:2:1:[1179.2,1127.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> microtheory(c_tptp_member3717_mt)
% 56.33/14.55 === Backtracking. Learning clause 1286:2:1:[1128.1,254.1,1285.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3717_mt)
% 56.33/14.55 === Conflict found: 1286:2:1:[1128.1,254.1,1285.1]:Top: genlmt(c_cyclistsmt,x0) -> microtheory(c_tptp_member3717_mt) {x0 -> c_calendarsmt}
% 56.33/14.55 === Backtracking. Learning clause 1287:1:0:[1286.1,115.1]:: -> microtheory(c_tptp_member3717_mt)
% 56.33/14.55 === Conflict found: 1196:2:1:[1128.1,333.1]:Top: genlmt(c_humansociallifemt,x0) -> genlmt(c_reasoningaboutpossibleantecedentsmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1288:2:1:[1196.2,1127.1,1177.2]:Top: genlmt(c_basekb,x0) -> microtheory(c_reasoningaboutpossibleantecedentsmt)
% 56.33/14.55 === Backtracking. Learning clause 1289:1:0:[1127.1,333.1]:: -> microtheory(c_reasoningaboutpossibleantecedentsmt)
% 56.33/14.55 === Backtracking. Learning clause 1290:1:0:[1127.1,384.1]:: -> microtheory(c_unitedstatesgeographypeoplemt)
% 56.33/14.55 === Backtracking. Learning clause 1291:2:1:[1128.1,384.1]:Top: genlmt(c_peopledatamt,x0) -> genlmt(c_unitedstatesgeographypeoplemt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1292:2:2:[174.2,409.1]:TopTop: tptptypes_8_400(x0,x1) -> tptptypes_6_388(x0,x1)
% 56.33/14.55 === Backtracking. Learning clause 1293:2:2:[427.2,271.1]:TopTop: tptptypes_9_824(x0,x1) -> tptptypes_7_819(x0,x1)
% 56.33/14.55 === Backtracking. Learning clause 1294: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)
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 380
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1295:1:0:[205.1,475.1]:: -> fixedordercollection(c_tptpcol_16_62187)
% 56.33/14.55 === Backtracking. Learning clause 1296:2:1:[211.1,494.2]:Top: computerdataartifact(x0) -> inanimateobject_nonnatural(x0)
% 56.33/14.55 === Backtracking. Learning clause 1297:2:1:[437.2,312.1,225.2,1205.2]:Top: tptpcol_7_72707(x0) -> tptpcol_2_65537(x0)
% 56.33/14.55 === Backtracking. Learning clause 1298:2:1:[437.2,312.1]:Top: tptpcol_4_65539(x0) -> tptpcol_2_65537(x0)
% 56.33/14.55 === Backtracking. Learning clause 1299:2:1:[314.2,466.1]:Top: tptpcol_14_26921(x0) -> tptpcol_12_26919(x0)
% 56.33/14.55 === Backtracking. Learning clause 1300:2:1:[457.2,336.1]:Top: tptpcol_7_21508(x0) -> tptpcol_5_20483(x0)
% 56.33/14.55 === Backtracking. Learning clause 1301:2:1:[341.2,459.1]:Top: tptpcol_7_108547(x0) -> tptpcol_5_106498(x0)
% 56.33/14.55 === Backtracking. Learning clause 1302:2:1:[484.1,354.2]:Top: tptpcol_8_18438(x0) -> tptpcol_6_18436(x0)
% 56.33/14.55 === Backtracking. Learning clause 1303:2:1:[394.2,490.1]:Top: tptpcol_6_112641(x0) -> tptpcol_4_106497(x0)
% 56.33/14.55 === Backtracking. Learning clause 1304:2:1:[396.2,450.1]:Top: tptpcol_12_72775(x0) -> tptpcol_10_72710(x0)
% 56.33/14.55 === Backtracking. Learning clause 1305:2:1:[432.2,481.1]:Top: tptpcol_16_26926(x0) -> tptpcol_14_26921(x0)
% 56.33/14.55 === Backtracking. Learning clause 1306:2:0:[462.1,464.2]:: mtvisible(c_worldgeographymt) -> geographicalregion(c_georegion_l4_x75_y75)
% 56.33/14.55 === Backtracking. Learning clause 1307:2:1:[468.2,474.1]:Top: tptpcol_14_92264(x0) -> tptpcol_12_92262(x0)
% 56.33/14.55 === Conflict found: 1156:2:1:[1128.2,66.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_organizationdatamt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1308:2:1:[1156.2,1125.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> microtheory(c_organizationdatamt)
% 56.33/14.55 === Conflict found: 1157:2:1:[1128.2,88.1]:Top: genlmt(x0,c_patterndetectormt) -> genlmt(x0,c_basekb) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1309:2:1:[1157.2,1125.1]:Top: genlmt(x0,c_patterndetectormt) -> microtheory(c_basekb)
% 56.33/14.55 === Conflict found: 1197:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1310:2:1:[1197.2,1125.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> microtheory(c_unitedstatesgeographydualistmt)
% 56.33/14.55 === Conflict found: 1225:2:1:[1128.2,414.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> genlmt(x0,c_gregoriancalendarmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1311:2:1:[1225.2,1125.1,1149.2]:Top: genlmt(x0,c_peopledatamt) -> microtheory(c_gregoriancalendarmt)
% 56.33/14.55 === Backtracking. Learning clause 1312:2:1:[1128.2,453.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member1672_mt)
% 56.33/14.55 === Backtracking. Learning clause 1313:2:1:[1128.2,448.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member698_mt)
% 56.33/14.55 === Backtracking. Learning clause 1314:1:0:[1125.1,414.1]:: -> microtheory(c_gregoriancalendarmt)
% 56.33/14.55 === Conflict found: 1310:2:1:[1197.2,1125.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> microtheory(c_unitedstatesgeographydualistmt) {x0 -> c_ethnicgroupsvocabularymt}
% 56.33/14.55 === Backtracking. Learning clause 1315:1:0:[1310.1,367.1]:: -> microtheory(c_unitedstatesgeographydualistmt)
% 56.33/14.55 === Backtracking. Learning clause 1316:1:0:[1125.1,66.1]:: -> microtheory(c_organizationdatamt)
% 56.33/14.55 === Backtracking. Learning clause 1317:1:0:[1125.1,88.1]:: -> microtheory(c_basekb)
% 56.33/14.55 === Backtracking. Learning clause 1318:2:1:[1128.1,454.1]:Top: genlmt(c_worldgeographydualistmt,x0) -> genlmt(c_unitedstatesgeographydualistmt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1319:2:1:[1128.1,469.1]:Top: genlmt(c_basekb,x0) -> genlmt(c_gregoriancalendarmt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1320:1:0:[1127.1,446.1]:: -> microtheory(c_tptp_member2356_mt)
% 56.33/14.55 === Backtracking. Learning clause 1321:2:1:[1128.1,446.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2356_mt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1322:1:0:[1127.1,479.1]:: -> microtheory(c_tptp_member2862_mt)
% 56.33/14.55 === Backtracking. Learning clause 1323:2:1:[1128.1,479.1]:Top: genlmt(c_tptp_spindleheadmt,x0) -> genlmt(c_tptp_member2862_mt,x0)
% 56.33/14.55 === Backtracking. Learning clause 1324:2:1:[1128.2,486.1,1181.1]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,c_massmediadatamt)
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 445
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1325:1:0:[515.2,1133.1]:: tptpcol_15_4027(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1326:1:0:[513.2,1133.1]:: geolevel_4(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1327:1:0:[511.2,1133.1]:: tptpcol_13_92263(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1328:1:0:[509.2,1133.1]:: tptpcol_16_62187(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1329:1:0:[507.2,1133.1]:: tptpcol_16_26939(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1330:1:0:[502.2,1133.1]:: tptpcol_14_118118(c_wanica_districtsuriname) ->
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 513
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1331:1:0:[529.2,1133.1]:: tptpcol_15_22076(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1332:1:0:[527.2,1133.1]:: pushingwithopenhand(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1333:1:0:[525.2,1133.1]:: tptpcol_16_4451(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1334:1:0:[523.2,1133.1]:: footballteam(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1335:1:0:[517.2,1133.1]:: pushingwithfingers(c_wanica_districtsuriname) ->
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 579
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1336:1:0:[544.2,1133.1]:: tptpcol_5_90114(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1337:1:0:[542.2,1133.1]:: tptpcol_13_118117(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1338:1:0:[540.2,1133.1]:: tptpcol_16_26926(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1339:1:0:[538.2,1133.1]:: tptpcol_15_26925(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1340:1:0:[536.2,1133.1]:: tptpcol_8_39940(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1341:1:0:[534.2,1133.1]:: tptpcol_7_39939(c_wanica_districtsuriname) ->
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 644
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1342:1:0:[556.2,1133.1]:: tptpcol_6_71683(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1343:1:0:[554.2,1133.1]:: tptpcol_16_50958(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1344:1:0:[552.2,1133.1]:: tptpcol_15_50957(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1345:1:0:[550.2,1133.1]:: tptpcol_8_114177(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1346:1:0:[548.2,1133.1]:: tptpcol_16_72795(c_wanica_districtsuriname) ->
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 709
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1347:1:0:[570.2,1133.1]:: tptpcol_10_93700(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1348:1:0:[568.2,1133.1]:: tptpcol_4_90113(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1349:1:0:[564.2,1133.1]:: tptpcol_16_25972(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1350:1:0:[562.2,1133.1]:: tptpcol_5_110593(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1351:1:0:[560.2,1133.1]:: tptpcol_12_72775(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1352:1:0:[558.2,1133.1]:: tptpcol_11_72774(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1353:2:1:[565.1,391.2]:Top: shavingrazor_manual(x0) -> razor(x0)
% 56.33/14.55 === Backtracking. Learning clause 1354: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))
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 776
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1355:1:0:[582.2,1133.1]:: tptpcol_6_18436(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1356:1:0:[578.2,1133.1]:: tptpcol_8_117763(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1357:1:0:[576.2,1133.1]:: tptpcol_7_117762(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1358:1:0:[574.2,1133.1]:: aspatialthing(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1359:1:0:[572.2,1133.1]:: tptpcol_9_93699(c_wanica_districtsuriname) ->
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 910
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1360:2:0:[1123.2,1.1]:: mtvisible(c_tptpgeo_member8_mt) -> mtvisible(c_tptpgeo_spindleheadmt)
% 56.33/14.55 === Conflict found: 1144:2:1:[1128.2,20.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2610_mt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1361:2:1:[1144.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member2610_mt)
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1362:3:1:[1148.2,1123.2]:Top: genlmt(x0,c_tptp_member3205_mt),mtvisible(x0) -> mtvisible(c_tptp_spindleheadmt)
% 56.33/14.55 === Conflict found: 1149:2:1:[1128.2,35.1]:Top: genlmt(x0,c_peopledatamt) -> genlmt(x0,c_unitedstatessociallifemt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1363:3:1:[1149.2,1123.2]:Top: genlmt(x0,c_peopledatamt),mtvisible(x0) -> mtvisible(c_unitedstatessociallifemt)
% 56.33/14.55 === Conflict found: 1150:2:1:[1128.2,52.1]:Top: genlmt(x0,c_miptdatabase19681997_termsmt) -> genlmt(x0,c_ldscgeneralcollectormt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1364:3:1:[1150.2,1123.2]:Top: genlmt(x0,c_miptdatabase19681997_termsmt),mtvisible(x0) -> mtvisible(c_ldscgeneralcollectormt)
% 56.33/14.55 === Conflict found: 1151:2:1:[1128.2,53.1]:Top: genlmt(x0,c_ethnicgroupsmt) -> genlmt(x0,c_ethnicgroupsvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1365:3:1:[1151.2,1123.2]:Top: genlmt(x0,c_ethnicgroupsmt),mtvisible(x0) -> mtvisible(c_ethnicgroupsvocabularymt)
% 56.33/14.55 === Conflict found: 1154:2:1:[1128.2,59.1]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt) -> genlmt(x0,c_currentworlddatacollectormt_nonhomocentric) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1366:2:1:[1154.2,1125.1]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt) -> microtheory(c_currentworlddatacollectormt_nonhomocentric)
% 56.33/14.55 === Conflict found: 1156:2:1:[1128.2,66.1]:Top: genlmt(x0,c_nooescapearchitecturemt) -> genlmt(x0,c_organizationdatamt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1367:3:1:[1156.2,1123.2]:Top: genlmt(x0,c_nooescapearchitecturemt),mtvisible(x0) -> mtvisible(c_organizationdatamt)
% 56.33/14.55 === Conflict found: 1146:2:1:[1128.2,115.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_calendarsmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1368:3:1:[1146.2,1123.2]:Top: genlmt(x0,c_cyclistsmt),mtvisible(x0) -> mtvisible(c_calendarsmt)
% 56.33/14.55 === Conflict found: 1153:2:1:[1128.2,177.1]:Top: genlmt(x0,c_machinelearningspindleheadmt) -> genlmt(x0,c_cycnounlearnermt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1369:3:1:[1153.2,1123.2]:Top: genlmt(x0,c_machinelearningspindleheadmt),mtvisible(x0) -> mtvisible(c_cycnounlearnermt)
% 56.33/14.55 === Conflict found: 1175:2:1:[1128.2,257.1]:Top: genlmt(x0,c_keinteractionresourcetestmt) -> genlmt(x0,c_testvocabularymt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1370:3:1:[1175.2,1123.2]:Top: genlmt(x0,c_keinteractionresourcetestmt),mtvisible(x0) -> mtvisible(c_testvocabularymt)
% 56.33/14.55 === Conflict found: 1197:2:1:[1128.2,339.1]:Top: genlmt(x0,c_worldcompletedualistgeographymt) -> genlmt(x0,c_unitedstatesgeographydualistmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1371:3:1:[1197.2,1123.2]:Top: genlmt(x0,c_worldcompletedualistgeographymt),mtvisible(x0) -> mtvisible(c_unitedstatesgeographydualistmt)
% 56.33/14.55 === Conflict found: 1193:2:1:[1128.2,358.1]:Top: genlmt(x0,c_corecyclmt) -> genlmt(x0,c_logicaltruthmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1372:2:1:[1193.2,1125.1,1159.2]:Top: genlmt(x0,c_universalvocabularymt) -> microtheory(c_logicaltruthmt)
% 56.33/14.55 === Backtracking. Learning clause 1373:2:0:[1123.2,20.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member2610_mt)
% 56.33/14.55 === Backtracking. Learning clause 1374:1:0:[1125.1,20.1]:: -> microtheory(c_tptp_member2610_mt)
% 56.33/14.55 === Conflict found: 1312:2:1:[1128.2,453.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member1672_mt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1375:2:1:[1312.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member1672_mt)
% 56.33/14.55 === Backtracking. Learning clause 1376:2:0:[1123.2,453.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member1672_mt)
% 56.33/14.55 === Backtracking. Learning clause 1377:1:0:[1125.1,453.1]:: -> microtheory(c_tptp_member1672_mt)
% 56.33/14.55 === Conflict found: 1209:2:1:[1128.2,419.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member235_mt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1378:2:1:[1209.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member235_mt)
% 56.33/14.55 === Backtracking. Learning clause 1379:2:0:[1123.2,419.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member235_mt)
% 56.33/14.55 === Backtracking. Learning clause 1380:1:0:[1125.1,419.1]:: -> microtheory(c_tptp_member235_mt)
% 56.33/14.55 === Conflict found: 1145:2:1:[1128.2,198.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member237_mt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1381:2:1:[1145.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member237_mt)
% 56.33/14.55 === Backtracking. Learning clause 1382:2:0:[1123.2,198.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member237_mt)
% 56.33/14.55 === Backtracking. Learning clause 1383:1:0:[1125.1,198.1]:: -> microtheory(c_tptp_member237_mt)
% 56.33/14.55 === Conflict found: 1191:2:1:[1128.2,350.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2668_mt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1384:2:1:[1191.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member2668_mt)
% 56.33/14.55 === Backtracking. Learning clause 1385:2:0:[1123.2,350.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member2668_mt)
% 56.33/14.55 === Backtracking. Learning clause 1386:1:0:[1125.1,350.1]:: -> microtheory(c_tptp_member2668_mt)
% 56.33/14.55 === Conflict found: 1192:2:1:[1128.2,344.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member2701_mt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1387:2:1:[1192.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member2701_mt)
% 56.33/14.55 === Backtracking. Learning clause 1388:2:0:[1123.2,344.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member2701_mt)
% 56.33/14.55 === Backtracking. Learning clause 1389:1:0:[1125.1,344.1]:: -> microtheory(c_tptp_member2701_mt)
% 56.33/14.55 === Conflict found: 1313:2:1:[1128.2,448.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> genlmt(x0,c_tptp_member698_mt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1390:2:1:[1313.2,1125.1]:Top: genlmt(x0,c_tptp_spindlecollectormt) -> microtheory(c_tptp_member698_mt)
% 56.33/14.55 === Backtracking. Learning clause 1391:2:0:[1123.2,448.1]:: mtvisible(c_tptp_spindlecollectormt) -> mtvisible(c_tptp_member698_mt)
% 56.33/14.55 === Backtracking. Learning clause 1392:1:0:[1125.1,448.1]:: -> microtheory(c_tptp_member698_mt)
% 56.33/14.55 === Backtracking. Learning clause 1393:2:0:[1123.2,115.1]:: mtvisible(c_cyclistsmt) -> mtvisible(c_calendarsmt)
% 56.33/14.55 === Conflict found: 1147:2:1:[1128.2,125.1]:Top: genlmt(x0,c_cyclistsmt) -> genlmt(x0,c_hpkbvocabmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1394:2:1:[1147.2,1125.1]:Top: genlmt(x0,c_cyclistsmt) -> microtheory(c_hpkbvocabmt)
% 56.33/14.55 === Backtracking. Learning clause 1395:2:0:[1123.2,125.1]:: mtvisible(c_cyclistsmt) -> mtvisible(c_hpkbvocabmt)
% 56.33/14.55 === Backtracking. Learning clause 1396:1:0:[1125.1,125.1]:: -> microtheory(c_hpkbvocabmt)
% 56.33/14.55 === Conflict found: 1370:3:1:[1175.2,1123.2]:Top: genlmt(x0,c_keinteractionresourcetestmt),mtvisible(x0) -> mtvisible(c_testvocabularymt) {x0 -> c_cyclistsmt}
% 56.33/14.55 === Backtracking. Learning clause 1397:2:0:[1370.1,310.1]:: mtvisible(c_cyclistsmt) -> mtvisible(c_testvocabularymt)
% 56.33/14.55 === Backtracking. Learning clause 1398:2:0:[1123.2,34.1]:: mtvisible(c_tptp_member3205_mt) -> mtvisible(c_tptp_spindleheadmt)
% 56.33/14.55 === Backtracking. Learning clause 1399:2:0:[1123.2,35.1]:: mtvisible(c_peopledatamt) -> mtvisible(c_unitedstatessociallifemt)
% 56.33/14.55 === Conflict found: 1225:2:1:[1128.2,414.1]:Top: genlmt(x0,c_unitedstatessociallifemt) -> genlmt(x0,c_gregoriancalendarmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1400:3:1:[1225.2,1123.2,1149.2]:Top: mtvisible(x0),genlmt(x0,c_peopledatamt) -> mtvisible(c_gregoriancalendarmt)
% 56.33/14.55 === Backtracking. Learning clause 1401:2:0:[1123.2,414.1]:: mtvisible(c_unitedstatessociallifemt) -> mtvisible(c_gregoriancalendarmt)
% 56.33/14.55 === Backtracking. Learning clause 1402:2:0:[1123.2,52.1]:: mtvisible(c_miptdatabase19681997_termsmt) -> mtvisible(c_ldscgeneralcollectormt)
% 56.33/14.55 === Conflict found: 1366:2:1:[1154.2,1125.1]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt) -> microtheory(c_currentworlddatacollectormt_nonhomocentric) {x0 -> c_ldscgeneralcollectormt}
% 56.33/14.55 === Backtracking. Learning clause 1403:1:0:[1366.1,87.1]:: -> microtheory(c_currentworlddatacollectormt_nonhomocentric)
% 56.33/14.55 === Conflict found: 1154:2:1:[1128.2,59.1]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt) -> genlmt(x0,c_currentworlddatacollectormt_nonhomocentric) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1404:3:1:[1154.2,1123.2]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt),mtvisible(x0) -> mtvisible(c_currentworlddatacollectormt_nonhomocentric)
% 56.33/14.55 === Conflict found: 1404:3:1:[1154.2,1123.2]:Top: genlmt(x0,c_ldscdemonstrationspindleheadmt),mtvisible(x0) -> mtvisible(c_currentworlddatacollectormt_nonhomocentric) {x0 -> c_ldscgeneralcollectormt}
% 56.33/14.55 === Backtracking. Learning clause 1405:2:0:[1404.1,87.1]:: mtvisible(c_ldscgeneralcollectormt) -> mtvisible(c_currentworlddatacollectormt_nonhomocentric)
% 56.33/14.55 === Backtracking. Learning clause 1406:2:0:[1123.2,53.1]:: mtvisible(c_ethnicgroupsmt) -> mtvisible(c_ethnicgroupsvocabularymt)
% 56.33/14.55 === Conflict found: 1371:3:1:[1197.2,1123.2]:Top: genlmt(x0,c_worldcompletedualistgeographymt),mtvisible(x0) -> mtvisible(c_unitedstatesgeographydualistmt) {x0 -> c_ethnicgroupsvocabularymt}
% 56.33/14.55 === Backtracking. Learning clause 1407:2:0:[1371.1,367.1]:: mtvisible(c_ethnicgroupsvocabularymt) -> mtvisible(c_unitedstatesgeographydualistmt)
% 56.33/14.55 === Backtracking. Learning clause 1408:2:0:[1123.2,177.1]:: mtvisible(c_machinelearningspindleheadmt) -> mtvisible(c_cycnounlearnermt)
% 56.33/14.55 === Conflict found: 1170:2:1:[1128.2,269.1]:Top: genlmt(x0,c_cycnounlearnermt) -> genlmt(x0,c_cycorpproductsmt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1409:3:1:[1170.2,1123.2,1153.2]:Top: mtvisible(x0),genlmt(x0,c_machinelearningspindleheadmt) -> mtvisible(c_cycorpproductsmt)
% 56.33/14.55 === Backtracking. Learning clause 1410:2:0:[1123.2,66.1]:: mtvisible(c_nooescapearchitecturemt) -> mtvisible(c_organizationdatamt)
% 56.33/14.55 === Conflict found: 1324:2:1:[1128.2,486.1,1181.1]:Top: genlmt(x0,c_organizationdatamt) -> genlmt(x0,c_massmediadatamt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1411:3:1:[1324.2,1123.2,1156.2]:Top: mtvisible(x0),genlmt(x0,c_nooescapearchitecturemt) -> mtvisible(c_massmediadatamt)
% 56.33/14.55 === Conflict found: 1372:2:1:[1193.2,1125.1,1159.2]:Top: genlmt(x0,c_universalvocabularymt) -> microtheory(c_logicaltruthmt) {x0 -> c_basekb}
% 56.33/14.55 === Backtracking. Learning clause 1412:1:0:[1372.1,455.1]:: -> microtheory(c_logicaltruthmt)
% 56.33/14.55 === Backtracking. Learning clause 1413:2:0:[1123.2,273.1]:: mtvisible(c_tptpgeo_spindlecollectormt) -> mtvisible(c_tptpgeo_member2_mt)
% 56.33/14.55 === Backtracking. Learning clause 1414:1:0:[1125.1,273.1]:: -> microtheory(c_tptpgeo_member2_mt)
% 56.33/14.55 === Backtracking. Learning clause 1415:1:0:[1125.1,407.1]:: -> microtheory(c_tptpgeo_member5_mt)
% 56.33/14.55 === Backtracking. Learning clause 1416:1:0:[1125.1,140.1]:: -> microtheory(c_tptpgeo_member1_mt)
% 56.33/14.55 === Backtracking. Learning clause 1417:2:0:[1123.2,269.1]:: mtvisible(c_cycnounlearnermt) -> mtvisible(c_cycorpproductsmt)
% 56.33/14.55 === Conflict found: 1411:3:1:[1324.2,1123.2,1156.2]:Top: mtvisible(x0),genlmt(x0,c_nooescapearchitecturemt) -> mtvisible(c_massmediadatamt) {x0 -> c_testvocabularymt}
% 56.33/14.55 === Backtracking. Learning clause 1418:2:0:[1411.2,275.1,1397.2]:: mtvisible(c_cyclistsmt) -> mtvisible(c_massmediadatamt)
% 56.33/14.55 === Backtracking. Learning clause 1419:1:0:[590.2,1133.1]:: tptpcol_6_20484(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1420:1:0:[588.2,1133.1]:: tptpcol_6_108546(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1421:1:0:[586.2,1133.1]:: tptpcol_11_109125(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1422:1:0:[584.2,1133.1]:: tptpcol_8_93698(c_wanica_districtsuriname) ->
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 976
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1423:1:0:[605.2,1133.1]:: tptpcol_16_130924(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1424:1:0:[603.2,1133.1]:: tptpcol_15_130923(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1425:1:0:[601.2,1133.1]:: tptpcol_7_92163(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1426:1:0:[599.2,1133.1]:: tptpcol_16_130933(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1427:1:0:[597.2,1133.1]:: tptpcol_15_130931(c_wanica_districtsuriname) ->
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 1042
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1428:1:0:[619.2,1133.1]:: tptpcol_16_27189(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1429:1:0:[617.2,1133.1]:: tptpcol_3_65538(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1430:1:0:[615.2,1133.1]:: tptpcol_14_26921(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1431:1:0:[613.2,1133.1]:: tptpcol_13_26920(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1432:1:0:[607.2,1133.1]:: intangibleindividual(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1433:1:0:[623.2,1133.1]:: reflexivebinarypredicate(c_wanica_districtsuriname) ->
% 56.33/14.55 === Clause set with instances from active satisfied. Growing active. New size: 1344
% 56.33/14.55 === Restarting.
% 56.33/14.55 === Backtracking. Learning clause 1434:1:0:[457.2,1419.1]:: tptpcol_7_21508(c_wanica_districtsuriname) ->
% 56.33/14.55 === Backtracking. Learning clause 1435:1:0:[1108.1,111.1]:: -> collection(c_setorcollection)
% 56.33/14.55 === Backtracking. Learning clause 1436:1:0:[1106.1,150.1]:: -> collection(c_collection)
% 56.33/14.55 === Backtracking. Learning clause 1437:1:0:[629.2,1133.1,321.2]:: mtvisible(c_worldgeographymt) ->
% 56.33/14.55 === Conflict found: 1190:2:1:[1128.2,326.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_worldgeographymt) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1438:1:0:[1190.2,1123.2,1.1,1437.1]:: mtvisible(c_tptpgeo_member8_mt) ->
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1439:3:1:[1155.2,1123.2]:Top: genlmt(c_tptpgeo_spindleheadmt,x0),mtvisible(c_tptpgeo_member7_mt) -> mtvisible(x0)
% 56.33/14.55 === Conflict found: 1439:3:1:[1155.2,1123.2]:Top: genlmt(c_tptpgeo_spindleheadmt,x0),mtvisible(c_tptpgeo_member7_mt) -> mtvisible(x0) {x0 -> c_worldgeographymt}
% 56.33/14.55 === Backtracking. Learning clause 1440:1:0:[1439.1,326.1,1437.1]:: mtvisible(c_tptpgeo_member7_mt) ->
% 56.33/14.55 === Conflict found: 1163:2:1:[1128.1,137.1]:Top: genlmt(c_worldgeographymt,x0) -> genlmt(c_worldgeographydualistmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1441:3:1:[1163.2,1123.2]:Top: genlmt(c_worldgeographymt,x0),mtvisible(c_worldgeographydualistmt) -> mtvisible(x0)
% 56.33/14.55 === Backtracking. Learning clause 1443:1:0:[1437.0,1442.1,1123.2,137.1]:: mtvisible(c_worldgeographydualistmt) ->
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1444:3:1:[1171.2,1123.2]:Top: genlmt(c_tptpgeo_spindleheadmt,x0),mtvisible(c_tptpgeo_member3_mt) -> mtvisible(x0)
% 56.33/14.55 === Conflict found: 1444:3:1:[1171.2,1123.2]:Top: genlmt(c_tptpgeo_spindleheadmt,x0),mtvisible(c_tptpgeo_member3_mt) -> mtvisible(x0) {x0 -> c_worldgeographymt}
% 56.33/14.55 === Backtracking. Learning clause 1446:1:0:[1437.0,1445.1,1444.1,326.1]:: mtvisible(c_tptpgeo_member3_mt) ->
% 56.33/14.55 === Conflict found: 1318:2:1:[1128.1,454.1]:Top: genlmt(c_worldgeographydualistmt,x0) -> genlmt(c_unitedstatesgeographydualistmt,x0) {x0 -> c_tptpgeo_member8_mt}
% 56.33/14.55 === Backtracking. Learning clause 1447:3:1:[1318.2,1123.2,1163.2]:Top: mtvisible(c_unitedstatesgeographydualistmt),genlmt(c_worldgeographymt,x0) -> mtvisible(x0)
% 56.33/14.55 === Backtracking. Learning clause 1448:1:0:[1123.2,454.1,1407.2,1443.1,1406.2]:: mtvisible(c_ethnicgroupsmt) ->
% 56.33/14.55 === Conflict found: 1365:3:1:[1151.2,1123.2]:Top: genlmt(x0,c_ethnicgroupsmt),mtvisible(x0) -> mtvisible(c_ethnicgroupsvocabularymt) {x0 -> c_massmediadatamt}
% 56.33/14.55 === Backtracking. Learning clause 1449:2:0:[1365.1,329.1,1418.2]:: mtvisible(c_cyclistsmt) -> mtvisible(c_ethnicgroupsvocabularymt)
% 56.33/14.55 === Backtracking. Learning clause 1450:1:0:[1123.2,329.1,1418.2,1448.1]:: mtvisible(c_cyclistsmt) ->
% 56.33/14.55 === Backtracking. Learning clause 1452:1:0:[1450.0,1451.1,1123.2,254.1,1398.2]:: mtvisible(c_tptp_member3205_mt) ->
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1453:3:1:[1160.2,1123.2]:Top: genlmt(c_tptp_spindleheadmt,x0),mtvisible(c_tptp_member2831_mt) -> mtvisible(x0)
% 56.33/14.55 === Conflict found: 1453:3:1:[1160.2,1123.2]:Top: genlmt(c_tptp_spindleheadmt,x0),mtvisible(c_tptp_member2831_mt) -> mtvisible(x0) {x0 -> c_cyclistsmt}
% 56.33/14.55 === Backtracking. Learning clause 1455:1:0:[1450.0,1454.1,1453.1,254.1]:: mtvisible(c_tptp_member2831_mt) ->
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1456:3:1:[1161.2,1123.2]:Top: genlmt(c_tptp_spindleheadmt,x0),mtvisible(c_tptp_member3393_mt) -> mtvisible(x0)
% 56.33/14.55 === Conflict found: 1456:3:1:[1161.2,1123.2]:Top: genlmt(c_tptp_spindleheadmt,x0),mtvisible(c_tptp_member3393_mt) -> mtvisible(x0) {x0 -> c_cyclistsmt}
% 56.33/14.55 === Backtracking. Learning clause 1458:1:0:[1450.0,1457.1,1456.1,254.1]:: mtvisible(c_tptp_member3393_mt) ->
% 56.33/14.55 === 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}
% 56.33/14.55 === Backtracking. Learning clause 1460:2:1:[1132.0,1459.1,1166.2,1123.2]:Top: genlmt(c_tptp_spindleheadmt,x0) -> mtvisible(x0)
% 56.33/14.55 === Conflict found: 1460:2:1:[1132.0,1459.1,1166.2,1123.2]:Top: genlmt(c_tptp_spindleheadmt,x0) -> mtvisible(x0) {x0 -> c_cyclistsmt}
% 56.33/14.55
% 56.33/14.55 SZS status Unsatisfiable
% 56.33/14.55
% 56.33/14.55 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 56.33/14.55
% 56.33/14.55 SPASS-SCL-FOL Statistics:
% 56.33/14.55 Number of learned clauses: 321
% 56.33/14.55 Number of propagations: 56075
% 56.33/14.55 Number of decisions: 23613
% 56.33/14.55 Number of resolutions: 368
% 56.33/14.55 Number of condensations: 0
% 56.33/14.55 Number of sub resolutions: 6
% 56.33/14.55 Number of input literals (deduplicated): 891
% 56.33/14.55 Number of grows: 13
% 56.33/14.55 Number of considered ground atoms: 1344
% 56.33/14.55
% 56.33/14.55 Needed: 0:0:13.99
% 56.33/14.55
%------------------------------------------------------------------------------