%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP126-3.004 : TPTP v8.1.0. Released v1.2.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n022.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:37 EDT 2022 % Result : Unsatisfiable 0.20s 0.48s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : GRP126-3.004 : TPTP v8.1.0. Released v1.2.0. % 0.07/0.13 % Command : run_spass %d %s % 0.14/0.35 % Computer : n022.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Mon Jun 13 13:24:03 EDT 2022 % 0.14/0.35 % CPUTime : % 0.20/0.48 % 0.20/0.48 SPASS V 3.9 % 0.20/0.48 SPASS beiseite: Proof found. % 0.20/0.48 % SZS status Theorem % 0.20/0.48 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.48 SPASS derived 406 clauses, backtracked 262 clauses, performed 12 splits and kept 486 clauses. % 0.20/0.48 SPASS allocated 76025 KBytes. % 0.20/0.48 SPASS spent 0:00:00.13 on the problem. % 0.20/0.48 0:00:00.04 for the input. % 0.20/0.48 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.48 0:00:00.01 for inferences. % 0.20/0.48 0:00:00.00 for the backtracking. % 0.20/0.48 0:00:00.06 for the reduction. % 0.20/0.48 % 0.20/0.48 % 0.20/0.48 Here is a proof with depth 16, length 113 : % 0.20/0.48 % SZS output start Refutation % 0.20/0.48 3[0:Inp] || -> next(e_2,e_3)*. % 0.20/0.48 5[0:Inp] || -> greater(e_1,e_0)*. % 0.20/0.48 6[0:Inp] || -> greater(e_2,e_0)*. % 0.20/0.48 7[0:Inp] || -> greater(e_3,e_0)*. % 0.20/0.48 12[0:Inp] || -> greater(e_3,e_2)*. % 0.20/0.48 13[0:Inp] || -> greater(e_4,e_2)*. % 0.20/0.48 16[0:Inp] group_element(u) || -> cycle(u,e_3) cycle(u,e_2) cycle(u,e_1) cycle(u,e_0)*. % 0.20/0.48 20[0:Inp] || greater(u,v) cycle(v,e_0) product(v,e_1,u)*+ -> . % 0.20/0.48 21[0:Inp] || next(u,v)* cycle(u,w)* greater(w,e_0)* product(u,e_1,x)*+ -> equalish(x,v)*. % 0.20/0.48 22[0:Inp] || -> group_element(e_1)*. % 0.20/0.48 23[0:Inp] || -> group_element(e_2)*. % 0.20/0.48 24[0:Inp] || -> group_element(e_3)*. % 0.20/0.48 25[0:Inp] || -> group_element(e_4)*. % 0.20/0.48 26[0:Inp] || equalish(e_1,e_2)*+ -> . % 0.20/0.48 27[0:Inp] || equalish(e_1,e_3)*+ -> . % 0.20/0.48 28[0:Inp] || equalish(e_1,e_4)*+ -> . % 0.20/0.48 29[0:Inp] || equalish(e_2,e_1)*+ -> . % 0.20/0.48 30[0:Inp] || equalish(e_2,e_3)*+ -> . % 0.20/0.48 32[0:Inp] || equalish(e_3,e_1)*+ -> . % 0.20/0.48 35[0:Inp] || equalish(e_4,e_1)*+ -> . % 0.20/0.48 36[0:Inp] || equalish(e_4,e_2)*+ -> . % 0.20/0.48 37[0:Inp] || equalish(e_4,e_3)*+ -> . % 0.20/0.48 38[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.20/0.48 39[0:Inp] || product(u,v,w)*+ product(u,v,x)* -> equalish(x,w)*. % 0.20/0.48 40[0:Inp] || product(u,v,w)*+ product(u,x,w)* -> equalish(x,v)*. % 0.20/0.48 41[0:Inp] || product(u,v,w)*+ product(x,v,w)* -> equalish(x,u)*. % 0.20/0.48 42[0:Inp] || -> product(u,u,u)*. % 0.20/0.48 43[0:Inp] || product(u,v,w)*+ product(v,u,x)* -> product(x,w,u)*. % 0.20/0.48 55[0:Res:42.0,41.0] || product(u,v,v)*+ -> equalish(u,v). % 0.20/0.48 57[0:Res:42.0,40.0] || product(u,v,u)*+ -> equalish(v,u). % 0.20/0.48 59[0:Res:42.0,39.0] || product(u,u,v)*+ -> equalish(v,u). % 0.20/0.48 81[0:Res:38.5,55.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.20/0.48 83[0:SSi:81.0,22.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.20/0.48 97[0:Res:83.3,57.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.20/0.48 104[0:SSi:97.0,23.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.20/0.48 105[0:MRR:104.2,104.3,29.0,26.0] || -> product(e_2,e_1,e_4) product(e_2,e_1,e_3)*. % 0.20/0.48 106[0:Res:105.1,20.2] || greater(e_3,e_2) cycle(e_2,e_0) -> product(e_2,e_1,e_4)*. % 0.20/0.48 107[0:Res:105.1,43.0] || product(e_1,e_2,u)* -> product(e_2,e_1,e_4) product(u,e_3,e_2)*. % 0.20/0.48 108[0:Res:105.1,39.0] || product(e_2,e_1,u)*+ -> product(e_2,e_1,e_4)* equalish(u,e_3). % 0.20/0.48 109[0:Res:105.1,40.0] || product(e_2,u,e_3)*+ -> product(e_2,e_1,e_4)* equalish(u,e_1). % 0.20/0.48 110[0:Res:105.1,41.0] || product(u,e_1,e_3)*+ -> product(e_2,e_1,e_4)* equalish(u,e_2). % 0.20/0.48 112[0:MRR:106.0,12.0] || cycle(e_2,e_0)+ -> product(e_2,e_1,e_4)*. % 0.20/0.48 113[0:Res:16.4,112.0] group_element(e_2) || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 0.20/0.48 114[0:SSi:113.0,23.0] || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1) product(e_2,e_1,e_4)*. % 0.20/0.48 115[1:Spt:108.0,108.2] || product(e_2,e_1,u)*+ -> equalish(u,e_3). % 0.20/0.48 129[2:Spt:109.0,109.2] || product(e_2,u,e_3)*+ -> equalish(u,e_1). % 0.20/0.48 131[3:Spt:110.0,110.2] || product(u,e_1,e_3)*+ -> equalish(u,e_2). % 0.20/0.48 133[4:Spt:114.3] || -> product(e_2,e_1,e_4)*. % 0.20/0.48 140[4:Res:133.0,115.0] || -> equalish(e_4,e_3)*. % 0.20/0.48 141[4:MRR:140.0,37.0] || -> . % 0.20/0.48 143[4:Spt:141.0,114.3,133.0] || product(e_2,e_1,e_4)*+ -> . % 0.20/0.48 144[4:Spt:141.0,114.0,114.1,114.2] || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.48 147[4:MRR:107.1,143.0] || product(e_1,e_2,u)*+ -> product(u,e_3,e_2)*. % 0.20/0.48 162[4:Res:38.5,147.0] group_element(e_2) group_element(e_1) || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3) product(e_1,e_2,e_2)* product(e_1,e_3,e_2). % 0.20/0.48 163[4:SSi:162.1,162.0,22.0,23.0] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3) product(e_1,e_2,e_2)* product(e_1,e_3,e_2). % 0.20/0.48 177[4:Res:163.2,55.0] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)* product(e_1,e_3,e_2) equalish(e_1,e_2). % 0.20/0.48 178[4:MRR:177.3,26.0] || -> product(e_1,e_2,e_4) product(e_1,e_2,e_3)* product(e_1,e_3,e_2). % 0.20/0.48 183[4:Res:178.1,147.0] || -> product(e_1,e_2,e_4)* product(e_1,e_3,e_2) product(e_3,e_3,e_2). % 0.20/0.48 188[5:Spt:183.0] || -> product(e_1,e_2,e_4)*. % 0.20/0.48 189[5:Res:188.0,147.0] || -> product(e_4,e_3,e_2)*. % 0.20/0.48 196[5:Res:189.0,40.0] || product(e_4,u,e_2)*+ -> equalish(u,e_3). % 0.20/0.48 208[5:Res:83.3,196.0] group_element(e_4) || -> product(e_4,e_1,e_4) product(e_4,e_1,e_3)* equalish(e_4,e_1) equalish(e_1,e_3). % 0.20/0.48 210[5:SSi:208.0,25.0] || -> product(e_4,e_1,e_4) product(e_4,e_1,e_3)* equalish(e_4,e_1) equalish(e_1,e_3). % 0.20/0.48 211[5:MRR:210.2,210.3,35.0,27.0] || -> product(e_4,e_1,e_4) product(e_4,e_1,e_3)*. % 0.20/0.48 223[5:Res:211.1,131.0] || -> product(e_4,e_1,e_4)* equalish(e_4,e_2). % 0.20/0.48 224[5:MRR:223.1,36.0] || -> product(e_4,e_1,e_4)*. % 0.20/0.48 225[5:Res:224.0,57.0] || -> equalish(e_1,e_4)*. % 0.20/0.48 232[5:MRR:225.0,28.0] || -> . % 0.20/0.48 234[5:Spt:232.0,183.0,188.0] || product(e_1,e_2,e_4)*+ -> . % 0.20/0.48 235[5:Spt:232.0,183.1,183.2] || -> product(e_1,e_3,e_2)* product(e_3,e_3,e_2). % 0.20/0.48 241[6:Spt:235.0] || -> product(e_1,e_3,e_2)*. % 0.20/0.48 242[6:Res:241.0,43.0] || product(e_3,e_1,u)*+ -> product(u,e_2,e_1)*. % 0.20/0.48 266[6:Res:83.3,242.0] group_element(e_3) || -> product(e_3,e_1,e_4) product(e_3,e_1,e_3) equalish(e_3,e_1) product(e_2,e_2,e_1)*. % 0.20/0.48 267[6:SSi:266.0,24.0] || -> product(e_3,e_1,e_4) product(e_3,e_1,e_3) equalish(e_3,e_1) product(e_2,e_2,e_1)*. % 0.20/0.48 268[6:MRR:267.2,32.0] || -> product(e_3,e_1,e_4) product(e_3,e_1,e_3) product(e_2,e_2,e_1)*. % 0.20/0.48 286[6:Res:268.2,59.0] || -> product(e_3,e_1,e_4) product(e_3,e_1,e_3)* equalish(e_1,e_2). % 0.20/0.48 293[6:MRR:286.2,26.0] || -> product(e_3,e_1,e_4) product(e_3,e_1,e_3)*. % 0.20/0.48 294[6:Res:293.1,57.0] || -> product(e_3,e_1,e_4)* equalish(e_1,e_3). % 0.20/0.48 303[6:MRR:294.1,27.0] || -> product(e_3,e_1,e_4)*. % 0.20/0.48 306[6:Res:303.0,43.0] || product(e_1,e_3,u)*+ -> product(u,e_4,e_3)*. % 0.20/0.48 386[6:Res:241.0,306.0] || -> product(e_2,e_4,e_3)*. % 0.20/0.48 400[6:Res:386.0,129.0] || -> equalish(e_4,e_1)*. % 0.20/0.48 405[6:MRR:400.0,35.0] || -> . % 0.20/0.48 406[6:Spt:405.0,235.0,241.0] || product(e_1,e_3,e_2)* -> . % 0.20/0.48 407[6:Spt:405.0,235.1] || -> product(e_3,e_3,e_2)*. % 0.20/0.48 414[6:Res:407.0,59.0] || -> equalish(e_2,e_3)*. % 0.20/0.48 421[6:MRR:414.0,30.0] || -> . % 0.20/0.48 422[3:Spt:421.0,110.1] || -> product(e_2,e_1,e_4)*. % 0.20/0.48 429[3:Res:422.0,115.0] || -> equalish(e_4,e_3)*. % 0.20/0.48 430[3:MRR:429.0,37.0] || -> . % 0.20/0.48 432[2:Spt:430.0,109.1] || -> product(e_2,e_1,e_4)*. % 0.20/0.48 439[2:Res:432.0,115.0] || -> equalish(e_4,e_3)*. % 0.20/0.48 440[2:MRR:439.0,37.0] || -> . % 0.20/0.48 442[1:Spt:440.0,108.1] || -> product(e_2,e_1,e_4)*. % 0.20/0.48 443[1:Res:442.0,20.2] || greater(e_4,e_2)* cycle(e_2,e_0) -> . % 0.20/0.48 448[1:Res:442.0,21.3] || next(e_2,u)+ cycle(e_2,v) greater(v,e_0)* -> equalish(e_4,u)*. % 0.20/0.48 449[1:MRR:443.0,13.0] || cycle(e_2,e_0)*+ -> . % 0.20/0.48 450[1:Res:16.4,449.0] group_element(e_2) || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.48 451[1:SSi:450.0,23.0] || -> cycle(e_2,e_3) cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.48 471[2:Spt:451.0] || -> cycle(e_2,e_3)*. % 0.20/0.48 544[1:Res:3.0,448.0] || cycle(e_2,u) greater(u,e_0)* -> equalish(e_4,e_3)*. % 0.20/0.48 545[1:MRR:544.2,37.0] || cycle(e_2,u)+ greater(u,e_0)* -> . % 0.20/0.48 551[2:Res:471.0,545.0] || greater(e_3,e_0)* -> . % 0.20/0.48 552[2:MRR:551.0,7.0] || -> . % 0.20/0.48 553[2:Spt:552.0,451.0,471.0] || cycle(e_2,e_3)* -> . % 0.20/0.48 554[2:Spt:552.0,451.1,451.2] || -> cycle(e_2,e_2) cycle(e_2,e_1)*. % 0.20/0.48 567[3:Spt:554.0] || -> cycle(e_2,e_2)*. % 0.20/0.48 574[3:Res:567.0,545.0] || greater(e_2,e_0)* -> . % 0.20/0.48 575[3:MRR:574.0,6.0] || -> . % 0.20/0.48 576[3:Spt:575.0,554.0,567.0] || cycle(e_2,e_2)* -> . % 0.20/0.48 577[3:Spt:575.0,554.1] || -> cycle(e_2,e_1)*. % 0.20/0.48 582[3:Res:577.0,545.0] || greater(e_1,e_0)* -> . % 0.20/0.48 583[3:MRR:582.0,5.0] || -> . % 0.20/0.48 % SZS output end Refutation % 0.20/0.48 Formulae used in the proof : e_2_then_e_3 e_1_greater_e_0 e_2_greater_e_0 e_3_greater_e_0 e_3_greater_e_2 e_4_greater_e_2 cycle2 cycle6 cycle7 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_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 qg4 % 0.20/0.49 %------------------------------------------------------------------------------