%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP349-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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:58 EDT 2022 % Result : Unsatisfiable 0.19s 0.52s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : GRP349-1 : TPTP v8.1.0. Released v2.5.0. % 0.12/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n006.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jun 13 15:10:11 EDT 2022 % 0.12/0.33 % CPUTime : % 0.19/0.52 % 0.19/0.52 SPASS V 3.9 % 0.19/0.52 SPASS beiseite: Proof found. % 0.19/0.52 % SZS status Theorem % 0.19/0.52 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.52 SPASS derived 1615 clauses, backtracked 689 clauses, performed 16 splits and kept 1175 clauses. % 0.19/0.52 SPASS allocated 63999 KBytes. % 0.19/0.52 SPASS spent 0:00:00.18 on the problem. % 0.19/0.52 0:00:00.03 for the input. % 0.19/0.52 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.52 0:00:00.01 for inferences. % 0.19/0.52 0:00:00.00 for the backtracking. % 0.19/0.52 0:00:00.10 for the reduction. % 0.19/0.52 % 0.19/0.52 % 0.19/0.52 Here is a proof with depth 5, length 353 : % 0.19/0.52 % SZS output start Refutation % 0.19/0.52 3[0:Inp] || -> equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c10),sk_c8). % 0.19/0.52 4[0:Inp] || -> equal(inverse(sk_c5),sk_c10) equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.52 5[0:Inp] || -> equal(multiply(sk_c5,sk_c9),sk_c10)** equal(multiply(sk_c9,sk_c10),sk_c8). % 0.19/0.52 10[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.19/0.52 11[0:Inp] || -> equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.19/0.52 12[0:Inp] || -> equal(inverse(sk_c5),sk_c10) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.19/0.52 13[0:Inp] || -> equal(multiply(sk_c5,sk_c9),sk_c10)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.19/0.52 17[0:Inp] || -> equal(inverse(sk_c10),sk_c8) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.52 18[0:Inp] || -> equal(inverse(sk_c4),sk_c10)** equal(inverse(sk_c10),sk_c8). % 0.19/0.52 19[0:Inp] || -> equal(inverse(sk_c10),sk_c8) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 20[0:Inp] || -> equal(inverse(sk_c5),sk_c10)** equal(inverse(sk_c10),sk_c8). % 0.19/0.52 21[0:Inp] || -> equal(inverse(sk_c10),sk_c8) equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 22[0:Inp] || -> equal(inverse(sk_c10),sk_c8) equal(multiply(sk_c6,sk_c7),sk_c9)**. % 0.19/0.52 23[0:Inp] || -> equal(inverse(sk_c6),sk_c7)** equal(inverse(sk_c10),sk_c8). % 0.19/0.52 24[0:Inp] || -> equal(inverse(sk_c10),sk_c8) equal(multiply(sk_c7,sk_c8),sk_c9)**. % 0.19/0.52 27[0:Inp] || -> equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c1,sk_c2),sk_c9)**. % 0.19/0.52 28[0:Inp] || -> equal(inverse(sk_c5),sk_c10) equal(multiply(sk_c1,sk_c2),sk_c9)**. % 0.19/0.52 29[0:Inp] || -> equal(multiply(sk_c5,sk_c9),sk_c10) equal(multiply(sk_c1,sk_c2),sk_c9)**. % 0.19/0.52 35[0:Inp] || -> equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 36[0:Inp] || -> equal(inverse(sk_c5),sk_c10) equal(inverse(sk_c1),sk_c2)**. % 0.19/0.52 37[0:Inp] || -> equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 43[0:Inp] || -> equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.19/0.52 44[0:Inp] || -> equal(inverse(sk_c5),sk_c10) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.19/0.52 45[0:Inp] || -> equal(multiply(sk_c5,sk_c9),sk_c10) equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.19/0.52 49[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.52 50[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(inverse(sk_c3),sk_c8)**. % 0.19/0.52 51[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 52[0:Inp] || -> equal(inverse(sk_c5),sk_c10) equal(inverse(sk_c3),sk_c8)**. % 0.19/0.52 53[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 57[0:Inp] || -> equal(multiply(sk_c4,sk_c10),sk_c9) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.52 58[0:Inp] || -> equal(inverse(sk_c4),sk_c10) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.52 59[0:Inp] || -> equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.52 60[0:Inp] || -> equal(inverse(sk_c5),sk_c10) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.52 61[0:Inp] || -> equal(multiply(sk_c5,sk_c9),sk_c10) equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.52 65[0:Inp] || equal(multiply(sk_c9,sk_c10),sk_c8) equal(multiply(sk_c9,sk_c8),sk_c10) equal(inverse(sk_c10),sk_c8) equal(multiply(u,v),sk_c9)** equal(inverse(u),v) equal(multiply(v,sk_c8),sk_c9)** equal(inverse(w),sk_c8) equal(multiply(w,sk_c9),sk_c8)** equal(multiply(x,sk_c10),sk_c9)** equal(inverse(x),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)** equal(inverse(y),sk_c10) equal(multiply(y,sk_c9),sk_c10)** equal(multiply(z,x1),sk_c9)** equal(inverse(z),x1) equal(multiply(x1,sk_c8),sk_c9)** -> . % 0.19/0.52 66[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.52 67[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.52 68[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.52 69[0:Con:65.3] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c8) equal(inverse(sk_c10),sk_c8) equal(multiply(u,sk_c9),sk_c10)**+ equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c8)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) equal(multiply(sk_c9,sk_c10),sk_c8) -> . % 0.19/0.52 70[1:Spt:69.2,69.6] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c9),sk_c8)** -> . % 0.19/0.52 71[2:Spt:19.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.52 73[3:Spt:11.1] || -> equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.19/0.52 79[4:Spt:51.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.52 85[5:Spt:59.1] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.52 87[5:SpL:85.0,70.1] || equal(inverse(sk_c3),sk_c8)** equal(sk_c8,sk_c8) -> . % 0.19/0.52 88[5:Obv:87.1] || equal(inverse(sk_c3),sk_c8)** -> . % 0.19/0.52 89[5:Rew:79.0,88.0] || equal(sk_c8,sk_c8)* -> . % 0.19/0.52 90[5:Obv:89.0] || -> . % 0.19/0.52 91[5:Spt:90.0,59.1,85.0] || equal(multiply(sk_c3,sk_c9),sk_c8)** -> . % 0.19/0.52 92[5:Spt:90.0,59.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 94[5:MRR:60.1,91.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.52 95[5:MRR:58.1,91.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.52 98[5:MRR:61.1,91.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 99[5:MRR:57.1,91.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.52 107[5:SpL:98.0,70.1] || equal(inverse(sk_c5),sk_c8)** equal(sk_c8,sk_c10) -> . % 0.19/0.52 108[5:Rew:94.0,107.0] || equal(sk_c8,sk_c10)** equal(sk_c8,sk_c10)** -> . % 0.19/0.52 109[5:Obv:108.0] || equal(sk_c8,sk_c10)** -> . % 0.19/0.52 112[2:SpR:71.0,67.0] || -> equal(multiply(sk_c8,sk_c10),identity)**. % 0.19/0.52 116[5:SpR:94.0,67.0] || -> equal(multiply(sk_c10,sk_c5),identity)**. % 0.19/0.52 117[5:SpR:95.0,67.0] || -> equal(multiply(sk_c10,sk_c4),identity)**. % 0.19/0.52 129[0:SpR:67.0,68.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.52 134[2:SpR:112.0,68.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),multiply(identity,u))**. % 0.19/0.52 138[2:Rew:66.0,134.0] || -> equal(multiply(sk_c8,multiply(sk_c10,u)),u)**. % 0.19/0.52 141[0:Rew:66.0,129.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.52 155[5:SpR:116.0,138.0] || -> equal(multiply(sk_c8,identity),sk_c5)**. % 0.19/0.52 156[5:SpR:117.0,138.0] || -> equal(multiply(sk_c8,identity),sk_c4)**. % 0.19/0.52 157[5:Rew:155.0,156.0] || -> equal(sk_c5,sk_c4)**. % 0.19/0.52 163[5:Rew:157.0,155.0] || -> equal(multiply(sk_c8,identity),sk_c4)**. % 0.19/0.52 174[5:SpR:163.0,68.0] || -> equal(multiply(sk_c8,multiply(identity,u)),multiply(sk_c4,u))**. % 0.19/0.52 175[5:Rew:66.0,174.0] || -> equal(multiply(sk_c4,u),multiply(sk_c8,u))**. % 0.19/0.52 176[5:Rew:175.0,99.0] || -> equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.52 181[5:Rew:112.0,176.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 182[5:Rew:181.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.52 195[5:Rew:182.0,73.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 204[5:MRR:195.0,109.0] || -> . % 0.19/0.52 221[4:Spt:204.0,51.0,79.0] || equal(inverse(sk_c3),sk_c8)** -> . % 0.19/0.52 222[4:Spt:204.0,51.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 224[4:MRR:52.1,221.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.52 225[4:MRR:50.1,221.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.52 228[4:MRR:53.0,221.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 229[4:MRR:49.0,221.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.52 251[4:SpL:228.0,70.1] || equal(inverse(sk_c5),sk_c8)** equal(sk_c8,sk_c10) -> . % 0.19/0.52 252[4:Rew:224.0,251.0] || equal(sk_c8,sk_c10)** equal(sk_c8,sk_c10)** -> . % 0.19/0.52 253[4:Obv:252.0] || equal(sk_c8,sk_c10)** -> . % 0.19/0.52 264[4:SpR:224.0,67.0] || -> equal(multiply(sk_c10,sk_c5),identity)**. % 0.19/0.52 265[4:SpR:225.0,67.0] || -> equal(multiply(sk_c10,sk_c4),identity)**. % 0.19/0.52 283[4:SpR:264.0,138.0] || -> equal(multiply(sk_c8,identity),sk_c5)**. % 0.19/0.52 284[4:SpR:265.0,138.0] || -> equal(multiply(sk_c8,identity),sk_c4)**. % 0.19/0.52 285[4:Rew:283.0,284.0] || -> equal(sk_c5,sk_c4)**. % 0.19/0.52 291[4:Rew:285.0,283.0] || -> equal(multiply(sk_c8,identity),sk_c4)**. % 0.19/0.52 301[4:SpR:291.0,68.0] || -> equal(multiply(sk_c8,multiply(identity,u)),multiply(sk_c4,u))**. % 0.19/0.52 303[4:Rew:66.0,301.0] || -> equal(multiply(sk_c4,u),multiply(sk_c8,u))**. % 0.19/0.52 304[4:Rew:303.0,229.0] || -> equal(multiply(sk_c8,sk_c10),sk_c9)**. % 0.19/0.52 309[4:Rew:112.0,304.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 312[4:Rew:309.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.52 322[4:Rew:312.0,73.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 330[4:MRR:322.0,253.0] || -> . % 0.19/0.52 344[3:Spt:330.0,11.1,73.0] || equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.19/0.52 345[3:Spt:330.0,11.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 347[3:MRR:12.1,344.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.52 348[3:MRR:10.1,344.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.52 351[3:MRR:13.1,344.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 367[3:SpL:351.0,70.1] || equal(inverse(sk_c5),sk_c8)** equal(sk_c8,sk_c10) -> . % 0.19/0.52 368[3:Rew:347.0,367.0] || equal(sk_c8,sk_c10)** equal(sk_c8,sk_c10)** -> . % 0.19/0.52 369[3:Obv:368.0] || equal(sk_c8,sk_c10)** -> . % 0.19/0.52 379[3:SpR:347.0,67.0] || -> equal(multiply(sk_c10,sk_c5),identity)**. % 0.19/0.52 380[3:SpR:348.0,67.0] || -> equal(multiply(sk_c10,sk_c4),identity)**. % 0.19/0.52 394[3:SpR:345.0,138.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.19/0.52 395[3:SpR:379.0,138.0] || -> equal(multiply(sk_c8,identity),sk_c5)**. % 0.19/0.52 396[3:SpR:380.0,138.0] || -> equal(multiply(sk_c8,identity),sk_c4)**. % 0.19/0.52 397[3:Rew:395.0,396.0] || -> equal(sk_c5,sk_c4)**. % 0.19/0.52 399[3:Rew:397.0,351.0] || -> equal(multiply(sk_c4,sk_c9),sk_c10)**. % 0.19/0.52 403[3:Rew:397.0,395.0] || -> equal(multiply(sk_c8,identity),sk_c4)**. % 0.19/0.52 413[3:SpR:403.0,68.0] || -> equal(multiply(sk_c8,multiply(identity,u)),multiply(sk_c4,u))**. % 0.19/0.52 415[3:Rew:66.0,413.0] || -> equal(multiply(sk_c4,u),multiply(sk_c8,u))**. % 0.19/0.52 417[3:Rew:415.0,399.0] || -> equal(multiply(sk_c8,sk_c9),sk_c10)**. % 0.19/0.52 430[3:Rew:394.0,417.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 431[3:MRR:430.0,369.0] || -> . % 0.19/0.52 450[2:Spt:431.0,19.0,71.0] || equal(inverse(sk_c10),sk_c8)** -> . % 0.19/0.52 451[2:Spt:431.0,19.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 452[2:MRR:23.1,450.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.19/0.52 453[2:MRR:20.1,450.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.52 454[2:MRR:18.1,450.0] || -> equal(inverse(sk_c4),sk_c10)**. % 0.19/0.52 455[2:MRR:24.0,450.0] || -> equal(multiply(sk_c7,sk_c8),sk_c9)**. % 0.19/0.52 456[2:MRR:22.0,450.0] || -> equal(multiply(sk_c6,sk_c7),sk_c9)**. % 0.19/0.52 457[2:MRR:21.0,450.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 458[2:MRR:17.0,450.0] || -> equal(multiply(sk_c4,sk_c10),sk_c9)**. % 0.19/0.52 469[2:SpR:457.0,68.0] || -> equal(multiply(sk_c5,multiply(sk_c9,u)),multiply(sk_c10,u))**. % 0.19/0.52 470[2:SpL:457.0,70.1] || equal(inverse(sk_c5),sk_c8)** equal(sk_c8,sk_c10) -> . % 0.19/0.52 471[2:Rew:453.0,470.0] || equal(sk_c8,sk_c10)** equal(sk_c8,sk_c10)** -> . % 0.19/0.52 472[2:Obv:471.0] || equal(sk_c8,sk_c10)** -> . % 0.19/0.52 480[2:SpR:452.0,67.0] || -> equal(multiply(sk_c7,sk_c6),identity)**. % 0.19/0.52 481[2:SpR:453.0,67.0] || -> equal(multiply(sk_c10,sk_c5),identity)**. % 0.19/0.52 485[2:SpR:480.0,68.0] || -> equal(multiply(sk_c7,multiply(sk_c6,u)),multiply(identity,u))**. % 0.19/0.52 487[2:Rew:66.0,485.0] || -> equal(multiply(sk_c7,multiply(sk_c6,u)),u)**. % 0.19/0.52 496[2:SpR:456.0,487.0] || -> equal(multiply(sk_c7,sk_c9),sk_c7)**. % 0.19/0.52 506[0:SpR:141.0,141.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.52 510[2:SpR:451.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.52 511[2:SpR:455.0,141.0] || -> equal(multiply(inverse(sk_c7),sk_c9),sk_c8)**. % 0.19/0.52 513[2:SpR:458.0,141.0] || -> equal(multiply(inverse(sk_c4),sk_c9),sk_c10)**. % 0.19/0.52 515[0:SpR:67.0,141.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.52 516[2:SpR:480.0,141.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c6)**. % 0.19/0.52 517[2:SpR:487.0,141.0] || -> equal(multiply(inverse(sk_c7),u),multiply(sk_c6,u))**. % 0.19/0.52 518[2:SpR:496.0,141.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c9)**. % 0.19/0.52 519[2:SpR:481.0,141.0] || -> equal(multiply(inverse(sk_c10),identity),sk_c5)**. % 0.19/0.52 527[2:Rew:454.0,513.0] || -> equal(multiply(sk_c10,sk_c9),sk_c10)**. % 0.19/0.52 528[2:Rew:67.0,518.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 529[2:Rew:528.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.52 537[2:Rew:528.0,516.0] || -> equal(multiply(inverse(sk_c7),sk_c9),sk_c6)**. % 0.19/0.52 541[2:Rew:529.0,469.0] || -> equal(multiply(sk_c5,u),multiply(sk_c10,u))**. % 0.19/0.52 544[2:Rew:510.0,519.0,528.0,519.0] || -> equal(sk_c5,sk_c8)**. % 0.19/0.52 545[2:Rew:544.0,453.0] || -> equal(inverse(sk_c8),sk_c10)**. % 0.19/0.52 554[2:Rew:511.0,537.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.52 555[2:Rew:554.0,452.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.19/0.52 559[2:Rew:545.0,555.0] || -> equal(sk_c7,sk_c10)**. % 0.19/0.52 572[2:Rew:544.0,541.0] || -> equal(multiply(sk_c8,u),multiply(sk_c10,u))**. % 0.19/0.52 581[2:Rew:559.0,517.0,572.0,517.0,554.0,517.0] || -> equal(multiply(inverse(sk_c10),u),multiply(sk_c10,u))**. % 0.19/0.52 582[2:Rew:581.0,510.0] || -> equal(multiply(sk_c10,sk_c9),sk_c8)**. % 0.19/0.52 583[2:Rew:527.0,582.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 584[2:MRR:583.0,472.0] || -> . % 0.19/0.52 590[1:Spt:584.0,69.0,69.1,69.3,69.4,69.5,69.7,69.8,69.9] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(sk_c10),sk_c8) equal(multiply(u,sk_c9),sk_c10)**+ equal(multiply(v,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) equal(multiply(sk_c9,sk_c10),sk_c8) -> . % 0.19/0.52 591[0:Rew:506.0,515.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.52 593[2:Spt:19.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.52 594[2:Rew:593.0,590.2] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(sk_c8,sk_c8) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) equal(multiply(sk_c9,sk_c10),sk_c8) -> . % 0.19/0.52 596[2:Obv:594.2] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) equal(multiply(sk_c9,sk_c10),sk_c8) -> . % 0.19/0.52 600[3:Spt:3.1] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.19/0.52 602[3:Rew:600.0,596.6] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) equal(sk_c8,sk_c8) -> . % 0.19/0.52 603[3:Obv:602.6] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) -> . % 0.19/0.52 608[4:Spt:11.1] || -> equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.19/0.52 610[4:Rew:608.0,603.5] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(sk_c10,sk_c10) -> . % 0.19/0.52 611[4:Obv:610.5] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9)** -> . % 0.19/0.52 616[5:Spt:51.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.52 619[6:Spt:35.0] || -> equal(inverse(sk_c1),sk_c2)**. % 0.19/0.52 622[7:Spt:43.1] || -> equal(multiply(sk_c2,sk_c8),sk_c9)**. % 0.19/0.52 624[7:SpR:622.0,141.0] || -> equal(multiply(inverse(sk_c2),sk_c9),sk_c8)**. % 0.19/0.52 626[8:Spt:59.1] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.19/0.52 628[8:SpR:626.0,141.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c9)**. % 0.19/0.52 630[8:Rew:616.0,628.0] || -> equal(multiply(sk_c8,sk_c8),sk_c9)**. % 0.19/0.52 634[9:Spt:27.1] || -> equal(multiply(sk_c1,sk_c2),sk_c9)**. % 0.19/0.52 636[9:SpR:634.0,141.0] || -> equal(multiply(inverse(sk_c1),sk_c9),sk_c2)**. % 0.19/0.52 638[9:Rew:619.0,636.0] || -> equal(multiply(sk_c2,sk_c9),sk_c2)**. % 0.19/0.52 640[9:SpR:638.0,141.0] || -> equal(multiply(inverse(sk_c2),sk_c2),sk_c9)**. % 0.19/0.52 642[9:Rew:67.0,640.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 643[9:Rew:642.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.52 646[9:Rew:642.0,591.0] || -> equal(multiply(u,sk_c9),u)**. % 0.19/0.52 647[9:Rew:643.0,608.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 655[9:Rew:647.0,593.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.52 659[9:Rew:647.0,630.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.19/0.52 661[9:Rew:647.0,611.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c10),sk_c9)** -> . % 0.19/0.52 679[9:Rew:659.0,661.4,646.0,661.2] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(u,sk_c10) equal(multiply(v,sk_c10),sk_c9)** equal(sk_c9,sk_c9) -> . % 0.19/0.52 680[9:Obv:679.4] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(u,sk_c10) equal(multiply(v,sk_c10),sk_c9)**+ -> . % 0.19/0.52 739[9:SpL:659.0,680.3] || equal(inverse(u),sk_c10)** equal(inverse(sk_c10),sk_c10)** equal(u,sk_c10) equal(sk_c9,sk_c9) -> . % 0.19/0.52 740[9:Obv:739.3] || equal(inverse(u),sk_c10)** equal(inverse(sk_c10),sk_c10)** equal(u,sk_c10) -> . % 0.19/0.52 741[9:Rew:655.0,740.1] || equal(inverse(u),sk_c10)** equal(sk_c10,sk_c10) equal(u,sk_c10) -> . % 0.19/0.52 742[9:Obv:741.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.19/0.52 868[9:SpL:655.0,742.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.19/0.52 871[9:Obv:868.1] || -> . % 0.19/0.52 873[9:Spt:871.0,27.1,634.0] || equal(multiply(sk_c1,sk_c2),sk_c9)** -> . % 0.19/0.52 874[9:Spt:871.0,27.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 876[9:MRR:28.1,873.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.52 881[9:MRR:29.1,873.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 889[9:SpR:874.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.52 891[9:Rew:593.0,889.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.19/0.52 928[9:SpR:881.0,141.0] || -> equal(multiply(inverse(sk_c5),sk_c10),sk_c9)**. % 0.19/0.52 930[9:Rew:876.0,928.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.19/0.52 936[9:SpR:891.0,141.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.19/0.52 938[9:Rew:67.0,936.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 939[9:Rew:938.0,591.0] || -> equal(multiply(u,sk_c9),u)**. % 0.19/0.52 942[9:Rew:938.0,67.0] || -> equal(multiply(inverse(u),u),sk_c9)**. % 0.19/0.52 943[9:Rew:939.0,881.0] || -> equal(sk_c5,sk_c10)**. % 0.19/0.52 944[9:Rew:939.0,626.0] || -> equal(sk_c3,sk_c8)**. % 0.19/0.52 948[9:Rew:939.0,624.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.52 950[9:Rew:943.0,876.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.52 953[9:Rew:944.0,616.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.52 956[9:Rew:593.0,950.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 975[9:Rew:956.0,948.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.19/0.52 977[9:Rew:956.0,953.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.52 1039[9:SpR:619.0,942.0] || -> equal(multiply(sk_c2,sk_c1),sk_c9)**. % 0.19/0.52 1072[9:SpR:1039.0,141.0] || -> equal(multiply(inverse(sk_c2),sk_c9),sk_c1)**. % 0.19/0.52 1074[9:Rew:939.0,1072.0,975.0,1072.0] || -> equal(sk_c1,sk_c10)**. % 0.19/0.52 1075[9:Rew:1074.0,619.0] || -> equal(inverse(sk_c10),sk_c2)**. % 0.19/0.52 1076[9:Rew:1074.0,873.0] || equal(multiply(sk_c10,sk_c2),sk_c9)** -> . % 0.19/0.52 1079[9:Rew:977.0,1075.0] || -> equal(sk_c2,sk_c10)**. % 0.19/0.52 1086[9:Rew:1079.0,1076.0] || equal(multiply(sk_c10,sk_c10),sk_c9)** -> . % 0.19/0.52 1087[9:Rew:930.0,1086.0] || equal(sk_c9,sk_c9)* -> . % 0.19/0.52 1088[9:Obv:1087.0] || -> . % 0.19/0.52 1092[8:Spt:1088.0,59.1,626.0] || equal(multiply(sk_c3,sk_c9),sk_c8)** -> . % 0.19/0.52 1093[8:Spt:1088.0,59.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 1106[8:SpR:1093.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.52 1108[8:Rew:593.0,1106.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.19/0.52 1146[8:SpR:1108.0,141.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.19/0.52 1148[8:Rew:67.0,1146.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 1149[8:Rew:1148.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.52 1150[8:Rew:1148.0,591.0] || -> equal(multiply(u,sk_c9),u)**. % 0.19/0.52 1151[8:Rew:1148.0,67.0] || -> equal(multiply(inverse(u),u),sk_c9)**. % 0.19/0.52 1153[8:Rew:1149.0,600.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 1164[8:Rew:1153.0,616.0] || -> equal(inverse(sk_c3),sk_c10)**. % 0.19/0.52 1165[8:Rew:1153.0,593.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.52 1172[8:Rew:1153.0,1092.0] || equal(multiply(sk_c3,sk_c9),sk_c10)** -> . % 0.19/0.52 1182[8:Rew:1150.0,1172.0] || equal(sk_c3,sk_c10)** -> . % 0.19/0.52 1234[8:SpR:1164.0,1151.0] || -> equal(multiply(sk_c10,sk_c3),sk_c9)**. % 0.19/0.52 1301[8:SpR:1234.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c3)**. % 0.19/0.52 1303[8:Rew:1150.0,1301.0,1165.0,1301.0] || -> equal(sk_c3,sk_c10)**. % 0.19/0.52 1304[8:MRR:1303.0,1182.0] || -> . % 0.19/0.52 1306[7:Spt:1304.0,43.1,622.0] || equal(multiply(sk_c2,sk_c8),sk_c9)** -> . % 0.19/0.52 1307[7:Spt:1304.0,43.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 1309[7:MRR:44.1,1306.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.52 1313[7:MRR:45.1,1306.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 1315[7:Rew:1307.0,611.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(sk_c9,sk_c9) -> . % 0.19/0.52 1316[7:Obv:1315.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** -> . % 0.19/0.52 1320[7:SpR:1307.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.52 1322[7:Rew:593.0,1320.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.19/0.52 1349[7:SpR:1313.0,141.0] || -> equal(multiply(inverse(sk_c5),sk_c10),sk_c9)**. % 0.19/0.52 1351[7:Rew:1309.0,1349.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.19/0.52 1360[7:SpR:1322.0,141.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.19/0.52 1362[7:Rew:67.0,1360.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 1363[7:Rew:1362.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.52 1364[7:Rew:1362.0,591.0] || -> equal(multiply(u,sk_c9),u)**. % 0.19/0.52 1367[7:Rew:1363.0,600.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 1377[7:Rew:1367.0,593.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.52 1389[7:Rew:1364.0,1316.2] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(u,sk_c10) equal(multiply(v,sk_c10),sk_c9)**+ -> . % 0.19/0.52 1507[7:SpL:1351.0,1389.3] || equal(inverse(u),sk_c10)** equal(inverse(sk_c10),sk_c10)** equal(u,sk_c10) equal(sk_c9,sk_c9) -> . % 0.19/0.52 1510[7:Obv:1507.3] || equal(inverse(u),sk_c10)** equal(inverse(sk_c10),sk_c10)** equal(u,sk_c10) -> . % 0.19/0.52 1511[7:Rew:1377.0,1510.1] || equal(inverse(u),sk_c10)** equal(sk_c10,sk_c10) equal(u,sk_c10) -> . % 0.19/0.52 1512[7:Obv:1511.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.19/0.52 1595[7:SpL:1377.0,1512.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.19/0.52 1599[7:Obv:1595.1] || -> . % 0.19/0.52 1601[6:Spt:1599.0,35.0,619.0] || equal(inverse(sk_c1),sk_c2)** -> . % 0.19/0.52 1602[6:Spt:1599.0,35.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 1604[6:MRR:36.1,1601.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.52 1608[6:MRR:37.0,1601.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 1610[6:Rew:1602.0,611.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(sk_c9,sk_c9) -> . % 0.19/0.52 1611[6:Obv:1610.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** -> . % 0.19/0.52 1615[6:SpR:1602.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.52 1617[6:Rew:593.0,1615.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.19/0.52 1642[6:SpR:1608.0,141.0] || -> equal(multiply(inverse(sk_c5),sk_c10),sk_c9)**. % 0.19/0.52 1644[6:Rew:1604.0,1642.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.19/0.52 1650[6:SpR:1617.0,141.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.19/0.52 1652[6:Rew:67.0,1650.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 1653[6:Rew:1652.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.52 1654[6:Rew:1652.0,591.0] || -> equal(multiply(u,sk_c9),u)**. % 0.19/0.52 1657[6:Rew:1653.0,600.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.52 1668[6:Rew:1657.0,593.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.52 1678[6:Rew:1654.0,1611.2] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(u,sk_c10) equal(multiply(v,sk_c10),sk_c9)**+ -> . % 0.19/0.52 1779[6:SpL:1644.0,1678.3] || equal(inverse(u),sk_c10)** equal(inverse(sk_c10),sk_c10)** equal(u,sk_c10) equal(sk_c9,sk_c9) -> . % 0.19/0.52 1782[6:Obv:1779.3] || equal(inverse(u),sk_c10)** equal(inverse(sk_c10),sk_c10)** equal(u,sk_c10) -> . % 0.19/0.52 1783[6:Rew:1668.0,1782.1] || equal(inverse(u),sk_c10)** equal(sk_c10,sk_c10) equal(u,sk_c10) -> . % 0.19/0.52 1784[6:Obv:1783.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.19/0.52 1900[6:SpL:1668.0,1784.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.19/0.52 1903[6:Obv:1900.1] || -> . % 0.19/0.52 1905[5:Spt:1903.0,51.0,616.0] || equal(inverse(sk_c3),sk_c8)** -> . % 0.19/0.52 1906[5:Spt:1903.0,51.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.52 1908[5:MRR:52.1,1905.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.52 1913[5:MRR:53.0,1905.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.52 1916[5:Rew:1906.0,611.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(sk_c9,sk_c9) -> . % 0.19/0.52 1917[5:Obv:1916.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** -> . % 0.19/0.52 1921[5:SpR:1906.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.52 1923[5:Rew:593.0,1921.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.19/0.52 1946[5:SpR:1913.0,141.0] || -> equal(multiply(inverse(sk_c5),sk_c10),sk_c9)**. % 0.19/0.52 1948[5:Rew:1908.0,1946.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.19/0.52 1954[5:SpR:1923.0,141.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.19/0.52 1956[5:Rew:67.0,1954.0] || -> equal(identity,sk_c9)**. % 0.19/0.52 1957[5:Rew:1956.0,591.0] || -> equal(multiply(u,sk_c9),u)**. % 0.19/0.52 1961[5:Rew:1957.0,1913.0] || -> equal(sk_c5,sk_c10)**. % 0.19/0.53 1964[5:Rew:1957.0,1917.2] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(u,sk_c10) equal(multiply(v,sk_c10),sk_c9)**+ -> . % 0.19/0.53 1965[5:Rew:1961.0,1908.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.53 1968[5:Rew:593.0,1965.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.53 1970[5:Rew:1968.0,593.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.53 2093[5:SpL:1948.0,1964.3] || equal(inverse(u),sk_c10)** equal(inverse(sk_c10),sk_c10)** equal(u,sk_c10) equal(sk_c9,sk_c9) -> . % 0.19/0.53 2096[5:Obv:2093.3] || equal(inverse(u),sk_c10)** equal(inverse(sk_c10),sk_c10)** equal(u,sk_c10) -> . % 0.19/0.53 2097[5:Rew:1970.0,2096.1] || equal(inverse(u),sk_c10)** equal(sk_c10,sk_c10) equal(u,sk_c10) -> . % 0.19/0.53 2098[5:Obv:2097.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.19/0.53 2120[5:SpL:1970.0,2098.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.19/0.53 2123[5:Obv:2120.1] || -> . % 0.19/0.53 2125[4:Spt:2123.0,11.1,608.0] || equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.19/0.53 2126[4:Spt:2123.0,11.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.53 2135[4:SpR:2126.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.53 2137[4:Rew:593.0,2135.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.19/0.53 2165[4:SpR:2137.0,141.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.19/0.53 2167[4:Rew:67.0,2165.0] || -> equal(identity,sk_c9)**. % 0.19/0.53 2168[4:Rew:2167.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.53 2172[4:Rew:2168.0,600.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.53 2174[4:Rew:2168.0,2125.0] || equal(sk_c8,sk_c10)** -> . % 0.19/0.53 2187[4:Rew:2172.0,2174.0] || equal(sk_c10,sk_c10)* -> . % 0.19/0.53 2188[4:Obv:2187.0] || -> . % 0.19/0.53 2198[3:Spt:2188.0,3.1,600.0] || equal(multiply(sk_c9,sk_c10),sk_c8)** -> . % 0.19/0.53 2199[3:Spt:2188.0,3.0] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.53 2201[3:MRR:4.1,2198.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.19/0.53 2205[3:MRR:5.1,2198.0] || -> equal(multiply(sk_c5,sk_c9),sk_c10)**. % 0.19/0.53 2208[3:SpR:2199.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.53 2210[3:Rew:593.0,2208.0] || -> equal(multiply(sk_c8,sk_c9),sk_c8)**. % 0.19/0.53 2235[3:SpR:2210.0,141.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c9)**. % 0.19/0.53 2237[3:Rew:67.0,2235.0] || -> equal(identity,sk_c9)**. % 0.19/0.53 2238[3:Rew:2237.0,591.0] || -> equal(multiply(u,sk_c9),u)**. % 0.19/0.53 2239[3:Rew:2237.0,66.0] || -> equal(multiply(sk_c9,u),u)**. % 0.19/0.53 2242[3:Rew:2238.0,2205.0] || -> equal(sk_c5,sk_c10)**. % 0.19/0.53 2244[3:Rew:2242.0,2201.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.19/0.53 2247[3:Rew:593.0,2244.0] || -> equal(sk_c8,sk_c10)**. % 0.19/0.53 2251[3:Rew:2247.0,2198.0] || equal(multiply(sk_c9,sk_c10),sk_c10)** -> . % 0.19/0.53 2258[3:Rew:2239.0,2251.0] || equal(sk_c10,sk_c10)* -> . % 0.19/0.53 2259[3:Obv:2258.0] || -> . % 0.19/0.53 2264[2:Spt:2259.0,19.0,593.0] || equal(inverse(sk_c10),sk_c8)** -> . % 0.19/0.53 2265[2:Spt:2259.0,19.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.19/0.53 2266[2:MRR:23.1,2264.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.19/0.53 2270[2:MRR:22.0,2264.0] || -> equal(multiply(sk_c6,sk_c7),sk_c9)**. % 0.19/0.53 2274[2:SpR:2265.0,141.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.19/0.53 2286[2:SpR:2270.0,141.0] || -> equal(multiply(inverse(sk_c6),sk_c9),sk_c7)**. % 0.19/0.53 2288[2:Rew:2266.0,2286.0] || -> equal(multiply(sk_c7,sk_c9),sk_c7)**. % 0.19/0.53 2301[2:SpR:2288.0,141.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c9)**. % 0.19/0.53 2303[2:Rew:67.0,2301.0] || -> equal(identity,sk_c9)**. % 0.19/0.53 2305[2:Rew:2303.0,591.0] || -> equal(multiply(u,sk_c9),u)**. % 0.19/0.53 2315[2:Rew:2305.0,2274.0] || -> equal(inverse(sk_c10),sk_c8)**. % 0.19/0.53 2318[2:MRR:2315.0,2264.0] || -> . % 0.19/0.53 % SZS output end Refutation % 0.19/0.53 Formulae used in the proof : prove_this_3 prove_this_4 prove_this_5 prove_this_10 prove_this_11 prove_this_12 prove_this_13 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_27 prove_this_28 prove_this_29 prove_this_35 prove_this_36 prove_this_37 prove_this_43 prove_this_44 prove_this_45 prove_this_49 prove_this_50 prove_this_51 prove_this_52 prove_this_53 prove_this_57 prove_this_58 prove_this_59 prove_this_60 prove_this_61 prove_this_65 left_identity left_inverse associativity % 0.19/0.53 %------------------------------------------------------------------------------