%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP379-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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:06 EDT 2022 % Result : Unsatisfiable 0.39s 0.62s % Output : Refutation 0.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : GRP379-1 : TPTP v8.1.0. Released v2.5.0. % 0.04/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n027.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Mon Jun 13 17:15:47 EDT 2022 % 0.14/0.35 % CPUTime : % 0.39/0.62 % 0.39/0.62 SPASS V 3.9 % 0.39/0.62 SPASS beiseite: Proof found. % 0.39/0.62 % SZS status Theorem % 0.39/0.62 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.39/0.62 SPASS derived 2034 clauses, backtracked 577 clauses, performed 11 splits and kept 1169 clauses. % 0.39/0.62 SPASS allocated 65004 KBytes. % 0.39/0.62 SPASS spent 0:00:00.26 on the problem. % 0.39/0.62 0:00:00.03 for the input. % 0.39/0.62 0:00:00.00 for the FLOTTER CNF translation. % 0.39/0.62 0:00:00.02 for inferences. % 0.39/0.62 0:00:00.00 for the backtracking. % 0.39/0.62 0:00:00.17 for the reduction. % 0.39/0.62 % 0.39/0.62 % 0.39/0.62 Here is a proof with depth 5, length 407 : % 0.39/0.62 % SZS output start Refutation % 0.39/0.62 1[0:Inp] || -> equal(inverse(sk_c11),sk_c10) equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.39/0.62 2[0:Inp] || -> equal(inverse(sk_c3),sk_c11)** equal(inverse(sk_c11),sk_c10). % 0.39/0.62 5[0:Inp] || -> equal(inverse(sk_c11),sk_c10) equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 6[0:Inp] || -> equal(inverse(sk_c5),sk_c8)** equal(inverse(sk_c11),sk_c10). % 0.39/0.62 7[0:Inp] || -> equal(inverse(sk_c11),sk_c10) equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 8[0:Inp] || -> equal(inverse(sk_c7),sk_c6)** equal(inverse(sk_c11),sk_c10). % 0.39/0.62 9[0:Inp] || -> equal(inverse(sk_c6),sk_c8)** equal(inverse(sk_c11),sk_c10). % 0.39/0.62 11[0:Inp] || -> equal(multiply(sk_c3,sk_c11),sk_c10)** equal(multiply(sk_c10,sk_c9),sk_c11). % 0.39/0.62 12[0:Inp] || -> equal(inverse(sk_c3),sk_c11) equal(multiply(sk_c10,sk_c9),sk_c11)**. % 0.39/0.62 13[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c9),sk_c11). % 0.39/0.62 14[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c10,sk_c9),sk_c11)**. % 0.39/0.62 15[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11)** equal(multiply(sk_c10,sk_c9),sk_c11). % 0.39/0.62 16[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c10,sk_c9),sk_c11)**. % 0.39/0.62 17[0:Inp] || -> equal(multiply(sk_c8,sk_c10),sk_c11)** equal(multiply(sk_c10,sk_c9),sk_c11). % 0.39/0.62 18[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c10,sk_c9),sk_c11)**. % 0.39/0.62 19[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c10,sk_c9),sk_c11)**. % 0.39/0.62 20[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c6)** equal(multiply(sk_c10,sk_c9),sk_c11). % 0.39/0.62 23[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9) equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 24[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 25[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11) equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 26[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 27[0:Inp] || -> equal(multiply(sk_c8,sk_c10),sk_c11) equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 29[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 33[0:Inp] || -> equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.39/0.62 34[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(inverse(sk_c1),sk_c2)**. % 0.39/0.62 35[0:Inp] || -> equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 36[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c1),sk_c2)**. % 0.39/0.62 37[0:Inp] || -> equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 39[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(inverse(sk_c1),sk_c2)**. % 0.39/0.62 43[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9) equal(multiply(sk_c2,sk_c9),sk_c11)**. % 0.39/0.62 44[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c2,sk_c9),sk_c11)**. % 0.39/0.62 45[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c11) equal(multiply(sk_c2,sk_c9),sk_c11)**. % 0.39/0.62 46[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c2,sk_c9),sk_c11)**. % 0.39/0.62 47[0:Inp] || -> equal(multiply(sk_c8,sk_c10),sk_c11) equal(multiply(sk_c2,sk_c9),sk_c11)**. % 0.39/0.62 49[0:Inp] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c2,sk_c9),sk_c11)**. % 0.39/0.62 51[0:Inp] || equal(inverse(u),v)* equal(inverse(w),u) equal(inverse(x),v) equal(inverse(y),z) equal(inverse(x1),sk_c10) equal(inverse(x2),sk_c11) equal(inverse(sk_c11),sk_c10) equal(multiply(w,v),u)*+ equal(multiply(x,v),sk_c11)** equal(multiply(y,z),sk_c11)** equal(multiply(v,sk_c10),sk_c11)** equal(multiply(x1,sk_c10),sk_c9)** equal(multiply(x2,sk_c11),sk_c10)** equal(multiply(z,sk_c9),sk_c11)** equal(multiply(sk_c10,sk_c9),sk_c11)** -> . % 0.39/0.62 52[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.39/0.62 53[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.39/0.62 54[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.39/0.62 55[1:Spt:51.0,51.1,51.2,51.7,51.8,51.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.39/0.62 56[1:EqR:55.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.39/0.62 57[2:Spt:9.1] || -> equal(inverse(sk_c11),sk_c10)**. % 0.39/0.62 59[3:Spt:19.1] || -> equal(multiply(sk_c10,sk_c9),sk_c11)**. % 0.39/0.62 61[3:SpL:59.0,55.3] || equal(inverse(u),sk_c9)** equal(inverse(sk_c10),u)* equal(inverse(v),sk_c9) equal(sk_c11,u) equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.39/0.62 62[4:Spt:39.1] || -> equal(inverse(sk_c1),sk_c2)**. % 0.39/0.62 64[5:Spt:49.1] || -> equal(multiply(sk_c2,sk_c9),sk_c11)**. % 0.39/0.62 67[6:Spt:29.1] || -> equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 74[2:SpR:57.0,53.0] || -> equal(multiply(sk_c10,sk_c11),identity)**. % 0.39/0.62 75[4:SpR:62.0,53.0] || -> equal(multiply(sk_c2,sk_c1),identity)**. % 0.39/0.62 87[0:SpR:53.0,54.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.39/0.62 88[2:SpR:74.0,54.0] || -> equal(multiply(sk_c10,multiply(sk_c11,u)),multiply(identity,u))**. % 0.39/0.62 89[4:SpR:75.0,54.0] || -> equal(multiply(sk_c2,multiply(sk_c1,u)),multiply(identity,u))**. % 0.39/0.62 91[2:Rew:52.0,88.0] || -> equal(multiply(sk_c10,multiply(sk_c11,u)),u)**. % 0.39/0.62 92[4:Rew:52.0,89.0] || -> equal(multiply(sk_c2,multiply(sk_c1,u)),u)**. % 0.39/0.62 93[0:Rew:52.0,87.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.39/0.62 102[6:SpR:67.0,92.0] || -> equal(multiply(sk_c2,sk_c11),sk_c2)**. % 0.39/0.62 110[0:SpR:93.0,93.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.39/0.62 112[3:SpR:59.0,93.0] || -> equal(multiply(inverse(sk_c10),sk_c11),sk_c9)**. % 0.39/0.62 116[0:SpR:53.0,93.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.39/0.62 119[6:SpR:102.0,93.0] || -> equal(multiply(inverse(sk_c2),sk_c2),sk_c11)**. % 0.39/0.62 120[2:SpR:91.0,93.0] || -> equal(multiply(inverse(sk_c10),u),multiply(sk_c11,u))**. % 0.39/0.62 127[6:Rew:53.0,119.0] || -> equal(identity,sk_c11)**. % 0.39/0.62 128[6:Rew:127.0,52.0] || -> equal(multiply(sk_c11,u),u)**. % 0.39/0.62 129[6:Rew:127.0,53.0] || -> equal(multiply(inverse(u),u),sk_c11)**. % 0.39/0.62 131[6:Rew:127.0,75.0] || -> equal(multiply(sk_c2,sk_c1),sk_c11)**. % 0.39/0.62 139[6:Rew:128.0,91.0] || -> equal(multiply(sk_c10,u),u)**. % 0.39/0.62 146[6:Rew:139.0,59.0] || -> equal(sk_c9,sk_c11)**. % 0.39/0.62 147[6:Rew:146.0,64.0] || -> equal(multiply(sk_c2,sk_c11),sk_c11)**. % 0.39/0.62 152[6:Rew:102.0,147.0] || -> equal(sk_c2,sk_c11)**. % 0.39/0.62 153[6:Rew:152.0,62.0] || -> equal(inverse(sk_c1),sk_c11)**. % 0.39/0.62 159[6:Rew:152.0,131.0] || -> equal(multiply(sk_c11,sk_c1),sk_c11)**. % 0.39/0.62 160[6:Rew:128.0,159.0] || -> equal(sk_c1,sk_c11)**. % 0.39/0.62 161[6:Rew:160.0,153.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 163[6:Rew:57.0,161.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 165[6:Rew:163.0,57.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 167[6:Rew:163.0,56.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_c11),sk_c11) -> . % 0.39/0.62 174[6:Rew:127.0,116.0] || -> equal(multiply(inverse(inverse(u)),sk_c11),u)**. % 0.39/0.62 183[6:Rew:110.0,174.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 198[6:Rew:183.0,167.4] || equal(inverse(multiply(u,v)),v)**+ equal(multiply(u,v),inverse(u)) equal(inverse(w),v) equal(multiply(w,v),sk_c11)** equal(v,sk_c11) -> . % 0.39/0.62 215[6:SpR:129.0,93.0] || -> equal(multiply(inverse(inverse(u)),sk_c11),u)**. % 0.39/0.62 217[6:Rew:183.0,215.0] || -> equal(inverse(inverse(u)),u)**. % 0.39/0.62 236[6:SpR:217.0,129.0] || -> equal(multiply(u,inverse(u)),sk_c11)**. % 0.39/0.62 854[6:SpL:129.0,198.0] || equal(inverse(sk_c11),u) equal(multiply(inverse(u),u),inverse(inverse(u)))** equal(inverse(v),u) equal(multiply(v,u),sk_c11)** equal(u,sk_c11) -> . % 0.39/0.62 864[6:Rew:129.0,854.1,217.0,854.1,165.0,854.0] || equal(sk_c11,u) equal(sk_c11,u) equal(inverse(v),u) equal(multiply(v,u),sk_c11)** equal(u,sk_c11) -> . % 0.39/0.62 865[6:Obv:864.1] || equal(inverse(u),v) equal(multiply(u,v),sk_c11)** equal(v,sk_c11) -> . % 0.39/0.62 950[6:SpL:236.0,865.1] || equal(inverse(u),inverse(u))* equal(sk_c11,sk_c11) equal(inverse(u),sk_c11) -> . % 0.39/0.62 972[6:Obv:950.1] || equal(inverse(u),sk_c11)** -> . % 0.39/0.62 973[6:UnC:972.0,217.0] || -> . % 0.39/0.62 979[6:Spt:973.0,29.1,67.0] || equal(multiply(sk_c1,sk_c2),sk_c11)** -> . % 0.39/0.62 980[6:Spt:973.0,29.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.39/0.62 981[3:Rew:120.0,112.0] || -> equal(multiply(sk_c11,sk_c11),sk_c9)**. % 0.39/0.62 986[6:MRR:26.1,979.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 987[6:MRR:24.1,979.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.39/0.62 989[0:Rew:110.0,116.0] || -> equal(multiply(u,identity),u)**. % 0.39/0.62 992[6:MRR:27.1,979.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 993[6:MRR:25.1,979.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 994[6:MRR:23.1,979.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.39/0.62 1020[4:SpR:75.0,93.0] || -> equal(multiply(inverse(sk_c2),identity),sk_c1)**. % 0.39/0.62 1022[4:Rew:989.0,1020.0] || -> equal(inverse(sk_c2),sk_c1)**. % 0.39/0.62 1035[2:SpR:74.0,93.0] || -> equal(multiply(inverse(sk_c10),identity),sk_c11)**. % 0.39/0.62 1037[2:Rew:989.0,1035.0] || -> equal(inverse(sk_c10),sk_c11)**. % 0.39/0.62 1041[3:Rew:1037.0,61.1] || equal(inverse(u),sk_c9)** equal(sk_c11,u) equal(inverse(v),sk_c9) equal(sk_c11,u) equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.39/0.62 1043[3:Obv:1041.1] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c11,u) equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.39/0.62 1066[6:SpR:993.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 1068[6:Rew:986.0,1066.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 1070[6:SpR:994.0,93.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.39/0.62 1072[6:Rew:59.0,1070.0,987.0,1070.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 1073[6:Rew:1072.0,57.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 1075[6:Rew:1072.0,74.0] || -> equal(multiply(sk_c11,sk_c11),identity)**. % 0.39/0.62 1078[6:Rew:1072.0,992.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.39/0.62 1098[6:Rew:981.0,1075.0] || -> equal(identity,sk_c9)**. % 0.39/0.62 1103[6:Rew:1098.0,989.0] || -> equal(multiply(u,sk_c9),u)**. % 0.39/0.62 1104[6:Rew:1068.0,1078.0] || -> equal(sk_c8,sk_c11)**. % 0.39/0.62 1114[6:Rew:1104.0,1068.0] || -> equal(multiply(sk_c11,sk_c11),sk_c11)**. % 0.39/0.62 1118[6:Rew:1103.0,64.0] || -> equal(sk_c2,sk_c11)**. % 0.39/0.62 1120[6:Rew:1118.0,1022.0] || -> equal(inverse(sk_c11),sk_c1)**. % 0.39/0.62 1121[6:Rew:1118.0,979.0] || equal(multiply(sk_c1,sk_c11),sk_c11)** -> . % 0.39/0.62 1125[6:Rew:1073.0,1120.0] || -> equal(sk_c1,sk_c11)**. % 0.39/0.62 1128[6:Rew:981.0,1114.0] || -> equal(sk_c9,sk_c11)**. % 0.39/0.62 1133[6:Rew:1128.0,1103.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 1156[6:Rew:1133.0,1121.0,1125.0,1121.0] || equal(sk_c11,sk_c11)* -> . % 0.39/0.62 1157[6:Obv:1156.0] || -> . % 0.39/0.62 1188[5:Spt:1157.0,49.1,64.0] || equal(multiply(sk_c2,sk_c9),sk_c11)** -> . % 0.39/0.62 1189[5:Spt:1157.0,49.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.39/0.62 1191[5:MRR:46.1,1188.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 1192[5:MRR:44.1,1188.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.39/0.62 1195[5:MRR:47.1,1188.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 1196[5:MRR:45.1,1188.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 1197[5:MRR:43.1,1188.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.39/0.62 1243[5:SpR:1196.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 1245[5:Rew:1191.0,1243.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 1247[5:SpR:1197.0,93.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.39/0.62 1249[5:Rew:59.0,1247.0,1192.0,1247.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 1250[5:Rew:1249.0,1037.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 1254[5:Rew:1249.0,74.0] || -> equal(multiply(sk_c11,sk_c11),identity)**. % 0.39/0.62 1255[5:Rew:1249.0,1195.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.39/0.62 1262[5:Rew:1249.0,1043.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c11,u) equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c11)** -> . % 0.39/0.62 1275[5:Rew:981.0,1254.0] || -> equal(identity,sk_c9)**. % 0.39/0.62 1277[5:Rew:1275.0,989.0] || -> equal(multiply(u,sk_c9),u)**. % 0.39/0.62 1281[5:Rew:1245.0,1255.0] || -> equal(sk_c8,sk_c11)**. % 0.39/0.62 1291[5:Rew:1281.0,1245.0] || -> equal(multiply(sk_c11,sk_c11),sk_c11)**. % 0.39/0.62 1294[5:Rew:981.0,1291.0] || -> equal(sk_c9,sk_c11)**. % 0.39/0.62 1299[5:Rew:1294.0,1277.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 1333[5:Rew:1294.0,1262.4,1299.0,1262.4,1299.0,1262.3,1294.0,1262.3,1294.0,1262.1,1294.0,1262.0] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c11)** equal(sk_c11,u) equal(v,sk_c11) equal(sk_c11,sk_c11) -> . % 0.39/0.62 1334[5:Obv:1333.4] || equal(inverse(u),sk_c11)**+ equal(inverse(v),sk_c11)** equal(sk_c11,u) equal(v,sk_c11) -> . % 0.39/0.62 1701[5:SpL:1250.0,1334.0] || equal(sk_c11,sk_c11) equal(inverse(u),sk_c11)** equal(sk_c11,sk_c11) equal(u,sk_c11) -> . % 0.39/0.62 1705[5:Obv:1701.2] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.39/0.62 1765[5:SpL:1250.0,1705.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.39/0.62 1769[5:Obv:1765.1] || -> . % 0.39/0.62 1770[4:Spt:1769.0,39.1,62.0] || equal(inverse(sk_c1),sk_c2)** -> . % 0.39/0.62 1771[4:Spt:1769.0,39.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.39/0.62 1773[4:MRR:36.1,1770.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 1774[4:MRR:34.1,1770.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.39/0.62 1778[4:MRR:37.0,1770.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 1779[4:MRR:35.0,1770.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 1780[4:MRR:33.0,1770.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.39/0.62 1825[4:SpR:1779.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 1827[4:Rew:1773.0,1825.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 1829[4:SpR:1780.0,93.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.39/0.62 1831[4:Rew:59.0,1829.0,1774.0,1829.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 1832[4:Rew:1831.0,57.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 1835[4:Rew:1831.0,74.0] || -> equal(multiply(sk_c11,sk_c11),identity)**. % 0.39/0.62 1837[4:Rew:1831.0,1778.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.39/0.62 1844[4:Rew:1831.0,1043.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c11,u) equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c9,sk_c11),sk_c11)** -> . % 0.39/0.62 1855[4:Rew:981.0,1835.0] || -> equal(identity,sk_c9)**. % 0.39/0.62 1857[4:Rew:1855.0,989.0] || -> equal(multiply(u,sk_c9),u)**. % 0.39/0.62 1860[4:Rew:1827.0,1837.0] || -> equal(sk_c8,sk_c11)**. % 0.39/0.62 1870[4:Rew:1860.0,1827.0] || -> equal(multiply(sk_c11,sk_c11),sk_c11)**. % 0.39/0.62 1872[4:Rew:981.0,1870.0] || -> equal(sk_c9,sk_c11)**. % 0.39/0.62 1877[4:Rew:1872.0,1857.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 1910[4:Rew:1872.0,1844.4,1877.0,1844.4,1877.0,1844.3,1872.0,1844.3,1872.0,1844.1,1872.0,1844.0] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c11)** equal(sk_c11,u) equal(v,sk_c11) equal(sk_c11,sk_c11) -> . % 0.39/0.62 1911[4:Obv:1910.4] || equal(inverse(u),sk_c11)**+ equal(inverse(v),sk_c11)** equal(sk_c11,u) equal(v,sk_c11) -> . % 0.39/0.62 2153[4:SpL:1832.0,1911.0] || equal(sk_c11,sk_c11) equal(inverse(u),sk_c11)** equal(sk_c11,sk_c11) equal(u,sk_c11) -> . % 0.39/0.62 2156[4:Obv:2153.2] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.39/0.62 2158[4:SpL:1832.0,2156.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.39/0.62 2161[4:Obv:2158.1] || -> . % 0.39/0.62 2162[3:Spt:2161.0,19.1,59.0] || equal(multiply(sk_c10,sk_c9),sk_c11)** -> . % 0.39/0.62 2163[3:Spt:2161.0,19.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.39/0.62 2164[3:MRR:18.1,2162.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.39/0.62 2165[3:MRR:16.1,2162.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 2166[3:MRR:14.1,2162.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.39/0.62 2167[3:MRR:12.1,2162.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.39/0.62 2168[3:MRR:20.1,2162.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.39/0.62 2169[3:MRR:17.1,2162.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 2170[3:MRR:15.1,2162.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 2171[3:MRR:13.1,2162.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.39/0.62 2172[3:MRR:11.1,2162.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.39/0.62 2181[3:SpR:2165.0,93.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),u)**. % 0.39/0.62 2185[3:SpR:2167.0,93.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.39/0.62 2193[3:SpR:2168.0,93.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.39/0.62 2195[3:Rew:2164.0,2193.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.39/0.62 2196[3:SpR:2169.0,54.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),multiply(sk_c11,u))**. % 0.39/0.62 2197[3:SpR:2169.0,93.0] || -> equal(multiply(inverse(sk_c8),sk_c11),sk_c10)**. % 0.39/0.62 2200[3:SpR:2170.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 2202[3:Rew:2165.0,2200.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 2204[3:SpR:2171.0,93.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.39/0.62 2206[3:Rew:2166.0,2204.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.39/0.62 2207[3:Rew:2206.0,2162.0] || equal(sk_c10,sk_c11)** -> . % 0.39/0.62 2218[3:SpR:2195.0,93.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c6)**. % 0.39/0.62 2220[3:Rew:2163.0,2218.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.39/0.62 2222[3:SpR:2202.0,93.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c11)**. % 0.39/0.62 2224[3:Rew:53.0,2222.0] || -> equal(identity,sk_c11)**. % 0.39/0.62 2226[3:Rew:2224.0,52.0] || -> equal(multiply(sk_c11,u),u)**. % 0.39/0.62 2227[3:Rew:2224.0,989.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 2235[3:Rew:2226.0,2185.0] || -> equal(multiply(sk_c3,u),u)**. % 0.39/0.62 2238[3:Rew:2226.0,2196.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),u)**. % 0.39/0.62 2242[3:Rew:2227.0,2172.0] || -> equal(sk_c3,sk_c10)**. % 0.39/0.62 2243[3:Rew:2227.0,2197.0] || -> equal(inverse(sk_c8),sk_c10)**. % 0.39/0.62 2247[3:Rew:2242.0,2235.0] || -> equal(multiply(sk_c10,u),u)**. % 0.39/0.62 2253[3:Rew:2247.0,2238.0] || -> equal(multiply(sk_c8,u),u)**. % 0.39/0.62 2255[3:Rew:2253.0,2220.0] || -> equal(sk_c6,sk_c8)**. % 0.39/0.62 2256[3:Rew:2253.0,2181.0] || -> equal(multiply(sk_c5,u),u)**. % 0.39/0.62 2261[3:Rew:2255.0,2163.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.39/0.62 2266[3:Rew:2243.0,2261.0] || -> equal(sk_c8,sk_c10)**. % 0.39/0.62 2268[3:Rew:2266.0,2170.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.39/0.62 2278[3:Rew:2256.0,2268.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 2279[3:MRR:2278.0,2207.0] || -> . % 0.39/0.62 2291[2:Spt:2279.0,9.1,57.0] || equal(inverse(sk_c11),sk_c10)** -> . % 0.39/0.62 2292[2:Spt:2279.0,9.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.39/0.62 2294[2:MRR:6.1,2291.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 2296[2:MRR:2.1,2291.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.39/0.62 2298[2:MRR:7.0,2291.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 2299[2:MRR:5.0,2291.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 2301[2:MRR:1.0,2291.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.39/0.62 2320[2:SpR:2299.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 2322[2:Rew:2294.0,2320.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 2328[2:SpR:2301.0,93.0] || -> equal(multiply(inverse(sk_c3),sk_c10),sk_c11)**. % 0.39/0.62 2330[2:Rew:2296.0,2328.0] || -> equal(multiply(sk_c11,sk_c10),sk_c11)**. % 0.39/0.62 2336[2:SpR:2322.0,93.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c11)**. % 0.39/0.62 2338[2:Rew:53.0,2336.0] || -> equal(identity,sk_c11)**. % 0.39/0.62 2339[2:Rew:2338.0,52.0] || -> equal(multiply(sk_c11,u),u)**. % 0.39/0.62 2340[2:Rew:2338.0,989.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 2345[2:Rew:2339.0,2330.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 2351[2:Rew:2345.0,2291.0] || equal(inverse(sk_c11),sk_c11)** -> . % 0.39/0.62 2352[2:Rew:2345.0,2298.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.39/0.62 2363[2:Rew:2340.0,2352.0] || -> equal(sk_c8,sk_c11)**. % 0.39/0.62 2365[2:Rew:2363.0,2294.0] || -> equal(inverse(sk_c5),sk_c11)**. % 0.39/0.62 2367[2:Rew:2363.0,2299.0] || -> equal(multiply(sk_c5,sk_c11),sk_c11)**. % 0.39/0.62 2387[2:Rew:2340.0,2367.0] || -> equal(sk_c5,sk_c11)**. % 0.39/0.62 2388[2:Rew:2387.0,2365.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 2389[2:MRR:2388.0,2351.0] || -> . % 0.39/0.62 2410[1:Spt:2389.0,51.3,51.4,51.5,51.6,51.9,51.11,51.12,51.13,51.14] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(inverse(sk_c11),sk_c10) equal(multiply(u,v),sk_c11)**+ equal(multiply(w,sk_c10),sk_c9)** equal(multiply(x,sk_c11),sk_c10)** equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c10,sk_c9),sk_c11)** -> . % 0.39/0.62 2414[2:Spt:8.1] || -> equal(inverse(sk_c11),sk_c10)**. % 0.39/0.62 2415[2:Rew:2414.0,2410.3] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(sk_c10,sk_c10) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(x,sk_c11),sk_c10)** equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c10,sk_c9),sk_c11)** -> . % 0.39/0.62 2418[2:Obv:2415.3] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(x,sk_c11),sk_c10)** equal(multiply(v,sk_c9),sk_c11)** equal(multiply(sk_c10,sk_c9),sk_c11)** -> . % 0.39/0.62 2421[2:SpR:2414.0,93.0] || -> equal(multiply(sk_c10,multiply(sk_c11,u)),u)**. % 0.39/0.62 2423[3:Spt:18.1] || -> equal(multiply(sk_c10,sk_c9),sk_c11)**. % 0.39/0.62 2426[3:Rew:2423.0,2418.7] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(x,sk_c11),sk_c10)** equal(multiply(v,sk_c9),sk_c11)** equal(sk_c11,sk_c11) -> . % 0.39/0.62 2427[3:Obv:2426.7] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(x,sk_c11),sk_c10)** equal(multiply(v,sk_c9),sk_c11)** -> . % 0.39/0.62 2430[3:SpR:2423.0,54.0] || -> equal(multiply(sk_c10,multiply(sk_c9,u)),multiply(sk_c11,u))**. % 0.39/0.62 2431[3:SpR:2423.0,93.0] || -> equal(multiply(inverse(sk_c10),sk_c11),sk_c9)**. % 0.39/0.62 2433[4:Spt:39.1] || -> equal(inverse(sk_c1),sk_c2)**. % 0.39/0.62 2434[4:SpR:2433.0,93.0] || -> equal(multiply(sk_c2,multiply(sk_c1,u)),u)**. % 0.39/0.62 2436[5:Spt:29.1] || -> equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 2438[5:SpR:2436.0,93.0] || -> equal(multiply(inverse(sk_c1),sk_c11),sk_c2)**. % 0.39/0.62 2440[5:Rew:2433.0,2438.0] || -> equal(multiply(sk_c2,sk_c11),sk_c2)**. % 0.39/0.62 2449[5:SpR:2440.0,93.0] || -> equal(multiply(inverse(sk_c2),sk_c2),sk_c11)**. % 0.39/0.62 2451[5:Rew:53.0,2449.0] || -> equal(identity,sk_c11)**. % 0.39/0.62 2452[5:Rew:2451.0,52.0] || -> equal(multiply(sk_c11,u),u)**. % 0.39/0.62 2453[5:Rew:2451.0,989.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 2455[5:Rew:2451.0,53.0] || -> equal(multiply(inverse(u),u),sk_c11)**. % 0.39/0.62 2456[5:Rew:2452.0,2421.0] || -> equal(multiply(sk_c10,u),u)**. % 0.39/0.62 2464[5:Rew:2453.0,2427.5] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11)** equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c10),sk_c9)** equal(x,sk_c10) equal(multiply(v,sk_c9),sk_c11)** -> . % 0.39/0.62 2465[5:Rew:2456.0,2423.0] || -> equal(sk_c9,sk_c11)**. % 0.39/0.62 2512[5:SpR:2455.0,93.0] || -> equal(multiply(inverse(inverse(u)),sk_c11),u)**. % 0.39/0.62 2513[5:SpR:2455.0,2453.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 2516[5:Rew:2453.0,2512.0] || -> equal(inverse(inverse(u)),u)**. % 0.39/0.62 2521[5:SpR:2516.0,2455.0] || -> equal(multiply(u,inverse(u)),sk_c11)**. % 0.39/0.62 2529[5:SpR:2521.0,2452.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 2608[5:Rew:2414.0,2513.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 2663[5:Rew:2453.0,2464.6,2465.0,2464.6,2465.0,2464.4] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11)** equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c10),sk_c11)** equal(x,sk_c10) equal(v,sk_c11) -> . % 0.39/0.62 2664[5:Rew:2608.0,2663.5,2608.0,2663.4,2608.0,2663.1] || equal(inverse(u),v) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11)** equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c11),sk_c11)** equal(x,sk_c11) equal(v,sk_c11) -> . % 0.39/0.62 2665[5:Rew:2453.0,2664.4] || equal(inverse(u),v) equal(inverse(w),sk_c11)** equal(inverse(x),sk_c11)** equal(multiply(u,v),sk_c11)** equal(w,sk_c11) equal(x,sk_c11) equal(v,sk_c11) -> . % 0.39/0.62 2666[5:Con:2665.2] || equal(inverse(u),v) equal(inverse(w),sk_c11)** equal(multiply(u,v),sk_c11)**+ equal(w,sk_c11) equal(v,sk_c11) -> . % 0.39/0.62 2717[5:SpL:2452.0,2666.2] || equal(inverse(sk_c11),u)* equal(inverse(v),sk_c11)** equal(u,sk_c11) equal(v,sk_c11) equal(u,sk_c11) -> . % 0.39/0.62 2725[5:Obv:2717.2] || equal(inverse(sk_c11),u)* equal(inverse(v),sk_c11)** equal(v,sk_c11) equal(u,sk_c11) -> . % 0.39/0.62 2726[5:Rew:2529.0,2725.0] || equal(sk_c11,u)* equal(inverse(v),sk_c11)** equal(v,sk_c11) equal(u,sk_c11)* -> . % 0.39/0.62 2727[5:Obv:2726.0] || equal(inverse(u),sk_c11)** equal(u,sk_c11) equal(v,sk_c11)* -> . % 0.39/0.62 2728[5:Con:2727.2] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.39/0.62 2760[5:SpL:2529.0,2728.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.39/0.62 2762[5:Obv:2760.1] || -> . % 0.39/0.62 2763[5:Spt:2762.0,29.1,2436.0] || equal(multiply(sk_c1,sk_c2),sk_c11)** -> . % 0.39/0.62 2764[5:Spt:2762.0,29.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.39/0.62 2766[5:MRR:26.1,2763.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 2767[5:MRR:24.1,2763.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.39/0.62 2770[5:MRR:27.1,2763.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 2771[5:MRR:25.1,2763.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 2772[5:MRR:23.1,2763.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.39/0.62 2797[5:SpR:2771.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 2799[5:Rew:2766.0,2797.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 2801[5:SpR:2772.0,93.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.39/0.62 2803[5:Rew:2423.0,2801.0,2767.0,2801.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 2804[5:Rew:2803.0,2414.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 2807[5:Rew:2803.0,2770.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.39/0.62 2809[5:Rew:2803.0,2431.0] || -> equal(multiply(inverse(sk_c11),sk_c11),sk_c9)**. % 0.39/0.62 2810[5:Rew:2803.0,2421.0] || -> equal(multiply(sk_c11,multiply(sk_c11,u)),u)**. % 0.39/0.62 2811[5:Rew:2803.0,2430.0] || -> equal(multiply(sk_c11,multiply(sk_c9,u)),multiply(sk_c11,u))**. % 0.39/0.62 2819[5:Rew:2799.0,2807.0] || -> equal(sk_c8,sk_c11)**. % 0.39/0.62 2829[5:Rew:2819.0,2799.0] || -> equal(multiply(sk_c11,sk_c11),sk_c11)**. % 0.39/0.62 2830[5:Rew:2829.0,2809.0,2804.0,2809.0] || -> equal(sk_c9,sk_c11)**. % 0.39/0.62 2835[5:Rew:2810.0,2811.0,2830.0,2811.0] || -> equal(multiply(sk_c11,u),u)**. % 0.39/0.62 2879[4:SpR:989.0,2434.0] || -> equal(multiply(sk_c2,sk_c1),identity)**. % 0.39/0.62 2884[4:SpR:2879.0,93.0] || -> equal(multiply(inverse(sk_c2),identity),sk_c1)**. % 0.39/0.62 2886[4:Rew:989.0,2884.0] || -> equal(inverse(sk_c2),sk_c1)**. % 0.39/0.62 2893[5:SpR:2835.0,989.0] || -> equal(identity,sk_c11)**. % 0.39/0.62 2898[5:Rew:2893.0,53.0] || -> equal(multiply(inverse(u),u),sk_c11)**. % 0.39/0.62 2923[5:SpR:2886.0,2898.0] || -> equal(multiply(sk_c1,sk_c2),sk_c11)**. % 0.39/0.62 2936[5:MRR:2923.0,2763.0] || -> . % 0.39/0.62 2939[4:Spt:2936.0,39.1,2433.0] || equal(inverse(sk_c1),sk_c2)** -> . % 0.39/0.62 2940[4:Spt:2936.0,39.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.39/0.62 2942[4:MRR:36.1,2939.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 2943[4:MRR:34.1,2939.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.39/0.62 2946[4:MRR:37.0,2939.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 2947[4:MRR:35.0,2939.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 2948[4:MRR:33.0,2939.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.39/0.62 2973[4:SpR:2947.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 2975[4:Rew:2942.0,2973.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 2977[4:SpR:2948.0,93.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.39/0.62 2979[4:Rew:2423.0,2977.0,2943.0,2977.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 2980[4:Rew:2979.0,2414.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.62 2983[4:Rew:2979.0,2946.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.39/0.62 2985[4:Rew:2979.0,2431.0] || -> equal(multiply(inverse(sk_c11),sk_c11),sk_c9)**. % 0.39/0.62 2986[4:Rew:2979.0,2421.0] || -> equal(multiply(sk_c11,multiply(sk_c11,u)),u)**. % 0.39/0.62 2987[4:Rew:2979.0,2430.0] || -> equal(multiply(sk_c11,multiply(sk_c9,u)),multiply(sk_c11,u))**. % 0.39/0.62 2990[4:Rew:2979.0,2427.1] || equal(inverse(u),v) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(x,sk_c11),sk_c10)** equal(multiply(v,sk_c9),sk_c11)** -> . % 0.39/0.62 2995[4:Rew:2975.0,2983.0] || -> equal(sk_c8,sk_c11)**. % 0.39/0.62 3005[4:Rew:2995.0,2975.0] || -> equal(multiply(sk_c11,sk_c11),sk_c11)**. % 0.39/0.62 3006[4:Rew:3005.0,2985.0,2980.0,2985.0] || -> equal(sk_c9,sk_c11)**. % 0.39/0.62 3011[4:Rew:2986.0,2987.0,3006.0,2987.0] || -> equal(multiply(sk_c11,u),u)**. % 0.39/0.62 3026[4:Rew:3006.0,2990.6,2979.0,2990.5,2979.0,2990.4,3006.0,2990.4] || equal(inverse(u),v) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c11),sk_c11)** equal(multiply(x,sk_c11),sk_c11)** equal(multiply(v,sk_c11),sk_c11)** -> . % 0.39/0.62 3027[4:Con:3026.2] || equal(inverse(u),v) equal(inverse(w),sk_c11) equal(multiply(u,v),sk_c11)** equal(multiply(w,sk_c11),sk_c11)** equal(multiply(v,sk_c11),sk_c11)** -> . % 0.39/0.62 3060[4:SpR:3011.0,989.0] || -> equal(identity,sk_c11)**. % 0.39/0.62 3063[4:Rew:3060.0,989.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 3068[4:Rew:3063.0,3027.3] || equal(inverse(u),v) equal(inverse(w),sk_c11)** equal(multiply(u,v),sk_c11)** equal(w,sk_c11) equal(multiply(v,sk_c11),sk_c11)** -> . % 0.39/0.62 3071[4:Rew:3063.0,3068.4] || equal(inverse(u),v) equal(inverse(w),sk_c11)** equal(multiply(u,v),sk_c11)**+ equal(w,sk_c11) equal(v,sk_c11) -> . % 0.39/0.62 3107[4:SpL:3011.0,3071.2] || equal(inverse(sk_c11),u)* equal(inverse(v),sk_c11)** equal(u,sk_c11) equal(v,sk_c11) equal(u,sk_c11) -> . % 0.39/0.62 3109[4:Obv:3107.2] || equal(inverse(sk_c11),u)* equal(inverse(v),sk_c11)** equal(v,sk_c11) equal(u,sk_c11) -> . % 0.39/0.62 3110[4:Rew:2980.0,3109.0] || equal(sk_c11,u)* equal(inverse(v),sk_c11)** equal(v,sk_c11) equal(u,sk_c11)* -> . % 0.39/0.62 3111[4:Obv:3110.0] || equal(inverse(u),sk_c11)** equal(u,sk_c11) equal(v,sk_c11)* -> . % 0.39/0.62 3112[4:Con:3111.2] || equal(inverse(u),sk_c11)** equal(u,sk_c11) -> . % 0.39/0.62 3122[4:SpL:2980.0,3112.0] || equal(sk_c11,sk_c11)* equal(sk_c11,sk_c11)* -> . % 0.39/0.62 3123[4:Obv:3122.1] || -> . % 0.39/0.62 3124[3:Spt:3123.0,18.1,2423.0] || equal(multiply(sk_c10,sk_c9),sk_c11)** -> . % 0.39/0.62 3125[3:Spt:3123.0,18.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.39/0.62 3126[3:MRR:16.1,3124.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 3127[3:MRR:14.1,3124.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.39/0.62 3128[3:MRR:12.1,3124.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.39/0.62 3129[3:MRR:19.1,3124.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.39/0.62 3130[3:MRR:20.1,3124.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.39/0.62 3131[3:MRR:17.1,3124.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 3132[3:MRR:15.1,3124.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 3133[3:MRR:13.1,3124.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.39/0.62 3134[3:MRR:11.1,3124.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.39/0.62 3139[3:SpR:3126.0,93.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),u)**. % 0.39/0.62 3143[3:SpR:3128.0,93.0] || -> equal(multiply(sk_c11,multiply(sk_c3,u)),u)**. % 0.39/0.62 3148[3:SpR:3130.0,93.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.39/0.62 3150[3:Rew:3125.0,3148.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.39/0.62 3151[3:SpR:3131.0,54.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),multiply(sk_c11,u))**. % 0.39/0.62 3152[3:SpR:3131.0,93.0] || -> equal(multiply(inverse(sk_c8),sk_c11),sk_c10)**. % 0.39/0.62 3155[3:SpR:3132.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 3157[3:Rew:3126.0,3155.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 3159[3:SpR:3133.0,93.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.39/0.62 3161[3:Rew:3127.0,3159.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.39/0.62 3162[3:Rew:3161.0,3124.0] || equal(sk_c10,sk_c11)** -> . % 0.39/0.62 3168[3:SpR:3150.0,93.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c6)**. % 0.39/0.62 3170[3:Rew:3129.0,3168.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.39/0.62 3175[3:SpR:3157.0,93.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c11)**. % 0.39/0.62 3177[3:Rew:53.0,3175.0] || -> equal(identity,sk_c11)**. % 0.39/0.62 3178[3:Rew:3177.0,52.0] || -> equal(multiply(sk_c11,u),u)**. % 0.39/0.62 3179[3:Rew:3177.0,989.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.62 3183[3:Rew:3178.0,3143.0] || -> equal(multiply(sk_c3,u),u)**. % 0.39/0.62 3185[3:Rew:3178.0,3151.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),u)**. % 0.39/0.62 3189[3:Rew:3179.0,3134.0] || -> equal(sk_c3,sk_c10)**. % 0.39/0.62 3190[3:Rew:3179.0,3152.0] || -> equal(inverse(sk_c8),sk_c10)**. % 0.39/0.62 3192[3:Rew:3189.0,3183.0] || -> equal(multiply(sk_c10,u),u)**. % 0.39/0.62 3198[3:Rew:3192.0,3185.0] || -> equal(multiply(sk_c8,u),u)**. % 0.39/0.62 3201[3:Rew:3198.0,3139.0] || -> equal(multiply(sk_c5,u),u)**. % 0.39/0.62 3202[3:Rew:3198.0,3170.0] || -> equal(sk_c6,sk_c8)**. % 0.39/0.62 3207[3:Rew:3202.0,3129.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.39/0.62 3211[3:Rew:3190.0,3207.0] || -> equal(sk_c8,sk_c10)**. % 0.39/0.62 3213[3:Rew:3211.0,3132.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.39/0.62 3223[3:Rew:3201.0,3213.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.62 3224[3:MRR:3223.0,3162.0] || -> . % 0.39/0.62 3232[2:Spt:3224.0,8.1,2414.0] || equal(inverse(sk_c11),sk_c10)** -> . % 0.39/0.62 3233[2:Spt:3224.0,8.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.39/0.62 3234[2:MRR:6.1,3232.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.39/0.62 3236[2:MRR:2.1,3232.0] || -> equal(inverse(sk_c3),sk_c11)**. % 0.39/0.62 3239[2:MRR:7.0,3232.0] || -> equal(multiply(sk_c8,sk_c10),sk_c11)**. % 0.39/0.62 3240[2:MRR:5.0,3232.0] || -> equal(multiply(sk_c5,sk_c8),sk_c11)**. % 0.39/0.62 3242[2:MRR:1.0,3232.0] || -> equal(multiply(sk_c3,sk_c11),sk_c10)**. % 0.39/0.62 3261[2:SpR:3240.0,93.0] || -> equal(multiply(inverse(sk_c5),sk_c11),sk_c8)**. % 0.39/0.62 3263[2:Rew:3234.0,3261.0] || -> equal(multiply(sk_c8,sk_c11),sk_c8)**. % 0.39/0.62 3269[2:SpR:3242.0,93.0] || -> equal(multiply(inverse(sk_c3),sk_c10),sk_c11)**. % 0.39/0.62 3271[2:Rew:3236.0,3269.0] || -> equal(multiply(sk_c11,sk_c10),sk_c11)**. % 0.39/0.62 3277[2:SpR:3263.0,93.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c11)**. % 0.39/0.62 3279[2:Rew:53.0,3277.0] || -> equal(identity,sk_c11)**. % 0.39/0.62 3280[2:Rew:3279.0,52.0] || -> equal(multiply(sk_c11,u),u)**. % 0.39/0.63 3281[2:Rew:3279.0,989.0] || -> equal(multiply(u,sk_c11),u)**. % 0.39/0.63 3284[2:Rew:3280.0,3271.0] || -> equal(sk_c10,sk_c11)**. % 0.39/0.63 3290[2:Rew:3284.0,3232.0] || equal(inverse(sk_c11),sk_c11)** -> . % 0.39/0.63 3291[2:Rew:3284.0,3239.0] || -> equal(multiply(sk_c8,sk_c11),sk_c11)**. % 0.39/0.63 3298[2:Rew:3281.0,3291.0] || -> equal(sk_c8,sk_c11)**. % 0.39/0.63 3299[2:Rew:3298.0,3234.0] || -> equal(inverse(sk_c5),sk_c11)**. % 0.39/0.63 3302[2:Rew:3298.0,3240.0] || -> equal(multiply(sk_c5,sk_c11),sk_c11)**. % 0.39/0.63 3322[2:Rew:3281.0,3302.0] || -> equal(sk_c5,sk_c11)**. % 0.39/0.63 3323[2:Rew:3322.0,3299.0] || -> equal(inverse(sk_c11),sk_c11)**. % 0.39/0.63 3324[2:MRR:3323.0,3290.0] || -> . % 0.39/0.63 % SZS output end Refutation % 0.39/0.63 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_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_23 prove_this_24 prove_this_25 prove_this_26 prove_this_27 prove_this_29 prove_this_33 prove_this_34 prove_this_35 prove_this_36 prove_this_37 prove_this_39 prove_this_43 prove_this_44 prove_this_45 prove_this_46 prove_this_47 prove_this_49 prove_this_51 left_identity left_inverse associativity % 0.39/0.63 %------------------------------------------------------------------------------