%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP135-2.002 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:52 EDT 2022 % Result : Unsatisfiable 0.11s 0.42s % Output : Refutation 0.11s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.06 % Problem : GRP135-2.002 : TPTP v8.1.0. Released v1.2.0. % 0.00/0.07 % Command : run_spass %d %s % 0.06/0.26 % Computer : n007.cluster.edu % 0.06/0.26 % Model : x86_64 x86_64 % 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.26 % Memory : 8042.1875MB % 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.26 % CPULimit : 300 % 0.06/0.27 % WCLimit : 600 % 0.06/0.27 % DateTime : Tue Jun 14 12:11:09 EDT 2022 % 0.06/0.27 % CPUTime : % 0.11/0.42 % 0.11/0.42 SPASS V 3.9 % 0.11/0.42 SPASS beiseite: Proof found. % 0.11/0.42 % SZS status Theorem % 0.11/0.42 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.11/0.42 SPASS derived 434 clauses, backtracked 81 clauses, performed 11 splits and kept 342 clauses. % 0.11/0.42 SPASS allocated 76050 KBytes. % 0.11/0.42 SPASS spent 0:00:00.15 on the problem. % 0.11/0.42 0:00:00.04 for the input. % 0.11/0.42 0:00:00.00 for the FLOTTER CNF translation. % 0.11/0.42 0:00:00.01 for inferences. % 0.11/0.42 0:00:00.00 for the backtracking. % 0.11/0.42 0:00:00.08 for the reduction. % 0.11/0.42 % 0.11/0.42 % 0.11/0.42 Here is a proof with depth 13, length 96 : % 0.11/0.42 % SZS output start Refutation % 0.11/0.42 4[0:Inp] || -> group_element(e_1)*. % 0.11/0.42 5[0:Inp] || -> group_element(e_2)*. % 0.11/0.42 6[0:Inp] || equalish(e_1,e_2)*+ -> . % 0.11/0.42 7[0:Inp] || equalish(e_2,e_1)*+ -> . % 0.11/0.42 8[0:Inp] group_element(u) group_element(v) || -> product(v,u,e_2) product(v,u,e_1)*. % 0.11/0.42 9[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 0.11/0.42 10[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 0.11/0.42 11[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 0.11/0.42 12[0:Inp] || product(u,v,w)*+ product(v,x,u)* -> product(w,v,x)*. % 0.11/0.42 16[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.11/0.42 17[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.11/0.42 20[0:Res:8.3,12.0] group_element(u) group_element(v) || product(u,w,v)*+ -> product(v,u,e_2)* product(e_1,u,w)*. % 0.11/0.42 21[0:Res:8.3,16.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.11/0.42 22[0:Obv:21.4] group_element(u) group_element(v) || -> product(v,u,e_2)* equalish(e_1,e_1). % 0.11/0.42 25[1:Spt:22.0,22.1,22.2] group_element(u) group_element(v) || -> product(v,u,e_2)*. % 0.11/0.42 29[1:Res:25.2,10.0] group_element(u) group_element(v) || product(v,w,e_2)*+ -> equalish(w,u)*. % 0.11/0.42 36[1:Res:25.2,29.2] group_element(u) group_element(v) group_element(w) group_element(v) || -> equalish(u,w)*. % 0.11/0.42 37[1:Obv:36.1] group_element(u) group_element(v) group_element(w) || -> equalish(u,v)*. % 0.11/0.42 38[1:Con:37.2] group_element(u) group_element(v) || -> equalish(u,v)*. % 0.11/0.42 42[1:Res:38.2,6.0] group_element(e_1) group_element(e_2) || -> . % 0.11/0.42 44[1:SSi:42.1,42.0,5.0,4.0] || -> . % 0.11/0.42 45[1:Spt:44.0,22.3] || -> equalish(e_1,e_1)*. % 0.11/0.42 57[0:Res:8.3,20.2] group_element(u) group_element(v) group_element(v) group_element(e_1) || -> product(v,u,e_2)* product(e_1,v,e_2)* product(e_1,v,u)*. % 0.11/0.42 58[0:Obv:57.1] group_element(u) group_element(v) group_element(e_1) || -> product(v,u,e_2)* product(e_1,v,e_2)* product(e_1,v,u)*. % 0.11/0.42 59[0:SSi:58.2,4.0] group_element(u) group_element(v) || -> product(v,u,e_2)* product(e_1,v,e_2)* product(e_1,v,u)*. % 0.11/0.42 60[0:Fac:59.3,59.4] group_element(e_2) group_element(u) || -> product(u,e_2,e_2)* product(e_1,u,e_2)*. % 0.11/0.42 67[0:Res:59.2,20.2] group_element(u) group_element(v) group_element(v) group_element(e_2) || -> product(e_1,v,e_2)* product(e_1,v,u)* product(e_2,v,e_2) product(e_1,v,u)*. % 0.11/0.42 84[0:SSi:60.0,5.0] group_element(u) || -> product(u,e_2,e_2)* product(e_1,u,e_2)*. % 0.11/0.42 96[0:Obv:67.5] group_element(u) group_element(v) group_element(e_2) || -> product(e_1,v,e_2)* product(e_2,v,e_2) product(e_1,v,u)*. % 0.11/0.42 97[0:Con:96.0] group_element(u) group_element(e_2) || -> product(e_1,u,e_2)* product(e_2,u,e_2). % 0.11/0.42 98[0:SSi:97.1,5.0] group_element(u) || -> product(e_1,u,e_2)* product(e_2,u,e_2). % 0.11/0.42 126[0:Res:84.1,11.0] group_element(u) || product(v,e_2,e_2)* -> product(e_1,u,e_2)* equalish(v,u)*. % 0.11/0.42 135[0:Res:84.2,20.2] group_element(u) group_element(e_1) group_element(e_2) || -> product(u,e_2,e_2)* product(e_2,e_1,e_2) product(e_1,e_1,u)*. % 0.11/0.42 139[0:SSi:135.2,135.1,5.0,4.0] group_element(u) || -> product(u,e_2,e_2)* product(e_2,e_1,e_2) product(e_1,e_1,u)*. % 0.11/0.42 218[2:Spt:139.0,139.1,139.3] group_element(u) || -> product(u,e_2,e_2)* product(e_1,e_1,u)*. % 0.11/0.42 231[2:Res:218.2,17.2] group_element(e_1) group_element(u) group_element(e_1) || -> product(e_1,e_2,e_2)* product(e_1,u,e_2)* equalish(e_1,u). % 0.11/0.42 236[2:Obv:231.0] group_element(u) group_element(e_1) || -> product(e_1,e_2,e_2)* product(e_1,u,e_2)* equalish(e_1,u). % 0.11/0.42 237[2:SSi:236.1,4.0] group_element(u) || -> product(e_1,e_2,e_2)* product(e_1,u,e_2)* equalish(e_1,u). % 0.11/0.42 238[2:MRR:237.1,126.1] group_element(u) || -> product(e_1,u,e_2)* equalish(e_1,u). % 0.11/0.42 251[2:Res:238.1,20.2] group_element(u) group_element(e_1) group_element(e_2) || -> equalish(e_1,u) product(e_2,e_1,e_2) product(e_1,e_1,u)*. % 0.11/0.42 253[2:SSi:251.2,251.1,5.0,4.0] group_element(u) || -> equalish(e_1,u) product(e_2,e_1,e_2) product(e_1,e_1,u)*. % 0.11/0.42 276[3:Spt:253.0,253.1,253.3] group_element(u) || -> equalish(e_1,u) product(e_1,e_1,u)*. % 0.11/0.42 282[3:Res:276.2,16.2] group_element(u) group_element(e_1) group_element(e_1) || -> equalish(e_1,u)* product(e_1,e_1,e_2)* equalish(u,e_1)*. % 0.11/0.42 286[3:Obv:282.1] group_element(u) group_element(e_1) || -> equalish(e_1,u)* product(e_1,e_1,e_2)* equalish(u,e_1)*. % 0.11/0.42 287[3:SSi:286.1,4.0] group_element(u) || -> equalish(e_1,u)* product(e_1,e_1,e_2)* equalish(u,e_1)*. % 0.11/0.42 291[4:Spt:287.0,287.1,287.3] group_element(u) || -> equalish(e_1,u)* equalish(u,e_1)*. % 0.11/0.42 293[4:Res:291.1,6.0] group_element(e_2) || -> equalish(e_2,e_1)*. % 0.11/0.42 294[4:SSi:293.0,5.0] || -> equalish(e_2,e_1)*. % 0.11/0.42 295[4:MRR:294.0,7.0] || -> . % 0.11/0.42 296[4:Spt:295.0,287.2] || -> product(e_1,e_1,e_2)*. % 0.11/0.42 299[4:Res:296.0,9.0] || product(e_1,e_1,u)*+ -> equalish(u,e_2). % 0.11/0.42 300[4:Res:296.0,10.0] || product(e_1,u,e_2)*+ -> equalish(u,e_1). % 0.11/0.42 303[4:Res:296.0,20.2] group_element(e_1) group_element(e_2) || -> product(e_2,e_1,e_2) product(e_1,e_1,e_1)*. % 0.11/0.42 305[4:SSi:303.1,303.0,5.0,4.0] || -> product(e_2,e_1,e_2) product(e_1,e_1,e_1)*. % 0.11/0.42 307[5:Spt:305.0] || -> product(e_2,e_1,e_2)*. % 0.11/0.42 311[5:Res:307.0,10.0] || product(e_2,u,e_2)* -> equalish(u,e_1). % 0.11/0.42 369[4:Res:98.1,300.0] group_element(u) || -> product(e_2,u,e_2)* equalish(u,e_1). % 0.11/0.42 374[5:MRR:369.1,311.0] group_element(u) || -> equalish(u,e_1)*. % 0.11/0.42 377[5:Res:374.1,7.0] group_element(e_2) || -> . % 0.11/0.42 378[5:SSi:377.0,5.0] || -> . % 0.11/0.42 379[5:Spt:378.0,305.0,307.0] || product(e_2,e_1,e_2)* -> . % 0.11/0.42 380[5:Spt:378.0,305.1] || -> product(e_1,e_1,e_1)*. % 0.11/0.42 390[5:Res:380.0,299.0] || -> equalish(e_1,e_2)*. % 0.11/0.42 399[5:MRR:390.0,6.0] || -> . % 0.11/0.42 402[3:Spt:399.0,253.2] || -> product(e_2,e_1,e_2)*. % 0.11/0.42 406[3:Res:402.0,10.0] || product(e_2,u,e_2)*+ -> equalish(u,e_1). % 0.11/0.42 407[3:Res:402.0,11.0] || product(u,e_1,e_2)*+ -> equalish(u,e_2). % 0.11/0.42 409[3:Res:402.0,20.2] group_element(e_2) group_element(e_2) || -> product(e_2,e_2,e_2) product(e_1,e_2,e_1)*. % 0.11/0.42 410[3:Obv:409.0] group_element(e_2) || -> product(e_2,e_2,e_2) product(e_1,e_2,e_1)*. % 0.11/0.42 411[3:SSi:410.0,5.0] || -> product(e_2,e_2,e_2) product(e_1,e_2,e_1)*. % 0.11/0.42 438[3:Res:411.1,20.2] group_element(e_1) group_element(e_1) || -> product(e_2,e_2,e_2) product(e_1,e_1,e_2)* product(e_1,e_1,e_2)*. % 0.11/0.42 442[3:Obv:438.3] group_element(e_1) || -> product(e_2,e_2,e_2) product(e_1,e_1,e_2)*. % 0.11/0.42 443[3:SSi:442.0,4.0] || -> product(e_2,e_2,e_2) product(e_1,e_1,e_2)*. % 0.11/0.42 444[4:Spt:443.0] || -> product(e_2,e_2,e_2)*. % 0.11/0.42 474[4:Res:444.0,406.0] || -> equalish(e_2,e_1)*. % 0.11/0.42 475[4:MRR:474.0,7.0] || -> . % 0.11/0.42 483[4:Spt:475.0,443.0,444.0] || product(e_2,e_2,e_2)*+ -> . % 0.11/0.42 484[4:Spt:475.0,443.1] || -> product(e_1,e_1,e_2)*. % 0.11/0.42 527[4:Res:484.0,407.0] || -> equalish(e_1,e_2)*. % 0.11/0.42 541[4:MRR:527.0,6.0] || -> . % 0.11/0.42 548[2:Spt:541.0,139.2] || -> product(e_2,e_1,e_2)*. % 0.11/0.42 552[2:Res:548.0,10.0] || product(e_2,u,e_2)*+ -> equalish(u,e_1). % 0.11/0.42 553[2:Res:548.0,11.0] || product(u,e_1,e_2)*+ -> equalish(u,e_2). % 0.11/0.42 555[2:Res:548.0,20.2] group_element(e_2) group_element(e_2) || -> product(e_2,e_2,e_2) product(e_1,e_2,e_1)*. % 0.11/0.42 556[2:Obv:555.0] group_element(e_2) || -> product(e_2,e_2,e_2) product(e_1,e_2,e_1)*. % 0.11/0.42 557[2:SSi:556.0,5.0] || -> product(e_2,e_2,e_2) product(e_1,e_2,e_1)*. % 0.11/0.42 565[2:Res:557.1,20.2] group_element(e_1) group_element(e_1) || -> product(e_2,e_2,e_2) product(e_1,e_1,e_2)* product(e_1,e_1,e_2)*. % 0.11/0.42 569[2:Obv:565.3] group_element(e_1) || -> product(e_2,e_2,e_2) product(e_1,e_1,e_2)*. % 0.11/0.42 570[2:SSi:569.0,4.0] || -> product(e_2,e_2,e_2) product(e_1,e_1,e_2)*. % 0.11/0.42 571[3:Spt:570.0] || -> product(e_2,e_2,e_2)*. % 0.11/0.42 601[3:Res:571.0,552.0] || -> equalish(e_2,e_1)*. % 0.11/0.42 602[3:MRR:601.0,7.0] || -> . % 0.11/0.42 610[3:Spt:602.0,570.0,571.0] || product(e_2,e_2,e_2)*+ -> . % 0.11/0.42 611[3:Spt:602.0,570.1] || -> product(e_1,e_1,e_2)*. % 0.11/0.42 652[3:Res:611.0,553.0] || -> equalish(e_1,e_2)*. % 0.11/0.42 665[3:MRR:652.0,6.0] || -> . % 0.11/0.42 % SZS output end Refutation % 0.11/0.43 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 qg3 % 0.11/0.43 %------------------------------------------------------------------------------