%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP130-4.003 : TPTP v8.1.0. Bugfixed v1.2.1. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:47 EDT 2022 % Result : Unsatisfiable 13.85s 14.06s % Output : Refutation 14.95s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP130-4.003 : TPTP v8.1.0. Bugfixed v1.2.1. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n013.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 : Tue Jun 14 05:05:44 EDT 2022 % 0.13/0.34 % CPUTime : % 13.85/14.06 % 13.85/14.06 SPASS V 3.9 % 13.85/14.06 SPASS beiseite: Proof found. % 13.85/14.06 % SZS status Theorem % 13.85/14.06 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 13.85/14.06 SPASS derived 7234 clauses, backtracked 5158 clauses, performed 72 splits and kept 9619 clauses. % 13.85/14.06 SPASS allocated 84563 KBytes. % 13.85/14.06 SPASS spent 0:0:13.69 on the problem. % 13.85/14.06 0:00:00.03 for the input. % 13.85/14.06 0:00:00.00 for the FLOTTER CNF translation. % 13.85/14.06 0:00:00.08 for inferences. % 13.85/14.06 0:00:00.09 for the backtracking. % 13.85/14.06 0:0:13.45 for the reduction. % 13.85/14.06 % 13.85/14.06 % 13.85/14.06 Here is a proof with depth 16, length 344 : % 13.85/14.06 % SZS output start Refutation % 13.85/14.06 1[0:Inp] group_element(u) group_element(v) || -> product(e_3,v,u) product(e_2,v,u) product(e_1,v,u)*. % 13.85/14.06 2[0:Inp] group_element(u) group_element(v) || -> product(v,e_3,u) product(v,e_2,u) product(v,e_1,u)*. % 13.85/14.06 3[0:Inp] || -> group_element(e_1)*. % 13.85/14.06 4[0:Inp] || -> group_element(e_2)*. % 13.85/14.06 5[0:Inp] || -> group_element(e_3)*. % 13.85/14.06 6[0:Inp] || equalish(e_1,e_2)*+ -> . % 13.85/14.06 7[0:Inp] || equalish(e_1,e_3)*+ -> . % 13.85/14.06 8[0:Inp] || equalish(e_2,e_1)*+ -> . % 13.85/14.06 9[0:Inp] || equalish(e_2,e_3)*+ -> . % 13.85/14.06 10[0:Inp] || equalish(e_3,e_1)*+ -> . % 13.85/14.06 11[0:Inp] || equalish(e_3,e_2)*+ -> . % 13.85/14.06 12[0:Inp] group_element(u) group_element(v) || -> product(v,u,e_3) product(v,u,e_2) product(v,u,e_1)*. % 13.85/14.06 13[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 13.85/14.06 14[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 13.85/14.06 15[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 13.85/14.06 16[0:Inp] || product(u,v,w)*+ product(w,x,u)* -> product(u,x,v)*. % 13.85/14.06 17[0:Inp] || product(u,v,w)*+ product(x,v,u)* -> product(u,w,x)*. % 13.85/14.06 18[0:Inp] || product(u,v,w)*+ product(u,x,v)* -> product(w,x,u)*. % 13.85/14.06 23[0:Res:1.4,17.0] group_element(u) group_element(v) || product(w,v,e_1)*+ -> product(e_3,v,u) product(e_2,v,u)* product(e_1,u,w)*. % 13.85/14.06 27[0:Res:1.4,15.0] group_element(u) group_element(v) || product(w,v,u)*+ -> product(e_3,v,u) product(e_2,v,u)* equalish(w,e_1). % 13.85/14.06 28[0:Res:2.4,16.0] group_element(u) group_element(v) || product(u,w,v)*+ -> product(v,e_3,u) product(v,e_2,u)* product(v,w,e_1)*. % 13.85/14.06 32[0:Res:2.4,14.0] group_element(u) group_element(v) || product(v,w,u)*+ -> product(v,e_3,u) product(v,e_2,u)* equalish(w,e_1). % 13.85/14.06 34[0:Res:12.4,16.0] group_element(u) group_element(v) || product(e_1,w,v)*+ -> product(v,u,e_3) product(v,u,e_2)* product(v,w,u)*. % 13.85/14.06 35[0:Res:12.4,17.0] group_element(u) group_element(v) || product(w,u,v)*+ -> product(v,u,e_3) product(v,u,e_2)* product(v,e_1,w)*. % 13.85/14.06 36[0:Res:12.4,18.0] group_element(u) group_element(v) || product(v,w,u)*+ -> product(v,u,e_3) product(v,u,e_2)* product(e_1,w,v)*. % 13.85/14.06 40[0:Res:1.4,27.2] group_element(u) group_element(v) group_element(u) group_element(v) || -> product(e_3,v,u) product(e_2,v,u)* product(e_3,v,u) product(e_2,v,u)* equalish(e_1,e_1). % 13.85/14.06 47[0:Obv:40.5] group_element(u) group_element(v) || -> product(e_3,v,u) product(e_2,v,u)* equalish(e_1,e_1). % 13.85/14.06 56[1:Spt:47.0,47.1,47.2,47.3] group_element(u) group_element(v) || -> product(e_3,v,u) product(e_2,v,u)*. % 13.85/14.06 58[1:Res:56.3,17.0] group_element(u) group_element(v) || product(w,v,e_2)*+ -> product(e_3,v,u)* product(e_2,u,w)*. % 13.85/14.06 60[1:Res:56.3,13.0] group_element(u) group_element(v) || product(e_2,v,w)*+ -> product(e_3,v,u)* equalish(w,u)*. % 13.85/14.06 62[1:Res:56.3,15.0] group_element(u) group_element(v) || product(w,v,u)*+ -> product(e_3,v,u)* equalish(w,e_2). % 13.85/14.06 77[1:Res:56.3,62.2] group_element(u) group_element(v) group_element(u) group_element(v) || -> product(e_3,v,u)* product(e_3,v,u)* equalish(e_2,e_2). % 13.85/14.06 80[1:Obv:77.4] group_element(u) group_element(v) || -> product(e_3,v,u)* equalish(e_2,e_2). % 13.85/14.06 93[2:Spt:80.0,80.1,80.2] group_element(u) group_element(v) || -> product(e_3,v,u)*. % 13.85/14.06 97[2:Res:93.2,13.0] group_element(u) group_element(v) || product(e_3,v,w)*+ -> equalish(w,u)*. % 13.85/14.06 104[2:Res:93.2,97.2] group_element(u) group_element(v) group_element(w) group_element(v) || -> equalish(u,w)*. % 13.85/14.06 107[2:Obv:104.1] group_element(u) group_element(v) group_element(w) || -> equalish(u,v)*. % 13.85/14.06 108[2:Con:107.2] group_element(u) group_element(v) || -> equalish(u,v)*. % 13.85/14.06 115[2:Res:108.2,6.0] group_element(e_1) group_element(e_2) || -> . % 13.85/14.06 121[2:SSi:115.1,115.0,4.0,3.0] || -> . % 13.85/14.06 122[2:Spt:121.0,80.3] || -> equalish(e_2,e_2)*. % 13.85/14.06 132[0:Res:2.4,32.2] group_element(u) group_element(v) group_element(u) group_element(v) || -> product(v,e_3,u) product(v,e_2,u)* product(v,e_3,u) product(v,e_2,u)* equalish(e_1,e_1). % 13.85/14.06 138[0:Obv:132.5] group_element(u) group_element(v) || -> product(v,e_3,u) product(v,e_2,u)* equalish(e_1,e_1). % 13.85/14.06 139[3:Spt:138.0,138.1,138.2,138.3] group_element(u) group_element(v) || -> product(v,e_3,u) product(v,e_2,u)*. % 13.85/14.06 1359[1:Res:56.3,58.2] group_element(e_2) group_element(u) group_element(v) group_element(u) || -> product(e_3,u,e_2)* product(e_3,u,v)* product(e_2,v,e_2)*. % 13.85/14.06 1361[3:Res:139.3,58.2] group_element(e_2) group_element(u) group_element(v) group_element(e_2) || -> product(u,e_3,e_2)* product(e_3,e_2,v) product(e_2,v,u)*. % 13.85/14.06 1381[3:Obv:1361.0] group_element(u) group_element(v) group_element(e_2) || -> product(u,e_3,e_2)* product(e_3,e_2,v) product(e_2,v,u)*. % 13.85/14.06 1382[3:SSi:1381.2,4.0] group_element(u) group_element(v) || -> product(u,e_3,e_2)* product(e_3,e_2,v) product(e_2,v,u)*. % 13.85/14.06 1383[1:Obv:1359.1] group_element(e_2) group_element(u) group_element(v) || -> product(e_3,v,e_2)* product(e_3,v,u)* product(e_2,u,e_2)*. % 13.85/14.06 1384[1:SSi:1383.0,4.0] group_element(u) group_element(v) || -> product(e_3,v,e_2)* product(e_3,v,u)* product(e_2,u,e_2)*. % 13.85/14.06 1412[3:Fac:1382.2,1382.4] group_element(e_2) group_element(e_3) || -> product(e_3,e_2,e_3) product(e_2,e_3,e_2)*. % 13.85/14.06 1447[3:SSi:1412.1,1412.0,5.0,4.0] || -> product(e_3,e_2,e_3) product(e_2,e_3,e_2)*. % 13.85/14.06 1477[4:Spt:1447.0] || -> product(e_3,e_2,e_3)*. % 13.85/14.06 1478[4:Res:1477.0,16.0] || product(e_3,u,e_3)+ -> product(e_3,u,e_2)*. % 13.85/14.06 1481[4:Res:1477.0,13.0] || product(e_3,e_2,u)*+ -> equalish(u,e_3). % 13.85/14.06 1603[4:Res:1477.0,1478.0] || -> product(e_3,e_2,e_2)*. % 13.85/14.06 1682[4:Res:1603.0,1481.0] || -> equalish(e_2,e_3)*. % 13.85/14.06 1688[4:MRR:1682.0,9.0] || -> . % 13.85/14.06 1699[4:Spt:1688.0,1447.0,1477.0] || product(e_3,e_2,e_3)*+ -> . % 13.85/14.06 1700[4:Spt:1688.0,1447.1] || -> product(e_2,e_3,e_2)*. % 13.85/14.06 1729[4:Res:1700.0,13.0] || product(e_2,e_3,u)*+ -> equalish(u,e_2). % 13.85/14.06 1731[4:Res:1700.0,15.0] || product(u,e_3,e_2)* -> equalish(u,e_2). % 13.85/14.06 1795[4:Res:1382.4,1729.0] group_element(u) group_element(e_3) || -> product(u,e_3,e_2)* product(e_3,e_2,e_3)* equalish(u,e_2). % 13.85/14.06 1815[4:SSi:1795.1,5.0] group_element(u) || -> product(u,e_3,e_2)* product(e_3,e_2,e_3)* equalish(u,e_2). % 13.85/14.06 1816[4:MRR:1815.2,1699.0] group_element(u) || -> product(u,e_3,e_2)* equalish(u,e_2). % 13.85/14.06 1817[4:MRR:1816.1,1731.0] group_element(u) || -> equalish(u,e_2)*. % 13.85/14.06 1839[4:Res:1817.1,6.0] group_element(e_1) || -> . % 13.85/14.06 1841[4:SSi:1839.0,3.0] || -> . % 13.85/14.06 1842[3:Spt:1841.0,138.4] || -> equalish(e_1,e_1)*. % 13.85/14.06 1855[1:Fac:1384.2,1384.3] group_element(e_2) group_element(u) || -> product(e_3,u,e_2)* product(e_2,e_2,e_2)*. % 13.85/14.06 1889[1:SSi:1855.0,4.0] group_element(u) || -> product(e_3,u,e_2)* product(e_2,e_2,e_2)*. % 13.85/14.06 1906[4:Spt:1889.0,1889.1] group_element(u) || -> product(e_3,u,e_2)*. % 13.85/14.06 1911[4:Res:1906.1,14.0] group_element(u) || product(e_3,v,e_2)*+ -> equalish(v,u)*. % 13.85/14.06 1958[4:Res:1906.1,1911.1] group_element(u) group_element(v) || -> equalish(u,v)*. % 13.85/14.06 1964[4:Res:1958.2,6.0] group_element(e_1) group_element(e_2) || -> . % 13.85/14.06 1970[4:SSi:1964.1,1964.0,4.0,3.0] || -> . % 13.85/14.06 1971[4:Spt:1970.0,1889.2] || -> product(e_2,e_2,e_2)*. % 13.85/14.06 1977[4:Res:1971.0,15.0] || product(u,e_2,e_2)*+ -> equalish(u,e_2). % 13.85/14.06 1978[4:Res:1971.0,60.2] group_element(u) group_element(e_2) || -> product(e_3,e_2,u)* equalish(e_2,u). % 13.85/14.06 1983[4:SSi:1978.1,4.0] group_element(u) || -> product(e_3,e_2,u)* equalish(e_2,u). % 13.85/14.06 2025[4:Res:1983.1,15.0] group_element(u) || product(v,e_2,u)*+ -> equalish(e_2,u) equalish(v,e_3). % 13.85/14.06 2174[4:Res:1983.1,2025.1] group_element(u) group_element(u) || -> equalish(e_2,u)* equalish(e_2,u)* equalish(e_3,e_3). % 13.85/14.06 2175[4:Res:12.4,2025.1] group_element(e_2) group_element(u) group_element(e_1) || -> product(u,e_2,e_3) product(u,e_2,e_2)* equalish(e_2,e_1) equalish(u,e_3). % 13.85/14.06 2181[4:Obv:2174.2] group_element(u) || -> equalish(e_2,u)* equalish(e_3,e_3). % 13.85/14.06 2187[4:SSi:2175.2,2175.0,3.0,4.0] group_element(u) || -> product(u,e_2,e_3) product(u,e_2,e_2)* equalish(e_2,e_1) equalish(u,e_3). % 13.85/14.06 2188[4:MRR:2187.3,8.0] group_element(u) || -> product(u,e_2,e_3) product(u,e_2,e_2)* equalish(u,e_3). % 13.85/14.06 2189[5:Spt:2181.0,2181.1] group_element(u) || -> equalish(e_2,u)*. % 13.85/14.06 2191[5:Res:2189.1,8.0] group_element(e_1) || -> . % 13.85/14.06 2193[5:SSi:2191.0,3.0] || -> . % 13.85/14.06 2194[5:Spt:2193.0,2181.2] || -> equalish(e_3,e_3)*. % 13.85/14.06 2252[4:Res:2188.2,1977.0] group_element(u) || -> product(u,e_2,e_3)* equalish(u,e_3) equalish(u,e_2). % 13.85/14.06 2266[4:Res:2252.1,62.2] group_element(u) group_element(e_3) group_element(e_2) || -> equalish(u,e_3) equalish(u,e_2)* product(e_3,e_2,e_3)* equalish(u,e_2)*. % 13.85/14.06 2270[4:Obv:2266.4] group_element(u) group_element(e_3) group_element(e_2) || -> equalish(u,e_3) product(e_3,e_2,e_3)* equalish(u,e_2)*. % 13.85/14.06 2271[4:SSi:2270.2,2270.1,4.0,5.0] group_element(u) || -> equalish(u,e_3) product(e_3,e_2,e_3)* equalish(u,e_2)*. % 13.85/14.06 2299[6:Spt:2271.0,2271.1,2271.3] group_element(u) || -> equalish(u,e_3) equalish(u,e_2)*. % 13.85/14.06 2301[6:Res:2299.2,6.0] group_element(e_1) || -> equalish(e_1,e_3)*. % 13.85/14.06 2302[6:SSi:2301.0,3.0] || -> equalish(e_1,e_3)*. % 13.85/14.06 2303[6:MRR:2302.0,7.0] || -> . % 13.85/14.06 2304[6:Spt:2303.0,2271.2] || -> product(e_3,e_2,e_3)*. % 13.85/14.06 2305[6:Res:2304.0,16.0] || product(e_3,u,e_3)+ -> product(e_3,u,e_2)*. % 13.85/14.06 2355[6:Res:2304.0,2305.0] || -> product(e_3,e_2,e_2)*. % 13.85/14.06 2370[6:Res:2355.0,1977.0] || -> equalish(e_3,e_2)*. % 13.85/14.06 2372[6:MRR:2370.0,11.0] || -> . % 13.85/14.06 2378[1:Spt:2372.0,47.4] || -> equalish(e_1,e_1)*. % 13.85/14.06 2441[0:Res:2.4,23.2] group_element(e_1) group_element(u) group_element(v) group_element(e_1) || -> product(u,e_3,e_1) product(u,e_2,e_1)* product(e_3,e_1,v) product(e_2,e_1,v) product(e_1,v,u)*. % 13.85/14.06 2444[0:Obv:2441.0] group_element(u) group_element(v) group_element(e_1) || -> product(u,e_3,e_1) product(u,e_2,e_1)* product(e_3,e_1,v) product(e_2,e_1,v) product(e_1,v,u)*. % 13.85/14.06 2445[0:SSi:2444.2,3.0] group_element(u) group_element(v) || -> product(u,e_3,e_1) product(u,e_2,e_1)* product(e_3,e_1,v) product(e_2,e_1,v) product(e_1,v,u)*. % 13.85/14.06 2482[0:Res:12.4,34.2] group_element(u) group_element(e_1) group_element(v) group_element(e_1) || -> product(e_1,u,e_3) product(e_1,u,e_2)* product(e_1,v,e_3) product(e_1,v,e_2)* product(e_1,u,v)*. % 13.85/14.06 2483[0:Obv:2482.1] group_element(u) group_element(v) group_element(e_1) || -> product(e_1,u,e_3) product(e_1,u,e_2)* product(e_1,v,e_3) product(e_1,v,e_2)* product(e_1,u,v)*. % 13.85/14.06 2484[0:SSi:2483.2,3.0] group_element(u) group_element(v) || -> product(e_1,u,e_3) product(e_1,u,e_2)* product(e_1,v,e_3) product(e_1,v,e_2)* product(e_1,u,v)*. % 13.85/14.06 4181[0:Fac:2445.3,2445.6] group_element(e_1) group_element(e_2) || -> product(e_1,e_3,e_1) product(e_3,e_1,e_2) product(e_2,e_1,e_2) product(e_1,e_2,e_1)*. % 13.85/14.06 4231[0:SSi:4181.1,4181.0,4.0,3.0] || -> product(e_1,e_3,e_1) product(e_3,e_1,e_2) product(e_2,e_1,e_2) product(e_1,e_2,e_1)*. % 13.85/14.06 6612[2:Spt:4231.0] || -> product(e_1,e_3,e_1)*. % 13.85/14.06 6613[2:Res:6612.0,16.0] || product(e_1,u,e_1)*+ -> product(e_1,u,e_3). % 13.85/14.06 6616[2:Res:6612.0,13.0] || product(e_1,e_3,u)*+ -> equalish(u,e_1). % 13.85/14.06 6698[0:Fac:2484.5,2484.6] group_element(e_2) group_element(e_2) || -> product(e_1,e_2,e_3) product(e_1,e_2,e_2)* product(e_1,e_2,e_3) product(e_1,e_2,e_2)*. % 13.85/14.06 6761[0:Obv:6698.3] group_element(e_2) || -> product(e_1,e_2,e_3) product(e_1,e_2,e_2)*. % 13.85/14.06 6762[0:SSi:6761.0,4.0] || -> product(e_1,e_2,e_3) product(e_1,e_2,e_2)*. % 13.85/14.06 7339[2:Res:6612.0,6613.0] || -> product(e_1,e_3,e_3)*. % 13.85/14.06 7361[2:Res:7339.0,6616.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 7368[2:MRR:7361.0,10.0] || -> . % 13.85/14.06 7397[2:Spt:7368.0,4231.0,6612.0] || product(e_1,e_3,e_1)*+ -> . % 13.85/14.06 7398[2:Spt:7368.0,4231.1,4231.2,4231.3] || -> product(e_3,e_1,e_2) product(e_2,e_1,e_2) product(e_1,e_2,e_1)*. % 13.85/14.06 7466[3:Spt:7398.0] || -> product(e_3,e_1,e_2)*. % 13.85/14.06 7470[3:Res:7466.0,13.0] || product(e_3,e_1,u)*+ -> equalish(u,e_2). % 13.85/14.06 7471[3:Res:7466.0,14.0] || product(e_3,u,e_2)*+ -> equalish(u,e_1). % 13.85/14.06 7472[3:Res:7466.0,15.0] || product(u,e_1,e_2)*+ -> equalish(u,e_3). % 13.85/14.06 7476[3:Res:7466.0,36.2] group_element(e_2) group_element(e_3) || -> product(e_3,e_2,e_3) product(e_3,e_2,e_2) product(e_1,e_1,e_3)*. % 13.85/14.06 7481[3:Res:7466.0,35.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_2,e_1,e_3). % 13.85/14.06 7485[3:SSi:7476.1,7476.0,5.0,4.0] || -> product(e_3,e_2,e_3) product(e_3,e_2,e_2) product(e_1,e_1,e_3)*. % 13.85/14.06 7488[3:Obv:7481.2] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_2)* product(e_2,e_1,e_3). % 13.85/14.06 7489[3:SSi:7488.1,7488.0,4.0,3.0] || -> product(e_2,e_1,e_2)* product(e_2,e_1,e_3). % 13.85/14.06 7490[2:Res:1.4,7397.0] group_element(e_1) group_element(e_3) || -> product(e_3,e_3,e_1) product(e_2,e_3,e_1)*. % 13.85/14.06 7491[2:Res:12.4,7397.0] group_element(e_3) group_element(e_1) || -> product(e_1,e_3,e_3) product(e_1,e_3,e_2)*. % 13.85/14.06 7494[2:SSi:7490.1,7490.0,5.0,3.0] || -> product(e_3,e_3,e_1) product(e_2,e_3,e_1)*. % 13.85/14.06 7495[2:SSi:7491.1,7491.0,3.0,5.0] || -> product(e_1,e_3,e_3) product(e_1,e_3,e_2)*. % 13.85/14.06 7497[4:Spt:6762.0] || -> product(e_1,e_2,e_3)*. % 13.85/14.06 7502[4:Res:7497.0,14.0] || product(e_1,u,e_3)*+ -> equalish(u,e_2). % 13.85/14.06 7537[5:Spt:7494.0] || -> product(e_3,e_3,e_1)*. % 13.85/14.06 7541[5:Res:7537.0,13.0] || product(e_3,e_3,u)*+ -> equalish(u,e_1). % 13.85/14.06 7561[6:Spt:7489.0] || -> product(e_2,e_1,e_2)*. % 13.85/14.06 7713[6:Res:7561.0,7472.0] || -> equalish(e_2,e_3)*. % 13.85/14.06 7715[6:MRR:7713.0,9.0] || -> . % 13.85/14.06 7725[6:Spt:7715.0,7489.0,7561.0] || product(e_2,e_1,e_2)*+ -> . % 13.85/14.06 7726[6:Spt:7715.0,7489.1] || -> product(e_2,e_1,e_3)*. % 13.85/14.06 7731[6:Res:7726.0,14.0] || product(e_2,u,e_3)*+ -> equalish(u,e_1). % 13.85/14.06 7768[7:Spt:7495.0] || -> product(e_1,e_3,e_3)*. % 13.85/14.06 7861[7:Res:7768.0,7502.0] || -> equalish(e_3,e_2)*. % 13.85/14.06 7862[7:MRR:7861.0,11.0] || -> . % 13.85/14.06 7864[7:Spt:7862.0,7495.0,7768.0] || product(e_1,e_3,e_3)*+ -> . % 13.85/14.06 7865[7:Spt:7862.0,7495.1] || -> product(e_1,e_3,e_2)*. % 13.85/14.06 7908[7:Res:1.4,7864.0] group_element(e_3) group_element(e_3) || -> product(e_3,e_3,e_3) product(e_2,e_3,e_3)*. % 13.85/14.06 7910[7:Obv:7908.0] group_element(e_3) || -> product(e_3,e_3,e_3) product(e_2,e_3,e_3)*. % 13.85/14.06 7911[7:SSi:7910.0,5.0] || -> product(e_3,e_3,e_3) product(e_2,e_3,e_3)*. % 13.85/14.06 7942[8:Spt:7911.0] || -> product(e_3,e_3,e_3)*. % 13.85/14.06 7972[8:Res:7942.0,7541.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 7973[8:MRR:7972.0,10.0] || -> . % 13.85/14.06 7975[8:Spt:7973.0,7911.0,7942.0] || product(e_3,e_3,e_3)*+ -> . % 13.85/14.06 7976[8:Spt:7973.0,7911.1] || -> product(e_2,e_3,e_3)*. % 13.85/14.06 8118[8:Res:7976.0,7731.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 8119[8:MRR:8118.0,10.0] || -> . % 13.85/14.06 8120[5:Spt:8119.0,7494.0,7537.0] || product(e_3,e_3,e_1)*+ -> . % 13.85/14.06 8121[5:Spt:8119.0,7494.1] || -> product(e_2,e_3,e_1)*. % 13.85/14.06 8127[5:Res:8121.0,13.0] || product(e_2,e_3,u)*+ -> equalish(u,e_1). % 13.85/14.06 8203[6:Spt:7489.0] || -> product(e_2,e_1,e_2)*. % 13.85/14.06 8211[6:Res:8203.0,7472.0] || -> equalish(e_2,e_3)*. % 13.85/14.06 8220[6:MRR:8211.0,9.0] || -> . % 13.85/14.06 8237[6:Spt:8220.0,7489.0,8203.0] || product(e_2,e_1,e_2)*+ -> . % 13.85/14.06 8238[6:Spt:8220.0,7489.1] || -> product(e_2,e_1,e_3)*. % 13.85/14.06 8248[6:Res:8238.0,36.2] group_element(e_3) group_element(e_2) || -> product(e_2,e_3,e_3) product(e_2,e_3,e_2) product(e_1,e_1,e_2)*. % 13.85/14.06 8264[6:SSi:8248.1,8248.0,4.0,5.0] || -> product(e_2,e_3,e_3) product(e_2,e_3,e_2) product(e_1,e_1,e_2)*. % 13.85/14.06 8269[6:Res:2.4,8237.0] group_element(e_2) group_element(e_2) || -> product(e_2,e_3,e_2) product(e_2,e_2,e_2)*. % 13.85/14.06 8277[6:Obv:8269.0] group_element(e_2) || -> product(e_2,e_3,e_2) product(e_2,e_2,e_2)*. % 13.85/14.06 8278[6:SSi:8277.0,4.0] || -> product(e_2,e_3,e_2) product(e_2,e_2,e_2)*. % 13.85/14.06 8367[7:Spt:8278.0] || -> product(e_2,e_3,e_2)*. % 13.85/14.06 8434[7:Res:8367.0,8127.0] || -> equalish(e_2,e_1)*. % 13.85/14.06 8435[7:MRR:8434.0,8.0] || -> . % 13.85/14.06 8437[7:Spt:8435.0,8278.0,8367.0] || product(e_2,e_3,e_2)*+ -> . % 13.85/14.06 8438[7:Spt:8435.0,8278.1] || -> product(e_2,e_2,e_2)*. % 13.85/14.06 8439[7:MRR:8264.1,8437.0] || -> product(e_2,e_3,e_3) product(e_1,e_1,e_2)*. % 13.85/14.06 8459[8:Spt:8439.0] || -> product(e_2,e_3,e_3)*. % 13.85/14.06 8472[8:Res:8459.0,8127.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 8473[8:MRR:8472.0,10.0] || -> . % 13.85/14.06 8479[8:Spt:8473.0,8439.0,8459.0] || product(e_2,e_3,e_3)* -> . % 13.85/14.06 8480[8:Spt:8473.0,8439.1] || -> product(e_1,e_1,e_2)*. % 13.85/14.06 8490[8:Res:8480.0,7472.0] || -> equalish(e_1,e_3)*. % 13.85/14.06 8502[8:MRR:8490.0,7.0] || -> . % 13.85/14.06 8516[4:Spt:8502.0,6762.0,7497.0] || product(e_1,e_2,e_3)*+ -> . % 13.85/14.06 8517[4:Spt:8502.0,6762.1] || -> product(e_1,e_2,e_2)*. % 13.85/14.06 8558[4:Res:1.4,8516.0] group_element(e_3) group_element(e_2) || -> product(e_3,e_2,e_3) product(e_2,e_2,e_3)*. % 13.85/14.06 8562[4:SSi:8558.1,8558.0,4.0,5.0] || -> product(e_3,e_2,e_3) product(e_2,e_2,e_3)*. % 13.85/14.06 8563[5:Spt:7489.0] || -> product(e_2,e_1,e_2)*. % 13.85/14.06 8571[5:Res:8563.0,7472.0] || -> equalish(e_2,e_3)*. % 13.85/14.06 8580[5:MRR:8571.0,9.0] || -> . % 13.85/14.06 8598[5:Spt:8580.0,7489.0,8563.0] || product(e_2,e_1,e_2)*+ -> . % 13.85/14.06 8599[5:Spt:8580.0,7489.1] || -> product(e_2,e_1,e_3)*. % 13.85/14.06 8611[5:Res:8599.0,28.2] group_element(e_2) group_element(e_3) || -> product(e_3,e_3,e_2) product(e_3,e_2,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 8627[5:SSi:8611.1,8611.0,5.0,4.0] || -> product(e_3,e_3,e_2) product(e_3,e_2,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 8641[6:Spt:7495.0] || -> product(e_1,e_3,e_3)*. % 13.85/14.06 8657[6:Res:8641.0,35.2] group_element(e_3) group_element(e_3) || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 8680[6:Obv:8657.0] group_element(e_3) || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 8681[6:SSi:8680.0,5.0] || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 8731[7:Spt:8562.0] || -> product(e_3,e_2,e_3)*. % 13.85/14.06 8732[7:Res:8731.0,16.0] || product(e_3,u,e_3) -> product(e_3,u,e_2)*. % 13.85/14.06 8746[7:MRR:8681.0,8732.0] || -> product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 8862[8:Spt:8746.0] || -> product(e_3,e_3,e_2)*. % 13.85/14.06 8873[8:Res:8862.0,7471.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 8876[8:MRR:8873.0,10.0] || -> . % 13.85/14.06 8883[8:Spt:8876.0,8746.0,8862.0] || product(e_3,e_3,e_2)* -> . % 13.85/14.06 8884[8:Spt:8876.0,8746.1] || -> product(e_3,e_1,e_1)*. % 13.85/14.06 8897[8:Res:8884.0,7470.0] || -> equalish(e_1,e_2)*. % 13.85/14.06 8906[8:MRR:8897.0,6.0] || -> . % 13.85/14.06 8947[7:Spt:8906.0,8562.0,8731.0] || product(e_3,e_2,e_3)*+ -> . % 13.85/14.06 8948[7:Spt:8906.0,8562.1] || -> product(e_2,e_2,e_3)*. % 13.85/14.06 8949[7:MRR:7485.0,8947.0] || -> product(e_3,e_2,e_2) product(e_1,e_1,e_3)*. % 13.85/14.06 9049[8:Spt:8949.0] || -> product(e_3,e_2,e_2)*. % 13.85/14.06 9060[8:Res:9049.0,7471.0] || -> equalish(e_2,e_1)*. % 13.85/14.06 9063[8:MRR:9060.0,8.0] || -> . % 13.85/14.06 9068[8:Spt:9063.0,8949.0,9049.0] || product(e_3,e_2,e_2)*+ -> . % 13.85/14.06 9069[8:Spt:9063.0,8949.1] || -> product(e_1,e_1,e_3)*. % 13.85/14.06 9070[8:MRR:8627.1,9068.0] || -> product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 9119[9:Spt:9070.0] || -> product(e_3,e_3,e_2)*. % 13.85/14.06 9130[9:Res:9119.0,7471.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 9133[9:MRR:9130.0,10.0] || -> . % 13.85/14.06 9140[9:Spt:9133.0,9070.0,9119.0] || product(e_3,e_3,e_2)* -> . % 13.85/14.06 9141[9:Spt:9133.0,9070.1] || -> product(e_3,e_1,e_1)*. % 13.85/14.06 9155[9:Res:9141.0,7470.0] || -> equalish(e_1,e_2)*. % 13.85/14.06 9164[9:MRR:9155.0,6.0] || -> . % 13.85/14.06 9198[6:Spt:9164.0,7495.0,8641.0] || product(e_1,e_3,e_3)*+ -> . % 13.85/14.06 9199[6:Spt:9164.0,7495.1] || -> product(e_1,e_3,e_2)*. % 13.85/14.06 9307[7:Spt:8562.0] || -> product(e_3,e_2,e_3)*. % 13.85/14.06 9308[7:Res:9307.0,16.0] || product(e_3,u,e_3) -> product(e_3,u,e_2)*. % 13.85/14.06 9315[7:Res:9307.0,36.2] group_element(e_3) group_element(e_3) || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_1,e_2,e_3)*. % 13.85/14.06 9322[7:Obv:9315.0] group_element(e_3) || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_1,e_2,e_3)*. % 13.85/14.06 9323[7:SSi:9322.0,5.0] || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_1,e_2,e_3)*. % 13.85/14.06 9324[7:MRR:9323.2,8516.0] || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2)*. % 13.85/14.06 9325[7:MRR:9324.0,9308.0] || -> product(e_3,e_3,e_2)*. % 13.85/14.06 9393[7:Res:9325.0,7471.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 9396[7:MRR:9393.0,10.0] || -> . % 13.85/14.06 9402[7:Spt:9396.0,8562.0,9307.0] || product(e_3,e_2,e_3)*+ -> . % 13.85/14.06 9403[7:Spt:9396.0,8562.1] || -> product(e_2,e_2,e_3)*. % 13.85/14.06 9404[7:MRR:7485.0,9402.0] || -> product(e_3,e_2,e_2) product(e_1,e_1,e_3)*. % 13.85/14.06 9498[8:Spt:9404.0] || -> product(e_3,e_2,e_2)*. % 13.85/14.06 9509[8:Res:9498.0,7471.0] || -> equalish(e_2,e_1)*. % 13.85/14.06 9512[8:MRR:9509.0,8.0] || -> . % 13.85/14.06 9516[8:Spt:9512.0,9404.0,9498.0] || product(e_3,e_2,e_2)*+ -> . % 13.85/14.06 9517[8:Spt:9512.0,9404.1] || -> product(e_1,e_1,e_3)*. % 13.85/14.06 9518[8:MRR:8627.1,9516.0] || -> product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 9568[9:Spt:9518.0] || -> product(e_3,e_3,e_2)*. % 13.85/14.06 9576[9:Res:9568.0,36.2] group_element(e_2) group_element(e_3) || -> product(e_3,e_2,e_3) product(e_3,e_2,e_2) product(e_1,e_3,e_3)*. % 13.85/14.06 9588[9:SSi:9576.1,9576.0,5.0,4.0] || -> product(e_3,e_2,e_3) product(e_3,e_2,e_2) product(e_1,e_3,e_3)*. % 13.85/14.06 9589[9:MRR:9588.0,9588.1,9588.2,9402.0,9516.0,9198.0] || -> . % 13.85/14.06 9590[9:Spt:9589.0,9518.0,9568.0] || product(e_3,e_3,e_2)* -> . % 13.85/14.06 9591[9:Spt:9589.0,9518.1] || -> product(e_3,e_1,e_1)*. % 13.85/14.06 9606[9:Res:9591.0,7470.0] || -> equalish(e_1,e_2)*. % 13.85/14.06 9615[9:MRR:9606.0,6.0] || -> . % 13.85/14.06 9655[3:Spt:9615.0,7398.0,7466.0] || product(e_3,e_1,e_2)*+ -> . % 13.85/14.06 9656[3:Spt:9615.0,7398.1,7398.2] || -> product(e_2,e_1,e_2) product(e_1,e_2,e_1)*. % 13.85/14.06 9663[4:Spt:9656.0] || -> product(e_2,e_1,e_2)*. % 13.85/14.06 9667[4:Res:9663.0,13.0] || product(e_2,e_1,u)*+ -> equalish(u,e_2). % 13.85/14.06 9668[4:Res:9663.0,14.0] || product(e_2,u,e_2)*+ -> equalish(u,e_1). % 13.85/14.06 9675[4:Res:9663.0,28.2] group_element(e_2) group_element(e_2) || -> product(e_2,e_3,e_2) product(e_2,e_2,e_2) product(e_2,e_1,e_1)*. % 13.85/14.06 9692[4:Obv:9675.0] group_element(e_2) || -> product(e_2,e_3,e_2) product(e_2,e_2,e_2) product(e_2,e_1,e_1)*. % 13.85/14.06 9693[4:SSi:9692.0,4.0] || -> product(e_2,e_3,e_2) product(e_2,e_2,e_2) product(e_2,e_1,e_1)*. % 13.85/14.06 9697[3:Res:2.4,9655.0] group_element(e_2) group_element(e_3) || -> product(e_3,e_3,e_2) product(e_3,e_2,e_2)*. % 13.85/14.06 9703[3:SSi:9697.1,9697.0,5.0,4.0] || -> product(e_3,e_3,e_2) product(e_3,e_2,e_2)*. % 13.85/14.06 9708[5:Spt:7494.0] || -> product(e_3,e_3,e_1)*. % 13.85/14.06 9712[5:Res:9708.0,13.0] || product(e_3,e_3,u)*+ -> equalish(u,e_1). % 13.85/14.06 9713[5:Res:9708.0,14.0] || product(e_3,u,e_1)*+ -> equalish(u,e_3). % 13.85/14.06 9738[6:Spt:7495.0] || -> product(e_1,e_3,e_3)*. % 13.85/14.06 9754[6:Res:9738.0,35.2] group_element(e_3) group_element(e_3) || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 9776[6:Obv:9754.0] group_element(e_3) || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 9777[6:SSi:9776.0,5.0] || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_1)*. % 13.85/14.06 9815[7:Spt:9703.0] || -> product(e_3,e_3,e_2)*. % 13.85/14.06 9954[7:Res:9815.0,9712.0] || -> equalish(e_2,e_1)*. % 13.85/14.06 9955[7:MRR:9954.0,8.0] || -> . % 13.85/14.06 9957[7:Spt:9955.0,9703.0,9815.0] || product(e_3,e_3,e_2)*+ -> . % 13.85/14.06 9958[7:Spt:9955.0,9703.1] || -> product(e_3,e_2,e_2)*. % 13.85/14.06 9959[7:MRR:9777.1,9957.0] || -> product(e_3,e_3,e_3) product(e_3,e_1,e_1)*. % 13.85/14.06 9976[8:Spt:9959.0] || -> product(e_3,e_3,e_3)*. % 13.85/14.06 9989[8:Res:9976.0,9712.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 9990[8:MRR:9989.0,10.0] || -> . % 13.85/14.06 9998[8:Spt:9990.0,9959.0,9976.0] || product(e_3,e_3,e_3)*+ -> . % 13.85/14.06 9999[8:Spt:9990.0,9959.1] || -> product(e_3,e_1,e_1)*. % 13.85/14.06 10124[8:Res:9999.0,9713.0] || -> equalish(e_1,e_3)*. % 13.85/14.06 10125[8:MRR:10124.0,7.0] || -> . % 13.85/14.06 10127[6:Spt:10125.0,7495.0,9738.0] || product(e_1,e_3,e_3)*+ -> . % 13.85/14.06 10128[6:Spt:10125.0,7495.1] || -> product(e_1,e_3,e_2)*. % 13.85/14.06 10172[6:Res:1.4,10127.0] group_element(e_3) group_element(e_3) || -> product(e_3,e_3,e_3) product(e_2,e_3,e_3)*. % 13.85/14.06 10174[6:Obv:10172.0] group_element(e_3) || -> product(e_3,e_3,e_3) product(e_2,e_3,e_3)*. % 13.85/14.06 10175[6:SSi:10174.0,5.0] || -> product(e_3,e_3,e_3) product(e_2,e_3,e_3)*. % 13.85/14.06 10247[7:Spt:9703.0] || -> product(e_3,e_3,e_2)*. % 13.85/14.06 10260[7:Res:10247.0,9712.0] || -> equalish(e_2,e_1)*. % 13.85/14.06 10261[7:MRR:10260.0,8.0] || -> . % 13.85/14.06 10273[7:Spt:10261.0,9703.0,10247.0] || product(e_3,e_3,e_2)*+ -> . % 13.85/14.06 10274[7:Spt:10261.0,9703.1] || -> product(e_3,e_2,e_2)*. % 13.85/14.06 10292[8:Spt:10175.0] || -> product(e_3,e_3,e_3)*. % 13.85/14.06 10305[8:Res:10292.0,9712.0] || -> equalish(e_3,e_1)*. % 13.85/14.06 10306[8:MRR:10305.0,10.0] || -> . % 13.85/14.06 10315[8:Spt:10306.0,10175.0,10292.0] || product(e_3,e_3,e_3)* -> . % 13.85/14.06 10316[8:Spt:10306.0,10175.1] || -> product(e_2,e_3,e_3)*. % 13.85/14.06 10330[8:Res:10316.0,35.2] group_element(e_3) group_element(e_3) || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_2)*. % 13.85/14.06 10332[8:Obv:10330.0] group_element(e_3) || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_2)*. % 13.85/14.06 10333[8:SSi:10332.0,5.0] || -> product(e_3,e_3,e_3) product(e_3,e_3,e_2) product(e_3,e_1,e_2)*. % 13.85/14.06 10334[8:MRR:10333.1,10333.2,10273.0,9655.0] || -> product(e_3,e_3,e_3)*. % 13.85/14.06 10335[8:MRR:10334.0,10315.0] || -> . % 13.85/14.06 10336[5:Spt:10335.0,7494.0,9708.0] || product(e_3,e_3,e_1)*+ -> . % 13.85/14.06 10337[5:Spt:10335.0,7494.1] || -> product(e_2,e_3,e_1)*. % 13.85/14.06 10339[5:Res:10337.0,17.0] || product(u,e_3,e_2)* -> product(e_2,e_1,u)*. % 13.85/14.06 10341[5:Res:10337.0,13.0] || product(e_2,e_3,u)*+ -> equalish(u,e_1). % 13.85/14.06 10342[5:Res:10337.0,14.0] || product(e_2,u,e_1)*+ -> equalish(u,e_3). % 13.85/14.06 10381[3:Res:9703.1,35.2] group_element(e_2) group_element(e_2) || -> product(e_3,e_3,e_2) product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_3)*. % 13.85/14.06 10384[3:Obv:10381.0] group_element(e_2) || -> product(e_3,e_3,e_2) product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_3)*. % 13.85/14.06 10385[3:SSi:10384.0,4.0] || -> product(e_3,e_3,e_2) product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_3)*. % 14.95/15.10 10386[5:MRR:10385.0,10339.0] || -> product(e_2,e_2,e_3) product(e_2,e_2,e_2) product(e_2,e_1,e_3)*. % 14.95/15.10 10565[6:Spt:10386.0] || -> product(e_2,e_2,e_3)*. % 14.95/15.10 10567[6:Res:10565.0,17.0] || product(u,e_2,e_2)* -> product(e_2,e_3,u)*. % 14.95/15.10 10602[6:MRR:9693.1,10567.0] || -> product(e_2,e_3,e_2) product(e_2,e_1,e_1)*. % 14.95/15.10 10607[7:Spt:10602.0] || -> product(e_2,e_3,e_2)*. % 14.95/15.10 10621[7:Res:10607.0,10341.0] || -> equalish(e_2,e_1)*. % 14.95/15.10 10623[7:MRR:10621.0,8.0] || -> . % 14.95/15.10 10671[7:Spt:10623.0,10602.0,10607.0] || product(e_2,e_3,e_2)* -> . % 14.95/15.10 10672[7:Spt:10623.0,10602.1] || -> product(e_2,e_1,e_1)*. % 14.95/15.10 10693[7:Res:10672.0,10342.0] || -> equalish(e_1,e_3)*. % 14.95/15.10 10698[7:MRR:10693.0,7.0] || -> . % 14.95/15.10 10734[6:Spt:10698.0,10386.0,10565.0] || product(e_2,e_2,e_3)* -> . % 14.95/15.10 10735[6:Spt:10698.0,10386.1,10386.2] || -> product(e_2,e_2,e_2) product(e_2,e_1,e_3)*. % 14.95/15.10 10738[7:Spt:10735.0] || -> product(e_2,e_2,e_2)*. % 14.95/15.10 10749[7:Res:10738.0,9668.0] || -> equalish(e_2,e_1)*. % 14.95/15.10 10752[7:MRR:10749.0,8.0] || -> . % 14.95/15.10 10761[7:Spt:10752.0,10735.0,10738.0] || product(e_2,e_2,e_2)* -> . % 14.95/15.10 10762[7:Spt:10752.0,10735.1] || -> product(e_2,e_1,e_3)*. % 14.95/15.10 10776[7:Res:10762.0,9667.0] || -> equalish(e_3,e_2)*. % 14.95/15.10 10781[7:MRR:10776.0,11.0] || -> . % 14.95/15.10 10797[4:Spt:10781.0,9656.0,9663.0] || product(e_2,e_1,e_2)*+ -> . % 14.95/15.10 10798[4:Spt:10781.0,9656.1] || -> product(e_1,e_2,e_1)*. % 14.95/15.10 10825[4:Res:10798.0,13.0] || product(e_1,e_2,u)*+ -> equalish(u,e_1). % 14.95/15.10 10981[5:Spt:6762.0] || -> product(e_1,e_2,e_3)*. % 14.95/15.10 11053[5:Res:10981.0,10825.0] || -> equalish(e_3,e_1)*. % 14.95/15.10 11057[5:MRR:11053.0,10.0] || -> . % 14.95/15.10 11065[5:Spt:11057.0,6762.0,10981.0] || product(e_1,e_2,e_3)* -> . % 14.95/15.10 11066[5:Spt:11057.0,6762.1] || -> product(e_1,e_2,e_2)*. % 14.95/15.10 11086[5:Res:11066.0,10825.0] || -> equalish(e_2,e_1)*. % 14.95/15.10 11087[5:MRR:11086.0,8.0] || -> . % 14.95/15.10 % SZS output end Refutation % 14.95/15.10 Formulae used in the proof : row_surjectivity column_surjectivity 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 qg3_1 qg3_2 qg3 % 14.95/15.10 %------------------------------------------------------------------------------