%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP339-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:55 EDT 2022 % Result : Unsatisfiable 0.21s 0.50s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : GRP339-1 : TPTP v8.1.0. Released v2.5.0. % 0.03/0.14 % Command : run_spass %d %s % 0.13/0.35 % Computer : n019.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Tue Jun 14 11:07:09 EDT 2022 % 0.13/0.35 % CPUTime : % 0.21/0.50 % 0.21/0.50 SPASS V 3.9 % 0.21/0.50 SPASS beiseite: Proof found. % 0.21/0.50 % SZS status Theorem % 0.21/0.50 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.50 SPASS derived 991 clauses, backtracked 366 clauses, performed 9 splits and kept 735 clauses. % 0.21/0.50 SPASS allocated 63751 KBytes. % 0.21/0.50 SPASS spent 0:00:00.14 on the problem. % 0.21/0.50 0:00:00.04 for the input. % 0.21/0.50 0:00:00.00 for the FLOTTER CNF translation. % 0.21/0.50 0:00:00.01 for inferences. % 0.21/0.50 0:00:00.00 for the backtracking. % 0.21/0.50 0:00:00.07 for the reduction. % 0.21/0.50 % 0.21/0.50 % 0.21/0.50 Here is a proof with depth 4, length 329 : % 0.21/0.50 % SZS output start Refutation % 0.21/0.50 1[0:Inp] || -> equal(multiply(sk_c8,sk_c9),sk_c7)**. % 0.21/0.50 2[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.21/0.50 3[0:Inp] || -> equal(inverse(sk_c3),sk_c9)** equal(inverse(sk_c1),sk_c9). % 0.21/0.50 4[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(inverse(sk_c1),sk_c9)**. % 0.21/0.50 5[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.21/0.50 6[0:Inp] || -> equal(inverse(sk_c4),sk_c8)** equal(inverse(sk_c1),sk_c9). % 0.21/0.50 7[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.21/0.50 8[0:Inp] || -> equal(inverse(sk_c6),sk_c5)** equal(inverse(sk_c1),sk_c9). % 0.21/0.50 9[0:Inp] || -> equal(inverse(sk_c5),sk_c9)** equal(inverse(sk_c1),sk_c9). % 0.21/0.50 10[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c6,sk_c9),sk_c5)**. % 0.21/0.50 11[0:Inp] || -> equal(multiply(sk_c3,sk_c9),sk_c8)** equal(multiply(sk_c1,sk_c8),sk_c9). % 0.21/0.50 12[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c1,sk_c8),sk_c9)**. % 0.21/0.50 13[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c9)**. % 0.21/0.50 15[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c8),sk_c9)**. % 0.21/0.50 16[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c8)** equal(multiply(sk_c1,sk_c8),sk_c9). % 0.21/0.50 17[0:Inp] || -> equal(inverse(sk_c6),sk_c5) equal(multiply(sk_c1,sk_c8),sk_c9)**. % 0.21/0.50 18[0:Inp] || -> equal(inverse(sk_c5),sk_c9) equal(multiply(sk_c1,sk_c8),sk_c9)**. % 0.21/0.50 19[0:Inp] || -> equal(multiply(sk_c6,sk_c9),sk_c5)** equal(multiply(sk_c1,sk_c8),sk_c9). % 0.21/0.50 20[0:Inp] || -> equal(multiply(sk_c3,sk_c9),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.21/0.50 21[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.21/0.50 22[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.21/0.50 23[0:Inp] || -> equal(multiply(sk_c9,sk_c7),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.21/0.50 24[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.21/0.50 25[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.21/0.50 29[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.21/0.50 30[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(inverse(sk_c2),sk_c8)**. % 0.21/0.50 31[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(inverse(sk_c2),sk_c8)**. % 0.21/0.50 32[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.21/0.50 33[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c2),sk_c8)**. % 0.21/0.50 34[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.21/0.50 35[0:Inp] || -> equal(inverse(sk_c6),sk_c5) equal(inverse(sk_c2),sk_c8)**. % 0.21/0.50 36[0:Inp] || -> equal(inverse(sk_c5),sk_c9) equal(inverse(sk_c2),sk_c8)**. % 0.21/0.50 37[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c6,sk_c9),sk_c5)**. % 0.21/0.50 38[0:Inp] || equal(multiply(sk_c8,sk_c9),sk_c7) equal(inverse(u),sk_c9) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c8),sk_c9)** equal(inverse(v),sk_c8) equal(multiply(w,sk_c9),sk_c8)** equal(inverse(w),sk_c9) equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c9,sk_c7),sk_c8)** equal(inverse(x),sk_c8) equal(multiply(x,sk_c7),sk_c8)** equal(inverse(y),z) equal(inverse(z),sk_c9)** equal(multiply(y,sk_c9),z)* -> . % 0.21/0.50 39[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.21/0.50 40[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.21/0.50 41[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.21/0.50 42[0:Rew:1.0,38.0] || equal(sk_c7,sk_c7) equal(inverse(u),sk_c9) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c8),sk_c9)** equal(inverse(v),sk_c8) equal(multiply(w,sk_c9),sk_c8)** equal(inverse(w),sk_c9) equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c9,sk_c7),sk_c8)** equal(inverse(x),sk_c8) equal(multiply(x,sk_c7),sk_c8)** equal(inverse(y),z) equal(inverse(z),sk_c9)** equal(multiply(y,sk_c9),z)* -> . % 0.21/0.50 43[0:Obv:42.0] || equal(inverse(u),v) equal(inverse(v),sk_c9)** equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(inverse(y),sk_c8) equal(inverse(z),sk_c9) equal(inverse(sk_c8),sk_c7) equal(multiply(u,sk_c9),v)*+ equal(multiply(w,sk_c7),sk_c8)** equal(multiply(x,sk_c9),sk_c8)** equal(multiply(y,sk_c8),sk_c9)** equal(multiply(z,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c7),sk_c8)** -> . % 0.21/0.50 44[1:Spt:43.0,43.1,43.7] || equal(inverse(u),v) equal(inverse(v),sk_c9)** equal(multiply(u,sk_c9),v)* -> . % 0.21/0.50 46[2:Spt:4.1] || -> equal(inverse(sk_c1),sk_c9)**. % 0.21/0.50 48[3:Spt:31.1] || -> equal(inverse(sk_c2),sk_c8)**. % 0.21/0.50 50[4:Spt:22.1] || -> equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.21/0.50 52[5:Spt:13.1] || -> equal(multiply(sk_c1,sk_c8),sk_c9)**. % 0.21/0.50 55[1:SpL:1.0,44.2] || equal(inverse(sk_c8),u)* equal(inverse(u),sk_c9)** equal(sk_c7,u) -> . % 0.21/0.50 57[1:SpL:39.0,44.2] || equal(inverse(identity),u)* equal(inverse(u),sk_c9)** equal(sk_c9,u) -> . % 0.21/0.50 59[2:SpR:46.0,40.0] || -> equal(multiply(sk_c9,sk_c1),identity)**. % 0.21/0.50 60[3:SpR:48.0,40.0] || -> equal(multiply(sk_c8,sk_c2),identity)**. % 0.21/0.50 69[0:SpR:40.0,41.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.21/0.50 70[2:SpR:59.0,41.0] || -> equal(multiply(sk_c9,multiply(sk_c1,u)),multiply(identity,u))**. % 0.21/0.50 72[2:Rew:39.0,70.0] || -> equal(multiply(sk_c9,multiply(sk_c1,u)),u)**. % 0.21/0.50 73[0:Rew:39.0,69.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.21/0.50 75[3:SpR:60.0,41.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),multiply(identity,u))**. % 0.21/0.50 77[3:Rew:39.0,75.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),u)**. % 0.21/0.50 80[5:SpR:52.0,72.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.21/0.50 87[4:SpR:50.0,77.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.21/0.50 88[4:Rew:1.0,87.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.50 89[4:Rew:88.0,1.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.21/0.50 98[0:SpR:73.0,73.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.21/0.50 103[0:SpR:40.0,73.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.21/0.50 108[3:SpR:60.0,73.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c2)**. % 0.21/0.50 110[4:SpR:89.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.21/0.50 115[4:Rew:40.0,110.0] || -> equal(identity,sk_c9)**. % 0.21/0.50 116[4:Rew:115.0,39.0] || -> equal(multiply(sk_c9,u),u)**. % 0.21/0.50 118[4:Rew:115.0,59.0] || -> equal(multiply(sk_c9,sk_c1),sk_c9)**. % 0.21/0.50 119[4:Rew:115.0,60.0] || -> equal(multiply(sk_c8,sk_c2),sk_c9)**. % 0.21/0.50 120[4:Rew:115.0,57.0] || equal(inverse(sk_c9),u)* equal(inverse(u),sk_c9)** equal(sk_c9,u) -> . % 0.21/0.50 125[5:Rew:116.0,80.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 142[5:Rew:125.0,116.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.50 144[5:Rew:125.0,119.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.21/0.50 146[5:Rew:142.0,144.0] || -> equal(sk_c2,sk_c8)**. % 0.21/0.50 148[5:Rew:146.0,48.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.50 167[5:Rew:125.0,120.2,125.0,120.1,148.0,120.0,125.0,120.0] || equal(sk_c8,u) equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.21/0.50 168[5:Obv:167.0] || equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.21/0.50 230[5:SpL:148.0,168.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.21/0.50 232[5:Obv:230.1] || -> . % 0.21/0.50 233[5:Spt:232.0,13.1,52.0] || equal(multiply(sk_c1,sk_c8),sk_c9)** -> . % 0.21/0.50 234[5:Spt:232.0,13.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.50 235[5:Rew:88.0,234.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.50 236[4:Rew:116.0,118.0] || -> equal(sk_c1,sk_c9)**. % 0.21/0.50 245[5:Rew:116.0,233.0,236.0,233.0] || equal(sk_c9,sk_c8)** -> . % 0.21/0.50 247[4:Rew:115.0,103.0] || -> equal(multiply(inverse(inverse(u)),sk_c9),u)**. % 0.21/0.50 259[4:Rew:116.0,12.1,236.0,12.1] || -> equal(inverse(sk_c3),sk_c9)** equal(sk_c9,sk_c8). % 0.21/0.50 260[5:MRR:259.1,245.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.21/0.50 261[4:Rew:98.0,247.0] || -> equal(multiply(u,sk_c9),u)**. % 0.21/0.50 273[4:Rew:116.0,11.1,236.0,11.1,261.0,11.0] || -> equal(sk_c3,sk_c8)** equal(sk_c9,sk_c8). % 0.21/0.50 274[5:MRR:273.1,245.0] || -> equal(sk_c3,sk_c8)**. % 0.21/0.50 275[5:Rew:274.0,260.0] || -> equal(inverse(sk_c8),sk_c9)**. % 0.21/0.50 276[5:Rew:235.0,275.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 277[5:MRR:276.0,245.0] || -> . % 0.21/0.50 285[4:Spt:277.0,22.1,50.0] || equal(multiply(sk_c2,sk_c8),sk_c9)** -> . % 0.21/0.50 286[4:Spt:277.0,22.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.50 287[4:Rew:286.0,108.0] || -> equal(multiply(sk_c7,identity),sk_c2)**. % 0.21/0.50 288[0:Rew:98.0,103.0] || -> equal(multiply(u,identity),u)**. % 0.21/0.50 289[4:Rew:288.0,287.0] || -> equal(sk_c2,sk_c7)**. % 0.21/0.50 292[4:Rew:289.0,60.0] || -> equal(multiply(sk_c8,sk_c7),identity)**. % 0.21/0.50 293[4:Rew:289.0,285.0] || equal(multiply(sk_c7,sk_c8),sk_c9)** -> . % 0.21/0.50 301[4:Rew:289.0,24.1] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c7,sk_c8),sk_c9)**. % 0.21/0.50 302[4:MRR:301.1,293.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.50 303[4:Rew:289.0,21.1] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c7,sk_c8),sk_c9)**. % 0.21/0.50 304[4:MRR:303.1,293.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.21/0.50 307[4:Rew:289.0,25.1] || -> equal(multiply(sk_c4,sk_c7),sk_c8)** equal(multiply(sk_c7,sk_c8),sk_c9). % 0.21/0.50 308[4:MRR:307.1,293.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.21/0.50 309[4:Rew:289.0,23.1] || -> equal(multiply(sk_c9,sk_c7),sk_c8) equal(multiply(sk_c7,sk_c8),sk_c9)**. % 0.21/0.50 310[4:MRR:309.1,293.0] || -> equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.21/0.50 311[4:Rew:289.0,20.1] || -> equal(multiply(sk_c3,sk_c9),sk_c8)** equal(multiply(sk_c7,sk_c8),sk_c9). % 0.21/0.50 312[4:MRR:311.1,293.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.21/0.50 334[0:SpR:1.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c9)**. % 0.21/0.50 336[4:Rew:286.0,334.0] || -> equal(multiply(sk_c7,sk_c7),sk_c9)**. % 0.21/0.50 352[4:SpR:308.0,73.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c7)**. % 0.21/0.50 354[4:Rew:302.0,352.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.21/0.50 360[4:SpR:312.0,73.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.21/0.50 362[4:Rew:304.0,360.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.21/0.50 375[4:SpR:354.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c8)**. % 0.21/0.50 377[4:Rew:336.0,375.0,286.0,375.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 385[4:Rew:377.0,310.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.21/0.50 390[4:Rew:377.0,293.0] || equal(multiply(sk_c7,sk_c8),sk_c8)** -> . % 0.21/0.50 406[4:Rew:377.0,362.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.50 412[4:Rew:292.0,385.0] || -> equal(identity,sk_c8)**. % 0.21/0.50 414[4:Rew:412.0,39.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.50 418[4:Rew:354.0,406.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.50 445[4:Rew:414.0,390.0,418.0,390.0] || equal(sk_c8,sk_c8)* -> . % 0.21/0.50 446[4:Obv:445.0] || -> . % 0.21/0.50 471[3:Spt:446.0,31.1,48.0] || equal(inverse(sk_c2),sk_c8)** -> . % 0.21/0.50 472[3:Spt:446.0,31.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.50 473[3:Rew:472.0,334.0] || -> equal(multiply(sk_c7,sk_c7),sk_c9)**. % 0.21/0.50 476[3:MRR:33.1,471.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.50 477[3:MRR:30.1,471.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.21/0.50 479[3:MRR:34.0,471.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.21/0.50 481[3:MRR:29.0,471.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.21/0.50 482[3:Rew:472.0,55.0] || equal(sk_c7,u) equal(inverse(u),sk_c9)** equal(sk_c7,u) -> . % 0.21/0.50 483[3:Obv:482.0] || equal(inverse(u),sk_c9)** equal(sk_c7,u) -> . % 0.21/0.50 515[3:SpR:479.0,73.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c7)**. % 0.21/0.50 517[3:Rew:476.0,515.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.21/0.50 523[3:SpR:481.0,73.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.21/0.50 525[3:Rew:477.0,523.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.21/0.50 531[3:SpR:517.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c8)**. % 0.21/0.50 533[3:Rew:473.0,531.0,472.0,531.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 554[3:Rew:533.0,483.0] || equal(inverse(u),sk_c8)** equal(sk_c7,u) -> . % 0.21/0.50 562[3:Rew:533.0,525.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.50 574[3:Rew:517.0,562.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.50 575[3:Rew:574.0,472.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.50 613[3:Rew:574.0,554.1] || equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.21/0.50 652[3:SpL:575.0,613.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.21/0.50 653[3:Obv:652.1] || -> . % 0.21/0.50 654[2:Spt:653.0,4.1,46.0] || equal(inverse(sk_c1),sk_c9)** -> . % 0.21/0.50 655[2:Spt:653.0,4.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.50 656[2:Rew:655.0,334.0] || -> equal(multiply(sk_c7,sk_c7),sk_c9)**. % 0.21/0.50 660[2:MRR:6.1,654.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.50 661[2:MRR:3.1,654.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.21/0.50 663[2:MRR:7.0,654.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.21/0.50 665[2:MRR:2.0,654.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.21/0.50 666[2:Rew:655.0,55.0] || equal(sk_c7,u) equal(inverse(u),sk_c9)** equal(sk_c7,u) -> . % 0.21/0.50 667[2:Obv:666.0] || equal(inverse(u),sk_c9)** equal(sk_c7,u) -> . % 0.21/0.50 690[2:SpR:663.0,73.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c7)**. % 0.21/0.50 692[2:Rew:660.0,690.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.21/0.50 697[2:SpR:665.0,73.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.21/0.50 699[2:Rew:661.0,697.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.21/0.50 708[2:SpR:692.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c8)**. % 0.21/0.50 710[2:Rew:656.0,708.0,655.0,708.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 727[2:Rew:710.0,667.0] || equal(inverse(u),sk_c8)** equal(sk_c7,u) -> . % 0.21/0.50 736[2:Rew:710.0,699.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.50 738[2:Rew:692.0,736.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.50 739[2:Rew:738.0,655.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.50 765[2:Rew:738.0,727.1] || equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.21/0.50 793[0:SpR:40.0,288.0] || -> equal(inverse(identity),identity)**. % 0.21/0.50 849[2:SpL:739.0,765.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.21/0.50 850[2:Obv:849.1] || -> . % 0.21/0.50 851[1:Spt:850.0,43.2,43.3,43.4,43.5,43.6,43.8,43.9,43.10,43.11,43.12] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(inverse(sk_c8),sk_c7) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c7),sk_c8)** -> . % 0.21/0.50 855[2:Spt:31.1] || -> equal(inverse(sk_c2),sk_c8)**. % 0.21/0.50 856[2:SpR:855.0,73.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),u)**. % 0.21/0.50 858[3:Spt:4.1] || -> equal(inverse(sk_c1),sk_c9)**. % 0.21/0.50 859[3:SpR:858.0,73.0] || -> equal(multiply(sk_c9,multiply(sk_c1,u)),u)**. % 0.21/0.50 861[4:Spt:13.1] || -> equal(multiply(sk_c1,sk_c8),sk_c9)**. % 0.21/0.50 863[4:SpR:861.0,73.0] || -> equal(multiply(inverse(sk_c1),sk_c9),sk_c8)**. % 0.21/0.50 865[4:Rew:858.0,863.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.21/0.50 866[5:Spt:22.1] || -> equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.21/0.50 868[5:SpR:866.0,73.0] || -> equal(multiply(inverse(sk_c2),sk_c9),sk_c8)**. % 0.21/0.50 870[5:Rew:855.0,868.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.21/0.50 871[5:Rew:1.0,870.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.50 872[5:Rew:871.0,851.4] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(inverse(sk_c8),sk_c8) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c7),sk_c8)** -> . % 0.21/0.50 874[5:Rew:871.0,334.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.21/0.50 877[5:Rew:40.0,874.0] || -> equal(identity,sk_c9)**. % 0.21/0.50 878[5:Rew:877.0,793.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.21/0.50 879[5:Rew:877.0,288.0] || -> equal(multiply(u,sk_c9),u)**. % 0.21/0.50 882[5:Rew:879.0,865.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 889[5:Rew:882.0,878.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.50 890[5:Rew:882.0,879.0] || -> equal(multiply(u,sk_c8),u)**. % 0.21/0.50 903[5:Rew:882.0,872.9,890.0,872.9,871.0,872.9,890.0,872.8,882.0,872.8,890.0,872.7,882.0,872.7,890.0,872.6,882.0,872.6,890.0,872.5,871.0,872.5,889.0,872.4,882.0,872.3,882.0,872.1] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c8)** equal(inverse(x),sk_c8)** equal(sk_c8,sk_c8) equal(u,sk_c8) equal(v,sk_c8) equal(w,sk_c8) equal(x,sk_c8) equal(sk_c8,sk_c8) -> . % 0.21/0.50 904[5:Obv:903.9] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c8)** equal(inverse(x),sk_c8)** equal(u,sk_c8) equal(v,sk_c8) equal(w,sk_c8) equal(x,sk_c8) -> . % 0.21/0.50 905[5:Con:904.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.21/0.50 935[5:SpL:889.0,905.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.21/0.50 936[5:Obv:935.1] || -> . % 0.21/0.50 937[5:Spt:936.0,22.1,866.0] || equal(multiply(sk_c2,sk_c8),sk_c9)** -> . % 0.21/0.50 938[5:Spt:936.0,22.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.50 939[5:Rew:938.0,334.0] || -> equal(multiply(sk_c7,sk_c7),sk_c9)**. % 0.21/0.50 946[5:MRR:23.1,937.0] || -> equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.21/0.50 952[5:SpR:938.0,73.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),u)**. % 0.21/0.50 974[4:SpR:865.0,73.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.21/0.50 991[5:SpR:946.0,41.0] || -> equal(multiply(sk_c9,multiply(sk_c7,u)),multiply(sk_c8,u))**. % 0.21/0.50 992[5:SpR:946.0,73.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c7)**. % 0.21/0.50 994[5:Rew:974.0,992.0] || -> equal(sk_c7,sk_c9)**. % 0.21/0.50 997[5:Rew:994.0,939.0] || -> equal(multiply(sk_c9,sk_c9),sk_c9)**. % 0.21/0.50 1004[5:Rew:994.0,952.0] || -> equal(multiply(sk_c9,multiply(sk_c8,u)),u)**. % 0.21/0.50 1008[5:Rew:865.0,997.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 1015[5:Rew:1008.0,937.0] || equal(multiply(sk_c2,sk_c8),sk_c8)** -> . % 0.21/0.50 1025[5:Rew:1008.0,994.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.50 1033[5:Rew:1008.0,1004.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.21/0.50 1034[5:Rew:1033.0,991.0,1008.0,991.0,1025.0,991.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.50 1040[5:Rew:1034.0,856.0] || -> equal(multiply(sk_c2,u),u)**. % 0.21/0.50 1047[5:UnC:1040.0,1015.0] || -> . % 0.21/0.50 1055[4:Spt:1047.0,13.1,861.0] || equal(multiply(sk_c1,sk_c8),sk_c9)** -> . % 0.21/0.50 1056[4:Spt:1047.0,13.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.50 1057[4:Rew:1056.0,334.0] || -> equal(multiply(sk_c7,sk_c7),sk_c9)**. % 0.21/0.50 1059[4:MRR:18.1,1055.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.21/0.50 1060[4:MRR:17.1,1055.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.21/0.50 1061[4:MRR:15.1,1055.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.50 1062[4:MRR:12.1,1055.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.21/0.50 1063[4:MRR:19.1,1055.0] || -> equal(multiply(sk_c6,sk_c9),sk_c5)**. % 0.21/0.50 1064[4:MRR:16.1,1055.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.21/0.50 1065[4:MRR:11.1,1055.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.21/0.50 1075[4:SpR:1059.0,73.0] || -> equal(multiply(sk_c9,multiply(sk_c5,u)),u)**. % 0.21/0.50 1091[4:SpR:1063.0,73.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c9)**. % 0.21/0.50 1093[4:Rew:1060.0,1091.0] || -> equal(multiply(sk_c5,sk_c5),sk_c9)**. % 0.21/0.50 1095[4:SpR:1064.0,73.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c7)**. % 0.21/0.50 1097[4:Rew:1061.0,1095.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.21/0.50 1099[4:SpR:1065.0,73.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.21/0.50 1101[4:Rew:1062.0,1099.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.21/0.50 1106[4:SpR:1093.0,73.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c5)**. % 0.21/0.50 1108[4:Rew:1059.0,1106.0] || -> equal(multiply(sk_c9,sk_c9),sk_c5)**. % 0.21/0.50 1113[4:SpR:1097.0,41.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c7,u))**. % 0.21/0.50 1114[4:SpR:1097.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c8)**. % 0.21/0.50 1116[4:Rew:1057.0,1114.0,1056.0,1114.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 1126[4:Rew:1116.0,1055.0] || equal(multiply(sk_c1,sk_c8),sk_c8)** -> . % 0.21/0.50 1127[4:Rew:1116.0,859.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.21/0.50 1135[4:Rew:1116.0,1075.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),u)**. % 0.21/0.50 1138[4:Rew:1116.0,1101.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.50 1141[4:Rew:1116.0,1108.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.21/0.50 1142[4:Rew:1097.0,1138.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.50 1145[4:Rew:1142.0,1097.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.50 1150[4:Rew:1141.0,1145.0] || -> equal(sk_c5,sk_c8)**. % 0.21/0.50 1159[4:Rew:1150.0,1135.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.21/0.50 1160[4:Rew:1159.0,1113.0,1142.0,1113.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.50 1164[4:Rew:1160.0,1127.0] || -> equal(multiply(sk_c1,u),u)**. % 0.21/0.50 1167[4:UnC:1164.0,1126.0] || -> . % 0.21/0.50 1175[3:Spt:1167.0,4.1,858.0] || equal(inverse(sk_c1),sk_c9)** -> . % 0.21/0.50 1176[3:Spt:1167.0,4.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.50 1177[3:Rew:1176.0,334.0] || -> equal(multiply(sk_c7,sk_c7),sk_c9)**. % 0.21/0.50 1180[3:MRR:9.1,1175.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.21/0.50 1181[3:MRR:8.1,1175.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.21/0.50 1182[3:MRR:6.1,1175.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.50 1183[3:MRR:3.1,1175.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.21/0.50 1184[3:MRR:10.0,1175.0] || -> equal(multiply(sk_c6,sk_c9),sk_c5)**. % 0.21/0.50 1185[3:MRR:7.0,1175.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.21/0.50 1186[3:MRR:5.0,1175.0] || -> equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.21/0.50 1187[3:MRR:2.0,1175.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.21/0.50 1188[3:Rew:1186.0,851.9,1176.0,851.4] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(sk_c7,sk_c7) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c8),sk_c9)** equal(sk_c8,sk_c8) -> . % 0.21/0.50 1189[3:Obv:1188.9] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c8),sk_c9)** -> . % 0.21/0.50 1194[3:SpR:1180.0,73.0] || -> equal(multiply(sk_c9,multiply(sk_c5,u)),u)**. % 0.21/0.50 1210[3:SpR:1184.0,73.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c9)**. % 0.21/0.50 1212[3:Rew:1181.0,1210.0] || -> equal(multiply(sk_c5,sk_c5),sk_c9)**. % 0.21/0.50 1214[3:SpR:1185.0,73.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c7)**. % 0.21/0.50 1216[3:Rew:1182.0,1214.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.21/0.50 1221[3:SpR:1187.0,73.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.21/0.50 1223[3:Rew:1183.0,1221.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.21/0.50 1225[3:SpR:1212.0,73.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c5)**. % 0.21/0.50 1227[3:Rew:1180.0,1225.0] || -> equal(multiply(sk_c9,sk_c9),sk_c5)**. % 0.21/0.50 1228[3:SpR:1216.0,41.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c7,u))**. % 0.21/0.50 1229[3:SpR:1216.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c8)**. % 0.21/0.50 1231[3:Rew:1177.0,1229.0,1176.0,1229.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.50 1246[3:Rew:1231.0,1189.1] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c8),sk_c9)** -> . % 0.21/0.50 1248[3:Rew:1231.0,1194.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),u)**. % 0.21/0.50 1253[3:Rew:1231.0,1223.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.50 1254[3:Rew:1231.0,1227.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.21/0.50 1255[3:Rew:1216.0,1253.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.50 1256[3:Rew:1255.0,1176.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.50 1258[3:Rew:1255.0,1216.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.50 1263[3:Rew:1254.0,1258.0] || -> equal(sk_c5,sk_c8)**. % 0.21/0.50 1272[3:Rew:1263.0,1248.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.21/0.50 1273[3:Rew:1272.0,1228.0,1255.0,1228.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.50 1284[3:Rew:1231.0,1246.7,1231.0,1246.6,1231.0,1246.5,1255.0,1246.4,1231.0,1246.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(x),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** equal(multiply(x,sk_c8),sk_c8)** -> . % 0.21/0.50 1285[3:Con:1284.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.21/0.50 1307[3:SpR:1273.0,288.0] || -> equal(identity,sk_c8)**. % 0.21/0.50 1311[3:Rew:1307.0,288.0] || -> equal(multiply(u,sk_c8),u)**. % 0.21/0.50 1313[3:Rew:1311.0,1285.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.21/0.50 1342[3:SpL:1256.0,1313.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.21/0.50 1343[3:Obv:1342.1] || -> . % 0.21/0.50 1344[2:Spt:1343.0,31.1,855.0] || equal(inverse(sk_c2),sk_c8)** -> . % 0.21/0.50 1345[2:Spt:1343.0,31.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.50 1346[2:Rew:1345.0,334.0] || -> equal(multiply(sk_c7,sk_c7),sk_c9)**. % 0.21/0.50 1350[2:MRR:36.1,1344.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.21/0.50 1351[2:MRR:35.1,1344.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.21/0.50 1352[2:MRR:33.1,1344.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.50 1353[2:MRR:30.1,1344.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.21/0.50 1354[2:MRR:37.0,1344.0] || -> equal(multiply(sk_c6,sk_c9),sk_c5)**. % 0.21/0.50 1355[2:MRR:34.0,1344.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.21/0.50 1356[2:MRR:32.0,1344.0] || -> equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.21/0.50 1357[2:MRR:29.0,1344.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.21/0.50 1358[2:Rew:1356.0,851.9,1345.0,851.4] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(sk_c7,sk_c7) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c8),sk_c9)** equal(sk_c8,sk_c8) -> . % 0.21/0.50 1359[2:Obv:1358.9] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c8),sk_c9)** -> . % 0.21/0.51 1367[2:SpR:1350.0,73.0] || -> equal(multiply(sk_c9,multiply(sk_c5,u)),u)**. % 0.21/0.51 1383[2:SpR:1354.0,73.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c9)**. % 0.21/0.51 1385[2:Rew:1351.0,1383.0] || -> equal(multiply(sk_c5,sk_c5),sk_c9)**. % 0.21/0.51 1387[2:SpR:1355.0,73.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c7)**. % 0.21/0.51 1389[2:Rew:1352.0,1387.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.21/0.51 1394[2:SpR:1357.0,73.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.21/0.51 1396[2:Rew:1353.0,1394.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.21/0.51 1398[2:SpR:1385.0,73.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c5)**. % 0.21/0.51 1400[2:Rew:1350.0,1398.0] || -> equal(multiply(sk_c9,sk_c9),sk_c5)**. % 0.21/0.51 1401[2:SpR:1389.0,41.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c7,u))**. % 0.21/0.51 1402[2:SpR:1389.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c8)**. % 0.21/0.51 1404[2:Rew:1346.0,1402.0,1345.0,1402.0] || -> equal(sk_c9,sk_c8)**. % 0.21/0.51 1418[2:Rew:1404.0,1359.1] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c8),sk_c9)** -> . % 0.21/0.51 1420[2:Rew:1404.0,1367.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),u)**. % 0.21/0.51 1425[2:Rew:1404.0,1396.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.51 1426[2:Rew:1404.0,1400.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.21/0.51 1427[2:Rew:1389.0,1425.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.51 1428[2:Rew:1427.0,1345.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.51 1430[2:Rew:1427.0,1389.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.21/0.51 1435[2:Rew:1426.0,1430.0] || -> equal(sk_c5,sk_c8)**. % 0.21/0.51 1444[2:Rew:1435.0,1420.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.21/0.51 1445[2:Rew:1444.0,1401.0,1427.0,1401.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.51 1455[2:Rew:1404.0,1418.7,1404.0,1418.6,1404.0,1418.5,1427.0,1418.4,1404.0,1418.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(x),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** equal(multiply(x,sk_c8),sk_c8)** -> . % 0.21/0.51 1456[2:Con:1455.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.21/0.51 1482[2:SpR:1445.0,288.0] || -> equal(identity,sk_c8)**. % 0.21/0.51 1485[2:Rew:1482.0,288.0] || -> equal(multiply(u,sk_c8),u)**. % 0.21/0.51 1488[2:Rew:1485.0,1456.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.21/0.51 1520[2:SpL:1428.0,1488.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.21/0.51 1521[2:Obv:1520.1] || -> . % 0.21/0.51 % SZS output end Refutation % 0.21/0.51 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 prove_this_5 prove_this_6 prove_this_7 prove_this_8 prove_this_9 prove_this_10 prove_this_11 prove_this_12 prove_this_13 prove_this_15 prove_this_16 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_29 prove_this_30 prove_this_31 prove_this_32 prove_this_33 prove_this_34 prove_this_35 prove_this_36 prove_this_37 prove_this_38 left_identity left_inverse associativity % 0.21/0.51 %------------------------------------------------------------------------------