%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP243-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n018.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:46:29 EDT 2022 % Result : Unsatisfiable 0.42s 0.60s % Output : Refutation 0.42s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : GRP243-1 : TPTP v8.1.0. Released v2.5.0. % 0.03/0.11 % Command : run_spass %d %s % 0.11/0.32 % Computer : n018.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Mon Jun 13 22:16:28 EDT 2022 % 0.11/0.33 % CPUTime : % 0.42/0.60 % 0.42/0.60 SPASS V 3.9 % 0.42/0.60 SPASS beiseite: Proof found. % 0.42/0.60 % SZS status Theorem % 0.42/0.60 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.42/0.60 SPASS derived 1974 clauses, backtracked 583 clauses, performed 14 splits and kept 939 clauses. % 0.42/0.60 SPASS allocated 64984 KBytes. % 0.42/0.60 SPASS spent 0:00:00.26 on the problem. % 0.42/0.60 0:00:00.04 for the input. % 0.42/0.60 0:00:00.00 for the FLOTTER CNF translation. % 0.42/0.60 0:00:00.02 for inferences. % 0.42/0.60 0:00:00.00 for the backtracking. % 0.42/0.60 0:00:00.16 for the reduction. % 0.42/0.60 % 0.42/0.60 % 0.42/0.60 Here is a proof with depth 7, length 373 : % 0.42/0.60 % SZS output start Refutation % 0.42/0.60 1[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(multiply(sk_c1,sk_c12),sk_c11)**. % 0.42/0.60 3[0:Inp] || -> equal(inverse(sk_c7),sk_c11) equal(multiply(sk_c1,sk_c12),sk_c11)**. % 0.42/0.60 6[0:Inp] || -> equal(inverse(sk_c8),sk_c9) equal(multiply(sk_c1,sk_c12),sk_c11)**. % 0.42/0.60 8[0:Inp] || -> equal(inverse(sk_c6),sk_c12)** equal(inverse(sk_c1),sk_c12). % 0.42/0.60 10[0:Inp] || -> equal(inverse(sk_c7),sk_c11)** equal(inverse(sk_c1),sk_c12). % 0.42/0.60 13[0:Inp] || -> equal(inverse(sk_c8),sk_c9)** equal(inverse(sk_c1),sk_c12). % 0.42/0.60 15[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 17[0:Inp] || -> equal(inverse(sk_c7),sk_c11) equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 18[0:Inp] || -> equal(multiply(sk_c7,sk_c10),sk_c11) equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 19[0:Inp] || -> equal(multiply(sk_c8,sk_c9),sk_c11) equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 20[0:Inp] || -> equal(inverse(sk_c8),sk_c9) equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 22[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(inverse(sk_c2),sk_c11)**. % 0.42/0.60 24[0:Inp] || -> equal(inverse(sk_c7),sk_c11) equal(inverse(sk_c2),sk_c11)**. % 0.42/0.60 25[0:Inp] || -> equal(inverse(sk_c2),sk_c11) equal(multiply(sk_c7,sk_c10),sk_c11)**. % 0.42/0.60 26[0:Inp] || -> equal(inverse(sk_c2),sk_c11) equal(multiply(sk_c8,sk_c9),sk_c11)**. % 0.42/0.60 27[0:Inp] || -> equal(inverse(sk_c8),sk_c9) equal(inverse(sk_c2),sk_c11)**. % 0.42/0.60 29[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(inverse(sk_c3),sk_c12)**. % 0.42/0.60 30[0:Inp] || -> equal(inverse(sk_c3),sk_c12) equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.42/0.60 31[0:Inp] || -> equal(inverse(sk_c7),sk_c11) equal(inverse(sk_c3),sk_c12)**. % 0.42/0.60 33[0:Inp] || -> equal(inverse(sk_c3),sk_c12) equal(multiply(sk_c8,sk_c9),sk_c11)**. % 0.42/0.60 34[0:Inp] || -> equal(inverse(sk_c8),sk_c9) equal(inverse(sk_c3),sk_c12)**. % 0.42/0.60 36[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 37[0:Inp] || -> equal(multiply(sk_c6,sk_c11),sk_c12) equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 38[0:Inp] || -> equal(inverse(sk_c7),sk_c11) equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 40[0:Inp] || -> equal(multiply(sk_c8,sk_c9),sk_c11) equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 41[0:Inp] || -> equal(inverse(sk_c8),sk_c9) equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 43[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 47[0:Inp] || -> equal(multiply(sk_c8,sk_c9),sk_c11) equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 48[0:Inp] || -> equal(inverse(sk_c8),sk_c9) equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 49[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c11) equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 50[0:Inp] || -> equal(inverse(sk_c6),sk_c12) equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 51[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.42/0.60 52[0:Inp] || -> equal(inverse(sk_c7),sk_c11) equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 53[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c7,sk_c10),sk_c11)**. % 0.42/0.60 54[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c8,sk_c9),sk_c11)**. % 0.42/0.60 55[0:Inp] || -> equal(inverse(sk_c8),sk_c9) equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 56[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c9,sk_c10),sk_c11)**. % 0.42/0.60 61[0:Inp] || -> equal(multiply(sk_c8,sk_c9),sk_c11) equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 62[0:Inp] || -> equal(inverse(sk_c8),sk_c9) equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 63[0:Inp] || -> equal(multiply(sk_c9,sk_c10),sk_c11) equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 64[0:Inp] || equal(multiply(u,sk_c12),sk_c11)** equal(inverse(u),sk_c12) equal(multiply(v,sk_c11),sk_c10)** equal(inverse(v),sk_c11) equal(inverse(w),sk_c12) equal(multiply(w,sk_c11),sk_c12)** equal(multiply(x,y),sk_c11)** equal(inverse(x),y) equal(multiply(y,sk_c10),sk_c11)** equal(inverse(z),sk_c12) equal(multiply(z,sk_c11),sk_c12)** equal(inverse(x1),sk_c11) equal(multiply(x1,sk_c10),sk_c11)** equal(multiply(x2,x3),sk_c11)** equal(inverse(x2),x3) equal(multiply(x3,sk_c10),sk_c11)** -> . % 0.42/0.60 65[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.42/0.60 66[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.42/0.60 67[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.42/0.60 68[0:Con:64.9] || equal(inverse(u),v) equal(inverse(w),sk_c11) equal(inverse(x),sk_c12) equal(inverse(y),sk_c11) equal(inverse(z),sk_c12) equal(multiply(u,v),sk_c11)**+ equal(multiply(w,sk_c10),sk_c11)** equal(multiply(v,sk_c10),sk_c11)** equal(multiply(x,sk_c11),sk_c12)** equal(multiply(y,sk_c11),sk_c10)** equal(multiply(z,sk_c12),sk_c11)** -> . % 0.42/0.60 69[1:Spt:68.0,68.5,68.7] || equal(inverse(u),v) equal(multiply(u,v),sk_c11)**+ equal(multiply(v,sk_c10),sk_c11)** -> . % 0.42/0.60 70[2:Spt:55.0] || -> equal(inverse(sk_c8),sk_c9)**. % 0.42/0.60 76[3:Spt:56.1] || -> equal(multiply(sk_c9,sk_c10),sk_c11)**. % 0.42/0.60 80[4:Spt:54.1] || -> equal(multiply(sk_c8,sk_c9),sk_c11)**. % 0.42/0.60 82[4:SpL:80.0,69.1] || equal(inverse(sk_c8),sk_c9) equal(sk_c11,sk_c11) equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.42/0.60 83[4:Obv:82.1] || equal(inverse(sk_c8),sk_c9) equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.42/0.60 84[4:Rew:76.0,83.1,70.0,83.0] || equal(sk_c9,sk_c9) equal(sk_c11,sk_c11)* -> . % 0.42/0.60 85[4:Obv:84.1] || -> . % 0.42/0.60 86[4:Spt:85.0,54.1,80.0] || equal(multiply(sk_c8,sk_c9),sk_c11)** -> . % 0.42/0.60 87[4:Spt:85.0,54.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 91[4:MRR:61.0,86.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 92[4:MRR:47.0,86.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 104[4:SpL:92.0,69.1] || equal(inverse(sk_c4),sk_c5) equal(sk_c11,sk_c11) equal(multiply(sk_c5,sk_c10),sk_c11)** -> . % 0.42/0.60 105[4:Obv:104.1] || equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c5,sk_c10),sk_c11)** -> . % 0.42/0.60 106[4:Rew:91.0,105.1,87.0,105.0] || equal(sk_c5,sk_c5) equal(sk_c11,sk_c11)* -> . % 0.42/0.60 107[4:Obv:106.1] || -> . % 0.42/0.60 108[3:Spt:107.0,56.1,76.0] || equal(multiply(sk_c9,sk_c10),sk_c11)** -> . % 0.42/0.60 109[3:Spt:107.0,56.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 113[3:MRR:63.0,108.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 114[3:MRR:49.0,108.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 126[3:SpL:114.0,69.1] || equal(inverse(sk_c4),sk_c5) equal(sk_c11,sk_c11) equal(multiply(sk_c5,sk_c10),sk_c11)** -> . % 0.42/0.60 127[3:Obv:126.1] || equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c5,sk_c10),sk_c11)** -> . % 0.42/0.60 128[3:Rew:113.0,127.1,109.0,127.0] || equal(sk_c5,sk_c5) equal(sk_c11,sk_c11)* -> . % 0.42/0.60 129[3:Obv:128.1] || -> . % 0.42/0.60 130[2:Spt:129.0,55.0,70.0] || equal(inverse(sk_c8),sk_c9)** -> . % 0.42/0.60 131[2:Spt:129.0,55.1] || -> equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 135[2:MRR:62.0,130.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 136[2:MRR:48.0,130.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 148[2:SpL:136.0,69.1] || equal(inverse(sk_c4),sk_c5) equal(sk_c11,sk_c11) equal(multiply(sk_c5,sk_c10),sk_c11)** -> . % 0.42/0.60 149[2:Obv:148.1] || equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c5,sk_c10),sk_c11)** -> . % 0.42/0.60 150[2:Rew:135.0,149.1,131.0,149.0] || equal(sk_c5,sk_c5) equal(sk_c11,sk_c11)* -> . % 0.42/0.60 151[2:Obv:150.1] || -> . % 0.42/0.60 152[1:Spt:151.0,68.1,68.2,68.3,68.4,68.6,68.8,68.9,68.10] || equal(inverse(u),sk_c11) equal(inverse(v),sk_c12) equal(inverse(w),sk_c11) equal(inverse(x),sk_c12) equal(multiply(u,sk_c10),sk_c11)**+ equal(multiply(v,sk_c11),sk_c12)** equal(multiply(w,sk_c11),sk_c10)** equal(multiply(x,sk_c12),sk_c11)** -> . % 0.42/0.60 153[2:Spt:50.0] || -> equal(inverse(sk_c6),sk_c12)**. % 0.42/0.60 155[3:Spt:52.0] || -> equal(inverse(sk_c7),sk_c11)**. % 0.42/0.60 157[4:Spt:34.0] || -> equal(inverse(sk_c8),sk_c9)**. % 0.42/0.60 159[5:Spt:53.1] || -> equal(multiply(sk_c7,sk_c10),sk_c11)**. % 0.42/0.60 161[5:SpL:159.0,152.4] || equal(inverse(sk_c7),sk_c11) equal(inverse(u),sk_c12) equal(inverse(v),sk_c11) equal(inverse(w),sk_c12) equal(sk_c11,sk_c11) equal(multiply(u,sk_c11),sk_c12)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c12),sk_c11)** -> . % 0.42/0.60 162[5:Obv:161.4] || equal(inverse(sk_c7),sk_c11) equal(inverse(u),sk_c12) equal(inverse(v),sk_c11) equal(inverse(w),sk_c12) equal(multiply(u,sk_c11),sk_c12)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c12),sk_c11)** -> . % 0.42/0.60 163[5:Rew:155.0,162.0] || equal(sk_c11,sk_c11) equal(inverse(u),sk_c12) equal(inverse(v),sk_c11) equal(inverse(w),sk_c12) equal(multiply(u,sk_c11),sk_c12)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c12),sk_c11)** -> . % 0.42/0.60 164[5:Obv:163.0] || equal(inverse(u),sk_c12) equal(inverse(v),sk_c11) equal(inverse(w),sk_c12) equal(multiply(u,sk_c11),sk_c12)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c12),sk_c11)** -> . % 0.42/0.60 165[6:Spt:51.1] || -> equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.42/0.60 167[7:Spt:54.1] || -> equal(multiply(sk_c8,sk_c9),sk_c11)**. % 0.42/0.60 173[2:SpR:153.0,66.0] || -> equal(multiply(sk_c12,sk_c6),identity)**. % 0.42/0.60 174[3:SpR:155.0,66.0] || -> equal(multiply(sk_c11,sk_c7),identity)**. % 0.42/0.60 175[4:SpR:157.0,66.0] || -> equal(multiply(sk_c9,sk_c8),identity)**. % 0.42/0.60 184[0:SpR:66.0,67.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.42/0.60 185[2:SpR:173.0,67.0] || -> equal(multiply(sk_c12,multiply(sk_c6,u)),multiply(identity,u))**. % 0.42/0.60 186[2:Rew:65.0,185.0] || -> equal(multiply(sk_c12,multiply(sk_c6,u)),u)**. % 0.42/0.60 187[0:Rew:65.0,184.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.42/0.60 197[6:SpR:165.0,186.0] || -> equal(multiply(sk_c12,sk_c12),sk_c11)**. % 0.42/0.60 202[0:SpR:187.0,187.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.42/0.60 204[5:SpR:159.0,187.0] || -> equal(multiply(inverse(sk_c7),sk_c11),sk_c10)**. % 0.42/0.60 208[0:SpR:65.0,187.0] || -> equal(multiply(inverse(identity),u),u)**. % 0.42/0.60 209[0:SpR:66.0,187.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.42/0.60 214[3:SpR:174.0,187.0] || -> equal(multiply(inverse(sk_c11),identity),sk_c7)**. % 0.42/0.60 215[4:SpR:175.0,187.0] || -> equal(multiply(inverse(sk_c9),identity),sk_c8)**. % 0.42/0.60 219[5:Rew:155.0,204.0] || -> equal(multiply(sk_c11,sk_c11),sk_c10)**. % 0.42/0.60 224[0:Rew:202.0,209.0] || -> equal(multiply(u,identity),u)**. % 0.42/0.60 225[4:Rew:224.0,215.0] || -> equal(inverse(sk_c9),sk_c8)**. % 0.42/0.60 226[3:Rew:224.0,214.0] || -> equal(inverse(sk_c11),sk_c7)**. % 0.42/0.60 229[4:SpR:225.0,66.0] || -> equal(multiply(sk_c8,sk_c9),identity)**. % 0.42/0.60 232[7:Rew:167.0,229.0] || -> equal(sk_c11,identity)**. % 0.42/0.60 233[7:Rew:232.0,155.0] || -> equal(inverse(sk_c7),identity)**. % 0.42/0.60 235[7:Rew:232.0,165.0] || -> equal(multiply(sk_c6,identity),sk_c12)**. % 0.42/0.60 238[7:Rew:232.0,174.0] || -> equal(multiply(identity,sk_c7),identity)**. % 0.42/0.60 239[7:Rew:232.0,197.0] || -> equal(multiply(sk_c12,sk_c12),identity)**. % 0.42/0.60 240[7:Rew:232.0,164.1] || equal(inverse(u),sk_c12) equal(inverse(v),identity) equal(inverse(w),sk_c12) equal(multiply(u,sk_c11),sk_c12)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(w,sk_c12),sk_c11)** -> . % 0.42/0.60 247[7:Rew:232.0,219.0] || -> equal(multiply(identity,identity),sk_c10)**. % 0.42/0.60 249[7:Rew:232.0,226.0] || -> equal(inverse(identity),sk_c7)**. % 0.42/0.60 251[7:Rew:249.0,208.0] || -> equal(multiply(sk_c7,u),u)**. % 0.42/0.60 252[7:Rew:224.0,235.0] || -> equal(sk_c6,sk_c12)**. % 0.42/0.60 253[7:Rew:252.0,153.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.42/0.60 257[7:Rew:65.0,238.0] || -> equal(identity,sk_c7)**. % 0.42/0.60 261[7:Rew:257.0,224.0] || -> equal(multiply(u,sk_c7),u)**. % 0.42/0.60 262[7:Rew:257.0,232.0] || -> equal(sk_c11,sk_c7)**. % 0.42/0.60 263[7:Rew:257.0,233.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.42/0.60 268[7:Rew:257.0,239.0] || -> equal(multiply(sk_c12,sk_c12),sk_c7)**. % 0.42/0.60 269[7:Rew:257.0,247.0] || -> equal(multiply(sk_c7,sk_c7),sk_c10)**. % 0.42/0.60 272[7:Rew:251.0,269.0] || -> equal(sk_c10,sk_c7)**. % 0.42/0.60 296[7:Rew:262.0,240.5,261.0,240.4,262.0,240.4,272.0,240.4,261.0,240.3,262.0,240.3,257.0,240.1] || equal(inverse(u),sk_c12)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c12) equal(u,sk_c12) equal(v,sk_c7) equal(multiply(w,sk_c12),sk_c7)**+ -> . % 0.42/0.60 470[7:SpL:268.0,296.5] || equal(inverse(u),sk_c12)** equal(inverse(v),sk_c7)** equal(inverse(sk_c12),sk_c12)** equal(u,sk_c12) equal(v,sk_c7) equal(sk_c7,sk_c7) -> . % 0.42/0.60 476[7:Obv:470.5] || equal(inverse(u),sk_c12)** equal(inverse(v),sk_c7)** equal(inverse(sk_c12),sk_c12)** equal(u,sk_c12) equal(v,sk_c7) -> . % 0.42/0.60 477[7:Rew:253.0,476.2] || equal(inverse(u),sk_c12)** equal(inverse(v),sk_c7)** equal(sk_c12,sk_c12) equal(u,sk_c12) equal(v,sk_c7) -> . % 0.42/0.60 478[7:Obv:477.2] || equal(inverse(u),sk_c12)**+ equal(inverse(v),sk_c7)** equal(u,sk_c12) equal(v,sk_c7) -> . % 0.42/0.60 1078[7:SpL:253.0,478.0] || equal(sk_c12,sk_c12) equal(inverse(u),sk_c7)** equal(sk_c12,sk_c12) equal(u,sk_c7) -> . % 0.42/0.60 1083[7:Obv:1078.2] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.42/0.60 1086[7:SpL:263.0,1083.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.42/0.60 1091[7:Obv:1086.1] || -> . % 0.42/0.60 1092[7:Spt:1091.0,54.1,167.0] || equal(multiply(sk_c8,sk_c9),sk_c11)** -> . % 0.42/0.60 1093[7:Spt:1091.0,54.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 1094[7:Rew:229.0,1092.0] || equal(sk_c11,identity)** -> . % 0.42/0.60 1095[4:Rew:229.0,33.1] || -> equal(inverse(sk_c3),sk_c12)** equal(sk_c11,identity). % 0.42/0.60 1097[4:Rew:229.0,26.1] || -> equal(inverse(sk_c2),sk_c11)** equal(sk_c11,identity). % 0.42/0.60 1102[4:Rew:229.0,61.0] || -> equal(sk_c11,identity) equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 1104[4:Rew:229.0,47.0] || -> equal(sk_c11,identity) equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 1105[7:MRR:1104.0,1094.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 1106[4:Rew:229.0,40.0] || -> equal(sk_c11,identity) equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 1108[4:Rew:229.0,19.0] || -> equal(sk_c11,identity) equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 1161[2:SpR:173.0,187.0] || -> equal(multiply(inverse(sk_c12),identity),sk_c6)**. % 0.42/0.60 1163[2:Rew:224.0,1161.0] || -> equal(inverse(sk_c12),sk_c6)**. % 0.42/0.60 1169[7:SpR:1105.0,187.0] || -> equal(multiply(inverse(sk_c4),sk_c11),sk_c5)**. % 0.42/0.60 1171[7:Rew:1093.0,1169.0] || -> equal(multiply(sk_c5,sk_c11),sk_c5)**. % 0.42/0.60 1193[7:SpR:1171.0,187.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c11)**. % 0.42/0.60 1195[7:Rew:66.0,1193.0] || -> equal(sk_c11,identity)**. % 0.42/0.60 1196[7:MRR:1195.0,1094.0] || -> . % 0.42/0.60 1197[6:Spt:1196.0,51.1,165.0] || equal(multiply(sk_c6,sk_c11),sk_c12)** -> . % 0.42/0.60 1198[6:Spt:1196.0,51.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 1205[4:Rew:224.0,30.1,1095.1,30.1] || -> equal(inverse(sk_c3),sk_c12)** equal(sk_c6,sk_c12). % 0.42/0.60 1220[4:Rew:224.0,37.0,1106.0,37.0] || -> equal(sk_c6,sk_c12) equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 1234[0:SpR:208.0,224.0] || -> equal(inverse(identity),identity)**. % 0.42/0.60 1241[0:SpR:66.0,187.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.42/0.60 1247[3:SpR:226.0,66.0] || -> equal(multiply(sk_c7,sk_c11),identity)**. % 0.42/0.60 1249[2:SpR:1163.0,66.0] || -> equal(multiply(sk_c6,sk_c12),identity)**. % 0.42/0.60 1250[6:SpR:1198.0,66.0] || -> equal(multiply(sk_c5,sk_c4),identity)**. % 0.42/0.60 1251[0:Rew:224.0,1241.0] || -> equal(inverse(inverse(u)),u)**. % 0.42/0.60 1269[6:SpR:1250.0,187.0] || -> equal(multiply(inverse(sk_c5),identity),sk_c4)**. % 0.42/0.60 1271[6:Rew:224.0,1269.0] || -> equal(inverse(sk_c5),sk_c4)**. % 0.42/0.60 1273[7:Spt:1095.1] || -> equal(sk_c11,identity)**. % 0.42/0.60 1275[7:Rew:1273.0,226.0] || -> equal(inverse(identity),sk_c7)**. % 0.42/0.60 1279[7:Rew:1273.0,1197.0] || equal(multiply(sk_c6,identity),sk_c12)** -> . % 0.42/0.60 1292[7:Rew:1273.0,1220.1] || -> equal(sk_c6,sk_c12) equal(multiply(sk_c3,identity),sk_c12)**. % 0.42/0.60 1298[7:Rew:1234.0,1275.0] || -> equal(identity,sk_c7)**. % 0.42/0.60 1303[7:Rew:1298.0,224.0] || -> equal(multiply(u,sk_c7),u)**. % 0.42/0.60 1317[7:Rew:1303.0,1279.0,1298.0,1279.0] || equal(sk_c6,sk_c12)** -> . % 0.42/0.60 1318[7:MRR:1205.1,1317.0] || -> equal(inverse(sk_c3),sk_c12)**. % 0.42/0.60 1335[7:Rew:1303.0,1292.1,1298.0,1292.1] || -> equal(sk_c6,sk_c12) equal(sk_c3,sk_c12)**. % 0.42/0.60 1336[7:MRR:1335.0,1317.0] || -> equal(sk_c3,sk_c12)**. % 0.42/0.60 1337[7:Rew:1336.0,1318.0] || -> equal(inverse(sk_c12),sk_c12)**. % 0.42/0.60 1338[7:Rew:1163.0,1337.0] || -> equal(sk_c6,sk_c12)**. % 0.42/0.60 1339[7:MRR:1338.0,1317.0] || -> . % 0.42/0.60 1369[7:Spt:1339.0,1095.1,1273.0] || equal(sk_c11,identity)** -> . % 0.42/0.60 1370[7:Spt:1339.0,1095.0] || -> equal(inverse(sk_c3),sk_c12)**. % 0.42/0.60 1373[7:MRR:1102.0,1369.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 1374[7:MRR:1104.0,1369.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 1389[6:SpR:1271.0,187.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),u)**. % 0.42/0.60 1441[7:SpR:1374.0,67.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c11,u))**. % 0.42/0.60 1442[7:SpR:1374.0,187.0] || -> equal(multiply(inverse(sk_c4),sk_c11),sk_c5)**. % 0.42/0.60 1444[7:Rew:1198.0,1442.0] || -> equal(multiply(sk_c5,sk_c11),sk_c5)**. % 0.42/0.60 1445[7:Rew:1389.0,1441.0] || -> equal(multiply(sk_c11,u),u)**. % 0.42/0.60 1446[7:Rew:1445.0,174.0] || -> equal(identity,sk_c7)**. % 0.42/0.60 1447[7:Rew:1445.0,219.0] || -> equal(sk_c11,sk_c10)**. % 0.42/0.60 1455[7:Rew:1446.0,1369.0] || equal(sk_c11,sk_c7)** -> . % 0.42/0.60 1457[7:Rew:1446.0,1250.0] || -> equal(multiply(sk_c5,sk_c4),sk_c7)**. % 0.42/0.60 1461[7:Rew:1446.0,224.0] || -> equal(multiply(u,sk_c7),u)**. % 0.42/0.60 1465[7:Rew:1447.0,226.0] || -> equal(inverse(sk_c10),sk_c7)**. % 0.42/0.60 1469[7:Rew:1447.0,1373.0] || -> equal(multiply(sk_c5,sk_c10),sk_c10)**. % 0.42/0.60 1477[7:Rew:1447.0,1444.0] || -> equal(multiply(sk_c5,sk_c10),sk_c5)**. % 0.42/0.60 1479[7:Rew:1447.0,1455.0] || equal(sk_c10,sk_c7)** -> . % 0.42/0.60 1484[7:Rew:1469.0,1477.0] || -> equal(sk_c5,sk_c10)**. % 0.42/0.60 1486[7:Rew:1484.0,1271.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.42/0.60 1489[7:Rew:1484.0,1457.0] || -> equal(multiply(sk_c10,sk_c4),sk_c7)**. % 0.42/0.60 1492[7:Rew:1465.0,1486.0] || -> equal(sk_c4,sk_c7)**. % 0.42/0.60 1497[7:Rew:1461.0,1489.0,1492.0,1489.0] || -> equal(sk_c10,sk_c7)**. % 0.42/0.60 1498[7:MRR:1497.0,1479.0] || -> . % 0.42/0.60 1506[5:Spt:1498.0,53.1,159.0] || equal(multiply(sk_c7,sk_c10),sk_c11)** -> . % 0.42/0.60 1507[5:Spt:1498.0,53.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 1509[4:Rew:1097.1,25.1] || -> equal(inverse(sk_c2),sk_c11) equal(multiply(sk_c7,sk_c10),identity)**. % 0.42/0.60 1514[4:Rew:1108.0,18.0] || -> equal(multiply(sk_c7,sk_c10),identity) equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 1559[0:SpR:1251.0,187.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.42/0.60 1566[5:SpR:1507.0,1251.0] || -> equal(inverse(sk_c5),sk_c4)**. % 0.42/0.60 1593[5:SpR:1566.0,66.0] || -> equal(multiply(sk_c4,sk_c5),identity)**. % 0.42/0.60 1597[5:Rew:1593.0,1104.1] || -> equal(sk_c11,identity)** equal(sk_c11,identity)**. % 0.42/0.60 1603[5:Obv:1597.0] || -> equal(sk_c11,identity)**. % 0.42/0.60 1605[5:Rew:1603.0,226.0] || -> equal(inverse(identity),sk_c7)**. % 0.42/0.60 1608[5:Rew:1603.0,1506.0] || equal(multiply(sk_c7,sk_c10),identity)** -> . % 0.42/0.60 1609[5:Rew:1603.0,1509.0] || -> equal(inverse(sk_c2),identity) equal(multiply(sk_c7,sk_c10),identity)**. % 0.42/0.60 1617[5:Rew:1603.0,1514.1] || -> equal(multiply(sk_c7,sk_c10),identity) equal(multiply(sk_c2,identity),sk_c10)**. % 0.42/0.60 1622[5:Rew:1234.0,1605.0] || -> equal(identity,sk_c7)**. % 0.42/0.60 1623[5:Rew:1622.0,1234.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.42/0.60 1624[5:Rew:1622.0,65.0] || -> equal(multiply(sk_c7,u),u)**. % 0.42/0.60 1629[5:Rew:1622.0,224.0] || -> equal(multiply(u,sk_c7),u)**. % 0.42/0.60 1642[5:Rew:1624.0,1608.0,1622.0,1608.0] || equal(sk_c10,sk_c7)** -> . % 0.42/0.60 1661[5:Rew:1624.0,1609.1,1622.0,1609.1,1622.0,1609.0] || -> equal(inverse(sk_c2),sk_c7)** equal(sk_c10,sk_c7). % 0.42/0.60 1662[5:MRR:1661.1,1642.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.42/0.60 1677[5:Rew:1629.0,1617.1,1622.0,1617.1,1624.0,1617.0,1622.0,1617.0] || -> equal(sk_c10,sk_c7) equal(sk_c2,sk_c10)**. % 0.42/0.60 1678[5:MRR:1677.0,1642.0] || -> equal(sk_c2,sk_c10)**. % 0.42/0.60 1679[5:Rew:1678.0,1662.0] || -> equal(inverse(sk_c10),sk_c7)**. % 0.42/0.60 1715[5:SpR:1679.0,1251.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.42/0.60 1717[5:Rew:1623.0,1715.0] || -> equal(sk_c10,sk_c7)**. % 0.42/0.60 1718[5:MRR:1717.0,1642.0] || -> . % 0.42/0.60 1720[4:Spt:1718.0,34.0,157.0] || equal(inverse(sk_c8),sk_c9)** -> . % 0.42/0.60 1721[4:Spt:1718.0,34.1] || -> equal(inverse(sk_c3),sk_c12)**. % 0.42/0.60 1723[4:MRR:27.0,1720.0] || -> equal(inverse(sk_c2),sk_c11)**. % 0.42/0.60 1724[4:MRR:13.0,1720.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.42/0.60 1726[4:MRR:62.0,1720.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.42/0.60 1728[4:MRR:41.0,1720.0] || -> equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 1729[4:MRR:20.0,1720.0] || -> equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 1730[4:MRR:6.0,1720.0] || -> equal(multiply(sk_c1,sk_c12),sk_c11)**. % 0.42/0.60 1733[4:SpR:1721.0,1251.0] || -> equal(inverse(sk_c12),sk_c3)**. % 0.42/0.60 1735[4:Rew:1163.0,1733.0] || -> equal(sk_c3,sk_c6)**. % 0.42/0.60 1737[4:Rew:1735.0,1728.0] || -> equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.42/0.60 1741[4:SpR:1723.0,1251.0] || -> equal(inverse(sk_c11),sk_c2)**. % 0.42/0.60 1743[4:Rew:226.0,1741.0] || -> equal(sk_c2,sk_c7)**. % 0.42/0.60 1745[4:Rew:1743.0,1729.0] || -> equal(multiply(sk_c7,sk_c11),sk_c10)**. % 0.42/0.60 1746[4:Rew:1247.0,1745.0] || -> equal(identity,sk_c10)**. % 0.42/0.60 1747[4:Rew:1746.0,1234.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.42/0.60 1750[4:Rew:1746.0,224.0] || -> equal(multiply(u,sk_c10),u)**. % 0.42/0.60 1751[4:Rew:1746.0,1249.0] || -> equal(multiply(sk_c6,sk_c12),sk_c10)**. % 0.42/0.60 1752[4:Rew:1746.0,173.0] || -> equal(multiply(sk_c12,sk_c6),sk_c10)**. % 0.42/0.60 1756[4:Rew:1750.0,1726.0] || -> equal(sk_c11,sk_c5)**. % 0.42/0.60 1757[4:Rew:1750.0,152.4] || equal(inverse(u),sk_c11)** equal(inverse(v),sk_c12) equal(inverse(w),sk_c11) equal(inverse(x),sk_c12) equal(u,sk_c11) equal(multiply(v,sk_c11),sk_c12)** equal(multiply(w,sk_c11),sk_c10)** equal(multiply(x,sk_c12),sk_c11)** -> . % 0.42/0.60 1758[4:Rew:1756.0,226.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.42/0.60 1759[4:Rew:1756.0,155.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.42/0.60 1763[4:Rew:1756.0,1730.0] || -> equal(multiply(sk_c1,sk_c12),sk_c5)**. % 0.42/0.60 1764[4:Rew:1756.0,1737.0] || -> equal(multiply(sk_c6,sk_c5),sk_c12)**. % 0.42/0.60 1768[4:Rew:1756.0,1757.7,1756.0,1757.6,1756.0,1757.5,1756.0,1757.4,1756.0,1757.2,1756.0,1757.0] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c12) equal(inverse(w),sk_c5) equal(inverse(x),sk_c12) equal(u,sk_c5) equal(multiply(v,sk_c5),sk_c12)** equal(multiply(w,sk_c5),sk_c10)** equal(multiply(x,sk_c12),sk_c5)** -> . % 0.42/0.60 1776[4:SpR:1724.0,1251.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.42/0.60 1778[4:Rew:1163.0,1776.0] || -> equal(sk_c6,sk_c1)**. % 0.42/0.60 1784[4:Rew:1778.0,1751.0] || -> equal(multiply(sk_c1,sk_c12),sk_c10)**. % 0.42/0.60 1785[4:Rew:1778.0,1752.0] || -> equal(multiply(sk_c12,sk_c1),sk_c10)**. % 0.42/0.60 1786[4:Rew:1778.0,1764.0] || -> equal(multiply(sk_c1,sk_c5),sk_c12)**. % 0.42/0.60 1787[4:Rew:1763.0,1784.0] || -> equal(sk_c5,sk_c10)**. % 0.42/0.60 1790[4:Rew:1787.0,1758.0] || -> equal(inverse(sk_c10),sk_c7)**. % 0.42/0.60 1791[4:Rew:1787.0,1759.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.42/0.60 1798[4:Rew:1787.0,1768.0] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c12) equal(inverse(w),sk_c5) equal(inverse(x),sk_c12) equal(u,sk_c5) equal(multiply(v,sk_c5),sk_c12)** equal(multiply(w,sk_c5),sk_c10)** equal(multiply(x,sk_c12),sk_c5)** -> . % 0.42/0.60 1799[4:Rew:1747.0,1790.0] || -> equal(sk_c10,sk_c7)**. % 0.42/0.60 1802[4:Rew:1799.0,1750.0] || -> equal(multiply(u,sk_c7),u)**. % 0.42/0.60 1806[4:Rew:1799.0,1787.0] || -> equal(sk_c5,sk_c7)**. % 0.42/0.60 1809[4:Rew:1799.0,1791.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.42/0.60 1810[4:Rew:1799.0,1785.0] || -> equal(multiply(sk_c12,sk_c1),sk_c7)**. % 0.42/0.60 1811[4:Rew:1806.0,1786.0] || -> equal(multiply(sk_c1,sk_c7),sk_c12)**. % 0.42/0.60 1817[4:Rew:1802.0,1811.0] || -> equal(sk_c12,sk_c1)**. % 0.42/0.60 1819[4:Rew:1817.0,1724.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.42/0.60 1821[4:Rew:1817.0,1810.0] || -> equal(multiply(sk_c1,sk_c1),sk_c7)**. % 0.42/0.60 1828[4:Rew:1817.0,1798.7,1806.0,1798.7,1802.0,1798.6,1806.0,1798.6,1799.0,1798.6,1802.0,1798.5,1806.0,1798.5,1817.0,1798.5,1806.0,1798.4,1817.0,1798.3,1806.0,1798.2,1817.0,1798.1,1799.0,1798.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c1)** equal(inverse(w),sk_c7)** equal(inverse(x),sk_c1) equal(u,sk_c7) equal(v,sk_c1) equal(w,sk_c7) equal(multiply(x,sk_c1),sk_c7)** -> . % 0.42/0.60 1829[4:Con:1828.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1) equal(u,sk_c7) equal(v,sk_c1) equal(multiply(w,sk_c1),sk_c7)**+ -> . % 0.42/0.60 1956[4:SpL:1821.0,1829.5] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c1)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c7) equal(v,sk_c1) equal(sk_c7,sk_c7) -> . % 0.42/0.60 1962[4:Obv:1956.5] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c1)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c7) equal(v,sk_c1) -> . % 0.42/0.60 1963[4:Rew:1819.0,1962.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c1)** equal(sk_c1,sk_c1) equal(u,sk_c7) equal(v,sk_c1) -> . % 0.42/0.60 1964[4:Obv:1963.2] || equal(inverse(u),sk_c7)**+ equal(inverse(v),sk_c1)** equal(u,sk_c7) equal(v,sk_c1) -> . % 0.42/0.60 2491[4:SpL:1809.0,1964.0] || equal(sk_c7,sk_c7) equal(inverse(u),sk_c1)** equal(sk_c7,sk_c7) equal(u,sk_c1) -> . % 0.42/0.60 2495[4:Obv:2491.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.42/0.60 2499[4:SpL:1819.0,2495.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.42/0.60 2503[4:Obv:2499.1] || -> . % 0.42/0.60 2504[3:Spt:2503.0,52.0,155.0] || equal(inverse(sk_c7),sk_c11)** -> . % 0.42/0.60 2505[3:Spt:2503.0,52.1] || -> equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 2506[3:MRR:31.0,2504.0] || -> equal(inverse(sk_c3),sk_c12)**. % 0.42/0.60 2507[3:MRR:24.0,2504.0] || -> equal(inverse(sk_c2),sk_c11)**. % 0.42/0.60 2508[3:MRR:10.0,2504.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.42/0.60 2513[3:MRR:38.0,2504.0] || -> equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 2514[3:MRR:17.0,2504.0] || -> equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 2515[3:MRR:3.0,2504.0] || -> equal(multiply(sk_c1,sk_c12),sk_c11)**. % 0.42/0.60 2541[3:SpR:2506.0,1251.0] || -> equal(inverse(sk_c12),sk_c3)**. % 0.42/0.60 2544[3:Rew:1163.0,2541.0] || -> equal(sk_c3,sk_c6)**. % 0.42/0.60 2546[3:Rew:2544.0,2513.0] || -> equal(multiply(sk_c6,sk_c11),sk_c12)**. % 0.42/0.60 2551[3:SpR:2507.0,1251.0] || -> equal(inverse(sk_c11),sk_c2)**. % 0.42/0.60 2555[3:SpR:2508.0,1251.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.42/0.60 2558[3:Rew:1163.0,2555.0] || -> equal(sk_c6,sk_c1)**. % 0.42/0.60 2563[3:Rew:2558.0,1249.0] || -> equal(multiply(sk_c1,sk_c12),identity)**. % 0.42/0.60 2566[3:Rew:2558.0,2546.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.42/0.60 2567[3:Rew:2515.0,2563.0] || -> equal(sk_c11,identity)**. % 0.42/0.60 2572[3:Rew:2567.0,2514.0] || -> equal(multiply(sk_c2,identity),sk_c10)**. % 0.42/0.60 2573[3:Rew:2567.0,2515.0] || -> equal(multiply(sk_c1,sk_c12),identity)**. % 0.42/0.60 2574[3:Rew:2567.0,152.0] || equal(inverse(u),identity) equal(inverse(v),sk_c12) equal(inverse(w),sk_c11) equal(inverse(x),sk_c12) equal(multiply(u,sk_c10),sk_c11)** equal(multiply(v,sk_c11),sk_c12)** equal(multiply(w,sk_c11),sk_c10)** equal(multiply(x,sk_c12),sk_c11)** -> . % 0.42/0.60 2575[3:Rew:2567.0,2551.0] || -> equal(inverse(identity),sk_c2)**. % 0.42/0.60 2578[3:Rew:1234.0,2575.0] || -> equal(identity,sk_c2)**. % 0.42/0.60 2579[3:Rew:2578.0,1234.0] || -> equal(inverse(sk_c2),sk_c2)**. % 0.42/0.60 2580[3:Rew:2578.0,65.0] || -> equal(multiply(sk_c2,u),u)**. % 0.42/0.60 2581[3:Rew:2578.0,224.0] || -> equal(multiply(u,sk_c2),u)**. % 0.42/0.60 2585[3:Rew:2578.0,2567.0] || -> equal(sk_c11,sk_c2)**. % 0.42/0.60 2587[3:Rew:2585.0,2566.0] || -> equal(multiply(sk_c1,sk_c2),sk_c12)**. % 0.42/0.60 2591[3:Rew:2578.0,2572.0] || -> equal(multiply(sk_c2,sk_c2),sk_c10)**. % 0.42/0.60 2592[3:Rew:2578.0,2573.0] || -> equal(multiply(sk_c1,sk_c12),sk_c2)**. % 0.42/0.60 2593[3:Rew:2580.0,2591.0] || -> equal(sk_c2,sk_c10)**. % 0.42/0.60 2594[3:Rew:2593.0,2578.0] || -> equal(identity,sk_c10)**. % 0.42/0.60 2595[3:Rew:2593.0,2585.0] || -> equal(sk_c11,sk_c10)**. % 0.42/0.60 2596[3:Rew:2593.0,2579.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.42/0.60 2597[3:Rew:2593.0,2587.0] || -> equal(multiply(sk_c1,sk_c10),sk_c12)**. % 0.42/0.60 2601[3:Rew:2593.0,2592.0] || -> equal(multiply(sk_c1,sk_c12),sk_c10)**. % 0.42/0.60 2603[3:Rew:2593.0,2581.0] || -> equal(multiply(u,sk_c10),u)**. % 0.42/0.60 2605[3:Rew:2603.0,2597.0] || -> equal(sk_c12,sk_c1)**. % 0.42/0.60 2606[3:Rew:2605.0,2508.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.42/0.60 2617[3:Rew:2605.0,2601.0] || -> equal(multiply(sk_c1,sk_c1),sk_c10)**. % 0.42/0.60 2628[3:Rew:2605.0,2574.7,2595.0,2574.7,2603.0,2574.6,2595.0,2574.6,2603.0,2574.5,2595.0,2574.5,2605.0,2574.5,2603.0,2574.4,2595.0,2574.4,2605.0,2574.3,2595.0,2574.2,2605.0,2574.1,2594.0,2574.0] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(inverse(w),sk_c10)** equal(inverse(x),sk_c1) equal(u,sk_c10) equal(v,sk_c1) equal(w,sk_c10) equal(multiply(x,sk_c1),sk_c10)** -> . % 0.42/0.60 2629[3:Con:2628.2] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1) equal(u,sk_c10) equal(v,sk_c1) equal(multiply(w,sk_c1),sk_c10)**+ -> . % 0.42/0.60 2690[3:SpL:2617.0,2629.5] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c10) equal(v,sk_c1) equal(sk_c10,sk_c10) -> . % 0.42/0.60 2695[3:Obv:2690.5] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c10) equal(v,sk_c1) -> . % 0.42/0.60 2696[3:Rew:2606.0,2695.2] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(sk_c1,sk_c1) equal(u,sk_c10) equal(v,sk_c1) -> . % 0.42/0.60 2697[3:Obv:2696.2] || equal(inverse(u),sk_c10)**+ equal(inverse(v),sk_c1)** equal(u,sk_c10) equal(v,sk_c1) -> . % 0.42/0.60 2886[3:SpL:2596.0,2697.0] || equal(sk_c10,sk_c10) equal(inverse(u),sk_c1)** equal(sk_c10,sk_c10) equal(u,sk_c1) -> . % 0.42/0.60 2888[3:Obv:2886.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.42/0.60 2892[3:SpL:2606.0,2888.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.42/0.60 2894[3:Obv:2892.1] || -> . % 0.42/0.60 2895[2:Spt:2894.0,50.0,153.0] || equal(inverse(sk_c6),sk_c12)** -> . % 0.42/0.60 2896[2:Spt:2894.0,50.1] || -> equal(inverse(sk_c4),sk_c5)**. % 0.42/0.60 2897[2:MRR:29.0,2895.0] || -> equal(inverse(sk_c3),sk_c12)**. % 0.42/0.60 2898[2:MRR:22.0,2895.0] || -> equal(inverse(sk_c2),sk_c11)**. % 0.42/0.60 2899[2:MRR:8.0,2895.0] || -> equal(inverse(sk_c1),sk_c12)**. % 0.42/0.60 2901[2:MRR:43.0,2895.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.42/0.60 2902[2:MRR:36.0,2895.0] || -> equal(multiply(sk_c3,sk_c11),sk_c12)**. % 0.42/0.60 2903[2:MRR:15.0,2895.0] || -> equal(multiply(sk_c2,sk_c11),sk_c10)**. % 0.42/0.60 2904[2:MRR:1.0,2895.0] || -> equal(multiply(sk_c1,sk_c12),sk_c11)**. % 0.42/0.60 2907[2:SpR:2896.0,1559.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),u)**. % 0.42/0.60 2916[2:SpR:2897.0,1251.0] || -> equal(inverse(sk_c12),sk_c3)**. % 0.42/0.60 2919[2:SpR:2898.0,187.0] || -> equal(multiply(sk_c11,multiply(sk_c2,u)),u)**. % 0.42/0.60 2924[2:SpR:2899.0,1251.0] || -> equal(inverse(sk_c12),sk_c1)**. % 0.42/0.60 2927[2:Rew:2916.0,2924.0] || -> equal(sk_c3,sk_c1)**. % 0.42/0.60 2929[2:Rew:2927.0,2902.0] || -> equal(multiply(sk_c1,sk_c11),sk_c12)**. % 0.42/0.60 2950[2:SpR:2901.0,67.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c11,u))**. % 0.42/0.60 2954[2:Rew:2907.0,2950.0] || -> equal(multiply(sk_c11,u),u)**. % 0.42/0.60 2955[2:Rew:2954.0,2919.0] || -> equal(multiply(sk_c2,u),u)**. % 0.42/0.60 2958[2:Rew:2955.0,2903.0] || -> equal(sk_c11,sk_c10)**. % 0.42/0.60 2959[2:Rew:2958.0,2898.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.42/0.60 2963[2:Rew:2958.0,2904.0] || -> equal(multiply(sk_c1,sk_c12),sk_c10)**. % 0.42/0.60 2964[2:Rew:2958.0,152.0] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c12) equal(inverse(w),sk_c11) equal(inverse(x),sk_c12) equal(multiply(u,sk_c10),sk_c11)** equal(multiply(v,sk_c11),sk_c12)** equal(multiply(w,sk_c11),sk_c10)** equal(multiply(x,sk_c12),sk_c11)** -> . % 0.42/0.60 2965[2:Rew:2958.0,2929.0] || -> equal(multiply(sk_c1,sk_c10),sk_c12)**. % 0.42/0.60 2983[2:Rew:2958.0,2964.7,2958.0,2964.6,2958.0,2964.5,2958.0,2964.4,2958.0,2964.2] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c12) equal(inverse(w),sk_c10) equal(inverse(x),sk_c12) equal(multiply(u,sk_c10),sk_c10)** equal(multiply(v,sk_c10),sk_c12)** equal(multiply(w,sk_c10),sk_c10)** equal(multiply(x,sk_c12),sk_c10)** -> . % 0.42/0.60 2984[2:Con:2983.2] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c12) equal(inverse(w),sk_c12) equal(multiply(u,sk_c10),sk_c10)** equal(multiply(v,sk_c10),sk_c12)** equal(multiply(w,sk_c12),sk_c10)** -> . % 0.42/0.60 3031[2:SpR:2955.0,224.0] || -> equal(identity,sk_c2)**. % 0.42/0.60 3033[2:Rew:3031.0,1234.0] || -> equal(inverse(sk_c2),sk_c2)**. % 0.42/0.60 3035[2:Rew:3031.0,224.0] || -> equal(multiply(u,sk_c2),u)**. % 0.42/0.60 3038[2:Rew:2959.0,3033.0] || -> equal(sk_c2,sk_c10)**. % 0.42/0.60 3039[2:Rew:3038.0,2959.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.42/0.60 3045[2:Rew:3038.0,3035.0] || -> equal(multiply(u,sk_c10),u)**. % 0.42/0.60 3046[2:Rew:3045.0,2965.0] || -> equal(sk_c12,sk_c1)**. % 0.42/0.60 3047[2:Rew:3045.0,2984.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c12)** equal(inverse(w),sk_c12) equal(multiply(u,sk_c10),sk_c10)** equal(v,sk_c12) equal(multiply(w,sk_c12),sk_c10)** -> . % 0.42/0.60 3048[2:Rew:3046.0,2899.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.42/0.60 3051[2:Rew:3046.0,2963.0] || -> equal(multiply(sk_c1,sk_c1),sk_c10)**. % 0.42/0.60 3058[2:Rew:3046.0,3047.5,3046.0,3047.4,3045.0,3047.3,3046.0,3047.2,3046.0,3047.1] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(inverse(w),sk_c1) equal(u,sk_c10) equal(v,sk_c1) equal(multiply(w,sk_c1),sk_c10)**+ -> . % 0.42/0.60 3115[2:SpL:3051.0,3058.5] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c10) equal(v,sk_c1) equal(sk_c10,sk_c10) -> . % 0.42/0.60 3120[2:Obv:3115.5] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c10) equal(v,sk_c1) -> . % 0.42/0.60 3121[2:Rew:3048.0,3120.2] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c1)** equal(sk_c1,sk_c1) equal(u,sk_c10) equal(v,sk_c1) -> . % 0.42/0.60 3122[2:Obv:3121.2] || equal(inverse(u),sk_c10)**+ equal(inverse(v),sk_c1)** equal(u,sk_c10) equal(v,sk_c1) -> . % 0.42/0.60 3311[2:SpL:3039.0,3122.0] || equal(sk_c10,sk_c10) equal(inverse(u),sk_c1)** equal(sk_c10,sk_c10) equal(u,sk_c1) -> . % 0.42/0.60 3313[2:Obv:3311.2] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.42/0.60 3317[2:SpL:3048.0,3313.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.42/0.60 3319[2:Obv:3317.1] || -> . % 0.42/0.60 % SZS output end Refutation % 0.42/0.60 Formulae used in the proof : prove_this_1 prove_this_3 prove_this_6 prove_this_8 prove_this_10 prove_this_13 prove_this_15 prove_this_17 prove_this_18 prove_this_19 prove_this_20 prove_this_22 prove_this_24 prove_this_25 prove_this_26 prove_this_27 prove_this_29 prove_this_30 prove_this_31 prove_this_33 prove_this_34 prove_this_36 prove_this_37 prove_this_38 prove_this_40 prove_this_41 prove_this_43 prove_this_47 prove_this_48 prove_this_49 prove_this_50 prove_this_51 prove_this_52 prove_this_53 prove_this_54 prove_this_55 prove_this_56 prove_this_61 prove_this_62 prove_this_63 prove_this_64 left_identity left_inverse associativity % 0.42/0.62 %------------------------------------------------------------------------------