%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP373-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n024.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:47:05 EDT 2022 % Result : Unsatisfiable 0.38s 0.56s % Output : Refutation 0.38s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : GRP373-1 : TPTP v8.1.0. Released v2.5.0. % 0.08/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n024.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Tue Jun 14 07:52:33 EDT 2022 % 0.12/0.35 % CPUTime : % 0.38/0.56 % 0.38/0.56 SPASS V 3.9 % 0.38/0.56 SPASS beiseite: Proof found. % 0.38/0.56 % SZS status Theorem % 0.38/0.56 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.38/0.56 SPASS derived 1476 clauses, backtracked 660 clauses, performed 12 splits and kept 1134 clauses. % 0.38/0.56 SPASS allocated 64211 KBytes. % 0.38/0.56 SPASS spent 0:00:00.21 on the problem. % 0.38/0.56 0:00:00.04 for the input. % 0.38/0.56 0:00:00.00 for the FLOTTER CNF translation. % 0.38/0.56 0:00:00.01 for inferences. % 0.38/0.56 0:00:00.00 for the backtracking. % 0.38/0.56 0:00:00.13 for the reduction. % 0.38/0.56 % 0.38/0.56 % 0.38/0.56 Here is a proof with depth 5, length 375 : % 0.38/0.56 % SZS output start Refutation % 0.38/0.56 1[0:Inp] || -> equal(inverse(sk_c11),sk_c10) equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.56 2[0:Inp] || -> equal(inverse(sk_c3),sk_c11)** equal(inverse(sk_c11),sk_c10). % 0.38/0.56 5[0:Inp] || -> equal(inverse(sk_c11),sk_c10) equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 6[0:Inp] || -> equal(inverse(sk_c5),sk_c8)** equal(inverse(sk_c11),sk_c10). % 0.38/0.56 7[0:Inp] || -> equal(inverse(sk_c11),sk_c10) equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.38/0.56 8[0:Inp] || -> equal(inverse(sk_c7),sk_c6)** equal(inverse(sk_c11),sk_c10). % 0.38/0.56 9[0:Inp] || -> equal(inverse(sk_c6),sk_c8)** equal(inverse(sk_c11),sk_c10). % 0.38/0.56 10[0:Inp] || -> equal(inverse(sk_c11),sk_c10) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.38/0.56 15[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11) equal(multiply(sk_c1,sk_c11),sk_c10)**. % 0.38/0.56 16[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c1,sk_c11),sk_c10)**. % 0.38/0.56 17[0:Inp] || -> equal(multiply(sk_c8,sk_c10),sk_c11) equal(multiply(sk_c1,sk_c11),sk_c10)**. % 0.38/0.56 18[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c1,sk_c11),sk_c10)**. % 0.38/0.56 19[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c1,sk_c11),sk_c10)**. % 0.38/0.56 20[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c6) equal(multiply(sk_c1,sk_c11),sk_c10)**. % 0.38/0.56 21[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.56 22[0:Inp] || -> equal(inverse(sk_c3),sk_c11) equal(inverse(sk_c1),sk_c11)**. % 0.38/0.56 25[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 26[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c1),sk_c11)**. % 0.38/0.56 29[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(inverse(sk_c1),sk_c11)**. % 0.38/0.56 31[0:Inp] || -> equal(multiply(sk_c3,sk_c11),sk_c10)** equal(multiply(sk_c11,sk_c9),sk_c10). % 0.38/0.56 32[0:Inp] || -> equal(inverse(sk_c3),sk_c11) equal(multiply(sk_c11,sk_c9),sk_c10)**. % 0.38/0.56 33[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(multiply(sk_c11,sk_c9),sk_c10). % 0.38/0.56 34[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c11,sk_c9),sk_c10)**. % 0.38/0.56 35[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11)** equal(multiply(sk_c11,sk_c9),sk_c10). % 0.38/0.56 36[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c11,sk_c9),sk_c10)**. % 0.38/0.56 38[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c11,sk_c9),sk_c10)**. % 0.38/0.56 39[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c11,sk_c9),sk_c10)**. % 0.38/0.56 41[0:Inp] || -> equal(multiply(sk_c3,sk_c11),sk_c10) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.38/0.56 42[0:Inp] || -> equal(inverse(sk_c3),sk_c11) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.38/0.56 45[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.38/0.56 46[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.38/0.56 49[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.38/0.56 51[0:Inp] || -> equal(inverse(sk_c2),sk_c9) equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.56 52[0:Inp] || -> equal(inverse(sk_c3),sk_c11) equal(inverse(sk_c2),sk_c9)**. % 0.38/0.56 55[0:Inp] || -> equal(inverse(sk_c2),sk_c9) equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 56[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c2),sk_c9)**. % 0.38/0.56 59[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(inverse(sk_c2),sk_c9)**. % 0.38/0.56 61[0:Inp] || equal(inverse(sk_c11),sk_c10) equal(multiply(u,sk_c11),sk_c10)** equal(inverse(u),sk_c11) equal(multiply(sk_c11,sk_c9),sk_c10)** equal(multiply(v,sk_c9),sk_c10)** equal(inverse(v),sk_c9) equal(multiply(w,sk_c11),sk_c10)** equal(inverse(w),sk_c11) equal(multiply(x,sk_c10),sk_c9)** equal(inverse(x),sk_c10) equal(multiply(y,z),sk_c11)** equal(inverse(y),z) equal(multiply(z,sk_c10),sk_c11)** equal(inverse(x1),x2) equal(inverse(x2),z)* equal(multiply(x1,z),x2)* -> . % 0.38/0.56 62[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.38/0.56 63[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.38/0.56 64[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.38/0.56 65[0:Con:61.6] || equal(inverse(u),v)* equal(inverse(w),u) equal(inverse(x),v) equal(inverse(y),sk_c10) equal(inverse(z),sk_c9) equal(inverse(x1),sk_c11) equal(inverse(sk_c11),sk_c10) 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_c9),sk_c10)** equal(multiply(x1,sk_c11),sk_c10)** equal(multiply(sk_c11,sk_c9),sk_c10)** -> . % 0.38/0.56 66[1:Spt:65.0,65.1,65.2,65.7,65.8,65.9] || 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.38/0.56 68[2:Spt:9.1] || -> equal(inverse(sk_c11),sk_c10)**. % 0.38/0.56 70[3:Spt:39.1] || -> equal(multiply(sk_c11,sk_c9),sk_c10)**. % 0.38/0.56 72[3:SpL:70.0,66.3] || equal(inverse(u),sk_c9)** equal(inverse(sk_c11),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.38/0.56 73[3:Rew:68.0,72.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.38/0.56 74[3:Obv:73.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.38/0.56 75[4:Spt:59.1] || -> equal(inverse(sk_c2),sk_c9)**. % 0.38/0.56 77[5:Spt:29.1] || -> equal(inverse(sk_c1),sk_c11)**. % 0.38/0.56 79[6:Spt:49.1] || -> equal(multiply(sk_c2,sk_c9),sk_c10)**. % 0.38/0.56 84[7:Spt:19.1] || -> equal(multiply(sk_c1,sk_c11),sk_c10)**. % 0.38/0.56 89[2:SpR:68.0,63.0] || -> equal(multiply(sk_c10,sk_c11),identity)**. % 0.38/0.56 90[4:SpR:75.0,63.0] || -> equal(multiply(sk_c9,sk_c2),identity)**. % 0.38/0.56 91[5:SpR:77.0,63.0] || -> equal(multiply(sk_c11,sk_c1),identity)**. % 0.38/0.56 100[6:SpR:79.0,64.0] || -> equal(multiply(sk_c2,multiply(sk_c9,u)),multiply(sk_c10,u))**. % 0.38/0.56 102[0:SpR:63.0,64.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.38/0.56 104[2:SpR:89.0,64.0] || -> equal(multiply(sk_c10,multiply(sk_c11,u)),multiply(identity,u))**. % 0.38/0.56 107[2:Rew:62.0,104.0] || -> equal(multiply(sk_c10,multiply(sk_c11,u)),u)**. % 0.38/0.56 109[0:Rew:62.0,102.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.38/0.56 118[3:SpR:70.0,107.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.38/0.56 119[5:SpR:91.0,107.0] || -> equal(multiply(sk_c10,identity),sk_c1)**. % 0.38/0.56 127[5:SpR:119.0,64.0] || -> equal(multiply(sk_c10,multiply(identity,u)),multiply(sk_c1,u))**. % 0.38/0.56 130[5:Rew:62.0,127.0] || -> equal(multiply(sk_c1,u),multiply(sk_c10,u))**. % 0.38/0.56 131[7:Rew:130.0,84.0] || -> equal(multiply(sk_c10,sk_c11),sk_c10)**. % 0.38/0.56 135[7:Rew:89.0,131.0] || -> equal(identity,sk_c10)**. % 0.38/0.56 136[7:Rew:135.0,62.0] || -> equal(multiply(sk_c10,u),u)**. % 0.38/0.56 137[7:Rew:135.0,63.0] || -> equal(multiply(inverse(u),u),sk_c10)**. % 0.38/0.56 138[7:Rew:135.0,89.0] || -> equal(multiply(sk_c10,sk_c11),sk_c10)**. % 0.38/0.56 146[7:Rew:136.0,118.0] || -> equal(sk_c9,sk_c10)**. % 0.38/0.56 147[7:Rew:136.0,107.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.56 155[7:Rew:146.0,74.0] || equal(inverse(u),sk_c10)** 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.38/0.56 158[7:Rew:136.0,138.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.56 160[7:Rew:158.0,68.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.38/0.56 167[7:Rew:158.0,146.0] || -> equal(sk_c9,sk_c11)**. % 0.38/0.56 179[7:Rew:158.0,137.0] || -> equal(multiply(inverse(u),u),sk_c11)**. % 0.38/0.56 186[7:Rew:147.0,155.4,167.0,155.4,158.0,155.4,167.0,155.3,158.0,155.2,167.0,155.1,158.0,155.0] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c11) equal(sk_c11,u) equal(multiply(v,sk_c11),sk_c11)** equal(sk_c11,sk_c11) -> . % 0.38/0.56 187[7:Obv:186.4] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c11) equal(sk_c11,u) equal(multiply(v,sk_c11),sk_c11)** -> . % 0.38/0.56 215[0:SpR:109.0,109.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.38/0.56 218[7:SpR:179.0,109.0] || -> equal(multiply(inverse(inverse(u)),sk_c11),u)**. % 0.38/0.56 223[7:Rew:215.0,218.0] || -> equal(multiply(u,sk_c11),u)**. % 0.38/0.56 229[7:Rew:223.0,187.3] || equal(inverse(u),sk_c11)**+ equal(inverse(v),sk_c11)** equal(sk_c11,u) equal(v,sk_c11) -> . % 0.38/0.56 251[0:SpR:215.0,109.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.38/0.56 473[7:SpL:160.0,229.0] || equal(sk_c11,sk_c11) equal(inverse(u),sk_c11)** equal(sk_c11,sk_c11) equal(u,sk_c11) -> . % 0.38/0.56 476[7:Obv:473.2] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.38/0.56 478[7:SpL:160.0,476.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.38/0.56 481[7:Obv:478.1] || -> . % 0.38/0.56 482[7:Spt:481.0,19.1,84.0] || equal(multiply(sk_c1,sk_c11),sk_c10)** -> . % 0.38/0.56 483[7:Spt:481.0,19.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.56 484[7:Rew:130.0,482.0] || equal(multiply(sk_c10,sk_c11),sk_c10)** -> . % 0.38/0.56 485[7:Rew:89.0,484.0] || equal(identity,sk_c10)** -> . % 0.38/0.56 516[4:SpR:75.0,251.0] || -> equal(multiply(sk_c2,multiply(sk_c9,u)),u)**. % 0.38/0.56 518[6:Rew:100.0,516.0] || -> equal(multiply(sk_c10,u),u)**. % 0.38/0.56 526[6:Rew:518.0,89.0] || -> equal(identity,sk_c11)**. % 0.38/0.56 527[6:Rew:518.0,119.0] || -> equal(identity,sk_c1)**. % 0.38/0.56 541[7:Rew:526.0,485.0] || equal(sk_c10,sk_c11)** -> . % 0.38/0.56 547[6:Rew:526.0,527.0] || -> equal(sk_c1,sk_c11)**. % 0.38/0.56 548[6:Rew:547.0,77.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.38/0.56 549[6:Rew:68.0,548.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.56 550[7:MRR:549.0,541.0] || -> . % 0.38/0.56 568[6:Spt:550.0,49.1,79.0] || equal(multiply(sk_c2,sk_c9),sk_c10)** -> . % 0.38/0.56 569[6:Spt:550.0,49.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.56 575[6:MRR:46.1,568.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.56 577[6:MRR:42.1,568.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.38/0.56 585[6:MRR:45.1,568.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 587[6:MRR:41.1,568.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.56 606[6:SpR:575.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.56 611[6:SpR:577.0,109.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.38/0.56 645[6:SpR:585.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.56 649[6:Rew:606.0,645.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.56 650[6:Rew:649.0,91.0] || -> equal(identity,sk_c1)**. % 0.38/0.56 651[6:Rew:649.0,70.0] || -> equal(sk_c9,sk_c10)**. % 0.38/0.56 654[6:Rew:649.0,611.0] || -> equal(multiply(sk_c3,u),u)**. % 0.38/0.56 661[6:Rew:650.0,89.0] || -> equal(multiply(sk_c10,sk_c11),sk_c1)**. % 0.38/0.56 662[6:Rew:650.0,90.0] || -> equal(multiply(sk_c9,sk_c2),sk_c1)**. % 0.38/0.56 676[6:Rew:651.0,568.0] || equal(multiply(sk_c2,sk_c10),sk_c10)** -> . % 0.38/0.56 684[6:Rew:654.0,587.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.56 695[6:Rew:684.0,651.0] || -> equal(sk_c9,sk_c11)**. % 0.38/0.56 700[6:Rew:649.0,661.0,684.0,661.0] || -> equal(sk_c1,sk_c11)**. % 0.38/0.56 703[6:Rew:649.0,662.0,695.0,662.0,700.0,662.0] || -> equal(sk_c2,sk_c11)**. % 0.38/0.56 725[6:Rew:649.0,676.0,703.0,676.0,684.0,676.0] || equal(sk_c11,sk_c11)* -> . % 0.38/0.56 726[6:Obv:725.0] || -> . % 0.38/0.56 764[5:Spt:726.0,29.1,77.0] || equal(inverse(sk_c1),sk_c11)** -> . % 0.38/0.56 765[5:Spt:726.0,29.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.56 767[5:MRR:26.1,764.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.56 769[5:MRR:22.1,764.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.38/0.56 772[5:MRR:25.0,764.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 774[5:MRR:21.0,764.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.56 788[5:SpR:767.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.56 793[5:SpR:769.0,109.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.38/0.56 818[5:SpR:772.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.56 822[5:Rew:788.0,818.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.56 823[5:Rew:822.0,70.0] || -> equal(sk_c9,sk_c10)**. % 0.38/0.56 825[5:Rew:822.0,793.0] || -> equal(multiply(sk_c3,u),u)**. % 0.38/0.56 833[5:Rew:823.0,90.0] || -> equal(multiply(sk_c10,sk_c2),identity)**. % 0.38/0.56 842[5:Rew:823.0,74.0] || equal(inverse(u),sk_c10)** 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.38/0.56 844[5:Rew:825.0,774.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.56 845[5:Rew:844.0,68.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.38/0.56 847[5:Rew:844.0,89.0] || -> equal(multiply(sk_c11,sk_c11),identity)**. % 0.38/0.56 858[5:Rew:844.0,823.0] || -> equal(sk_c9,sk_c11)**. % 0.38/0.56 862[5:Rew:822.0,833.0,844.0,833.0] || -> equal(identity,sk_c2)**. % 0.38/0.56 864[5:Rew:862.0,63.0] || -> equal(multiply(inverse(u),u),sk_c2)**. % 0.38/0.56 868[5:Rew:822.0,847.0,862.0,847.0] || -> equal(sk_c2,sk_c11)**. % 0.38/0.56 888[5:Rew:868.0,864.0] || -> equal(multiply(inverse(u),u),sk_c11)**. % 0.38/0.56 909[5:Rew:822.0,842.4,858.0,842.4,844.0,842.4,858.0,842.3,844.0,842.2,858.0,842.1,844.0,842.0] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c11) equal(sk_c11,u) equal(multiply(v,sk_c11),sk_c11)** equal(sk_c11,sk_c11) -> . % 0.38/0.56 910[5:Obv:909.4] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c11) equal(sk_c11,u) equal(multiply(v,sk_c11),sk_c11)** -> . % 0.38/0.56 960[5:SpR:888.0,251.0] || -> equal(multiply(u,sk_c11),u)**. % 0.38/0.56 972[5:Rew:960.0,910.3] || equal(inverse(u),sk_c11)**+ equal(inverse(v),sk_c11)** equal(sk_c11,u) equal(v,sk_c11) -> . % 0.38/0.56 1072[5:SpL:845.0,972.0] || equal(sk_c11,sk_c11) equal(inverse(u),sk_c11)** equal(sk_c11,sk_c11) equal(u,sk_c11) -> . % 0.38/0.56 1074[5:Obv:1072.2] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.38/0.56 1076[5:SpL:845.0,1074.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.38/0.56 1078[5:Obv:1076.1] || -> . % 0.38/0.56 1079[4:Spt:1078.0,59.1,75.0] || equal(inverse(sk_c2),sk_c9)** -> . % 0.38/0.56 1080[4:Spt:1078.0,59.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.56 1082[4:MRR:56.1,1079.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.56 1084[4:MRR:52.1,1079.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.38/0.56 1087[4:MRR:55.0,1079.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 1089[4:MRR:51.0,1079.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.56 1100[4:SpR:1082.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.56 1105[4:SpR:1084.0,109.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.38/0.56 1126[4:SpR:1087.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.56 1130[4:Rew:1100.0,1126.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.56 1131[4:Rew:1130.0,70.0] || -> equal(sk_c9,sk_c10)**. % 0.38/0.56 1133[4:Rew:1130.0,1105.0] || -> equal(multiply(sk_c3,u),u)**. % 0.38/0.56 1145[4:Rew:1131.0,74.0] || equal(inverse(u),sk_c10)** 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.38/0.56 1147[4:Rew:1133.0,1089.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.56 1148[4:Rew:1147.0,68.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.38/0.56 1150[4:Rew:1147.0,89.0] || -> equal(multiply(sk_c11,sk_c11),identity)**. % 0.38/0.56 1161[4:Rew:1147.0,1131.0] || -> equal(sk_c9,sk_c11)**. % 0.38/0.56 1167[4:Rew:1130.0,1150.0] || -> equal(identity,sk_c11)**. % 0.38/0.56 1170[4:Rew:1167.0,63.0] || -> equal(multiply(inverse(u),u),sk_c11)**. % 0.38/0.56 1204[4:Rew:1130.0,1145.4,1161.0,1145.4,1147.0,1145.4,1161.0,1145.3,1147.0,1145.2,1161.0,1145.1,1147.0,1145.0] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c11) equal(sk_c11,u) equal(multiply(v,sk_c11),sk_c11)** equal(sk_c11,sk_c11) -> . % 0.38/0.56 1205[4:Obv:1204.4] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c11) equal(sk_c11,u) equal(multiply(v,sk_c11),sk_c11)** -> . % 0.38/0.56 1246[4:SpR:1170.0,251.0] || -> equal(multiply(u,sk_c11),u)**. % 0.38/0.56 1258[4:Rew:1246.0,1205.3] || equal(inverse(u),sk_c11)**+ equal(inverse(v),sk_c11)** equal(sk_c11,u) equal(v,sk_c11) -> . % 0.38/0.56 1358[4:SpL:1148.0,1258.0] || equal(sk_c11,sk_c11) equal(inverse(u),sk_c11)** equal(sk_c11,sk_c11) equal(u,sk_c11) -> . % 0.38/0.56 1360[4:Obv:1358.2] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.38/0.56 1362[4:SpL:1148.0,1360.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.38/0.56 1364[4:Obv:1362.1] || -> . % 0.38/0.56 1365[3:Spt:1364.0,39.1,70.0] || equal(multiply(sk_c11,sk_c9),sk_c10)** -> . % 0.38/0.56 1366[3:Spt:1364.0,39.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.56 1368[3:MRR:36.1,1365.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.56 1369[3:MRR:34.1,1365.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.38/0.56 1370[3:MRR:32.1,1365.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.38/0.56 1373[3:MRR:35.1,1365.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 1374[3:MRR:33.1,1365.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.38/0.56 1375[3:MRR:31.1,1365.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.56 1386[3:SpR:1368.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.56 1389[3:SpR:1369.0,251.0] || -> equal(multiply(sk_c4,multiply(sk_c10,u)),u)**. % 0.38/0.56 1391[3:SpR:1370.0,109.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.38/0.56 1405[3:SpR:1373.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.56 1409[3:Rew:1386.0,1405.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.56 1411[3:Rew:1409.0,1365.0] || equal(sk_c9,sk_c10)** -> . % 0.38/0.56 1412[3:Rew:1409.0,1391.0] || -> equal(multiply(sk_c3,u),u)**. % 0.38/0.56 1418[3:Rew:1412.0,1375.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.56 1424[3:Rew:1418.0,1389.0] || -> equal(multiply(sk_c4,multiply(sk_c11,u)),u)**. % 0.38/0.56 1425[3:Rew:1418.0,1374.0] || -> equal(multiply(sk_c4,sk_c11),sk_c9)**. % 0.38/0.56 1433[3:Rew:1418.0,1411.0] || equal(sk_c9,sk_c11)** -> . % 0.38/0.56 1456[3:Rew:1409.0,1424.0] || -> equal(multiply(sk_c4,u),u)**. % 0.38/0.56 1457[3:Rew:1456.0,1425.0] || -> equal(sk_c9,sk_c11)**. % 0.38/0.56 1458[3:MRR:1457.0,1433.0] || -> . % 0.38/0.56 1477[2:Spt:1458.0,9.1,68.0] || equal(inverse(sk_c11),sk_c10)** -> . % 0.38/0.56 1478[2:Spt:1458.0,9.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.56 1479[2:MRR:8.1,1477.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.38/0.56 1480[2:MRR:6.1,1477.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.56 1482[2:MRR:2.1,1477.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.38/0.56 1483[2:MRR:10.0,1477.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.38/0.56 1484[2:MRR:7.0,1477.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.38/0.56 1485[2:MRR:5.0,1477.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 1487[2:MRR:1.0,1477.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.56 1488[2:SpR:1478.0,109.0] || -> equal(multiply(sk_c8,multiply(sk_c6,u)),u)**. % 0.38/0.56 1495[2:SpR:1480.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.56 1500[2:SpR:1482.0,109.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.38/0.56 1504[2:SpR:1483.0,109.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.38/0.56 1506[2:Rew:1479.0,1504.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.38/0.56 1510[2:SpR:1485.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.56 1511[2:SpR:1485.0,109.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.38/0.56 1513[2:Rew:1480.0,1511.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.38/0.56 1514[2:Rew:1495.0,1510.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.56 1515[2:Rew:1514.0,1500.0] || -> equal(multiply(sk_c3,u),u)**. % 0.38/0.56 1518[2:Rew:1515.0,1487.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.56 1520[2:Rew:1518.0,1477.0] || equal(inverse(sk_c11),sk_c11)** -> . % 0.38/0.56 1521[2:Rew:1518.0,1484.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.38/0.56 1531[2:Rew:1513.0,1521.0] || -> equal(sk_c8,sk_c11)**. % 0.38/0.56 1532[2:Rew:1531.0,1478.0] || -> equal(inverse(sk_c6),sk_c11)**. % 0.38/0.56 1536[2:Rew:1531.0,1488.0] || -> equal(multiply(sk_c11,multiply(sk_c6,u)),u)**. % 0.38/0.56 1541[2:Rew:1531.0,1506.0] || -> equal(multiply(sk_c6,sk_c6),sk_c11)**. % 0.38/0.56 1551[2:Rew:1514.0,1536.0] || -> equal(multiply(sk_c6,u),u)**. % 0.38/0.56 1552[2:Rew:1551.0,1541.0] || -> equal(sk_c6,sk_c11)**. % 0.38/0.56 1556[2:Rew:1552.0,1532.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.38/0.56 1559[2:MRR:1556.0,1520.0] || -> . % 0.38/0.56 1566[1:Spt:1559.0,65.3,65.4,65.5,65.6,65.10,65.11,65.12,65.13] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c9) equal(inverse(w),sk_c11) equal(inverse(sk_c11),sk_c10) equal(multiply(u,sk_c10),sk_c9)**+ equal(multiply(v,sk_c9),sk_c10)** equal(multiply(w,sk_c11),sk_c10)** equal(multiply(sk_c11,sk_c9),sk_c10)** -> . % 0.38/0.56 1568[2:Spt:8.1] || -> equal(inverse(sk_c11),sk_c10)**. % 0.38/0.56 1569[2:Rew:1568.0,1566.3] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c9) equal(inverse(w),sk_c11) equal(sk_c10,sk_c10) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c9),sk_c10)** equal(multiply(w,sk_c11),sk_c10)** equal(multiply(sk_c11,sk_c9),sk_c10)** -> . % 0.38/0.56 1571[2:Obv:1569.3] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c9) equal(inverse(w),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c9),sk_c10)** equal(multiply(w,sk_c11),sk_c10)** equal(multiply(sk_c11,sk_c9),sk_c10)** -> . % 0.38/0.56 1573[2:SpR:1568.0,109.0] || -> equal(multiply(sk_c10,multiply(sk_c11,u)),u)**. % 0.38/0.56 1576[3:Spt:38.1] || -> equal(multiply(sk_c11,sk_c9),sk_c10)**. % 0.38/0.56 1578[3:Rew:1576.0,1571.6] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c9) equal(inverse(w),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c9),sk_c10)** equal(multiply(w,sk_c11),sk_c10)** equal(sk_c10,sk_c10) -> . % 0.38/0.56 1579[3:Obv:1578.6] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c9) equal(inverse(w),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c9),sk_c10)** equal(multiply(w,sk_c11),sk_c10)** -> . % 0.38/0.56 1582[3:SpR:1576.0,109.0] || -> equal(multiply(inverse(sk_c11),sk_c10),sk_c9)**. % 0.38/0.56 1584[3:Rew:1568.0,1582.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.38/0.56 1585[4:Spt:29.1] || -> equal(inverse(sk_c1),sk_c11)**. % 0.38/0.56 1587[4:SpR:1585.0,251.0] || -> equal(multiply(sk_c1,multiply(sk_c11,u)),u)**. % 0.38/0.56 1593[5:Spt:19.1] || -> equal(multiply(sk_c1,sk_c11),sk_c10)**. % 0.38/0.56 1594[5:SpR:1593.0,64.0] || -> equal(multiply(sk_c1,multiply(sk_c11,u)),multiply(sk_c10,u))**. % 0.38/0.56 1595[5:SpR:1593.0,109.0] || -> equal(multiply(inverse(sk_c1),sk_c10),sk_c11)**. % 0.38/0.56 1597[5:Rew:1585.0,1595.0] || -> equal(multiply(sk_c11,sk_c10),sk_c11)**. % 0.38/0.56 1598[5:Rew:1587.0,1594.0] || -> equal(multiply(sk_c10,u),u)**. % 0.38/0.56 1599[5:Rew:1598.0,1584.0] || -> equal(sk_c9,sk_c10)**. % 0.38/0.56 1600[5:Rew:1598.0,1573.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.56 1615[5:Rew:1599.0,1579.1] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c9),sk_c10)** equal(multiply(w,sk_c11),sk_c10)** -> . % 0.38/0.56 1619[5:Rew:1600.0,1597.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.56 1622[5:Rew:1619.0,1568.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.38/0.56 1625[5:Rew:1619.0,1599.0] || -> equal(sk_c9,sk_c11)**. % 0.38/0.56 1630[5:Rew:1619.0,1615.5,1625.0,1615.4,1619.0,1615.4,1619.0,1615.3,1625.0,1615.3,1619.0,1615.1,1619.0,1615.0] || equal(inverse(u),sk_c11) equal(inverse(v),sk_c11) equal(inverse(w),sk_c11) equal(multiply(u,sk_c11),sk_c11)** equal(multiply(v,sk_c11),sk_c11)** equal(multiply(w,sk_c11),sk_c11)** -> . % 0.38/0.56 1631[5:Con:1630.1] || equal(inverse(u),sk_c11) equal(multiply(u,sk_c11),sk_c11)** -> . % 0.38/0.56 1657[0:SpR:63.0,109.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.38/0.56 1658[0:SpR:63.0,251.0] || -> equal(multiply(u,identity),u)**. % 0.38/0.56 1660[4:SpR:1585.0,63.0] || -> equal(multiply(sk_c11,sk_c1),identity)**. % 0.38/0.56 1661[5:SpR:1622.0,63.0] || -> equal(multiply(sk_c11,sk_c11),identity)**. % 0.38/0.56 1663[5:Rew:1600.0,1660.0] || -> equal(identity,sk_c1)**. % 0.38/0.56 1667[5:Rew:1663.0,1658.0] || -> equal(multiply(u,sk_c1),u)**. % 0.38/0.56 1668[5:Rew:1600.0,1661.0] || -> equal(identity,sk_c11)**. % 0.38/0.56 1669[5:Rew:1663.0,1668.0] || -> equal(sk_c1,sk_c11)**. % 0.38/0.56 1678[5:Rew:1669.0,1667.0] || -> equal(multiply(u,sk_c11),u)**. % 0.38/0.56 1679[5:Rew:1678.0,1631.1] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.38/0.56 1724[5:SpL:1622.0,1679.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.38/0.56 1726[5:Obv:1724.1] || -> . % 0.38/0.56 1727[5:Spt:1726.0,19.1,1593.0] || equal(multiply(sk_c1,sk_c11),sk_c10)** -> . % 0.38/0.56 1728[5:Spt:1726.0,19.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.56 1729[0:Rew:1658.0,1657.0] || -> equal(inverse(inverse(u)),u)**. % 0.38/0.56 1730[5:MRR:18.1,1727.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.38/0.56 1731[5:MRR:16.1,1727.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.56 1735[5:MRR:20.1,1727.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.38/0.56 1736[5:MRR:17.1,1727.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.38/0.56 1737[5:MRR:15.1,1727.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.56 1741[5:SpR:1728.0,109.0] || -> equal(multiply(sk_c8,multiply(sk_c6,u)),u)**. % 0.38/0.56 1757[5:SpR:1731.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.56 1773[4:SpR:1660.0,109.0] || -> equal(multiply(inverse(sk_c11),identity),sk_c1)**. % 0.38/0.56 1775[4:Rew:1568.0,1773.0] || -> equal(multiply(sk_c10,identity),sk_c1)**. % 0.38/0.56 1776[4:Rew:1658.0,1775.0] || -> equal(sk_c1,sk_c10)**. % 0.38/0.56 1778[4:Rew:1776.0,1660.0] || -> equal(multiply(sk_c11,sk_c10),identity)**. % 0.38/0.56 1779[5:Rew:1776.0,1727.0] || equal(multiply(sk_c10,sk_c11),sk_c10)** -> . % 0.38/0.56 1786[5:SpR:1735.0,109.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.38/0.56 1788[5:Rew:1730.0,1786.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.38/0.56 1795[5:SpR:1737.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.56 1799[5:Rew:1757.0,1795.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.56 1801[5:Rew:1799.0,1778.0] || -> equal(identity,sk_c10)**. % 0.38/0.56 1802[5:Rew:1799.0,1573.0] || -> equal(multiply(sk_c10,u),u)**. % 0.38/0.56 1817[5:Rew:1801.0,1658.0] || -> equal(multiply(u,sk_c10),u)**. % 0.38/0.56 1820[5:Rew:1802.0,1779.0] || equal(sk_c10,sk_c11)** -> . % 0.38/0.56 1825[5:Rew:1817.0,1736.0] || -> equal(sk_c8,sk_c11)**. % 0.38/0.56 1827[5:Rew:1825.0,1728.0] || -> equal(inverse(sk_c6),sk_c11)**. % 0.38/0.56 1831[5:Rew:1825.0,1741.0] || -> equal(multiply(sk_c11,multiply(sk_c6,u)),u)**. % 0.38/0.57 1836[5:Rew:1825.0,1788.0] || -> equal(multiply(sk_c6,sk_c6),sk_c11)**. % 0.38/0.57 1849[5:Rew:1799.0,1831.0] || -> equal(multiply(sk_c6,u),u)**. % 0.38/0.57 1850[5:Rew:1849.0,1836.0] || -> equal(sk_c6,sk_c11)**. % 0.38/0.57 1854[5:Rew:1850.0,1827.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.38/0.57 1857[5:Rew:1568.0,1854.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.57 1858[5:MRR:1857.0,1820.0] || -> . % 0.38/0.57 1867[4:Spt:1858.0,29.1,1585.0] || equal(inverse(sk_c1),sk_c11)** -> . % 0.38/0.57 1868[4:Spt:1858.0,29.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.57 1870[4:MRR:26.1,1867.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.57 1872[4:MRR:22.1,1867.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.38/0.57 1875[4:MRR:25.0,1867.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.57 1877[4:MRR:21.0,1867.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.57 1885[4:SpR:1870.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.57 1890[4:SpR:1872.0,109.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.38/0.57 1907[4:SpR:1875.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.57 1911[4:Rew:1885.0,1907.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.57 1912[4:Rew:1911.0,1576.0] || -> equal(sk_c9,sk_c10)**. % 0.38/0.57 1913[4:Rew:1911.0,1890.0] || -> equal(multiply(sk_c3,u),u)**. % 0.38/0.57 1923[4:Rew:1912.0,1579.1] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c11) equal(multiply(u,sk_c10),sk_c9)** equal(multiply(v,sk_c9),sk_c10)** equal(multiply(w,sk_c11),sk_c10)** -> . % 0.38/0.57 1925[4:Rew:1913.0,1877.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.57 1926[4:Rew:1925.0,1568.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.38/0.57 1932[4:Rew:1925.0,1912.0] || -> equal(sk_c9,sk_c11)**. % 0.38/0.57 1968[4:Rew:1925.0,1923.5,1932.0,1923.4,1925.0,1923.4,1925.0,1923.3,1932.0,1923.3,1925.0,1923.1,1925.0,1923.0] || equal(inverse(u),sk_c11) equal(inverse(v),sk_c11) equal(inverse(w),sk_c11) equal(multiply(u,sk_c11),sk_c11)** equal(multiply(v,sk_c11),sk_c11)** equal(multiply(w,sk_c11),sk_c11)** -> . % 0.38/0.57 1969[4:Con:1968.1] || equal(inverse(u),sk_c11) equal(multiply(u,sk_c11),sk_c11)** -> . % 0.38/0.57 2036[4:SpR:1911.0,1658.0] || -> equal(identity,sk_c11)**. % 0.38/0.57 2040[4:Rew:2036.0,1658.0] || -> equal(multiply(u,sk_c11),u)**. % 0.38/0.57 2044[4:Rew:2040.0,1969.1] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.38/0.57 2076[4:SpL:1926.0,2044.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.38/0.57 2078[4:Obv:2076.1] || -> . % 0.38/0.57 2079[3:Spt:2078.0,38.1,1576.0] || equal(multiply(sk_c11,sk_c9),sk_c10)** -> . % 0.38/0.57 2080[3:Spt:2078.0,38.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.38/0.57 2081[3:MRR:36.1,2079.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.57 2082[3:MRR:34.1,2079.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.38/0.57 2087[3:MRR:35.1,2079.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.57 2088[3:MRR:33.1,2079.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.38/0.57 2100[3:SpR:2081.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.57 2113[2:SpR:1568.0,1729.0] || -> equal(inverse(sk_c10),sk_c11)**. % 0.38/0.57 2117[3:SpR:2082.0,1729.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.38/0.57 2119[3:Rew:2113.0,2117.0] || -> equal(sk_c4,sk_c11)**. % 0.38/0.57 2121[3:Rew:2119.0,2088.0] || -> equal(multiply(sk_c11,sk_c10),sk_c9)**. % 0.38/0.57 2147[3:SpR:2087.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.57 2151[3:Rew:2100.0,2147.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.57 2152[3:Rew:2151.0,2121.0] || -> equal(sk_c9,sk_c10)**. % 0.38/0.57 2153[3:Rew:2151.0,2079.0] || equal(sk_c9,sk_c10)** -> . % 0.38/0.57 2157[3:Rew:2152.0,2153.0] || equal(sk_c10,sk_c10)* -> . % 0.38/0.57 2158[3:Obv:2157.0] || -> . % 0.38/0.57 2186[2:Spt:2158.0,8.1,1568.0] || equal(inverse(sk_c11),sk_c10)** -> . % 0.38/0.57 2187[2:Spt:2158.0,8.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.38/0.57 2188[2:MRR:6.1,2186.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.38/0.57 2190[2:MRR:2.1,2186.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.38/0.57 2191[2:MRR:9.1,2186.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.38/0.57 2192[2:MRR:10.0,2186.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.38/0.57 2193[2:MRR:7.0,2186.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.38/0.57 2194[2:MRR:5.0,2186.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.38/0.57 2196[2:MRR:1.0,2186.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.38/0.57 2199[2:SpR:2187.0,1729.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.38/0.57 2201[2:Rew:2191.0,2199.0] || -> equal(sk_c7,sk_c8)**. % 0.38/0.57 2202[2:Rew:2201.0,2187.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.38/0.57 2203[2:Rew:2201.0,2192.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.38/0.57 2208[2:SpR:2188.0,251.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.38/0.57 2209[2:SpR:2188.0,1729.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.38/0.57 2211[2:Rew:2202.0,2209.0] || -> equal(sk_c6,sk_c5)**. % 0.38/0.57 2213[2:Rew:2211.0,2202.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.38/0.57 2214[2:Rew:2211.0,2203.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.38/0.57 2222[2:SpR:2190.0,109.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.38/0.57 2224[2:SpR:2190.0,1729.0] || -> equal(inverse(sk_c11),sk_c3)**. % 0.38/0.57 2226[2:Rew:2224.0,2186.0] || equal(sk_c3,sk_c10)** -> . % 0.38/0.57 2243[2:SpR:2194.0,64.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c11,u))**. % 0.38/0.57 2244[2:SpR:2194.0,109.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.38/0.57 2246[2:Rew:2188.0,2244.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.38/0.57 2247[2:Rew:2208.0,2243.0] || -> equal(multiply(sk_c11,u),u)**. % 0.38/0.57 2248[2:Rew:2247.0,2222.0] || -> equal(multiply(sk_c3,u),u)**. % 0.38/0.57 2251[2:Rew:2248.0,2196.0] || -> equal(sk_c10,sk_c11)**. % 0.38/0.57 2254[2:Rew:2251.0,2226.0] || equal(sk_c3,sk_c11)** -> . % 0.38/0.57 2255[2:Rew:2251.0,2193.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.38/0.57 2262[2:Rew:2246.0,2255.0] || -> equal(sk_c8,sk_c11)**. % 0.38/0.57 2265[2:Rew:2262.0,2213.0] || -> equal(inverse(sk_c11),sk_c5)**. % 0.38/0.57 2267[2:Rew:2262.0,2214.0] || -> equal(multiply(sk_c11,sk_c11),sk_c5)**. % 0.38/0.57 2271[2:Rew:2224.0,2265.0] || -> equal(sk_c5,sk_c3)**. % 0.38/0.57 2277[2:Rew:2247.0,2267.0,2271.0,2267.0] || -> equal(sk_c3,sk_c11)**. % 0.38/0.57 2278[2:MRR:2277.0,2254.0] || -> . % 0.38/0.57 % SZS output end Refutation % 0.38/0.57 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_5 prove_this_6 prove_this_7 prove_this_8 prove_this_9 prove_this_10 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_25 prove_this_26 prove_this_29 prove_this_31 prove_this_32 prove_this_33 prove_this_34 prove_this_35 prove_this_36 prove_this_38 prove_this_39 prove_this_41 prove_this_42 prove_this_45 prove_this_46 prove_this_49 prove_this_51 prove_this_52 prove_this_55 prove_this_56 prove_this_59 prove_this_61 left_identity left_inverse associativity % 0.38/0.57 %------------------------------------------------------------------------------