%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP335-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.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:54 EDT 2022 % Result : Unsatisfiable 0.22s 0.50s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.14 % Problem : GRP335-1 : TPTP v8.1.0. Released v2.5.0. % 0.09/0.14 % Command : run_spass %d %s % 0.14/0.36 % Computer : n026.cluster.edu % 0.14/0.36 % Model : x86_64 x86_64 % 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.36 % Memory : 8042.1875MB % 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.36 % CPULimit : 300 % 0.14/0.36 % WCLimit : 600 % 0.14/0.36 % DateTime : Tue Jun 14 07:39:51 EDT 2022 % 0.14/0.36 % CPUTime : % 0.22/0.50 % 0.22/0.50 SPASS V 3.9 % 0.22/0.50 SPASS beiseite: Proof found. % 0.22/0.50 % SZS status Theorem % 0.22/0.50 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.22/0.50 SPASS derived 958 clauses, backtracked 368 clauses, performed 13 splits and kept 777 clauses. % 0.22/0.50 SPASS allocated 63687 KBytes. % 0.22/0.50 SPASS spent 0:00:00.13 on the problem. % 0.22/0.50 0:00:00.03 for the input. % 0.22/0.50 0:00:00.00 for the FLOTTER CNF translation. % 0.22/0.50 0:00:00.01 for inferences. % 0.22/0.50 0:00:00.00 for the backtracking. % 0.22/0.50 0:00:00.07 for the reduction. % 0.22/0.50 % 0.22/0.50 % 0.22/0.50 Here is a proof with depth 4, length 382 : % 0.22/0.50 % SZS output start Refutation % 0.22/0.50 1[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c8),sk_c6). % 0.22/0.50 4[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7)** equal(multiply(sk_c7,sk_c8),sk_c6). % 0.22/0.50 5[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5)** equal(multiply(sk_c7,sk_c8),sk_c6). % 0.22/0.50 6[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.22/0.50 7[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.50 8[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.50 9[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.50 10[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.50 11[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.50 12[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.50 13[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.50 14[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 15[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c1),sk_c7)**. % 0.22/0.50 16[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 17[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 18[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c1),sk_c7)**. % 0.22/0.50 19[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.22/0.50 20[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.22/0.50 21[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.22/0.50 22[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.22/0.50 23[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.22/0.50 24[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.22/0.50 25[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.50 26[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 27[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c2),sk_c7)**. % 0.22/0.50 28[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 29[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 30[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c2),sk_c7)**. % 0.22/0.50 31[0:Inp] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(inverse(x),sk_c7) equal(multiply(u,sk_c8),y)*+ equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(x,sk_c7),sk_c6)** equal(multiply(sk_c8,y),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c8),sk_c6) -> . % 0.22/0.50 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.22/0.50 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.22/0.50 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.22/0.50 35[1:Spt:31.3,31.7] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c6)** -> . % 0.22/0.50 36[2:Spt:1.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.22/0.50 38[3:Spt:25.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.22/0.50 40[4:Spt:13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.22/0.50 43[1:SpL:32.0,35.1] || equal(inverse(identity),sk_c7)** equal(sk_c6,sk_c7) -> . % 0.22/0.50 44[5:Spt:19.1] || -> equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.22/0.50 46[5:SpL:44.0,35.1] || equal(inverse(sk_c2),sk_c7)** equal(sk_c6,sk_c8) -> . % 0.22/0.50 47[5:Rew:38.0,46.0] || equal(sk_c7,sk_c7) equal(sk_c6,sk_c8)** -> . % 0.22/0.50 48[5:Obv:47.0] || equal(sk_c6,sk_c8)** -> . % 0.22/0.50 49[6:Spt:7.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.50 51[6:SpL:49.0,35.1] || equal(inverse(sk_c1),sk_c7)** equal(sk_c6,sk_c6) -> . % 0.22/0.50 52[6:Obv:51.1] || equal(inverse(sk_c1),sk_c7)** -> . % 0.22/0.50 53[6:Rew:40.0,52.0] || equal(sk_c7,sk_c7)* -> . % 0.22/0.50 54[6:Obv:53.0] || -> . % 0.22/0.50 55[6:Spt:54.0,7.1,49.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.22/0.50 56[6:Spt:54.0,7.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.50 57[6:MRR:12.1,55.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.50 58[6:MRR:9.1,55.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.22/0.50 59[6:MRR:11.1,55.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 60[6:MRR:10.1,55.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 61[6:MRR:8.1,55.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 71[3:SpR:38.0,33.0] || -> equal(multiply(sk_c7,sk_c2),identity)**. % 0.22/0.50 72[4:SpR:40.0,33.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.22/0.50 73[6:SpR:57.0,33.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.22/0.50 74[6:SpR:58.0,33.0] || -> equal(multiply(sk_c8,sk_c3),identity)**. % 0.22/0.50 75[1:SpL:33.0,35.1] || equal(inverse(inverse(sk_c7)),sk_c7)** equal(identity,sk_c6) -> . % 0.22/0.50 88[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.22/0.50 90[6:SpR:73.0,34.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),multiply(identity,u))**. % 0.22/0.50 95[6:Rew:32.0,90.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),u)**. % 0.22/0.50 99[0:Rew:32.0,88.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.22/0.50 103[6:SpR:59.0,95.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.50 104[6:Rew:60.0,103.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 105[6:Rew:104.0,36.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.50 108[6:Rew:104.0,48.0] || equal(sk_c6,sk_c7)** -> . % 0.22/0.50 111[6:Rew:104.0,59.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.22/0.50 112[6:Rew:104.0,60.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.22/0.50 113[6:Rew:104.0,61.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.22/0.50 115[6:Rew:104.0,73.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.22/0.50 116[6:Rew:104.0,74.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.22/0.50 156[0:SpR:99.0,99.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.22/0.50 161[0:SpR:32.0,99.0] || -> equal(multiply(inverse(identity),u),u)**. % 0.22/0.50 162[0:SpR:33.0,99.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.22/0.50 163[3:SpR:71.0,99.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c2)**. % 0.22/0.50 164[4:SpR:72.0,99.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.22/0.50 165[6:SpR:105.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.22/0.50 166[6:SpR:112.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.22/0.50 167[6:SpR:115.0,99.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c4)**. % 0.22/0.50 168[6:SpR:116.0,99.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c3)**. % 0.22/0.50 179[4:Rew:163.0,164.0] || -> equal(sk_c2,sk_c1)**. % 0.22/0.50 185[4:Rew:179.0,163.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.22/0.50 187[6:Rew:33.0,166.0] || -> equal(identity,sk_c5)**. % 0.22/0.50 194[6:Rew:187.0,161.0] || -> equal(multiply(inverse(sk_c5),u),u)**. % 0.22/0.50 197[6:Rew:187.0,167.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c4)**. % 0.22/0.50 198[6:Rew:197.0,168.0,187.0,168.0] || -> equal(sk_c4,sk_c3)**. % 0.22/0.50 200[6:Rew:198.0,111.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.22/0.50 204[6:Rew:113.0,200.0] || -> equal(sk_c5,sk_c7)**. % 0.22/0.50 236[6:Rew:204.0,194.0] || -> equal(multiply(inverse(sk_c7),u),u)**. % 0.22/0.50 237[6:Rew:236.0,165.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.50 238[6:MRR:237.0,108.0] || -> . % 0.22/0.50 255[5:Spt:238.0,19.1,44.0] || equal(multiply(sk_c2,sk_c7),sk_c8)** -> . % 0.22/0.50 256[5:Spt:238.0,19.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.50 257[5:Rew:179.0,255.0] || equal(multiply(sk_c1,sk_c7),sk_c8)** -> . % 0.22/0.50 258[0:Rew:156.0,162.0] || -> equal(multiply(u,identity),u)**. % 0.22/0.50 259[4:Rew:258.0,185.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.22/0.50 261[4:Rew:12.1,24.1,179.0,24.1] || -> equal(inverse(sk_c4),sk_c8)** equal(sk_c6,sk_c8). % 0.22/0.50 262[4:Rew:261.1,12.1] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.22/0.50 263[4:Rew:9.1,21.1,179.0,21.1] || -> equal(inverse(sk_c3),sk_c8)** equal(sk_c6,sk_c8). % 0.22/0.50 264[4:Rew:263.1,9.1] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.22/0.50 265[5:MRR:262.1,257.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.50 266[5:MRR:264.1,257.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.22/0.50 269[4:Rew:11.1,23.1,179.0,23.1] || -> equal(multiply(sk_c4,sk_c8),sk_c5)** equal(sk_c6,sk_c8). % 0.22/0.50 270[4:Rew:269.1,11.1] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.22/0.50 271[4:Rew:10.1,22.1,179.0,22.1] || -> equal(multiply(sk_c8,sk_c5),sk_c7)** equal(sk_c6,sk_c8). % 0.22/0.50 272[4:Rew:271.1,10.1] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.22/0.50 273[4:Rew:8.1,20.1,179.0,20.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(sk_c6,sk_c8). % 0.22/0.50 274[4:Rew:273.1,8.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.22/0.50 275[5:MRR:270.1,257.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 276[5:MRR:272.1,257.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 277[5:MRR:274.1,257.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 291[2:SpR:36.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.22/0.50 293[4:Rew:259.0,291.0] || -> equal(multiply(sk_c1,sk_c6),sk_c8)**. % 0.22/0.50 300[5:SpR:275.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.22/0.50 302[5:Rew:265.0,300.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.50 303[5:Rew:276.0,302.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 304[5:Rew:303.0,256.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.50 306[5:Rew:303.0,266.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.22/0.50 309[5:Rew:303.0,257.0] || equal(multiply(sk_c1,sk_c7),sk_c7)** -> . % 0.22/0.50 311[5:Rew:303.0,276.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.22/0.50 312[5:Rew:303.0,277.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.22/0.50 317[5:Rew:303.0,293.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.22/0.50 334[5:SpR:311.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.22/0.50 336[5:Rew:259.0,334.0] || -> equal(multiply(sk_c1,sk_c7),sk_c5)**. % 0.22/0.50 337[5:Rew:336.0,309.0] || equal(sk_c5,sk_c7)** -> . % 0.22/0.50 339[5:SpR:312.0,99.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.22/0.50 341[5:Rew:304.0,339.0,306.0,339.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.50 347[5:Rew:341.0,317.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.22/0.50 349[5:Rew:336.0,347.0] || -> equal(sk_c5,sk_c7)**. % 0.22/0.50 350[5:MRR:349.0,337.0] || -> . % 0.22/0.50 352[4:Spt:350.0,13.0,40.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.22/0.50 353[4:Spt:350.0,13.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.50 354[3:Rew:258.0,163.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.22/0.50 355[3:Rew:354.0,291.0] || -> equal(multiply(sk_c2,sk_c6),sk_c8)**. % 0.22/0.50 356[4:MRR:18.1,352.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.50 357[4:MRR:15.1,352.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.22/0.50 358[4:MRR:17.0,352.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 359[4:MRR:16.0,352.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 360[4:MRR:14.0,352.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 368[3:SpR:354.0,99.0] || -> equal(multiply(sk_c2,multiply(sk_c7,u)),u)**. % 0.22/0.50 383[3:SpR:355.0,34.0] || -> equal(multiply(sk_c2,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.22/0.50 388[4:SpR:358.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.22/0.50 390[4:Rew:356.0,388.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.50 391[4:Rew:359.0,390.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 392[4:Rew:391.0,353.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.50 394[4:Rew:391.0,357.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.22/0.50 399[4:Rew:391.0,383.0] || -> equal(multiply(sk_c2,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.22/0.50 401[4:Rew:391.0,360.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.22/0.50 430[4:SpR:401.0,99.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.22/0.50 432[4:Rew:392.0,430.0,394.0,430.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.50 436[4:Rew:432.0,43.1] || equal(inverse(identity),sk_c7)** equal(sk_c7,sk_c7) -> . % 0.22/0.50 440[4:Rew:432.0,399.0] || -> equal(multiply(sk_c2,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.22/0.50 447[4:Obv:436.1] || equal(inverse(identity),sk_c7)** -> . % 0.22/0.50 448[4:Rew:368.0,440.0] || -> equal(multiply(sk_c7,u),u)**. % 0.22/0.50 449[4:Rew:448.0,71.0] || -> equal(identity,sk_c2)**. % 0.22/0.50 458[4:Rew:449.0,447.0] || equal(inverse(sk_c2),sk_c7)** -> . % 0.22/0.50 461[4:Rew:38.0,458.0] || equal(sk_c7,sk_c7)* -> . % 0.22/0.50 462[4:Obv:461.0] || -> . % 0.22/0.50 464[3:Spt:462.0,25.0,38.0] || equal(inverse(sk_c2),sk_c7)** -> . % 0.22/0.50 465[3:Spt:462.0,25.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.50 466[3:MRR:30.1,464.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.50 467[3:MRR:27.1,464.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.22/0.50 468[3:MRR:29.0,464.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 469[3:MRR:28.0,464.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 470[3:MRR:26.0,464.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 482[3:SpR:468.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.22/0.50 484[3:Rew:466.0,482.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.50 485[3:Rew:469.0,484.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 486[3:Rew:485.0,465.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.50 488[3:Rew:485.0,467.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.22/0.50 491[3:Rew:485.0,291.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.22/0.50 493[3:Rew:485.0,469.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.22/0.50 494[3:Rew:485.0,470.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.22/0.50 513[3:SpR:493.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.22/0.50 515[3:Rew:33.0,513.0] || -> equal(identity,sk_c5)**. % 0.22/0.50 516[3:Rew:515.0,258.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.50 520[3:Rew:515.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.22/0.50 521[3:Rew:515.0,75.1] || equal(inverse(inverse(sk_c7)),sk_c7)** equal(sk_c5,sk_c6) -> . % 0.22/0.50 526[3:SpR:494.0,99.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.22/0.50 528[3:Rew:486.0,526.0,488.0,526.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.50 532[3:Rew:528.0,491.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.22/0.50 535[3:Rew:528.0,521.1] || equal(inverse(inverse(sk_c7)),sk_c7)** equal(sk_c5,sk_c7) -> . % 0.22/0.50 536[3:Rew:520.0,532.0] || -> equal(sk_c5,sk_c7)**. % 0.22/0.50 539[3:Rew:536.0,516.0] || -> equal(multiply(u,sk_c7),u)**. % 0.22/0.50 543[3:Rew:539.0,494.0] || -> equal(sk_c3,sk_c7)**. % 0.22/0.50 545[3:Rew:543.0,488.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.22/0.50 558[3:Rew:536.0,535.1,545.0,535.0,545.0,535.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.22/0.50 559[3:Obv:558.1] || -> . % 0.22/0.50 562[2:Spt:559.0,1.1,36.0] || equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.22/0.50 563[2:Spt:559.0,1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.50 564[2:MRR:6.1,562.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.50 566[2:MRR:5.1,562.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 567[2:MRR:4.1,562.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 577[2:SpR:566.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.22/0.50 579[2:Rew:564.0,577.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.50 580[2:Rew:567.0,579.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 581[2:Rew:580.0,563.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.50 585[2:Rew:580.0,562.0] || equal(multiply(sk_c7,sk_c7),sk_c6)** -> . % 0.22/0.50 592[2:Rew:581.0,585.0] || equal(sk_c6,sk_c6)* -> . % 0.22/0.50 593[2:Obv:592.0] || -> . % 0.22/0.50 595[1:Spt:593.0,31.0,31.1,31.2,31.4,31.5,31.6,31.8,31.9,31.10] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),x)*+ equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,x),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c8),sk_c6) -> . % 0.22/0.50 596[1:EqR:595.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6) equal(multiply(sk_c7,sk_c8),sk_c6) -> . % 0.22/0.50 598[2:Spt:1.1] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.22/0.50 601[2:Rew:598.0,596.7] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6) equal(sk_c6,sk_c6) -> . % 0.22/0.50 602[2:Obv:601.7] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6) -> . % 0.22/0.50 606[2:SpR:598.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.22/0.50 608[3:Spt:13.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.50 611[3:Rew:608.0,602.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** equal(sk_c6,sk_c6) -> . % 0.22/0.50 612[3:Obv:611.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.22/0.50 616[3:SpR:608.0,99.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.22/0.50 618[4:Spt:30.1] || -> equal(inverse(sk_c2),sk_c7)**. % 0.22/0.50 621[5:Spt:18.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.22/0.50 622[5:SpR:621.0,99.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.22/0.50 627[6:Spt:12.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.50 629[6:SpR:627.0,99.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.22/0.50 631[6:Rew:621.0,629.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.22/0.50 633[6:SpR:631.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.22/0.50 635[6:Rew:33.0,633.0] || -> equal(identity,sk_c6)**. % 0.22/0.50 636[6:Rew:635.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.22/0.50 637[6:Rew:635.0,258.0] || -> equal(multiply(u,sk_c6),u)**. % 0.22/0.50 638[6:Rew:635.0,33.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.22/0.50 643[6:Rew:637.0,616.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.22/0.50 644[6:Rew:637.0,606.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.22/0.50 662[6:SpR:638.0,99.0] || -> equal(multiply(inverse(inverse(u)),sk_c6),u)**. % 0.22/0.50 663[6:SpR:638.0,637.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.22/0.50 665[6:SpR:618.0,638.0] || -> equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.22/0.50 670[6:Rew:637.0,662.0] || -> equal(inverse(inverse(u)),u)**. % 0.22/0.50 682[6:SpR:665.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c2)**. % 0.22/0.50 684[6:Rew:637.0,682.0,644.0,682.0] || -> equal(sk_c2,sk_c8)**. % 0.22/0.50 687[6:Rew:684.0,20.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c8). % 0.22/0.50 690[6:Rew:684.0,21.1] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.22/0.50 694[6:Rew:608.0,690.1] || -> equal(inverse(sk_c3),sk_c8)** equal(sk_c6,sk_c8). % 0.22/0.50 695[6:Rew:608.0,687.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(sk_c6,sk_c8). % 0.22/0.50 710[7:Spt:694.1] || -> equal(sk_c6,sk_c8)**. % 0.22/0.50 714[7:Rew:710.0,636.0] || -> equal(multiply(sk_c8,u),u)**. % 0.22/0.50 715[7:Rew:710.0,637.0] || -> equal(multiply(u,sk_c8),u)**. % 0.22/0.50 717[7:Rew:710.0,663.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.22/0.50 719[7:Rew:643.0,717.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 720[7:Rew:719.0,643.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.22/0.50 725[7:Rew:719.0,612.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.22/0.50 735[7:Rew:719.0,714.0] || -> equal(multiply(sk_c7,u),u)**. % 0.22/0.50 736[7:Rew:719.0,715.0] || -> equal(multiply(u,sk_c7),u)**. % 0.22/0.50 743[7:Rew:736.0,725.5,735.0,725.5,719.0,725.5,736.0,725.4,719.0,725.4,736.0,725.3,719.0,725.3,719.0,725.1] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c7)** equal(v,sk_c7) equal(w,sk_c7) equal(u,sk_c7) -> . % 0.22/0.50 744[7:Con:743.0] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.22/0.50 806[7:SpL:720.0,744.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.22/0.50 808[7:Obv:806.1] || -> . % 0.22/0.50 809[7:Spt:808.0,694.1,710.0] || equal(sk_c6,sk_c8)** -> . % 0.22/0.50 810[7:Spt:808.0,694.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.22/0.50 811[7:MRR:695.1,809.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 815[7:SpR:810.0,670.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.22/0.50 818[7:Rew:643.0,815.0] || -> equal(sk_c3,sk_c7)**. % 0.22/0.50 820[7:Rew:818.0,811.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.22/0.50 821[7:Rew:598.0,820.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.50 823[7:Rew:821.0,663.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.22/0.50 824[7:Rew:821.0,809.0] || equal(sk_c8,sk_c7)** -> . % 0.22/0.50 831[7:Rew:644.0,823.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 845[7:Rew:831.0,824.0] || equal(sk_c7,sk_c7)* -> . % 0.22/0.50 846[7:Obv:845.0] || -> . % 0.22/0.50 864[6:Spt:846.0,12.1,627.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.22/0.50 865[6:Spt:846.0,12.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.50 866[6:MRR:9.1,864.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.22/0.50 867[6:MRR:11.1,864.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 868[6:MRR:10.1,864.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 869[6:MRR:8.1,864.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 885[6:SpR:867.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.22/0.50 887[6:Rew:865.0,885.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.50 888[6:Rew:868.0,887.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 890[6:Rew:888.0,866.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.22/0.50 891[6:Rew:888.0,598.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.50 894[6:Rew:888.0,606.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.22/0.50 898[6:Rew:888.0,868.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.22/0.50 899[6:Rew:888.0,869.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.22/0.50 925[6:SpR:898.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.22/0.50 927[6:Rew:33.0,925.0] || -> equal(identity,sk_c5)**. % 0.22/0.50 928[6:Rew:927.0,32.0] || -> equal(multiply(sk_c5,u),u)**. % 0.22/0.50 929[6:Rew:927.0,258.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.50 931[6:Rew:927.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.22/0.50 936[6:SpR:899.0,99.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.22/0.50 938[6:Rew:891.0,936.0,890.0,936.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.50 940[6:Rew:938.0,864.0] || equal(multiply(sk_c1,sk_c7),sk_c7)** -> . % 0.22/0.50 941[6:Rew:938.0,894.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.22/0.50 943[6:Rew:931.0,941.0] || -> equal(sk_c5,sk_c7)**. % 0.22/0.50 946[6:Rew:943.0,928.0] || -> equal(multiply(sk_c7,u),u)**. % 0.22/0.50 947[6:Rew:943.0,929.0] || -> equal(multiply(u,sk_c7),u)**. % 0.22/0.50 956[6:Rew:946.0,622.0] || -> equal(multiply(sk_c1,u),u)**. % 0.22/0.50 960[6:Rew:947.0,940.0] || equal(sk_c1,sk_c7)** -> . % 0.22/0.50 993[6:SpR:956.0,947.0] || -> equal(sk_c1,sk_c7)**. % 0.22/0.50 995[6:MRR:993.0,960.0] || -> . % 0.22/0.50 997[5:Spt:995.0,18.1,621.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.22/0.50 998[5:Spt:995.0,18.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.50 999[5:MRR:15.1,997.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.22/0.50 1000[5:MRR:17.0,997.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.50 1001[5:MRR:16.0,997.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.50 1002[5:MRR:14.0,997.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.50 1014[5:SpR:1000.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.22/0.50 1016[5:Rew:998.0,1014.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.50 1017[5:Rew:1001.0,1016.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.50 1019[5:Rew:1017.0,999.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.22/0.50 1020[5:Rew:1017.0,608.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.50 1023[5:Rew:1017.0,616.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.22/0.50 1027[5:Rew:1017.0,1001.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.22/0.50 1028[5:Rew:1017.0,1002.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.22/0.50 1030[5:Rew:1017.0,612.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.22/0.50 1035[5:Rew:1017.0,1030.5,1017.0,1030.4,1017.0,1030.3,1017.0,1030.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c7)** -> . % 0.22/0.50 1036[5:Con:1035.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c7)** -> . % 0.22/0.50 1054[5:SpR:1027.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.22/0.50 1056[5:Rew:33.0,1054.0] || -> equal(identity,sk_c5)**. % 0.22/0.50 1057[5:Rew:1056.0,258.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.50 1058[5:Rew:1056.0,32.0] || -> equal(multiply(sk_c5,u),u)**. % 0.22/0.50 1059[5:Rew:1056.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.22/0.50 1064[5:SpR:1028.0,99.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.22/0.50 1066[5:Rew:1020.0,1064.0,1019.0,1064.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.50 1068[5:Rew:1066.0,1023.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.22/0.50 1070[5:Rew:1059.0,1068.0] || -> equal(sk_c5,sk_c7)**. % 0.22/0.50 1073[5:Rew:1070.0,1057.0] || -> equal(multiply(u,sk_c7),u)**. % 0.22/0.50 1074[5:Rew:1070.0,1058.0] || -> equal(multiply(sk_c7,u),u)**. % 0.22/0.50 1077[5:Rew:1073.0,1028.0] || -> equal(sk_c3,sk_c7)**. % 0.22/0.50 1080[5:Rew:1073.0,1036.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(sk_c7,u),sk_c7)** -> . % 0.22/0.50 1082[5:Rew:1077.0,1019.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.22/0.50 1093[5:Rew:1074.0,1080.3,1073.0,1080.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(v,sk_c7) equal(u,sk_c7) -> . % 0.22/0.51 1094[5:Con:1093.0] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.22/0.51 1163[5:SpL:1082.0,1094.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.22/0.51 1165[5:Obv:1163.1] || -> . % 0.22/0.51 1166[4:Spt:1165.0,30.1,618.0] || equal(inverse(sk_c2),sk_c7)** -> . % 0.22/0.51 1167[4:Spt:1165.0,30.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.51 1168[4:MRR:27.1,1166.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.22/0.51 1169[4:MRR:29.0,1166.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.51 1170[4:MRR:28.0,1166.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.51 1171[4:MRR:26.0,1166.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.22/0.51 1183[4:SpR:1169.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.22/0.51 1185[4:Rew:1167.0,1183.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.51 1186[4:Rew:1170.0,1185.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.51 1188[4:Rew:1186.0,1168.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.22/0.51 1189[4:Rew:1186.0,598.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.51 1192[4:Rew:1186.0,606.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.22/0.51 1196[4:Rew:1186.0,1170.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.22/0.51 1197[4:Rew:1186.0,1171.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.22/0.51 1199[4:Rew:1186.0,612.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.22/0.51 1204[4:Rew:1186.0,1199.5,1186.0,1199.4,1186.0,1199.3,1186.0,1199.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c7)** -> . % 0.22/0.51 1205[4:Con:1204.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c7)** -> . % 0.22/0.51 1223[4:SpR:1196.0,99.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.22/0.51 1225[4:Rew:33.0,1223.0] || -> equal(identity,sk_c5)**. % 0.22/0.51 1226[4:Rew:1225.0,32.0] || -> equal(multiply(sk_c5,u),u)**. % 0.22/0.51 1227[4:Rew:1225.0,258.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.51 1229[4:Rew:1225.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.22/0.51 1234[4:SpR:1197.0,99.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.22/0.51 1236[4:Rew:1189.0,1234.0,1188.0,1234.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.51 1238[4:Rew:1236.0,1192.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.22/0.51 1240[4:Rew:1229.0,1238.0] || -> equal(sk_c5,sk_c7)**. % 0.22/0.51 1243[4:Rew:1240.0,1226.0] || -> equal(multiply(sk_c7,u),u)**. % 0.22/0.51 1244[4:Rew:1240.0,1227.0] || -> equal(multiply(u,sk_c7),u)**. % 0.22/0.51 1250[4:Rew:1243.0,1205.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(u,sk_c7),sk_c7)** -> . % 0.22/0.51 1253[4:Rew:1244.0,1197.0] || -> equal(sk_c3,sk_c7)**. % 0.22/0.51 1255[4:Rew:1253.0,1188.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.22/0.51 1262[4:Con:1250.0] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.22/0.51 1263[4:Rew:1244.0,1262.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.22/0.51 1306[4:SpL:1255.0,1263.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.22/0.51 1308[4:Obv:1306.1] || -> . % 0.22/0.51 1309[3:Spt:1308.0,13.1,608.0] || equal(multiply(sk_c8,sk_c7),sk_c6)** -> . % 0.22/0.51 1310[3:Spt:1308.0,13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.22/0.51 1311[3:MRR:25.1,1309.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.22/0.51 1313[3:MRR:19.0,1309.0] || -> equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.22/0.51 1326[3:SpR:1313.0,99.0] || -> equal(multiply(inverse(sk_c2),sk_c8),sk_c7)**. % 0.22/0.51 1328[3:Rew:598.0,1326.0,1311.0,1326.0] || -> equal(sk_c6,sk_c7)**. % 0.22/0.51 1331[3:Rew:1328.0,606.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.22/0.51 1332[3:Rew:1328.0,1309.0] || equal(multiply(sk_c8,sk_c7),sk_c7)** -> . % 0.22/0.51 1336[3:Rew:33.0,1331.0] || -> equal(identity,sk_c8)**. % 0.22/0.51 1338[3:Rew:1336.0,32.0] || -> equal(multiply(sk_c8,u),u)**. % 0.22/0.51 1341[3:Rew:1338.0,1332.0] || equal(sk_c7,sk_c7)* -> . % 0.22/0.51 1342[3:Obv:1341.0] || -> . % 0.22/0.51 1345[2:Spt:1342.0,1.1,598.0] || equal(multiply(sk_c7,sk_c8),sk_c6)** -> . % 0.22/0.51 1346[2:Spt:1342.0,1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.22/0.51 1347[2:MRR:6.1,1345.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.22/0.51 1349[2:MRR:5.1,1345.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.22/0.51 1350[2:MRR:4.1,1345.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.22/0.51 1360[2:SpR:1349.0,99.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.22/0.51 1362[2:Rew:1347.0,1360.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.22/0.51 1363[2:Rew:1350.0,1362.0] || -> equal(sk_c8,sk_c7)**. % 0.22/0.51 1364[2:Rew:1363.0,1346.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.22/0.51 1368[2:Rew:1363.0,1345.0] || equal(multiply(sk_c7,sk_c7),sk_c6)** -> . % 0.22/0.51 1375[2:Rew:1364.0,1368.0] || equal(sk_c6,sk_c6)* -> . % 0.22/0.51 1376[2:Obv:1375.0] || -> . % 0.22/0.51 % SZS output end Refutation % 0.22/0.51 Formulae used in the proof : prove_this_1 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.22/0.51 %------------------------------------------------------------------------------