%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP131-1.002 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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.46s 0.65s % Output : Refutation 0.46s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP131-1.002 : TPTP v8.1.0. Released v1.2.0. % 0.06/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n017.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 09:19:38 EDT 2022 % 0.13/0.34 % CPUTime : % 0.46/0.65 % 0.46/0.65 SPASS V 3.9 % 0.46/0.65 SPASS beiseite: Proof found. % 0.46/0.65 % SZS status Theorem % 0.46/0.65 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.46/0.65 SPASS derived 651 clauses, backtracked 161 clauses, performed 8 splits and kept 476 clauses. % 0.46/0.65 SPASS allocated 76510 KBytes. % 0.46/0.65 SPASS spent 0:00:00.30 on the problem. % 0.46/0.65 0:00:00.03 for the input. % 0.46/0.65 0:00:00.00 for the FLOTTER CNF translation. % 0.46/0.65 0:00:00.01 for inferences. % 0.46/0.65 0:00:00.00 for the backtracking. % 0.46/0.65 0:00:00.23 for the reduction. % 0.46/0.65 % 0.46/0.65 % 0.46/0.65 Here is a proof with depth 12, length 117 : % 0.46/0.65 % SZS output start Refutation % 0.46/0.65 1[0:Inp] || -> group_element(e_1)*. % 0.46/0.65 2[0:Inp] || -> group_element(e_2)*. % 0.46/0.65 3[0:Inp] || equalish(e_1,e_2)*+ -> . % 0.46/0.65 4[0:Inp] || equalish(e_2,e_1)*+ -> . % 0.46/0.65 5[0:Inp] group_element(u) group_element(v) || -> product(v,u,e_2) product(v,u,e_1)*. % 0.46/0.65 6[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 0.46/0.65 7[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 0.46/0.65 8[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 0.46/0.65 10[0:Inp] || product(u,v,w)*+ product(u,x,y)* product(w,v,z)* product(y,x,z)* -> equalish(x,v)*. % 0.46/0.65 12[0:Res:10.4,3.0] || product(u,e_2,v)*+ product(u,e_1,w)* product(v,e_2,x)* product(w,e_1,x)* -> . % 0.46/0.65 17[0:Res:5.3,6.0] group_element(u) group_element(v) || product(v,u,w)*+ -> product(v,u,e_2)* equalish(w,e_1). % 0.46/0.65 18[0:Res:5.3,7.0] group_element(u) group_element(v) || product(v,w,e_1)*+ -> product(v,u,e_2)* equalish(w,u)*. % 0.46/0.65 19[0:Res:5.3,8.0] group_element(u) group_element(v) || product(w,u,e_1)*+ -> product(v,u,e_2)* equalish(w,v)*. % 0.46/0.65 20[0:Res:5.3,17.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.46/0.65 21[0:Obv:20.4] group_element(u) group_element(v) || -> product(v,u,e_2)* equalish(e_1,e_1). % 0.46/0.65 23[1:Spt:21.0,21.1,21.2] group_element(u) group_element(v) || -> product(v,u,e_2)*. % 0.46/0.65 26[1:Res:23.2,7.0] group_element(u) group_element(v) || product(v,w,e_2)*+ -> equalish(w,u)*. % 0.46/0.65 34[1:Res:23.2,26.2] group_element(u) group_element(v) group_element(w) group_element(v) || -> equalish(u,w)*. % 0.46/0.65 35[1:Obv:34.1] group_element(u) group_element(v) group_element(w) || -> equalish(u,v)*. % 0.46/0.65 36[1:Con:35.2] group_element(u) group_element(v) || -> equalish(u,v)*. % 0.46/0.65 38[1:Res:36.2,3.0] group_element(e_1) group_element(e_2) || -> . % 0.46/0.65 40[1:SSi:38.1,38.0,2.0,1.0] || -> . % 0.46/0.65 41[1:Spt:40.0,21.3] || -> equalish(e_1,e_1)*. % 0.46/0.65 49[0:Res:5.3,18.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.46/0.65 50[0:Obv:49.1] group_element(u) group_element(v) group_element(w) || -> product(w,u,e_2)* product(w,v,e_2)* equalish(u,v)*. % 0.46/0.65 51[0:Res:5.3,19.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.46/0.65 52[0:Obv:51.0] group_element(u) group_element(v) group_element(w) || -> product(u,v,e_2)* product(w,v,e_2)* equalish(u,w)*. % 0.46/0.65 53[0:Res:5.3,12.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.46/0.65 54[0:SSi:53.0,2.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.46/0.65 55[0:Fac:50.3,50.4] group_element(u) group_element(u) group_element(v) || -> product(v,u,e_2)* equalish(u,u)*. % 0.46/0.65 72[0:Obv:55.0] group_element(u) group_element(v) || -> product(v,u,e_2)* equalish(u,u)*. % 0.46/0.65 92[0:Res:72.2,12.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.46/0.65 96[0:SSi:92.0,2.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.46/0.65 149[0:Res:5.3,96.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.46/0.65 153[0:Obv:149.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.46/0.65 154[0:SSi:153.0,1.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.46/0.65 162[2:Spt:154.0,154.3] group_element(u) || -> product(u,e_1,e_2)*. % 0.46/0.65 167[2:Res:162.1,8.0] group_element(u) || product(v,e_1,e_2)*+ -> equalish(v,u)*. % 0.46/0.65 196[0:Res:5.3,54.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.46/0.65 201[0:Obv:196.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.46/0.65 218[2:Res:162.1,167.1] group_element(u) group_element(v) || -> equalish(u,v)*. % 0.46/0.65 224[2:Res:218.2,3.0] group_element(e_1) group_element(e_2) || -> . % 0.46/0.65 226[2:SSi:224.1,224.0,2.0,1.0] || -> . % 0.46/0.65 227[2:Spt:226.0,154.1,154.2,154.4] || product(e_2,e_2,u)+ product(e_1,e_1,u)* -> equalish(e_2,e_2). % 0.46/0.65 228[0:SSi:201.0,1.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.46/0.65 309[0:Res:5.3,228.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.46/0.65 313[0:SSi:309.1,309.0,1.0,2.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.46/0.65 318[3:Spt:313.0,313.3,313.4] group_element(u) || -> product(u,e_1,e_2)* product(u,e_2,e_2). % 0.46/0.65 321[3:Res:318.1,6.0] group_element(u) || product(u,e_1,v)*+ -> product(u,e_2,e_2) equalish(v,e_2). % 0.46/0.65 325[3:Res:318.1,54.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.46/0.65 332[3:Obv:325.4] group_element(u) || product(e_1,e_2,v)*+ product(e_2,e_1,v) -> product(u,e_2,e_2)*. % 0.46/0.65 337[3:Res:318.1,321.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.46/0.65 342[3:Obv:337.2] group_element(u) || -> product(u,e_2,e_2)* equalish(e_2,e_2). % 0.46/0.65 364[4:Spt:342.0,342.1] group_element(u) || -> product(u,e_2,e_2)*. % 0.46/0.65 369[4:Res:364.1,8.0] group_element(u) || product(v,e_2,e_2)*+ -> equalish(v,u)*. % 0.46/0.65 419[4:Res:364.1,369.1] group_element(u) group_element(v) || -> equalish(u,v)*. % 0.46/0.65 425[4:Res:419.2,3.0] group_element(e_1) group_element(e_2) || -> . % 0.46/0.65 427[4:SSi:425.1,425.0,2.0,1.0] || -> . % 0.46/0.65 428[4:Spt:427.0,342.2] || -> equalish(e_2,e_2)*. % 0.46/0.65 489[3:Res:5.3,332.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.46/0.65 492[3:Con:489.2] group_element(e_2) group_element(e_1) || product(e_2,e_1,e_1) -> product(e_1,e_2,e_2)*. % 0.46/0.65 493[3:SSi:492.1,492.0,1.0,2.0] || product(e_2,e_1,e_1)+ -> product(e_1,e_2,e_2)*. % 0.46/0.65 524[3:Res:52.4,332.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.46/0.65 532[3:Con:524.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.46/0.65 533[3:SSi:532.2,532.1,1.0,2.0] group_element(u) || product(e_2,e_1,e_2)* -> product(u,e_2,e_2)* equalish(u,e_1). % 0.46/0.65 542[3:Res:5.3,493.0] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_2) product(e_1,e_2,e_2)*. % 0.46/0.65 543[3:SSi:542.1,542.0,2.0,1.0] || -> product(e_2,e_1,e_2) product(e_1,e_2,e_2)*. % 0.46/0.65 544[5:Spt:543.1] || -> product(e_1,e_2,e_2)*. % 0.46/0.65 549[5:Res:544.0,8.0] || product(u,e_2,e_2)*+ -> equalish(u,e_1). % 0.46/0.65 558[5:MRR:533.2,549.0] group_element(u) || product(e_2,e_1,e_2)*+ -> equalish(u,e_1)*. % 0.46/0.65 598[5:Res:318.1,558.1] group_element(e_2) group_element(u) || -> product(e_2,e_2,e_2)* equalish(u,e_1)*. % 0.46/0.65 602[5:SSi:598.0,2.0] group_element(u) || -> product(e_2,e_2,e_2)* equalish(u,e_1)*. % 0.46/0.65 608[6:Spt:602.0,602.2] group_element(u) || -> equalish(u,e_1)*. % 0.46/0.65 609[6:Res:608.1,4.0] group_element(e_2) || -> . % 0.46/0.65 610[6:SSi:609.0,2.0] || -> . % 0.46/0.65 611[6:Spt:610.0,602.1] || -> product(e_2,e_2,e_2)*. % 0.46/0.65 620[6:Res:611.0,549.0] || -> equalish(e_2,e_1)*. % 0.46/0.65 624[6:MRR:620.0,4.0] || -> . % 0.46/0.65 628[5:Spt:624.0,543.1,544.0] || product(e_1,e_2,e_2)*+ -> . % 0.46/0.65 629[5:Spt:624.0,543.0] || -> product(e_2,e_1,e_2)*. % 0.46/0.65 639[5:Res:629.0,8.0] || product(u,e_1,e_2)*+ -> equalish(u,e_2). % 0.46/0.65 651[5:Res:50.3,628.0] group_element(e_2) group_element(u) group_element(e_1) || -> product(e_1,u,e_2)* equalish(e_2,u). % 0.46/0.65 654[5:SSi:651.2,651.0,1.0,2.0] group_element(u) || -> product(e_1,u,e_2)* equalish(e_2,u). % 0.46/0.67 703[5:Res:654.1,639.0] group_element(e_1) || -> equalish(e_2,e_1) equalish(e_1,e_2)*. % 0.46/0.67 704[5:SSi:703.0,1.0] || -> equalish(e_2,e_1) equalish(e_1,e_2)*. % 0.46/0.67 705[5:MRR:704.0,704.1,4.0,3.0] || -> . % 0.46/0.67 709[3:Spt:705.0,313.1,313.2] || product(e_1,e_1,e_1)*+ -> product(e_1,e_2,e_2). % 0.46/0.67 710[3:Res:5.3,709.0] group_element(e_1) group_element(e_1) || -> product(e_1,e_1,e_2)* product(e_1,e_2,e_2). % 0.46/0.67 711[3:Obv:710.0] group_element(e_1) || -> product(e_1,e_1,e_2)* product(e_1,e_2,e_2). % 0.46/0.67 712[3:SSi:711.0,1.0] || -> product(e_1,e_1,e_2)* product(e_1,e_2,e_2). % 0.46/0.67 718[4:Spt:712.1] || -> product(e_1,e_2,e_2)*. % 0.46/0.67 722[4:Res:718.0,7.0] || product(e_1,u,e_2)*+ -> equalish(u,e_2). % 0.46/0.67 723[4:Res:718.0,8.0] || product(u,e_2,e_2)*+ -> equalish(u,e_1). % 0.46/0.67 742[4:Res:52.4,722.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.46/0.67 747[4:SSi:742.2,1.0] group_element(u) group_element(v) || -> product(u,v,e_2)* equalish(u,e_1) equalish(v,e_2). % 0.46/0.67 904[4:Res:747.2,54.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.46/0.67 922[4:Obv:904.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.46/0.67 923[4:SSi:922.0,1.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.46/0.67 924[4:MRR:923.4,923.5,3.0,723.0] group_element(u) || product(e_1,e_2,v)*+ product(e_2,e_1,v) -> equalish(u,e_1)*. % 0.46/0.67 938[4:Res:718.0,924.1] group_element(u) || product(e_2,e_1,e_2)*+ -> equalish(u,e_1)*. % 0.46/0.67 944[4:Res:747.2,938.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.46/0.67 950[4:Con:944.2] group_element(e_2) group_element(e_1) || -> equalish(e_2,e_1) equalish(e_1,e_2)*. % 0.46/0.67 951[4:SSi:950.1,950.0,1.0,2.0] || -> equalish(e_2,e_1) equalish(e_1,e_2)*. % 0.46/0.67 952[4:MRR:951.0,951.1,4.0,3.0] || -> . % 0.46/0.67 957[4:Spt:952.0,712.1,718.0] || product(e_1,e_2,e_2)*+ -> . % 0.46/0.67 958[4:Spt:952.0,712.0] || -> product(e_1,e_1,e_2)*. % 0.46/0.67 968[4:Res:958.0,8.0] || product(u,e_1,e_2)*+ -> equalish(u,e_1). % 0.46/0.67 970[4:Res:958.0,54.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.46/0.67 978[4:SSi:970.0,1.0] || product(e_1,e_2,u)* product(e_2,e_1,u) -> product(e_1,e_2,e_2)*. % 0.46/0.67 979[4:MRR:978.2,957.0] || product(e_1,e_2,u)*+ product(e_2,e_1,u) -> . % 0.46/0.67 1049[4:Res:5.3,979.0] group_element(e_2) group_element(e_1) || product(e_2,e_1,e_1) -> product(e_1,e_2,e_2)*. % 0.46/0.67 1053[4:SSi:1049.1,1049.0,1.0,2.0] || product(e_2,e_1,e_1) -> product(e_1,e_2,e_2)*. % 0.46/0.67 1054[4:MRR:1053.1,957.0] || product(e_2,e_1,e_1)*+ -> . % 0.46/0.67 1055[4:Res:5.3,1054.0] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_2)*. % 0.46/0.67 1056[4:SSi:1055.1,1055.0,2.0,1.0] || -> product(e_2,e_1,e_2)*. % 0.46/0.67 1064[4:Res:1056.0,968.0] || -> equalish(e_2,e_1)*. % 0.46/0.67 1071[4:MRR:1064.0,4.0] || -> . % 0.46/0.67 % SZS output end Refutation % 0.46/0.67 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.46/0.67 %------------------------------------------------------------------------------