%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GRP127-3.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 : n022.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:05 PM UTC 2026
% Result : Satisfiable 7.22s 2.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : GRP127-3.005 : TPTP v9.2.1. Released v1.2.0.
% 0.00/0.13 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.16/0.34 % Computer : n022.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:22 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.34 SPASS-SCL-FOL version:
% 0.19/0.43 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 7.22/2.02 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.22/2.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.22/2.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.22/2.02 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.22/2.02 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.22/2.02 Execution normal ended with status: satisfiable
% 7.22/2.02 Used heuristic: normal
% 7.22/2.02
% 7.22/2.02 Input Clauses:
% 7.22/2.02
% 7.22/2.02 Predicates: next greater cycle equalish group_element product
% 7.22/2.02 Fol Constants: e_0 e_1 e_2 e_3 e_4 e_5
% 7.22/2.02 Fol Functions:
% 7.22/2.02 Problem Properties:
% 7.22/2.02 This is a Bernays Schoenfinkel problem.
% 7.22/2.02
% 7.22/2.02 After reduction: Problem Properties:
% 7.22/2.02 This is a Bernays Schoenfinkel problem.
% 7.22/2.02
% 7.22/2.02
% 7.22/2.02 Reduced Input Clauses:
% 7.22/2.02
% 7.22/2.02 Most General Atoms: cycle(x3,x4) greater(x1,x0) next(x0,x3) group_element(x1) equalish(x0,x3) product(x3,x0,x1)
% 7.22/2.02
% 7.22/2.02 === Starting SPASS-SCL-FOL A Little Less Naive, considering 366 atoms initially, heuristics mode: normal ===
% 7.22/2.02
% 7.22/2.02 === Backtracking. Learning clause 63:27:7:[15.0,59.0,6.0,60.1,29.0,61.3,28.0,62.5,22.2,26.1,27.1,53.5,58.2,53.4,55.1,53.5,58.2,53.3,58.2,55.1,56.1]:TopTopTopTopTopTopTop: next(e_2,x0),group_element(x1),group_element(x2),group_element(x3),product(x3,x4,x2),product(e_2,x5,e_5),product(x6,x1,e_5) -> cycle(e_2,e_2),cycle(e_2,e_3),cycle(e_2,e_4),equalish(e_3,x0),product(e_2,e_1,e_1),product(e_2,e_1,e_2),product(e_4,e_1,x1),product(e_1,x1,e_1),product(e_1,x1,e_4),equalish(x1,x2),product(e_1,x2,e_1),product(e_1,x2,e_4),product(e_1,x2,e_5),product(e_2,x2,x3),product(x2,x3,e_2),product(x2,x3,e_4),product(x2,x3,e_5),product(e_3,x3,x4),equalish(e_1,x5),equalish(e_1,x6)
% 7.22/2.02 === Backtracking. Learning clause 78:41:12:[17.0,64.0,6.0,65.1,28.0,66.3,31.0,67.4,30.0,68.5,32.0,69.8,29.0,70.9,7.0,71.12,8.0,72.16,9.0,73.20,48.0,74.25,47.0,75.26,51.0,76.27,33.0,77.51,22.2,26.1,27.1,53.7,58.1,53.7,56.1,56.1,53.5,56.1,53.3,58.2,55.1,53.5,63.5,24.1,24.1,24.1]:TopTopTopTopTopTopTopTopTopTopTopTop: next(e_2,x0),next(e_2,x1),group_element(x2),cycle(x3,x4),next(e_2,x3),next(x4,x5),cycle(x6,x7),next(e_2,x6),next(x7,x8),cycle(x9,x10),next(e_2,x9),next(x10,x11) -> equalish(e_5,x0),product(e_4,e_2,e_2),product(e_4,e_2,e_4),product(e_3,e_2,e_2),product(e_3,e_2,e_3),product(e_3,e_2,e_4),product(e_5,e_2,x2),product(e_2,x2,e_1),product(e_2,x2,e_2),product(e_2,x2,e_4),equalish(e_3,x1),product(e_2,e_1,e_1),product(e_2,e_1,e_2),product(e_4,e_1,x2),product(e_1,x2,e_1),product(e_1,x2,e_4),equalish(x2,e_5),product(e_1,e_5,e_1),product(e_1,e_5,e_4),product(e_1,e_5,e_5),product(e_2,e_5,e_2),product(e_5,e_2,e_2),product(e_5,e_2,e_4),product(e_5,e_2,e_5),product(e_3,e_2,x2),equalish(e_1,x2),equalish(e_2,x5),equalish(e_3,x8),equalish(e_4,x11)
% 7.22/2.02 === Backtracking. Learning clause 83:6:4:[9.0,79.1,8.0,80.2,7.0,81.3,6.0,82.7,22.6,27.1,27.1,27.1,26.1,27.1]:TopTopTopTop: group_element(x0),product(x0,e_1,x1),greater(x1,x0),product(x0,e_1,x2),next(x0,x3) -> equalish(x2,x3)
% 7.22/2.02 === Backtracking. Learning clause 84:3:1:[27.5,47.1,8.1]:Top: cycle(x0,e_3),product(x0,e_1,e_4),next(x0,e_3) ->
% 7.22/2.02 === Backtracking. Learning clause 85:5:0:[22.1,29.1]:: -> cycle(e_2,e_0),cycle(e_2,e_1),cycle(e_2,e_2),cycle(e_2,e_3),cycle(e_2,e_4)
% 7.22/2.02 === Conflict found: 83:6:4:[9.0,79.1,8.0,80.2,7.0,81.3,6.0,82.7,22.6,27.1,27.1,27.1,26.1,27.1]:TopTopTopTop: group_element(x0),product(x0,e_1,x1),greater(x1,x0),product(x0,e_1,x2),next(x0,x3) -> equalish(x2,x3) {x0 -> e_2, x1 -> e_4, x2 -> e_4, x3 -> e_3}
% 7.22/2.02 === Backtracking. Learning clause 87:3:1:[3.0,86.3,83.1,29.1,47.1]:Top: product(e_2,e_1,x0),greater(x0,e_2),product(e_2,e_1,e_4) ->
% 7.22/2.02 === Backtracking. Learning clause 89:16:9:[7.0,88.3,22.4,24.1,24.2,24.2,1.1]:TopTopTopTopTopTopTopTopTop: group_element(x0),cycle(x1,x2),next(x0,x1),next(x2,x3),cycle(x4,x5),next(x4,x0),greater(x5,e_0),cycle(x6,x7),next(x6,x0),greater(x7,e_0),next(e_3,x8) -> cycle(x0,e_1),cycle(x0,e_4),equalish(e_2,x3),equalish(x5,e_1),equalish(x7,x8)
% 7.22/2.02 === Conflict found: 89:16:9:[7.0,88.3,22.4,24.1,24.2,24.2,1.1]:TopTopTopTopTopTopTopTopTop: group_element(x0),cycle(x1,x2),next(x0,x1),next(x2,x3),cycle(x4,x5),next(x4,x0),greater(x5,e_0),cycle(x6,x7),next(x6,x0),greater(x7,e_0),next(e_3,x8) -> cycle(x0,e_1),cycle(x0,e_4),equalish(e_2,x3),equalish(x5,e_1),equalish(x7,x8) {x0 -> e_1, x1 -> e_2, x2 -> e_3, x3 -> e_4, x4 -> e_0, x5 -> e_2, x6 -> e_0, x7 -> e_2, x8 -> e_4}
% 7.22/2.02 === Backtracking. Learning clause 91:18:11:[9.0,90.12,89.13,27.1]:TopTopTopTopTopTopTopTopTopTopTop: group_element(x0),cycle(x1,x2),next(x0,x1),next(x2,x3),cycle(x4,x5),next(x4,x0),greater(x5,e_0),cycle(x6,x7),next(x6,x0),greater(x7,e_0),next(e_3,x8),product(x0,e_1,x9),next(x0,x10) -> cycle(x0,e_1),equalish(e_2,x3),equalish(x5,e_1),equalish(x7,x8),equalish(x9,x10)
% 7.22/2.02 === Backtracking. Learning clause 92:4:5:[58.2,58.3]:TopTopTopTopTop: product(x0,x1,x2),product(x0,x3,x4),product(x4,x0,x2) -> product(x3,x0,x1)
% 7.22/2.02 === Conflict found: 92:4:5:[58.2,58.3]:TopTopTopTopTop: product(x0,x1,x2),product(x0,x3,x4),product(x4,x0,x2) -> product(x3,x0,x1) {x0 -> e_5, x1 -> e_4, x2 -> e_3, x3 -> e_0, x4 -> e_1}
% 7.22/2.02 === Backtracking. Learning clause 93:6:7:[92.2,58.3,55.1]:TopTopTopTopTopTopTop: product(x0,x1,x2),product(x3,x0,x2),product(x4,x3,x5),product(x5,x4,x0),product(x4,x6,x1) -> equalish(x0,x6)
% 7.22/2.02 === Backtracking. Learning clause 105:24:7:[32.0,94.0,29.0,95.1,31.0,96.2,30.0,97.6,28.0,98.7,41.0,99.15,36.0,100.16,52.0,101.19,46.0,102.24,35.0,103.25,47.0,104.32,53.7,56.1,58.2,53.7,56.1,53.4,56.1,58.2,58.2,53.5,55.1,53.7,27.2,93.5,56.1,58.1,53.6,56.2,27.2,56.2,37.1,55.1,57.1,55.2]:TopTopTopTopTopTopTop: cycle(e_4,x0),greater(x0,e_0),next(e_4,x1),product(x2,e_1,e_3),cycle(e_3,x3),greater(x3,e_0),next(e_3,x4),product(e_1,x5,e_1),product(e_2,x6,e_2) -> product(e_3,e_4,e_3),product(e_5,e_4,e_3),product(e_5,e_4,e_5),product(e_4,e_2,e_1),product(e_4,e_2,e_2),product(e_4,e_1,e_1),equalish(e_2,x1),product(e_4,e_1,e_4),product(e_3,e_1,e_1),product(e_3,e_1,e_3),product(e_3,e_1,e_5),equalish(x2,e_4),equalish(e_2,x4),equalish(e_4,x5),equalish(x6,e_4)
% 7.22/2.02 === Backtracking. Learning clause 118:48:20:[32.0,106.0,30.0,107.2,6.0,108.7,31.0,109.9,9.0,110.27,34.0,111.29,42.0,112.30,33.0,113.31,52.0,114.32,43.0,115.44,89.1,116.47,47.0,117.52,53.6,93.5,92.1,55.2,55.1,53.4,93.4,53.7,56.1,58.1,53.6,57.1,27.2,56.2,27.2,105.13,93.5,27.2,22.3,53.5,56.2,56.1,57.1,27.2,28.1,89.2,24.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: product(e_1,e_1,x0),next(e_4,x1),next(e_3,x2),product(e_1,x3,e_1),product(e_2,x4,e_2),next(e_4,x5),group_element(x6),product(x7,e_1,e_1),cycle(e_3,x8),greater(x8,e_0),next(e_3,x9),group_element(x10),next(x10,e_4),next(e_2,x11),cycle(x12,x13),next(x12,x10),greater(x13,e_0),cycle(x14,x15),next(x14,x10),greater(x15,e_0),next(e_3,x16),cycle(x17,x18),next(e_4,x17),next(x18,x19) -> product(e_5,e_4,e_3),product(e_5,e_4,e_5),product(e_4,e_2,e_2),product(e_4,e_1,e_1),equalish(e_2,x1),product(e_3,e_1,e_1),product(e_3,e_1,e_5),equalish(x6,e_4),equalish(e_2,x2),equalish(e_4,x3),equalish(x4,e_4),equalish(e_4,x5),cycle(e_4,e_0),product(x6,e_1,e_2),product(x6,e_1,e_4),product(x6,e_1,e_5),equalish(x7,x6),equalish(e_3,x9),cycle(x10,e_1),cycle(x10,e_4),equalish(e_2,x11),equalish(x13,e_1),equalish(x15,x16),equalish(e_4,x19)
% 7.22/2.02
% 7.22/2.02 Linear Model Building succeeded.
% 7.22/2.02 SZS status Satisfiable
% 7.22/2.02
% 7.22/2.02 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.22/2.02
% 7.22/2.02 SPASS-SCL-FOL Statistics:
% 7.22/2.02 Number of learned clauses: 12
% 7.22/2.02 Number of propagations: 1290
% 7.22/2.02 Number of decisions: 67
% 7.22/2.02 Number of resolutions: 96
% 7.22/2.02 Number of condensations: 2
% 7.22/2.02 Number of sub resolutions: 48
% 7.22/2.02 Number of input literals (deduplicated): 65
% 7.22/2.02 Number of grows: 0
% 7.22/2.02 Number of considered ground atoms: 366
% 7.22/2.02
% 7.22/2.02 Needed: 0:00:01.47
% 7.22/2.02
%------------------------------------------------------------------------------