%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN431-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 : n022.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:47 PM UTC 2026
% Result : Satisfiable 0.39s 0.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SYN431-1 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n022.cluster.edu
% 0.16/0.34 % Model : x86_64 x86_64
% 0.16/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.34 % Memory : 8042.1875MB
% 0.16/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.34 % CPULimit : 300
% 0.16/0.34 % WCLimit : 300
% 0.16/0.34 % DateTime : Thu May 7 13:41:52 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.22/0.44 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.62 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.62 Execution resolution_3 ended with status: satisfiable
% 0.39/0.62 Used heuristic: resolution_3
% 0.39/0.62
% 0.39/0.62 Input Clauses:
% 0.39/0.62
% 0.39/0.62 Predicates: hskp28 ndr1_0 hskp27 hskp26 hskp25 hskp24 hskp23 hskp22 hskp21 hskp20 hskp19 hskp18 hskp17 hskp16 hskp15 hskp14 hskp13 hskp12 hskp11 hskp10 hskp9 hskp8 hskp7 hskp6 hskp5 hskp4 hskp3 hskp2 hskp1 hskp0 c1_1 c2_1 c3_1 c0_1
% 0.39/0.62 Fol Constants: a158 a157 a153 a152 a150 a149 a148 a147 a144 a143 a138 a134 a161 a159 a156 a151 a146 a142 a141 a140 a139 a137 a136 a135 a133 a160 a154 a145 a132
% 0.39/0.62 Fol Functions:
% 0.39/0.62 Problem Properties:
% 0.39/0.62 This is a Bernays Schoenfinkel problem.
% 0.39/0.62
% 0.39/0.62 After reduction: Problem Properties:
% 0.39/0.62 This is a Bernays Schoenfinkel problem.
% 0.39/0.62
% 0.39/0.62
% 0.39/0.62 Reduced Input Clauses:
% 0.39/0.62
% 0.39/0.62 Most General Atoms: hskp28 ndr1_0 hskp27 hskp26 hskp25 hskp24 hskp23 hskp22 hskp21 hskp20 hskp19 hskp18 hskp17 hskp16 hskp15 hskp14 hskp13 hskp12 hskp11 hskp10 hskp9 hskp8 hskp7 hskp6 hskp5 hskp4 hskp3 hskp2 hskp1 hskp0 c3_1(x1) c1_1(x2) c0_1(x2) c2_1(x2)
% 0.39/0.62
% 0.39/0.62 === Starting SPASS-SCL-FOL A Little Less Naive, considering 60 atoms initially, heuristics mode: resolution_3 ===
% 0.39/0.62
% 0.39/0.62 === Backtracking. Learning clause 134:4:0:[21.1,133.0,121.4,107.1,65.2]:: hskp8 -> c2_1(a142),hskp0,hskp1
% 0.39/0.62 === Backtracking. Learning clause 137:4:0:[27.1,135.1,114.0,136.3,121.4,115.1]:: c3_1(a135),hskp2 -> hskp0,hskp1
% 0.39/0.62 === Clause set with instances from active satisfied. Growing active. New size: 130
% 0.39/0.62 === Restarting.
% 0.39/0.62 === Backtracking. Learning clause 141:4:1:[7.1,138.2,46.1,139.3,45.1,140.4,130.7,85.1]:Top: c3_1(x0),c2_1(x0),hskp22 -> c1_1(x0)
% 0.39/0.62 === Conflict found: 141:4:1:[7.1,138.2,46.1,139.3,45.1,140.4,130.7,85.1]:Top: c3_1(x0),c2_1(x0),hskp22 -> c1_1(x0) {x0 -> a147}
% 0.39/0.62 === Backtracking. Learning clause 142:3:0:[141.1,48.2,47.2]:: hskp22,hskp21 -> c1_1(a147)
% 0.39/0.62 === Conflict found: 141:4:1:[7.1,138.2,46.1,139.3,45.1,140.4,130.7,85.1]:Top: c3_1(x0),c2_1(x0),hskp22 -> c1_1(x0) {x0 -> a144}
% 0.39/0.62 === Backtracking. Learning clause 143:3:0:[141.1,50.2,49.2]:: hskp22,hskp20 -> c1_1(a144)
% 0.39/0.62
% 0.39/0.62 Linear Model Building succeeded.
% 0.39/0.62 SZS status Satisfiable
% 0.39/0.62
% 0.39/0.62 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.39/0.62
% 0.39/0.62 SPASS-SCL-FOL Statistics:
% 0.39/0.62 Number of learned clauses: 5
% 0.39/0.62 Number of propagations: 214
% 0.39/0.62 Number of decisions: 234
% 0.39/0.62 Number of resolutions: 8
% 0.39/0.62 Number of condensations: 0
% 0.39/0.62 Number of sub resolutions: 6
% 0.39/0.62 Number of input literals (deduplicated): 121
% 0.39/0.62 Number of grows: 1
% 0.39/0.62 Number of considered ground atoms: 130
% 0.39/0.62
% 0.39/0.62 Needed: 0:00:00.02
% 0.39/0.62
%------------------------------------------------------------------------------