%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP272-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n008.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:37 EDT 2022 % Result : Unsatisfiable 0.20s 0.47s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP272-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n008.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Mon Jun 13 09:21:22 EDT 2022 % 0.14/0.34 % CPUTime : % 0.20/0.47 % 0.20/0.47 SPASS V 3.9 % 0.20/0.47 SPASS beiseite: Proof found. % 0.20/0.47 % SZS status Theorem % 0.20/0.47 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.47 SPASS derived 851 clauses, backtracked 302 clauses, performed 11 splits and kept 688 clauses. % 0.20/0.47 SPASS allocated 63635 KBytes. % 0.20/0.47 SPASS spent 0:00:00.12 on the problem. % 0.20/0.47 0:00:00.04 for the input. % 0.20/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.47 0:00:00.00 for inferences. % 0.20/0.47 0:00:00.00 for the backtracking. % 0.20/0.47 0:00:00.05 for the reduction. % 0.20/0.47 % 0.20/0.47 % 0.20/0.47 Here is a proof with depth 4, length 367 : % 0.20/0.47 % SZS output start Refutation % 0.20/0.47 1[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c1,sk_c7),sk_c6). % 0.20/0.47 2[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 3[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c1,sk_c7),sk_c6). % 0.20/0.47 4[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 5[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6)** equal(multiply(sk_c1,sk_c7),sk_c6). % 0.20/0.47 6[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 7[0:Inp] || -> equal(inverse(sk_c3),sk_c7)** equal(inverse(sk_c1),sk_c7). % 0.20/0.47 8[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 9[0:Inp] || -> equal(inverse(sk_c4),sk_c6)** equal(inverse(sk_c1),sk_c7). % 0.20/0.47 10[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 11[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c7,sk_c5),sk_c6). % 0.20/0.47 12[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.47 13[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c7,sk_c5),sk_c6). % 0.20/0.47 14[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.47 15[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6). % 0.20/0.47 16[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c2,sk_c6),sk_c5). % 0.20/0.47 17[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 19[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 20[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 21[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 22[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 23[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 24[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 25[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 26[0:Inp] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(inverse(x),sk_c7) equal(multiply(u,sk_c5),sk_c6)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c6),sk_c5)** equal(multiply(x,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c7,sk_c5),sk_c6) -> . % 0.20/0.47 27[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.20/0.47 28[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.20/0.47 29[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.20/0.47 30[1:Spt:26.0,26.4] || equal(inverse(u),sk_c6) equal(multiply(u,sk_c5),sk_c6)** -> . % 0.20/0.47 31[2:Spt:11.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 33[3:Spt:14.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 35[4:Spt:12.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 39[5:Spt:15.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 41[5:SpL:39.0,30.1] || equal(inverse(sk_c4),sk_c6)** equal(sk_c6,sk_c6) -> . % 0.20/0.47 42[5:Obv:41.1] || equal(inverse(sk_c4),sk_c6)** -> . % 0.20/0.47 43[5:Rew:33.0,42.0] || equal(sk_c6,sk_c6)* -> . % 0.20/0.47 44[5:Obv:43.0] || -> . % 0.20/0.47 45[5:Spt:44.0,15.0,39.0] || equal(multiply(sk_c4,sk_c5),sk_c6)** -> . % 0.20/0.47 46[5:Spt:44.0,15.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.47 47[5:MRR:25.1,45.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 48[5:MRR:10.1,45.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 49[5:MRR:20.0,45.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 50[5:MRR:5.0,45.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 52[5:SpL:46.0,30.1] || equal(inverse(sk_c7),sk_c6)** equal(sk_c6,sk_c6) -> . % 0.20/0.47 53[5:Obv:52.1] || equal(inverse(sk_c7),sk_c6)** -> . % 0.20/0.47 59[3:SpR:33.0,28.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.20/0.47 60[4:SpR:35.0,28.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.20/0.47 61[5:SpR:47.0,28.0] || -> equal(multiply(sk_c6,sk_c2),identity)**. % 0.20/0.47 62[5:SpR:48.0,28.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.20/0.47 63[1:SpL:28.0,30.1] || equal(inverse(inverse(sk_c5)),sk_c6)** equal(sk_c6,identity) -> . % 0.20/0.47 71[0:SpR:28.0,29.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.47 72[5:SpR:49.0,29.0] || -> equal(multiply(sk_c2,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.20/0.47 73[3:SpR:59.0,29.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),multiply(identity,u))**. % 0.20/0.47 75[3:Rew:27.0,73.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),u)**. % 0.20/0.47 76[0:Rew:27.0,71.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.47 91[0:SpR:76.0,76.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.47 93[5:SpR:46.0,76.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c5)**. % 0.20/0.47 94[2:SpR:31.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 97[0:SpR:28.0,76.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.47 99[3:SpR:59.0,76.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c4)**. % 0.20/0.47 100[5:SpR:61.0,76.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c2)**. % 0.20/0.47 101[3:SpR:75.0,76.0] || -> equal(multiply(inverse(sk_c6),u),multiply(sk_c4,u))**. % 0.20/0.47 103[4:SpR:60.0,76.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c3)**. % 0.20/0.47 104[5:SpR:62.0,76.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.20/0.47 111[5:Rew:99.0,100.0] || -> equal(sk_c2,sk_c4)**. % 0.20/0.47 115[5:Rew:111.0,72.0] || -> equal(multiply(sk_c4,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.20/0.47 117[5:Rew:103.0,104.0] || -> equal(sk_c3,sk_c1)**. % 0.20/0.47 121[5:Rew:117.0,103.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.20/0.47 125[3:Rew:101.0,94.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.20/0.47 127[0:Rew:91.0,97.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.47 128[5:Rew:127.0,121.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.20/0.47 129[5:Rew:128.0,53.0] || equal(sk_c6,sk_c1)** -> . % 0.20/0.47 130[5:Rew:128.0,93.0] || -> equal(multiply(sk_c1,sk_c6),sk_c5)**. % 0.20/0.47 134[5:SpR:128.0,28.0] || -> equal(multiply(sk_c1,sk_c7),identity)**. % 0.20/0.47 137[5:Rew:50.0,134.0] || -> equal(sk_c6,identity)**. % 0.20/0.47 139[5:Rew:137.0,31.0] || -> equal(multiply(identity,sk_c7),sk_c5)**. % 0.20/0.47 141[5:Rew:137.0,46.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.20/0.47 143[5:Rew:137.0,59.0] || -> equal(multiply(identity,sk_c4),identity)**. % 0.20/0.47 150[5:Rew:137.0,115.0] || -> equal(multiply(sk_c4,multiply(identity,u)),multiply(sk_c5,u))**. % 0.20/0.47 157[5:Rew:137.0,129.0] || equal(identity,sk_c1)** -> . % 0.20/0.47 158[5:Rew:137.0,130.0] || -> equal(multiply(sk_c1,identity),sk_c5)**. % 0.20/0.47 159[5:Rew:27.0,139.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 161[5:Rew:159.0,141.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.20/0.47 162[5:Rew:27.0,143.0] || -> equal(identity,sk_c4)**. % 0.20/0.47 163[5:Rew:162.0,27.0] || -> equal(multiply(sk_c4,u),u)**. % 0.20/0.47 167[5:Rew:162.0,127.0] || -> equal(multiply(u,sk_c4),u)**. % 0.20/0.47 171[5:Rew:162.0,157.0] || equal(sk_c4,sk_c1)** -> . % 0.20/0.47 172[5:Rew:162.0,161.0] || -> equal(multiply(sk_c7,sk_c7),sk_c4)**. % 0.20/0.47 177[5:Rew:162.0,158.0,159.0,158.0] || -> equal(multiply(sk_c1,sk_c4),sk_c7)**. % 0.20/0.47 184[5:Rew:167.0,177.0] || -> equal(sk_c7,sk_c1)**. % 0.20/0.47 188[5:Rew:184.0,159.0] || -> equal(sk_c5,sk_c1)**. % 0.20/0.47 191[5:Rew:184.0,172.0] || -> equal(multiply(sk_c1,sk_c1),sk_c4)**. % 0.20/0.47 201[5:Rew:163.0,150.0,163.0,150.0,162.0,150.0,188.0,150.0] || -> equal(multiply(sk_c1,u),u)**. % 0.20/0.47 203[5:Rew:201.0,191.0] || -> equal(sk_c4,sk_c1)**. % 0.20/0.47 204[5:MRR:203.0,171.0] || -> . % 0.20/0.47 210[4:Spt:204.0,12.0,35.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.20/0.47 211[4:Spt:204.0,12.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.47 212[4:MRR:22.0,210.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 213[4:MRR:7.0,210.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 214[4:MRR:17.0,210.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 215[4:MRR:2.0,210.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 239[4:SpR:214.0,76.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.47 241[4:Rew:212.0,239.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 243[4:SpR:215.0,76.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.47 245[4:Rew:213.0,243.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 247[4:SpR:241.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.47 249[4:Rew:101.0,247.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 254[4:SpR:245.0,76.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.47 256[4:Rew:28.0,254.0] || -> equal(sk_c6,identity)**. % 0.20/0.47 260[4:Rew:256.0,59.0] || -> equal(multiply(identity,sk_c4),identity)**. % 0.20/0.47 263[4:Rew:256.0,215.0] || -> equal(multiply(sk_c1,sk_c7),identity)**. % 0.20/0.47 264[4:Rew:256.0,241.0] || -> equal(multiply(identity,sk_c5),identity)**. % 0.20/0.47 265[4:Rew:256.0,245.0] || -> equal(multiply(sk_c7,identity),sk_c7)**. % 0.20/0.47 270[4:Rew:256.0,63.0] || equal(inverse(inverse(sk_c5)),identity)** equal(sk_c6,identity) -> . % 0.20/0.47 278[4:Rew:256.0,249.0] || -> equal(multiply(sk_c4,identity),sk_c5)**. % 0.20/0.47 280[4:Rew:27.0,260.0] || -> equal(identity,sk_c4)**. % 0.20/0.47 282[4:Rew:280.0,127.0] || -> equal(multiply(u,sk_c4),u)**. % 0.20/0.47 285[4:Rew:280.0,256.0] || -> equal(sk_c6,sk_c4)**. % 0.20/0.47 291[4:Rew:280.0,263.0] || -> equal(multiply(sk_c1,sk_c7),sk_c4)**. % 0.20/0.47 292[4:Rew:280.0,264.0] || -> equal(multiply(sk_c4,sk_c5),sk_c4)**. % 0.20/0.47 293[4:Rew:125.0,292.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.47 296[4:Rew:293.0,280.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 297[4:Rew:293.0,285.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 302[4:Rew:293.0,291.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.20/0.47 303[4:Rew:296.0,265.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 304[4:Rew:303.0,278.0,293.0,278.0,296.0,278.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 307[4:Rew:293.0,282.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 313[4:Rew:307.0,302.0] || -> equal(sk_c7,sk_c1)**. % 0.20/0.47 314[4:Rew:313.0,213.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.20/0.47 317[4:Rew:313.0,296.0] || -> equal(identity,sk_c1)**. % 0.20/0.47 318[4:Rew:313.0,297.0] || -> equal(sk_c6,sk_c1)**. % 0.20/0.47 320[4:Rew:313.0,304.0] || -> equal(sk_c5,sk_c1)**. % 0.20/0.47 339[4:Rew:318.0,270.1,317.0,270.1,314.0,270.0,314.0,270.0,320.0,270.0,317.0,270.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.20/0.47 340[4:Obv:339.1] || -> . % 0.20/0.47 343[3:Spt:340.0,14.0,33.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.20/0.47 344[3:Spt:340.0,14.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.47 345[3:MRR:24.0,343.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 346[3:MRR:9.0,343.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 347[3:MRR:19.0,343.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 348[3:MRR:4.0,343.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 360[3:SpR:347.0,76.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.47 362[3:Rew:345.0,360.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 364[3:SpR:348.0,76.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.47 366[3:Rew:346.0,364.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 368[3:SpR:362.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.47 370[3:Rew:28.0,368.0] || -> equal(identity,sk_c5)**. % 0.20/0.47 372[3:Rew:370.0,127.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.47 376[3:Rew:370.0,63.1] || equal(inverse(inverse(sk_c5)),sk_c6)** equal(sk_c6,sk_c5) -> . % 0.20/0.47 380[3:Rew:372.0,344.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 385[3:Rew:380.0,31.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.20/0.47 388[3:Rew:380.0,348.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.20/0.47 392[3:Rew:380.0,366.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 394[3:Rew:385.0,392.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 397[3:Rew:394.0,372.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 401[3:Rew:397.0,388.0] || -> equal(sk_c7,sk_c1)**. % 0.20/0.47 402[3:Rew:401.0,346.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.20/0.47 403[3:Rew:401.0,380.0] || -> equal(sk_c6,sk_c1)**. % 0.20/0.47 407[3:Rew:401.0,394.0] || -> equal(sk_c5,sk_c1)**. % 0.20/0.47 426[3:Rew:403.0,376.1,407.0,376.1,402.0,376.0,402.0,376.0,407.0,376.0,403.0,376.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.20/0.47 427[3:Obv:426.1] || -> . % 0.20/0.47 429[2:Spt:427.0,11.0,31.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.20/0.47 430[2:Spt:427.0,11.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.47 431[2:MRR:21.1,429.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 432[2:MRR:6.1,429.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 433[2:MRR:16.0,429.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 434[2:MRR:1.0,429.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 443[2:SpR:433.0,76.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.47 445[2:Rew:431.0,443.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 447[2:SpR:434.0,76.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.47 449[2:Rew:432.0,447.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 451[2:SpR:445.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.47 453[2:Rew:28.0,451.0] || -> equal(identity,sk_c5)**. % 0.20/0.47 454[2:Rew:453.0,127.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.47 456[2:Rew:453.0,28.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.20/0.47 460[2:Rew:454.0,430.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 466[2:Rew:460.0,429.0] || equal(multiply(sk_c7,sk_c7),sk_c5)** -> . % 0.20/0.47 472[2:Rew:460.0,449.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 473[2:Rew:472.0,466.0] || equal(sk_c5,sk_c7)** -> . % 0.20/0.47 498[2:SpR:472.0,76.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.20/0.47 500[2:Rew:456.0,498.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 501[2:MRR:500.0,473.0] || -> . % 0.20/0.47 502[1:Spt:501.0,26.1,26.2,26.3,26.5,26.6,26.7,26.8,26.9] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c7)**+ equal(multiply(v,sk_c6),sk_c5)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c7,sk_c5),sk_c6) -> . % 0.20/0.47 504[2:Spt:11.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 505[2:Rew:504.0,502.6] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c6),sk_c5)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c5,sk_c5) equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.20/0.47 507[2:Obv:505.6] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c6),sk_c5)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.20/0.47 510[2:SpR:504.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 512[3:Spt:12.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.47 514[3:Rew:512.0,507.6] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c6),sk_c5)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c6,sk_c6) -> . % 0.20/0.47 515[3:Obv:514.6] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c6),sk_c5)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.20/0.47 518[3:SpR:512.0,76.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c5)**. % 0.20/0.47 520[4:Spt:24.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 521[4:SpR:520.0,76.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),u)**. % 0.20/0.47 526[5:Spt:22.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 527[5:SpR:526.0,76.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.20/0.47 529[6:Spt:25.1] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 531[6:SpR:529.0,76.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.47 533[6:Rew:520.0,531.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 534[7:Spt:23.1] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 536[7:SpR:534.0,76.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.47 538[7:Rew:526.0,536.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 540[6:SpR:533.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.47 542[6:Rew:510.0,540.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 543[6:Rew:542.0,504.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.20/0.47 545[6:Rew:542.0,520.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.47 546[6:Rew:542.0,529.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.20/0.47 549[6:Rew:542.0,510.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c7)**. % 0.20/0.47 551[6:Rew:542.0,515.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c6),sk_c5)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.20/0.47 553[6:Rew:542.0,518.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.20/0.47 558[7:Rew:542.0,538.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 559[7:Rew:543.0,558.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 562[7:Rew:559.0,546.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7)**. % 0.20/0.47 563[7:Rew:28.0,549.0,559.0,549.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 565[7:Rew:563.0,127.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 569[7:Rew:565.0,562.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.47 571[7:Rew:569.0,545.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 582[7:Rew:565.0,551.5,542.0,551.5,565.0,551.4,542.0,551.4,559.0,551.4,565.0,551.3,542.0,551.3] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) equal(w,sk_c7) -> . % 0.20/0.47 583[7:Con:582.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.47 612[7:SpL:571.0,583.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.47 613[7:Obv:612.1] || -> . % 0.20/0.47 614[7:Spt:613.0,23.1,534.0] || equal(multiply(sk_c3,sk_c6),sk_c7)** -> . % 0.20/0.47 615[7:Spt:613.0,23.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 617[6:Rew:28.0,553.0] || -> equal(identity,sk_c5)**. % 0.20/0.47 618[6:Rew:617.0,27.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.47 619[6:Rew:617.0,127.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.47 625[7:Rew:542.0,614.0] || equal(multiply(sk_c3,sk_c7),sk_c7)** -> . % 0.20/0.47 627[6:Rew:542.0,8.1] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.47 628[7:MRR:627.1,625.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 636[6:Rew:542.0,3.1,542.0,3.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)** equal(multiply(sk_c1,sk_c7),sk_c7). % 0.20/0.47 637[7:MRR:636.0,625.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.20/0.47 662[7:SpR:637.0,76.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c7)**. % 0.20/0.47 664[7:Rew:543.0,662.0,628.0,662.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 668[7:Rew:664.0,618.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 669[7:Rew:664.0,619.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 676[7:Rew:668.0,527.0] || -> equal(multiply(sk_c3,u),u)**. % 0.20/0.47 678[7:Rew:669.0,637.0] || -> equal(sk_c7,sk_c1)**. % 0.20/0.47 680[7:Rew:669.0,625.0] || equal(sk_c3,sk_c7)** -> . % 0.20/0.47 690[7:Rew:678.0,669.0] || -> equal(multiply(u,sk_c1),u)**. % 0.20/0.47 692[7:Rew:678.0,680.0] || equal(sk_c3,sk_c1)** -> . % 0.20/0.47 726[7:SpR:690.0,676.0] || -> equal(sk_c3,sk_c1)**. % 0.20/0.47 727[7:MRR:726.0,692.0] || -> . % 0.20/0.47 730[6:Spt:727.0,25.1,529.0] || equal(multiply(sk_c4,sk_c5),sk_c6)** -> . % 0.20/0.47 731[6:Spt:727.0,25.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 732[6:MRR:10.1,730.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 733[6:MRR:20.0,730.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 734[6:MRR:5.0,730.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 750[6:SpR:733.0,76.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.47 752[6:Rew:731.0,750.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 754[6:SpR:734.0,76.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.47 756[6:Rew:732.0,754.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 758[6:SpR:752.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.47 760[6:Rew:28.0,758.0] || -> equal(identity,sk_c5)**. % 0.20/0.47 761[6:Rew:760.0,127.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.47 762[6:Rew:760.0,27.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.47 765[6:Rew:761.0,512.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 766[6:Rew:761.0,730.0] || equal(sk_c6,sk_c4)** -> . % 0.20/0.47 770[6:Rew:765.0,504.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.20/0.47 772[6:Rew:765.0,734.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.20/0.47 774[6:Rew:765.0,521.0] || -> equal(multiply(sk_c7,multiply(sk_c4,u)),u)**. % 0.20/0.47 782[6:Rew:765.0,756.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 783[6:Rew:765.0,766.0] || equal(sk_c4,sk_c7)** -> . % 0.20/0.47 785[6:Rew:770.0,782.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 787[6:Rew:785.0,761.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 788[6:Rew:785.0,762.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 791[6:Rew:787.0,772.0] || -> equal(sk_c7,sk_c1)**. % 0.20/0.47 797[6:Rew:791.0,783.0] || equal(sk_c4,sk_c1)** -> . % 0.20/0.47 803[6:Rew:791.0,787.0] || -> equal(multiply(u,sk_c1),u)**. % 0.20/0.47 804[6:Rew:791.0,788.0] || -> equal(multiply(sk_c1,u),u)**. % 0.20/0.47 812[6:Rew:804.0,774.0,791.0,774.0] || -> equal(multiply(sk_c4,u),u)**. % 0.20/0.47 851[6:SpR:812.0,803.0] || -> equal(sk_c4,sk_c1)**. % 0.20/0.47 853[6:MRR:851.0,797.0] || -> . % 0.20/0.47 855[5:Spt:853.0,22.0,526.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.20/0.47 856[5:Spt:853.0,22.1] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 857[5:MRR:7.0,855.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 858[5:MRR:17.0,855.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 859[5:MRR:2.0,855.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 873[5:SpR:858.0,76.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.47 875[5:Rew:856.0,873.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 877[5:SpR:859.0,76.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.47 879[5:Rew:857.0,877.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 881[5:SpR:875.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.47 883[5:Rew:28.0,881.0] || -> equal(identity,sk_c5)**. % 0.20/0.47 885[5:Rew:883.0,127.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.47 891[5:Rew:885.0,512.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 895[5:Rew:891.0,504.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.20/0.47 897[5:Rew:891.0,859.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.20/0.47 901[5:Rew:891.0,515.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c6),sk_c5)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.20/0.47 904[5:Rew:891.0,879.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 906[5:Rew:895.0,904.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 909[5:Rew:906.0,885.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 913[5:Rew:909.0,897.0] || -> equal(sk_c7,sk_c1)**. % 0.20/0.47 914[5:Rew:913.0,857.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.20/0.47 916[5:Rew:913.0,891.0] || -> equal(sk_c6,sk_c1)**. % 0.20/0.47 920[5:Rew:913.0,906.0] || -> equal(sk_c5,sk_c1)**. % 0.20/0.47 923[5:Rew:913.0,909.0] || -> equal(multiply(u,sk_c1),u)**. % 0.20/0.47 937[5:Rew:923.0,901.5,913.0,901.5,916.0,901.5,923.0,901.4,916.0,901.4,920.0,901.4,923.0,901.3,916.0,901.3,913.0,901.3,913.0,901.2,913.0,901.1,913.0,901.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(u,sk_c1) equal(v,sk_c1) equal(w,sk_c1) -> . % 0.20/0.47 938[5:Con:937.1] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.20/0.47 1011[5:SpL:914.0,938.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.20/0.47 1013[5:Obv:1011.1] || -> . % 0.20/0.47 1014[4:Spt:1013.0,24.0,520.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.20/0.47 1015[4:Spt:1013.0,24.1] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 1016[4:MRR:9.0,1014.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 1017[4:MRR:19.0,1014.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 1018[4:MRR:4.0,1014.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 1030[4:SpR:1017.0,76.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.47 1032[4:Rew:1015.0,1030.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 1034[4:SpR:1018.0,76.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.47 1036[4:Rew:1016.0,1034.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 1038[4:SpR:1032.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.47 1040[4:Rew:28.0,1038.0] || -> equal(identity,sk_c5)**. % 0.20/0.47 1041[4:Rew:1040.0,127.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.47 1045[4:Rew:1041.0,512.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 1048[4:Rew:1045.0,504.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.20/0.47 1051[4:Rew:1045.0,1018.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.20/0.47 1057[4:Rew:1045.0,515.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c6),sk_c5)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.20/0.47 1060[4:Rew:1045.0,1036.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 1062[4:Rew:1048.0,1060.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 1064[4:Rew:1062.0,1041.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 1068[4:Rew:1064.0,1051.0] || -> equal(sk_c7,sk_c1)**. % 0.20/0.47 1069[4:Rew:1068.0,1016.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.20/0.47 1071[4:Rew:1068.0,1045.0] || -> equal(sk_c6,sk_c1)**. % 0.20/0.47 1075[4:Rew:1068.0,1062.0] || -> equal(sk_c5,sk_c1)**. % 0.20/0.47 1077[4:Rew:1068.0,1064.0] || -> equal(multiply(u,sk_c1),u)**. % 0.20/0.47 1092[4:Rew:1077.0,1057.5,1068.0,1057.5,1071.0,1057.5,1077.0,1057.4,1071.0,1057.4,1075.0,1057.4,1077.0,1057.3,1071.0,1057.3,1068.0,1057.3,1068.0,1057.2,1068.0,1057.1,1068.0,1057.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1)** equal(u,sk_c1) equal(v,sk_c1) equal(w,sk_c1) -> . % 0.20/0.47 1093[4:Con:1092.1] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.20/0.47 1122[4:SpL:1069.0,1093.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.20/0.47 1123[4:Obv:1122.1] || -> . % 0.20/0.47 1124[3:Spt:1123.0,12.1,512.0] || equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.20/0.47 1125[3:Spt:1123.0,12.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 1126[3:MRR:14.1,1124.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 1127[3:MRR:13.1,1124.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 1128[3:MRR:15.1,1124.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.48 1137[3:SpR:1127.0,76.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.48 1139[3:Rew:1125.0,1137.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.48 1141[3:SpR:1128.0,76.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.48 1143[3:Rew:1126.0,1141.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.48 1148[3:SpR:1143.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.48 1150[3:Rew:510.0,1148.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.48 1152[3:Rew:1150.0,504.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.20/0.48 1155[3:Rew:1150.0,1139.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.48 1157[3:Rew:1150.0,510.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c7)**. % 0.20/0.48 1158[3:Rew:1150.0,1124.0] || equal(multiply(sk_c7,sk_c5),sk_c7)** -> . % 0.20/0.48 1165[3:Rew:1152.0,1155.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.48 1169[3:Rew:28.0,1157.0,1165.0,1157.0] || -> equal(identity,sk_c7)**. % 0.20/0.48 1170[3:Rew:1169.0,27.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.48 1180[3:Rew:1170.0,1158.0,1165.0,1158.0] || equal(sk_c7,sk_c7)* -> . % 0.20/0.48 1181[3:Obv:1180.0] || -> . % 0.20/0.48 1189[2:Spt:1181.0,11.0,504.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.20/0.48 1190[2:Spt:1181.0,11.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.48 1191[2:MRR:21.1,1189.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.48 1192[2:MRR:6.1,1189.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.48 1193[2:MRR:16.0,1189.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.48 1194[2:MRR:1.0,1189.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.48 1203[2:SpR:1193.0,76.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.48 1205[2:Rew:1191.0,1203.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.48 1207[2:SpR:1194.0,76.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.48 1209[2:Rew:1192.0,1207.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.48 1211[2:SpR:1205.0,76.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.48 1213[2:Rew:28.0,1211.0] || -> equal(identity,sk_c5)**. % 0.20/0.48 1214[2:Rew:1213.0,127.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.48 1217[2:Rew:1213.0,28.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.20/0.48 1218[2:Rew:1214.0,1190.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.48 1222[2:Rew:1218.0,1189.0] || equal(multiply(sk_c7,sk_c7),sk_c5)** -> . % 0.20/0.48 1228[2:Rew:1218.0,1209.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.48 1229[2:Rew:1228.0,1222.0] || equal(sk_c5,sk_c7)** -> . % 0.20/0.48 1250[2:SpR:1228.0,76.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.20/0.48 1252[2:Rew:1217.0,1250.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.48 1253[2:MRR:1252.0,1229.0] || -> . % 0.20/0.48 % SZS output end Refutation % 0.20/0.48 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_8 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_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_25 prove_this_26 left_identity left_inverse associativity % 0.20/0.48 %------------------------------------------------------------------------------