%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP351-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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:58 EDT 2022 % Result : Unsatisfiable 0.22s 0.49s % Output : Refutation 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GRP351-1 : TPTP v8.1.0. Released v2.5.0. % 0.12/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n027.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 04:14:18 EDT 2022 % 0.13/0.35 % CPUTime : % 0.22/0.49 % 0.22/0.49 SPASS V 3.9 % 0.22/0.49 SPASS beiseite: Proof found. % 0.22/0.49 % SZS status Theorem % 0.22/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.22/0.49 SPASS derived 815 clauses, backtracked 367 clauses, performed 13 splits and kept 733 clauses. % 0.22/0.49 SPASS allocated 63588 KBytes. % 0.22/0.49 SPASS spent 0:00:00.13 on the problem. % 0.22/0.49 0:00:00.03 for the input. % 0.22/0.49 0:00:00.00 for the FLOTTER CNF translation. % 0.22/0.49 0:00:00.01 for inferences. % 0.22/0.49 0:00:00.00 for the backtracking. % 0.22/0.49 0:00:00.06 for the reduction. % 0.22/0.49 % 0.22/0.49 % 0.22/0.49 Here is a proof with depth 4, length 301 : % 0.22/0.49 % SZS output start Refutation % 0.22/0.49 1[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.22/0.49 2[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.22/0.49 3[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 4[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 5[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.22/0.49 6[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.49 8[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.49 9[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.49 10[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.49 11[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.22/0.49 12[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.22/0.49 13[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(inverse(sk_c1),sk_c7)**. % 0.22/0.49 14[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(inverse(sk_c1),sk_c7)**. % 0.22/0.49 15[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.22/0.49 16[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 17[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 18[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 19[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 20[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 21[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.22/0.49 22[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.22/0.49 23[0:Inp] || -> equal(inverse(sk_c3),sk_c6) equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 24[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 25[0:Inp] || -> equal(inverse(sk_c2),sk_c6) equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.22/0.49 26[0:Inp] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(inverse(x),sk_c7) equal(multiply(u,sk_c6),sk_c5)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c6),sk_c5)** equal(multiply(x,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.22/0.49 27[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.22/0.49 28[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.22/0.49 29[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.22/0.49 30[1:Spt:26.2,26.6] || equal(inverse(u),sk_c6) equal(multiply(u,sk_c6),sk_c5)** -> . % 0.22/0.49 31[2:Spt:1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.22/0.49 33[3:Spt:4.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.22/0.49 35[4:Spt:3.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.22/0.49 39[5:Spt:5.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.22/0.49 41[5:SpL:39.0,30.1] || equal(inverse(sk_c4),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.22/0.49 42[5:Obv:41.1] || equal(inverse(sk_c4),sk_c6)** -> . % 0.22/0.49 43[5:Rew:33.0,42.0] || equal(sk_c5,sk_c6)** -> . % 0.22/0.49 44[6:Spt:2.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.22/0.49 52[1:SpL:28.0,30.1] || equal(inverse(inverse(sk_c6)),sk_c6)** equal(identity,sk_c5) -> . % 0.22/0.49 59[0:SpR:28.0,29.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.22/0.49 61[0:Rew:27.0,59.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.22/0.49 76[0:SpR:61.0,61.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.22/0.49 79[6:SpR:44.0,61.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.22/0.49 80[2:SpR:31.0,61.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.22/0.49 83[0:SpR:28.0,61.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.22/0.49 91[6:Rew:31.0,79.0,35.0,79.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 92[6:MRR:91.0,43.0] || -> . % 0.22/0.49 95[0:Rew:76.0,83.0] || -> equal(multiply(u,identity),u)**. % 0.22/0.49 102[6:Spt:92.0,2.0,44.0] || equal(multiply(sk_c3,sk_c6),sk_c7)** -> . % 0.22/0.49 103[6:Spt:92.0,2.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 104[6:MRR:22.1,102.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 106[6:MRR:17.0,102.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 129[6:SpL:106.0,30.1] || equal(inverse(sk_c2),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.22/0.49 145[6:Obv:129.1] || equal(inverse(sk_c2),sk_c6)** -> . % 0.22/0.49 146[6:Rew:104.0,145.0] || equal(sk_c6,sk_c6)* -> . % 0.22/0.49 147[6:Obv:146.0] || -> . % 0.22/0.49 148[5:Spt:147.0,5.0,39.0] || equal(multiply(sk_c4,sk_c6),sk_c5)** -> . % 0.22/0.49 149[5:Spt:147.0,5.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 152[5:MRR:25.1,148.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 156[5:MRR:20.0,148.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 171[5:SpL:156.0,30.1] || equal(inverse(sk_c2),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.22/0.49 186[5:Obv:171.1] || equal(inverse(sk_c2),sk_c6)** -> . % 0.22/0.49 187[5:Rew:152.0,186.0] || equal(sk_c6,sk_c6)* -> . % 0.22/0.49 188[5:Obv:187.0] || -> . % 0.22/0.49 189[4:Spt:188.0,3.0,35.0] || equal(inverse(sk_c3),sk_c6)** -> . % 0.22/0.49 190[4:Spt:188.0,3.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 191[4:MRR:23.0,189.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 193[4:MRR:18.0,189.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 196[4:SpR:190.0,61.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c5)**. % 0.22/0.49 209[4:SpR:193.0,61.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.22/0.49 211[4:Rew:190.0,209.0,191.0,209.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 215[4:Rew:211.0,80.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.22/0.49 219[4:Rew:211.0,196.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.22/0.49 222[4:Rew:28.0,219.0] || -> equal(identity,sk_c5)**. % 0.22/0.49 228[4:Rew:222.0,95.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.49 229[4:Rew:222.0,52.1] || equal(inverse(inverse(sk_c6)),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.22/0.49 236[4:Rew:228.0,215.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.22/0.49 248[4:Obv:229.1] || equal(inverse(inverse(sk_c6)),sk_c6)** -> . % 0.22/0.49 249[4:Rew:236.0,248.0,236.0,248.0] || equal(sk_c6,sk_c6)* -> . % 0.22/0.49 250[4:Obv:249.0] || -> . % 0.22/0.49 251[3:Spt:250.0,4.0,33.0] || equal(inverse(sk_c4),sk_c5)** -> . % 0.22/0.49 252[3:Spt:250.0,4.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 253[3:MRR:24.0,251.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 255[3:MRR:19.0,251.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 258[3:SpR:252.0,61.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c5)**. % 0.22/0.49 269[3:SpR:255.0,61.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.22/0.49 271[3:Rew:252.0,269.0,253.0,269.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 275[3:Rew:271.0,80.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.22/0.49 279[3:Rew:271.0,258.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.22/0.49 281[3:Rew:28.0,279.0] || -> equal(identity,sk_c5)**. % 0.22/0.49 283[3:Rew:281.0,95.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.49 287[3:Rew:281.0,52.1] || equal(inverse(inverse(sk_c6)),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.22/0.49 288[3:Rew:283.0,275.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.22/0.49 295[3:Obv:287.1] || equal(inverse(inverse(sk_c6)),sk_c6)** -> . % 0.22/0.49 296[3:Rew:288.0,295.0,288.0,295.0] || equal(sk_c6,sk_c6)* -> . % 0.22/0.49 297[3:Obv:296.0] || -> . % 0.22/0.49 298[2:Spt:297.0,1.0,31.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.22/0.49 299[2:Spt:297.0,1.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 300[2:MRR:21.1,298.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 302[2:MRR:16.0,298.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 314[2:SpL:302.0,30.1] || equal(inverse(sk_c2),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.22/0.49 331[2:Obv:314.1] || equal(inverse(sk_c2),sk_c6)** -> . % 0.22/0.49 332[2:Rew:300.0,331.0] || equal(sk_c6,sk_c6)* -> . % 0.22/0.49 333[2:Obv:332.0] || -> . % 0.22/0.49 336[1:Spt:333.0,26.0,26.1,26.3,26.4,26.5,26.7,26.8,26.9] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c5)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.22/0.49 338[2:Spt:1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.22/0.49 339[2:Rew:338.0,336.6] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c5,sk_c5) equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.22/0.49 341[2:Obv:339.6] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.22/0.49 344[2:SpR:338.0,61.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.22/0.49 346[3:Spt:3.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 348[3:Rew:346.0,341.6] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c7,sk_c7) -> . % 0.22/0.49 349[3:Obv:348.6] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.22/0.49 352[3:SpR:346.0,61.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c5)**. % 0.22/0.49 354[4:Spt:24.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.22/0.49 360[5:Spt:23.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.22/0.49 363[6:Spt:25.1] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.22/0.49 365[6:SpR:363.0,61.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c6)**. % 0.22/0.49 367[6:Rew:354.0,365.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.22/0.49 371[4:SpR:354.0,28.0] || -> equal(multiply(sk_c5,sk_c4),identity)**. % 0.22/0.49 372[5:SpR:360.0,28.0] || -> equal(multiply(sk_c6,sk_c3),identity)**. % 0.22/0.49 375[6:SpR:367.0,29.0] || -> equal(multiply(sk_c5,multiply(sk_c5,u)),multiply(sk_c6,u))**. % 0.22/0.49 379[4:SpR:371.0,61.0] || -> equal(multiply(inverse(sk_c5),identity),sk_c4)**. % 0.22/0.49 381[4:Rew:95.0,379.0] || -> equal(inverse(sk_c5),sk_c4)**. % 0.22/0.49 385[4:SpR:381.0,28.0] || -> equal(multiply(sk_c4,sk_c5),identity)**. % 0.22/0.49 388[5:SpR:372.0,61.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c3)**. % 0.22/0.49 390[5:Rew:95.0,388.0] || -> equal(inverse(sk_c6),sk_c3)**. % 0.22/0.49 392[5:Rew:390.0,352.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.22/0.49 394[7:Spt:22.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 396[7:SpR:394.0,28.0] || -> equal(multiply(sk_c6,sk_c2),identity)**. % 0.22/0.49 399[5:SpR:390.0,28.0] || -> equal(multiply(sk_c3,sk_c6),identity)**. % 0.22/0.49 402[5:Rew:399.0,17.0] || -> equal(identity,sk_c7) equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 403[5:Rew:399.0,12.1] || -> equal(inverse(sk_c1),sk_c7)** equal(identity,sk_c7). % 0.22/0.49 417[8:Spt:403.1] || -> equal(identity,sk_c7)**. % 0.22/0.49 423[8:Rew:417.0,95.0] || -> equal(multiply(u,sk_c7),u)**. % 0.22/0.49 426[8:Rew:417.0,399.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.22/0.49 431[8:Rew:423.0,392.0] || -> equal(sk_c3,sk_c5)**. % 0.22/0.49 432[8:Rew:423.0,338.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 434[8:Rew:423.0,349.5] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c7)** equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c7)** equal(w,sk_c6) -> . % 0.22/0.49 435[8:Rew:431.0,360.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.22/0.49 443[8:Rew:432.0,363.0] || -> equal(multiply(sk_c4,sk_c6),sk_c6)**. % 0.22/0.49 445[8:Rew:432.0,381.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.22/0.49 452[8:Rew:432.0,431.0] || -> equal(sk_c3,sk_c6)**. % 0.22/0.49 453[8:Rew:432.0,435.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.22/0.49 455[8:Rew:453.0,445.0] || -> equal(sk_c4,sk_c6)**. % 0.22/0.49 457[8:Rew:452.0,426.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.22/0.49 460[8:Rew:457.0,443.0,455.0,443.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 463[8:Rew:460.0,423.0] || -> equal(multiply(u,sk_c6),u)**. % 0.22/0.49 483[8:Rew:463.0,434.4,460.0,434.4,463.0,434.3,432.0,434.3,460.0,434.2,432.0,434.0] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(inverse(w),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) equal(w,sk_c6) -> . % 0.22/0.49 484[8:Con:483.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.22/0.49 545[8:SpL:453.0,484.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.22/0.49 547[8:Obv:545.1] || -> . % 0.22/0.49 548[8:Spt:547.0,403.1,417.0] || equal(identity,sk_c7)** -> . % 0.22/0.49 549[8:Spt:547.0,403.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.22/0.49 551[8:MRR:402.0,548.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 584[8:SpR:551.0,61.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.22/0.49 586[8:Rew:394.0,584.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.22/0.49 587[8:Rew:346.0,586.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 589[8:Rew:587.0,548.0] || equal(identity,sk_c6)** -> . % 0.22/0.49 592[8:Rew:587.0,392.0] || -> equal(multiply(sk_c3,sk_c6),sk_c5)**. % 0.22/0.49 604[8:Rew:399.0,592.0] || -> equal(identity,sk_c5)**. % 0.22/0.49 608[8:Rew:604.0,27.0] || -> equal(multiply(sk_c5,u),u)**. % 0.22/0.49 610[8:Rew:604.0,396.0] || -> equal(multiply(sk_c6,sk_c2),sk_c5)**. % 0.22/0.49 614[8:Rew:604.0,589.0] || equal(sk_c5,sk_c6)** -> . % 0.22/0.49 618[8:Rew:608.0,375.0] || -> equal(multiply(sk_c5,u),multiply(sk_c6,u))**. % 0.22/0.49 640[8:Rew:608.0,618.0] || -> equal(multiply(sk_c6,u),u)**. % 0.22/0.49 641[8:Rew:640.0,610.0] || -> equal(sk_c2,sk_c5)**. % 0.22/0.49 646[8:Rew:641.0,551.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.22/0.49 651[8:Rew:608.0,646.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 652[8:MRR:651.0,614.0] || -> . % 0.22/0.49 665[7:Spt:652.0,22.0,394.0] || equal(inverse(sk_c2),sk_c6)** -> . % 0.22/0.49 666[7:Spt:652.0,22.1] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.22/0.49 667[7:Rew:399.0,666.0] || -> equal(identity,sk_c7)**. % 0.22/0.49 671[7:Rew:667.0,95.0] || -> equal(multiply(u,sk_c7),u)**. % 0.22/0.49 672[7:Rew:667.0,399.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.22/0.49 674[7:Rew:671.0,338.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 675[7:Rew:671.0,392.0] || -> equal(sk_c3,sk_c5)**. % 0.22/0.49 680[7:Rew:674.0,367.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.22/0.49 684[7:Rew:674.0,675.0] || -> equal(sk_c3,sk_c6)**. % 0.22/0.49 686[7:Rew:684.0,390.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.22/0.49 691[7:Rew:684.0,672.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.22/0.49 693[7:Rew:691.0,680.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 695[7:Rew:693.0,671.0] || -> equal(multiply(u,sk_c6),u)**. % 0.22/0.49 717[7:Rew:695.0,349.5,693.0,349.5,695.0,349.4,693.0,349.4,695.0,349.3,674.0,349.3,693.0,349.2,674.0,349.0] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(inverse(w),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) equal(w,sk_c6) -> . % 0.22/0.49 718[7:Con:717.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.22/0.49 778[7:SpL:686.0,718.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.22/0.49 780[7:Obv:778.1] || -> . % 0.22/0.49 781[6:Spt:780.0,25.1,363.0] || equal(multiply(sk_c4,sk_c6),sk_c5)** -> . % 0.22/0.49 782[6:Spt:780.0,25.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 783[6:MRR:15.1,781.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.22/0.49 784[6:MRR:20.0,781.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 785[6:MRR:10.0,781.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.49 799[6:SpR:784.0,61.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.22/0.49 801[6:Rew:782.0,799.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.22/0.49 802[6:Rew:346.0,801.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 803[6:Rew:802.0,783.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.22/0.49 804[6:Rew:802.0,392.0] || -> equal(multiply(sk_c3,sk_c6),sk_c5)**. % 0.22/0.49 805[6:Rew:802.0,338.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.22/0.49 812[6:Rew:802.0,785.0] || -> equal(multiply(sk_c1,sk_c6),sk_c6)**. % 0.22/0.49 816[6:Rew:399.0,804.0] || -> equal(identity,sk_c5)**. % 0.22/0.49 817[6:Rew:816.0,27.0] || -> equal(multiply(sk_c5,u),u)**. % 0.22/0.49 819[6:Rew:816.0,95.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.49 820[6:Rew:816.0,385.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.22/0.49 833[6:Rew:819.0,820.0] || -> equal(sk_c4,sk_c5)**. % 0.22/0.49 836[6:Rew:833.0,781.0] || equal(multiply(sk_c5,sk_c6),sk_c5)** -> . % 0.22/0.49 842[6:Rew:817.0,836.0] || equal(sk_c5,sk_c6)** -> . % 0.22/0.49 869[6:SpR:812.0,61.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c6)**. % 0.22/0.49 871[6:Rew:805.0,869.0,803.0,869.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 872[6:MRR:871.0,842.0] || -> . % 0.22/0.49 873[5:Spt:872.0,23.0,360.0] || equal(inverse(sk_c3),sk_c6)** -> . % 0.22/0.49 874[5:Spt:872.0,23.1] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 875[5:MRR:13.0,873.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.22/0.49 876[5:MRR:18.0,873.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 877[5:MRR:8.0,873.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.49 903[5:SpR:876.0,61.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.22/0.49 905[5:Rew:346.0,903.0,874.0,903.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 906[5:Rew:905.0,875.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.22/0.49 908[5:Rew:905.0,338.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.22/0.49 909[5:Rew:905.0,352.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.22/0.49 910[5:Rew:905.0,344.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.22/0.49 913[5:Rew:905.0,877.0] || -> equal(multiply(sk_c1,sk_c6),sk_c6)**. % 0.22/0.49 914[5:Rew:905.0,349.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.22/0.49 917[5:Rew:28.0,909.0] || -> equal(identity,sk_c5)**. % 0.22/0.49 920[5:Rew:917.0,95.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.49 930[5:Rew:920.0,910.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.22/0.49 937[5:Rew:905.0,914.5,905.0,914.4] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c6)** equal(multiply(w,sk_c6),sk_c6)** -> . % 0.22/0.49 938[5:Con:937.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c6)** -> . % 0.22/0.49 950[5:SpR:913.0,61.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c6)**. % 0.22/0.49 952[5:Rew:906.0,950.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.22/0.49 953[5:Rew:908.0,952.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 959[5:Rew:953.0,920.0] || -> equal(multiply(u,sk_c6),u)**. % 0.22/0.49 962[5:Rew:953.0,938.0] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c6)** -> . % 0.22/0.49 976[5:Rew:959.0,962.3,959.0,962.2,953.0,962.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.22/0.49 977[5:Con:976.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.22/0.49 1007[5:SpL:930.0,977.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.22/0.49 1008[5:Obv:1007.1] || -> . % 0.22/0.49 1009[4:Spt:1008.0,24.0,354.0] || equal(inverse(sk_c4),sk_c5)** -> . % 0.22/0.49 1010[4:Spt:1008.0,24.1] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 1011[4:MRR:14.0,1009.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.22/0.49 1012[4:MRR:19.0,1009.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 1013[4:MRR:9.0,1009.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.49 1025[4:SpR:1012.0,61.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.22/0.49 1027[4:Rew:346.0,1025.0,1010.0,1025.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 1028[4:Rew:1027.0,1011.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.22/0.49 1029[4:Rew:1027.0,338.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.22/0.49 1031[4:Rew:1027.0,344.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.22/0.49 1032[4:Rew:1027.0,352.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.22/0.49 1035[4:Rew:1027.0,1013.0] || -> equal(multiply(sk_c1,sk_c6),sk_c6)**. % 0.22/0.49 1036[4:Rew:1027.0,349.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.22/0.49 1039[4:Rew:28.0,1032.0] || -> equal(identity,sk_c5)**. % 0.22/0.49 1041[4:Rew:1039.0,95.0] || -> equal(multiply(u,sk_c5),u)**. % 0.22/0.49 1044[4:Rew:1041.0,1031.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.22/0.49 1048[4:Rew:1027.0,1036.5,1027.0,1036.4] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(inverse(w),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c6)** equal(multiply(w,sk_c6),sk_c6)** -> . % 0.22/0.49 1049[4:Con:1048.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c6)** -> . % 0.22/0.49 1059[4:SpR:1035.0,61.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c6)**. % 0.22/0.49 1061[4:Rew:1028.0,1059.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.22/0.49 1062[4:Rew:1029.0,1061.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 1068[4:Rew:1062.0,1041.0] || -> equal(multiply(u,sk_c6),u)**. % 0.22/0.49 1071[4:Rew:1062.0,1049.0] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c6),sk_c6)** -> . % 0.22/0.49 1086[4:Rew:1068.0,1071.3,1068.0,1071.2,1062.0,1071.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.22/0.49 1087[4:Con:1086.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.22/0.49 1118[4:SpL:1044.0,1087.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.22/0.49 1120[4:Obv:1118.1] || -> . % 0.22/0.49 1121[3:Spt:1120.0,3.1,346.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.22/0.49 1122[3:Spt:1120.0,3.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.22/0.49 1123[3:MRR:4.1,1121.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.22/0.49 1124[3:MRR:2.1,1121.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.22/0.49 1125[3:MRR:5.1,1121.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.22/0.49 1134[3:SpR:1124.0,61.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c6)**. % 0.22/0.49 1136[3:Rew:338.0,1134.0,1122.0,1134.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 1137[3:Rew:1136.0,1123.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.22/0.49 1139[3:Rew:1136.0,344.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c7)**. % 0.22/0.49 1140[3:Rew:1136.0,1121.0] || equal(multiply(sk_c6,sk_c6),sk_c7)** -> . % 0.22/0.49 1142[3:Rew:1136.0,1125.0] || -> equal(multiply(sk_c4,sk_c6),sk_c6)**. % 0.22/0.49 1144[3:Rew:28.0,1139.0] || -> equal(identity,sk_c7)**. % 0.22/0.49 1147[3:Rew:1144.0,28.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.22/0.49 1156[3:SpR:1142.0,61.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c6)**. % 0.22/0.49 1158[3:Rew:1137.0,1156.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.22/0.49 1159[3:Rew:1158.0,1140.0] || equal(sk_c7,sk_c6)** -> . % 0.22/0.49 1161[3:SpR:1158.0,61.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c6)**. % 0.22/0.49 1163[3:Rew:1147.0,1161.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 1164[3:MRR:1163.0,1159.0] || -> . % 0.22/0.49 1165[2:Spt:1164.0,1.0,338.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.22/0.49 1166[2:Spt:1164.0,1.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.22/0.49 1167[2:MRR:21.1,1165.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.22/0.49 1168[2:MRR:11.1,1165.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.22/0.49 1169[2:MRR:16.0,1165.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.22/0.49 1170[2:MRR:6.0,1165.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.22/0.49 1172[2:SpR:1166.0,61.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c5)**. % 0.22/0.49 1179[2:SpR:1169.0,61.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c6)**. % 0.22/0.49 1181[2:Rew:1166.0,1179.0,1167.0,1179.0] || -> equal(sk_c7,sk_c6)**. % 0.22/0.49 1183[2:Rew:1181.0,1168.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.22/0.49 1184[2:Rew:1181.0,1165.0] || equal(multiply(sk_c6,sk_c6),sk_c5)** -> . % 0.22/0.49 1185[2:Rew:1181.0,1170.0] || -> equal(multiply(sk_c1,sk_c6),sk_c6)**. % 0.22/0.49 1186[2:Rew:1181.0,1172.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.22/0.49 1189[2:Rew:28.0,1186.0] || -> equal(identity,sk_c5)**. % 0.22/0.49 1193[2:Rew:1189.0,28.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.22/0.49 1201[2:SpR:1185.0,61.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c6)**. % 0.22/0.49 1203[2:Rew:1183.0,1201.0] || -> equal(multiply(sk_c6,sk_c6),sk_c6)**. % 0.22/0.49 1204[2:Rew:1203.0,1184.0] || equal(sk_c5,sk_c6)** -> . % 0.22/0.49 1206[2:SpR:1203.0,61.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c6)**. % 0.22/0.49 1208[2:Rew:1193.0,1206.0] || -> equal(sk_c5,sk_c6)**. % 0.22/0.49 1209[2:MRR:1208.0,1204.0] || -> . % 0.22/0.49 % SZS output end Refutation % 0.22/0.49 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 prove_this_5 prove_this_6 prove_this_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 left_identity left_inverse associativity % 0.22/0.49 %------------------------------------------------------------------------------