%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP235-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n008.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:27 EDT 2022 % Result : Unsatisfiable 0.20s 0.48s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP235-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.12 % Command : run_spass %d %s % 0.14/0.33 % Computer : n008.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 600 % 0.14/0.33 % DateTime : Tue Jun 14 04:15:22 EDT 2022 % 0.14/0.33 % CPUTime : % 0.20/0.48 % 0.20/0.48 SPASS V 3.9 % 0.20/0.48 SPASS beiseite: Proof found. % 0.20/0.48 % SZS status Theorem % 0.20/0.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.48 SPASS derived 1030 clauses, backtracked 429 clauses, performed 12 splits and kept 744 clauses. % 0.20/0.48 SPASS allocated 63786 KBytes. % 0.20/0.48 SPASS spent 0:00:00.14 on the problem. % 0.20/0.48 0:00:00.03 for the input. % 0.20/0.48 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.48 0:00:00.01 for inferences. % 0.20/0.48 0:00:00.00 for the backtracking. % 0.20/0.48 0:00:00.07 for the reduction. % 0.20/0.48 % 0.20/0.48 % 0.20/0.48 Here is a proof with depth 5, length 413 : % 0.20/0.48 % SZS output start Refutation % 0.20/0.48 1[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c8),sk_c7)**. % 0.20/0.48 2[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.20/0.48 3[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.20/0.48 4[0:Inp] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.48 5[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c8),sk_c7)**. % 0.20/0.48 6[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c1),sk_c8)**. % 0.20/0.48 8[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.20/0.49 9[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.49 10[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c1),sk_c8)**. % 0.20/0.49 11[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 13[0:Inp] || -> equal(multiply(sk_c8,sk_c6),sk_c7)** equal(multiply(sk_c1,sk_c7),sk_c8). % 0.20/0.49 14[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 15[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 16[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 17[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c8) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 18[0:Inp] || -> equal(multiply(sk_c8,sk_c6),sk_c7)** equal(multiply(sk_c2,sk_c3),sk_c7). % 0.20/0.49 19[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 20[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 21[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 22[0:Inp] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.20/0.49 23[0:Inp] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.20/0.49 24[0:Inp] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.49 25[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 27[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c8) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 28[0:Inp] || -> equal(multiply(sk_c8,sk_c6),sk_c7)** equal(multiply(sk_c3,sk_c8),sk_c7). % 0.20/0.49 31[0:Inp] || equal(inverse(sk_c8),sk_c7) equal(inverse(u),sk_c8) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,w),sk_c7)** equal(inverse(v),w) equal(multiply(w,sk_c8),sk_c7)** equal(inverse(x),sk_c8) equal(multiply(x,sk_c7),sk_c8)** equal(multiply(sk_c8,y),sk_c7)** equal(multiply(z,sk_c8),y)* equal(inverse(z),sk_c8) -> . % 0.20/0.49 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.20/0.49 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.20/0.49 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.20/0.49 35[0:Con:31.6] || equal(inverse(u),v) equal(inverse(w),sk_c8) equal(inverse(x),sk_c8) equal(inverse(sk_c8),sk_c7) equal(multiply(u,v),sk_c7)**+ equal(multiply(w,sk_c8),y)* equal(multiply(v,sk_c8),sk_c7)** equal(multiply(x,sk_c7),sk_c8)** equal(multiply(sk_c8,y),sk_c7)** -> . % 0.20/0.49 36[1:Spt:35.0,35.4,35.6] || equal(inverse(u),v) equal(multiply(u,v),sk_c7)**+ equal(multiply(v,sk_c8),sk_c7)** -> . % 0.20/0.49 37[2:Spt:5.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.20/0.49 39[3:Spt:1.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 41[4:Spt:4.1] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.49 43[4:SpL:41.0,36.1] || equal(inverse(sk_c5),sk_c8) equal(sk_c6,sk_c7) equal(multiply(sk_c8,sk_c8),sk_c7)** -> . % 0.20/0.49 44[4:Rew:37.0,43.0] || equal(sk_c8,sk_c8) equal(sk_c6,sk_c7) equal(multiply(sk_c8,sk_c8),sk_c7)** -> . % 0.20/0.49 45[4:Obv:44.0] || equal(sk_c6,sk_c7) equal(multiply(sk_c8,sk_c8),sk_c7)** -> . % 0.20/0.49 47[1:SpL:32.0,36.1] || equal(inverse(identity),u) equal(u,sk_c7) equal(multiply(u,sk_c8),sk_c7)** -> . % 0.20/0.49 48[5:Spt:3.1] || -> equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.20/0.49 50[5:SpL:48.0,36.1] || equal(inverse(sk_c8),sk_c6) equal(sk_c7,sk_c7) equal(multiply(sk_c6,sk_c8),sk_c7)** -> . % 0.20/0.49 51[5:Obv:50.1] || equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c6,sk_c8),sk_c7)** -> . % 0.20/0.49 52[6:Spt:2.1] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.20/0.49 58[2:SpR:37.0,33.0] || -> equal(multiply(sk_c8,sk_c5),identity)**. % 0.20/0.49 59[3:SpR:39.0,33.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.20/0.49 62[2:SpL:58.0,36.1] || equal(inverse(sk_c8),sk_c5) equal(identity,sk_c7) equal(multiply(sk_c5,sk_c8),sk_c7)** -> . % 0.20/0.49 63[4:Rew:41.0,62.2] || equal(inverse(sk_c8),sk_c5)** equal(identity,sk_c7) equal(sk_c6,sk_c7) -> . % 0.20/0.49 68[4:SpR:41.0,34.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),multiply(sk_c6,u))**. % 0.20/0.49 70[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.49 72[2:SpR:58.0,34.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),multiply(identity,u))**. % 0.20/0.49 73[3:SpR:59.0,34.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),multiply(identity,u))**. % 0.20/0.49 76[2:Rew:32.0,72.0] || -> equal(multiply(sk_c8,multiply(sk_c5,u)),u)**. % 0.20/0.49 77[3:Rew:32.0,73.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),u)**. % 0.20/0.49 78[0:Rew:32.0,70.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.49 82[4:SpR:41.0,76.0] || -> equal(multiply(sk_c8,sk_c6),sk_c8)**. % 0.20/0.49 83[2:SpL:76.0,36.1] || equal(multiply(sk_c5,u),inverse(sk_c8)) equal(u,sk_c7) equal(multiply(multiply(sk_c5,u),sk_c8),sk_c7)** -> . % 0.20/0.49 84[5:Rew:48.0,82.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 87[5:Rew:84.0,39.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.49 88[5:Rew:84.0,41.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.20/0.49 89[5:Rew:84.0,48.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.49 90[6:Rew:84.0,52.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7)**. % 0.20/0.49 91[5:Rew:84.0,58.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.20/0.49 92[5:Rew:84.0,59.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.20/0.49 94[5:Rew:84.0,51.0] || equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c6,sk_c8),sk_c7)** -> . % 0.20/0.49 95[5:Rew:84.0,63.0] || equal(inverse(sk_c7),sk_c5)** equal(identity,sk_c7) equal(sk_c6,sk_c7) -> . % 0.20/0.49 104[5:Rew:84.0,77.0] || -> equal(multiply(sk_c7,multiply(sk_c4,u)),u)**. % 0.20/0.49 110[5:Rew:84.0,94.1] || equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c7)** -> . % 0.20/0.49 113[2:Rew:34.0,83.2] || equal(multiply(sk_c5,u),inverse(sk_c8)) equal(u,sk_c7) equal(multiply(sk_c5,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 133[0:SpR:78.0,78.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.49 135[0:SpR:32.0,78.0] || -> equal(multiply(inverse(identity),u),u)**. % 0.20/0.49 136[0:SpR:33.0,78.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.49 140[5:SpR:89.0,78.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.49 141[5:SpR:91.0,78.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c5)**. % 0.20/0.49 142[5:SpR:92.0,78.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c4)**. % 0.20/0.49 148[5:Rew:33.0,140.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 149[5:Rew:148.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 155[5:Rew:148.0,95.1] || equal(inverse(sk_c7),sk_c5)** equal(sk_c6,sk_c7) equal(sk_c6,sk_c7) -> . % 0.20/0.49 157[5:Rew:148.0,135.0] || -> equal(multiply(inverse(sk_c6),u),u)**. % 0.20/0.49 160[5:Rew:149.0,110.1] || equal(inverse(sk_c7),sk_c6)** equal(sk_c7,sk_c7) -> . % 0.20/0.49 161[5:Rew:148.0,141.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c5)**. % 0.20/0.49 162[5:Rew:161.0,142.0,148.0,142.0] || -> equal(sk_c5,sk_c4)**. % 0.20/0.49 164[5:Rew:162.0,88.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.49 168[5:Rew:162.0,161.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c4)**. % 0.20/0.49 169[6:Rew:90.0,164.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 178[6:Rew:169.0,157.0] || -> equal(multiply(inverse(sk_c7),u),u)**. % 0.20/0.49 179[6:Rew:178.0,168.0,169.0,168.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.49 180[6:Rew:179.0,87.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 184[6:Rew:179.0,162.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.49 199[5:Obv:160.1] || equal(inverse(sk_c7),sk_c6)** -> . % 0.20/0.49 205[5:Obv:155.1] || equal(inverse(sk_c7),sk_c5)** equal(sk_c6,sk_c7) -> . % 0.20/0.49 206[6:Rew:169.0,205.1,180.0,205.0,184.0,205.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.49 207[6:Obv:206.1] || -> . % 0.20/0.49 213[6:Spt:207.0,2.1,52.0] || equal(multiply(sk_c4,sk_c7),sk_c8)** -> . % 0.20/0.49 214[6:Spt:207.0,2.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.20/0.49 215[6:Rew:84.0,214.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 216[6:Rew:215.0,199.0] || equal(sk_c6,sk_c7)** -> . % 0.20/0.49 217[6:Rew:89.0,168.0,215.0,168.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.49 220[6:Rew:217.0,164.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 224[6:Rew:217.0,104.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.49 230[5:Rew:84.0,22.1] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c4,sk_c7),sk_c7)**. % 0.20/0.49 231[6:Rew:220.0,230.1,217.0,230.1] || -> equal(inverse(sk_c2),sk_c3)** equal(sk_c6,sk_c7). % 0.20/0.49 232[6:MRR:231.1,216.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 238[5:Rew:84.0,27.1,84.0,27.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.49 239[6:Rew:220.0,238.0,217.0,238.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.49 240[6:MRR:239.0,216.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.49 241[5:Rew:84.0,17.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 242[6:Rew:220.0,241.0,217.0,241.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 243[6:MRR:242.0,216.0] || -> equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 266[6:SpR:240.0,34.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.49 270[6:SpR:243.0,78.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c3)**. % 0.20/0.49 272[6:Rew:240.0,270.0,232.0,270.0] || -> equal(sk_c3,sk_c7)**. % 0.20/0.49 278[6:Rew:272.0,266.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.49 284[6:Rew:224.0,278.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 285[6:Rew:284.0,220.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 291[6:MRR:285.0,216.0] || -> . % 0.20/0.49 294[5:Spt:291.0,3.1,48.0] || equal(multiply(sk_c8,sk_c6),sk_c7)** -> . % 0.20/0.49 295[5:Spt:291.0,3.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.20/0.49 296[5:Rew:82.0,294.0] || equal(sk_c8,sk_c7)** -> . % 0.20/0.49 297[0:Rew:133.0,136.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.49 298[4:Rew:82.0,23.1] || -> equal(inverse(sk_c2),sk_c3)** equal(sk_c8,sk_c7). % 0.20/0.49 299[5:MRR:298.1,296.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 300[4:Rew:82.0,8.1] || -> equal(inverse(sk_c1),sk_c8)** equal(sk_c8,sk_c7). % 0.20/0.49 301[5:MRR:300.1,296.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.20/0.49 302[4:Rew:82.0,28.0] || -> equal(sk_c8,sk_c7) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 303[5:MRR:302.0,296.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 304[4:Rew:82.0,18.0] || -> equal(sk_c8,sk_c7) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 305[5:MRR:304.0,296.0] || -> equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 306[4:Rew:82.0,13.0] || -> equal(sk_c8,sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 307[5:MRR:306.0,296.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 314[5:SpR:295.0,78.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),u)**. % 0.20/0.49 325[4:SpR:82.0,78.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c6)**. % 0.20/0.49 327[5:Rew:295.0,325.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.20/0.49 329[3:SpR:59.0,78.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c4)**. % 0.20/0.49 343[5:SpR:303.0,34.0] || -> equal(multiply(sk_c3,multiply(sk_c8,u)),multiply(sk_c7,u))**. % 0.20/0.49 347[2:SpR:58.0,78.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c5)**. % 0.20/0.49 349[5:Rew:295.0,347.0] || -> equal(multiply(sk_c7,identity),sk_c5)**. % 0.20/0.49 350[5:Rew:297.0,349.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.49 356[5:Rew:350.0,68.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),multiply(sk_c6,u))**. % 0.20/0.49 358[5:Rew:314.0,356.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 363[5:SpR:305.0,78.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c3)**. % 0.20/0.49 365[5:Rew:299.0,363.0] || -> equal(multiply(sk_c3,sk_c7),sk_c3)**. % 0.20/0.49 367[5:SpR:307.0,78.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.20/0.49 369[5:Rew:301.0,367.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.20/0.49 370[5:Rew:369.0,45.1] || equal(sk_c6,sk_c7)** equal(sk_c7,sk_c7) -> . % 0.20/0.49 371[5:Obv:370.1] || equal(sk_c6,sk_c7)** -> . % 0.20/0.49 386[5:SpR:365.0,78.0] || -> equal(multiply(inverse(sk_c3),sk_c3),sk_c7)**. % 0.20/0.49 388[5:Rew:33.0,386.0] || -> equal(identity,sk_c7)**. % 0.20/0.49 389[5:Rew:388.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 396[5:Rew:389.0,327.0] || -> equal(sk_c8,sk_c6)**. % 0.20/0.49 398[5:Rew:389.0,343.0] || -> equal(multiply(sk_c3,multiply(sk_c8,u)),u)**. % 0.20/0.49 408[5:Rew:396.0,303.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.49 426[5:Rew:358.0,398.0,396.0,398.0] || -> equal(multiply(sk_c3,u),u)**. % 0.20/0.49 427[5:Rew:426.0,408.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 429[5:MRR:427.0,371.0] || -> . % 0.20/0.49 443[4:Spt:429.0,4.1,41.0] || equal(multiply(sk_c5,sk_c8),sk_c6)** -> . % 0.20/0.49 444[4:Spt:429.0,4.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.20/0.49 445[4:Rew:297.0,329.0,444.0,329.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.49 447[4:Rew:445.0,59.0] || -> equal(multiply(sk_c8,sk_c7),identity)**. % 0.20/0.49 448[4:Rew:297.0,347.0,444.0,347.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.49 451[4:Rew:448.0,443.0] || equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.20/0.49 458[4:Rew:448.0,24.1] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.20/0.49 459[4:MRR:458.1,451.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 467[4:Rew:448.0,19.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 468[4:MRR:467.0,451.0] || -> equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 469[4:Rew:448.0,14.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 470[4:MRR:469.0,451.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 475[4:Rew:448.0,113.2,448.0,113.0,444.0,113.0] || equal(multiply(sk_c7,u),sk_c7) equal(u,sk_c7) equal(multiply(sk_c7,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 498[4:SpR:468.0,78.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c3)**. % 0.20/0.49 500[4:Rew:459.0,498.0] || -> equal(multiply(sk_c3,sk_c7),sk_c3)**. % 0.20/0.49 506[4:SpR:500.0,78.0] || -> equal(multiply(inverse(sk_c3),sk_c3),sk_c7)**. % 0.20/0.49 508[4:Rew:33.0,506.0] || -> equal(identity,sk_c7)**. % 0.20/0.49 509[4:Rew:508.0,447.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7)**. % 0.20/0.49 510[4:Rew:508.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 511[4:Rew:508.0,297.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 519[4:Rew:510.0,475.0] || equal(u,sk_c7) equal(u,sk_c7) equal(multiply(sk_c7,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 524[4:Rew:511.0,470.0] || -> equal(sk_c8,sk_c1)**. % 0.20/0.49 525[4:Rew:511.0,509.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 536[4:Rew:524.0,525.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.49 537[4:Rew:536.0,524.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 568[4:Obv:519.0] || equal(u,sk_c7) equal(multiply(sk_c7,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 569[4:Rew:511.0,568.1,537.0,568.1,510.0,568.1] || equal(u,sk_c7)* equal(u,sk_c7)* -> . % 0.20/0.49 570[4:Obv:569.0] || equal(u,sk_c7)* -> . % 0.20/0.49 571[4:UnC:570.0,448.0] || -> . % 0.20/0.49 574[3:Spt:571.0,1.0,39.0] || equal(inverse(sk_c4),sk_c8)** -> . % 0.20/0.49 575[3:Spt:571.0,1.1] || -> equal(inverse(sk_c8),sk_c7)**. % 0.20/0.49 576[3:Rew:297.0,347.0,575.0,347.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.49 578[3:Rew:576.0,58.0] || -> equal(multiply(sk_c8,sk_c7),identity)**. % 0.20/0.49 580[3:MRR:21.0,574.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 584[3:MRR:16.0,574.0] || -> equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 585[3:MRR:11.0,574.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 588[3:Rew:576.0,113.2,576.0,113.0,575.0,113.0] || equal(multiply(sk_c7,u),sk_c7) equal(u,sk_c7) equal(multiply(sk_c7,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 611[3:SpR:584.0,78.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c3)**. % 0.20/0.49 613[3:Rew:580.0,611.0] || -> equal(multiply(sk_c3,sk_c7),sk_c3)**. % 0.20/0.49 619[3:SpR:613.0,78.0] || -> equal(multiply(inverse(sk_c3),sk_c3),sk_c7)**. % 0.20/0.49 621[3:Rew:33.0,619.0] || -> equal(identity,sk_c7)**. % 0.20/0.49 622[3:Rew:621.0,578.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7)**. % 0.20/0.49 623[3:Rew:621.0,297.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 624[3:Rew:621.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 630[3:Rew:623.0,585.0] || -> equal(sk_c8,sk_c1)**. % 0.20/0.49 631[3:Rew:623.0,622.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 639[3:Rew:630.0,588.2] || equal(multiply(sk_c7,u),sk_c7) equal(u,sk_c7) equal(multiply(sk_c7,multiply(u,sk_c1)),sk_c7)** -> . % 0.20/0.49 647[3:Rew:630.0,631.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.49 681[3:Rew:623.0,639.2,647.0,639.2,624.0,639.2,624.0,639.0] || equal(u,sk_c7)* equal(u,sk_c7)* equal(u,sk_c7)* -> . % 0.20/0.49 682[3:Obv:681.1] || equal(u,sk_c7)* -> . % 0.20/0.49 683[3:UnC:682.0,576.0] || -> . % 0.20/0.49 685[2:Spt:683.0,5.0,37.0] || equal(inverse(sk_c5),sk_c8)** -> . % 0.20/0.49 686[2:Spt:683.0,5.1] || -> equal(inverse(sk_c8),sk_c7)**. % 0.20/0.49 687[2:MRR:25.0,685.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 688[2:MRR:10.0,685.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.20/0.49 690[2:MRR:20.0,685.0] || -> equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 691[2:MRR:15.0,685.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 702[2:SpR:690.0,78.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c3)**. % 0.20/0.49 704[2:Rew:687.0,702.0] || -> equal(multiply(sk_c3,sk_c7),sk_c3)**. % 0.20/0.49 710[2:SpR:704.0,78.0] || -> equal(multiply(inverse(sk_c3),sk_c3),sk_c7)**. % 0.20/0.49 712[2:Rew:33.0,710.0] || -> equal(identity,sk_c7)**. % 0.20/0.49 714[2:Rew:712.0,297.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 716[2:Rew:712.0,47.0] || equal(inverse(sk_c7),u) equal(u,sk_c7) equal(multiply(u,sk_c8),sk_c7)** -> . % 0.20/0.49 723[2:Rew:714.0,691.0] || -> equal(sk_c8,sk_c1)**. % 0.20/0.49 725[2:Rew:723.0,686.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 726[2:Rew:723.0,688.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.20/0.49 734[2:Rew:725.0,726.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.49 735[2:Rew:734.0,723.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 737[2:Rew:734.0,725.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 755[2:Rew:714.0,716.2,735.0,716.2,737.0,716.0] || equal(sk_c7,u)* equal(u,sk_c7)* equal(u,sk_c7)* -> . % 0.20/0.49 756[2:Obv:755.1] || equal(u,sk_c7)* -> . % 0.20/0.49 757[2:UnC:756.0,78.0] || -> . % 0.20/0.49 762[1:Spt:757.0,35.1,35.2,35.3,35.5,35.7,35.8] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(sk_c8),sk_c7) equal(multiply(u,sk_c8),w)*+ equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,w),sk_c7)** -> . % 0.20/0.49 763[1:EqR:762.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(sk_c8),sk_c7) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 765[2:Spt:1.1] || -> equal(inverse(sk_c8),sk_c7)**. % 0.20/0.49 768[2:Rew:765.0,763.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(sk_c7,sk_c7) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 769[2:Obv:768.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 774[3:Spt:25.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.20/0.49 777[4:Spt:21.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 791[0:SpR:33.0,78.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.49 792[0:SpR:33.0,297.0] || -> equal(inverse(identity),identity)**. % 0.20/0.49 794[2:SpR:765.0,33.0] || -> equal(multiply(sk_c7,sk_c8),identity)**. % 0.20/0.49 795[3:SpR:774.0,33.0] || -> equal(multiply(sk_c8,sk_c5),identity)**. % 0.20/0.49 796[4:SpR:777.0,33.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.20/0.49 798[0:Rew:297.0,791.0] || -> equal(inverse(inverse(u)),u)**. % 0.20/0.49 801[5:Spt:22.0] || -> equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 803[5:SpR:801.0,33.0] || -> equal(multiply(sk_c3,sk_c2),identity)**. % 0.20/0.49 810[2:SpR:794.0,78.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c8)**. % 0.20/0.49 812[2:Rew:297.0,810.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.20/0.49 815[2:SpR:812.0,33.0] || -> equal(multiply(sk_c8,sk_c7),identity)**. % 0.20/0.49 818[3:SpR:795.0,78.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c5)**. % 0.20/0.49 820[3:Rew:297.0,818.0,765.0,818.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.49 823[3:Rew:820.0,14.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 824[3:Rew:820.0,19.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 826[3:Rew:820.0,9.1] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.20/0.49 830[3:Rew:794.0,826.1] || -> equal(inverse(sk_c1),sk_c8)** equal(identity,sk_c6). % 0.20/0.49 831[3:Rew:794.0,823.0] || -> equal(identity,sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 832[3:Rew:794.0,824.0] || -> equal(identity,sk_c6) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 834[6:Spt:830.1] || -> equal(identity,sk_c6)**. % 0.20/0.49 835[6:Rew:834.0,297.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 836[6:Rew:834.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 837[6:Rew:834.0,33.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.20/0.49 838[6:Rew:834.0,792.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.49 840[6:Rew:834.0,796.0] || -> equal(multiply(sk_c8,sk_c4),sk_c6)**. % 0.20/0.49 841[6:Rew:834.0,803.0] || -> equal(multiply(sk_c3,sk_c2),sk_c6)**. % 0.20/0.49 842[6:Rew:834.0,815.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 844[6:Rew:835.0,18.0] || -> equal(sk_c8,sk_c7) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 849[6:Rew:844.0,17.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 862[6:SpR:840.0,78.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c4)**. % 0.20/0.49 864[6:Rew:765.0,862.0] || -> equal(multiply(sk_c7,sk_c6),sk_c4)**. % 0.20/0.49 865[6:Rew:835.0,864.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.49 870[6:Rew:865.0,849.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7) equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 880[6:SpR:841.0,78.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c2)**. % 0.20/0.49 882[6:Rew:835.0,880.0] || -> equal(inverse(sk_c3),sk_c2)**. % 0.20/0.49 898[6:SpR:882.0,837.0] || -> equal(multiply(sk_c2,sk_c3),sk_c6)**. % 0.20/0.49 899[6:Rew:898.0,870.1] || -> equal(multiply(sk_c7,sk_c7),sk_c7)** equal(sk_c6,sk_c7). % 0.20/0.49 900[6:Rew:898.0,844.1] || -> equal(sk_c8,sk_c7)** equal(sk_c6,sk_c7). % 0.20/0.49 908[0:SpR:798.0,78.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.20/0.49 913[5:SpR:801.0,798.0] || -> equal(inverse(sk_c3),sk_c2)**. % 0.20/0.49 925[7:Spt:900.1] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 927[7:Rew:925.0,838.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 929[7:Rew:925.0,836.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 934[7:Rew:925.0,835.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 936[7:Rew:812.0,927.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 937[7:Rew:936.0,765.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 940[7:Rew:936.0,769.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 951[7:Rew:934.0,940.3,929.0,940.3,936.0,940.3,934.0,940.2,936.0,940.2,936.0,940.1] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(v,sk_c7) equal(u,sk_c7) -> . % 0.20/0.49 952[7:Con:951.0] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.49 1015[7:SpL:937.0,952.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.49 1016[7:Obv:1015.1] || -> . % 0.20/0.49 1017[7:Spt:1016.0,900.1,925.0] || equal(sk_c6,sk_c7)** -> . % 0.20/0.49 1018[7:Spt:1016.0,900.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 1021[7:Rew:1018.0,842.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 1025[7:Rew:1021.0,899.0] || -> equal(sk_c6,sk_c7)** equal(sk_c6,sk_c7)**. % 0.20/0.49 1026[7:Obv:1025.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 1027[7:MRR:1026.0,1017.0] || -> . % 0.20/0.49 1037[6:Spt:1027.0,830.1,834.0] || equal(identity,sk_c6)** -> . % 0.20/0.49 1038[6:Spt:1027.0,830.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.20/0.49 1039[6:MRR:831.0,1037.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 1040[6:MRR:832.0,1037.0] || -> equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 1044[6:SpR:1038.0,798.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.20/0.49 1046[6:Rew:765.0,1044.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.49 1048[6:Rew:1046.0,1039.0] || -> equal(multiply(sk_c7,sk_c7),sk_c8)**. % 0.20/0.49 1062[4:SpR:777.0,798.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.20/0.49 1064[4:Rew:765.0,1062.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.49 1070[5:SpR:913.0,78.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.20/0.49 1078[6:SpR:1040.0,34.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c7,u))**. % 0.20/0.49 1083[6:Rew:1070.0,1078.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 1084[6:Rew:1083.0,794.0] || -> equal(sk_c8,identity)**. % 0.20/0.49 1085[6:Rew:1083.0,1048.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 1088[6:Rew:1084.0,812.0] || -> equal(inverse(sk_c7),identity)**. % 0.20/0.49 1093[6:Rew:1084.0,769.0] || equal(inverse(u),identity) equal(inverse(v),sk_c8) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 1095[6:Rew:1084.0,1085.0] || -> equal(identity,sk_c7)**. % 0.20/0.49 1099[6:Rew:1095.0,297.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 1102[6:Rew:1095.0,1084.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 1103[6:Rew:1095.0,1088.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 1121[6:Rew:1099.0,1093.3,1083.0,1093.3,1102.0,1093.3,1099.0,1093.2,1102.0,1093.2,1102.0,1093.1,1095.0,1093.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(v,sk_c7) equal(u,sk_c7) -> . % 0.20/0.49 1122[6:Con:1121.0] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.49 1153[6:SpL:1103.0,1122.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.49 1154[6:Obv:1153.1] || -> . % 0.20/0.49 1155[5:Spt:1154.0,22.0,801.0] || equal(inverse(sk_c2),sk_c3)** -> . % 0.20/0.49 1156[5:Spt:1154.0,22.1] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.20/0.49 1157[5:Rew:1064.0,1156.0] || -> equal(multiply(sk_c7,sk_c7),sk_c8)**. % 0.20/0.49 1159[3:Rew:820.0,24.1] || -> equal(inverse(sk_c2),sk_c3) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.20/0.49 1160[3:Rew:794.0,1159.1] || -> equal(inverse(sk_c2),sk_c3)** equal(identity,sk_c6). % 0.20/0.49 1161[5:MRR:1160.0,1155.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 1163[5:Rew:1161.0,794.0] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.20/0.49 1165[5:Rew:1161.0,297.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 1166[5:Rew:1161.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 1169[5:Rew:1165.0,23.1] || -> equal(inverse(sk_c2),sk_c3)** equal(sk_c8,sk_c7). % 0.20/0.49 1170[5:MRR:1169.0,1155.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 1171[5:Rew:1170.0,765.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 1173[5:Rew:1170.0,1157.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.49 1176[5:Rew:1170.0,1163.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 1178[5:Rew:1173.0,1176.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 1181[5:Rew:1178.0,1165.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 1182[5:Rew:1178.0,1166.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 1196[5:Rew:1181.0,769.3,1182.0,769.3,1170.0,769.3,1181.0,769.2,1170.0,769.2,1170.0,769.1,1170.0,769.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(v,sk_c7) equal(u,sk_c7) -> . % 0.20/0.49 1197[5:Con:1196.0] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.49 1235[5:SpL:1171.0,1197.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.49 1236[5:Obv:1235.1] || -> . % 0.20/0.49 1237[4:Spt:1236.0,21.0,777.0] || equal(inverse(sk_c4),sk_c8)** -> . % 0.20/0.49 1238[4:Spt:1236.0,21.1] || -> equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 1239[4:MRR:6.0,1237.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.20/0.49 1241[4:MRR:16.0,1237.0] || -> equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 1242[4:MRR:11.0,1237.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 1244[4:SpR:1238.0,798.0] || -> equal(inverse(sk_c3),sk_c2)**. % 0.20/0.49 1257[4:SpR:1239.0,798.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.20/0.49 1259[4:Rew:765.0,1257.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.49 1261[4:Rew:1259.0,1242.0] || -> equal(multiply(sk_c7,sk_c7),sk_c8)**. % 0.20/0.49 1264[4:SpR:1244.0,78.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.20/0.49 1281[4:SpR:1241.0,34.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c7,u))**. % 0.20/0.49 1285[4:Rew:1264.0,1281.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 1286[4:Rew:1285.0,794.0] || -> equal(sk_c8,identity)**. % 0.20/0.49 1287[4:Rew:1285.0,1261.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 1291[4:Rew:1286.0,812.0] || -> equal(inverse(sk_c7),identity)**. % 0.20/0.49 1297[4:Rew:1286.0,769.0] || equal(inverse(u),identity) equal(inverse(v),sk_c8) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 1300[4:Rew:1286.0,1287.0] || -> equal(identity,sk_c7)**. % 0.20/0.49 1303[4:Rew:1300.0,297.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 1305[4:Rew:1300.0,1286.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 1306[4:Rew:1300.0,1291.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 1326[4:Rew:1303.0,1297.3,1285.0,1297.3,1305.0,1297.3,1303.0,1297.2,1305.0,1297.2,1305.0,1297.1,1300.0,1297.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(v,sk_c7) equal(u,sk_c7) -> . % 0.20/0.49 1327[4:Con:1326.0] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.49 1383[4:SpL:1306.0,1327.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.49 1384[4:Obv:1383.1] || -> . % 0.20/0.49 1385[3:Spt:1384.0,25.0,774.0] || equal(inverse(sk_c5),sk_c8)** -> . % 0.20/0.49 1386[3:Spt:1384.0,25.1] || -> equal(inverse(sk_c2),sk_c3)**. % 0.20/0.49 1387[3:MRR:10.0,1385.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.20/0.49 1389[3:MRR:20.0,1385.0] || -> equal(multiply(sk_c2,sk_c3),sk_c7)**. % 0.20/0.49 1390[3:MRR:15.0,1385.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 1393[3:SpR:1386.0,908.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),u)**. % 0.20/0.49 1400[3:SpR:1387.0,798.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.20/0.49 1403[3:Rew:765.0,1400.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.49 1405[3:Rew:1403.0,1390.0] || -> equal(multiply(sk_c7,sk_c7),sk_c8)**. % 0.20/0.49 1437[3:SpR:1389.0,34.0] || -> equal(multiply(sk_c2,multiply(sk_c3,u)),multiply(sk_c7,u))**. % 0.20/0.49 1441[3:Rew:1393.0,1437.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 1442[3:Rew:1441.0,794.0] || -> equal(sk_c8,identity)**. % 0.20/0.49 1445[3:Rew:1441.0,1405.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 1447[3:Rew:1442.0,765.0] || -> equal(inverse(identity),sk_c7)**. % 0.20/0.49 1453[3:Rew:1442.0,769.0] || equal(inverse(u),identity) equal(inverse(v),sk_c8) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.20/0.49 1456[3:Rew:1442.0,1445.0] || -> equal(identity,sk_c7)**. % 0.20/0.49 1458[3:Rew:1456.0,297.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 1461[3:Rew:1456.0,1442.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 1462[3:Rew:1456.0,1447.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 1482[3:Rew:1458.0,1453.3,1441.0,1453.3,1461.0,1453.3,1458.0,1453.2,1461.0,1453.2,1461.0,1453.1,1456.0,1453.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(v,sk_c7) equal(u,sk_c7) -> . % 0.20/0.49 1483[3:Con:1482.0] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.49 1530[3:SpL:1462.0,1483.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.49 1531[3:Obv:1530.1] || -> . % 0.20/0.49 1532[2:Spt:1531.0,1.1,765.0] || equal(inverse(sk_c8),sk_c7)** -> . % 0.20/0.49 1533[2:Spt:1531.0,1.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 1534[2:MRR:5.1,1532.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.20/0.49 1535[2:MRR:2.0,1532.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.20/0.49 1536[2:MRR:3.0,1532.0] || -> equal(multiply(sk_c8,sk_c6),sk_c7)**. % 0.20/0.49 1537[2:MRR:4.0,1532.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.49 1539[2:SpR:1533.0,798.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.20/0.49 1540[2:SpR:1533.0,908.0] || -> equal(multiply(sk_c4,multiply(sk_c8,u)),u)**. % 0.20/0.49 1542[2:Rew:1539.0,1532.0] || equal(sk_c4,sk_c7)** -> . % 0.20/0.49 1550[2:SpR:1534.0,798.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.20/0.49 1553[2:Rew:1539.0,1550.0] || -> equal(sk_c5,sk_c4)**. % 0.20/0.49 1555[2:Rew:1553.0,1537.0] || -> equal(multiply(sk_c4,sk_c8),sk_c6)**. % 0.20/0.49 1568[2:SpR:1536.0,78.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c6)**. % 0.20/0.49 1570[2:Rew:1535.0,1568.0,1539.0,1568.0] || -> equal(sk_c8,sk_c6)**. % 0.20/0.49 1571[2:Rew:1570.0,1533.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.49 1572[2:Rew:1570.0,1539.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.20/0.49 1574[2:Rew:1570.0,1536.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.20/0.49 1576[2:Rew:1570.0,1540.0] || -> equal(multiply(sk_c4,multiply(sk_c6,u)),u)**. % 0.20/0.49 1578[2:Rew:1570.0,1555.0] || -> equal(multiply(sk_c4,sk_c6),sk_c6)**. % 0.20/0.49 1598[2:SpR:1578.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c6,u)),multiply(sk_c6,u))**. % 0.20/0.49 1599[2:SpR:1578.0,78.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c6)**. % 0.20/0.49 1601[2:Rew:1574.0,1599.0,1571.0,1599.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 1603[2:Rew:1601.0,1571.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.49 1605[2:Rew:1601.0,1572.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.20/0.49 1609[2:Rew:1601.0,1576.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.20/0.49 1612[2:Rew:1609.0,1598.0,1601.0,1598.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 1613[2:Rew:1612.0,1609.0] || -> equal(multiply(sk_c4,u),u)**. % 0.20/0.49 1650[2:SpR:1603.0,33.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.20/0.49 1651[2:SpR:1605.0,33.0] || -> equal(multiply(sk_c4,sk_c7),identity)**. % 0.20/0.49 1652[2:Rew:1612.0,1650.0] || -> equal(identity,sk_c4)**. % 0.20/0.49 1660[2:Rew:1613.0,1651.0,1652.0,1651.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.49 1661[2:MRR:1660.0,1542.0] || -> . % 0.20/0.49 % SZS output end Refutation % 0.20/0.49 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 prove_this_5 prove_this_6 prove_this_8 prove_this_9 prove_this_10 prove_this_11 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_27 prove_this_28 prove_this_31 left_identity left_inverse associativity % 0.20/0.49 %------------------------------------------------------------------------------