%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP366-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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:47:03 EDT 2022 % Result : Unsatisfiable 0.19s 0.58s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP366-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n018.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 18:13:58 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.58 % 0.19/0.58 SPASS V 3.9 % 0.19/0.58 SPASS beiseite: Proof found. % 0.19/0.58 % SZS status Theorem % 0.19/0.58 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.58 SPASS derived 1539 clauses, backtracked 656 clauses, performed 12 splits and kept 1262 clauses. % 0.19/0.58 SPASS allocated 64070 KBytes. % 0.19/0.58 SPASS spent 0:00:00.22 on the problem. % 0.19/0.58 0:00:00.04 for the input. % 0.19/0.58 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.58 0:00:00.01 for inferences. % 0.19/0.58 0:00:00.00 for the backtracking. % 0.19/0.58 0:00:00.14 for the reduction. % 0.19/0.58 % 0.19/0.58 % 0.19/0.58 Here is a proof with depth 4, length 500 : % 0.19/0.58 % SZS output start Refutation % 0.19/0.58 1[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c8)** equal(multiply(sk_c8,sk_c10),sk_c9). % 0.19/0.58 2[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(multiply(sk_c8,sk_c10),sk_c9). % 0.19/0.58 3[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.58 4[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.58 6[0:Inp] || -> equal(inverse(sk_c5),sk_c9) equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.58 7[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c9)** equal(multiply(sk_c8,sk_c10),sk_c9). % 0.19/0.58 8[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.58 9[0:Inp] || -> equal(inverse(sk_c6),sk_c10) equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.58 10[0:Inp] || -> equal(multiply(sk_c7,sk_c10),sk_c6)** equal(multiply(sk_c8,sk_c10),sk_c9). % 0.19/0.58 11[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c8)** equal(multiply(sk_c10,sk_c2),sk_c9). % 0.19/0.58 12[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c2),sk_c9). % 0.19/0.58 13[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.19/0.58 14[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.19/0.58 15[0:Inp] || -> equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.19/0.58 16[0:Inp] || -> equal(inverse(sk_c5),sk_c9) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.19/0.58 17[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c9)** equal(multiply(sk_c10,sk_c2),sk_c9). % 0.19/0.58 21[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c8) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 22[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 23[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 24[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 26[0:Inp] || -> equal(inverse(sk_c5),sk_c9) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 27[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c9) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 28[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 29[0:Inp] || -> equal(inverse(sk_c6),sk_c10) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 30[0:Inp] || -> equal(multiply(sk_c7,sk_c10),sk_c6) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 31[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 32[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 33[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(inverse(sk_c1),sk_c10)**. % 0.19/0.58 34[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(inverse(sk_c1),sk_c10)**. % 0.19/0.58 35[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.58 36[0:Inp] || -> equal(inverse(sk_c5),sk_c9) equal(inverse(sk_c1),sk_c10)**. % 0.19/0.58 37[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 41[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c8) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 42[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 43[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 44[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 46[0:Inp] || -> equal(inverse(sk_c5),sk_c9) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 47[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c9) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 48[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 49[0:Inp] || -> equal(inverse(sk_c6),sk_c10) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 50[0:Inp] || -> equal(multiply(sk_c7,sk_c10),sk_c6) equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 51[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 52[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 53[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(inverse(sk_c3),sk_c8)**. % 0.19/0.58 54[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(inverse(sk_c3),sk_c8)**. % 0.19/0.58 55[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.58 56[0:Inp] || -> equal(inverse(sk_c5),sk_c9) equal(inverse(sk_c3),sk_c8)**. % 0.19/0.58 57[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 61[0:Inp] || equal(inverse(u),v) equal(inverse(v),sk_c10)** equal(inverse(w),sk_c9) equal(inverse(x),sk_c10) equal(inverse(y),sk_c8) equal(inverse(z),sk_c10) equal(inverse(sk_c9),sk_c8) equal(multiply(u,sk_c10),v)*+ equal(multiply(z,sk_c10),x1)* equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c10),sk_c9)** equal(multiply(y,sk_c8),sk_c10)** equal(multiply(sk_c10,x1),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c10),sk_c8)** equal(multiply(sk_c8,sk_c10),sk_c9) -> . % 0.19/0.58 62[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.58 63[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.58 64[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.58 65[1:Spt:61.0,61.1,61.7] || equal(inverse(u),v) equal(inverse(v),sk_c10)** equal(multiply(u,sk_c10),v)* -> . % 0.19/0.58 67[2:Spt:4.1] || -> equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.58 69[2:SpL:67.0,65.2] || equal(inverse(sk_c8),u)* equal(inverse(u),sk_c10)** equal(sk_c9,u) -> . % 0.19/0.58 70[3:Spt:34.1] || -> equal(inverse(sk_c1),sk_c10)**. % 0.19/0.58 72[4:Spt:54.1] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.58 74[5:Spt:24.1] || -> equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 76[5:SpL:74.0,65.2] || equal(inverse(sk_c1),u)* equal(inverse(u),sk_c10)** equal(sk_c2,u) -> . % 0.19/0.58 77[5:Rew:70.0,76.0] || equal(sk_c10,u) equal(inverse(u),sk_c10)** equal(sk_c2,u) -> . % 0.19/0.58 78[6:Spt:44.1] || -> equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 80[7:Spt:14.1] || -> equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.19/0.58 85[3:SpR:70.0,63.0] || -> equal(multiply(sk_c10,sk_c1),identity)**. % 0.19/0.58 86[4:SpR:72.0,63.0] || -> equal(multiply(sk_c8,sk_c3),identity)**. % 0.19/0.58 96[3:SpR:85.0,64.0] || -> equal(multiply(sk_c10,multiply(sk_c1,u)),multiply(identity,u))**. % 0.19/0.58 98[0:SpR:63.0,64.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.58 101[3:Rew:62.0,96.0] || -> equal(multiply(sk_c10,multiply(sk_c1,u)),u)**. % 0.19/0.58 103[0:Rew:62.0,98.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.58 107[5:SpR:74.0,101.0] || -> equal(multiply(sk_c10,sk_c2),sk_c10)**. % 0.19/0.58 108[7:Rew:80.0,107.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 109[7:Rew:108.0,67.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)**. % 0.19/0.58 110[7:Rew:108.0,80.0] || -> equal(multiply(sk_c10,sk_c2),sk_c10)**. % 0.19/0.58 122[0:SpR:103.0,103.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.58 125[7:SpR:109.0,103.0] || -> equal(multiply(inverse(sk_c8),sk_c10),sk_c10)**. % 0.19/0.58 126[6:SpR:78.0,103.0] || -> equal(multiply(inverse(sk_c3),sk_c10),sk_c8)**. % 0.19/0.58 129[7:SpR:110.0,103.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c2)**. % 0.19/0.58 131[0:SpR:63.0,103.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.58 132[4:SpR:86.0,103.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c3)**. % 0.19/0.58 137[7:Rew:109.0,126.0,72.0,126.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 151[7:Rew:137.0,77.1] || equal(sk_c10,u) equal(inverse(u),sk_c8)** equal(sk_c2,u) -> . % 0.19/0.58 157[7:Rew:137.0,125.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c8)**. % 0.19/0.58 159[7:Rew:63.0,129.0] || -> equal(identity,sk_c2)**. % 0.19/0.58 160[7:Rew:159.0,62.0] || -> equal(multiply(sk_c2,u),u)**. % 0.19/0.58 161[7:Rew:159.0,63.0] || -> equal(multiply(inverse(u),u),sk_c2)**. % 0.19/0.58 162[7:Rew:159.0,86.0] || -> equal(multiply(sk_c8,sk_c3),sk_c2)**. % 0.19/0.58 167[7:Rew:161.0,157.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.58 171[7:Rew:167.0,160.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.58 172[7:Rew:167.0,162.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.58 178[7:Rew:171.0,172.0] || -> equal(sk_c3,sk_c8)**. % 0.19/0.58 179[7:Rew:178.0,72.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 198[7:Rew:167.0,151.2,137.0,151.0] || equal(sk_c8,u) equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.19/0.58 199[7:Obv:198.0] || equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.19/0.58 267[7:SpL:179.0,199.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.58 269[7:Obv:267.1] || -> . % 0.19/0.58 270[7:Spt:269.0,14.1,80.0] || equal(multiply(sk_c10,sk_c2),sk_c9)** -> . % 0.19/0.58 271[7:Spt:269.0,14.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 273[6:Rew:67.0,126.0,72.0,126.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.58 274[7:Rew:273.0,271.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 276[7:Rew:274.0,132.0] || -> equal(multiply(sk_c8,identity),sk_c3)**. % 0.19/0.58 277[7:Rew:107.0,270.0,273.0,270.0] || equal(sk_c10,sk_c8)** -> . % 0.19/0.58 285[6:Rew:107.0,13.1,273.0,13.1] || -> equal(inverse(sk_c4),sk_c10)** equal(sk_c10,sk_c8). % 0.19/0.58 286[7:MRR:285.1,277.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 288[0:Rew:122.0,131.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.58 289[7:Rew:288.0,276.0] || -> equal(sk_c3,sk_c8)**. % 0.19/0.58 291[7:Rew:289.0,78.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 292[7:Rew:289.0,86.0] || -> equal(multiply(sk_c8,sk_c8),identity)**. % 0.19/0.58 295[7:Rew:291.0,292.0] || -> equal(identity,sk_c10)**. % 0.19/0.58 297[7:Rew:295.0,62.0] || -> equal(multiply(sk_c10,u),u)**. % 0.19/0.58 300[7:Rew:295.0,288.0] || -> equal(multiply(u,sk_c10),u)**. % 0.19/0.58 305[7:Rew:297.0,107.0] || -> equal(sk_c2,sk_c10)**. % 0.19/0.58 325[7:Rew:305.0,12.1,297.0,12.1,273.0,12.1,300.0,12.0,273.0,12.0] || -> equal(sk_c4,sk_c8)** equal(sk_c10,sk_c8). % 0.19/0.58 326[7:MRR:325.1,277.0] || -> equal(sk_c4,sk_c8)**. % 0.19/0.58 327[7:Rew:326.0,286.0] || -> equal(inverse(sk_c8),sk_c10)**. % 0.19/0.58 328[7:Rew:274.0,327.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 329[7:MRR:328.0,277.0] || -> . % 0.19/0.58 340[6:Spt:329.0,44.1,78.0] || equal(multiply(sk_c3,sk_c8),sk_c10)** -> . % 0.19/0.58 341[6:Spt:329.0,44.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 342[4:Rew:288.0,132.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.19/0.58 347[6:MRR:49.1,340.0] || -> equal(inverse(sk_c6),sk_c10)**. % 0.19/0.58 348[6:MRR:48.1,340.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.19/0.58 349[6:MRR:46.1,340.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 350[6:MRR:43.1,340.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 356[6:MRR:50.1,340.0] || -> equal(multiply(sk_c7,sk_c10),sk_c6)**. % 0.19/0.58 357[6:MRR:47.1,340.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 359[6:MRR:42.1,340.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 360[6:MRR:41.1,340.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 361[4:Rew:342.0,69.0] || equal(sk_c3,u) equal(inverse(u),sk_c10)** equal(sk_c9,u) -> . % 0.19/0.58 393[6:SpR:356.0,103.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c10)**. % 0.19/0.58 395[6:Rew:348.0,393.0] || -> equal(multiply(sk_c6,sk_c6),sk_c10)**. % 0.19/0.58 401[2:SpR:67.0,103.0] || -> equal(multiply(inverse(sk_c8),sk_c9),sk_c10)**. % 0.19/0.58 403[4:Rew:342.0,401.0] || -> equal(multiply(sk_c3,sk_c9),sk_c10)**. % 0.19/0.58 405[6:SpR:357.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 407[6:Rew:349.0,405.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 413[6:SpR:359.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 415[6:Rew:350.0,413.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 417[6:SpR:360.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 419[6:Rew:341.0,417.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 421[6:SpR:395.0,103.0] || -> equal(multiply(inverse(sk_c6),sk_c10),sk_c6)**. % 0.19/0.58 423[6:Rew:347.0,421.0] || -> equal(multiply(sk_c10,sk_c10),sk_c6)**. % 0.19/0.58 429[6:SpR:407.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 431[6:Rew:341.0,429.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 432[6:Rew:419.0,431.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 439[6:Rew:432.0,360.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 440[6:Rew:432.0,403.0] || -> equal(multiply(sk_c3,sk_c10),sk_c10)**. % 0.19/0.58 441[6:Rew:432.0,407.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 451[6:Rew:432.0,415.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 455[6:Rew:423.0,439.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.58 456[6:Rew:455.0,347.0] || -> equal(inverse(sk_c8),sk_c10)**. % 0.19/0.58 465[6:Rew:342.0,456.0] || -> equal(sk_c3,sk_c10)**. % 0.19/0.58 468[6:Rew:465.0,86.0] || -> equal(multiply(sk_c8,sk_c10),identity)**. % 0.19/0.58 469[6:Rew:465.0,340.0] || equal(multiply(sk_c10,sk_c8),sk_c10)** -> . % 0.19/0.58 472[6:Rew:465.0,440.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 473[6:Rew:472.0,441.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 500[6:Rew:473.0,451.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.19/0.58 504[6:Rew:500.0,468.0,473.0,468.0] || -> equal(identity,sk_c8)**. % 0.19/0.58 506[6:Rew:504.0,62.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.58 521[6:Rew:506.0,469.0,473.0,469.0] || equal(sk_c8,sk_c8)* -> . % 0.19/0.58 522[6:Obv:521.0] || -> . % 0.19/0.58 554[5:Spt:522.0,24.1,74.0] || equal(multiply(sk_c1,sk_c10),sk_c2)** -> . % 0.19/0.58 555[5:Spt:522.0,24.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 556[5:MRR:29.1,554.0] || -> equal(inverse(sk_c6),sk_c10)**. % 0.19/0.58 557[5:MRR:28.1,554.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.19/0.58 558[5:MRR:26.1,554.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 559[5:MRR:23.1,554.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 560[5:MRR:30.1,554.0] || -> equal(multiply(sk_c7,sk_c10),sk_c6)**. % 0.19/0.58 561[5:MRR:27.1,554.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 563[5:MRR:22.1,554.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 564[5:MRR:21.1,554.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 595[5:SpR:560.0,103.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c10)**. % 0.19/0.58 597[5:Rew:557.0,595.0] || -> equal(multiply(sk_c6,sk_c6),sk_c10)**. % 0.19/0.58 604[5:SpR:561.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 606[5:Rew:558.0,604.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 612[5:SpR:563.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 614[5:Rew:559.0,612.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 616[5:SpR:564.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 618[5:Rew:555.0,616.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 620[5:SpR:597.0,103.0] || -> equal(multiply(inverse(sk_c6),sk_c10),sk_c6)**. % 0.19/0.58 622[5:Rew:556.0,620.0] || -> equal(multiply(sk_c10,sk_c10),sk_c6)**. % 0.19/0.58 624[5:SpR:606.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 626[5:Rew:555.0,624.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 627[5:Rew:618.0,626.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 628[5:Rew:627.0,555.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.58 635[5:Rew:627.0,564.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 636[5:Rew:627.0,606.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 643[5:Rew:627.0,361.2] || equal(sk_c3,u) equal(inverse(u),sk_c10)** equal(sk_c10,u) -> . % 0.19/0.58 646[5:Rew:627.0,614.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 650[5:Rew:622.0,635.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.58 651[5:Rew:650.0,556.0] || -> equal(inverse(sk_c8),sk_c10)**. % 0.19/0.58 660[5:Rew:342.0,651.0] || -> equal(sk_c3,sk_c10)**. % 0.19/0.58 668[5:Rew:636.0,646.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 680[5:Rew:668.0,628.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 686[5:Rew:668.0,660.0] || -> equal(sk_c3,sk_c8)**. % 0.19/0.58 727[5:Rew:668.0,643.2,668.0,643.1,686.0,643.0] || equal(sk_c8,u) equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.19/0.58 728[5:Obv:727.0] || equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.19/0.58 766[5:SpL:680.0,728.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.58 767[5:Obv:766.1] || -> . % 0.19/0.58 768[4:Spt:767.0,54.1,72.0] || equal(inverse(sk_c3),sk_c8)** -> . % 0.19/0.58 769[4:Spt:767.0,54.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 772[4:MRR:56.1,768.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 773[4:MRR:53.1,768.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 775[4:MRR:57.0,768.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 777[4:MRR:52.0,768.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 778[4:MRR:51.0,768.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 804[4:SpR:775.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 806[4:Rew:772.0,804.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 812[4:SpR:777.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 814[4:Rew:773.0,812.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 816[4:SpR:778.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 818[4:Rew:769.0,816.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 824[4:SpR:806.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 826[4:Rew:769.0,824.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 827[4:Rew:818.0,826.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 828[4:Rew:827.0,769.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.58 835[4:Rew:827.0,806.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 842[4:Rew:827.0,69.2] || equal(inverse(sk_c8),u)* equal(inverse(u),sk_c10)** equal(sk_c10,u) -> . % 0.19/0.58 845[4:Rew:827.0,814.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 859[4:Rew:835.0,845.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 871[4:Rew:859.0,828.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 906[4:Rew:859.0,842.2,859.0,842.1,871.0,842.0] || equal(sk_c8,u) equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.19/0.58 907[4:Obv:906.0] || equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.19/0.58 1008[4:SpL:871.0,907.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.58 1009[4:Obv:1008.1] || -> . % 0.19/0.58 1010[3:Spt:1009.0,34.1,70.0] || equal(inverse(sk_c1),sk_c10)** -> . % 0.19/0.58 1011[3:Spt:1009.0,34.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 1014[3:MRR:36.1,1010.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 1015[3:MRR:33.1,1010.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 1017[3:MRR:37.0,1010.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 1019[3:MRR:32.0,1010.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 1020[3:MRR:31.0,1010.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 1039[3:SpR:1017.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 1041[3:Rew:1014.0,1039.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 1046[3:SpR:1019.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 1048[3:Rew:1015.0,1046.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 1050[3:SpR:1020.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 1052[3:Rew:1011.0,1050.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 1061[3:SpR:1041.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 1063[3:Rew:1011.0,1061.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 1064[3:Rew:1052.0,1063.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 1065[3:Rew:1064.0,1011.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.58 1072[3:Rew:1064.0,1041.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 1079[3:Rew:1064.0,69.2] || equal(inverse(sk_c8),u)* equal(inverse(u),sk_c10)** equal(sk_c10,u) -> . % 0.19/0.58 1082[3:Rew:1064.0,1048.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 1095[3:Rew:1072.0,1082.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 1105[3:Rew:1095.0,1065.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 1131[3:Rew:1095.0,1079.2,1095.0,1079.1,1105.0,1079.0] || equal(sk_c8,u) equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.19/0.58 1132[3:Obv:1131.0] || equal(inverse(u),sk_c8)** equal(sk_c8,u) -> . % 0.19/0.58 1211[3:SpL:1105.0,1132.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.58 1212[3:Obv:1211.1] || -> . % 0.19/0.58 1213[2:Spt:1212.0,4.1,67.0] || equal(multiply(sk_c8,sk_c10),sk_c9)** -> . % 0.19/0.58 1214[2:Spt:1212.0,4.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 1215[2:MRR:9.1,1213.0] || -> equal(inverse(sk_c6),sk_c10)**. % 0.19/0.58 1216[2:MRR:8.1,1213.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.19/0.58 1217[2:MRR:6.1,1213.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 1218[2:MRR:3.1,1213.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 1219[2:MRR:10.1,1213.0] || -> equal(multiply(sk_c7,sk_c10),sk_c6)**. % 0.19/0.58 1220[2:MRR:7.1,1213.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 1222[2:MRR:2.1,1213.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 1223[2:MRR:1.1,1213.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 1235[2:SpR:1219.0,103.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c10)**. % 0.19/0.58 1237[2:Rew:1216.0,1235.0] || -> equal(multiply(sk_c6,sk_c6),sk_c10)**. % 0.19/0.58 1239[2:SpR:1220.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 1241[2:Rew:1217.0,1239.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 1246[2:SpR:1222.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 1248[2:Rew:1218.0,1246.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 1250[2:SpR:1223.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 1252[2:Rew:1214.0,1250.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 1254[2:SpR:1237.0,103.0] || -> equal(multiply(inverse(sk_c6),sk_c10),sk_c6)**. % 0.19/0.58 1256[2:Rew:1215.0,1254.0] || -> equal(multiply(sk_c10,sk_c10),sk_c6)**. % 0.19/0.58 1258[2:SpR:1241.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 1260[2:Rew:1214.0,1258.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 1261[2:Rew:1252.0,1260.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 1267[2:Rew:1261.0,1223.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 1268[2:Rew:1261.0,1241.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 1269[2:Rew:1261.0,1213.0] || equal(multiply(sk_c8,sk_c10),sk_c10)** -> . % 0.19/0.58 1276[2:Rew:1261.0,1248.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 1279[2:Rew:1256.0,1267.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.58 1283[2:Rew:1279.0,1237.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 1289[2:Rew:1268.0,1276.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 1306[2:Rew:1289.0,1283.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.19/0.58 1308[2:Rew:1306.0,1269.0,1289.0,1269.0] || equal(sk_c8,sk_c8)* -> . % 0.19/0.58 1309[2:Obv:1308.0] || -> . % 0.19/0.58 1329[1:Spt:1309.0,61.2,61.3,61.4,61.5,61.6,61.8,61.9,61.10,61.11,61.12,61.13,61.14,61.15] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(inverse(sk_c9),sk_c8) equal(multiply(x,sk_c10),y)*+ equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,y),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c10),sk_c8)** equal(multiply(sk_c8,sk_c10),sk_c9) -> . % 0.19/0.58 1330[1:EqR:1329.5] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(inverse(sk_c9),sk_c8) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c10),sk_c8) equal(multiply(sk_c8,sk_c10),sk_c9) -> . % 0.19/0.58 1332[2:Spt:4.1] || -> equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.58 1335[2:Rew:1332.0,1330.11] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(inverse(sk_c9),sk_c8) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c10),sk_c8) equal(sk_c9,sk_c9) -> . % 0.19/0.58 1336[2:Obv:1335.11] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(inverse(sk_c9),sk_c8) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c10),sk_c8) -> . % 0.19/0.58 1340[2:SpR:1332.0,103.0] || -> equal(multiply(inverse(sk_c8),sk_c9),sk_c10)**. % 0.19/0.58 1342[3:Spt:54.1] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.58 1343[3:SpR:1342.0,103.0] || -> equal(multiply(sk_c8,multiply(sk_c3,u)),u)**. % 0.19/0.58 1345[4:Spt:34.1] || -> equal(inverse(sk_c1),sk_c10)**. % 0.19/0.58 1346[4:SpR:1345.0,103.0] || -> equal(multiply(sk_c10,multiply(sk_c1,u)),u)**. % 0.19/0.58 1348[5:Spt:14.1] || -> equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.19/0.58 1352[6:Spt:44.1] || -> equal(multiply(sk_c3,sk_c8),sk_c10)**. % 0.19/0.58 1354[6:SpR:1352.0,103.0] || -> equal(multiply(inverse(sk_c3),sk_c10),sk_c8)**. % 0.19/0.58 1356[6:Rew:1332.0,1354.0,1342.0,1354.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.58 1358[6:Rew:1356.0,1348.0] || -> equal(multiply(sk_c10,sk_c2),sk_c8)**. % 0.19/0.58 1361[6:Rew:1356.0,1336.4] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(inverse(sk_c8),sk_c8) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c10),sk_c8) -> . % 0.19/0.58 1362[6:Rew:1356.0,24.0] || -> equal(inverse(sk_c8),sk_c8) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 1366[6:Rew:1356.0,22.0] || -> equal(multiply(sk_c4,sk_c10),sk_c8) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.58 1368[6:Rew:1356.0,1340.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c10)**. % 0.19/0.58 1372[6:Rew:63.0,1368.0] || -> equal(identity,sk_c10)**. % 0.19/0.58 1373[6:Rew:1372.0,288.0] || -> equal(multiply(u,sk_c10),u)**. % 0.19/0.58 1374[6:Rew:1372.0,62.0] || -> equal(multiply(sk_c10,u),u)**. % 0.19/0.58 1378[6:Rew:1373.0,23.1] || -> equal(inverse(sk_c4),sk_c10)** equal(sk_c1,sk_c2). % 0.19/0.58 1381[6:Rew:1374.0,1358.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.58 1382[6:Rew:1374.0,1346.0] || -> equal(multiply(sk_c1,u),u)**. % 0.19/0.58 1384[6:Rew:1381.0,1378.1] || -> equal(inverse(sk_c4),sk_c10)** equal(sk_c1,sk_c8). % 0.19/0.58 1389[6:Rew:1382.0,1362.1,1381.0,1362.1] || -> equal(inverse(sk_c8),sk_c8)** equal(sk_c10,sk_c8). % 0.19/0.58 1394[6:Rew:1382.0,1366.1,1381.0,1366.1,1373.0,1366.0] || -> equal(sk_c4,sk_c8)** equal(sk_c10,sk_c8). % 0.19/0.58 1395[6:Rew:1356.0,1361.10,1373.0,1361.10,1374.0,1361.9,1356.0,1361.9,1373.0,1361.8,1374.0,1361.8,1356.0,1361.8,1373.0,1361.6,1356.0,1361.6,1356.0,1361.5,1356.0,1361.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c10)** equal(inverse(w),sk_c8) equal(inverse(x),sk_c10)** equal(inverse(sk_c8),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(v,sk_c8) equal(multiply(w,sk_c8),sk_c10)** equal(x,sk_c8) equal(sk_c8,sk_c8) equal(sk_c8,sk_c8) -> . % 0.19/0.58 1396[6:Obv:1395.10] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c10)** equal(inverse(w),sk_c8) equal(inverse(x),sk_c10)** equal(inverse(sk_c8),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(v,sk_c8) equal(multiply(w,sk_c8),sk_c10)** equal(x,sk_c8) -> . % 0.19/0.58 1397[6:Con:1396.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c10)** equal(inverse(w),sk_c8) equal(inverse(sk_c8),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(v,sk_c8) equal(multiply(w,sk_c8),sk_c10)** -> . % 0.19/0.58 1417[6:SpR:1382.0,1373.0] || -> equal(sk_c1,sk_c10)**. % 0.19/0.58 1419[6:Rew:1417.0,1345.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.58 1423[6:Rew:1417.0,1384.1] || -> equal(inverse(sk_c4),sk_c10)** equal(sk_c10,sk_c8). % 0.19/0.58 1430[6:Rew:1389.0,1423.0,1394.0,1423.0] || -> equal(sk_c10,sk_c8)** equal(sk_c10,sk_c8)**. % 0.19/0.58 1431[6:Obv:1430.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 1435[6:Rew:1431.0,1373.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.58 1437[6:Rew:1431.0,1397.1] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8)** equal(inverse(w),sk_c8) equal(inverse(sk_c8),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(v,sk_c8) equal(multiply(w,sk_c8),sk_c10)** -> . % 0.19/0.58 1439[6:Rew:1431.0,1419.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 1447[6:Rew:1435.0,1437.6,1431.0,1437.6,1435.0,1437.4,1439.0,1437.3] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c8)** equal(sk_c8,sk_c8) equal(u,sk_c8) equal(v,sk_c8) equal(w,sk_c8) -> . % 0.19/0.58 1448[6:Obv:1447.3] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c8)** equal(u,sk_c8) equal(v,sk_c8) equal(w,sk_c8) -> . % 0.19/0.58 1449[6:Con:1448.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.58 1475[6:SpL:1439.0,1449.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.58 1476[6:Obv:1475.1] || -> . % 0.19/0.58 1477[6:Spt:1476.0,44.1,1352.0] || equal(multiply(sk_c3,sk_c8),sk_c10)** -> . % 0.19/0.58 1478[6:Spt:1476.0,44.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 1481[6:MRR:46.1,1477.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 1482[6:MRR:43.1,1477.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 1484[6:MRR:47.1,1477.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 1486[6:MRR:42.1,1477.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 1487[6:MRR:41.1,1477.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 1494[6:SpR:1478.0,103.0] || -> equal(multiply(sk_c8,multiply(sk_c9,u)),u)**. % 0.19/0.58 1519[6:SpR:1484.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 1521[6:Rew:1481.0,1519.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 1531[6:SpR:1486.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 1533[6:Rew:1482.0,1531.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 1535[6:SpR:1487.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 1537[6:Rew:1478.0,1535.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 1542[6:SpR:1521.0,64.0] || -> equal(multiply(sk_c9,multiply(sk_c9,u)),multiply(sk_c8,u))**. % 0.19/0.58 1543[6:SpR:1521.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 1545[6:Rew:1478.0,1543.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 1546[6:Rew:1537.0,1545.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 1554[6:Rew:1546.0,1521.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 1557[6:Rew:1546.0,1494.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),u)**. % 0.19/0.58 1566[6:Rew:1546.0,1533.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 1578[6:Rew:1554.0,1566.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 1581[6:Rew:1578.0,1477.0] || equal(multiply(sk_c3,sk_c8),sk_c8)** -> . % 0.19/0.58 1585[6:Rew:1578.0,1546.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.58 1599[6:Rew:1578.0,1557.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.19/0.58 1602[6:Rew:1599.0,1542.0,1585.0,1542.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.58 1608[6:Rew:1602.0,1343.0] || -> equal(multiply(sk_c3,u),u)**. % 0.19/0.58 1609[6:UnC:1608.0,1581.0] || -> . % 0.19/0.58 1621[5:Spt:1609.0,14.1,1348.0] || equal(multiply(sk_c10,sk_c2),sk_c9)** -> . % 0.19/0.58 1622[5:Spt:1609.0,14.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 1625[5:MRR:16.1,1621.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 1626[5:MRR:13.1,1621.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 1628[5:MRR:17.1,1621.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 1629[5:MRR:15.1,1621.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.58 1630[5:MRR:12.1,1621.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 1631[5:MRR:11.1,1621.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 1632[5:Rew:1631.0,1336.10,1629.0,1336.9,1622.0,1336.4] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(sk_c8,sk_c8) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** equal(sk_c9,sk_c9) equal(sk_c8,sk_c8) -> . % 0.19/0.58 1633[5:Obv:1632.10] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** -> . % 0.19/0.58 1638[5:SpR:1622.0,103.0] || -> equal(multiply(sk_c8,multiply(sk_c9,u)),u)**. % 0.19/0.58 1658[5:SpR:1628.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 1660[5:Rew:1625.0,1658.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 1665[5:SpR:1630.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 1667[5:Rew:1626.0,1665.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 1669[5:SpR:1631.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 1671[5:Rew:1622.0,1669.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 1679[5:SpR:1660.0,64.0] || -> equal(multiply(sk_c9,multiply(sk_c9,u)),multiply(sk_c8,u))**. % 0.19/0.58 1680[5:SpR:1660.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 1682[5:Rew:1622.0,1680.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 1683[5:Rew:1671.0,1682.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 1684[5:Rew:1683.0,1622.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.58 1691[5:Rew:1683.0,1660.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 1695[5:Rew:1683.0,1638.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),u)**. % 0.19/0.58 1701[5:Rew:1683.0,1633.0] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** -> . % 0.19/0.58 1704[5:Rew:1683.0,1667.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 1716[5:Rew:1691.0,1704.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 1722[5:Rew:1716.0,1683.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.58 1723[5:Rew:1716.0,1684.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 1737[5:Rew:1716.0,1695.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.19/0.58 1740[5:Rew:1737.0,1679.0,1722.0,1679.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.58 1753[5:Rew:1740.0,1701.7,1716.0,1701.7,1722.0,1701.7,1716.0,1701.6,1716.0,1701.5,1722.0,1701.5,1722.0,1701.4,1716.0,1701.3,1716.0,1701.1,1716.0,1701.0] || 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.19/0.58 1754[5:Con:1753.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.19/0.58 1786[5:SpR:1740.0,288.0] || -> equal(identity,sk_c8)**. % 0.19/0.58 1789[5:Rew:1786.0,288.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.58 1792[5:Rew:1789.0,1754.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.58 1835[5:SpL:1723.0,1792.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.58 1836[5:Obv:1835.1] || -> . % 0.19/0.58 1837[4:Spt:1836.0,34.1,1345.0] || equal(inverse(sk_c1),sk_c10)** -> . % 0.19/0.58 1838[4:Spt:1836.0,34.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 1841[4:MRR:36.1,1837.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 1842[4:MRR:33.1,1837.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 1844[4:MRR:37.0,1837.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 1845[4:MRR:35.0,1837.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.58 1846[4:MRR:32.0,1837.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 1847[4:MRR:31.0,1837.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 1848[4:Rew:1847.0,1336.10,1845.0,1336.9,1838.0,1336.4] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(sk_c8,sk_c8) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** equal(sk_c9,sk_c9) equal(sk_c8,sk_c8) -> . % 0.19/0.58 1849[4:Obv:1848.10] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** -> . % 0.19/0.58 1854[4:SpR:1838.0,103.0] || -> equal(multiply(sk_c8,multiply(sk_c9,u)),u)**. % 0.19/0.58 1874[4:SpR:1844.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 1876[4:Rew:1841.0,1874.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 1881[4:SpR:1846.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 1883[4:Rew:1842.0,1881.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 1885[4:SpR:1847.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 1887[4:Rew:1838.0,1885.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 1895[4:SpR:1876.0,64.0] || -> equal(multiply(sk_c9,multiply(sk_c9,u)),multiply(sk_c8,u))**. % 0.19/0.58 1896[4:SpR:1876.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 1898[4:Rew:1838.0,1896.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 1899[4:Rew:1887.0,1898.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 1900[4:Rew:1899.0,1838.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.58 1907[4:Rew:1899.0,1876.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 1910[4:Rew:1899.0,1854.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),u)**. % 0.19/0.58 1916[4:Rew:1899.0,1849.0] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** -> . % 0.19/0.58 1919[4:Rew:1899.0,1883.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 1931[4:Rew:1907.0,1919.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 1936[4:Rew:1931.0,1899.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.58 1937[4:Rew:1931.0,1900.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 1950[4:Rew:1931.0,1910.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.19/0.58 1953[4:Rew:1950.0,1895.0,1936.0,1895.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.58 1964[4:Rew:1953.0,1916.7,1931.0,1916.7,1936.0,1916.7,1931.0,1916.6,1931.0,1916.5,1936.0,1916.5,1936.0,1916.4,1931.0,1916.3,1931.0,1916.1,1931.0,1916.0] || 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.19/0.58 1965[4:Con:1964.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.19/0.58 1994[4:SpR:1953.0,288.0] || -> equal(identity,sk_c8)**. % 0.19/0.58 1997[4:Rew:1994.0,288.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.58 2000[4:Rew:1997.0,1965.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.58 2042[4:SpL:1937.0,2000.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.58 2043[4:Obv:2042.1] || -> . % 0.19/0.58 2044[3:Spt:2043.0,54.1,1342.0] || equal(inverse(sk_c3),sk_c8)** -> . % 0.19/0.58 2045[3:Spt:2043.0,54.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 2048[3:MRR:56.1,2044.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 2049[3:MRR:53.1,2044.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 2051[3:MRR:57.0,2044.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 2052[3:MRR:55.0,2044.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.58 2053[3:MRR:52.0,2044.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 2054[3:MRR:51.0,2044.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 2055[3:Rew:2054.0,1336.10,2052.0,1336.9,2045.0,1336.4] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(sk_c8,sk_c8) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** equal(sk_c9,sk_c9) equal(sk_c8,sk_c8) -> . % 0.19/0.58 2056[3:Obv:2055.10] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** -> . % 0.19/0.58 2061[3:SpR:2045.0,103.0] || -> equal(multiply(sk_c8,multiply(sk_c9,u)),u)**. % 0.19/0.58 2079[3:SpR:2051.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 2081[3:Rew:2048.0,2079.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 2086[3:SpR:2053.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.58 2088[3:Rew:2049.0,2086.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.58 2090[3:SpR:2054.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.58 2092[3:Rew:2045.0,2090.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.58 2097[3:SpR:2081.0,64.0] || -> equal(multiply(sk_c9,multiply(sk_c9,u)),multiply(sk_c8,u))**. % 0.19/0.58 2098[3:SpR:2081.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.58 2100[3:Rew:2045.0,2098.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.58 2101[3:Rew:2092.0,2100.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.58 2102[3:Rew:2101.0,2045.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.58 2109[3:Rew:2101.0,2081.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.58 2112[3:Rew:2101.0,2061.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),u)**. % 0.19/0.58 2118[3:Rew:2101.0,2056.0] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c8),sk_c10)** equal(multiply(sk_c10,multiply(x,sk_c10)),sk_c9)** -> . % 0.19/0.58 2121[3:Rew:2101.0,2088.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.58 2133[3:Rew:2109.0,2121.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.58 2137[3:Rew:2133.0,2101.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.58 2138[3:Rew:2133.0,2102.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.58 2151[3:Rew:2133.0,2112.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.19/0.58 2154[3:Rew:2151.0,2097.0,2137.0,2097.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.58 2164[3:Rew:2154.0,2118.7,2133.0,2118.7,2137.0,2118.7,2133.0,2118.6,2133.0,2118.5,2137.0,2118.5,2137.0,2118.4,2133.0,2118.3,2133.0,2118.1,2133.0,2118.0] || 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.19/0.58 2165[3:Con:2164.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.19/0.58 2197[3:SpR:2154.0,288.0] || -> equal(identity,sk_c8)**. % 0.19/0.58 2199[3:Rew:2197.0,288.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.58 2203[3:Rew:2199.0,2165.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.58 2236[3:SpL:2138.0,2203.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.58 2237[3:Obv:2236.1] || -> . % 0.19/0.58 2238[2:Spt:2237.0,4.1,1332.0] || equal(multiply(sk_c8,sk_c10),sk_c9)** -> . % 0.19/0.58 2239[2:Spt:2237.0,4.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.19/0.58 2240[2:MRR:9.1,2238.0] || -> equal(inverse(sk_c6),sk_c10)**. % 0.19/0.58 2241[2:MRR:8.1,2238.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.19/0.58 2242[2:MRR:6.1,2238.0] || -> equal(inverse(sk_c5),sk_c9)**. % 0.19/0.58 2243[2:MRR:3.1,2238.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.58 2244[2:MRR:10.1,2238.0] || -> equal(multiply(sk_c7,sk_c10),sk_c6)**. % 0.19/0.58 2245[2:MRR:7.1,2238.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.58 2247[2:MRR:2.1,2238.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.58 2248[2:MRR:1.1,2238.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.58 2260[2:SpR:2244.0,103.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c10)**. % 0.19/0.58 2262[2:Rew:2241.0,2260.0] || -> equal(multiply(sk_c6,sk_c6),sk_c10)**. % 0.19/0.58 2264[2:SpR:2245.0,103.0] || -> equal(multiply(inverse(sk_c5),sk_c9),sk_c8)**. % 0.19/0.58 2266[2:Rew:2242.0,2264.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.19/0.58 2271[2:SpR:2247.0,103.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.59 2273[2:Rew:2243.0,2271.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.59 2275[2:SpR:2248.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.19/0.59 2277[2:Rew:2239.0,2275.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.59 2279[2:SpR:2262.0,103.0] || -> equal(multiply(inverse(sk_c6),sk_c10),sk_c6)**. % 0.19/0.59 2281[2:Rew:2240.0,2279.0] || -> equal(multiply(sk_c10,sk_c10),sk_c6)**. % 0.19/0.59 2283[2:SpR:2266.0,103.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.19/0.59 2285[2:Rew:2239.0,2283.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.59 2286[2:Rew:2277.0,2285.0] || -> equal(sk_c9,sk_c10)**. % 0.19/0.59 2292[2:Rew:2286.0,2248.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.59 2293[2:Rew:2286.0,2266.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.19/0.59 2294[2:Rew:2286.0,2238.0] || equal(multiply(sk_c8,sk_c10),sk_c10)** -> . % 0.19/0.59 2301[2:Rew:2286.0,2273.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.19/0.59 2303[2:Rew:2281.0,2292.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.59 2307[2:Rew:2303.0,2262.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.19/0.59 2313[2:Rew:2293.0,2301.0] || -> equal(sk_c10,sk_c8)**. % 0.19/0.59 2326[2:Rew:2313.0,2307.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.19/0.59 2328[2:Rew:2326.0,2294.0,2313.0,2294.0] || equal(sk_c8,sk_c8)* -> . % 0.19/0.59 2329[2:Obv:2328.0] || -> . % 0.19/0.59 % SZS output end Refutation % 0.19/0.59 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 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_14 prove_this_15 prove_this_16 prove_this_17 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_26 prove_this_27 prove_this_28 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_41 prove_this_42 prove_this_43 prove_this_44 prove_this_46 prove_this_47 prove_this_48 prove_this_49 prove_this_50 prove_this_51 prove_this_52 prove_this_53 prove_this_54 prove_this_55 prove_this_56 prove_this_57 prove_this_61 left_identity left_inverse associativity % 0.19/0.59 %------------------------------------------------------------------------------