%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP306-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n029.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:46 EDT 2022 % Result : Unsatisfiable 0.21s 0.48s % Output : Refutation 0.21s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GRP306-1 : TPTP v8.1.0. Released v2.5.0. % 0.12/0.14 % Command : run_spass %d %s % 0.13/0.35 % Computer : n029.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 15:12:25 EDT 2022 % 0.13/0.35 % CPUTime : % 0.21/0.48 % 0.21/0.48 SPASS V 3.9 % 0.21/0.48 SPASS beiseite: Proof found. % 0.21/0.48 % SZS status Theorem % 0.21/0.48 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.21/0.48 SPASS derived 774 clauses, backtracked 230 clauses, performed 9 splits and kept 540 clauses. % 0.21/0.48 SPASS allocated 63608 KBytes. % 0.21/0.48 SPASS spent 0:00:00.12 on the problem. % 0.21/0.48 0:00:00.04 for the input. % 0.21/0.48 0:00:00.00 for the FLOTTER CNF translation. % 0.21/0.48 0:00:00.01 for inferences. % 0.21/0.48 0:00:00.00 for the backtracking. % 0.21/0.48 0:00:00.05 for the reduction. % 0.21/0.48 % 0.21/0.48 % 0.21/0.48 Here is a proof with depth 5, length 286 : % 0.21/0.48 % SZS output start Refutation % 0.21/0.48 1[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.21/0.48 2[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.48 3[0:Inp] || -> equal(inverse(sk_c3),sk_c8)** equal(inverse(sk_c8),sk_c6). % 0.21/0.48 4[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.48 5[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.48 6[0:Inp] || -> equal(inverse(sk_c4),sk_c8)** equal(inverse(sk_c8),sk_c6). % 0.21/0.48 7[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c2),sk_c8)**. % 0.21/0.48 8[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c1,sk_c2),sk_c8)**. % 0.21/0.48 9[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c2),sk_c8)**. % 0.21/0.48 10[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c1,sk_c2),sk_c8)**. % 0.21/0.48 11[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c2),sk_c8)**. % 0.21/0.48 12[0:Inp] || -> equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.48 13[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c1),sk_c2)**. % 0.21/0.48 14[0:Inp] || -> equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.48 15[0:Inp] || -> equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.48 16[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c1),sk_c2)**. % 0.21/0.48 17[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.21/0.48 18[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.21/0.48 19[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.21/0.48 20[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.21/0.48 21[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.21/0.48 22[0:Inp] || equal(multiply(sk_c8,sk_c7),sk_c6)** equal(inverse(sk_c8),sk_c6) equal(multiply(u,v),sk_c8)** equal(inverse(u),v) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c8),sk_c7)** equal(inverse(w),sk_c8) equal(multiply(sk_c8,x),sk_c7)** equal(multiply(y,sk_c8),x)* equal(inverse(y),sk_c8) -> . % 0.21/0.48 23[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.21/0.48 24[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.21/0.48 25[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.21/0.48 26[0:Rew:1.0,22.0] || equal(sk_c6,sk_c6) equal(inverse(sk_c8),sk_c6) equal(multiply(u,v),sk_c8)** equal(inverse(u),v) equal(multiply(v,sk_c7),sk_c8)** equal(multiply(w,sk_c8),sk_c7)** equal(inverse(w),sk_c8) equal(multiply(sk_c8,x),sk_c7)** equal(multiply(y,sk_c8),x)* equal(inverse(y),sk_c8) -> . % 0.21/0.48 27[0:Obv:26.0] || equal(inverse(u),v) equal(inverse(w),sk_c8) equal(inverse(x),sk_c8) equal(inverse(sk_c8),sk_c6) equal(multiply(u,v),sk_c8)**+ equal(multiply(w,sk_c8),y)* equal(multiply(x,sk_c8),sk_c7)** equal(multiply(v,sk_c7),sk_c8)** equal(multiply(sk_c8,y),sk_c7)** -> . % 0.21/0.48 28[1:Spt:27.0,27.4,27.7] || equal(inverse(u),v) equal(multiply(u,v),sk_c8)**+ equal(multiply(v,sk_c7),sk_c8)** -> . % 0.21/0.48 29[2:Spt:6.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.21/0.48 31[3:Spt:16.1] || -> equal(inverse(sk_c1),sk_c2)**. % 0.21/0.48 36[4:Spt:21.1] || -> equal(multiply(sk_c2,sk_c7),sk_c8)**. % 0.21/0.48 40[5:Spt:11.1] || -> equal(multiply(sk_c1,sk_c2),sk_c8)**. % 0.21/0.48 42[5:SpL:40.0,28.1] || equal(inverse(sk_c1),sk_c2) equal(sk_c8,sk_c8) equal(multiply(sk_c2,sk_c7),sk_c8)** -> . % 0.21/0.48 43[5:Obv:42.1] || equal(inverse(sk_c1),sk_c2) equal(multiply(sk_c2,sk_c7),sk_c8)** -> . % 0.21/0.48 44[5:Rew:36.0,43.1,31.0,43.0] || equal(sk_c2,sk_c2)* equal(sk_c8,sk_c8) -> . % 0.21/0.48 45[5:Obv:44.1] || -> . % 0.21/0.48 46[5:Spt:45.0,11.1,40.0] || equal(multiply(sk_c1,sk_c2),sk_c8)** -> . % 0.21/0.48 47[5:Spt:45.0,11.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.48 48[5:MRR:8.1,46.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.21/0.48 49[5:MRR:10.1,46.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.48 50[5:MRR:9.1,46.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.48 51[5:MRR:7.1,46.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.48 68[2:SpR:29.0,24.0] || -> equal(multiply(sk_c6,sk_c8),identity)**. % 0.21/0.48 69[3:SpR:31.0,24.0] || -> equal(multiply(sk_c2,sk_c1),identity)**. % 0.21/0.48 70[5:SpR:47.0,24.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.21/0.48 71[5:SpR:48.0,24.0] || -> equal(multiply(sk_c8,sk_c3),identity)**. % 0.21/0.48 78[0:SpR:1.0,25.0] || -> equal(multiply(sk_c8,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.21/0.48 79[4:SpR:36.0,25.0] || -> equal(multiply(sk_c2,multiply(sk_c7,u)),multiply(sk_c8,u))**. % 0.21/0.48 82[2:SpR:68.0,25.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),multiply(identity,u))**. % 0.21/0.48 85[0:SpR:24.0,25.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.21/0.48 87[2:Rew:23.0,82.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),u)**. % 0.21/0.48 88[0:Rew:23.0,85.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.21/0.48 108[5:SpR:70.0,87.0] || -> equal(multiply(sk_c6,identity),sk_c4)**. % 0.21/0.48 109[5:SpR:71.0,87.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.21/0.48 111[5:Rew:108.0,109.0] || -> equal(sk_c4,sk_c3)**. % 0.21/0.48 113[5:Rew:111.0,49.0] || -> equal(multiply(sk_c3,sk_c8),sk_c5)**. % 0.21/0.48 118[5:Rew:111.0,108.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.21/0.48 119[5:Rew:51.0,113.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.48 120[5:Rew:119.0,50.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7)**. % 0.21/0.48 125[5:Rew:1.0,120.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.48 128[5:Rew:125.0,68.0] || -> equal(multiply(sk_c7,sk_c8),identity)**. % 0.21/0.48 129[5:Rew:125.0,87.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),u)**. % 0.21/0.48 136[5:Rew:125.0,118.0] || -> equal(multiply(sk_c7,identity),sk_c3)**. % 0.21/0.48 167[5:SpR:136.0,25.0] || -> equal(multiply(sk_c7,multiply(identity,u)),multiply(sk_c3,u))**. % 0.21/0.48 170[5:Rew:23.0,167.0] || -> equal(multiply(sk_c3,u),multiply(sk_c7,u))**. % 0.21/0.48 171[5:Rew:170.0,51.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.21/0.48 175[5:Rew:128.0,171.0] || -> equal(identity,sk_c7)**. % 0.21/0.48 176[5:Rew:175.0,23.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.48 178[5:Rew:175.0,69.0] || -> equal(multiply(sk_c2,sk_c1),sk_c7)**. % 0.21/0.48 181[5:Rew:175.0,136.0] || -> equal(multiply(sk_c7,sk_c7),sk_c3)**. % 0.21/0.48 185[5:Rew:176.0,129.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.48 186[5:Rew:176.0,79.0] || -> equal(multiply(sk_c2,u),multiply(sk_c8,u))**. % 0.21/0.48 191[5:Rew:176.0,181.0] || -> equal(sk_c3,sk_c7)**. % 0.21/0.48 192[5:Rew:191.0,48.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.21/0.48 198[5:Rew:185.0,186.0] || -> equal(multiply(sk_c2,u),u)**. % 0.21/0.48 200[5:Rew:198.0,178.0] || -> equal(sk_c1,sk_c7)**. % 0.21/0.48 203[5:Rew:200.0,31.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.21/0.48 204[5:Rew:200.0,46.0] || equal(multiply(sk_c7,sk_c2),sk_c8)** -> . % 0.21/0.48 205[5:Rew:192.0,203.0] || -> equal(sk_c2,sk_c8)**. % 0.21/0.48 208[5:Rew:176.0,204.0,205.0,204.0] || equal(sk_c8,sk_c8)* -> . % 0.21/0.48 209[5:Obv:208.0] || -> . % 0.21/0.48 219[4:Spt:209.0,21.1,36.0] || equal(multiply(sk_c2,sk_c7),sk_c8)** -> . % 0.21/0.48 220[4:Spt:209.0,21.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.48 221[4:MRR:18.1,219.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.21/0.48 222[4:MRR:20.1,219.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.48 223[4:MRR:19.1,219.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.48 224[4:MRR:17.1,219.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.48 245[4:SpL:222.0,28.1] || equal(inverse(sk_c4),sk_c8) equal(sk_c5,sk_c8) equal(multiply(sk_c8,sk_c7),sk_c8)** -> . % 0.21/0.48 246[4:Rew:1.0,245.2,220.0,245.0] || equal(sk_c8,sk_c8) equal(sk_c5,sk_c8)** equal(sk_c6,sk_c8) -> . % 0.21/0.48 247[4:Obv:246.0] || equal(sk_c5,sk_c8)** equal(sk_c6,sk_c8) -> . % 0.21/0.48 266[4:SpR:220.0,24.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.21/0.48 268[4:SpR:221.0,24.0] || -> equal(multiply(sk_c8,sk_c3),identity)**. % 0.21/0.48 286[4:SpR:266.0,87.0] || -> equal(multiply(sk_c6,identity),sk_c4)**. % 0.21/0.48 287[4:SpR:268.0,87.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.21/0.48 290[4:Rew:286.0,287.0] || -> equal(sk_c4,sk_c3)**. % 0.21/0.48 292[4:Rew:290.0,222.0] || -> equal(multiply(sk_c3,sk_c8),sk_c5)**. % 0.21/0.48 297[4:Rew:290.0,286.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.21/0.48 298[4:Rew:224.0,292.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.48 299[4:Rew:298.0,223.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7)**. % 0.21/0.48 301[4:Rew:298.0,247.0] || equal(sk_c7,sk_c8) equal(sk_c6,sk_c8)** -> . % 0.21/0.48 304[4:Rew:1.0,299.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.48 306[4:Rew:304.0,68.0] || -> equal(multiply(sk_c7,sk_c8),identity)**. % 0.21/0.48 317[4:Rew:304.0,297.0] || -> equal(multiply(sk_c7,identity),sk_c3)**. % 0.21/0.48 319[4:Rew:304.0,301.1] || equal(sk_c7,sk_c8)** equal(sk_c7,sk_c8)** -> . % 0.21/0.48 320[4:Obv:319.0] || equal(sk_c7,sk_c8)** -> . % 0.21/0.48 345[4:SpR:317.0,25.0] || -> equal(multiply(sk_c7,multiply(identity,u)),multiply(sk_c3,u))**. % 0.21/0.48 348[4:Rew:23.0,345.0] || -> equal(multiply(sk_c3,u),multiply(sk_c7,u))**. % 0.21/0.48 349[4:Rew:348.0,224.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.21/0.48 353[4:Rew:306.0,349.0] || -> equal(identity,sk_c7)**. % 0.21/0.48 355[4:Rew:353.0,23.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.48 358[4:Rew:353.0,306.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.21/0.48 366[4:Rew:355.0,358.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.48 367[4:MRR:366.0,320.0] || -> . % 0.21/0.48 384[3:Spt:367.0,16.1,31.0] || equal(inverse(sk_c1),sk_c2)** -> . % 0.21/0.48 385[3:Spt:367.0,16.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.48 386[3:MRR:13.1,384.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.21/0.48 387[3:MRR:15.0,384.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.48 388[3:MRR:14.0,384.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.48 389[3:MRR:12.0,384.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.48 426[3:SpR:385.0,24.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.21/0.48 428[3:SpR:386.0,24.0] || -> equal(multiply(sk_c8,sk_c3),identity)**. % 0.21/0.48 444[3:SpR:388.0,87.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.21/0.48 445[3:SpR:428.0,87.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.21/0.48 446[3:SpR:426.0,87.0] || -> equal(multiply(sk_c6,identity),sk_c4)**. % 0.21/0.48 447[2:SpL:87.0,28.1] || equal(multiply(sk_c8,u),inverse(sk_c6)) equal(u,sk_c8) equal(multiply(multiply(sk_c8,u),sk_c7),sk_c8)** -> . % 0.21/0.48 449[3:Rew:445.0,446.0] || -> equal(sk_c4,sk_c3)**. % 0.21/0.48 451[3:Rew:449.0,387.0] || -> equal(multiply(sk_c3,sk_c8),sk_c5)**. % 0.21/0.48 456[3:Rew:389.0,451.0] || -> equal(sk_c5,sk_c7)**. % 0.21/0.48 457[3:Rew:456.0,388.0] || -> equal(multiply(sk_c8,sk_c7),sk_c7)**. % 0.21/0.48 461[3:Rew:456.0,444.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.21/0.48 462[3:Rew:1.0,457.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.48 467[3:Rew:462.0,87.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),u)**. % 0.21/0.48 475[3:Rew:462.0,445.0] || -> equal(multiply(sk_c7,identity),sk_c3)**. % 0.21/0.48 476[3:Rew:462.0,461.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.21/0.48 485[2:Rew:25.0,447.2] || equal(multiply(sk_c8,u),inverse(sk_c6)) equal(u,sk_c8) equal(multiply(sk_c8,multiply(u,sk_c7)),sk_c8)** -> . % 0.21/0.48 486[3:Rew:462.0,485.0] || equal(multiply(sk_c8,u),inverse(sk_c7)) equal(u,sk_c8) equal(multiply(sk_c8,multiply(u,sk_c7)),sk_c8)** -> . % 0.21/0.48 499[0:SpR:88.0,88.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.21/0.48 501[3:SpR:476.0,88.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.21/0.48 507[0:SpR:24.0,88.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.21/0.48 511[3:Rew:24.0,501.0] || -> equal(identity,sk_c7)**. % 0.21/0.48 512[3:Rew:511.0,23.0] || -> equal(multiply(sk_c7,u),u)**. % 0.21/0.48 519[3:Rew:511.0,475.0] || -> equal(multiply(sk_c7,sk_c7),sk_c3)**. % 0.21/0.48 520[3:Rew:512.0,467.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.48 525[3:Rew:512.0,519.0] || -> equal(sk_c3,sk_c7)**. % 0.21/0.48 526[3:Rew:525.0,386.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.21/0.48 531[3:Rew:526.0,486.0] || equal(multiply(sk_c8,u),sk_c8) equal(u,sk_c8) equal(multiply(sk_c8,multiply(u,sk_c7)),sk_c8)** -> . % 0.21/0.48 540[3:Rew:511.0,507.0] || -> equal(multiply(inverse(inverse(u)),sk_c7),u)**. % 0.21/0.48 545[3:Rew:499.0,540.0] || -> equal(multiply(u,sk_c7),u)**. % 0.21/0.48 552[3:Rew:545.0,531.2,520.0,531.2,520.0,531.0] || equal(u,sk_c8)* equal(u,sk_c8)* equal(u,sk_c8)* -> . % 0.21/0.48 553[3:Obv:552.1] || equal(u,sk_c8)* -> . % 0.21/0.48 554[3:UnC:553.0,88.0] || -> . % 0.21/0.48 557[2:Spt:554.0,6.1,29.0] || equal(inverse(sk_c8),sk_c6)** -> . % 0.21/0.48 558[2:Spt:554.0,6.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.48 559[0:Rew:499.0,507.0] || -> equal(multiply(u,identity),u)**. % 0.21/0.48 560[2:MRR:3.1,557.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.21/0.48 561[2:MRR:5.0,557.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.48 562[2:MRR:4.0,557.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.48 563[2:MRR:2.0,557.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.48 570[0:SpR:1.0,88.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.21/0.48 573[2:SpR:561.0,88.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.21/0.48 575[2:Rew:558.0,573.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.21/0.48 576[2:Rew:562.0,575.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.48 577[2:Rew:576.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.21/0.48 579[2:Rew:576.0,562.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.21/0.48 580[2:Rew:576.0,563.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.21/0.48 587[2:Rew:576.0,570.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c8)**. % 0.21/0.48 595[2:SpR:579.0,88.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c5)**. % 0.21/0.48 597[2:Rew:24.0,595.0] || -> equal(identity,sk_c5)**. % 0.21/0.48 599[2:Rew:597.0,24.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.21/0.48 602[2:Rew:597.0,559.0] || -> equal(multiply(u,sk_c5),u)**. % 0.21/0.48 608[2:SpR:580.0,88.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.21/0.48 610[2:Rew:577.0,608.0,560.0,608.0] || -> equal(sk_c6,sk_c8)**. % 0.21/0.48 611[2:Rew:610.0,557.0] || equal(inverse(sk_c8),sk_c8)** -> . % 0.21/0.48 613[2:Rew:610.0,587.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c8)**. % 0.21/0.48 616[2:Rew:599.0,613.0] || -> equal(sk_c5,sk_c8)**. % 0.21/0.48 617[2:Rew:616.0,561.0] || -> equal(multiply(sk_c4,sk_c8),sk_c8)**. % 0.21/0.48 620[2:Rew:616.0,602.0] || -> equal(multiply(u,sk_c8),u)**. % 0.21/0.48 629[2:Rew:620.0,617.0] || -> equal(sk_c4,sk_c8)**. % 0.21/0.48 634[2:Rew:629.0,558.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.48 636[2:MRR:634.0,611.0] || -> . % 0.21/0.48 646[1:Spt:636.0,27.1,27.2,27.3,27.5,27.6,27.8] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(sk_c8),sk_c6) equal(multiply(u,sk_c8),w)*+ equal(multiply(v,sk_c8),sk_c7)** equal(multiply(sk_c8,w),sk_c7)** -> . % 0.21/0.48 647[1:EqR:646.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(sk_c8),sk_c6) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.21/0.48 649[2:Spt:3.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.21/0.48 651[2:Rew:649.0,570.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.21/0.48 653[2:Rew:649.0,647.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(sk_c6,sk_c6) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.21/0.48 654[2:Obv:653.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.21/0.48 657[2:SpR:649.0,88.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),u)**. % 0.21/0.48 659[3:Spt:16.1] || -> equal(inverse(sk_c1),sk_c2)**. % 0.21/0.48 662[4:Spt:11.1] || -> equal(multiply(sk_c1,sk_c2),sk_c8)**. % 0.21/0.48 664[4:SpR:662.0,88.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c2)**. % 0.21/0.48 666[4:Rew:659.0,664.0] || -> equal(multiply(sk_c2,sk_c8),sk_c2)**. % 0.21/0.48 676[2:SpR:651.0,88.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c6)**. % 0.21/0.48 679[4:SpR:666.0,88.0] || -> equal(multiply(inverse(sk_c2),sk_c2),sk_c8)**. % 0.21/0.48 681[4:Rew:24.0,679.0] || -> equal(identity,sk_c8)**. % 0.21/0.48 682[4:Rew:681.0,559.0] || -> equal(multiply(u,sk_c8),u)**. % 0.21/0.48 683[4:Rew:681.0,23.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.48 685[4:Rew:681.0,24.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.21/0.48 688[4:Rew:682.0,654.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c7)** equal(multiply(sk_c8,u),sk_c7)** -> . % 0.21/0.48 690[4:Rew:683.0,1.0] || -> equal(sk_c6,sk_c7)**. % 0.21/0.48 695[4:Rew:690.0,649.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.21/0.48 697[4:Rew:690.0,676.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.21/0.48 701[4:Rew:685.0,697.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.48 705[4:Rew:701.0,695.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.48 720[4:Rew:683.0,688.3,701.0,688.3,682.0,688.2,701.0,688.2] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(v,sk_c8) equal(u,sk_c8) -> . % 0.21/0.48 721[4:Con:720.0] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.21/0.48 781[4:SpL:705.0,721.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.21/0.48 783[4:Obv:781.1] || -> . % 0.21/0.48 784[4:Spt:783.0,11.1,662.0] || equal(multiply(sk_c1,sk_c2),sk_c8)** -> . % 0.21/0.48 785[4:Spt:783.0,11.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.48 786[4:MRR:8.1,784.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.21/0.48 787[4:MRR:10.1,784.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.48 788[4:MRR:9.1,784.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.48 789[4:MRR:7.1,784.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.49 803[4:SpR:787.0,88.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.21/0.49 805[4:Rew:785.0,803.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.21/0.49 806[4:Rew:788.0,805.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.49 807[4:Rew:806.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.21/0.49 810[4:Rew:806.0,78.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c6,u))**. % 0.21/0.49 813[4:Rew:806.0,789.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.21/0.49 833[4:SpR:813.0,88.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.21/0.49 835[4:Rew:807.0,833.0,786.0,833.0] || -> equal(sk_c6,sk_c8)**. % 0.21/0.49 839[4:Rew:835.0,657.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.21/0.49 841[4:Rew:835.0,810.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c8,u))**. % 0.21/0.49 850[4:Rew:839.0,841.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.49 876[4:SpR:850.0,559.0] || -> equal(identity,sk_c8)**. % 0.21/0.49 879[4:Rew:876.0,559.0] || -> equal(multiply(u,sk_c8),u)**. % 0.21/0.49 880[4:Rew:876.0,24.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.21/0.49 894[4:SpR:659.0,880.0] || -> equal(multiply(sk_c2,sk_c1),sk_c8)**. % 0.21/0.49 909[4:SpR:894.0,88.0] || -> equal(multiply(inverse(sk_c2),sk_c8),sk_c1)**. % 0.21/0.49 911[4:Rew:879.0,909.0] || -> equal(inverse(sk_c2),sk_c1)**. % 0.21/0.49 914[4:SpR:911.0,880.0] || -> equal(multiply(sk_c1,sk_c2),sk_c8)**. % 0.21/0.49 916[4:MRR:914.0,784.0] || -> . % 0.21/0.49 917[3:Spt:916.0,16.1,659.0] || equal(inverse(sk_c1),sk_c2)** -> . % 0.21/0.49 918[3:Spt:916.0,16.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.49 919[3:MRR:13.1,917.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.21/0.49 920[3:MRR:15.0,917.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.49 921[3:MRR:14.0,917.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.49 922[3:MRR:12.0,917.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.49 937[3:SpR:920.0,88.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.21/0.49 939[3:Rew:918.0,937.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.21/0.49 940[3:Rew:921.0,939.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.49 941[3:Rew:940.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.21/0.49 945[3:Rew:940.0,78.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c6,u))**. % 0.21/0.49 947[3:Rew:940.0,922.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.21/0.49 949[3:Rew:940.0,654.2] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c7)** -> . % 0.21/0.49 951[3:Rew:940.0,949.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(sk_c8,multiply(u,sk_c8)),sk_c8)** -> . % 0.21/0.49 967[3:SpR:947.0,88.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.21/0.49 969[3:Rew:941.0,967.0,919.0,967.0] || -> equal(sk_c6,sk_c8)**. % 0.21/0.49 970[3:Rew:969.0,649.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.49 973[3:Rew:969.0,657.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.21/0.49 975[3:Rew:969.0,945.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),multiply(sk_c8,u))**. % 0.21/0.49 984[3:Rew:973.0,975.0] || -> equal(multiply(sk_c8,u),u)**. % 0.21/0.49 989[3:Rew:984.0,951.3] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(multiply(v,sk_c8),sk_c8)** equal(multiply(u,sk_c8),sk_c8)** -> . % 0.21/0.49 992[3:Con:989.0] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.21/0.49 1010[3:SpR:984.0,559.0] || -> equal(identity,sk_c8)**. % 0.21/0.49 1012[3:Rew:1010.0,559.0] || -> equal(multiply(u,sk_c8),u)**. % 0.21/0.49 1016[3:Rew:1012.0,992.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.21/0.49 1058[3:SpL:970.0,1016.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.21/0.49 1060[3:Obv:1058.1] || -> . % 0.21/0.49 1061[2:Spt:1060.0,3.1,649.0] || equal(inverse(sk_c8),sk_c6)** -> . % 0.21/0.49 1062[2:Spt:1060.0,3.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.21/0.49 1063[2:MRR:6.1,1061.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.21/0.49 1064[2:MRR:5.0,1061.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.21/0.49 1065[2:MRR:4.0,1061.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.21/0.49 1066[2:MRR:2.0,1061.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.21/0.49 1075[2:SpR:1064.0,88.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.21/0.49 1077[2:Rew:1063.0,1075.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.21/0.49 1078[2:Rew:1065.0,1077.0] || -> equal(sk_c7,sk_c8)**. % 0.21/0.49 1079[2:Rew:1078.0,1.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.21/0.49 1080[2:Rew:1078.0,570.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c8)**. % 0.21/0.49 1082[2:Rew:1078.0,1065.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.21/0.49 1083[2:Rew:1078.0,1066.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.21/0.49 1089[2:SpR:1082.0,88.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c5)**. % 0.21/0.49 1091[2:Rew:24.0,1089.0] || -> equal(identity,sk_c5)**. % 0.21/0.49 1093[2:Rew:1091.0,559.0] || -> equal(multiply(u,sk_c5),u)**. % 0.21/0.49 1094[2:Rew:1091.0,24.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.21/0.49 1100[2:SpR:1083.0,88.0] || -> equal(multiply(inverse(sk_c3),sk_c8),sk_c8)**. % 0.21/0.49 1102[2:Rew:1079.0,1100.0,1062.0,1100.0] || -> equal(sk_c6,sk_c8)**. % 0.21/0.49 1103[2:Rew:1102.0,1061.0] || equal(inverse(sk_c8),sk_c8)** -> . % 0.21/0.49 1105[2:Rew:1102.0,1080.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c8)**. % 0.21/0.49 1107[2:Rew:1094.0,1105.0] || -> equal(sk_c5,sk_c8)**. % 0.21/0.49 1108[2:Rew:1107.0,1064.0] || -> equal(multiply(sk_c4,sk_c8),sk_c8)**. % 0.21/0.49 1111[2:Rew:1107.0,1093.0] || -> equal(multiply(u,sk_c8),u)**. % 0.21/0.49 1118[2:Rew:1111.0,1108.0] || -> equal(sk_c4,sk_c8)**. % 0.21/0.49 1120[2:Rew:1118.0,1063.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.21/0.49 1122[2:MRR:1120.0,1103.0] || -> . % 0.21/0.49 % SZS output end Refutation % 0.21/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_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 prove_this_22 left_identity left_inverse associativity % 0.21/0.49 %------------------------------------------------------------------------------