%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP249-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:46:31 EDT 2022 % Result : Unsatisfiable 0.36s 0.53s % Output : Refutation 0.36s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP249-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 13 14:27:39 EDT 2022 % 0.12/0.34 % CPUTime : % 0.36/0.53 % 0.36/0.53 SPASS V 3.9 % 0.36/0.53 SPASS beiseite: Proof found. % 0.36/0.53 % SZS status Theorem % 0.36/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.36/0.53 SPASS derived 1694 clauses, backtracked 447 clauses, performed 12 splits and kept 861 clauses. % 0.36/0.53 SPASS allocated 64497 KBytes. % 0.36/0.53 SPASS spent 0:00:00.18 on the problem. % 0.36/0.53 0:00:00.04 for the input. % 0.36/0.53 0:00:00.00 for the FLOTTER CNF translation. % 0.36/0.53 0:00:00.01 for inferences. % 0.36/0.53 0:00:00.00 for the backtracking. % 0.36/0.53 0:00:00.10 for the reduction. % 0.36/0.53 % 0.36/0.53 % 0.36/0.53 Here is a proof with depth 5, length 354 : % 0.36/0.53 % SZS output start Refutation % 0.36/0.53 1[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.53 2[0:Inp] || -> equal(inverse(sk_c4),sk_c9) equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.53 3[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c9)** equal(multiply(sk_c1,sk_c9),sk_c8). % 0.36/0.53 4[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c8)** equal(multiply(sk_c1,sk_c9),sk_c8). % 0.36/0.53 5[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.53 7[0:Inp] || -> equal(inverse(sk_c8),sk_c7)** equal(inverse(sk_c1),sk_c9). % 0.36/0.53 8[0:Inp] || -> equal(inverse(sk_c4),sk_c9)** equal(inverse(sk_c1),sk_c9). % 0.36/0.53 9[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c4,sk_c8),sk_c9)**. % 0.36/0.53 10[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.36/0.53 11[0:Inp] || -> equal(inverse(sk_c5),sk_c6)** equal(inverse(sk_c1),sk_c9). % 0.36/0.53 12[0:Inp] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.36/0.53 13[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 14[0:Inp] || -> equal(inverse(sk_c4),sk_c9) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 15[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c9) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 16[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 17[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 18[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 19[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 20[0:Inp] || -> equal(inverse(sk_c4),sk_c9) equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 21[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c4,sk_c8),sk_c9)**. % 0.36/0.53 22[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.36/0.53 23[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 24[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.36/0.53 25[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 26[0:Inp] || -> equal(inverse(sk_c4),sk_c9) equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 27[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c4,sk_c8),sk_c9)**. % 0.36/0.53 28[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.36/0.53 29[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 30[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.36/0.53 31[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c9)**. % 0.36/0.53 32[0:Inp] || -> equal(inverse(sk_c4),sk_c9) equal(multiply(sk_c3,sk_c7),sk_c9)**. % 0.36/0.53 33[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c9) equal(multiply(sk_c3,sk_c7),sk_c9)**. % 0.36/0.53 35[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c3,sk_c7),sk_c9)**. % 0.36/0.53 37[0:Inp] || equal(inverse(u),v) equal(inverse(w),sk_c9) equal(inverse(x),sk_c9) equal(inverse(y),sk_c8) equal(inverse(z),sk_c9) equal(inverse(sk_c8),sk_c7) equal(multiply(u,v),sk_c8)**+ equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c8),sk_c9)** equal(multiply(x,sk_c7),sk_c9)** equal(multiply(y,sk_c8),sk_c7)** equal(multiply(z,sk_c9),sk_c8)** -> . % 0.36/0.53 38[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.36/0.53 39[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.36/0.53 40[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.36/0.53 41[1:Spt:37.0,37.6,37.7] || equal(inverse(u),v) equal(multiply(u,v),sk_c8)**+ equal(multiply(v,sk_c7),sk_c8)** -> . % 0.36/0.53 42[2:Spt:25.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.36/0.53 44[3:Spt:29.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.36/0.53 50[4:Spt:30.1] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.36/0.53 54[5:Spt:28.1] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.36/0.53 56[5:SpL:54.0,41.1] || equal(inverse(sk_c5),sk_c6) equal(sk_c8,sk_c8) equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.36/0.53 57[5:Obv:56.1] || equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.36/0.53 58[5:Rew:50.0,57.1,44.0,57.0] || equal(sk_c6,sk_c6)* equal(sk_c8,sk_c8) -> . % 0.36/0.53 59[5:Obv:58.1] || -> . % 0.36/0.53 60[5:Spt:59.0,28.1,54.0] || equal(multiply(sk_c5,sk_c6),sk_c8)** -> . % 0.36/0.53 61[5:Spt:59.0,28.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 62[5:MRR:22.1,60.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 65[5:MRR:16.0,60.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 83[2:SpR:42.0,39.0] || -> equal(multiply(sk_c7,sk_c8),identity)**. % 0.36/0.53 87[5:SpR:62.0,39.0] || -> equal(multiply(sk_c8,sk_c2),identity)**. % 0.36/0.53 95[0:SpR:39.0,40.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.36/0.53 99[0:Rew:38.0,95.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.36/0.53 101[2:SpR:83.0,40.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),multiply(identity,u))**. % 0.36/0.53 103[2:SpL:83.0,41.1] || equal(inverse(sk_c7),sk_c8) equal(identity,sk_c8) equal(multiply(sk_c8,sk_c7),sk_c8)** -> . % 0.36/0.53 104[2:Rew:38.0,101.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),u)**. % 0.36/0.53 129[5:SpR:87.0,104.0] || -> equal(multiply(sk_c7,identity),sk_c2)**. % 0.36/0.53 130[2:SpL:104.0,41.1] || equal(multiply(sk_c8,u),inverse(sk_c7)) equal(u,sk_c8) equal(multiply(multiply(sk_c8,u),sk_c7),sk_c8)** -> . % 0.36/0.53 132[2:Rew:40.0,130.2] || equal(multiply(sk_c8,u),inverse(sk_c7)) equal(u,sk_c8) equal(multiply(sk_c8,multiply(u,sk_c7)),sk_c8)** -> . % 0.36/0.53 133[5:SpR:129.0,40.0] || -> equal(multiply(sk_c7,multiply(identity,u)),multiply(sk_c2,u))**. % 0.36/0.53 136[5:Rew:38.0,133.0] || -> equal(multiply(sk_c2,u),multiply(sk_c7,u))**. % 0.36/0.53 137[5:Rew:136.0,65.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.36/0.53 141[5:Rew:83.0,137.0] || -> equal(identity,sk_c7)**. % 0.36/0.53 142[5:Rew:141.0,38.0] || -> equal(multiply(sk_c7,u),u)**. % 0.36/0.53 144[5:Rew:141.0,83.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.36/0.53 156[5:Rew:141.0,103.1] || equal(inverse(sk_c7),sk_c8) equal(sk_c7,sk_c8) equal(multiply(sk_c8,sk_c7),sk_c8)** -> . % 0.36/0.53 158[5:Rew:142.0,104.0] || -> equal(multiply(sk_c8,u),u)**. % 0.36/0.53 164[5:Rew:142.0,144.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.53 166[5:Rew:164.0,42.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.36/0.53 219[5:Rew:164.0,156.2,158.0,156.2,164.0,156.1,166.0,156.0,164.0,156.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.36/0.53 220[5:Obv:219.2] || -> . % 0.36/0.53 225[4:Spt:220.0,30.1,50.0] || equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.36/0.53 226[4:Spt:220.0,30.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 227[4:MRR:24.1,225.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 230[4:MRR:18.0,225.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 259[4:SpR:227.0,39.0] || -> equal(multiply(sk_c8,sk_c2),identity)**. % 0.36/0.53 273[0:SpR:99.0,99.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.36/0.53 281[2:SpR:83.0,99.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c8)**. % 0.36/0.53 282[4:SpR:230.0,99.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c8)**. % 0.36/0.53 285[0:SpR:39.0,99.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.36/0.53 286[4:SpR:259.0,99.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c2)**. % 0.36/0.53 309[4:Rew:227.0,282.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.36/0.53 312[4:Rew:42.0,286.0] || -> equal(multiply(sk_c7,identity),sk_c2)**. % 0.36/0.53 316[0:Rew:273.0,285.0] || -> equal(multiply(u,identity),u)**. % 0.36/0.53 317[4:Rew:316.0,312.0] || -> equal(sk_c2,sk_c7)**. % 0.36/0.53 319[2:Rew:316.0,281.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.36/0.53 322[4:Rew:317.0,230.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.36/0.53 323[4:Rew:317.0,259.0] || -> equal(multiply(sk_c8,sk_c7),identity)**. % 0.36/0.53 326[2:Rew:319.0,132.0] || equal(multiply(sk_c8,u),sk_c8) equal(u,sk_c8) equal(multiply(sk_c8,multiply(u,sk_c7)),sk_c8)** -> . % 0.36/0.53 328[4:Rew:83.0,322.0] || -> equal(identity,sk_c7)**. % 0.36/0.53 331[4:Rew:328.0,38.0] || -> equal(multiply(sk_c7,u),u)**. % 0.36/0.53 337[4:Rew:328.0,316.0] || -> equal(multiply(u,sk_c7),u)**. % 0.36/0.53 338[4:Rew:309.0,323.0,328.0,323.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.53 352[4:Rew:338.0,331.0] || -> equal(multiply(sk_c8,u),u)**. % 0.36/0.53 355[4:Rew:338.0,337.0] || -> equal(multiply(u,sk_c8),u)**. % 0.36/0.53 386[4:Rew:355.0,326.2,338.0,326.2,352.0,326.2,352.0,326.0] || equal(u,sk_c8)* equal(u,sk_c8)* equal(u,sk_c8)* -> . % 0.36/0.53 387[4:Obv:386.1] || equal(u,sk_c8)* -> . % 0.36/0.53 388[4:UnC:387.0,99.0] || -> . % 0.36/0.53 390[3:Spt:388.0,29.0,44.0] || equal(inverse(sk_c5),sk_c6)** -> . % 0.36/0.53 391[3:Spt:388.0,29.1] || -> equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 392[3:MRR:23.0,390.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 395[3:MRR:17.0,390.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 403[2:SpR:319.0,99.0] || -> equal(multiply(sk_c8,multiply(sk_c7,u)),u)**. % 0.36/0.53 419[3:SpR:395.0,99.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c8)**. % 0.36/0.53 421[3:Rew:392.0,419.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.36/0.53 432[3:SpR:421.0,99.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c7)**. % 0.36/0.53 434[3:Rew:83.0,432.0,42.0,432.0] || -> equal(identity,sk_c7)**. % 0.36/0.53 437[3:Rew:434.0,38.0] || -> equal(multiply(sk_c7,u),u)**. % 0.36/0.53 438[3:Rew:434.0,316.0] || -> equal(multiply(u,sk_c7),u)**. % 0.36/0.53 443[3:Rew:437.0,403.0] || -> equal(multiply(sk_c8,u),u)**. % 0.36/0.53 453[3:Rew:438.0,326.2] || equal(multiply(sk_c8,u),sk_c8)** equal(u,sk_c8) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.36/0.53 469[3:Obv:453.0] || equal(u,sk_c8) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.36/0.53 470[3:Rew:443.0,469.1] || equal(u,sk_c8)* equal(u,sk_c8)* -> . % 0.36/0.53 471[3:Obv:470.0] || equal(u,sk_c8)* -> . % 0.36/0.53 472[3:UnC:471.0,392.0] || -> . % 0.36/0.53 473[2:Spt:472.0,25.0,42.0] || equal(inverse(sk_c8),sk_c7)** -> . % 0.36/0.53 474[2:Spt:472.0,25.1] || -> equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 475[2:MRR:19.0,473.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 476[2:MRR:7.0,473.0] || -> equal(inverse(sk_c1),sk_c9)**. % 0.36/0.53 477[2:MRR:31.0,473.0] || -> equal(multiply(sk_c3,sk_c7),sk_c9)**. % 0.36/0.53 478[2:MRR:13.0,473.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 479[2:MRR:1.0,473.0] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.53 487[2:SpR:477.0,99.0] || -> equal(multiply(inverse(sk_c3),sk_c9),sk_c7)**. % 0.36/0.53 489[2:Rew:474.0,487.0] || -> equal(multiply(sk_c9,sk_c9),sk_c7)**. % 0.36/0.53 491[2:SpR:478.0,99.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c8)**. % 0.36/0.53 493[2:Rew:475.0,491.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.36/0.53 495[2:SpR:479.0,99.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c9)**. % 0.36/0.53 497[2:Rew:476.0,495.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.36/0.53 499[2:SpR:489.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c7),sk_c9)**. % 0.36/0.53 505[2:SpR:493.0,99.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c7)**. % 0.36/0.53 507[2:Rew:39.0,505.0] || -> equal(identity,sk_c7)**. % 0.36/0.53 509[2:Rew:507.0,316.0] || -> equal(multiply(u,sk_c7),u)**. % 0.36/0.53 518[2:Rew:509.0,499.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.36/0.53 536[2:SpR:497.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c9),sk_c8)**. % 0.36/0.53 538[2:Rew:489.0,536.0,518.0,536.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.53 539[2:Rew:538.0,473.0] || equal(inverse(sk_c8),sk_c8)** -> . % 0.36/0.53 540[2:Rew:538.0,478.0] || -> equal(multiply(sk_c2,sk_c8),sk_c8)**. % 0.36/0.53 544[2:Rew:538.0,509.0] || -> equal(multiply(u,sk_c8),u)**. % 0.36/0.53 552[2:Rew:544.0,540.0] || -> equal(sk_c2,sk_c8)**. % 0.36/0.53 553[2:Rew:552.0,475.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.36/0.53 554[2:MRR:553.0,539.0] || -> . % 0.36/0.53 559[1:Spt:554.0,37.1,37.2,37.3,37.4,37.5,37.8,37.9,37.10,37.11] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(inverse(sk_c8),sk_c7) equal(multiply(u,sk_c8),sk_c9)**+ equal(multiply(v,sk_c7),sk_c9)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 561[2:Spt:19.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.36/0.53 562[2:Rew:561.0,559.4] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(sk_c7,sk_c7) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c7),sk_c9)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 564[2:Obv:562.4] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c7),sk_c9)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 566[2:SpR:561.0,99.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),u)**. % 0.36/0.53 568[3:Spt:26.0] || -> equal(inverse(sk_c4),sk_c9)**. % 0.36/0.53 571[4:Spt:29.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.36/0.53 572[4:SpR:571.0,99.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),u)**. % 0.36/0.53 574[5:Spt:27.1] || -> equal(multiply(sk_c4,sk_c8),sk_c9)**. % 0.36/0.53 576[5:SpR:574.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c8)**. % 0.36/0.53 578[5:Rew:568.0,576.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.36/0.53 580[5:SpR:578.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.36/0.53 582[6:Spt:28.1] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.36/0.53 584[6:SpR:582.0,99.0] || -> equal(multiply(inverse(sk_c5),sk_c8),sk_c6)**. % 0.36/0.53 586[6:Rew:571.0,584.0] || -> equal(multiply(sk_c6,sk_c8),sk_c6)**. % 0.36/0.53 587[7:Spt:24.1] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.36/0.53 588[7:SpR:587.0,40.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c8,u))**. % 0.36/0.53 592[6:SpR:586.0,99.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c8)**. % 0.36/0.53 594[6:Rew:39.0,592.0] || -> equal(identity,sk_c8)**. % 0.36/0.53 595[6:Rew:594.0,38.0] || -> equal(multiply(sk_c8,u),u)**. % 0.36/0.53 596[6:Rew:594.0,316.0] || -> equal(multiply(u,sk_c8),u)**. % 0.36/0.53 597[6:Rew:594.0,39.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.36/0.53 599[6:Rew:595.0,566.0] || -> equal(multiply(sk_c7,u),u)**. % 0.36/0.53 603[7:Rew:595.0,588.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.36/0.53 606[6:Rew:596.0,580.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.36/0.53 608[6:Rew:596.0,564.6] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8)** equal(inverse(x),sk_c9) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c7),sk_c9)** equal(w,sk_c7) equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 613[7:Rew:599.0,603.0] || -> equal(multiply(sk_c6,u),u)**. % 0.36/0.53 614[7:Rew:613.0,587.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.53 617[7:Rew:614.0,561.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.36/0.53 625[7:Rew:614.0,608.6,596.0,608.5,614.0,608.5,596.0,608.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9)** equal(inverse(w),sk_c8)** equal(inverse(x),sk_c9) equal(u,sk_c9) equal(v,sk_c9) equal(w,sk_c8) equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 626[7:Con:625.1] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c9) equal(u,sk_c9) equal(v,sk_c8) equal(multiply(w,sk_c9),sk_c8)**+ -> . % 0.36/0.53 640[6:SpR:597.0,99.0] || -> equal(multiply(inverse(inverse(u)),sk_c8),u)**. % 0.36/0.53 643[6:Rew:596.0,640.0] || -> equal(inverse(inverse(u)),u)**. % 0.36/0.53 664[6:SpR:596.0,597.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.36/0.53 668[7:SpL:578.0,626.5] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c8)** equal(inverse(sk_c9),sk_c9)** equal(u,sk_c9) equal(v,sk_c8) equal(sk_c8,sk_c8) -> . % 0.36/0.53 674[7:Obv:668.5] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c8)** equal(inverse(sk_c9),sk_c9)** equal(u,sk_c9) equal(v,sk_c8) -> . % 0.36/0.53 675[7:Rew:606.0,674.2] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c8)** equal(sk_c9,sk_c9) equal(u,sk_c9) equal(v,sk_c8) -> . % 0.36/0.53 676[7:Obv:675.2] || equal(inverse(u),sk_c9)**+ equal(inverse(v),sk_c8)** equal(u,sk_c9) equal(v,sk_c8) -> . % 0.36/0.53 679[6:SpR:643.0,597.0] || -> equal(multiply(u,inverse(u)),sk_c8)**. % 0.36/0.53 688[6:SpR:679.0,595.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.36/0.53 991[7:SpL:606.0,676.0] || equal(sk_c9,sk_c9) equal(inverse(u),sk_c8)** equal(sk_c9,sk_c9) equal(u,sk_c8) -> . % 0.36/0.53 995[7:Obv:991.2] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.36/0.53 998[7:SpL:617.0,995.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.36/0.53 1002[7:Obv:998.1] || -> . % 0.36/0.53 1003[7:Spt:1002.0,24.1,587.0] || equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.36/0.53 1004[7:Spt:1002.0,24.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 1005[6:Rew:561.0,664.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.53 1013[7:Rew:1005.0,1003.0] || equal(multiply(sk_c6,sk_c8),sk_c8)** -> . % 0.36/0.53 1014[7:Rew:596.0,1013.0] || equal(sk_c6,sk_c8)** -> . % 0.36/0.53 1035[6:Rew:1005.0,12.1] || -> equal(inverse(sk_c1),sk_c9) equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.36/0.53 1036[6:Rew:596.0,1035.1] || -> equal(inverse(sk_c1),sk_c9)** equal(sk_c6,sk_c8). % 0.36/0.53 1037[7:MRR:1036.1,1014.0] || -> equal(inverse(sk_c1),sk_c9)**. % 0.36/0.53 1065[6:Rew:596.0,608.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(inverse(w),sk_c8)** equal(inverse(x),sk_c9) equal(u,sk_c9) equal(multiply(v,sk_c7),sk_c9)** equal(w,sk_c7) equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 1066[6:Rew:1005.0,1065.6,1005.0,1065.5] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(inverse(w),sk_c8)** equal(inverse(x),sk_c9) equal(u,sk_c9) equal(multiply(v,sk_c8),sk_c9)** equal(w,sk_c8) equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 1067[6:Rew:596.0,1066.5] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9)** equal(inverse(w),sk_c8)** equal(inverse(x),sk_c9) equal(u,sk_c9) equal(v,sk_c9) equal(w,sk_c8) equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 1068[6:Con:1067.1] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c9) equal(u,sk_c9) equal(v,sk_c8) equal(multiply(w,sk_c9),sk_c8)** -> . % 0.36/0.53 1104[7:SpR:1037.0,597.0] || -> equal(multiply(sk_c9,sk_c1),sk_c8)**. % 0.36/0.53 1105[7:SpR:1037.0,643.0] || -> equal(inverse(sk_c9),sk_c1)**. % 0.36/0.53 1114[7:Rew:606.0,1105.0] || -> equal(sk_c9,sk_c1)**. % 0.36/0.53 1117[7:Rew:1114.0,606.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.36/0.53 1127[7:Rew:1114.0,1068.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c9) equal(u,sk_c9) equal(v,sk_c8) equal(multiply(w,sk_c9),sk_c8)** -> . % 0.36/0.53 1130[7:Rew:1114.0,1104.0] || -> equal(multiply(sk_c1,sk_c1),sk_c8)**. % 0.36/0.53 1139[7:Rew:1114.0,1127.5,1114.0,1127.3,1114.0,1127.2] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c1) equal(u,sk_c1) equal(v,sk_c8) equal(multiply(w,sk_c1),sk_c8)**+ -> . % 0.36/0.53 1240[7:SpL:1130.0,1139.5] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c1) equal(v,sk_c8) equal(sk_c8,sk_c8) -> . % 0.36/0.53 1241[7:Obv:1240.5] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.53 1242[7:Rew:1117.0,1241.2] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(sk_c1,sk_c1) equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.53 1243[7:Obv:1242.2] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c8)** equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.53 1343[7:SpL:1117.0,1243.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c8)** equal(sk_c1,sk_c1) equal(u,sk_c8) -> . % 0.36/0.53 1345[7:Obv:1343.2] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.36/0.53 1472[7:SpL:688.0,1345.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.36/0.53 1475[7:Obv:1472.1] || -> . % 0.36/0.53 1477[6:Spt:1475.0,28.1,582.0] || equal(multiply(sk_c5,sk_c6),sk_c8)** -> . % 0.36/0.53 1478[6:Spt:1475.0,28.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 1480[6:MRR:10.1,1477.0] || -> equal(inverse(sk_c1),sk_c9)**. % 0.36/0.53 1484[6:MRR:4.0,1477.0] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.53 1530[6:SpR:1484.0,99.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c9)**. % 0.36/0.53 1532[6:Rew:1480.0,1530.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.36/0.53 1542[6:SpR:1532.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c9),sk_c8)**. % 0.36/0.53 1544[6:Rew:39.0,1542.0] || -> equal(identity,sk_c8)**. % 0.36/0.53 1545[6:Rew:1544.0,316.0] || -> equal(multiply(u,sk_c8),u)**. % 0.36/0.53 1548[6:Rew:1544.0,39.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.36/0.53 1583[6:SpR:1545.0,572.0] || -> equal(multiply(sk_c6,sk_c5),sk_c8)**. % 0.36/0.53 1592[6:SpR:1583.0,99.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c5)**. % 0.36/0.53 1594[6:Rew:1545.0,1592.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.36/0.53 1607[6:SpR:1594.0,1548.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.36/0.53 1608[6:MRR:1607.0,1477.0] || -> . % 0.36/0.53 1612[5:Spt:1608.0,27.1,574.0] || equal(multiply(sk_c4,sk_c8),sk_c9)** -> . % 0.36/0.53 1613[5:Spt:1608.0,27.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 1614[5:MRR:21.1,1612.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 1615[5:MRR:9.1,1612.0] || -> equal(inverse(sk_c1),sk_c9)**. % 0.36/0.53 1616[5:MRR:33.0,1612.0] || -> equal(multiply(sk_c3,sk_c7),sk_c9)**. % 0.36/0.53 1617[5:MRR:15.0,1612.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 1618[5:MRR:3.0,1612.0] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.53 1634[5:SpR:1617.0,99.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c8)**. % 0.36/0.53 1636[5:Rew:1614.0,1634.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.36/0.53 1638[5:SpR:1618.0,99.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c9)**. % 0.36/0.53 1640[5:Rew:1615.0,1638.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.36/0.53 1649[5:SpR:1640.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c9),sk_c8)**. % 0.36/0.53 1651[5:Rew:39.0,1649.0] || -> equal(identity,sk_c8)**. % 0.36/0.53 1652[5:Rew:1651.0,38.0] || -> equal(multiply(sk_c8,u),u)**. % 0.36/0.53 1653[5:Rew:1651.0,316.0] || -> equal(multiply(u,sk_c8),u)**. % 0.36/0.53 1654[5:Rew:1651.0,39.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.36/0.53 1656[5:Rew:1652.0,1636.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.53 1663[5:Rew:1656.0,1616.0] || -> equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.36/0.53 1672[5:Rew:1653.0,1612.0] || equal(sk_c4,sk_c9)** -> . % 0.36/0.53 1674[5:Rew:1653.0,1663.0] || -> equal(sk_c3,sk_c9)**. % 0.36/0.53 1675[5:Rew:1674.0,1613.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.36/0.53 1725[5:SpR:568.0,1654.0] || -> equal(multiply(sk_c9,sk_c4),sk_c8)**. % 0.36/0.53 1740[5:SpR:1725.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c4)**. % 0.36/0.53 1742[5:Rew:1653.0,1740.0,1675.0,1740.0] || -> equal(sk_c4,sk_c9)**. % 0.36/0.53 1743[5:MRR:1742.0,1672.0] || -> . % 0.36/0.53 1745[4:Spt:1743.0,29.0,571.0] || equal(inverse(sk_c5),sk_c6)** -> . % 0.36/0.53 1746[4:Spt:1743.0,29.1] || -> equal(inverse(sk_c3),sk_c9)**. % 0.36/0.53 1747[4:MRR:23.0,1745.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.53 1748[4:MRR:11.0,1745.0] || -> equal(inverse(sk_c1),sk_c9)**. % 0.36/0.53 1749[4:MRR:35.0,1745.0] || -> equal(multiply(sk_c3,sk_c7),sk_c9)**. % 0.36/0.53 1750[4:MRR:17.0,1745.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.53 1751[4:MRR:5.0,1745.0] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.53 1765[4:SpR:1750.0,99.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c8)**. % 0.36/0.53 1767[4:Rew:1747.0,1765.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.36/0.53 1769[4:SpR:1751.0,99.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c9)**. % 0.36/0.53 1771[4:Rew:1748.0,1769.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.36/0.53 1780[4:SpR:1771.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c9),sk_c8)**. % 0.36/0.53 1782[4:Rew:39.0,1780.0] || -> equal(identity,sk_c8)**. % 0.36/0.53 1783[4:Rew:1782.0,316.0] || -> equal(multiply(u,sk_c8),u)**. % 0.36/0.53 1784[4:Rew:1782.0,38.0] || -> equal(multiply(sk_c8,u),u)**. % 0.36/0.53 1786[4:Rew:1782.0,39.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.36/0.53 1789[4:Rew:1783.0,564.6] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8)** equal(inverse(x),sk_c9) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c7),sk_c9)** equal(w,sk_c7) equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 1793[4:Rew:1784.0,1767.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.53 1797[4:Rew:1793.0,561.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.36/0.53 1798[4:Rew:1793.0,1749.0] || -> equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.36/0.53 1806[4:Rew:1783.0,1798.0] || -> equal(sk_c3,sk_c9)**. % 0.36/0.53 1807[4:Rew:1806.0,1746.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.36/0.53 1817[4:Rew:1793.0,1789.6,1783.0,1789.5,1793.0,1789.5,1783.0,1789.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9)** equal(inverse(w),sk_c8)** equal(inverse(x),sk_c9) equal(u,sk_c9) equal(v,sk_c9) equal(w,sk_c8) equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.53 1818[4:Con:1817.1] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c9) equal(u,sk_c9) equal(v,sk_c8) equal(multiply(w,sk_c9),sk_c8)** -> . % 0.36/0.53 1851[4:SpR:1748.0,1786.0] || -> equal(multiply(sk_c9,sk_c1),sk_c8)**. % 0.36/0.53 1867[4:SpR:1851.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c1)**. % 0.36/0.53 1869[4:Rew:1783.0,1867.0,1807.0,1867.0] || -> equal(sk_c9,sk_c1)**. % 0.36/0.53 1870[4:Rew:1869.0,1748.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.36/0.53 1871[4:Rew:1869.0,1751.0] || -> equal(multiply(sk_c1,sk_c1),sk_c8)**. % 0.36/0.53 1879[4:Rew:1869.0,1818.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c9) equal(u,sk_c9) equal(v,sk_c8) equal(multiply(w,sk_c9),sk_c8)** -> . % 0.36/0.53 1883[4:Rew:1869.0,1879.5,1869.0,1879.3,1869.0,1879.2] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c1) equal(u,sk_c1) equal(v,sk_c8) equal(multiply(w,sk_c1),sk_c8)**+ -> . % 0.36/0.53 1943[4:SpL:1871.0,1883.5] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c1) equal(v,sk_c8) equal(sk_c8,sk_c8) -> . % 0.36/0.53 1944[4:Obv:1943.5] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.53 1945[4:Rew:1870.0,1944.2] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(sk_c1,sk_c1) equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.53 1946[4:Obv:1945.2] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c8)** equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.53 2275[4:SpL:1870.0,1946.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c8)** equal(sk_c1,sk_c1) equal(u,sk_c8) -> . % 0.36/0.53 2279[4:Obv:2275.2] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.36/0.53 2280[4:SpL:1797.0,2279.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.36/0.54 2284[4:Obv:2280.1] || -> . % 0.36/0.54 2286[3:Spt:2284.0,26.0,568.0] || equal(inverse(sk_c4),sk_c9)** -> . % 0.36/0.54 2287[3:Spt:2284.0,26.1] || -> equal(inverse(sk_c3),sk_c9)**. % 0.36/0.54 2288[3:MRR:20.0,2286.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.54 2289[3:MRR:8.0,2286.0] || -> equal(inverse(sk_c1),sk_c9)**. % 0.36/0.54 2291[3:MRR:32.0,2286.0] || -> equal(multiply(sk_c3,sk_c7),sk_c9)**. % 0.36/0.54 2292[3:MRR:14.0,2286.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.54 2293[3:MRR:2.0,2286.0] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.54 2315[3:SpR:2292.0,99.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c8)**. % 0.36/0.54 2317[3:Rew:2288.0,2315.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.36/0.54 2319[3:SpR:2293.0,99.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c9)**. % 0.36/0.54 2321[3:Rew:2289.0,2319.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.36/0.54 2333[3:SpR:2321.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c9),sk_c8)**. % 0.36/0.54 2335[3:Rew:39.0,2333.0] || -> equal(identity,sk_c8)**. % 0.36/0.54 2336[3:Rew:2335.0,38.0] || -> equal(multiply(sk_c8,u),u)**. % 0.36/0.54 2337[3:Rew:2335.0,316.0] || -> equal(multiply(u,sk_c8),u)**. % 0.36/0.54 2338[3:Rew:2335.0,39.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.36/0.54 2340[3:Rew:2336.0,2317.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.54 2346[3:Rew:2340.0,561.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.36/0.54 2347[3:Rew:2340.0,2291.0] || -> equal(multiply(sk_c3,sk_c8),sk_c9)**. % 0.36/0.54 2350[3:Rew:2340.0,564.5] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c9) equal(inverse(w),sk_c8) equal(inverse(x),sk_c9) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c8),sk_c9)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(x,sk_c9),sk_c8)** -> . % 0.36/0.54 2357[3:Rew:2337.0,2347.0] || -> equal(sk_c3,sk_c9)**. % 0.36/0.54 2358[3:Rew:2357.0,2287.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.36/0.54 2367[3:Con:2350.1] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c8) equal(inverse(w),sk_c9) equal(multiply(u,sk_c8),sk_c9)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c9),sk_c8)** -> . % 0.36/0.54 2368[3:Rew:2337.0,2367.4,2340.0,2367.4,2337.0,2367.3] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c9) equal(u,sk_c9) equal(v,sk_c8) equal(multiply(w,sk_c9),sk_c8)** -> . % 0.36/0.54 2392[3:SpR:2289.0,2338.0] || -> equal(multiply(sk_c9,sk_c1),sk_c8)**. % 0.36/0.54 2402[3:SpR:2392.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c1)**. % 0.36/0.54 2404[3:Rew:2358.0,2402.0] || -> equal(multiply(sk_c9,sk_c8),sk_c1)**. % 0.36/0.54 2405[3:Rew:2337.0,2404.0] || -> equal(sk_c9,sk_c1)**. % 0.36/0.54 2406[3:Rew:2405.0,2289.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.36/0.54 2408[3:Rew:2405.0,2293.0] || -> equal(multiply(sk_c1,sk_c1),sk_c8)**. % 0.36/0.54 2416[3:Rew:2405.0,2368.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c9) equal(u,sk_c9) equal(v,sk_c8) equal(multiply(w,sk_c9),sk_c8)** -> . % 0.36/0.54 2419[3:Rew:2405.0,2416.5,2405.0,2416.3,2405.0,2416.2] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c1) equal(u,sk_c1) equal(v,sk_c8) equal(multiply(w,sk_c1),sk_c8)**+ -> . % 0.36/0.54 2449[3:SpL:2408.0,2419.5] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c1) equal(v,sk_c8) equal(sk_c8,sk_c8) -> . % 0.36/0.54 2450[3:Obv:2449.5] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.54 2451[3:Rew:2406.0,2450.2] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c8)** equal(sk_c1,sk_c1) equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.54 2452[3:Obv:2451.2] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c8)** equal(u,sk_c1) equal(v,sk_c8) -> . % 0.36/0.54 2458[0:SpR:273.0,99.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.36/0.54 2669[3:SpL:2406.0,2452.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c8)** equal(sk_c1,sk_c1) equal(u,sk_c8) -> . % 0.36/0.54 2672[3:Obv:2669.2] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.36/0.54 2673[3:SpL:2346.0,2672.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.36/0.54 2676[3:Obv:2673.1] || -> . % 0.36/0.54 2678[2:Spt:2676.0,19.0,561.0] || equal(inverse(sk_c8),sk_c7)** -> . % 0.36/0.54 2679[2:Spt:2676.0,19.1] || -> equal(inverse(sk_c2),sk_c8)**. % 0.36/0.54 2680[2:MRR:7.0,2678.0] || -> equal(inverse(sk_c1),sk_c9)**. % 0.36/0.54 2684[2:MRR:13.0,2678.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.36/0.54 2685[2:MRR:1.0,2678.0] || -> equal(multiply(sk_c1,sk_c9),sk_c8)**. % 0.36/0.54 2696[2:SpR:2680.0,2458.0] || -> equal(multiply(sk_c1,multiply(sk_c9,u)),u)**. % 0.36/0.54 2706[2:SpR:2684.0,99.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c8)**. % 0.36/0.54 2708[2:Rew:2679.0,2706.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.36/0.54 2714[2:SpR:2685.0,40.0] || -> equal(multiply(sk_c1,multiply(sk_c9,u)),multiply(sk_c8,u))**. % 0.36/0.54 2715[2:SpR:2685.0,99.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c9)**. % 0.36/0.54 2717[2:Rew:2680.0,2715.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.36/0.54 2718[2:Rew:2696.0,2714.0] || -> equal(multiply(sk_c8,u),u)**. % 0.36/0.54 2719[2:Rew:2718.0,2708.0] || -> equal(sk_c7,sk_c8)**. % 0.36/0.54 2722[2:Rew:2719.0,2678.0] || equal(inverse(sk_c8),sk_c8)** -> . % 0.36/0.54 2729[2:SpR:2717.0,99.0] || -> equal(multiply(inverse(sk_c9),sk_c9),sk_c8)**. % 0.36/0.54 2731[2:Rew:39.0,2729.0] || -> equal(identity,sk_c8)**. % 0.36/0.54 2735[2:Rew:2731.0,39.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.36/0.54 2754[2:SpR:2679.0,2735.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.36/0.54 2758[2:Rew:2718.0,2754.0] || -> equal(sk_c2,sk_c8)**. % 0.36/0.54 2759[2:Rew:2758.0,2679.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.36/0.54 2761[2:MRR:2759.0,2722.0] || -> . % 0.36/0.54 % SZS output end Refutation % 0.36/0.54 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 prove_this_5 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 prove_this_32 prove_this_33 prove_this_35 prove_this_37 left_identity left_inverse associativity % 0.36/0.54 %------------------------------------------------------------------------------