%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN495-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 : n012.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:53 PM UTC 2026
% Result : Satisfiable 0.15s 0.35s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.07 % Problem : SYN495-1 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.07 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.07/0.26 % Computer : n012.cluster.edu
% 0.07/0.26 % Model : x86_64 x86_64
% 0.07/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.26 % Memory : 8042.1875MB
% 0.07/0.26 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.26 % CPULimit : 300
% 0.07/0.26 % WCLimit : 300
% 0.07/0.26 % DateTime : Thu May 7 13:42:16 EDT 2026
% 0.07/0.26 % CPUTime :
% 0.07/0.26 SPASS-SCL-FOL version:
% 0.07/0.30 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.35 Execution normal ended with status: satisfiable
% 0.15/0.35 Used heuristic: normal
% 0.15/0.35
% 0.15/0.35 Input Clauses:
% 0.15/0.35
% 0.15/0.35 Predicates: hskp16 ndr1_0 hskp15 hskp14 hskp13 hskp12 hskp11 hskp10 hskp9 hskp8 hskp7 hskp6 hskp5 hskp4 hskp3 hskp2 hskp1 hskp0 c2_1 c3_1 c1_1 c0_1
% 0.15/0.35 Fol Constants: a74 a72 a70 a68 a67 a65 a64 a63 a62 a77 a76 a75 a73 a71 a69 a66 a61
% 0.15/0.35 Fol Functions:
% 0.15/0.35 Problem Properties:
% 0.15/0.35 This is a Bernays Schoenfinkel problem.
% 0.15/0.35
% 0.15/0.35 After reduction: Problem Properties:
% 0.15/0.35 This is a Bernays Schoenfinkel problem.
% 0.15/0.35
% 0.15/0.35
% 0.15/0.35 Reduced Input Clauses:
% 0.15/0.35
% 0.15/0.35 Most General Atoms: hskp16 ndr1_0 hskp15 hskp14 hskp13 hskp12 hskp11 hskp10 hskp9 hskp8 hskp7 hskp6 hskp5 hskp4 hskp3 hskp2 hskp1 hskp0 c2_1(x0) c3_1(x1) c1_1(x1) c0_1(x1)
% 0.15/0.35
% 0.15/0.35 === Starting SPASS-SCL-FOL A Little Less Naive, considering 86 atoms initially, heuristics mode: normal ===
% 0.15/0.35
% 0.15/0.35 === Backtracking. Learning clause 77:8:1:[75.1,73.4,11.2,20.3,65.2]:Top: c3_1(x0),c1_1(a75) -> hskp3,hskp15,c0_1(x0),hskp7,hskp12,hskp16
% 0.15/0.35 === Backtracking. Learning clause 78:6:1:[20.3,11.1,12.1,73.2]:Top: c3_1(x0) -> hskp16,c0_1(x0),c1_1(x0),hskp7,hskp12
% 0.15/0.35 === Backtracking. Learning clause 79:7:1:[20.2,12.1,11.1,75.3,78.4]:Top: c3_1(x0) -> hskp3,hskp15,hskp16,c0_1(x0),hskp7,hskp12
% 0.15/0.35 === Conflict found: 79:7:1:[20.2,12.1,11.1,75.3,78.4]:Top: c3_1(x0) -> hskp3,hskp15,hskp16,c0_1(x0),hskp7,hskp12 {x0 -> a69}
% 0.15/0.35 === Backtracking. Learning clause 80:7:0:[79.5,68.1,45.2,19.2,26.1]:: -> hskp3,hskp15,hskp16,hskp7,hskp12,hskp13,c3_1(a70)
% 0.15/0.35 === Conflict found: 79:7:1:[20.2,12.1,11.1,75.3,78.4]:Top: c3_1(x0) -> hskp3,hskp15,hskp16,c0_1(x0),hskp7,hskp12 {x0 -> a69}
% 0.15/0.35 === Backtracking. Learning clause 81:6:0:[79.1,45.2,68.1,19.2,51.2,79.5,80.7,28.1]:: -> hskp3,hskp15,hskp16,hskp7,hskp12,c2_1(a68)
% 0.15/0.35
% 0.15/0.35 Linear Model Building succeeded.
% 0.15/0.35 SZS status Satisfiable
% 0.15/0.35
% 0.15/0.35 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.15/0.35
% 0.15/0.35 SPASS-SCL-FOL Statistics:
% 0.15/0.35 Number of learned clauses: 5
% 0.15/0.35 Number of propagations: 70
% 0.15/0.35 Number of decisions: 70
% 0.15/0.35 Number of resolutions: 22
% 0.15/0.35 Number of condensations: 0
% 0.15/0.35 Number of sub resolutions: 0
% 0.15/0.35 Number of input literals (deduplicated): 73
% 0.15/0.35 Number of grows: 0
% 0.15/0.35 Number of considered ground atoms: 86
% 0.15/0.35
% 0.15/0.35 Needed: 0:00:00.00
% 0.15/0.35
%------------------------------------------------------------------------------