%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : CSR072+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 : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Thu May 7 07:20:10 PM UTC 2026 % Result : Theorem 0.34s 0.59s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.14 % Problem : CSR072+2 : TPTP v9.2.1. Released v3.4.0. % 0.11/0.14 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.16/0.35 % Computer : n014.cluster.edu % 0.16/0.35 % Model : x86_64 x86_64 % 0.16/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.35 % Memory : 8042.1875MB % 0.16/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.35 % CPULimit : 300 % 0.16/0.35 % WCLimit : 300 % 0.16/0.35 % DateTime : Thu May 7 11:42:12 EDT 2026 % 0.16/0.35 % CPUTime : % 0.16/0.36 SPASS-SCL-FOL version: % 0.25/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.34/0.58 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.58 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.58 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.58 Execution normal ended with status: unsatisfiable % 0.34/0.58 Used heuristic: normal % 0.34/0.58 % 0.34/0.58 Input Clauses: % 0.34/0.58 % 0.34/0.58 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 % 0.34/0.58 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 % 0.34/0.58 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 % 0.34/0.58 Problem Properties: % 0.34/0.58 This is a full first-order problem without equality. % 0.34/0.58 % 0.34/0.58 % 0.34/0.58 Reduced Input Clauses: % 0.34/0.59 1134:0:0:[1133.0,322.0]:: -> % 0.34/0.59 % 0.34/0.59 SZS status Unsatisfiable % 0.34/0.59 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.34/0.59 % 0.34/0.59 SPASS-SCL-FOL Statistics: % 0.34/0.59 Number of learned clauses: 0 % 0.34/0.59 Number of propagations: 0 % 0.34/0.59 Number of decisions: 0 % 0.34/0.59 Number of resolutions: 0 % 0.34/0.59 Number of condensations: 0 % 0.34/0.59 Number of sub resolutions: 1 % 0.34/0.59 % 0.34/0.59 Needed: 0:00:00.02 % 0.34/0.59 %------------------------------------------------------------------------------