%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP327-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n026.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:46:52 EDT 2022 % Result : Unsatisfiable 0.19s 0.47s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GRP327-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.13 % Command : run_spass %d %s % 0.12/0.34 % Computer : n026.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 18:44:21 EDT 2022 % 0.12/0.34 % CPUTime : % 0.19/0.47 % 0.19/0.47 SPASS V 3.9 % 0.19/0.47 SPASS beiseite: Proof found. % 0.19/0.47 % SZS status Theorem % 0.19/0.47 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.19/0.47 SPASS derived 693 clauses, backtracked 308 clauses, performed 12 splits and kept 566 clauses. % 0.19/0.47 SPASS allocated 63594 KBytes. % 0.19/0.47 SPASS spent 0:00:00.12 on the problem. % 0.19/0.47 0:00:00.03 for the input. % 0.19/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.47 0:00:00.00 for inferences. % 0.19/0.47 0:00:00.00 for the backtracking. % 0.19/0.47 0:00:00.06 for the reduction. % 0.19/0.47 % 0.19/0.47 % 0.19/0.47 Here is a proof with depth 5, length 290 : % 0.19/0.47 % SZS output start Refutation % 0.19/0.47 1[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c6)**. % 0.19/0.47 2[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.47 3[0:Inp] || -> equal(multiply(sk_c6,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.47 4[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.47 5[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c8)** equal(multiply(sk_c1,sk_c7),sk_c8). % 0.19/0.47 6[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.47 7[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c7)** equal(multiply(sk_c1,sk_c7),sk_c8). % 0.19/0.47 8[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 9[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.19/0.47 10[0:Inp] || -> equal(inverse(sk_c4),sk_c8)** equal(inverse(sk_c1),sk_c7). % 0.19/0.47 11[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.47 12[0:Inp] || -> equal(inverse(sk_c5),sk_c7)** equal(inverse(sk_c1),sk_c7). % 0.19/0.47 13[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.47 14[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.47 16[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.47 18[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.47 19[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c7)** equal(multiply(sk_c8,sk_c3),sk_c7). % 0.19/0.47 20[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.47 22[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.47 24[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.47 25[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c7) equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.47 26[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(inverse(sk_c2),sk_c8)**. % 0.19/0.47 28[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c2),sk_c8)**. % 0.19/0.47 30[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(inverse(sk_c2),sk_c8)**. % 0.19/0.47 31[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.47 32[0:Inp] || equal(multiply(sk_c7,sk_c8),sk_c6) equal(multiply(u,sk_c7),sk_c8)** equal(inverse(u),sk_c7) equal(multiply(sk_c8,v),sk_c7)** equal(multiply(w,sk_c8),v)* equal(inverse(w),sk_c8) equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c6,sk_c8),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.47 33[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.47 34[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.47 35[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.47 36[0:Rew:1.0,32.0] || equal(sk_c6,sk_c6) equal(multiply(u,sk_c7),sk_c8)** equal(inverse(u),sk_c7) equal(multiply(sk_c8,v),sk_c7)** equal(multiply(w,sk_c8),v)* equal(inverse(w),sk_c8) equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c6,sk_c8),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.47 37[0:Obv:36.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(x),sk_c7) equal(inverse(sk_c7),sk_c6) equal(multiply(w,sk_c8),y)*+ equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(x,sk_c7),sk_c8)** equal(multiply(sk_c8,y),sk_c7)** equal(multiply(sk_c6,sk_c8),sk_c7)** -> . % 0.19/0.47 38[1:Spt:37.3,37.8] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c8)** -> . % 0.19/0.47 41[2:Spt:8.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 48[3:Spt:2.1] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.47 50[3:SpL:48.0,38.1] || equal(inverse(sk_c1),sk_c7)** equal(sk_c8,sk_c8) -> . % 0.19/0.47 51[3:Obv:50.1] || equal(inverse(sk_c1),sk_c7)** -> . % 0.19/0.47 52[3:Rew:41.0,51.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.47 53[3:Obv:52.0] || -> . % 0.19/0.47 54[3:Spt:53.0,2.1,48.0] || equal(multiply(sk_c1,sk_c7),sk_c8)** -> . % 0.19/0.47 55[3:Spt:53.0,2.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.19/0.47 56[3:MRR:6.1,54.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.19/0.47 57[3:MRR:4.1,54.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.47 58[3:MRR:7.1,54.0] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.47 59[3:MRR:5.1,54.0] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.47 60[3:MRR:3.1,54.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.19/0.47 66[3:SpL:59.0,38.1] || equal(inverse(sk_c4),sk_c7)** equal(sk_c8,sk_c8) -> . % 0.19/0.47 67[3:Obv:66.1] || equal(inverse(sk_c4),sk_c7)** -> . % 0.19/0.47 68[3:Rew:57.0,67.0] || equal(sk_c8,sk_c7)** -> . % 0.19/0.47 74[2:SpR:41.0,34.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.19/0.47 75[3:SpR:55.0,34.0] || -> equal(multiply(sk_c6,sk_c7),identity)**. % 0.19/0.47 76[3:SpR:56.0,34.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.19/0.47 77[3:SpR:57.0,34.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.19/0.47 78[1:SpL:34.0,38.1] || equal(inverse(inverse(sk_c7)),sk_c7)** equal(identity,sk_c8) -> . % 0.19/0.47 88[3:SpR:75.0,35.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(identity,u))**. % 0.19/0.47 91[3:SpR:60.0,35.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),multiply(sk_c7,u))**. % 0.19/0.47 94[3:SpR:58.0,35.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.19/0.47 96[0:SpR:34.0,35.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.47 100[3:Rew:33.0,88.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.19/0.47 104[0:Rew:33.0,96.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.47 111[3:SpR:1.0,100.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.19/0.47 112[3:SpR:74.0,100.0] || -> equal(multiply(sk_c6,identity),sk_c1)**. % 0.19/0.47 113[3:SpR:76.0,100.0] || -> equal(multiply(sk_c6,identity),sk_c5)**. % 0.19/0.47 114[3:Rew:112.0,113.0] || -> equal(sk_c5,sk_c1)**. % 0.19/0.47 118[3:Rew:114.0,94.0] || -> equal(multiply(sk_c1,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.19/0.47 122[3:SpR:111.0,35.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.19/0.47 126[3:SpR:112.0,35.0] || -> equal(multiply(sk_c6,multiply(identity,u)),multiply(sk_c1,u))**. % 0.19/0.47 128[3:Rew:33.0,126.0] || -> equal(multiply(sk_c1,u),multiply(sk_c6,u))**. % 0.19/0.47 131[3:Rew:128.0,118.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.19/0.47 136[3:Rew:122.0,131.0] || -> equal(multiply(sk_c8,u),multiply(sk_c7,u))**. % 0.19/0.47 137[3:Rew:136.0,77.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.47 146[3:Rew:136.0,91.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.19/0.47 148[3:Rew:100.0,146.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.47 149[3:Rew:148.0,100.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.47 150[3:Rew:148.0,74.0] || -> equal(identity,sk_c1)**. % 0.19/0.47 151[3:Rew:148.0,1.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.47 158[3:Rew:148.0,137.0] || -> equal(identity,sk_c4)**. % 0.19/0.47 165[3:Rew:150.0,75.0] || -> equal(multiply(sk_c6,sk_c7),sk_c1)**. % 0.19/0.47 175[3:Rew:150.0,158.0] || -> equal(sk_c4,sk_c1)**. % 0.19/0.47 177[3:Rew:175.0,59.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.47 182[3:Rew:151.0,149.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.47 187[3:Rew:182.0,165.0,151.0,165.0] || -> equal(sk_c1,sk_c7)**. % 0.19/0.47 202[3:Rew:148.0,177.0,187.0,177.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.47 203[3:MRR:202.0,68.0] || -> . % 0.19/0.47 210[2:Spt:203.0,8.1,41.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.19/0.47 211[2:Spt:203.0,8.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.19/0.47 212[2:MRR:12.1,210.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.19/0.47 214[2:MRR:13.0,210.0] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.47 216[2:MRR:9.0,210.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.19/0.47 217[2:Rew:211.0,78.0] || equal(inverse(sk_c6),sk_c7)** equal(identity,sk_c8) -> . % 0.19/0.47 241[2:SpR:211.0,34.0] || -> equal(multiply(sk_c6,sk_c7),identity)**. % 0.19/0.47 243[2:SpR:212.0,34.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.19/0.47 249[2:SpR:241.0,35.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(identity,u))**. % 0.19/0.47 251[2:Rew:33.0,249.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.19/0.47 264[2:SpR:243.0,251.0] || -> equal(multiply(sk_c6,identity),sk_c5)**. % 0.19/0.47 269[0:SpR:104.0,104.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.47 274[0:SpR:1.0,104.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c8)**. % 0.19/0.47 275[2:SpR:216.0,104.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c8)**. % 0.19/0.47 279[2:SpR:214.0,104.0] || -> equal(multiply(inverse(sk_c5),sk_c7),sk_c6)**. % 0.19/0.47 281[0:SpR:34.0,104.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.47 283[2:SpR:251.0,104.0] || -> equal(multiply(inverse(sk_c6),u),multiply(sk_c7,u))**. % 0.19/0.47 296[2:Rew:212.0,279.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.47 303[2:Rew:283.0,275.0] || -> equal(multiply(sk_c7,sk_c7),sk_c8)**. % 0.19/0.47 304[2:Rew:296.0,303.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.47 306[2:Rew:304.0,1.0] || -> equal(multiply(sk_c7,sk_c8),sk_c8)**. % 0.19/0.47 314[2:Rew:304.0,217.0] || equal(inverse(sk_c8),sk_c7)** equal(identity,sk_c8) -> . % 0.19/0.47 317[2:Rew:304.0,264.0] || -> equal(multiply(sk_c8,identity),sk_c5)**. % 0.19/0.47 333[0:Rew:269.0,281.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.47 334[2:Rew:333.0,317.0] || -> equal(sk_c5,sk_c8)**. % 0.19/0.47 335[2:Rew:334.0,212.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.19/0.47 336[2:Rew:334.0,243.0] || -> equal(multiply(sk_c7,sk_c8),identity)**. % 0.19/0.47 340[2:Rew:306.0,336.0] || -> equal(identity,sk_c8)**. % 0.19/0.47 358[2:Rew:340.0,314.1,335.0,314.0] || equal(sk_c7,sk_c7) equal(sk_c8,sk_c8)* -> . % 0.19/0.47 359[2:Obv:358.1] || -> . % 0.19/0.47 363[1:Spt:359.0,37.0,37.1,37.2,37.4,37.5,37.6,37.7,37.9,37.10] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(sk_c7),sk_c6) equal(multiply(w,sk_c8),x)*+ equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,x),sk_c7)** equal(multiply(sk_c6,sk_c8),sk_c7)** -> . % 0.19/0.47 364[1:EqR:363.4] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(sk_c7),sk_c6) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(w,sk_c8)),sk_c7)** equal(multiply(sk_c6,sk_c8),sk_c7) -> . % 0.19/0.47 366[2:Spt:8.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.19/0.47 368[2:Rew:366.0,274.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.19/0.47 370[2:Rew:366.0,364.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(sk_c6,sk_c6) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(w,sk_c8)),sk_c7)** equal(multiply(sk_c6,sk_c8),sk_c7) -> . % 0.19/0.47 371[2:Obv:370.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(w,sk_c8)),sk_c7)** equal(multiply(sk_c6,sk_c8),sk_c7) -> . % 0.19/0.47 374[2:SpR:366.0,104.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.19/0.47 376[3:Spt:9.1] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.19/0.47 379[3:Rew:376.0,371.6] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(w,sk_c8)),sk_c7)** equal(sk_c7,sk_c7) -> . % 0.19/0.47 380[3:Obv:379.6] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(w,sk_c8)),sk_c7)** -> . % 0.19/0.47 384[3:SpR:376.0,104.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c8)**. % 0.19/0.47 386[4:Spt:12.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.19/0.47 389[5:Spt:10.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.47 396[6:Spt:13.1] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.47 398[6:SpR:396.0,104.0] || -> equal(multiply(inverse(sk_c5),sk_c7),sk_c6)**. % 0.19/0.47 400[6:Rew:386.0,398.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.47 401[7:Spt:11.1] || -> equal(multiply(sk_c4,sk_c7),sk_c8)**. % 0.19/0.47 403[7:SpR:401.0,104.0] || -> equal(multiply(inverse(sk_c4),sk_c8),sk_c7)**. % 0.19/0.47 405[7:Rew:389.0,403.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.19/0.47 406[2:SpR:368.0,35.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.19/0.47 407[2:SpR:368.0,104.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c6)**. % 0.19/0.47 409[6:SpR:400.0,35.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.19/0.47 410[6:SpR:400.0,104.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.19/0.47 412[6:Rew:368.0,410.0,366.0,410.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.47 414[6:Rew:412.0,389.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.47 424[6:Rew:412.0,380.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(w,sk_c8)),sk_c7)** -> . % 0.19/0.47 425[6:Rew:412.0,384.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c7)**. % 0.19/0.47 427[7:Rew:412.0,405.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.19/0.47 428[6:Rew:412.0,407.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c6)**. % 0.19/0.47 429[7:Rew:400.0,427.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.47 430[7:Rew:429.0,366.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.47 434[7:Rew:429.0,374.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.19/0.47 439[7:Rew:434.0,409.0,429.0,409.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.47 446[7:Rew:439.0,424.5,412.0,424.5,412.0,424.4,429.0,424.3,412.0,424.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.19/0.47 447[7:Con:446.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.19/0.47 472[0:SpR:34.0,333.0] || -> equal(inverse(identity),identity)**. % 0.19/0.47 474[4:SpR:386.0,34.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.19/0.47 475[6:SpR:414.0,34.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.47 478[7:Rew:439.0,474.0] || -> equal(identity,sk_c5)**. % 0.19/0.47 480[7:Rew:478.0,333.0] || -> equal(multiply(u,sk_c5),u)**. % 0.19/0.47 482[7:Rew:478.0,472.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.47 483[7:Rew:386.0,482.0] || -> equal(sk_c5,sk_c7)**. % 0.19/0.47 493[7:Rew:483.0,480.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.47 494[7:Rew:493.0,447.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.47 520[7:SpL:430.0,494.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.47 521[7:Obv:520.1] || -> . % 0.19/0.47 522[7:Spt:521.0,11.1,401.0] || equal(multiply(sk_c4,sk_c7),sk_c8)** -> . % 0.19/0.47 523[7:Spt:521.0,11.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 524[6:Rew:425.0,428.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.47 531[7:Rew:412.0,522.0] || equal(multiply(sk_c4,sk_c7),sk_c7)** -> . % 0.19/0.47 533[6:Rew:524.0,374.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.19/0.47 538[6:Rew:533.0,409.0,524.0,409.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.47 543[6:Rew:538.0,475.0] || -> equal(identity,sk_c4)**. % 0.19/0.47 545[6:Rew:543.0,472.0] || -> equal(inverse(sk_c4),sk_c4)**. % 0.19/0.47 552[6:Rew:414.0,545.0] || -> equal(sk_c4,sk_c7)**. % 0.19/0.47 554[7:Rew:552.0,531.0] || equal(multiply(sk_c7,sk_c7),sk_c7)** -> . % 0.19/0.47 565[7:Rew:538.0,554.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.47 566[7:Obv:565.0] || -> . % 0.19/0.47 587[6:Spt:566.0,13.1,396.0] || equal(multiply(sk_c5,sk_c6),sk_c7)** -> . % 0.19/0.47 588[6:Spt:566.0,13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 589[6:MRR:31.1,587.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.47 590[6:MRR:7.0,587.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.47 591[6:MRR:19.0,587.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.47 592[6:MRR:25.0,587.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.47 600[6:SpR:589.0,104.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),u)**. % 0.19/0.47 615[6:SpR:590.0,104.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.19/0.47 617[6:Rew:1.0,615.0,588.0,615.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.47 624[6:Rew:617.0,587.0] || equal(multiply(sk_c5,sk_c7),sk_c7)** -> . % 0.19/0.47 625[6:Rew:617.0,374.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.19/0.47 627[6:Rew:617.0,406.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),multiply(sk_c8,u))**. % 0.19/0.47 634[6:Rew:625.0,627.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.47 637[6:Rew:634.0,600.0] || -> equal(multiply(sk_c2,u),u)**. % 0.19/0.47 638[6:Rew:634.0,591.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.47 640[6:Rew:638.0,592.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.47 641[6:Rew:637.0,640.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.47 647[6:Rew:641.0,634.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.47 651[6:Rew:647.0,474.0] || -> equal(identity,sk_c5)**. % 0.19/0.47 652[6:Rew:651.0,472.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.47 656[6:Rew:386.0,652.0] || -> equal(sk_c5,sk_c7)**. % 0.19/0.47 658[6:Rew:656.0,624.0] || equal(multiply(sk_c7,sk_c7),sk_c7)** -> . % 0.19/0.47 664[6:Rew:647.0,658.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.47 665[6:Obv:664.0] || -> . % 0.19/0.47 674[5:Spt:665.0,10.0,389.0] || equal(inverse(sk_c4),sk_c8)** -> . % 0.19/0.47 675[5:Spt:665.0,10.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.47 676[5:MRR:28.0,674.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 677[5:MRR:4.0,674.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 678[5:MRR:16.0,674.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 679[5:MRR:22.0,674.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 702[4:SpR:474.0,104.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c5)**. % 0.19/0.48 704[4:Rew:366.0,702.0] || -> equal(multiply(sk_c6,identity),sk_c5)**. % 0.19/0.48 705[4:Rew:333.0,704.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.48 706[4:Rew:705.0,386.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.19/0.48 707[4:Rew:705.0,474.0] || -> equal(multiply(sk_c7,sk_c6),identity)**. % 0.19/0.48 710[4:Rew:706.0,384.0] || -> equal(multiply(sk_c7,sk_c7),sk_c8)**. % 0.19/0.48 716[5:SpR:677.0,104.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.19/0.48 718[5:Rew:1.0,716.0,675.0,716.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 719[5:Rew:718.0,366.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.48 732[5:Rew:718.0,380.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(w,sk_c8)),sk_c7)** -> . % 0.19/0.48 733[5:Rew:718.0,707.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.19/0.48 734[5:Rew:710.0,733.0] || -> equal(identity,sk_c8)**. % 0.19/0.48 736[5:Rew:734.0,333.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.48 737[5:Rew:734.0,33.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.48 739[5:Rew:736.0,679.0] || -> equal(sk_c2,sk_c3)**. % 0.19/0.48 740[5:Rew:739.0,676.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.48 742[5:Rew:737.0,678.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.48 744[5:Rew:742.0,740.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.19/0.48 745[5:Rew:719.0,744.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 751[5:Rew:745.0,736.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.48 752[5:Rew:745.0,737.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.48 765[5:Rew:751.0,732.5,752.0,732.5,745.0,732.5,751.0,732.4,745.0,732.4,751.0,732.3,745.0,732.2,745.0,732.1] || 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.48 766[5:Con:765.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.48 830[5:SpL:719.0,766.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.48 832[5:Obv:830.1] || -> . % 0.19/0.48 833[4:Spt:832.0,12.0,386.0] || equal(inverse(sk_c5),sk_c7)** -> . % 0.19/0.48 834[4:Spt:832.0,12.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 835[4:MRR:30.0,833.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 836[4:MRR:6.0,833.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 837[4:MRR:18.0,833.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 838[4:MRR:24.0,833.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 843[4:SpR:835.0,104.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),u)**. % 0.19/0.48 859[4:SpR:836.0,104.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.19/0.48 861[4:Rew:1.0,859.0,834.0,859.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 862[4:Rew:861.0,366.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.19/0.48 868[4:Rew:861.0,374.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.19/0.48 870[4:Rew:861.0,406.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),multiply(sk_c8,u))**. % 0.19/0.48 874[4:Rew:861.0,380.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,multiply(w,sk_c8)),sk_c7)** -> . % 0.19/0.48 877[4:Rew:868.0,870.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.48 880[4:Rew:877.0,843.0] || -> equal(multiply(sk_c2,u),u)**. % 0.19/0.48 881[4:Rew:877.0,837.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.48 882[4:Rew:881.0,838.0] || -> equal(multiply(sk_c2,sk_c8),sk_c7)**. % 0.19/0.48 883[4:Rew:880.0,882.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 884[4:Rew:883.0,835.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.19/0.48 888[4:Rew:883.0,877.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.48 893[4:Rew:888.0,874.5,883.0,874.5,883.0,874.4,883.0,874.2,883.0,874.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.19/0.48 894[4:Con:893.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.19/0.48 917[4:SpR:880.0,333.0] || -> equal(identity,sk_c2)**. % 0.19/0.48 919[4:Rew:917.0,472.0] || -> equal(inverse(sk_c2),sk_c2)**. % 0.19/0.48 921[4:Rew:917.0,333.0] || -> equal(multiply(u,sk_c2),u)**. % 0.19/0.48 923[4:Rew:884.0,919.0] || -> equal(sk_c2,sk_c7)**. % 0.19/0.48 928[4:Rew:923.0,921.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.48 929[4:Rew:928.0,894.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.19/0.48 959[4:SpL:862.0,929.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.19/0.48 960[4:Obv:959.1] || -> . % 0.19/0.48 961[3:Spt:960.0,9.1,376.0] || equal(multiply(sk_c6,sk_c8),sk_c7)** -> . % 0.19/0.48 962[3:Spt:960.0,9.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 964[3:MRR:3.0,961.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 984[3:SpR:964.0,104.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.19/0.48 986[3:Rew:1.0,984.0,962.0,984.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 988[3:Rew:986.0,1.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.19/0.48 991[3:Rew:986.0,961.0] || equal(multiply(sk_c7,sk_c8),sk_c7)** -> . % 0.19/0.48 996[3:Rew:988.0,991.0] || equal(sk_c7,sk_c7)* -> . % 0.19/0.48 997[3:Obv:996.0] || -> . % 0.19/0.48 1013[2:Spt:997.0,8.0,366.0] || equal(inverse(sk_c7),sk_c6)** -> . % 0.19/0.48 1014[2:Spt:997.0,8.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 1015[2:MRR:26.0,1013.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.19/0.48 1016[2:MRR:2.0,1013.0] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.19/0.48 1017[2:MRR:14.0,1013.0] || -> equal(multiply(sk_c8,sk_c3),sk_c7)**. % 0.19/0.48 1018[2:MRR:20.0,1013.0] || -> equal(multiply(sk_c2,sk_c8),sk_c3)**. % 0.19/0.48 1019[2:SpR:1014.0,104.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.19/0.48 1021[2:SpR:1015.0,104.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),u)**. % 0.19/0.48 1027[2:SpR:1016.0,104.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.19/0.48 1029[2:Rew:1.0,1027.0,1014.0,1027.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.48 1031[2:Rew:1029.0,1013.0] || equal(inverse(sk_c7),sk_c7)** -> . % 0.19/0.48 1032[2:Rew:1029.0,274.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.19/0.48 1034[2:Rew:34.0,1032.0] || -> equal(identity,sk_c8)**. % 0.19/0.48 1036[2:Rew:1034.0,333.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.48 1037[2:Rew:1034.0,33.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.48 1039[2:Rew:1036.0,1018.0] || -> equal(sk_c2,sk_c3)**. % 0.19/0.48 1040[2:Rew:1039.0,1015.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.48 1041[2:Rew:1039.0,1021.0] || -> equal(multiply(sk_c8,multiply(sk_c3,u)),u)**. % 0.19/0.48 1042[2:Rew:1037.0,1017.0] || -> equal(sk_c3,sk_c7)**. % 0.19/0.48 1044[2:Rew:1042.0,1040.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.19/0.48 1045[2:Rew:1044.0,1031.0] || equal(sk_c8,sk_c7)** -> . % 0.19/0.48 1046[2:Rew:1037.0,1041.0,1042.0,1041.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.48 1047[2:Rew:1046.0,1019.0] || -> equal(multiply(sk_c1,u),u)**. % 0.19/0.48 1048[2:Rew:1047.0,1016.0] || -> equal(sk_c8,sk_c7)**. % 0.19/0.48 1049[2:MRR:1048.0,1045.0] || -> . % 0.19/0.48 % SZS output end Refutation % 0.19/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_16 prove_this_18 prove_this_19 prove_this_20 prove_this_22 prove_this_24 prove_this_25 prove_this_26 prove_this_28 prove_this_30 prove_this_31 prove_this_32 left_identity left_inverse associativity % 0.19/0.48 %------------------------------------------------------------------------------