%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : HWV003-3 : TPTP v9.2.1. Released v2.7.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n023.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:24:05 PM UTC 2026
% Result : Unsatisfiable 0.30s 0.51s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : HWV003-3 : TPTP v9.2.1. Released v2.7.0.
% 0.11/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n023.cluster.edu
% 0.17/0.34 % Model : x86_64 x86_64
% 0.17/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.34 % Memory : 8042.1875MB
% 0.17/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.17/0.34 % CPULimit : 300
% 0.17/0.34 % WCLimit : 300
% 0.17/0.34 % DateTime : Thu May 7 12:06:39 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.30/0.51 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.51 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.51 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.51 Execution normal ended with status: unsatisfiable
% 0.30/0.51 Used heuristic: normal
% 0.30/0.51
% 0.30/0.51 Input Clauses:
% 0.30/0.51
% 0.30/0.51 Predicates: a11 a b a12 a13 a14 a15 cI a16 a17 s1 c1 a21 a22 a23 a24 a25 a26 s2 c2 conjline18 conjline19
% 0.30/0.51 Fol Constants: a
% 0.30/0.51 Fol Functions:
% 0.30/0.51 Problem Properties:
% 0.30/0.51 This is a propositional problem.
% 0.30/0.51
% 0.30/0.51 After reduction: Problem Properties:
% 0.30/0.51 This is a propositional problem.
% 0.30/0.51
% 0.30/0.51
% 0.30/0.51 Reduced Input Clauses:
% 0.30/0.51
% 0.30/0.51 Most General Atoms: a11 a b a12 a13 a14 a15 cI a16 a17 s1 c1 a21 a22 a23 a24 a25 a26 s2 c2 conjline18 conjline19
% 0.30/0.51
% 0.30/0.51 === Starting SPASS-SCL-FOL A Little Less Naive, considering 22 atoms initially, heuristics mode: normal ===
% 0.30/0.51
% 0.30/0.51 === Backtracking. Learning clause 62:6:0:[45.1,38.1,51.1,60.3,61.2,55.1,48.1,24.1,20.1,34.1]:: a25,c1,a16,a23 -> a21,a22
% 0.30/0.51 === Backtracking. Learning clause 63:1:0:[56.1,61.1,23.1,47.2,60.1,21.1,32.2,50.2,62.6,31.1,42.3,13.1,1.2,16.1,36.2,26.1,12.1,2.2,5.1,8.1]:: -> a11
% 0.30/0.51 === Backtracking. Learning clause 65:2:0:[63.0,64.0,52.3,44.1,59.3,27.1,61.2,56.1,23.1,21.1,13.1,12.1,7.1,47.2,30.1,40.1,36.1,4.1,35.1,34.2]:: cI -> a22
% 0.30/0.51 === Backtracking. Learning clause 66:3:0:[12.2,4.1,7.1,29.1]:: a14 -> a21,b
% 0.30/0.51 === Backtracking. Learning clause 69:3:0:[63.0,67.0,20.0,68.1,3.2,28.3,66.3,16.2,24.2,46.1,56.3]:: conjline18,s1 -> cI
% 0.30/0.51 === Backtracking. Learning clause 71:3:0:[63.0,70.2,18.1,22.2,10.1,6.1]:: a15,a -> s1
% 0.30/0.51 === Backtracking. Learning clause 74:2:0:[63.0,72.0,14.0,73.1,9.1,11.2,30.3,48.3,55.3,18.2,22.2,71.2,69.2,61.1]:: -> cI,conjline19
% 0.30/0.51 === Backtracking. Learning clause 75:3:0:[24.3,20.1]:: s1,a16 -> cI
% 0.30/0.51 === Backtracking. Learning clause 76:3:0:[18.3,14.1]:: a16,a14 -> cI
% 0.30/0.51 === Backtracking. Learning clause 79:2:0:[63.0,77.0,32.0,78.2,44.1,52.3,41.1,59.3,27.1,74.2,14.1,3.3]:: a -> cI
% 0.30/0.51 === Backtracking. Learning clause 81:1:0:[63.0,80.0,52.3,44.1,59.3,27.1,40.1,74.2,14.1,79.1,65.1]:: -> a22
% 0.30/0.51 === Backtracking. Learning clause 82:1:0:[50.1,81.1]:: -> c2
% 0.30/0.51 === Backtracking. Learning clause 84:2:0:[82.0,83.1,27.3,63.1,57.3]:: a15 -> conjline19
% 0.30/0.51 === Backtracking. Learning clause 85:2:0:[6.3,63.1,10.2,15.2,79.2]:: a15,a ->
% 0.30/0.51 === Backtracking. Learning clause 87:1:0:[82.0,86.0,55.1,61.1,24.1,19.1,49.1,66.2,3.3,63.1,17.1,79.2,13.2,60.1,25.1,85.1]:: a ->
% 0.30/0.51 === Conflict found: 66:3:0:[12.2,4.1,7.1,29.1]:: a14 -> a21,b {}
% 0.30/0.51 === Backtracking. Learning clause 89:2:0:[87.0,88.1,66.2,30.1]:: a14 -> b
% 0.30/0.51 === Backtracking. Learning clause 90:2:0:[32.1,81.1,15.3]:: a15,a14 ->
% 0.30/0.51 === Backtracking. Learning clause 92:1:0:[87.0,91.0,33.2,37.1,81.1]:: -> b
% 0.30/0.51 === Backtracking. Learning clause 95:2:0:[14.1,93.0,84.0,94.3,55.1,61.1,24.1,19.1,49.1,17.1]:: a21 -> conjline19
% 0.30/0.51 === Backtracking. Learning clause 98:1:0:[89.1,96.0,87.0,97.2,60.3,82.1,95.2,28.2,25.1,90.1]:: a14 ->
% 0.30/0.51
% 0.30/0.51 SZS status Unsatisfiable
% 0.30/0.51
% 0.30/0.51 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.30/0.51
% 0.30/0.51 SPASS-SCL-FOL Statistics:
% 0.30/0.51 Number of learned clauses: 20
% 0.30/0.51 Number of propagations: 268
% 0.30/0.51 Number of decisions: 31
% 0.30/0.51 Number of resolutions: 122
% 0.30/0.51 Number of condensations: 0
% 0.30/0.51 Number of sub resolutions: 17
% 0.30/0.51 Number of input literals (deduplicated): 22
% 0.30/0.51 Number of grows: 0
% 0.30/0.51 Number of considered ground atoms: 22
% 0.30/0.51
% 0.30/0.51 Needed: 0:00:00.00
% 0.30/0.51
%------------------------------------------------------------------------------