%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP346-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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:57 EDT 2022 % Result : Unsatisfiable 0.19s 0.47s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP346-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n017.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 : Tue Jun 14 07:53:23 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.47 % 0.19/0.47 SPASS V 3.9 % 0.19/0.47 SPASS beiseite: Proof found. % 0.19/0.47 % SZS status Theorem % 0.19/0.47 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.47 SPASS derived 699 clauses, backtracked 341 clauses, performed 14 splits and kept 592 clauses. % 0.19/0.47 SPASS allocated 63625 KBytes. % 0.19/0.47 SPASS spent 0:00:00.12 on the problem. % 0.19/0.47 0:00:00.03 for the input. % 0.19/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.47 0:00:00.01 for inferences. % 0.19/0.47 0:00:00.00 for the backtracking. % 0.19/0.47 0:00:00.06 for the reduction. % 0.19/0.47 % 0.19/0.47 % 0.19/0.47 Here is a proof with depth 5, length 307 : % 0.19/0.47 % SZS output start Refutation % 0.19/0.47 2[0:Inp] || -> equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5). % 0.19/0.47 3[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.47 4[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5). % 0.19/0.47 5[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.47 6[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c7),sk_c5). % 0.19/0.47 7[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.47 8[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.19/0.47 9[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.47 10[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 11[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.19/0.47 12[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 13[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.19/0.47 14[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 15[0:Inp] || -> equal(multiply(sk_c6,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 16[0:Inp] || -> equal(multiply(sk_c7,sk_c5),sk_c6) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 17[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 18[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 19[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 20[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c5) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 21[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 22[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.19/0.47 23[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.47 24[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 26[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 27[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.19/0.47 28[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 29[0:Inp] || -> equal(multiply(sk_c6,sk_c5),sk_c7) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 30[0:Inp] || -> equal(multiply(sk_c7,sk_c5),sk_c6) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 31[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 32[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 33[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 35[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 36[0:Inp] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(inverse(x),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c7),sk_c5)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c5),sk_c6)** equal(multiply(x,sk_c6),sk_c7)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5) -> . % 0.19/0.47 37[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.47 38[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.47 39[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.47 40[1:Spt:36.3,36.8] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c6),sk_c7)** -> . % 0.19/0.47 45[2:Spt:10.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 51[3:Spt:17.1] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 53[3:SpL:51.0,40.1] || equal(inverse(sk_c1),sk_c7)** equal(sk_c7,sk_c7) -> . % 0.19/0.47 54[3:Obv:53.1] || equal(inverse(sk_c1),sk_c7)** -> . % 0.19/0.47 55[3:Rew:45.0,54.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.47 56[3:Obv:55.0] || -> . % 0.19/0.47 57[3:Spt:56.0,17.1,51.0] || equal(multiply(sk_c1,sk_c6),sk_c7)** -> . % 0.19/0.47 58[3:Spt:56.0,17.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.19/0.47 59[3:MRR:21.1,57.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.47 60[3:MRR:19.1,57.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.19/0.47 61[3:MRR:20.1,57.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.19/0.47 62[3:MRR:18.1,57.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.19/0.47 63[3:MRR:16.1,57.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.47 70[3:SpL:62.0,40.1] || equal(inverse(sk_c3),sk_c7)** equal(sk_c7,sk_c7) -> . % 0.19/0.47 71[3:Obv:70.1] || equal(inverse(sk_c3),sk_c7)** -> . % 0.19/0.47 72[3:Rew:60.0,71.0] || equal(sk_c7,sk_c6)** -> . % 0.19/0.47 77[2:SpR:45.0,38.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.19/0.47 78[3:SpR:58.0,38.0] || -> equal(multiply(sk_c5,sk_c7),identity)**. % 0.19/0.47 79[3:SpR:59.0,38.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.47 80[3:SpR:60.0,38.0] || -> equal(multiply(sk_c6,sk_c3),identity)**. % 0.19/0.47 91[3:SpR:78.0,39.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),multiply(identity,u))**. % 0.19/0.47 96[0:SpR:38.0,39.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.47 101[3:Rew:37.0,91.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.19/0.47 105[0:Rew:37.0,96.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.47 112[3:SpR:63.0,101.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.19/0.47 113[3:SpR:77.0,101.0] || -> equal(multiply(sk_c5,identity),sk_c1)**. % 0.19/0.47 114[3:SpR:79.0,101.0] || -> equal(multiply(sk_c5,identity),sk_c4)**. % 0.19/0.47 115[3:Rew:113.0,114.0] || -> equal(sk_c1,sk_c4)**. % 0.19/0.47 120[3:Rew:115.0,113.0] || -> equal(multiply(sk_c5,identity),sk_c4)**. % 0.19/0.47 126[3:SpR:120.0,39.0] || -> equal(multiply(sk_c5,multiply(identity,u)),multiply(sk_c4,u))**. % 0.19/0.47 128[3:Rew:37.0,126.0] || -> equal(multiply(sk_c4,u),multiply(sk_c5,u))**. % 0.19/0.47 129[3:Rew:128.0,61.0] || -> equal(multiply(sk_c5,sk_c7),sk_c5)**. % 0.19/0.47 133[3:Rew:78.0,129.0] || -> equal(identity,sk_c5)**. % 0.19/0.47 134[3:Rew:133.0,37.0] || -> equal(multiply(sk_c5,u),u)**. % 0.19/0.47 138[3:Rew:133.0,79.0] || -> equal(multiply(sk_c7,sk_c4),sk_c5)**. % 0.19/0.47 139[3:Rew:133.0,80.0] || -> equal(multiply(sk_c6,sk_c3),sk_c5)**. % 0.19/0.47 142[3:Rew:134.0,101.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.47 143[3:Rew:134.0,112.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.47 149[3:Rew:134.0,128.0] || -> equal(multiply(sk_c4,u),u)**. % 0.19/0.47 160[3:Rew:143.0,138.0] || -> equal(multiply(sk_c7,sk_c4),sk_c6)**. % 0.19/0.47 161[3:Rew:143.0,139.0] || -> equal(multiply(sk_c6,sk_c3),sk_c6)**. % 0.19/0.47 163[3:Rew:142.0,160.0] || -> equal(sk_c4,sk_c6)**. % 0.19/0.47 168[3:Rew:163.0,149.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.47 169[3:Rew:168.0,161.0] || -> equal(sk_c3,sk_c6)**. % 0.19/0.47 175[3:Rew:169.0,62.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.19/0.47 189[3:Rew:168.0,175.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 190[3:MRR:189.0,72.0] || -> . % 0.19/0.47 205[2:Spt:190.0,10.1,45.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.19/0.47 206[2:Spt:190.0,10.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.19/0.47 207[2:MRR:14.1,205.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.47 208[2:MRR:12.1,205.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.19/0.47 209[2:MRR:13.0,205.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.19/0.47 210[2:MRR:11.0,205.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.19/0.47 211[2:MRR:9.0,205.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.47 226[2:SpL:210.0,40.1] || equal(inverse(sk_c3),sk_c7)** equal(sk_c7,sk_c7) -> . % 0.19/0.47 227[2:Obv:226.1] || equal(inverse(sk_c3),sk_c7)** -> . % 0.19/0.47 228[2:Rew:208.0,227.0] || equal(sk_c7,sk_c6)** -> . % 0.19/0.47 240[2:SpR:207.0,38.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.47 244[2:SpR:240.0,39.0] || -> equal(multiply(sk_c7,multiply(sk_c4,u)),multiply(identity,u))**. % 0.19/0.47 246[2:Rew:37.0,244.0] || -> equal(multiply(sk_c7,multiply(sk_c4,u)),u)**. % 0.19/0.47 258[2:SpR:209.0,246.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.19/0.47 259[2:Rew:211.0,258.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 260[2:MRR:259.0,228.0] || -> . % 0.19/0.47 262[1:Spt:260.0,36.0,36.1,36.2,36.4,36.5,36.6,36.7,36.9,36.10,36.11] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c7),sk_c5)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5) -> . % 0.19/0.47 264[1:SpL:37.0,262.4] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(inverse(sk_c7),sk_c5) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5) -> . % 0.19/0.47 265[1:SpL:38.0,262.4] || equal(inverse(inverse(sk_c7)),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(inverse(sk_c7),sk_c5) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5) -> . % 0.19/0.47 266[2:Spt:3.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.47 269[2:Rew:266.0,265.9] || equal(inverse(inverse(sk_c7)),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(inverse(sk_c7),sk_c5) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) equal(sk_c5,sk_c5) -> . % 0.19/0.47 270[2:Rew:266.0,264.9] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(inverse(sk_c7),sk_c5) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) equal(sk_c5,sk_c5) -> . % 0.19/0.47 271[2:Obv:270.9] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(inverse(sk_c7),sk_c5) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.19/0.47 272[2:Obv:269.9] || equal(inverse(inverse(sk_c7)),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(inverse(sk_c7),sk_c5) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.19/0.47 277[3:Spt:10.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.19/0.47 280[3:Rew:277.0,272.3] || equal(inverse(inverse(sk_c7)),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c5) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.19/0.47 281[3:Rew:277.0,271.3] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c5) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.19/0.47 282[3:Obv:281.3] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.19/0.47 283[3:Obv:280.3] || equal(inverse(inverse(sk_c7)),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.19/0.47 284[3:Rew:277.0,283.0] || equal(inverse(sk_c5),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.19/0.47 287[3:SpR:277.0,38.0] || -> equal(multiply(sk_c5,sk_c7),identity)**. % 0.19/0.47 289[4:Spt:9.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.47 292[4:Rew:289.0,284.6] || equal(inverse(sk_c5),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(sk_c6,sk_c6) equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.19/0.47 293[4:Rew:289.0,282.6] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(sk_c6,sk_c6) equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.19/0.47 294[4:Obv:292.6] || equal(inverse(sk_c5),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.19/0.47 295[4:Obv:293.6] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.19/0.47 300[5:Spt:8.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.19/0.47 303[5:Rew:300.0,295.6] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(sk_c7,sk_c7) -> . % 0.19/0.47 304[5:Rew:300.0,294.6] || equal(inverse(sk_c5),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** equal(sk_c7,sk_c7) -> . % 0.19/0.47 305[5:Obv:303.6] || equal(inverse(identity),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.19/0.47 306[5:Obv:304.6] || equal(inverse(sk_c5),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.19/0.47 311[6:Spt:14.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.47 312[6:SpR:311.0,38.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.47 314[7:Spt:12.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.19/0.47 315[7:SpR:314.0,38.0] || -> equal(multiply(sk_c6,sk_c3),identity)**. % 0.19/0.47 317[8:Spt:13.1] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.19/0.47 323[3:SpR:287.0,39.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),multiply(identity,u))**. % 0.19/0.47 325[3:Rew:37.0,323.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.19/0.47 334[4:SpR:289.0,325.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.19/0.47 335[6:SpR:312.0,325.0] || -> equal(multiply(sk_c5,identity),sk_c4)**. % 0.19/0.47 338[0:SpR:105.0,105.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.47 342[0:SpR:38.0,105.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.47 343[2:SpR:266.0,105.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.19/0.47 344[8:SpR:317.0,105.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c7)**. % 0.19/0.47 355[8:Rew:289.0,344.0,311.0,344.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 357[8:Rew:355.0,277.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.19/0.47 363[8:Rew:355.0,287.0] || -> equal(multiply(sk_c5,sk_c6),identity)**. % 0.19/0.47 371[8:Rew:355.0,305.0] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.19/0.47 377[8:Rew:334.0,363.0] || -> equal(identity,sk_c5)**. % 0.19/0.47 378[8:Rew:377.0,37.0] || -> equal(multiply(sk_c5,u),u)**. % 0.19/0.47 384[8:Rew:378.0,334.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.47 385[8:Rew:384.0,357.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.19/0.47 389[8:Rew:384.0,377.0] || -> equal(identity,sk_c6)**. % 0.19/0.47 413[8:Rew:389.0,342.0] || -> equal(multiply(inverse(inverse(u)),sk_c6),u)**. % 0.19/0.47 420[8:Rew:338.0,413.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.47 427[8:Rew:420.0,371.5,384.0,371.5,420.0,371.4,355.0,371.4,384.0,371.3,355.0,371.3,385.0,371.0,389.0,371.0] || equal(sk_c6,sk_c6) equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(sk_c6,sk_c6) equal(u,sk_c6) equal(v,sk_c6) -> . % 0.19/0.47 428[8:Obv:427.3] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.19/0.47 429[8:Con:428.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.19/0.47 494[8:SpL:385.0,429.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.19/0.47 496[8:Obv:494.1] || -> . % 0.19/0.47 497[8:Spt:496.0,13.1,317.0] || equal(multiply(sk_c4,sk_c7),sk_c5)** -> . % 0.19/0.47 498[8:Spt:496.0,13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 502[8:MRR:27.1,497.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 503[0:Rew:338.0,342.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.47 504[6:Rew:503.0,335.0] || -> equal(sk_c4,sk_c5)**. % 0.19/0.47 507[6:Rew:504.0,312.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.19/0.47 508[8:Rew:504.0,497.0] || equal(multiply(sk_c5,sk_c7),sk_c5)** -> . % 0.19/0.47 513[6:Rew:289.0,507.0] || -> equal(identity,sk_c6)**. % 0.19/0.47 515[7:Rew:513.0,315.0] || -> equal(multiply(sk_c6,sk_c3),sk_c6)**. % 0.19/0.47 516[6:Rew:513.0,37.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.47 519[6:Rew:513.0,503.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.47 521[7:Rew:516.0,515.0] || -> equal(sk_c3,sk_c6)**. % 0.19/0.47 525[6:Rew:516.0,300.0] || -> equal(sk_c5,sk_c7)**. % 0.19/0.47 531[6:Rew:525.0,277.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.47 532[6:Rew:525.0,289.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.47 541[8:Rew:532.0,508.0,525.0,508.0] || equal(sk_c7,sk_c6)** -> . % 0.19/0.47 550[7:Rew:525.0,32.1,521.0,32.0,519.0,32.0] || -> equal(sk_c7,sk_c6) equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.19/0.47 551[8:MRR:550.0,541.0] || -> equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.19/0.47 556[6:Rew:525.0,306.5,519.0,306.4,513.0,306.3,525.0,306.3,531.0,306.0,525.0,306.0] || equal(sk_c7,sk_c7) equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6) equal(sk_c7,sk_c6) equal(u,sk_c7) equal(multiply(v,sk_c7),sk_c6)** -> . % 0.19/0.47 557[6:Obv:556.0] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6) equal(sk_c7,sk_c6) equal(u,sk_c7) equal(multiply(v,sk_c7),sk_c6)** -> . % 0.19/0.47 565[8:SpR:502.0,105.0] || -> equal(multiply(sk_c6,multiply(sk_c2,u)),u)**. % 0.19/0.47 567[8:Rew:516.0,565.0] || -> equal(multiply(sk_c2,u),u)**. % 0.19/0.47 568[8:Rew:567.0,551.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 569[8:MRR:568.0,541.0] || -> . % 0.19/0.47 570[7:Spt:569.0,12.0,314.0] || equal(inverse(sk_c3),sk_c6)** -> . % 0.19/0.47 571[7:Spt:569.0,12.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 574[7:MRR:26.0,570.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 578[6:Rew:525.0,33.1] || -> equal(inverse(sk_c3),sk_c6) equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.19/0.47 579[7:MRR:578.0,570.0] || -> equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.19/0.47 591[7:SpR:574.0,105.0] || -> equal(multiply(sk_c6,multiply(sk_c2,u)),u)**. % 0.19/0.47 593[7:Rew:516.0,591.0] || -> equal(multiply(sk_c2,u),u)**. % 0.19/0.47 594[7:Rew:593.0,579.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 598[7:Rew:594.0,531.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.19/0.47 604[7:Rew:594.0,557.4] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6) equal(sk_c7,sk_c6) equal(u,sk_c7) equal(multiply(v,sk_c6),sk_c6)** -> . % 0.19/0.47 607[7:Rew:519.0,604.4,594.0,604.3,594.0,604.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(sk_c6,sk_c6) equal(u,sk_c6) equal(v,sk_c6) -> . % 0.19/0.47 608[7:Obv:607.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.19/0.47 609[7:Con:608.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.19/0.47 647[7:SpL:598.0,609.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.19/0.47 648[7:Obv:647.1] || -> . % 0.19/0.47 649[6:Spt:648.0,14.0,311.0] || equal(inverse(sk_c4),sk_c7)** -> . % 0.19/0.47 650[6:Spt:648.0,14.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 651[6:MRR:28.0,649.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 652[6:MRR:21.0,649.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 653[6:MRR:35.0,649.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 680[6:SpR:652.0,105.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.19/0.47 682[6:Rew:650.0,680.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.47 684[6:SpR:653.0,105.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.19/0.47 686[6:Rew:651.0,684.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.19/0.47 688[6:SpR:682.0,105.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.19/0.47 690[6:Rew:334.0,688.0,277.0,688.0] || -> equal(sk_c5,sk_c7)**. % 0.19/0.47 692[6:Rew:690.0,287.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.19/0.47 702[6:Rew:690.0,306.0] || equal(inverse(sk_c7),sk_c7) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(identity,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.19/0.47 711[6:Rew:690.0,686.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.19/0.47 712[6:Rew:682.0,692.0] || -> equal(identity,sk_c6)**. % 0.19/0.47 713[6:Rew:712.0,503.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.47 717[6:Rew:713.0,652.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.47 718[6:Rew:713.0,711.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 719[6:Rew:717.0,650.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.47 724[6:Rew:718.0,690.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.47 729[6:Rew:718.0,719.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.19/0.47 745[6:Rew:713.0,702.5,724.0,702.5,713.0,702.4,718.0,702.4,712.0,702.3,724.0,702.3,729.0,702.0,718.0,702.0] || equal(sk_c6,sk_c6) equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(sk_c6,sk_c6) equal(u,sk_c6) equal(v,sk_c6) -> . % 0.19/0.47 746[6:Obv:745.3] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.19/0.47 747[6:Con:746.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.19/0.47 813[6:SpL:729.0,747.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.19/0.47 815[6:Obv:813.1] || -> . % 0.19/0.47 816[5:Spt:815.0,8.1,300.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.19/0.47 817[5:Spt:815.0,8.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 818[5:MRR:22.1,816.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 819[5:MRR:15.0,816.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 820[5:MRR:29.0,816.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 844[5:SpR:819.0,105.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.19/0.47 846[5:Rew:817.0,844.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.47 848[5:SpR:820.0,105.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.19/0.47 850[5:Rew:818.0,848.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.19/0.47 852[5:SpR:846.0,105.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.19/0.47 854[5:Rew:334.0,852.0,277.0,852.0] || -> equal(sk_c5,sk_c7)**. % 0.19/0.47 859[5:Rew:854.0,287.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.19/0.47 862[5:Rew:854.0,816.0] || equal(multiply(sk_c6,sk_c7),sk_c7)** -> . % 0.19/0.47 869[5:Rew:854.0,850.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.19/0.47 870[5:Rew:846.0,859.0] || -> equal(identity,sk_c6)**. % 0.19/0.47 871[5:Rew:870.0,37.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.47 875[5:Rew:871.0,869.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 889[5:Rew:871.0,862.0,875.0,862.0] || equal(sk_c6,sk_c6)* -> . % 0.19/0.47 890[5:Obv:889.0] || -> . % 0.19/0.47 900[4:Spt:890.0,9.1,289.0] || equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.19/0.47 901[4:Spt:890.0,9.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 902[4:MRR:23.1,900.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 903[4:MRR:16.0,900.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 904[4:MRR:30.0,900.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 912[4:SpR:903.0,105.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.19/0.47 914[4:Rew:901.0,912.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.47 924[4:SpR:904.0,105.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.19/0.47 926[4:Rew:902.0,924.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.19/0.47 928[4:SpR:914.0,105.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.19/0.47 930[4:Rew:277.0,928.0] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.47 935[4:SpR:926.0,105.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.19/0.47 937[4:Rew:343.0,935.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 941[4:Rew:937.0,287.0] || -> equal(multiply(sk_c5,sk_c6),identity)**. % 0.19/0.47 943[4:Rew:937.0,914.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.19/0.47 945[4:Rew:937.0,900.0] || equal(multiply(sk_c6,sk_c5),sk_c6)** -> . % 0.19/0.47 951[4:Rew:937.0,930.0] || -> equal(multiply(sk_c5,sk_c6),sk_c6)**. % 0.19/0.47 953[4:Rew:926.0,943.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.47 958[4:Rew:953.0,941.0] || -> equal(multiply(sk_c6,sk_c6),identity)**. % 0.19/0.47 959[4:Rew:953.0,951.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.19/0.47 960[4:Rew:959.0,958.0] || -> equal(identity,sk_c6)**. % 0.19/0.47 961[4:Rew:960.0,37.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.47 972[4:Rew:961.0,945.0,953.0,945.0] || equal(sk_c6,sk_c6)* -> . % 0.19/0.47 973[4:Obv:972.0] || -> . % 0.19/0.47 982[3:Spt:973.0,10.0,277.0] || equal(inverse(sk_c7),sk_c5)** -> . % 0.19/0.47 983[3:Spt:973.0,10.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 984[3:MRR:24.0,982.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.19/0.47 985[3:MRR:17.0,982.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.47 986[3:MRR:31.0,982.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.19/0.47 995[3:SpR:985.0,105.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.19/0.47 997[3:Rew:983.0,995.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.47 999[3:SpR:986.0,105.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.19/0.47 1001[3:Rew:984.0,999.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.19/0.47 1003[3:SpR:997.0,105.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.19/0.47 1006[3:SpR:1001.0,105.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.19/0.47 1008[3:Rew:343.0,1006.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.47 1011[3:Rew:1008.0,982.0] || equal(inverse(sk_c6),sk_c5)** -> . % 0.19/0.47 1013[3:Rew:1008.0,997.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.19/0.47 1014[3:Rew:1008.0,343.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.19/0.47 1018[3:Rew:1008.0,1003.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c6)**. % 0.19/0.48 1020[3:Rew:1001.0,1013.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.48 1024[3:Rew:1020.0,1011.0] || equal(inverse(sk_c6),sk_c6)** -> . % 0.19/0.48 1025[3:Rew:38.0,1014.0,1020.0,1014.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 1027[3:Rew:1025.0,503.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 1038[3:Rew:1027.0,1018.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.19/0.48 1039[3:MRR:1038.0,1024.0] || -> . % 0.19/0.48 1045[2:Spt:1039.0,3.1,266.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.19/0.48 1046[2:Spt:1039.0,3.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.19/0.48 1047[2:MRR:7.1,1045.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.48 1048[2:MRR:5.1,1045.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.19/0.48 1049[2:MRR:6.1,1045.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.19/0.48 1050[2:MRR:4.1,1045.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.19/0.48 1051[2:MRR:2.1,1045.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.48 1060[2:SpR:1049.0,105.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c7)**. % 0.19/0.48 1062[2:Rew:1047.0,1060.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.19/0.48 1063[2:Rew:1051.0,1062.0] || -> equal(sk_c7,sk_c6)**. % 0.19/0.48 1064[2:Rew:1063.0,1046.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.19/0.48 1067[2:Rew:1063.0,1045.0] || equal(multiply(sk_c6,sk_c6),sk_c5)** -> . % 0.19/0.48 1068[2:Rew:1063.0,1050.0] || -> equal(multiply(sk_c3,sk_c6),sk_c6)**. % 0.19/0.48 1069[2:Rew:1063.0,1051.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.19/0.48 1084[2:SpR:1068.0,105.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c6)**. % 0.19/0.48 1086[2:Rew:1048.0,1084.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.19/0.48 1087[2:Rew:1086.0,1067.0] || equal(sk_c5,sk_c6)** -> . % 0.19/0.48 1089[2:SpR:1069.0,105.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.19/0.48 1091[2:Rew:1064.0,1089.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.19/0.48 1093[2:SpR:1086.0,105.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c6)**. % 0.19/0.48 1095[2:Rew:1064.0,1093.0] || -> equal(multiply(sk_c5,sk_c6),sk_c6)**. % 0.19/0.48 1096[2:Rew:1091.0,1095.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.48 1097[2:MRR:1096.0,1087.0] || -> . % 0.19/0.48 % SZS output end Refutation % 0.19/0.48 Formulae used in the proof : prove_this_2 prove_this_3 prove_this_4 prove_this_5 prove_this_6 prove_this_7 prove_this_8 prove_this_9 prove_this_10 prove_this_11 prove_this_12 prove_this_13 prove_this_14 prove_this_15 prove_this_16 prove_this_17 prove_this_18 prove_this_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_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_36 left_identity left_inverse associativity % 0.19/0.48 %------------------------------------------------------------------------------