%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : CSR074+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 : n021.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:12 PM UTC 2026 % Result : Theorem 46.00s 9.79s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : CSR074+2 : TPTP v9.2.1. Released v3.4.0. % 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.14/0.34 % Computer : n021.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Thu May 7 11:42:32 EDT 2026 % 0.14/0.35 % CPUTime : % 0.14/0.35 SPASS-SCL-FOL version: % 0.18/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 46.00/9.79 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 46.00/9.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 46.00/9.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 46.00/9.79 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 46.00/9.79 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 46.00/9.79 Execution normal ended with status: unsatisfiable % 46.00/9.79 Used heuristic: normal % 46.00/9.79 % 46.00/9.79 Input Clauses: % 46.00/9.79 % 46.00/9.79 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 % 46.00/9.79 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 % 46.00/9.79 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 % 46.00/9.79 Problem Properties: % 46.00/9.79 This is a full first-order problem without equality. % 46.00/9.79 % 46.00/9.79 After reduction: Problem Properties: % 46.00/9.79 This is a full first-order problem without equality. % 46.00/9.79 % 46.00/9.79 % 46.00/9.79 Reduced Input Clauses: % 46.00/9.79 1134:1:0:[1132.0,82.0]:: -> inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74) % 46.00/9.79 1135:1:0:[1132.0,122.0]:: -> borderson(c_georegion_l4_x27_y64,c_georegion_l4_x27_y65) % 46.00/9.79 1136:1:0:[1132.0,188.0]:: -> geographicalsubregions(c_georegion_l3_x15_y24,c_georegion_l4_x45_y72) % 46.00/9.79 1137:1:0:[1132.0,276.0]:: -> geographicalsubregions(c_georegion_l2_x5_y8,c_georegion_l3_x15_y24) % 46.00/9.79 1138:1:0:[1132.0,472.0]:: -> geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74) % 46.00/9.79 1139:1:0:[1132.0,485.0]:: -> borderson(c_georegion_l4_x29_y75,c_georegion_l4_x29_y76) % 46.00/9.79 % 46.00/9.79 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) % 46.00/9.79 % 46.00/9.79 === Starting SPASS-SCL-FOL A Little Less Naive, considering 890 atoms initially, heuristics mode: normal === % 46.00/9.79 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 954 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1018 % 46.00/9.79 === Backtracking. Learning clause 1140:2:1:[9.1,1095.2,3.2]:Top: isa(x0,c_inanimateobject),intangible(x0) -> % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1082 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1146 % 46.00/9.79 === Backtracking. Learning clause 1141:2:1:[124.2,445.1]:Top: tptpcol_1_65536(x0) -> individual(x0) % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1210 % 46.00/9.79 === Backtracking. Learning clause 1142:2:1:[146.2,153.1,386.2,223.2]:Top: tptpcol_1_65536(x0),tptpcol_4_24578(x0) -> % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1274 % 46.00/9.79 === Backtracking. Learning clause 1143:2:1:[468.2,474.1,103.2]:Top: tptpcol_15_92268(x0) -> tptpcol_12_92262(x0) % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1338 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1402 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1466 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1530 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1594 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1658 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1722 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1786 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1850 % 46.00/9.79 === Clause set with instances from active satisfied. Growing active. New size: 1914 % 46.00/9.79 % 46.00/9.79 SZS status Unsatisfiable % 46.00/9.79 % 46.00/9.79 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 46.00/9.79 % 46.00/9.79 SPASS-SCL-FOL Statistics: % 46.00/9.79 Number of learned clauses: 4 % 46.00/9.79 Number of propagations: 2939 % 46.00/9.79 Number of decisions: 929 % 46.00/9.79 Number of resolutions: 18 % 46.00/9.79 Number of condensations: 0 % 46.00/9.79 Number of sub resolutions: 6 % 46.00/9.79 Number of input literals (deduplicated): 890 % 46.00/9.79 Number of grows: 16 % 46.00/9.79 Number of considered ground atoms: 1914 % 46.00/9.79 % 46.00/9.79 Needed: 0:00:09.21 % 46.00/9.79 %------------------------------------------------------------------------------