%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GRP129-2.005 : TPTP v9.2.1. Released v1.2.0.
% Transfm : none
% Format : tptp
% Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n010.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:06 PM UTC 2026
% Result : Satisfiable 0.42s 0.83s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.15 % Problem : GRP129-2.005 : TPTP v9.2.1. Released v1.2.0.
% 0.09/0.16 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.21/0.39 % Computer : n010.cluster.edu
% 0.21/0.39 % Model : x86_64 x86_64
% 0.21/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.21/0.39 % Memory : 8042.1875MB
% 0.21/0.39 % OS : Linux 3.10.0-693.el7.x86_64
% 0.21/0.39 % CPULimit : 300
% 0.21/0.39 % WCLimit : 300
% 0.21/0.39 % DateTime : Thu May 7 12:00:52 EDT 2026
% 0.21/0.39 % CPUTime :
% 0.21/0.39 SPASS-SCL-FOL version:
% 0.30/0.49 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 0.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/0.83 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/0.83 Execution resolution_1 ended with status: satisfiable
% 0.42/0.83 Used heuristic: resolution_1
% 0.42/0.83
% 0.42/0.83 Input Clauses:
% 0.42/0.83
% 0.42/0.83 Predicates: next greater product group_element equalish
% 0.42/0.83 Fol Constants: e_1 e_2 e_3 e_4 e_5
% 0.42/0.83 Fol Functions:
% 0.42/0.83 Problem Properties:
% 0.42/0.83 This is a Bernays Schoenfinkel problem.
% 0.42/0.83
% 0.42/0.83 After reduction: Problem Properties:
% 0.42/0.83 This is a Bernays Schoenfinkel problem.
% 0.42/0.83
% 0.42/0.83
% 0.42/0.83 Reduced Input Clauses:
% 0.42/0.83
% 0.42/0.83 Most General Atoms: next(x0,x2) greater(x1,x2) group_element(x1) equalish(x0,x3) product(x2,x0,x3)
% 0.42/0.83
% 0.42/0.83 === Starting SPASS-SCL-FOL A Little Less Naive, considering 12 atoms initially, heuristics mode: resolution_1 ===
% 0.42/0.83
% 0.42/0.83 === Backtracking. Learning clause 47:6:3:[16.0,46.1,41.7,15.1,44.1,44.1,44.1,15.1]:TopTopTop: group_element(x0),next(x0,x1),greater(e_5,x1),next(x0,x2),greater(e_1,x2) -> equalish(x0,x0)
% 0.42/0.83 === Backtracking. Learning clause 49:7:2:[16.0,48.1,41.7,15.1]:TopTop: group_element(x0),next(x0,x1),greater(e_5,x1) -> product(x0,e_1,e_1),product(x0,e_1,e_2),product(x0,e_1,e_3),product(x0,e_1,e_4)
% 0.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 15
% 0.42/0.83 === Restarting.
% 0.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 57
% 0.42/0.83 === Backtracking. Learning clause 50:1:0:[15.2,1.1,11.1]:: product(e_1,e_1,e_5) ->
% 0.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 121
% 0.42/0.83 === Backtracking. Learning clause 51:4:4:[45.3,15.1]:TopTopTopTop: product(e_1,x0,x1),product(x0,x1,x2),next(x1,x3),greater(x2,x3) ->
% 0.42/0.83 === Backtracking. Learning clause 53:12:3:[16.0,52.3,45.3,45.1,41.3,43.1,41.6]:TopTopTop: product(x0,e_1,x1),product(x0,e_1,e_4),group_element(x1),group_element(x2) -> product(e_1,x1,e_2),product(e_1,x1,e_3),product(e_1,x1,e_5),equalish(x1,x2),product(e_1,x2,e_1),product(e_1,x2,e_2),product(e_1,x2,e_3),product(e_1,x2,e_5)
% 0.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 184
% 0.42/0.83 === Backtracking. Learning clause 66:15:5:[19.0,54.0,18.0,55.4,17.0,56.5,16.0,57.12,35.0,58.14,34.0,59.17,30.0,60.18,25.0,61.20,33.0,62.21,29.0,63.22,15.0,64.25,50.0,65.26,45.3,44.1,41.6,43.1,53.9,43.1,43.1,41.7,41.6,45.2,45.2,43.1,43.1,45.1,45.2,43.1,43.1,41.5,51.1,41.6,43.1,44.1,49.6,44.1,45.2,44.1,43.1,45.1,45.1,43.1,43.1,51.2,43.1,15.1,51.2,15.1,41.4]:TopTopTopTopTop: group_element(x0),next(e_1,x1),greater(e_4,x1),next(e_2,x2),greater(e_5,x2),next(e_3,x3),greater(e_5,x3),next(e_2,x4),greater(e_4,x4) -> equalish(e_4,x0),equalish(x0,e_3),equalish(x0,e_2),equalish(x0,e_1),product(e_1,e_1,e_1),product(e_1,e_1,e_3)
% 0.42/0.83 === Backtracking. Learning clause 67:2:2:[42.3,23.1]:TopTop: product(x0,x1,e_1),product(x0,x1,e_4) ->
% 0.42/0.83 === Backtracking. Learning clause 68:2:2:[43.3,23.1]:TopTop: product(x0,e_1,x1),product(x0,e_4,x1) ->
% 0.42/0.83 === Backtracking. Learning clause 69:11:6:[41.3,45.1,44.1,44.2,45.3]:TopTopTopTopTopTop: group_element(x0),group_element(x1),product(x1,e_1,x2),product(x3,x1,e_5),product(x1,x4,x5),product(x4,x5,e_4) -> product(x0,x1,e_2),product(x0,x1,e_3),product(e_1,x0,x2),equalish(x0,x5),equalish(x3,x0)
% 0.42/0.83 === Conflict found: 69:11:6:[41.3,45.1,44.1,44.2,45.3]:TopTopTopTopTopTop: group_element(x0),group_element(x1),product(x1,e_1,x2),product(x3,x1,e_5),product(x1,x4,x5),product(x4,x5,e_4) -> product(x0,x1,e_2),product(x0,x1,e_3),product(e_1,x0,x2),equalish(x0,x5),equalish(x3,x0) {x0 -> e_3, x1 -> e_3, x2 -> e_4, x3 -> e_2, x4 -> e_1, x5 -> e_4}
% 0.42/0.83 === Backtracking. Learning clause 79:22:6:[19.0,70.0,18.0,71.2,16.0,72.3,43.0,73.11,31.0,74.12,42.1,75.14,35.0,76.16,43.0,77.19,22.0,78.25,69.7,45.2,45.2,53.11,41.7,45.1,44.1,69.4,45.3,41.6,44.2,43.2,49.6,45.1,44.1,43.1,45.1]:TopTopTopTopTopTop: product(e_1,e_4,e_4),group_element(x0),next(x0,x1),greater(e_5,x1),product(e_1,e_2,x2),product(x3,x0,x2),product(e_1,x4,e_2),product(e_1,e_2,x5) -> product(e_1,e_4,e_2),product(e_1,e_4,e_5),product(e_1,e_3,e_1),product(x0,e_3,e_2),equalish(x0,e_4),equalish(e_1,x0),product(e_3,e_1,e_1),product(e_3,e_1,e_5),equalish(x0,e_3),product(x0,e_1,e_1),product(x0,e_1,e_4),equalish(e_2,x3),equalish(e_3,x4),product(e_2,e_3,x5)
% 0.42/0.83 === Backtracking. Learning clause 80:11:6:[45.3,45.1,41.5,45.2,45.2]:TopTopTopTopTopTop: product(x0,x1,x2),product(x0,e_3,x3),group_element(x1),group_element(x2),product(x4,x1,x2),product(x5,x1,x2) -> product(e_3,x2,x3),product(x1,x2,e_1),product(x1,x2,e_5),product(x2,x4,e_2),product(x2,x5,e_4)
% 0.42/0.83 === Backtracking. Learning clause 81:20:11:[45.3,42.2,53.5,45.2,42.1,43.2,43.2,42.2,45.3]:TopTopTopTopTopTopTopTopTopTopTop: product(x0,e_1,x1),product(x1,x0,x2),product(x3,e_1,x1),product(x3,e_1,e_4),group_element(x1),group_element(x4),product(x5,e_1,x1),product(x1,x5,x6),product(e_1,x7,e_5),product(e_1,x8,e_5),product(x4,x9,e_1),product(x9,e_1,x10) -> equalish(x2,e_2),equalish(x1,x4),product(e_1,x4,e_1),product(e_1,x4,e_3),equalish(e_3,x6),equalish(x7,x4),equalish(x8,x1),equalish(x10,e_2)
% 0.42/0.83 === Backtracking. Learning clause 82:8:2:[45.3,45.2,41.4]:TopTop: product(e_2,x0,x1),group_element(x0),group_element(x1) -> product(e_2,x0,e_2),product(x0,x1,e_1),product(x0,x1,e_3),product(x0,x1,e_4),product(x0,x1,e_5)
% 0.42/0.83 === Backtracking. Learning clause 83:20:11:[45.3,42.2,53.7,45.2,42.2,45.2,42.1,42.2,42.2,45.3]:TopTopTopTopTopTopTopTopTopTopTop: product(x0,e_1,x1),product(x1,x0,x2),product(x3,e_1,x1),product(x3,e_1,e_4),group_element(x1),group_element(x4),product(x5,e_1,x1),product(x1,x5,x6),product(x7,e_1,x1),product(x1,x7,x8),product(x4,x9,e_1),product(x9,e_1,x10) -> equalish(x2,e_5),equalish(x1,x4),product(e_1,x4,e_1),product(e_1,x4,e_3),equalish(x6,e_2),equalish(e_3,x8),equalish(x10,e_5),equalish(x10,e_2)
% 0.42/0.83 === Backtracking. Learning clause 84:13:3:[45.3,45.2,53.6]:TopTopTop: product(e_3,e_1,x0),product(x1,e_1,x0),product(x1,e_1,e_4),group_element(x0),group_element(x2) -> product(e_3,e_1,e_3),product(e_1,x0,e_2),product(e_1,x0,e_5),equalish(x0,x2),product(e_1,x2,e_1),product(e_1,x2,e_2),product(e_1,x2,e_3),product(e_1,x2,e_5)
% 0.42/0.83 === Conflict found: 80:11:6:[45.3,45.1,41.5,45.2,45.2]:TopTopTopTopTopTop: product(x0,x1,x2),product(x0,e_3,x3),group_element(x1),group_element(x2),product(x4,x1,x2),product(x5,x1,x2) -> product(e_3,x2,x3),product(x1,x2,e_1),product(x1,x2,e_5),product(x2,x4,e_2),product(x2,x5,e_4) {x0 -> e_4, x1 -> e_3, x2 -> e_2, x3 -> e_2, x4 -> e_4, x5 -> e_4}
% 0.42/0.83 === Backtracking. Learning clause 85:25:10:[80.8,45.1,45.2,44.2,45.2,44.2,69.4,49.5]:TopTopTopTopTopTopTopTopTopTop: product(x0,x1,x2),product(x0,e_3,e_2),group_element(x1),product(x3,x1,x2),product(x4,x1,x2),product(x5,x2,x4),product(x6,x5,e_4),product(x3,e_3,x2),product(x7,x3,e_2),group_element(x8),product(e_1,e_2,e_4),group_element(x2),next(x2,x9),greater(e_5,x9) -> product(e_1,x1,e_2),equalish(x6,x4),equalish(x7,x2),product(x8,x2,e_2),product(x8,x2,e_3),product(e_1,x8,e_2),equalish(x8,e_2),equalish(x1,x8),product(x2,e_1,e_1),product(x2,e_1,e_3),product(x2,e_1,e_4)
% 0.42/0.83 === Conflict found: 69:11:6:[41.3,45.1,44.1,44.2,45.3]:TopTopTopTopTopTop: group_element(x0),group_element(x1),product(x1,e_1,x2),product(x3,x1,e_5),product(x1,x4,x5),product(x4,x5,e_4) -> product(x0,x1,e_2),product(x0,x1,e_3),product(e_1,x0,x2),equalish(x0,x5),equalish(x3,x0) {x0 -> e_5, x1 -> e_1, x2 -> e_1, x3 -> e_4, x4 -> e_5, x5 -> e_3}
% 0.42/0.83 === Backtracking. Learning clause 86:18:8:[69.6,45.3,45.3,41.6]:TopTopTopTopTopTopTopTop: group_element(x0),group_element(x1),product(x1,e_1,x2),product(x1,x3,x4),product(x4,x5,x3),product(x1,x6,x7),product(x6,x7,e_5),group_element(x5),group_element(x3) -> product(x0,x1,e_2),product(x0,x1,e_3),product(e_1,x0,x2),equalish(x0,x4),equalish(x7,x0),product(x5,x3,e_1),product(x5,x3,e_2),product(x5,x3,e_3),product(x5,x3,e_5)
% 0.42/0.83 === Backtracking. Learning clause 87:8:3:[41.5,43.2]:TopTopTop: group_element(x0),group_element(x1),product(x0,x2,e_3) -> product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_4),product(x0,x1,e_5),equalish(x2,x1)
% 0.42/0.83 === Clause set with instances from active satisfied. Growing active. New size: 205
% 0.42/0.83
% 0.42/0.83 Linear Model Building succeeded.
% 0.42/0.83 SZS status Satisfiable
% 0.42/0.83
% 0.42/0.83 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.42/0.83
% 0.42/0.83 SPASS-SCL-FOL Statistics:
% 0.42/0.83 Number of learned clauses: 18
% 0.42/0.83 Number of propagations: 771
% 0.42/0.83 Number of decisions: 75
% 0.42/0.83 Number of resolutions: 107
% 0.42/0.83 Number of condensations: 1
% 0.42/0.83 Number of sub resolutions: 24
% 0.42/0.83 Number of input literals (deduplicated): 50
% 0.42/0.83 Number of grows: 5
% 0.42/0.83 Number of considered ground atoms: 205
% 0.42/0.83
% 0.42/0.83 Needed: 0:00:00.22
% 0.42/0.83
%------------------------------------------------------------------------------