%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GRP129-3.004 : 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 : 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:23:06 PM UTC 2026
% Result : Unsatisfiable 2.87s 0.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.06 % Problem : GRP129-3.004 : TPTP v9.2.1. Released v1.2.0.
% 0.00/0.06 % Command : /export/starexec/sandbox2/solver/bin/execute.py 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.24 % Computer : n012.cluster.edu
% 0.06/0.24 % Model : x86_64 x86_64
% 0.06/0.24 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.24 % Memory : 8042.1875MB
% 0.06/0.24 % OS : Linux 3.10.0-693.el7.x86_64
% 0.06/0.24 % CPULimit : 300
% 0.06/0.24 % WCLimit : 300
% 0.06/0.24 % DateTime : Thu May 7 12:01:01 EDT 2026
% 0.06/0.24 % CPUTime :
% 0.06/0.25 SPASS-SCL-FOL version:
% 0.06/0.30 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 2.87/0.95 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.87/0.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.87/0.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.87/0.95 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.87/0.95 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.87/0.95 Execution resolution_1 ended with status: unsatisfiable
% 2.87/0.95 Used heuristic: resolution_1
% 2.87/0.95
% 2.87/0.95 Input Clauses:
% 2.87/0.95
% 2.87/0.95 Predicates: next greater cycle equalish group_element product
% 2.87/0.95 Fol Constants: e_0 e_1 e_2 e_3 e_4
% 2.87/0.95 Fol Functions:
% 2.87/0.95 Problem Properties:
% 2.87/0.95 This is a Bernays Schoenfinkel problem.
% 2.87/0.95
% 2.87/0.95 After reduction: Problem Properties:
% 2.87/0.95 This is a Bernays Schoenfinkel problem.
% 2.87/0.95
% 2.87/0.95
% 2.87/0.95 Reduced Input Clauses:
% 2.87/0.95
% 2.87/0.95 Most General Atoms: cycle(x3,x4) greater(x1,x0) next(x0,x3) group_element(x1) equalish(x0,x3) product(x2,x0,x3)
% 2.87/0.95
% 2.87/0.95 === Starting SPASS-SCL-FOL A Little Less Naive, considering 45 atoms initially, heuristics mode: resolution_1 ===
% 2.87/0.95
% 2.87/0.95 === Backtracking. Learning clause 45:5:1:[7.0,43.1,1.0,44.2,18.6,32.1,17.1,16.5]:Top: next(x0,e_4),group_element(x0) -> cycle(x0,e_0),cycle(x0,e_1),cycle(x0,e_2)
% 2.87/0.95 === Backtracking. Learning clause 48:4:1:[6.0,46.0,1.0,47.1,18.6,29.1,17.1,45.5]:Top: next(x0,e_4),group_element(x0) -> cycle(x0,e_0),cycle(x0,e_1)
% 2.87/0.95 === Backtracking. Learning clause 49:6:1:[18.6,26.1,17.1,48.4,19.1,5.1]:Top: next(e_0,e_2),next(x0,e_4),group_element(x0),next(x0,x0),greater(x0,x0),greater(e_0,e_0) ->
% 2.87/0.95 === Backtracking. Learning clause 50:5:3:[19.1,17.1]:TopTopTop: cycle(x0,e_0),cycle(x1,x2),next(x0,x1),greater(x0,e_4),greater(e_0,x2) ->
% 2.87/0.95 === Backtracking. Learning clause 51:7:3:[38.6,39.1]:TopTopTop: group_element(x0),group_element(x1),product(x0,x1,x2) -> product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_3),equalish(e_4,x2)
% 2.87/0.95 === Backtracking. Learning clause 53:6:1:[22.0,52.1,38.6,20.2,20.2,20.2,20.2]:Top: group_element(x0),greater(e_4,x0),greater(e_3,x0),greater(e_2,x0),cycle(x0,e_0),greater(e_1,x0) ->
% 2.87/0.95 === Backtracking. Learning clause 54:3:0:[18.6,26.1,17.1,48.4,53.5,8.1,7.1,6.1,5.1]:: next(e_0,e_2),next(e_0,e_4),group_element(e_0) ->
% 2.87/0.95 === Backtracking. Learning clause 55:2:1:[15.3,34.1]:Top: cycle(x0,e_3),cycle(x0,e_4) ->
% 2.87/0.95 === Backtracking. Learning clause 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5)
% 2.87/0.95 === Conflict found: 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5) {x0 -> e_0, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_3, x5 -> e_3}
% 2.87/0.95 === Backtracking. Learning clause 59:6:1:[7.0,58.1,57.8,35.1,32.1,29.1,27.1,16.5]:Top: next(x0,e_1),next(x0,e_3),group_element(x0) -> cycle(x0,e_0),cycle(x0,e_1),cycle(x0,e_2)
% 2.87/0.95 === Backtracking. Learning clause 60:2:1:[15.3,30.1]:Top: cycle(x0,e_2),cycle(x0,e_3) ->
% 2.87/0.95 === Backtracking. Learning clause 61:2:1:[15.3,31.1]:Top: cycle(x0,e_2),cycle(x0,e_4) ->
% 2.87/0.95 === Conflict found: 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5) {x0 -> e_0, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_2, x5 -> e_3}
% 2.87/0.95 === Backtracking. Learning clause 63:5:1:[6.0,62.0,57.8,35.1,32.1,29.1,27.1,59.6]:Top: next(x0,e_1),next(x0,e_3),group_element(x0) -> cycle(x0,e_0),cycle(x0,e_1)
% 2.87/0.95 === Backtracking. Learning clause 64:2:1:[15.3,27.1]:Top: cycle(x0,e_1),cycle(x0,e_3) ->
% 2.87/0.95 === Backtracking. Learning clause 65:2:1:[15.3,28.1]:Top: cycle(x0,e_1),cycle(x0,e_4) ->
% 2.87/0.95 === Conflict found: 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5) {x0 -> e_0, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_1, x5 -> e_3}
% 2.87/0.95 === Backtracking. Learning clause 66:6:1:[57.8,35.1,32.1,29.1,27.1,63.5,19.1,5.1]:Top: next(x0,e_1),next(x0,e_3),group_element(x0),next(x0,x0),greater(x0,x0),greater(e_0,e_0) ->
% 2.87/0.95 === Conflict found: 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5) {x0 -> e_0, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_1, x5 -> e_3}
% 2.87/0.95 === Backtracking. Learning clause 68:2:0:[1.0,67.0,57.8,35.1,32.1,29.1,27.1,63.5,53.5,8.1,7.1,6.1,5.1]:: next(e_0,e_3),group_element(e_0) ->
% 2.87/0.95 === Conflict found: 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5) {x0 -> e_0, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_3, x5 -> e_2}
% 2.87/0.95 === Backtracking. Learning clause 70:6:1:[7.0,69.1,57.8,35.1,32.1,29.1,26.1,16.5]:Top: next(x0,e_1),next(x0,e_2),group_element(x0) -> cycle(x0,e_0),cycle(x0,e_1),cycle(x0,e_2)
% 2.87/0.95 === Conflict found: 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5) {x0 -> e_0, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_2, x5 -> e_2}
% 2.87/0.95 === Backtracking. Learning clause 72:5:1:[6.0,71.0,57.8,35.1,32.1,29.1,26.1,70.6]:Top: next(x0,e_1),next(x0,e_2),group_element(x0) -> cycle(x0,e_0),cycle(x0,e_1)
% 2.87/0.95 === Conflict found: 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5) {x0 -> e_0, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_1, x5 -> e_2}
% 2.87/0.95 === Backtracking. Learning clause 73:6:1:[57.8,35.1,32.1,29.1,26.1,72.5,19.1,5.1]:Top: next(x0,e_1),next(x0,e_2),group_element(x0),next(x0,x0),greater(x0,x0),greater(e_0,e_0) ->
% 2.87/0.95 === Conflict found: 57:11:6:[22.0,56.1,38.6,21.2,21.2,21.2,21.2]:TopTopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),next(x0,x3),cycle(x0,x4),greater(x4,e_0),next(x0,x5) -> equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x3),equalish(e_1,x5) {x0 -> e_0, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_1, x5 -> e_2}
% 2.87/0.95 === Backtracking. Learning clause 75:2:0:[1.0,74.0,57.8,35.1,32.1,29.1,26.1,72.5,53.5,8.1,7.1,6.1,5.1]:: next(e_0,e_2),group_element(e_0) ->
% 2.87/0.95 === Backtracking. Learning clause 76:6:1:[18.6,28.1,17.1,48.4,19.1,5.1]:Top: next(e_0,e_4),next(x0,e_4),group_element(x0),next(x0,x0),greater(x0,x0),greater(e_0,e_0) ->
% 2.87/0.95 === Backtracking. Learning clause 77:2:0:[18.6,28.1,17.1,48.4,53.5,8.1,7.1,6.1,5.1]:: next(e_0,e_4),group_element(e_0) ->
% 2.87/0.95 === Backtracking. Learning clause 79:10:5:[22.0,78.1,38.6,21.2,21.2,21.2]:TopTopTopTopTop: group_element(x0),next(x0,x1),next(x0,x2),cycle(x0,x3),greater(x3,e_0),next(x0,x4) -> product(x0,e_1,e_1),equalish(e_4,x1),equalish(e_3,x2),equalish(e_2,x4)
% 2.87/0.95 === Clause set with instances from active satisfied. Growing active. New size: 59
% 2.87/0.95 === Restarting.
% 2.87/0.95 === Clause set with instances from active satisfied. Growing active. New size: 100
% 2.87/0.95 === Conflict found: 48:4:1:[6.0,46.0,1.0,47.1,18.6,29.1,17.1,45.5]:Top: next(x0,e_4),group_element(x0) -> cycle(x0,e_0),cycle(x0,e_1) {x0 -> e_3}
% 2.87/0.95 === Backtracking. Learning clause 81:4:2:[5.0,80.3,48.3,19.2,18.1,4.1,24.1,26.1,17.1]:TopTop: cycle(x0,x1),greater(e_3,x0),greater(x1,e_0),next(e_0,e_2) ->
% 2.87/0.95 === Backtracking. Learning clause 82:2:2:[39.3,30.1]:TopTop: product(x0,x1,e_2),product(x0,x1,e_3) ->
% 2.87/0.95 === Backtracking. Learning clause 83:2:2:[39.3,34.1]:TopTop: product(x0,x1,e_3),product(x0,x1,e_4) ->
% 2.87/0.95 === Backtracking. Learning clause 85:2:0:[22.0,84.0,16.2,19.1,19.1,19.1,19.1,10.1,48.3,24.1,18.1,4.1,17.1,26.1,7.1,6.1,5.1]:: greater(e_0,e_0),next(e_0,e_2) ->
% 2.87/0.95 === Clause set with instances from active satisfied. Growing active. New size: 157
% 2.87/0.95 === Backtracking. Learning clause 86:4:5:[40.2,42.3]:TopTopTopTopTop: product(x0,x1,x2),product(x3,x4,x0),product(x4,x0,x2) -> equalish(x1,x3)
% 2.87/0.95 === Backtracking. Learning clause 88:7:2:[22.0,87.1,38.4,20.2,20.2,41.1,20.2]:TopTop: group_element(x0),greater(e_2,x0),greater(e_4,x0),product(x1,e_1,e_1),cycle(x0,e_0),greater(e_3,x0) -> equalish(x0,x1)
% 2.87/0.95 === Clause set with instances from active satisfied. Growing active. New size: 213
% 2.87/0.95 === Backtracking. Learning clause 89:8:4:[38.5,41.1,41.1]:TopTopTopTop: group_element(x0),group_element(x1),product(x2,x1,e_3),product(x3,x1,e_2) -> product(x0,x1,e_1),product(x0,x1,e_4),equalish(x0,x2),equalish(x0,x3)
% 2.87/0.95 === Backtracking. Learning clause 90:9:5:[42.3,39.1,38.6,41.1]:TopTopTopTopTop: product(x0,x1,x2),product(x2,x0,x3),group_element(x1),group_element(x2),product(x4,x2,e_2) -> equalish(e_4,x3),product(x1,x2,e_1),product(x1,x2,e_3),equalish(x1,x4)
% 2.87/0.95 === Backtracking. Learning clause 92:1:0:[22.0,91.0,42.3,41.2,38.6,42.2,90.2,86.3,38.5,41.1,38.4,20.2,20.2,16.2,20.2,23.1,36.1,81.1,88.4,14.1,81.1,86.1,88.4,81.1,38.3,20.2,20.2,20.2,11.1,13.1,12.1,33.1,9.1,16.2,81.1,81.1,81.1,10.1,48.3,18.1,4.1,24.1,27.1,6.1,7.1,17.1,32.1,26.1,5.1]:: next(e_0,e_2) ->
% 2.87/0.95 === Backtracking. Learning clause 93:4:2:[21.5,31.1]:TopTop: cycle(x0,x1),product(x0,e_1,e_2),greater(x1,e_0),next(x0,e_4) ->
% 2.87/0.95 === Backtracking. Learning clause 96:5:2:[24.0,94.0,4.0,95.5,38.2,22.1,21.2,34.1,20.2,14.1,21.2,93.2]:TopTop: cycle(e_3,e_0),next(e_3,x0),cycle(e_3,x1),greater(x1,e_0) -> equalish(e_1,x0)
% 2.87/0.95 === Backtracking. Learning clause 99:11:6:[10.0,97.0,26.0,98.12,38.5,20.2,20.2,16.2,88.4,19.1,41.2,33.1,11.1,19.1,9.1,19.1,13.1,12.1,23.1,16.2,22.1,19.1,19.1,19.1]:TopTopTopTopTopTop: cycle(x0,x1),next(e_3,x0),greater(e_2,x1),product(e_3,e_1,e_2),cycle(x2,x3),next(e_3,x2),greater(e_3,x3),cycle(e_3,e_0),cycle(x4,x5),next(e_3,x4),greater(e_1,x5) ->
% 2.87/0.95 === Backtracking. Learning clause 103:10:6:[24.0,100.0,10.0,101.1,27.0,102.12,42.3,41.2,38.6,42.2,90.2,36.1,86.3,42.1,20.2,38.5,88.4,20.2,14.1,11.1,9.1,16.2,22.1,19.1,19.1,19.1,99.4]:TopTopTopTopTopTop: cycle(x0,x1),next(e_3,x0),greater(e_2,x1),cycle(x2,x3),next(e_3,x2),greater(e_3,x3),cycle(e_3,e_0),cycle(x4,x5),next(e_3,x4),greater(e_1,x5) ->
% 2.87/0.95 === Conflict found: 48:4:1:[6.0,46.0,1.0,47.1,18.6,29.1,17.1,45.5]:Top: next(x0,e_4),group_element(x0) -> cycle(x0,e_0),cycle(x0,e_1) {x0 -> e_3}
% 2.87/0.95 === Backtracking. Learning clause 106:10:6:[5.0,104.1,4.0,105.2,48.2,24.1,93.1,103.7]:TopTopTopTopTopTop: product(e_3,e_1,e_2),cycle(x0,x1),next(e_3,x0),greater(e_2,x1),cycle(x2,x3),next(e_3,x2),greater(e_3,x3),cycle(x4,x5),next(e_3,x4),greater(e_1,x5) ->
% 2.87/0.95 === Backtracking. Learning clause 108:5:1:[22.0,107.1,38.6,86.1,86.1,86.1,86.1,38.3]:Top: group_element(x0) -> equalish(e_1,x0),product(x0,e_1,e_2),product(x0,e_1,e_3),product(x0,e_1,e_4)
% 2.87/0.95 === Backtracking. Learning clause 111:5:1:[22.0,109.2,26.0,110.3,21.4,2.1,38.3]:Top: cycle(e_1,x0),greater(x0,e_0) -> product(e_1,e_1,e_2),product(e_1,e_1,e_3),product(e_1,e_1,e_4)
% 2.87/0.95 === Backtracking. Learning clause 112:8:3:[18.5,3.1,16.4]:TopTopTop: cycle(x0,x1),next(x0,x2),greater(x1,e_0),group_element(x2) -> equalish(x1,e_3),cycle(x2,e_0),cycle(x2,e_1),cycle(x2,e_3)
% 2.87/0.95 === Backtracking. Learning clause 114:2:0:[6.0,113.2,18.6,30.1,2.1,3.1]:: cycle(e_1,e_2),cycle(e_2,e_2) ->
% 2.87/0.95 === Conflict found: 112:8:3:[18.5,3.1,16.4]:TopTopTop: cycle(x0,x1),next(x0,x2),greater(x1,e_0),group_element(x2) -> equalish(x1,e_3),cycle(x2,e_0),cycle(x2,e_1),cycle(x2,e_3) {x0 -> e_1, x1 -> e_2, x2 -> e_2}
% 2.87/0.95 === Backtracking. Learning clause 121:4:0:[6.0,115.0,7.0,116.1,9.0,117.2,5.0,118.4,22.0,119.5,26.0,120.6,112.8,18.1,19.2,33.1,23.1,30.1,18.1,2.1,3.1,16.4]:: cycle(e_3,e_1) -> cycle(e_1,e_0),cycle(e_1,e_1),cycle(e_1,e_3)
% 2.87/0.95 === Backtracking. Learning clause 127:6:0:[7.0,122.1,5.0,123.2,29.0,124.4,27.0,125.5,26.0,126.8,20.2,108.4,12.1,41.1,41.1,112.6,18.1,23.1,33.1,30.1,111.3,18.1,2.1,3.1,121.3]:: product(e_3,e_1,e_4),cycle(e_3,e_1) -> product(e_1,e_1,e_3),product(e_1,e_1,e_4),cycle(e_1,e_0),cycle(e_1,e_3)
% 2.87/0.95 === Backtracking. Learning clause 129:13:7:[23.0,128.1,38.5,86.1,86.1,38.4,40.2,42.2,42.2,86.2,40.1]:TopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_2),product(x2,x0,e_2),product(x3,x0,e_2),product(e_1,x4,x5),product(e_2,e_1,x5),product(x0,x6,e_4) -> equalish(e_2,x0),equalish(x1,e_2),product(e_2,x2,e_3),product(e_2,x3,e_1),equalish(x4,e_2),equalish(e_2,x6)
% 2.87/0.95 === Backtracking. Learning clause 130:15:8:[38.3,40.2,86.3,41.1,40.1,38.5,40.2]:TopTopTopTopTopTopTopTop: group_element(x0),product(x0,x2,e_1),product(x1,x3,e_2),product(x4,x0,x1),product(x0,x5,e_4),group_element(x6),group_element(x1),product(x6,x7,e_2) -> equalish(x2,x1),equalish(x3,x4),equalish(x0,x6),equalish(x1,x5),product(x6,x1,e_1),product(x6,x1,e_4),equalish(x7,x1)
% 2.87/0.95 === Backtracking. Learning clause 131:11:6:[42.3,41.2,38.5,40.2,86.3,40.1]:TopTopTopTopTopTop: product(x0,x1,x0),group_element(x1),group_element(x0),product(x1,x2,e_1),product(x0,x3,e_2),product(x4,x1,x0),product(x1,x5,e_4) -> equalish(x1,x0),equalish(x2,x0),equalish(x3,x4),equalish(x0,x5)
% 2.87/0.95 === Backtracking. Learning clause 132:9:5:[38.5,42.1,42.1,41.1]:TopTopTopTopTop: group_element(x0),group_element(x1),product(x1,e_3,x2),product(x1,e_1,x3),product(x4,x1,e_2) -> product(x0,x1,e_4),product(e_3,x0,x2),product(e_1,x0,x3),equalish(x0,x4)
% 2.87/0.95 === Conflict found: 129:13:7:[23.0,128.1,38.5,86.1,86.1,38.4,40.2,42.2,42.2,86.2,40.1]:TopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_2),product(x2,x0,e_2),product(x3,x0,e_2),product(e_1,x4,x5),product(e_2,e_1,x5),product(x0,x6,e_4) -> equalish(e_2,x0),equalish(x1,e_2),product(e_2,x2,e_3),product(e_2,x3,e_1),equalish(x4,e_2),equalish(e_2,x6) {x0 -> e_3, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_3, x5 -> e_2, x6 -> e_1}
% 2.87/0.95 === Backtracking. Learning clause 133:14:8:[129.11,41.2]:TopTopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_2),product(x2,x0,e_2),product(x3,x0,e_2),product(e_1,x4,x5),product(e_2,e_1,x5),product(x0,x6,e_4),product(x7,x3,e_1) -> equalish(e_2,x0),equalish(x1,e_2),product(e_2,x2,e_3),equalish(x4,e_2),equalish(e_2,x6),equalish(x7,e_2)
% 2.87/0.95 === Backtracking. Learning clause 138:13:5:[22.0,134.1,23.0,135.6,12.0,136.8,26.0,137.15,42.3,41.2,38.6,40.1,40.2,86.3,38.5,42.1,131.7,133.3,108.3,20.2]:TopTopTopTopTop: product(x0,e_1,x1),product(e_1,x2,e_1),group_element(x0),product(x0,x3,e_4),product(x4,e_1,e_1),cycle(e_2,e_0) -> product(e_1,e_1,x1),equalish(x2,e_2),equalish(e_2,x0),equalish(x0,e_2),equalish(e_2,x3),equalish(x4,e_2),product(e_2,e_1,e_4)
% 2.87/0.95 === Backtracking. Learning clause 142:17:6:[6.0,139.1,23.0,140.3,26.0,141.9,42.3,42.2,108.4,21.2,16.4,138.6]:TopTopTopTopTopTop: product(e_1,e_3,e_2),next(e_2,x0),product(x1,e_1,x2),product(e_1,x3,e_1),group_element(x1),product(x1,x4,e_4),product(x5,e_1,e_1) -> equalish(e_2,x0),cycle(e_2,e_1),cycle(e_2,e_3),product(e_1,e_1,x2),equalish(x3,e_2),equalish(e_2,x1),equalish(x1,e_2),equalish(e_2,x4),equalish(x5,e_2),product(e_2,e_1,e_4)
% 2.87/0.95 === Conflict found: 89:8:4:[38.5,41.1,41.1]:TopTopTopTop: group_element(x0),group_element(x1),product(x2,x1,e_3),product(x3,x1,e_2) -> product(x0,x1,e_1),product(x0,x1,e_4),equalish(x0,x2),equalish(x0,x3) {x0 -> e_2, x1 -> e_2, x2 -> e_3, x3 -> e_1}
% 2.87/0.95 === Backtracking. Learning clause 143:10:6:[89.5,86.2,86.1]:TopTopTopTopTopTop: group_element(x0),product(x1,x0,e_3),product(x2,x0,e_2),product(e_1,x3,x4),product(x0,e_1,x4),product(x5,x0,x0) -> equalish(x0,x1),equalish(x0,x2),equalish(x3,x0),equalish(x0,x5)
% 2.87/0.95 === Conflict found: 89:8:4:[38.5,41.1,41.1]:TopTopTopTop: group_element(x0),group_element(x1),product(x2,x1,e_3),product(x3,x1,e_2) -> product(x0,x1,e_1),product(x0,x1,e_4),equalish(x0,x2),equalish(x0,x3) {x0 -> e_4, x1 -> e_2, x2 -> e_3, x3 -> e_2}
% 2.87/0.95 === Backtracking. Learning clause 153:5:0:[6.0,144.0,24.0,145.1,22.0,146.2,7.0,147.3,9.0,148.4,5.0,149.7,35.0,150.8,29.0,151.9,26.0,152.13,89.7,37.1,86.2,25.1,41.1,34.1,38.4,36.1,86.2,41.2,38.6,143.3,42.3,40.2,40.2,40.1,38.5,42.1,86.3,108.4,21.2,16.4,138.6,142.1,41.1,38.3,23.1,18.1,33.1,20.2,127.5,30.1,18.1,2.1,3.1]:: product(e_3,e_1,e_4),cycle(e_3,e_1) -> product(e_1,e_1,e_3),product(e_1,e_1,e_4),cycle(e_1,e_3)
% 2.87/0.95 === Backtracking. Learning clause 154:2:2:[40.3,30.1]:TopTop: product(x0,e_2,x1),product(x0,e_3,x1) ->
% 2.87/0.95 === Conflict found: 133:14:8:[129.11,41.2]:TopTopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_2),product(x2,x0,e_2),product(x3,x0,e_2),product(e_1,x4,x5),product(e_2,e_1,x5),product(x0,x6,e_4),product(x7,x3,e_1) -> equalish(e_2,x0),equalish(x1,e_2),product(e_2,x2,e_3),equalish(x4,e_2),equalish(e_2,x6),equalish(x7,e_2) {x0 -> e_3, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_3, x5 -> e_2, x6 -> e_1, x7 -> e_1}
% 2.87/0.95 === Backtracking. Learning clause 155:18:8:[133.8,38.3,33.1,39.2]:TopTopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_2),product(x2,x0,e_2),product(x3,x0,e_2),product(e_1,e_3,x4),product(e_2,e_1,x4),product(x0,x5,e_4),group_element(x6),group_element(x3),product(e_2,x2,x7) -> equalish(e_2,x0),equalish(x1,e_2),equalish(e_2,x5),equalish(x6,e_2),product(x6,x3,e_2),product(x6,x3,e_3),product(x6,x3,e_4),equalish(x7,e_3)
% 2.87/0.95 === Conflict found: 111:5:1:[22.0,109.2,26.0,110.3,21.4,2.1,38.3]:Top: cycle(e_1,x0),greater(x0,e_0) -> product(e_1,e_1,e_2),product(e_1,e_1,e_3),product(e_1,e_1,e_4) {x0 -> e_3}
% 2.87/0.95 === Backtracking. Learning clause 157:6:1:[7.0,156.0,111.1,153.5,40.2]:Top: product(e_3,e_1,e_4),cycle(e_3,e_1),product(e_1,x0,e_2) -> product(e_1,e_1,e_3),product(e_1,e_1,e_4),equalish(x0,e_1)
% 2.87/0.95 === Backtracking. Learning clause 161:13:4:[22.0,158.2,24.0,159.3,7.0,160.4,42.3,41.1,38.6,23.1,42.1,154.1,38.5,42.1,111.3,153.5,86.3]:TopTopTopTop: product(x0,e_1,e_4),product(e_2,e_1,x1),product(e_3,e_1,e_4),cycle(e_3,e_1),product(e_3,x2,e_4),product(x3,e_1,e_3) -> equalish(e_2,x0),product(e_1,e_2,e_2),product(e_1,e_1,x1),product(e_1,e_3,e_2),product(e_1,e_1,e_3),product(e_1,e_1,e_4),equalish(x2,x3)
% 2.87/0.95 === Conflict found: 108:5:1:[22.0,107.1,38.6,86.1,86.1,86.1,86.1,38.3]:Top: group_element(x0) -> equalish(e_1,x0),product(x0,e_1,e_2),product(x0,e_1,e_3),product(x0,e_1,e_4) {x0 -> e_2}
% 2.87/0.95 === Backtracking. Learning clause 167:3:0:[7.0,162.0,26.0,163.3,29.0,164.4,41.1,165.6,32.0,166.7,108.5,41.1,23.1,41.1,111.3,153.5,161.2,30.1,157.3,157.3]:: product(e_3,e_1,e_4),cycle(e_3,e_1) -> product(e_1,e_1,e_3)
% 2.87/0.95 === Backtracking. Learning clause 168:4:1:[41.2,167.3]:Top: product(x0,e_1,e_3),product(e_3,e_1,e_4),cycle(e_3,e_1) -> equalish(x0,e_1)
% 2.87/0.95 === Backtracking. Learning clause 169:4:1:[42.1,167.3]:Top: product(e_1,e_3,x0),product(e_3,e_1,e_4),cycle(e_3,e_1) -> product(e_3,e_1,x0)
% 2.87/0.95 === Conflict found: 108:5:1:[22.0,107.1,38.6,86.1,86.1,86.1,86.1,38.3]:Top: group_element(x0) -> equalish(e_1,x0),product(x0,e_1,e_2),product(x0,e_1,e_3),product(x0,e_1,e_4) {x0 -> e_2}
% 2.87/0.95 === Backtracking. Learning clause 172:4:1:[23.0,170.0,26.0,171.5,108.5,41.1,86.1]:Top: product(x0,e_1,e_4),product(e_1,e_2,e_2) -> product(e_2,e_1,e_3),equalish(e_2,x0)
% 2.87/0.95 === Backtracking. Learning clause 178:3:0:[22.0,173.0,24.0,174.2,26.0,175.3,29.0,176.4,27.0,177.5,38.3,86.2,154.2,38.6,42.1,40.1,169.1,108.3,41.1,172.2,30.1,23.1,82.1,167.3,168.1,169.1,108.5]:: cycle(e_3,e_1) -> product(e_3,e_1,e_2),product(e_3,e_1,e_3)
% 2.87/0.95 === Backtracking. Learning clause 179:3:0:[41.1,178.3,33.1]:: product(e_2,e_1,e_3),cycle(e_3,e_1) -> product(e_3,e_1,e_2)
% 2.87/0.95 === Backtracking. Learning clause 180:5:2:[42.3,41.2,178.3]:TopTop: product(e_1,e_3,x0),product(x1,e_3,x0),cycle(e_3,e_1) -> equalish(x1,e_3),product(e_3,e_1,e_2)
% 2.87/0.95 === Backtracking. Learning clause 181:4:2:[38.4,86.1,42.2,86.1,86.1,23.1]:TopTop: product(x0,e_2,e_2),product(x1,e_2,e_2) -> product(e_2,x0,e_3),equalish(e_2,x1)
% 2.87/0.95 === Backtracking. Learning clause 182:4:5:[41.2,42.3]:TopTopTopTopTop: product(x0,x1,x2),product(x1,x3,x4),product(x3,x4,x2) -> equalish(x0,x4)
% 2.87/0.95
% 2.87/0.95 SZS status Unsatisfiable
% 2.87/0.95
% 2.87/0.95 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p
% 2.87/0.95
% 2.87/0.95 SPASS-SCL-FOL Statistics:
% 2.87/0.95 Number of learned clauses: 66
% 2.87/0.95 Number of propagations: 1654
% 2.87/0.95 Number of decisions: 311
% 2.87/0.95 Number of resolutions: 408
% 2.87/0.95 Number of condensations: 11
% 2.87/0.95 Number of sub resolutions: 74
% 2.87/0.95 Number of input literals (deduplicated): 47
% 2.87/0.95 Number of grows: 4
% 2.87/0.95 Number of considered ground atoms: 213
% 2.87/0.95
% 2.87/0.95 Needed: 0:00:00.56
% 2.87/0.95
%------------------------------------------------------------------------------