%------------------------------------------------------------------------------
% 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 : n011.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.43s 0.63s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.13 % Problem : SYN527-1 : TPTP v9.2.1. Released v2.1.0.
% 0.12/0.14 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/0.36 % Computer : n011.cluster.edu
% 0.18/0.36 % Model : x86_64 x86_64
% 0.18/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/0.36 % Memory : 8042.1875MB
% 0.18/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.18/0.36 % CPULimit : 300
% 0.18/0.36 % WCLimit : 300
% 0.18/0.36 % DateTime : Thu May 7 13:45:03 EDT 2026
% 0.18/0.36 % CPUTime :
% 0.18/0.36 SPASS-SCL-FOL version:
% 0.30/0.46 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.63 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.63 Execution normal ended with status: satisfiable
% 0.43/0.63 Used heuristic: normal
% 0.43/0.63
% 0.43/0.63 Input Clauses:
% 0.43/0.63
% 0.43/0.63 Predicates: ndr1_0 ssSkC0 c5_0 c3_0 c1_0 c2_0 c4_0 ndr1_1 ssSkP1 ssSkP0 c5_1 c4_1 c5_2 c2_1 c2_2 c1_1 c3_2 c1_2 c4_2 c3_1 ssSkC1
% 0.43/0.63 Fol Constants: a251 a264 a262 a258 a256 a252 a254 a263 a260 a259 a257 a253 a272 a274 a267 a265 a268 a266 a261 a269 a275 a255 a276 a270 a271 a273
% 0.43/0.63 Fol Functions:
% 0.43/0.63 Problem Properties:
% 0.43/0.63 This is a Bernays Schoenfinkel problem.
% 0.43/0.63
% 0.43/0.63 After reduction: Problem Properties:
% 0.43/0.63 This is a Bernays Schoenfinkel problem.
% 0.43/0.63
% 0.43/0.63
% 0.43/0.63 Reduced Input Clauses:
% 0.43/0.63 85:2:0:[4.0,5.2]:: -> ndr1_0,c4_0
% 0.43/0.63 87:1:0:[1.1,6.0,4.0,86.2]:: -> ndr1_0
% 0.43/0.63 88:2:0:[85.1,19.1]:: c3_0 -> ndr1_0
% 0.43/0.63 89:3:1:[87.1,43.0]:Top: -> ndr1_1(x0),c1_1(x0),c2_0
% 0.43/0.63 90:2:0:[7.1,48.0]:: c1_0,c4_0 ->
% 0.43/0.63 91:3:1:[87.1,54.0]:Top: -> c4_2(x0,a261),c1_1(x0),c2_0
% 0.43/0.63 92:3:1:[87.1,55.0]:Top: -> c1_2(x0,a261),c1_1(x0),c2_0
% 0.43/0.63 93:3:1:[87.1,56.0]:Top: -> c3_2(x0,a261),c1_1(x0),c2_0
% 0.43/0.63 94:3:1:[87.1,57.1]:Top: c4_1(x0) -> c2_1(x0),c3_0
% 0.43/0.63 95:4:1:[87.1,59.0]:Top: c3_0 -> c3_1(x0),c4_1(x0),c1_0
% 0.43/0.63 96:4:1:[87.1,60.1]:Top: c1_1(x0) -> ndr1_1(x0),c4_1(x0),ssSkC1
% 0.43/0.63 98:4:1:[10.1,61.0,87.1,97.2]:Top: c2_1(x0) -> ndr1_1(x0),c3_0,c2_0
% 0.43/0.63 99:3:1:[15.1,63.0]:Top: c2_0 -> c1_2(a258,x0),c3_2(a258,x0)
% 0.43/0.63 100:4:1:[87.1,64.1]:Top: c1_1(x0) -> c5_2(x0,a269),c4_1(x0),ssSkC1
% 0.43/0.63 101:5:1:[85.0,65.1]:Top: c2_1(x0) -> c4_1(x0),c3_1(x0),ndr1_1(a275),c4_0
% 0.43/0.63 102:5:1:[87.1,66.2]:Top: ssSkP0(x0),c2_1(x0) -> c4_2(x0,a255),c3_0,c2_0
% 0.43/0.63 103:4:1:[87.1,67.2]:Top: c3_2(x0,a269),c1_1(x0) -> c4_1(x0),ssSkC1
% 0.43/0.63 104:5:1:[85.0,68.1]:Top: c2_1(x0) -> c4_1(x0),c3_1(x0),c1_2(a275,a276),c4_0
% 0.43/0.63 105:5:1:[85.0,69.1]:Top: c2_1(x0) -> c4_1(x0),c3_1(x0),c4_2(a275,a276),c4_0
% 0.43/0.63 106:5:1:[87.1,70.3]:Top: ssSkC1,c5_1(x0),c3_1(x0) -> c2_1(x0),ndr1_1(a270)
% 0.43/0.63 107:5:1:[87.1,71.3]:Top: ssSkC1,c5_1(x0),c3_1(x0) -> c2_1(x0),c4_1(a270)
% 0.43/0.63 108:5:1:[87.1,72.3]:Top: ssSkP0(x0),c1_2(x0,a255),c2_1(x0) -> c3_0,c2_0
% 0.43/0.63 109:5:1:[87.1,73.3]:Top: ssSkP0(x0),c5_2(x0,a255),c2_1(x0) -> c3_0,c2_0
% 0.43/0.63 110:5:1:[85.0,74.1]:Top: c2_1(x0),c5_2(a275,a276) -> c4_1(x0),c3_1(x0),c4_0
% 0.43/0.63 111:5:1:[87.1,75.3]:Top: ssSkC1,c5_1(x0),c3_1(x0) -> c2_1(x0),c3_2(a270,a271)
% 0.43/0.63 112:5:1:[87.1,76.3]:Top: ssSkC1,c5_1(x0),c3_1(x0) -> c2_1(x0),c5_2(a270,a271)
% 0.43/0.63 113:5:1:[87.1,77.3]:Top: ssSkC1,c5_1(x0),c3_1(x0),c5_1(a270) -> c2_1(x0)
% 0.43/0.63 114:5:1:[16.0,78.0]:Top: -> c1_2(a256,x0),c4_2(a256,x0),c3_2(a256,x0),c4_0,c2_0
% 0.43/0.63 115:5:1:[87.1,79.3]:Top: ssSkC1,c5_1(x0),c3_1(x0),c2_2(a270,a271) -> c2_1(x0)
% 0.43/0.63 116:5:1:[40.2,80.1]:Top: c2_2(a265,x0),c3_0,c4_0 -> c4_2(a265,x0),c3_2(a265,x0)
% 0.43/0.63 118:6:2:[85.0,81.1,101.4,117.2]:TopTop: c2_1(x0) -> c4_1(x0),c3_1(x0),c1_2(a275,x1),c2_2(a275,x1),c4_0
% 0.43/0.63 119:7:2:[87.1,82.4]:TopTop: ssSkP1(x0),c3_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c3_0 -> c1_2(x0,x1),c2_2(x0,a273)
% 0.43/0.63 120:7:2:[87.1,83.5]:TopTop: ssSkP1(x0),c3_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c5_2(x0,a273),c3_0 -> c1_2(x0,x1)
% 0.43/0.63 121:8:2:[85.0,84.6]:TopTop: c4_2(x0,x1),c5_2(x0,x1),c2_2(x0,x1),ndr1_1(x0),c1_1(x0),c4_1(x0) -> c1_0,c4_0
% 0.43/0.63
% 0.43/0.63 Most General Atoms: ndr1_0 ssSkC0 c5_0 c3_0 c1_0 c2_0 c4_0 ndr1_1(x0) ssSkP1(x0) ssSkP0(x0) c1_1(x0) c4_1(x0) c2_1(x0) c3_1(x0) ssSkC1 c5_1(x0) c3_2(x0,x1) c2_2(x0,x1) c1_2(x0,x1) c4_2(x0,x1) c5_2(x0,x1)
% 0.43/0.63
% 0.43/0.63 === Starting SPASS-SCL-FOL A Little Less Naive, considering 94 atoms initially, heuristics mode: normal ===
% 0.43/0.63
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 133
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 197
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 261
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 325
% 0.43/0.63 === Conflict found: 99:3:1:[15.1,63.0]:Top: c2_0 -> c1_2(a258,x0),c3_2(a258,x0) {x0 -> a272}
% 0.43/0.63 === Backtracking. Learning clause 123:6:1:[15.1,122.3,99.3,119.2]:Top: c2_0,ssSkP1(a258),c2_2(a258,x0),c3_0 -> c1_2(a258,x0),c2_2(a258,a273)
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 389
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 453
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 517
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 581
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 645
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 709
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 773
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 833
% 0.43/0.63 === Clause set with instances from active satisfied. Growing active. New size: 897
% 0.43/0.63
% 0.43/0.63 Linear Model Building succeeded.
% 0.43/0.63 SZS status Satisfiable
% 0.43/0.63
% 0.43/0.63 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.63
% 0.43/0.63 SPASS-SCL-FOL Statistics:
% 0.43/0.63 Number of learned clauses: 1
% 0.43/0.63 Number of propagations: 109
% 0.43/0.63 Number of decisions: 885
% 0.43/0.63 Number of resolutions: 1
% 0.43/0.63 Number of condensations: 0
% 0.43/0.63 Number of sub resolutions: 38
% 0.43/0.63 Number of input literals (deduplicated): 94
% 0.43/0.63 Number of grows: 13
% 0.43/0.63 Number of considered ground atoms: 897
% 0.43/0.63
% 0.43/0.63 Needed: 0:00:00.01
% 0.43/0.63
%------------------------------------------------------------------------------