%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN526-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 : n002.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 : Satisfiable 0.30s 0.55s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN526-1 : TPTP v9.2.1. Released v2.1.0.
% 0.11/0.12 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.33 % Computer : n002.cluster.edu
% 0.15/0.33 % Model : x86_64 x86_64
% 0.15/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.33 % Memory : 8042.1875MB
% 0.15/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.33 % CPULimit : 300
% 0.15/0.33 % WCLimit : 300
% 0.15/0.33 % DateTime : Thu May 7 13:45:32 EDT 2026
% 0.15/0.33 % CPUTime :
% 0.15/0.33 SPASS-SCL-FOL version:
% 0.18/0.41 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.30/0.55 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.55 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.55 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.55 Execution resolution_3 ended with status: satisfiable
% 0.30/0.55 Used heuristic: resolution_3
% 0.30/0.55
% 0.30/0.55 Input Clauses:
% 0.30/0.55
% 0.30/0.55 Predicates: ndr1_0 c3_0 c2_0 ssSkC8 ssSkC7 ssSkC4 ssSkC0 ndr1_1 c3_1 ssSkC9 ssSkC5 ssSkC6 c5_0 c4_0 ssSkP0 c2_1 c5_1 c4_2 c2_2 ssSkC1 c4_1 c1_2 c3_2 c5_2 c1_0 ssSkC2 ssSkC3 c1_1
% 0.30/0.55 Fol Constants: a248 a236 a223 a249 a240 a221 a245 a242 a227 a224 a247 a241 a237 a225 a222 a232 a229 a226 a235 a238 a243 a228 a230 a246 a233 a239 a219 a231 a244 a234 a218 a250 a220
% 0.30/0.55 Fol Functions:
% 0.30/0.55 Problem Properties:
% 0.30/0.55 This is a Bernays Schoenfinkel problem.
% 0.30/0.55
% 0.30/0.55 After reduction: Problem Properties:
% 0.30/0.55 This is a Bernays Schoenfinkel problem.
% 0.30/0.55
% 0.30/0.55
% 0.30/0.55 Reduced Input Clauses:
% 0.30/0.55 114:2:0:[3.1,9.0]:: ssSkC9 -> ndr1_0
% 0.30/0.55 116:1:0:[5.1,22.0,1.1,115.1]:: -> ndr1_0
% 0.30/0.55 170:13:4:[116.2,113.3]:TopTopTopTop: c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c2_2(x2,x3),ndr1_1(x2),c3_2(x2,a220),c2_1(x2),c4_0 -> c2_2(x0,x1),c2_1(x0),c5_1(x0),c4_2(x2,x3),c3_2(x2,x3)
% 0.30/0.55 169:13:4:[116.2,112.3]:TopTopTopTop: c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c2_2(x2,x3),ndr1_1(x2),c2_1(x2),c4_0 -> c2_2(x0,x1),c2_1(x0),c5_1(x0),c4_2(x2,x3),c3_2(x2,x3),c4_2(x2,a220)
% 0.30/0.55 117:2:0:[12.1,52.1]:: c1_0,c3_0 ->
% 0.30/0.55 118:4:1:[116.2,53.2]:Top: ssSkC2,ssSkC3 -> ndr1_1(x0),c5_1(x0)
% 0.30/0.55 119:3:1:[116.2,55.1]:Top: c2_1(x0) -> ndr1_1(x0),ssSkC5
% 0.30/0.55 120:4:1:[116.2,56.1]:Top: ssSkC7,c4_0 -> ndr1_1(x0),c4_1(x0)
% 0.30/0.55 121:4:1:[116.2,57.2]:Top: ssSkC2,ssSkC3 -> c4_2(x0,a235),c5_1(x0)
% 0.30/0.55 122:4:1:[116.2,58.2]:Top: ssSkC2,ssSkC3 -> c1_2(x0,a235),c5_1(x0)
% 0.30/0.55 123:4:1:[116.2,59.0]:Top: -> ndr1_1(x0),c1_1(x0),c3_1(x0),ssSkC9
% 0.30/0.55 125:3:1:[14.1,60.0,116.2,124.1]:Top: -> ndr1_1(x0),c5_1(x0),ssSkC1
% 0.30/0.55 126:3:1:[116.2,61.1]:Top: c2_1(x0) -> c3_2(x0,a238),ssSkC5
% 0.30/0.55 127:3:1:[116.2,62.1]:Top: c2_1(x0) -> c1_2(x0,a238),ssSkC5
% 0.30/0.55 128:4:1:[116.2,63.1]:Top: ssSkC7,c4_0 -> c1_2(x0,a243),c4_1(x0)
% 0.30/0.55 129:4:1:[116.2,64.3]:Top: ssSkC2,ssSkC3,c5_2(x0,a235) -> c5_1(x0)
% 0.30/0.55 130:4:1:[116.2,65.1]:Top: c2_1(x0) -> ndr1_1(x0),c4_1(x0),ssSkC2
% 0.30/0.55 131:4:1:[116.2,66.1]:Top: ssSkP0(x0) -> c1_2(x0,a228),c5_1(x0),ssSkC1
% 0.30/0.55 132:5:1:[11.0,67.1]:Top: c2_1(x0) -> ndr1_1(x0),c4_1(x0),c5_0,c4_0
% 0.30/0.55 133:3:1:[116.2,68.2]:Top: c2_2(x0,a238),c2_1(x0) -> ssSkC5
% 0.30/0.55 134:4:1:[116.2,69.2]:Top: ssSkC7,c5_2(x0,a243),c4_0 -> c4_1(x0)
% 0.30/0.55 135:4:1:[116.2,70.1]:Top: c2_1(x0),c4_0 -> c5_1(x0),ndr1_1(a230)
% 0.30/0.55 136:4:1:[116.2,71.1]:Top: c2_1(x0),c4_0 -> c5_1(x0),c2_1(a230)
% 0.30/0.55 137:4:1:[116.2,72.1]:Top: c2_1(x0),c4_0 -> c5_1(x0),c3_1(a230)
% 0.30/0.55 138:4:1:[116.2,73.1]:Top: c1_2(x0,a246) -> c1_1(x0),c3_1(x0),ssSkC9
% 0.30/0.55 139:4:1:[116.2,74.1]:Top: c2_2(x0,a246) -> c1_1(x0),c3_1(x0),ssSkC9
% 0.30/0.55 140:4:1:[116.2,75.1]:Top: c3_2(x0,a246) -> c1_1(x0),c3_1(x0),ssSkC9
% 0.30/0.55 141:4:1:[116.2,76.2]:Top: c4_1(x0),c3_1(x0) -> ndr1_1(x0),ssSkC6
% 0.30/0.55 142:4:1:[116.2,77.1]:Top: c2_1(x0) -> c3_2(x0,a233),c4_1(x0),ssSkC2
% 0.30/0.55 143:4:1:[116.2,78.1]:Top: c2_1(x0) -> c2_2(x0,a233),c4_1(x0),ssSkC2
% 0.30/0.55 144:4:1:[116.2,79.2]:Top: ssSkP0(x0),c2_2(x0,a228) -> c5_1(x0),ssSkC1
% 0.30/0.55 145:5:1:[116.2,80.0]:Top: c1_0,c4_0 -> c2_1(x0),c3_1(x0),c4_1(x0)
% 0.30/0.55 146:4:1:[116.2,83.2]:Top: c4_1(x0),c3_1(x0) -> c2_2(x0,a239),ssSkC6
% 0.30/0.55 147:4:1:[116.2,84.2]:Top: c5_2(x0,a233),c2_1(x0) -> c4_1(x0),ssSkC2
% 0.30/0.55 148:5:1:[11.0,85.2]:Top: c1_2(x0,a219),c2_1(x0) -> c4_1(x0),c5_0,c4_0
% 0.30/0.55 149:5:1:[11.0,86.2]:Top: c2_2(x0,a219),c2_1(x0) -> c4_1(x0),c5_0,c4_0
% 0.30/0.55 150:5:1:[11.0,87.2]:Top: c3_2(x0,a219),c2_1(x0) -> c4_1(x0),c5_0,c4_0
% 0.30/0.55 151:4:1:[116.2,89.1]:Top: c2_1(x0),c1_2(a230,a231),c4_0 -> c5_1(x0)
% 0.30/0.55 152:4:1:[116.2,90.1]:Top: c2_1(x0),c5_2(a230,a231),c4_0 -> c5_1(x0)
% 0.30/0.55 153:4:1:[116.2,91.3]:Top: c5_2(x0,a239),c4_1(x0),c3_1(x0) -> ssSkC6
% 0.30/0.55 154:4:1:[116.2,92.3]:Top: c4_2(x0,a239),c4_1(x0),c3_1(x0) -> ssSkC6
% 0.30/0.55 155:5:1:[25.0,96.2]:Top: c2_2(a221,x0),c1_2(a221,x0) -> c5_2(a221,x0),c5_0,c4_0
% 0.30/0.55 156:7:2:[116.2,99.3]:TopTop: c5_2(x0,x1),ndr1_1(x0),c5_1(x0),c5_0 -> c3_2(x0,x1),c4_2(x0,x1),c5_2(x0,a244)
% 0.30/0.55 157:7:2:[116.2,100.3]:TopTop: c5_2(x0,x1),ndr1_1(x0),c5_1(x0),c5_0 -> c3_2(x0,x1),c4_2(x0,x1),c2_2(x0,a244)
% 0.30/0.55 158:7:2:[116.2,101.4]:TopTop: c5_2(x0,x1),ndr1_1(x0),c3_2(x0,a244),c5_1(x0),c5_0 -> c3_2(x0,x1),c4_2(x0,x1)
% 0.30/0.55 159:8:3:[116.2,102.4]:TopTopTop: c3_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_1(x0),c5_0 -> c3_1(x0),ndr1_1(x2),c1_1(x2)
% 0.30/0.55 160:7:2:[116.2,103.5]:TopTop: c2_2(x0,x1),c4_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c1_1(x0) -> c4_2(x0,a234),ssSkC3
% 0.30/0.55 161:8:3:[116.2,104.4]:TopTopTop: c3_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_1(x0),c5_0 -> c3_1(x0),c5_2(x2,a218),c1_1(x2)
% 0.30/0.55 162:8:3:[116.2,105.4]:TopTopTop: c3_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_1(x0),c5_0 -> c3_1(x0),c1_2(x2,a218),c1_1(x2)
% 0.30/0.55 163:7:2:[116.2,106.6]:TopTop: c2_2(x0,x1),c4_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c5_2(x0,a234),c1_1(x0) -> ssSkC3
% 0.30/0.55 164:8:3:[116.2,107.4]:TopTopTop: c3_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_1(x0),c3_2(x2,a218),c5_0 -> c3_1(x0),c1_1(x2)
% 0.30/0.55 165:9:3:[116.2,108.5]:TopTopTop: c4_2(x0,x1),c1_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_1(x0),c3_1(x2) -> c5_1(x0),ndr1_1(x2),c4_1(x2)
% 0.30/0.55 166:9:3:[116.2,109.5]:TopTopTop: c4_2(x0,x1),c1_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_1(x0),c3_1(x2) -> c5_1(x0),c4_2(x2,a250),c4_1(x2)
% 0.30/0.55 167:9:3:[116.2,110.5]:TopTopTop: c4_2(x0,x1),c1_2(x0,x1),c5_2(x0,x1),ndr1_1(x0),c2_1(x0),c5_2(x2,a250),c3_1(x2) -> c5_1(x0),c4_1(x2)
% 0.30/0.55 168:13:4:[116.2,111.3]:TopTopTopTop: c5_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c2_2(x2,x3),ndr1_1(x2),c2_1(x2),c4_0 -> c2_2(x0,x1),c2_1(x0),c5_1(x0),c4_2(x2,x3),c3_2(x2,x3),c1_2(x2,a220)
% 0.30/0.55
% 0.30/0.55 Most General Atoms: ndr1_0 c3_0 c2_0 ssSkC8 ssSkC7 ssSkC4 ssSkC0 ssSkC9 ssSkC5 ssSkC6 c5_0 c4_0 ssSkP0(x0) c5_2(x0,x1) c1_2(x0,x1) ndr1_1(x2) c2_2(x0,x1) c2_1(x0) c5_1(x0) ssSkC1 c1_0 ssSkC2 ssSkC3 c3_2(x0,x1) c4_2(x0,x1) c1_1(x2) c3_1(x2) c4_1(x2)
% 0.30/0.55
% 0.30/0.55 === Starting SPASS-SCL-FOL A Little Less Naive, considering 63 atoms initially, heuristics mode: resolution_3 ===
% 0.30/0.55
% 0.30/0.55 === Conflict found: 119:3:1:[116.2,55.1]:Top: c2_1(x0) -> ndr1_1(x0),ssSkC5 {x0 -> a237}
% 0.30/0.55 === Backtracking. Learning clause 171:4:0:[119.1,39.3]:: ssSkC4,c3_0 -> ndr1_1(a237),ssSkC5
% 0.30/0.55 === Conflict found: 118:4:1:[116.2,53.2]:Top: ssSkC2,ssSkC3 -> ndr1_1(x0),c5_1(x0) {x0 -> a245}
% 0.30/0.55 === Backtracking. Learning clause 172:4:0:[118.4,26.1]:: ssSkC2,ssSkC3 -> ndr1_1(a245),ssSkC8
% 0.30/0.55 === Conflict found: 135:4:1:[116.2,70.1]:Top: c2_1(x0),c4_0 -> c5_1(x0),ndr1_1(a230) {x0 -> a245}
% 0.30/0.55 === Backtracking. Learning clause 173:4:0:[135.3,26.1]:: c2_1(a245),c4_0 -> ndr1_1(a230),ssSkC8
% 0.30/0.55 === Backtracking. Learning clause 174:4:0:[81.3,43.1]:: c3_2(a245,a227),ndr1_1(a245) -> ssSkC8,ssSkP0(a245)
% 0.30/0.55 === Backtracking. Learning clause 177:4:0:[118.2,175.1,26.0,176.5,81.3,129.3]:: c3_2(a245,a235),ssSkC2,ssSkC3 -> ssSkC8
% 0.30/0.55 === Clause set with instances from active satisfied. Growing active. New size: 130
% 0.30/0.55 === Restarting.
% 0.30/0.55 === Clause set with instances from active satisfied. Growing active. New size: 201
% 0.30/0.55 === Restarting.
% 0.30/0.55 === Backtracking. Learning clause 178:6:0:[97.6,43.1]:: ssSkC4,c3_2(a237,a227),c2_2(a237,a227),ndr1_1(a237),c3_0 -> ssSkP0(a237)
% 0.30/0.55 === Clause set with instances from active satisfied. Growing active. New size: 269
% 0.30/0.55 === Restarting.
% 0.30/0.55 === Backtracking. Learning clause 179:6:1:[97.6,88.2]:Top: c3_2(a237,x0),c2_2(a237,x0),ssSkC4,ndr1_1(a237),c3_0 -> c4_2(a237,x0)
% 0.30/0.55 === Clause set with instances from active satisfied. Growing active. New size: 274
% 0.30/0.55 === Restarting.
% 0.30/0.55 === Clause set with instances from active satisfied. Growing active. New size: 338
% 0.30/0.55
% 0.30/0.55 Linear Model Building succeeded.
% 0.30/0.55 SZS status Satisfiable
% 0.30/0.55
% 0.30/0.55 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.55
% 0.30/0.55 SPASS-SCL-FOL Statistics:
% 0.30/0.55 Number of learned clauses: 7
% 0.30/0.55 Number of propagations: 391
% 0.30/0.55 Number of decisions: 963
% 0.30/0.55 Number of resolutions: 7
% 0.30/0.55 Number of condensations: 0
% 0.30/0.55 Number of sub resolutions: 59
% 0.30/0.55 Number of input literals (deduplicated): 131
% 0.30/0.55 Number of grows: 5
% 0.30/0.55 Number of considered ground atoms: 338
% 0.30/0.55
% 0.30/0.55 Needed: 0:00:00.05
% 0.30/0.55
%------------------------------------------------------------------------------