%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN530+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 : n007.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:58 PM UTC 2026
% Result : CounterSatisfiable 0.43s 0.66s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.15 % Problem : SYN530+1 : TPTP v9.2.1. Released v2.1.0.
% 0.10/0.16 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.39 % Computer : n007.cluster.edu
% 0.20/0.39 % Model : x86_64 x86_64
% 0.20/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.39 % Memory : 8042.1875MB
% 0.20/0.39 % OS : Linux 3.10.0-693.el7.x86_64
% 0.20/0.39 % CPULimit : 300
% 0.20/0.39 % WCLimit : 300
% 0.20/0.40 % DateTime : Thu May 7 13:44:39 EDT 2026
% 0.20/0.40 % CPUTime :
% 0.20/0.40 SPASS-SCL-FOL version:
% 0.29/0.50 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.43/0.66 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.66 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.66 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.66 Execution resolution_2 ended with status: satisfiable
% 0.43/0.66 Used heuristic: resolution_2
% 0.43/0.66
% 0.43/0.66 Input Clauses:
% 0.43/0.66
% 0.43/0.66 Predicates: ndr1_0 c5_1 c1_1 ndr1_1 c5_2 c1_2 c3_2 c2_1 c3_1 c5_0 c1_0 c2_2 c2_0 c4_2 c4_1 c3_0 c4_0 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20 ren21 ren22 ren23 ren24
% 0.43/0.66 Fol Constants: a357 a358 a359 a360 a361 a362 a363 a364 a365 a366 a367 a368 a369 a370 a371 a372 a373 a374 a375 a376 a377 a378 a379 a380 a381 a382 a383 a384 a385 a386
% 0.43/0.66 Fol Functions:
% 0.43/0.66 Problem Properties:
% 0.43/0.66 This is a Bernays Schoenfinkel problem.
% 0.43/0.66
% 0.43/0.66 After reduction: Problem Properties:
% 0.43/0.66 This is a Bernays Schoenfinkel problem.
% 0.43/0.66
% 0.43/0.66
% 0.43/0.66 Reduced Input Clauses:
% 0.43/0.66 122:3:1:[21.1,26.1]:Top: ren6,c3_2(a363,x0) -> c1_2(a363,x0)
% 0.43/0.66 123:4:1:[50.1,49.1]:Top: ren13,c5_2(a371,x0),c1_2(a371,x0) -> c4_2(a371,x0)
% 0.43/0.66 124:2:0:[113.0,108.1]:: c3_0 -> c5_0
% 0.43/0.66 125:7:2:[112.1,115.4]:TopTop: ndr1_0,ndr1_1(x0),c3_2(x0,x1),c2_0 -> c1_1(x0),c1_2(x0,x1),ren16(x0)
% 0.43/0.66
% 0.43/0.66 Most General Atoms: ren1 ndr1_0 ren2 ren3 ren4 c1_0 ren24 c5_1(x0) ndr1_1(x0) ren6 ren7(x0) ren10(x0) ren11 ren12(x0) ren13 c4_0 ren23 ren14(x0) ren15(x0) ren16(x0) ren17 ren18 ren19(x0) ren20(x0) ren21 ren22 c1_1(x0) c5_0 c2_0 c4_1(x4) c4_2(x0,x1) c5_2(x0,x2) c1_2(x0,x3) ren5(x4) c3_0 c3_2(x0,x1) c2_2(x0,x1) ren8(x2) ren9(x2) c3_1(x0) c2_1(x0)
% 0.43/0.66
% 0.43/0.66 === Starting SPASS-SCL-FOL A Little Less Naive, considering 120 atoms initially, heuristics mode: resolution_2 ===
% 0.43/0.66
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 120
% 0.43/0.66 === Restarting.
% 0.43/0.66 === Conflict found: 125:7:2:[112.1,115.4]:TopTop: ndr1_0,ndr1_1(x0),c3_2(x0,x1),c2_0 -> c1_1(x0),c1_2(x0,x1),ren16(x0) {x0 -> a357, x1 -> a357}
% 0.43/0.66 === Backtracking. Learning clause 127:6:1:[1.1,126.0,125.2,2.2]:Top: c3_2(a357,x0),c2_0,ren1 -> c1_1(a357),c1_2(a357,x0),ren16(a357)
% 0.43/0.66 === Backtracking. Learning clause 129:6:1:[1.1,128.1,117.3,2.2]:Top: c3_0,c2_2(a357,x0),c3_2(a357,x0),ren1 -> c3_1(a357),ren18
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.43/0.66 === Restarting.
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.43/0.66 === Restarting.
% 0.43/0.66 === Conflict found: 125:7:2:[112.1,115.4]:TopTop: ndr1_0,ndr1_1(x0),c3_2(x0,x1),c2_0 -> c1_1(x0),c1_2(x0,x1),ren16(x0) {x0 -> a357, x1 -> a358}
% 0.43/0.66 === Backtracking. Learning clause 131:4:0:[5.1,130.0,125.6,4.2,2.2,1.2]:: c2_0,ren1 -> c1_1(a357),ren16(a357)
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.43/0.66 === Restarting.
% 0.43/0.66 === Backtracking. Learning clause 132:5:0:[117.5,5.2,2.2,1.2]:: c3_0,c2_2(a357,a358),ren1 -> c3_1(a357),ren18
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 185
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 185
% 0.43/0.66 === Restarting.
% 0.43/0.66 === Backtracking. Learning clause 134:5:0:[1.1,133.1,114.4,7.2]:: c1_0,c5_0,ren1 -> ren14(a357),ren15(a357)
% 0.43/0.66 === Backtracking. Learning clause 136:5:0:[1.1,135.0,109.3,7.2]:: c1_1(a357),ren1 -> c4_1(a357),c3_0,ren11
% 0.43/0.66 === Backtracking. Learning clause 138:4:0:[1.1,137.1,121.4,7.2]:: c1_0,ren1 -> ren24,c4_1(a357)
% 0.43/0.66 === Backtracking. Learning clause 140:4:0:[1.1,139.0,110.3,7.2]:: ren1 -> ren12(a357),c4_1(a357),c4_0
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 185
% 0.43/0.66 === Restarting.
% 0.43/0.66 === Backtracking. Learning clause 141:2:0:[116.2,68.1,111.3,48.1]:: -> c1_0,ndr1_0
% 0.43/0.66 === Backtracking. Learning clause 142:1:0:[103.2,113.2,14.1,120.2,96.1,141.1]:: -> ndr1_0
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 190
% 0.43/0.66 === Restarting.
% 0.43/0.66 === Backtracking. Learning clause 144:5:0:[8.1,143.0,107.4,9.2]:: ren2 -> c5_0,c2_0,c4_1(a359),ren10(a359)
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 196
% 0.43/0.66 === Restarting.
% 0.43/0.66 === Backtracking. Learning clause 146:5:0:[8.1,145.0,109.3,10.2]:: c1_1(a359),ren2 -> c4_1(a359),c3_0,ren11
% 0.43/0.66 === Backtracking. Learning clause 148:10:2:[8.1,147.2,106.5,10.2]:TopTop: ndr1_1(a359),c3_2(a359,x0),c2_1(x1),ren2 -> ren7(a359),c2_2(a359,x0),c1_2(a359,x0),c5_0,ren8(x1),ren9(x1)
% 0.43/0.66 === Clause set with instances from active satisfied. Growing active. New size: 260
% 0.43/0.66
% 0.43/0.66 Linear Model Building succeeded.
% 0.43/0.66 SZS status Satisfiable
% 0.43/0.66
% 0.43/0.66 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.43/0.66
% 0.43/0.66 SPASS-SCL-FOL Statistics:
% 0.43/0.66 Number of learned clauses: 13
% 0.43/0.66 Number of propagations: 511
% 0.43/0.66 Number of decisions: 1148
% 0.43/0.66 Number of resolutions: 23
% 0.43/0.66 Number of condensations: 0
% 0.43/0.66 Number of sub resolutions: 14
% 0.43/0.66 Number of input literals (deduplicated): 120
% 0.43/0.66 Number of grows: 10
% 0.43/0.66 Number of considered ground atoms: 260
% 0.43/0.66
% 0.43/0.66 Needed: 0:00:00.04
% 0.43/0.66
%------------------------------------------------------------------------------