%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP251-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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:31 EDT 2022 % Result : Unsatisfiable 0.19s 0.51s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP251-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n006.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 18:37:11 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.51 % 0.19/0.51 SPASS V 3.9 % 0.19/0.51 SPASS beiseite: Proof found. % 0.19/0.51 % SZS status Theorem % 0.19/0.51 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.51 SPASS derived 1058 clauses, backtracked 298 clauses, performed 12 splits and kept 602 clauses. % 0.19/0.51 SPASS allocated 64090 KBytes. % 0.19/0.51 SPASS spent 0:00:00.16 on the problem. % 0.19/0.51 0:00:00.04 for the input. % 0.19/0.51 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.51 0:00:00.01 for inferences. % 0.19/0.51 0:00:00.00 for the backtracking. % 0.19/0.51 0:00:00.08 for the reduction. % 0.19/0.51 % 0.19/0.51 % 0.19/0.51 Here is a proof with depth 6, length 295 : % 0.19/0.51 % SZS output start Refutation % 0.19/0.51 1[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(multiply(sk_c1,sk_c10),sk_c9). % 0.19/0.51 2[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c1,sk_c10),sk_c9)**. % 0.19/0.51 3[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c9)** equal(multiply(sk_c1,sk_c10),sk_c9). % 0.19/0.51 4[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c1,sk_c10),sk_c9)**. % 0.19/0.51 5[0:Inp] || -> equal(multiply(sk_c9,sk_c7),sk_c8)** equal(multiply(sk_c1,sk_c10),sk_c9). % 0.19/0.51 6[0:Inp] || -> equal(multiply(sk_c6,sk_c9),sk_c7)** equal(multiply(sk_c1,sk_c10),sk_c9). % 0.19/0.51 7[0:Inp] || -> equal(inverse(sk_c6),sk_c9) equal(multiply(sk_c1,sk_c10),sk_c9)**. % 0.19/0.51 9[0:Inp] || -> equal(inverse(sk_c4),sk_c10)** equal(inverse(sk_c1),sk_c10). % 0.19/0.51 10[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.51 11[0:Inp] || -> equal(inverse(sk_c5),sk_c8)** equal(inverse(sk_c1),sk_c10). % 0.19/0.51 12[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.19/0.51 13[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c6,sk_c9),sk_c7)**. % 0.19/0.51 14[0:Inp] || -> equal(inverse(sk_c6),sk_c9)** equal(inverse(sk_c1),sk_c10). % 0.19/0.51 15[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9) equal(multiply(sk_c2,sk_c9),sk_c8)**. % 0.19/0.51 16[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c2,sk_c9),sk_c8)**. % 0.19/0.51 17[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c9) equal(multiply(sk_c2,sk_c9),sk_c8)**. % 0.19/0.51 18[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c2,sk_c9),sk_c8)**. % 0.19/0.51 19[0:Inp] || -> equal(multiply(sk_c9,sk_c7),sk_c8)** equal(multiply(sk_c2,sk_c9),sk_c8). % 0.19/0.51 20[0:Inp] || -> equal(multiply(sk_c6,sk_c9),sk_c7) equal(multiply(sk_c2,sk_c9),sk_c8)**. % 0.19/0.51 21[0:Inp] || -> equal(inverse(sk_c6),sk_c9) equal(multiply(sk_c2,sk_c9),sk_c8)**. % 0.19/0.51 22[0:Inp] || -> equal(inverse(sk_c2),sk_c9) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.51 23[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(inverse(sk_c2),sk_c9)**. % 0.19/0.51 25[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c2),sk_c9)**. % 0.19/0.51 26[0:Inp] || -> equal(inverse(sk_c2),sk_c9) equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.19/0.51 27[0:Inp] || -> equal(inverse(sk_c2),sk_c9) equal(multiply(sk_c6,sk_c9),sk_c7)**. % 0.19/0.51 28[0:Inp] || -> equal(inverse(sk_c6),sk_c9) equal(inverse(sk_c2),sk_c9)**. % 0.19/0.51 31[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.51 32[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c3),sk_c9)**. % 0.19/0.51 33[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.19/0.51 34[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c6,sk_c9),sk_c7)**. % 0.19/0.51 35[0:Inp] || -> equal(inverse(sk_c6),sk_c9) equal(inverse(sk_c3),sk_c9)**. % 0.19/0.51 37[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.19/0.51 38[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c9) equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.19/0.51 39[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.19/0.51 40[0:Inp] || -> equal(multiply(sk_c9,sk_c7),sk_c8)** equal(multiply(sk_c3,sk_c8),sk_c9). % 0.19/0.51 41[0:Inp] || -> equal(multiply(sk_c6,sk_c9),sk_c7) equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.19/0.51 42[0:Inp] || -> equal(inverse(sk_c6),sk_c9) equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.19/0.51 43[0:Inp] || equal(multiply(u,sk_c10),sk_c9)** equal(inverse(u),sk_c10) equal(multiply(v,sk_c9),sk_c8)** equal(inverse(v),sk_c9) equal(inverse(w),sk_c9) equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c10),sk_c9)** equal(inverse(x),sk_c10) equal(multiply(y,sk_c8),sk_c9)** equal(inverse(y),sk_c8) equal(multiply(sk_c9,z),sk_c8)** equal(multiply(x1,sk_c9),z)* equal(inverse(x1),sk_c9) -> . % 0.19/0.51 44[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.51 45[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.51 46[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.51 47[0:Con:43.6] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c8) equal(inverse(w),sk_c9) equal(inverse(x),sk_c9) equal(inverse(y),sk_c10) equal(multiply(u,sk_c9),z)*+ equal(multiply(v,sk_c8),sk_c9)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c9),sk_c8)** equal(multiply(y,sk_c10),sk_c9)** equal(multiply(sk_c9,z),sk_c8)** -> . % 0.19/0.51 48[1:Spt:47.2,47.7] || equal(inverse(u),sk_c9) equal(multiply(u,sk_c8),sk_c9)** -> . % 0.19/0.51 49[2:Spt:32.1] || -> equal(inverse(sk_c3),sk_c9)**. % 0.19/0.51 55[3:Spt:37.1] || -> equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.19/0.51 57[3:SpL:55.0,48.1] || equal(inverse(sk_c3),sk_c9)** equal(sk_c9,sk_c9) -> . % 0.19/0.51 58[3:Obv:57.1] || equal(inverse(sk_c3),sk_c9)** -> . % 0.19/0.51 59[3:Rew:49.0,58.0] || equal(sk_c9,sk_c9)* -> . % 0.19/0.51 60[3:Obv:59.0] || -> . % 0.19/0.51 61[3:Spt:60.0,37.1,55.0] || equal(multiply(sk_c3,sk_c8),sk_c9)** -> . % 0.19/0.51 62[3:Spt:60.0,37.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.51 63[3:MRR:42.1,61.0] || -> equal(inverse(sk_c6),sk_c9)**. % 0.19/0.51 64[3:MRR:39.1,61.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.51 65[3:MRR:41.1,61.0] || -> equal(multiply(sk_c6,sk_c9),sk_c7)**. % 0.19/0.51 66[3:MRR:40.1,61.0] || -> equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.19/0.51 67[3:MRR:38.1,61.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.51 75[3:SpL:67.0,48.1] || equal(inverse(sk_c5),sk_c9)** equal(sk_c9,sk_c9) -> . % 0.19/0.51 76[3:Obv:75.1] || equal(inverse(sk_c5),sk_c9)** -> . % 0.19/0.51 77[3:Rew:64.0,76.0] || equal(sk_c9,sk_c8)** -> . % 0.19/0.51 88[1:SpL:45.0,48.1] || equal(inverse(inverse(sk_c8)),sk_c9)** equal(sk_c9,identity) -> . % 0.19/0.51 102[0:SpR:45.0,46.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.51 110[0:Rew:44.0,102.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.51 125[0:SpR:110.0,110.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.51 128[3:SpR:65.0,110.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c9)**. % 0.19/0.51 136[0:SpR:44.0,110.0] || -> equal(multiply(inverse(identity),u),u)**. % 0.19/0.51 137[0:SpR:45.0,110.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.51 149[3:Rew:66.0,128.0,63.0,128.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.51 150[3:MRR:149.0,77.0] || -> . % 0.19/0.51 179[0:Rew:125.0,137.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.51 185[2:Spt:150.0,32.1,49.0] || equal(inverse(sk_c3),sk_c9)** -> . % 0.19/0.51 186[2:Spt:150.0,32.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.51 187[2:MRR:35.1,185.0] || -> equal(inverse(sk_c6),sk_c9)**. % 0.19/0.51 189[2:MRR:34.0,185.0] || -> equal(multiply(sk_c6,sk_c9),sk_c7)**. % 0.19/0.51 190[2:MRR:33.0,185.0] || -> equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.19/0.51 191[2:MRR:31.0,185.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.51 193[2:SpR:186.0,45.0] || -> equal(multiply(sk_c8,sk_c5),identity)**. % 0.19/0.51 203[2:SpR:189.0,110.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c9)**. % 0.19/0.51 205[2:Rew:187.0,203.0] || -> equal(multiply(sk_c9,sk_c7),sk_c9)**. % 0.19/0.51 206[2:Rew:190.0,205.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.51 214[2:Rew:206.0,191.0] || -> equal(multiply(sk_c5,sk_c8),sk_c8)**. % 0.19/0.51 216[2:Rew:206.0,88.0] || equal(inverse(inverse(sk_c8)),sk_c8)** equal(sk_c9,identity) -> . % 0.19/0.51 222[2:Rew:206.0,216.1] || equal(inverse(inverse(sk_c8)),sk_c8)** equal(identity,sk_c8) -> . % 0.19/0.51 230[2:SpR:193.0,110.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c5)**. % 0.19/0.51 232[2:Rew:179.0,230.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.19/0.51 233[2:Rew:232.0,222.0] || equal(inverse(sk_c5),sk_c8)** equal(identity,sk_c8) -> . % 0.19/0.51 235[2:Rew:186.0,233.0] || equal(sk_c8,sk_c8) equal(identity,sk_c8)** -> . % 0.19/0.51 236[2:Obv:235.0] || equal(identity,sk_c8)** -> . % 0.19/0.51 237[2:SpR:232.0,45.0] || -> equal(multiply(sk_c5,sk_c8),identity)**. % 0.19/0.51 240[2:Rew:214.0,237.0] || -> equal(identity,sk_c8)**. % 0.19/0.51 241[2:MRR:240.0,236.0] || -> . % 0.19/0.51 242[1:Spt:241.0,47.0,47.1,47.3,47.4,47.5,47.6,47.8,47.9,47.10] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c8) equal(inverse(w),sk_c9) equal(inverse(x),sk_c10) equal(multiply(u,sk_c9),y)*+ equal(multiply(v,sk_c8),sk_c9)** equal(multiply(w,sk_c9),sk_c8)** equal(multiply(x,sk_c10),sk_c9)** equal(multiply(sk_c9,y),sk_c8)** -> . % 0.19/0.51 243[1:EqR:242.4] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c8) equal(inverse(w),sk_c9) equal(inverse(x),sk_c10) equal(multiply(v,sk_c8),sk_c9)** equal(multiply(w,sk_c9),sk_c8)** equal(multiply(x,sk_c10),sk_c9)** equal(multiply(sk_c9,multiply(u,sk_c9)),sk_c8)** -> . % 0.19/0.51 245[1:SpL:45.0,242.4] || equal(inverse(inverse(sk_c9)),sk_c9) equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c10) equal(identity,x) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(sk_c9,x),sk_c8)** -> . % 0.19/0.51 247[2:Spt:11.1] || -> equal(inverse(sk_c1),sk_c10)**. % 0.19/0.51 248[2:SpR:247.0,45.0] || -> equal(multiply(sk_c10,sk_c1),identity)**. % 0.19/0.51 251[3:Spt:25.1] || -> equal(inverse(sk_c2),sk_c9)**. % 0.19/0.51 252[3:SpR:251.0,45.0] || -> equal(multiply(sk_c9,sk_c2),identity)**. % 0.19/0.51 259[4:Spt:16.1] || -> equal(multiply(sk_c2,sk_c9),sk_c8)**. % 0.19/0.51 260[4:SpR:259.0,46.0] || -> equal(multiply(sk_c2,multiply(sk_c9,u)),multiply(sk_c8,u))**. % 0.19/0.51 267[5:Spt:2.1] || -> equal(multiply(sk_c1,sk_c10),sk_c9)**. % 0.19/0.51 273[2:SpR:248.0,110.0] || -> equal(multiply(inverse(sk_c10),identity),sk_c1)**. % 0.19/0.51 275[2:Rew:179.0,273.0] || -> equal(inverse(sk_c10),sk_c1)**. % 0.19/0.51 283[3:SpR:252.0,110.0] || -> equal(multiply(inverse(sk_c9),identity),sk_c2)**. % 0.19/0.51 285[3:Rew:179.0,283.0] || -> equal(inverse(sk_c9),sk_c2)**. % 0.19/0.51 286[3:Rew:285.0,245.0] || equal(inverse(sk_c2),sk_c9) equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c10) equal(identity,x) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(sk_c9,x),sk_c8)** -> . % 0.19/0.51 288[3:Rew:251.0,286.0] || equal(sk_c9,sk_c9) equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c10) equal(identity,x) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(sk_c9,x),sk_c8)** -> . % 0.19/0.51 289[3:Obv:288.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c10) equal(identity,x) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(sk_c9,x),sk_c8)** -> . % 0.19/0.51 290[2:SpR:275.0,45.0] || -> equal(multiply(sk_c1,sk_c10),identity)**. % 0.19/0.51 291[2:SpR:275.0,110.0] || -> equal(multiply(sk_c1,multiply(sk_c10,u)),u)**. % 0.19/0.51 293[5:Rew:267.0,290.0] || -> equal(sk_c9,identity)**. % 0.19/0.51 295[5:Rew:293.0,251.0] || -> equal(inverse(sk_c2),identity)**. % 0.19/0.51 297[5:Rew:293.0,259.0] || -> equal(multiply(sk_c2,identity),sk_c8)**. % 0.19/0.51 298[5:Rew:293.0,267.0] || -> equal(multiply(sk_c1,sk_c10),identity)**. % 0.19/0.51 300[5:Rew:293.0,252.0] || -> equal(multiply(identity,sk_c2),identity)**. % 0.19/0.51 303[5:Rew:293.0,289.1] || equal(inverse(u),sk_c8) equal(inverse(v),identity) equal(inverse(w),sk_c10) equal(identity,x) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(sk_c9,x),sk_c8)** -> . % 0.19/0.51 315[5:Rew:293.0,285.0] || -> equal(inverse(identity),sk_c2)**. % 0.19/0.51 316[5:Rew:315.0,136.0] || -> equal(multiply(sk_c2,u),u)**. % 0.19/0.51 317[5:Rew:179.0,297.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.51 318[5:Rew:317.0,295.0] || -> equal(inverse(sk_c8),identity)**. % 0.19/0.51 320[5:Rew:44.0,300.0] || -> equal(identity,sk_c2)**. % 0.19/0.51 321[5:Rew:317.0,320.0] || -> equal(identity,sk_c8)**. % 0.19/0.51 325[5:Rew:321.0,179.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.51 326[5:Rew:321.0,293.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.51 328[5:Rew:321.0,318.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.51 330[5:Rew:321.0,298.0] || -> equal(multiply(sk_c1,sk_c10),sk_c8)**. % 0.19/0.51 336[5:Rew:317.0,316.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.51 345[5:Rew:336.0,303.7,326.0,303.7,326.0,303.6,325.0,303.5,326.0,303.5,325.0,303.4,326.0,303.4,321.0,303.3,321.0,303.1] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c10) equal(sk_c8,x)* equal(u,sk_c8) equal(v,sk_c8) equal(multiply(w,sk_c10),sk_c8)** equal(x,sk_c8)* -> . % 0.19/0.51 346[5:Obv:345.3] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c10) equal(u,sk_c8) equal(v,sk_c8) equal(multiply(w,sk_c10),sk_c8)** equal(x,sk_c8)* -> . % 0.19/0.51 347[5:Con:346.1] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c10) equal(u,sk_c8) equal(multiply(v,sk_c10),sk_c8)**+ -> . % 0.19/0.51 586[5:SpL:330.0,347.3] || equal(inverse(u),sk_c8)** equal(inverse(sk_c1),sk_c10)** equal(u,sk_c8) equal(sk_c8,sk_c8) -> . % 0.19/0.51 589[5:Obv:586.3] || equal(inverse(u),sk_c8)** equal(inverse(sk_c1),sk_c10)** equal(u,sk_c8) -> . % 0.19/0.51 590[5:Rew:247.0,589.1] || equal(inverse(u),sk_c8)** equal(sk_c10,sk_c10) equal(u,sk_c8) -> . % 0.19/0.51 591[5:Obv:590.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.51 681[5:SpL:328.0,591.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.51 685[5:Obv:681.1] || -> . % 0.19/0.51 686[5:Spt:685.0,2.1,267.0] || equal(multiply(sk_c1,sk_c10),sk_c9)** -> . % 0.19/0.51 687[5:Spt:685.0,2.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.51 688[5:Rew:290.0,686.0] || equal(sk_c9,identity)** -> . % 0.19/0.51 691[2:Rew:290.0,7.1] || -> equal(inverse(sk_c6),sk_c9)** equal(sk_c9,identity). % 0.19/0.51 693[2:Rew:290.0,4.1] || -> equal(inverse(sk_c5),sk_c8)** equal(sk_c9,identity). % 0.19/0.51 694[5:MRR:693.1,688.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.51 696[2:Rew:290.0,6.1] || -> equal(multiply(sk_c6,sk_c9),sk_c7)** equal(sk_c9,identity). % 0.19/0.51 698[2:Rew:290.0,5.1] || -> equal(multiply(sk_c9,sk_c7),sk_c8)** equal(sk_c9,identity). % 0.19/0.51 700[2:Rew:290.0,3.1] || -> equal(multiply(sk_c5,sk_c8),sk_c9)** equal(sk_c9,identity). % 0.19/0.51 701[5:MRR:700.1,688.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.51 702[2:Rew:290.0,1.1] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(sk_c9,identity). % 0.19/0.51 703[5:MRR:702.1,688.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.51 711[3:SpR:285.0,110.0] || -> equal(multiply(sk_c2,multiply(sk_c9,u)),u)**. % 0.19/0.51 713[4:Rew:260.0,711.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.51 717[5:SpR:694.0,110.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),u)**. % 0.19/0.51 719[5:Rew:713.0,717.0] || -> equal(multiply(sk_c5,u),u)**. % 0.19/0.51 720[5:Rew:719.0,701.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.51 724[5:Rew:720.0,688.0] || equal(identity,sk_c8)** -> . % 0.19/0.51 726[5:Rew:720.0,252.0] || -> equal(multiply(sk_c8,sk_c2),identity)**. % 0.19/0.51 734[5:Rew:720.0,703.0] || -> equal(multiply(sk_c4,sk_c10),sk_c8)**. % 0.19/0.51 743[5:Rew:713.0,726.0] || -> equal(identity,sk_c2)**. % 0.19/0.51 744[5:Rew:743.0,290.0] || -> equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.19/0.51 750[5:Rew:743.0,724.0] || equal(sk_c2,sk_c8)** -> . % 0.19/0.51 788[5:SpR:734.0,110.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c10)**. % 0.19/0.51 790[5:Rew:687.0,788.0] || -> equal(multiply(sk_c10,sk_c8),sk_c10)**. % 0.19/0.51 805[5:SpR:790.0,110.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c8)**. % 0.19/0.51 810[5:Rew:744.0,805.0,275.0,805.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.51 811[5:MRR:810.0,750.0] || -> . % 0.19/0.51 813[4:Spt:811.0,16.1,259.0] || equal(multiply(sk_c2,sk_c9),sk_c8)** -> . % 0.19/0.51 814[4:Spt:811.0,16.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.51 819[2:Rew:179.0,21.1,691.1,21.1] || -> equal(inverse(sk_c6),sk_c9)** equal(sk_c2,sk_c8). % 0.19/0.51 820[2:Rew:179.0,18.1,693.1,18.1] || -> equal(inverse(sk_c5),sk_c8)** equal(sk_c2,sk_c8). % 0.19/0.51 829[2:Rew:179.0,20.1,696.1,20.1] || -> equal(multiply(sk_c6,sk_c9),sk_c7)** equal(sk_c2,sk_c8). % 0.19/0.51 830[2:Rew:179.0,19.1,698.1,19.1] || -> equal(multiply(sk_c9,sk_c7),sk_c8)** equal(sk_c2,sk_c8). % 0.19/0.51 831[2:Rew:179.0,17.1,700.1,17.1] || -> equal(multiply(sk_c5,sk_c8),sk_c9)** equal(sk_c2,sk_c8). % 0.19/0.51 832[2:Rew:179.0,15.1,702.1,15.1] || -> equal(multiply(sk_c4,sk_c10),sk_c9)** equal(sk_c2,sk_c8). % 0.19/0.51 894[0:SpR:45.0,110.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.51 895[0:SpR:45.0,179.0] || -> equal(inverse(identity),identity)**. % 0.19/0.51 899[4:SpR:814.0,45.0] || -> equal(multiply(sk_c10,sk_c4),identity)**. % 0.19/0.51 900[3:SpR:285.0,45.0] || -> equal(multiply(sk_c2,sk_c9),identity)**. % 0.19/0.51 904[4:Rew:900.0,813.0] || equal(identity,sk_c8)** -> . % 0.19/0.51 905[0:Rew:179.0,894.0] || -> equal(inverse(inverse(u)),u)**. % 0.19/0.51 915[4:SpR:899.0,291.0] || -> equal(multiply(sk_c1,identity),sk_c4)**. % 0.19/0.51 916[4:Rew:179.0,915.0] || -> equal(sk_c4,sk_c1)**. % 0.19/0.51 920[4:Rew:916.0,832.0] || -> equal(multiply(sk_c1,sk_c10),sk_c9)** equal(sk_c2,sk_c8). % 0.19/0.51 921[4:Rew:916.0,702.0] || -> equal(multiply(sk_c1,sk_c10),sk_c9)** equal(sk_c9,identity). % 0.19/0.51 924[4:Rew:290.0,920.0] || -> equal(sk_c9,identity)** equal(sk_c2,sk_c8). % 0.19/0.51 925[4:Rew:924.0,819.0] || -> equal(inverse(sk_c6),identity)** equal(sk_c2,sk_c8). % 0.19/0.51 926[4:Rew:924.0,829.0] || -> equal(multiply(sk_c6,identity),sk_c7)** equal(sk_c2,sk_c8). % 0.19/0.51 927[4:Rew:924.0,830.0] || -> equal(multiply(identity,sk_c7),sk_c8)** equal(sk_c2,sk_c8). % 0.19/0.51 928[4:Rew:924.0,831.0] || -> equal(multiply(sk_c5,sk_c8),identity)** equal(sk_c2,sk_c8). % 0.19/0.51 929[4:Rew:290.0,921.0] || -> equal(sk_c9,identity)** equal(sk_c9,identity)**. % 0.19/0.51 930[4:Obv:929.0] || -> equal(sk_c9,identity)**. % 0.19/0.51 931[4:Rew:930.0,285.0] || -> equal(inverse(identity),sk_c2)**. % 0.19/0.51 946[4:Rew:895.0,931.0] || -> equal(identity,sk_c2)**. % 0.19/0.51 947[4:Rew:946.0,44.0] || -> equal(multiply(sk_c2,u),u)**. % 0.19/0.51 950[4:Rew:946.0,179.0] || -> equal(multiply(u,sk_c2),u)**. % 0.19/0.51 953[4:Rew:946.0,904.0] || equal(sk_c2,sk_c8)** -> . % 0.19/0.51 955[4:Rew:946.0,925.0] || -> equal(inverse(sk_c6),sk_c2)** equal(sk_c2,sk_c8). % 0.19/0.51 958[4:MRR:820.1,953.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.51 963[4:MRR:955.1,953.0] || -> equal(inverse(sk_c6),sk_c2)**. % 0.19/0.51 964[4:Rew:950.0,926.0,946.0,926.0] || -> equal(sk_c6,sk_c7) equal(sk_c2,sk_c8)**. % 0.19/0.51 965[4:MRR:964.1,953.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.51 966[4:Rew:965.0,963.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.19/0.51 967[4:Rew:947.0,927.0,946.0,927.0] || -> equal(sk_c7,sk_c8) equal(sk_c2,sk_c8)**. % 0.19/0.51 968[4:MRR:967.1,953.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.51 970[4:Rew:968.0,966.0] || -> equal(inverse(sk_c8),sk_c2)**. % 0.19/0.51 971[4:Rew:946.0,928.0] || -> equal(multiply(sk_c5,sk_c8),sk_c2)** equal(sk_c2,sk_c8). % 0.19/0.51 972[4:MRR:971.1,953.0] || -> equal(multiply(sk_c5,sk_c8),sk_c2)**. % 0.19/0.51 994[4:SpR:958.0,110.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),u)**. % 0.19/0.51 996[4:SpR:970.0,110.0] || -> equal(multiply(sk_c2,multiply(sk_c8,u)),u)**. % 0.19/0.51 998[4:Rew:947.0,996.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.51 999[4:Rew:998.0,994.0] || -> equal(multiply(sk_c5,u),u)**. % 0.19/0.51 1000[4:Rew:999.0,972.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.51 1001[4:MRR:1000.0,953.0] || -> . % 0.19/0.51 1002[3:Spt:1001.0,25.1,251.0] || equal(inverse(sk_c2),sk_c9)** -> . % 0.19/0.51 1003[3:Spt:1001.0,25.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.51 1005[2:Rew:819.1,28.1,691.1,28.1] || -> equal(inverse(sk_c6),sk_c9)** equal(inverse(sk_c8),identity). % 0.19/0.51 1006[3:MRR:23.1,1002.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.51 1011[2:Rew:829.1,27.0,696.1,27.0] || -> equal(inverse(sk_c8),identity) equal(multiply(sk_c6,sk_c9),sk_c7)**. % 0.19/0.51 1012[2:Rew:830.1,26.0,698.1,26.0] || -> equal(inverse(sk_c8),identity) equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.19/0.51 1014[2:Rew:832.1,22.0,702.1,22.0] || -> equal(inverse(sk_c8),identity) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.51 1015[1:Rew:905.0,245.0] || equal(sk_c9,sk_c9) equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c10) equal(identity,x) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(sk_c9,x),sk_c8)** -> . % 0.19/0.51 1016[1:Obv:1015.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c10) equal(identity,x) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(sk_c9,x),sk_c8)** -> . % 0.19/0.51 1036[0:SpR:905.0,110.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.19/0.51 1041[3:SpR:1003.0,905.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.19/0.51 1043[3:SpR:1006.0,905.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.19/0.51 1044[3:Rew:1041.0,1014.0] || -> equal(identity,sk_c5) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.51 1046[3:Rew:1041.0,1012.0] || -> equal(identity,sk_c5) equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.19/0.51 1047[3:Rew:1041.0,1011.0] || -> equal(identity,sk_c5) equal(multiply(sk_c6,sk_c9),sk_c7)**. % 0.19/0.51 1048[3:Rew:1041.0,1005.1] || -> equal(inverse(sk_c6),sk_c9)** equal(identity,sk_c5). % 0.19/0.51 1049[3:Rew:275.0,1043.0] || -> equal(sk_c4,sk_c1)**. % 0.19/0.51 1054[3:Rew:1049.0,702.0] || -> equal(multiply(sk_c1,sk_c10),sk_c9)** equal(sk_c9,identity). % 0.19/0.51 1059[3:Rew:1049.0,1044.1] || -> equal(identity,sk_c5) equal(multiply(sk_c1,sk_c10),sk_c9)**. % 0.19/0.51 1060[3:Rew:290.0,1059.1] || -> equal(identity,sk_c5) equal(sk_c9,identity)**. % 0.19/0.51 1061[3:Rew:1060.1,1048.0] || -> equal(inverse(sk_c6),identity)** equal(identity,sk_c5). % 0.19/0.51 1063[3:Rew:44.0,1046.1,1060.1,1046.1] || -> equal(identity,sk_c5)** equal(sk_c7,sk_c8). % 0.19/0.51 1064[3:Rew:179.0,1047.1,1060.1,1047.1,1063.1,1047.1] || -> equal(identity,sk_c5)** equal(sk_c6,sk_c8). % 0.19/0.51 1065[3:Rew:1064.1,1061.0] || -> equal(inverse(sk_c8),identity)** equal(identity,sk_c5). % 0.19/0.51 1066[3:Rew:1041.0,1065.0] || -> equal(identity,sk_c5)** equal(identity,sk_c5)**. % 0.19/0.51 1067[3:Obv:1066.0] || -> equal(identity,sk_c5)**. % 0.19/0.51 1068[3:Rew:1067.0,895.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.51 1069[3:Rew:1067.0,290.0] || -> equal(multiply(sk_c1,sk_c10),sk_c5)**. % 0.19/0.51 1071[3:Rew:1067.0,179.0] || -> equal(multiply(u,sk_c5),u)**. % 0.19/0.51 1072[3:Rew:1067.0,44.0] || -> equal(multiply(sk_c5,u),u)**. % 0.19/0.51 1084[3:Rew:1067.0,1016.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c9) equal(inverse(w),sk_c10) equal(sk_c5,x) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(w,sk_c10),sk_c9)** equal(multiply(sk_c9,x),sk_c8)** -> . % 0.19/0.51 1085[3:Rew:1003.0,1068.0] || -> equal(sk_c8,sk_c5)**. % 0.19/0.51 1086[3:Rew:1085.0,1003.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.51 1099[3:Rew:1067.0,1054.1,1069.0,1054.0] || -> equal(sk_c9,sk_c5)** equal(sk_c9,sk_c5)**. % 0.19/0.51 1100[3:Obv:1099.0] || -> equal(sk_c9,sk_c5)**. % 0.19/0.51 1122[3:Rew:1072.0,1084.7,1100.0,1084.7,1085.0,1084.7,1100.0,1084.6,1071.0,1084.5,1100.0,1084.5,1085.0,1084.5,1071.0,1084.4,1085.0,1084.4,1100.0,1084.4,1100.0,1084.1,1085.0,1084.0] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c5)** equal(inverse(w),sk_c10) equal(sk_c5,x)* equal(u,sk_c5) equal(v,sk_c5) equal(multiply(w,sk_c10),sk_c5)** equal(x,sk_c5)* -> . % 0.19/0.51 1123[3:Obv:1122.3] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c5)** equal(inverse(w),sk_c10) equal(u,sk_c5) equal(v,sk_c5) equal(multiply(w,sk_c10),sk_c5)** equal(x,sk_c5)* -> . % 0.19/0.51 1124[3:Con:1123.1] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c10) equal(u,sk_c5) equal(multiply(v,sk_c10),sk_c5)**+ -> . % 0.19/0.51 1367[3:SpL:1069.0,1124.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c1),sk_c10)** equal(u,sk_c5) equal(sk_c5,sk_c5) -> . % 0.19/0.51 1371[3:Obv:1367.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c1),sk_c10)** equal(u,sk_c5) -> . % 0.19/0.51 1372[3:Rew:247.0,1371.1] || equal(inverse(u),sk_c5)** equal(sk_c10,sk_c10) equal(u,sk_c5) -> . % 0.19/0.51 1373[3:Obv:1372.1] || equal(inverse(u),sk_c5)** equal(u,sk_c5) -> . % 0.19/0.51 1450[3:SpL:1086.0,1373.0] || equal(sk_c5,sk_c5)* equal(sk_c5,sk_c5)* -> . % 0.19/0.51 1453[3:Obv:1450.1] || -> . % 0.19/0.51 1454[2:Spt:1453.0,11.1,247.0] || equal(inverse(sk_c1),sk_c10)** -> . % 0.19/0.51 1455[2:Spt:1453.0,11.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.51 1456[2:MRR:14.1,1454.0] || -> equal(inverse(sk_c6),sk_c9)**. % 0.19/0.51 1457[2:MRR:9.1,1454.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.51 1459[2:MRR:13.0,1454.0] || -> equal(multiply(sk_c6,sk_c9),sk_c7)**. % 0.19/0.51 1460[2:MRR:12.0,1454.0] || -> equal(multiply(sk_c9,sk_c7),sk_c8)**. % 0.19/0.51 1461[2:MRR:10.0,1454.0] || -> equal(multiply(sk_c5,sk_c8),sk_c9)**. % 0.19/0.51 1464[2:SpR:1455.0,905.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.19/0.51 1465[2:SpR:1455.0,1036.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.19/0.51 1468[2:SpR:1456.0,905.0] || -> equal(inverse(sk_c9),sk_c6)**. % 0.19/0.51 1478[2:SpR:1457.0,905.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.19/0.51 1493[2:SpR:1459.0,46.0] || -> equal(multiply(sk_c6,multiply(sk_c9,u)),multiply(sk_c7,u))**. % 0.19/0.51 1494[2:SpR:1459.0,110.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c9)**. % 0.19/0.51 1496[2:Rew:1456.0,1494.0] || -> equal(multiply(sk_c9,sk_c7),sk_c9)**. % 0.19/0.51 1497[2:Rew:1460.0,1496.0] || -> equal(sk_c9,sk_c8)**. % 0.19/0.51 1499[2:Rew:1497.0,1468.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.19/0.51 1500[2:Rew:1497.0,1459.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.19/0.51 1502[2:Rew:1497.0,1461.0] || -> equal(multiply(sk_c5,sk_c8),sk_c8)**. % 0.19/0.51 1508[2:Rew:1497.0,243.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c9) equal(inverse(x),sk_c10) equal(multiply(v,sk_c8),sk_c9)** equal(multiply(w,sk_c9),sk_c8)** equal(multiply(x,sk_c10),sk_c9)** equal(multiply(sk_c9,multiply(u,sk_c9)),sk_c8)** -> . % 0.19/0.51 1511[2:Rew:1464.0,1499.0] || -> equal(sk_c6,sk_c5)**. % 0.19/0.51 1513[2:Rew:1511.0,1500.0] || -> equal(multiply(sk_c5,sk_c8),sk_c7)**. % 0.19/0.51 1514[2:Rew:1513.0,1502.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.51 1519[2:Rew:1465.0,1493.0,1511.0,1493.0,1497.0,1493.0,1514.0,1493.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.51 1524[2:Rew:1519.0,1508.7,1497.0,1508.7,1497.0,1508.6,1497.0,1508.5,1497.0,1508.4,1497.0,1508.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(x),sk_c10) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** equal(multiply(x,sk_c10),sk_c8)** equal(multiply(u,sk_c8),sk_c8)** -> . % 0.19/0.51 1525[2:Con:1524.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c10) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c10),sk_c8)** -> . % 0.19/0.52 1568[2:SpR:1455.0,45.0] || -> equal(multiply(sk_c8,sk_c5),identity)**. % 0.19/0.52 1572[2:SpR:1478.0,45.0] || -> equal(multiply(sk_c4,sk_c10),identity)**. % 0.19/0.52 1573[2:Rew:1519.0,1568.0] || -> equal(identity,sk_c5)**. % 0.19/0.52 1574[2:Rew:1573.0,895.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.52 1576[2:Rew:1573.0,179.0] || -> equal(multiply(u,sk_c5),u)**. % 0.19/0.52 1579[2:Rew:1455.0,1574.0] || -> equal(sk_c8,sk_c5)**. % 0.19/0.52 1580[2:Rew:1579.0,1455.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.52 1587[2:Rew:1579.0,1525.0] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c10) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c10),sk_c8)** -> . % 0.19/0.52 1591[2:Rew:1573.0,1572.0] || -> equal(multiply(sk_c4,sk_c10),sk_c5)**. % 0.19/0.52 1597[2:Rew:1579.0,1587.3,1576.0,1587.2,1579.0,1587.2] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c10) equal(u,sk_c5) equal(multiply(v,sk_c10),sk_c5)**+ -> . % 0.19/0.52 1736[2:SpL:1591.0,1597.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c4),sk_c10)** equal(u,sk_c5) equal(sk_c5,sk_c5) -> . % 0.19/0.52 1738[2:Obv:1736.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c4),sk_c10)** equal(u,sk_c5) -> . % 0.19/0.52 1739[2:Rew:1457.0,1738.1] || equal(inverse(u),sk_c5)** equal(sk_c10,sk_c10) equal(u,sk_c5) -> . % 0.19/0.52 1740[2:Obv:1739.1] || equal(inverse(u),sk_c5)** equal(u,sk_c5) -> . % 0.19/0.52 1745[2:SpL:1580.0,1740.0] || equal(sk_c5,sk_c5)* equal(sk_c5,sk_c5)* -> . % 0.19/0.52 1746[2:Obv:1745.1] || -> . % 0.19/0.52 % SZS output end Refutation % 0.19/0.52 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_10 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_25 prove_this_26 prove_this_27 prove_this_28 prove_this_31 prove_this_32 prove_this_33 prove_this_34 prove_this_35 prove_this_37 prove_this_38 prove_this_39 prove_this_40 prove_this_41 prove_this_42 prove_this_43 left_identity left_inverse associativity % 0.19/0.52 %------------------------------------------------------------------------------