%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN515-1 : TPTP v9.2.1. Released v2.1.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n019.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:56 PM UTC 2026
% Result : Satisfiable 0.37s 0.56s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN515-1 : TPTP v9.2.1. Released v2.1.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n019.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 13:44:45 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.37/0.56 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/0.56 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/0.56 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/0.56 Execution normal ended with status: satisfiable
% 0.37/0.56 Used heuristic: normal
% 0.37/0.56
% 0.37/0.56 Input Clauses:
% 0.37/0.56
% 0.37/0.56 Predicates: ndr1_0 ssSkC6 ssSkC3 ssSkC2 ssSkC1 ssSkC0 ssSkC5 c4_0 ndr1_1 ssSkP2 c5_1 c4_1 c3_1 c1_1 ssSkP1 ssSkP0 c1_0 c2_0 c1_2 c3_2 c4_2 c5_2 c2_2 c5_0 c2_1 ssSkC4 c3_0
% 0.37/0.56 Fol Constants: a24 a14 a12 a8 a25 a22 a15 a9 a5 a1 a26 a13 a10 a7 a11 a16 a6 a4 a17 a2 a19 a23 a20 a18 a21 a3
% 0.37/0.56 Fol Functions:
% 0.37/0.56 Problem Properties:
% 0.37/0.56 This is a Bernays Schoenfinkel problem.
% 0.37/0.56
% 0.37/0.56 After reduction: Problem Properties:
% 0.37/0.56 This is a Bernays Schoenfinkel problem.
% 0.37/0.56
% 0.37/0.56
% 0.37/0.56 Reduced Input Clauses:
% 0.37/0.56 90:2:0:[1.1,6.1]:: ssSkC5 -> ndr1_0
% 0.37/0.56 91:2:0:[3.1,7.0]:: -> ndr1_0,c4_0
% 0.37/0.56 93:1:0:[4.1,18.0,91.2,92.1]:: -> ndr1_0
% 0.37/0.56 94:4:1:[93.2,51.1]:Top: ssSkC3,c3_1(a16) -> c2_1(x0),c5_1(x0)
% 0.37/0.56 95:4:1:[93.2,52.1]:Top: ssSkC3,c5_1(a16) -> c2_1(x0),c5_1(x0)
% 0.37/0.56 97:4:1:[16.1,53.0,91.1,96.3]:Top: ssSkC0,c3_1(x0) -> ndr1_1(x0),c4_0
% 0.37/0.56 98:4:1:[93.2,55.2]:Top: c5_1(x0),c2_1(x0) -> ndr1_1(x0),ssSkC4
% 0.37/0.56 99:5:1:[91.1,56.3]:Top: ssSkP1(x0),ssSkC0,c3_1(x0) -> c3_2(x0,a6),c4_0
% 0.37/0.56 100:5:1:[91.1,57.3]:Top: ssSkP1(x0),ssSkC0,c3_1(x0) -> c2_2(x0,a6),c4_0
% 0.37/0.56 102:4:1:[17.1,58.0,93.2,101.2]:Top: c1_1(x0),c3_0 -> ndr1_1(x0),c5_0
% 0.37/0.56 103:3:1:[10.0,59.1]:Top: c3_2(a14,x0) -> c5_2(a14,x0),ssSkC3
% 0.37/0.56 104:4:1:[93.2,61.2]:Top: c5_1(x0),c2_1(x0) -> c5_2(x0,a17),ssSkC4
% 0.37/0.56 105:4:1:[93.2,62.2]:Top: c5_1(x0),c2_1(x0) -> c1_2(x0,a17),ssSkC4
% 0.37/0.56 106:5:1:[91.1,63.4]:Top: ssSkP1(x0),ssSkC0,c5_2(x0,a6),c3_1(x0) -> c4_0
% 0.37/0.56 107:5:1:[93.2,64.2]:Top: ssSkP0(x0),c1_1(x0),c3_0 -> c3_2(x0,a2),c5_0
% 0.37/0.56 108:4:1:[93.2,65.3]:Top: c4_2(x0,a17),c5_1(x0),c2_1(x0) -> ssSkC4
% 0.37/0.56 109:5:1:[93.2,66.3]:Top: ssSkP0(x0),c5_2(x0,a2),c1_1(x0),c3_0 -> c5_0
% 0.37/0.56 110:5:1:[93.2,68.3]:Top: c4_1(x0),c3_1(x0),c2_1(x0),c4_0 -> ndr1_1(a19)
% 0.37/0.56 111:4:1:[8.0,70.2]:Top: c1_2(a24,x0),c2_2(a24,x0) -> c4_2(a24,x0),ssSkC6
% 0.37/0.56 112:4:1:[8.0,71.2]:Top: c4_2(a24,x0),c3_2(a24,x0) -> c1_2(a24,x0),ssSkC6
% 0.37/0.56 113:6:2:[93.2,72.2]:TopTop: ssSkP2(x0),ndr1_1(x0) -> c5_2(x0,x1),c4_2(x0,x1),c2_2(x0,a23),ssSkC5
% 0.37/0.56 114:6:2:[93.2,73.2]:TopTop: ssSkP2(x0),ndr1_1(x0) -> c5_2(x0,x1),c4_2(x0,x1),c4_2(x0,a23),ssSkC5
% 0.37/0.56 115:5:1:[93.2,76.3]:Top: c4_1(x0),c3_1(x0),c2_1(x0),c4_0 -> c3_2(a19,a20)
% 0.37/0.56 116:5:1:[93.2,77.3]:Top: c4_1(x0),c3_1(x0),c2_1(x0),c2_1(a19),c4_0 ->
% 0.37/0.56 117:6:2:[93.2,78.3]:TopTop: ssSkP2(x0),ndr1_1(x0),c5_2(x0,a23) -> c5_2(x0,x1),c4_2(x0,x1),ssSkC5
% 0.37/0.56 118:5:1:[93.2,79.3]:Top: c4_1(x0),c3_1(x0),c2_1(x0),c4_2(a19,a20),c4_0 ->
% 0.37/0.56 119:8:2:[93.2,80.3]:TopTop: ssSkC4,c4_2(x0,x1),ndr1_1(x0),c5_0 -> c3_2(x0,x1),c1_2(x0,x1),c2_2(x0,a18),c1_1(x0)
% 0.37/0.56 120:8:2:[93.2,81.3]:TopTop: ssSkC4,c4_2(x0,x1),ndr1_1(x0),c5_0 -> c3_2(x0,x1),c1_2(x0,x1),c3_2(x0,a18),c1_1(x0)
% 0.37/0.56 121:7:2:[93.2,82.1]:TopTop: ssSkC3,c4_2(a16,x0),c1_2(a16,x0),c3_2(a16,x0),ndr1_1(a16) -> c2_1(x1),c5_1(x1)
% 0.37/0.56 122:8:2:[91.1,83.5]:TopTop: c2_2(x0,x1),c4_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c5_1(x0),c3_0 -> c5_2(x0,a21),c4_0
% 0.37/0.56 124:6:2:[93.2,84.3,110.5,123.6]:TopTop: c4_1(x0),c3_1(x0),c2_1(x0),c3_2(a19,x1),c4_2(a19,x1),c4_0 ->
% 0.37/0.56 125:8:2:[91.1,85.6]:TopTop: c2_2(x0,x1),c4_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c1_2(x0,a21),c5_1(x0),c3_0 -> c4_0
% 0.37/0.56 126:8:2:[91.1,86.6]:TopTop: c2_2(x0,x1),c4_2(x0,x1),c1_2(x0,x1),ndr1_1(x0),c4_2(x0,a21),c5_1(x0),c3_0 -> c4_0
% 0.37/0.56 127:8:2:[93.2,87.6]:TopTop: c5_2(x0,x1),c3_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c3_1(x0),c5_1(x0),c5_1(a3) -> c1_0
% 0.37/0.56 128:8:2:[93.2,88.6]:TopTop: c5_2(x0,x1),c3_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c3_1(x0),c5_1(x0),c3_1(a3) -> c1_0
% 0.37/0.56 129:11:3:[93.2,89.6]:TopTopTop: c5_2(x0,x1),c3_2(x0,x1),c4_2(x0,x1),ndr1_1(x0),c3_1(x0),c5_1(x0),c5_2(a3,x2),c1_2(a3,x2),ndr1_1(a3) -> c3_2(a3,x2),c1_0
% 0.37/0.56
% 0.37/0.56 Most General Atoms: ndr1_0 ssSkC6 ssSkC3 ssSkC2 ssSkC1 ssSkC0 ssSkC5 c4_0 ndr1_1(x0) ssSkP2(x0) ssSkP1(x0) ssSkP0(x0) c1_0 c2_0 c5_0 c3_1(x0) ssSkC4 c1_1(x0) c3_0 c4_1(x0) c5_2(x0,x1) c4_2(x0,x1) c3_2(x0,x1) c1_2(x0,x1) c2_1(x1) c5_1(x1) c2_2(x0,x1)
% 0.37/0.56
% 0.37/0.56 === Starting SPASS-SCL-FOL A Little Less Naive, considering 118 atoms initially, heuristics mode: normal ===
% 0.37/0.56
% 0.37/0.56 === Clause set with instances from active satisfied. Growing active. New size: 182
% 0.37/0.56 === Conflict found: 112:4:1:[8.0,71.2]:Top: c4_2(a24,x0),c3_2(a24,x0) -> c1_2(a24,x0),ssSkC6 {x0 -> a1}
% 0.37/0.56 === Backtracking. Learning clause 131:7:1:[8.0,130.2,112.1,117.5]:Top: c3_2(a24,x0),ssSkP2(a24),c5_2(a24,a23) -> c1_2(a24,x0),ssSkC6,c5_2(a24,x0),ssSkC5
% 0.37/0.56 === Clause set with instances from active satisfied. Growing active. New size: 246
% 0.37/0.56 === Backtracking. Learning clause 132:3:0:[69.2,31.1,44.1,45.1,17.1]:: ssSkC2 -> c4_0,ssSkP0(a13)
% 0.37/0.56 === Clause set with instances from active satisfied. Growing active. New size: 310
% 0.37/0.56 === Clause set with instances from active satisfied. Growing active. New size: 374
% 0.37/0.56 === Clause set with instances from active satisfied. Growing active. New size: 438
% 0.37/0.56
% 0.37/0.56 Linear Model Building succeeded.
% 0.37/0.56 SZS status Satisfiable
% 0.37/0.56
% 0.37/0.56 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.37/0.56
% 0.37/0.56 SPASS-SCL-FOL Statistics:
% 0.37/0.56 Number of learned clauses: 2
% 0.37/0.56 Number of propagations: 142
% 0.37/0.56 Number of decisions: 467
% 0.37/0.56 Number of resolutions: 5
% 0.37/0.56 Number of condensations: 0
% 0.37/0.56 Number of sub resolutions: 41
% 0.37/0.56 Number of input literals (deduplicated): 118
% 0.37/0.56 Number of grows: 5
% 0.37/0.56 Number of considered ground atoms: 438
% 0.37/0.56
% 0.37/0.56 Needed: 0:00:00.02
% 0.37/0.56
%------------------------------------------------------------------------------