%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP345-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.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:57 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.10/0.13 % Problem : GRP345-1 : TPTP v8.1.0. Released v2.5.0. % 0.10/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n025.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Tue Jun 14 12:12:09 EDT 2022 % 0.13/0.35 % 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/sandbox2/benchmark/theBenchmark.p % 0.20/0.47 SPASS derived 623 clauses, backtracked 295 clauses, performed 11 splits and kept 533 clauses. % 0.20/0.47 SPASS allocated 63539 KBytes. % 0.20/0.47 SPASS spent 0:00:00.11 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.00 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 4, length 260 : % 0.20/0.47 % SZS output start Refutation % 0.20/0.47 1[0:Inp] || -> equal(multiply(sk_c6,sk_c5),sk_c7)** 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_c6,sk_c7),sk_c5). % 0.20/0.47 3[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 4[0:Inp] || -> equal(inverse(sk_c6),sk_c5) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 5[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5)** equal(multiply(sk_c6,sk_c7),sk_c5). % 0.20/0.47 6[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 7[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 8[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.47 9[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 10[0:Inp] || -> equal(inverse(sk_c6),sk_c5) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 11[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 12[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 13[0:Inp] || -> equal(multiply(sk_c6,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 14[0:Inp] || -> equal(multiply(sk_c3,sk_c7),sk_c6) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 15[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 16[0:Inp] || -> equal(inverse(sk_c6),sk_c5) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 17[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 18[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 19[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 22[0:Inp] || -> equal(inverse(sk_c6),sk_c5) equal(inverse(sk_c2),sk_c6)**. % 0.20/0.47 25[0:Inp] || -> equal(multiply(sk_c6,sk_c5),sk_c7) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.47 28[0:Inp] || -> equal(inverse(sk_c6),sk_c5) equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.47 31[0:Inp] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(inverse(x),sk_c7) equal(inverse(sk_c6),sk_c5) 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)** equal(multiply(sk_c6,sk_c5),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5) -> . % 0.20/0.47 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.20/0.47 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.20/0.47 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.20/0.47 35[1:Spt:31.3,31.8] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c6),sk_c7)** -> . % 0.20/0.47 36[2:Spt:4.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 38[3:Spt:10.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 44[4:Spt:16.1] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 46[4:SpL:44.0,35.1] || equal(inverse(sk_c1),sk_c7)** equal(sk_c7,sk_c7) -> . % 0.20/0.47 47[4:Obv:46.1] || equal(inverse(sk_c1),sk_c7)** -> . % 0.20/0.47 48[4:Rew:38.0,47.0] || equal(sk_c7,sk_c7)* -> . % 0.20/0.47 49[4:Obv:48.0] || -> . % 0.20/0.47 50[4:Spt:49.0,16.1,44.0] || equal(multiply(sk_c1,sk_c6),sk_c7)** -> . % 0.20/0.47 51[4:Spt:49.0,16.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 52[4:MRR:18.1,50.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 53[4:MRR:15.1,50.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 54[4:MRR:17.1,50.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 55[4:MRR:14.1,50.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.47 56[4:MRR:13.1,50.0] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 68[4:SpR:51.0,33.0] || -> equal(multiply(sk_c5,sk_c6),identity)**. % 0.20/0.47 71[1:SpL:33.0,35.1] || equal(inverse(inverse(sk_c6)),sk_c7)** equal(identity,sk_c7) -> . % 0.20/0.47 72[4:Rew:51.0,71.0] || equal(inverse(sk_c5),sk_c7)** equal(identity,sk_c7) -> . % 0.20/0.47 77[2:SpR:36.0,34.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c5,u))**. % 0.20/0.47 80[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.47 85[0:Rew:32.0,80.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.47 101[0:SpR:85.0,85.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.47 103[4:SpR:54.0,85.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c6)**. % 0.20/0.47 106[4:SpR:55.0,85.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c7)**. % 0.20/0.47 107[0:SpR:32.0,85.0] || -> equal(multiply(inverse(identity),u),u)**. % 0.20/0.47 108[0:SpR:33.0,85.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.47 120[4:Rew:56.0,103.0,52.0,103.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 122[4:Rew:120.0,36.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 124[4:Rew:120.0,53.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.20/0.47 132[4:Rew:120.0,72.0] || equal(inverse(sk_c5),sk_c6)** equal(identity,sk_c7) -> . % 0.20/0.47 141[4:Rew:122.0,106.0,124.0,106.0,120.0,106.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 142[4:Rew:141.0,51.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 144[4:Rew:141.0,68.0] || -> equal(multiply(sk_c6,sk_c6),identity)**. % 0.20/0.47 147[4:Rew:141.0,122.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 151[4:Rew:144.0,147.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 197[4:Rew:151.0,132.1,120.0,132.1,142.0,132.0,141.0,132.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.20/0.47 198[4:Obv:197.1] || -> . % 0.20/0.47 206[3:Spt:198.0,10.1,38.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.20/0.47 207[3:Spt:198.0,10.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 209[0:Rew:101.0,108.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.47 210[3:MRR:12.1,206.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 211[3:MRR:9.1,206.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 212[3:MRR:11.0,206.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 213[3:MRR:8.0,206.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.47 214[3:MRR:7.0,206.0] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 215[3:Rew:207.0,71.0] || equal(inverse(sk_c5),sk_c7)** equal(identity,sk_c7) -> . % 0.20/0.47 216[3:SpR:207.0,85.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.20/0.47 227[3:SpR:212.0,85.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c6)**. % 0.20/0.47 229[3:Rew:210.0,227.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 230[3:Rew:214.0,229.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 231[3:Rew:230.0,211.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.20/0.47 232[3:Rew:230.0,36.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.47 235[3:Rew:230.0,77.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.20/0.47 237[3:Rew:230.0,213.0] || -> equal(multiply(sk_c3,sk_c6),sk_c6)**. % 0.20/0.47 239[3:Rew:230.0,215.0] || equal(inverse(sk_c5),sk_c6)** equal(identity,sk_c7) -> . % 0.20/0.47 245[3:Rew:230.0,239.1] || equal(inverse(sk_c5),sk_c6)** equal(identity,sk_c6) -> . % 0.20/0.47 256[3:SpR:237.0,85.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c6)**. % 0.20/0.47 258[3:Rew:232.0,256.0,231.0,256.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 259[3:Rew:258.0,207.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 262[3:Rew:258.0,216.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),u)**. % 0.20/0.47 266[3:Rew:258.0,235.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c6,u))**. % 0.20/0.47 267[3:Rew:258.0,245.0] || equal(inverse(sk_c6),sk_c6)** equal(identity,sk_c6) -> . % 0.20/0.47 268[3:Rew:262.0,266.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 274[3:Rew:259.0,267.0] || equal(sk_c6,sk_c6) equal(identity,sk_c6)** -> . % 0.20/0.47 275[3:Obv:274.0] || equal(identity,sk_c6)** -> . % 0.20/0.47 292[3:SpR:268.0,209.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 294[3:MRR:292.0,275.0] || -> . % 0.20/0.47 296[2:Spt:294.0,4.1,36.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.20/0.47 297[2:Spt:294.0,4.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 298[2:MRR:6.1,296.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 299[2:MRR:3.1,296.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.47 301[2:MRR:5.1,296.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 302[2:MRR:2.1,296.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.47 303[2:MRR:1.1,296.0] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 311[2:SpR:301.0,85.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c6)**. % 0.20/0.47 313[2:Rew:298.0,311.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 314[2:Rew:303.0,313.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 315[2:Rew:314.0,299.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.20/0.47 316[2:Rew:314.0,296.0] || equal(multiply(sk_c6,sk_c6),sk_c5)** -> . % 0.20/0.47 319[2:Rew:314.0,302.0] || -> equal(multiply(sk_c3,sk_c6),sk_c6)**. % 0.20/0.47 320[2:Rew:314.0,303.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.20/0.47 333[2:SpR:319.0,85.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c6)**. % 0.20/0.47 335[2:Rew:315.0,333.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.20/0.47 336[2:Rew:335.0,316.0] || equal(sk_c5,sk_c6)** -> . % 0.20/0.47 338[2:SpR:320.0,85.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.20/0.47 340[2:Rew:297.0,338.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.20/0.47 342[2:SpR:335.0,85.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c6)**. % 0.20/0.47 344[2:Rew:297.0,342.0] || -> equal(multiply(sk_c5,sk_c6),sk_c6)**. % 0.20/0.47 345[2:Rew:340.0,344.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 346[2:MRR:345.0,336.0] || -> . % 0.20/0.47 347[1:Spt:346.0,31.0,31.1,31.2,31.4,31.5,31.6,31.7,31.9,31.10] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(inverse(sk_c6),sk_c5) equal(multiply(u,sk_c6),sk_c5)**+ equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5) -> . % 0.20/0.47 349[1:SpL:32.0,347.4] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(sk_c6),sk_c5) equal(sk_c5,sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5) -> . % 0.20/0.47 350[2:Spt:4.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.47 351[2:Rew:350.0,347.8] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(inverse(sk_c6),sk_c5) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** equal(sk_c5,sk_c5) -> . % 0.20/0.47 353[2:Rew:350.0,349.8] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(sk_c6),sk_c5) equal(sk_c5,sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** equal(sk_c5,sk_c5) -> . % 0.20/0.47 354[2:Obv:353.8] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(inverse(sk_c6),sk_c5) equal(sk_c5,sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.47 355[2:Obv:351.8] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(inverse(sk_c6),sk_c5) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.47 358[2:SpR:350.0,85.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.20/0.47 360[3:Spt:22.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 362[3:Rew:360.0,355.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c6) equal(sk_c5,sk_c5) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.47 363[3:Rew:360.0,354.3] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(sk_c5,sk_c5) equal(sk_c5,sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.47 364[3:Rew:360.0,358.0] || -> equal(multiply(sk_c5,sk_c5),sk_c7)**. % 0.20/0.47 365[3:Obv:363.3] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(sk_c5,sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.47 366[3:Obv:362.3] || 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)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.47 370[4:Spt:7.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.47 372[4:Rew:370.0,366.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)** equal(sk_c7,sk_c7) -> . % 0.20/0.47 373[4:Rew:370.0,365.6] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(sk_c5,sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** equal(sk_c7,sk_c7) -> . % 0.20/0.47 374[4:Obv:373.6] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c7) equal(inverse(v),sk_c6) equal(sk_c5,sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 375[4:Obv:372.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 378[4:SpR:370.0,85.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c5)**. % 0.20/0.47 380[4:Rew:360.0,378.0] || -> equal(multiply(sk_c5,sk_c7),sk_c5)**. % 0.20/0.47 381[5:Spt:12.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.20/0.47 385[3:SpR:364.0,85.0] || -> equal(multiply(inverse(sk_c5),sk_c7),sk_c5)**. % 0.20/0.47 390[6:Spt:11.1] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.20/0.47 392[6:SpR:390.0,85.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c6)**. % 0.20/0.47 394[6:Rew:370.0,392.0,381.0,392.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 406[6:Rew:394.0,374.1] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 409[6:Rew:394.0,380.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.20/0.47 414[6:Rew:394.0,406.4] || equal(inverse(identity),sk_c6) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c6) equal(multiply(u,sk_c6),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 419[0:SpR:33.0,85.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.47 420[0:SpR:33.0,209.0] || -> equal(inverse(identity),identity)**. % 0.20/0.47 422[3:SpR:360.0,33.0] || -> equal(multiply(sk_c5,sk_c6),identity)**. % 0.20/0.47 423[5:SpR:381.0,33.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.20/0.47 424[0:Rew:420.0,107.0] || -> equal(multiply(identity,u),u)**. % 0.20/0.47 425[6:Rew:420.0,414.0] || equal(identity,sk_c6) equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(sk_c5,sk_c6) equal(multiply(u,sk_c6),sk_c6)** equal(multiply(v,sk_c5),sk_c6)** -> . % 0.20/0.47 426[6:Rew:409.0,422.0] || -> equal(identity,sk_c5)**. % 0.20/0.47 428[6:Rew:426.0,209.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.47 433[6:Rew:426.0,424.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.47 438[6:Rew:433.0,409.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 441[6:Rew:438.0,360.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 448[6:Rew:438.0,426.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 455[6:Rew:438.0,428.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.47 471[6:Rew:455.0,425.5,438.0,425.5,455.0,425.4,438.0,425.3,448.0,425.0] || equal(sk_c6,sk_c6) equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(sk_c6,sk_c6) equal(u,sk_c6) equal(v,sk_c6) -> . % 0.20/0.47 472[6:Obv:471.3] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.20/0.47 473[6:Con:472.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.20/0.47 546[6:SpL:441.0,473.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.20/0.47 548[6:Obv:546.1] || -> . % 0.20/0.47 549[6:Spt:548.0,11.1,390.0] || equal(multiply(sk_c4,sk_c6),sk_c5)** -> . % 0.20/0.47 550[6:Spt:548.0,11.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 551[0:Rew:209.0,419.0] || -> equal(inverse(inverse(u)),u)**. % 0.20/0.47 554[6:MRR:17.0,549.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.47 572[6:SpR:554.0,85.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c6)**. % 0.20/0.47 574[6:Rew:550.0,572.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 587[4:SpR:380.0,85.0] || -> equal(multiply(inverse(sk_c5),sk_c5),sk_c7)**. % 0.20/0.47 589[4:Rew:33.0,587.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 592[4:Rew:589.0,209.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 593[4:Rew:589.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 594[5:Rew:589.0,423.0] || -> equal(multiply(sk_c6,sk_c4),sk_c7)**. % 0.20/0.47 597[4:Rew:592.0,350.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.47 598[6:Rew:592.0,574.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.47 600[4:Rew:592.0,375.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7)** equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(v,sk_c6) equal(multiply(w,sk_c5),sk_c6)** -> . % 0.20/0.47 601[4:Rew:592.0,385.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.20/0.47 605[6:Rew:597.0,549.0] || equal(multiply(sk_c4,sk_c6),sk_c6)** -> . % 0.20/0.47 621[4:Rew:597.0,601.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 622[6:Rew:598.0,593.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 625[6:Rew:622.0,594.0,598.0,594.0] || -> equal(sk_c4,sk_c6)**. % 0.20/0.48 637[6:Rew:622.0,605.0,625.0,605.0] || equal(sk_c6,sk_c6)* -> . % 0.20/0.48 638[6:Obv:637.0] || -> . % 0.20/0.48 654[5:Spt:638.0,12.0,381.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.20/0.48 655[5:Spt:638.0,12.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.48 662[5:MRR:18.0,654.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.48 669[4:Rew:597.0,600.5,597.0,600.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7)** equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c6)** equal(v,sk_c6) equal(multiply(w,sk_c6),sk_c6)** -> . % 0.20/0.48 670[4:Con:669.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7)** equal(multiply(u,sk_c6),sk_c6)** equal(v,sk_c6) -> . % 0.20/0.48 672[5:SpR:655.0,85.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.20/0.48 674[5:Rew:593.0,672.0] || -> equal(multiply(sk_c1,u),u)**. % 0.20/0.48 675[5:Rew:674.0,662.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.48 679[5:Rew:675.0,592.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.48 683[5:Rew:675.0,670.1] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6)** equal(multiply(u,sk_c6),sk_c6)** equal(v,sk_c6) -> . % 0.20/0.48 687[5:Rew:679.0,683.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.20/0.48 688[5:Con:687.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.20/0.48 699[0:SpR:551.0,85.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.20/0.48 752[5:SpL:621.0,688.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.20/0.48 754[5:Obv:752.1] || -> . % 0.20/0.48 755[4:Spt:754.0,7.1,370.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.48 756[4:Spt:754.0,7.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.48 757[4:MRR:19.1,755.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.48 758[4:MRR:13.0,755.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.48 759[4:MRR:25.0,755.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.48 761[4:SpR:756.0,551.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.20/0.48 765[4:SpR:757.0,551.0] || -> equal(inverse(sk_c6),sk_c2)**. % 0.20/0.48 768[4:Rew:360.0,765.0] || -> equal(sk_c2,sk_c5)**. % 0.20/0.48 770[4:Rew:768.0,759.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.48 772[4:Rew:364.0,770.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.48 776[4:Rew:772.0,755.0] || equal(multiply(sk_c6,sk_c5),sk_c6)** -> . % 0.20/0.48 780[4:Rew:772.0,758.0] || -> equal(multiply(sk_c1,sk_c6),sk_c6)**. % 0.20/0.48 781[4:Rew:772.0,761.0] || -> equal(inverse(sk_c6),sk_c1)**. % 0.20/0.48 783[4:Rew:360.0,781.0] || -> equal(sk_c1,sk_c5)**. % 0.20/0.48 786[4:Rew:422.0,780.0,783.0,780.0] || -> equal(identity,sk_c6)**. % 0.20/0.48 787[4:Rew:786.0,420.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.48 788[4:Rew:786.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.48 792[4:Rew:360.0,787.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.48 801[4:Rew:788.0,776.0,792.0,776.0] || equal(sk_c6,sk_c6)* -> . % 0.20/0.48 802[4:Obv:801.0] || -> . % 0.20/0.48 810[3:Spt:802.0,22.0,360.0] || equal(inverse(sk_c6),sk_c5)** -> . % 0.20/0.48 811[3:Spt:802.0,22.1] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.48 812[3:MRR:10.0,810.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.48 813[3:MRR:28.0,810.0] || -> equal(multiply(sk_c2,sk_c5),sk_c6)**. % 0.20/0.48 814[3:MRR:16.0,810.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.20/0.48 816[3:SpR:811.0,551.0] || -> equal(inverse(sk_c6),sk_c2)**. % 0.20/0.48 819[3:Rew:816.0,810.0] || equal(sk_c2,sk_c5)** -> . % 0.20/0.48 820[3:Rew:816.0,358.0] || -> equal(multiply(sk_c2,sk_c5),sk_c7)**. % 0.20/0.48 821[3:Rew:813.0,820.0] || -> equal(sk_c7,sk_c6)**. % 0.20/0.48 822[3:Rew:821.0,350.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.20/0.48 823[3:Rew:821.0,812.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.20/0.48 825[3:Rew:821.0,814.0] || -> equal(multiply(sk_c1,sk_c6),sk_c6)**. % 0.20/0.48 837[3:SpR:823.0,85.0] || -> equal(multiply(sk_c6,multiply(sk_c1,u)),u)**. % 0.20/0.48 838[3:SpR:823.0,551.0] || -> equal(inverse(sk_c6),sk_c1)**. % 0.20/0.48 839[3:SpR:823.0,699.0] || -> equal(multiply(sk_c1,multiply(sk_c6,u)),u)**. % 0.20/0.48 841[3:Rew:816.0,838.0] || -> equal(sk_c2,sk_c1)**. % 0.20/0.48 843[3:Rew:841.0,816.0] || -> equal(inverse(sk_c6),sk_c1)**. % 0.20/0.48 844[3:Rew:841.0,819.0] || equal(sk_c1,sk_c5)** -> . % 0.20/0.48 857[3:SpR:825.0,34.0] || -> equal(multiply(sk_c1,multiply(sk_c6,u)),multiply(sk_c6,u))**. % 0.20/0.48 858[3:SpR:825.0,85.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c6)**. % 0.20/0.48 860[3:Rew:822.0,858.0,823.0,858.0] || -> equal(sk_c5,sk_c6)**. % 0.20/0.48 861[3:Rew:860.0,844.0] || equal(sk_c1,sk_c6)** -> . % 0.20/0.48 865[3:Rew:839.0,857.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.48 866[3:Rew:865.0,837.0] || -> equal(multiply(sk_c1,u),u)**. % 0.20/0.48 890[3:SpR:823.0,33.0] || -> equal(multiply(sk_c6,sk_c1),identity)**. % 0.20/0.48 891[3:SpR:843.0,33.0] || -> equal(multiply(sk_c1,sk_c6),identity)**. % 0.20/0.48 892[3:Rew:865.0,890.0] || -> equal(identity,sk_c1)**. % 0.20/0.48 900[3:Rew:866.0,891.0,892.0,891.0] || -> equal(sk_c1,sk_c6)**. % 0.20/0.48 901[3:MRR:900.0,861.0] || -> . % 0.20/0.48 907[2:Spt:901.0,4.1,350.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.20/0.48 908[2:Spt:901.0,4.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.48 911[2:MRR:3.1,907.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.48 914[2:MRR:2.1,907.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.20/0.48 915[2:MRR:1.1,907.0] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.48 938[2:SpR:911.0,699.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),u)**. % 0.20/0.48 940[2:SpR:914.0,34.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.20/0.48 944[2:Rew:938.0,940.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.48 946[2:Rew:944.0,915.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.48 947[2:Rew:944.0,907.0] || equal(sk_c5,sk_c7)** -> . % 0.20/0.48 953[2:Rew:946.0,947.0] || equal(sk_c7,sk_c7)* -> . % 0.20/0.48 954[2:Obv:953.0] || -> . % 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_16 prove_this_17 prove_this_18 prove_this_19 prove_this_22 prove_this_25 prove_this_28 prove_this_31 left_identity left_inverse associativity % 0.20/0.48 %------------------------------------------------------------------------------