%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : CSR061+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 : n016.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.75s 0.68s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : CSR061+1 : TPTP v9.2.1. Released v3.4.0. % 0.13/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.34 % Computer : n016.cluster.edu % 0.15/0.34 % Model : x86_64 x86_64 % 0.15/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.34 % Memory : 8042.1875MB % 0.15/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.34 % CPULimit : 300 % 0.15/0.34 % WCLimit : 300 % 0.15/0.34 % DateTime : Thu May 7 11:41:27 EDT 2026 % 0.15/0.35 % CPUTime : % 0.15/0.35 SPASS-SCL-FOL version: % 0.19/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.75/0.68 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.75/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.75/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.75/0.68 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.75/0.68 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.75/0.68 Execution normal ended with status: unsatisfiable % 0.75/0.68 Used heuristic: normal % 0.75/0.68 % 0.75/0.68 Input Clauses: % 0.75/0.68 % 0.75/0.68 Predicates: transitivebinarypredicate genlmt genls tptpcol_4_106497 tptpcol_3_98305 tptpcol_5_110593 tptpcol_6_112641 tptpcol_7_113665 tptpcol_8_114177 tptpcol_4_114689 tptpcol_3_114688 tptpcol_5_114690 tptpcol_6_116738 tptpcol_7_117762 tptpcol_8_117763 tptpcol_9_118019 tptpcol_10_118020 tptpcol_11_118084 tptpcol_12_118116 tptpcol_13_118117 tptpcol_14_118118 disjointwith isa genlinverse genlpreds predicate binarypredicate collection mtvisible microtheory thing % 0.75/0.68 Fol Constants: c_genlmt c_generictemporalmt c_basekb c_timehasnoendmt c_universalvocabularymt c_tptpcol_4_106497 c_tptpcol_3_98305 c_tptpcol_5_110593 c_tptpcol_6_112641 c_tptpcol_7_113665 c_tptpcol_8_114177 c_tptpcol_4_114689 c_tptpcol_3_114688 c_tptpcol_5_114690 c_tptpcol_6_116738 c_tptpcol_7_117762 c_tptpcol_8_117763 c_tptpcol_9_118019 c_tptpcol_10_118020 c_tptpcol_11_118084 c_tptpcol_12_118116 c_tptpcol_13_118117 c_tptpcol_14_118118 c_transitivebinarypredicate % 0.75/0.68 Fol Functions: % 0.75/0.68 Problem Properties: % 0.75/0.68 This is a Bernays Schoenfinkel problem. % 0.75/0.68 % 0.75/0.68 After reduction: Problem Properties: % 0.75/0.68 This is a Bernays Schoenfinkel problem. % 0.75/0.68 % 0.75/0.68 % 0.75/0.68 Reduced Input Clauses: % 0.75/0.68 % 0.75/0.68 Most General Atoms: tptpcol_4_106497(x0) tptpcol_3_98305(x0) tptpcol_5_110593(x0) tptpcol_6_112641(x0) tptpcol_7_113665(x0) tptpcol_8_114177(x0) tptpcol_4_114689(x0) tptpcol_3_114688(x0) tptpcol_5_114690(x0) tptpcol_6_116738(x0) tptpcol_7_117762(x0) tptpcol_8_117763(x0) tptpcol_9_118019(x0) tptpcol_10_118020(x0) tptpcol_11_118084(x0) tptpcol_12_118116(x0) tptpcol_13_118117(x0) tptpcol_14_118118(x0) isa(x0,x2) predicate(x0) binarypredicate(x0) genlpreds(x2,x0) genlinverse(x0,x2) collection(x0) disjointwith(x2,x1) thing(x0) genlmt(x0,x2) genls(x0,x2) transitivebinarypredicate(x0) mtvisible(x1) microtheory(x1) % 0.75/0.68 % 0.75/0.68 === Starting SPASS-SCL-FOL A Little Less Naive, considering 78 atoms initially, heuristics mode: normal === % 0.75/0.68 % 0.75/0.68 === Clause set with instances from active satisfied. Growing active. New size: 142 % 0.75/0.68 === Clause set with instances from active satisfied. Growing active. New size: 206 % 0.75/0.68 === Clause set with instances from active satisfied. Growing active. New size: 270 % 0.75/0.68 === Backtracking. Learning clause 121:2:1:[16.2,38.2]:Top: tptpcol_4_114689(x0),tptpcol_3_98305(x0) -> % 0.75/0.68 === Clause set with instances from active satisfied. Growing active. New size: 334 % 0.75/0.68 === Clause set with instances from active satisfied. Growing active. New size: 398 % 0.75/0.68 === Backtracking. Learning clause 122:4:2:[117.1,88.2,117.1,89.1,121.2,18.2]:TopTop: genls(c_tptpcol_5_110593,x0),tptpcol_5_110593(x1),genls(x0,c_tptpcol_3_98305),tptpcol_5_114690(x1) -> % 0.75/0.68 === Clause set with instances from active satisfied. Growing active. New size: 462 % 0.75/0.68 === Clause set with instances from active satisfied. Growing active. New size: 526 % 0.75/0.68 === Clause set with instances from active satisfied. Growing active. New size: 590 % 0.75/0.68 % 0.75/0.68 SZS status Unsatisfiable % 0.75/0.68 % 0.75/0.68 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.75/0.68 % 0.75/0.68 SPASS-SCL-FOL Statistics: % 0.75/0.68 Number of learned clauses: 2 % 0.75/0.68 Number of propagations: 709 % 0.75/0.68 Number of decisions: 114 % 0.75/0.68 Number of resolutions: 39 % 0.75/0.68 Number of condensations: 0 % 0.75/0.68 Number of sub resolutions: 0 % 0.75/0.68 Number of input literals (deduplicated): 78 % 0.75/0.68 Number of grows: 8 % 0.75/0.68 Number of considered ground atoms: 590 % 0.75/0.68 % 0.75/0.68 Needed: 0:00:00.14 % 0.75/0.68 %------------------------------------------------------------------------------