%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : CSR049+1 : 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 : n014.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:19:50 PM UTC 2026 % Result : Theorem 8.87s 2.91s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.37 % Problem : CSR049+1 : TPTP v9.2.1. Released v3.4.0. % 0.11/0.38 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 0.13/0.59 % Computer : n014.cluster.edu % 0.13/0.59 % Model : x86_64 x86_64 % 0.13/0.59 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.59 % Memory : 8042.1875MB % 0.13/0.59 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.59 % CPULimit : 300 % 0.13/0.59 % WCLimit : 300 % 0.13/0.59 % DateTime : Thu May 7 11:39:53 EDT 2026 % 0.13/0.59 % CPUTime : % 0.13/0.59 SPASS-SCL-FOL version: % 0.18/0.68 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 8.87/2.91 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 8.87/2.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 8.87/2.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 8.87/2.91 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 8.87/2.91 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p % 8.87/2.91 Execution normal ended with status: unsatisfiable % 8.87/2.91 Used heuristic: normal % 8.87/2.91 % 8.87/2.91 Input Clauses: % 8.87/2.91 % 8.87/2.91 Predicates: genlmt transitivebinarypredicate genls tptpcol_2_2 tptpcol_1_1 tptpcol_3_16386 tptpcol_4_24578 tptpcol_5_24579 tptpcol_6_26627 tptpcol_7_26628 tptpcol_8_26629 tptpcol_9_26885 tptpcol_10_26886 tptpcol_11_26887 tptpcol_12_26919 tptpcol_13_26920 tptpcol_14_26921 tptpcol_15_26925 tptpcol_16_26926 tptpcol_2_65537 tptpcol_1_65536 tptpcol_3_81921 tptpcol_4_90113 tptpcol_5_90114 tptpcol_6_92162 tptpcol_7_92163 tptpcol_8_92164 tptpcol_9_92165 tptpcol_10_92166 tptpcol_11_92230 tptpcol_12_92262 tptpcol_13_92263 tptpcol_14_92264 tptpcol_15_92268 tptpcol_16_92269 disjointwith isa genlinverse genlpreds predicate binarypredicate collection thing mtvisible microtheory % 8.87/2.91 Fol Constants: c_gregoriancalendarmt c_basekb c_unitedstatesgeographypeoplemt c_peopledatamt c_unitedstatessociallifemt c_genlmt c_universalvocabularymt c_tptpcol_2_2 c_tptpcol_1_1 c_tptpcol_3_16386 c_tptpcol_4_24578 c_tptpcol_5_24579 c_tptpcol_6_26627 c_tptpcol_7_26628 c_tptpcol_8_26629 c_tptpcol_9_26885 c_tptpcol_10_26886 c_tptpcol_11_26887 c_tptpcol_12_26919 c_tptpcol_13_26920 c_tptpcol_14_26921 c_tptpcol_15_26925 c_tptpcol_16_26926 c_tptpcol_2_65537 c_tptpcol_1_65536 c_tptpcol_3_81921 c_tptpcol_4_90113 c_tptpcol_5_90114 c_tptpcol_6_92162 c_tptpcol_7_92163 c_tptpcol_8_92164 c_tptpcol_9_92165 c_tptpcol_10_92166 c_tptpcol_11_92230 c_tptpcol_12_92262 c_tptpcol_13_92263 c_tptpcol_14_92264 c_tptpcol_15_92268 c_tptpcol_16_92269 c_transitivebinarypredicate % 8.87/2.91 Fol Functions: % 8.87/2.91 Problem Properties: % 8.87/2.91 This is a Bernays Schoenfinkel problem. % 8.87/2.91 % 8.87/2.91 After reduction: Problem Properties: % 8.87/2.91 This is a Bernays Schoenfinkel problem. % 8.87/2.91 % 8.87/2.91 % 8.87/2.91 Reduced Input Clauses: % 8.87/2.91 % 8.87/2.91 Most General Atoms: tptpcol_2_2(x0) tptpcol_1_1(x0) tptpcol_3_16386(x0) tptpcol_4_24578(x0) tptpcol_5_24579(x0) tptpcol_6_26627(x0) tptpcol_7_26628(x0) tptpcol_8_26629(x0) tptpcol_9_26885(x0) tptpcol_10_26886(x0) tptpcol_11_26887(x0) tptpcol_12_26919(x0) tptpcol_13_26920(x0) tptpcol_14_26921(x0) tptpcol_15_26925(x0) tptpcol_16_26926(x0) tptpcol_2_65537(x0) tptpcol_1_65536(x0) tptpcol_3_81921(x0) tptpcol_4_90113(x0) tptpcol_5_90114(x0) tptpcol_6_92162(x0) tptpcol_7_92163(x0) tptpcol_8_92164(x0) tptpcol_9_92165(x0) tptpcol_10_92166(x0) tptpcol_11_92230(x0) tptpcol_12_92262(x0) tptpcol_13_92263(x0) tptpcol_14_92264(x0) tptpcol_15_92268(x0) tptpcol_16_92269(x0) isa(x0,x2) predicate(x0) binarypredicate(x0) genlpreds(x2,x0) genlinverse(x0,x2) collection(x0) disjointwith(x2,x1) genlmt(x0,x2) microtheory(x1) mtvisible(x1) genls(x0,x2) transitivebinarypredicate(x0) thing(x0) % 8.87/2.91 % 8.87/2.91 === Starting SPASS-SCL-FOL A Little Less Naive, considering 122 atoms initially, heuristics mode: normal === % 8.87/2.91 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 186 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 250 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 314 % 8.87/2.91 === Backtracking. Learning clause 179:5:4:[168.3,168.1,173.3]:TopTopTopTop: mtvisible(x0),genlmt(x1,x2),genlmt(x0,x3),genlmt(x3,x1) -> mtvisible(x2) % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 378 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 442 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 506 % 8.87/2.91 === Backtracking. Learning clause 180:4:2:[166.1,114.2,91.1,42.2,44.2,46.2,48.2,50.2,52.2,54.2,56.2,159.3]:TopTop: tptpcol_11_92230(x0),genls(c_tptpcol_3_81921,x1),genls(x1,c_tptpcol_14_92264) -> tptpcol_14_92264(x0) % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 570 % 8.87/2.91 === Backtracking. Learning clause 181:2:1:[10.2,8.1,12.2,14.2,16.2,18.2,20.2,22.2,24.2,26.2,28.2]:Top: tptpcol_12_26919(x0) -> tptpcol_1_1(x0) % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 634 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 698 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 762 % 8.87/2.91 === Backtracking. Learning clause 182:3:1:[166.3,89.1,114.2,42.2,44.2,46.2,48.2,50.2,52.2,54.2]:Top: genls(c_tptpcol_3_81921,c_tptpcol_15_92268),tptpcol_10_92166(x0) -> tptpcol_15_92268(x0) % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 826 % 8.87/2.91 === Backtracking. Learning clause 183:2:1:[18.2,16.1]:Top: tptpcol_7_26628(x0) -> tptpcol_5_24579(x0) % 8.87/2.91 === Backtracking. Learning clause 184:4:4:[69.1,166.3]:TopTopTopTop: isa(x0,x1),disjointwith(x2,x1),isa(x0,x3),genls(x3,x2) -> % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 890 % 8.87/2.91 === Backtracking. Learning clause 185:3:1:[50.2,106.1,52.2,54.2,56.2,166.1,117.1,58.2]:Top: genls(c_tptpcol_7_92163,c_tptpcol_2_65537),tptpcol_12_92262(x0) -> tptpcol_2_65537(x0) % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 954 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 1018 % 8.87/2.91 === Clause set with instances from active satisfied. Growing active. New size: 1082 % 8.87/2.91 % 8.87/2.91 SZS status Unsatisfiable % 8.87/2.91 % 8.87/2.91 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 8.87/2.91 % 8.87/2.91 SPASS-SCL-FOL Statistics: % 8.87/2.91 Number of learned clauses: 7 % 8.87/2.91 Number of propagations: 3311 % 8.87/2.91 Number of decisions: 368 % 8.87/2.91 Number of resolutions: 102 % 8.87/2.91 Number of condensations: 0 % 8.87/2.91 Number of sub resolutions: 0 % 8.87/2.91 Number of input literals (deduplicated): 122 % 8.87/2.91 Number of grows: 15 % 8.87/2.91 Number of considered ground atoms: 1082 % 8.87/2.91 % 8.87/2.91 Needed: 0:00:02.14 % 8.87/2.91 %------------------------------------------------------------------------------