%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP323-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:51 EDT 2022 % Result : Unsatisfiable 0.19s 0.48s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP323-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n008.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 : Tue Jun 14 09:37:07 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.48 % 0.19/0.48 SPASS V 3.9 % 0.19/0.48 SPASS beiseite: Proof found. % 0.19/0.48 % SZS status Theorem % 0.19/0.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.48 SPASS derived 1020 clauses, backtracked 396 clauses, performed 12 splits and kept 776 clauses. % 0.19/0.48 SPASS allocated 63742 KBytes. % 0.19/0.48 SPASS spent 0:00:00.14 on the problem. % 0.19/0.48 0:00:00.03 for the input. % 0.19/0.48 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.48 0:00:00.01 for inferences. % 0.19/0.48 0:00:00.00 for the backtracking. % 0.19/0.48 0:00:00.07 for the reduction. % 0.19/0.48 % 0.19/0.48 % 0.19/0.48 Here is a proof with depth 4, length 410 : % 0.19/0.48 % SZS output start Refutation % 0.19/0.48 1[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c8),sk_c6). % 0.19/0.48 2[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c7)** equal(multiply(sk_c7,sk_c8),sk_c6). % 0.19/0.48 3[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.48 4[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6)** equal(multiply(sk_c7,sk_c8),sk_c6). % 0.19/0.48 5[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.48 6[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 7[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 8[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 9[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 10[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 11[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.48 12[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c8),sk_c7)**. % 0.19/0.48 13[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 14[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.48 15[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 16[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 17[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c7)** equal(multiply(sk_c8,sk_c3),sk_c7). % 0.19/0.48 18[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 19[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6)** equal(multiply(sk_c8,sk_c3),sk_c7). % 0.19/0.48 20[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 21[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 22[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c7) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 23[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 24[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 25[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 26[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.48 27[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c4,sk_c8),sk_c7)**. % 0.19/0.48 28[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 29[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.48 30[0:Inp] || -> equal(inverse(sk_c5),sk_c8) equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 31[0:Inp] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(x),sk_c7) equal(multiply(w,sk_c8),y)*+ equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(x,sk_c7),sk_c8)** equal(multiply(sk_c8,y),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c8),sk_c6) -> . % 0.19/0.48 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.48 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.48 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.48 35[1:Spt:31.2,31.4,31.8] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),v)*+ equal(multiply(sk_c8,v),sk_c7)** -> . % 0.19/0.48 37[2:Spt:1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.48 39[3:Spt:5.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.48 41[4:Spt:3.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.48 44[1:SpL:32.0,35.1] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.19/0.48 45[5:Spt:4.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.48 50[6:Spt:2.0] || -> equal(multiply(sk_c4,sk_c8),sk_c7)**. % 0.19/0.48 56[3:SpR:39.0,33.0] || -> equal(multiply(sk_c8,sk_c5),identity)**. % 0.19/0.48 57[4:SpR:41.0,33.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.19/0.48 58[1:SpL:33.0,35.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.19/0.48 67[4:SpR:57.0,34.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),multiply(identity,u))**. % 0.19/0.48 69[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.48 72[4:Rew:32.0,67.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),u)**. % 0.19/0.48 73[0:Rew:32.0,69.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.48 83[6:SpR:50.0,72.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.19/0.48 84[6:Rew:37.0,83.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.48 85[6:Rew:84.0,37.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.19/0.48 86[6:Rew:84.0,45.0] || -> equal(multiply(sk_c5,sk_c8),sk_c8)**. % 0.19/0.48 104[0:SpR:73.0,73.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.48 108[3:SpR:56.0,73.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c5)**. % 0.19/0.48 109[4:SpR:57.0,73.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c4)**. % 0.19/0.48 112[6:SpR:85.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c7)**. % 0.19/0.48 115[0:SpR:33.0,73.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.48 121[4:Rew:108.0,109.0] || -> equal(sk_c5,sk_c4)**. % 0.19/0.48 125[6:Rew:121.0,86.0] || -> equal(multiply(sk_c4,sk_c8),sk_c8)**. % 0.19/0.48 127[4:Rew:121.0,108.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c4)**. % 0.19/0.48 128[6:Rew:50.0,125.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 130[6:Rew:128.0,41.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.48 132[6:Rew:128.0,57.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.48 139[6:Rew:128.0,58.2] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.19/0.48 145[6:Rew:33.0,112.0] || -> equal(identity,sk_c7)**. % 0.19/0.48 146[6:Rew:145.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.48 148[6:Rew:145.0,132.0] || -> equal(multiply(sk_c7,sk_c4),sk_c7)**. % 0.19/0.48 149[6:Rew:146.0,148.0] || -> equal(sk_c4,sk_c7)**. % 0.19/0.48 151[6:Rew:149.0,130.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.48 174[6:Rew:146.0,139.2,145.0,139.1,151.0,139.0,151.0,139.0,128.0,139.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.19/0.48 175[6:Obv:174.1] || equal(u,sk_c7)* -> . % 0.19/0.48 176[6:UnC:175.0,73.0] || -> . % 0.19/0.48 179[6:Spt:176.0,2.0,50.0] || equal(multiply(sk_c4,sk_c8),sk_c7)** -> . % 0.19/0.48 180[6:Spt:176.0,2.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.48 181[5:Rew:121.0,45.0] || -> equal(multiply(sk_c4,sk_c8),sk_c6)**. % 0.19/0.48 182[6:Rew:181.0,179.0] || equal(sk_c6,sk_c7)** -> . % 0.19/0.48 183[0:Rew:104.0,115.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.48 184[4:Rew:183.0,127.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.19/0.48 188[5:Rew:181.0,27.1] || -> equal(inverse(sk_c2),sk_c8)** equal(sk_c6,sk_c7). % 0.19/0.48 189[6:MRR:188.1,182.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 190[5:Rew:181.0,12.1] || -> equal(inverse(sk_c1),sk_c7)** equal(sk_c6,sk_c7). % 0.19/0.48 191[6:MRR:190.1,182.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 193[5:Rew:181.0,22.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 194[6:MRR:193.0,182.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 195[5:Rew:181.0,17.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 196[6:MRR:195.0,182.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 197[5:Rew:181.0,7.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 198[6:MRR:197.0,182.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 219[6:SpR:194.0,73.0] || -> equal(multiply(inverse(sk_c2),sk_c3),sk_c8)**. % 0.19/0.48 221[6:Rew:189.0,219.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.48 222[6:Rew:196.0,221.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 223[6:Rew:222.0,180.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.48 239[6:Rew:222.0,198.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.19/0.48 294[6:SpR:239.0,73.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c7)**. % 0.19/0.48 296[6:Rew:223.0,294.0,191.0,294.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 297[6:MRR:296.0,182.0] || -> . % 0.19/0.48 298[5:Spt:297.0,4.0,45.0] || equal(multiply(sk_c5,sk_c8),sk_c6)** -> . % 0.19/0.48 299[5:Spt:297.0,4.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.48 300[5:Rew:121.0,298.0] || equal(multiply(sk_c4,sk_c8),sk_c6)** -> . % 0.19/0.48 301[4:Rew:121.0,29.1] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c4,sk_c8),sk_c6)**. % 0.19/0.48 302[4:Rew:27.1,301.1] || -> equal(inverse(sk_c2),sk_c8)** equal(sk_c6,sk_c7). % 0.19/0.48 303[4:Rew:121.0,14.1] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c8),sk_c6)**. % 0.19/0.48 304[4:Rew:12.1,303.1] || -> equal(inverse(sk_c1),sk_c7)** equal(sk_c6,sk_c7). % 0.19/0.48 305[4:Rew:121.0,24.0] || -> equal(multiply(sk_c4,sk_c8),sk_c6) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 306[4:Rew:22.0,305.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 307[4:Rew:121.0,19.0] || -> equal(multiply(sk_c4,sk_c8),sk_c6)** equal(multiply(sk_c8,sk_c3),sk_c7). % 0.19/0.48 308[4:Rew:17.0,307.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 309[4:Rew:121.0,9.0] || -> equal(multiply(sk_c4,sk_c8),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 310[4:Rew:7.0,309.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 312[5:SpR:299.0,73.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.19/0.48 327[2:SpR:37.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.19/0.48 346[0:SpR:33.0,73.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.48 347[0:SpR:33.0,183.0] || -> equal(inverse(identity),identity)**. % 0.19/0.48 349[4:SpR:184.0,33.0] || -> equal(multiply(sk_c4,sk_c8),identity)**. % 0.19/0.48 352[1:Rew:347.0,44.0] || equal(identity,sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.19/0.48 353[5:Rew:349.0,300.0] || equal(identity,sk_c6)** -> . % 0.19/0.48 354[4:Rew:349.0,7.0] || -> equal(identity,sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 355[4:Rew:349.0,17.0] || -> equal(identity,sk_c7) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 356[4:Rew:349.0,22.0] || -> equal(identity,sk_c7) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 357[4:Rew:349.0,12.1] || -> equal(inverse(sk_c1),sk_c7)** equal(identity,sk_c7). % 0.19/0.48 358[4:Rew:349.0,27.1] || -> equal(inverse(sk_c2),sk_c8)** equal(identity,sk_c7). % 0.19/0.48 359[0:Rew:183.0,346.0] || -> equal(inverse(inverse(u)),u)**. % 0.19/0.48 366[6:Spt:302.1] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 370[6:Rew:366.0,312.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.19/0.48 371[6:Rew:366.0,353.0] || equal(identity,sk_c7)** -> . % 0.19/0.48 376[6:MRR:357.1,371.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 377[6:MRR:358.1,371.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 378[6:MRR:354.0,371.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 379[6:MRR:355.0,371.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 380[6:MRR:356.0,371.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 381[6:Rew:33.0,370.0] || -> equal(identity,sk_c8)**. % 0.19/0.48 382[6:Rew:381.0,32.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.48 384[6:Rew:381.0,183.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.48 390[6:Rew:381.0,371.0] || equal(sk_c8,sk_c7)** -> . % 0.19/0.48 398[6:Rew:382.0,379.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.48 402[6:Rew:398.0,380.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.48 405[6:Rew:384.0,402.0] || -> equal(sk_c2,sk_c7)**. % 0.19/0.48 406[6:Rew:405.0,377.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.19/0.48 424[6:SpR:376.0,73.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.19/0.48 429[6:SpR:406.0,73.0] || -> equal(multiply(sk_c8,multiply(sk_c7,u)),u)**. % 0.19/0.48 431[6:Rew:382.0,429.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.48 432[6:Rew:431.0,424.0] || -> equal(multiply(sk_c1,u),u)**. % 0.19/0.48 433[6:Rew:432.0,378.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 434[6:MRR:433.0,390.0] || -> . % 0.19/0.48 435[6:Spt:434.0,302.1,366.0] || equal(sk_c6,sk_c7)** -> . % 0.19/0.48 436[6:Spt:434.0,302.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 437[6:MRR:304.1,435.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 438[6:MRR:306.0,435.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 439[6:MRR:308.0,435.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 440[6:MRR:310.0,435.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 465[6:SpR:438.0,73.0] || -> equal(multiply(inverse(sk_c2),sk_c3),sk_c8)**. % 0.19/0.48 467[6:Rew:436.0,465.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.48 468[6:Rew:439.0,467.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 472[6:Rew:468.0,37.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.48 485[6:Rew:468.0,440.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.19/0.48 543[6:SpR:485.0,73.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c7)**. % 0.19/0.48 545[6:Rew:472.0,543.0,437.0,543.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 546[6:MRR:545.0,435.0] || -> . % 0.19/0.48 547[4:Spt:546.0,3.0,41.0] || equal(inverse(sk_c4),sk_c8)** -> . % 0.19/0.48 548[4:Spt:546.0,3.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.48 549[3:Rew:183.0,108.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.19/0.48 550[3:Rew:549.0,327.0] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.48 552[4:MRR:28.0,547.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 553[4:MRR:13.0,547.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 555[4:MRR:23.0,547.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 556[4:MRR:18.0,547.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 557[4:MRR:8.0,547.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 570[3:SpR:549.0,73.0] || -> equal(multiply(sk_c5,multiply(sk_c8,u)),u)**. % 0.19/0.48 583[3:SpR:550.0,34.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.19/0.48 588[4:SpR:555.0,73.0] || -> equal(multiply(inverse(sk_c2),sk_c3),sk_c8)**. % 0.19/0.48 590[4:Rew:552.0,588.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.48 591[4:Rew:556.0,590.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 592[4:Rew:591.0,548.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.48 594[4:Rew:591.0,39.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.19/0.48 598[4:Rew:591.0,56.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.19/0.48 603[4:Rew:591.0,557.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.19/0.48 606[4:Rew:591.0,352.0] || equal(identity,sk_c7) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.19/0.48 609[4:Rew:591.0,570.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.19/0.48 616[4:Rew:591.0,606.2,591.0,606.1] || equal(identity,sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.19/0.48 644[4:SpR:603.0,73.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c7)**. % 0.19/0.48 646[4:Rew:592.0,644.0,553.0,644.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 649[4:Rew:646.0,583.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.19/0.48 657[4:Rew:609.0,649.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.48 658[4:Rew:657.0,598.0] || -> equal(identity,sk_c5)**. % 0.19/0.48 665[4:Rew:657.0,616.2] || equal(identity,sk_c7)** equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.19/0.48 669[4:Rew:658.0,347.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.48 673[4:Rew:594.0,669.0] || -> equal(sk_c5,sk_c7)**. % 0.19/0.48 677[4:Rew:673.0,658.0] || -> equal(identity,sk_c7)**. % 0.19/0.48 687[4:Obv:665.1] || equal(identity,sk_c7)** equal(u,sk_c7)* -> . % 0.19/0.48 688[4:Con:687.1] || equal(identity,sk_c7)** -> . % 0.19/0.48 689[4:Rew:677.0,688.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.48 690[4:Obv:689.0] || -> . % 0.19/0.48 693[3:Spt:690.0,5.0,39.0] || equal(inverse(sk_c5),sk_c8)** -> . % 0.19/0.48 694[3:Spt:690.0,5.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.48 695[3:MRR:30.0,693.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 696[3:MRR:15.0,693.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 697[3:MRR:25.0,693.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 698[3:MRR:20.0,693.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 699[3:MRR:10.0,693.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 714[3:SpR:697.0,73.0] || -> equal(multiply(inverse(sk_c2),sk_c3),sk_c8)**. % 0.19/0.48 716[3:Rew:695.0,714.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.48 717[3:Rew:698.0,716.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 718[3:Rew:717.0,694.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.48 723[3:Rew:717.0,327.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.19/0.48 725[3:Rew:717.0,698.0] || -> equal(multiply(sk_c7,sk_c3),sk_c7)**. % 0.19/0.48 726[3:Rew:717.0,699.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.19/0.48 727[3:Rew:717.0,352.2] || equal(identity,sk_c8) equal(sk_c8,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.19/0.48 737[3:Rew:717.0,727.1,717.0,727.0] || equal(identity,sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.19/0.48 751[3:SpR:725.0,73.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c3)**. % 0.19/0.48 753[3:Rew:33.0,751.0] || -> equal(identity,sk_c3)**. % 0.19/0.48 756[3:Rew:753.0,32.0] || -> equal(multiply(sk_c3,u),u)**. % 0.19/0.48 757[3:Rew:753.0,33.0] || -> equal(multiply(inverse(u),u),sk_c3)**. % 0.19/0.48 759[3:Rew:753.0,737.0] || equal(sk_c3,sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.19/0.48 767[3:SpR:726.0,73.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c7)**. % 0.19/0.48 769[3:Rew:718.0,767.0,696.0,767.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 771[3:Rew:769.0,723.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.19/0.48 773[3:Rew:757.0,771.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.48 778[3:Rew:773.0,756.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.49 781[3:Rew:773.0,759.0] || equal(sk_c7,sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.19/0.49 800[3:Obv:781.0] || equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.19/0.49 801[3:Rew:778.0,800.1] || equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.19/0.49 802[3:Obv:801.0] || equal(u,sk_c7)* -> . % 0.19/0.49 803[3:UnC:802.0,717.0] || -> . % 0.19/0.49 806[2:Spt:803.0,1.0,37.0] || equal(multiply(sk_c8,sk_c7),sk_c6)** -> . % 0.19/0.49 807[2:Spt:803.0,1.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.49 808[2:MRR:26.1,806.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.49 810[2:MRR:21.0,806.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.49 811[2:MRR:16.0,806.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.49 824[2:SpR:810.0,73.0] || -> equal(multiply(inverse(sk_c2),sk_c3),sk_c8)**. % 0.19/0.49 826[2:Rew:808.0,824.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.49 827[2:Rew:811.0,826.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.49 828[2:Rew:827.0,807.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.49 831[2:Rew:827.0,806.0] || equal(multiply(sk_c7,sk_c7),sk_c6)** -> . % 0.19/0.49 842[2:Rew:828.0,831.0] || equal(sk_c6,sk_c6)* -> . % 0.19/0.49 843[2:Obv:842.0] || -> . % 0.19/0.49 849[1:Spt:843.0,31.0,31.1,31.3,31.5,31.6,31.7,31.9,31.10] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)**+ equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c8),sk_c6) -> . % 0.19/0.49 851[2:Spt:1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.49 852[2:Rew:851.0,849.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(sk_c6,sk_c6) equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.19/0.49 854[2:Obv:852.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.19/0.49 857[2:SpR:851.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.19/0.49 859[3:Spt:3.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.49 862[4:Spt:5.0] || -> equal(inverse(sk_c5),sk_c8)**. % 0.19/0.49 865[5:Spt:2.0] || -> equal(multiply(sk_c4,sk_c8),sk_c7)**. % 0.19/0.49 867[5:SpR:865.0,73.0] || -> equal(multiply(inverse(sk_c4),sk_c7),sk_c8)**. % 0.19/0.49 869[5:Rew:851.0,867.0,859.0,867.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 872[5:Rew:869.0,854.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c7,sk_c8),sk_c8)** -> . % 0.19/0.49 874[5:Rew:869.0,9.0] || -> equal(multiply(sk_c5,sk_c8),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.49 877[5:Rew:869.0,14.1] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c5,sk_c8),sk_c8)**. % 0.19/0.49 879[5:Rew:869.0,857.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c7)**. % 0.19/0.49 881[5:Rew:33.0,879.0] || -> equal(identity,sk_c7)**. % 0.19/0.49 882[5:Rew:881.0,347.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.49 883[5:Rew:881.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.49 884[5:Rew:881.0,183.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.49 888[5:Rew:884.0,874.1] || -> equal(multiply(sk_c5,sk_c8),sk_c8)** equal(sk_c1,sk_c8). % 0.19/0.49 889[5:Rew:888.1,877.0] || -> equal(inverse(sk_c8),sk_c7) equal(multiply(sk_c5,sk_c8),sk_c8)**. % 0.19/0.49 890[5:Rew:883.0,872.6,884.0,872.5,869.0,872.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7)** equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** equal(w,sk_c8) equal(sk_c8,sk_c8) -> . % 0.19/0.49 891[5:Obv:890.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7)** equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** equal(w,sk_c8) -> . % 0.19/0.49 903[0:SpR:359.0,73.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.19/0.49 906[3:SpR:859.0,359.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.19/0.49 907[4:SpR:862.0,359.0] || -> equal(inverse(sk_c8),sk_c5)**. % 0.19/0.49 909[5:Rew:906.0,889.0] || -> equal(sk_c4,sk_c7) equal(multiply(sk_c5,sk_c8),sk_c8)**. % 0.19/0.49 910[4:Rew:906.0,907.0] || -> equal(sk_c5,sk_c4)**. % 0.19/0.49 917[5:Rew:910.0,909.1] || -> equal(sk_c4,sk_c7) equal(multiply(sk_c4,sk_c8),sk_c8)**. % 0.19/0.49 918[5:Rew:865.0,917.1] || -> equal(sk_c4,sk_c7)** equal(sk_c8,sk_c7). % 0.19/0.49 924[3:SpR:906.0,73.0] || -> equal(multiply(sk_c4,multiply(sk_c8,u)),u)**. % 0.19/0.49 927[6:Spt:918.0] || -> equal(sk_c4,sk_c7)**. % 0.19/0.49 928[6:Rew:927.0,859.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.19/0.49 934[6:Rew:882.0,928.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.49 936[6:Rew:934.0,891.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7)** equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c7)** equal(w,sk_c8) -> . % 0.19/0.49 944[6:Rew:934.0,936.5,884.0,936.4,934.0,936.4,884.0,936.3,934.0,936.3,934.0,936.1] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) equal(w,sk_c7) -> . % 0.19/0.49 945[6:Con:944.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.49 992[6:SpL:882.0,945.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.49 994[6:Obv:992.1] || -> . % 0.19/0.49 995[6:Spt:994.0,918.0,927.0] || equal(sk_c4,sk_c7)** -> . % 0.19/0.49 996[6:Spt:994.0,918.1] || -> equal(sk_c8,sk_c7)**. % 0.19/0.49 998[6:Rew:996.0,906.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.19/0.49 999[6:Rew:882.0,998.0] || -> equal(sk_c4,sk_c7)**. % 0.19/0.49 1002[6:Rew:999.0,995.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.49 1003[6:Obv:1002.0] || -> . % 0.19/0.49 1014[5:Spt:1003.0,2.0,865.0] || equal(multiply(sk_c4,sk_c8),sk_c7)** -> . % 0.19/0.49 1015[5:Spt:1003.0,2.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.49 1016[3:Rew:906.0,857.0] || -> equal(multiply(sk_c4,sk_c6),sk_c7)**. % 0.19/0.49 1017[5:MRR:27.1,1014.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.49 1018[5:MRR:12.1,1014.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.49 1019[5:MRR:22.0,1014.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.49 1020[5:MRR:17.0,1014.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.49 1021[5:MRR:7.0,1014.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.49 1031[5:SpR:1017.0,359.0] || -> equal(inverse(sk_c8),sk_c2)**. % 0.19/0.49 1034[5:Rew:906.0,1031.0] || -> equal(sk_c2,sk_c4)**. % 0.19/0.49 1036[5:Rew:1034.0,1019.0] || -> equal(multiply(sk_c4,sk_c8),sk_c3)**. % 0.19/0.49 1037[5:Rew:1036.0,1014.0] || equal(sk_c3,sk_c7)** -> . % 0.19/0.49 1055[5:SpR:1018.0,73.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.19/0.49 1057[5:SpR:1018.0,903.0] || -> equal(multiply(sk_c1,multiply(sk_c7,u)),u)**. % 0.19/0.49 1072[5:SpR:1020.0,34.0] || -> equal(multiply(sk_c8,multiply(sk_c3,u)),multiply(sk_c7,u))**. % 0.19/0.49 1076[5:SpR:1021.0,34.0] || -> equal(multiply(sk_c1,multiply(sk_c7,u)),multiply(sk_c8,u))**. % 0.19/0.49 1091[5:Rew:1057.0,1076.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 1093[5:Rew:1091.0,924.0] || -> equal(multiply(sk_c4,u),u)**. % 0.19/0.49 1094[5:Rew:1091.0,1072.0] || -> equal(multiply(sk_c3,u),multiply(sk_c7,u))**. % 0.19/0.49 1098[5:Rew:1093.0,1036.0] || -> equal(sk_c3,sk_c8)**. % 0.19/0.49 1100[5:Rew:1098.0,1037.0] || equal(sk_c8,sk_c7)** -> . % 0.19/0.49 1101[5:Rew:1091.0,1094.0,1098.0,1094.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.49 1103[5:Rew:1101.0,1055.0] || -> equal(multiply(sk_c1,u),u)**. % 0.19/0.49 1106[5:Rew:1103.0,1021.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.49 1107[5:MRR:1106.0,1100.0] || -> . % 0.19/0.49 1110[4:Spt:1107.0,5.0,862.0] || equal(inverse(sk_c5),sk_c8)** -> . % 0.19/0.49 1111[4:Spt:1107.0,5.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.49 1112[4:MRR:30.0,1110.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.49 1113[4:MRR:15.0,1110.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.49 1114[4:MRR:25.0,1110.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.49 1115[4:MRR:20.0,1110.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.49 1116[4:MRR:10.0,1110.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.49 1117[4:Rew:1111.0,854.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(sk_c6,sk_c6) -> . % 0.19/0.49 1118[4:Obv:1117.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.19/0.49 1125[4:SpR:1112.0,359.0] || -> equal(inverse(sk_c8),sk_c2)**. % 0.19/0.49 1128[4:Rew:906.0,1125.0] || -> equal(sk_c2,sk_c4)**. % 0.19/0.49 1130[4:Rew:1128.0,1114.0] || -> equal(multiply(sk_c4,sk_c8),sk_c3)**. % 0.19/0.49 1136[4:SpR:1113.0,903.0] || -> equal(multiply(sk_c1,multiply(sk_c7,u)),u)**. % 0.19/0.49 1152[4:SpR:1115.0,73.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c3)**. % 0.19/0.49 1154[4:Rew:906.0,1152.0] || -> equal(multiply(sk_c4,sk_c7),sk_c3)**. % 0.19/0.49 1155[4:SpR:1116.0,34.0] || -> equal(multiply(sk_c1,multiply(sk_c7,u)),multiply(sk_c8,u))**. % 0.19/0.49 1156[4:SpR:1116.0,73.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.19/0.49 1158[4:Rew:1111.0,1156.0,1113.0,1156.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.49 1160[4:Rew:1158.0,1016.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7)**. % 0.19/0.49 1165[4:Rew:1158.0,1118.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.19/0.49 1168[4:Rew:1154.0,1160.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.49 1170[4:Rew:1168.0,1130.0] || -> equal(multiply(sk_c4,sk_c8),sk_c7)**. % 0.19/0.49 1173[4:Rew:1136.0,1155.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 1174[4:Rew:1173.0,924.0] || -> equal(multiply(sk_c4,u),u)**. % 0.19/0.49 1176[4:Rew:1174.0,1170.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.49 1178[4:Rew:1176.0,859.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.49 1182[4:Rew:1176.0,1173.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.49 1194[4:Con:1165.1] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** -> . % 0.19/0.49 1195[4:Rew:1176.0,1194.3,1176.0,1194.2,1176.0,1194.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** -> . % 0.19/0.49 1196[4:Con:1195.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.19/0.49 1236[4:SpR:1178.0,33.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.49 1238[4:Rew:1182.0,1236.0] || -> equal(identity,sk_c4)**. % 0.19/0.49 1239[4:Rew:1238.0,347.0] || -> equal(inverse(sk_c4),sk_c4)**. % 0.19/0.49 1240[4:Rew:1238.0,183.0] || -> equal(multiply(u,sk_c4),u)**. % 0.19/0.49 1244[4:Rew:1178.0,1239.0] || -> equal(sk_c4,sk_c7)**. % 0.19/0.49 1247[4:Rew:1244.0,1178.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.49 1252[4:Rew:1244.0,1240.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.49 1253[4:Rew:1252.0,1196.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.49 1306[4:SpL:1247.0,1253.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.49 1307[4:Obv:1306.1] || -> . % 0.19/0.49 1308[3:Spt:1307.0,3.0,859.0] || equal(inverse(sk_c4),sk_c8)** -> . % 0.19/0.49 1309[3:Spt:1307.0,3.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.49 1311[3:MRR:28.0,1308.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.49 1312[3:MRR:13.0,1308.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.49 1313[3:MRR:23.0,1308.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.49 1314[3:MRR:18.0,1308.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.49 1315[3:MRR:8.0,1308.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.49 1317[3:Rew:1309.0,854.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(sk_c6,sk_c6) -> . % 0.19/0.49 1318[3:Obv:1317.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.19/0.49 1331[3:SpR:1311.0,359.0] || -> equal(inverse(sk_c8),sk_c2)**. % 0.19/0.49 1336[3:SpR:1312.0,359.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.19/0.49 1337[3:SpR:1312.0,903.0] || -> equal(multiply(sk_c1,multiply(sk_c7,u)),u)**. % 0.19/0.49 1352[3:SpR:1313.0,34.0] || -> equal(multiply(sk_c2,multiply(sk_c8,u)),multiply(sk_c3,u))**. % 0.19/0.49 1353[3:SpR:1313.0,73.0] || -> equal(multiply(inverse(sk_c2),sk_c3),sk_c8)**. % 0.19/0.49 1355[3:Rew:1311.0,1353.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.49 1356[3:Rew:1314.0,1355.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.49 1357[3:Rew:1356.0,1309.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.49 1359[3:Rew:1356.0,1331.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.19/0.49 1362[3:Rew:1356.0,1313.0] || -> equal(multiply(sk_c2,sk_c7),sk_c3)**. % 0.19/0.49 1364[3:Rew:1356.0,1314.0] || -> equal(multiply(sk_c7,sk_c3),sk_c7)**. % 0.19/0.49 1365[3:Rew:1356.0,1315.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.19/0.49 1366[3:Rew:1356.0,1318.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.19/0.49 1372[3:Rew:1336.0,1359.0] || -> equal(sk_c2,sk_c1)**. % 0.19/0.49 1375[3:Rew:1372.0,1362.0] || -> equal(multiply(sk_c1,sk_c7),sk_c3)**. % 0.19/0.49 1376[3:Rew:1375.0,1365.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.49 1378[3:Rew:1376.0,1364.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.19/0.49 1379[3:Rew:1357.0,1378.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.49 1384[3:Rew:1337.0,1352.0,1372.0,1352.0,1356.0,1352.0,1376.0,1352.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.49 1389[3:Rew:1356.0,1366.5,1356.0,1366.4,1356.0,1366.3,1379.0,1366.3,1356.0,1366.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.19/0.49 1390[3:Con:1389.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.19/0.49 1409[3:SpR:1312.0,33.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.19/0.49 1411[3:Rew:1384.0,1409.0] || -> equal(identity,sk_c1)**. % 0.19/0.49 1412[3:Rew:1411.0,347.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.19/0.49 1415[3:Rew:1411.0,183.0] || -> equal(multiply(u,sk_c1),u)**. % 0.19/0.49 1417[3:Rew:1312.0,1412.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.49 1418[3:Rew:1417.0,1312.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.49 1425[3:Rew:1417.0,1415.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.49 1426[3:Rew:1425.0,1390.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.49 1477[3:SpL:1418.0,1426.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.49 1478[3:Obv:1477.1] || -> . % 0.19/0.49 1479[2:Spt:1478.0,1.0,851.0] || equal(multiply(sk_c8,sk_c7),sk_c6)** -> . % 0.19/0.49 1480[2:Spt:1478.0,1.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.49 1482[2:MRR:26.1,1479.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.49 1483[2:MRR:11.1,1479.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.49 1485[2:MRR:21.0,1479.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.49 1486[2:MRR:16.0,1479.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.49 1487[2:MRR:6.0,1479.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.49 1492[2:SpR:1482.0,359.0] || -> equal(inverse(sk_c8),sk_c2)**. % 0.19/0.49 1502[2:SpR:1483.0,359.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.19/0.49 1515[2:SpR:1485.0,73.0] || -> equal(multiply(inverse(sk_c2),sk_c3),sk_c8)**. % 0.19/0.49 1517[2:Rew:1482.0,1515.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.49 1518[2:Rew:1486.0,1517.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.49 1519[2:Rew:1518.0,1480.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.49 1521[2:Rew:1518.0,1492.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.19/0.49 1522[2:Rew:1518.0,1485.0] || -> equal(multiply(sk_c2,sk_c7),sk_c3)**. % 0.19/0.49 1523[2:Rew:1518.0,1479.0] || equal(multiply(sk_c7,sk_c7),sk_c6)** -> . % 0.19/0.49 1524[2:Rew:1518.0,1486.0] || -> equal(multiply(sk_c7,sk_c3),sk_c7)**. % 0.19/0.49 1525[2:Rew:1518.0,1487.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.19/0.49 1530[2:Rew:1502.0,1521.0] || -> equal(sk_c2,sk_c1)**. % 0.19/0.49 1532[2:Rew:1530.0,1522.0] || -> equal(multiply(sk_c1,sk_c7),sk_c3)**. % 0.19/0.49 1533[2:Rew:1532.0,1525.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.49 1535[2:Rew:1533.0,1524.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.19/0.49 1536[2:Rew:1519.0,1535.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.49 1537[2:Rew:1536.0,1519.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.19/0.49 1539[2:Rew:1537.0,1523.0,1536.0,1523.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.49 1540[2:Obv:1539.0] || -> . % 0.19/0.49 % SZS output end Refutation % 0.19/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_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 prove_this_28 prove_this_29 prove_this_30 prove_this_31 left_identity left_inverse associativity % 0.19/0.49 %------------------------------------------------------------------------------