%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP360-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n020.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:47:01 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.03/0.13 % Problem : GRP360-1 : TPTP v8.1.0. Released v2.5.0. % 0.03/0.14 % Command : run_spass %d %s % 0.14/0.35 % Computer : n020.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Tue Jun 14 09:07:20 EDT 2022 % 0.14/0.35 % 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/sandbox/benchmark/theBenchmark.p % 0.20/0.47 SPASS derived 807 clauses, backtracked 304 clauses, performed 11 splits and kept 666 clauses. % 0.20/0.47 SPASS allocated 63601 KBytes. % 0.20/0.47 SPASS spent 0:00:00.11 on the problem. % 0.20/0.47 0:00:00.03 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 5, length 382 : % 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_c6,sk_c5),sk_c7). % 0.20/0.47 2[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 3[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.20/0.47 4[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 5[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.20/0.47 6[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 7[0:Inp] || -> equal(inverse(sk_c3),sk_c7)** equal(inverse(sk_c7),sk_c5). % 0.20/0.47 8[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 9[0:Inp] || -> equal(inverse(sk_c4),sk_c6)** equal(inverse(sk_c7),sk_c5). % 0.20/0.47 10[0:Inp] || -> equal(inverse(sk_c7),sk_c5) 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_c2),sk_c6)**. % 0.20/0.47 12[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.20/0.47 13[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c7,sk_c2),sk_c6). % 0.20/0.47 14[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.20/0.47 15[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c2),sk_c6). % 0.20/0.47 16[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.20/0.47 17[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.20/0.47 18[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.20/0.47 19[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.20/0.47 20[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.20/0.47 21[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 22[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 23[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 24[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 25[0:Inp] || -> equal(inverse(sk_c1),sk_c7) 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_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(w,sk_c7),x)*+ equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c7,x),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 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.2,26.4,26.7] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),v)*+ equal(multiply(sk_c7,v),sk_c6)** -> . % 0.20/0.47 32[2:Spt:6.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.47 34[3:Spt:1.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 36[4:Spt:21.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 40[5:Spt:16.1] || -> equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.20/0.47 45[6:Spt:11.1] || -> equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.20/0.47 48[2:SpR:32.0,28.0] || -> equal(multiply(sk_c5,sk_c7),identity)**. % 0.20/0.47 49[4:SpR:36.0,28.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.20/0.47 50[1:SpL:28.0,30.1] || equal(inverse(inverse(sk_c7)),sk_c7) equal(identity,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.20/0.47 51[2:Rew:32.0,50.0] || equal(inverse(sk_c5),sk_c7) equal(identity,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.20/0.47 58[2:SpR:48.0,29.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),multiply(identity,u))**. % 0.20/0.47 59[6:SpR:45.0,29.0] || -> equal(multiply(sk_c7,multiply(sk_c2,u)),multiply(sk_c6,u))**. % 0.20/0.47 60[4:SpR:49.0,29.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),multiply(identity,u))**. % 0.20/0.47 61[3:SpR:34.0,29.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.20/0.47 63[0:SpR:28.0,29.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.47 65[2:Rew:27.0,58.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.47 66[4:Rew:27.0,60.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.20/0.47 67[0:Rew:27.0,63.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.47 72[4:SpR:49.0,65.0] || -> equal(multiply(sk_c5,identity),sk_c1)**. % 0.20/0.47 76[4:SpR:72.0,29.0] || -> equal(multiply(sk_c5,multiply(identity,u)),multiply(sk_c1,u))**. % 0.20/0.47 78[4:Rew:27.0,76.0] || -> equal(multiply(sk_c1,u),multiply(sk_c5,u))**. % 0.20/0.47 79[5:Rew:78.0,40.0] || -> equal(multiply(sk_c5,sk_c7),sk_c2)**. % 0.20/0.47 81[4:Rew:78.0,66.0] || -> equal(multiply(sk_c7,multiply(sk_c5,u)),u)**. % 0.20/0.47 82[5:Rew:48.0,79.0] || -> equal(identity,sk_c2)**. % 0.20/0.47 83[5:Rew:82.0,27.0] || -> equal(multiply(sk_c2,u),u)**. % 0.20/0.47 84[5:Rew:82.0,28.0] || -> equal(multiply(inverse(u),u),sk_c2)**. % 0.20/0.47 85[5:Rew:82.0,48.0] || -> equal(multiply(sk_c5,sk_c7),sk_c2)**. % 0.20/0.47 89[5:Rew:82.0,51.1] || equal(inverse(sk_c5),sk_c7) equal(sk_c2,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.20/0.47 90[6:Rew:83.0,59.0] || -> equal(multiply(sk_c7,u),multiply(sk_c6,u))**. % 0.20/0.47 93[6:Rew:90.0,45.0] || -> equal(multiply(sk_c6,sk_c2),sk_c6)**. % 0.20/0.47 95[6:Rew:90.0,81.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),u)**. % 0.20/0.47 99[6:Rew:90.0,61.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),multiply(sk_c6,u))**. % 0.20/0.47 102[6:Rew:95.0,99.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 103[6:Rew:102.0,34.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.47 104[6:Rew:102.0,95.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.47 106[6:Rew:102.0,93.0] || -> equal(sk_c2,sk_c6)**. % 0.20/0.47 109[6:Rew:103.0,32.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.20/0.47 111[6:Rew:103.0,85.0] || -> equal(multiply(sk_c5,sk_c5),sk_c2)**. % 0.20/0.47 117[6:Rew:106.0,84.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.20/0.47 121[6:Rew:104.0,111.0,106.0,111.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 122[6:Rew:121.0,103.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 123[6:Rew:121.0,109.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 136[6:Rew:102.0,89.2,122.0,89.2,106.0,89.1,123.0,89.0,121.0,89.0,122.0,89.0] || equal(sk_c6,sk_c6)* equal(sk_c6,u)* equal(u,sk_c6)* -> . % 0.20/0.47 137[6:Obv:136.1] || equal(u,sk_c6)* -> . % 0.20/0.47 138[6:UnC:137.0,117.0] || -> . % 0.20/0.47 141[6:Spt:138.0,11.1,45.0] || equal(multiply(sk_c7,sk_c2),sk_c6)** -> . % 0.20/0.47 142[6:Spt:138.0,11.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 143[6:MRR:14.1,141.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 146[6:MRR:15.1,141.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 174[6:SpR:143.0,84.0] || -> equal(multiply(sk_c6,sk_c4),sk_c2)**. % 0.20/0.47 186[0:SpR:67.0,67.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.47 189[6:SpR:142.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 198[5:SpR:84.0,67.0] || -> equal(multiply(inverse(inverse(u)),sk_c2),u)**. % 0.20/0.47 199[6:SpR:174.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c2),sk_c4)**. % 0.20/0.47 217[5:Rew:186.0,198.0] || -> equal(multiply(u,sk_c2),u)**. % 0.20/0.47 218[6:Rew:217.0,141.0] || equal(sk_c7,sk_c6)** -> . % 0.20/0.47 220[6:Rew:217.0,199.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.20/0.47 227[6:Rew:220.0,189.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.20/0.47 229[6:Rew:146.0,227.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 230[6:MRR:229.0,218.0] || -> . % 0.20/0.47 232[5:Spt:230.0,16.1,40.0] || equal(multiply(sk_c1,sk_c7),sk_c2)** -> . % 0.20/0.47 233[5:Spt:230.0,16.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 234[5:Rew:78.0,232.0] || equal(multiply(sk_c5,sk_c7),sk_c2)** -> . % 0.20/0.47 235[5:Rew:48.0,234.0] || equal(identity,sk_c2)** -> . % 0.20/0.47 237[4:Rew:48.0,19.1,78.0,19.1] || -> equal(inverse(sk_c4),sk_c6)** equal(identity,sk_c2). % 0.20/0.47 238[5:MRR:237.1,235.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 239[4:Rew:48.0,17.1,78.0,17.1] || -> equal(inverse(sk_c3),sk_c7)** equal(identity,sk_c2). % 0.20/0.47 240[5:MRR:239.1,235.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 241[4:Rew:48.0,20.1,78.0,20.1] || -> equal(multiply(sk_c4,sk_c5),sk_c6)** equal(identity,sk_c2). % 0.20/0.47 242[5:MRR:241.1,235.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 243[4:Rew:48.0,18.1,78.0,18.1] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(identity,sk_c2). % 0.20/0.47 244[5:MRR:243.1,235.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 246[5:SpR:233.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 256[5:SpR:242.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.47 258[5:Rew:238.0,256.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 273[5:SpR:244.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.47 275[5:Rew:240.0,273.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 280[5:SpR:258.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.47 282[5:Rew:246.0,280.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 283[5:Rew:282.0,32.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 289[5:Rew:282.0,48.0] || -> equal(multiply(sk_c5,sk_c6),identity)**. % 0.20/0.47 294[5:Rew:282.0,51.2] || equal(inverse(sk_c5),sk_c7) equal(identity,u) equal(multiply(sk_c6,u),sk_c6)** -> . % 0.20/0.47 305[5:Rew:282.0,275.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 306[5:Rew:258.0,305.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 309[5:Rew:306.0,258.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 313[5:Rew:306.0,283.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 315[5:Rew:306.0,289.0] || -> equal(multiply(sk_c6,sk_c6),identity)**. % 0.20/0.47 316[5:Rew:309.0,315.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 318[5:Rew:316.0,27.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 343[5:Rew:318.0,294.2,316.0,294.1,313.0,294.0,306.0,294.0,282.0,294.0] || equal(sk_c6,sk_c6)* equal(sk_c6,u)* equal(u,sk_c6)* -> . % 0.20/0.47 344[5:Obv:343.1] || equal(u,sk_c6)* -> . % 0.20/0.47 345[5:UnC:344.0,238.0] || -> . % 0.20/0.47 348[4:Spt:345.0,21.0,36.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.20/0.47 349[4:Spt:345.0,21.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 350[4:MRR:24.1,348.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 351[4:MRR:22.1,348.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 352[4:MRR:25.0,348.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 353[4:MRR:23.0,348.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 355[4:SpR:349.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 371[4:SpR:352.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.47 373[4:Rew:350.0,371.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 375[4:SpR:353.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.47 377[4:Rew:351.0,375.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 382[4:SpR:373.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.47 384[4:Rew:355.0,382.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 386[4:Rew:384.0,32.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 389[4:Rew:384.0,48.0] || -> equal(multiply(sk_c5,sk_c6),identity)**. % 0.20/0.47 397[4:Rew:384.0,51.2] || equal(inverse(sk_c5),sk_c7) equal(identity,u) equal(multiply(sk_c6,u),sk_c6)** -> . % 0.20/0.47 405[4:Rew:384.0,377.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 406[4:Rew:373.0,405.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 408[4:Rew:406.0,373.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 410[4:Rew:406.0,386.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 411[4:Rew:406.0,389.0] || -> equal(multiply(sk_c6,sk_c6),identity)**. % 0.20/0.47 413[4:Rew:408.0,411.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 414[4:Rew:413.0,27.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 431[4:Rew:414.0,397.2,413.0,397.1,410.0,397.0,406.0,397.0,384.0,397.0] || equal(sk_c6,sk_c6)* equal(sk_c6,u)* equal(u,sk_c6)* -> . % 0.20/0.47 432[4:Obv:431.1] || equal(u,sk_c6)* -> . % 0.20/0.47 433[4:UnC:432.0,350.0] || -> . % 0.20/0.47 436[3:Spt:433.0,1.1,34.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.47 437[3:Spt:433.0,1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 438[3:MRR:4.1,436.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 439[3:MRR:2.1,436.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 440[3:MRR:5.1,436.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 441[3:MRR:3.1,436.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 443[3:SpR:437.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 452[3:SpR:440.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.47 454[3:Rew:438.0,452.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 460[3:SpR:441.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.47 462[3:Rew:439.0,460.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 464[3:SpR:454.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.47 466[3:Rew:443.0,464.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 468[3:Rew:466.0,32.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 470[3:Rew:466.0,48.0] || -> equal(multiply(sk_c5,sk_c6),identity)**. % 0.20/0.47 476[3:Rew:466.0,51.2] || equal(inverse(sk_c5),sk_c7) equal(identity,u) equal(multiply(sk_c6,u),sk_c6)** -> . % 0.20/0.47 484[3:Rew:466.0,462.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 485[3:Rew:454.0,484.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 487[3:Rew:485.0,454.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 489[3:Rew:485.0,468.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 490[3:Rew:485.0,470.0] || -> equal(multiply(sk_c6,sk_c6),identity)**. % 0.20/0.47 491[3:Rew:487.0,490.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 492[3:Rew:491.0,27.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 509[3:Rew:492.0,476.2,491.0,476.1,489.0,476.0,485.0,476.0,466.0,476.0] || equal(sk_c6,sk_c6)* equal(sk_c6,u)* equal(u,sk_c6)* -> . % 0.20/0.47 510[3:Obv:509.1] || equal(u,sk_c6)* -> . % 0.20/0.47 511[3:UnC:510.0,438.0] || -> . % 0.20/0.47 514[2:Spt:511.0,6.0,32.0] || equal(inverse(sk_c7),sk_c5)** -> . % 0.20/0.47 515[2:Spt:511.0,6.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 516[2:MRR:9.1,514.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 517[2:MRR:7.1,514.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 518[2:MRR:10.0,514.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 519[2:MRR:8.0,514.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 521[2:SpR:515.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 528[2:SpR:518.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.47 530[2:Rew:516.0,528.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 532[2:SpR:519.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.47 534[2:Rew:517.0,532.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 536[2:SpR:530.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.47 538[2:Rew:521.0,536.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 540[2:Rew:538.0,517.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.20/0.47 541[2:Rew:538.0,514.0] || equal(inverse(sk_c6),sk_c5)** -> . % 0.20/0.47 550[2:Rew:538.0,521.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.47 552[2:Rew:538.0,534.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 553[2:Rew:530.0,552.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 557[2:Rew:553.0,541.0] || equal(inverse(sk_c6),sk_c6)** -> . % 0.20/0.47 558[2:Rew:28.0,550.0,553.0,550.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 559[2:Rew:558.0,27.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 561[2:Rew:558.0,28.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.20/0.47 602[2:SpR:540.0,561.0] || -> equal(multiply(sk_c6,sk_c3),sk_c6)**. % 0.20/0.47 607[2:Rew:559.0,602.0] || -> equal(sk_c3,sk_c6)**. % 0.20/0.47 608[2:Rew:607.0,540.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 610[2:MRR:608.0,557.0] || -> . % 0.20/0.47 616[1:Spt:610.0,26.0,26.1,26.3,26.5,26.6,26.8,26.9] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c5),sk_c6)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.20/0.47 618[2:Spt:6.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.20/0.47 619[2:Rew:618.0,616.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(sk_c5,sk_c5) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.20/0.47 621[2:Obv:619.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.20/0.47 623[2:SpR:618.0,67.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.20/0.47 625[3:Spt:1.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 627[3:Rew:625.0,621.5] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(sk_c7,sk_c7) -> . % 0.20/0.47 628[3:Obv:627.5] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.20/0.47 631[3:SpR:625.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c5)**. % 0.20/0.47 633[4:Spt:21.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 634[4:SpR:633.0,67.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.20/0.47 636[5:Spt:11.1] || -> equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.20/0.47 638[5:SpR:636.0,67.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c2)**. % 0.20/0.47 640[5:Rew:618.0,638.0] || -> equal(multiply(sk_c5,sk_c6),sk_c2)**. % 0.20/0.47 642[5:SpR:640.0,67.0] || -> equal(multiply(inverse(sk_c5),sk_c2),sk_c6)**. % 0.20/0.47 644[6:Spt:16.1] || -> equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.20/0.47 646[6:SpR:644.0,67.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c7)**. % 0.20/0.47 648[6:Rew:636.0,646.0,633.0,646.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 649[6:Rew:648.0,618.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 650[6:Rew:648.0,625.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 655[6:Rew:648.0,628.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c6),sk_c5)** -> . % 0.20/0.47 658[6:Rew:648.0,631.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.47 661[6:Rew:649.0,658.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.20/0.47 662[6:Rew:640.0,661.0] || -> equal(sk_c2,sk_c5)**. % 0.20/0.47 665[6:Rew:662.0,642.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c6)**. % 0.20/0.47 668[6:Rew:28.0,665.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 669[6:Rew:668.0,27.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 670[6:Rew:668.0,28.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.20/0.47 672[6:Rew:669.0,650.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 673[6:Rew:672.0,649.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 684[6:Rew:669.0,655.4,672.0,655.4,648.0,655.3,672.0,655.2,648.0,655.1] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(u,sk_c6),sk_c6)** equal(multiply(v,sk_c6),sk_c6)** equal(sk_c6,sk_c6) -> . % 0.20/0.47 685[6:Obv:684.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(u,sk_c6),sk_c6)** equal(multiply(v,sk_c6),sk_c6)** -> . % 0.20/0.47 686[6:Con:685.1] || equal(inverse(u),sk_c6) equal(multiply(u,sk_c6),sk_c6)** -> . % 0.20/0.47 708[6:SpR:670.0,67.0] || -> equal(multiply(inverse(inverse(u)),sk_c6),u)**. % 0.20/0.47 715[6:Rew:186.0,708.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.47 716[6:Rew:715.0,686.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.20/0.47 727[6:SpL:673.0,716.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.20/0.47 728[6:Obv:727.1] || -> . % 0.20/0.47 729[6:Spt:728.0,16.1,644.0] || equal(multiply(sk_c1,sk_c7),sk_c2)** -> . % 0.20/0.47 730[6:Spt:728.0,16.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 731[6:MRR:19.1,729.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 732[6:MRR:17.1,729.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 733[6:MRR:20.1,729.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 734[6:MRR:18.1,729.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 740[6:SpR:730.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 758[6:SpR:733.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.47 760[6:Rew:731.0,758.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 765[6:SpR:734.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.47 767[6:Rew:732.0,765.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 768[6:SpR:760.0,29.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.20/0.47 769[6:SpR:760.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.47 771[6:Rew:740.0,769.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 780[6:Rew:771.0,729.0] || equal(multiply(sk_c1,sk_c6),sk_c2)** -> . % 0.20/0.47 781[6:Rew:771.0,634.0] || -> equal(multiply(sk_c6,multiply(sk_c1,u)),u)**. % 0.20/0.47 782[6:Rew:771.0,623.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.20/0.47 791[6:Rew:771.0,767.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 792[6:Rew:760.0,791.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 794[6:Rew:792.0,640.0] || -> equal(multiply(sk_c6,sk_c6),sk_c2)**. % 0.20/0.47 795[6:Rew:792.0,760.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 801[6:Rew:794.0,795.0] || -> equal(sk_c2,sk_c6)**. % 0.20/0.47 805[6:Rew:801.0,780.0] || equal(multiply(sk_c1,sk_c6),sk_c6)** -> . % 0.20/0.47 808[6:Rew:792.0,782.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),u)**. % 0.20/0.47 809[6:Rew:808.0,768.0,792.0,768.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 812[6:Rew:809.0,781.0] || -> equal(multiply(sk_c1,u),u)**. % 0.20/0.47 814[6:UnC:812.0,805.0] || -> . % 0.20/0.47 822[5:Spt:814.0,11.1,636.0] || equal(multiply(sk_c7,sk_c2),sk_c6)** -> . % 0.20/0.47 823[5:Spt:814.0,11.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 824[5:MRR:14.1,822.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 825[5:MRR:12.1,822.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 826[5:MRR:15.1,822.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 827[5:MRR:13.1,822.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 828[5:Rew:823.0,628.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(sk_c5,sk_c5) -> . % 0.20/0.47 829[5:Obv:828.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** -> . % 0.20/0.47 833[5:SpR:823.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 847[5:SpR:826.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.47 849[5:Rew:824.0,847.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 851[5:SpR:827.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.47 853[5:Rew:825.0,851.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 854[5:SpR:849.0,29.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.20/0.47 855[5:SpR:849.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.47 857[5:Rew:833.0,855.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 859[5:Rew:857.0,618.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 861[5:Rew:857.0,825.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.20/0.47 866[5:Rew:857.0,623.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.20/0.47 871[5:Rew:857.0,829.1] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** -> . % 0.20/0.47 875[5:Rew:857.0,853.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 876[5:Rew:849.0,875.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 880[5:Rew:876.0,859.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 884[5:Rew:876.0,866.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),u)**. % 0.20/0.47 885[5:Rew:884.0,854.0,876.0,854.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 893[5:Rew:857.0,871.3,876.0,871.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(u,sk_c6),sk_c6)** equal(multiply(v,sk_c6),sk_c6)** -> . % 0.20/0.47 894[5:Con:893.1] || equal(inverse(u),sk_c6) equal(multiply(u,sk_c6),sk_c6)** -> . % 0.20/0.47 915[0:SpR:28.0,67.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.47 917[5:SpR:824.0,28.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.20/0.47 919[5:SpR:861.0,28.0] || -> equal(multiply(sk_c6,sk_c3),identity)**. % 0.20/0.47 920[5:SpR:880.0,28.0] || -> equal(multiply(sk_c6,sk_c6),identity)**. % 0.20/0.47 921[5:Rew:885.0,917.0] || -> equal(identity,sk_c4)**. % 0.20/0.47 929[5:Rew:885.0,919.0] || -> equal(identity,sk_c3)**. % 0.20/0.47 930[5:Rew:921.0,929.0] || -> equal(sk_c4,sk_c3)**. % 0.20/0.47 933[5:Rew:930.0,921.0] || -> equal(identity,sk_c3)**. % 0.20/0.47 935[5:Rew:885.0,920.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 936[5:Rew:933.0,935.0] || -> equal(sk_c3,sk_c6)**. % 0.20/0.47 940[5:Rew:936.0,933.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 948[5:Rew:186.0,915.0,940.0,915.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.47 949[5:Rew:948.0,894.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.20/0.47 970[5:SpL:880.0,949.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.20/0.47 971[5:Obv:970.1] || -> . % 0.20/0.47 972[4:Spt:971.0,21.0,633.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.20/0.47 973[4:Spt:971.0,21.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 974[0:Rew:186.0,915.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.47 975[4:MRR:24.1,972.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 976[4:MRR:22.1,972.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 977[4:MRR:25.0,972.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.47 978[4:MRR:23.0,972.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 980[4:Rew:973.0,628.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(sk_c5,sk_c5) -> . % 0.20/0.47 981[4:Obv:980.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** -> . % 0.20/0.47 985[4:SpR:973.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 997[4:SpR:977.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.47 999[4:Rew:975.0,997.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 1001[4:SpR:978.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.47 1003[4:Rew:976.0,1001.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 1007[4:SpR:999.0,29.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.20/0.47 1008[4:SpR:999.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.48 1010[4:Rew:985.0,1008.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.48 1012[4:Rew:1010.0,618.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.48 1018[4:Rew:1010.0,623.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.20/0.48 1022[4:Rew:1010.0,981.1] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** -> . % 0.20/0.48 1026[4:Rew:1010.0,1003.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.48 1027[4:Rew:999.0,1026.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.48 1031[4:Rew:1027.0,1012.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.48 1035[4:Rew:1027.0,1018.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),u)**. % 0.20/0.48 1036[4:Rew:1035.0,1007.0,1027.0,1007.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.48 1042[4:Rew:1010.0,1022.3,1027.0,1022.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(u,sk_c6),sk_c6)** equal(multiply(v,sk_c6),sk_c6)** -> . % 0.20/0.48 1043[4:Con:1042.1] || equal(inverse(u),sk_c6) equal(multiply(u,sk_c6),sk_c6)** -> . % 0.20/0.48 1062[4:SpR:1036.0,974.0] || -> equal(identity,sk_c6)**. % 0.20/0.48 1065[4:Rew:1062.0,974.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.48 1068[4:Rew:1065.0,1043.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.20/0.48 1096[4:SpL:1031.0,1068.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.20/0.48 1097[4:Obv:1096.1] || -> . % 0.20/0.48 1098[3:Spt:1097.0,1.1,625.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.48 1099[3:Spt:1097.0,1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.48 1100[3:MRR:4.1,1098.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.48 1101[3:MRR:2.1,1098.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.48 1102[3:MRR:5.1,1098.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.48 1103[3:MRR:3.1,1098.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.48 1105[3:SpR:1099.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.48 1114[3:SpR:1102.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.48 1116[3:Rew:1100.0,1114.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.48 1118[3:SpR:1103.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.48 1120[3:Rew:1101.0,1118.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.48 1125[3:SpR:1116.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.48 1127[3:Rew:1105.0,1125.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.48 1132[3:Rew:1127.0,1098.0] || equal(multiply(sk_c6,sk_c5),sk_c6)** -> . % 0.20/0.48 1138[3:Rew:1127.0,1120.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.48 1139[3:Rew:1116.0,1138.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.48 1141[3:Rew:1139.0,1116.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.48 1144[3:Rew:1141.0,1132.0,1139.0,1132.0] || equal(sk_c6,sk_c6)* -> . % 0.20/0.48 1145[3:Obv:1144.0] || -> . % 0.20/0.48 1153[2:Spt:1145.0,6.0,618.0] || equal(inverse(sk_c7),sk_c5)** -> . % 0.20/0.48 1154[2:Spt:1145.0,6.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.48 1155[2:MRR:9.1,1153.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.48 1156[2:MRR:7.1,1153.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.48 1157[2:MRR:10.0,1153.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.20/0.48 1158[2:MRR:8.0,1153.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.48 1160[2:SpR:1154.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.48 1167[2:SpR:1157.0,67.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c5)**. % 0.20/0.48 1169[2:Rew:1155.0,1167.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.48 1171[2:SpR:1158.0,67.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.20/0.48 1173[2:Rew:1156.0,1171.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.48 1175[2:SpR:1169.0,67.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.48 1177[2:Rew:1160.0,1175.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.48 1179[2:Rew:1177.0,1156.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.20/0.48 1180[2:Rew:1177.0,1153.0] || equal(inverse(sk_c6),sk_c5)** -> . % 0.20/0.48 1181[2:Rew:1177.0,1158.0] || -> equal(multiply(sk_c3,sk_c6),sk_c6)**. % 0.20/0.48 1182[2:Rew:1177.0,1160.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.20/0.48 1186[2:Rew:1177.0,1173.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.48 1187[2:Rew:1169.0,1186.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.48 1191[2:Rew:1187.0,1180.0] || equal(inverse(sk_c6),sk_c6)** -> . % 0.20/0.48 1192[2:Rew:28.0,1182.0,1187.0,1182.0] || -> equal(identity,sk_c6)**. % 0.20/0.48 1194[2:Rew:1192.0,974.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.48 1199[2:Rew:1194.0,1181.0] || -> equal(sk_c3,sk_c6)**. % 0.20/0.48 1201[2:Rew:1199.0,1179.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.48 1203[2:MRR:1201.0,1191.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_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 left_identity left_inverse associativity % 0.20/0.48 %------------------------------------------------------------------------------