%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP350-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:46:58 EDT 2022 % Result : Unsatisfiable 0.52s 0.74s % Output : Refutation 0.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP350-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n019.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Tue Jun 14 13:15:24 EDT 2022 % 0.14/0.34 % CPUTime : % 0.52/0.74 % 0.52/0.74 SPASS V 3.9 % 0.52/0.74 SPASS beiseite: Proof found. % 0.52/0.74 % SZS status Theorem % 0.52/0.74 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.52/0.74 SPASS derived 2692 clauses, backtracked 1011 clauses, performed 15 splits and kept 1734 clauses. % 0.52/0.74 SPASS allocated 65354 KBytes. % 0.52/0.74 SPASS spent 0:00:00.38 on the problem. % 0.52/0.74 0:00:00.04 for the input. % 0.52/0.74 0:00:00.00 for the FLOTTER CNF translation. % 0.52/0.74 0:00:00.02 for inferences. % 0.52/0.74 0:00:00.01 for the backtracking. % 0.52/0.74 0:00:00.29 for the reduction. % 0.52/0.74 % 0.52/0.74 % 0.52/0.74 Here is a proof with depth 6, length 493 : % 0.52/0.74 % SZS output start Refutation % 0.52/0.74 1[0:Inp] || -> equal(multiply(sk_c3,sk_c11),sk_c10)** equal(multiply(sk_c10,sk_c11),sk_c9). % 0.52/0.74 2[0:Inp] || -> equal(inverse(sk_c3),sk_c11) equal(multiply(sk_c10,sk_c11),sk_c9)**. % 0.52/0.74 3[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c11),sk_c9). % 0.52/0.74 4[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c10,sk_c11),sk_c9)**. % 0.52/0.74 5[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11)** equal(multiply(sk_c10,sk_c11),sk_c9). % 0.52/0.74 6[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c10,sk_c11),sk_c9)**. % 0.52/0.74 7[0:Inp] || -> equal(multiply(sk_c8,sk_c10),sk_c11)** equal(multiply(sk_c10,sk_c11),sk_c9). % 0.52/0.74 9[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c10,sk_c11),sk_c9)**. % 0.52/0.74 11[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.52/0.74 12[0:Inp] || -> equal(inverse(sk_c3),sk_c11)** equal(inverse(sk_c10),sk_c9). % 0.52/0.74 13[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 14[0:Inp] || -> equal(inverse(sk_c4),sk_c10)** equal(inverse(sk_c10),sk_c9). % 0.52/0.74 15[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.52/0.74 16[0:Inp] || -> equal(inverse(sk_c5),sk_c8)** equal(inverse(sk_c10),sk_c9). % 0.52/0.74 17[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.52/0.74 18[0:Inp] || -> equal(inverse(sk_c7),sk_c6)** equal(inverse(sk_c10),sk_c9). % 0.52/0.74 19[0:Inp] || -> equal(inverse(sk_c6),sk_c8)** equal(inverse(sk_c10),sk_c9). % 0.52/0.74 20[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.52/0.74 21[0:Inp] || -> equal(multiply(sk_c3,sk_c11),sk_c10)** equal(multiply(sk_c9,sk_c11),sk_c10). % 0.52/0.74 22[0:Inp] || -> equal(inverse(sk_c3),sk_c11) equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.52/0.74 23[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(multiply(sk_c9,sk_c11),sk_c10). % 0.52/0.74 24[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.52/0.74 25[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c10). % 0.52/0.74 26[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.52/0.74 27[0:Inp] || -> equal(multiply(sk_c8,sk_c10),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c10). % 0.52/0.74 28[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.52/0.74 29[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.52/0.74 33[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 34[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(inverse(sk_c1),sk_c11)**. % 0.52/0.74 39[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(inverse(sk_c1),sk_c11)**. % 0.52/0.74 53[0:Inp] || -> equal(inverse(sk_c2),sk_c10) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 54[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(inverse(sk_c2),sk_c10)**. % 0.52/0.74 59[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(inverse(sk_c2),sk_c10)**. % 0.52/0.74 61[0:Inp] || -> equal(multiply(sk_c3,sk_c11),sk_c10) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.52/0.74 62[0:Inp] || -> equal(inverse(sk_c3),sk_c11) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.52/0.74 65[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.52/0.74 66[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.52/0.74 68[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.52/0.74 69[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.52/0.74 71[0:Inp] || equal(inverse(u),v)* equal(inverse(w),u) equal(inverse(x),v) equal(inverse(y),sk_c10) equal(inverse(z),sk_c11) equal(inverse(x1),sk_c10) equal(inverse(x2),sk_c11) equal(inverse(sk_c10),sk_c9) equal(multiply(w,v),u)*+ equal(multiply(x,v),sk_c11)** equal(multiply(v,sk_c10),sk_c11)** equal(multiply(y,sk_c10),sk_c9)** equal(multiply(z,sk_c11),sk_c10)** equal(multiply(x1,sk_c9),sk_c10)** equal(multiply(x2,sk_c10),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c10)** equal(multiply(sk_c10,sk_c11),sk_c9) -> . % 0.52/0.74 72[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.52/0.74 73[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.52/0.74 74[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.52/0.74 75[1:Spt:71.0,71.1,71.2,71.8,71.9,71.10] || equal(inverse(u),v)* equal(inverse(w),u) equal(inverse(x),v) equal(multiply(w,v),u)*+ equal(multiply(x,v),sk_c11)** equal(multiply(v,sk_c10),sk_c11)** -> . % 0.52/0.74 76[1:EqR:75.3] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c11)** equal(multiply(v,sk_c10),sk_c11) -> . % 0.52/0.74 77[2:Spt:19.1] || -> equal(inverse(sk_c10),sk_c9)**. % 0.52/0.74 79[3:Spt:29.1] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.52/0.74 82[4:Spt:9.1] || -> equal(multiply(sk_c10,sk_c11),sk_c9)**. % 0.52/0.74 87[5:Spt:59.1] || -> equal(inverse(sk_c2),sk_c10)**. % 0.52/0.74 89[6:Spt:39.1] || -> equal(inverse(sk_c1),sk_c11)**. % 0.52/0.74 91[7:Spt:69.1] || -> equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.52/0.74 93[7:SpL:91.0,75.3] || equal(inverse(u),sk_c9)** equal(inverse(sk_c2),u)* equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.52/0.74 94[7:Rew:87.0,93.1] || equal(inverse(u),sk_c9)** equal(sk_c10,u) equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.52/0.74 95[7:Obv:94.1] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.52/0.74 104[2:SpR:77.0,73.0] || -> equal(multiply(sk_c9,sk_c10),identity)**. % 0.52/0.74 105[5:SpR:87.0,73.0] || -> equal(multiply(sk_c10,sk_c2),identity)**. % 0.52/0.74 106[6:SpR:89.0,73.0] || -> equal(multiply(sk_c11,sk_c1),identity)**. % 0.52/0.74 108[7:Rew:104.0,95.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c11)** equal(identity,sk_c11) -> . % 0.52/0.74 117[2:SpR:104.0,74.0] || -> equal(multiply(sk_c9,multiply(sk_c10,u)),multiply(identity,u))**. % 0.52/0.74 122[0:SpR:73.0,74.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.52/0.74 125[2:Rew:72.0,117.0] || -> equal(multiply(sk_c9,multiply(sk_c10,u)),u)**. % 0.52/0.74 127[0:Rew:72.0,122.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.52/0.74 137[4:SpR:82.0,125.0] || -> equal(multiply(sk_c9,sk_c9),sk_c11)**. % 0.52/0.74 138[5:SpR:105.0,125.0] || -> equal(multiply(sk_c9,identity),sk_c2)**. % 0.52/0.74 146[5:SpR:138.0,74.0] || -> equal(multiply(sk_c9,multiply(identity,u)),multiply(sk_c2,u))**. % 0.52/0.74 149[5:Rew:72.0,146.0] || -> equal(multiply(sk_c2,u),multiply(sk_c9,u))**. % 0.52/0.74 150[7:Rew:149.0,91.0] || -> equal(multiply(sk_c9,sk_c9),sk_c10)**. % 0.52/0.74 154[7:Rew:137.0,150.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 156[7:Rew:154.0,79.0] || -> equal(multiply(sk_c9,sk_c10),sk_c10)**. % 0.52/0.74 157[7:Rew:154.0,82.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.52/0.74 158[7:Rew:154.0,89.0] || -> equal(inverse(sk_c1),sk_c10)**. % 0.52/0.74 160[7:Rew:154.0,106.0] || -> equal(multiply(sk_c10,sk_c1),identity)**. % 0.52/0.74 171[7:Rew:154.0,108.3] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c10)** equal(identity,sk_c11) -> . % 0.52/0.74 179[7:Rew:104.0,156.0] || -> equal(identity,sk_c10)**. % 0.52/0.74 180[7:Rew:179.0,72.0] || -> equal(multiply(sk_c10,u),u)**. % 0.52/0.74 181[7:Rew:179.0,73.0] || -> equal(multiply(inverse(u),u),sk_c10)**. % 0.52/0.74 185[7:Rew:179.0,160.0] || -> equal(multiply(sk_c10,sk_c1),sk_c10)**. % 0.52/0.74 187[7:Rew:180.0,185.0] || -> equal(sk_c1,sk_c10)**. % 0.52/0.74 188[7:Rew:180.0,157.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 189[7:Rew:187.0,158.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 207[7:Rew:179.0,171.4,154.0,171.4,188.0,171.3,188.0,171.1,188.0,171.0] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(sk_c10,u) equal(multiply(v,sk_c10),sk_c10)** equal(sk_c10,sk_c10) -> . % 0.52/0.74 208[7:Obv:207.4] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(sk_c10,u) equal(multiply(v,sk_c10),sk_c10)** -> . % 0.52/0.74 244[0:SpR:127.0,127.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.52/0.74 246[0:SpR:74.0,127.0] || -> equal(multiply(inverse(multiply(u,v)),multiply(u,multiply(v,w))),w)**. % 0.52/0.74 248[7:SpR:181.0,127.0] || -> equal(multiply(inverse(inverse(u)),sk_c10),u)**. % 0.52/0.74 252[7:Rew:244.0,248.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.74 258[7:Rew:252.0,208.3] || equal(inverse(u),sk_c10)**+ equal(inverse(v),sk_c10)** equal(sk_c10,u) equal(v,sk_c10) -> . % 0.52/0.74 280[0:SpR:244.0,127.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.52/0.74 337[0:SpR:280.0,246.0] || -> equal(multiply(inverse(multiply(u,v)),multiply(u,w)),multiply(inverse(v),w))**. % 0.52/0.74 502[7:SpL:189.0,258.0] || equal(sk_c10,sk_c10) equal(inverse(u),sk_c10)** equal(sk_c10,sk_c10) equal(u,sk_c10) -> . % 0.52/0.74 505[7:Obv:502.2] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.52/0.74 507[7:SpL:189.0,505.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.52/0.74 510[7:Obv:507.1] || -> . % 0.52/0.74 511[7:Spt:510.0,69.1,91.0] || equal(multiply(sk_c2,sk_c9),sk_c10)** -> . % 0.52/0.74 512[7:Spt:510.0,69.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.74 513[7:Rew:149.0,511.0] || equal(multiply(sk_c9,sk_c9),sk_c10)** -> . % 0.52/0.74 514[7:Rew:137.0,513.0] || equal(sk_c11,sk_c10)** -> . % 0.52/0.74 515[5:Rew:137.0,68.1,149.0,68.1] || -> equal(inverse(sk_c7),sk_c6)** equal(sk_c11,sk_c10). % 0.52/0.74 517[5:Rew:137.0,66.1,149.0,66.1] || -> equal(inverse(sk_c5),sk_c8)** equal(sk_c11,sk_c10). % 0.52/0.74 518[7:MRR:517.1,514.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.52/0.74 521[5:Rew:137.0,62.1,149.0,62.1] || -> equal(inverse(sk_c3),sk_c11)** equal(sk_c11,sk_c10). % 0.52/0.74 522[7:MRR:521.1,514.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.52/0.74 528[5:Rew:137.0,65.1,149.0,65.1] || -> equal(multiply(sk_c5,sk_c8),sk_c11)** equal(sk_c11,sk_c10). % 0.52/0.74 529[7:MRR:528.1,514.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.52/0.74 532[5:Rew:137.0,61.1,149.0,61.1] || -> equal(multiply(sk_c3,sk_c11),sk_c10)** equal(sk_c11,sk_c10). % 0.52/0.74 533[7:MRR:532.1,514.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.52/0.74 559[7:SpR:518.0,280.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.52/0.74 564[7:SpR:522.0,127.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.52/0.74 583[3:SpR:79.0,127.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c11)**. % 0.52/0.74 598[2:SpR:104.0,127.0] || -> equal(multiply(inverse(sk_c9),identity),sk_c10)**. % 0.52/0.74 601[7:SpR:529.0,74.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.52/0.74 605[7:Rew:559.0,601.0] || -> equal(multiply(sk_c11,u),u)**. % 0.52/0.74 607[7:Rew:605.0,564.0] || -> equal(multiply(sk_c3,u),u)**. % 0.52/0.74 632[7:Rew:607.0,533.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 633[7:MRR:632.0,514.0] || -> . % 0.52/0.74 684[6:Spt:633.0,39.1,89.0] || equal(inverse(sk_c1),sk_c11)** -> . % 0.52/0.74 685[6:Spt:633.0,39.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.74 752[0:SpR:73.0,127.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.52/0.74 753[0:SpR:73.0,280.0] || -> equal(multiply(u,identity),u)**. % 0.52/0.74 755[6:SpR:685.0,73.0] || -> equal(multiply(sk_c8,sk_c6),identity)**. % 0.52/0.74 760[2:Rew:753.0,598.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.52/0.74 767[3:Rew:760.0,583.0] || -> equal(multiply(sk_c10,sk_c10),sk_c11)**. % 0.52/0.74 773[0:Rew:753.0,752.0] || -> equal(inverse(inverse(u)),u)**. % 0.52/0.74 788[6:SpR:755.0,127.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c6)**. % 0.52/0.74 790[6:Rew:753.0,788.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.52/0.74 794[6:SpR:790.0,73.0] || -> equal(multiply(sk_c6,sk_c8),identity)**. % 0.52/0.74 796[7:Spt:515.1] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 799[7:Rew:796.0,79.0] || -> equal(multiply(sk_c9,sk_c10),sk_c10)**. % 0.52/0.74 800[7:Rew:796.0,82.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.52/0.74 803[7:Rew:796.0,76.3] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c10)** equal(multiply(v,sk_c10),sk_c11) -> . % 0.52/0.74 821[7:Rew:796.0,767.0] || -> equal(multiply(sk_c10,sk_c10),sk_c10)**. % 0.52/0.74 830[7:Rew:104.0,799.0] || -> equal(identity,sk_c10)**. % 0.52/0.74 833[7:Rew:830.0,73.0] || -> equal(multiply(inverse(u),u),sk_c10)**. % 0.52/0.74 836[7:Rew:830.0,753.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.74 839[7:Rew:800.0,821.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 840[7:Rew:839.0,77.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 904[7:Rew:836.0,803.4,796.0,803.4] || equal(inverse(multiply(u,v)),v)**+ equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c10)** equal(v,sk_c10) -> . % 0.52/0.74 938[7:SpR:836.0,280.0] || -> equal(multiply(u,inverse(u)),sk_c10)**. % 0.52/0.74 1560[7:SpL:833.0,904.0] || equal(inverse(sk_c10),u) equal(multiply(inverse(u),u),inverse(inverse(u)))** equal(inverse(v),u) equal(multiply(v,u),sk_c10)** equal(u,sk_c10) -> . % 0.52/0.74 1571[7:Rew:833.0,1560.1,773.0,1560.1,840.0,1560.0] || equal(sk_c10,u) equal(sk_c10,u) equal(inverse(v),u) equal(multiply(v,u),sk_c10)** equal(u,sk_c10) -> . % 0.52/0.74 1572[7:Obv:1571.1] || equal(inverse(u),v) equal(multiply(u,v),sk_c10)** equal(v,sk_c10) -> . % 0.52/0.74 1574[7:SpL:938.0,1572.1] || equal(inverse(u),inverse(u))* equal(sk_c10,sk_c10) equal(inverse(u),sk_c10) -> . % 0.52/0.74 1596[7:Obv:1574.1] || equal(inverse(u),sk_c10)** -> . % 0.52/0.74 1597[7:UnC:1596.0,773.0] || -> . % 0.52/0.74 1603[7:Spt:1597.0,515.1,796.0] || equal(sk_c11,sk_c10)** -> . % 0.52/0.74 1604[7:Spt:1597.0,515.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.52/0.74 1605[7:MRR:517.1,1603.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.52/0.74 1607[7:MRR:521.1,1603.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.52/0.74 1610[7:MRR:528.1,1603.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.52/0.74 1612[7:MRR:532.1,1603.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.52/0.74 1647[7:SpR:1605.0,773.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.74 1649[7:Rew:790.0,1647.0] || -> equal(sk_c6,sk_c5)**. % 0.52/0.74 1653[7:Rew:1649.0,794.0] || -> equal(multiply(sk_c5,sk_c8),identity)**. % 0.52/0.74 1657[7:Rew:1610.0,1653.0] || -> equal(identity,sk_c11)**. % 0.52/0.74 1661[7:Rew:1657.0,753.0] || -> equal(multiply(u,sk_c11),u)**. % 0.52/0.74 1675[7:Rew:1661.0,1612.0] || -> equal(sk_c3,sk_c10)**. % 0.52/0.74 1676[7:Rew:1661.0,79.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 1678[7:Rew:1675.0,1607.0] || -> equal(inverse(sk_c10),sk_c11)**. % 0.52/0.74 1681[7:Rew:1676.0,77.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 1690[7:Rew:1678.0,1681.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 1691[7:MRR:1690.0,1603.0] || -> . % 0.52/0.74 1699[5:Spt:1691.0,59.1,87.0] || equal(inverse(sk_c2),sk_c10)** -> . % 0.52/0.74 1700[5:Spt:1691.0,59.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.74 1703[5:MRR:54.1,1699.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.74 1708[5:MRR:53.0,1699.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 1744[5:SpR:1703.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.74 1746[5:Rew:77.0,1744.0] || -> equal(sk_c4,sk_c9)**. % 0.52/0.74 1748[5:Rew:1746.0,1708.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 1749[5:Rew:104.0,1748.0] || -> equal(identity,sk_c9)**. % 0.52/0.74 1750[5:Rew:1749.0,753.0] || -> equal(multiply(u,sk_c9),u)**. % 0.52/0.74 1751[5:Rew:1749.0,104.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 1752[5:Rew:1749.0,72.0] || -> equal(multiply(sk_c9,u),u)**. % 0.52/0.74 1756[5:Rew:1749.0,73.0] || -> equal(multiply(inverse(u),u),sk_c9)**. % 0.52/0.74 1760[5:Rew:1750.0,137.0] || -> equal(sk_c9,sk_c11)**. % 0.52/0.74 1761[5:Rew:1760.0,77.0] || -> equal(inverse(sk_c10),sk_c11)**. % 0.52/0.74 1773[5:Rew:1760.0,1750.0] || -> equal(multiply(u,sk_c11),u)**. % 0.52/0.74 1774[5:Rew:1760.0,1751.0] || -> equal(multiply(sk_c11,sk_c10),sk_c11)**. % 0.52/0.74 1776[5:Rew:1760.0,1752.0] || -> equal(multiply(sk_c11,u),u)**. % 0.52/0.74 1777[5:Rew:1776.0,1774.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 1781[5:Rew:1777.0,76.4] || equal(inverse(multiply(u,v)),v)** equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c11)** equal(multiply(v,sk_c10),sk_c10) -> . % 0.52/0.74 1787[5:Rew:1777.0,1760.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 1790[5:Rew:1777.0,1761.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 1796[5:Rew:1777.0,1773.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.74 1812[5:Rew:1787.0,1756.0] || -> equal(multiply(inverse(u),u),sk_c10)**. % 0.52/0.74 1831[5:Rew:1796.0,1781.4,1777.0,1781.3] || equal(inverse(multiply(u,v)),v)**+ equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c10)** equal(v,sk_c10) -> . % 0.52/0.74 1856[5:SpR:1796.0,280.0] || -> equal(multiply(u,inverse(u)),sk_c10)**. % 0.52/0.74 2265[5:SpL:1812.0,1831.0] || equal(inverse(sk_c10),u) equal(multiply(inverse(u),u),inverse(inverse(u)))** equal(inverse(v),u) equal(multiply(v,u),sk_c10)** equal(u,sk_c10) -> . % 0.52/0.74 2275[5:Rew:1812.0,2265.1,773.0,2265.1,1790.0,2265.0] || equal(sk_c10,u) equal(sk_c10,u) equal(inverse(v),u) equal(multiply(v,u),sk_c10)** equal(u,sk_c10) -> . % 0.52/0.74 2276[5:Obv:2275.1] || equal(inverse(u),v) equal(multiply(u,v),sk_c10)** equal(v,sk_c10) -> . % 0.52/0.74 2437[5:SpL:1856.0,2276.1] || equal(inverse(u),inverse(u))* equal(sk_c10,sk_c10) equal(inverse(u),sk_c10) -> . % 0.52/0.74 2459[5:Obv:2437.1] || equal(inverse(u),sk_c10)** -> . % 0.52/0.74 2460[5:UnC:2459.0,1790.0] || -> . % 0.52/0.74 2466[4:Spt:2460.0,9.1,82.0] || equal(multiply(sk_c10,sk_c11),sk_c9)** -> . % 0.52/0.74 2467[4:Spt:2460.0,9.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.74 2471[4:MRR:4.1,2466.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.74 2476[4:MRR:3.1,2466.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 2536[4:SpR:2471.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.74 2540[4:Rew:77.0,2536.0] || -> equal(sk_c4,sk_c9)**. % 0.52/0.74 2542[4:Rew:2540.0,2476.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 2543[4:Rew:104.0,2542.0] || -> equal(identity,sk_c9)**. % 0.52/0.74 2545[4:Rew:2543.0,72.0] || -> equal(multiply(sk_c9,u),u)**. % 0.52/0.74 2546[4:Rew:2543.0,104.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 2547[4:Rew:2543.0,753.0] || -> equal(multiply(u,sk_c9),u)**. % 0.52/0.74 2559[4:Rew:2545.0,79.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 2561[4:Rew:2559.0,2466.0] || equal(multiply(sk_c10,sk_c10),sk_c9)** -> . % 0.52/0.74 2571[4:Rew:2545.0,2546.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 2579[4:Rew:2571.0,2547.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.74 2600[4:Rew:2579.0,2561.0,2571.0,2561.0] || equal(sk_c10,sk_c10)* -> . % 0.52/0.74 2601[4:Obv:2600.0] || -> . % 0.52/0.74 2627[3:Spt:2601.0,29.1,79.0] || equal(multiply(sk_c9,sk_c11),sk_c10)** -> . % 0.52/0.74 2628[3:Spt:2601.0,29.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.74 2630[3:MRR:26.1,2627.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.52/0.74 2631[3:MRR:24.1,2627.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.74 2632[3:MRR:22.1,2627.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.52/0.74 2634[3:MRR:27.1,2627.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.52/0.74 2635[3:MRR:25.1,2627.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.52/0.74 2636[3:MRR:23.1,2627.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 2637[3:MRR:21.1,2627.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.52/0.74 2640[3:SpR:2628.0,773.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.52/0.74 2672[3:SpR:2630.0,773.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.74 2676[3:Rew:2640.0,2672.0] || -> equal(sk_c6,sk_c5)**. % 0.52/0.74 2678[3:Rew:2676.0,2640.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.74 2689[3:SpR:2631.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.74 2693[3:Rew:77.0,2689.0] || -> equal(sk_c4,sk_c9)**. % 0.52/0.74 2695[3:Rew:2693.0,2636.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 2696[3:Rew:104.0,2695.0] || -> equal(identity,sk_c9)**. % 0.52/0.74 2697[3:Rew:2696.0,753.0] || -> equal(multiply(u,sk_c9),u)**. % 0.52/0.74 2698[3:Rew:2696.0,104.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 2699[3:Rew:2696.0,72.0] || -> equal(multiply(sk_c9,u),u)**. % 0.52/0.74 2706[3:Rew:2699.0,2698.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 2712[3:Rew:2699.0,2627.0] || equal(sk_c11,sk_c10)** -> . % 0.52/0.74 2717[3:Rew:2706.0,2697.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.74 2724[3:Rew:2717.0,2634.0] || -> equal(sk_c8,sk_c11)**. % 0.52/0.74 2727[3:Rew:2724.0,2635.0] || -> equal(multiply(sk_c5,sk_c11),sk_c11)**. % 0.52/0.74 2728[3:Rew:2724.0,2678.0] || -> equal(inverse(sk_c11),sk_c5)**. % 0.52/0.74 2755[3:SpR:2632.0,773.0] || -> equal(inverse(sk_c11),sk_c3)**. % 0.52/0.74 2759[3:Rew:2728.0,2755.0] || -> equal(sk_c5,sk_c3)**. % 0.52/0.74 2763[3:Rew:2759.0,2727.0] || -> equal(multiply(sk_c3,sk_c11),sk_c11)**. % 0.52/0.74 2771[3:Rew:2637.0,2763.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 2772[3:MRR:2771.0,2712.0] || -> . % 0.52/0.74 2773[2:Spt:2772.0,19.1,77.0] || equal(inverse(sk_c10),sk_c9)** -> . % 0.52/0.74 2774[2:Spt:2772.0,19.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.74 2775[2:MRR:18.1,2773.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.52/0.74 2776[2:MRR:16.1,2773.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.52/0.74 2777[2:MRR:14.1,2773.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.74 2778[2:MRR:12.1,2773.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.52/0.74 2779[2:MRR:20.0,2773.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.52/0.74 2780[2:MRR:17.0,2773.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.52/0.74 2781[2:MRR:15.0,2773.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.52/0.74 2782[2:MRR:13.0,2773.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 2783[2:MRR:11.0,2773.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.52/0.74 2786[2:SpR:2774.0,773.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.52/0.74 2792[2:SpR:2775.0,773.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.52/0.74 2796[2:Rew:2774.0,2792.0] || -> equal(sk_c7,sk_c8)**. % 0.52/0.74 2798[2:Rew:2796.0,2779.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.52/0.74 2804[2:SpR:2776.0,280.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.52/0.74 2805[2:SpR:2776.0,773.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.74 2809[2:Rew:2786.0,2805.0] || -> equal(sk_c6,sk_c5)**. % 0.52/0.74 2811[2:Rew:2809.0,2786.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.74 2816[2:Rew:2809.0,2798.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.52/0.74 2823[2:SpR:2777.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.74 2827[2:Rew:2823.0,2773.0] || equal(sk_c4,sk_c9)** -> . % 0.52/0.74 2828[2:SpR:2778.0,127.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.52/0.74 2830[2:SpR:2778.0,773.0] || -> equal(inverse(sk_c11),sk_c3)**. % 0.52/0.74 2860[2:SpR:2781.0,74.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.52/0.74 2861[2:SpR:2781.0,127.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.52/0.74 2865[2:Rew:2776.0,2861.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.52/0.74 2866[2:Rew:2804.0,2860.0] || -> equal(multiply(sk_c11,u),u)**. % 0.52/0.74 2868[2:Rew:2866.0,2828.0] || -> equal(multiply(sk_c3,u),u)**. % 0.52/0.74 2873[2:Rew:2868.0,2783.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 2877[2:Rew:2873.0,2830.0] || -> equal(inverse(sk_c10),sk_c3)**. % 0.52/0.74 2878[2:Rew:2873.0,2780.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)**. % 0.52/0.74 2886[2:Rew:2873.0,2865.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.52/0.74 2887[2:Rew:2873.0,2866.0] || -> equal(multiply(sk_c10,u),u)**. % 0.52/0.74 2888[2:Rew:2823.0,2877.0] || -> equal(sk_c4,sk_c3)**. % 0.52/0.74 2890[2:Rew:2888.0,2827.0] || equal(sk_c3,sk_c9)** -> . % 0.52/0.74 2891[2:Rew:2888.0,2823.0] || -> equal(inverse(sk_c10),sk_c3)**. % 0.52/0.74 2892[2:Rew:2888.0,2782.0] || -> equal(multiply(sk_c3,sk_c10),sk_c9)**. % 0.52/0.74 2899[2:Rew:2878.0,2886.0] || -> equal(sk_c8,sk_c10)**. % 0.52/0.74 2902[2:Rew:2899.0,2811.0] || -> equal(inverse(sk_c10),sk_c5)**. % 0.52/0.74 2903[2:Rew:2899.0,2816.0] || -> equal(multiply(sk_c10,sk_c10),sk_c5)**. % 0.52/0.74 2912[2:Rew:2891.0,2902.0] || -> equal(sk_c5,sk_c3)**. % 0.52/0.74 2916[2:Rew:2868.0,2892.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 2917[2:Rew:2916.0,2890.0] || equal(sk_c3,sk_c10)** -> . % 0.52/0.74 2918[2:Rew:2887.0,2903.0,2912.0,2903.0] || -> equal(sk_c3,sk_c10)**. % 0.52/0.74 2919[2:MRR:2918.0,2917.0] || -> . % 0.52/0.74 2945[1:Spt:2919.0,71.3,71.4,71.5,71.6,71.7,71.11,71.12,71.13,71.14,71.15,71.16] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(inverse(sk_c10),sk_c9) equal(multiply(u,sk_c10),sk_c9)**+ equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c10)** equal(multiply(sk_c10,sk_c11),sk_c9) -> . % 0.52/0.74 2947[2:Spt:18.1] || -> equal(inverse(sk_c10),sk_c9)**. % 0.52/0.74 2948[2:Rew:2947.0,2945.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(sk_c9,sk_c9) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c10)** equal(multiply(sk_c10,sk_c11),sk_c9) -> . % 0.52/0.74 2950[2:Obv:2948.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c10)** equal(multiply(sk_c10,sk_c11),sk_c9) -> . % 0.52/0.74 2954[2:SpR:2947.0,773.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.52/0.74 2958[3:Spt:9.1] || -> equal(multiply(sk_c10,sk_c11),sk_c9)**. % 0.52/0.74 2960[3:Rew:2958.0,2950.9] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c10)** equal(sk_c9,sk_c9) -> . % 0.52/0.74 2961[3:Obv:2960.9] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c10)** -> . % 0.52/0.74 2964[3:SpR:2958.0,127.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c11)**. % 0.52/0.74 2965[3:SpR:2958.0,337.0] || -> equal(multiply(inverse(sk_c9),multiply(sk_c10,u)),multiply(inverse(sk_c11),u))**. % 0.52/0.74 2968[3:Rew:2947.0,2964.0] || -> equal(multiply(sk_c9,sk_c9),sk_c11)**. % 0.52/0.74 2969[3:Rew:2954.0,2965.0] || -> equal(multiply(sk_c10,multiply(sk_c10,u)),multiply(inverse(sk_c11),u))**. % 0.52/0.74 2971[4:Spt:28.1] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.52/0.74 2973[4:Rew:2971.0,2961.8] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(sk_c10,sk_c10) -> . % 0.52/0.74 2974[4:Obv:2973.8] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** -> . % 0.52/0.74 2977[4:SpR:2971.0,127.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c11)**. % 0.52/0.74 2978[4:SpR:2971.0,337.0] || -> equal(multiply(inverse(sk_c10),multiply(sk_c9,u)),multiply(inverse(sk_c11),u))**. % 0.52/0.74 2981[4:Rew:2954.0,2977.0] || -> equal(multiply(sk_c10,sk_c10),sk_c11)**. % 0.52/0.74 2982[4:Rew:2947.0,2978.0] || -> equal(multiply(sk_c9,multiply(sk_c9,u)),multiply(inverse(sk_c11),u))**. % 0.52/0.74 2983[5:Spt:39.1] || -> equal(inverse(sk_c1),sk_c11)**. % 0.52/0.74 2986[5:SpR:2983.0,773.0] || -> equal(inverse(sk_c11),sk_c1)**. % 0.52/0.74 2990[5:Rew:2986.0,2969.0] || -> equal(multiply(sk_c10,multiply(sk_c10,u)),multiply(sk_c1,u))**. % 0.52/0.74 2991[5:Rew:2986.0,2982.0] || -> equal(multiply(sk_c9,multiply(sk_c9,u)),multiply(sk_c1,u))**. % 0.52/0.74 2992[6:Spt:59.1] || -> equal(inverse(sk_c2),sk_c10)**. % 0.52/0.74 2995[6:SpR:2992.0,773.0] || -> equal(inverse(sk_c10),sk_c2)**. % 0.52/0.74 2999[6:Rew:2947.0,2995.0] || -> equal(sk_c2,sk_c9)**. % 0.52/0.74 3001[6:Rew:2999.0,61.1] || -> equal(multiply(sk_c3,sk_c11),sk_c10)** equal(multiply(sk_c9,sk_c9),sk_c10). % 0.52/0.74 3006[6:Rew:2999.0,62.1] || -> equal(inverse(sk_c3),sk_c11) equal(multiply(sk_c9,sk_c9),sk_c10)**. % 0.52/0.74 3013[6:Rew:2968.0,3006.1] || -> equal(inverse(sk_c3),sk_c11)** equal(sk_c11,sk_c10). % 0.52/0.74 3023[6:Rew:2968.0,3001.1] || -> equal(multiply(sk_c3,sk_c11),sk_c10)** equal(sk_c11,sk_c10). % 0.52/0.74 3050[3:SpR:2968.0,74.0] || -> equal(multiply(sk_c9,multiply(sk_c9,u)),multiply(sk_c11,u))**. % 0.52/0.74 3056[5:Rew:2991.0,3050.0] || -> equal(multiply(sk_c1,u),multiply(sk_c11,u))**. % 0.52/0.74 3071[5:Rew:3056.0,2990.0] || -> equal(multiply(sk_c10,multiply(sk_c10,u)),multiply(sk_c11,u))**. % 0.52/0.74 3123[0:SpR:73.0,753.0] || -> equal(inverse(identity),identity)**. % 0.52/0.74 3131[2:SpR:2947.0,73.0] || -> equal(multiply(sk_c9,sk_c10),identity)**. % 0.52/0.74 3132[5:SpR:2983.0,73.0] || -> equal(multiply(sk_c11,sk_c1),identity)**. % 0.52/0.74 3134[5:SpR:2986.0,73.0] || -> equal(multiply(sk_c1,sk_c11),identity)**. % 0.52/0.74 3136[5:Rew:3056.0,3134.0] || -> equal(multiply(sk_c11,sk_c11),identity)**. % 0.52/0.74 3155[7:Spt:3013.1] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 3157[7:Rew:3155.0,2971.0] || -> equal(multiply(sk_c9,sk_c10),sk_c10)**. % 0.52/0.74 3167[7:Rew:3155.0,2974.1] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** -> . % 0.52/0.74 3179[7:Rew:3131.0,3157.0] || -> equal(identity,sk_c10)**. % 0.52/0.74 3181[7:Rew:3179.0,753.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.74 3183[7:Rew:3179.0,3123.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 3187[7:Rew:2947.0,3183.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 3188[7:Rew:3187.0,2947.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 3220[7:Rew:3181.0,3167.7,3155.0,3167.7,3181.0,3167.6,3187.0,3167.6,3181.0,3167.5,3155.0,3167.5,3181.0,3167.4,3187.0,3167.4,3155.0,3167.3] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10)** equal(inverse(w),sk_c10)** equal(inverse(x),sk_c10)** equal(u,sk_c10) equal(v,sk_c10) equal(w,sk_c10) equal(x,sk_c10) -> . % 0.52/0.74 3221[7:Con:3220.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.52/0.74 3299[7:SpL:3188.0,3221.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.52/0.74 3300[7:Obv:3299.1] || -> . % 0.52/0.74 3301[7:Spt:3300.0,3013.1,3155.0] || equal(sk_c11,sk_c10)** -> . % 0.52/0.74 3302[7:Spt:3300.0,3013.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.52/0.74 3307[7:MRR:3023.1,3301.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.52/0.74 3314[7:SpR:3302.0,773.0] || -> equal(inverse(sk_c11),sk_c3)**. % 0.52/0.74 3318[7:Rew:2986.0,3314.0] || -> equal(sk_c1,sk_c3)**. % 0.52/0.74 3321[7:Rew:3318.0,3132.0] || -> equal(multiply(sk_c11,sk_c3),identity)**. % 0.52/0.74 3322[7:Rew:3318.0,3056.0] || -> equal(multiply(sk_c3,u),multiply(sk_c11,u))**. % 0.52/0.74 3324[7:Rew:3322.0,3307.0] || -> equal(multiply(sk_c11,sk_c11),sk_c10)**. % 0.52/0.74 3327[7:Rew:3136.0,3324.0] || -> equal(identity,sk_c10)**. % 0.52/0.74 3328[7:Rew:3327.0,3123.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 3331[7:Rew:3327.0,72.0] || -> equal(multiply(sk_c10,u),u)**. % 0.52/0.74 3336[7:Rew:3327.0,3321.0] || -> equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.52/0.74 3337[7:Rew:2947.0,3328.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 3339[7:Rew:3337.0,2954.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 3365[7:Rew:3331.0,3071.0] || -> equal(multiply(sk_c11,u),multiply(sk_c10,u))**. % 0.52/0.74 3378[7:Rew:3331.0,3365.0] || -> equal(multiply(sk_c11,u),u)**. % 0.52/0.74 3379[7:Rew:3378.0,3336.0] || -> equal(sk_c3,sk_c10)**. % 0.52/0.74 3385[7:Rew:3379.0,3302.0] || -> equal(inverse(sk_c10),sk_c11)**. % 0.52/0.74 3389[7:Rew:3339.0,3385.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 3390[7:MRR:3389.0,3301.0] || -> . % 0.52/0.74 3407[6:Spt:3390.0,59.1,2992.0] || equal(inverse(sk_c2),sk_c10)** -> . % 0.52/0.74 3408[6:Spt:3390.0,59.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.74 3411[6:MRR:54.1,3407.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.74 3416[6:MRR:53.0,3407.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 3502[6:SpR:3411.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.74 3506[6:Rew:2947.0,3502.0] || -> equal(sk_c4,sk_c9)**. % 0.52/0.74 3508[6:Rew:3506.0,3416.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 3509[6:Rew:3131.0,3508.0] || -> equal(identity,sk_c9)**. % 0.52/0.74 3510[6:Rew:3509.0,3123.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.52/0.74 3512[6:Rew:3509.0,3131.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 3515[6:Rew:3509.0,753.0] || -> equal(multiply(u,sk_c9),u)**. % 0.52/0.74 3519[6:Rew:2954.0,3510.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 3520[6:Rew:3519.0,2947.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 3536[6:Rew:3519.0,2974.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,sk_c10),sk_c10)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** -> . % 0.52/0.74 3541[6:Rew:2981.0,3512.0,3519.0,3512.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 3560[6:Rew:3519.0,3515.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.74 3612[6:Rew:3560.0,3536.7,3541.0,3536.7,3560.0,3536.6,3519.0,3536.6,3560.0,3536.5,3541.0,3536.5,3560.0,3536.4,3541.0,3536.3,3541.0,3536.1] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10)** equal(inverse(w),sk_c10)** equal(inverse(x),sk_c10)** equal(u,sk_c10) equal(v,sk_c10) equal(w,sk_c10) equal(x,sk_c10) -> . % 0.52/0.74 3613[6:Con:3612.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.52/0.74 3695[6:SpL:3520.0,3613.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.52/0.74 3696[6:Obv:3695.1] || -> . % 0.52/0.74 3697[5:Spt:3696.0,39.1,2983.0] || equal(inverse(sk_c1),sk_c11)** -> . % 0.52/0.74 3698[5:Spt:3696.0,39.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.74 3701[5:MRR:34.1,3697.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.74 3706[5:MRR:33.0,3697.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.74 3773[5:SpR:3701.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.74 3777[5:Rew:2947.0,3773.0] || -> equal(sk_c4,sk_c9)**. % 0.52/0.74 3779[5:Rew:3777.0,3706.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.74 3780[5:Rew:3131.0,3779.0] || -> equal(identity,sk_c9)**. % 0.52/0.74 3781[5:Rew:3780.0,3123.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.52/0.74 3782[5:Rew:3780.0,753.0] || -> equal(multiply(u,sk_c9),u)**. % 0.52/0.74 3788[5:Rew:2954.0,3781.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.74 3789[5:Rew:3788.0,2954.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.52/0.74 3805[5:Rew:3788.0,2974.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,sk_c10),sk_c10)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** -> . % 0.52/0.74 3809[5:Rew:3788.0,3782.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.74 3811[5:Rew:3809.0,2981.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.74 3866[5:Rew:3809.0,3805.7,3811.0,3805.7,3809.0,3805.6,3788.0,3805.6,3809.0,3805.5,3811.0,3805.5,3809.0,3805.4,3811.0,3805.3,3811.0,3805.1] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10)** equal(inverse(w),sk_c10)** equal(inverse(x),sk_c10)** equal(u,sk_c10) equal(v,sk_c10) equal(w,sk_c10) equal(x,sk_c10) -> . % 0.52/0.75 3867[5:Con:3866.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.52/0.75 3932[5:SpL:3789.0,3867.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.52/0.75 3933[5:Obv:3932.1] || -> . % 0.52/0.75 3934[4:Spt:3933.0,28.1,2971.0] || equal(multiply(sk_c9,sk_c11),sk_c10)** -> . % 0.52/0.75 3935[4:Spt:3933.0,28.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.52/0.75 3937[4:MRR:24.1,3934.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.75 3943[4:MRR:23.1,3934.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.75 3999[4:SpR:3937.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.75 4003[4:Rew:2947.0,3999.0] || -> equal(sk_c4,sk_c9)**. % 0.52/0.75 4005[4:Rew:4003.0,3943.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.75 4006[4:Rew:3131.0,4005.0] || -> equal(identity,sk_c9)**. % 0.52/0.75 4007[4:Rew:4006.0,3123.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.52/0.75 4010[4:Rew:4006.0,72.0] || -> equal(multiply(sk_c9,u),u)**. % 0.52/0.75 4011[4:Rew:4006.0,753.0] || -> equal(multiply(u,sk_c9),u)**. % 0.52/0.75 4014[4:Rew:2954.0,4007.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.75 4017[4:Rew:4014.0,2958.0] || -> equal(multiply(sk_c10,sk_c11),sk_c10)**. % 0.52/0.75 4019[4:Rew:4014.0,3934.0] || equal(multiply(sk_c10,sk_c11),sk_c10)** -> . % 0.52/0.75 4033[4:Rew:4014.0,4010.0] || -> equal(multiply(sk_c10,u),u)**. % 0.52/0.75 4035[4:Rew:4014.0,4011.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.75 4048[4:Rew:4033.0,4017.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.75 4065[4:Rew:4035.0,4019.0,4048.0,4019.0] || equal(sk_c10,sk_c10)* -> . % 0.52/0.75 4066[4:Obv:4065.0] || -> . % 0.52/0.75 4087[3:Spt:4066.0,9.1,2958.0] || equal(multiply(sk_c10,sk_c11),sk_c9)** -> . % 0.52/0.75 4088[3:Spt:4066.0,9.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.75 4090[3:MRR:6.1,4087.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.52/0.75 4091[3:MRR:4.1,4087.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.75 4092[3:MRR:2.1,4087.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.52/0.75 4094[3:MRR:7.1,4087.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.52/0.75 4095[3:MRR:5.1,4087.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.52/0.75 4096[3:MRR:3.1,4087.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.75 4097[3:MRR:1.1,4087.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.52/0.75 4100[3:SpR:4088.0,773.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.52/0.75 4142[3:SpR:4090.0,773.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.75 4146[3:Rew:4100.0,4142.0] || -> equal(sk_c6,sk_c5)**. % 0.52/0.75 4148[3:Rew:4146.0,4100.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.75 4159[3:SpR:4091.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.75 4163[3:Rew:2947.0,4159.0] || -> equal(sk_c4,sk_c9)**. % 0.52/0.75 4165[3:Rew:4163.0,4096.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.52/0.75 4166[3:Rew:3131.0,4165.0] || -> equal(identity,sk_c9)**. % 0.52/0.75 4167[3:Rew:4166.0,3123.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.52/0.75 4168[3:Rew:4166.0,753.0] || -> equal(multiply(u,sk_c9),u)**. % 0.52/0.75 4169[3:Rew:4166.0,72.0] || -> equal(multiply(sk_c9,u),u)**. % 0.52/0.75 4174[3:Rew:2954.0,4167.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.75 4177[3:Rew:4174.0,4087.0] || equal(multiply(sk_c10,sk_c11),sk_c10)** -> . % 0.52/0.75 4186[3:Rew:4174.0,4168.0] || -> equal(multiply(u,sk_c10),u)**. % 0.52/0.75 4187[3:Rew:4186.0,4094.0] || -> equal(sk_c8,sk_c11)**. % 0.52/0.75 4190[3:Rew:4187.0,4095.0] || -> equal(multiply(sk_c5,sk_c11),sk_c11)**. % 0.52/0.75 4191[3:Rew:4187.0,4148.0] || -> equal(inverse(sk_c11),sk_c5)**. % 0.52/0.75 4199[3:Rew:4174.0,4169.0] || -> equal(multiply(sk_c10,u),u)**. % 0.52/0.75 4202[3:Rew:4199.0,4177.0] || equal(sk_c11,sk_c10)** -> . % 0.52/0.75 4219[3:SpR:4092.0,773.0] || -> equal(inverse(sk_c11),sk_c3)**. % 0.52/0.75 4223[3:Rew:4191.0,4219.0] || -> equal(sk_c5,sk_c3)**. % 0.52/0.75 4227[3:Rew:4223.0,4190.0] || -> equal(multiply(sk_c3,sk_c11),sk_c11)**. % 0.52/0.75 4235[3:Rew:4097.0,4227.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.75 4236[3:MRR:4235.0,4202.0] || -> . % 0.52/0.75 4237[2:Spt:4236.0,18.1,2947.0] || equal(inverse(sk_c10),sk_c9)** -> . % 0.52/0.75 4238[2:Spt:4236.0,18.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.52/0.75 4239[2:MRR:16.1,4237.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.52/0.75 4240[2:MRR:14.1,4237.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.52/0.75 4241[2:MRR:12.1,4237.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.52/0.75 4242[2:MRR:19.1,4237.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.52/0.75 4243[2:MRR:20.0,4237.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.52/0.75 4244[2:MRR:17.0,4237.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.52/0.75 4245[2:MRR:15.0,4237.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.52/0.75 4246[2:MRR:13.0,4237.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.52/0.75 4247[2:MRR:11.0,4237.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.52/0.75 4250[2:SpR:4238.0,773.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.52/0.75 4254[2:Rew:4242.0,4250.0] || -> equal(sk_c7,sk_c8)**. % 0.52/0.75 4255[2:Rew:4254.0,4238.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.52/0.75 4256[2:Rew:4254.0,4243.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.52/0.75 4273[2:SpR:4239.0,280.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.52/0.75 4274[2:SpR:4239.0,773.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.75 4278[2:Rew:4255.0,4274.0] || -> equal(sk_c6,sk_c5)**. % 0.52/0.75 4280[2:Rew:4278.0,4255.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.52/0.75 4281[2:Rew:4278.0,4256.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.52/0.75 4289[2:SpR:4240.0,773.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.52/0.75 4293[2:Rew:4289.0,4237.0] || equal(sk_c4,sk_c9)** -> . % 0.52/0.75 4294[2:SpR:4241.0,127.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.52/0.75 4296[2:SpR:4241.0,773.0] || -> equal(inverse(sk_c11),sk_c3)**. % 0.52/0.75 4327[2:SpR:4245.0,74.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.52/0.75 4328[2:SpR:4245.0,127.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.52/0.75 4332[2:Rew:4239.0,4328.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.52/0.75 4333[2:Rew:4273.0,4327.0] || -> equal(multiply(sk_c11,u),u)**. % 0.52/0.75 4335[2:Rew:4333.0,4294.0] || -> equal(multiply(sk_c3,u),u)**. % 0.52/0.75 4340[2:Rew:4335.0,4247.0] || -> equal(sk_c11,sk_c10)**. % 0.52/0.75 4344[2:Rew:4340.0,4244.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)**. % 0.52/0.75 4345[2:Rew:4340.0,4296.0] || -> equal(inverse(sk_c10),sk_c3)**. % 0.52/0.75 4348[2:Rew:4340.0,4332.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.52/0.75 4349[2:Rew:4340.0,4333.0] || -> equal(multiply(sk_c10,u),u)**. % 0.52/0.75 4350[2:Rew:4289.0,4345.0] || -> equal(sk_c4,sk_c3)**. % 0.52/0.75 4352[2:Rew:4350.0,4289.0] || -> equal(inverse(sk_c10),sk_c3)**. % 0.52/0.75 4353[2:Rew:4350.0,4293.0] || equal(sk_c3,sk_c9)** -> . % 0.52/0.75 4354[2:Rew:4350.0,4246.0] || -> equal(multiply(sk_c3,sk_c10),sk_c9)**. % 0.52/0.75 4361[2:Rew:4344.0,4348.0] || -> equal(sk_c8,sk_c10)**. % 0.52/0.75 4364[2:Rew:4361.0,4280.0] || -> equal(inverse(sk_c10),sk_c5)**. % 0.52/0.75 4365[2:Rew:4361.0,4281.0] || -> equal(multiply(sk_c10,sk_c10),sk_c5)**. % 0.52/0.75 4374[2:Rew:4352.0,4364.0] || -> equal(sk_c5,sk_c3)**. % 0.52/0.75 4378[2:Rew:4335.0,4354.0] || -> equal(sk_c9,sk_c10)**. % 0.52/0.75 4379[2:Rew:4378.0,4353.0] || equal(sk_c3,sk_c10)** -> . % 0.52/0.75 4380[2:Rew:4349.0,4365.0,4374.0,4365.0] || -> equal(sk_c3,sk_c10)**. % 0.52/0.75 4381[2:MRR:4380.0,4379.0] || -> . % 0.52/0.75 % SZS output end Refutation % 0.52/0.75 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 prove_this_5 prove_this_6 prove_this_7 prove_this_9 prove_this_11 prove_this_12 prove_this_13 prove_this_14 prove_this_15 prove_this_16 prove_this_17 prove_this_18 prove_this_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_25 prove_this_26 prove_this_27 prove_this_28 prove_this_29 prove_this_33 prove_this_34 prove_this_39 prove_this_53 prove_this_54 prove_this_59 prove_this_61 prove_this_62 prove_this_65 prove_this_66 prove_this_68 prove_this_69 prove_this_71 left_identity left_inverse associativity % 0.52/0.75 %------------------------------------------------------------------------------