%------------------------------------------------------------------------------
% File : SPASS-SCL---0.1
% Problem : GRP130-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 : n011.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:07 PM UTC 2026
% Result : Satisfiable 152.03s 30.96s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : GRP130-2.005 : TPTP v9.2.1. Released v1.2.0.
% 0.11/0.13 % Command : /export/starexec/sandbox/solver/bin/execute.py 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.34 % Computer : n011.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:00:48 EDT 2026
% 0.17/0.34 % CPUTime :
% 0.17/0.34 SPASS-SCL-FOL version:
% 0.19/0.42 SPASS-SCL-FOL 0.1 (595c0c7b1) [parallel mode]
% 152.03/30.96 Starting: ./SPASS-SCL-FOL --heuristics_normal -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 152.03/30.96 Starting: ./SPASS-SCL-FOL --heuristics_resolution_1 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 152.03/30.96 Starting: ./SPASS-SCL-FOL --heuristics_resolution_2 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 152.03/30.96 Starting: ./SPASS-SCL-FOL --heuristics_resolution_3 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 152.03/30.96 Starting: ./SPASS-SCL-FOL --heuristics_lmodel_grow -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 152.03/30.96 Execution normal ended with status: satisfiable
% 152.03/30.96 Used heuristic: normal
% 152.03/30.96
% 152.03/30.96 Input Clauses:
% 152.03/30.96
% 152.03/30.96 Predicates: next greater product group_element equalish
% 152.03/30.96 Fol Constants: e_1 e_2 e_3 e_4 e_5
% 152.03/30.96 Fol Functions:
% 152.03/30.96 Problem Properties:
% 152.03/30.96 This is a Bernays Schoenfinkel problem.
% 152.03/30.96
% 152.03/30.96 After reduction: Problem Properties:
% 152.03/30.96 This is a Bernays Schoenfinkel problem.
% 152.03/30.96
% 152.03/30.96
% 152.03/30.96 Reduced Input Clauses:
% 152.03/30.96
% 152.03/30.96 Most General Atoms: next(x0,x2) greater(x1,x2) group_element(x1) equalish(x0,x3) product(x3,x1,x0)
% 152.03/30.96
% 152.03/30.96 === Starting SPASS-SCL-FOL A Little Less Naive, considering 205 atoms initially, heuristics mode: normal ===
% 152.03/30.96
% 152.03/30.96 === Backtracking. Learning clause 47:12:7:[17.0,46.1,45.2,41.3,44.1,45.1,45.2,45.2,43.1,44.1]:TopTopTopTopTopTopTop: product(e_2,x0,x1),group_element(x1),product(x2,x0,e_2),product(e_2,e_4,e_2),product(e_2,x3,x1),product(e_2,x4,x1),product(e_2,x5,e_2),product(x6,x4,e_2) -> equalish(e_1,x2),product(e_5,x3,e_2),equalish(x1,x5),equalish(e_3,x6)
% 152.03/30.96 === Backtracking. Learning clause 49:11:2:[19.0,48.0,41.7,45.2,45.2,41.6]:TopTop: group_element(x0),group_element(x1) -> product(x0,e_4,e_1),product(x0,e_4,e_2),product(x0,e_4,e_4),product(e_5,x1,x0),product(e_3,x1,x0),product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_3),product(x0,x1,e_5)
% 152.03/30.96 === Backtracking. Learning clause 51:18:3:[16.0,50.1,45.3,44.2,41.5,45.1,43.2,49.8]:TopTopTop: product(e_1,x0,x1),group_element(x1),product(e_1,e_4,x2),group_element(x2),group_element(x0) -> equalish(x2,e_3),product(e_1,x1,e_1),product(e_1,x1,e_2),product(e_1,x1,e_5),equalish(x0,x1),product(x2,e_4,e_1),product(x2,e_4,e_2),product(x2,e_4,e_4),product(e_5,x0,x2),product(e_3,x0,x2),product(x2,x0,e_2),product(x2,x0,e_3),product(x2,x0,e_5)
% 152.03/30.96 === Backtracking. Learning clause 62:33:9:[18.0,52.0,20.0,53.3,16.0,54.6,17.0,55.7,22.0,56.19,30.0,57.27,26.0,58.28,28.0,59.30,44.1,60.32,21.0,61.36,45.3,44.1,41.6,41.4,44.1,43.2,43.1,45.2,49.11,43.2,41.5,43.1,43.1,51.16,45.1,45.1,45.2,43.1,44.2,41.7,45.1,45.2,45.2,45.2,45.2,44.1,43.1,44.1]:TopTopTopTopTopTopTopTopTop: group_element(x0),group_element(x1),product(e_1,e_4,e_2),product(e_1,x2,e_2),product(e_1,x3,e_2),product(e_1,x4,e_2),product(e_1,x5,e_2),product(x6,e_4,e_2),product(e_1,x7,e_2),product(x8,x1,e_2) -> equalish(e_4,x0),product(x0,e_1,e_1),product(x0,e_1,e_4),product(x0,e_1,e_5),equalish(x0,e_2),equalish(e_3,x1),product(e_5,x1,e_2),product(e_2,x1,e_1),product(e_2,x1,e_2),equalish(e_1,x1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),product(e_1,e_5,e_5),product(e_2,e_4,e_1),product(e_3,e_2,e_2),product(e_2,e_2,e_3),equalish(e_5,x2),product(e_3,x3,e_1),product(e_1,x4,e_1),product(e_4,x5,e_1),equalish(e_4,x6),equalish(e_1,x7),equalish(e_3,x8)
% 152.03/30.96 === Conflict found: 49:11:2:[19.0,48.0,41.7,45.2,45.2,41.6]:TopTop: group_element(x0),group_element(x1) -> product(x0,e_4,e_1),product(x0,e_4,e_2),product(x0,e_4,e_4),product(e_5,x1,x0),product(e_3,x1,x0),product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_3),product(x0,x1,e_5) {x0 -> e_2, x1 -> e_2}
% 152.03/30.96 === Backtracking. Learning clause 63:11:3:[49.5,42.2,45.1,43.2]:TopTopTop: group_element(x0),product(x0,e_4,x1),product(x0,x2,e_5) -> product(x0,e_4,e_1),product(x0,e_4,e_2),product(e_3,x0,x0),product(x0,x0,e_1),product(x0,x0,e_2),product(x0,x0,e_3),equalish(x1,e_4),equalish(x2,x0)
% 152.03/30.96 === Backtracking. Learning clause 66:15:3:[17.0,64.0,16.0,65.2,41.6,45.2,45.1,45.2,45.3,41.3,45.1,44.2,41.5,45.1,45.2,44.1]:TopTopTop: group_element(x0),product(e_2,e_2,x0),product(x0,x1,e_1),product(x2,e_2,e_5) -> product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),product(e_2,e_2,e_1),equalish(x0,e_2),product(x0,e_1,e_1),product(x0,e_1,e_4),product(x0,e_1,e_5),product(e_2,x1,x0),equalish(e_1,x2)
% 152.03/30.96 === Backtracking. Learning clause 74:14:0:[20.0,67.0,17.0,68.2,27.0,69.3,38.0,70.8,21.0,71.12,40.0,72.19,34.0,73.20,43.1,41.6,49.5,45.1,66.2,63.2]:: product(e_5,e_4,e_1) -> product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),product(e_5,e_1,e_1),product(e_5,e_1,e_4),product(e_5,e_1,e_5),product(e_2,e_4,e_1),product(e_2,e_4,e_2),product(e_3,e_2,e_2),product(e_2,e_2,e_1),product(e_2,e_2,e_2),product(e_2,e_2,e_3)
% 152.03/30.96 === Backtracking. Learning clause 75:15:1:[42.1,74.12]:Top: product(e_2,e_2,x0),product(e_5,e_4,e_1) -> equalish(e_1,x0),product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),product(e_5,e_1,e_1),product(e_5,e_1,e_4),product(e_5,e_1,e_5),product(e_2,e_4,e_1),product(e_2,e_4,e_2),product(e_3,e_2,e_2),product(e_2,e_2,e_2),product(e_2,e_2,e_3)
% 152.03/30.96 === Backtracking. Learning clause 79:13:0:[17.0,76.0,16.0,77.1,25.0,78.3,41.4,45.2,43.2,45.2,74.12]:: product(e_5,e_4,e_1) -> product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),product(e_5,e_1,e_1),product(e_5,e_1,e_4),product(e_5,e_1,e_5),product(e_2,e_4,e_1),product(e_2,e_4,e_2),product(e_3,e_2,e_2),product(e_2,e_2,e_2),product(e_2,e_2,e_3)
% 152.03/30.96 === Conflict found: 66:15:3:[17.0,64.0,16.0,65.2,41.6,45.2,45.1,45.2,45.3,41.3,45.1,44.2,41.5,45.1,45.2,44.1]:TopTopTop: group_element(x0),product(e_2,e_2,x0),product(x0,x1,e_1),product(x2,e_2,e_5) -> product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),product(e_2,e_2,e_1),equalish(x0,e_2),product(x0,e_1,e_1),product(x0,e_1,e_4),product(x0,e_1,e_5),product(e_2,x1,x0),equalish(e_1,x2) {x0 -> e_5, x1 -> e_4, x2 -> e_2}
% 152.03/30.96 === Backtracking. Learning clause 80:17:5:[66.14,43.1,42.1]:TopTopTopTopTop: group_element(x0),product(e_2,e_2,x0),product(x0,x1,e_1),product(x2,e_2,e_5),product(e_2,x3,x0),product(e_2,e_2,x4) -> product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),equalish(x0,e_2),product(x0,e_1,e_1),product(x0,e_1,e_4),product(x0,e_1,e_5),equalish(e_1,x2),equalish(x1,x3),equalish(e_1,x4)
% 152.03/30.96 === Backtracking. Learning clause 82:18:8:[17.0,81.0,41.7,43.2,43.2,45.2,45.2,45.2,44.2,44.2,41.4,44.1,42.2]:TopTopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_5),product(e_2,x2,e_3),product(e_2,x3,x0),product(e_2,x4,x0),group_element(x5),group_element(x4),product(x6,x4,e_3),product(e_2,x3,x7) -> equalish(x1,x0),equalish(x2,x0),equalish(x5,e_4),equalish(x5,e_1),product(x5,x4,e_1),product(x5,x4,e_4),product(x5,x4,e_5),equalish(x5,x6),equalish(x7,e_2)
% 152.03/30.96 === Backtracking. Learning clause 85:8:0:[17.0,83.0,16.0,84.1,41.4,45.1,45.1,45.2,45.2,45.2,45.3,41.3]:: -> product(e_2,e_2,e_1),product(e_4,e_1,e_1),product(e_5,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_2),product(e_2,e_1,e_3),product(e_2,e_1,e_4),product(e_2,e_1,e_5)
% 152.03/30.96 === Backtracking. Learning clause 86:12:3:[43.2,41.5,41.5]:TopTopTop: group_element(x1),group_element(x0),group_element(x2) -> equalish(x2,x1),product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_4),product(x0,x1,e_5),product(x0,x2,e_1),product(x0,x2,e_2),product(x0,x2,e_4),product(x0,x2,e_5)
% 152.03/30.96 === Backtracking. Learning clause 94:25:4:[17.0,87.1,18.0,88.4,16.0,89.7,29.0,90.10,25.0,91.12,22.0,92.24,30.0,93.31,45.3,45.2,86.11,45.1,45.1,43.1,43.2,45.1,43.1,41.5,44.1,85.5,82.3]:TopTopTopTop: product(e_2,e_4,x0),product(e_2,e_4,x1),group_element(x0),product(e_2,x2,e_5),group_element(x3) -> product(e_2,e_1,x0),product(e_2,e_2,e_5),product(e_2,e_2,x1),product(x0,e_1,e_1),product(x0,e_1,e_4),product(x0,e_1,e_5),equalish(x0,e_2),product(e_2,e_2,e_1),product(e_4,e_1,e_1),product(e_5,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),equalish(x2,e_3),equalish(x3,e_4),equalish(x3,e_1),product(x3,e_1,e_1),product(x3,e_1,e_4),product(x3,e_1,e_5),equalish(x3,e_2)
% 152.03/30.96 === Backtracking. Learning clause 96:14:2:[16.0,95.1,41.4,45.2,44.1,85.6]:TopTop: group_element(x0),product(x0,x1,e_1) -> product(x0,e_1,e_1),product(x0,e_1,e_4),product(x0,e_1,e_5),product(e_2,x1,x0),equalish(x0,e_2),product(e_2,e_2,e_1),product(e_4,e_1,e_1),product(e_5,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_2),product(e_2,e_1,e_4),product(e_2,e_1,e_5)
% 152.03/30.96 === Backtracking. Learning clause 98:13:4:[18.0,97.0,45.1,41.5,86.8,45.2,44.2]:TopTopTopTop: group_element(x0),group_element(x1),product(x0,x2,x1),product(x3,x2,x0) -> product(e_5,x1,x0),equalish(x1,e_3),product(x0,e_3,e_1),product(x0,e_3,e_2),product(x0,e_3,e_4),product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_5),equalish(x3,e_4)
% 152.03/30.96 === Conflict found: 86:12:3:[43.2,41.5,41.5]:TopTopTop: group_element(x1),group_element(x0),group_element(x2) -> equalish(x2,x1),product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_4),product(x0,x1,e_5),product(x0,x2,e_1),product(x0,x2,e_2),product(x0,x2,e_4),product(x0,x2,e_5) {x0 -> e_2, x1 -> e_2, x2 -> e_4}
% 152.03/30.96 === Backtracking. Learning clause 111:18:1:[19.0,99.0,17.0,100.1,20.0,101.3,34.0,102.5,44.1,103.6,31.0,104.8,26.0,105.9,27.0,106.10,22.0,107.11,25.0,108.12,38.0,109.16,35.0,110.23,86.11,43.2,43.1,98.9,45.1,43.2,45.1,43.1,96.12,94.1]:Top: product(e_5,e_4,e_1),group_element(x0) -> product(e_2,e_4,e_2),product(e_2,e_2,e_5),product(e_5,e_1,e_4),product(e_5,e_1,e_5),product(e_2,e_2,e_1),product(e_4,e_1,e_1),product(e_5,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),equalish(x0,e_4),equalish(x0,e_1),product(x0,e_1,e_1),product(x0,e_1,e_4),product(x0,e_1,e_5),equalish(x0,e_2)
% 152.03/30.96 === Backtracking. Learning clause 115:16:4:[17.0,112.0,18.0,113.2,30.0,114.18,41.3,43.2,82.3]:TopTopTopTop: product(e_2,x0,e_1),product(e_2,x1,e_5),group_element(x2),group_element(x3) -> product(e_2,x3,e_2),product(e_2,x3,e_4),product(e_2,x3,e_5),equalish(x0,x3),equalish(x1,e_3),equalish(x3,e_3),equalish(x2,e_4),equalish(x2,e_1),product(x2,x3,e_1),product(x2,x3,e_4),product(x2,x3,e_5),equalish(x2,e_2)
% 152.03/30.96 === Backtracking. Learning clause 116:9:4:[41.5,44.1,45.2]:TopTopTopTop: group_element(x0),group_element(x1),product(x2,x1,e_3),product(x0,x3,x1) -> product(x0,x1,e_1),product(x0,x1,e_4),product(x0,x1,e_5),equalish(x0,x2),product(e_2,x3,x0)
% 152.03/30.96 === Backtracking. Learning clause 120:40:5:[17.0,117.0,20.0,118.1,38.0,119.15,41.3,43.2,116.3,115.2,111.7]:TopTopTopTopTop: group_element(x0),product(e_5,x1,x0),group_element(x2),group_element(x3),product(e_5,e_4,e_1),group_element(x4) -> product(e_2,x0,e_2),product(e_2,x0,e_4),product(e_2,x0,e_5),equalish(e_2,x0),product(e_5,x0,e_1),product(e_5,x0,e_4),product(e_5,x0,e_5),product(e_2,x3,e_2),product(e_2,x3,e_4),product(e_2,x3,e_5),equalish(e_2,x3),equalish(x1,e_3),equalish(x3,e_3),equalish(x2,e_4),equalish(x2,e_1),product(x2,x3,e_1),product(x2,x3,e_4),product(x2,x3,e_5),equalish(x2,e_2),product(e_2,e_4,e_2),product(e_2,e_2,e_5),product(e_5,e_1,e_4),product(e_5,e_1,e_5),product(e_4,e_1,e_1),product(e_5,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),equalish(x4,e_4),equalish(x4,e_1),product(x4,e_1,e_1),product(x4,e_1,e_4),product(x4,e_1,e_5),equalish(x4,e_2)
% 152.03/30.96 === Backtracking. Learning clause 133:12:3:[16.0,121.1,20.0,122.3,17.0,123.6,25.0,124.7,22.0,125.9,40.0,126.10,37.0,127.11,38.0,128.16,24.0,129.19,21.0,130.21,27.0,131.22,30.0,132.23,45.3,43.1,111.7,120.7,80.2,45.2,42.1,45.1,47.1,42.1]:TopTopTop: product(e_5,x0,e_1),product(e_5,e_4,e_1),product(e_5,x1,e_1),product(e_5,e_4,x2) -> equalish(x0,e_3),product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_2,e_1,e_4),product(e_2,e_1,e_5),product(e_5,e_1,e_1),equalish(x1,e_2),product(x2,e_1,e_5)
% 152.03/30.96 === Backtracking. Learning clause 134:12:3:[45.3,45.1,86.11]:TopTopTop: product(x0,e_4,x1),group_element(x2),group_element(x0) -> product(x0,x0,x1),equalish(x0,x2),product(x0,x2,e_1),product(x0,x2,e_2),product(x0,x2,e_4),product(x0,x2,e_5),product(x0,x0,e_1),product(x0,x0,e_2),product(x0,x0,e_5)
% 152.03/30.96 === Backtracking. Learning clause 135:4:5:[44.2,45.3]:TopTopTopTopTop: product(x0,x1,x2),product(x2,x1,x3),product(x2,x3,x4) -> equalish(x0,x4)
% 152.03/30.96 === Conflict found: 86:12:3:[43.2,41.5,41.5]:TopTopTop: group_element(x1),group_element(x0),group_element(x2) -> equalish(x2,x1),product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_4),product(x0,x1,e_5),product(x0,x2,e_1),product(x0,x2,e_2),product(x0,x2,e_4),product(x0,x2,e_5) {x0 -> e_2, x1 -> e_1, x2 -> e_2}
% 152.03/30.96 === Backtracking. Learning clause 136:15:6:[86.12,43.2,45.1,43.1]:TopTopTopTopTopTop: group_element(x0),group_element(x1),group_element(x2),product(x1,x3,e_5),product(x1,e_4,x4),product(x4,x5,x1) -> equalish(x2,x0),product(x1,x0,e_1),product(x1,x0,e_2),product(x1,x0,e_4),product(x1,x0,e_5),product(x1,x2,e_1),product(x1,x2,e_2),equalish(x3,x2),equalish(x2,x5)
% 152.03/30.96 === Conflict found: 134:12:3:[45.3,45.1,86.11]:TopTopTop: product(x0,e_4,x1),group_element(x2),group_element(x0) -> product(x0,x0,x1),equalish(x0,x2),product(x0,x2,e_1),product(x0,x2,e_2),product(x0,x2,e_4),product(x0,x2,e_5),product(x0,x0,e_1),product(x0,x0,e_2),product(x0,x0,e_5) {x0 -> e_2, x1 -> e_5, x2 -> e_1}
% 152.03/30.96 === Backtracking. Learning clause 137:12:3:[134.4,43.2]:TopTopTop: product(x0,e_4,e_5),group_element(x1),group_element(x0),product(x0,x2,e_5) -> equalish(x0,x1),product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_4),product(x0,x1,e_5),product(x0,x0,e_1),product(x0,x0,e_2),equalish(x2,x0)
% 152.03/30.96 === Conflict found: 136:15:6:[86.12,43.2,45.1,43.1]:TopTopTopTopTopTop: group_element(x0),group_element(x1),group_element(x2),product(x1,x3,e_5),product(x1,e_4,x4),product(x4,x5,x1) -> equalish(x2,x0),product(x1,x0,e_1),product(x1,x0,e_2),product(x1,x0,e_4),product(x1,x0,e_5),product(x1,x2,e_1),product(x1,x2,e_2),equalish(x3,x2),equalish(x2,x5) {x0 -> e_1, x1 -> e_2, x2 -> e_3, x3 -> e_4, x4 -> e_5, x5 -> e_1}
% 152.03/30.96 === Backtracking. Learning clause 138:18:9:[136.12,135.3,45.2]:TopTopTopTopTopTopTopTopTop: group_element(x0),group_element(x1),group_element(x2),product(x1,x3,e_5),product(x1,e_4,x4),product(x4,x5,x1),product(x6,x7,x1),product(x1,x7,x2),product(x1,x8,x2) -> equalish(x2,x0),product(x1,x0,e_1),product(x1,x0,e_2),product(x1,x0,e_4),product(x1,x0,e_5),equalish(x3,x2),equalish(x2,x5),equalish(x6,e_1),product(e_2,x8,x1)
% 152.03/30.96 === Backtracking. Learning clause 152:41:10:[19.0,139.0,20.0,140.4,16.0,141.5,17.0,142.15,42.0,143.18,36.0,144.26,35.0,145.33,45.0,146.36,42.1,147.37,34.0,148.39,23.0,149.50,45.1,150.52,45.1,151.53,41.6,45.2,116.3,45.1,45.1,45.2,45.3,136.8,43.2,43.2,41.3,42.2,45.2,42.1,49.6,135.2,21.1,42.1,135.1,24.1,43.2,43.2,45.3,133.1,136.6,45.3,135.1,86.7]:TopTopTopTopTopTopTopTopTopTop: product(e_2,x0,e_5),product(e_2,x1,e_2),product(e_2,e_4,x2),product(x3,e_4,e_5),product(e_2,e_2,x4),product(e_2,x4,x5),group_element(x6),group_element(x7),product(e_2,x8,e_5),product(e_2,e_4,e_5),product(e_2,e_1,x9),group_element(x9) -> product(e_2,e_2,e_4),product(e_2,e_2,e_1),product(e_2,e_1,e_2),equalish(x0,e_1),equalish(e_1,x9),equalish(x1,e_5),product(e_1,e_1,e_3),product(e_1,e_1,e_4),equalish(x2,e_1),product(e_3,e_1,e_5),product(e_5,e_1,e_2),product(e_5,e_1,e_3),equalish(x3,e_4),equalish(e_4,x5),equalish(x9,e_5),product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_5,e_1,e_1),product(e_1,e_1,e_5),equalish(x7,x6),product(e_2,x6,e_1),product(e_2,x6,e_2),product(e_2,x6,e_4),product(e_2,x6,e_5),product(e_2,x7,e_1),product(e_2,x7,e_2),equalish(x8,x7),equalish(x7,e_4),product(e_2,x9,e_1)
% 152.03/30.96 === Backtracking. Learning clause 158:37:9:[16.0,153.0,17.0,154.8,28.0,155.17,34.0,156.22,37.0,157.40,41.4,45.1,45.2,45.1,45.2,45.2,45.3,152.37,44.1,45.2,135.2,137.11,138.6,42.2]:TopTopTopTopTopTopTopTopTop: product(e_2,x0,e_5),product(x1,e_4,e_5),product(e_2,x2,e_5),product(e_2,e_1,x3),group_element(x3),product(x4,e_1,e_3),group_element(x5),group_element(x6),product(e_2,x7,e_5),product(e_2,e_4,e_5),product(e_2,e_1,x6),product(e_2,x5,x8) -> product(e_2,e_1,e_2),equalish(x0,e_1),equalish(e_1,x3),product(e_1,e_1,e_3),product(e_1,e_1,e_4),product(e_3,e_1,e_5),equalish(x1,e_4),equalish(x3,e_5),product(e_4,e_1,e_1),product(e_3,e_1,e_1),product(e_5,e_1,e_1),product(e_1,e_1,e_5),equalish(x3,x5),equalish(x2,x3),equalish(x3,e_4),equalish(e_5,x4),equalish(e_2,x5),product(e_2,e_2,e_1),equalish(x6,x5),product(e_2,x5,e_2),product(e_2,x5,e_4),product(e_2,x5,e_5),equalish(x7,x6),equalish(x6,e_1),equalish(x8,e_1)
% 152.03/30.96 === Conflict found: 82:18:8:[17.0,81.0,41.7,43.2,43.2,45.2,45.2,45.2,44.2,44.2,41.4,44.1,42.2]:TopTopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_5),product(e_2,x2,e_3),product(e_2,x3,x0),product(e_2,x4,x0),group_element(x5),group_element(x4),product(x6,x4,e_3),product(e_2,x3,x7) -> equalish(x1,x0),equalish(x2,x0),equalish(x5,e_4),equalish(x5,e_1),product(x5,x4,e_1),product(x5,x4,e_4),product(x5,x4,e_5),equalish(x5,x6),equalish(x7,e_2) {x0 -> e_3, x1 -> e_2, x2 -> e_1, x3 -> e_1, x4 -> e_1, x5 -> e_5, x6 -> e_2, x7 -> e_3}
% 152.03/30.96 === Backtracking. Learning clause 160:30:12:[17.0,159.11,82.16,42.2,42.2,86.12,42.2]:TopTopTopTopTopTopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_3),product(e_2,x2,x0),product(e_2,x3,x0),group_element(x4),group_element(x3),product(x5,x3,e_3),product(e_2,x2,x6),product(x4,x3,x7),product(x4,x3,x8),group_element(x9),group_element(x10),product(e_2,x9,x11) -> equalish(x10,x0),equalish(x1,x0),equalish(x4,e_4),equalish(x4,e_1),product(x4,x3,e_1),equalish(x4,x5),equalish(x6,e_2),equalish(x7,e_5),equalish(x8,e_4),equalish(x10,x9),product(e_2,x9,e_2),product(e_2,x9,e_4),product(e_2,x9,e_5),product(e_2,x10,e_1),product(e_2,x10,e_2),product(e_2,x10,e_4),equalish(x11,e_1)
% 152.03/30.96 === Conflict found: 160:30:12:[17.0,159.11,82.16,42.2,42.2,86.12,42.2]:TopTopTopTopTopTopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_3),product(e_2,x2,x0),product(e_2,x3,x0),group_element(x4),group_element(x3),product(x5,x3,e_3),product(e_2,x2,x6),product(x4,x3,x7),product(x4,x3,x8),group_element(x9),group_element(x10),product(e_2,x9,x11) -> equalish(x10,x0),equalish(x1,x0),equalish(x4,e_4),equalish(x4,e_1),product(x4,x3,e_1),equalish(x4,x5),equalish(x6,e_2),equalish(x7,e_5),equalish(x8,e_4),equalish(x10,x9),product(e_2,x9,e_2),product(e_2,x9,e_4),product(e_2,x9,e_5),product(e_2,x10,e_1),product(e_2,x10,e_2),product(e_2,x10,e_4),equalish(x11,e_1) {x0 -> e_3, x1 -> e_1, x2 -> e_1, x3 -> e_1, x4 -> e_5, x5 -> e_2, x6 -> e_3, x7 -> e_2, x8 -> e_2, x9 -> e_1, x10 -> e_4, x11 -> e_3}
% 152.03/30.96 === Backtracking. Learning clause 165:54:22:[19.0,161.11,17.0,162.24,27.0,163.40,36.0,164.41,160.28,135.1,134.1,43.2,42.2,42.2,160.29]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: group_element(x0),product(e_2,x1,e_3),product(e_2,x2,x0),product(e_2,x3,x0),group_element(x4),group_element(x3),product(x5,x3,e_3),product(e_2,x2,x6),product(x4,x3,x7),product(x4,x3,x8),group_element(x9),product(e_2,x9,x10),group_element(x11),product(e_2,x12,e_3),product(e_2,x13,x11),product(e_2,x14,x11),group_element(x15),group_element(x14),product(x16,x14,e_3),product(e_2,x13,x17),product(x15,x14,x18),product(x15,x14,x19),group_element(x20),product(e_2,x20,x21) -> equalish(e_4,x0),equalish(x1,x0),equalish(x4,e_4),equalish(x4,e_1),product(x4,x3,e_1),equalish(x4,x5),equalish(x6,e_2),equalish(x7,e_5),equalish(x8,e_4),equalish(e_4,x9),product(e_2,x9,e_2),product(e_2,x9,e_4),product(e_2,x9,e_5),equalish(x10,e_1),equalish(e_2,x11),equalish(x12,x11),equalish(x15,e_4),equalish(x15,e_1),product(x15,x14,e_1),equalish(x15,x16),equalish(x17,e_2),equalish(x18,e_5),equalish(x19,e_4),equalish(e_2,x20),product(e_2,x20,e_2),product(e_2,x20,e_4),product(e_2,x20,e_5),product(e_2,e_2,e_1),product(e_2,e_2,e_2),equalish(x21,e_1)
% 152.03/30.96 === Backtracking. Learning clause 167:10:4:[19.0,166.0,41.5,135.3,135.1,135.3,45.3]:TopTopTopTop: group_element(x0),product(x1,e_4,e_4),product(x2,e_4,e_4),product(x0,e_4,x3),product(x0,x3,e_4) -> product(e_4,x0,e_2),product(e_4,x0,e_5),equalish(x1,e_3),equalish(e_4,x0),equalish(x2,e_1)
% 152.03/30.96 === Backtracking. Learning clause 173:45:18:[19.0,168.15,17.0,169.16,26.0,170.44,34.0,171.45,25.0,172.46,45.3,45.2,160.29,43.1,86.9,167.2,135.1,44.2,43.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: product(e_1,x0,x1),group_element(x2),product(e_2,x3,e_3),product(e_2,x4,x2),product(e_2,x5,x2),group_element(x6),group_element(x5),product(x7,x5,e_3),product(e_2,x4,x8),product(x6,x5,x9),product(x6,x5,x10),group_element(x11),group_element(x1),product(e_2,x11,x12),group_element(x13),product(e_2,e_2,x14),product(e_2,x14,x15),product(x16,e_2,e_5),product(e_2,x17,e_2) -> product(e_2,x0,e_1),equalish(x1,x2),equalish(x3,x2),equalish(x6,e_4),equalish(x6,e_1),product(x6,x5,e_1),equalish(x6,x7),equalish(x8,e_2),equalish(x9,e_5),equalish(x10,e_4),equalish(x1,x11),product(e_2,x11,e_2),product(e_2,x11,e_4),product(e_2,x11,e_5),equalish(x12,e_1),equalish(x1,e_4),equalish(e_4,x13),product(e_2,x13,e_1),product(e_2,x13,e_2),product(e_2,x13,e_4),product(e_2,x13,e_5),product(e_2,e_4,e_2),product(e_2,e_4,e_5),equalish(e_4,x15),equalish(x16,e_4),equalish(x17,x1)
% 152.03/30.96 === Conflict found: 135:4:5:[44.2,45.3]:TopTopTopTopTop: product(x0,x1,x2),product(x2,x1,x3),product(x2,x3,x4) -> equalish(x0,x4) {x0 -> e_2, x1 -> e_4, x2 -> e_4, x3 -> e_2, x4 -> e_5}
% 152.03/30.96 === Backtracking. Learning clause 174:15:9:[135.2,45.3,167.7,135.1]:TopTopTopTopTopTopTopTopTop: product(x0,x1,e_4),product(x2,x1,x3),product(x2,x3,e_4),group_element(x2),product(x4,e_4,e_4),product(x5,e_4,e_4),product(x2,e_4,x6),product(x2,x6,e_4),product(e_2,x2,x7),product(e_2,x7,x8) -> equalish(x0,e_5),equalish(x4,e_3),equalish(e_4,x2),equalish(x5,e_1),equalish(e_4,x8)
% 152.03/30.96 === Conflict found: 173:45:18:[19.0,168.15,17.0,169.16,26.0,170.44,34.0,171.45,25.0,172.46,45.3,45.2,160.29,43.1,86.9,167.2,135.1,44.2,43.2]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: product(e_1,x0,x1),group_element(x2),product(e_2,x3,e_3),product(e_2,x4,x2),product(e_2,x5,x2),group_element(x6),group_element(x5),product(x7,x5,e_3),product(e_2,x4,x8),product(x6,x5,x9),product(x6,x5,x10),group_element(x11),group_element(x1),product(e_2,x11,x12),group_element(x13),product(e_2,e_2,x14),product(e_2,x14,x15),product(x16,e_2,e_5),product(e_2,x17,e_2) -> product(e_2,x0,e_1),equalish(x1,x2),equalish(x3,x2),equalish(x6,e_4),equalish(x6,e_1),product(x6,x5,e_1),equalish(x6,x7),equalish(x8,e_2),equalish(x9,e_5),equalish(x10,e_4),equalish(x1,x11),product(e_2,x11,e_2),product(e_2,x11,e_4),product(e_2,x11,e_5),equalish(x12,e_1),equalish(x1,e_4),equalish(e_4,x13),product(e_2,x13,e_1),product(e_2,x13,e_2),product(e_2,x13,e_4),product(e_2,x13,e_5),product(e_2,e_4,e_2),product(e_2,e_4,e_5),equalish(e_4,x15),equalish(x16,e_4),equalish(x17,x1) {x0 -> e_2, x1 -> e_5, x2 -> e_3, x3 -> e_1, x4 -> e_1, x5 -> e_1, x6 -> e_5, x7 -> e_2, x8 -> e_3, x9 -> e_2, x10 -> e_2, x11 -> e_1, x12 -> e_3, x13 -> e_1, x14 -> e_2, x15 -> e_2, x16 -> e_1, x17 -> e_2}
% 152.03/30.96 === Backtracking. Learning clause 175:46:19:[173.41,43.1]:TopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTopTop: product(e_1,x0,x1),group_element(x2),product(e_2,x3,e_3),product(e_2,x4,x2),product(e_2,x5,x2),group_element(x6),group_element(x5),product(x7,x5,e_3),product(e_2,x4,x8),product(x6,x5,x9),product(x6,x5,x10),group_element(x11),group_element(x1),product(e_2,x11,x12),group_element(x13),product(e_2,e_2,x14),product(e_2,x14,x15),product(x16,e_2,e_5),product(e_2,x17,e_2),product(e_2,x18,e_2) -> product(e_2,x0,e_1),equalish(x1,x2),equalish(x3,x2),equalish(x6,e_4),equalish(x6,e_1),product(x6,x5,e_1),equalish(x6,x7),equalish(x8,e_2),equalish(x9,e_5),equalish(x10,e_4),equalish(x1,x11),product(e_2,x11,e_2),product(e_2,x11,e_4),product(e_2,x11,e_5),equalish(x12,e_1),equalish(x1,e_4),equalish(e_4,x13),product(e_2,x13,e_1),product(e_2,x13,e_2),product(e_2,x13,e_4),product(e_2,x13,e_5),product(e_2,e_4,e_5),equalish(e_4,x15),equalish(x16,e_4),equalish(x17,x1),equalish(e_4,x18)
% 152.03/30.96 === Conflict found: 49:11:2:[19.0,48.0,41.7,45.2,45.2,41.6]:TopTop: group_element(x0),group_element(x1) -> product(x0,e_4,e_1),product(x0,e_4,e_2),product(x0,e_4,e_4),product(e_5,x1,x0),product(e_3,x1,x0),product(x0,x1,e_1),product(x0,x1,e_2),product(x0,x1,e_3),product(x0,x1,e_5) {x0 -> e_4, x1 -> e_2}
% 152.03/30.96 === Backtracking. Learning clause 179:9:2:[19.0,176.1,35.0,177.5,40.0,178.7,49.3,44.2,44.2,43.2,44.1,41.6]:TopTop: product(x0,e_4,e_1),group_element(x1) -> product(e_4,e_4,e_2),equalish(x0,e_4),equalish(x1,e_4),product(e_4,x1,e_1),product(e_4,x1,e_2),product(e_4,x1,e_3),product(e_4,x1,e_5)
% 152.03/30.96
% 152.03/30.96 Linear Model Building succeeded.
% 152.03/30.96 SZS status Satisfiable
% 152.03/30.96
% 152.03/30.96 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p
% 152.03/30.96
% 152.03/30.96 SPASS-SCL-FOL Statistics:
% 152.03/30.96 Number of learned clauses: 35
% 152.03/30.96 Number of propagations: 870
% 152.03/30.96 Number of decisions: 88
% 152.03/30.96 Number of resolutions: 212
% 152.03/30.96 Number of condensations: 6
% 152.03/30.96 Number of sub resolutions: 99
% 152.03/30.96 Number of input literals (deduplicated): 50
% 152.03/30.96 Number of grows: 0
% 152.03/30.96 Number of considered ground atoms: 205
% 152.03/30.96
% 152.03/30.96 Needed: 0:0:30.44
% 152.03/30.96
%------------------------------------------------------------------------------