%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR063+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 : n011.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:02 PM UTC 2026
% Result : Theorem 4.50s 1.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.14 % Problem : CSR063+1 : TPTP v9.2.1. Released v3.4.0.
% 0.11/0.15 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.36 % Computer : n011.cluster.edu
% 0.16/0.36 % Model : x86_64 x86_64
% 0.16/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.36 % Memory : 8042.1875MB
% 0.16/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.36 % CPULimit : 300
% 0.16/0.36 % WCLimit : 300
% 0.16/0.36 % DateTime : Thu May 7 11:40:35 EDT 2026
% 0.16/0.36 % CPUTime :
% 0.16/0.36 SPASS-SCL-FOL version:
% 0.19/0.45 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 4.50/1.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.50/1.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.50/1.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.50/1.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.50/1.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.50/1.61 Execution resolution_1 ended with status: unsatisfiable
% 4.50/1.61 Used heuristic: resolution_1
% 4.50/1.61
% 4.50/1.61 Input Clauses:
% 4.50/1.61
% 4.50/1.61 Predicates: genls setorcollection mathematicalthing computerdataartifact mathematicalorcomputationalthing intangible disjointwith partiallytangible artifact genlmt inanimateobject_nonnatural inanimateobject isa genlinverse genlpreds no transitivebinarypredicate few arg2isa collection relation subsetof predicate binarypredicate mtvisible microtheory natfunction natargument uniformresourcelocator thing
% 4.50/1.61 Fol Constants: c_setorcollection c_mathematicalthing s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf c_mathematicalorcomputationalthing c_intangible c_partiallytangible c_computerdataartifact c_artifact c_universalvocabularymt c_basekb c_inanimateobject_nonnatural c_inanimateobject c_disjointwith c_no c_genlpreds c_few c_transitivebinarypredicate c_urlfn n_1 c_urlreferentfn c_tptpcol_16_118949
% 4.50/1.61 Fol Functions: f_urlfn f_urlreferentfn
% 4.50/1.61 Problem Properties:
% 4.50/1.61 This is a full first-order problem without equality.
% 4.50/1.61
% 4.50/1.61 After reduction: Problem Properties:
% 4.50/1.61 This is a full first-order problem without equality.
% 4.50/1.61
% 4.50/1.61
% 4.50/1.61 Reduced Input Clauses:
% 4.50/1.61
% 4.50/1.61 Most General Atoms: mathematicalthing(x0) mathematicalorcomputationalthing(x0) intangible(x0) partiallytangible(x0) computerdataartifact(x0) artifact(x0) inanimateobject_nonnatural(x0) inanimateobject(x0) collection(x1) isa(x0,x2) relation(x0) arg2isa(x0,x2) setorcollection(x1) few(x0,x2) transitivebinarypredicate(x0) genls(x2,x1) no(x0,x2) subsetof(x2,x0) thing(x0) predicate(x0) binarypredicate(x0) genlpreds(x2,x0) genlinverse(x0,x2) mtvisible(x1) natargument(f_urlreferentfn(x0),n_1,x0) microtheory(x0) genlmt(x0,x2) natfunction(f_urlreferentfn(x0),c_urlreferentfn) disjointwith(x2,x1) natfunction(f_urlfn(x0),c_urlfn) natargument(f_urlfn(x0),n_1,x0) uniformresourcelocator(f_urlfn(x0))
% 4.50/1.61
% 4.50/1.61 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: resolution_1 ===
% 4.50/1.61
% 4.50/1.61 === Backtracking. Learning clause 117:2:1:[16.2,18.1]:Top: inanimateobject_nonnatural(x0) -> partiallytangible(x0)
% 4.50/1.61 === Backtracking. Learning clause 118:1:0:[107.1,1.1]:: -> collection(c_mathematicalthing)
% 4.50/1.61 === Backtracking. Learning clause 119:1:0:[107.1,10.1]:: -> collection(c_mathematicalorcomputationalthing)
% 4.50/1.61 === Backtracking. Learning clause 120:1:0:[107.1,4.1]:: -> collection(c_intangible)
% 4.50/1.61 === Backtracking. Learning clause 121:2:1:[114.2,4.1]:Top: genls(x0,c_mathematicalorcomputationalthing) -> genls(x0,c_intangible)
% 4.50/1.61 === Backtracking. Learning clause 122:1:0:[107.1,8.1]:: -> collection(c_artifact)
% 4.50/1.61 === Backtracking. Learning clause 123:1:0:[109.1,8.1]:: -> collection(c_computerdataartifact)
% 4.50/1.61 === Backtracking. Learning clause 124:2:1:[114.2,8.1]:Top: genls(x0,c_computerdataartifact) -> genls(x0,c_artifact)
% 4.50/1.61 === Backtracking. Learning clause 125:1:0:[107.1,13.1]:: -> collection(c_inanimateobject_nonnatural)
% 4.50/1.61 === Backtracking. Learning clause 126:2:1:[114.2,13.1]:Top: genls(x0,c_artifact) -> genls(x0,c_inanimateobject_nonnatural)
% 4.50/1.61 === Backtracking. Learning clause 127:1:0:[107.1,15.1]:: -> collection(c_inanimateobject)
% 4.50/1.61 === Backtracking. Learning clause 128:2:1:[114.2,15.1]:Top: genls(x0,c_inanimateobject_nonnatural) -> genls(x0,c_inanimateobject)
% 4.50/1.61 === Backtracking. Learning clause 129:1:0:[107.1,17.1]:: -> collection(c_partiallytangible)
% 4.50/1.61 === Backtracking. Learning clause 130:2:1:[114.1,17.1]:Top: genls(c_partiallytangible,x0) -> genls(c_inanimateobject,x0)
% 4.50/1.61 === Backtracking. Learning clause 131:2:1:[114.2,17.1,128.2,126.2,124.2]:Top: genls(x0,c_computerdataartifact) -> genls(x0,c_partiallytangible)
% 4.50/1.61 === Backtracking. Learning clause 132:2:1:[30.1,105.2]:Top: disjointwith(c_setorcollection,c_setorcollection),setorcollection(x0) ->
% 4.50/1.61 === Backtracking. Learning clause 133:3:3:[31.3,53.1]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2) -> predicate(x2)
% 4.50/1.61 === Backtracking. Learning clause 134:1:0:[53.1,21.1]:: -> predicate(c_no)
% 4.50/1.61 === Backtracking. Learning clause 135:1:0:[53.1,24.1]:: -> predicate(c_few)
% 4.50/1.61 === Backtracking. Learning clause 136:1:0:[33.1,28.1]:: -> relation(c_few)
% 4.50/1.61 === Clause set with instances from active satisfied. Growing active. New size: 121
% 4.50/1.61 === Restarting.
% 4.50/1.61 === Backtracking. Learning clause 137:2:1:[14.2,117.1,9.2]:Top: computerdataartifact(x0) -> partiallytangible(x0)
% 4.50/1.61 === Backtracking. Learning clause 138:5:5:[82.1,82.3,82.1]:TopTopTopTopTop: genls(x0,x1),disjointwith(x2,x3),genls(x1,x3),genls(x4,x0) -> disjointwith(x2,x4)
% 4.50/1.61 === Backtracking. Learning clause 139:1:0:[69.1,12.1]:: -> microtheory(c_basekb)
% 4.50/1.61 === Backtracking. Learning clause 140:2:1:[97.1,42.2]:Top: transitivebinarypredicate(x0) -> collection(c_transitivebinarypredicate)
% 4.50/1.61 === Backtracking. Learning clause 141:3:1:[100.1,42.2,104.1]:Top: genls(c_transitivebinarypredicate,c_setorcollection),transitivebinarypredicate(x0) -> setorcollection(x0)
% 4.50/1.61 === Backtracking. Learning clause 142:1:0:[55.1,21.1]:: -> predicate(c_disjointwith)
% 4.50/1.61 === Backtracking. Learning clause 143:2:2:[22.2,43.1]:TopTop: disjointwith(x0,x1) -> setorcollection(x1)
% 4.50/1.61 === Backtracking. Learning clause 144:5:4:[83.1,6.1,138.2,143.1]:TopTopTopTop: genls(x0,c_intangible),genls(x1,x2),genls(x2,c_partiallytangible),genls(x3,x1) -> setorcollection(x3)
% 4.50/1.61 === Backtracking. Learning clause 145:2:2:[81.2,143.1]:TopTop: disjointwith(x0,x1) -> setorcollection(x0)
% 4.50/1.61 === Backtracking. Learning clause 146:2:1:[83.1,6.1,145.1,121.2]:Top: genls(x0,c_mathematicalorcomputationalthing) -> setorcollection(x0)
% 4.50/1.61 === Backtracking. Learning clause 147:1:0:[114.2,10.1,146.1,1.1]:: -> setorcollection(c_setorcollection)
% 4.50/1.61 === Backtracking. Learning clause 148:2:1:[7.2,137.2,5.2,11.2]:Top: computerdataartifact(x0),mathematicalthing(x0) ->
% 4.50/1.61 === Conflict found: 138:5:5:[82.1,82.3,82.1]:TopTopTopTopTop: genls(x0,x1),disjointwith(x2,x3),genls(x1,x3),genls(x4,x0) -> disjointwith(x2,x4) {x0 -> c_transitivebinarypredicate, x1 -> c_setorcollection, x2 -> c_intangible, x3 -> c_partiallytangible, x4 -> c_setorcollection}
% 4.50/1.61 === Backtracking. Learning clause 149:5:3:[138.2,6.1,83.1,132.1]:TopTopTop: genls(x0,x1),genls(x1,c_partiallytangible),genls(c_setorcollection,x0),genls(c_setorcollection,c_intangible),setorcollection(x2) ->
% 4.50/1.61 === Backtracking. Learning clause 150:1:0:[79.1,116.1]:: -> collection(c_tptpcol_16_118949)
% 4.50/1.61 === Backtracking. Learning clause 151:3:2:[82.1,116.1,83.1]:TopTop: genls(x0,c_tptpcol_16_118949),genls(x1,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) -> disjointwith(x1,x0)
% 4.50/1.61 === Backtracking. Learning clause 152:1:0:[81.1,116.1]:: -> disjointwith(c_tptpcol_16_118949,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
% 4.50/1.61 === Clause set with instances from active satisfied. Growing active. New size: 142
% 4.50/1.61 === Restarting.
% 4.50/1.61 === Backtracking. Learning clause 153:2:1:[14.2,117.1]:Top: artifact(x0) -> partiallytangible(x0)
% 4.50/1.61 === Backtracking. Learning clause 154:2:1:[114.2,10.1]:Top: genls(x0,c_mathematicalthing) -> genls(x0,c_mathematicalorcomputationalthing)
% 4.50/1.61 === Conflict found: 144:5:4:[83.1,6.1,138.2,143.1]:TopTopTopTop: genls(x0,c_intangible),genls(x1,x2),genls(x2,c_partiallytangible),genls(x3,x1) -> setorcollection(x3) {x0 -> c_intangible, x1 -> c_partiallytangible, x2 -> c_partiallytangible, x3 -> c_partiallytangible}
% 4.50/1.61 === Backtracking. Learning clause 155:1:0:[144.2,112.2,112.2,129.1,120.1]:: -> setorcollection(c_partiallytangible)
% 4.50/1.61 === Conflict found: 131:2:1:[114.2,17.1,128.2,126.2,124.2]:Top: genls(x0,c_computerdataartifact) -> genls(x0,c_partiallytangible) {x0 -> c_computerdataartifact}
% 4.50/1.61 === Backtracking. Learning clause 157:1:0:[123.0,156.0,131.1,112.2]:: -> genls(c_computerdataartifact,c_partiallytangible)
% 4.50/1.61 === Conflict found: 130:2:1:[114.1,17.1]:Top: genls(c_partiallytangible,x0) -> genls(c_inanimateobject,x0) {x0 -> c_mathematicalorcomputationalthing}
% 4.50/1.61 === Backtracking. Learning clause 158:2:0:[130.2,146.1]:: genls(c_partiallytangible,c_mathematicalorcomputationalthing) -> setorcollection(c_inanimateobject)
% 4.50/1.61 === Conflict found: 144:5:4:[83.1,6.1,138.2,143.1]:TopTopTopTop: genls(x0,c_intangible),genls(x1,x2),genls(x2,c_partiallytangible),genls(x3,x1) -> setorcollection(x3) {x0 -> c_intangible, x1 -> c_partiallytangible, x2 -> c_computerdataartifact, x3 -> c_inanimateobject}
% 4.50/1.61 === Backtracking. Learning clause 159:3:1:[144.4,17.1,157.1]:Top: genls(x0,c_intangible),genls(c_partiallytangible,c_computerdataartifact) -> setorcollection(c_inanimateobject)
% 4.50/1.61 === Conflict found: 144:5:4:[83.1,6.1,138.2,143.1]:TopTopTopTop: genls(x0,c_intangible),genls(x1,x2),genls(x2,c_partiallytangible),genls(x3,x1) -> setorcollection(x3) {x0 -> c_intangible, x1 -> c_partiallytangible, x2 -> c_partiallytangible, x3 -> c_inanimateobject}
% 4.50/1.61 === Backtracking. Learning clause 160:1:0:[144.4,17.1,112.2,112.2,129.1,120.1]:: -> setorcollection(c_inanimateobject)
% 4.50/1.61 === Conflict found: 149:5:3:[138.2,6.1,83.1,132.1]:TopTopTop: genls(x0,x1),genls(x1,c_partiallytangible),genls(c_setorcollection,x0),genls(c_setorcollection,c_intangible),setorcollection(x2) -> {x0 -> c_setorcollection, x1 -> c_inanimateobject, x2 -> c_inanimateobject}
% 4.50/1.61 === Backtracking. Learning clause 161:4:2:[149.2,17.1,128.2,126.2]:TopTop: genls(c_setorcollection,x0),genls(c_setorcollection,c_intangible),setorcollection(x1),genls(x0,c_artifact) ->
% 4.50/1.61 === Conflict found: 149:5:3:[138.2,6.1,83.1,132.1]:TopTopTop: genls(x0,x1),genls(x1,c_partiallytangible),genls(c_setorcollection,x0),genls(c_setorcollection,c_intangible),setorcollection(x2) -> {x0 -> c_setorcollection, x1 -> c_inanimateobject, x2 -> c_inanimateobject}
% 4.50/1.61 === Backtracking. Learning clause 162:4:2:[149.2,17.1]:TopTop: genls(x0,c_inanimateobject),genls(c_setorcollection,x0),genls(c_setorcollection,c_intangible),setorcollection(x1) ->
% 4.50/1.61 === Conflict found: 145:2:2:[81.2,143.1]:TopTop: disjointwith(x0,x1) -> setorcollection(x0) {x0 -> c_intangible, x1 -> c_partiallytangible}
% 4.50/1.61 === Backtracking. Learning clause 163:1:0:[145.1,6.1]:: -> setorcollection(c_intangible)
% 4.50/1.61 === Backtracking. Learning clause 164:2:1:[99.1,105.2]:Top: setorcollection(x0) -> thing(x0)
% 4.50/1.61 === Backtracking. Learning clause 165:4:3:[56.2,21.1,62.2,31.3]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2),genlinverse(x2,c_disjointwith) -> genlinverse(x0,c_no)
% 4.50/1.61 === Backtracking. Learning clause 166:2:1:[83.1,152.1,143.1]:Top: genls(x0,c_tptpcol_16_118949) -> setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
% 4.50/1.61 === Conflict found: 145:2:2:[81.2,143.1]:TopTop: disjointwith(x0,x1) -> setorcollection(x0) {x0 -> c_tptpcol_16_118949, x1 -> f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))}
% 4.50/1.61 === Backtracking. Learning clause 167:1:0:[145.1,152.1]:: -> setorcollection(c_tptpcol_16_118949)
% 4.50/1.61 === Clause set with instances from active satisfied. Growing active. New size: 151
% 4.50/1.61 === Restarting.
% 4.50/1.61 === Conflict found: 128:2:1:[114.2,15.1]:Top: genls(x0,c_inanimateobject_nonnatural) -> genls(x0,c_inanimateobject) {x0 -> c_setorcollection}
% 4.50/1.61 === Backtracking. Learning clause 168:4:2:[128.2,162.1]:TopTop: genls(x0,c_inanimateobject_nonnatural),genls(c_setorcollection,x0),genls(c_setorcollection,c_intangible),setorcollection(x1) ->
% 4.50/1.61 === Conflict found: 146:2:1:[83.1,6.1,145.1,121.2]:Top: genls(x0,c_mathematicalorcomputationalthing) -> setorcollection(x0) {x0 -> c_mathematicalthing}
% 4.50/1.61 === Backtracking. Learning clause 169:1:0:[146.1,10.1]:: -> setorcollection(c_mathematicalthing)
% 4.50/1.61 === Conflict found: 148:2:1:[7.2,137.2,5.2,11.2]:Top: computerdataartifact(x0),mathematicalthing(x0) -> {x0 -> f_urlreferentfn(c_setorcollection)}
% 4.50/1.61 === Backtracking. Learning clause 170:1:1:[148.1,95.1]:Top: mathematicalthing(f_urlreferentfn(x0)) ->
% 4.50/1.61 === Backtracking. Learning clause 171:1:0:[71.1,12.1]:: -> microtheory(c_universalvocabularymt)
% 4.50/1.61 === Backtracking. Learning clause 172:2:1:[56.2,24.1]:Top: genlpreds(x0,c_no) -> genlpreds(x0,c_few)
% 4.50/1.61 === Backtracking. Learning clause 173:1:0:[79.1,152.1]:: -> collection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
% 4.50/1.61 === Backtracking. Learning clause 174:2:1:[83.1,152.1]:Top: genls(x0,c_tptpcol_16_118949) -> disjointwith(x0,f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf)))
% 4.50/1.61 === Clause set with instances from active satisfied. Growing active. New size: 155
% 4.50/1.61 === Restarting.
% 4.50/1.61 === Backtracking. Learning clause 175:3:2:[114.3,146.1]:TopTop: genls(x0,x1),genls(x1,c_mathematicalorcomputationalthing) -> setorcollection(x0)
% 4.50/1.61 === Backtracking. Learning clause 176:1:0:[112.2,146.1,119.1]:: -> setorcollection(c_mathematicalorcomputationalthing)
% 4.50/1.61 === Conflict found: 144:5:4:[83.1,6.1,138.2,143.1]:TopTopTopTop: genls(x0,c_intangible),genls(x1,x2),genls(x2,c_partiallytangible),genls(x3,x1) -> setorcollection(x3) {x0 -> c_intangible, x1 -> c_partiallytangible, x2 -> c_partiallytangible, x3 -> c_computerdataartifact}
% 4.50/1.61 === Backtracking. Learning clause 177:1:0:[144.4,157.1,112.2,112.2,129.1,120.1]:: -> setorcollection(c_computerdataartifact)
% 4.50/1.61 === Backtracking. Learning clause 178:1:1:[2.2,170.1]:Top: setorcollection(f_urlreferentfn(x0)) ->
% 4.50/1.61 === Conflict found: 166:2:1:[83.1,152.1,143.1]:Top: genls(x0,c_tptpcol_16_118949) -> setorcollection(f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))) {x0 -> c_setorcollection}
% 4.50/1.61 === Backtracking. Learning clause 179:1:1:[166.2,178.1]:Top: genls(x0,c_tptpcol_16_118949) ->
% 4.50/1.61 === Conflict found: 143:2:2:[22.2,43.1]:TopTop: disjointwith(x0,x1) -> setorcollection(x1) {x0 -> c_tptpcol_16_118949, x1 -> f_urlreferentfn(f_urlfn(s_http_fwsistercitiesorgpdfsmbabanembabane20activity20pages2pdf))}
% 4.50/1.61
% 4.50/1.61 SZS status Unsatisfiable
% 4.50/1.61
% 4.50/1.61 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.50/1.61
% 4.50/1.61 SPASS-SCL-FOL Statistics:
% 4.50/1.61 Number of learned clauses: 62
% 4.50/1.61 Number of propagations: 2977
% 4.50/1.61 Number of decisions: 1041
% 4.50/1.61 Number of resolutions: 99
% 4.50/1.61 Number of condensations: 0
% 4.50/1.61 Number of sub resolutions: 1
% 4.50/1.61 Number of input literals (deduplicated): 62
% 4.50/1.61 Number of grows: 4
% 4.50/1.61 Number of considered ground atoms: 155
% 4.50/1.61
% 4.50/1.61 Needed: 0:00:01.01
% 4.50/1.61
%------------------------------------------------------------------------------