%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP264-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n010.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:46:35 EDT 2022 % Result : Unsatisfiable 0.19s 0.47s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP264-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n010.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 : Mon Jun 13 17:43:24 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.47 % 0.19/0.47 SPASS V 3.9 % 0.19/0.47 SPASS beiseite: Proof found. % 0.19/0.47 % SZS status Theorem % 0.19/0.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.47 SPASS derived 514 clauses, backtracked 176 clauses, performed 9 splits and kept 341 clauses. % 0.19/0.47 SPASS allocated 63537 KBytes. % 0.19/0.47 SPASS spent 0:00:00.12 on the problem. % 0.19/0.47 0:00:00.04 for the input. % 0.19/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.47 0:00:00.00 for inferences. % 0.19/0.47 0:00:00.00 for the backtracking. % 0.19/0.47 0:00:00.05 for the reduction. % 0.19/0.47 % 0.19/0.47 % 0.19/0.47 Here is a proof with depth 5, length 191 : % 0.19/0.47 % SZS output start Refutation % 0.19/0.47 1[0:Inp] || -> equal(multiply(sk_c3,sk_c9),sk_c8)** equal(multiply(sk_c1,sk_c9),sk_c8). % 0.19/0.47 2[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.19/0.47 4[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.19/0.47 7[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.19/0.47 8[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.47 9[0:Inp] || -> equal(inverse(sk_c3),sk_c9)** equal(inverse(sk_c1),sk_c9). % 0.19/0.47 10[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.47 11[0:Inp] || -> equal(inverse(sk_c4),sk_c7)** equal(inverse(sk_c1),sk_c9). % 0.19/0.47 12[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.19/0.47 13[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.47 14[0:Inp] || -> equal(inverse(sk_c5),sk_c8)** equal(inverse(sk_c1),sk_c9). % 0.19/0.47 17[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.47 18[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.47 19[0:Inp] || -> equal(multiply(sk_c8,sk_c6),sk_c7) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.47 20[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.47 21[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.47 22[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.47 23[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(inverse(sk_c2),sk_c8)**. % 0.19/0.47 24[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.47 25[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(inverse(sk_c2),sk_c8)**. % 0.19/0.47 26[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.19/0.47 27[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.47 28[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c2),sk_c8)**. % 0.19/0.47 29[0:Inp] || equal(multiply(u,sk_c9),sk_c8)** equal(inverse(u),sk_c9) equal(multiply(v,sk_c8),sk_c7)** equal(inverse(v),sk_c8) equal(multiply(w,sk_c9),sk_c8)** equal(inverse(w),sk_c9) equal(multiply(x,sk_c7),sk_c8)** equal(inverse(x),sk_c7) equal(multiply(sk_c8,y),sk_c7)** equal(multiply(z,sk_c8),y)* equal(inverse(z),sk_c8) -> . % 0.19/0.47 30[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.47 31[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.47 32[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.47 33[0:Con:29.4] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(multiply(u,sk_c8),y)*+ equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(x,sk_c9),sk_c8)** equal(multiply(sk_c8,y),sk_c7)** -> . % 0.19/0.47 34[1:Spt:33.3,33.7] || equal(inverse(u),sk_c9) equal(multiply(u,sk_c9),sk_c8)** -> . % 0.19/0.47 37[2:Spt:14.1] || -> equal(inverse(sk_c1),sk_c9)**. % 0.19/0.47 43[3:Spt:4.1] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.19/0.47 45[3:SpL:43.0,34.1] || equal(inverse(sk_c1),sk_c9)** equal(sk_c8,sk_c8) -> . % 0.19/0.47 46[3:Obv:45.1] || equal(inverse(sk_c1),sk_c9)** -> . % 0.19/0.47 47[3:Rew:37.0,46.0] || equal(sk_c9,sk_c9)* -> . % 0.19/0.47 48[3:Obv:47.0] || -> . % 0.19/0.47 49[3:Spt:48.0,4.1,43.0] || equal(multiply(sk_c1,sk_c9),sk_c8)** -> . % 0.19/0.47 50[3:Spt:48.0,4.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.47 52[3:MRR:2.1,49.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.19/0.47 56[3:MRR:1.1,49.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.47 64[3:SpL:56.0,34.1] || equal(inverse(sk_c3),sk_c9)** equal(sk_c8,sk_c8) -> . % 0.19/0.47 65[3:Obv:64.1] || equal(inverse(sk_c3),sk_c9)** -> . % 0.19/0.47 66[3:Rew:52.0,65.0] || equal(sk_c9,sk_c9)* -> . % 0.19/0.47 67[3:Obv:66.0] || -> . % 0.19/0.47 68[2:Spt:67.0,14.1,37.0] || equal(inverse(sk_c1),sk_c9)** -> . % 0.19/0.47 69[2:Spt:67.0,14.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.47 71[2:MRR:9.1,68.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.19/0.47 75[2:MRR:8.0,68.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.47 83[2:SpL:75.0,34.1] || equal(inverse(sk_c3),sk_c9)** equal(sk_c8,sk_c8) -> . % 0.19/0.47 84[2:Obv:83.1] || equal(inverse(sk_c3),sk_c9)** -> . % 0.19/0.47 85[2:Rew:71.0,84.0] || equal(sk_c9,sk_c9)* -> . % 0.19/0.47 86[2:Obv:85.0] || -> . % 0.19/0.47 87[1:Spt:86.0,33.0,33.1,33.2,33.4,33.5,33.6,33.8] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),x)*+ equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c8,x),sk_c7)** -> . % 0.19/0.47 88[1:EqR:87.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.19/0.47 90[2:Spt:11.1] || -> equal(inverse(sk_c1),sk_c9)**. % 0.19/0.47 92[3:Spt:28.1] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.47 94[4:Spt:7.1] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.19/0.47 96[5:Spt:21.1] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.47 98[5:SpL:96.0,87.3] || equal(inverse(sk_c2),sk_c8) equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(sk_c7,w) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(sk_c8,w),sk_c7)** -> . % 0.19/0.47 99[5:Rew:92.0,98.0] || equal(sk_c8,sk_c8) equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(sk_c7,w) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(sk_c8,w),sk_c7)** -> . % 0.19/0.47 100[5:Obv:99.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(sk_c7,w) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(sk_c8,w),sk_c7)** -> . % 0.19/0.47 102[2:SpR:90.0,31.0] || -> equal(multiply(sk_c9,sk_c1),identity)**. % 0.19/0.47 103[3:SpR:92.0,31.0] || -> equal(multiply(sk_c8,sk_c2),identity)**. % 0.19/0.47 110[0:SpR:31.0,32.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.47 112[3:SpR:103.0,32.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),multiply(identity,u))**. % 0.19/0.47 116[3:Rew:30.0,112.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),u)**. % 0.19/0.47 118[0:Rew:30.0,110.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.47 122[5:SpR:96.0,116.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.19/0.47 125[0:SpR:118.0,118.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.47 128[0:SpR:31.0,118.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.47 133[2:SpR:102.0,118.0] || -> equal(multiply(inverse(sk_c9),identity),sk_c1)**. % 0.19/0.47 140[0:Rew:125.0,128.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.47 141[2:Rew:140.0,133.0] || -> equal(inverse(sk_c9),sk_c1)**. % 0.19/0.47 143[2:SpR:141.0,31.0] || -> equal(multiply(sk_c1,sk_c9),identity)**. % 0.19/0.47 144[2:SpR:141.0,118.0] || -> equal(multiply(sk_c1,multiply(sk_c9,u)),u)**. % 0.19/0.47 146[4:Rew:94.0,143.0] || -> equal(identity,sk_c8)**. % 0.19/0.47 147[4:Rew:146.0,30.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.47 148[4:Rew:146.0,31.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.19/0.47 150[4:Rew:146.0,103.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.19/0.47 154[4:Rew:146.0,140.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.47 157[5:Rew:147.0,122.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.47 161[5:Rew:147.0,100.5] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(sk_c7,w)* equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** equal(w,sk_c7)* -> . % 0.19/0.47 164[4:Rew:147.0,150.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.47 165[4:Rew:164.0,92.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.47 172[5:Obv:161.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** equal(w,sk_c7)* -> . % 0.19/0.47 173[5:Con:172.4] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** -> . % 0.19/0.47 174[5:Rew:154.0,173.3,157.0,173.3,154.0,173.2,157.0,173.2,157.0,173.0] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(u,sk_c8) equal(v,sk_c8) -> . % 0.19/0.47 175[5:Con:174.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.47 212[4:SpR:148.0,118.0] || -> equal(multiply(inverse(inverse(u)),sk_c8),u)**. % 0.19/0.47 218[4:Rew:154.0,212.0] || -> equal(inverse(inverse(u)),u)**. % 0.19/0.47 283[5:SpL:165.0,175.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.48 285[5:Obv:283.1] || -> . % 0.19/0.48 286[5:Spt:285.0,21.1,96.0] || equal(multiply(sk_c2,sk_c8),sk_c7)** -> . % 0.19/0.48 287[5:Spt:285.0,21.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.48 288[5:Rew:147.0,286.0,164.0,286.0] || equal(sk_c7,sk_c8)** -> . % 0.19/0.48 289[4:Rew:164.0,18.1,154.0,18.1] || -> equal(inverse(sk_c4),sk_c7)** equal(sk_c7,sk_c8). % 0.19/0.48 290[5:MRR:289.1,288.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.48 293[4:Rew:164.0,20.1,154.0,20.1,154.0,20.0] || -> equal(sk_c5,sk_c6)** equal(sk_c7,sk_c8). % 0.19/0.48 294[5:MRR:293.1,288.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.48 295[5:Rew:294.0,287.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.19/0.48 296[4:Rew:164.0,19.1,154.0,19.1,147.0,19.0] || -> equal(sk_c6,sk_c7)** equal(sk_c7,sk_c8). % 0.19/0.48 297[5:MRR:296.1,288.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 299[5:Rew:297.0,295.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.19/0.48 300[4:Rew:164.0,17.1,154.0,17.1] || -> equal(multiply(sk_c4,sk_c7),sk_c8)** equal(sk_c7,sk_c8). % 0.19/0.48 301[5:MRR:300.1,288.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.48 317[5:SpR:290.0,218.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.19/0.48 321[5:Rew:299.0,317.0] || -> equal(sk_c4,sk_c8)**. % 0.19/0.48 323[5:Rew:321.0,301.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.19/0.48 332[5:Rew:147.0,323.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.48 333[5:MRR:332.0,288.0] || -> . % 0.19/0.48 337[4:Spt:333.0,7.1,94.0] || equal(multiply(sk_c1,sk_c9),sk_c8)** -> . % 0.19/0.48 338[4:Spt:333.0,7.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.48 339[4:Rew:143.0,337.0] || equal(identity,sk_c8)** -> . % 0.19/0.48 340[2:Rew:143.0,2.1] || -> equal(inverse(sk_c3),sk_c9)** equal(identity,sk_c8). % 0.19/0.48 341[4:MRR:340.1,339.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.19/0.48 350[2:Rew:143.0,1.1] || -> equal(multiply(sk_c3,sk_c9),sk_c8)** equal(identity,sk_c8). % 0.19/0.48 351[4:MRR:350.1,339.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.48 405[4:SpR:351.0,118.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.19/0.48 407[4:Rew:341.0,405.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.19/0.48 417[4:SpR:407.0,118.0] || -> equal(multiply(inverse(sk_c9),sk_c9),sk_c8)**. % 0.19/0.48 422[4:Rew:143.0,417.0,141.0,417.0] || -> equal(identity,sk_c8)**. % 0.19/0.48 423[4:MRR:422.0,339.0] || -> . % 0.19/0.48 424[3:Spt:423.0,28.1,92.0] || equal(inverse(sk_c2),sk_c8)** -> . % 0.19/0.48 425[3:Spt:423.0,28.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.48 426[3:MRR:23.1,424.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.19/0.48 427[3:MRR:25.1,424.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.48 428[3:MRR:27.0,424.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.48 429[3:MRR:26.0,424.0] || -> equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.19/0.48 430[3:MRR:24.0,424.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.48 431[3:MRR:22.0,424.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.48 439[3:SpR:428.0,118.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.19/0.48 441[3:Rew:425.0,439.0] || -> equal(multiply(sk_c8,sk_c6),sk_c8)**. % 0.19/0.48 442[3:Rew:429.0,441.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.48 443[3:Rew:442.0,427.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.48 444[3:Rew:442.0,429.0] || -> equal(multiply(sk_c8,sk_c6),sk_c8)**. % 0.19/0.48 445[3:Rew:442.0,430.0] || -> equal(multiply(sk_c4,sk_c8),sk_c8)**. % 0.19/0.48 447[3:Rew:442.0,88.1] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.19/0.48 452[3:Rew:442.0,447.5,442.0,447.4,442.0,447.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c8)** -> . % 0.19/0.48 453[3:Con:452.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c8)** -> . % 0.19/0.48 466[3:SpR:431.0,118.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.19/0.48 468[3:Rew:426.0,466.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.19/0.48 470[3:SpR:444.0,118.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c6)**. % 0.19/0.48 472[3:Rew:31.0,470.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 473[3:Rew:472.0,143.0] || -> equal(multiply(sk_c1,sk_c9),sk_c6)**. % 0.19/0.48 475[3:Rew:472.0,30.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 476[3:Rew:472.0,140.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 490[3:SpR:468.0,144.0] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.19/0.48 492[3:Rew:473.0,490.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.48 497[3:Rew:492.0,475.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.48 498[3:Rew:492.0,476.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.48 508[3:Rew:497.0,453.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(u,sk_c8),sk_c8)** -> . % 0.19/0.48 511[3:Rew:498.0,445.0] || -> equal(sk_c4,sk_c8)**. % 0.19/0.48 513[3:Rew:511.0,443.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.48 522[3:Con:508.0] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.19/0.48 523[3:Rew:498.0,522.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.48 635[3:SpL:513.0,523.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.48 637[3:Obv:635.1] || -> . % 0.19/0.48 638[2:Spt:637.0,11.1,90.0] || equal(inverse(sk_c1),sk_c9)** -> . % 0.19/0.48 639[2:Spt:637.0,11.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.48 640[2:MRR:9.1,638.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.19/0.48 641[2:MRR:14.1,638.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.48 642[2:MRR:13.0,638.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.48 643[2:MRR:12.0,638.0] || -> equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.19/0.48 644[2:MRR:10.0,638.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.48 645[2:MRR:8.0,638.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.48 653[2:SpR:642.0,118.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.19/0.48 655[2:Rew:641.0,653.0] || -> equal(multiply(sk_c8,sk_c6),sk_c8)**. % 0.19/0.48 656[2:Rew:643.0,655.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.48 657[2:Rew:656.0,639.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.48 658[2:Rew:656.0,643.0] || -> equal(multiply(sk_c8,sk_c6),sk_c8)**. % 0.19/0.48 659[2:Rew:656.0,644.0] || -> equal(multiply(sk_c4,sk_c8),sk_c8)**. % 0.19/0.48 661[2:Rew:656.0,88.1] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.19/0.48 666[2:Rew:656.0,661.5,656.0,661.4,656.0,661.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c8)** -> . % 0.19/0.48 667[2:Con:666.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c8)** -> . % 0.19/0.48 677[2:SpR:645.0,118.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.19/0.48 679[2:Rew:640.0,677.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.19/0.48 684[2:SpR:658.0,118.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c6)**. % 0.19/0.48 686[2:Rew:31.0,684.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 687[2:Rew:686.0,140.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 688[2:Rew:686.0,30.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 691[2:Rew:686.0,31.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.19/0.48 701[2:SpR:679.0,118.0] || -> equal(multiply(inverse(sk_c9),sk_c9),sk_c8)**. % 0.19/0.48 703[2:Rew:691.0,701.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.48 706[2:Rew:703.0,687.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.48 707[2:Rew:703.0,688.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.48 712[2:Rew:706.0,659.0] || -> equal(sk_c4,sk_c8)**. % 0.19/0.48 715[2:Rew:706.0,667.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(sk_c8,u),sk_c8)** -> . % 0.19/0.48 717[2:Rew:712.0,657.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.48 729[2:Rew:707.0,715.3,706.0,715.2] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(v,sk_c8) equal(u,sk_c8) -> . % 0.19/0.48 730[2:Con:729.0] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.48 834[2:SpL:717.0,730.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.48 837[2:Obv:834.1] || -> . % 0.19/0.48 % SZS output end Refutation % 0.19/0.48 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_4 prove_this_7 prove_this_8 prove_this_9 prove_this_10 prove_this_11 prove_this_12 prove_this_13 prove_this_14 prove_this_17 prove_this_18 prove_this_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_25 prove_this_26 prove_this_27 prove_this_28 prove_this_29 left_identity left_inverse associativity % 0.19/0.48 %------------------------------------------------------------------------------