%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP220-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:23 EDT 2022 % Result : Unsatisfiable 0.68s 0.92s % Output : Refutation 0.78s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP220-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n029.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jun 13 12:39:25 EDT 2022 % 0.12/0.33 % CPUTime : % 0.68/0.92 % 0.68/0.92 SPASS V 3.9 % 0.68/0.92 SPASS beiseite: Proof found. % 0.68/0.92 % SZS status Theorem % 0.68/0.92 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.68/0.92 SPASS derived 5728 clauses, backtracked 1394 clauses, performed 18 splits and kept 2350 clauses. % 0.68/0.92 SPASS allocated 67810 KBytes. % 0.68/0.92 SPASS spent 0:00:00.57 on the problem. % 0.68/0.92 0:00:00.04 for the input. % 0.68/0.92 0:00:00.00 for the FLOTTER CNF translation. % 0.68/0.92 0:00:00.04 for inferences. % 0.68/0.92 0:00:00.01 for the backtracking. % 0.68/0.92 0:00:00.45 for the reduction. % 0.68/0.92 % 0.68/0.92 % 0.68/0.92 Here is a proof with depth 5, length 662 : % 0.68/0.92 % SZS output start Refutation % 0.68/0.92 1[0:Inp] || -> equal(inverse(sk_c12),sk_c11)** equal(inverse(sk_c1),sk_c12). % 0.68/0.92 2[0:Inp] || -> equal(inverse(sk_c6),sk_c12)** equal(inverse(sk_c1),sk_c12). % 0.68/0.92 4[0:Inp] || -> equal(inverse(sk_c1),sk_c12) equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 5[0:Inp] || -> equal(inverse(sk_c7),sk_c10)** equal(inverse(sk_c1),sk_c12). % 0.68/0.92 6[0:Inp] || -> equal(inverse(sk_c1),sk_c12) equal(multiply(sk_c10,sk_c11),sk_c12)**. % 0.68/0.92 7[0:Inp] || -> equal(inverse(sk_c9),sk_c8)** equal(inverse(sk_c1),sk_c12). % 0.68/0.92 8[0:Inp] || -> equal(inverse(sk_c8),sk_c10)** equal(inverse(sk_c1),sk_c12). % 0.68/0.92 9[0:Inp] || -> equal(inverse(sk_c1),sk_c12) equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.68/0.92 10[0:Inp] || -> equal(inverse(sk_c12),sk_c11) equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 11[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 14[0:Inp] || -> equal(inverse(sk_c7),sk_c10) equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 15[0:Inp] || -> equal(multiply(sk_c10,sk_c11),sk_c12)** equal(multiply(sk_c1,sk_c11),sk_c12). % 0.68/0.92 16[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 17[0:Inp] || -> equal(inverse(sk_c8),sk_c10) equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 18[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c8)** equal(multiply(sk_c1,sk_c11),sk_c12). % 0.68/0.92 19[0:Inp] || -> equal(inverse(sk_c12),sk_c11) equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 20[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 22[0:Inp] || -> equal(multiply(sk_c7,sk_c10),sk_c12) equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 23[0:Inp] || -> equal(inverse(sk_c7),sk_c10) equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 24[0:Inp] || -> equal(multiply(sk_c10,sk_c11),sk_c12) equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 25[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 26[0:Inp] || -> equal(inverse(sk_c8),sk_c10) equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 27[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c8) equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 28[0:Inp] || -> equal(inverse(sk_c12),sk_c11) equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 29[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 30[0:Inp] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.68/0.92 31[0:Inp] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 32[0:Inp] || -> equal(inverse(sk_c7),sk_c10) equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 33[0:Inp] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c10,sk_c11),sk_c12)**. % 0.68/0.92 34[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 35[0:Inp] || -> equal(inverse(sk_c8),sk_c10) equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 36[0:Inp] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.68/0.92 37[0:Inp] || -> equal(inverse(sk_c12),sk_c11) equal(multiply(sk_c3,sk_c12),sk_c11)**. % 0.68/0.92 46[0:Inp] || -> equal(inverse(sk_c12),sk_c11) equal(multiply(sk_c12,sk_c5),sk_c11)**. % 0.68/0.92 51[0:Inp] || -> equal(multiply(sk_c10,sk_c11),sk_c12)** equal(multiply(sk_c12,sk_c5),sk_c11). % 0.68/0.92 52[0:Inp] || -> equal(inverse(sk_c9),sk_c8) equal(multiply(sk_c12,sk_c5),sk_c11)**. % 0.68/0.92 53[0:Inp] || -> equal(inverse(sk_c8),sk_c10) equal(multiply(sk_c12,sk_c5),sk_c11)**. % 0.68/0.92 54[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c8)** equal(multiply(sk_c12,sk_c5),sk_c11). % 0.68/0.92 55[0:Inp] || -> equal(inverse(sk_c12),sk_c11) equal(multiply(sk_c4,sk_c12),sk_c5)**. % 0.68/0.92 56[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(multiply(sk_c4,sk_c12),sk_c5)**. % 0.68/0.92 57[0:Inp] || -> equal(multiply(sk_c6,sk_c11),sk_c12) equal(multiply(sk_c4,sk_c12),sk_c5)**. % 0.68/0.92 58[0:Inp] || -> equal(multiply(sk_c7,sk_c10),sk_c12) equal(multiply(sk_c4,sk_c12),sk_c5)**. % 0.68/0.92 59[0:Inp] || -> equal(inverse(sk_c7),sk_c10) equal(multiply(sk_c4,sk_c12),sk_c5)**. % 0.68/0.92 64[0:Inp] || -> equal(inverse(sk_c12),sk_c11) equal(inverse(sk_c4),sk_c12)**. % 0.68/0.92 65[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(inverse(sk_c4),sk_c12)**. % 0.68/0.92 66[0:Inp] || -> equal(inverse(sk_c4),sk_c12) equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.68/0.92 67[0:Inp] || -> equal(inverse(sk_c4),sk_c12) equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 68[0:Inp] || -> equal(inverse(sk_c7),sk_c10) equal(inverse(sk_c4),sk_c12)**. % 0.68/0.92 72[0:Inp] || -> equal(inverse(sk_c4),sk_c12) equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.68/0.92 73[0:Inp] || equal(inverse(u),sk_c12) equal(multiply(u,sk_c11),sk_c12)** equal(multiply(v,w),sk_c11)** equal(inverse(v),w) equal(multiply(w,sk_c12),sk_c11)** equal(multiply(sk_c12,x),sk_c11)** equal(multiply(y,sk_c12),x)* equal(inverse(y),sk_c12) equal(inverse(sk_c12),sk_c11) equal(inverse(z),sk_c12) equal(multiply(z,sk_c11),sk_c12)** equal(multiply(x1,x2),sk_c12)** equal(inverse(x1),x2) equal(multiply(x2,sk_c11),sk_c12)** equal(inverse(x3),x4) equal(inverse(x4),x2)* equal(multiply(x3,x2),x4)* -> . % 0.68/0.92 74[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.68/0.92 75[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.68/0.92 76[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.68/0.92 77[0:Con:73.9] || equal(inverse(u),v)* equal(inverse(w),u) equal(inverse(x),v) equal(inverse(y),z) equal(inverse(x1),sk_c12) equal(inverse(x2),sk_c12) equal(inverse(sk_c12),sk_c11) equal(multiply(w,v),u)*+ equal(multiply(x,v),sk_c12)** equal(multiply(y,z),sk_c11)** equal(multiply(x1,sk_c12),x3)* equal(multiply(v,sk_c11),sk_c12)** equal(multiply(z,sk_c12),sk_c11)** equal(multiply(x2,sk_c11),sk_c12)** equal(multiply(sk_c12,x3),sk_c11)** -> . % 0.68/0.92 78[1:Spt:77.0,77.1,77.2,77.7,77.8,77.11] || equal(inverse(u),v)* equal(inverse(w),u) equal(inverse(x),v) equal(multiply(w,v),u)* equal(multiply(x,v),sk_c12)** equal(multiply(v,sk_c11),sk_c12)** -> . % 0.68/0.92 79[1:EqR:78.3] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(multiply(v,sk_c11),sk_c12) -> . % 0.68/0.92 80[2:Spt:28.1] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 82[3:Spt:64.1] || -> equal(inverse(sk_c4),sk_c12)**. % 0.68/0.92 84[4:Spt:1.1] || -> equal(inverse(sk_c1),sk_c12)**. % 0.68/0.92 86[5:Spt:55.1] || -> equal(multiply(sk_c4,sk_c12),sk_c5)**. % 0.68/0.92 90[6:Spt:19.1] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 92[6:SpL:90.0,78.3] || equal(inverse(u),sk_c3)** equal(inverse(sk_c2),u)* equal(inverse(v),sk_c3) equal(sk_c11,u) equal(multiply(v,sk_c3),sk_c12)** equal(multiply(sk_c3,sk_c11),sk_c12)** -> . % 0.68/0.92 93[6:Rew:80.0,92.1] || equal(inverse(u),sk_c3)** equal(sk_c3,u) equal(inverse(v),sk_c3) equal(sk_c11,u) equal(multiply(v,sk_c3),sk_c12)** equal(multiply(sk_c3,sk_c11),sk_c12)** -> . % 0.68/0.92 94[7:Spt:46.1] || -> equal(multiply(sk_c12,sk_c5),sk_c11)**. % 0.68/0.92 96[7:SpL:94.0,78.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c12),u)* equal(inverse(v),sk_c5) equal(sk_c11,u) equal(multiply(v,sk_c5),sk_c12)** equal(multiply(sk_c5,sk_c11),sk_c12)** -> . % 0.68/0.92 99[8:Spt:37.1] || -> equal(multiply(sk_c3,sk_c12),sk_c11)**. % 0.68/0.92 102[9:Spt:10.1] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 108[2:SpR:80.0,75.0] || -> equal(multiply(sk_c3,sk_c2),identity)**. % 0.68/0.92 109[3:SpR:82.0,75.0] || -> equal(multiply(sk_c12,sk_c4),identity)**. % 0.68/0.92 110[4:SpR:84.0,75.0] || -> equal(multiply(sk_c12,sk_c1),identity)**. % 0.68/0.92 121[6:SpR:90.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c11,u))**. % 0.68/0.92 123[3:SpR:109.0,76.0] || -> equal(multiply(sk_c12,multiply(sk_c4,u)),multiply(identity,u))**. % 0.68/0.92 125[0:SpR:75.0,76.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.68/0.92 126[2:SpR:108.0,76.0] || -> equal(multiply(sk_c3,multiply(sk_c2,u)),multiply(identity,u))**. % 0.68/0.92 128[3:Rew:74.0,123.0] || -> equal(multiply(sk_c12,multiply(sk_c4,u)),u)**. % 0.68/0.92 129[2:Rew:74.0,126.0] || -> equal(multiply(sk_c3,multiply(sk_c2,u)),u)**. % 0.68/0.92 130[0:Rew:74.0,125.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.68/0.92 132[4:SpR:110.0,76.0] || -> equal(multiply(sk_c12,multiply(sk_c1,u)),multiply(identity,u))**. % 0.68/0.92 135[4:Rew:74.0,132.0] || -> equal(multiply(sk_c12,multiply(sk_c1,u)),u)**. % 0.68/0.92 140[5:SpR:86.0,128.0] || -> equal(multiply(sk_c12,sk_c5),sk_c12)**. % 0.68/0.92 142[7:Rew:94.0,140.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 144[7:Rew:142.0,90.0] || -> equal(multiply(sk_c2,sk_c3),sk_c12)**. % 0.68/0.92 145[7:Rew:142.0,94.0] || -> equal(multiply(sk_c12,sk_c5),sk_c12)**. % 0.68/0.92 146[8:Rew:142.0,99.0] || -> equal(multiply(sk_c3,sk_c12),sk_c12)**. % 0.68/0.92 147[9:Rew:142.0,102.0] || -> equal(multiply(sk_c1,sk_c12),sk_c12)**. % 0.68/0.92 155[7:Rew:142.0,96.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c12),u)* equal(inverse(v),sk_c5) equal(sk_c12,u) equal(multiply(v,sk_c5),sk_c12)** equal(multiply(sk_c5,sk_c11),sk_c12)** -> . % 0.68/0.92 156[7:Rew:142.0,93.3] || equal(inverse(u),sk_c3)** equal(sk_c3,u) equal(inverse(v),sk_c3) equal(sk_c12,u) equal(multiply(v,sk_c3),sk_c12)** equal(multiply(sk_c3,sk_c11),sk_c12)** -> . % 0.68/0.92 161[7:Rew:142.0,121.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c12,u))**. % 0.68/0.92 165[8:Rew:146.0,156.5,142.0,156.5] || equal(inverse(u),sk_c3)** equal(sk_c3,u) equal(inverse(v),sk_c3) equal(sk_c12,u) equal(multiply(v,sk_c3),sk_c12)** equal(sk_c12,sk_c12) -> . % 0.68/0.92 166[8:Obv:165.5] || equal(inverse(u),sk_c3)** equal(sk_c3,u) equal(inverse(v),sk_c3) equal(sk_c12,u) equal(multiply(v,sk_c3),sk_c12)** -> . % 0.68/0.92 168[7:Rew:142.0,155.5] || equal(inverse(u),sk_c5)** equal(inverse(sk_c12),u)* equal(inverse(v),sk_c5) equal(sk_c12,u) equal(multiply(v,sk_c5),sk_c12)** equal(multiply(sk_c5,sk_c12),sk_c12)** -> . % 0.68/0.92 183[7:SpR:144.0,129.0] || -> equal(multiply(sk_c3,sk_c12),sk_c3)**. % 0.68/0.92 184[8:Rew:146.0,183.0] || -> equal(sk_c3,sk_c12)**. % 0.68/0.92 188[8:Rew:184.0,146.0] || -> equal(multiply(sk_c12,sk_c12),sk_c12)**. % 0.68/0.92 192[8:Rew:184.0,166.0] || equal(inverse(u),sk_c12)** equal(sk_c3,u) equal(inverse(v),sk_c3) equal(sk_c12,u) equal(multiply(v,sk_c3),sk_c12)** -> . % 0.68/0.92 197[8:Rew:184.0,192.4,184.0,192.2,184.0,192.1] || equal(inverse(u),sk_c12)** equal(sk_c12,u) equal(inverse(v),sk_c12) equal(sk_c12,u) equal(multiply(v,sk_c12),sk_c12)** -> . % 0.68/0.92 198[8:Obv:197.1] || equal(inverse(u),sk_c12)** equal(inverse(v),sk_c12) equal(sk_c12,u) equal(multiply(v,sk_c12),sk_c12)** -> . % 0.68/0.92 217[0:SpR:130.0,130.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.68/0.92 222[3:SpR:109.0,130.0] || -> equal(multiply(inverse(sk_c12),identity),sk_c4)**. % 0.68/0.92 223[4:SpR:110.0,130.0] || -> equal(multiply(inverse(sk_c12),identity),sk_c1)**. % 0.68/0.92 224[3:SpR:128.0,130.0] || -> equal(multiply(inverse(sk_c12),u),multiply(sk_c4,u))**. % 0.68/0.92 226[7:SpR:145.0,130.0] || -> equal(multiply(inverse(sk_c12),sk_c12),sk_c5)**. % 0.68/0.92 230[0:SpR:75.0,130.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.68/0.92 238[4:Rew:222.0,223.0] || -> equal(sk_c4,sk_c1)**. % 0.68/0.92 240[5:Rew:238.0,86.0] || -> equal(multiply(sk_c1,sk_c12),sk_c5)**. % 0.68/0.92 246[4:Rew:238.0,222.0] || -> equal(multiply(inverse(sk_c12),identity),sk_c1)**. % 0.68/0.92 247[9:Rew:147.0,240.0] || -> equal(sk_c5,sk_c12)**. % 0.68/0.92 251[7:Rew:75.0,226.0] || -> equal(identity,sk_c5)**. % 0.68/0.92 252[9:Rew:247.0,251.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 253[9:Rew:252.0,74.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 255[9:Rew:252.0,110.0] || -> equal(multiply(sk_c12,sk_c1),sk_c12)**. % 0.68/0.92 265[9:Rew:253.0,255.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 266[9:Rew:265.0,84.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 272[9:Rew:265.0,198.2] || equal(inverse(u),sk_c12)** equal(inverse(v),sk_c12) equal(sk_c1,u) equal(multiply(v,sk_c12),sk_c12)** -> . % 0.68/0.92 277[9:Rew:265.0,252.0] || -> equal(identity,sk_c1)**. % 0.68/0.92 290[9:Rew:277.0,230.0] || -> equal(multiply(inverse(inverse(u)),sk_c1),u)**. % 0.68/0.92 297[9:Rew:217.0,290.0] || -> equal(multiply(u,sk_c1),u)**. % 0.68/0.92 301[9:Rew:297.0,272.3,265.0,272.3,265.0,272.1,265.0,272.0] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(sk_c1,u) equal(v,sk_c1) -> . % 0.68/0.92 522[9:SpL:266.0,301.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(sk_c1,sk_c1) equal(u,sk_c1) -> . % 0.68/0.92 524[9:Obv:522.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 526[9:SpL:266.0,524.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.68/0.92 528[9:Obv:526.1] || -> . % 0.68/0.92 529[9:Spt:528.0,10.1,102.0] || equal(multiply(sk_c1,sk_c11),sk_c12)** -> . % 0.68/0.92 530[9:Spt:528.0,10.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 531[9:Rew:142.0,530.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 533[7:Rew:251.0,110.0] || -> equal(multiply(sk_c12,sk_c1),sk_c5)**. % 0.68/0.92 534[7:Rew:251.0,74.0] || -> equal(multiply(sk_c5,u),u)**. % 0.68/0.92 535[9:Rew:188.0,226.0,531.0,226.0] || -> equal(sk_c5,sk_c12)**. % 0.68/0.92 540[9:Rew:535.0,533.0] || -> equal(multiply(sk_c12,sk_c1),sk_c12)**. % 0.68/0.92 541[9:Rew:535.0,534.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 542[9:Rew:541.0,540.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 545[9:Rew:542.0,142.0] || -> equal(sk_c11,sk_c1)**. % 0.68/0.92 553[9:Rew:542.0,541.0] || -> equal(multiply(sk_c1,u),u)**. % 0.68/0.92 562[9:Rew:553.0,529.0,545.0,529.0,542.0,529.0] || equal(sk_c1,sk_c1)* -> . % 0.68/0.92 563[9:Obv:562.0] || -> . % 0.68/0.92 572[4:Rew:238.0,224.0] || -> equal(multiply(inverse(sk_c12),u),multiply(sk_c1,u))**. % 0.68/0.92 611[8:Spt:563.0,37.1,99.0] || equal(multiply(sk_c3,sk_c12),sk_c11)** -> . % 0.68/0.92 612[8:Spt:563.0,37.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 613[8:Rew:142.0,612.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 614[7:Rew:251.0,108.0] || -> equal(multiply(sk_c3,sk_c2),sk_c5)**. % 0.68/0.92 618[8:Rew:145.0,246.0,613.0,246.0,251.0,246.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 620[8:Rew:618.0,84.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 622[8:Rew:618.0,533.0] || -> equal(multiply(sk_c1,sk_c1),sk_c5)**. % 0.68/0.92 630[7:Rew:217.0,230.0,251.0,230.0] || -> equal(multiply(u,sk_c5),u)**. % 0.68/0.92 656[8:Rew:618.0,161.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c1,u))**. % 0.68/0.92 677[8:Rew:534.0,168.5,618.0,168.5,630.0,168.4,618.0,168.4,618.0,168.3,620.0,168.1,618.0,168.1] || equal(inverse(u),sk_c5)** equal(sk_c1,u) equal(inverse(v),sk_c5)** equal(sk_c1,u) equal(v,sk_c1) equal(sk_c1,sk_c1) -> . % 0.68/0.92 678[8:Obv:677.5] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c5)** equal(sk_c1,u) equal(v,sk_c1) -> . % 0.68/0.92 703[7:SpR:614.0,130.0] || -> equal(multiply(inverse(sk_c3),sk_c5),sk_c2)**. % 0.68/0.92 705[7:Rew:630.0,703.0] || -> equal(inverse(sk_c3),sk_c2)**. % 0.68/0.92 708[7:SpR:705.0,130.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 710[8:Rew:656.0,708.0] || -> equal(multiply(sk_c1,u),u)**. % 0.68/0.92 715[8:Rew:710.0,622.0] || -> equal(sk_c5,sk_c1)**. % 0.68/0.92 726[8:Rew:715.0,678.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c5)** equal(sk_c1,u) equal(v,sk_c1) -> . % 0.68/0.92 750[8:Rew:715.0,726.1] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(sk_c1,u) equal(v,sk_c1) -> . % 0.68/0.92 1183[8:SpL:620.0,750.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(sk_c1,sk_c1) equal(u,sk_c1) -> . % 0.68/0.92 1188[8:Obv:1183.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 1247[8:SpL:620.0,1188.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.68/0.92 1252[8:Obv:1247.1] || -> . % 0.68/0.92 1253[7:Spt:1252.0,46.1,94.0] || equal(multiply(sk_c12,sk_c5),sk_c11)** -> . % 0.68/0.92 1254[7:Spt:1252.0,46.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 1258[7:Rew:140.0,1253.0] || equal(sk_c11,sk_c12)** -> . % 0.68/0.92 1260[7:Rew:1254.0,572.0] || -> equal(multiply(sk_c11,u),multiply(sk_c1,u))**. % 0.68/0.92 1267[0:Rew:217.0,230.0] || -> equal(multiply(u,identity),u)**. % 0.68/0.92 1269[5:Rew:140.0,53.1] || -> equal(inverse(sk_c8),sk_c10)** equal(sk_c11,sk_c12). % 0.68/0.92 1270[7:MRR:1269.1,1258.0] || -> equal(inverse(sk_c8),sk_c10)**. % 0.68/0.92 1271[5:Rew:140.0,52.1] || -> equal(inverse(sk_c9),sk_c8)** equal(sk_c11,sk_c12). % 0.68/0.92 1272[7:MRR:1271.1,1258.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.68/0.92 1277[7:Rew:1260.0,121.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c1,u))**. % 0.68/0.92 1279[5:Rew:140.0,54.1] || -> equal(multiply(sk_c9,sk_c10),sk_c8)** equal(sk_c11,sk_c12). % 0.68/0.92 1280[7:MRR:1279.1,1258.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.68/0.92 1281[5:Rew:140.0,51.1] || -> equal(multiply(sk_c10,sk_c11),sk_c12)** equal(sk_c11,sk_c12). % 0.68/0.92 1282[7:MRR:1281.1,1258.0] || -> equal(multiply(sk_c10,sk_c11),sk_c12)**. % 0.68/0.92 1308[7:SpR:1270.0,130.0] || -> equal(multiply(sk_c10,multiply(sk_c8,u)),u)**. % 0.68/0.92 1317[7:SpR:1280.0,130.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.68/0.92 1319[7:Rew:1272.0,1317.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.68/0.92 1339[4:SpR:110.0,130.0] || -> equal(multiply(inverse(sk_c12),identity),sk_c1)**. % 0.68/0.92 1341[7:Rew:1254.0,1339.0] || -> equal(multiply(sk_c11,identity),sk_c1)**. % 0.68/0.92 1342[7:Rew:1267.0,1341.0] || -> equal(sk_c11,sk_c1)**. % 0.68/0.92 1343[7:Rew:1342.0,1254.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.68/0.92 1344[7:Rew:1342.0,1258.0] || equal(sk_c12,sk_c1)** -> . % 0.68/0.92 1347[7:Rew:1342.0,1282.0] || -> equal(multiply(sk_c10,sk_c1),sk_c12)**. % 0.68/0.92 1368[2:SpR:108.0,130.0] || -> equal(multiply(inverse(sk_c3),identity),sk_c2)**. % 0.68/0.92 1370[2:Rew:1267.0,1368.0] || -> equal(inverse(sk_c3),sk_c2)**. % 0.68/0.92 1374[2:SpR:1370.0,130.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 1376[7:Rew:1277.0,1374.0] || -> equal(multiply(sk_c1,u),u)**. % 0.68/0.92 1380[7:Rew:1376.0,135.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 1386[7:Rew:1380.0,110.0] || -> equal(identity,sk_c1)**. % 0.68/0.92 1393[7:Rew:1386.0,1267.0] || -> equal(multiply(u,sk_c1),u)**. % 0.68/0.92 1401[7:Rew:1393.0,1347.0] || -> equal(sk_c10,sk_c12)**. % 0.68/0.92 1402[7:Rew:1401.0,1270.0] || -> equal(inverse(sk_c8),sk_c12)**. % 0.68/0.92 1406[7:Rew:1401.0,1308.0] || -> equal(multiply(sk_c12,multiply(sk_c8,u)),u)**. % 0.68/0.92 1408[7:Rew:1401.0,1319.0] || -> equal(multiply(sk_c8,sk_c8),sk_c12)**. % 0.68/0.92 1411[7:Rew:1380.0,1406.0] || -> equal(multiply(sk_c8,u),u)**. % 0.68/0.92 1412[7:Rew:1411.0,1408.0] || -> equal(sk_c8,sk_c12)**. % 0.68/0.92 1415[7:Rew:1412.0,1402.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 1418[7:Rew:1343.0,1415.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 1419[7:MRR:1418.0,1344.0] || -> . % 0.68/0.92 1429[6:Spt:1419.0,19.1,90.0] || equal(multiply(sk_c2,sk_c3),sk_c11)** -> . % 0.68/0.92 1430[6:Spt:1419.0,19.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 1431[6:Rew:1267.0,246.0,1430.0,246.0] || -> equal(sk_c11,sk_c1)**. % 0.68/0.92 1435[6:Rew:1431.0,1429.0] || equal(multiply(sk_c2,sk_c3),sk_c1)** -> . % 0.68/0.92 1469[6:Rew:1431.0,23.1] || -> equal(inverse(sk_c7),sk_c10) equal(multiply(sk_c2,sk_c3),sk_c1)**. % 0.68/0.92 1470[6:MRR:1469.1,1435.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.68/0.92 1489[6:Rew:1431.0,22.1] || -> equal(multiply(sk_c7,sk_c10),sk_c12) equal(multiply(sk_c2,sk_c3),sk_c1)**. % 0.68/0.92 1490[6:MRR:1489.1,1435.0] || -> equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 1553[6:SpR:1490.0,130.0] || -> equal(multiply(inverse(sk_c7),sk_c12),sk_c10)**. % 0.68/0.92 1555[6:Rew:1470.0,1553.0] || -> equal(multiply(sk_c10,sk_c12),sk_c10)**. % 0.68/0.92 1568[6:SpR:1555.0,130.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c12)**. % 0.68/0.92 1570[6:Rew:75.0,1568.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 1571[6:Rew:1570.0,110.0] || -> equal(multiply(sk_c12,sk_c1),sk_c12)**. % 0.68/0.92 1573[6:Rew:1570.0,74.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 1577[6:Rew:1570.0,75.0] || -> equal(multiply(inverse(u),u),sk_c12)**. % 0.68/0.92 1584[6:Rew:1573.0,1571.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 1633[6:Rew:1584.0,1577.0] || -> equal(multiply(inverse(u),u),sk_c1)**. % 0.68/0.92 1701[6:SpR:1370.0,1633.0] || -> equal(multiply(sk_c2,sk_c3),sk_c1)**. % 0.68/0.92 1703[6:MRR:1701.0,1435.0] || -> . % 0.68/0.92 1708[5:Spt:1703.0,55.1,86.0] || equal(multiply(sk_c4,sk_c12),sk_c5)** -> . % 0.68/0.92 1709[5:Spt:1703.0,55.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 1710[5:Rew:1267.0,246.0,1709.0,246.0] || -> equal(sk_c11,sk_c1)**. % 0.68/0.92 1714[5:Rew:238.0,1708.0] || equal(multiply(sk_c1,sk_c12),sk_c5)** -> . % 0.68/0.92 1746[4:Rew:238.0,59.1] || -> equal(inverse(sk_c7),sk_c10) equal(multiply(sk_c1,sk_c12),sk_c5)**. % 0.68/0.92 1747[5:MRR:1746.1,1714.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.68/0.92 1748[4:Rew:238.0,56.1] || -> equal(inverse(sk_c6),sk_c12) equal(multiply(sk_c1,sk_c12),sk_c5)**. % 0.68/0.92 1749[5:MRR:1748.1,1714.0] || -> equal(inverse(sk_c6),sk_c12)**. % 0.68/0.92 1771[4:Rew:238.0,58.1] || -> equal(multiply(sk_c7,sk_c10),sk_c12)** equal(multiply(sk_c1,sk_c12),sk_c5). % 0.68/0.92 1772[5:MRR:1771.1,1714.0] || -> equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 1773[4:Rew:238.0,57.1] || -> equal(multiply(sk_c6,sk_c11),sk_c12)** equal(multiply(sk_c1,sk_c12),sk_c5). % 0.68/0.92 1774[5:Rew:1710.0,1773.0] || -> equal(multiply(sk_c6,sk_c1),sk_c12)** equal(multiply(sk_c1,sk_c12),sk_c5). % 0.68/0.92 1775[5:MRR:1774.1,1714.0] || -> equal(multiply(sk_c6,sk_c1),sk_c12)**. % 0.68/0.92 1785[5:Rew:1710.0,79.4] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(multiply(v,sk_c1),sk_c12) -> . % 0.68/0.92 1828[5:SpR:1772.0,130.0] || -> equal(multiply(inverse(sk_c7),sk_c12),sk_c10)**. % 0.68/0.92 1830[5:Rew:1747.0,1828.0] || -> equal(multiply(sk_c10,sk_c12),sk_c10)**. % 0.68/0.92 1832[5:SpR:1775.0,130.0] || -> equal(multiply(inverse(sk_c6),sk_c12),sk_c1)**. % 0.68/0.92 1834[5:Rew:1749.0,1832.0] || -> equal(multiply(sk_c12,sk_c12),sk_c1)**. % 0.68/0.92 1840[5:SpR:1830.0,130.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c12)**. % 0.68/0.92 1842[5:Rew:75.0,1840.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 1845[5:Rew:1842.0,74.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 1846[5:Rew:1842.0,1267.0] || -> equal(multiply(u,sk_c12),u)**. % 0.68/0.92 1847[5:Rew:1842.0,75.0] || -> equal(multiply(inverse(u),u),sk_c12)**. % 0.68/0.92 1853[5:Rew:1845.0,1834.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 1861[5:Rew:1853.0,84.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 1871[5:Rew:1853.0,1785.4] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(multiply(v,sk_c1),sk_c1) -> . % 0.68/0.92 1877[5:Rew:1853.0,1846.0] || -> equal(multiply(u,sk_c1),u)**. % 0.68/0.92 1899[5:Rew:1853.0,1847.0] || -> equal(multiply(inverse(u),u),sk_c1)**. % 0.68/0.92 1916[5:Rew:1877.0,1871.4,1853.0,1871.3] || equal(inverse(multiply(u,v)),v)**+ equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c1)** equal(v,sk_c1) -> . % 0.68/0.92 1951[5:SpR:1899.0,130.0] || -> equal(multiply(inverse(inverse(u)),sk_c1),u)**. % 0.68/0.92 1961[5:Rew:1877.0,1951.0] || -> equal(inverse(inverse(u)),u)**. % 0.68/0.92 1973[5:SpR:1961.0,1899.0] || -> equal(multiply(u,inverse(u)),sk_c1)**. % 0.68/0.92 2454[5:SpL:1899.0,1916.0] || equal(inverse(sk_c1),u) equal(multiply(inverse(u),u),inverse(inverse(u)))** equal(inverse(v),u) equal(multiply(v,u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 2471[5:Rew:1899.0,2454.1,1961.0,2454.1,1861.0,2454.0] || equal(sk_c1,u) equal(sk_c1,u) equal(inverse(v),u) equal(multiply(v,u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 2472[5:Obv:2471.1] || equal(inverse(u),v) equal(multiply(u,v),sk_c1)** equal(v,sk_c1) -> . % 0.68/0.92 2675[5:SpL:1973.0,2472.1] || equal(inverse(u),inverse(u))* equal(sk_c1,sk_c1) equal(inverse(u),sk_c1) -> . % 0.68/0.92 2707[5:Obv:2675.1] || equal(inverse(u),sk_c1)** -> . % 0.68/0.92 2708[5:UnC:2707.0,1961.0] || -> . % 0.68/0.92 2716[4:Spt:2708.0,1.1,84.0] || equal(inverse(sk_c1),sk_c12)** -> . % 0.68/0.92 2717[4:Spt:2708.0,1.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 2718[4:Rew:1267.0,222.0,2717.0,222.0] || -> equal(sk_c4,sk_c11)**. % 0.68/0.92 2720[4:Rew:2718.0,109.0] || -> equal(multiply(sk_c12,sk_c11),identity)**. % 0.68/0.92 2727[4:MRR:5.1,2716.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.68/0.92 2732[4:MRR:4.0,2716.0] || -> equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 2779[4:SpR:2732.0,130.0] || -> equal(multiply(inverse(sk_c7),sk_c12),sk_c10)**. % 0.68/0.92 2781[4:Rew:2727.0,2779.0] || -> equal(multiply(sk_c10,sk_c12),sk_c10)**. % 0.68/0.92 2794[4:SpR:2781.0,130.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c12)**. % 0.68/0.92 2796[4:Rew:75.0,2794.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 2798[4:Rew:2796.0,2720.0] || -> equal(multiply(sk_c12,sk_c11),sk_c12)**. % 0.68/0.92 2799[4:Rew:2796.0,74.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 2800[4:Rew:2796.0,1267.0] || -> equal(multiply(u,sk_c12),u)**. % 0.68/0.92 2803[4:Rew:2796.0,75.0] || -> equal(multiply(inverse(u),u),sk_c12)**. % 0.68/0.92 2808[4:Rew:2799.0,2798.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 2815[4:Rew:2808.0,2717.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 2822[4:Rew:2808.0,79.4] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(multiply(v,sk_c12),sk_c12) -> . % 0.68/0.92 2864[4:Rew:2800.0,2822.4] || equal(inverse(multiply(u,v)),v)**+ equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(v,sk_c12) -> . % 0.68/0.92 2916[4:SpR:2803.0,130.0] || -> equal(multiply(inverse(inverse(u)),sk_c12),u)**. % 0.68/0.92 2922[4:Rew:2800.0,2916.0] || -> equal(inverse(inverse(u)),u)**. % 0.68/0.92 2928[4:SpR:2922.0,2803.0] || -> equal(multiply(u,inverse(u)),sk_c12)**. % 0.68/0.92 3500[4:SpL:2803.0,2864.0] || equal(inverse(sk_c12),u) equal(multiply(inverse(u),u),inverse(inverse(u)))** equal(inverse(v),u) equal(multiply(v,u),sk_c12)** equal(u,sk_c12) -> . % 0.68/0.92 3519[4:Rew:2803.0,3500.1,2922.0,3500.1,2815.0,3500.0] || equal(sk_c12,u) equal(sk_c12,u) equal(inverse(v),u) equal(multiply(v,u),sk_c12)** equal(u,sk_c12) -> . % 0.68/0.92 3520[4:Obv:3519.1] || equal(inverse(u),v) equal(multiply(u,v),sk_c12)** equal(v,sk_c12) -> . % 0.68/0.92 3697[4:SpL:2928.0,3520.1] || equal(inverse(u),inverse(u))* equal(sk_c12,sk_c12) equal(inverse(u),sk_c12) -> . % 0.68/0.92 3729[4:Obv:3697.1] || equal(inverse(u),sk_c12)** -> . % 0.68/0.92 3730[4:UnC:3729.0,2815.0] || -> . % 0.68/0.92 3738[3:Spt:3730.0,64.1,82.0] || equal(inverse(sk_c4),sk_c12)** -> . % 0.68/0.92 3739[3:Spt:3730.0,64.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 3743[3:MRR:68.1,3738.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.68/0.92 3744[3:MRR:65.1,3738.0] || -> equal(inverse(sk_c6),sk_c12)**. % 0.68/0.92 3748[3:MRR:67.0,3738.0] || -> equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 3749[3:MRR:66.0,3738.0] || -> equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.68/0.92 3782[3:SpR:3748.0,130.0] || -> equal(multiply(inverse(sk_c7),sk_c12),sk_c10)**. % 0.68/0.92 3784[3:Rew:3743.0,3782.0] || -> equal(multiply(sk_c10,sk_c12),sk_c10)**. % 0.68/0.92 3786[3:SpR:3749.0,130.0] || -> equal(multiply(inverse(sk_c6),sk_c12),sk_c11)**. % 0.68/0.92 3788[3:Rew:3744.0,3786.0] || -> equal(multiply(sk_c12,sk_c12),sk_c11)**. % 0.68/0.92 3794[3:SpR:3784.0,130.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c12)**. % 0.68/0.92 3796[3:Rew:75.0,3794.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 3798[3:Rew:3796.0,74.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 3799[3:Rew:3796.0,1267.0] || -> equal(multiply(u,sk_c12),u)**. % 0.68/0.92 3800[3:Rew:3796.0,75.0] || -> equal(multiply(inverse(u),u),sk_c12)**. % 0.68/0.92 3805[3:Rew:3798.0,3788.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 3811[3:Rew:3805.0,3739.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 3816[3:Rew:3805.0,79.4] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(multiply(v,sk_c12),sk_c12) -> . % 0.68/0.92 3854[3:Rew:3799.0,3816.4] || equal(inverse(multiply(u,v)),v)**+ equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(v,sk_c12) -> . % 0.68/0.92 3904[3:SpR:3800.0,130.0] || -> equal(multiply(inverse(inverse(u)),sk_c12),u)**. % 0.68/0.92 3910[3:Rew:3799.0,3904.0] || -> equal(inverse(inverse(u)),u)**. % 0.68/0.92 3916[3:SpR:3910.0,3800.0] || -> equal(multiply(u,inverse(u)),sk_c12)**. % 0.68/0.92 4488[3:SpL:3800.0,3854.0] || equal(inverse(sk_c12),u) equal(multiply(inverse(u),u),inverse(inverse(u)))** equal(inverse(v),u) equal(multiply(v,u),sk_c12)** equal(u,sk_c12) -> . % 0.68/0.92 4507[3:Rew:3800.0,4488.1,3910.0,4488.1,3811.0,4488.0] || equal(sk_c12,u) equal(sk_c12,u) equal(inverse(v),u) equal(multiply(v,u),sk_c12)** equal(u,sk_c12) -> . % 0.68/0.92 4508[3:Obv:4507.1] || equal(inverse(u),v) equal(multiply(u,v),sk_c12)** equal(v,sk_c12) -> . % 0.68/0.92 4685[3:SpL:3916.0,4508.1] || equal(inverse(u),inverse(u))* equal(sk_c12,sk_c12) equal(inverse(u),sk_c12) -> . % 0.68/0.92 4717[3:Obv:4685.1] || equal(inverse(u),sk_c12)** -> . % 0.68/0.92 4718[3:UnC:4717.0,3811.0] || -> . % 0.68/0.92 4726[2:Spt:4718.0,28.1,80.0] || equal(inverse(sk_c2),sk_c3)** -> . % 0.68/0.92 4727[2:Spt:4718.0,28.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 4730[2:MRR:32.1,4726.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.68/0.92 4731[2:MRR:29.1,4726.0] || -> equal(inverse(sk_c6),sk_c12)**. % 0.68/0.92 4735[2:MRR:31.0,4726.0] || -> equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 4736[2:MRR:30.0,4726.0] || -> equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.68/0.92 4763[2:SpR:4735.0,130.0] || -> equal(multiply(inverse(sk_c7),sk_c12),sk_c10)**. % 0.68/0.92 4765[2:Rew:4730.0,4763.0] || -> equal(multiply(sk_c10,sk_c12),sk_c10)**. % 0.68/0.92 4767[2:SpR:4736.0,130.0] || -> equal(multiply(inverse(sk_c6),sk_c12),sk_c11)**. % 0.68/0.92 4769[2:Rew:4731.0,4767.0] || -> equal(multiply(sk_c12,sk_c12),sk_c11)**. % 0.68/0.92 4778[2:SpR:4765.0,130.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c12)**. % 0.68/0.92 4780[2:Rew:75.0,4778.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 4781[2:Rew:4780.0,74.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 4782[2:Rew:4780.0,1267.0] || -> equal(multiply(u,sk_c12),u)**. % 0.68/0.92 4785[2:Rew:4780.0,75.0] || -> equal(multiply(inverse(u),u),sk_c12)**. % 0.68/0.92 4787[2:Rew:4781.0,4769.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 4793[2:Rew:4787.0,4727.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 4798[2:Rew:4787.0,79.4] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(multiply(v,sk_c12),sk_c12) -> . % 0.68/0.92 4835[2:Rew:4782.0,4798.4] || equal(inverse(multiply(u,v)),v)**+ equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c12)** equal(v,sk_c12) -> . % 0.68/0.92 4870[2:SpR:4785.0,130.0] || -> equal(multiply(inverse(inverse(u)),sk_c12),u)**. % 0.68/0.92 4874[2:Rew:4782.0,4870.0] || -> equal(inverse(inverse(u)),u)**. % 0.68/0.92 4890[2:SpR:4874.0,4785.0] || -> equal(multiply(u,inverse(u)),sk_c12)**. % 0.68/0.92 5407[2:SpL:4785.0,4835.0] || equal(inverse(sk_c12),u) equal(multiply(inverse(u),u),inverse(inverse(u)))** equal(inverse(v),u) equal(multiply(v,u),sk_c12)** equal(u,sk_c12) -> . % 0.68/0.92 5417[2:Rew:4785.0,5407.1,4874.0,5407.1,4793.0,5407.0] || equal(sk_c12,u) equal(sk_c12,u) equal(inverse(v),u) equal(multiply(v,u),sk_c12)** equal(u,sk_c12) -> . % 0.68/0.92 5418[2:Obv:5417.1] || equal(inverse(u),v) equal(multiply(u,v),sk_c12)** equal(v,sk_c12) -> . % 0.68/0.92 5579[2:SpL:4890.0,5418.1] || equal(inverse(u),inverse(u))* equal(sk_c12,sk_c12) equal(inverse(u),sk_c12) -> . % 0.68/0.92 5601[2:Obv:5579.1] || equal(inverse(u),sk_c12)** -> . % 0.68/0.92 5602[2:UnC:5601.0,4793.0] || -> . % 0.68/0.92 5608[1:Spt:5602.0,77.3,77.4,77.5,77.6,77.9,77.10,77.12,77.13,77.14] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(inverse(sk_c12),sk_c11) equal(multiply(u,v),sk_c11)**+ equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(multiply(sk_c12,y),sk_c11)** -> . % 0.68/0.92 5621[2:Spt:1.0] || -> equal(inverse(sk_c12),sk_c11)**. % 0.68/0.92 5622[2:Rew:5621.0,5608.3] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(sk_c11,sk_c11) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(multiply(sk_c12,y),sk_c11)** -> . % 0.68/0.92 5625[2:Obv:5622.3] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(multiply(sk_c12,y),sk_c11)** -> . % 0.68/0.92 5628[2:SpR:5621.0,130.0] || -> equal(multiply(sk_c11,multiply(sk_c12,u)),u)**. % 0.68/0.92 5630[3:Spt:35.0] || -> equal(inverse(sk_c8),sk_c10)**. % 0.68/0.92 5633[4:Spt:34.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.68/0.92 5636[5:Spt:32.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.68/0.92 5637[5:SpR:5636.0,130.0] || -> equal(multiply(sk_c10,multiply(sk_c7,u)),u)**. % 0.68/0.92 5639[6:Spt:29.0] || -> equal(inverse(sk_c6),sk_c12)**. % 0.68/0.92 5642[7:Spt:36.1] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.68/0.92 5644[7:SpR:5642.0,130.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c10)**. % 0.68/0.92 5646[7:Rew:5633.0,5644.0] || -> equal(multiply(sk_c8,sk_c8),sk_c10)**. % 0.68/0.92 5647[8:Spt:33.1] || -> equal(multiply(sk_c10,sk_c11),sk_c12)**. % 0.68/0.92 5648[8:SpR:5647.0,76.0] || -> equal(multiply(sk_c10,multiply(sk_c11,u)),multiply(sk_c12,u))**. % 0.68/0.92 5652[7:SpR:5646.0,130.0] || -> equal(multiply(inverse(sk_c8),sk_c10),sk_c8)**. % 0.68/0.92 5654[7:Rew:5630.0,5652.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.68/0.92 5655[9:Spt:31.1] || -> equal(multiply(sk_c7,sk_c10),sk_c12)**. % 0.68/0.92 5657[9:SpR:5655.0,130.0] || -> equal(multiply(inverse(sk_c7),sk_c12),sk_c10)**. % 0.68/0.92 5659[9:Rew:5636.0,5657.0] || -> equal(multiply(sk_c10,sk_c12),sk_c10)**. % 0.68/0.92 5660[10:Spt:30.1] || -> equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.68/0.92 5662[10:SpR:5660.0,130.0] || -> equal(multiply(inverse(sk_c6),sk_c12),sk_c11)**. % 0.68/0.92 5664[10:Rew:5639.0,5662.0] || -> equal(multiply(sk_c12,sk_c12),sk_c11)**. % 0.68/0.92 5672[9:SpR:5659.0,130.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c12)**. % 0.68/0.92 5674[9:Rew:75.0,5672.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 5675[9:Rew:5674.0,74.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 5676[9:Rew:5674.0,1267.0] || -> equal(multiply(u,sk_c12),u)**. % 0.68/0.92 5677[9:Rew:5674.0,75.0] || -> equal(multiply(inverse(u),u),sk_c12)**. % 0.68/0.92 5680[10:Rew:5675.0,5664.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 5687[9:Rew:5675.0,5625.7] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(y,sk_c11) -> . % 0.68/0.92 5688[10:Rew:5680.0,5621.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 5730[10:Rew:5680.0,5687.7,5676.0,5687.6,5680.0,5687.6,5676.0,5687.5,5680.0,5687.5,5676.0,5687.4,5680.0,5687.3] || equal(inverse(u),v) equal(inverse(w),sk_c12)** equal(inverse(x),sk_c12)** equal(multiply(u,v),sk_c12)**+ equal(w,y)* equal(v,sk_c12) equal(x,sk_c12) equal(y,sk_c12)* -> . % 0.68/0.92 5746[9:SpR:5639.0,5677.0] || -> equal(multiply(sk_c12,sk_c6),sk_c12)**. % 0.68/0.92 5747[9:Rew:5675.0,5746.0] || -> equal(sk_c6,sk_c12)**. % 0.68/0.92 5748[9:Rew:5747.0,5639.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 5768[0:SpR:217.0,130.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.68/0.92 5782[10:SpL:5675.0,5730.3] || equal(inverse(sk_c12),u)* equal(inverse(v),sk_c12)** equal(inverse(w),sk_c12)** equal(u,sk_c12) equal(v,x)* equal(u,sk_c12) equal(w,sk_c12) equal(x,sk_c12)* -> . % 0.68/0.92 5784[10:Obv:5782.3] || equal(inverse(sk_c12),u)* equal(inverse(v),sk_c12)** equal(inverse(w),sk_c12)** equal(v,x)* equal(u,sk_c12) equal(w,sk_c12) equal(x,sk_c12)* -> . % 0.68/0.92 5785[10:Rew:5688.0,5784.0] || equal(sk_c12,u)* equal(inverse(v),sk_c12)** equal(inverse(w),sk_c12)** equal(v,x)* equal(u,sk_c12)* equal(w,sk_c12) equal(x,sk_c12)* -> . % 0.68/0.92 5786[10:Obv:5785.0] || equal(inverse(u),sk_c12)** equal(inverse(v),sk_c12)** equal(u,w)* equal(x,sk_c12)* equal(v,sk_c12) equal(w,sk_c12)* -> . % 0.68/0.92 5787[10:Con:5786.3] || equal(inverse(u),sk_c12)**+ equal(inverse(v),sk_c12)** equal(u,w)* equal(v,sk_c12) equal(w,sk_c12)* -> . % 0.68/0.92 6028[10:SpL:5688.0,5787.0] || equal(sk_c12,sk_c12) equal(inverse(u),sk_c12)** equal(sk_c12,v)* equal(u,sk_c12) equal(v,sk_c12)* -> . % 0.68/0.92 6031[10:Obv:6028.2] || equal(inverse(u),sk_c12)** equal(u,sk_c12) equal(v,sk_c12)* -> . % 0.68/0.92 6032[10:Con:6031.2] || equal(inverse(u),sk_c12)** equal(u,sk_c12) -> . % 0.68/0.92 6033[10:SpL:5688.0,6032.0] || equal(sk_c12,sk_c12)* equal(sk_c12,sk_c12)* -> . % 0.68/0.92 6036[10:Obv:6033.1] || -> . % 0.68/0.92 6037[10:Spt:6036.0,30.1,5660.0] || equal(multiply(sk_c6,sk_c11),sk_c12)** -> . % 0.68/0.92 6038[10:Spt:6036.0,30.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 6039[9:Rew:5621.0,5748.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 6063[10:Rew:5675.0,6037.0,5747.0,6037.0] || equal(sk_c11,sk_c12)** -> . % 0.68/0.92 6064[10:Rew:6039.0,6063.0] || equal(sk_c12,sk_c12)* -> . % 0.68/0.92 6065[10:Obv:6064.0] || -> . % 0.68/0.92 6123[9:Spt:6065.0,31.1,5655.0] || equal(multiply(sk_c7,sk_c10),sk_c12)** -> . % 0.68/0.92 6124[9:Spt:6065.0,31.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 6126[9:MRR:4.1,6123.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.68/0.92 6131[9:MRR:22.0,6123.0] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 6139[9:SpR:6124.0,5768.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 6145[2:SpR:5621.0,5768.0] || -> equal(multiply(sk_c12,multiply(sk_c11,u)),u)**. % 0.68/0.92 6187[9:SpR:6131.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c11,u))**. % 0.68/0.92 6191[9:Rew:6139.0,6187.0] || -> equal(multiply(sk_c11,u),u)**. % 0.68/0.92 6193[9:Rew:6191.0,5628.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 6194[9:Rew:6191.0,5648.0] || -> equal(multiply(sk_c10,u),multiply(sk_c12,u))**. % 0.68/0.92 6229[9:Rew:6193.0,6194.0] || -> equal(multiply(sk_c10,u),u)**. % 0.68/0.92 6230[9:Rew:6229.0,5654.0] || -> equal(sk_c8,sk_c10)**. % 0.68/0.92 6233[9:Rew:6229.0,5637.0] || -> equal(multiply(sk_c7,u),u)**. % 0.68/0.92 6239[9:Rew:6230.0,5633.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.68/0.92 6247[9:Rew:6233.0,6123.0] || equal(sk_c10,sk_c12)** -> . % 0.68/0.92 6302[9:SpR:6193.0,1267.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 6308[9:Rew:6302.0,75.0] || -> equal(multiply(inverse(u),u),sk_c12)**. % 0.68/0.92 6327[9:SpR:6126.0,6308.0] || -> equal(multiply(sk_c12,sk_c1),sk_c12)**. % 0.68/0.92 6331[9:SpR:6239.0,6308.0] || -> equal(multiply(sk_c10,sk_c9),sk_c12)**. % 0.68/0.92 6343[9:Rew:6193.0,6327.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 6344[9:Rew:6343.0,6126.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 6348[9:Rew:6343.0,6247.0] || equal(sk_c10,sk_c1)** -> . % 0.68/0.92 6368[9:Rew:6229.0,6331.0,6343.0,6331.0] || -> equal(sk_c9,sk_c1)**. % 0.68/0.92 6369[9:Rew:6368.0,6239.0] || -> equal(inverse(sk_c1),sk_c10)**. % 0.68/0.92 6371[9:Rew:6344.0,6369.0] || -> equal(sk_c10,sk_c1)**. % 0.68/0.92 6372[9:MRR:6371.0,6348.0] || -> . % 0.68/0.92 6382[8:Spt:6372.0,33.1,5647.0] || equal(multiply(sk_c10,sk_c11),sk_c12)** -> . % 0.68/0.92 6383[8:Spt:6372.0,33.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 6385[8:MRR:6.1,6382.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.68/0.92 6387[8:MRR:15.0,6382.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 6389[8:MRR:24.0,6382.0] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 6392[8:SpR:6383.0,5768.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 6412[8:SpR:6385.0,130.0] || -> equal(multiply(sk_c12,multiply(sk_c1,u)),u)**. % 0.68/0.92 6431[8:SpR:6387.0,130.0] || -> equal(multiply(inverse(sk_c1),sk_c12),sk_c11)**. % 0.68/0.92 6433[8:Rew:6385.0,6431.0] || -> equal(multiply(sk_c12,sk_c12),sk_c11)**. % 0.68/0.92 6437[8:SpR:6389.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c11,u))**. % 0.68/0.92 6441[8:Rew:6392.0,6437.0] || -> equal(multiply(sk_c11,u),u)**. % 0.68/0.92 6443[8:Rew:6441.0,5628.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 6450[8:Rew:6443.0,6433.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 6451[8:Rew:6443.0,6412.0] || -> equal(multiply(sk_c1,u),u)**. % 0.68/0.92 6455[8:Rew:6443.0,5625.7] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(y,sk_c11) -> . % 0.68/0.92 6482[8:Rew:6450.0,6455.7,6450.0,6455.6,6450.0,6455.5,6450.0,6455.3] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c12)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c12)** equal(multiply(x,sk_c12),sk_c12)** equal(y,sk_c12) -> . % 0.68/0.92 6512[8:SpR:6443.0,1267.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 6516[8:Rew:6512.0,1267.0] || -> equal(multiply(u,sk_c12),u)**. % 0.68/0.92 6518[8:Rew:6512.0,75.0] || -> equal(multiply(inverse(u),u),sk_c12)**. % 0.68/0.92 6523[8:Rew:6516.0,6482.6] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12)** equal(multiply(u,v),sk_c12)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c12)** equal(x,sk_c12) equal(y,sk_c12) -> . % 0.68/0.92 6527[8:Rew:6516.0,6523.5,6516.0,6523.4] || equal(inverse(u),v) equal(inverse(w),sk_c12)** equal(inverse(x),sk_c12)** equal(multiply(u,v),sk_c12)** equal(w,y)* equal(v,sk_c12) equal(x,sk_c12) equal(y,sk_c12)* -> . % 0.68/0.92 6564[8:SpR:6385.0,6518.0] || -> equal(multiply(sk_c12,sk_c1),sk_c12)**. % 0.68/0.92 6573[8:Rew:6443.0,6564.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 6574[8:Rew:6573.0,6385.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 6587[8:Rew:6573.0,6527.1] || equal(inverse(u),v) equal(inverse(w),sk_c1)** equal(inverse(x),sk_c12)** equal(multiply(u,v),sk_c12)** equal(w,y)* equal(v,sk_c12) equal(x,sk_c12) equal(y,sk_c12)* -> . % 0.68/0.92 6604[8:Rew:6573.0,6587.7,6573.0,6587.6,6573.0,6587.5,6573.0,6587.3,6573.0,6587.2] || equal(inverse(u),v) equal(inverse(w),sk_c1)** equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)**+ equal(w,y)* equal(v,sk_c1) equal(x,sk_c1) equal(y,sk_c1)* -> . % 0.68/0.92 6683[8:SpL:6451.0,6604.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(u,sk_c1) equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 6685[8:Obv:6683.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 6686[8:Rew:6574.0,6685.0] || equal(sk_c1,u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1)* equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 6687[8:Obv:6686.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1)** equal(u,w)* equal(x,sk_c1)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 6688[8:Con:6687.3] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(u,w)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 6994[8:SpL:6574.0,6688.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(sk_c1,v)* equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 6997[8:Obv:6994.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 6998[8:Con:6997.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 7061[8:SpL:6574.0,6998.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.68/0.92 7064[8:Obv:7061.1] || -> . % 0.68/0.92 7065[7:Spt:7064.0,36.1,5642.0] || equal(multiply(sk_c9,sk_c10),sk_c8)** -> . % 0.68/0.92 7066[7:Spt:7064.0,36.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 7067[7:MRR:72.1,7065.0] || -> equal(inverse(sk_c4),sk_c12)**. % 0.68/0.92 7068[7:MRR:9.1,7065.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.68/0.92 7070[7:MRR:18.0,7065.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 7072[7:MRR:27.0,7065.0] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 7093[7:SpR:7066.0,5768.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 7110[7:SpR:7068.0,130.0] || -> equal(multiply(sk_c12,multiply(sk_c1,u)),u)**. % 0.68/0.92 7118[7:SpR:7070.0,130.0] || -> equal(multiply(inverse(sk_c1),sk_c12),sk_c11)**. % 0.68/0.92 7120[7:Rew:7068.0,7118.0] || -> equal(multiply(sk_c12,sk_c12),sk_c11)**. % 0.68/0.92 7124[7:SpR:7072.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c11,u))**. % 0.68/0.92 7128[7:Rew:7093.0,7124.0] || -> equal(multiply(sk_c11,u),u)**. % 0.68/0.92 7130[7:Rew:7128.0,6145.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 7137[7:Rew:7130.0,7120.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 7138[7:Rew:7130.0,7110.0] || -> equal(multiply(sk_c1,u),u)**. % 0.68/0.92 7142[7:Rew:7130.0,5625.7] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(y,sk_c11) -> . % 0.68/0.92 7168[7:Rew:7137.0,7142.7,7137.0,7142.6,7137.0,7142.5,7137.0,7142.3] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c12)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c12)** equal(multiply(x,sk_c12),sk_c12)** equal(y,sk_c12) -> . % 0.68/0.92 7215[0:SpR:75.0,130.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.68/0.92 7216[0:SpR:75.0,1267.0] || -> equal(inverse(identity),identity)**. % 0.68/0.92 7220[7:SpR:7067.0,75.0] || -> equal(multiply(sk_c12,sk_c4),identity)**. % 0.68/0.92 7224[7:SpR:7068.0,75.0] || -> equal(multiply(sk_c12,sk_c1),identity)**. % 0.68/0.92 7229[7:Rew:7130.0,7220.0] || -> equal(identity,sk_c4)**. % 0.68/0.92 7231[7:Rew:7229.0,1267.0] || -> equal(multiply(u,sk_c4),u)**. % 0.68/0.92 7236[7:Rew:7229.0,7216.0] || -> equal(inverse(sk_c4),sk_c4)**. % 0.68/0.92 7237[7:Rew:7067.0,7236.0] || -> equal(sk_c4,sk_c12)**. % 0.68/0.92 7240[7:Rew:7237.0,7229.0] || -> equal(identity,sk_c12)**. % 0.68/0.92 7246[7:Rew:7130.0,7224.0,7240.0,7224.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 7247[7:Rew:7246.0,7068.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 7255[7:Rew:7246.0,7168.1] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c12)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c12)** equal(multiply(x,sk_c12),sk_c12)** equal(y,sk_c12) -> . % 0.68/0.92 7257[7:Rew:7246.0,7237.0] || -> equal(sk_c4,sk_c1)**. % 0.68/0.92 7269[7:Rew:7257.0,7231.0] || -> equal(multiply(u,sk_c1),u)**. % 0.68/0.92 7279[7:Rew:7246.0,7255.7,7269.0,7255.6,7246.0,7255.6,7269.0,7255.5,7246.0,7255.5,7269.0,7255.4,7246.0,7255.4,7246.0,7255.3,7246.0,7255.2] || equal(inverse(u),v) equal(inverse(w),sk_c1)** equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)**+ equal(w,y)* equal(v,sk_c1) equal(x,sk_c1) equal(y,sk_c1)* -> . % 0.68/0.92 7382[7:SpL:7138.0,7279.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(u,sk_c1) equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 7388[7:Obv:7382.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 7389[7:Rew:7247.0,7388.0] || equal(sk_c1,u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1)* equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 7390[7:Obv:7389.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1)** equal(u,w)* equal(x,sk_c1)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 7391[7:Con:7390.3] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(u,w)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 7517[7:SpL:7247.0,7391.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(sk_c1,v)* equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 7519[7:Obv:7517.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 7520[7:Con:7519.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 7605[7:SpL:7247.0,7520.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.68/0.92 7609[7:Obv:7605.1] || -> . % 0.68/0.92 7610[6:Spt:7609.0,29.0,5639.0] || equal(inverse(sk_c6),sk_c12)** -> . % 0.68/0.92 7611[6:Spt:7609.0,29.1] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 7612[0:Rew:1267.0,7215.0] || -> equal(inverse(inverse(u)),u)**. % 0.68/0.92 7614[6:MRR:2.0,7610.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.68/0.92 7617[6:MRR:11.0,7610.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 7619[6:MRR:20.0,7610.0] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 7624[6:SpR:7611.0,5768.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 7643[6:SpR:7614.0,130.0] || -> equal(multiply(sk_c12,multiply(sk_c1,u)),u)**. % 0.68/0.92 7683[6:SpR:7617.0,130.0] || -> equal(multiply(inverse(sk_c1),sk_c12),sk_c11)**. % 0.68/0.92 7685[6:Rew:7614.0,7683.0] || -> equal(multiply(sk_c12,sk_c12),sk_c11)**. % 0.68/0.92 7689[6:SpR:7619.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c11,u))**. % 0.68/0.92 7693[6:Rew:7624.0,7689.0] || -> equal(multiply(sk_c11,u),u)**. % 0.68/0.92 7695[6:Rew:7693.0,6145.0] || -> equal(multiply(sk_c12,u),u)**. % 0.68/0.92 7702[6:Rew:7695.0,7685.0] || -> equal(sk_c11,sk_c12)**. % 0.68/0.92 7703[6:Rew:7695.0,7643.0] || -> equal(multiply(sk_c1,u),u)**. % 0.68/0.92 7707[6:Rew:7695.0,5625.7] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(y,sk_c11) -> . % 0.68/0.92 7710[6:Rew:7702.0,5621.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 7731[6:Rew:7702.0,7707.7,7702.0,7707.6,7702.0,7707.5,7702.0,7707.3] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c12)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c12)** equal(multiply(x,sk_c12),sk_c12)** equal(y,sk_c12) -> . % 0.68/0.92 7771[6:SpR:7614.0,7612.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.68/0.92 7772[6:SpR:7710.0,7612.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.68/0.92 7777[6:Rew:7710.0,7771.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 7787[6:Rew:7777.0,7731.1] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c12)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c12)** equal(multiply(x,sk_c12),sk_c12)** equal(y,sk_c12) -> . % 0.68/0.92 7790[6:Rew:7777.0,7772.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 7796[6:Rew:7777.0,7787.7,7777.0,7787.6,7777.0,7787.5,7777.0,7787.4,7777.0,7787.3,7777.0,7787.2] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c1) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c1),y)* equal(multiply(v,sk_c1),sk_c1)** equal(multiply(x,sk_c1),sk_c1)** equal(y,sk_c1) -> . % 0.68/0.92 7819[6:SpR:7790.0,75.0] || -> equal(multiply(sk_c1,sk_c1),identity)**. % 0.68/0.92 7821[6:Rew:7703.0,7819.0] || -> equal(identity,sk_c1)**. % 0.68/0.92 7826[6:Rew:7821.0,1267.0] || -> equal(multiply(u,sk_c1),u)**. % 0.68/0.92 7831[6:Rew:7826.0,7796.6] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c1),y)* equal(multiply(v,sk_c1),sk_c1)** equal(x,sk_c1) equal(y,sk_c1) -> . % 0.68/0.92 7834[6:Rew:7826.0,7831.5,7826.0,7831.4] || equal(inverse(u),v) equal(inverse(w),sk_c1)** equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)**+ equal(w,y)* equal(v,sk_c1) equal(x,sk_c1) equal(y,sk_c1)* -> . % 0.68/0.92 7884[6:SpL:7703.0,7834.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(u,sk_c1) equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 7890[6:Obv:7884.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 7891[6:Rew:7790.0,7890.0] || equal(sk_c1,u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1)* equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 7892[6:Obv:7891.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1)** equal(u,w)* equal(x,sk_c1)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 7893[6:Con:7892.3] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(u,w)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 8025[6:SpL:7790.0,7893.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(sk_c1,v)* equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 8026[6:Obv:8025.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 8027[6:Con:8026.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 8113[6:SpL:7790.0,8027.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.68/0.92 8116[6:Obv:8113.1] || -> . % 0.68/0.92 8117[5:Spt:8116.0,32.0,5636.0] || equal(inverse(sk_c7),sk_c10)** -> . % 0.68/0.92 8118[5:Spt:8116.0,32.1] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 8120[5:MRR:5.0,8117.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.68/0.92 8122[5:MRR:14.0,8117.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 8124[5:MRR:23.0,8117.0] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 8129[5:SpR:8118.0,5768.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 8162[5:SpR:8120.0,7612.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.68/0.92 8164[5:Rew:5621.0,8162.0] || -> equal(sk_c11,sk_c1)**. % 0.68/0.92 8170[5:Rew:8164.0,8122.0] || -> equal(multiply(sk_c1,sk_c1),sk_c12)**. % 0.68/0.92 8172[5:Rew:8164.0,8124.0] || -> equal(multiply(sk_c2,sk_c3),sk_c1)**. % 0.68/0.92 8173[5:Rew:8164.0,5625.3] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(multiply(sk_c12,y),sk_c11)** -> . % 0.68/0.92 8178[5:Rew:8164.0,8173.7,8164.0,8173.6,8164.0,8173.5] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c1)** equal(multiply(x,sk_c1),sk_c12)** equal(multiply(sk_c12,y),sk_c1)** -> . % 0.68/0.92 8218[5:SpR:8172.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c1,u))**. % 0.68/0.92 8222[5:Rew:8129.0,8218.0] || -> equal(multiply(sk_c1,u),u)**. % 0.68/0.92 8223[5:Rew:8222.0,8170.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 8229[5:Rew:8223.0,8120.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 8234[5:Rew:8223.0,8178.1] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c1)** equal(multiply(x,sk_c1),sk_c12)** equal(multiply(sk_c12,y),sk_c1)** -> . % 0.68/0.92 8256[5:Rew:8222.0,8234.7,8223.0,8234.7,8223.0,8234.6,8223.0,8234.5,8223.0,8234.4,8223.0,8234.2] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c1) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c1),y)* equal(multiply(v,sk_c1),sk_c1)** equal(multiply(x,sk_c1),sk_c1)** equal(y,sk_c1) -> . % 0.68/0.92 8285[5:SpR:8222.0,1267.0] || -> equal(identity,sk_c1)**. % 0.68/0.92 8292[5:Rew:8285.0,1267.0] || -> equal(multiply(u,sk_c1),u)**. % 0.68/0.92 8297[5:Rew:8292.0,8256.6] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c1),y)* equal(multiply(v,sk_c1),sk_c1)** equal(x,sk_c1) equal(y,sk_c1) -> . % 0.68/0.92 8300[5:Rew:8292.0,8297.5,8292.0,8297.4] || equal(inverse(u),v) equal(inverse(w),sk_c1)** equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)**+ equal(w,y)* equal(v,sk_c1) equal(x,sk_c1) equal(y,sk_c1)* -> . % 0.68/0.92 8362[5:SpL:8222.0,8300.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(u,sk_c1) equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 8372[5:Obv:8362.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 8373[5:Rew:8229.0,8372.0] || equal(sk_c1,u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1)* equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 8374[5:Obv:8373.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1)** equal(u,w)* equal(x,sk_c1)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 8375[5:Con:8374.3] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(u,w)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 8505[5:SpL:8229.0,8375.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(sk_c1,v)* equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 8506[5:Obv:8505.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 8507[5:Con:8506.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 8593[5:SpL:8229.0,8507.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.68/0.92 8596[5:Obv:8593.1] || -> . % 0.68/0.92 8597[4:Spt:8596.0,34.0,5633.0] || equal(inverse(sk_c9),sk_c8)** -> . % 0.68/0.92 8598[4:Spt:8596.0,34.1] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 8601[4:MRR:7.0,8597.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.68/0.92 8605[4:MRR:16.0,8597.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 8607[4:MRR:25.0,8597.0] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 8610[4:SpR:8598.0,5768.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 8643[4:SpR:8601.0,7612.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.68/0.92 8645[4:Rew:5621.0,8643.0] || -> equal(sk_c11,sk_c1)**. % 0.68/0.92 8652[4:Rew:8645.0,8605.0] || -> equal(multiply(sk_c1,sk_c1),sk_c12)**. % 0.68/0.92 8654[4:Rew:8645.0,8607.0] || -> equal(multiply(sk_c2,sk_c3),sk_c1)**. % 0.68/0.92 8655[4:Rew:8645.0,5625.3] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(multiply(sk_c12,y),sk_c11)** -> . % 0.68/0.92 8659[4:Rew:8645.0,8655.7,8645.0,8655.6,8645.0,8655.5] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c1)** equal(multiply(x,sk_c1),sk_c12)** equal(multiply(sk_c12,y),sk_c1)** -> . % 0.68/0.92 8695[4:SpR:8654.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c1,u))**. % 0.68/0.92 8699[4:Rew:8610.0,8695.0] || -> equal(multiply(sk_c1,u),u)**. % 0.68/0.92 8700[4:Rew:8699.0,8652.0] || -> equal(sk_c12,sk_c1)**. % 0.68/0.92 8706[4:Rew:8700.0,8601.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.68/0.92 8711[4:Rew:8700.0,8659.1] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c1)** equal(multiply(x,sk_c1),sk_c12)** equal(multiply(sk_c12,y),sk_c1)** -> . % 0.68/0.92 8733[4:Rew:8699.0,8711.7,8700.0,8711.7,8700.0,8711.6,8700.0,8711.5,8700.0,8711.4,8700.0,8711.2] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c1) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c1),y)* equal(multiply(v,sk_c1),sk_c1)** equal(multiply(x,sk_c1),sk_c1)** equal(y,sk_c1) -> . % 0.68/0.92 8770[4:SpR:8699.0,1267.0] || -> equal(identity,sk_c1)**. % 0.68/0.92 8775[4:Rew:8770.0,1267.0] || -> equal(multiply(u,sk_c1),u)**. % 0.68/0.92 8782[4:Rew:8775.0,8733.6] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c1),y)* equal(multiply(v,sk_c1),sk_c1)** equal(x,sk_c1) equal(y,sk_c1) -> . % 0.68/0.92 8785[4:Rew:8775.0,8782.5,8775.0,8782.4] || equal(inverse(u),v) equal(inverse(w),sk_c1)** equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)**+ equal(w,y)* equal(v,sk_c1) equal(x,sk_c1) equal(y,sk_c1)* -> . % 0.68/0.92 8902[4:SpL:8699.0,8785.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(u,sk_c1) equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 8912[4:Obv:8902.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 8913[4:Rew:8706.0,8912.0] || equal(sk_c1,u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1)* equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.68/0.92 8914[4:Obv:8913.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1)** equal(u,w)* equal(x,sk_c1)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 8915[4:Con:8914.3] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(u,w)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.68/0.92 9003[4:SpL:8706.0,8915.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(sk_c1,v)* equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 9006[4:Obv:9003.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.68/0.92 9007[4:Con:9006.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.68/0.92 9065[4:SpL:8706.0,9007.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.68/0.92 9068[4:Obv:9065.1] || -> . % 0.68/0.92 9069[3:Spt:9068.0,35.0,5630.0] || equal(inverse(sk_c8),sk_c10)** -> . % 0.68/0.92 9070[3:Spt:9068.0,35.1] || -> equal(inverse(sk_c2),sk_c3)**. % 0.68/0.92 9072[3:MRR:8.0,9069.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.68/0.92 9074[3:MRR:17.0,9069.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.68/0.92 9076[3:MRR:26.0,9069.0] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.68/0.92 9079[3:SpR:9070.0,5768.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.68/0.92 9108[3:SpR:9072.0,7612.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.68/0.92 9110[3:Rew:5621.0,9108.0] || -> equal(sk_c11,sk_c1)**. % 0.68/0.92 9117[3:Rew:9110.0,9074.0] || -> equal(multiply(sk_c1,sk_c1),sk_c12)**. % 0.68/0.92 9119[3:Rew:9110.0,9076.0] || -> equal(multiply(sk_c2,sk_c3),sk_c1)**. % 0.68/0.92 9120[3:Rew:9110.0,5625.3] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(multiply(sk_c12,y),sk_c11)** -> . % 0.68/0.92 9124[3:Rew:9110.0,9120.7,9110.0,9120.6,9110.0,9120.5] || equal(inverse(u),v) equal(inverse(w),sk_c12) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c1)** equal(multiply(x,sk_c1),sk_c12)** equal(multiply(sk_c12,y),sk_c1)** -> . % 0.68/0.92 9154[3:SpR:9119.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c1,u))**. % 0.68/0.92 9158[3:Rew:9079.0,9154.0] || -> equal(multiply(sk_c1,u),u)**. % 0.78/0.94 9159[3:Rew:9158.0,9117.0] || -> equal(sk_c12,sk_c1)**. % 0.78/0.94 9165[3:Rew:9159.0,9072.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.78/0.94 9170[3:Rew:9159.0,9124.1] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c12) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c12),y)* equal(multiply(v,sk_c12),sk_c1)** equal(multiply(x,sk_c1),sk_c12)** equal(multiply(sk_c12,y),sk_c1)** -> . % 0.78/0.94 9192[3:Rew:9158.0,9170.7,9159.0,9170.7,9159.0,9170.6,9159.0,9170.5,9159.0,9170.4,9159.0,9170.2] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c1) equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c1),y)* equal(multiply(v,sk_c1),sk_c1)** equal(multiply(x,sk_c1),sk_c1)** equal(y,sk_c1) -> . % 0.78/0.94 9221[3:SpR:9158.0,1267.0] || -> equal(identity,sk_c1)**. % 0.78/0.94 9226[3:Rew:9221.0,1267.0] || -> equal(multiply(u,sk_c1),u)**. % 0.78/0.94 9231[3:Rew:9226.0,9192.6] || equal(inverse(u),v) equal(inverse(w),sk_c1) equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)** equal(multiply(w,sk_c1),y)* equal(multiply(v,sk_c1),sk_c1)** equal(x,sk_c1) equal(y,sk_c1) -> . % 0.78/0.94 9234[3:Rew:9226.0,9231.5,9226.0,9231.4] || equal(inverse(u),v) equal(inverse(w),sk_c1)** equal(inverse(x),sk_c1)** equal(multiply(u,v),sk_c1)**+ equal(w,y)* equal(v,sk_c1) equal(x,sk_c1) equal(y,sk_c1)* -> . % 0.78/0.94 9360[3:SpL:9158.0,9234.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(u,sk_c1) equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.78/0.94 9363[3:Obv:9360.3] || equal(inverse(sk_c1),u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1) equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.78/0.94 9364[3:Rew:9165.0,9363.0] || equal(sk_c1,u)* equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(v,x)* equal(u,sk_c1)* equal(w,sk_c1) equal(x,sk_c1)* -> . % 0.78/0.94 9365[3:Obv:9364.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1)** equal(u,w)* equal(x,sk_c1)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.78/0.94 9366[3:Con:9365.3] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(u,w)* equal(v,sk_c1) equal(w,sk_c1)* -> . % 0.78/0.94 9536[3:SpL:9165.0,9366.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(sk_c1,v)* equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.78/0.94 9539[3:Obv:9536.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) equal(v,sk_c1)* -> . % 0.78/0.94 9540[3:Con:9539.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.78/0.94 9542[3:SpL:9165.0,9540.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.78/0.94 9545[3:Obv:9542.1] || -> . % 0.78/0.94 9546[2:Spt:9545.0,1.0,5621.0] || equal(inverse(sk_c12),sk_c11)** -> . % 0.78/0.94 9547[2:Spt:9545.0,1.1] || -> equal(inverse(sk_c1),sk_c12)**. % 0.78/0.94 9548[2:MRR:64.0,9546.0] || -> equal(inverse(sk_c4),sk_c12)**. % 0.78/0.94 9549[2:MRR:28.0,9546.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.78/0.94 9550[2:MRR:10.0,9546.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.78/0.94 9552[2:MRR:46.0,9546.0] || -> equal(multiply(sk_c12,sk_c5),sk_c11)**. % 0.78/0.94 9553[2:MRR:19.0,9546.0] || -> equal(multiply(sk_c2,sk_c3),sk_c11)**. % 0.78/0.94 9554[2:MRR:55.0,9546.0] || -> equal(multiply(sk_c4,sk_c12),sk_c5)**. % 0.78/0.94 9560[2:SpR:9547.0,7612.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.78/0.94 9562[2:Rew:9560.0,9546.0] || equal(sk_c11,sk_c1)** -> . % 0.78/0.94 9571[2:SpR:9548.0,7612.0] || -> equal(inverse(sk_c12),sk_c4)**. % 0.78/0.94 9573[2:Rew:9560.0,9571.0] || -> equal(sk_c4,sk_c1)**. % 0.78/0.94 9575[2:Rew:9573.0,9554.0] || -> equal(multiply(sk_c1,sk_c12),sk_c5)**. % 0.78/0.94 9580[2:SpR:9549.0,5768.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.78/0.94 9591[2:SpR:9550.0,76.0] || -> equal(multiply(sk_c1,multiply(sk_c11,u)),multiply(sk_c12,u))**. % 0.78/0.94 9592[2:SpR:9550.0,130.0] || -> equal(multiply(inverse(sk_c1),sk_c12),sk_c11)**. % 0.78/0.94 9596[2:Rew:9547.0,9592.0] || -> equal(multiply(sk_c12,sk_c12),sk_c11)**. % 0.78/0.94 9606[2:SpR:9552.0,130.0] || -> equal(multiply(inverse(sk_c12),sk_c11),sk_c5)**. % 0.78/0.94 9610[2:Rew:9550.0,9606.0,9560.0,9606.0] || -> equal(sk_c5,sk_c12)**. % 0.78/0.94 9612[2:Rew:9610.0,9575.0] || -> equal(multiply(sk_c1,sk_c12),sk_c12)**. % 0.78/0.94 9618[2:SpR:9553.0,76.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c11,u))**. % 0.78/0.94 9624[2:Rew:9580.0,9618.0] || -> equal(multiply(sk_c11,u),u)**. % 0.78/0.94 9625[2:Rew:9624.0,9591.0] || -> equal(multiply(sk_c12,u),multiply(sk_c1,u))**. % 0.78/0.94 9628[2:Rew:9625.0,9596.0] || -> equal(multiply(sk_c1,sk_c12),sk_c11)**. % 0.78/0.94 9633[2:Rew:9612.0,9628.0] || -> equal(sk_c11,sk_c12)**. % 0.78/0.94 9634[2:Rew:9633.0,9562.0] || equal(sk_c12,sk_c1)** -> . % 0.78/0.94 9644[2:Rew:9633.0,9624.0] || -> equal(multiply(sk_c12,u),u)**. % 0.78/0.94 9655[2:Rew:9625.0,9644.0] || -> equal(multiply(sk_c1,u),u)**. % 0.78/0.94 9656[2:Rew:9655.0,9625.0] || -> equal(multiply(sk_c12,u),u)**. % 0.78/0.94 9708[2:SpR:9547.0,75.0] || -> equal(multiply(sk_c12,sk_c1),identity)**. % 0.78/0.94 9710[2:SpR:9560.0,75.0] || -> equal(multiply(sk_c1,sk_c12),identity)**. % 0.78/0.94 9711[2:Rew:9656.0,9708.0] || -> equal(identity,sk_c1)**. % 0.78/0.94 9720[2:Rew:9655.0,9710.0,9711.0,9710.0] || -> equal(sk_c12,sk_c1)**. % 0.78/0.94 9721[2:MRR:9720.0,9634.0] || -> . % 0.78/0.94 % SZS output end Refutation % 0.78/0.94 Formulae used in the proof : prove_this_1 prove_this_2 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_14 prove_this_15 prove_this_16 prove_this_17 prove_this_18 prove_this_19 prove_this_20 prove_this_22 prove_this_23 prove_this_24 prove_this_25 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_46 prove_this_51 prove_this_52 prove_this_53 prove_this_54 prove_this_55 prove_this_56 prove_this_57 prove_this_58 prove_this_59 prove_this_64 prove_this_65 prove_this_66 prove_this_67 prove_this_68 prove_this_72 prove_this_73 left_identity left_inverse associativity % 0.78/0.94 %------------------------------------------------------------------------------