%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : CSR074+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 : n013.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 0.30s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.16 % Problem : CSR074+1 : TPTP v9.2.1. Released v3.4.0.
% 0.11/0.17 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.40 % Computer : n013.cluster.edu
% 0.16/0.40 % Model : x86_64 x86_64
% 0.16/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.40 % Memory : 8042.1875MB
% 0.16/0.40 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.40 % CPULimit : 300
% 0.16/0.40 % WCLimit : 300
% 0.16/0.40 % DateTime : Thu May 7 11:41:31 EDT 2026
% 0.16/0.40 % CPUTime :
% 0.16/0.40 SPASS-SCL-FOL version:
% 0.22/0.51 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.30/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.62 Execution resolution_1 ended with status: unsatisfiable
% 0.30/0.62 Used heuristic: resolution_1
% 0.30/0.62
% 0.30/0.62 Input Clauses:
% 0.30/0.62
% 0.30/0.62 Predicates: genlmt transitivebinarypredicate genlinverse geographicalsubregions inregion mtvisible geolevel_3 isa disjointwith genlpreds predicate collection genls geographicalregion binarypredicate spatialthing_nonsituational thing microtheory
% 0.30/0.62 Fol Constants: c_geographymt c_basekb c_inregion c_worldgeographymt c_geographicalsubregions c_genlmt c_universalvocabularymt c_tptpgeo_spindleheadmt c_tptpgeo_member7_mt c_georegion_l3_x17_y24 c_georegion_l4_x53_y74 c_geolocation_x53_y74 c_geolevel_3 c_transitivebinarypredicate
% 0.30/0.62 Fol Functions:
% 0.30/0.62 Problem Properties:
% 0.30/0.62 This is a Bernays Schoenfinkel problem.
% 0.30/0.62
% 0.30/0.62 After reduction: Problem Properties:
% 0.30/0.62 This is a Bernays Schoenfinkel problem.
% 0.30/0.62
% 0.30/0.62
% 0.30/0.62 Reduced Input Clauses:
% 0.30/0.62 60:1:0:[58.0,11.0]:: -> geographicalsubregions(c_georegion_l3_x17_y24,c_georegion_l4_x53_y74)
% 0.30/0.62 61:1:0:[58.0,12.0]:: -> inregion(c_geolocation_x53_y74,c_georegion_l4_x53_y74)
% 0.30/0.62
% 0.30/0.62 Most General Atoms: isa(x0,x2) predicate(x0) collection(x0) disjointwith(x2,x1) geolevel_3(x0) geographicalregion(x0) geographicalsubregions(x0,x2) binarypredicate(x0) genlpreds(x2,x0) genlinverse(x0,x2) transitivebinarypredicate(x0) spatialthing_nonsituational(x0) inregion(x0,x2) genlmt(x0,x2) thing(x0) genls(x1,x2) mtvisible(x1) microtheory(x1)
% 0.30/0.62
% 0.30/0.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 55 atoms initially, heuristics mode: resolution_1 ===
% 0.30/0.62
% 0.30/0.62 === Backtracking. Learning clause 62:2:1:[54.2,7.1]:Top: genlmt(x0,c_basekb) -> genlmt(x0,c_universalvocabularymt)
% 0.30/0.62 === Backtracking. Learning clause 63:2:1:[54.1,8.1]:Top: genlmt(c_worldgeographymt,x0) -> genlmt(c_tptpgeo_spindleheadmt,x0)
% 0.30/0.62 === Backtracking. Learning clause 64:2:1:[54.1,9.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member7_mt,x0)
% 0.30/0.62 === Backtracking. Learning clause 65:1:0:[33.1,4.1]:: -> binarypredicate(c_inregion)
% 0.30/0.62 === Backtracking. Learning clause 66:1:0:[34.1,4.1]:: -> binarypredicate(c_geographicalsubregions)
% 0.30/0.62 === Backtracking. Learning clause 67:1:0:[29.1,60.1]:: -> geographicalregion(c_georegion_l4_x53_y74)
% 0.30/0.62 === Backtracking. Learning clause 68:1:0:[30.1,60.1]:: -> geographicalregion(c_georegion_l3_x17_y24)
% 0.30/0.62 === Backtracking. Learning clause 69:2:0:[5.2,59.1]:: geographicalsubregions(c_georegion_l3_x17_y24,c_geolocation_x53_y74),geolevel_3(c_georegion_l3_x17_y24) ->
% 0.30/0.62 === Backtracking. Learning clause 70:1:0:[39.1,61.1]:: -> spatialthing_nonsituational(c_georegion_l4_x53_y74)
% 0.30/0.62 === Backtracking. Learning clause 71:1:0:[40.1,61.1]:: -> spatialthing_nonsituational(c_geolocation_x53_y74)
% 0.30/0.62 === Backtracking. Learning clause 72:3:3:[14.3,16.1]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2) -> predicate(x2)
% 0.30/0.62 === Clause set with instances from active satisfied. Growing active. New size: 65
% 0.30/0.62 === Restarting.
% 0.30/0.62 === Backtracking. Learning clause 73:1:0:[53.1,1.1]:: -> microtheory(c_geographymt)
% 0.30/0.62 === Backtracking. Learning clause 74:1:0:[51.1,1.1]:: -> microtheory(c_basekb)
% 0.30/0.62 === Conflict found: 62:2:1:[54.2,7.1]:Top: genlmt(x0,c_basekb) -> genlmt(x0,c_universalvocabularymt) {x0 -> c_geographymt}
% 0.30/0.62 === Backtracking. Learning clause 75:1:0:[62.2,51.1,1.1]:: -> microtheory(c_universalvocabularymt)
% 0.30/0.62 === Backtracking. Learning clause 76:2:0:[49.2,3.1]:: mtvisible(c_worldgeographymt) -> mtvisible(c_geographymt)
% 0.30/0.62 === Conflict found: 64:2:1:[54.1,9.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member7_mt,x0) {x0 -> c_geographymt}
% 0.30/0.62 === Backtracking. Learning clause 77:1:0:[64.2,49.2,63.2,3.1,58.1]:: -> mtvisible(c_geographymt)
% 0.30/0.62 === Backtracking. Learning clause 78:1:0:[49.2,9.1,58.1]:: -> mtvisible(c_tptpgeo_spindleheadmt)
% 0.30/0.62 === Conflict found: 72:3:3:[14.3,16.1]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2) -> predicate(x2) {x0 -> c_geographicalsubregions, x1 -> c_inregion, x2 -> c_geographymt}
% 0.30/0.62 === Backtracking. Learning clause 79:2:1:[72.1,4.1]:Top: genlinverse(c_inregion,x0) -> predicate(x0)
% 0.30/0.62 === Backtracking. Learning clause 80:3:1:[41.3,59.1]:Top: inregion(c_geolocation_x53_y74,x0),inregion(x0,c_georegion_l3_x17_y24),geolevel_3(c_georegion_l3_x17_y24) ->
% 0.30/0.62 === Backtracking. Learning clause 81:3:1:[41.1,61.1,80.1]:Top: inregion(c_georegion_l4_x53_y74,x0),inregion(x0,c_georegion_l3_x17_y24),geolevel_3(c_georegion_l3_x17_y24) ->
% 0.30/0.62 === Clause set with instances from active satisfied. Growing active. New size: 68
% 0.30/0.62 === Restarting.
% 0.30/0.62 === Backtracking. Learning clause 82:1:0:[53.1,3.1]:: -> microtheory(c_worldgeographymt)
% 0.30/0.62 === Conflict found: 63:2:1:[54.1,8.1]:Top: genlmt(c_worldgeographymt,x0) -> genlmt(c_tptpgeo_spindleheadmt,x0) {x0 -> c_geographymt}
% 0.30/0.62 === Backtracking. Learning clause 83:1:0:[63.2,53.1,3.1]:: -> microtheory(c_tptpgeo_spindleheadmt)
% 0.30/0.62 === Backtracking. Learning clause 84:2:1:[54.2,8.1]:Top: genlmt(x0,c_tptpgeo_spindleheadmt) -> genlmt(x0,c_worldgeographymt)
% 0.30/0.62 === Conflict found: 64:2:1:[54.1,9.1]:Top: genlmt(c_tptpgeo_spindleheadmt,x0) -> genlmt(c_tptpgeo_member7_mt,x0) {x0 -> c_geographymt}
% 0.30/0.62 === Backtracking. Learning clause 85:1:0:[64.2,53.1,63.2,3.1]:: -> microtheory(c_tptpgeo_member7_mt)
% 0.30/0.62 === Backtracking. Learning clause 86:2:1:[54.2,9.1]:Top: genlmt(x0,c_tptpgeo_member7_mt) -> genlmt(x0,c_tptpgeo_spindleheadmt)
% 0.30/0.62 === Conflict found: 72:3:3:[14.3,16.1]:TopTopTop: genlinverse(x0,x1),genlinverse(x1,x2) -> predicate(x2) {x0 -> c_geographymt, x1 -> c_geographicalsubregions, x2 -> c_inregion}
% 0.30/0.62 === Backtracking. Learning clause 87:2:1:[72.2,4.1]:Top: genlinverse(x0,c_geographicalsubregions) -> predicate(c_inregion)
% 0.30/0.62 === Backtracking. Learning clause 88:2:1:[31.2,60.1]:Top: geographicalsubregions(x0,c_georegion_l3_x17_y24) -> geographicalsubregions(x0,c_georegion_l4_x53_y74)
% 0.30/0.62 === Backtracking. Learning clause 89:3:1:[31.3,69.1]:Top: geographicalsubregions(c_georegion_l3_x17_y24,x0),geographicalsubregions(x0,c_geolocation_x53_y74),geolevel_3(c_georegion_l3_x17_y24) ->
% 0.30/0.62 === Conflict found: 81:3:1:[41.1,61.1,80.1]:Top: inregion(c_georegion_l4_x53_y74,x0),inregion(x0,c_georegion_l3_x17_y24),geolevel_3(c_georegion_l3_x17_y24) -> {x0 -> c_geographymt}
% 0.30/0.62 === Backtracking. Learning clause 90:3:1:[81.1,5.2]:Top: inregion(x0,c_georegion_l3_x17_y24),geolevel_3(c_georegion_l3_x17_y24),geographicalsubregions(x0,c_georegion_l4_x53_y74) ->
% 0.30/0.62 === Conflict found: 81:3:1:[41.1,61.1,80.1]:Top: inregion(c_georegion_l4_x53_y74,x0),inregion(x0,c_georegion_l3_x17_y24),geolevel_3(c_georegion_l3_x17_y24) -> {x0 -> c_georegion_l4_x53_y74}
% 0.30/0.62 === Backtracking. Learning clause 91:1:0:[81.1,42.2,5.2,60.1,70.1,10.2]:: mtvisible(c_worldgeographymt) ->
% 0.30/0.62
% 0.30/0.62 SZS status Unsatisfiable
% 0.30/0.62
% 0.30/0.62 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.62
% 0.30/0.62 SPASS-SCL-FOL Statistics:
% 0.30/0.62 Number of learned clauses: 30
% 0.30/0.62 Number of propagations: 596
% 0.30/0.62 Number of decisions: 409
% 0.30/0.62 Number of resolutions: 46
% 0.30/0.62 Number of condensations: 0
% 0.30/0.62 Number of sub resolutions: 2
% 0.30/0.62 Number of input literals (deduplicated): 40
% 0.30/0.62 Number of grows: 2
% 0.30/0.62 Number of considered ground atoms: 68
% 0.30/0.62
% 0.30/0.62 Needed: 0:00:00.01
% 0.30/0.62
%------------------------------------------------------------------------------