%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP333-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n017.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.20s 0.47s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRP333-1 : TPTP v8.1.0. Released v2.5.0. % 0.03/0.13 % Command : run_spass %d %s % 0.14/0.34 % Computer : n017.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Mon Jun 13 08:05:22 EDT 2022 % 0.14/0.34 % CPUTime : % 0.20/0.47 % 0.20/0.47 SPASS V 3.9 % 0.20/0.47 SPASS beiseite: Proof found. % 0.20/0.47 % SZS status Theorem % 0.20/0.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.47 SPASS derived 783 clauses, backtracked 237 clauses, performed 9 splits and kept 570 clauses. % 0.20/0.47 SPASS allocated 63591 KBytes. % 0.20/0.47 SPASS spent 0:00:00.12 on the problem. % 0.20/0.47 0:00:00.03 for the input. % 0.20/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.47 0:00:00.01 for inferences. % 0.20/0.47 0:00:00.00 for the backtracking. % 0.20/0.47 0:00:00.05 for the reduction. % 0.20/0.47 % 0.20/0.47 % 0.20/0.47 Here is a proof with depth 5, length 301 : % 0.20/0.47 % SZS output start Refutation % 0.20/0.47 1[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 2[0:Inp] || -> equal(multiply(sk_c3,sk_c7),sk_c6)** equal(multiply(sk_c1,sk_c6),sk_c7). % 0.20/0.47 3[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 4[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5)** equal(multiply(sk_c1,sk_c6),sk_c7). % 0.20/0.47 5[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 6[0:Inp] || -> equal(inverse(sk_c1),sk_c6) equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.47 7[0:Inp] || -> equal(inverse(sk_c3),sk_c7)** equal(inverse(sk_c1),sk_c6). % 0.20/0.47 8[0:Inp] || -> equal(inverse(sk_c1),sk_c6) equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 9[0:Inp] || -> equal(inverse(sk_c4),sk_c6)** equal(inverse(sk_c1),sk_c6). % 0.20/0.47 10[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.47 11[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 12[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 13[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 14[0:Inp] || -> equal(multiply(sk_c3,sk_c7),sk_c6) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.47 15[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.47 17[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.47 18[0:Inp] || equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(u,sk_c6),sk_c7)** equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(v,sk_c5),sk_c6)** equal(multiply(w,sk_c7),sk_c6)** equal(inverse(w),sk_c7) equal(multiply(x,sk_c6),sk_c5)** equal(inverse(x),sk_c6) -> . % 0.20/0.47 19[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.20/0.47 20[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.20/0.47 21[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.20/0.47 22[0:Rew:1.0,18.0] || equal(sk_c5,sk_c5) equal(multiply(u,sk_c6),sk_c7)** equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(v,sk_c5),sk_c6)** equal(multiply(w,sk_c7),sk_c6)** equal(inverse(w),sk_c7) equal(multiply(x,sk_c6),sk_c5)** equal(inverse(x),sk_c6) -> . % 0.20/0.47 23[0:Obv:22.0] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(inverse(x),sk_c6) equal(multiply(u,sk_c6),sk_c5)**+ equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c5),sk_c6)** equal(multiply(x,sk_c6),sk_c7)** -> . % 0.20/0.47 24[1:Spt:23.3,23.7] || equal(inverse(u),sk_c6) equal(multiply(u,sk_c6),sk_c7)** -> . % 0.20/0.47 25[2:Spt:11.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 28[3:Spt:13.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 30[4:Spt:12.1] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 32[4:SpL:30.0,24.1] || equal(inverse(sk_c4),sk_c6)** equal(sk_c5,sk_c7) -> . % 0.20/0.47 33[4:Rew:28.0,32.0] || equal(sk_c6,sk_c6)* equal(sk_c5,sk_c7) -> . % 0.20/0.47 34[4:Obv:33.0] || equal(sk_c5,sk_c7)** -> . % 0.20/0.47 35[5:Spt:10.1] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.47 38[1:SpL:19.0,24.1] || equal(inverse(identity),sk_c6)** equal(sk_c6,sk_c7) -> . % 0.20/0.47 40[2:SpR:25.0,20.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.20/0.47 41[3:SpR:28.0,20.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.20/0.47 42[1:SpL:20.0,24.1] || equal(inverse(inverse(sk_c6)),sk_c6)** equal(identity,sk_c7) -> . % 0.20/0.47 45[4:SpR:30.0,21.0] || -> equal(multiply(sk_c4,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.20/0.47 46[0:SpR:1.0,21.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c5,u))**. % 0.20/0.47 49[0:SpR:20.0,21.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.47 51[0:Rew:19.0,49.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.47 53[2:SpR:40.0,21.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),multiply(identity,u))**. % 0.20/0.47 55[2:Rew:19.0,53.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.20/0.47 61[5:SpR:35.0,55.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 68[0:SpR:51.0,51.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.47 70[4:SpR:30.0,51.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c6)**. % 0.20/0.47 71[0:SpR:1.0,51.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 74[0:SpR:20.0,51.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.47 78[5:SpR:61.0,51.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.47 79[3:SpR:41.0,51.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c4)**. % 0.20/0.47 82[4:Rew:28.0,70.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 84[5:Rew:20.0,78.0] || -> equal(sk_c6,identity)**. % 0.20/0.47 89[5:Rew:84.0,35.0] || -> equal(multiply(sk_c3,sk_c7),identity)**. % 0.20/0.47 90[5:Rew:84.0,41.0] || -> equal(multiply(identity,sk_c4),identity)**. % 0.20/0.47 98[5:Rew:84.0,46.0] || -> equal(multiply(identity,multiply(sk_c7,u)),multiply(sk_c5,u))**. % 0.20/0.47 102[5:Rew:84.0,82.0] || -> equal(multiply(identity,sk_c5),identity)**. % 0.20/0.47 105[5:Rew:19.0,90.0] || -> equal(identity,sk_c4)**. % 0.20/0.47 106[5:Rew:105.0,19.0] || -> equal(multiply(sk_c4,u),u)**. % 0.20/0.47 108[5:Rew:105.0,40.0] || -> equal(multiply(sk_c7,sk_c3),sk_c4)**. % 0.20/0.47 114[5:Rew:105.0,89.0] || -> equal(multiply(sk_c3,sk_c7),sk_c4)**. % 0.20/0.47 117[5:Rew:105.0,102.0] || -> equal(multiply(sk_c4,sk_c5),sk_c4)**. % 0.20/0.47 118[5:Rew:106.0,117.0] || -> equal(sk_c4,sk_c5)**. % 0.20/0.47 119[5:Rew:118.0,105.0] || -> equal(identity,sk_c5)**. % 0.20/0.47 124[5:Rew:118.0,106.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.47 125[5:Rew:118.0,108.0] || -> equal(multiply(sk_c7,sk_c3),sk_c5)**. % 0.20/0.47 127[5:Rew:118.0,114.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.20/0.47 144[5:Rew:124.0,98.0,119.0,98.0,124.0,98.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 147[5:Rew:144.0,125.0] || -> equal(sk_c3,sk_c5)**. % 0.20/0.47 149[5:Rew:147.0,127.0] || -> equal(multiply(sk_c5,sk_c7),sk_c5)**. % 0.20/0.47 155[5:Rew:124.0,149.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 156[5:MRR:155.0,34.0] || -> . % 0.20/0.47 163[5:Spt:156.0,10.1,35.0] || equal(multiply(sk_c3,sk_c7),sk_c6)** -> . % 0.20/0.47 164[5:Spt:156.0,10.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 165[0:Rew:68.0,74.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.47 166[3:Rew:165.0,79.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.20/0.47 168[3:Rew:166.0,71.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.20/0.47 170[5:MRR:6.1,163.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.47 171[5:MRR:14.0,163.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.47 172[5:MRR:2.0,163.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 173[3:Rew:28.0,42.0,166.0,42.0] || equal(sk_c6,sk_c6)* equal(identity,sk_c7) -> . % 0.20/0.47 174[3:Obv:173.0] || equal(identity,sk_c7)** -> . % 0.20/0.47 181[3:SpR:166.0,51.0] || -> equal(multiply(sk_c4,multiply(sk_c6,u)),u)**. % 0.20/0.47 183[4:Rew:45.0,181.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.47 184[4:Rew:183.0,46.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.20/0.47 205[5:SpR:171.0,21.0] || -> equal(multiply(sk_c2,multiply(sk_c5,u)),multiply(sk_c6,u))**. % 0.20/0.47 209[5:Rew:183.0,205.0] || -> equal(multiply(sk_c6,u),multiply(sk_c2,u))**. % 0.20/0.47 210[5:Rew:209.0,1.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.20/0.47 211[5:Rew:209.0,41.0] || -> equal(multiply(sk_c2,sk_c4),identity)**. % 0.20/0.47 215[5:Rew:209.0,184.0] || -> equal(multiply(sk_c2,multiply(sk_c7,u)),u)**. % 0.20/0.47 224[3:SpR:168.0,21.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.20/0.47 235[5:SpR:172.0,51.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.20/0.47 237[5:Rew:170.0,235.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.47 238[5:Rew:210.0,237.0,209.0,237.0] || -> equal(sk_c6,sk_c5)**. % 0.20/0.47 240[5:Rew:238.0,28.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.20/0.47 249[5:Rew:238.0,209.0] || -> equal(multiply(sk_c2,u),multiply(sk_c5,u))**. % 0.20/0.47 254[5:Rew:183.0,249.0] || -> equal(multiply(sk_c2,u),u)**. % 0.20/0.47 256[5:Rew:254.0,215.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 258[5:Rew:254.0,211.0] || -> equal(identity,sk_c4)**. % 0.20/0.47 262[5:Rew:258.0,40.0] || -> equal(multiply(sk_c7,sk_c3),sk_c4)**. % 0.20/0.47 275[5:Rew:256.0,262.0] || -> equal(sk_c4,sk_c3)**. % 0.20/0.47 276[5:Rew:275.0,240.0] || -> equal(inverse(sk_c3),sk_c5)**. % 0.20/0.47 280[5:Rew:25.0,276.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 281[5:MRR:280.0,34.0] || -> . % 0.20/0.47 293[4:Spt:281.0,12.1,30.0] || equal(multiply(sk_c4,sk_c6),sk_c5)** -> . % 0.20/0.47 294[4:Spt:281.0,12.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 296[4:MRR:8.1,293.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.47 298[4:MRR:4.0,293.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 330[4:SpR:298.0,51.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.20/0.47 332[4:Rew:1.0,330.0,296.0,330.0] || -> equal(sk_c6,sk_c5)**. % 0.20/0.47 334[4:Rew:332.0,166.0] || -> equal(inverse(sk_c5),sk_c4)**. % 0.20/0.47 343[4:Rew:332.0,181.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),u)**. % 0.20/0.47 353[4:Rew:224.0,343.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 354[4:Rew:353.0,40.0] || -> equal(identity,sk_c3)**. % 0.20/0.47 358[4:Rew:354.0,174.0] || equal(sk_c3,sk_c7)** -> . % 0.20/0.47 362[4:Rew:354.0,20.0] || -> equal(multiply(inverse(u),u),sk_c3)**. % 0.20/0.47 401[4:SpR:334.0,362.0] || -> equal(multiply(sk_c4,sk_c5),sk_c3)**. % 0.20/0.47 405[4:Rew:168.0,401.0] || -> equal(sk_c3,sk_c7)**. % 0.20/0.47 406[4:MRR:405.0,358.0] || -> . % 0.20/0.47 410[3:Spt:406.0,13.0,28.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.20/0.47 411[3:Spt:406.0,13.1] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 412[3:MRR:9.0,410.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.47 413[3:MRR:17.0,410.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.47 414[3:MRR:5.0,410.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 428[3:SpR:413.0,51.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.20/0.47 430[3:Rew:411.0,428.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 432[3:SpR:414.0,51.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.20/0.47 434[3:Rew:1.0,432.0,412.0,432.0] || -> equal(sk_c6,sk_c5)**. % 0.20/0.47 441[3:Rew:434.0,71.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c7)**. % 0.20/0.47 443[3:Rew:434.0,38.0] || equal(inverse(identity),sk_c5)** equal(sk_c6,sk_c7) -> . % 0.20/0.47 449[3:Rew:434.0,430.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)**. % 0.20/0.47 451[3:Rew:20.0,441.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 452[3:Rew:451.0,40.0] || -> equal(multiply(sk_c7,sk_c3),sk_c7)**. % 0.20/0.47 453[3:Rew:451.0,19.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 455[3:Rew:451.0,20.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.20/0.47 458[3:Rew:453.0,452.0] || -> equal(sk_c3,sk_c7)**. % 0.20/0.47 460[3:Rew:458.0,25.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 467[3:Rew:434.0,443.1,460.0,443.0,451.0,443.0] || equal(sk_c5,sk_c7)** equal(sk_c5,sk_c7)** -> . % 0.20/0.47 468[3:Obv:467.0] || equal(sk_c5,sk_c7)** -> . % 0.20/0.47 493[3:SpR:449.0,51.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c5)**. % 0.20/0.47 495[3:Rew:455.0,493.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 496[3:MRR:495.0,468.0] || -> . % 0.20/0.47 497[2:Spt:496.0,11.0,25.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.20/0.47 498[2:Spt:496.0,11.1] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 499[2:MRR:7.0,497.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.47 500[2:MRR:15.0,497.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.47 501[2:MRR:3.0,497.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 510[2:SpR:500.0,51.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.20/0.47 512[2:Rew:498.0,510.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 514[2:SpR:501.0,51.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.20/0.47 516[2:Rew:1.0,514.0,499.0,514.0] || -> equal(sk_c6,sk_c5)**. % 0.20/0.47 517[2:Rew:516.0,498.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.20/0.47 520[2:Rew:516.0,500.0] || -> equal(multiply(sk_c2,sk_c5),sk_c5)**. % 0.20/0.47 522[2:Rew:516.0,71.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c7)**. % 0.20/0.47 523[2:Rew:516.0,38.0] || equal(inverse(identity),sk_c5)** equal(sk_c6,sk_c7) -> . % 0.20/0.47 530[2:Rew:516.0,512.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)**. % 0.20/0.47 532[2:Rew:20.0,522.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 533[2:Rew:532.0,165.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 536[2:Rew:532.0,20.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.20/0.47 538[2:Rew:516.0,523.1,532.0,523.0] || equal(inverse(sk_c7),sk_c5)** equal(sk_c5,sk_c7) -> . % 0.20/0.47 560[2:SpR:530.0,51.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c5)**. % 0.20/0.47 562[2:Rew:536.0,560.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 565[2:Rew:562.0,517.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.47 566[2:Rew:562.0,520.0] || -> equal(multiply(sk_c2,sk_c7),sk_c7)**. % 0.20/0.47 573[2:Rew:562.0,538.0] || equal(inverse(sk_c7),sk_c7)** equal(sk_c5,sk_c7) -> . % 0.20/0.47 577[2:Rew:533.0,566.0] || -> equal(sk_c2,sk_c7)**. % 0.20/0.47 578[2:Rew:577.0,565.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 589[2:Rew:562.0,573.1,578.0,573.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.47 590[2:Obv:589.1] || -> . % 0.20/0.47 593[1:Spt:590.0,23.0,23.1,23.2,23.4,23.5,23.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c5),sk_c6)** -> . % 0.20/0.47 595[2:Spt:13.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 596[2:SpR:595.0,51.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),u)**. % 0.20/0.47 598[3:Spt:7.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 599[3:SpR:598.0,51.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.20/0.47 604[4:Spt:10.1] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.47 605[4:SpR:604.0,21.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.20/0.47 606[4:SpR:604.0,51.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c7)**. % 0.20/0.47 608[4:Rew:598.0,606.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 609[5:Spt:8.1] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 611[5:SpR:609.0,51.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c6)**. % 0.20/0.47 613[5:SpL:609.0,593.3] || equal(inverse(sk_c4),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(sk_c5,sk_c5) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 614[5:Rew:595.0,611.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 615[5:Obv:613.3] || equal(inverse(sk_c4),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 616[5:Rew:595.0,615.0] || equal(sk_c6,sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 617[5:Obv:616.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 619[4:SpR:608.0,51.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.47 621[4:Rew:20.0,619.0] || -> equal(sk_c6,identity)**. % 0.20/0.47 622[4:Rew:621.0,595.0] || -> equal(inverse(sk_c4),identity)**. % 0.20/0.47 623[4:Rew:621.0,1.0] || -> equal(multiply(identity,sk_c7),sk_c5)**. % 0.20/0.47 624[4:Rew:621.0,604.0] || -> equal(multiply(sk_c3,sk_c7),identity)**. % 0.20/0.47 625[5:Rew:621.0,609.0] || -> equal(multiply(sk_c4,identity),sk_c5)**. % 0.20/0.47 629[4:Rew:621.0,596.0] || -> equal(multiply(identity,multiply(sk_c4,u)),u)**. % 0.20/0.47 630[4:Rew:621.0,605.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),multiply(identity,u))**. % 0.20/0.47 632[5:Rew:621.0,614.0] || -> equal(multiply(identity,sk_c5),identity)**. % 0.20/0.47 633[5:Rew:621.0,617.1] || equal(inverse(u),sk_c7) equal(inverse(v),identity) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 634[4:Rew:19.0,623.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.47 635[5:Rew:165.0,625.0,634.0,625.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.47 636[5:Rew:635.0,622.0] || -> equal(inverse(sk_c7),identity)**. % 0.20/0.47 637[5:Rew:19.0,632.0,634.0,632.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 639[5:Rew:637.0,165.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 642[5:Rew:637.0,621.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 644[5:Rew:637.0,636.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 656[5:Rew:639.0,633.3,634.0,633.3,642.0,633.3,639.0,633.2,642.0,633.2,637.0,633.1] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) -> . % 0.20/0.47 657[5:Con:656.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.47 715[5:SpL:644.0,657.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.47 717[5:Obv:715.1] || -> . % 0.20/0.47 718[5:Spt:717.0,8.1,609.0] || equal(multiply(sk_c4,sk_c6),sk_c5)** -> . % 0.20/0.47 719[5:Spt:717.0,8.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.47 720[5:Rew:621.0,719.0] || -> equal(inverse(sk_c1),identity)**. % 0.20/0.47 722[5:Rew:634.0,718.0] || equal(multiply(sk_c4,sk_c6),sk_c7)** -> . % 0.20/0.47 723[5:Rew:165.0,722.0,621.0,722.0] || equal(sk_c4,sk_c7)** -> . % 0.20/0.47 724[4:Rew:19.0,629.0] || -> equal(multiply(sk_c4,u),u)**. % 0.20/0.47 729[4:Rew:19.0,630.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),u)**. % 0.20/0.47 732[4:Rew:634.0,4.0] || -> equal(multiply(sk_c4,sk_c6),sk_c7)** equal(multiply(sk_c1,sk_c6),sk_c7). % 0.20/0.47 733[4:Rew:165.0,732.1,621.0,732.1,621.0,732.0,724.0,732.0] || -> equal(identity,sk_c7)** equal(sk_c1,sk_c7). % 0.20/0.47 744[5:SpR:720.0,51.0] || -> equal(multiply(identity,multiply(sk_c1,u)),u)**. % 0.20/0.47 746[5:Rew:19.0,744.0] || -> equal(multiply(sk_c1,u),u)**. % 0.20/0.47 764[4:SpR:724.0,165.0] || -> equal(identity,sk_c4)**. % 0.20/0.47 770[4:Rew:764.0,624.0] || -> equal(multiply(sk_c3,sk_c7),sk_c4)**. % 0.20/0.48 775[4:Rew:764.0,733.0] || -> equal(sk_c4,sk_c7)** equal(sk_c1,sk_c7). % 0.20/0.48 780[5:MRR:775.0,723.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.48 781[5:Rew:780.0,746.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.48 783[5:Rew:781.0,729.0] || -> equal(multiply(sk_c3,u),u)**. % 0.20/0.48 785[5:Rew:783.0,770.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.48 786[5:MRR:785.0,723.0] || -> . % 0.20/0.48 792[4:Spt:786.0,10.1,604.0] || equal(multiply(sk_c3,sk_c7),sk_c6)** -> . % 0.20/0.48 793[4:Spt:786.0,10.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.48 794[4:MRR:6.1,792.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.48 795[4:MRR:14.0,792.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.48 796[4:MRR:2.0,792.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.48 807[4:SpR:795.0,51.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.20/0.48 809[4:Rew:793.0,807.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.48 811[4:SpR:796.0,51.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.20/0.48 813[4:Rew:1.0,811.0,794.0,811.0] || -> equal(sk_c6,sk_c5)**. % 0.20/0.48 820[4:Rew:813.0,71.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c7)**. % 0.20/0.48 821[4:Rew:813.0,792.0] || equal(multiply(sk_c3,sk_c7),sk_c5)** -> . % 0.20/0.48 828[4:Rew:813.0,809.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)**. % 0.20/0.48 830[4:Rew:20.0,820.0] || -> equal(identity,sk_c7)**. % 0.20/0.48 832[4:Rew:830.0,19.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.48 833[4:Rew:830.0,20.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.20/0.48 835[4:Rew:832.0,599.0] || -> equal(multiply(sk_c3,u),u)**. % 0.20/0.48 836[4:Rew:835.0,821.0] || equal(sk_c5,sk_c7)** -> . % 0.20/0.48 860[4:SpR:828.0,51.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c5)**. % 0.20/0.48 862[4:Rew:833.0,860.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.48 863[4:MRR:862.0,836.0] || -> . % 0.20/0.48 864[3:Spt:863.0,7.0,598.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.20/0.48 865[3:Spt:863.0,7.1] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.48 866[3:MRR:11.0,864.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.48 867[3:MRR:15.0,864.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.48 868[3:MRR:3.0,864.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.48 879[3:SpR:867.0,51.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.20/0.48 881[3:Rew:866.0,879.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.48 883[3:SpR:868.0,51.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.20/0.48 885[3:Rew:1.0,883.0,865.0,883.0] || -> equal(sk_c6,sk_c5)**. % 0.20/0.48 888[3:Rew:885.0,866.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.20/0.48 890[3:Rew:885.0,867.0] || -> equal(multiply(sk_c2,sk_c5),sk_c5)**. % 0.20/0.48 892[3:Rew:885.0,71.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c7)**. % 0.20/0.48 895[3:Rew:885.0,593.0] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c5),sk_c6)** -> . % 0.20/0.48 899[3:Rew:885.0,881.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)**. % 0.20/0.48 901[3:Rew:20.0,892.0] || -> equal(identity,sk_c7)**. % 0.20/0.48 903[3:Rew:901.0,165.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.48 905[3:Rew:901.0,20.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.20/0.48 908[3:Rew:885.0,895.5,903.0,895.4,885.0,895.4,885.0,895.3,885.0,895.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7)** equal(inverse(w),sk_c5) equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) equal(multiply(w,sk_c5),sk_c5)** -> . % 0.20/0.48 909[3:Con:908.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) -> . % 0.20/0.48 929[3:SpR:899.0,51.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c5)**. % 0.20/0.48 931[3:Rew:905.0,929.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.48 933[3:Rew:931.0,888.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.48 936[3:Rew:931.0,890.0] || -> equal(multiply(sk_c2,sk_c7),sk_c7)**. % 0.20/0.48 944[3:Rew:931.0,909.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) -> . % 0.20/0.48 945[3:Rew:903.0,936.0] || -> equal(sk_c2,sk_c7)**. % 0.20/0.48 946[3:Rew:945.0,933.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.48 956[3:Rew:931.0,944.3,903.0,944.2,931.0,944.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) -> . % 0.20/0.48 957[3:Con:956.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.48 1022[3:SpL:946.0,957.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.48 1024[3:Obv:1022.1] || -> . % 0.20/0.48 1025[2:Spt:1024.0,13.0,595.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.20/0.48 1026[2:Spt:1024.0,13.1] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.48 1027[2:MRR:9.0,1025.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.48 1028[2:MRR:17.0,1025.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.48 1029[2:MRR:5.0,1025.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.48 1038[2:SpR:1028.0,51.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c5)**. % 0.20/0.48 1040[2:Rew:1026.0,1038.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.48 1042[2:SpR:1029.0,51.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.20/0.48 1044[2:Rew:1.0,1042.0,1027.0,1042.0] || -> equal(sk_c6,sk_c5)**. % 0.20/0.48 1045[2:Rew:1044.0,1026.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.20/0.48 1049[2:Rew:1044.0,1028.0] || -> equal(multiply(sk_c2,sk_c5),sk_c5)**. % 0.20/0.48 1051[2:Rew:1044.0,71.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c7)**. % 0.20/0.48 1053[2:Rew:1044.0,593.0] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c5),sk_c6)** -> . % 0.20/0.48 1057[2:Rew:1044.0,1040.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)**. % 0.20/0.48 1059[2:Rew:20.0,1051.0] || -> equal(identity,sk_c7)**. % 0.20/0.48 1060[2:Rew:1059.0,165.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.48 1062[2:Rew:1059.0,20.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.20/0.48 1066[2:Rew:1044.0,1053.5,1060.0,1053.4,1044.0,1053.4,1044.0,1053.3,1044.0,1053.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7)** equal(inverse(w),sk_c5) equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) equal(multiply(w,sk_c5),sk_c5)** -> . % 0.20/0.48 1067[2:Con:1066.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) -> . % 0.20/0.48 1085[2:SpR:1057.0,51.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c5)**. % 0.20/0.48 1087[2:Rew:1062.0,1085.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.48 1089[2:Rew:1087.0,1045.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.48 1092[2:Rew:1087.0,1049.0] || -> equal(multiply(sk_c2,sk_c7),sk_c7)**. % 0.20/0.48 1099[2:Rew:1087.0,1067.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) -> . % 0.20/0.48 1100[2:Rew:1060.0,1092.0] || -> equal(sk_c2,sk_c7)**. % 0.20/0.48 1101[2:Rew:1100.0,1089.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.48 1110[2:Rew:1087.0,1099.3,1060.0,1099.2,1087.0,1099.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) -> . % 0.20/0.48 1111[2:Con:1110.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.48 1151[2:SpL:1101.0,1111.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.48 1153[2:Obv:1151.1] || -> . % 0.20/0.48 % SZS output end Refutation % 0.20/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_17 prove_this_18 left_identity left_inverse associativity % 0.20/0.48 %------------------------------------------------------------------------------