%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP310-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:47 EDT 2022 % Result : Unsatisfiable 0.18s 0.47s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP310-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n007.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jun 13 10:31:09 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.47 % 0.18/0.47 SPASS V 3.9 % 0.18/0.47 SPASS beiseite: Proof found. % 0.18/0.47 % SZS status Theorem % 0.18/0.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.47 SPASS derived 765 clauses, backtracked 462 clauses, performed 13 splits and kept 812 clauses. % 0.18/0.47 SPASS allocated 63592 KBytes. % 0.18/0.47 SPASS spent 0:00:00.13 on the problem. % 0.18/0.47 0:00:00.04 for the input. % 0.18/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.18/0.47 0:00:00.00 for inferences. % 0.18/0.47 0:00:00.00 for the backtracking. % 0.18/0.47 0:00:00.06 for the reduction. % 0.18/0.47 % 0.18/0.47 % 0.18/0.47 Here is a proof with depth 4, length 406 : % 0.18/0.47 % SZS output start Refutation % 0.18/0.47 1[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.18/0.47 2[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.47 3[0:Inp] || -> equal(inverse(sk_c3),sk_c8)** equal(inverse(sk_c8),sk_c6). % 0.18/0.47 4[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.47 5[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.47 6[0:Inp] || -> equal(inverse(sk_c4),sk_c8)** equal(inverse(sk_c8),sk_c6). % 0.18/0.47 7[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c8). % 0.18/0.47 8[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 9[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 10[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5)** equal(multiply(sk_c6,sk_c7),sk_c8). % 0.18/0.47 11[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 12[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c8,sk_c2),sk_c7). % 0.18/0.47 13[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 14[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 15[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5)** equal(multiply(sk_c8,sk_c2),sk_c7). % 0.18/0.47 16[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 17[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 18[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 19[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 20[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 21[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 22[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.47 23[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c1),sk_c8)**. % 0.18/0.47 24[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.47 25[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.47 26[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c1),sk_c8)**. % 0.18/0.47 27[0:Inp] || equal(multiply(sk_c8,sk_c7),sk_c6) equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c8)** equal(multiply(sk_c8,u),sk_c7)** equal(multiply(v,sk_c8),u)* equal(inverse(v),sk_c8) equal(multiply(w,sk_c8),sk_c7)** equal(inverse(w),sk_c8) equal(multiply(sk_c8,x),sk_c7)** equal(multiply(y,sk_c8),x)* equal(inverse(y),sk_c8) -> . % 0.18/0.47 28[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.18/0.47 29[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.18/0.47 30[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.18/0.47 31[0:Con:27.8] || equal(multiply(sk_c8,sk_c7),sk_c6) equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c8)** equal(multiply(sk_c8,u),sk_c7)** equal(multiply(v,sk_c8),u)* equal(inverse(v),sk_c8) equal(multiply(w,sk_c8),sk_c7)** equal(inverse(w),sk_c8) -> . % 0.18/0.47 32[0:Rew:1.0,31.0] || equal(sk_c6,sk_c6) equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c8)** equal(multiply(sk_c8,u),sk_c7)** equal(multiply(v,sk_c8),u)* equal(inverse(v),sk_c8) equal(multiply(w,sk_c8),sk_c7)** equal(inverse(w),sk_c8) -> . % 0.18/0.47 33[0:Obv:32.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(sk_c8),sk_c6) equal(multiply(v,sk_c8),w)*+ equal(multiply(u,sk_c8),sk_c7)** equal(multiply(sk_c8,w),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.18/0.47 34[1:Spt:33.1,33.3,33.5] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),v)*+ equal(multiply(sk_c8,v),sk_c7)** -> . % 0.18/0.47 36[2:Spt:6.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.47 38[3:Spt:3.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.47 40[4:Spt:5.1] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.47 46[5:Spt:4.1] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.47 48[6:Spt:2.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.47 54[1:SpL:28.0,34.1] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.18/0.47 56[2:SpR:36.0,29.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.18/0.47 57[3:SpR:38.0,29.0] || -> equal(multiply(sk_c8,sk_c3),identity)**. % 0.18/0.47 58[1:SpL:29.0,34.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.18/0.47 64[0:SpR:1.0,30.0] || -> equal(multiply(sk_c8,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.18/0.47 66[2:SpR:56.0,30.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),multiply(identity,u))**. % 0.18/0.47 68[0:SpR:29.0,30.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.18/0.47 70[2:Rew:28.0,66.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),u)**. % 0.18/0.47 71[0:Rew:28.0,68.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.18/0.47 74[3:SpR:57.0,30.0] || -> equal(multiply(sk_c8,multiply(sk_c3,u)),multiply(identity,u))**. % 0.18/0.47 75[3:Rew:28.0,74.0] || -> equal(multiply(sk_c8,multiply(sk_c3,u)),u)**. % 0.18/0.47 78[4:SpR:40.0,70.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.47 79[5:Rew:46.0,78.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 82[5:Rew:79.0,46.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.18/0.47 83[6:Rew:79.0,48.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.18/0.47 85[5:Rew:79.0,58.2] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.47 113[0:SpR:71.0,71.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.18/0.47 117[2:SpR:56.0,71.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c4)**. % 0.18/0.47 118[3:SpR:57.0,71.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c3)**. % 0.18/0.47 121[5:SpR:82.0,71.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c5)**. % 0.18/0.47 124[0:SpR:29.0,71.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.47 130[3:Rew:117.0,118.0] || -> equal(sk_c4,sk_c3)**. % 0.18/0.47 132[4:Rew:130.0,40.0] || -> equal(multiply(sk_c3,sk_c8),sk_c5)**. % 0.18/0.47 136[3:Rew:130.0,117.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c3)**. % 0.18/0.47 137[6:Rew:83.0,132.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.47 141[5:Rew:29.0,121.0] || -> equal(identity,sk_c5)**. % 0.18/0.47 142[6:Rew:137.0,141.0] || -> equal(identity,sk_c8)**. % 0.18/0.47 143[6:Rew:142.0,28.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.47 145[6:Rew:142.0,57.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.18/0.47 146[6:Rew:142.0,85.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.47 153[6:Rew:143.0,145.0] || -> equal(sk_c3,sk_c8)**. % 0.18/0.47 154[6:Rew:153.0,38.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.47 178[6:Rew:143.0,146.2,154.0,146.0,154.0,146.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.47 179[6:Obv:178.1] || equal(u,sk_c8)* -> . % 0.18/0.47 180[6:UnC:179.0,71.0] || -> . % 0.18/0.47 182[6:Spt:180.0,2.1,48.0] || equal(multiply(sk_c3,sk_c8),sk_c7)** -> . % 0.18/0.47 183[6:Spt:180.0,2.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.18/0.47 186[6:Rew:183.0,121.0] || -> equal(multiply(sk_c6,sk_c8),sk_c5)**. % 0.18/0.47 189[6:Rew:183.0,136.0,141.0,136.0] || -> equal(multiply(sk_c6,sk_c5),sk_c3)**. % 0.18/0.47 190[6:Rew:79.0,182.0] || equal(multiply(sk_c3,sk_c8),sk_c8)** -> . % 0.18/0.47 191[6:Rew:132.0,190.0] || equal(sk_c5,sk_c8)** -> . % 0.18/0.47 192[5:Rew:113.0,124.0,141.0,124.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.47 193[6:Rew:192.0,189.0] || -> equal(sk_c3,sk_c6)**. % 0.18/0.47 215[5:Rew:79.0,7.1,79.0,7.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)** equal(multiply(sk_c6,sk_c8),sk_c8). % 0.18/0.47 216[6:Rew:186.0,215.1,186.0,215.0,193.0,215.0] || -> equal(sk_c5,sk_c8)** equal(sk_c5,sk_c8)**. % 0.18/0.47 217[6:Obv:216.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.47 218[6:MRR:217.0,191.0] || -> . % 0.18/0.47 222[5:Spt:218.0,4.1,46.0] || equal(multiply(sk_c8,sk_c5),sk_c7)** -> . % 0.18/0.47 223[5:Spt:218.0,4.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.18/0.47 226[5:Rew:78.0,222.0] || equal(sk_c7,sk_c8)** -> . % 0.18/0.47 228[0:Rew:113.0,124.0] || -> equal(multiply(u,identity),u)**. % 0.18/0.47 239[4:Rew:78.0,24.1] || -> equal(inverse(sk_c1),sk_c8)** equal(sk_c7,sk_c8). % 0.18/0.47 240[5:MRR:239.1,226.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.18/0.47 244[4:Rew:78.0,19.0] || -> equal(sk_c7,sk_c8) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 245[5:MRR:244.0,226.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 246[4:Rew:78.0,14.0] || -> equal(sk_c7,sk_c8) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 247[5:MRR:246.0,226.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 268[0:SpR:1.0,71.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.18/0.47 282[5:SpR:245.0,71.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c8)**. % 0.18/0.47 284[5:Rew:240.0,282.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.18/0.47 285[5:Rew:247.0,284.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 286[5:MRR:285.0,226.0] || -> . % 0.18/0.47 287[4:Spt:286.0,5.1,40.0] || equal(multiply(sk_c4,sk_c8),sk_c5)** -> . % 0.18/0.47 288[4:Spt:286.0,5.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.18/0.47 289[4:Rew:228.0,136.0,288.0,136.0] || -> equal(sk_c3,sk_c6)**. % 0.18/0.47 290[4:Rew:289.0,130.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.47 294[4:Rew:290.0,287.0] || equal(multiply(sk_c6,sk_c8),sk_c5)** -> . % 0.18/0.47 295[4:Rew:289.0,75.0] || -> equal(multiply(sk_c8,multiply(sk_c6,u)),u)**. % 0.18/0.47 298[4:Rew:289.0,22.1] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.18/0.47 299[4:Rew:298.1,25.1,290.0,25.1] || -> equal(inverse(sk_c1),sk_c8)** equal(sk_c5,sk_c7). % 0.18/0.47 300[4:Rew:299.1,24.1] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c8,sk_c7),sk_c7)**. % 0.18/0.47 301[4:Rew:1.0,300.1] || -> equal(inverse(sk_c1),sk_c8)** equal(sk_c6,sk_c7). % 0.18/0.47 303[4:Rew:289.0,17.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 304[4:Rew:289.0,12.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)** equal(multiply(sk_c8,sk_c2),sk_c7). % 0.18/0.47 305[4:Rew:289.0,7.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 306[4:Rew:303.0,20.0,290.0,20.0] || -> equal(sk_c5,sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 307[4:Rew:306.0,19.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 308[4:Rew:304.0,15.0,290.0,15.0] || -> equal(sk_c5,sk_c7) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 309[4:Rew:308.0,14.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 310[4:Rew:305.0,10.0,290.0,10.0] || -> equal(sk_c5,sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 311[4:Rew:310.0,9.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 312[4:Rew:1.0,307.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 314[4:Rew:1.0,309.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 316[4:Rew:1.0,311.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 320[4:SpR:288.0,71.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),u)**. % 0.18/0.47 346[0:SpR:29.0,71.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.47 347[0:SpR:29.0,228.0] || -> equal(inverse(identity),identity)**. % 0.18/0.47 349[4:SpR:288.0,29.0] || -> equal(multiply(sk_c6,sk_c8),identity)**. % 0.18/0.47 352[1:Rew:347.0,54.0] || equal(identity,sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.18/0.47 353[4:Rew:349.0,294.0] || equal(identity,sk_c5)** -> . % 0.18/0.47 354[0:Rew:228.0,346.0] || -> equal(inverse(inverse(u)),u)**. % 0.18/0.47 383[5:Spt:299.1] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 384[5:Rew:383.0,353.0] || equal(identity,sk_c7)** -> . % 0.18/0.47 386[6:Spt:301.1] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 388[6:Rew:386.0,288.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.18/0.47 394[6:Rew:386.0,349.0] || -> equal(multiply(sk_c7,sk_c8),identity)**. % 0.18/0.47 395[6:Rew:386.0,64.0] || -> equal(multiply(sk_c8,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.18/0.47 396[6:Rew:386.0,295.0] || -> equal(multiply(sk_c8,multiply(sk_c7,u)),u)**. % 0.18/0.47 398[6:Rew:386.0,320.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),u)**. % 0.18/0.47 408[6:Rew:396.0,395.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.47 409[6:Rew:408.0,398.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.47 411[6:Rew:408.0,394.0] || -> equal(identity,sk_c8)**. % 0.18/0.47 415[6:Rew:411.0,347.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.47 419[6:Rew:411.0,352.0] || equal(sk_c8,sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.18/0.47 421[6:Rew:388.0,415.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 446[6:Obv:419.0] || equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.18/0.47 447[6:Rew:409.0,446.1,421.0,446.1] || equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.47 448[6:Obv:447.0] || equal(u,sk_c8)* -> . % 0.18/0.47 449[6:UnC:448.0,354.0] || -> . % 0.18/0.47 452[6:Spt:449.0,301.1,386.0] || equal(sk_c6,sk_c7)** -> . % 0.18/0.47 453[6:Spt:449.0,301.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.18/0.47 454[6:MRR:312.0,452.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 455[6:MRR:314.0,452.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 456[6:MRR:316.0,452.0] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 458[6:SpR:453.0,354.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.18/0.47 460[6:Rew:288.0,458.0] || -> equal(sk_c1,sk_c6)**. % 0.18/0.47 462[6:Rew:460.0,454.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.18/0.47 463[6:Rew:349.0,462.0] || -> equal(identity,sk_c2)**. % 0.18/0.47 464[6:Rew:463.0,384.0] || equal(sk_c2,sk_c7)** -> . % 0.18/0.47 466[6:Rew:463.0,349.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.18/0.47 468[6:Rew:463.0,228.0] || -> equal(multiply(u,sk_c2),u)**. % 0.18/0.47 475[6:Rew:468.0,455.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 480[6:Rew:475.0,456.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.18/0.47 486[6:Rew:475.0,464.0] || equal(sk_c2,sk_c8)** -> . % 0.18/0.47 487[6:Rew:466.0,480.0] || -> equal(sk_c2,sk_c8)**. % 0.18/0.47 488[6:MRR:487.0,486.0] || -> . % 0.18/0.47 491[5:Spt:488.0,299.1,383.0] || equal(sk_c5,sk_c7)** -> . % 0.18/0.47 492[5:Spt:488.0,299.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.18/0.47 493[5:MRR:306.0,491.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 494[5:MRR:308.0,491.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 495[5:MRR:310.0,491.0] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 497[5:SpR:492.0,354.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.18/0.47 499[5:Rew:288.0,497.0] || -> equal(sk_c1,sk_c6)**. % 0.18/0.47 501[5:Rew:499.0,493.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.18/0.47 502[5:Rew:349.0,501.0] || -> equal(identity,sk_c2)**. % 0.18/0.47 505[5:Rew:502.0,28.0] || -> equal(multiply(sk_c2,u),u)**. % 0.18/0.47 506[5:Rew:502.0,228.0] || -> equal(multiply(u,sk_c2),u)**. % 0.18/0.47 508[5:Rew:502.0,349.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.18/0.47 513[5:Rew:502.0,352.0] || equal(sk_c2,sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.18/0.47 514[5:Rew:506.0,494.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 518[5:Rew:514.0,495.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.18/0.47 524[5:Rew:508.0,518.0] || -> equal(sk_c2,sk_c8)**. % 0.18/0.47 528[5:Rew:524.0,505.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.47 556[5:Rew:528.0,513.2,514.0,513.2,524.0,513.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.47 557[5:Obv:556.1] || equal(u,sk_c8)* -> . % 0.18/0.47 558[5:UnC:557.0,354.0] || -> . % 0.18/0.47 561[3:Spt:558.0,3.0,38.0] || equal(inverse(sk_c3),sk_c8)** -> . % 0.18/0.47 562[3:Spt:558.0,3.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.18/0.47 564[3:Rew:228.0,117.0,562.0,117.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.47 565[3:Rew:564.0,36.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.18/0.47 566[3:Rew:564.0,56.0] || -> equal(multiply(sk_c8,sk_c6),identity)**. % 0.18/0.47 570[3:MRR:23.0,561.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.18/0.47 571[3:MRR:18.0,561.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 572[3:MRR:13.0,561.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 573[3:MRR:8.0,561.0] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 585[3:SpR:570.0,354.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.18/0.47 587[3:Rew:562.0,585.0] || -> equal(sk_c1,sk_c6)**. % 0.18/0.47 589[3:Rew:587.0,571.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.18/0.47 600[3:SpR:572.0,71.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c2)**. % 0.18/0.47 602[3:Rew:562.0,600.0] || -> equal(multiply(sk_c6,sk_c7),sk_c2)**. % 0.18/0.47 603[3:Rew:573.0,602.0] || -> equal(sk_c2,sk_c8)**. % 0.18/0.47 604[3:Rew:603.0,572.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.18/0.47 605[3:Rew:603.0,589.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.18/0.47 626[3:SpR:605.0,71.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c8)**. % 0.18/0.47 628[3:Rew:604.0,626.0,565.0,626.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 629[3:Rew:628.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.47 632[3:Rew:628.0,604.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.18/0.47 639[3:Rew:628.0,352.2] || equal(identity,sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.47 642[3:Rew:629.0,632.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.47 647[3:Rew:642.0,566.0] || -> equal(multiply(sk_c8,sk_c8),identity)**. % 0.18/0.47 648[3:Rew:642.0,605.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.18/0.47 653[3:Rew:647.0,648.0] || -> equal(identity,sk_c8)**. % 0.18/0.47 656[3:Rew:653.0,28.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.47 671[3:Rew:656.0,639.2,653.0,639.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.47 672[3:Obv:671.1] || equal(u,sk_c8)* -> . % 0.18/0.47 673[3:UnC:672.0,603.0] || -> . % 0.18/0.47 676[2:Spt:673.0,6.0,36.0] || equal(inverse(sk_c4),sk_c8)** -> . % 0.18/0.47 677[2:Spt:673.0,6.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.18/0.47 680[2:MRR:26.0,676.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.18/0.47 681[2:MRR:21.0,676.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.18/0.47 682[2:MRR:16.0,676.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 683[2:MRR:11.0,676.0] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 685[2:SpR:677.0,354.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.18/0.47 691[2:SpR:680.0,71.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.18/0.47 692[2:SpR:680.0,354.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.18/0.47 694[2:Rew:677.0,692.0] || -> equal(sk_c1,sk_c6)**. % 0.18/0.47 696[2:Rew:694.0,681.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.18/0.47 697[2:Rew:694.0,691.0] || -> equal(multiply(sk_c8,multiply(sk_c6,u)),u)**. % 0.18/0.47 711[2:SpR:682.0,71.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c2)**. % 0.18/0.47 713[2:Rew:677.0,711.0] || -> equal(multiply(sk_c6,sk_c7),sk_c2)**. % 0.18/0.47 714[2:Rew:683.0,713.0] || -> equal(sk_c2,sk_c8)**. % 0.18/0.47 715[2:Rew:714.0,682.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.18/0.47 716[2:Rew:714.0,696.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.18/0.47 727[2:SpR:716.0,30.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),multiply(sk_c8,u))**. % 0.18/0.47 728[2:SpR:716.0,71.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c8)**. % 0.18/0.47 730[2:Rew:715.0,728.0,685.0,728.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 731[2:Rew:730.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.47 734[2:Rew:730.0,715.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.18/0.47 739[2:Rew:730.0,352.2] || equal(identity,sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.18/0.47 744[2:Rew:731.0,734.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.47 745[2:Rew:744.0,677.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.47 749[2:Rew:744.0,697.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.18/0.47 753[2:Rew:749.0,727.0,744.0,727.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.47 760[2:Rew:753.0,739.2] || equal(identity,sk_c8)** equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.18/0.47 761[2:Obv:760.1] || equal(identity,sk_c8)** equal(u,sk_c8)* -> . % 0.18/0.47 762[2:Con:761.1] || equal(identity,sk_c8)** -> . % 0.18/0.47 781[2:SpR:745.0,29.0] || -> equal(multiply(sk_c8,sk_c8),identity)**. % 0.18/0.47 782[2:Rew:753.0,781.0] || -> equal(identity,sk_c8)**. % 0.18/0.47 783[2:MRR:782.0,762.0] || -> . % 0.18/0.47 786[1:Spt:783.0,33.0,33.2,33.4,33.6] || equal(inverse(u),sk_c8) equal(inverse(sk_c8),sk_c6) equal(multiply(u,sk_c8),sk_c7)**+ equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.18/0.47 789[1:SpL:29.0,786.2] || equal(inverse(inverse(sk_c8)),sk_c8) equal(inverse(sk_c8),sk_c6) equal(identity,sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.18/0.47 791[1:Rew:354.0,789.0] || equal(sk_c8,sk_c8) equal(inverse(sk_c8),sk_c6) equal(identity,sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.18/0.47 792[1:Obv:791.0] || equal(inverse(sk_c8),sk_c6) equal(identity,sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.18/0.47 793[2:Spt:3.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.18/0.47 795[2:Rew:793.0,268.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.18/0.47 797[2:Rew:793.0,792.0] || equal(sk_c6,sk_c6) equal(identity,sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.18/0.47 799[2:Obv:797.0] || equal(identity,sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.18/0.47 804[2:SpR:793.0,354.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.18/0.47 805[2:SpR:793.0,29.0] || -> equal(multiply(sk_c6,sk_c8),identity)**. % 0.18/0.47 807[3:Spt:11.1] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.18/0.47 811[3:Rew:807.0,799.1] || equal(identity,sk_c7)** equal(sk_c8,sk_c8) -> . % 0.18/0.47 812[3:Obv:811.1] || equal(identity,sk_c7)** -> . % 0.18/0.47 817[3:SpR:807.0,71.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c7)**. % 0.18/0.47 819[3:Rew:804.0,817.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.18/0.47 820[4:Spt:26.1] || -> equal(inverse(sk_c1),sk_c8)**. % 0.18/0.47 822[4:SpR:820.0,354.0] || -> equal(inverse(sk_c8),sk_c1)**. % 0.18/0.47 823[4:SpR:820.0,29.0] || -> equal(multiply(sk_c8,sk_c1),identity)**. % 0.18/0.47 825[4:Rew:793.0,822.0] || -> equal(sk_c1,sk_c6)**. % 0.18/0.47 827[4:Rew:825.0,19.1] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.18/0.47 828[4:Rew:825.0,20.1] || -> equal(multiply(sk_c4,sk_c8),sk_c5)** equal(multiply(sk_c6,sk_c8),sk_c2). % 0.18/0.47 831[4:Rew:825.0,21.1] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.18/0.47 832[4:Rew:825.0,823.0] || -> equal(multiply(sk_c8,sk_c6),identity)**. % 0.18/0.47 835[4:Rew:805.0,831.1] || -> equal(inverse(sk_c4),sk_c8)** equal(identity,sk_c2). % 0.18/0.47 836[4:Rew:805.0,827.1] || -> equal(multiply(sk_c8,sk_c5),sk_c7)** equal(identity,sk_c2). % 0.18/0.47 837[4:Rew:805.0,828.1] || -> equal(multiply(sk_c4,sk_c8),sk_c5)** equal(identity,sk_c2). % 0.18/0.47 840[5:Spt:16.1] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.18/0.47 842[5:SpR:840.0,71.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c2)**. % 0.18/0.47 844[5:Rew:807.0,842.0,793.0,842.0] || -> equal(sk_c2,sk_c8)**. % 0.18/0.47 847[5:Rew:844.0,837.1] || -> equal(multiply(sk_c4,sk_c8),sk_c5)** equal(identity,sk_c8). % 0.18/0.47 848[5:Rew:844.0,836.1] || -> equal(multiply(sk_c8,sk_c5),sk_c7)** equal(identity,sk_c8). % 0.18/0.47 849[5:Rew:844.0,835.1] || -> equal(inverse(sk_c4),sk_c8)** equal(identity,sk_c8). % 0.18/0.47 861[2:SpR:795.0,30.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.18/0.47 870[3:SpR:819.0,30.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c7,u))**. % 0.18/0.47 879[6:Spt:849.1] || -> equal(identity,sk_c8)**. % 0.18/0.47 880[6:Rew:879.0,347.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.18/0.47 881[6:Rew:879.0,28.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.47 883[6:Rew:879.0,812.0] || equal(sk_c7,sk_c8)** -> . % 0.18/0.47 890[6:Rew:793.0,880.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.47 896[6:Rew:890.0,795.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.18/0.47 913[6:Rew:881.0,896.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 914[6:MRR:913.0,883.0] || -> . % 0.18/0.47 922[6:Spt:914.0,849.1,879.0] || equal(identity,sk_c8)** -> . % 0.18/0.47 923[6:Spt:914.0,849.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.47 926[6:MRR:847.1,922.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.47 927[6:MRR:848.1,922.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.47 928[6:SpR:923.0,71.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),u)**. % 0.18/0.47 929[6:SpR:923.0,354.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.18/0.47 931[6:Rew:793.0,929.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.47 933[6:Rew:931.0,926.0] || -> equal(multiply(sk_c6,sk_c8),sk_c5)**. % 0.18/0.47 934[6:Rew:805.0,933.0] || -> equal(identity,sk_c5)**. % 0.18/0.47 937[6:Rew:934.0,922.0] || equal(sk_c5,sk_c8)** -> . % 0.18/0.47 938[6:Rew:934.0,832.0] || -> equal(multiply(sk_c8,sk_c6),sk_c5)**. % 0.18/0.47 941[6:Rew:934.0,228.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.47 945[6:Rew:941.0,927.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 947[6:Rew:945.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.47 949[6:Rew:945.0,819.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.18/0.47 951[6:Rew:945.0,861.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.47 960[6:Rew:947.0,949.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.47 966[6:Rew:960.0,931.0] || -> equal(sk_c4,sk_c8)**. % 0.18/0.47 967[6:Rew:960.0,938.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.18/0.47 975[6:Rew:966.0,928.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.18/0.47 976[6:Rew:975.0,951.0,960.0,951.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.47 978[6:Rew:976.0,967.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.47 979[6:MRR:978.0,937.0] || -> . % 0.18/0.47 982[5:Spt:979.0,16.1,840.0] || equal(multiply(sk_c8,sk_c2),sk_c7)** -> . % 0.18/0.47 983[5:Spt:979.0,16.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.47 986[5:MRR:15.1,982.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.47 987[5:MRR:14.1,982.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.47 989[5:SpR:983.0,354.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.18/0.47 991[5:Rew:793.0,989.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.47 993[5:Rew:991.0,986.0] || -> equal(multiply(sk_c6,sk_c8),sk_c5)**. % 0.18/0.47 994[5:Rew:805.0,993.0] || -> equal(identity,sk_c5)**. % 0.18/0.47 996[5:Rew:994.0,812.0] || equal(sk_c5,sk_c7)** -> . % 0.18/0.47 997[5:Rew:994.0,228.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.47 1000[5:Rew:994.0,832.0] || -> equal(multiply(sk_c8,sk_c6),sk_c5)**. % 0.18/0.47 1005[5:Rew:997.0,987.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.47 1006[5:Rew:1005.0,819.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.18/0.47 1008[5:Rew:1005.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.47 1018[5:Rew:1005.0,996.0] || equal(sk_c5,sk_c8)** -> . % 0.18/0.47 1021[5:Rew:1006.0,1008.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.47 1029[5:Rew:1021.0,1000.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.18/0.47 1033[5:Rew:1006.0,1029.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.47 1034[5:MRR:1033.0,1018.0] || -> . % 0.18/0.47 1041[4:Spt:1034.0,26.1,820.0] || equal(inverse(sk_c1),sk_c8)** -> . % 0.18/0.48 1042[4:Spt:1034.0,26.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.48 1045[4:MRR:25.0,1041.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.48 1046[4:MRR:24.0,1041.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.48 1047[4:SpR:1042.0,71.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),u)**. % 0.18/0.48 1048[4:SpR:1042.0,354.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.18/0.48 1050[4:Rew:793.0,1048.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.48 1052[4:Rew:1050.0,1045.0] || -> equal(multiply(sk_c6,sk_c8),sk_c5)**. % 0.18/0.48 1053[4:Rew:805.0,1052.0] || -> equal(identity,sk_c5)**. % 0.18/0.48 1054[4:Rew:1053.0,812.0] || equal(sk_c5,sk_c7)** -> . % 0.18/0.48 1056[4:Rew:1053.0,805.0] || -> equal(multiply(sk_c6,sk_c8),sk_c5)**. % 0.18/0.48 1058[4:Rew:1053.0,228.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.48 1064[4:Rew:1058.0,1046.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.48 1066[4:Rew:1064.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.18/0.48 1068[4:Rew:1064.0,819.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.18/0.48 1069[4:Rew:1064.0,870.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c8,u))**. % 0.18/0.48 1076[4:Rew:1064.0,1054.0] || equal(sk_c5,sk_c8)** -> . % 0.18/0.48 1079[4:Rew:1066.0,1068.0] || -> equal(sk_c6,sk_c8)**. % 0.18/0.48 1084[4:Rew:1079.0,1050.0] || -> equal(sk_c4,sk_c8)**. % 0.18/0.48 1085[4:Rew:1079.0,1056.0] || -> equal(multiply(sk_c8,sk_c8),sk_c5)**. % 0.18/0.48 1093[4:Rew:1084.0,1047.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.18/0.48 1094[4:Rew:1093.0,1069.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.48 1096[4:Rew:1094.0,1085.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.48 1097[4:MRR:1096.0,1076.0] || -> . % 0.18/0.48 1101[3:Spt:1097.0,11.1,807.0] || equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.18/0.48 1102[3:Spt:1097.0,11.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.48 1103[3:MRR:8.1,1101.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.48 1104[3:MRR:7.1,1101.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.48 1105[3:MRR:10.1,1101.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.48 1106[3:MRR:9.1,1101.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.48 1108[3:SpR:1102.0,354.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.18/0.48 1110[3:Rew:793.0,1108.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.48 1112[3:Rew:1110.0,1105.0] || -> equal(multiply(sk_c6,sk_c8),sk_c5)**. % 0.18/0.48 1113[3:Rew:805.0,1112.0] || -> equal(identity,sk_c5)**. % 0.18/0.48 1116[3:Rew:1113.0,228.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.48 1118[3:Rew:1113.0,805.0] || -> equal(multiply(sk_c6,sk_c8),sk_c5)**. % 0.18/0.48 1122[3:Rew:1116.0,1106.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.48 1125[3:Rew:1122.0,1101.0] || equal(multiply(sk_c6,sk_c8),sk_c8)** -> . % 0.18/0.48 1128[3:Rew:1122.0,1104.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.18/0.48 1129[3:Rew:1118.0,1125.0] || equal(sk_c5,sk_c8)** -> . % 0.18/0.48 1138[3:SpR:1103.0,354.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.18/0.48 1140[3:Rew:793.0,1138.0] || -> equal(sk_c3,sk_c6)**. % 0.18/0.48 1142[3:Rew:1140.0,1128.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.18/0.48 1143[3:Rew:1118.0,1142.0] || -> equal(sk_c5,sk_c8)**. % 0.18/0.48 1144[3:MRR:1143.0,1129.0] || -> . % 0.18/0.48 1146[2:Spt:1144.0,3.1,793.0] || equal(inverse(sk_c8),sk_c6)** -> . % 0.18/0.48 1147[2:Spt:1144.0,3.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.18/0.48 1148[2:MRR:6.1,1146.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.18/0.48 1149[2:MRR:2.0,1146.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.18/0.48 1150[2:MRR:4.0,1146.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.18/0.48 1151[2:MRR:5.0,1146.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.18/0.48 1153[2:SpR:1147.0,354.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.18/0.48 1155[2:Rew:1153.0,1146.0] || equal(sk_c3,sk_c6)** -> . % 0.18/0.48 1162[2:SpR:1148.0,354.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.18/0.48 1164[2:Rew:1153.0,1162.0] || -> equal(sk_c4,sk_c3)**. % 0.18/0.48 1166[2:Rew:1164.0,1151.0] || -> equal(multiply(sk_c3,sk_c8),sk_c5)**. % 0.18/0.48 1167[2:Rew:1149.0,1166.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.48 1168[2:Rew:1167.0,1150.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7)**. % 0.18/0.48 1169[2:Rew:1.0,1168.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.48 1170[2:Rew:1169.0,1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7)**. % 0.18/0.48 1172[2:Rew:1169.0,1155.0] || equal(sk_c3,sk_c7)** -> . % 0.18/0.48 1178[2:SpR:1153.0,71.0] || -> equal(multiply(sk_c3,multiply(sk_c8,u)),u)**. % 0.18/0.48 1181[2:SpR:1149.0,30.0] || -> equal(multiply(sk_c3,multiply(sk_c8,u)),multiply(sk_c7,u))**. % 0.18/0.48 1182[2:SpR:1149.0,71.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c8)**. % 0.18/0.48 1184[2:Rew:1147.0,1182.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.18/0.48 1185[2:Rew:1170.0,1184.0] || -> equal(sk_c7,sk_c8)**. % 0.18/0.48 1188[2:Rew:1185.0,1172.0] || equal(sk_c3,sk_c8)** -> . % 0.18/0.48 1193[2:Rew:1178.0,1181.0,1185.0,1181.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.48 1194[2:Rew:1193.0,1178.0] || -> equal(multiply(sk_c3,u),u)**. % 0.18/0.48 1215[2:SpR:1147.0,29.0] || -> equal(multiply(sk_c8,sk_c3),identity)**. % 0.18/0.48 1217[2:SpR:1153.0,29.0] || -> equal(multiply(sk_c3,sk_c8),identity)**. % 0.18/0.48 1218[2:Rew:1193.0,1215.0] || -> equal(identity,sk_c3)**. % 0.18/0.48 1228[2:Rew:1194.0,1217.0,1218.0,1217.0] || -> equal(sk_c3,sk_c8)**. % 0.18/0.48 1229[2:MRR:1228.0,1188.0] || -> . % 0.18/0.48 % SZS output end Refutation % 0.18/0.48 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_7 prove_this_8 prove_this_9 prove_this_10 prove_this_11 prove_this_12 prove_this_13 prove_this_14 prove_this_15 prove_this_16 prove_this_17 prove_this_18 prove_this_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_25 prove_this_26 prove_this_27 left_identity left_inverse associativity % 0.18/0.48 %------------------------------------------------------------------------------