%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : SYN493-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 : 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.06 % Problem : SYN493-1 : TPTP v9.2.1. Released v2.1.0.
% 0.00/0.07 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.25 % Computer : n012.cluster.edu
% 0.07/0.25 % Model : x86_64 x86_64
% 0.07/0.25 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.25 % Memory : 8042.1875MB
% 0.07/0.25 % OS : Linux 3.10.0-693.el7.x86_64
% 0.07/0.25 % CPULimit : 300
% 0.07/0.25 % WCLimit : 300
% 0.07/0.25 % DateTime : Thu May 7 13:42:16 EDT 2026
% 0.07/0.25 % CPUTime :
% 0.07/0.25 SPASS-SCL-FOL version:
% 0.07/0.29 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.15/0.35 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/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: hskp10 ndr1_0 hskp9 hskp8 hskp7 hskp6 hskp5 hskp4 hskp3 hskp2 hskp1 hskp0 c3_1 c1_1 c0_1 c2_1
% 0.15/0.35 Fol Constants: a47 a46 a45 a44 a42 a40 a38 a48 a43 a41 a39
% 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: hskp10 ndr1_0 hskp9 hskp8 hskp7 hskp6 hskp5 hskp4 hskp3 hskp2 hskp1 hskp0 c0_1(x1) c3_1(x2) c1_1(x2) c2_1(x2)
% 0.15/0.35
% 0.15/0.35 === Starting SPASS-SCL-FOL A Little Less Naive, considering 56 atoms initially, heuristics mode: normal ===
% 0.15/0.35
% 0.15/0.35 === Backtracking. Learning clause 53:10:1:[47.1,48.6,43.2,48.5,9.2,40.1,12.2,22.1]:Top: c0_1(x0),c1_1(x0),c3_1(x0) -> hskp4,c0_1(a43),c2_1(a39),c1_1(a39),hskp8,hskp6,c0_1(a44)
% 0.15/0.35 === Backtracking. Learning clause 54:10:2:[48.6,47.1,4.2,12.3]:TopTop: c0_1(x0),c1_1(x0),c3_1(x0) -> hskp8,c1_1(x1),c0_1(x1),hskp4,hskp0,hskp6,hskp2
% 0.15/0.35 === Backtracking. Learning clause 55:9:2:[48.6,47.1,9.2,54.10,43.2]:TopTop: c0_1(x0),c1_1(x0),c3_1(x0),c0_1(a39) -> hskp8,c1_1(x1),c0_1(x1),hskp4,hskp6
% 0.15/0.35 === Conflict found: 54:10:2:[48.6,47.1,4.2,12.3]:TopTop: c0_1(x0),c1_1(x0),c3_1(x0) -> hskp8,c1_1(x1),c0_1(x1),hskp4,hskp0,hskp6,hskp2 {x0 -> a44, x1 -> a43}
% 0.15/0.35 === Backtracking. Learning clause 56:10:2:[54.8,11.1,9.1,48.1,55.4]:TopTop: c0_1(x0),c1_1(x0),c3_1(x0) -> c2_1(a39),c1_1(a39),hskp8,c1_1(x1),c0_1(x1),hskp4,hskp6
% 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/sandbox2/benchmark/theBenchmark.p
% 0.15/0.35
% 0.15/0.35 SPASS-SCL-FOL Statistics:
% 0.15/0.35 Number of learned clauses: 4
% 0.15/0.35 Number of propagations: 39
% 0.15/0.35 Number of decisions: 43
% 0.15/0.35 Number of resolutions: 18
% 0.15/0.35 Number of condensations: 3
% 0.15/0.35 Number of sub resolutions: 0
% 0.15/0.35 Number of input literals (deduplicated): 49
% 0.15/0.35 Number of grows: 0
% 0.15/0.35 Number of considered ground atoms: 56
% 0.15/0.35
% 0.15/0.35 Needed: 0:00:00.00
% 0.15/0.35
%------------------------------------------------------------------------------