%------------------------------------------------------------------------------ % File : SPASS-SCL---0.1 % Problem : SYN527+1 : TPTP v9.2.1. Released v2.1.0. % Transfm : none % Format : tptp % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % Computer : n029.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:39:57 PM UTC 2026 % Result : CounterSatisfiable 0.46s 0.59s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SYN527+1 : TPTP v9.2.1. Released v2.1.0. % 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.15/0.34 % Computer : n029.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 13:45:30 EDT 2026 % 0.15/0.34 % CPUTime : % 0.15/0.34 SPASS-SCL-FOL version: % 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode] % 0.46/0.59 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.46/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.46/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.46/0.59 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.46/0.59 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.46/0.59 Execution normal ended with status: satisfiable % 0.46/0.59 Used heuristic: normal % 0.46/0.59 % 0.46/0.59 Input Clauses: % 0.46/0.59 % 0.46/0.59 Predicates: c2_0 ndr1_0 ndr1_1 c2_2 c4_2 c5_1 c1_2 c5_2 c3_0 c2_1 c5_0 c4_0 c4_1 c3_2 c1_0 c1_1 c3_1 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 % 0.46/0.59 Fol Constants: a251 a252 a253 a254 a255 a256 a257 a258 a259 a260 a261 a262 a263 a264 a265 a266 a267 a268 a269 a270 a271 a272 a273 a274 a275 a276 % 0.46/0.59 Fol Functions: % 0.46/0.59 Problem Properties: % 0.46/0.59 This is a Bernays Schoenfinkel problem. % 0.46/0.59 % 0.46/0.59 After reduction: Problem Properties: % 0.46/0.59 This is a Bernays Schoenfinkel problem. % 0.46/0.59 % 0.46/0.59 % 0.46/0.59 Reduced Input Clauses: % 0.46/0.59 105:4:1:[19.1,18.1]:Top: ren5 -> c1_2(a256,x0),c4_2(a256,x0),c3_2(a256,x0) % 0.46/0.59 106:3:1:[24.1,27.1]:Top: ren6 -> c1_2(a258,x0),c3_2(a258,x0) % 0.46/0.59 107:4:1:[48.1,51.1]:Top: ren11,c2_2(a265,x0) -> c4_2(a265,x0),c3_2(a265,x0) % 0.46/0.59 108:3:1:[80.1,79.1]:Top: ren18 -> c1_2(a275,x0),c2_2(a275,x0) % 0.46/0.59 109:2:0:[89.1,92.0]:: c1_0,c4_0 -> % 0.46/0.59 % 0.46/0.59 Most General Atoms: ren1 ndr1_0 ren2 ren3(x0) ndr1_1(x0) ren4(x0) ren5 ren6 ren7 ren8(x0) ren9 ren10 ren11 ren12 ren13(x0) ren14 ren15(x0) ren16(x0) ren17 ren18 c2_0 c3_0 c5_0 c4_0 c1_1(x0) c4_1(x0) c4_2(x0,x1) c5_2(x0,x1) c2_2(x0,x1) c1_0 c5_1(x1) c2_1(x1) c3_2(x0,x1) c1_2(x0,x1) c3_1(x0) % 0.46/0.59 % 0.46/0.59 === Starting SPASS-SCL-FOL A Little Less Naive, considering 108 atoms initially, heuristics mode: normal === % 0.46/0.59 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 172 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 232 % 0.46/0.59 === Backtracking. Learning clause 110:8:2:[99.1,93.3,58.1,32.1]:TopTop: c5_1(x0),c3_1(x0),ndr1_0 -> c4_1(x1),ren14,c2_1(x0),c2_0,ndr1_1(x1) % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 296 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 360 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 424 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 488 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 552 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 616 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 680 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 744 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 808 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 872 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 936 % 0.46/0.59 === Clause set with instances from active satisfied. Growing active. New size: 987 % 0.46/0.59 % 0.46/0.59 Linear Model Building succeeded. % 0.46/0.59 SZS status Satisfiable % 0.46/0.59 % 0.46/0.59 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.46/0.59 % 0.46/0.59 SPASS-SCL-FOL Statistics: % 0.46/0.59 Number of learned clauses: 1 % 0.46/0.59 Number of propagations: 277 % 0.46/0.59 Number of decisions: 782 % 0.46/0.59 Number of resolutions: 3 % 0.46/0.59 Number of condensations: 0 % 0.46/0.59 Number of sub resolutions: 5 % 0.46/0.59 Number of input literals (deduplicated): 108 % 0.46/0.59 Number of grows: 14 % 0.46/0.59 Number of considered ground atoms: 987 % 0.46/0.59 % 0.46/0.59 Needed: 0:00:00.03 % 0.46/0.59 %------------------------------------------------------------------------------