%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP134-1.003 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.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:51 EDT 2022 % Result : Unsatisfiable 18.69s 18.91s % Output : Refutation 22.05s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP134-1.003 : TPTP v8.1.0. Released v1.2.0. % 0.06/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n024.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 06:39:48 EDT 2022 % 0.13/0.34 % CPUTime : % 18.69/18.91 % 18.69/18.91 SPASS V 3.9 % 18.69/18.91 SPASS beiseite: Proof found. % 18.69/18.91 % SZS status Theorem % 18.69/18.91 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 18.69/18.91 SPASS derived 8722 clauses, backtracked 3858 clauses, performed 57 splits and kept 6928 clauses. % 18.69/18.91 SPASS allocated 90476 KBytes. % 18.69/18.91 SPASS spent 0:0:18.55 on the problem. % 18.69/18.91 0:00:00.04 for the input. % 18.69/18.91 0:00:00.00 for the FLOTTER CNF translation. % 18.69/18.91 0:00:00.17 for inferences. % 18.69/18.91 0:00:00.09 for the backtracking. % 18.69/18.91 0:0:18.21 for the reduction. % 18.69/18.91 % 18.69/18.91 % 18.69/18.91 Here is a proof with depth 18, length 480 : % 18.69/18.91 % SZS output start Refutation % 18.69/18.91 1[0:Inp] || -> group_element(e_1)*. % 18.69/18.91 2[0:Inp] || -> group_element(e_2)*. % 18.69/18.91 3[0:Inp] || -> group_element(e_3)*. % 18.69/18.91 4[0:Inp] || equalish(e_1,e_2)*+ -> . % 18.69/18.91 5[0:Inp] || equalish(e_1,e_3)*+ -> . % 18.69/18.91 6[0:Inp] || equalish(e_2,e_1)*+ -> . % 18.69/18.91 7[0:Inp] || equalish(e_2,e_3)*+ -> . % 18.69/18.91 8[0:Inp] || equalish(e_3,e_1)*+ -> . % 18.69/18.91 9[0:Inp] || equalish(e_3,e_2)*+ -> . % 18.69/18.91 10[0:Inp] group_element(u) group_element(v) || -> product(v,u,e_3) product(v,u,e_2) product(v,u,e_1)*. % 18.69/18.91 11[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 18.69/18.91 12[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 18.69/18.91 13[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 18.69/18.91 14[0:Inp] || product(u,v,w)*+ product(v,u,x)* -> product(x,w,u)*. % 18.69/18.91 18[0:Res:10.4,14.0] group_element(u) group_element(v) || product(u,v,w)*+ -> product(v,u,e_3) product(v,u,e_2)* product(w,e_1,v)*. % 18.69/18.91 19[0:Res:10.4,11.0] group_element(u) group_element(v) || product(v,u,w)*+ -> product(v,u,e_3) product(v,u,e_2)* equalish(w,e_1). % 18.69/18.91 20[0:Res:10.4,12.0] group_element(u) group_element(v) || product(v,w,e_1)*+ -> product(v,u,e_3) product(v,u,e_2)* equalish(w,u)*. % 18.69/18.91 21[0:Res:10.4,13.0] group_element(u) group_element(v) || product(w,u,e_1)*+ -> product(v,u,e_3) product(v,u,e_2)* equalish(w,v)*. % 18.69/18.91 24[0:Res:10.4,20.2] group_element(u) group_element(v) group_element(w) group_element(v) || -> product(v,u,e_3) product(v,u,e_2)* product(v,w,e_3) product(v,w,e_2)* equalish(u,w)*. % 18.69/18.91 25[0:Obv:24.1] group_element(u) group_element(v) group_element(w) || -> product(w,u,e_3) product(w,u,e_2)* product(w,v,e_3) product(w,v,e_2)* equalish(u,v)*. % 18.69/18.91 26[0:Res:10.4,19.2] group_element(u) group_element(v) group_element(u) group_element(v) || -> product(v,u,e_3) product(v,u,e_2)* product(v,u,e_3) product(v,u,e_2)* equalish(e_1,e_1). % 18.69/18.91 27[0:Obv:26.5] group_element(u) group_element(v) || -> product(v,u,e_3) product(v,u,e_2)* equalish(e_1,e_1). % 18.69/18.91 28[1:Spt:27.0,27.1,27.2,27.3] group_element(u) group_element(v) || -> product(v,u,e_3) product(v,u,e_2)*. % 18.69/18.91 29[1:Res:28.3,14.0] group_element(u) group_element(v) || product(u,v,w)*+ -> product(v,u,e_3)* product(w,e_2,v)*. % 18.69/18.91 30[1:Res:28.3,11.0] group_element(u) group_element(v) || product(v,u,w)*+ -> product(v,u,e_3)* equalish(w,e_2). % 18.69/18.91 31[1:Res:28.3,12.0] group_element(u) group_element(v) || product(v,w,e_2)*+ -> product(v,u,e_3)* equalish(w,u)*. % 18.69/18.91 32[1:Res:28.3,13.0] group_element(u) group_element(v) || product(w,u,e_2)*+ -> product(v,u,e_3)* equalish(w,v)*. % 18.69/18.91 33[1:Res:28.3,30.2] group_element(u) group_element(v) group_element(u) group_element(v) || -> product(v,u,e_3)* product(v,u,e_3)* equalish(e_2,e_2). % 18.69/18.91 34[1:Obv:33.4] group_element(u) group_element(v) || -> product(v,u,e_3)* equalish(e_2,e_2). % 18.69/18.91 37[2:Spt:34.0,34.1,34.2] group_element(u) group_element(v) || -> product(v,u,e_3)*. % 18.69/18.91 40[2:Res:37.2,12.0] group_element(u) group_element(v) || product(v,w,e_3)*+ -> equalish(w,u)*. % 18.69/18.91 48[2:Res:37.2,40.2] group_element(u) group_element(v) group_element(w) group_element(v) || -> equalish(u,w)*. % 18.69/18.91 49[2:Obv:48.1] group_element(u) group_element(v) group_element(w) || -> equalish(u,v)*. % 18.69/18.91 50[2:Con:49.2] group_element(u) group_element(v) || -> equalish(u,v)*. % 18.69/18.91 56[2:Res:50.2,4.0] group_element(e_1) group_element(e_2) || -> . % 18.69/18.91 62[2:SSi:56.1,56.0,2.0,1.0] || -> . % 18.69/18.91 63[2:Spt:62.0,34.3] || -> equalish(e_2,e_2)*. % 18.69/18.91 74[1:Res:28.3,29.2] group_element(u) group_element(v) group_element(v) group_element(u) || -> product(v,u,e_3)* product(u,v,e_3)* product(e_2,e_2,u)*. % 18.69/18.91 75[1:Obv:74.1] group_element(u) group_element(v) || -> product(u,v,e_3)* product(v,u,e_3)* product(e_2,e_2,v)*. % 18.69/18.91 76[1:Fac:75.2,75.3] group_element(u) group_element(u) || -> product(u,u,e_3)* product(e_2,e_2,u)*. % 18.69/18.91 95[1:Res:75.4,31.2] group_element(u) group_element(e_2) group_element(v) group_element(e_2) || -> product(u,e_2,e_3)* product(e_2,u,e_3)* product(e_2,v,e_3)* equalish(e_2,v). % 18.69/18.91 96[1:Res:75.4,32.2] group_element(u) group_element(e_2) group_element(e_2) group_element(v) || -> product(u,e_2,e_3)* product(e_2,u,e_3)* product(v,e_2,e_3)* equalish(e_2,v). % 18.69/18.91 97[1:Obv:76.0] group_element(u) || -> product(u,u,e_3)* product(e_2,e_2,u)*. % 18.69/18.91 98[1:Obv:96.1] group_element(u) group_element(e_2) group_element(v) || -> product(u,e_2,e_3)* product(e_2,u,e_3)* product(v,e_2,e_3)* equalish(e_2,v). % 18.69/18.91 99[1:SSi:98.1,2.0] group_element(u) group_element(v) || -> product(u,e_2,e_3)* product(e_2,u,e_3)* product(v,e_2,e_3)* equalish(e_2,v). % 18.69/18.91 100[1:Obv:95.1] group_element(u) group_element(v) group_element(e_2) || -> product(u,e_2,e_3)* product(e_2,u,e_3)* product(e_2,v,e_3)* equalish(e_2,v). % 18.69/18.91 101[1:SSi:100.2,2.0] group_element(u) group_element(v) || -> product(u,e_2,e_3)* product(e_2,u,e_3)* product(e_2,v,e_3)* equalish(e_2,v). % 18.69/18.91 121[1:Res:97.2,30.2] group_element(u) group_element(e_2) group_element(e_2) || -> product(u,u,e_3)* product(e_2,e_2,e_3)* equalish(u,e_2). % 18.69/18.91 122[1:Res:97.2,31.2] group_element(e_2) group_element(u) group_element(e_2) || -> product(e_2,e_2,e_3)* product(e_2,u,e_3)* equalish(e_2,u). % 18.69/18.91 123[1:Res:97.2,32.2] group_element(e_2) group_element(e_2) group_element(u) || -> product(e_2,e_2,e_3)* product(u,e_2,e_3)* equalish(e_2,u). % 18.69/18.91 124[1:Obv:123.0] group_element(e_2) group_element(u) || -> product(e_2,e_2,e_3)* product(u,e_2,e_3)* equalish(e_2,u). % 18.69/18.91 125[1:SSi:124.0,2.0] group_element(u) || -> product(e_2,e_2,e_3)* product(u,e_2,e_3)* equalish(e_2,u). % 18.69/18.91 126[1:Obv:122.0] group_element(u) group_element(e_2) || -> product(e_2,e_2,e_3)* product(e_2,u,e_3)* equalish(e_2,u). % 18.69/18.91 127[1:SSi:126.1,2.0] group_element(u) || -> product(e_2,e_2,e_3)* product(e_2,u,e_3)* equalish(e_2,u). % 18.69/18.91 128[1:Obv:121.1] group_element(u) group_element(e_2) || -> product(u,u,e_3)* product(e_2,e_2,e_3)* equalish(u,e_2). % 18.69/18.91 129[1:SSi:128.1,2.0] group_element(u) || -> product(u,u,e_3)* product(e_2,e_2,e_3)* equalish(u,e_2). % 18.69/18.91 134[3:Spt:125.0,125.2,125.3] group_element(u) || -> product(u,e_2,e_3)* equalish(e_2,u). % 18.69/18.91 138[3:Res:134.1,12.0] group_element(u) || product(u,v,e_3)*+ -> equalish(e_2,u) equalish(v,e_2). % 18.69/18.91 170[4:Spt:127.0,127.2,127.3] group_element(u) || -> product(e_2,u,e_3)* equalish(e_2,u). % 18.69/18.91 179[5:Spt:129.0,129.1,129.3] group_element(u) || -> product(u,u,e_3)* equalish(u,e_2). % 18.69/18.91 333[5:Res:179.1,138.1] group_element(u) group_element(u) || -> equalish(u,e_2)* equalish(e_2,u)* equalish(u,e_2)*. % 18.69/18.91 340[5:Obv:333.2] group_element(u) || -> equalish(e_2,u)* equalish(u,e_2)*. % 18.69/18.91 360[5:Res:340.2,4.0] group_element(e_1) || -> equalish(e_2,e_1)*. % 18.69/18.91 363[5:SSi:360.0,1.0] || -> equalish(e_2,e_1)*. % 18.69/18.91 364[5:MRR:363.0,6.0] || -> . % 18.69/18.91 365[5:Spt:364.0,129.2] || -> product(e_2,e_2,e_3)*. % 18.69/18.91 369[5:Res:365.0,12.0] || product(e_2,u,e_3)*+ -> equalish(u,e_2). % 18.69/18.91 443[5:Res:170.1,369.0] group_element(u) || -> equalish(e_2,u)* equalish(u,e_2)*. % 18.69/18.91 613[5:Res:443.2,4.0] group_element(e_1) || -> equalish(e_2,e_1)*. % 18.75/18.91 616[5:SSi:613.0,1.0] || -> equalish(e_2,e_1)*. % 18.75/18.91 617[5:MRR:616.0,6.0] || -> . % 18.75/18.91 618[4:Spt:617.0,127.1] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 644[4:Res:618.0,12.0] || product(e_2,u,e_3)*+ -> equalish(u,e_2). % 18.75/18.91 645[4:Res:618.0,13.0] || product(u,e_2,e_3)*+ -> equalish(u,e_2). % 18.75/18.91 680[5:Spt:101.1,101.4,101.5] group_element(u) || -> product(e_2,u,e_3)* equalish(e_2,u). % 18.75/18.91 715[5:Res:680.1,644.0] group_element(u) || -> equalish(e_2,u)* equalish(u,e_2)*. % 18.75/18.91 878[5:Res:715.2,4.0] group_element(e_1) || -> equalish(e_2,e_1)*. % 18.75/18.91 881[5:SSi:878.0,1.0] || -> equalish(e_2,e_1)*. % 18.75/18.91 882[5:MRR:881.0,6.0] || -> . % 18.75/18.91 883[5:Spt:882.0,101.0,101.2,101.3] group_element(u) || -> product(u,e_2,e_3)* product(e_2,u,e_3)*. % 18.75/18.91 896[5:Res:883.1,645.0] group_element(u) || -> product(e_2,u,e_3)* equalish(u,e_2). % 18.75/18.91 908[5:MRR:896.1,644.0] group_element(u) || -> equalish(u,e_2)*. % 18.75/18.91 919[5:Res:908.1,4.0] group_element(e_1) || -> . % 18.75/18.91 921[5:SSi:919.0,1.0] || -> . % 18.75/18.91 922[3:Spt:921.0,125.1] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 942[3:Res:922.0,12.0] || product(e_2,u,e_3)*+ -> equalish(u,e_2). % 18.75/18.91 943[3:Res:922.0,13.0] || product(u,e_2,e_3)*+ -> equalish(u,e_2). % 18.75/18.91 980[4:Spt:99.1,99.4,99.5] group_element(u) || -> product(u,e_2,e_3)* equalish(e_2,u). % 18.75/18.91 1038[4:Res:980.1,943.0] group_element(u) || -> equalish(e_2,u)* equalish(u,e_2)*. % 18.75/18.91 1171[4:Res:1038.2,4.0] group_element(e_1) || -> equalish(e_2,e_1)*. % 18.75/18.91 1174[4:SSi:1171.0,1.0] || -> equalish(e_2,e_1)*. % 18.75/18.91 1175[4:MRR:1174.0,6.0] || -> . % 18.75/18.91 1176[4:Spt:1175.0,99.0,99.2,99.3] group_element(u) || -> product(u,e_2,e_3)* product(e_2,u,e_3)*. % 18.75/18.91 1188[4:Res:1176.1,943.0] group_element(u) || -> product(e_2,u,e_3)* equalish(u,e_2). % 18.75/18.91 1199[4:MRR:1188.1,942.0] group_element(u) || -> equalish(u,e_2)*. % 18.75/18.91 1209[4:Res:1199.1,4.0] group_element(e_1) || -> . % 18.75/18.91 1211[4:SSi:1209.0,1.0] || -> . % 18.75/18.91 1212[1:Spt:1211.0,27.4] || -> equalish(e_1,e_1)*. % 18.75/18.91 1223[0:Res:10.4,18.2] group_element(u) group_element(v) group_element(v) group_element(u) || -> product(v,u,e_3) product(v,u,e_2)* product(u,v,e_3) product(u,v,e_2)* product(e_1,e_1,u)*. % 18.75/18.91 1224[0:Obv:1223.1] group_element(u) group_element(v) || -> product(u,v,e_3) product(u,v,e_2)* product(v,u,e_3) product(v,u,e_2)* product(e_1,e_1,v)*. % 18.75/18.91 1225[0:Fac:1224.3,1224.5] group_element(u) group_element(u) || -> product(u,u,e_3) product(u,u,e_3) product(u,u,e_2)* product(e_1,e_1,u)*. % 18.75/18.91 1232[0:Res:1224.5,18.2] group_element(u) group_element(v) group_element(v) group_element(u) || -> product(u,v,e_3) product(u,v,e_2)* product(v,u,e_3)* product(e_1,e_1,v)* product(u,v,e_3) product(u,v,e_2)* product(e_2,e_1,u)*. % 18.75/18.91 1244[0:Res:1224.6,20.2] group_element(u) group_element(e_1) group_element(v) group_element(e_1) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)* product(e_1,v,e_3) product(e_1,v,e_2)* equalish(e_1,v). % 18.75/18.91 1245[0:Res:1224.6,21.2] group_element(u) group_element(e_1) group_element(e_1) group_element(v) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)* product(v,e_1,e_3) product(v,e_1,e_2)* equalish(e_1,v). % 18.75/18.91 1246[0:Obv:1225.2] group_element(u) || -> product(u,u,e_3) product(u,u,e_2)* product(e_1,e_1,u)*. % 18.75/18.91 1247[0:Obv:1245.1] group_element(u) group_element(e_1) group_element(v) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)* product(v,e_1,e_3) product(v,e_1,e_2)* equalish(e_1,v). % 18.75/18.91 1248[0:SSi:1247.1,1.0] group_element(u) group_element(v) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)* product(v,e_1,e_3) product(v,e_1,e_2)* equalish(e_1,v). % 18.75/18.91 1249[0:Obv:1244.1] group_element(u) group_element(v) group_element(e_1) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)* product(e_1,v,e_3) product(e_1,v,e_2)* equalish(e_1,v). % 18.75/18.91 1250[0:SSi:1249.2,1.0] group_element(u) group_element(v) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)* product(e_1,v,e_3) product(e_1,v,e_2)* equalish(e_1,v). % 18.75/18.91 1257[0:Obv:1232.5] group_element(u) group_element(v) || -> product(u,v,e_3)* product(e_1,e_1,u)* product(v,u,e_3) product(v,u,e_2)* product(e_2,e_1,v)*. % 18.75/18.91 1260[0:Res:1246.2,14.0] group_element(u) || product(u,u,v)*+ -> product(u,u,e_3)* product(e_1,e_1,u)* product(v,e_2,u)*. % 18.75/18.91 1261[0:Res:1246.2,11.0] group_element(u) || product(u,u,v)*+ -> product(u,u,e_3)* product(e_1,e_1,u)* equalish(v,e_2). % 18.75/18.91 1269[0:Res:1246.3,13.0] group_element(u) || product(v,e_1,u)*+ -> product(u,u,e_3) product(u,u,e_2)* equalish(v,e_1). % 18.75/18.91 1290[0:Res:25.6,18.2] group_element(u) group_element(v) group_element(w) group_element(w) group_element(v) || -> product(w,u,e_3) product(w,u,e_2)* product(w,v,e_3)* equalish(u,v)* product(v,w,e_3) product(v,w,e_2)* product(e_2,e_1,v)*. % 18.75/18.91 1299[0:Obv:1290.2] group_element(u) group_element(v) group_element(w) || -> product(v,u,e_3) product(v,u,e_2)* product(v,w,e_3)* equalish(u,w)* product(w,v,e_3) product(w,v,e_2)* product(e_2,e_1,w)*. % 18.75/18.91 1313[0:Res:1246.2,1261.1] group_element(u) group_element(u) || -> product(u,u,e_3)* product(e_1,e_1,u)* product(u,u,e_3)* product(e_1,e_1,u)* equalish(e_2,e_2). % 18.75/18.91 1317[0:Obv:1313.3] group_element(u) || -> product(u,u,e_3)* product(e_1,e_1,u)* equalish(e_2,e_2). % 18.75/18.91 1323[2:Spt:1317.0,1317.1,1317.2] group_element(u) || -> product(u,u,e_3)* product(e_1,e_1,u)*. % 18.75/18.91 1326[2:Res:1323.1,11.0] group_element(u) || product(u,u,v)*+ -> product(e_1,e_1,u)* equalish(v,e_3). % 18.75/18.91 1333[2:Res:1323.2,12.0] group_element(u) || product(e_1,v,u)*+ -> product(u,u,e_3)* equalish(v,e_1). % 18.75/18.91 1352[2:Res:1323.1,1326.1] group_element(u) group_element(u) || -> product(e_1,e_1,u)* product(e_1,e_1,u)* equalish(e_3,e_3). % 18.75/18.91 1354[2:Res:1323.2,1326.1] group_element(u) group_element(e_1) || -> product(u,u,e_3)* product(e_1,e_1,e_1)* equalish(u,e_3). % 18.75/18.91 1355[2:Obv:1352.2] group_element(u) || -> product(e_1,e_1,u)* equalish(e_3,e_3). % 18.75/18.91 1356[2:SSi:1354.1,1.0] group_element(u) || -> product(u,u,e_3)* product(e_1,e_1,e_1)* equalish(u,e_3). % 18.75/18.91 1384[3:Spt:1355.0,1355.1] group_element(u) || -> product(e_1,e_1,u)*. % 18.75/18.91 1387[3:Res:1384.1,11.0] group_element(u) || product(e_1,e_1,v)*+ -> equalish(v,u)*. % 18.75/18.91 1401[3:Res:1384.1,1387.1] group_element(u) group_element(v) || -> equalish(u,v)*. % 18.75/18.91 1419[3:Res:1401.2,4.0] group_element(e_1) group_element(e_2) || -> . % 18.75/18.91 1425[3:SSi:1419.1,1419.0,2.0,1.0] || -> . % 18.75/18.91 1426[3:Spt:1425.0,1355.2] || -> equalish(e_3,e_3)*. % 18.75/18.91 1477[4:Spt:1356.0,1356.1,1356.3] group_element(u) || -> product(u,u,e_3)* equalish(u,e_3). % 18.75/18.91 1479[4:Res:1477.1,14.0] group_element(u) || product(u,u,v)*+ -> equalish(u,e_3) product(v,e_3,u)*. % 18.75/18.91 1909[4:Res:1477.1,1479.1] group_element(u) group_element(u) || -> equalish(u,e_3) equalish(u,e_3) product(e_3,e_3,u)*. % 18.75/18.91 1915[4:Obv:1909.2] group_element(u) || -> equalish(u,e_3) product(e_3,e_3,u)*. % 18.75/18.91 1948[4:Res:1915.2,1326.1] group_element(u) group_element(e_3) || -> equalish(u,e_3)* product(e_1,e_1,e_3)* equalish(u,e_3)*. % 18.75/18.91 1960[4:Obv:1948.2] group_element(u) group_element(e_3) || -> product(e_1,e_1,e_3)* equalish(u,e_3)*. % 18.75/18.91 1961[4:SSi:1960.1,3.0] group_element(u) || -> product(e_1,e_1,e_3)* equalish(u,e_3)*. % 18.75/18.91 2007[5:Spt:1961.0,1961.2] group_element(u) || -> equalish(u,e_3)*. % 18.75/18.91 2009[5:Res:2007.1,5.0] group_element(e_1) || -> . % 18.75/18.91 2011[5:SSi:2009.0,1.0] || -> . % 18.75/18.91 2012[5:Spt:2011.0,1961.1] || -> product(e_1,e_1,e_3)*. % 18.75/18.91 2014[5:Res:2012.0,14.0] || product(e_1,e_1,u)*+ -> product(u,e_3,e_1)*. % 18.75/18.91 2157[5:Res:2012.0,2014.0] || -> product(e_3,e_3,e_1)*. % 18.75/18.91 2165[5:Res:2157.0,11.0] || product(e_3,e_3,u)*+ -> equalish(u,e_1). % 18.75/18.91 2231[5:Res:1915.2,2165.0] group_element(u) || -> equalish(u,e_3) equalish(u,e_1)*. % 18.75/18.91 2253[5:Res:2231.2,6.0] group_element(e_2) || -> equalish(e_2,e_3)*. % 18.75/18.91 2254[5:SSi:2253.0,2.0] || -> equalish(e_2,e_3)*. % 18.75/18.91 2255[5:MRR:2254.0,7.0] || -> . % 18.75/18.91 2256[4:Spt:2255.0,1356.2] || -> product(e_1,e_1,e_1)*. % 18.75/18.91 2262[4:Res:2256.0,11.0] || product(e_1,e_1,u)*+ -> equalish(u,e_1). % 18.75/18.91 2267[4:Res:2256.0,20.2] group_element(u) group_element(e_1) || -> product(e_1,u,e_3) product(e_1,u,e_2)* equalish(e_1,u). % 18.75/18.91 2288[4:SSi:2267.1,1.0] group_element(u) || -> product(e_1,u,e_3) product(e_1,u,e_2)* equalish(e_1,u). % 18.75/18.91 2327[4:Res:1323.2,2262.0] group_element(u) || -> product(u,u,e_3)* equalish(u,e_1). % 18.75/18.91 2423[4:Res:2327.1,13.0] group_element(u) || product(v,u,e_3)* -> equalish(u,e_1) equalish(v,u). % 18.75/18.91 2498[4:Res:2288.2,1333.1] group_element(u) group_element(e_2) || -> product(e_1,u,e_3)* equalish(e_1,u) product(e_2,e_2,e_3) equalish(u,e_1). % 18.75/18.91 2509[4:SSi:2498.1,2.0] group_element(u) || -> product(e_1,u,e_3)* equalish(e_1,u) product(e_2,e_2,e_3) equalish(u,e_1). % 18.75/18.91 2510[4:MRR:2509.1,2423.1] group_element(u) || -> equalish(e_1,u)* product(e_2,e_2,e_3)* equalish(u,e_1)*. % 18.75/18.91 2541[5:Spt:2510.0,2510.1,2510.3] group_element(u) || -> equalish(e_1,u)* equalish(u,e_1)*. % 18.75/18.91 2544[5:Res:2541.1,4.0] group_element(e_2) || -> equalish(e_2,e_1)*. % 18.75/18.91 2547[5:SSi:2544.0,2.0] || -> equalish(e_2,e_1)*. % 18.75/18.91 2548[5:MRR:2547.0,6.0] || -> . % 18.75/18.91 2549[5:Spt:2548.0,2510.2] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 2552[5:Res:2549.0,14.0] || product(e_2,e_2,u)*+ -> product(u,e_3,e_2)*. % 18.75/18.91 2642[5:Res:2549.0,2552.0] || -> product(e_3,e_3,e_2)*. % 18.75/18.91 2658[5:Res:2642.0,1326.1] group_element(e_3) || -> product(e_1,e_1,e_3)* equalish(e_2,e_3). % 18.75/18.91 2659[5:SSi:2658.0,3.0] || -> product(e_1,e_1,e_3)* equalish(e_2,e_3). % 18.75/18.91 2660[5:MRR:2659.1,7.0] || -> product(e_1,e_1,e_3)*. % 18.75/18.91 2674[5:Res:2660.0,2262.0] || -> equalish(e_3,e_1)*. % 18.75/18.91 2686[5:MRR:2674.0,8.0] || -> . % 18.75/18.91 2705[2:Spt:2686.0,1317.3] || -> equalish(e_2,e_2)*. % 18.75/18.91 3192[0:Res:1246.2,1260.1] group_element(u) group_element(u) || -> product(u,u,e_3)* product(e_1,e_1,u)* product(u,u,e_3)* product(e_1,e_1,u)* product(e_2,e_2,u). % 18.75/18.91 3195[0:Obv:3192.3] group_element(u) || -> product(u,u,e_3)* product(e_1,e_1,u)* product(e_2,e_2,u). % 18.75/18.91 3210[0:Res:3195.1,11.0] group_element(u) || product(u,u,v)*+ -> product(e_1,e_1,u)* product(e_2,e_2,u) equalish(v,e_3). % 18.75/18.91 3211[0:Res:3195.1,12.0] group_element(u) || product(u,v,e_3)*+ -> product(e_1,e_1,u)* product(e_2,e_2,u) equalish(v,u). % 18.75/18.91 3310[0:Res:3195.1,3210.1] group_element(u) group_element(u) || -> product(e_1,e_1,u)* product(e_2,e_2,u) product(e_1,e_1,u)* product(e_2,e_2,u) equalish(e_3,e_3). % 18.75/18.91 3316[0:Obv:3310.3] group_element(u) || -> product(e_1,e_1,u)* product(e_2,e_2,u) equalish(e_3,e_3). % 18.75/18.91 3329[3:Spt:3316.0,3316.1,3316.2] group_element(u) || -> product(e_1,e_1,u)* product(e_2,e_2,u). % 18.75/18.91 3333[3:Res:3329.1,11.0] group_element(u) || product(e_1,e_1,v)*+ -> product(e_2,e_2,u)* equalish(v,u)*. % 18.75/18.91 3334[3:Res:3329.1,12.0] group_element(u) || product(e_1,v,u)*+ -> product(e_2,e_2,u) equalish(v,e_1). % 18.75/18.91 3335[3:Res:3329.1,13.0] group_element(u) || product(v,e_1,u)*+ -> product(e_2,e_2,u)* equalish(v,e_1). % 18.75/18.91 3350[3:Res:3329.1,1261.1] group_element(u) group_element(e_1) || -> product(e_2,e_2,u)* product(e_1,e_1,e_3) product(e_1,e_1,e_1)* equalish(u,e_2). % 18.75/18.91 3358[3:SSi:3350.1,1.0] group_element(u) || -> product(e_2,e_2,u)* product(e_1,e_1,e_3) product(e_1,e_1,e_1)* equalish(u,e_2). % 18.75/18.91 3401[3:Res:10.4,3334.1] group_element(u) group_element(e_1) group_element(e_1) || -> product(e_1,u,e_3) product(e_1,u,e_2)* product(e_2,e_2,e_1) equalish(u,e_1). % 18.75/18.91 3413[3:Obv:3401.1] group_element(u) group_element(e_1) || -> product(e_1,u,e_3) product(e_1,u,e_2)* product(e_2,e_2,e_1) equalish(u,e_1). % 18.75/18.91 3414[3:SSi:3413.1,1.0] group_element(u) || -> product(e_1,u,e_3) product(e_1,u,e_2)* product(e_2,e_2,e_1) equalish(u,e_1). % 18.75/18.91 3470[3:Res:10.4,3335.1] group_element(e_1) group_element(u) group_element(e_1) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_2,e_2,e_1)* equalish(u,e_1). % 18.75/18.91 3483[3:Obv:3470.0] group_element(u) group_element(e_1) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_2,e_2,e_1)* equalish(u,e_1). % 18.75/18.91 3484[3:SSi:3483.1,1.0] group_element(u) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_2,e_2,e_1)* equalish(u,e_1). % 18.75/18.91 3608[4:Spt:3358.0,3358.1,3358.4] group_element(u) || -> product(e_2,e_2,u)* equalish(u,e_2). % 18.75/18.91 3628[4:Res:3608.1,1261.1] group_element(u) group_element(e_2) || -> equalish(u,e_2)* product(e_2,e_2,e_3) product(e_1,e_1,e_2)* equalish(u,e_2)*. % 18.75/18.91 3630[4:Obv:3628.2] group_element(u) group_element(e_2) || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)* equalish(u,e_2)*. % 18.75/18.91 3631[4:SSi:3630.1,2.0] group_element(u) || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)* equalish(u,e_2)*. % 18.75/18.91 3697[5:Spt:3631.0,3631.3] group_element(u) || -> equalish(u,e_2)*. % 18.75/18.91 3699[5:Res:3697.1,4.0] group_element(e_1) || -> . % 18.75/18.91 3701[5:SSi:3699.0,1.0] || -> . % 18.75/18.91 3702[5:Spt:3701.0,3631.1,3631.2] || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)*. % 18.75/18.91 3703[6:Spt:3702.0] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 3708[6:Res:3703.0,11.0] || product(e_2,e_2,u)*+ -> equalish(u,e_3). % 18.75/18.91 3923[6:Res:3608.1,3708.0] group_element(u) || -> equalish(u,e_2)* equalish(u,e_3). % 18.75/18.91 4010[6:Res:3923.1,4.0] group_element(e_1) || -> equalish(e_1,e_3)*. % 18.75/18.91 4011[6:SSi:4010.0,1.0] || -> equalish(e_1,e_3)*. % 18.75/18.91 4012[6:MRR:4011.0,5.0] || -> . % 18.75/18.91 4013[6:Spt:4012.0,3702.0,3703.0] || product(e_2,e_2,e_3)*+ -> . % 18.75/18.91 4014[6:Spt:4012.0,3702.1] || -> product(e_1,e_1,e_2)*. % 18.75/18.91 4107[6:Res:3608.1,4013.0] group_element(e_3) || -> equalish(e_3,e_2)*. % 18.75/18.91 4110[6:SSi:4107.0,3.0] || -> equalish(e_3,e_2)*. % 18.75/18.91 4111[6:MRR:4110.0,9.0] || -> . % 18.75/18.91 4114[4:Spt:4111.0,3358.2,3358.3] || -> product(e_1,e_1,e_3) product(e_1,e_1,e_1)*. % 18.75/18.91 4123[5:Spt:4114.0] || -> product(e_1,e_1,e_3)*. % 18.75/18.91 4128[5:Res:4123.0,11.0] || product(e_1,e_1,u)*+ -> equalish(u,e_3). % 18.75/18.91 4129[5:Res:4123.0,12.0] || product(e_1,u,e_3)*+ -> equalish(u,e_1). % 18.75/18.91 4130[5:Res:4123.0,13.0] || product(u,e_1,e_3)*+ -> equalish(u,e_1). % 18.75/18.91 4158[5:MRR:3414.1,4129.0] group_element(u) || -> product(e_1,u,e_2)* product(e_2,e_2,e_1) equalish(u,e_1). % 18.75/18.91 4184[5:MRR:3484.1,4130.0] group_element(u) || -> product(u,e_1,e_2)* product(e_2,e_2,e_1)* equalish(u,e_1). % 18.75/18.91 4222[5:Res:3329.1,4128.0] group_element(u) || -> product(e_2,e_2,u)* equalish(u,e_3). % 18.75/18.91 4738[6:Spt:4158.0,4158.1,4158.3] group_element(u) || -> product(e_1,u,e_2)* equalish(u,e_1). % 18.75/18.91 4742[6:Res:4738.1,14.0] group_element(u) || product(u,e_1,v)* -> equalish(u,e_1) product(v,e_2,e_1)*. % 18.75/18.91 4783[6:MRR:4184.1,4742.1] group_element(u) || -> product(e_2,e_2,e_1)* equalish(u,e_1)*. % 18.75/18.91 4816[7:Spt:4783.0,4783.2] group_element(u) || -> equalish(u,e_1)*. % 18.75/18.91 4818[7:Res:4816.1,6.0] group_element(e_2) || -> . % 18.75/18.91 4820[7:SSi:4818.0,2.0] || -> . % 18.75/18.91 4821[7:Spt:4820.0,4783.1] || -> product(e_2,e_2,e_1)*. % 18.75/18.91 4838[7:Res:4821.0,1261.1] group_element(e_2) || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)* equalish(e_1,e_2). % 18.75/18.91 4839[7:SSi:4838.0,2.0] || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)* equalish(e_1,e_2). % 18.75/18.91 4840[7:MRR:4839.2,4.0] || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)*. % 18.75/18.91 4852[8:Spt:4840.0] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 4857[8:Res:4852.0,11.0] || product(e_2,e_2,u)* -> equalish(u,e_3). % 18.75/18.91 4868[8:MRR:4222.1,4857.0] group_element(u) || -> equalish(u,e_3)*. % 18.75/18.91 4879[8:Res:4868.1,5.0] group_element(e_1) || -> . % 18.75/18.91 4881[8:SSi:4879.0,1.0] || -> . % 18.75/18.91 4882[8:Spt:4881.0,4840.0,4852.0] || product(e_2,e_2,e_3)* -> . % 18.75/18.91 4883[8:Spt:4881.0,4840.1] || -> product(e_1,e_1,e_2)*. % 18.75/18.91 4900[8:Res:4883.0,4128.0] || -> equalish(e_2,e_3)*. % 18.75/18.91 4931[8:MRR:4900.0,7.0] || -> . % 18.75/18.91 4950[6:Spt:4931.0,4158.2] || -> product(e_2,e_2,e_1)*. % 18.75/18.91 4967[6:Res:4950.0,1261.1] group_element(e_2) || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)* equalish(e_1,e_2). % 18.75/18.91 4968[6:SSi:4967.0,2.0] || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)* equalish(e_1,e_2). % 18.75/18.91 4969[6:MRR:4968.2,4.0] || -> product(e_2,e_2,e_3) product(e_1,e_1,e_2)*. % 18.75/18.91 5020[7:Spt:4969.0] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 5025[7:Res:5020.0,11.0] || product(e_2,e_2,u)* -> equalish(u,e_3). % 18.75/18.91 5036[7:MRR:4222.1,5025.0] group_element(u) || -> equalish(u,e_3)*. % 18.75/18.91 5047[7:Res:5036.1,5.0] group_element(e_1) || -> . % 18.75/18.91 5049[7:SSi:5047.0,1.0] || -> . % 18.75/18.91 5050[7:Spt:5049.0,4969.0,5020.0] || product(e_2,e_2,e_3)* -> . % 18.75/18.91 5051[7:Spt:5049.0,4969.1] || -> product(e_1,e_1,e_2)*. % 18.75/18.91 5074[7:Res:5051.0,4128.0] || -> equalish(e_2,e_3)*. % 18.75/18.91 5106[7:MRR:5074.0,7.0] || -> . % 18.75/18.91 5140[5:Spt:5106.0,4114.0,4123.0] || product(e_1,e_1,e_3)*+ -> . % 18.75/18.91 5141[5:Spt:5106.0,4114.1] || -> product(e_1,e_1,e_1)*. % 18.75/18.91 5226[5:Res:5141.0,3333.1] group_element(u) || -> product(e_2,e_2,u)* equalish(e_1,u). % 18.75/18.91 5262[5:Res:3329.1,5140.0] group_element(e_3) || -> product(e_2,e_2,e_3)*. % 18.75/18.91 5267[5:SSi:5262.0,3.0] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 5276[5:Res:5267.0,11.0] || product(e_2,e_2,u)*+ -> equalish(u,e_3). % 18.75/18.91 5898[5:Res:5226.1,5276.0] group_element(u) || -> equalish(e_1,u)* equalish(u,e_3)*. % 18.75/18.91 6015[5:Res:5898.1,4.0] group_element(e_2) || -> equalish(e_2,e_3)*. % 18.75/18.91 6016[5:SSi:6015.0,2.0] || -> equalish(e_2,e_3)*. % 18.75/18.91 6017[5:MRR:6016.0,7.0] || -> . % 18.75/18.91 6018[3:Spt:6017.0,3316.3] || -> equalish(e_3,e_3)*. % 18.75/18.91 6155[4:Spt:1248.1,1248.6,1248.7,1248.8] group_element(u) || -> product(u,e_1,e_3) product(u,e_1,e_2)* equalish(e_1,u). % 18.75/18.91 6162[4:Res:6155.2,13.0] group_element(u) || product(v,e_1,e_2)*+ -> product(u,e_1,e_3)* equalish(e_1,u) equalish(v,u)*. % 18.75/18.91 6298[4:Res:1246.3,6162.1] group_element(e_2) group_element(u) || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2)* product(u,e_1,e_3)* equalish(e_1,u) equalish(e_1,u). % 18.75/18.91 6311[4:Obv:6298.5] group_element(e_2) group_element(u) || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2)* product(u,e_1,e_3)* equalish(e_1,u). % 18.75/18.91 6312[4:SSi:6311.0,2.0] group_element(u) || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2)* product(u,e_1,e_3)* equalish(e_1,u). % 18.75/18.91 6328[5:Spt:6312.0,6312.3,6312.4] group_element(u) || -> product(u,e_1,e_3)* equalish(e_1,u). % 18.75/18.91 6334[5:Res:6328.1,12.0] group_element(u) || product(u,v,e_3)*+ -> equalish(e_1,u) equalish(v,e_1). % 18.75/18.91 6335[5:Res:6328.1,13.0] group_element(u) || product(v,e_1,e_3)*+ -> equalish(e_1,u)* equalish(v,u)*. % 18.75/18.91 6345[5:Res:6328.1,3211.1] group_element(u) group_element(u) || -> equalish(e_1,u) product(e_1,e_1,u)* product(e_2,e_2,u) equalish(e_1,u). % 18.75/18.91 6360[5:Obv:6345.2] group_element(u) || -> product(e_1,e_1,u)* product(e_2,e_2,u) equalish(e_1,u). % 18.75/18.91 6583[5:Res:6360.1,6335.1] group_element(e_3) group_element(u) || -> product(e_2,e_2,e_3)* equalish(e_1,e_3) equalish(e_1,u)* equalish(e_1,u)*. % 18.75/18.91 6592[5:Obv:6583.4] group_element(e_3) group_element(u) || -> product(e_2,e_2,e_3)* equalish(e_1,e_3) equalish(e_1,u)*. % 18.75/18.91 6593[5:Con:6592.1] group_element(e_3) || -> product(e_2,e_2,e_3)* equalish(e_1,e_3). % 18.75/18.91 6594[5:SSi:6593.0,3.0] || -> product(e_2,e_2,e_3)* equalish(e_1,e_3). % 18.75/18.91 6595[5:MRR:6594.1,5.0] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 6746[5:Res:6595.0,6334.1] group_element(e_2) || -> equalish(e_1,e_2)* equalish(e_2,e_1). % 18.75/18.91 6753[5:SSi:6746.0,2.0] || -> equalish(e_1,e_2)* equalish(e_2,e_1). % 18.75/18.91 6754[5:MRR:6753.0,6753.1,4.0,6.0] || -> . % 18.75/18.91 6765[5:Spt:6754.0,6312.1,6312.2] || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2)*. % 18.75/18.91 6770[5:Res:6765.1,11.0] || product(e_2,e_2,u)*+ -> product(e_2,e_2,e_3)* equalish(u,e_2). % 18.75/18.91 6771[5:Res:6765.1,12.0] || product(e_2,u,e_2)*+ -> product(e_2,e_2,e_3)* equalish(u,e_2). % 18.75/18.91 6772[5:Res:6765.1,13.0] || product(u,e_2,e_2)*+ -> product(e_2,e_2,e_3)* equalish(u,e_2). % 18.75/18.91 6821[6:Spt:6770.0,6770.2] || product(e_2,e_2,u)*+ -> equalish(u,e_2). % 18.75/18.91 6837[7:Spt:6771.0,6771.2] || product(e_2,u,e_2)*+ -> equalish(u,e_2). % 18.75/18.91 6851[8:Spt:6772.0,6772.2] || product(u,e_2,e_2)*+ -> equalish(u,e_2). % 18.75/18.91 6868[9:Spt:1250.1,1250.6,1250.7,1250.8] group_element(u) || -> product(e_1,u,e_3) product(e_1,u,e_2)* equalish(e_1,u). % 18.75/18.91 6895[9:Res:6868.2,6851.0] group_element(e_2) || -> product(e_1,e_2,e_3)* equalish(e_1,e_2) equalish(e_1,e_2). % 18.75/18.91 6909[9:Obv:6895.2] group_element(e_2) || -> product(e_1,e_2,e_3)* equalish(e_1,e_2). % 18.75/18.91 6910[9:SSi:6909.0,2.0] || -> product(e_1,e_2,e_3)* equalish(e_1,e_2). % 18.75/18.91 6911[9:MRR:6910.1,4.0] || -> product(e_1,e_2,e_3)*. % 18.75/18.91 6950[9:Res:6911.0,18.2] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_3) product(e_2,e_1,e_2)* product(e_3,e_1,e_2). % 18.75/18.91 6951[9:Res:6911.0,14.0] || product(e_2,e_1,u)*+ -> product(u,e_3,e_1)*. % 18.75/18.91 6953[9:Res:6911.0,12.0] || product(e_1,u,e_3)*+ -> equalish(u,e_2). % 18.75/18.91 6954[9:Res:6911.0,13.0] || product(u,e_2,e_3)*+ -> equalish(u,e_1). % 18.75/18.91 6962[9:Res:6911.0,3211.1] group_element(e_1) || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1) equalish(e_2,e_1). % 18.75/18.91 6965[9:SSi:6962.0,1.0] || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1) equalish(e_2,e_1). % 18.75/18.91 6966[9:MRR:6965.2,6.0] || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1). % 18.75/18.91 6969[9:SSi:6950.1,6950.0,2.0,1.0] || -> product(e_2,e_1,e_3) product(e_2,e_1,e_2)* product(e_3,e_1,e_2). % 18.75/18.91 6972[10:Spt:6966.0] || -> product(e_1,e_1,e_1)*. % 18.75/18.91 6978[10:Res:6972.0,12.0] || product(e_1,u,e_1)*+ -> equalish(u,e_1). % 18.75/18.91 7209[9:Res:3195.2,6953.0] group_element(e_3) || -> product(e_3,e_3,e_3) product(e_2,e_2,e_3)* equalish(e_1,e_2). % 18.75/18.91 7217[9:SSi:7209.0,3.0] || -> product(e_3,e_3,e_3) product(e_2,e_2,e_3)* equalish(e_1,e_2). % 18.75/18.91 7218[9:MRR:7217.2,4.0] || -> product(e_3,e_3,e_3) product(e_2,e_2,e_3)*. % 18.75/18.91 7224[11:Spt:7218.0] || -> product(e_3,e_3,e_3)*. % 18.75/18.91 7229[11:Res:7224.0,11.0] || product(e_3,e_3,u)*+ -> equalish(u,e_3). % 18.75/18.91 7416[9:Res:10.4,6951.0] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_3) product(e_2,e_1,e_2) product(e_1,e_3,e_1)*. % 18.75/18.91 7422[9:SSi:7416.1,7416.0,2.0,1.0] || -> product(e_2,e_1,e_3) product(e_2,e_1,e_2) product(e_1,e_3,e_1)*. % 18.75/18.91 7507[12:Spt:6969.0] || -> product(e_2,e_1,e_3)*. % 18.75/18.91 7528[12:Res:7507.0,6951.0] || -> product(e_3,e_3,e_1)*. % 18.75/18.91 7543[12:Res:7528.0,7229.0] || -> equalish(e_1,e_3)*. % 18.75/18.91 7557[12:MRR:7543.0,5.0] || -> . % 18.75/18.91 7575[12:Spt:7557.0,6969.0,7507.0] || product(e_2,e_1,e_3)* -> . % 18.75/18.91 7576[12:Spt:7557.0,6969.1,6969.2] || -> product(e_2,e_1,e_2)* product(e_3,e_1,e_2). % 18.75/18.91 7577[12:MRR:7422.0,7575.0] || -> product(e_2,e_1,e_2) product(e_1,e_3,e_1)*. % 18.75/18.91 7590[13:Spt:7576.0] || -> product(e_2,e_1,e_2)*. % 18.75/18.91 7624[13:Res:7590.0,6837.0] || -> equalish(e_1,e_2)*. % 18.75/18.91 7626[13:MRR:7624.0,4.0] || -> . % 18.75/18.91 7643[13:Spt:7626.0,7576.0,7590.0] || product(e_2,e_1,e_2)* -> . % 18.75/18.91 7644[13:Spt:7626.0,7576.1] || -> product(e_3,e_1,e_2)*. % 18.75/18.91 7645[13:MRR:7577.0,7643.0] || -> product(e_1,e_3,e_1)*. % 18.75/18.91 7724[13:Res:7645.0,6978.0] || -> equalish(e_3,e_1)*. % 18.75/18.91 7725[13:MRR:7724.0,8.0] || -> . % 18.75/18.91 7736[11:Spt:7725.0,7218.0,7224.0] || product(e_3,e_3,e_3)* -> . % 18.75/18.91 7737[11:Spt:7725.0,7218.1] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 7771[11:Res:7737.0,6954.0] || -> equalish(e_2,e_1)*. % 18.75/18.91 7777[11:MRR:7771.0,6.0] || -> . % 18.75/18.91 7801[10:Spt:7777.0,6966.0,6972.0] || product(e_1,e_1,e_1)* -> . % 18.75/18.91 7802[10:Spt:7777.0,6966.1] || -> product(e_2,e_2,e_1)*. % 18.75/18.91 7833[10:Res:7802.0,6821.0] || -> equalish(e_1,e_2)*. % 18.75/18.91 7847[10:MRR:7833.0,4.0] || -> . % 18.75/18.91 7871[9:Spt:7847.0,1250.0,1250.2,1250.3,1250.4,1250.5] group_element(u) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)*. % 18.75/18.91 7885[9:Fac:7871.2,7871.4] group_element(e_1) || -> product(e_1,e_1,e_3) product(e_1,e_1,e_3) product(e_1,e_1,e_2)*. % 18.75/18.91 7953[9:Obv:7885.1] group_element(e_1) || -> product(e_1,e_1,e_3) product(e_1,e_1,e_2)*. % 18.75/18.91 7954[9:SSi:7953.0,1.0] || -> product(e_1,e_1,e_3) product(e_1,e_1,e_2)*. % 18.75/18.91 8007[10:Spt:6765.0] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 8017[10:Res:8007.0,6821.0] || -> equalish(e_3,e_2)*. % 18.75/18.91 8030[10:MRR:8017.0,9.0] || -> . % 18.75/18.91 8057[10:Spt:8030.0,6765.0,8007.0] || product(e_2,e_2,e_3)*+ -> . % 18.75/18.91 8058[10:Spt:8030.0,6765.1] || -> product(e_2,e_2,e_2)*. % 18.75/18.91 8122[11:Spt:7954.0] || -> product(e_1,e_1,e_3)*. % 18.75/18.91 8129[11:Res:8122.0,13.0] || product(u,e_1,e_3)*+ -> equalish(u,e_1). % 18.75/18.91 8713[7:Res:6155.2,6837.0] group_element(e_2) || -> product(e_2,e_1,e_3)* equalish(e_1,e_2) equalish(e_1,e_2). % 18.75/18.91 8714[7:Obv:8713.2] group_element(e_2) || -> product(e_2,e_1,e_3)* equalish(e_1,e_2). % 18.75/18.91 8715[7:SSi:8714.0,2.0] || -> product(e_2,e_1,e_3)* equalish(e_1,e_2). % 18.75/18.91 8716[7:MRR:8715.1,4.0] || -> product(e_2,e_1,e_3)*. % 18.75/18.91 9035[7:Res:8716.0,12.0] || product(e_2,u,e_3)*+ -> equalish(u,e_1). % 18.75/18.91 9050[11:Res:8716.0,8129.0] || -> equalish(e_2,e_1)*. % 18.75/18.91 9052[11:MRR:9050.0,6.0] || -> . % 18.75/18.91 9063[11:Spt:9052.0,7954.0,8122.0] || product(e_1,e_1,e_3)*+ -> . % 18.75/18.91 9064[11:Spt:9052.0,7954.1] || -> product(e_1,e_1,e_2)*. % 18.75/18.91 9128[11:Res:9064.0,11.0] || product(e_1,e_1,u)*+ -> equalish(u,e_2). % 18.75/18.91 9153[11:Res:9064.0,3210.1] group_element(e_1) || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1) equalish(e_2,e_3). % 18.75/18.91 9196[11:SSi:9153.0,1.0] || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1) equalish(e_2,e_3). % 18.75/18.91 9197[11:MRR:9196.2,7.0] || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1). % 18.75/18.91 9272[12:Spt:9197.0] || -> product(e_1,e_1,e_1)*. % 18.75/18.91 9646[12:Res:9272.0,9128.0] || -> equalish(e_1,e_2)*. % 18.75/18.91 9647[12:MRR:9646.0,4.0] || -> . % 18.75/18.91 9660[12:Spt:9647.0,9197.0,9272.0] || product(e_1,e_1,e_1)* -> . % 18.75/18.91 9661[12:Spt:9647.0,9197.1] || -> product(e_2,e_2,e_1)*. % 18.75/18.91 9680[12:Res:9661.0,6821.0] || -> equalish(e_1,e_2)*. % 18.75/18.91 9695[12:MRR:9680.0,4.0] || -> . % 18.75/18.91 9716[8:Spt:9695.0,6772.1] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 9755[8:Res:9716.0,9035.0] || -> equalish(e_2,e_1)*. % 18.75/18.91 9757[8:MRR:9755.0,6.0] || -> . % 18.75/18.91 9790[7:Spt:9757.0,6771.1] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 9878[7:Res:9790.0,6821.0] || -> equalish(e_3,e_2)*. % 18.75/18.91 9892[7:MRR:9878.0,9.0] || -> . % 18.75/18.91 9908[6:Spt:9892.0,6770.1] || -> product(e_2,e_2,e_3)*. % 18.75/18.91 9912[6:Res:9908.0,14.0] || product(e_2,e_2,u)*+ -> product(u,e_3,e_2)*. % 18.75/18.91 9946[7:Spt:1250.1,1250.6,1250.7,1250.8] group_element(u) || -> product(e_1,u,e_3) product(e_1,u,e_2)* equalish(e_1,u). % 18.75/18.91 10092[6:Res:9908.0,9912.0] || -> product(e_3,e_3,e_2)*. % 18.75/18.91 10241[6:Res:10092.0,12.0] || product(e_3,u,e_2)*+ -> equalish(u,e_3). % 18.75/18.91 10242[6:Res:10092.0,13.0] || product(u,e_3,e_2)*+ -> equalish(u,e_3). % 18.75/18.91 10320[6:Res:6155.2,10241.0] group_element(e_3) || -> product(e_3,e_1,e_3)* equalish(e_1,e_3) equalish(e_1,e_3). % 18.75/18.91 10322[6:Obv:10320.2] group_element(e_3) || -> product(e_3,e_1,e_3)* equalish(e_1,e_3). % 18.75/18.91 10323[6:SSi:10322.0,3.0] || -> product(e_3,e_1,e_3)* equalish(e_1,e_3). % 18.75/18.91 10324[6:MRR:10323.1,5.0] || -> product(e_3,e_1,e_3)*. % 18.75/18.91 10338[6:Res:10324.0,14.0] || product(e_1,e_3,u)*+ -> product(u,e_3,e_3)*. % 18.75/18.91 10340[6:Res:10324.0,12.0] || product(e_3,u,e_3)*+ -> equalish(u,e_1). % 18.75/18.91 10573[7:Res:9946.2,10242.0] group_element(e_3) || -> product(e_1,e_3,e_3)* equalish(e_1,e_3) equalish(e_1,e_3). % 18.75/18.91 10575[7:Obv:10573.2] group_element(e_3) || -> product(e_1,e_3,e_3)* equalish(e_1,e_3). % 18.75/18.91 10576[7:SSi:10575.0,3.0] || -> product(e_1,e_3,e_3)* equalish(e_1,e_3). % 18.75/18.91 10577[7:MRR:10576.1,5.0] || -> product(e_1,e_3,e_3)*. % 22.05/22.22 10674[0:Fac:1299.4,1299.9] group_element(e_1) group_element(e_2) group_element(e_2) || -> product(e_2,e_1,e_3) product(e_2,e_2,e_3) equalish(e_1,e_2) product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_2)*. % 22.05/22.22 10826[0:Obv:10674.4] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_3) equalish(e_1,e_2) product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_2)*. % 22.05/22.22 11480[6:Res:10.4,10338.0] group_element(e_3) group_element(e_1) || -> product(e_1,e_3,e_3) product(e_1,e_3,e_2)* product(e_1,e_3,e_3). % 22.05/22.22 11498[7:Res:10577.0,10338.0] || -> product(e_3,e_3,e_3)*. % 22.05/22.22 11499[6:Obv:11480.2] group_element(e_3) group_element(e_1) || -> product(e_1,e_3,e_2)* product(e_1,e_3,e_3). % 22.05/22.22 11525[7:Res:11498.0,10340.0] || -> equalish(e_3,e_1)*. % 22.05/22.22 11528[7:MRR:11525.0,8.0] || -> . % 22.05/22.22 11557[7:Spt:11528.0,1250.0,1250.2,1250.3,1250.4,1250.5] group_element(u) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)*. % 22.05/22.22 11558[6:SSi:11499.1,11499.0,1.0,3.0] || -> product(e_1,e_3,e_2)* product(e_1,e_3,e_3). % 22.05/22.22 11738[8:Spt:11558.0] || -> product(e_1,e_3,e_2)*. % 22.05/22.22 11766[8:Res:11738.0,10242.0] || -> equalish(e_1,e_3)*. % 22.05/22.22 11775[8:MRR:11766.0,5.0] || -> . % 22.05/22.22 11812[8:Spt:11775.0,11558.0,11738.0] || product(e_1,e_3,e_2)*+ -> . % 22.05/22.22 11813[8:Spt:11775.0,11558.1] || -> product(e_1,e_3,e_3)*. % 22.05/22.22 11835[8:Res:11813.0,10338.0] || -> product(e_3,e_3,e_3)*. % 22.05/22.22 11882[8:Res:11835.0,10340.0] || -> equalish(e_3,e_1)*. % 22.05/22.22 11884[8:MRR:11882.0,8.0] || -> . % 22.05/22.22 11915[4:Spt:11884.0,1248.0,1248.2,1248.3,1248.4,1248.5] group_element(u) || -> product(u,e_1,e_3) product(u,e_1,e_2)* product(e_1,u,e_3) product(e_1,u,e_2)*. % 22.05/22.22 11916[0:SSi:10826.1,10826.0,2.0,1.0] || -> product(e_2,e_1,e_3) equalish(e_1,e_2) product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_2)*. % 22.05/22.22 11917[0:MRR:11916.1,4.0] || -> product(e_2,e_1,e_3) product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_2)*. % 22.05/22.22 11959[4:Fac:11915.2,11915.4] group_element(e_1) || -> product(e_1,e_1,e_3) product(e_1,e_1,e_3) product(e_1,e_1,e_2)*. % 22.05/22.22 12028[4:Obv:11959.1] group_element(e_1) || -> product(e_1,e_1,e_3) product(e_1,e_1,e_2)*. % 22.05/22.22 12029[4:SSi:12028.0,1.0] || -> product(e_1,e_1,e_3) product(e_1,e_1,e_2)*. % 22.05/22.22 12087[5:Spt:12029.0] || -> product(e_1,e_1,e_3)*. % 22.05/22.22 12091[5:Res:12087.0,14.0] || product(e_1,e_1,u)*+ -> product(u,e_3,e_1)*. % 22.05/22.22 12093[5:Res:12087.0,12.0] || product(e_1,u,e_3)*+ -> equalish(u,e_1). % 22.05/22.22 12094[5:Res:12087.0,13.0] || product(u,e_1,e_3)*+ -> equalish(u,e_1). % 22.05/22.22 12272[6:Spt:11917.0] || -> product(e_2,e_1,e_3)*. % 22.05/22.22 12581[6:Res:12272.0,12094.0] || -> equalish(e_2,e_1)*. % 22.05/22.22 12587[6:MRR:12581.0,6.0] || -> . % 22.05/22.22 12608[6:Spt:12587.0,11917.0,12272.0] || product(e_2,e_1,e_3)*+ -> . % 22.05/22.22 12609[6:Spt:12587.0,11917.1,11917.2,11917.3] || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_2)*. % 22.05/22.22 12664[7:Spt:12609.0] || -> product(e_2,e_2,e_3)*. % 22.05/22.22 12668[7:Res:12664.0,14.0] || product(e_2,e_2,u)*+ -> product(u,e_3,e_2)*. % 22.05/22.22 12776[5:Res:12087.0,12091.0] || -> product(e_3,e_3,e_1)*. % 22.05/22.22 13047[5:Res:12776.0,11.0] || product(e_3,e_3,u)*+ -> equalish(u,e_1). % 22.05/22.22 13321[7:Res:12664.0,12668.0] || -> product(e_3,e_3,e_2)*. % 22.05/22.22 13336[7:Res:13321.0,13047.0] || -> equalish(e_2,e_1)*. % 22.05/22.22 13363[7:MRR:13336.0,6.0] || -> . % 22.05/22.22 13388[7:Spt:13363.0,12609.0,12664.0] || product(e_2,e_2,e_3)*+ -> . % 22.05/22.22 13389[7:Spt:13363.0,12609.1,12609.2] || -> product(e_2,e_2,e_2) product(e_2,e_1,e_2)*. % 22.05/22.22 13429[8:Spt:13389.0] || -> product(e_2,e_2,e_2)*. % 22.05/22.22 13435[8:Res:13429.0,12.0] || product(e_2,u,e_2)*+ -> equalish(u,e_2). % 22.05/22.22 13436[8:Res:13429.0,13.0] || product(u,e_2,e_2)*+ -> equalish(u,e_2). % 22.05/22.22 13773[8:Res:11915.4,13436.0] group_element(e_2) || -> product(e_2,e_1,e_3) product(e_2,e_1,e_2) product(e_1,e_2,e_3)* equalish(e_1,e_2). % 22.05/22.22 13775[8:SSi:13773.0,2.0] || -> product(e_2,e_1,e_3) product(e_2,e_1,e_2) product(e_1,e_2,e_3)* equalish(e_1,e_2). % 22.05/22.22 13776[8:MRR:13775.0,13775.1,13775.3,12608.0,13435.0,4.0] || -> product(e_1,e_2,e_3)*. % 22.05/22.22 13810[8:Res:13776.0,12093.0] || -> equalish(e_2,e_1)*. % 22.05/22.22 13811[8:MRR:13810.0,6.0] || -> . % 22.05/22.22 13843[8:Spt:13811.0,13389.0,13429.0] || product(e_2,e_2,e_2)* -> . % 22.05/22.22 13844[8:Spt:13811.0,13389.1] || -> product(e_2,e_1,e_2)*. % 22.05/22.22 13888[8:Res:13844.0,1269.1] group_element(e_2) || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2)* equalish(e_2,e_1). % 22.05/22.22 13920[8:SSi:13888.0,2.0] || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2)* equalish(e_2,e_1). % 22.05/22.22 13921[8:MRR:13920.0,13920.2,13388.0,6.0] || -> product(e_2,e_2,e_2)*. % 22.05/22.22 13922[8:MRR:13921.0,13843.0] || -> . % 22.05/22.22 13943[5:Spt:13922.0,12029.0,12087.0] || product(e_1,e_1,e_3)*+ -> . % 22.05/22.22 13944[5:Spt:13922.0,12029.1] || -> product(e_1,e_1,e_2)*. % 22.05/22.22 14091[5:Res:13944.0,11.0] || product(e_1,e_1,u)*+ -> equalish(u,e_2). % 22.05/22.22 14092[5:Res:13944.0,12.0] || product(e_1,u,e_2)*+ -> equalish(u,e_1). % 22.05/22.22 14116[5:Res:13944.0,3210.1] group_element(e_1) || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1) equalish(e_2,e_3). % 22.05/22.22 14212[5:SSi:14116.0,1.0] || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1) equalish(e_2,e_3). % 22.05/22.22 14213[5:MRR:14212.2,7.0] || -> product(e_1,e_1,e_1)* product(e_2,e_2,e_1). % 22.05/22.22 14247[5:Res:3195.2,13943.0] group_element(e_3) || -> product(e_3,e_3,e_3) product(e_2,e_2,e_3)*. % 22.05/22.22 14249[5:Res:1257.3,13943.0] group_element(e_3) group_element(u) || -> product(e_3,u,e_3) product(u,e_3,e_3) product(u,e_3,e_2)* product(e_2,e_1,u)*. % 22.05/22.22 14255[5:SSi:14247.0,3.0] || -> product(e_3,e_3,e_3) product(e_2,e_2,e_3)*. % 22.05/22.22 14262[5:SSi:14249.0,3.0] group_element(u) || -> product(e_3,u,e_3) product(u,e_3,e_3) product(u,e_3,e_2)* product(e_2,e_1,u)*. % 22.05/22.22 14387[6:Spt:14213.0] || -> product(e_1,e_1,e_1)*. % 22.05/22.22 14505[6:Res:14387.0,14091.0] || -> equalish(e_1,e_2)*. % 22.05/22.22 14506[6:MRR:14505.0,4.0] || -> . % 22.05/22.22 14520[6:Spt:14506.0,14213.0,14387.0] || product(e_1,e_1,e_1)*+ -> . % 22.05/22.22 14521[6:Spt:14506.0,14213.1] || -> product(e_2,e_2,e_1)*. % 22.05/22.22 14558[6:Res:14521.0,14.0] || product(e_2,e_2,u)*+ -> product(u,e_1,e_2)*. % 22.05/22.22 14559[6:Res:14521.0,11.0] || product(e_2,e_2,u)*+ -> equalish(u,e_1). % 22.05/22.22 14579[6:MRR:11917.2,14558.0] || -> product(e_2,e_1,e_3) product(e_2,e_2,e_3) product(e_2,e_1,e_2)*. % 22.05/22.22 14678[7:Spt:14255.0] || -> product(e_3,e_3,e_3)*. % 22.05/22.22 14684[7:Res:14678.0,12.0] || product(e_3,u,e_3)*+ -> equalish(u,e_3). % 22.05/22.22 14685[7:Res:14678.0,13.0] || product(u,e_3,e_3)*+ -> equalish(u,e_3). % 22.05/22.22 14813[8:Spt:14579.0] || -> product(e_2,e_1,e_3)*. % 22.05/22.22 14818[8:Res:14813.0,11.0] || product(e_2,e_1,u)*+ -> equalish(u,e_3). % 22.05/22.22 14999[8:Res:14262.4,14818.0] group_element(u) || -> product(e_3,u,e_3)* product(u,e_3,e_3) product(u,e_3,e_2)* equalish(u,e_3). % 22.05/22.22 15000[8:MRR:14999.1,14999.2,14684.0,14685.0] group_element(u) || -> product(u,e_3,e_2)* equalish(u,e_3). % 22.05/22.22 15266[8:Res:15000.1,14092.0] group_element(e_1) || -> equalish(e_1,e_3)* equalish(e_3,e_1). % 22.05/22.22 15274[8:SSi:15266.0,1.0] || -> equalish(e_1,e_3)* equalish(e_3,e_1). % 22.05/22.22 15275[8:MRR:15274.0,15274.1,5.0,8.0] || -> . % 22.05/22.22 15321[8:Spt:15275.0,14579.0,14813.0] || product(e_2,e_1,e_3)* -> . % 22.05/22.22 15322[8:Spt:15275.0,14579.1,14579.2] || -> product(e_2,e_2,e_3) product(e_2,e_1,e_2)*. % 22.05/22.22 15403[9:Spt:15322.0] || -> product(e_2,e_2,e_3)*. % 22.05/22.22 15414[9:Res:15403.0,14559.0] || -> equalish(e_3,e_1)*. % 22.05/22.22 15428[9:MRR:15414.0,8.0] || -> . % 22.05/22.22 15445[9:Spt:15428.0,15322.0,15403.0] || product(e_2,e_2,e_3)* -> . % 22.05/22.22 15446[9:Spt:15428.0,15322.1] || -> product(e_2,e_1,e_2)*. % 22.05/22.22 15464[9:Res:15446.0,1269.1] group_element(e_2) || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2)* equalish(e_2,e_1). % 22.05/22.22 15504[9:SSi:15464.0,2.0] || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2)* equalish(e_2,e_1). % 22.05/22.22 15505[9:MRR:15504.1,15504.2,14559.0,6.0] || -> product(e_2,e_2,e_3)*. % 22.05/22.22 15506[9:MRR:15505.0,15445.0] || -> . % 22.05/22.22 15521[7:Spt:15506.0,14255.0,14678.0] || product(e_3,e_3,e_3)* -> . % 22.05/22.22 15522[7:Spt:15506.0,14255.1] || -> product(e_2,e_2,e_3)*. % 22.05/22.22 15550[7:Res:15522.0,14559.0] || -> equalish(e_3,e_1)*. % 22.05/22.22 15564[7:MRR:15550.0,8.0] || -> . % 22.05/22.22 % SZS output end Refutation % 22.05/22.22 Formulae used in the proof : element_1 element_2 element_3 e_1_is_not_e_2 e_1_is_not_e_3 e_2_is_not_e_1 e_2_is_not_e_3 e_3_is_not_e_1 e_3_is_not_e_2 product_total_function1 product_total_function2 product_right_cancellation product_left_cancellation qg4 % 22.05/22.22 %------------------------------------------------------------------------------