%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP131-2.002 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:48 EDT 2022 % Result : Unsatisfiable 0.45s 0.64s % Output : Refutation 0.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : GRP131-2.002 : TPTP v8.1.0. Released v1.2.0. % 0.08/0.14 % Command : run_spass %d %s % 0.14/0.36 % Computer : n029.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Mon Jun 13 12:00:40 EDT 2022 % 0.14/0.36 % CPUTime : % 0.45/0.64 % 0.45/0.64 SPASS V 3.9 % 0.45/0.64 SPASS beiseite: Proof found. % 0.45/0.64 % SZS status Theorem % 0.45/0.64 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.45/0.64 SPASS derived 654 clauses, backtracked 169 clauses, performed 8 splits and kept 497 clauses. % 0.45/0.64 SPASS allocated 76458 KBytes. % 0.45/0.64 SPASS spent 0:00:00.27 on the problem. % 0.45/0.64 0:00:00.04 for the input. % 0.45/0.64 0:00:00.00 for the FLOTTER CNF translation. % 0.45/0.64 0:00:00.01 for inferences. % 0.45/0.64 0:00:00.00 for the backtracking. % 0.45/0.64 0:00:00.19 for the reduction. % 0.45/0.64 % 0.45/0.64 % 0.45/0.64 Here is a proof with depth 12, length 118 : % 0.45/0.64 % SZS output start Refutation % 0.45/0.64 4[0:Inp] || -> group_element(e_1)*. % 0.45/0.64 5[0:Inp] || -> group_element(e_2)*. % 0.45/0.64 6[0:Inp] || equalish(e_1,e_2)*+ -> . % 0.45/0.64 7[0:Inp] || equalish(e_2,e_1)*+ -> . % 0.45/0.64 8[0:Inp] group_element(u) group_element(v) || -> product(v,u,e_2) product(v,u,e_1)*. % 0.45/0.64 9[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 0.45/0.64 10[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 0.45/0.64 11[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 0.45/0.64 13[0:Inp] || product(u,v,w)*+ product(u,x,y)* product(w,v,z)* product(y,x,z)* -> equalish(x,v)*. % 0.45/0.64 15[0:Res:13.4,6.0] || product(u,e_2,v)*+ product(u,e_1,w)* product(v,e_2,x)* product(w,e_1,x)* -> . % 0.45/0.64 21[0:Res:8.3,9.0] group_element(u) group_element(v) || product(v,u,w)*+ -> product(v,u,e_2)* equalish(w,e_1). % 0.45/0.64 22[0:Res:8.3,10.0] group_element(u) group_element(v) || product(v,w,e_1)*+ -> product(v,u,e_2)* equalish(w,u)*. % 0.45/0.64 23[0:Res:8.3,11.0] group_element(u) group_element(v) || product(w,u,e_1)*+ -> product(v,u,e_2)* equalish(w,v)*. % 0.45/0.64 25[0:Res:8.3,21.2] group_element(u) group_element(v) group_element(u) group_element(v) || -> product(v,u,e_2)* product(v,u,e_2)* equalish(e_1,e_1). % 0.45/0.64 26[0:Obv:25.4] group_element(u) group_element(v) || -> product(v,u,e_2)* equalish(e_1,e_1). % 0.45/0.64 27[1:Spt:26.0,26.1,26.2] group_element(u) group_element(v) || -> product(v,u,e_2)*. % 0.45/0.64 30[1:Res:27.2,10.0] group_element(u) group_element(v) || product(v,w,e_2)*+ -> equalish(w,u)*. % 0.45/0.64 41[1:Res:27.2,30.2] group_element(u) group_element(v) group_element(w) group_element(v) || -> equalish(u,w)*. % 0.45/0.64 42[1:Obv:41.1] group_element(u) group_element(v) group_element(w) || -> equalish(u,v)*. % 0.45/0.64 43[1:Con:42.2] group_element(u) group_element(v) || -> equalish(u,v)*. % 0.45/0.64 45[1:Res:43.2,6.0] group_element(e_1) group_element(e_2) || -> . % 0.45/0.64 47[1:SSi:45.1,45.0,5.0,4.0] || -> . % 0.45/0.64 48[1:Spt:47.0,26.3] || -> equalish(e_1,e_1)*. % 0.45/0.64 57[0:Res:8.3,22.2] group_element(u) group_element(v) group_element(w) group_element(v) || -> product(v,u,e_2)* product(v,w,e_2)* equalish(u,w)*. % 0.45/0.64 58[0:Obv:57.1] group_element(u) group_element(v) group_element(w) || -> product(w,u,e_2)* product(w,v,e_2)* equalish(u,v)*. % 0.45/0.64 59[0:Res:8.3,23.2] group_element(u) group_element(v) group_element(u) group_element(w) || -> product(v,u,e_2)* product(w,u,e_2)* equalish(v,w)*. % 0.45/0.64 60[0:Obv:59.0] group_element(u) group_element(v) group_element(w) || -> product(u,v,e_2)* product(w,v,e_2)* equalish(u,w)*. % 0.45/0.64 61[0:Res:8.3,15.0] group_element(e_2) group_element(u) || product(u,e_1,v)* product(e_1,e_2,w)* product(v,e_1,w)* -> product(u,e_2,e_2). % 0.45/0.64 62[0:SSi:61.0,5.0] group_element(u) || product(u,e_1,v)*+ product(e_1,e_2,w)* product(v,e_1,w)* -> product(u,e_2,e_2). % 0.45/0.64 66[0:Fac:58.3,58.4] group_element(u) group_element(u) group_element(v) || -> product(v,u,e_2)* equalish(u,u)*. % 0.45/0.64 87[0:Obv:66.0] group_element(u) group_element(v) || -> product(v,u,e_2)* equalish(u,u)*. % 0.45/0.64 105[0:Res:87.2,15.0] group_element(e_2) group_element(u) || product(u,e_1,v)* product(e_2,e_2,w)* product(v,e_1,w)* -> equalish(e_2,e_2). % 0.45/0.64 109[0:SSi:105.0,5.0] group_element(u) || product(u,e_1,v)*+ product(e_2,e_2,w)* product(v,e_1,w)* -> equalish(e_2,e_2). % 0.45/0.64 169[0:Res:8.3,109.1] group_element(e_1) group_element(u) group_element(u) || product(e_2,e_2,v) product(e_1,e_1,v)* -> product(u,e_1,e_2)* equalish(e_2,e_2). % 0.45/0.64 170[0:Obv:169.1] group_element(e_1) group_element(u) || product(e_2,e_2,v) product(e_1,e_1,v)* -> product(u,e_1,e_2)* equalish(e_2,e_2). % 0.45/0.64 171[0:SSi:170.0,4.0] group_element(u) || product(e_2,e_2,v)+ product(e_1,e_1,v)* -> product(u,e_1,e_2)* equalish(e_2,e_2). % 0.45/0.64 178[2:Spt:171.0,171.3] group_element(u) || -> product(u,e_1,e_2)*. % 0.45/0.64 184[2:Res:178.1,11.0] group_element(u) || product(v,e_1,e_2)*+ -> equalish(v,u)*. % 0.45/0.64 201[0:Res:8.3,62.1] group_element(e_1) group_element(u) group_element(u) || product(e_1,e_2,v) product(e_1,e_1,v)* -> product(u,e_1,e_2)* product(u,e_2,e_2). % 0.45/0.64 203[0:Obv:201.1] group_element(e_1) group_element(u) || product(e_1,e_2,v) product(e_1,e_1,v)* -> product(u,e_1,e_2)* product(u,e_2,e_2). % 0.45/0.64 247[2:Res:178.1,184.1] group_element(u) group_element(v) || -> equalish(u,v)*. % 0.45/0.64 250[2:Res:247.2,6.0] group_element(e_1) group_element(e_2) || -> . % 0.45/0.64 252[2:SSi:250.1,250.0,5.0,4.0] || -> . % 0.45/0.64 253[2:Spt:252.0,171.1,171.2,171.4] || product(e_2,e_2,u)+ product(e_1,e_1,u)* -> equalish(e_2,e_2). % 0.45/0.64 254[0:SSi:203.0,4.0] group_element(u) || product(e_1,e_2,v)+ product(e_1,e_1,v)* -> product(u,e_1,e_2)* product(u,e_2,e_2). % 0.45/0.64 342[0:Res:8.3,254.1] group_element(e_2) group_element(e_1) group_element(u) || product(e_1,e_1,e_1)* -> product(e_1,e_2,e_2) product(u,e_1,e_2)* product(u,e_2,e_2). % 0.45/0.64 343[0:SSi:342.1,342.0,4.0,5.0] group_element(u) || product(e_1,e_1,e_1)*+ -> product(e_1,e_2,e_2) product(u,e_1,e_2)* product(u,e_2,e_2). % 0.45/0.64 348[3:Spt:343.0,343.3,343.4] group_element(u) || -> product(u,e_1,e_2)* product(u,e_2,e_2). % 0.45/0.64 352[3:Res:348.1,9.0] group_element(u) || product(u,e_1,v)*+ -> product(u,e_2,e_2) equalish(v,e_2). % 0.45/0.64 356[3:Res:348.1,62.1] group_element(u) group_element(u) || product(e_1,e_2,v)* product(e_2,e_1,v) -> product(u,e_2,e_2)* product(u,e_2,e_2)*. % 0.45/0.64 363[3:Obv:356.4] group_element(u) || product(e_1,e_2,v)*+ product(e_2,e_1,v) -> product(u,e_2,e_2)*. % 0.45/0.64 373[3:Res:348.1,352.1] group_element(u) group_element(u) || -> product(u,e_2,e_2)* product(u,e_2,e_2)* equalish(e_2,e_2). % 0.45/0.64 375[3:Obv:373.2] group_element(u) || -> product(u,e_2,e_2)* equalish(e_2,e_2). % 0.45/0.64 381[4:Spt:375.0,375.1] group_element(u) || -> product(u,e_2,e_2)*. % 0.45/0.64 386[4:Res:381.1,11.0] group_element(u) || product(v,e_2,e_2)*+ -> equalish(v,u)*. % 0.45/0.64 428[4:Res:381.1,386.1] group_element(u) group_element(v) || -> equalish(u,v)*. % 0.45/0.64 431[4:Res:428.2,6.0] group_element(e_1) group_element(e_2) || -> . % 0.45/0.64 433[4:SSi:431.1,431.0,5.0,4.0] || -> . % 0.45/0.64 434[4:Spt:433.0,375.2] || -> equalish(e_2,e_2)*. % 0.45/0.64 501[3:Res:8.3,363.1] group_element(e_2) group_element(e_1) group_element(u) || product(e_2,e_1,e_1) -> product(e_1,e_2,e_2)* product(u,e_2,e_2)*. % 0.45/0.64 502[3:Con:501.2] group_element(e_2) group_element(e_1) || product(e_2,e_1,e_1) -> product(e_1,e_2,e_2)*. % 0.45/0.64 503[3:SSi:502.1,502.0,4.0,5.0] || product(e_2,e_1,e_1)+ -> product(e_1,e_2,e_2)*. % 0.45/0.64 536[3:Res:60.4,363.1] group_element(u) group_element(e_2) group_element(e_1) group_element(v) || product(e_2,e_1,e_2)* -> product(u,e_2,e_2)* equalish(u,e_1) product(v,e_2,e_2)*. % 0.45/0.64 544[3:Con:536.3] group_element(u) group_element(e_2) group_element(e_1) || product(e_2,e_1,e_2)* -> product(u,e_2,e_2)* equalish(u,e_1). % 0.45/0.64 545[3:SSi:544.2,544.1,4.0,5.0] group_element(u) || product(e_2,e_1,e_2)* -> product(u,e_2,e_2)* equalish(u,e_1). % 0.45/0.64 554[3:Res:8.3,503.0] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_2) product(e_1,e_2,e_2)*. % 0.45/0.64 555[3:SSi:554.1,554.0,5.0,4.0] || -> product(e_2,e_1,e_2) product(e_1,e_2,e_2)*. % 0.45/0.64 556[5:Spt:555.1] || -> product(e_1,e_2,e_2)*. % 0.45/0.64 561[5:Res:556.0,11.0] || product(u,e_2,e_2)*+ -> equalish(u,e_1). % 0.45/0.64 570[5:MRR:545.2,561.0] group_element(u) || product(e_2,e_1,e_2)*+ -> equalish(u,e_1)*. % 0.45/0.64 613[5:Res:348.1,570.1] group_element(e_2) group_element(u) || -> product(e_2,e_2,e_2)* equalish(u,e_1)*. % 0.45/0.64 614[5:SSi:613.0,5.0] group_element(u) || -> product(e_2,e_2,e_2)* equalish(u,e_1)*. % 0.45/0.64 620[6:Spt:614.0,614.2] group_element(u) || -> equalish(u,e_1)*. % 0.45/0.64 621[6:Res:620.1,7.0] group_element(e_2) || -> . % 0.45/0.64 622[6:SSi:621.0,5.0] || -> . % 0.45/0.64 623[6:Spt:622.0,614.1] || -> product(e_2,e_2,e_2)*. % 0.45/0.64 632[6:Res:623.0,561.0] || -> equalish(e_2,e_1)*. % 0.45/0.64 636[6:MRR:632.0,7.0] || -> . % 0.45/0.64 640[5:Spt:636.0,555.1,556.0] || product(e_1,e_2,e_2)*+ -> . % 0.45/0.64 641[5:Spt:636.0,555.0] || -> product(e_2,e_1,e_2)*. % 0.45/0.64 652[5:Res:641.0,11.0] || product(u,e_1,e_2)*+ -> equalish(u,e_2). % 0.45/0.64 664[5:Res:58.4,640.0] group_element(u) group_element(e_2) group_element(e_1) || -> product(e_1,u,e_2)* equalish(u,e_2). % 0.45/0.64 667[5:SSi:664.2,664.1,4.0,5.0] group_element(u) || -> product(e_1,u,e_2)* equalish(u,e_2). % 0.45/0.65 745[5:Res:667.1,652.0] group_element(e_1) || -> equalish(e_1,e_2)* equalish(e_1,e_2)*. % 0.45/0.65 748[5:Obv:745.1] group_element(e_1) || -> equalish(e_1,e_2)*. % 0.45/0.65 749[5:SSi:748.0,4.0] || -> equalish(e_1,e_2)*. % 0.45/0.65 750[5:MRR:749.0,6.0] || -> . % 0.45/0.65 754[3:Spt:750.0,343.1,343.2] || product(e_1,e_1,e_1)*+ -> product(e_1,e_2,e_2). % 0.45/0.65 755[3:Res:8.3,754.0] group_element(e_1) group_element(e_1) || -> product(e_1,e_1,e_2)* product(e_1,e_2,e_2). % 0.45/0.65 756[3:Obv:755.0] group_element(e_1) || -> product(e_1,e_1,e_2)* product(e_1,e_2,e_2). % 0.45/0.65 757[3:SSi:756.0,4.0] || -> product(e_1,e_1,e_2)* product(e_1,e_2,e_2). % 0.45/0.65 758[4:Spt:757.1] || -> product(e_1,e_2,e_2)*. % 0.45/0.65 762[4:Res:758.0,10.0] || product(e_1,u,e_2)*+ -> equalish(u,e_2). % 0.45/0.65 763[4:Res:758.0,11.0] || product(u,e_2,e_2)*+ -> equalish(u,e_1). % 0.45/0.65 785[4:Res:60.4,762.0] group_element(u) group_element(v) group_element(e_1) || -> product(u,v,e_2)* equalish(u,e_1) equalish(v,e_2). % 0.45/0.65 790[4:SSi:785.2,4.0] group_element(u) group_element(v) || -> product(u,v,e_2)* equalish(u,e_1) equalish(v,e_2). % 0.45/0.65 839[4:Res:790.2,62.1] group_element(u) group_element(e_1) group_element(u) || product(e_1,e_2,v)* product(e_2,e_1,v) -> equalish(u,e_1) equalish(e_1,e_2) product(u,e_2,e_2)*. % 0.45/0.65 856[4:Obv:839.0] group_element(e_1) group_element(u) || product(e_1,e_2,v)* product(e_2,e_1,v) -> equalish(u,e_1) equalish(e_1,e_2) product(u,e_2,e_2)*. % 0.45/0.65 857[4:SSi:856.0,4.0] group_element(u) || product(e_1,e_2,v)* product(e_2,e_1,v) -> equalish(u,e_1) equalish(e_1,e_2) product(u,e_2,e_2)*. % 0.45/0.65 858[4:MRR:857.4,857.5,6.0,763.0] group_element(u) || product(e_1,e_2,v)*+ product(e_2,e_1,v) -> equalish(u,e_1)*. % 0.45/0.65 870[4:Res:758.0,858.1] group_element(u) || product(e_2,e_1,e_2)*+ -> equalish(u,e_1)*. % 0.45/0.65 876[4:Res:790.2,870.1] group_element(e_2) group_element(e_1) group_element(u) || -> equalish(e_2,e_1) equalish(e_1,e_2)* equalish(u,e_1)*. % 0.45/0.65 878[4:Con:876.2] group_element(e_2) group_element(e_1) || -> equalish(e_2,e_1) equalish(e_1,e_2)*. % 0.45/0.65 879[4:SSi:878.1,878.0,4.0,5.0] || -> equalish(e_2,e_1) equalish(e_1,e_2)*. % 0.45/0.65 880[4:MRR:879.0,879.1,7.0,6.0] || -> . % 0.45/0.65 886[4:Spt:880.0,757.1,758.0] || product(e_1,e_2,e_2)*+ -> . % 0.45/0.65 887[4:Spt:880.0,757.0] || -> product(e_1,e_1,e_2)*. % 0.45/0.65 898[4:Res:887.0,11.0] || product(u,e_1,e_2)*+ -> equalish(u,e_1). % 0.45/0.65 900[4:Res:887.0,62.1] group_element(e_1) || product(e_1,e_2,u)* product(e_2,e_1,u) -> product(e_1,e_2,e_2)*. % 0.45/0.65 905[4:SSi:900.0,4.0] || product(e_1,e_2,u)* product(e_2,e_1,u) -> product(e_1,e_2,e_2)*. % 0.45/0.65 906[4:MRR:905.2,886.0] || product(e_1,e_2,u)*+ product(e_2,e_1,u) -> . % 0.45/0.65 1014[4:Res:8.3,906.0] group_element(e_2) group_element(e_1) || product(e_2,e_1,e_1) -> product(e_1,e_2,e_2)*. % 0.45/0.65 1017[4:SSi:1014.1,1014.0,4.0,5.0] || product(e_2,e_1,e_1) -> product(e_1,e_2,e_2)*. % 0.45/0.65 1018[4:MRR:1017.1,886.0] || product(e_2,e_1,e_1)*+ -> . % 0.45/0.65 1019[4:Res:8.3,1018.0] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_2)*. % 0.45/0.65 1020[4:SSi:1019.1,1019.0,5.0,4.0] || -> product(e_2,e_1,e_2)*. % 0.45/0.65 1028[4:Res:1020.0,898.0] || -> equalish(e_2,e_1)*. % 0.45/0.65 1033[4:MRR:1028.0,7.0] || -> . % 0.45/0.65 % SZS output end Refutation % 0.45/0.65 Formulae used in the proof : element_1 element_2 e_1_is_not_e_2 e_2_is_not_e_1 product_total_function1 product_total_function2 product_right_cancellation product_left_cancellation qg1_2 % 0.45/0.65 %------------------------------------------------------------------------------