%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR060+1 : TPTP v9.2.1. Released v3.4.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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:00 PM UTC 2026
% Result : Theorem 0.44s 0.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.13 % Problem : CSR060+1 : TPTP v9.2.1. Released v3.4.0.
% 0.11/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.35 % Computer : n026.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:41:52 EDT 2026
% 0.17/0.35 % CPUTime :
% 0.17/0.35 SPASS-SCL-FOL version:
% 0.17/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.44/0.57 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/0.57 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/0.57 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/0.57 Execution resolution_3 ended with status: unsatisfiable
% 0.44/0.57 Used heuristic: resolution_3
% 0.44/0.57
% 0.44/0.57 Input Clauses:
% 0.44/0.58
% 0.44/0.58 Predicates: genlmt isa relationexistsall resultisaarg transitivebinarypredicate mtvisible tptp_9_51 subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma disjointwith genlinverse genlpreds predicate binarypredicate collection genls objectfoundinlocation spatialthing_nonsituational spatialthing_localized geopoliticalsubdivision geographicallysubsumes subregions ship natfunction natargument tptpcol_16_27189 tptpcol_7_26628 thing positiveinteger function_denotational uniformresourcelocator computerdataartifact microtheory
% 0.44/0.58 Fol Constants: c_ldscdemonstrationspindleheadmt c_currentworlddatacollectormt_nonhomocentric c_cycorpproductsmt c_basekb c_cycnounlearnermt s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988 c_translation_0_885 c_machinelearningspindleheadmt c_miptdatabase19681997_termsmt c_relationexistsallfn n_3 c_ldscgeneralcollectormt c_genlmt c_universalvocabularymt c_ship c_objectfoundinlocation c_cityofbostonma c_tptp_9_51 c_tptpcol_16_27189 c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802 c_subcollectionofwithrelationtofn n_1 n_2 c_transitivebinarypredicate n_4 c_urlfn c_urlreferentfn c_contentmtofcdafromeventfn
% 0.44/0.58 Fol Functions: f_urlfn f_urlreferentfn f_contentmtofcdafromeventfn f_relationexistsallfn f_subcollectionofwithrelationtofn
% 0.44/0.58 Problem Properties:
% 0.44/0.58 This is a full first-order problem without equality.
% 0.44/0.58
% 0.44/0.58 After reduction: Problem Properties:
% 0.44/0.58 This is a full first-order problem without equality.
% 0.44/0.58
% 0.44/0.58
% 0.44/0.58 Reduced Input Clauses:
% 0.44/0.58
% 0.44/0.58 Most General Atoms: isa(x0,x2) tptpcol_16_27189(x0) predicate(x0) binarypredicate(x0) genlpreds(x2,x0) genlinverse(x0,x2) disjointwith(x2,x1) spatialthing_nonsituational(x0) 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) tptp_9_51(x0,x1) subcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma(x1) tptpcol_7_26628(x0) relationexistsall(x0,x1,x2) collection(x2) transitivebinarypredicate(x0) genlmt(x0,x2) thing(x0) genls(x1,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) 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) computerdataartifact(f_urlreferentfn(x0)) natfunction(f_contentmtofcdafromeventfn(x0,x1),c_contentmtofcdafromeventfn) natargument(f_contentmtofcdafromeventfn(x0,x1),n_1,x0) natargument(f_contentmtofcdafromeventfn(x0,x1),n_2,x1) mtvisible(x1) microtheory(x1)
% 0.44/0.58
% 0.44/0.58 === Starting SPASS-SCL-FOL A Little Less Naive, considering 67 atoms initially, heuristics mode: resolution_3 ===
% 0.44/0.58
% 0.44/0.58 === Backtracking. Learning clause 97:2:1:[91.2,2.1]:Top: genlmt(x0,c_cycorpproductsmt) -> genlmt(x0,c_basekb)
% 0.44/0.58 === Backtracking. Learning clause 98:2:1:[91.2,12.1]:Top: genlmt(x0,c_basekb) -> genlmt(x0,c_universalvocabularymt)
% 0.44/0.58 === Backtracking. Learning clause 99:2:1:[91.1,3.1]:Top: genlmt(c_cycorpproductsmt,x0) -> genlmt(c_cycnounlearnermt,x0)
% 0.44/0.58 === Backtracking. Learning clause 100:3:3:[18.3,22.1]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2) -> predicate(x0)
% 0.44/0.58 === Backtracking. Learning clause 101:2:1:[91.1,4.1]:Top: genlmt(c_machinelearningspindleheadmt,x0) -> genlmt(f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885),x0)
% 0.44/0.58 === Backtracking. Learning clause 102:2:1:[91.2,4.1]:Top: genlmt(x0,f_contentmtofcdafromeventfn(f_urlreferentfn(f_urlfn(s_http_wwwsurgerydoorcoukmedconsprintasprecno23068988)),c_translation_0_885)) -> genlmt(x0,c_machinelearningspindleheadmt)
% 0.44/0.58 === Backtracking. Learning clause 103:2:0:[59.1,14.2]:: mtvisible(c_currentworlddatacollectormt_nonhomocentric) -> binarypredicate(c_tptp_9_51)
% 0.44/0.58 === Backtracking. Learning clause 104:2:0:[58.1,14.2]:: mtvisible(c_currentworlddatacollectormt_nonhomocentric) -> collection(c_tptpcol_16_27189)
% 0.44/0.58 === Backtracking. Learning clause 106:2:0:[15.0,105.2,96.1,13.3]:: tptpcol_16_27189(f_relationexistsallfn(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802,c_tptp_9_51,c_tptpcol_16_27189,f_subcollectionofwithrelationtofn(c_ship,c_objectfoundinlocation,c_cityofbostonma))),mtvisible(c_currentworlddatacollectormt_nonhomocentric) ->
% 0.44/0.58 === Clause set with instances from active satisfied. Growing active. New size: 97
% 0.44/0.58 === Restarting.
% 0.44/0.58 === Backtracking. Learning clause 107:1:0:[88.1,1.1]:: -> microtheory(c_currentworlddatacollectormt_nonhomocentric)
% 0.44/0.58 === Backtracking. Learning clause 108:1:0:[90.1,2.1]:: -> microtheory(c_cycorpproductsmt)
% 0.44/0.58 === Conflict found: 97:2:1:[91.2,2.1]:Top: genlmt(x0,c_cycorpproductsmt) -> genlmt(x0,c_basekb) {x0 -> c_ldscdemonstrationspindleheadmt}
% 0.44/0.58 === Backtracking. Learning clause 109:2:1:[97.2,88.1]:Top: genlmt(x0,c_cycorpproductsmt) -> microtheory(c_basekb)
% 0.44/0.58 === Backtracking. Learning clause 110:1:0:[88.1,2.1]:: -> microtheory(c_basekb)
% 0.44/0.58 === Conflict found: 98:2:1:[91.2,12.1]:Top: genlmt(x0,c_basekb) -> genlmt(x0,c_universalvocabularymt) {x0 -> c_ldscdemonstrationspindleheadmt}
% 0.44/0.58 === Backtracking. Learning clause 111:2:1:[98.2,88.1,97.2]:Top: genlmt(x0,c_cycorpproductsmt) -> microtheory(c_universalvocabularymt)
% 0.44/0.58 === Backtracking. Learning clause 112:1:0:[88.1,12.1]:: -> microtheory(c_universalvocabularymt)
% 0.44/0.58 === Conflict found: 99:2:1:[91.1,3.1]:Top: genlmt(c_cycorpproductsmt,x0) -> genlmt(c_cycnounlearnermt,x0) {x0 -> c_ldscdemonstrationspindleheadmt}
% 0.44/0.58 === Backtracking. Learning clause 113:2:1:[99.2,90.1]:Top: genlmt(c_cycorpproductsmt,x0) -> microtheory(c_cycnounlearnermt)
% 0.44/0.58 === Conflict found: 113:2:1:[99.2,90.1]:Top: genlmt(c_cycorpproductsmt,x0) -> microtheory(c_cycnounlearnermt) {x0 -> c_basekb}
% 0.44/0.58 === Backtracking. Learning clause 114:1:0:[113.1,2.1]:: -> microtheory(c_cycnounlearnermt)
% 0.44/0.58 === Backtracking. Learning clause 115:1:0:[90.1,11.1]:: -> microtheory(c_machinelearningspindleheadmt)
% 0.44/0.58 === Backtracking. Learning clause 116:1:0:[88.1,5.1]:: -> microtheory(c_miptdatabase19681997_termsmt)
% 0.44/0.58 === Backtracking. Learning clause 117:1:0:[88.1,8.1]:: -> microtheory(c_ldscgeneralcollectormt)
% 0.44/0.58 === Backtracking. Learning clause 118:1:0:[73.1,7.1]:: -> positiveinteger(n_3)
% 0.44/0.58 === Backtracking. Learning clause 119:1:0:[74.1,7.1]:: -> function_denotational(c_relationexistsallfn)
% 0.44/0.58 === Backtracking. Learning clause 120:1:0:[65.1,15.1]:: -> thing(c_tptpnsubcollectionofwithrelationtofnshipobjectfoundinlocationcityofbostonma_802)
% 0.44/0.58 === Backtracking. Learning clause 121:1:0:[86.2,4.1,95.1]:: -> mtvisible(c_machinelearningspindleheadmt)
% 0.44/0.58 === Backtracking. Learning clause 123:1:0:[121.0,122.0,86.2,5.1]:: -> mtvisible(c_miptdatabase19681997_termsmt)
% 0.44/0.58 === Backtracking. Learning clause 125:1:0:[123.0,124.0,86.2,8.1]:: -> mtvisible(c_ldscgeneralcollectormt)
% 0.44/0.58 === Clause set with instances from active satisfied. Growing active. New size: 101
% 0.44/0.58 === Restarting.
% 0.44/0.58 === Clause set with instances from active satisfied. Growing active. New size: 165
% 0.44/0.58 === Clause set with instances from active satisfied. Growing active. New size: 229
% 0.44/0.58 === Backtracking. Learning clause 126:1:0:[61.2,63.1,10.1]:: -> collection(c_transitivebinarypredicate)
% 0.44/0.58
% 0.44/0.58 SZS status Unsatisfiable
% 0.44/0.58
% 0.44/0.58 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.44/0.58
% 0.44/0.58 SPASS-SCL-FOL Statistics:
% 0.44/0.58 Number of learned clauses: 27
% 0.44/0.58 Number of propagations: 917
% 0.44/0.58 Number of decisions: 601
% 0.44/0.58 Number of resolutions: 39
% 0.44/0.58 Number of condensations: 0
% 0.44/0.58 Number of sub resolutions: 3
% 0.44/0.58 Number of input literals (deduplicated): 77
% 0.44/0.58 Number of grows: 4
% 0.44/0.58 Number of considered ground atoms: 229
% 0.44/0.58
% 0.44/0.58 Needed: 0:00:00.05
% 0.44/0.58
%------------------------------------------------------------------------------