%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GRP125-2.005 : TPTP v9.2.1. Released v1.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n003.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:23:03 PM UTC 2026
% Result : Unsatisfiable 0.67s 0.61s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP125-2.005 : TPTP v9.2.1. Released v1.2.0.
% 0.12/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n003.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 12:01:12 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.20/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.67/0.61 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.67/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.67/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.67/0.61 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.67/0.61 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.67/0.61 Execution normal ended with status: unsatisfiable
% 0.67/0.61 Used heuristic: normal
% 0.67/0.61
% 0.67/0.61 Input Clauses:
% 0.67/0.61
% 0.67/0.61 Predicates: next greater product group_element equalish
% 0.67/0.61 Fol Constants: e_1 e_2 e_3 e_4 e_5
% 0.67/0.61 Fol Functions:
% 0.67/0.61 Problem Properties:
% 0.67/0.61 This is a Bernays Schoenfinkel problem.
% 0.67/0.61
% 0.67/0.61 After reduction: Problem Properties:
% 0.67/0.61 This is a Bernays Schoenfinkel problem.
% 0.67/0.61
% 0.67/0.61
% 0.67/0.61 Reduced Input Clauses:
% 0.67/0.61
% 0.67/0.61 Most General Atoms: next(x0,x2) greater(x1,x2) group_element(x1) equalish(x0,x3) product(x2,x3,x0)
% 0.67/0.61
% 0.67/0.61 === Starting SPASS-SCL-FOL A Little Less Naive, considering 205 atoms initially, heuristics mode: normal ===
% 0.67/0.61
% 0.67/0.61 === Backtracking. Learning clause 47:9:4:[41.4,46.1,43.1]:TopTopTopTop: group_element(x0),group_element(x1),product(x1,x0,x2),product(x0,x3,e_5) -> product(x0,x1,e_1),product(x0,x1,e_3),product(x0,x1,e_4),product(e_2,x2,x0),equalish(x1,x3)
% 0.67/0.61 === Backtracking. Learning clause 49:11:2:[16.0,48.1,41.6,46.2,46.1,46.2,41.4,15.1]:TopTop: group_element(x0),next(x0,x1),greater(e_4,x1) -> product(e_1,x0,e_1),product(e_1,x0,e_3),product(e_2,e_4,x0),product(e_2,e_2,e_1),product(e_2,e_5,x0),product(x0,e_1,e_1),product(x0,e_1,e_3),product(x0,e_1,e_5)
% 0.67/0.61 === Backtracking. Learning clause 50:11:2:[41.7,46.2,46.2,46.2,41.4]:TopTop: group_element(x1),group_element(x0) -> product(x0,x1,e_1),product(x0,x1,e_3),product(e_2,e_5,x1),product(e_2,e_2,x1),product(e_2,e_4,x1),product(x1,x0,e_1),product(x1,x0,e_3),product(x1,x0,e_4),product(x1,x0,e_5)
% 0.67/0.61 === Backtracking. Learning clause 59:27:11:[19.0,51.1,18.0,52.2,17.0,53.6,16.0,54.7,14.0,55.11,45.0,56.14,24.0,57.25,40.0,58.33,46.3,43.1,41.3,43.1,46.3,41.6,47.4,41.7,46.1,46.1,50.10,44.1,43.1,43.2,46.1,44.2,41.5,46.1,42.2,44.2,42.1,15.1,43.2,42.1,42.1,42.1,28.1,15.1,27.1,15.1,3.1,42.2,45.1,46.1,30.1]:TopTopTopTopTopTopTopTopTopTopTop: product(e_2,e_4,x0),product(x1,e_1,e_1),product(e_1,x2,e_1),product(x3,e_3,e_3),product(e_2,e_4,e_5),product(e_3,e_3,x4),product(e_2,e_4,x5),product(e_1,x6,e_1),product(e_4,e_4,x7),next(e_2,x8),greater(e_5,x8),next(e_2,x9),greater(e_4,x9),product(e_2,e_4,x10) -> equalish(x0,e_2),product(e_1,e_2,e_2),product(e_3,e_1,e_3),equalish(e_3,x1),equalish(e_3,x2),equalish(x3,e_1),product(e_2,e_1,e_1),product(e_2,e_1,e_2),equalish(x4,e_1),equalish(e_3,x5),equalish(x6,e_2),equalish(e_1,x7),product(e_4,x10,e_4)
% 0.67/0.61 === Backtracking. Learning clause 64:12:4:[17.0,60.0,18.0,61.4,16.0,62.5,14.0,63.6,41.6,15.1,43.1,46.3,41.4,15.1,15.1,44.1,3.1]:TopTopTopTop: next(e_2,x0),greater(e_4,x0),product(e_1,e_3,x1),next(e_2,x2),greater(e_5,x2),product(x3,e_1,e_1) -> product(e_2,e_1,e_1),product(e_2,e_1,e_2),equalish(e_1,x1),product(e_3,e_1,e_3),product(e_3,e_1,e_4),equalish(e_3,x3)
% 0.67/0.61 === Backtracking. Learning clause 65:14:6:[46.3,42.1,64.11]:TopTopTopTopTopTop: product(e_1,e_3,x0),product(x0,e_4,x1),next(e_2,x2),greater(e_4,x2),product(e_1,e_3,x3),next(e_2,x4),greater(e_5,x4),product(x5,e_1,e_1) -> equalish(e_1,x1),product(e_2,e_1,e_1),product(e_2,e_1,e_2),equalish(e_1,x3),product(e_3,e_1,e_3),equalish(e_3,x5)
% 0.67/0.61 === Backtracking. Learning clause 70:15:5:[16.0,66.0,18.0,67.1,24.0,68.12,21.0,69.15,41.3,43.1,44.2,64.3,64.3]:TopTopTopTopTop: product(e_1,x0,e_1),product(x1,e_3,e_3),next(e_2,x2),greater(e_4,x2),next(e_2,x3),greater(e_5,x3),product(x4,e_1,e_1) -> product(e_1,e_3,e_4),equalish(e_3,x0),equalish(x1,e_1),product(e_2,e_1,e_1),product(e_2,e_1,e_2),product(e_3,e_1,e_3),product(e_3,e_1,e_4),equalish(e_3,x4)
% 0.67/0.61 === Backtracking. Learning clause 78:22:6:[20.0,71.1,17.0,72.5,16.0,73.10,18.0,74.11,39.0,75.16,24.0,76.17,38.0,77.19,41.6,44.2,47.3,43.1,44.1,44.1,43.2,41.6,43.2,30.1,46.1,46.3,43.2,42.2,45.1,28.1,41.5,15.1,15.1,41.7]:TopTopTopTopTopTop: product(x0,e_1,e_4),product(e_3,e_1,x1),product(e_1,x2,e_1),product(e_3,e_3,x3),next(e_2,x4),greater(e_4,x4),next(e_2,x5),greater(e_5,x5) -> product(e_5,e_1,e_1),equalish(x0,e_5),product(e_1,e_5,e_1),product(e_2,e_2,e_1),equalish(e_1,x1),product(e_1,e_2,e_2),equalish(x2,e_2),equalish(x3,e_1),product(e_2,e_1,e_1),product(e_2,e_1,e_2),product(e_1,e_3,e_1),product(e_1,e_3,e_2),product(e_1,e_3,e_3),product(e_1,e_3,e_4)
% 0.67/0.61 === Backtracking. Learning clause 79:13:4:[41.4,47.3,19.1,36.1,43.2,42.1,44.2]:TopTopTopTop: group_element(x0),product(x0,e_5,e_5),product(e_4,x1,e_1),product(e_2,e_2,x2),product(x3,x0,e_5) -> product(e_4,x0,e_3),product(e_4,x0,e_4),product(x0,e_4,e_1),product(x0,e_4,e_3),product(x0,e_4,e_4),equalish(x1,x0),equalish(x0,x2),equalish(x3,e_4)
% 0.67/0.61 === Backtracking. Learning clause 80:25:11:[41.4,43.1,46.2,46.1,46.3,44.1,41.4,44.2,43.2,19.1,79.9,46.3,42.1,44.1]:TopTopTopTopTopTopTopTopTopTopTop: group_element(x0),group_element(x1),product(x0,x2,e_2),product(x1,x0,e_2),product(x3,x1,e_5),group_element(x4),product(x4,e_5,e_5),product(e_2,e_2,x5),product(x6,x4,e_5),product(e_1,x7,e_4),product(x7,e_1,x8),product(x1,x4,x9),product(x10,e_4,e_1) -> product(x0,x1,e_1),product(x0,x1,e_4),equalish(x1,x2),equalish(x0,x3),product(e_4,x4,e_3),product(e_4,x4,e_4),product(x4,e_4,e_4),equalish(x8,x4),equalish(x4,x5),equalish(x6,e_4),equalish(e_2,x9),equalish(x4,x10)
% 0.67/0.61 === Conflict found: 47:9:4:[41.4,46.1,43.1]:TopTopTopTop: group_element(x0),group_element(x1),product(x1,x0,x2),product(x0,x3,e_5) -> product(x0,x1,e_1),product(x0,x1,e_3),product(x0,x1,e_4),product(e_2,x2,x0),equalish(x1,x3) {x0 -> e_5, x1 -> e_4, x2 -> e_1, x3 -> e_5}
% 0.67/0.61 === Backtracking. Learning clause 81:12:3:[47.6,46.1,41.3]:TopTopTop: product(x0,x2,e_5),group_element(x1),group_element(x0) -> product(x0,x1,e_1),product(x0,x1,e_4),product(e_2,e_1,x0),equalish(x1,x2),product(e_3,e_1,x0),product(x1,x0,e_2),product(x1,x0,e_3),product(x1,x0,e_4),product(x1,x0,e_5)
% 0.67/0.61 === Conflict found: 47:9:4:[41.4,46.1,43.1]:TopTopTopTop: group_element(x0),group_element(x1),product(x1,x0,x2),product(x0,x3,e_5) -> product(x0,x1,e_1),product(x0,x1,e_3),product(x0,x1,e_4),product(e_2,x2,x0),equalish(x1,x3) {x0 -> e_5, x1 -> e_4, x2 -> e_1, x3 -> e_5}
% 0.67/0.61 === Backtracking. Learning clause 83:11:2:[19.0,82.2,47.9,36.1,44.1,46.1,41.3]:TopTop: product(x0,e_5,e_5),product(x1,e_4,e_1),group_element(x0) -> product(x0,e_4,e_4),product(e_2,e_1,x0),equalish(x0,x1),product(e_3,e_1,x0),product(e_4,x0,e_2),product(e_4,x0,e_3),product(e_4,x0,e_4),product(e_4,x0,e_5)
% 0.67/0.61 === Conflict found: 47:9:4:[41.4,46.1,43.1]:TopTopTopTop: group_element(x0),group_element(x1),product(x1,x0,x2),product(x0,x3,e_5) -> product(x0,x1,e_1),product(x0,x1,e_3),product(x0,x1,e_4),product(e_2,x2,x0),equalish(x1,x3) {x0 -> e_5, x1 -> e_4, x2 -> e_2, x3 -> e_5}
% 0.67/0.61 === Backtracking. Learning clause 85:9:4:[19.0,84.1,47.8,42.1,36.1,44.1]:TopTopTopTop: group_element(x0),product(e_4,x0,x1),product(x0,e_5,e_5),product(e_2,x1,x2),product(x3,e_4,e_1) -> product(x0,e_4,e_3),product(x0,e_4,e_4),equalish(x0,x2),equalish(x0,x3)
% 0.67/0.61
% 0.67/0.61 SZS status Unsatisfiable
% 0.67/0.61
% 0.67/0.61 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.67/0.61
% 0.67/0.61 SPASS-SCL-FOL Statistics:
% 0.67/0.61 Number of learned clauses: 13
% 0.67/0.61 Number of propagations: 682
% 0.67/0.61 Number of decisions: 19
% 0.67/0.61 Number of resolutions: 166
% 0.67/0.61 Number of condensations: 3
% 0.67/0.61 Number of sub resolutions: 26
% 0.67/0.61 Number of input literals (deduplicated): 51
% 0.67/0.61 Number of grows: 0
% 0.67/0.61 Number of considered ground atoms: 205
% 0.67/0.61
% 0.67/0.61 Needed: 0:00:00.09
% 0.67/0.61
%------------------------------------------------------------------------------