%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP332-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.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:53 EDT 2022 % Result : Unsatisfiable 0.18s 0.49s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP332-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n018.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Tue Jun 14 09:05:13 EDT 2022 % 0.13/0.34 % CPUTime : % 0.18/0.49 % 0.18/0.49 SPASS V 3.9 % 0.18/0.49 SPASS beiseite: Proof found. % 0.18/0.49 % SZS status Theorem % 0.18/0.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.49 SPASS derived 838 clauses, backtracked 343 clauses, performed 11 splits and kept 722 clauses. % 0.18/0.49 SPASS allocated 63631 KBytes. % 0.18/0.49 SPASS spent 0:00:00.14 on the problem. % 0.18/0.49 0:00:00.04 for the input. % 0.18/0.49 0:00:00.00 for the FLOTTER CNF translation. % 0.18/0.49 0:00:00.01 for inferences. % 0.18/0.49 0:00:00.00 for the backtracking. % 0.18/0.49 0:00:00.07 for the reduction. % 0.18/0.49 % 0.18/0.49 % 0.18/0.49 Here is a proof with depth 5, length 373 : % 0.18/0.49 % SZS output start Refutation % 0.18/0.49 1[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.18/0.49 4[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.18/0.49 5[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.18/0.49 6[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.18/0.49 7[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.18/0.49 8[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.18/0.49 9[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.18/0.49 10[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.18/0.49 11[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.18/0.49 12[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.18/0.49 13[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 14[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.49 15[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c1),sk_c7)**. % 0.18/0.49 16[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 17[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 18[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c1),sk_c7)**. % 0.18/0.49 19[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 20[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.49 21[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c2),sk_c7)**. % 0.18/0.49 22[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 23[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 24[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c2),sk_c7)**. % 0.18/0.49 25[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.18/0.49 26[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.18/0.49 27[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.18/0.49 28[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.18/0.49 29[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.18/0.49 30[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.18/0.49 31[0:Inp] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(inverse(x),sk_c7) equal(multiply(u,sk_c8),y)*+ equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c6),sk_c7)** equal(multiply(x,sk_c7),sk_c8)** equal(multiply(sk_c8,y),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.18/0.49 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.18/0.49 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.18/0.49 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.18/0.49 35[1:Spt:31.0,31.4,31.8] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),v)*+ equal(multiply(sk_c8,v),sk_c7)** -> . % 0.18/0.49 37[2:Spt:1.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.18/0.49 40[3:Spt:19.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.49 42[4:Spt:13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.49 45[1:SpL:32.0,35.1] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.18/0.49 46[5:Spt:25.1] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.18/0.49 48[6:Spt:7.1] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.18/0.49 51[3:SpR:40.0,33.0] || -> equal(multiply(sk_c7,sk_c2),identity)**. % 0.18/0.49 52[4:SpR:42.0,33.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.18/0.49 53[1:SpL:33.0,35.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.18/0.49 60[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.18/0.49 61[5:SpR:46.0,34.0] || -> equal(multiply(sk_c2,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.18/0.49 63[3:SpR:51.0,34.0] || -> equal(multiply(sk_c7,multiply(sk_c2,u)),multiply(identity,u))**. % 0.18/0.49 64[4:SpR:52.0,34.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),multiply(identity,u))**. % 0.18/0.49 66[3:Rew:32.0,63.0] || -> equal(multiply(sk_c7,multiply(sk_c2,u)),u)**. % 0.18/0.49 67[4:Rew:32.0,64.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.18/0.49 68[0:Rew:32.0,60.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.18/0.49 72[5:SpR:46.0,66.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.18/0.49 78[6:SpR:48.0,67.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.18/0.49 79[6:Rew:37.0,78.0] || -> equal(sk_c7,sk_c6)**. % 0.18/0.49 81[6:Rew:79.0,37.0] || -> equal(multiply(sk_c6,sk_c8),sk_c6)**. % 0.18/0.49 82[6:Rew:79.0,40.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.18/0.49 84[6:Rew:79.0,46.0] || -> equal(multiply(sk_c2,sk_c6),sk_c6)**. % 0.18/0.49 89[6:Rew:79.0,72.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.18/0.49 93[6:Rew:79.0,53.2] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c6)** -> . % 0.18/0.49 115[0:SpR:68.0,68.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.18/0.49 117[0:SpR:32.0,68.0] || -> equal(multiply(inverse(identity),u),u)**. % 0.18/0.49 118[0:SpR:33.0,68.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.49 120[6:SpR:81.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c8)**. % 0.18/0.49 125[6:Rew:33.0,120.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 126[6:Rew:125.0,32.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 127[6:Rew:125.0,33.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.18/0.49 132[6:Rew:125.0,93.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c6)** -> . % 0.18/0.49 141[6:Rew:125.0,118.0] || -> equal(multiply(inverse(inverse(u)),sk_c8),u)**. % 0.18/0.49 142[6:Rew:115.0,141.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 149[6:Rew:126.0,132.2] || equal(inverse(inverse(sk_c8)),sk_c8)** equal(sk_c8,u) equal(u,sk_c6)* -> . % 0.18/0.49 153[6:SpR:89.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c6)**. % 0.18/0.49 155[6:Rew:127.0,153.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 157[6:Rew:155.0,82.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.18/0.49 159[6:Rew:155.0,84.0] || -> equal(multiply(sk_c2,sk_c8),sk_c8)**. % 0.18/0.49 169[6:Rew:155.0,149.2] || equal(inverse(inverse(sk_c8)),sk_c8)** equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.49 173[6:Rew:142.0,159.0] || -> equal(sk_c2,sk_c8)**. % 0.18/0.49 174[6:Rew:173.0,157.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.49 187[6:Obv:169.1] || equal(inverse(inverse(sk_c8)),sk_c8)** equal(u,sk_c8)* -> . % 0.18/0.49 188[6:Con:187.1] || equal(inverse(inverse(sk_c8)),sk_c8)** -> . % 0.18/0.49 189[6:Rew:174.0,188.0,174.0,188.0] || equal(sk_c8,sk_c8)* -> . % 0.18/0.49 190[6:Obv:189.0] || -> . % 0.18/0.49 191[6:Spt:190.0,7.1,48.0] || equal(multiply(sk_c1,sk_c7),sk_c8)** -> . % 0.18/0.49 192[6:Spt:190.0,7.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 193[0:Rew:115.0,118.0] || -> equal(multiply(u,identity),u)**. % 0.18/0.49 194[6:MRR:12.1,191.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 195[6:MRR:9.1,191.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.49 196[6:MRR:11.1,191.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 197[6:MRR:10.1,191.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 198[6:MRR:8.1,191.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.49 215[4:SpR:52.0,68.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.18/0.49 217[4:Rew:193.0,215.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.49 221[4:SpR:217.0,68.0] || -> equal(multiply(sk_c1,multiply(sk_c7,u)),u)**. % 0.18/0.49 224[6:SpR:196.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 226[6:Rew:194.0,224.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 227[6:Rew:197.0,226.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 228[6:Rew:227.0,192.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.49 229[6:Rew:227.0,42.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.18/0.49 232[6:Rew:227.0,52.0] || -> equal(multiply(sk_c8,sk_c1),identity)**. % 0.18/0.49 233[6:Rew:227.0,217.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.18/0.49 234[6:Rew:227.0,51.0] || -> equal(multiply(sk_c8,sk_c2),identity)**. % 0.18/0.49 240[6:Rew:227.0,61.0] || -> equal(multiply(sk_c2,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 242[6:Rew:227.0,221.0] || -> equal(multiply(sk_c1,multiply(sk_c8,u)),u)**. % 0.18/0.49 246[6:Rew:227.0,198.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.18/0.49 250[6:Rew:227.0,45.2] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.49 280[6:SpR:234.0,68.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c2)**. % 0.18/0.49 282[6:Rew:233.0,280.0] || -> equal(multiply(sk_c1,identity),sk_c2)**. % 0.18/0.49 283[6:Rew:193.0,282.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.49 288[6:Rew:283.0,240.0] || -> equal(multiply(sk_c1,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 291[6:SpR:246.0,68.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.18/0.49 293[6:Rew:228.0,291.0,195.0,291.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 297[6:Rew:293.0,288.0] || -> equal(multiply(sk_c1,multiply(sk_c8,u)),multiply(sk_c8,u))**. % 0.18/0.49 301[6:Rew:242.0,297.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 302[6:Rew:301.0,232.0] || -> equal(identity,sk_c1)**. % 0.18/0.49 309[6:Rew:301.0,250.2] || equal(inverse(identity),sk_c8)** equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.49 329[6:Obv:309.1] || equal(inverse(identity),sk_c8)** equal(u,sk_c8)* -> . % 0.18/0.49 330[6:Con:329.1] || equal(inverse(identity),sk_c8)** -> . % 0.18/0.49 331[6:Rew:302.0,330.0] || equal(inverse(sk_c1),sk_c8)** -> . % 0.18/0.49 332[6:Rew:229.0,331.0] || equal(sk_c8,sk_c8)* -> . % 0.18/0.49 333[6:Obv:332.0] || -> . % 0.18/0.49 337[5:Spt:333.0,25.1,46.0] || equal(multiply(sk_c2,sk_c6),sk_c7)** -> . % 0.18/0.49 338[5:Spt:333.0,25.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 339[5:MRR:30.1,337.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 341[5:MRR:29.1,337.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 342[5:MRR:28.1,337.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 363[2:SpR:37.0,68.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.18/0.49 365[4:Rew:217.0,363.0] || -> equal(multiply(sk_c1,sk_c6),sk_c8)**. % 0.18/0.49 367[3:SpR:51.0,68.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c2)**. % 0.18/0.49 369[4:Rew:217.0,367.0] || -> equal(multiply(sk_c1,identity),sk_c2)**. % 0.18/0.49 370[4:Rew:193.0,369.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.49 373[5:Rew:370.0,337.0] || equal(multiply(sk_c1,sk_c6),sk_c7)** -> . % 0.18/0.49 375[5:Rew:365.0,373.0] || equal(sk_c7,sk_c8)** -> . % 0.18/0.49 379[5:SpR:341.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 381[5:Rew:339.0,379.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 382[5:Rew:342.0,381.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 383[5:MRR:382.0,375.0] || -> . % 0.18/0.49 384[4:Spt:383.0,13.0,42.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.18/0.49 385[4:Spt:383.0,13.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 386[3:Rew:193.0,367.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.18/0.49 387[3:Rew:386.0,363.0] || -> equal(multiply(sk_c2,sk_c6),sk_c8)**. % 0.18/0.49 388[4:MRR:18.1,384.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 389[4:MRR:15.1,384.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.49 390[4:MRR:17.0,384.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 391[4:MRR:16.0,384.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 392[4:MRR:14.0,384.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.49 400[3:SpR:386.0,68.0] || -> equal(multiply(sk_c2,multiply(sk_c7,u)),u)**. % 0.18/0.49 411[3:SpR:387.0,34.0] || -> equal(multiply(sk_c2,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 416[4:SpR:390.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 418[4:Rew:388.0,416.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 419[4:Rew:391.0,418.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 420[4:Rew:419.0,37.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.49 422[4:Rew:419.0,40.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.18/0.49 424[4:Rew:419.0,51.0] || -> equal(multiply(sk_c8,sk_c2),identity)**. % 0.18/0.49 430[4:Rew:419.0,45.2] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.49 435[4:Rew:419.0,392.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.18/0.49 438[4:Rew:419.0,400.0] || -> equal(multiply(sk_c2,multiply(sk_c8,u)),u)**. % 0.18/0.49 461[4:SpR:435.0,68.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.18/0.49 463[4:Rew:420.0,461.0,389.0,461.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 466[4:Rew:463.0,411.0] || -> equal(multiply(sk_c2,multiply(sk_c8,u)),multiply(sk_c8,u))**. % 0.18/0.49 475[4:Rew:438.0,466.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 476[4:Rew:475.0,424.0] || -> equal(identity,sk_c2)**. % 0.18/0.49 485[4:Rew:475.0,430.2] || equal(inverse(identity),sk_c8)** equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.49 493[4:Obv:485.1] || equal(inverse(identity),sk_c8)** equal(u,sk_c8)* -> . % 0.18/0.49 494[4:Con:493.1] || equal(inverse(identity),sk_c8)** -> . % 0.18/0.49 495[4:Rew:476.0,494.0] || equal(inverse(sk_c2),sk_c8)** -> . % 0.18/0.49 496[4:Rew:422.0,495.0] || equal(sk_c8,sk_c8)* -> . % 0.18/0.49 497[4:Obv:496.0] || -> . % 0.18/0.49 501[3:Spt:497.0,19.0,40.0] || equal(inverse(sk_c2),sk_c7)** -> . % 0.18/0.49 502[3:Spt:497.0,19.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 503[3:MRR:24.1,501.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 504[3:MRR:21.1,501.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.49 505[3:MRR:23.0,501.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 506[3:MRR:22.0,501.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 507[3:MRR:20.0,501.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.49 519[3:SpR:505.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 521[3:Rew:503.0,519.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 522[3:Rew:506.0,521.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 523[3:Rew:522.0,502.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.49 526[3:Rew:522.0,363.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c8)**. % 0.18/0.49 529[3:Rew:522.0,506.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 530[3:Rew:522.0,507.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.18/0.49 532[3:Rew:522.0,53.2] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.49 544[3:SpR:529.0,68.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c5)**. % 0.18/0.49 546[3:Rew:33.0,544.0] || -> equal(identity,sk_c5)**. % 0.18/0.49 547[3:Rew:546.0,32.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.49 548[3:Rew:546.0,193.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.49 549[3:Rew:546.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.18/0.49 552[3:Rew:546.0,532.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(sk_c5,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.49 557[3:SpR:530.0,68.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.18/0.49 559[3:Rew:523.0,557.0,504.0,557.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 561[3:Rew:559.0,526.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c8)**. % 0.18/0.49 564[3:Rew:549.0,561.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.49 567[3:Rew:564.0,547.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 568[3:Rew:564.0,548.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 572[3:Rew:564.0,552.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.49 579[3:Rew:568.0,530.0] || -> equal(sk_c3,sk_c8)**. % 0.18/0.49 581[3:Rew:579.0,504.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.49 596[3:Rew:567.0,572.2,581.0,572.0,581.0,572.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.49 597[3:Obv:596.1] || equal(u,sk_c8)* -> . % 0.18/0.49 598[3:UnC:597.0,522.0] || -> . % 0.18/0.49 600[2:Spt:598.0,1.1,37.0] || equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.18/0.49 601[2:Spt:598.0,1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 602[2:MRR:6.1,600.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 604[2:MRR:5.1,600.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 605[2:MRR:4.1,600.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 615[2:SpR:604.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 617[2:Rew:602.0,615.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 618[2:Rew:605.0,617.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 619[2:Rew:618.0,601.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.49 620[2:Rew:618.0,600.0] || equal(multiply(sk_c8,sk_c8),sk_c6)** -> . % 0.18/0.49 630[2:Rew:619.0,620.0] || equal(sk_c6,sk_c6)* -> . % 0.18/0.49 631[2:Obv:630.0] || -> . % 0.18/0.49 632[1:Spt:631.0,31.1,31.2,31.3,31.5,31.6,31.7,31.9,31.10] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.18/0.49 634[2:Spt:1.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.18/0.49 635[2:Rew:634.0,632.7] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6)** equal(sk_c6,sk_c6) -> . % 0.18/0.49 637[2:Obv:635.7] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6)** -> . % 0.18/0.49 640[2:SpR:634.0,68.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.18/0.49 642[3:Spt:13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.49 643[3:SpR:642.0,68.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.18/0.49 645[4:Spt:19.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.49 648[5:Spt:7.1] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.18/0.49 650[5:SpR:648.0,68.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.18/0.49 652[5:Rew:634.0,650.0,642.0,650.0] || -> equal(sk_c7,sk_c6)**. % 0.18/0.49 654[5:Rew:652.0,642.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.18/0.49 655[5:Rew:652.0,645.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.18/0.49 656[5:Rew:652.0,648.0] || -> equal(multiply(sk_c1,sk_c6),sk_c8)**. % 0.18/0.49 658[5:Rew:652.0,637.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c6),sk_c6)** -> . % 0.18/0.49 660[5:Rew:652.0,26.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c6)**. % 0.18/0.49 663[5:Rew:652.0,27.1] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c2,sk_c6),sk_c6)**. % 0.18/0.49 665[5:Rew:652.0,640.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c8)**. % 0.18/0.49 669[5:Rew:33.0,665.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 670[5:Rew:669.0,193.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 671[5:Rew:669.0,32.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 672[5:Rew:669.0,117.0] || -> equal(multiply(inverse(sk_c8),u),u)**. % 0.18/0.49 673[5:Rew:669.0,33.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.18/0.49 676[5:Rew:670.0,660.0,652.0,660.0] || -> equal(sk_c3,sk_c6) equal(multiply(sk_c2,sk_c6),sk_c6)**. % 0.18/0.49 677[5:Rew:676.0,663.0] || -> equal(inverse(sk_c6),sk_c8) equal(multiply(sk_c2,sk_c6),sk_c6)**. % 0.18/0.49 681[5:Rew:671.0,658.6,652.0,658.5,652.0,658.4,670.0,658.3,652.0,658.3,652.0,658.2,652.0,658.1] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(u,sk_c6) equal(multiply(v,sk_c6),sk_c6)** equal(multiply(w,sk_c6),sk_c8)** equal(sk_c6,sk_c6) -> . % 0.18/0.49 682[5:Obv:681.6] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(u,sk_c6) equal(multiply(v,sk_c6),sk_c6)** equal(multiply(w,sk_c6),sk_c8)** -> . % 0.18/0.49 708[5:SpR:672.0,670.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.49 718[5:SpR:654.0,673.0] || -> equal(multiply(sk_c6,sk_c1),sk_c8)**. % 0.18/0.49 719[5:SpR:655.0,673.0] || -> equal(multiply(sk_c6,sk_c2),sk_c8)**. % 0.18/0.49 728[5:SpR:718.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c1)**. % 0.18/0.49 730[5:Rew:670.0,728.0] || -> equal(inverse(sk_c6),sk_c1)**. % 0.18/0.49 731[5:Rew:730.0,677.0] || -> equal(sk_c1,sk_c8) equal(multiply(sk_c2,sk_c6),sk_c6)**. % 0.18/0.49 737[5:SpR:719.0,68.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c2)**. % 0.18/0.49 739[5:Rew:670.0,737.0,730.0,737.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.49 743[5:Rew:739.0,731.1] || -> equal(sk_c1,sk_c8) equal(multiply(sk_c1,sk_c6),sk_c6)**. % 0.18/0.49 747[5:Rew:656.0,743.1] || -> equal(sk_c1,sk_c8)** equal(sk_c6,sk_c8). % 0.18/0.49 753[6:Spt:747.1] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 761[6:Rew:753.0,682.1] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8) equal(inverse(w),sk_c6) equal(u,sk_c6) equal(multiply(v,sk_c6),sk_c6)** equal(multiply(w,sk_c6),sk_c8)** -> . % 0.18/0.49 771[6:Rew:753.0,761.5,753.0,761.4,753.0,761.3,753.0,761.2] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(u,sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** -> . % 0.18/0.49 772[6:Con:771.2] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8) equal(u,sk_c8) equal(multiply(v,sk_c8),sk_c8)** -> . % 0.18/0.49 773[6:Rew:670.0,772.3] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(u,sk_c8) equal(v,sk_c8) -> . % 0.18/0.49 774[6:Con:773.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.18/0.49 784[6:SpL:708.0,774.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.18/0.49 786[6:Obv:784.1] || -> . % 0.18/0.49 787[6:Spt:786.0,747.1,753.0] || equal(sk_c6,sk_c8)** -> . % 0.18/0.49 788[6:Spt:786.0,747.0] || -> equal(sk_c1,sk_c8)**. % 0.18/0.49 791[6:Rew:788.0,654.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.18/0.49 792[6:Rew:708.0,791.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 795[6:Rew:792.0,787.0] || equal(sk_c8,sk_c8)* -> . % 0.18/0.49 796[6:Obv:795.0] || -> . % 0.18/0.49 807[5:Spt:796.0,7.1,648.0] || equal(multiply(sk_c1,sk_c7),sk_c8)** -> . % 0.18/0.49 808[5:Spt:796.0,7.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 809[5:MRR:12.1,807.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 810[5:MRR:9.1,807.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.49 811[5:MRR:11.1,807.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 812[5:MRR:10.1,807.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 813[5:MRR:8.1,807.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.49 830[5:SpR:811.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 832[5:Rew:809.0,830.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 833[5:Rew:812.0,832.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 834[5:Rew:833.0,808.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.49 838[5:Rew:833.0,640.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c8)**. % 0.18/0.49 839[5:Rew:833.0,807.0] || equal(multiply(sk_c1,sk_c8),sk_c8)** -> . % 0.18/0.49 841[5:Rew:833.0,643.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.18/0.49 843[5:Rew:833.0,812.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 844[5:Rew:833.0,813.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.18/0.49 861[5:SpR:843.0,68.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c5)**. % 0.18/0.49 863[5:Rew:33.0,861.0] || -> equal(identity,sk_c5)**. % 0.18/0.49 864[5:Rew:863.0,32.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.49 865[5:Rew:863.0,193.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.49 866[5:Rew:863.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.18/0.49 872[5:SpR:844.0,68.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.18/0.49 874[5:Rew:834.0,872.0,810.0,872.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 876[5:Rew:874.0,838.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c8)**. % 0.18/0.49 879[5:Rew:866.0,876.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.49 882[5:Rew:879.0,864.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 883[5:Rew:879.0,865.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 887[5:Rew:882.0,841.0] || -> equal(multiply(sk_c1,u),u)**. % 0.18/0.49 893[5:Rew:883.0,839.0] || equal(sk_c1,sk_c8)** -> . % 0.18/0.49 924[5:SpR:887.0,883.0] || -> equal(sk_c1,sk_c8)**. % 0.18/0.49 926[5:MRR:924.0,893.0] || -> . % 0.18/0.49 928[4:Spt:926.0,19.0,645.0] || equal(inverse(sk_c2),sk_c7)** -> . % 0.18/0.49 929[4:Spt:926.0,19.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 930[4:MRR:24.1,928.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 931[4:MRR:21.1,928.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.49 932[4:MRR:23.0,928.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 933[4:MRR:22.0,928.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 934[4:MRR:20.0,928.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.49 935[4:Rew:929.0,637.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(sk_c6,sk_c6) -> . % 0.18/0.49 936[4:Obv:935.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.18/0.49 952[4:SpR:932.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 954[4:Rew:930.0,952.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 955[4:Rew:933.0,954.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 956[4:Rew:955.0,929.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.49 960[4:Rew:955.0,640.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c8)**. % 0.18/0.49 963[4:Rew:955.0,933.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 964[4:Rew:955.0,934.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.18/0.49 965[4:Rew:955.0,936.1] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.18/0.49 969[4:Rew:955.0,965.5,955.0,965.4,955.0,965.3,955.0,965.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c6),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** -> . % 0.18/0.49 970[4:Con:969.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c6),sk_c8)** -> . % 0.18/0.49 979[4:SpR:963.0,68.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c5)**. % 0.18/0.49 981[4:Rew:33.0,979.0] || -> equal(identity,sk_c5)**. % 0.18/0.49 982[4:Rew:981.0,193.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.49 985[4:Rew:981.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.18/0.49 990[4:SpR:964.0,68.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.18/0.49 992[4:Rew:956.0,990.0,931.0,990.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 994[4:Rew:992.0,960.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c8)**. % 0.18/0.49 996[4:Rew:992.0,970.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c8)** -> . % 0.18/0.49 997[4:Rew:985.0,994.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.49 1000[4:Rew:997.0,982.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 1004[4:Rew:1000.0,964.0] || -> equal(sk_c3,sk_c8)**. % 0.18/0.49 1006[4:Rew:1004.0,931.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.49 1017[4:Con:996.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.18/0.49 1018[4:Rew:1000.0,1017.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.18/0.49 1086[4:SpL:1006.0,1018.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.18/0.49 1088[4:Obv:1086.1] || -> . % 0.18/0.49 1089[3:Spt:1088.0,13.0,642.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.18/0.49 1090[3:Spt:1088.0,13.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 1091[3:MRR:18.1,1089.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 1092[3:MRR:15.1,1089.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.49 1093[3:MRR:17.0,1089.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 1094[3:MRR:16.0,1089.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 1095[3:MRR:14.0,1089.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.49 1096[3:Rew:1090.0,637.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(sk_c6,sk_c6) -> . % 0.18/0.49 1097[3:Obv:1096.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.18/0.49 1111[3:SpR:1093.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 1113[3:Rew:1091.0,1111.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 1114[3:Rew:1094.0,1113.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 1115[3:Rew:1114.0,1090.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.49 1118[3:Rew:1114.0,640.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c8)**. % 0.18/0.49 1120[3:Rew:1114.0,1094.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 1121[3:Rew:1114.0,1095.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.18/0.49 1122[3:Rew:1114.0,1097.1] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.18/0.49 1126[3:Rew:1114.0,1122.5,1114.0,1122.4,1114.0,1122.3,1114.0,1122.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c6),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** -> . % 0.18/0.49 1127[3:Con:1126.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c6),sk_c8)** -> . % 0.18/0.49 1134[3:SpR:1120.0,68.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c5)**. % 0.18/0.49 1136[3:Rew:33.0,1134.0] || -> equal(identity,sk_c5)**. % 0.18/0.49 1138[3:Rew:1136.0,193.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.49 1139[3:Rew:1136.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.18/0.49 1144[3:SpR:1121.0,68.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.18/0.49 1146[3:Rew:1115.0,1144.0,1092.0,1144.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.49 1148[3:Rew:1146.0,1118.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c8)**. % 0.18/0.49 1150[3:Rew:1146.0,1127.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c8)** -> . % 0.18/0.49 1151[3:Rew:1139.0,1148.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.49 1155[3:Rew:1151.0,1138.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 1161[3:Rew:1155.0,1121.0] || -> equal(sk_c3,sk_c8)**. % 0.18/0.49 1163[3:Rew:1161.0,1092.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.49 1170[3:Con:1150.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.18/0.49 1171[3:Rew:1155.0,1170.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.18/0.49 1199[3:SpL:1163.0,1171.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.18/0.49 1200[3:Obv:1199.1] || -> . % 0.18/0.49 1201[2:Spt:1200.0,1.1,634.0] || equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.18/0.49 1202[2:Spt:1200.0,1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.49 1203[2:MRR:6.1,1201.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.49 1205[2:MRR:5.1,1201.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.49 1206[2:MRR:4.1,1201.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.49 1216[2:SpR:1205.0,68.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.18/0.49 1218[2:Rew:1203.0,1216.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.49 1219[2:Rew:1206.0,1218.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.49 1220[2:Rew:1219.0,1202.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.49 1221[2:Rew:1219.0,1201.0] || equal(multiply(sk_c8,sk_c8),sk_c6)** -> . % 0.18/0.49 1226[2:Rew:1220.0,1221.0] || equal(sk_c6,sk_c6)* -> . % 0.18/0.49 1227[2:Obv:1226.0] || -> . % 0.18/0.49 % SZS output end Refutation % 0.18/0.49 Formulae used in the proof : prove_this_1 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.18/0.49 %------------------------------------------------------------------------------