%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP124-8.004 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n004.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 : 600s % DateTime : Sat Jul 16 11:45:33 EDT 2022 % Result : Unsatisfiable 0.56s 0.74s % Output : Refutation 0.56s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP124-8.004 : TPTP v8.1.0. Released v1.2.0. % 0.03/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n004.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon Jun 13 23:21:54 EDT 2022 % 0.13/0.35 % CPUTime : % 0.56/0.74 % 0.56/0.74 SPASS V 3.9 % 0.56/0.74 SPASS beiseite: Proof found. % 0.56/0.74 % SZS status Theorem % 0.56/0.74 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.56/0.74 SPASS derived 1645 clauses, backtracked 1168 clauses, performed 71 splits and kept 1975 clauses. % 0.56/0.74 SPASS allocated 76959 KBytes. % 0.56/0.74 SPASS spent 0:00:00.38 on the problem. % 0.56/0.74 0:00:00.04 for the input. % 0.56/0.74 0:00:00.00 for the FLOTTER CNF translation. % 0.56/0.74 0:00:00.03 for inferences. % 0.56/0.74 0:00:00.01 for the backtracking. % 0.56/0.74 0:00:00.27 for the reduction. % 0.56/0.74 % 0.56/0.74 % 0.56/0.74 Here is a proof with depth 14, length 340 : % 0.56/0.74 % SZS output start Refutation % 0.56/0.74 1[0:Inp] || -> next(e_0,e_1)*. % 0.56/0.74 2[0:Inp] || -> next(e_1,e_2)*. % 0.56/0.74 3[0:Inp] || -> next(e_2,e_3)*. % 0.56/0.74 4[0:Inp] || -> next(e_3,e_4)*. % 0.56/0.74 5[0:Inp] || -> greater(e_1,e_0)*. % 0.56/0.74 6[0:Inp] || -> greater(e_2,e_0)*. % 0.56/0.74 7[0:Inp] || -> greater(e_3,e_0)*. % 0.56/0.74 9[0:Inp] || -> greater(e_2,e_1)*. % 0.56/0.74 12[0:Inp] || -> greater(e_3,e_2)*. % 0.56/0.74 15[0:Inp] || cycle(u,v)*+ cycle(u,w)* -> equalish(w,v)*. % 0.56/0.74 16[0:Inp] group_element(u) || -> cycle(u,e_3) cycle(u,e_2) cycle(u,e_1) cycle(u,e_0)*. % 0.56/0.74 17[0:Inp] || -> cycle(e_4,e_0)*. % 0.56/0.74 18[0:Inp] || next(u,v)*+ next(w,x)* cycle(x,u)* cycle(w,y)* greater(y,e_0) -> equalish(y,v)*. % 0.56/0.74 19[0:Inp] || greater(u,v)*+ greater(w,x)* next(w,y)* cycle(y,v)* cycle(x,u)* cycle(w,e_0) -> . % 0.56/0.74 22[0:Inp] || -> group_element(e_1)*. % 0.56/0.74 23[0:Inp] || -> group_element(e_2)*. % 0.56/0.74 24[0:Inp] || -> group_element(e_3)*. % 0.56/0.74 25[0:Inp] || -> group_element(e_4)*. % 0.56/0.74 26[0:Inp] || equalish(e_1,e_2)*+ -> . % 0.56/0.74 27[0:Inp] || equalish(e_1,e_3)*+ -> . % 0.56/0.74 28[0:Inp] || equalish(e_1,e_4)*+ -> . % 0.56/0.74 29[0:Inp] || equalish(e_2,e_1)*+ -> . % 0.56/0.74 30[0:Inp] || equalish(e_2,e_3)*+ -> . % 0.56/0.74 31[0:Inp] || equalish(e_2,e_4)*+ -> . % 0.56/0.74 32[0:Inp] || equalish(e_3,e_1)*+ -> . % 0.56/0.74 33[0:Inp] || equalish(e_3,e_2)*+ -> . % 0.56/0.74 34[0:Inp] || equalish(e_3,e_4)*+ -> . % 0.56/0.74 35[0:Inp] || equalish(e_4,e_1)*+ -> . % 0.56/0.74 36[0:Inp] || equalish(e_4,e_2)*+ -> . % 0.56/0.74 37[0:Inp] || equalish(e_4,e_3)*+ -> . % 0.56/0.74 38[0:Inp] group_element(u) group_element(v) || -> product1(v,u,e_4) product1(v,u,e_3) product1(v,u,e_2) product1(v,u,e_1)*. % 0.56/0.74 39[0:Inp] || product1(u,v,w)*+ product1(u,v,x)* -> equalish(x,w)*. % 0.56/0.74 40[0:Inp] || product1(u,v,w)*+ product1(u,x,w)* -> equalish(x,v)*. % 0.56/0.74 41[0:Inp] || product1(u,v,w)*+ product1(x,v,w)* -> equalish(x,u)*. % 0.56/0.74 42[0:Inp] || -> product1(u,u,u)*. % 0.56/0.74 43[0:Inp] group_element(u) group_element(v) || -> product2(v,u,e_4) product2(v,u,e_3) product2(v,u,e_2) product2(v,u,e_1)*. % 0.56/0.74 44[0:Inp] || product2(u,v,w)*+ product2(u,v,x)* -> equalish(x,w)*. % 0.56/0.74 45[0:Inp] || product2(u,v,w)*+ product2(u,x,w)* -> equalish(x,v)*. % 0.56/0.74 46[0:Inp] || product2(u,v,w)*+ product2(x,v,w)* -> equalish(x,u)*. % 0.56/0.74 47[0:Inp] || -> product2(u,u,u)*. % 0.56/0.74 48[0:Inp] || product1(u,v,w)*+ product1(v,x,u)* -> product2(w,x,v)*. % 0.56/0.74 59[0:Res:47.0,46.0] || product2(u,v,v)*+ -> equalish(u,v). % 0.56/0.74 61[0:Res:47.0,45.0] || product2(u,v,u)*+ -> equalish(v,u). % 0.56/0.74 63[0:Res:47.0,44.0] || product2(u,u,v)*+ -> equalish(v,u). % 0.56/0.74 65[0:Res:42.0,41.0] || product1(u,v,v)*+ -> equalish(u,v). % 0.56/0.74 67[0:Res:42.0,40.0] || product1(u,v,u)*+ -> equalish(v,u). % 0.56/0.74 77[0:Res:43.5,61.0] group_element(u) group_element(e_1) || -> product2(e_1,u,e_4) product2(e_1,u,e_3) product2(e_1,u,e_2)* equalish(u,e_1). % 0.56/0.74 85[0:SSi:77.1,22.0] group_element(u) || -> product2(e_1,u,e_4) product2(e_1,u,e_3) product2(e_1,u,e_2)* equalish(u,e_1). % 0.56/0.74 96[0:Res:38.5,67.0] group_element(u) group_element(e_1) || -> product1(e_1,u,e_4) product1(e_1,u,e_3) product1(e_1,u,e_2)* equalish(u,e_1). % 0.56/0.74 100[0:Res:38.5,48.0] group_element(u) group_element(v) || product1(u,w,v)*+ -> product1(v,u,e_4) product1(v,u,e_3) product1(v,u,e_2)* product2(e_1,w,u)*. % 0.56/0.74 103[0:Res:38.5,41.0] group_element(u) group_element(v) || product1(w,u,e_1)*+ -> product1(v,u,e_4) product1(v,u,e_3) product1(v,u,e_2)* equalish(w,v)*. % 0.56/0.74 104[0:Res:38.5,65.0] group_element(e_1) group_element(u) || -> product1(u,e_1,e_4) product1(u,e_1,e_3) product1(u,e_1,e_2)* equalish(u,e_1). % 0.56/0.74 105[0:SSi:104.0,22.0] group_element(u) || -> product1(u,e_1,e_4) product1(u,e_1,e_3) product1(u,e_1,e_2)* equalish(u,e_1). % 0.56/0.74 107[0:SSi:96.1,22.0] group_element(u) || -> product1(e_1,u,e_4) product1(e_1,u,e_3) product1(e_1,u,e_2)* equalish(u,e_1). % 0.56/0.74 121[0:Res:85.3,59.0] group_element(e_2) || -> product2(e_1,e_2,e_4) product2(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.56/0.74 123[0:SSi:121.0,23.0] || -> product2(e_1,e_2,e_4) product2(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.56/0.74 124[0:MRR:123.2,123.3,29.0,26.0] || -> product2(e_1,e_2,e_4) product2(e_1,e_2,e_3)*. % 0.56/0.74 127[0:Res:2.0,18.0] || next(u,v)*+ cycle(v,e_1) cycle(u,w)* greater(w,e_0) -> equalish(w,e_2)*. % 0.56/0.74 128[0:Res:1.0,18.0] || next(u,v)*+ cycle(v,e_0) cycle(u,w)* greater(w,e_0) -> equalish(w,e_1)*. % 0.56/0.74 129[0:Res:124.1,44.0] || product2(e_1,e_2,u)*+ -> product2(e_1,e_2,e_4)* equalish(u,e_3). % 0.56/0.74 132[1:Spt:129.0,129.2] || product2(e_1,e_2,u)*+ -> equalish(u,e_3). % 0.56/0.74 146[0:Res:7.0,19.0] || greater(u,v)*+ next(u,w)* cycle(w,e_0) cycle(v,e_3) cycle(u,e_0) -> . % 0.56/0.74 147[0:Res:9.0,19.0] || greater(u,v)*+ next(u,w)* cycle(w,e_1) cycle(v,e_2) cycle(u,e_0) -> . % 0.56/0.74 148[0:Res:6.0,19.0] || greater(u,v)*+ next(u,w)* cycle(w,e_0) cycle(v,e_2) cycle(u,e_0) -> . % 0.56/0.74 150[0:Res:105.3,67.0] group_element(e_2) || -> product1(e_2,e_1,e_4) product1(e_2,e_1,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.56/0.74 158[0:SSi:150.0,23.0] || -> product1(e_2,e_1,e_4) product1(e_2,e_1,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.56/0.74 159[0:MRR:158.2,158.3,29.0,26.0] || -> product1(e_2,e_1,e_4) product1(e_2,e_1,e_3)*. % 0.56/0.74 160[0:Res:159.1,48.0] || product1(e_1,u,e_2)+ -> product1(e_2,e_1,e_4) product2(e_3,u,e_1)*. % 0.56/0.74 161[0:Res:159.1,39.0] || product1(e_2,e_1,u)*+ -> product1(e_2,e_1,e_4)* equalish(u,e_3). % 0.56/0.74 163[0:Res:159.1,41.0] || product1(u,e_1,e_3)*+ -> product1(e_2,e_1,e_4)* equalish(u,e_2). % 0.56/0.74 164[2:Spt:161.0,161.2] || product1(e_2,e_1,u)*+ -> equalish(u,e_3). % 0.56/0.74 174[3:Spt:163.0,163.2] || product1(u,e_1,e_3)*+ -> equalish(u,e_2). % 0.56/0.74 176[4:Spt:160.1] || -> product1(e_2,e_1,e_4)*. % 0.56/0.74 181[4:Res:176.0,164.0] || -> equalish(e_4,e_3)*. % 0.56/0.74 182[4:MRR:181.0,37.0] || -> . % 0.56/0.74 183[4:Spt:182.0,160.1,176.0] || product1(e_2,e_1,e_4)*+ -> . % 0.56/0.74 184[4:Spt:182.0,160.0,160.2] || product1(e_1,u,e_2)+ -> product2(e_3,u,e_1)*. % 0.56/0.74 185[4:MRR:159.0,183.0] || -> product1(e_2,e_1,e_3)*. % 0.56/0.74 199[0:Res:3.0,127.0] || cycle(e_3,e_1)+ cycle(e_2,u) greater(u,e_0) -> equalish(u,e_2)*. % 0.56/0.74 202[0:Res:4.0,128.0] || cycle(e_4,e_0) cycle(e_3,u) greater(u,e_0) -> equalish(u,e_1)*. % 0.56/0.74 206[0:MRR:202.0,17.0] || cycle(e_3,u)+ greater(u,e_0) -> equalish(u,e_1)*. % 0.56/0.74 207[0:Res:16.4,206.0] group_element(e_3) || greater(e_0,e_0) -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1) equalish(e_0,e_1)*. % 0.56/0.74 208[0:SSi:207.0,24.0] || greater(e_0,e_0)+ -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1) equalish(e_0,e_1)*. % 0.56/0.74 232[0:Res:5.0,148.0] || next(e_1,u)*+ cycle(u,e_0) cycle(e_0,e_2) cycle(e_1,e_0) -> . % 0.56/0.74 246[0:Res:5.0,147.0] || next(e_1,u)*+ cycle(u,e_1) cycle(e_0,e_2) cycle(e_1,e_0) -> . % 0.56/0.74 255[0:Res:12.0,146.0] || next(e_3,u)* cycle(u,e_0) cycle(e_2,e_3) cycle(e_3,e_0) -> . % 0.56/0.74 363[5:Spt:208.1] || -> cycle(e_3,e_3)*. % 0.56/0.74 370[5:Res:363.0,206.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 0.56/0.74 371[5:MRR:370.0,370.1,7.0,32.0] || -> . % 0.56/0.74 372[5:Spt:371.0,208.1,363.0] || cycle(e_3,e_3)*+ -> . % 0.56/0.74 373[5:Spt:371.0,208.0,208.2,208.3,208.4] || greater(e_0,e_0)+ -> cycle(e_3,e_2) cycle(e_3,e_1) equalish(e_0,e_1)*. % 0.56/0.74 375[6:Spt:373.1] || -> cycle(e_3,e_2)*. % 0.56/0.74 381[6:Res:375.0,206.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 0.56/0.74 382[6:MRR:381.0,381.1,6.0,29.0] || -> . % 0.56/0.74 383[6:Spt:382.0,373.1,375.0] || cycle(e_3,e_2)*+ -> . % 0.56/0.74 384[6:Spt:382.0,373.0,373.2,373.3] || greater(e_0,e_0)+ -> cycle(e_3,e_1) equalish(e_0,e_1)*. % 0.56/0.74 408[0:Res:42.0,103.2] group_element(e_1) group_element(u) || -> product1(u,e_1,e_4) product1(u,e_1,e_3) product1(u,e_1,e_2)* equalish(e_1,u). % 0.56/0.74 410[0:SSi:408.0,22.0] group_element(u) || -> product1(u,e_1,e_4) product1(u,e_1,e_3) product1(u,e_1,e_2)* equalish(e_1,u). % 0.56/0.74 426[4:Res:185.0,100.2] group_element(e_2) group_element(e_3) || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3) product1(e_3,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 427[4:SSi:426.1,426.0,24.0,23.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3) product1(e_3,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 466[4:Res:427.3,63.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3) product1(e_3,e_2,e_2)* equalish(e_2,e_1). % 0.56/0.74 468[4:MRR:466.3,29.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3) product1(e_3,e_2,e_2)*. % 0.56/0.74 476[4:Res:468.2,65.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3)* equalish(e_3,e_2). % 0.56/0.74 478[4:MRR:476.2,33.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3)*. % 0.56/0.74 480[4:Res:478.1,67.0] || -> product1(e_3,e_2,e_4)* equalish(e_2,e_3). % 0.56/0.74 488[4:MRR:480.1,30.0] || -> product1(e_3,e_2,e_4)*. % 0.56/0.74 494[4:Res:488.0,40.0] || product1(e_3,u,e_4)*+ -> equalish(u,e_2). % 0.56/0.74 542[0:Res:2.0,232.0] || cycle(e_2,e_0)+ cycle(e_0,e_2)* cycle(e_1,e_0) -> . % 0.56/0.74 543[0:Res:2.0,246.0] || cycle(e_2,e_1)+ cycle(e_0,e_2)* cycle(e_1,e_0) -> . % 0.56/0.74 582[0:Res:107.3,65.0] group_element(e_2) || -> product1(e_1,e_2,e_4) product1(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.56/0.74 583[4:Res:107.3,184.0] group_element(u) || -> product1(e_1,u,e_4) product1(e_1,u,e_3) equalish(u,e_1) product2(e_3,u,e_1)*. % 0.56/0.74 585[0:SSi:582.0,23.0] || -> product1(e_1,e_2,e_4) product1(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.56/0.74 586[0:MRR:585.2,585.3,29.0,26.0] || -> product1(e_1,e_2,e_4) product1(e_1,e_2,e_3)*. % 0.56/0.74 592[0:Res:586.1,41.0] || product1(u,e_2,e_3)*+ -> product1(e_1,e_2,e_4)* equalish(u,e_1). % 0.56/0.74 712[4:Res:583.4,63.0] group_element(e_3) || -> product1(e_1,e_3,e_4) product1(e_1,e_3,e_3)* equalish(e_3,e_1) equalish(e_1,e_3). % 0.56/0.74 717[4:SSi:712.0,24.0] || -> product1(e_1,e_3,e_4) product1(e_1,e_3,e_3)* equalish(e_3,e_1) equalish(e_1,e_3). % 0.56/0.74 718[4:MRR:717.1,717.2,717.3,65.0,32.0,27.0] || -> product1(e_1,e_3,e_4)*. % 0.56/0.74 722[4:Res:718.0,100.2] group_element(e_1) group_element(e_4) || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product1(e_4,e_1,e_2) product2(e_1,e_3,e_1)*. % 0.56/0.74 728[4:SSi:722.1,722.0,25.0,22.0] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product1(e_4,e_1,e_2) product2(e_1,e_3,e_1)*. % 0.56/0.74 747[4:Res:728.3,61.0] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product1(e_4,e_1,e_2)* equalish(e_3,e_1). % 0.56/0.74 754[4:MRR:747.3,32.0] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product1(e_4,e_1,e_2)*. % 0.56/0.74 773[4:Res:754.2,39.0] || product1(e_4,e_1,u)*+ -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)* equalish(u,e_2). % 0.56/0.74 775[4:Res:754.2,41.0] || product1(u,e_1,e_2)*+ -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)* equalish(u,e_4). % 0.56/0.74 779[7:Spt:773.0,773.3] || product1(e_4,e_1,u)*+ -> equalish(u,e_2). % 0.56/0.74 789[8:Spt:775.0,775.3] || product1(u,e_1,e_2)*+ -> equalish(u,e_4). % 0.56/0.74 790[8:Res:410.3,789.0] group_element(u) || -> product1(u,e_1,e_4) product1(u,e_1,e_3)* equalish(e_1,u) equalish(u,e_4). % 0.56/0.74 845[8:Res:790.2,67.0] group_element(e_3) || -> product1(e_3,e_1,e_4)* equalish(e_1,e_3) equalish(e_3,e_4) equalish(e_1,e_3). % 0.56/0.74 861[8:Obv:845.2] group_element(e_3) || -> product1(e_3,e_1,e_4)* equalish(e_3,e_4) equalish(e_1,e_3). % 0.56/0.74 862[8:SSi:861.0,24.0] || -> product1(e_3,e_1,e_4)* equalish(e_3,e_4) equalish(e_1,e_3). % 0.56/0.74 863[8:MRR:862.1,862.2,34.0,27.0] || -> product1(e_3,e_1,e_4)*. % 0.56/0.74 873[8:Res:863.0,494.0] || -> equalish(e_1,e_2)*. % 0.56/0.74 874[8:MRR:873.0,26.0] || -> . % 0.56/0.74 876[8:Spt:874.0,775.1,775.2] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)*. % 0.56/0.74 882[8:Res:876.1,174.0] || -> product1(e_4,e_1,e_4)* equalish(e_4,e_2). % 0.56/0.74 885[8:MRR:882.0,882.1,779.0,36.0] || -> . % 0.56/0.74 888[7:Spt:885.0,773.1,773.2] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)*. % 0.56/0.74 894[7:Res:888.1,174.0] || -> product1(e_4,e_1,e_4)* equalish(e_4,e_2). % 0.56/0.74 896[7:MRR:894.1,36.0] || -> product1(e_4,e_1,e_4)*. % 0.56/0.74 898[7:Res:896.0,67.0] || -> equalish(e_1,e_4)*. % 0.56/0.74 906[7:MRR:898.0,28.0] || -> . % 0.56/0.74 908[3:Spt:906.0,163.1] || -> product1(e_2,e_1,e_4)*. % 0.56/0.74 915[3:Res:908.0,164.0] || -> equalish(e_4,e_3)*. % 0.56/0.74 917[3:MRR:915.0,37.0] || -> . % 0.56/0.74 921[2:Spt:917.0,161.1] || -> product1(e_2,e_1,e_4)*. % 0.56/0.74 925[2:Res:921.0,100.2] group_element(e_2) group_element(e_4) || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 929[2:Res:921.0,41.0] || product1(u,e_1,e_4)*+ -> equalish(u,e_2). % 0.56/0.74 933[2:SSi:925.1,925.0,25.0,23.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 948[0:Res:16.4,542.0] group_element(e_2) || cycle(e_0,e_2)* cycle(e_1,e_0) -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1). % 0.56/0.74 949[0:SSi:948.0,23.0] || cycle(e_0,e_2)* cycle(e_1,e_0) -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1). % 0.56/0.74 950[0:MRR:949.4,543.0] || cycle(e_0,e_2)*+ cycle(e_1,e_0) -> cycle(e_2,e_3) cycle(e_2,e_2). % 0.56/0.74 963[3:Spt:592.0,592.2] || product1(u,e_2,e_3)*+ -> equalish(u,e_1). % 0.56/0.74 1004[2:Res:933.3,63.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2)* equalish(e_2,e_1). % 0.56/0.74 1006[2:MRR:1004.3,29.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2)*. % 0.56/0.74 1013[2:Res:1006.2,65.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3)* equalish(e_4,e_2). % 0.56/0.74 1015[2:MRR:1013.2,36.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3)*. % 0.56/0.74 1017[2:Res:1015.1,100.2] group_element(e_4) group_element(e_3) || -> product1(e_4,e_2,e_4) product1(e_3,e_4,e_4) product1(e_3,e_4,e_3) product1(e_3,e_4,e_2) product2(e_1,e_2,e_4)*. % 0.56/0.74 1022[3:Res:1015.1,963.0] || -> product1(e_4,e_2,e_4)* equalish(e_4,e_1). % 0.56/0.74 1024[3:MRR:1022.1,35.0] || -> product1(e_4,e_2,e_4)*. % 0.56/0.74 1026[3:Res:1024.0,67.0] || -> equalish(e_2,e_4)*. % 0.56/0.74 1034[3:MRR:1026.0,31.0] || -> . % 0.56/0.74 1036[3:Spt:1034.0,592.1] || -> product1(e_1,e_2,e_4)*. % 0.56/0.74 1037[2:SSi:1017.1,1017.0,24.0,25.0] || -> product1(e_4,e_2,e_4) product1(e_3,e_4,e_4) product1(e_3,e_4,e_3) product1(e_3,e_4,e_2) product2(e_1,e_2,e_4)*. % 0.56/0.74 1046[4:Spt:1015.0] || -> product1(e_4,e_2,e_4)*. % 0.56/0.74 1047[4:Res:1046.0,67.0] || -> equalish(e_2,e_4)*. % 0.56/0.74 1055[4:MRR:1047.0,31.0] || -> . % 0.56/0.74 1057[4:Spt:1055.0,1015.0,1046.0] || product1(e_4,e_2,e_4)*+ -> . % 0.56/0.74 1058[4:Spt:1055.0,1015.1] || -> product1(e_4,e_2,e_3)*. % 0.56/0.74 1063[4:MRR:1037.0,1057.0] || -> product1(e_3,e_4,e_4) product1(e_3,e_4,e_3) product1(e_3,e_4,e_2) product2(e_1,e_2,e_4)*. % 0.56/0.74 1158[4:Res:1063.3,132.0] || -> product1(e_3,e_4,e_4) product1(e_3,e_4,e_3) product1(e_3,e_4,e_2)* equalish(e_4,e_3). % 0.56/0.74 1159[4:MRR:1158.1,1158.3,67.0,37.0] || -> product1(e_3,e_4,e_4) product1(e_3,e_4,e_2)*. % 0.56/0.74 1162[4:Res:1159.1,39.0] || product1(e_3,e_4,u)*+ -> product1(e_3,e_4,e_4)* equalish(u,e_2). % 0.56/0.74 1163[4:Res:1159.1,40.0] || product1(e_3,u,e_2)*+ -> product1(e_3,e_4,e_4)* equalish(u,e_4). % 0.56/0.74 1169[5:Spt:1162.0,1162.2] || product1(e_3,e_4,u)*+ -> equalish(u,e_2). % 0.56/0.74 1172[6:Spt:1163.0,1163.2] || product1(e_3,u,e_2)*+ -> equalish(u,e_4). % 0.56/0.74 1173[6:Res:410.3,1172.0] group_element(e_3) || -> product1(e_3,e_1,e_4) product1(e_3,e_1,e_3)* equalish(e_1,e_3) equalish(e_1,e_4). % 0.56/0.74 1178[6:SSi:1173.0,24.0] || -> product1(e_3,e_1,e_4) product1(e_3,e_1,e_3)* equalish(e_1,e_3) equalish(e_1,e_4). % 0.56/0.74 1179[6:MRR:1178.1,1178.2,1178.3,67.0,27.0,28.0] || -> product1(e_3,e_1,e_4)*. % 0.56/0.74 1185[6:Res:1179.0,929.0] || -> equalish(e_3,e_2)*. % 0.56/0.74 1187[6:MRR:1185.0,33.0] || -> . % 0.56/0.74 1191[6:Spt:1187.0,1163.1] || -> product1(e_3,e_4,e_4)*. % 0.56/0.74 1199[6:Res:1191.0,1169.0] || -> equalish(e_4,e_2)*. % 0.56/0.74 1201[6:MRR:1199.0,36.0] || -> . % 0.56/0.74 1203[5:Spt:1201.0,1162.1] || -> product1(e_3,e_4,e_4)*. % 0.56/0.74 1209[5:Res:1203.0,65.0] || -> equalish(e_3,e_4)*. % 0.56/0.74 1211[5:MRR:1209.0,34.0] || -> . % 0.56/0.74 1213[1:Spt:1211.0,129.1] || -> product2(e_1,e_2,e_4)*. % 0.56/0.74 1214[1:Res:1213.0,44.0] || product2(e_1,e_2,u)*+ -> equalish(u,e_4). % 0.56/0.74 1218[2:Spt:586.0] || -> product1(e_1,e_2,e_4)*. % 0.56/0.74 1219[2:Res:1218.0,100.2] group_element(e_1) group_element(e_4) || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product1(e_4,e_1,e_2) product2(e_1,e_2,e_1)*. % 0.56/0.74 1223[2:Res:1218.0,41.0] || product1(u,e_2,e_4)*+ -> equalish(u,e_1). % 0.56/0.74 1225[2:SSi:1219.1,1219.0,25.0,22.0] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product1(e_4,e_1,e_2) product2(e_1,e_2,e_1)*. % 0.56/0.74 1227[3:Spt:159.0] || -> product1(e_2,e_1,e_4)*. % 0.56/0.74 1228[3:Res:1227.0,100.2] group_element(e_2) group_element(e_4) || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 1232[3:Res:1227.0,41.0] || product1(u,e_1,e_4)*+ -> equalish(u,e_2). % 0.56/0.74 1236[3:SSi:1228.1,1228.0,25.0,23.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 1269[4:Spt:950.2] || -> cycle(e_2,e_3)*. % 0.56/0.74 1276[4:MRR:255.2,1269.0] || next(e_3,u)*+ cycle(u,e_0) cycle(e_3,e_0) -> . % 0.56/0.74 1285[4:Res:4.0,1276.0] || cycle(e_4,e_0) cycle(e_3,e_0)* -> . % 0.56/0.74 1286[4:MRR:1285.0,17.0] || cycle(e_3,e_0)*+ -> . % 0.56/0.74 1287[4:Res:16.4,1286.0] group_element(e_3) || -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 0.56/0.74 1288[4:SSi:1287.0,24.0] || -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 0.56/0.74 1289[5:Spt:1288.0] || -> cycle(e_3,e_3)*. % 0.56/0.74 1293[5:Res:1289.0,206.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 0.56/0.74 1294[5:MRR:1293.0,1293.1,7.0,32.0] || -> . % 0.56/0.74 1295[5:Spt:1294.0,1288.0,1289.0] || cycle(e_3,e_3)*+ -> . % 0.56/0.74 1296[5:Spt:1294.0,1288.1,1288.2] || -> cycle(e_3,e_2) cycle(e_3,e_1)*. % 0.56/0.74 1299[5:Res:1296.1,15.0] || cycle(e_3,u)+ -> cycle(e_3,e_2) equalish(u,e_1)*. % 0.56/0.74 1301[5:Res:1296.1,199.0] || cycle(e_2,u)+ greater(u,e_0) -> cycle(e_3,e_2) equalish(u,e_2)*. % 0.56/0.74 1303[6:Spt:1299.0,1299.2] || cycle(e_3,u)+ -> equalish(u,e_1)*. % 0.56/0.74 1306[7:Spt:1301.0,1301.1,1301.3] || cycle(e_2,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 0.56/0.74 1308[7:Res:1269.0,1306.0] || greater(e_3,e_0) -> equalish(e_3,e_2)*. % 0.56/0.74 1309[7:MRR:1308.0,1308.1,7.0,33.0] || -> . % 0.56/0.74 1310[7:Spt:1309.0,1301.2] || -> cycle(e_3,e_2)*. % 0.56/0.74 1313[7:Res:1310.0,1303.0] || -> equalish(e_2,e_1)*. % 0.56/0.74 1314[7:MRR:1313.0,29.0] || -> . % 0.56/0.74 1315[6:Spt:1314.0,1299.1] || -> cycle(e_3,e_2)*. % 0.56/0.74 1321[6:Res:1315.0,206.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 0.56/0.74 1322[6:MRR:1321.0,1321.1,6.0,29.0] || -> . % 0.56/0.74 1323[4:Spt:1322.0,950.2,1269.0] || cycle(e_2,e_3)*+ -> . % 0.56/0.74 1324[4:Spt:1322.0,950.0,950.1,950.3] || cycle(e_0,e_2)*+ cycle(e_1,e_0) -> cycle(e_2,e_2). % 0.56/0.74 1368[2:Res:1225.3,61.0] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product1(e_4,e_1,e_2)* equalish(e_2,e_1). % 0.56/0.74 1376[2:MRR:1368.3,29.0] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product1(e_4,e_1,e_2)*. % 0.56/0.74 1378[2:Res:1376.2,48.0] || product1(e_1,u,e_4)+ -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3) product2(e_2,u,e_1)*. % 0.56/0.74 1379[2:Res:1376.2,39.0] || product1(e_4,e_1,u)*+ -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)* equalish(u,e_2). % 0.56/0.74 1388[3:Res:1236.3,63.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2)* equalish(e_2,e_1). % 0.56/0.74 1390[3:MRR:1388.3,29.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2)*. % 0.56/0.74 1397[3:Res:1390.2,65.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3)* equalish(e_4,e_2). % 0.56/0.74 1399[3:MRR:1397.2,36.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3)*. % 0.56/0.74 1404[3:Res:1399.1,39.0] || product1(e_4,e_2,u)*+ -> product1(e_4,e_2,e_4)* equalish(u,e_3). % 0.56/0.74 1405[3:Res:1399.1,40.0] || product1(e_4,u,e_3)*+ -> product1(e_4,e_2,e_4)* equalish(u,e_2). % 0.56/0.74 1409[5:Spt:1404.0,1404.2] || product1(e_4,e_2,u)*+ -> equalish(u,e_3). % 0.56/0.74 1412[6:Spt:1405.0,1405.2] || product1(e_4,u,e_3)*+ -> equalish(u,e_2). % 0.56/0.74 1452[7:Spt:1379.0,1379.3] || product1(e_4,e_1,u)*+ -> equalish(u,e_2). % 0.56/0.74 1485[8:Spt:1378.0,1378.3] || product1(e_1,u,e_4)+ -> product2(e_2,u,e_1)*. % 0.56/0.74 1486[8:Res:1218.0,1485.0] || -> product2(e_2,e_2,e_1)*. % 0.56/0.74 1490[8:Res:1486.0,63.0] || -> equalish(e_1,e_2)*. % 0.56/0.74 1494[8:MRR:1490.0,26.0] || -> . % 0.56/0.74 1498[8:Spt:1494.0,1378.1,1378.2] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)*. % 0.56/0.74 1505[8:Res:1498.1,1452.0] || -> product1(e_4,e_1,e_4)* equalish(e_3,e_2). % 0.56/0.74 1507[8:MRR:1505.1,33.0] || -> product1(e_4,e_1,e_4)*. % 0.56/0.74 1518[8:Res:1507.0,1452.0] || -> equalish(e_4,e_2)*. % 0.56/0.74 1521[8:MRR:1518.0,36.0] || -> . % 0.56/0.74 1527[7:Spt:1521.0,1379.1,1379.2] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)*. % 0.56/0.74 1534[7:Res:1527.1,1412.0] || -> product1(e_4,e_1,e_4)* equalish(e_1,e_2). % 0.56/0.74 1535[7:MRR:1534.1,26.0] || -> product1(e_4,e_1,e_4)*. % 0.56/0.74 1544[7:Res:1535.0,1232.0] || -> equalish(e_4,e_2)*. % 0.56/0.74 1547[7:MRR:1544.0,36.0] || -> . % 0.56/0.74 1551[6:Spt:1547.0,1405.1] || -> product1(e_4,e_2,e_4)*. % 0.56/0.74 1561[6:Res:1551.0,1409.0] || -> equalish(e_4,e_3)*. % 0.56/0.74 1564[6:MRR:1561.0,37.0] || -> . % 0.56/0.74 1567[5:Spt:1564.0,1404.1] || -> product1(e_4,e_2,e_4)*. % 0.56/0.74 1576[5:Res:1567.0,1223.0] || -> equalish(e_4,e_1)*. % 0.56/0.74 1578[5:MRR:1576.0,35.0] || -> . % 0.56/0.74 1581[3:Spt:1578.0,159.0,1227.0] || product1(e_2,e_1,e_4)*+ -> . % 0.56/0.74 1582[3:Spt:1578.0,159.1] || -> product1(e_2,e_1,e_3)*. % 0.56/0.74 1583[3:MRR:163.1,1581.0] || product1(u,e_1,e_3)*+ -> equalish(u,e_2). % 0.56/0.74 1609[4:Spt:1376.0] || -> product1(e_4,e_1,e_4)*. % 0.56/0.74 1610[4:Res:1609.0,67.0] || -> equalish(e_1,e_4)*. % 0.56/0.74 1618[4:MRR:1610.0,28.0] || -> . % 0.56/0.74 1620[4:Spt:1618.0,1376.0,1609.0] || product1(e_4,e_1,e_4)*+ -> . % 0.56/0.74 1621[4:Spt:1618.0,1376.1,1376.2] || -> product1(e_4,e_1,e_3) product1(e_4,e_1,e_2)*. % 0.56/0.74 1625[4:MRR:1378.1,1620.0] || product1(e_1,u,e_4) -> product1(e_4,e_1,e_3) product2(e_2,u,e_1)*. % 0.56/0.74 1627[5:Spt:1621.0] || -> product1(e_4,e_1,e_3)*. % 0.56/0.74 1633[5:Res:1627.0,1583.0] || -> equalish(e_4,e_2)*. % 0.56/0.74 1635[5:MRR:1633.0,36.0] || -> . % 0.56/0.74 1639[5:Spt:1635.0,1621.0,1627.0] || product1(e_4,e_1,e_3)*+ -> . % 0.56/0.74 1640[5:Spt:1635.0,1621.1] || -> product1(e_4,e_1,e_2)*. % 0.56/0.74 1644[5:MRR:1625.1,1639.0] || product1(e_1,u,e_4)+ -> product2(e_2,u,e_1)*. % 0.56/0.74 1669[5:Res:1218.0,1644.0] || -> product2(e_2,e_2,e_1)*. % 0.56/0.74 1673[5:Res:1669.0,63.0] || -> equalish(e_1,e_2)*. % 0.56/0.74 1677[5:MRR:1673.0,26.0] || -> . % 0.56/0.74 1681[2:Spt:1677.0,586.0,1218.0] || product1(e_1,e_2,e_4)*+ -> . % 0.56/0.74 1682[2:Spt:1677.0,586.1] || -> product1(e_1,e_2,e_3)*. % 0.56/0.74 1685[2:MRR:592.1,1681.0] || product1(u,e_2,e_3)*+ -> equalish(u,e_1). % 0.56/0.74 1695[3:Spt:159.0] || -> product1(e_2,e_1,e_4)*. % 0.56/0.74 1696[3:Res:1695.0,100.2] group_element(e_2) group_element(e_4) || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 1704[3:SSi:1696.1,1696.0,25.0,23.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 1849[3:Res:1704.3,63.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2)* equalish(e_2,e_1). % 0.56/0.74 1851[3:MRR:1849.3,29.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3) product1(e_4,e_2,e_2)*. % 0.56/0.74 1858[3:Res:1851.2,65.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3)* equalish(e_4,e_2). % 0.56/0.74 1860[3:MRR:1858.2,36.0] || -> product1(e_4,e_2,e_4) product1(e_4,e_2,e_3)*. % 0.56/0.74 1868[3:Res:1860.1,1685.0] || -> product1(e_4,e_2,e_4)* equalish(e_4,e_1). % 0.56/0.74 1870[3:MRR:1868.1,35.0] || -> product1(e_4,e_2,e_4)*. % 0.56/0.74 1872[3:Res:1870.0,67.0] || -> equalish(e_2,e_4)*. % 0.56/0.74 1880[3:MRR:1872.0,31.0] || -> . % 0.56/0.74 1882[3:Spt:1880.0,159.0,1695.0] || product1(e_2,e_1,e_4)*+ -> . % 0.56/0.74 1883[3:Spt:1880.0,159.1] || -> product1(e_2,e_1,e_3)*. % 0.56/0.74 1884[3:MRR:163.1,1882.0] || product1(u,e_1,e_3)*+ -> equalish(u,e_2). % 0.56/0.74 1890[3:Res:1883.0,100.2] group_element(e_2) group_element(e_3) || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3) product1(e_3,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 1896[3:SSi:1890.1,1890.0,24.0,23.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3) product1(e_3,e_2,e_2) product2(e_1,e_1,e_2)*. % 0.56/0.74 1917[4:Spt:950.2] || -> cycle(e_2,e_3)*. % 0.56/0.74 1924[4:MRR:255.2,1917.0] || next(e_3,u)*+ cycle(u,e_0) cycle(e_3,e_0) -> . % 0.56/0.74 1933[4:Res:4.0,1924.0] || cycle(e_4,e_0) cycle(e_3,e_0)* -> . % 0.56/0.74 1934[4:MRR:1933.0,17.0] || cycle(e_3,e_0)*+ -> . % 0.56/0.74 1935[4:Res:16.4,1934.0] group_element(e_3) || -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 0.56/0.74 1936[4:SSi:1935.0,24.0] || -> cycle(e_3,e_3) cycle(e_3,e_2) cycle(e_3,e_1)*. % 0.56/0.74 1937[5:Spt:1936.0] || -> cycle(e_3,e_3)*. % 0.56/0.74 1941[5:Res:1937.0,206.0] || greater(e_3,e_0) -> equalish(e_3,e_1)*. % 0.56/0.74 1942[5:MRR:1941.0,1941.1,7.0,32.0] || -> . % 0.56/0.74 1943[5:Spt:1942.0,1936.0,1937.0] || cycle(e_3,e_3)*+ -> . % 0.56/0.74 1944[5:Spt:1942.0,1936.1,1936.2] || -> cycle(e_3,e_2) cycle(e_3,e_1)*. % 0.56/0.74 1947[5:Res:1944.1,15.0] || cycle(e_3,u)+ -> cycle(e_3,e_2) equalish(u,e_1)*. % 0.56/0.74 1950[6:Spt:1947.0,1947.2] || cycle(e_3,u)+ -> equalish(u,e_1)*. % 0.56/0.74 1953[5:Res:1944.1,199.0] || cycle(e_2,u)+ greater(u,e_0) -> cycle(e_3,e_2) equalish(u,e_2)*. % 0.56/0.74 1954[7:Spt:1953.0,1953.1,1953.3] || cycle(e_2,u)+ greater(u,e_0) -> equalish(u,e_2)*. % 0.56/0.74 1956[7:Res:1917.0,1954.0] || greater(e_3,e_0) -> equalish(e_3,e_2)*. % 0.56/0.74 1957[7:MRR:1956.0,1956.1,7.0,33.0] || -> . % 0.56/0.74 1958[7:Spt:1957.0,1953.2] || -> cycle(e_3,e_2)*. % 0.56/0.74 1961[7:Res:1958.0,1950.0] || -> equalish(e_2,e_1)*. % 0.56/0.74 1962[7:MRR:1961.0,29.0] || -> . % 0.56/0.74 1963[6:Spt:1962.0,1947.1] || -> cycle(e_3,e_2)*. % 0.56/0.74 1969[6:Res:1963.0,206.0] || greater(e_2,e_0) -> equalish(e_2,e_1)*. % 0.56/0.74 1970[6:MRR:1969.0,1969.1,6.0,29.0] || -> . % 0.56/0.74 1971[4:Spt:1970.0,950.2,1917.0] || cycle(e_2,e_3)*+ -> . % 0.56/0.74 1972[4:Spt:1970.0,950.0,950.1,950.3] || cycle(e_0,e_2)*+ cycle(e_1,e_0) -> cycle(e_2,e_2). % 0.56/0.74 2019[3:Res:1896.3,63.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3) product1(e_3,e_2,e_2)* equalish(e_2,e_1). % 0.56/0.74 2021[3:MRR:2019.3,29.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3) product1(e_3,e_2,e_2)*. % 0.56/0.74 2028[3:Res:2021.2,65.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3)* equalish(e_3,e_2). % 0.56/0.74 2030[3:MRR:2028.2,33.0] || -> product1(e_3,e_2,e_4) product1(e_3,e_2,e_3)*. % 0.56/0.74 2033[3:Res:2030.1,67.0] || -> product1(e_3,e_2,e_4)* equalish(e_2,e_3). % 0.56/0.74 2042[3:MRR:2033.1,30.0] || -> product1(e_3,e_2,e_4)*. % 0.56/0.74 2045[3:Res:2042.0,100.2] group_element(e_3) group_element(e_4) || -> product1(e_4,e_3,e_4) product1(e_4,e_3,e_3) product1(e_4,e_3,e_2) product2(e_1,e_2,e_3)*. % 0.56/0.75 2051[3:SSi:2045.1,2045.0,25.0,24.0] || -> product1(e_4,e_3,e_4) product1(e_4,e_3,e_3) product1(e_4,e_3,e_2) product2(e_1,e_2,e_3)*. % 0.56/0.75 2091[3:Res:2051.3,1214.0] || -> product1(e_4,e_3,e_4) product1(e_4,e_3,e_3) product1(e_4,e_3,e_2)* equalish(e_3,e_4). % 0.56/0.75 2096[3:MRR:2091.0,2091.3,67.0,34.0] || -> product1(e_4,e_3,e_3) product1(e_4,e_3,e_2)*. % 0.56/0.75 2099[3:Res:2096.1,39.0] || product1(e_4,e_3,u)*+ -> product1(e_4,e_3,e_3)* equalish(u,e_2). % 0.56/0.75 2100[3:Res:2096.1,40.0] || product1(e_4,u,e_2)*+ -> product1(e_4,e_3,e_3)* equalish(u,e_3). % 0.56/0.75 2119[5:Spt:2099.0,2099.2] || product1(e_4,e_3,u)*+ -> equalish(u,e_2). % 0.56/0.75 2122[6:Spt:2100.0,2100.2] || product1(e_4,u,e_2)*+ -> equalish(u,e_3). % 0.56/0.75 2123[6:Res:410.3,2122.0] group_element(e_4) || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)* equalish(e_1,e_4) equalish(e_1,e_3). % 0.56/0.75 2128[6:SSi:2123.0,25.0] || -> product1(e_4,e_1,e_4) product1(e_4,e_1,e_3)* equalish(e_1,e_4) equalish(e_1,e_3). % 0.56/0.75 2129[6:MRR:2128.0,2128.2,2128.3,67.0,28.0,27.0] || -> product1(e_4,e_1,e_3)*. % 0.56/0.75 2135[6:Res:2129.0,1884.0] || -> equalish(e_4,e_2)*. % 0.56/0.75 2137[6:MRR:2135.0,36.0] || -> . % 0.56/0.75 2141[6:Spt:2137.0,2100.1] || -> product1(e_4,e_3,e_3)*. % 0.56/0.75 2149[6:Res:2141.0,2119.0] || -> equalish(e_3,e_2)*. % 0.56/0.75 2151[6:MRR:2149.0,33.0] || -> . % 0.56/0.75 2153[5:Spt:2151.0,2099.1] || -> product1(e_4,e_3,e_3)*. % 0.56/0.75 2159[5:Res:2153.0,65.0] || -> equalish(e_4,e_3)*. % 0.56/0.75 2161[5:MRR:2159.0,37.0] || -> . % 0.56/0.75 % SZS output end Refutation % 0.56/0.75 Formulae used in the proof : e_0_then_e_1 e_1_then_e_2 e_2_then_e_3 e_3_then_e_4 e_1_greater_e_0 e_2_greater_e_0 e_3_greater_e_0 e_2_greater_e_1 e_3_greater_e_2 cycle1 cycle2 cycle3 cycle4 cycle5 element_1 element_2 element_3 element_4 e_1_is_not_e_2 e_1_is_not_e_3 e_1_is_not_e_4 e_2_is_not_e_1 e_2_is_not_e_3 e_2_is_not_e_4 e_3_is_not_e_1 e_3_is_not_e_2 e_3_is_not_e_4 e_4_is_not_e_1 e_4_is_not_e_2 e_4_is_not_e_3 product1_total_function1 product1_total_function2 product1_right_cancellation product1_left_cancellation product1_idempotence product2_total_function1 product2_total_function2 product2_right_cancellation product2_left_cancellation product2_idempotence qg2a % 0.56/0.75 %------------------------------------------------------------------------------