%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP124-1.004 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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:30 EDT 2022 % Result : Unsatisfiable 0.34s 0.52s % Output : Refutation 0.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP124-1.004 : TPTP v8.1.0. Released v1.2.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.33 % Computer : n026.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Mon Jun 13 22:17:06 EDT 2022 % 0.13/0.34 % CPUTime : % 0.34/0.52 % 0.34/0.52 SPASS V 3.9 % 0.34/0.52 SPASS beiseite: Proof found. % 0.34/0.52 % SZS status Theorem % 0.34/0.52 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.34/0.52 SPASS derived 683 clauses, backtracked 116 clauses, performed 12 splits and kept 436 clauses. % 0.34/0.52 SPASS allocated 76162 KBytes. % 0.34/0.52 SPASS spent 0:00:00.17 on the problem. % 0.34/0.52 0:00:00.04 for the input. % 0.34/0.52 0:00:00.00 for the FLOTTER CNF translation. % 0.34/0.52 0:00:00.01 for inferences. % 0.34/0.52 0:00:00.00 for the backtracking. % 0.34/0.52 0:00:00.09 for the reduction. % 0.34/0.52 % 0.34/0.52 % 0.34/0.52 Here is a proof with depth 13, length 125 : % 0.34/0.52 % SZS output start Refutation % 0.34/0.52 1[0:Inp] || -> group_element(e_1)*. % 0.34/0.52 2[0:Inp] || -> group_element(e_2)*. % 0.34/0.52 3[0:Inp] || -> group_element(e_3)*. % 0.34/0.52 4[0:Inp] || -> group_element(e_4)*. % 0.34/0.52 5[0:Inp] || equalish(e_1,e_2)*+ -> . % 0.34/0.52 6[0:Inp] || equalish(e_1,e_3)*+ -> . % 0.34/0.52 7[0:Inp] || equalish(e_1,e_4)*+ -> . % 0.34/0.52 8[0:Inp] || equalish(e_2,e_1)*+ -> . % 0.34/0.52 9[0:Inp] || equalish(e_2,e_3)*+ -> . % 0.34/0.52 11[0:Inp] || equalish(e_3,e_1)*+ -> . % 0.34/0.52 12[0:Inp] || equalish(e_3,e_2)*+ -> . % 0.34/0.52 13[0:Inp] || equalish(e_3,e_4)*+ -> . % 0.34/0.52 14[0:Inp] || equalish(e_4,e_1)*+ -> . % 0.34/0.52 15[0:Inp] || equalish(e_4,e_2)*+ -> . % 0.34/0.52 16[0:Inp] || equalish(e_4,e_3)*+ -> . % 0.34/0.52 17[0:Inp] group_element(u) group_element(v) || -> product(v,u,e_4) product(v,u,e_3) product(v,u,e_2) product(v,u,e_1)*. % 0.34/0.52 18[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 0.34/0.52 19[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 0.34/0.52 20[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 0.34/0.52 21[0:Inp] || -> product(u,u,u)*. % 0.34/0.52 22[0:Inp] || product(u,v,w)*+ product(u,x,y)* product(v,w,z)* product(x,y,z)* -> equalish(x,v)*. % 0.34/0.52 23[0:Inp] || product(u,v,w)*+ product(u,x,y)* product(v,w,z)* product(x,y,z)* -> equalish(y,w)*. % 0.34/0.52 25[0:Res:21.0,23.1] || product(u,v,v)*+ product(u,w,x)* product(w,x,v)* -> equalish(x,v). % 0.34/0.52 41[0:Res:21.0,22.1] || product(u,v,v)*+ product(u,w,x)* product(w,x,v)* -> equalish(w,v). % 0.34/0.52 42[0:Res:21.0,22.2] || product(u,v,w)*+ product(v,w,x)* product(u,u,x)* -> equalish(u,v). % 0.34/0.52 60[0:Res:21.0,20.0] || product(u,v,v)*+ -> equalish(u,v). % 0.34/0.52 62[0:Res:21.0,19.0] || product(u,v,u)*+ -> equalish(v,u). % 0.34/0.52 70[0:Res:17.5,60.0] group_element(e_1) group_element(u) || -> product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(u,e_1). % 0.34/0.52 71[0:Res:17.5,62.0] group_element(u) group_element(e_1) || -> product(e_1,u,e_4) product(e_1,u,e_3) product(e_1,u,e_2)* equalish(u,e_1). % 0.34/0.52 72[0:SSi:71.1,1.0] group_element(u) || -> product(e_1,u,e_4) product(e_1,u,e_3) product(e_1,u,e_2)* equalish(u,e_1). % 0.34/0.52 73[0:SSi:70.0,1.0] group_element(u) || -> product(u,e_1,e_4) product(u,e_1,e_3) product(u,e_1,e_2)* equalish(u,e_1). % 0.34/0.52 79[0:Res:72.3,60.0] group_element(e_2) || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.34/0.52 80[0:SSi:79.0,2.0] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.34/0.52 81[0:MRR:80.2,80.3,8.0,5.0] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)*. % 0.34/0.52 82[0:Res:81.1,18.0] || product(e_1,e_2,u)*+ -> product(e_1,e_2,e_4)* equalish(u,e_3). % 0.34/0.52 83[0:Res:81.1,19.0] || product(e_1,u,e_3)*+ -> product(e_1,e_2,e_4)* equalish(u,e_2). % 0.34/0.52 85[1:Spt:82.0,82.2] || product(e_1,e_2,u)*+ -> equalish(u,e_3). % 0.34/0.52 89[2:Spt:83.0,83.2] || product(e_1,u,e_3)*+ -> equalish(u,e_2). % 0.34/0.52 102[0:Res:73.3,62.0] group_element(e_2) || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.34/0.52 103[0:SSi:102.0,2.0] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)* equalish(e_2,e_1) equalish(e_1,e_2). % 0.34/0.52 104[0:MRR:103.2,103.3,8.0,5.0] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 0.34/0.52 106[0:Res:104.1,18.0] || product(e_2,e_1,u)*+ -> product(e_2,e_1,e_4)* equalish(u,e_3). % 0.34/0.52 109[3:Spt:106.0,106.2] || product(e_2,e_1,u)*+ -> equalish(u,e_3). % 0.34/0.52 143[0:Res:21.0,41.0] || product(u,v,w)*+ product(v,w,u)* -> equalish(v,u). % 0.34/0.52 155[0:Res:81.1,143.0] || product(e_2,e_3,e_1) -> product(e_1,e_2,e_4)* equalish(e_2,e_1). % 0.34/0.52 156[0:Res:104.1,143.0] || product(e_1,e_3,e_2)* -> product(e_2,e_1,e_4) equalish(e_1,e_2). % 0.34/0.52 157[0:MRR:155.2,8.0] || product(e_2,e_3,e_1)+ -> product(e_1,e_2,e_4)*. % 0.34/0.52 158[0:MRR:156.2,5.0] || product(e_1,e_3,e_2)*+ -> product(e_2,e_1,e_4). % 0.34/0.52 160[0:Res:17.5,157.0] group_element(e_3) group_element(e_2) || -> product(e_2,e_3,e_4) product(e_2,e_3,e_3) product(e_2,e_3,e_2) product(e_1,e_2,e_4)*. % 0.34/0.52 161[0:SSi:160.1,160.0,2.0,3.0] || -> product(e_2,e_3,e_4) product(e_2,e_3,e_3) product(e_2,e_3,e_2) product(e_1,e_2,e_4)*. % 0.34/0.52 162[0:Res:72.3,158.0] group_element(e_3) || -> product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_3,e_1) product(e_2,e_1,e_4). % 0.34/0.52 163[0:SSi:162.0,3.0] || -> product(e_1,e_3,e_4) product(e_1,e_3,e_3)* equalish(e_3,e_1) product(e_2,e_1,e_4). % 0.34/0.52 164[0:MRR:163.2,11.0] || -> product(e_1,e_3,e_4) product(e_1,e_3,e_3)* product(e_2,e_1,e_4). % 0.34/0.52 165[4:Spt:164.2] || -> product(e_2,e_1,e_4)*. % 0.34/0.52 172[4:Res:165.0,109.0] || -> equalish(e_4,e_3)*. % 0.34/0.52 173[4:MRR:172.0,16.0] || -> . % 0.34/0.52 175[4:Spt:173.0,164.2,165.0] || product(e_2,e_1,e_4)*+ -> . % 0.34/0.52 176[4:Spt:173.0,164.0,164.1] || -> product(e_1,e_3,e_4) product(e_1,e_3,e_3)*. % 0.34/0.52 188[4:Res:176.1,60.0] || -> product(e_1,e_3,e_4)* equalish(e_1,e_3). % 0.34/0.52 190[4:MRR:188.1,6.0] || -> product(e_1,e_3,e_4)*. % 0.34/0.52 205[4:Res:190.0,20.0] || product(u,e_3,e_4)*+ -> equalish(u,e_1). % 0.34/0.52 210[0:Res:21.0,25.0] || product(u,v,w)*+ product(v,w,u)* -> equalish(w,u). % 0.34/0.52 306[5:Spt:161.3] || -> product(e_1,e_2,e_4)*. % 0.34/0.52 318[5:Res:306.0,85.0] || -> equalish(e_4,e_3)*. % 0.34/0.52 320[5:MRR:318.0,16.0] || -> . % 0.34/0.52 323[5:Spt:320.0,161.3,306.0] || product(e_1,e_2,e_4)*+ -> . % 0.34/0.52 324[5:Spt:320.0,161.0,161.1,161.2] || -> product(e_2,e_3,e_4) product(e_2,e_3,e_3) product(e_2,e_3,e_2)*. % 0.34/0.52 341[5:Res:324.2,62.0] || -> product(e_2,e_3,e_4) product(e_2,e_3,e_3)* equalish(e_3,e_2). % 0.34/0.52 342[5:MRR:341.2,12.0] || -> product(e_2,e_3,e_4) product(e_2,e_3,e_3)*. % 0.34/0.52 380[5:Res:342.1,60.0] || -> product(e_2,e_3,e_4)* equalish(e_2,e_3). % 0.34/0.52 383[5:MRR:380.1,9.0] || -> product(e_2,e_3,e_4)*. % 0.34/0.52 395[5:Res:383.0,205.0] || -> equalish(e_2,e_1)*. % 0.34/0.52 396[5:MRR:395.0,8.0] || -> . % 0.34/0.52 400[3:Spt:396.0,106.1] || -> product(e_2,e_1,e_4)*. % 0.34/0.52 404[3:Res:400.0,210.0] || product(e_1,e_4,e_2)* -> equalish(e_4,e_2). % 0.34/0.52 412[3:MRR:404.1,15.0] || product(e_1,e_4,e_2)*+ -> . % 0.34/0.52 414[3:Res:72.3,412.0] group_element(e_4) || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)* equalish(e_4,e_1). % 0.34/0.52 415[3:SSi:414.0,4.0] || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)* equalish(e_4,e_1). % 0.34/0.52 416[3:MRR:415.2,14.0] || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)*. % 0.34/0.52 467[3:Res:416.1,89.0] || -> product(e_1,e_4,e_4)* equalish(e_4,e_2). % 0.34/0.52 468[3:MRR:467.1,15.0] || -> product(e_1,e_4,e_4)*. % 0.34/0.52 482[3:Res:468.0,60.0] || -> equalish(e_1,e_4)*. % 0.34/0.52 483[3:MRR:482.0,7.0] || -> . % 0.34/0.52 486[2:Spt:483.0,83.1] || -> product(e_1,e_2,e_4)*. % 0.34/0.52 498[2:Res:486.0,85.0] || -> equalish(e_4,e_3)*. % 0.34/0.52 499[2:MRR:498.0,16.0] || -> . % 0.34/0.52 502[1:Spt:499.0,82.1] || -> product(e_1,e_2,e_4)*. % 0.34/0.52 506[1:Res:502.0,210.0] || product(e_2,e_4,e_1)* -> equalish(e_4,e_1). % 0.34/0.52 512[1:Res:502.0,19.0] || product(e_1,u,e_4)*+ -> equalish(u,e_2). % 0.34/0.52 514[1:MRR:506.1,14.0] || product(e_2,e_4,e_1)*+ -> . % 0.34/0.52 516[1:Res:17.5,514.0] group_element(e_4) group_element(e_2) || -> product(e_2,e_4,e_4) product(e_2,e_4,e_3) product(e_2,e_4,e_2)*. % 0.34/0.52 517[1:SSi:516.1,516.0,2.0,4.0] || -> product(e_2,e_4,e_4) product(e_2,e_4,e_3) product(e_2,e_4,e_2)*. % 0.34/0.52 527[2:Spt:104.0] || -> product(e_2,e_1,e_4)*. % 0.34/0.52 532[2:Res:527.0,210.0] || product(e_1,e_4,e_2)* -> equalish(e_4,e_2). % 0.34/0.52 538[2:Res:527.0,19.0] || product(e_2,u,e_4)*+ -> equalish(u,e_1). % 0.34/0.52 540[2:MRR:532.1,15.0] || product(e_1,e_4,e_2)*+ -> . % 0.34/0.52 542[2:Res:72.3,540.0] group_element(e_4) || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)* equalish(e_4,e_1). % 0.34/0.52 543[2:SSi:542.0,4.0] || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)* equalish(e_4,e_1). % 0.34/0.52 544[2:MRR:543.2,14.0] || -> product(e_1,e_4,e_4) product(e_1,e_4,e_3)*. % 0.34/0.52 545[2:Res:544.1,42.0] || product(e_4,e_3,u) product(e_1,e_1,u)* -> product(e_1,e_4,e_4) equalish(e_1,e_4). % 0.34/0.52 558[2:MRR:545.2,545.3,60.0,7.0] || product(e_4,e_3,u)+ product(e_1,e_1,u)* -> . % 0.34/0.52 606[2:Res:17.5,558.0] group_element(e_3) group_element(e_4) || product(e_1,e_1,e_1)* -> product(e_4,e_3,e_4) product(e_4,e_3,e_3) product(e_4,e_3,e_2). % 0.34/0.52 607[2:SSi:606.1,606.0,4.0,3.0] || product(e_1,e_1,e_1)* -> product(e_4,e_3,e_4) product(e_4,e_3,e_3) product(e_4,e_3,e_2). % 0.34/0.52 608[2:MRR:607.0,21.0] || -> product(e_4,e_3,e_4) product(e_4,e_3,e_3) product(e_4,e_3,e_2)*. % 0.34/0.52 622[1:Res:517.2,62.0] || -> product(e_2,e_4,e_4) product(e_2,e_4,e_3)* equalish(e_4,e_2). % 0.34/0.53 625[1:MRR:622.2,15.0] || -> product(e_2,e_4,e_4) product(e_2,e_4,e_3)*. % 0.34/0.53 631[1:Res:625.1,210.0] || product(e_4,e_3,e_2) -> product(e_2,e_4,e_4)* equalish(e_3,e_2). % 0.34/0.53 641[1:MRR:631.2,12.0] || product(e_4,e_3,e_2)+ -> product(e_2,e_4,e_4)*. % 0.34/0.53 666[2:Res:608.2,641.0] || -> product(e_4,e_3,e_4) product(e_4,e_3,e_3) product(e_2,e_4,e_4)*. % 0.34/0.53 669[3:Spt:666.2] || -> product(e_2,e_4,e_4)*. % 0.34/0.53 688[3:Res:669.0,538.0] || -> equalish(e_4,e_1)*. % 0.34/0.53 690[3:MRR:688.0,14.0] || -> . % 0.34/0.53 693[3:Spt:690.0,666.2,669.0] || product(e_2,e_4,e_4)*+ -> . % 0.34/0.53 694[3:Spt:690.0,666.0,666.1] || -> product(e_4,e_3,e_4) product(e_4,e_3,e_3)*. % 0.34/0.53 722[3:Res:694.1,60.0] || -> product(e_4,e_3,e_4)* equalish(e_4,e_3). % 0.34/0.53 725[3:MRR:722.1,16.0] || -> product(e_4,e_3,e_4)*. % 0.34/0.53 754[3:Res:725.0,62.0] || -> equalish(e_3,e_4)*. % 0.34/0.53 757[3:MRR:754.0,13.0] || -> . % 0.34/0.53 758[2:Spt:757.0,104.0,527.0] || product(e_2,e_1,e_4)*+ -> . % 0.34/0.53 759[2:Spt:757.0,104.1] || -> product(e_2,e_1,e_3)*. % 0.34/0.53 761[2:MRR:164.2,758.0] || -> product(e_1,e_3,e_4) product(e_1,e_3,e_3)*. % 0.34/0.53 851[2:Res:761.1,60.0] || -> product(e_1,e_3,e_4)* equalish(e_1,e_3). % 0.34/0.53 853[2:MRR:851.1,6.0] || -> product(e_1,e_3,e_4)*. % 0.34/0.53 868[2:Res:853.0,512.0] || -> equalish(e_3,e_2)*. % 0.34/0.53 869[2:MRR:868.0,12.0] || -> . % 0.34/0.53 % SZS output end Refutation % 0.34/0.53 Formulae used in the proof : element_1 element_2 element_3 element_4 e_1_is_not_e_2 e_1_is_not_e_3 e_1_is_not_e_4 e_2_is_not_e_1 e_2_is_not_e_3 e_3_is_not_e_1 e_3_is_not_e_2 e_3_is_not_e_4 e_4_is_not_e_1 e_4_is_not_e_2 e_4_is_not_e_3 product_total_function1 product_total_function2 product_right_cancellation product_left_cancellation product_idempotence qg2_1 qg2_2 % 0.34/0.53 %------------------------------------------------------------------------------