%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP314-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n005.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:48 EDT 2022 % Result : Unsatisfiable 0.19s 0.46s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GRP314-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n005.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Mon Jun 13 06:11:54 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.46 % 0.19/0.46 SPASS V 3.9 % 0.19/0.46 SPASS beiseite: Proof found. % 0.19/0.46 % SZS status Theorem % 0.19/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.46 SPASS derived 541 clauses, backtracked 250 clauses, performed 9 splits and kept 488 clauses. % 0.19/0.46 SPASS allocated 63462 KBytes. % 0.19/0.46 SPASS spent 0:00:00.11 on the problem. % 0.19/0.46 0:00:00.04 for the input. % 0.19/0.46 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.46 0:00:00.00 for inferences. % 0.19/0.46 0:00:00.00 for the backtracking. % 0.19/0.46 0:00:00.05 for the reduction. % 0.19/0.46 % 0.19/0.46 % 0.19/0.46 Here is a proof with depth 4, length 267 : % 0.19/0.46 % SZS output start Refutation % 0.19/0.46 1[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.46 2[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c8),sk_c7)**. % 0.19/0.46 3[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c8)** equal(multiply(sk_c1,sk_c8),sk_c7). % 0.19/0.46 4[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c7)**. % 0.19/0.46 6[0:Inp] || -> equal(inverse(sk_c4),sk_c8)** equal(inverse(sk_c1),sk_c8). % 0.19/0.46 7[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.46 8[0:Inp] || -> equal(inverse(sk_c5),sk_c7)** equal(inverse(sk_c1),sk_c8). % 0.19/0.46 9[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.46 14[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c2),sk_c7)**. % 0.19/0.46 18[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 19[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c8) equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 20[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 21[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 22[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c3),sk_c7)**. % 0.19/0.46 23[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.46 24[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(inverse(sk_c3),sk_c7)**. % 0.19/0.46 25[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.46 26[0:Inp] || equal(multiply(sk_c7,sk_c8),sk_c6)** equal(multiply(u,sk_c8),sk_c7)** equal(inverse(u),sk_c8) equal(multiply(v,sk_c7),sk_c6)** equal(inverse(v),sk_c7) equal(multiply(w,sk_c7),sk_c8)** equal(inverse(w),sk_c7) equal(inverse(x),sk_c8) equal(multiply(x,sk_c7),sk_c8)** equal(inverse(y),sk_c7) equal(multiply(y,sk_c6),sk_c7)** -> . % 0.19/0.46 27[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.46 28[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.46 29[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.46 30[0:Rew:1.0,26.0] || equal(sk_c6,sk_c6) equal(multiply(u,sk_c8),sk_c7)** equal(inverse(u),sk_c8) equal(multiply(v,sk_c7),sk_c6)** equal(inverse(v),sk_c7) equal(multiply(w,sk_c7),sk_c8)** equal(inverse(w),sk_c7) equal(inverse(x),sk_c8) equal(multiply(x,sk_c7),sk_c8)** equal(inverse(y),sk_c7) equal(multiply(y,sk_c6),sk_c7)** -> . % 0.19/0.46 31[0:Obv:30.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(inverse(x),sk_c7) equal(inverse(y),sk_c8) equal(multiply(u,sk_c6),sk_c7)**+ equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(x,sk_c7),sk_c6)** equal(multiply(y,sk_c8),sk_c7)** -> . % 0.19/0.46 32[1:Spt:31.2,31.7] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c8)** -> . % 0.19/0.46 33[2:Spt:22.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.46 35[3:Spt:8.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.19/0.46 38[4:Spt:9.1] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.46 40[5:Spt:23.1] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.46 42[5:SpL:40.0,32.1] || equal(inverse(sk_c4),sk_c7)** equal(sk_c8,sk_c8) -> . % 0.19/0.46 43[5:Obv:42.1] || equal(inverse(sk_c4),sk_c7)** -> . % 0.19/0.46 44[5:Rew:33.0,43.0] || equal(sk_c8,sk_c7)** -> . % 0.19/0.46 48[2:SpR:33.0,28.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.19/0.46 49[3:SpR:35.0,28.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.19/0.46 50[1:SpL:28.0,32.1] || equal(inverse(inverse(sk_c7)),sk_c7)** equal(identity,sk_c8) -> . % 0.19/0.46 55[4:SpR:38.0,29.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.19/0.46 57[0:SpR:28.0,29.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.46 59[0:Rew:27.0,57.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.46 61[2:SpR:48.0,29.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),multiply(identity,u))**. % 0.19/0.46 63[2:Rew:27.0,61.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),u)**. % 0.19/0.46 74[0:SpR:59.0,59.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.46 77[0:SpR:1.0,59.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.19/0.46 78[3:SpR:49.0,59.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c5)**. % 0.19/0.46 79[4:SpR:38.0,59.0] || -> equal(multiply(inverse(sk_c5),sk_c7),sk_c6)**. % 0.19/0.46 81[0:SpR:28.0,59.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.46 84[2:SpR:63.0,59.0] || -> equal(multiply(inverse(sk_c8),u),multiply(sk_c4,u))**. % 0.19/0.46 89[4:Rew:35.0,79.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.46 92[0:Rew:74.0,81.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.46 93[3:Rew:92.0,78.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.19/0.46 94[3:Rew:93.0,50.0] || equal(inverse(sk_c5),sk_c7)** equal(identity,sk_c8) -> . % 0.19/0.46 95[3:Rew:93.0,77.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.19/0.46 96[4:Rew:38.0,95.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.46 97[5:MRR:96.0,44.0] || -> . % 0.19/0.46 98[3:Rew:35.0,94.0] || equal(sk_c7,sk_c7) equal(identity,sk_c8)** -> . % 0.19/0.46 99[3:Obv:98.0] || equal(identity,sk_c8)** -> . % 0.19/0.46 101[5:Spt:97.0,23.1,40.0] || equal(multiply(sk_c4,sk_c7),sk_c8)** -> . % 0.19/0.46 102[5:Spt:97.0,23.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.46 106[4:Rew:96.0,48.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.46 110[4:Rew:96.0,84.0] || -> equal(multiply(inverse(sk_c7),u),multiply(sk_c4,u))**. % 0.19/0.46 111[4:Rew:96.0,99.0] || equal(identity,sk_c7)** -> . % 0.19/0.46 113[5:Rew:96.0,101.0] || equal(multiply(sk_c4,sk_c7),sk_c7)** -> . % 0.19/0.46 114[4:Rew:93.0,110.0] || -> equal(multiply(sk_c5,u),multiply(sk_c4,u))**. % 0.19/0.46 117[4:Rew:114.0,55.0] || -> equal(multiply(sk_c4,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.19/0.46 120[4:Rew:96.0,7.1,96.0,7.0] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c7),sk_c7)**. % 0.19/0.46 121[5:MRR:120.1,113.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.46 124[4:Rew:96.0,19.1,96.0,19.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.19/0.46 125[5:MRR:124.0,113.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.19/0.46 134[3:SpR:93.0,28.0] || -> equal(multiply(sk_c5,sk_c7),identity)**. % 0.19/0.46 135[3:SpR:93.0,59.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.19/0.46 137[4:Rew:114.0,134.0] || -> equal(multiply(sk_c4,sk_c7),identity)**. % 0.19/0.46 139[4:Rew:114.0,135.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.19/0.46 146[5:SpR:121.0,28.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.19/0.46 166[5:SpR:125.0,59.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.19/0.46 168[5:Rew:89.0,166.0,102.0,166.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.46 172[5:Rew:168.0,117.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.19/0.46 176[5:Rew:139.0,172.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.46 177[5:Rew:176.0,106.0] || -> equal(identity,sk_c4)**. % 0.19/0.46 178[5:Rew:176.0,139.0] || -> equal(multiply(sk_c4,u),u)**. % 0.19/0.46 181[5:Rew:176.0,146.0] || -> equal(identity,sk_c1)**. % 0.19/0.46 189[5:Rew:177.0,111.0] || equal(sk_c4,sk_c7)** -> . % 0.19/0.46 193[5:Rew:177.0,137.0] || -> equal(multiply(sk_c4,sk_c7),sk_c4)**. % 0.19/0.46 194[5:Rew:177.0,181.0] || -> equal(sk_c4,sk_c1)**. % 0.19/0.46 207[5:Rew:194.0,189.0] || equal(sk_c1,sk_c7)** -> . % 0.19/0.46 209[5:Rew:194.0,178.0] || -> equal(multiply(sk_c1,u),u)**. % 0.19/0.46 219[5:Rew:209.0,193.0,194.0,193.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.46 220[5:MRR:219.0,207.0] || -> . % 0.19/0.46 225[4:Spt:220.0,9.1,38.0] || equal(multiply(sk_c5,sk_c6),sk_c7)** -> . % 0.19/0.46 226[4:Spt:220.0,9.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.46 227[4:Rew:95.0,225.0] || equal(sk_c8,sk_c7)** -> . % 0.19/0.46 228[3:Rew:95.0,25.1] || -> equal(inverse(sk_c3),sk_c7)** equal(sk_c8,sk_c7). % 0.19/0.46 229[4:MRR:228.1,227.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.46 232[3:Rew:95.0,21.0] || -> equal(sk_c8,sk_c7) equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 233[4:MRR:232.0,227.0] || -> equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 260[4:SpR:233.0,59.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c7)**. % 0.19/0.46 262[4:Rew:1.0,260.0,229.0,260.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.46 264[4:Rew:262.0,95.0] || -> equal(multiply(sk_c5,sk_c7),sk_c8)**. % 0.19/0.46 267[4:Rew:134.0,264.0] || -> equal(identity,sk_c8)**. % 0.19/0.46 268[4:MRR:267.0,99.0] || -> . % 0.19/0.46 269[3:Spt:268.0,8.0,35.0] || equal(inverse(sk_c5),sk_c7)** -> . % 0.19/0.46 270[3:Spt:268.0,8.1] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.46 271[3:MRR:24.0,269.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.46 273[3:MRR:20.0,269.0] || -> equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 275[3:MRR:4.0,269.0] || -> equal(multiply(sk_c1,sk_c8),sk_c7)**. % 0.19/0.46 276[3:SpR:270.0,59.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.19/0.46 278[3:SpR:271.0,59.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.19/0.46 286[3:SpR:273.0,59.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c7)**. % 0.19/0.46 288[3:Rew:1.0,286.0,271.0,286.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.46 290[3:Rew:288.0,77.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.19/0.46 293[3:Rew:28.0,290.0] || -> equal(identity,sk_c8)**. % 0.19/0.46 294[3:Rew:293.0,48.0] || -> equal(multiply(sk_c8,sk_c4),sk_c8)**. % 0.19/0.46 295[3:Rew:293.0,27.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.46 296[3:Rew:293.0,92.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.46 300[3:Rew:293.0,50.1] || equal(inverse(inverse(sk_c7)),sk_c7)** equal(sk_c8,sk_c8) -> . % 0.19/0.46 301[3:Rew:295.0,294.0] || -> equal(sk_c4,sk_c8)**. % 0.19/0.46 302[3:Rew:295.0,276.0] || -> equal(multiply(sk_c1,u),u)**. % 0.19/0.46 304[3:Rew:301.0,33.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.46 306[3:Rew:296.0,275.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.46 308[3:Rew:306.0,302.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.46 310[3:Rew:308.0,278.0] || -> equal(multiply(sk_c3,u),u)**. % 0.19/0.46 312[3:Rew:310.0,273.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.46 318[3:Rew:312.0,304.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.46 328[3:Obv:300.1] || equal(inverse(inverse(sk_c7)),sk_c7)** -> . % 0.19/0.46 329[3:Rew:318.0,328.0,318.0,328.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.46 330[3:Obv:329.0] || -> . % 0.19/0.46 333[2:Spt:330.0,22.0,33.0] || equal(inverse(sk_c4),sk_c8)** -> . % 0.19/0.46 334[2:Spt:330.0,22.1] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.46 336[2:MRR:6.0,333.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.46 337[2:MRR:18.0,333.0] || -> equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 339[2:MRR:2.0,333.0] || -> equal(multiply(sk_c1,sk_c8),sk_c7)**. % 0.19/0.46 340[2:SpR:334.0,59.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.19/0.46 344[2:SpR:336.0,59.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.19/0.46 350[2:SpR:337.0,59.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c7)**. % 0.19/0.46 352[2:Rew:1.0,350.0,334.0,350.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.46 354[2:Rew:352.0,77.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.19/0.46 357[2:Rew:28.0,354.0] || -> equal(identity,sk_c8)**. % 0.19/0.46 358[2:Rew:357.0,92.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.46 359[2:Rew:357.0,27.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.46 363[2:Rew:357.0,50.1] || equal(inverse(inverse(sk_c7)),sk_c7)** equal(sk_c8,sk_c8) -> . % 0.19/0.46 364[2:Rew:358.0,339.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.46 365[2:Rew:364.0,336.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.19/0.46 366[2:Rew:364.0,344.0] || -> equal(multiply(sk_c8,multiply(sk_c7,u)),u)**. % 0.19/0.46 367[2:Rew:359.0,366.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.46 369[2:Rew:367.0,340.0] || -> equal(multiply(sk_c3,u),u)**. % 0.19/0.46 370[2:Rew:369.0,337.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.46 376[2:Rew:370.0,365.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.46 385[2:Obv:363.1] || equal(inverse(inverse(sk_c7)),sk_c7)** -> . % 0.19/0.46 386[2:Rew:376.0,385.0,376.0,385.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.46 387[2:Obv:386.0] || -> . % 0.19/0.46 390[1:Spt:387.0,31.0,31.1,31.3,31.4,31.5,31.6,31.8,31.9] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(inverse(x),sk_c8) equal(multiply(u,sk_c6),sk_c7)**+ equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(x,sk_c8),sk_c7)** -> . % 0.19/0.46 392[2:Spt:24.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.19/0.46 393[2:SpR:392.0,59.0] || -> equal(multiply(sk_c7,multiply(sk_c5,u)),u)**. % 0.19/0.46 395[3:Spt:14.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.46 396[3:SpR:395.0,59.0] || -> equal(multiply(sk_c8,multiply(sk_c4,u)),u)**. % 0.19/0.46 398[4:Spt:23.1] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.46 400[4:SpR:398.0,59.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c7)**. % 0.19/0.46 402[4:Rew:395.0,400.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.19/0.46 406[5:Spt:9.1] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.46 408[5:SpR:406.0,59.0] || -> equal(multiply(inverse(sk_c5),sk_c7),sk_c6)**. % 0.19/0.46 410[5:SpL:406.0,390.4] || equal(inverse(sk_c5),sk_c7) equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(sk_c7,sk_c7) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.46 411[5:Rew:392.0,408.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.46 412[5:Obv:410.4] || equal(inverse(sk_c5),sk_c7) equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.46 413[5:Rew:392.0,412.0] || equal(sk_c7,sk_c7) equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.46 414[5:Obv:413.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.46 419[5:SpR:411.0,59.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.19/0.46 421[5:Rew:77.0,419.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.46 425[5:Rew:421.0,402.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.19/0.46 426[5:Rew:421.0,77.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.19/0.46 430[5:Rew:421.0,414.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c7),sk_c8)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.46 433[5:Rew:411.0,425.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.46 434[5:Rew:433.0,406.0] || -> equal(multiply(sk_c5,sk_c7),sk_c7)**. % 0.19/0.46 437[5:Rew:28.0,426.0,433.0,426.0] || -> equal(identity,sk_c7)**. % 0.19/0.46 439[5:Rew:437.0,92.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.46 443[5:Rew:439.0,434.0] || -> equal(sk_c5,sk_c7)**. % 0.19/0.46 445[5:Rew:443.0,392.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.46 455[5:Rew:439.0,430.5,421.0,430.5,439.0,430.4,433.0,430.4,439.0,430.3,421.0,430.3,421.0,430.2] || 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.46 456[5:Con:455.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.46 483[5:SpL:445.0,456.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.46 484[5:Obv:483.1] || -> . % 0.19/0.46 485[5:Spt:484.0,9.1,406.0] || equal(multiply(sk_c5,sk_c6),sk_c7)** -> . % 0.19/0.46 486[5:Spt:484.0,9.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.46 487[5:MRR:25.1,485.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.46 489[5:MRR:21.0,485.0] || -> equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 509[5:SpR:489.0,59.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c7)**. % 0.19/0.46 511[5:Rew:1.0,509.0,487.0,509.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.46 513[5:Rew:511.0,77.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.19/0.46 514[5:Rew:511.0,485.0] || equal(multiply(sk_c5,sk_c7),sk_c7)** -> . % 0.19/0.46 519[5:Rew:28.0,513.0] || -> equal(identity,sk_c8)**. % 0.19/0.46 520[5:Rew:519.0,92.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.46 521[5:Rew:519.0,27.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.46 524[5:Rew:520.0,402.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.46 538[5:Rew:524.0,521.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.46 541[5:Rew:538.0,393.0] || -> equal(multiply(sk_c5,u),u)**. % 0.19/0.46 550[5:Rew:541.0,514.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.46 551[5:Obv:550.0] || -> . % 0.19/0.46 563[4:Spt:551.0,23.1,398.0] || equal(multiply(sk_c4,sk_c7),sk_c8)** -> . % 0.19/0.46 564[4:Spt:551.0,23.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.46 565[4:MRR:7.1,563.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.46 567[4:MRR:19.0,563.0] || -> equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.46 569[4:MRR:3.0,563.0] || -> equal(multiply(sk_c1,sk_c8),sk_c7)**. % 0.19/0.46 570[4:SpR:564.0,59.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.19/0.46 574[4:SpR:565.0,59.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.19/0.46 582[4:SpR:567.0,59.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c7)**. % 0.19/0.46 584[4:Rew:1.0,582.0,564.0,582.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.46 586[4:Rew:584.0,77.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.19/0.46 591[4:Rew:28.0,586.0] || -> equal(identity,sk_c8)**. % 0.19/0.46 592[4:Rew:591.0,27.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.46 593[4:Rew:591.0,92.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.46 596[4:Rew:592.0,574.0] || -> equal(multiply(sk_c1,u),u)**. % 0.19/0.46 597[4:Rew:592.0,396.0] || -> equal(multiply(sk_c4,u),u)**. % 0.19/0.46 598[4:Rew:593.0,569.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.46 600[4:Rew:598.0,596.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.46 602[4:Rew:600.0,570.0] || -> equal(multiply(sk_c3,u),u)**. % 0.19/0.46 604[4:Rew:597.0,563.0] || equal(sk_c8,sk_c7)** -> . % 0.19/0.47 605[4:Rew:602.0,567.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.47 606[4:MRR:605.0,604.0] || -> . % 0.19/0.47 612[3:Spt:606.0,14.0,395.0] || equal(inverse(sk_c4),sk_c8)** -> . % 0.19/0.47 613[3:Spt:606.0,14.1] || -> equal(inverse(sk_c2),sk_c7)**. % 0.19/0.47 614[3:MRR:6.0,612.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.47 615[3:MRR:22.0,612.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.47 616[3:MRR:18.0,612.0] || -> equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.47 618[3:MRR:2.0,612.0] || -> equal(multiply(sk_c1,sk_c8),sk_c7)**. % 0.19/0.47 621[3:SpR:614.0,59.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.19/0.47 623[3:SpR:615.0,59.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.19/0.47 629[3:SpR:616.0,59.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c7)**. % 0.19/0.47 631[3:Rew:1.0,629.0,615.0,629.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.47 633[3:Rew:631.0,77.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.19/0.47 636[3:Rew:631.0,390.4] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(inverse(x),sk_c8) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(x,sk_c8),sk_c7)** -> . % 0.19/0.47 638[3:Rew:28.0,633.0] || -> equal(identity,sk_c8)**. % 0.19/0.47 639[3:Rew:638.0,92.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.47 640[3:Rew:638.0,27.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.47 643[3:Rew:639.0,618.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.47 644[3:Rew:643.0,614.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.19/0.47 645[3:Rew:643.0,621.0] || -> equal(multiply(sk_c8,multiply(sk_c7,u)),u)**. % 0.19/0.47 646[3:Rew:640.0,645.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.47 647[3:Rew:646.0,623.0] || -> equal(multiply(sk_c3,u),u)**. % 0.19/0.47 650[3:Rew:647.0,616.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.47 653[3:Rew:650.0,639.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.47 654[3:Rew:650.0,644.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.47 661[3:Rew:653.0,636.7,650.0,636.7,653.0,636.6,631.0,636.6,653.0,636.5,650.0,636.5,653.0,636.4,650.0,636.3,650.0,636.1] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c7)** equal(inverse(x),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) equal(w,sk_c7) equal(x,sk_c7) -> . % 0.19/0.47 662[3:Con:661.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.47 713[3:SpL:654.0,662.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.47 714[3:Obv:713.1] || -> . % 0.19/0.47 715[2:Spt:714.0,24.0,392.0] || equal(inverse(sk_c5),sk_c7)** -> . % 0.19/0.47 716[2:Spt:714.0,24.1] || -> equal(inverse(sk_c3),sk_c7)**. % 0.19/0.47 718[2:MRR:8.0,715.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.47 719[2:MRR:20.0,715.0] || -> equal(multiply(sk_c3,sk_c7),sk_c8)**. % 0.19/0.47 721[2:MRR:4.0,715.0] || -> equal(multiply(sk_c1,sk_c8),sk_c7)**. % 0.19/0.47 722[2:SpR:716.0,59.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.19/0.47 726[2:SpR:718.0,59.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.19/0.47 732[2:SpR:719.0,59.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c7)**. % 0.19/0.47 734[2:Rew:1.0,732.0,716.0,732.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.47 736[2:Rew:734.0,77.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.19/0.47 739[2:Rew:734.0,390.4] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(inverse(x),sk_c8) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(x,sk_c8),sk_c7)** -> . % 0.19/0.47 741[2:Rew:28.0,736.0] || -> equal(identity,sk_c8)**. % 0.19/0.47 742[2:Rew:741.0,27.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.47 743[2:Rew:741.0,92.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.47 746[2:Rew:742.0,726.0] || -> equal(multiply(sk_c1,u),u)**. % 0.19/0.47 747[2:Rew:743.0,721.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.47 748[2:Rew:747.0,718.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.19/0.47 749[2:Rew:747.0,746.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.47 751[2:Rew:749.0,722.0] || -> equal(multiply(sk_c3,u),u)**. % 0.19/0.47 752[2:Rew:751.0,719.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.47 755[2:Rew:752.0,743.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.47 756[2:Rew:752.0,748.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.47 761[2:Rew:755.0,739.7,752.0,739.7,755.0,739.6,734.0,739.6,755.0,739.5,752.0,739.5,755.0,739.4,752.0,739.3,752.0,739.1] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c7)** equal(inverse(x),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) equal(w,sk_c7) equal(x,sk_c7) -> . % 0.19/0.47 762[2:Con:761.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.47 820[2:SpL:756.0,762.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.47 822[2:Obv:820.1] || -> . % 0.19/0.47 % SZS output end Refutation % 0.19/0.47 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 prove_this_6 prove_this_7 prove_this_8 prove_this_9 prove_this_14 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 left_identity left_inverse associativity % 0.19/0.47 %------------------------------------------------------------------------------