%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN536+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 : n028.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:59 PM UTC 2026
% Result : CounterSatisfiable 0.37s 0.60s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.15 % Problem : SYN536+1 : TPTP v9.2.1. Released v2.1.0.
% 0.13/0.16 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.21/0.38 % Computer : n028.cluster.edu
% 0.21/0.38 % Model : x86_64 x86_64
% 0.21/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.38 % Memory : 8042.1875MB
% 0.21/0.38 % OS : Linux 3.10.0-693.el7.x86_64
% 0.21/0.38 % CPULimit : 300
% 0.21/0.38 % WCLimit : 300
% 0.21/0.38 % DateTime : Thu May 7 13:45:16 EDT 2026
% 0.21/0.38 % CPUTime :
% 0.21/0.38 SPASS-SCL-FOL version:
% 0.29/0.48 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.37/0.60 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.60 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.60 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.60 Execution resolution_2 ended with status: satisfiable
% 0.37/0.60 Used heuristic: resolution_2
% 0.37/0.60
% 0.37/0.60 Input Clauses:
% 0.37/0.60
% 0.37/0.60 Predicates: ndr1_0 c5_1 ndr1_1 c3_2 c2_2 c4_0 c2_0 c1_2 c5_2 c1_1 c5_0 c3_0 c2_1 c3_1 c4_1 c4_2 c1_0 ren1 ren2 ren3 ren4 ren5 ren6 ren7 ren8 ren9 ren10 ren11 ren12 ren13 ren14 ren15 ren16 ren17 ren18 ren19 ren20
% 0.37/0.60 Fol Constants: a520 a521 a522 a523 a524 a525 a526 a527 a528 a529 a530 a531 a532 a533 a534 a535 a536 a537 a538 a539 a540 a541 a542 a543 a544 a545
% 0.37/0.60 Fol Functions:
% 0.37/0.60 Problem Properties:
% 0.37/0.60 This is a Bernays Schoenfinkel problem.
% 0.37/0.60
% 0.37/0.60 After reduction: Problem Properties:
% 0.37/0.60 This is a Bernays Schoenfinkel problem.
% 0.37/0.60
% 0.37/0.60
% 0.37/0.60 Reduced Input Clauses:
% 0.37/0.60 108:2:0:[101.0,90.2]:: -> ren1,c5_0
% 0.37/0.60
% 0.37/0.60 Most General Atoms: ren1 ndr1_0 ren2 ren3(x0) ren4(x0) ren6 ren7 ren8 c1_0 ren19(x0) ren20 ren9(x0) ren10 ren11(x0) ren13 ren14 ren15(x0) ren16 ren17 ren18(x0) c4_0 c2_0 c5_0 c3_1(x0) ndr1_1(x1) c3_0 c2_2(x0,x3) ren5(x1) c4_2(x0,x3) c5_1(x1) c3_2(x0,x2) c1_1(x2) ren12(x2) c4_1(x2) c1_2(x0,x1) c5_2(x0,x1) c2_1(x0)
% 0.37/0.60
% 0.37/0.60 === Starting SPASS-SCL-FOL A Little Less Naive, considering 121 atoms initially, heuristics mode: resolution_2 ===
% 0.37/0.60
% 0.37/0.60 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.37/0.60 === Restarting.
% 0.37/0.60 === Conflict found: 108:2:0:[101.0,90.2]:: -> ren1,c5_0 {}
% 0.37/0.60 === Backtracking. Learning clause 109:2:0:[108.1,1.1]:: -> c5_0,ndr1_0
% 0.37/0.60 === Backtracking. Learning clause 110:1:0:[94.2,19.1,96.2,109.1]:: -> ndr1_0
% 0.37/0.60
% 0.37/0.60 Linear Model Building succeeded.
% 0.37/0.60 SZS status Satisfiable
% 0.37/0.60
% 0.37/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.37/0.60
% 0.37/0.60 SPASS-SCL-FOL Statistics:
% 0.37/0.60 Number of learned clauses: 2
% 0.37/0.60 Number of propagations: 63
% 0.37/0.60 Number of decisions: 190
% 0.37/0.60 Number of resolutions: 4
% 0.37/0.60 Number of condensations: 0
% 0.37/0.60 Number of sub resolutions: 1
% 0.37/0.60 Number of input literals (deduplicated): 121
% 0.37/0.60 Number of grows: 1
% 0.37/0.60 Number of considered ground atoms: 121
% 0.37/0.60
% 0.37/0.60 Needed: 0:00:00.01
% 0.37/0.60
%------------------------------------------------------------------------------