%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP301-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:45 EDT 2022 % Result : Unsatisfiable 0.20s 0.46s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : GRP301-1 : TPTP v8.1.0. Released v2.5.0. % 0.10/0.12 % Command : run_spass %d %s % 0.13/0.33 % Computer : n013.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Tue Jun 14 09:19:59 EDT 2022 % 0.13/0.33 % CPUTime : % 0.20/0.46 % 0.20/0.46 SPASS V 3.9 % 0.20/0.46 SPASS beiseite: Proof found. % 0.20/0.46 % SZS status Theorem % 0.20/0.46 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.46 SPASS derived 757 clauses, backtracked 349 clauses, performed 11 splits and kept 680 clauses. % 0.20/0.46 SPASS allocated 63597 KBytes. % 0.20/0.46 SPASS spent 0:00:00.12 on the problem. % 0.20/0.46 0:00:00.03 for the input. % 0.20/0.46 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.46 0:00:00.00 for inferences. % 0.20/0.46 0:00:00.00 for the backtracking. % 0.20/0.46 0:00:00.06 for the reduction. % 0.20/0.46 % 0.20/0.46 % 0.20/0.46 Here is a proof with depth 5, length 371 : % 0.20/0.46 % SZS output start Refutation % 0.20/0.46 1[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c7,sk_c6),sk_c5). % 0.20/0.46 2[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 3[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c7,sk_c6),sk_c5). % 0.20/0.46 4[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 5[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5). % 0.20/0.46 6[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 7[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 8[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 9[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 10[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 11[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.46 12[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 13[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.46 14[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 15[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.46 16[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.46 17[0:Inp] || -> equal(inverse(sk_c3),sk_c7)** equal(inverse(sk_c7),sk_c5). % 0.20/0.46 18[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.46 19[0:Inp] || -> equal(inverse(sk_c4),sk_c6)** equal(inverse(sk_c7),sk_c5). % 0.20/0.46 20[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.46 21[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 22[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 23[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 24[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 25[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 26[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.46 27[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 28[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.46 29[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 30[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.46 31[0:Inp] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(inverse(x),sk_c7) equal(inverse(sk_c7),sk_c5) 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_c6),sk_c5) -> . % 0.20/0.46 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.20/0.46 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.20/0.46 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.20/0.46 35[1:Spt:31.2,31.7] || equal(inverse(u),sk_c6) equal(multiply(u,sk_c6),sk_c5)** -> . % 0.20/0.46 36[2:Spt:16.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.46 38[3:Spt:19.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.46 40[4:Spt:17.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.46 44[5:Spt:20.1] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.46 46[6:Spt:18.1] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.46 48[6:SpL:46.0,35.1] || equal(inverse(sk_c3),sk_c6)** equal(sk_c5,sk_c7) -> . % 0.20/0.46 49[6:Rew:40.0,48.0] || equal(sk_c6,sk_c7) equal(sk_c5,sk_c7)** -> . % 0.20/0.46 51[3:SpR:38.0,33.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.20/0.46 52[4:SpR:40.0,33.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.20/0.46 53[1:SpL:33.0,35.1] || equal(inverse(inverse(sk_c6)),sk_c6)** equal(identity,sk_c5) -> . % 0.20/0.46 59[2:SpR:36.0,34.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c5,u))**. % 0.20/0.46 60[3:SpR:51.0,34.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),multiply(identity,u))**. % 0.20/0.46 62[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.46 64[4:SpR:52.0,34.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),multiply(identity,u))**. % 0.20/0.46 66[3:Rew:32.0,60.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),u)**. % 0.20/0.46 67[4:Rew:32.0,64.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.20/0.46 68[0:Rew:32.0,62.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.46 72[5:SpR:44.0,66.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.46 76[5:SpL:72.0,35.1] || equal(inverse(sk_c6),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.20/0.46 77[5:Obv:76.1] || equal(inverse(sk_c6),sk_c6)** -> . % 0.20/0.46 80[6:SpR:46.0,67.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.46 83[0:SpR:68.0,68.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.46 86[2:SpR:36.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.46 87[3:SpR:51.0,68.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c4)**. % 0.20/0.46 89[5:SpR:72.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.46 91[0:SpR:33.0,68.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.46 93[4:SpR:52.0,68.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c3)**. % 0.20/0.46 99[5:Rew:86.0,89.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 101[5:Rew:99.0,36.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.20/0.46 108[5:Rew:99.0,77.0] || equal(inverse(sk_c7),sk_c7)** -> . % 0.20/0.46 110[6:Rew:99.0,49.0] || equal(sk_c7,sk_c7) equal(sk_c5,sk_c7)** -> . % 0.20/0.46 111[5:Rew:99.0,86.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c7)**. % 0.20/0.46 119[6:Rew:99.0,80.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.46 120[6:Rew:101.0,119.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 150[6:Obv:110.0] || equal(sk_c5,sk_c7)** -> . % 0.20/0.46 151[6:Rew:120.0,150.0] || equal(sk_c7,sk_c7)* -> . % 0.20/0.46 152[6:Obv:151.0] || -> . % 0.20/0.46 165[6:Spt:152.0,18.1,46.0] || equal(multiply(sk_c3,sk_c6),sk_c7)** -> . % 0.20/0.46 166[6:Spt:152.0,18.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 167[6:Rew:166.0,108.0] || equal(sk_c5,sk_c7)** -> . % 0.20/0.46 169[6:Rew:166.0,111.0] || -> equal(multiply(sk_c5,sk_c5),sk_c7)**. % 0.20/0.46 170[6:Rew:166.0,93.0] || -> equal(multiply(sk_c5,identity),sk_c3)**. % 0.20/0.46 175[6:Rew:99.0,165.0] || equal(multiply(sk_c3,sk_c7),sk_c7)** -> . % 0.20/0.46 176[0:Rew:83.0,91.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.46 177[6:Rew:176.0,170.0] || -> equal(sk_c3,sk_c5)**. % 0.20/0.46 179[6:Rew:177.0,52.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.20/0.46 182[6:Rew:177.0,175.0] || equal(multiply(sk_c5,sk_c7),sk_c7)** -> . % 0.20/0.46 189[6:Rew:177.0,28.1,99.0,28.1,99.0,28.0] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c5,sk_c7),sk_c7)**. % 0.20/0.46 190[6:MRR:189.1,182.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.46 195[6:Rew:99.0,23.1,177.0,23.0,99.0,23.0] || -> equal(multiply(sk_c5,sk_c7),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.20/0.46 196[6:MRR:195.0,182.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.20/0.46 204[6:SpR:166.0,68.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.46 220[6:SpR:196.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c7)**. % 0.20/0.46 222[6:Rew:190.0,220.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.20/0.46 223[6:Rew:179.0,222.0] || -> equal(identity,sk_c7)**. % 0.20/0.46 225[6:Rew:223.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.46 233[6:Rew:225.0,204.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.46 249[6:Rew:233.0,169.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 250[6:MRR:249.0,167.0] || -> . % 0.20/0.46 257[5:Spt:250.0,20.1,44.0] || equal(multiply(sk_c4,sk_c5),sk_c6)** -> . % 0.20/0.46 258[5:Spt:250.0,20.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 262[3:Rew:176.0,87.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.20/0.46 263[3:Rew:262.0,86.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.20/0.46 264[5:Rew:263.0,257.0] || equal(sk_c6,sk_c7)** -> . % 0.20/0.46 271[3:Rew:263.0,30.1] || -> equal(inverse(sk_c2),sk_c6)** equal(sk_c6,sk_c7). % 0.20/0.46 272[5:MRR:271.1,264.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 273[3:Rew:263.0,15.1] || -> equal(inverse(sk_c1),sk_c7)** equal(sk_c6,sk_c7). % 0.20/0.46 274[5:MRR:273.1,264.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 278[3:Rew:263.0,25.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 279[5:MRR:278.0,264.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 280[3:Rew:263.0,10.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 281[5:MRR:280.0,264.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 282[3:Rew:263.0,5.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 283[5:MRR:282.0,264.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 284[3:Rew:38.0,53.0,262.0,53.0] || equal(sk_c6,sk_c6) equal(identity,sk_c5)** -> . % 0.20/0.46 285[3:Obv:284.0] || equal(identity,sk_c5)** -> . % 0.20/0.46 305[5:SpR:279.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.46 307[5:Rew:272.0,305.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.46 317[3:SpR:263.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.20/0.46 322[5:SpR:281.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.46 324[5:Rew:274.0,322.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.46 325[5:Rew:283.0,324.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 331[5:Rew:325.0,36.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.46 343[5:Rew:325.0,307.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.46 344[5:Rew:331.0,343.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 345[5:MRR:344.0,264.0] || -> . % 0.20/0.46 346[4:Spt:345.0,17.0,40.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.20/0.46 347[4:Spt:345.0,17.1] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 348[4:MRR:27.0,346.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 349[4:MRR:12.0,346.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 350[4:MRR:22.0,346.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 351[4:MRR:7.0,346.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 352[4:MRR:2.0,346.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 353[4:SpR:347.0,68.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.46 368[4:SpR:350.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.46 370[4:Rew:348.0,368.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.46 372[4:SpR:351.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.46 374[4:Rew:349.0,372.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.46 375[4:Rew:352.0,374.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 376[4:Rew:375.0,347.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.46 377[4:Rew:375.0,285.0] || equal(identity,sk_c7)** -> . % 0.20/0.46 379[4:Rew:375.0,36.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.46 382[4:Rew:375.0,317.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.46 388[4:Rew:375.0,353.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.46 389[4:Rew:375.0,370.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.46 390[4:Rew:379.0,389.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 392[4:Rew:390.0,262.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.20/0.46 393[4:Rew:390.0,51.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.20/0.46 402[4:Rew:376.0,392.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.46 405[4:Rew:402.0,393.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.20/0.46 417[4:Rew:388.0,382.0,402.0,382.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.46 418[4:Rew:417.0,405.0] || -> equal(identity,sk_c7)**. % 0.20/0.46 423[4:MRR:418.0,377.0] || -> . % 0.20/0.46 428[3:Spt:423.0,19.0,38.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.20/0.46 429[3:Spt:423.0,19.1] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 430[3:MRR:29.0,428.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 431[3:MRR:14.0,428.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 432[3:MRR:24.0,428.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 433[3:MRR:9.0,428.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 434[3:MRR:4.0,428.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 435[3:SpR:429.0,68.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.46 445[3:SpR:432.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.46 447[3:Rew:430.0,445.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.46 449[3:SpR:433.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.46 451[3:Rew:431.0,449.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.46 452[3:Rew:434.0,451.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 453[3:Rew:452.0,429.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.46 454[3:Rew:452.0,36.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.46 457[3:Rew:452.0,59.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.46 461[3:Rew:452.0,53.1] || equal(inverse(inverse(sk_c6)),sk_c6)** equal(identity,sk_c7) -> . % 0.20/0.46 464[3:Rew:452.0,435.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.46 465[3:Rew:452.0,447.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.46 466[3:Rew:454.0,465.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 476[3:Rew:464.0,457.0,466.0,457.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.46 484[3:Rew:453.0,461.0,453.0,461.0,466.0,461.0] || equal(sk_c7,sk_c7) equal(identity,sk_c7)** -> . % 0.20/0.46 485[3:Obv:484.0] || equal(identity,sk_c7)** -> . % 0.20/0.46 508[3:SpR:476.0,176.0] || -> equal(identity,sk_c7)**. % 0.20/0.46 510[3:MRR:508.0,485.0] || -> . % 0.20/0.46 512[2:Spt:510.0,16.1,36.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.20/0.46 513[2:Spt:510.0,16.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 514[2:MRR:26.1,512.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 515[2:MRR:11.1,512.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 516[2:MRR:21.0,512.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 517[2:MRR:6.0,512.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 518[2:MRR:1.0,512.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 521[2:SpR:514.0,68.0] || -> equal(multiply(sk_c6,multiply(sk_c2,u)),u)**. % 0.20/0.46 523[2:SpR:515.0,68.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.20/0.46 526[2:SpR:516.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.46 528[2:Rew:514.0,526.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.46 530[2:SpR:517.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.46 532[2:Rew:515.0,530.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.46 533[2:Rew:518.0,532.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 535[2:Rew:533.0,516.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.46 536[2:Rew:533.0,512.0] || equal(multiply(sk_c6,sk_c7),sk_c7)** -> . % 0.20/0.46 543[2:Rew:533.0,528.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.46 545[2:Rew:543.0,536.0] || equal(sk_c6,sk_c7)** -> . % 0.20/0.46 558[2:SpR:543.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c7)**. % 0.20/0.46 560[2:Rew:33.0,558.0] || -> equal(identity,sk_c7)**. % 0.20/0.46 561[2:Rew:560.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.46 562[2:Rew:560.0,176.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.46 572[2:Rew:561.0,523.0] || -> equal(multiply(sk_c1,u),u)**. % 0.20/0.46 575[2:Rew:562.0,517.0] || -> equal(sk_c1,sk_c6)**. % 0.20/0.46 577[2:Rew:575.0,572.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.46 578[2:Rew:577.0,521.0] || -> equal(multiply(sk_c2,u),u)**. % 0.20/0.46 579[2:Rew:578.0,535.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 580[2:MRR:579.0,545.0] || -> . % 0.20/0.46 589[1:Spt:580.0,31.0,31.1,31.3,31.4,31.5,31.6,31.8,31.9,31.10] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c5),sk_c6)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c7,sk_c6),sk_c5) -> . % 0.20/0.46 591[2:Spt:16.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.46 592[2:Rew:591.0,589.7] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c5,sk_c5) equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.20/0.46 594[2:Obv:592.7] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.20/0.46 596[2:SpR:591.0,34.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c5,u))**. % 0.20/0.46 597[2:SpR:591.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.46 599[3:Spt:17.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.46 600[3:SpR:599.0,68.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.20/0.46 602[4:Spt:19.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.46 603[4:SpR:602.0,68.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),u)**. % 0.20/0.46 605[5:Spt:18.1] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.46 607[5:SpR:605.0,68.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.46 609[5:Rew:599.0,607.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.46 613[6:Spt:20.1] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.46 615[6:SpR:613.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.46 617[6:Rew:602.0,615.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.46 622[6:SpR:617.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.46 624[6:Rew:597.0,622.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 625[6:Rew:624.0,591.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.20/0.46 626[6:Rew:624.0,602.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.46 628[6:Rew:624.0,609.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.46 629[6:Rew:624.0,613.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.20/0.46 632[6:Rew:624.0,594.7] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c7),sk_c5)** -> . % 0.20/0.46 633[6:Rew:624.0,597.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c7)**. % 0.20/0.46 640[6:Rew:625.0,628.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 642[6:Rew:640.0,629.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7)**. % 0.20/0.46 644[6:Rew:33.0,633.0,640.0,633.0] || -> equal(identity,sk_c7)**. % 0.20/0.46 645[6:Rew:644.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.46 646[6:Rew:644.0,176.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.46 650[6:Rew:646.0,642.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.46 652[6:Rew:650.0,626.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.46 662[6:Rew:645.0,632.7,640.0,632.7,646.0,632.6,624.0,632.6,646.0,632.5,624.0,632.5,646.0,632.4,640.0,632.4,624.0,632.4,652.0,632.3,640.0,632.3,624.0,632.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c7)** equal(sk_c7,sk_c7) equal(u,sk_c7) equal(v,sk_c7) equal(w,sk_c7) equal(sk_c7,sk_c7) -> . % 0.20/0.46 663[6:Obv:662.7] || 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.46 664[6:Con:663.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.46 725[6:SpL:652.0,664.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.46 727[6:Obv:725.1] || -> . % 0.20/0.46 728[6:Spt:727.0,20.1,613.0] || equal(multiply(sk_c4,sk_c5),sk_c6)** -> . % 0.20/0.46 729[6:Spt:727.0,20.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 731[6:MRR:30.1,728.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 732[6:MRR:15.1,728.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 733[6:MRR:25.0,728.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 734[6:MRR:10.0,728.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 735[6:MRR:5.0,728.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 740[6:SpR:729.0,68.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.46 755[6:SpR:733.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.46 757[6:Rew:731.0,755.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.46 769[6:SpR:734.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.46 771[6:Rew:732.0,769.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.46 772[6:Rew:735.0,771.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 775[6:Rew:772.0,591.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.46 778[6:Rew:772.0,728.0] || equal(multiply(sk_c4,sk_c7),sk_c6)** -> . % 0.20/0.46 779[6:Rew:772.0,596.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.46 784[6:Rew:772.0,740.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.46 785[6:Rew:772.0,757.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.46 788[6:Rew:775.0,785.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 794[6:Rew:788.0,603.0] || -> equal(multiply(sk_c7,multiply(sk_c4,u)),u)**. % 0.20/0.46 802[6:Rew:788.0,778.0] || equal(multiply(sk_c4,sk_c7),sk_c7)** -> . % 0.20/0.46 805[6:Rew:784.0,779.0,788.0,779.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.46 809[6:Rew:805.0,794.0] || -> equal(multiply(sk_c4,u),u)**. % 0.20/0.46 812[6:UnC:809.0,802.0] || -> . % 0.20/0.46 819[5:Spt:812.0,18.1,605.0] || equal(multiply(sk_c3,sk_c6),sk_c7)** -> . % 0.20/0.46 820[5:Spt:812.0,18.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 821[5:MRR:28.1,819.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 822[5:MRR:13.1,819.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 823[5:MRR:23.0,819.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 824[5:MRR:8.0,819.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 825[5:MRR:3.0,819.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 830[5:SpR:820.0,68.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.46 842[5:SpR:823.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.46 844[5:Rew:821.0,842.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.46 846[5:SpR:824.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.46 848[5:Rew:822.0,846.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.46 849[5:Rew:825.0,848.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 851[5:Rew:849.0,591.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.46 854[5:Rew:849.0,596.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.46 859[5:Rew:849.0,830.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.46 860[5:Rew:849.0,844.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.46 861[5:Rew:851.0,860.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 865[5:Rew:861.0,819.0] || equal(multiply(sk_c3,sk_c7),sk_c7)** -> . % 0.20/0.46 873[5:Rew:859.0,854.0,861.0,854.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.46 878[5:Rew:873.0,600.0] || -> equal(multiply(sk_c3,u),u)**. % 0.20/0.46 880[5:UnC:878.0,865.0] || -> . % 0.20/0.46 886[4:Spt:880.0,19.0,602.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.20/0.46 887[4:Spt:880.0,19.1] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 888[4:MRR:29.0,886.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 889[4:MRR:14.0,886.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 890[4:MRR:24.0,886.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 891[4:MRR:9.0,886.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 892[4:MRR:4.0,886.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 893[4:Rew:892.0,594.7,887.0,594.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(sk_c5,sk_c5) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.20/0.46 894[4:Obv:893.7] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.20/0.46 897[4:SpR:887.0,68.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.46 907[4:SpR:890.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.46 909[4:Rew:888.0,907.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.46 911[4:SpR:891.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.46 913[4:Rew:889.0,911.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.46 914[4:Rew:892.0,913.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.46 915[4:Rew:914.0,887.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.46 916[4:Rew:914.0,591.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.46 919[4:Rew:914.0,596.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.46 922[4:Rew:914.0,894.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.20/0.46 924[4:Rew:914.0,897.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.46 925[4:Rew:914.0,909.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.46 926[4:Rew:916.0,925.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.46 936[4:Rew:924.0,919.0,926.0,919.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.46 943[4:Rew:926.0,922.5,926.0,922.4,926.0,922.3,926.0,922.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.20/0.46 944[4:Con:943.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.20/0.46 967[4:SpR:936.0,176.0] || -> equal(identity,sk_c7)**. % 0.20/0.46 970[4:Rew:967.0,176.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.46 973[4:Rew:970.0,944.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.46 998[4:SpL:915.0,973.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.46 999[4:Obv:998.1] || -> . % 0.20/0.46 1000[3:Spt:999.0,17.0,599.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.20/0.46 1001[3:Spt:999.0,17.1] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.46 1002[3:MRR:27.0,1000.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.46 1003[3:MRR:12.0,1000.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.46 1004[3:MRR:22.0,1000.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.46 1005[3:MRR:7.0,1000.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.46 1006[3:MRR:2.0,1000.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.46 1007[3:Rew:1006.0,594.7,1001.0,594.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(sk_c5,sk_c5) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.20/0.47 1008[3:Obv:1007.7] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.20/0.47 1011[3:SpR:1001.0,68.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.47 1021[3:SpR:1004.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.47 1023[3:Rew:1002.0,1021.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 1025[3:SpR:1005.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.47 1027[3:Rew:1003.0,1025.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 1028[3:Rew:1006.0,1027.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 1029[3:Rew:1028.0,1001.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 1030[3:Rew:1028.0,591.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.47 1033[3:Rew:1028.0,596.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.47 1036[3:Rew:1028.0,1008.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.20/0.47 1038[3:Rew:1028.0,1011.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.47 1039[3:Rew:1028.0,1023.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.47 1040[3:Rew:1030.0,1039.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 1049[3:Rew:1038.0,1033.0,1040.0,1033.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 1055[3:Rew:1040.0,1036.5,1040.0,1036.4,1040.0,1036.3,1040.0,1036.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.20/0.47 1056[3:Con:1055.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.20/0.47 1079[3:SpR:1049.0,176.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 1081[3:Rew:1079.0,176.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 1085[3:Rew:1081.0,1056.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.47 1113[3:SpL:1029.0,1085.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.47 1114[3:Obv:1113.1] || -> . % 0.20/0.47 1115[2:Spt:1114.0,16.1,591.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.20/0.47 1116[2:Spt:1114.0,16.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.47 1117[2:MRR:26.1,1115.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 1118[2:MRR:11.1,1115.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 1119[2:MRR:21.0,1115.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.47 1120[2:MRR:6.0,1115.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.47 1121[2:MRR:1.0,1115.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.20/0.47 1124[2:SpR:1117.0,68.0] || -> equal(multiply(sk_c6,multiply(sk_c2,u)),u)**. % 0.20/0.47 1126[2:SpR:1118.0,68.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.20/0.47 1129[2:SpR:1119.0,68.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.20/0.47 1131[2:Rew:1117.0,1129.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 1133[2:SpR:1120.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.47 1135[2:Rew:1118.0,1133.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 1136[2:Rew:1121.0,1135.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 1138[2:Rew:1136.0,1119.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.47 1139[2:Rew:1136.0,1115.0] || equal(multiply(sk_c6,sk_c7),sk_c7)** -> . % 0.20/0.47 1142[2:Rew:1136.0,1131.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.47 1144[2:Rew:1142.0,1139.0] || equal(sk_c6,sk_c7)** -> . % 0.20/0.47 1157[2:SpR:1142.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c7)**. % 0.20/0.47 1159[2:Rew:33.0,1157.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 1160[2:Rew:1159.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 1161[2:Rew:1159.0,176.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 1168[2:Rew:1160.0,1126.0] || -> equal(multiply(sk_c1,u),u)**. % 0.20/0.47 1173[2:Rew:1161.0,1120.0] || -> equal(sk_c1,sk_c6)**. % 0.20/0.47 1175[2:Rew:1173.0,1168.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 1176[2:Rew:1175.0,1124.0] || -> equal(multiply(sk_c2,u),u)**. % 0.20/0.47 1177[2:Rew:1176.0,1138.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 1178[2:MRR:1177.0,1144.0] || -> . % 0.20/0.47 % SZS output end Refutation % 0.20/0.47 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_18 prove_this_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_25 prove_this_26 prove_this_27 prove_this_28 prove_this_29 prove_this_30 prove_this_31 left_identity left_inverse associativity % 0.20/0.47 %------------------------------------------------------------------------------