%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP234-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n007.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:27 EDT 2022 % Result : Unsatisfiable 0.21s 0.46s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : GRP234-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.13 % Command : run_spass %d %s % 0.13/0.35 % Computer : n007.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 : Mon Jun 13 23:03:54 EDT 2022 % 0.13/0.35 % CPUTime : % 0.21/0.46 % 0.21/0.46 SPASS V 3.9 % 0.21/0.46 SPASS beiseite: Proof found. % 0.21/0.46 % SZS status Theorem % 0.21/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.21/0.46 SPASS derived 570 clauses, backtracked 174 clauses, performed 8 splits and kept 423 clauses. % 0.21/0.46 SPASS allocated 63462 KBytes. % 0.21/0.46 SPASS spent 0:00:00.10 on the problem. % 0.21/0.46 0:00:00.03 for the input. % 0.21/0.46 0:00:00.00 for the FLOTTER CNF translation. % 0.21/0.46 0:00:00.00 for inferences. % 0.21/0.46 0:00:00.00 for the backtracking. % 0.21/0.46 0:00:00.04 for the reduction. % 0.21/0.46 % 0.21/0.46 % 0.21/0.46 Here is a proof with depth 5, length 277 : % 0.21/0.46 % SZS output start Refutation % 0.21/0.46 1[0:Inp] || -> equal(inverse(sk_c3),sk_c7)** equal(inverse(sk_c7),sk_c6). % 0.21/0.46 2[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.46 3[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.46 4[0:Inp] || -> equal(inverse(sk_c7),sk_c6) equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.46 5[0:Inp] || -> equal(inverse(sk_c4),sk_c7)** equal(inverse(sk_c7),sk_c6). % 0.21/0.46 6[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.21/0.46 7[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.21/0.46 8[0:Inp] || -> equal(multiply(sk_c7,sk_c5),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.21/0.46 9[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.21/0.46 10[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.21/0.46 11[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.21/0.46 12[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.21/0.46 13[0:Inp] || -> equal(multiply(sk_c7,sk_c5),sk_c6) equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.21/0.46 14[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c5) equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.21/0.46 15[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.21/0.46 16[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c2),sk_c7)**. % 0.21/0.46 17[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.46 18[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.46 19[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.46 20[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(inverse(sk_c2),sk_c7)**. % 0.21/0.46 21[0:Inp] || equal(inverse(sk_c7),sk_c6) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(w,sk_c6),sk_c7)** equal(multiply(sk_c7,x),sk_c6)** equal(multiply(y,sk_c7),x)* equal(inverse(y),sk_c7) -> . % 0.21/0.46 22[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.21/0.46 23[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.21/0.46 24[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.21/0.46 25[0:Con:21.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(inverse(sk_c7),sk_c6) equal(multiply(u,sk_c7),x)*+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c7,x),sk_c6)** -> . % 0.21/0.46 26[1:Spt:25.2,25.6] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c6)** -> . % 0.21/0.46 27[2:Spt:5.1] || -> equal(inverse(sk_c7),sk_c6)**. % 0.21/0.46 29[3:Spt:20.1] || -> equal(inverse(sk_c2),sk_c7)**. % 0.21/0.46 33[4:Spt:15.1] || -> equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.21/0.46 35[4:SpL:33.0,26.1] || equal(inverse(sk_c2),sk_c7)** equal(sk_c6,sk_c6) -> . % 0.21/0.46 36[4:Obv:35.1] || equal(inverse(sk_c2),sk_c7)** -> . % 0.21/0.46 37[4:Rew:29.0,36.0] || equal(sk_c7,sk_c7)* -> . % 0.21/0.46 38[4:Obv:37.0] || -> . % 0.21/0.46 39[4:Spt:38.0,15.1,33.0] || equal(multiply(sk_c2,sk_c7),sk_c6)** -> . % 0.21/0.46 40[4:Spt:38.0,15.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.21/0.46 41[4:MRR:11.1,39.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.21/0.46 42[4:MRR:14.1,39.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.46 43[4:MRR:13.1,39.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.46 44[4:MRR:12.1,39.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.46 48[4:SpL:42.0,26.1] || equal(inverse(sk_c4),sk_c7)** equal(sk_c6,sk_c5) -> . % 0.21/0.46 49[4:Rew:40.0,48.0] || equal(sk_c7,sk_c7) equal(sk_c6,sk_c5)** -> . % 0.21/0.46 50[4:Obv:49.0] || equal(sk_c6,sk_c5)** -> . % 0.21/0.46 54[2:SpR:27.0,23.0] || -> equal(multiply(sk_c6,sk_c7),identity)**. % 0.21/0.46 55[3:SpR:29.0,23.0] || -> equal(multiply(sk_c7,sk_c2),identity)**. % 0.21/0.46 56[4:SpR:40.0,23.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.21/0.46 57[4:SpR:41.0,23.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.21/0.46 65[2:SpR:54.0,24.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(identity,u))**. % 0.21/0.46 67[0:SpR:23.0,24.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.21/0.46 71[2:Rew:22.0,65.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.21/0.46 72[0:Rew:22.0,67.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.21/0.46 85[4:SpR:43.0,71.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.21/0.46 86[3:SpR:55.0,71.0] || -> equal(multiply(sk_c6,identity),sk_c2)**. % 0.21/0.46 87[4:SpR:56.0,71.0] || -> equal(multiply(sk_c6,identity),sk_c4)**. % 0.21/0.46 88[4:SpR:57.0,71.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.21/0.46 89[4:Rew:86.0,87.0] || -> equal(sk_c2,sk_c4)**. % 0.21/0.46 94[4:Rew:89.0,86.0] || -> equal(multiply(sk_c6,identity),sk_c4)**. % 0.21/0.46 95[4:Rew:88.0,94.0] || -> equal(sk_c4,sk_c3)**. % 0.21/0.46 97[4:Rew:95.0,42.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.21/0.46 112[4:SpR:88.0,24.0] || -> equal(multiply(sk_c6,multiply(identity,u)),multiply(sk_c3,u))**. % 0.21/0.46 114[4:Rew:22.0,112.0] || -> equal(multiply(sk_c6,u),multiply(sk_c3,u))**. % 0.21/0.46 116[4:Rew:114.0,85.0] || -> equal(multiply(sk_c3,sk_c6),sk_c5)**. % 0.21/0.46 118[4:Rew:114.0,54.0] || -> equal(multiply(sk_c3,sk_c7),identity)**. % 0.21/0.46 122[4:Rew:44.0,116.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.46 123[4:Rew:122.0,50.0] || equal(sk_c6,sk_c7)** -> . % 0.21/0.46 125[4:Rew:122.0,97.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.21/0.46 127[4:Rew:118.0,125.0] || -> equal(identity,sk_c7)**. % 0.21/0.46 128[4:Rew:127.0,22.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.46 130[4:Rew:127.0,57.0] || -> equal(multiply(sk_c7,sk_c3),sk_c7)**. % 0.21/0.46 137[4:Rew:128.0,130.0] || -> equal(sk_c3,sk_c7)**. % 0.21/0.46 139[4:Rew:137.0,44.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.21/0.46 148[4:Rew:128.0,139.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.46 149[4:MRR:148.0,123.0] || -> . % 0.21/0.46 156[3:Spt:149.0,20.1,29.0] || equal(inverse(sk_c2),sk_c7)** -> . % 0.21/0.46 157[3:Spt:149.0,20.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.21/0.46 158[3:MRR:16.1,156.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.21/0.46 159[3:MRR:19.0,156.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.46 160[3:MRR:18.0,156.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.46 161[3:MRR:17.0,156.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.46 170[3:SpL:159.0,26.1] || equal(inverse(sk_c4),sk_c7)** equal(sk_c6,sk_c5) -> . % 0.21/0.46 171[3:Rew:157.0,170.0] || equal(sk_c7,sk_c7) equal(sk_c6,sk_c5)** -> . % 0.21/0.46 172[3:Obv:171.0] || equal(sk_c6,sk_c5)** -> . % 0.21/0.46 175[3:SpR:161.0,24.0] || -> equal(multiply(sk_c3,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.21/0.46 183[3:SpR:157.0,23.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.21/0.46 184[3:SpR:158.0,23.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.21/0.46 196[3:SpR:160.0,71.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.21/0.46 197[3:SpR:183.0,71.0] || -> equal(multiply(sk_c6,identity),sk_c4)**. % 0.21/0.46 198[3:SpR:184.0,71.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.21/0.46 199[3:Rew:197.0,198.0] || -> equal(sk_c4,sk_c3)**. % 0.21/0.46 201[3:Rew:199.0,159.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.21/0.46 205[3:Rew:199.0,197.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.21/0.46 214[0:SpR:72.0,72.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.21/0.46 217[3:SpR:201.0,72.0] || -> equal(multiply(inverse(sk_c3),sk_c5),sk_c7)**. % 0.21/0.46 223[0:SpR:23.0,72.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.21/0.46 226[2:SpR:27.0,72.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.21/0.46 228[3:Rew:160.0,217.0,158.0,217.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.46 231[3:Rew:228.0,54.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.21/0.46 232[3:Rew:228.0,172.0] || equal(sk_c5,sk_c7)** -> . % 0.21/0.46 233[3:Rew:228.0,160.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.46 236[3:Rew:228.0,196.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.21/0.46 242[3:Rew:228.0,175.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.21/0.46 243[3:Rew:228.0,205.0] || -> equal(multiply(sk_c7,identity),sk_c3)**. % 0.21/0.46 247[3:Rew:231.0,236.0] || -> equal(identity,sk_c5)**. % 0.21/0.46 250[3:Rew:247.0,184.0] || -> equal(multiply(sk_c7,sk_c3),sk_c5)**. % 0.21/0.46 252[3:Rew:233.0,243.0,247.0,243.0] || -> equal(sk_c3,sk_c7)**. % 0.21/0.46 258[3:Rew:252.0,250.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.21/0.46 267[3:Rew:228.0,226.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.21/0.46 276[3:Rew:267.0,242.0,252.0,242.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.46 278[3:Rew:276.0,258.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.46 279[3:MRR:278.0,232.0] || -> . % 0.21/0.46 283[2:Spt:279.0,5.1,27.0] || equal(inverse(sk_c7),sk_c6)** -> . % 0.21/0.46 284[2:Spt:279.0,5.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.21/0.46 285[0:Rew:214.0,223.0] || -> equal(multiply(u,identity),u)**. % 0.21/0.46 286[2:MRR:1.1,283.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.21/0.46 287[2:MRR:4.0,283.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.46 288[2:MRR:3.0,283.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.46 289[2:MRR:2.0,283.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.46 295[2:SpR:287.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c7)**. % 0.21/0.46 297[2:Rew:284.0,295.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.46 298[2:Rew:288.0,297.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.46 299[2:Rew:298.0,283.0] || equal(inverse(sk_c7),sk_c7)** -> . % 0.21/0.46 301[2:Rew:298.0,288.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.46 302[2:Rew:298.0,289.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.21/0.46 309[2:SpR:301.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.21/0.46 311[2:Rew:23.0,309.0] || -> equal(identity,sk_c5)**. % 0.21/0.46 313[2:Rew:311.0,23.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.21/0.46 316[2:Rew:311.0,285.0] || -> equal(multiply(u,sk_c5),u)**. % 0.21/0.46 322[2:SpR:302.0,72.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.21/0.46 324[2:Rew:286.0,322.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.21/0.46 329[2:SpR:324.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.21/0.46 331[2:Rew:313.0,329.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.46 332[2:Rew:331.0,287.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7)**. % 0.21/0.46 337[2:Rew:331.0,316.0] || -> equal(multiply(u,sk_c7),u)**. % 0.21/0.46 345[2:Rew:337.0,332.0] || -> equal(sk_c4,sk_c7)**. % 0.21/0.46 349[2:Rew:345.0,284.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.21/0.46 351[2:MRR:349.0,299.0] || -> . % 0.21/0.46 357[1:Spt:351.0,25.0,25.1,25.3,25.4,25.5,25.7] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(sk_c7),sk_c6) equal(multiply(u,sk_c7),w)*+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c7,w),sk_c6)** -> . % 0.21/0.46 358[1:EqR:357.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(sk_c7),sk_c6) equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c6)** -> . % 0.21/0.46 360[2:Spt:1.1] || -> equal(inverse(sk_c7),sk_c6)**. % 0.21/0.46 363[2:Rew:360.0,358.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(sk_c6,sk_c6) equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c6)** -> . % 0.21/0.46 364[2:Obv:363.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c6)** -> . % 0.21/0.46 367[2:SpR:360.0,72.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.21/0.46 369[3:Spt:20.1] || -> equal(inverse(sk_c2),sk_c7)**. % 0.21/0.46 370[3:SpR:369.0,72.0] || -> equal(multiply(sk_c7,multiply(sk_c2,u)),u)**. % 0.21/0.46 372[4:Spt:10.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.21/0.46 382[5:Spt:11.1] || -> equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.21/0.46 384[5:SpR:382.0,72.0] || -> equal(multiply(inverse(sk_c2),sk_c6),sk_c7)**. % 0.21/0.46 386[5:Rew:369.0,384.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.21/0.46 388[5:SpR:386.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.21/0.46 390[5:Rew:360.0,388.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.21/0.46 392[5:SpR:390.0,72.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c7)**. % 0.21/0.46 394[5:Rew:23.0,392.0] || -> equal(identity,sk_c7)**. % 0.21/0.46 395[5:Rew:394.0,285.0] || -> equal(multiply(u,sk_c7),u)**. % 0.21/0.46 396[5:Rew:394.0,22.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.46 399[5:Rew:395.0,382.0] || -> equal(sk_c6,sk_c2)**. % 0.21/0.46 400[5:Rew:395.0,372.0] || -> equal(sk_c6,sk_c1)**. % 0.21/0.46 402[5:Rew:395.0,364.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c7,u),sk_c6)** -> . % 0.21/0.46 404[5:Rew:399.0,360.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.21/0.46 405[5:Rew:399.0,386.0] || -> equal(multiply(sk_c7,sk_c2),sk_c7)**. % 0.21/0.46 411[5:Rew:399.0,400.0] || -> equal(sk_c2,sk_c1)**. % 0.21/0.46 414[5:Rew:411.0,399.0] || -> equal(sk_c6,sk_c1)**. % 0.21/0.46 415[5:Rew:411.0,404.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.21/0.46 416[5:Rew:396.0,405.0,411.0,405.0] || -> equal(sk_c1,sk_c7)**. % 0.21/0.46 418[5:Rew:416.0,414.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.46 419[5:Rew:416.0,415.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.21/0.46 429[5:Rew:396.0,402.3,418.0,402.3,395.0,402.2,418.0,402.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(v,sk_c7) equal(u,sk_c7) -> . % 0.21/0.46 430[5:Con:429.0] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.21/0.46 472[5:SpL:419.0,430.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.21/0.46 474[5:Obv:472.1] || -> . % 0.21/0.46 475[5:Spt:474.0,11.1,382.0] || equal(multiply(sk_c2,sk_c7),sk_c6)** -> . % 0.21/0.46 476[5:Spt:474.0,11.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.21/0.46 477[5:MRR:15.1,475.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.21/0.46 478[5:MRR:14.1,475.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.46 479[5:MRR:13.1,475.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.46 480[5:MRR:12.1,475.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.46 493[5:SpR:478.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c7)**. % 0.21/0.46 495[5:Rew:477.0,493.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.46 496[5:Rew:479.0,495.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.46 497[5:Rew:496.0,360.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.21/0.46 500[5:Rew:496.0,475.0] || equal(multiply(sk_c2,sk_c7),sk_c7)** -> . % 0.21/0.46 501[5:Rew:496.0,367.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.21/0.46 503[5:Rew:496.0,479.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.46 504[5:Rew:496.0,480.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.21/0.46 517[5:SpR:503.0,24.0] || -> equal(multiply(sk_c7,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.21/0.46 518[5:SpR:503.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.21/0.46 520[5:Rew:497.0,518.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.21/0.46 522[5:SpR:504.0,72.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.21/0.46 524[5:Rew:476.0,522.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.21/0.46 525[5:Rew:520.0,524.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.46 529[5:Rew:525.0,517.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.21/0.46 531[5:Rew:501.0,529.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.46 541[5:Rew:531.0,370.0] || -> equal(multiply(sk_c2,u),u)**. % 0.21/0.46 542[5:UnC:541.0,500.0] || -> . % 0.21/0.46 544[4:Spt:542.0,10.1,372.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.21/0.46 545[4:Spt:542.0,10.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.21/0.46 546[4:MRR:6.1,544.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.21/0.46 547[4:MRR:9.1,544.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.46 548[4:MRR:8.1,544.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.46 549[4:MRR:7.1,544.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.46 557[4:SpR:547.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c7)**. % 0.21/0.46 559[4:Rew:545.0,557.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.46 560[4:Rew:548.0,559.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.46 561[4:Rew:560.0,360.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.21/0.46 563[4:Rew:560.0,367.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.21/0.46 564[4:Rew:560.0,548.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.46 565[4:Rew:560.0,549.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.21/0.46 567[4:Rew:560.0,364.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c6)** -> . % 0.21/0.46 569[4:Rew:560.0,567.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c7)** -> . % 0.21/0.46 573[4:SpR:564.0,24.0] || -> equal(multiply(sk_c7,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.21/0.46 574[4:SpR:564.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.21/0.46 576[4:Rew:561.0,574.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.21/0.46 580[4:SpR:565.0,72.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.21/0.46 582[4:Rew:546.0,580.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.21/0.46 583[4:Rew:576.0,582.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.46 587[4:Rew:583.0,573.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.21/0.46 589[4:Rew:563.0,587.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.46 595[4:Rew:589.0,569.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(u,sk_c7),sk_c7)** -> . % 0.21/0.46 599[4:Con:595.0] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.21/0.46 613[4:SpR:589.0,285.0] || -> equal(identity,sk_c7)**. % 0.21/0.46 615[4:Rew:613.0,285.0] || -> equal(multiply(u,sk_c7),u)**. % 0.21/0.47 620[4:Rew:615.0,599.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.21/0.47 657[4:SpL:561.0,620.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.21/0.47 658[4:Obv:657.1] || -> . % 0.21/0.47 659[3:Spt:658.0,20.1,369.0] || equal(inverse(sk_c2),sk_c7)** -> . % 0.21/0.47 660[3:Spt:658.0,20.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.21/0.47 661[3:MRR:16.1,659.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.21/0.47 662[3:MRR:19.0,659.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.47 663[3:MRR:18.0,659.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.47 664[3:MRR:17.0,659.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.47 672[3:SpR:662.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c7)**. % 0.21/0.47 674[3:Rew:660.0,672.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.47 675[3:Rew:663.0,674.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.47 676[3:Rew:675.0,360.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.21/0.47 677[3:Rew:675.0,367.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.21/0.47 678[3:Rew:675.0,663.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.47 679[3:Rew:675.0,664.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.21/0.47 681[3:Rew:675.0,364.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c6)** -> . % 0.21/0.47 683[3:Rew:675.0,681.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(sk_c7,multiply(u,sk_c7)),sk_c7)** -> . % 0.21/0.47 686[3:SpR:678.0,24.0] || -> equal(multiply(sk_c7,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.21/0.47 687[3:SpR:678.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.21/0.47 689[3:Rew:676.0,687.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.21/0.47 694[3:SpR:679.0,72.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.21/0.47 696[3:Rew:661.0,694.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.21/0.47 697[3:Rew:689.0,696.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.47 701[3:Rew:697.0,686.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.21/0.47 703[3:Rew:677.0,701.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.47 709[3:Rew:703.0,683.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(v,sk_c7),sk_c7)** equal(multiply(u,sk_c7),sk_c7)** -> . % 0.21/0.47 712[3:Con:709.0] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.21/0.47 726[3:SpR:703.0,285.0] || -> equal(identity,sk_c7)**. % 0.21/0.47 729[3:Rew:726.0,285.0] || -> equal(multiply(u,sk_c7),u)**. % 0.21/0.47 732[3:Rew:729.0,712.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.21/0.47 764[3:SpL:676.0,732.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.21/0.47 765[3:Obv:764.1] || -> . % 0.21/0.47 766[2:Spt:765.0,1.1,360.0] || equal(inverse(sk_c7),sk_c6)** -> . % 0.21/0.47 767[2:Spt:765.0,1.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.21/0.47 768[2:MRR:5.1,766.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.21/0.47 769[2:MRR:4.0,766.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.21/0.47 770[2:MRR:3.0,766.0] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.21/0.47 771[2:MRR:2.0,766.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.21/0.47 777[2:SpR:769.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c7)**. % 0.21/0.47 779[2:Rew:768.0,777.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.47 780[2:Rew:770.0,779.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.47 781[2:Rew:780.0,766.0] || equal(inverse(sk_c7),sk_c7)** -> . % 0.21/0.47 782[2:Rew:780.0,770.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.21/0.47 783[2:Rew:780.0,771.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.21/0.47 786[2:SpR:782.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.21/0.47 788[2:Rew:23.0,786.0] || -> equal(identity,sk_c5)**. % 0.21/0.47 789[2:Rew:788.0,285.0] || -> equal(multiply(u,sk_c5),u)**. % 0.21/0.47 791[2:Rew:788.0,23.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.21/0.47 797[2:SpR:783.0,72.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.21/0.47 799[2:Rew:767.0,797.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.21/0.47 801[2:SpR:799.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.21/0.47 803[2:Rew:791.0,801.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.47 804[2:Rew:803.0,769.0] || -> equal(multiply(sk_c4,sk_c7),sk_c7)**. % 0.21/0.47 806[2:Rew:803.0,789.0] || -> equal(multiply(u,sk_c7),u)**. % 0.21/0.47 811[2:Rew:806.0,804.0] || -> equal(sk_c4,sk_c7)**. % 0.21/0.47 815[2:Rew:811.0,768.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.21/0.47 819[2:MRR:815.0,781.0] || -> . % 0.21/0.47 % SZS output end Refutation % 0.21/0.47 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_20 prove_this_21 left_identity left_inverse associativity % 0.21/0.47 %------------------------------------------------------------------------------