%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP356-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n021.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:47:00 EDT 2022 % Result : Unsatisfiable 0.20s 0.49s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : GRP356-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n021.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 17:23:57 EDT 2022 % 0.13/0.34 % CPUTime : % 0.20/0.49 % 0.20/0.49 SPASS V 3.9 % 0.20/0.49 SPASS beiseite: Proof found. % 0.20/0.49 % SZS status Theorem % 0.20/0.49 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.20/0.49 SPASS derived 984 clauses, backtracked 367 clauses, performed 11 splits and kept 809 clauses. % 0.20/0.49 SPASS allocated 63715 KBytes. % 0.20/0.49 SPASS spent 0:00:00.14 on the problem. % 0.20/0.49 0:00:00.04 for the input. % 0.20/0.49 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.49 0:00:00.01 for inferences. % 0.20/0.49 0:00:00.00 for the backtracking. % 0.20/0.49 0:00:00.07 for the reduction. % 0.20/0.49 % 0.20/0.49 % 0.20/0.49 Here is a proof with depth 5, length 392 : % 0.20/0.49 % SZS output start Refutation % 0.20/0.49 1[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c8). % 0.20/0.49 2[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c7,sk_c6),sk_c8). % 0.20/0.49 3[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.49 4[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7)** equal(multiply(sk_c7,sk_c6),sk_c8). % 0.20/0.49 5[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5)** equal(multiply(sk_c7,sk_c6),sk_c8). % 0.20/0.49 6[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.49 7[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c1,sk_c7),sk_c8). % 0.20/0.49 8[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 9[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 10[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7)** equal(multiply(sk_c1,sk_c7),sk_c8). % 0.20/0.49 11[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 12[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 13[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 14[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 15[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 16[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.49 17[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.49 18[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 19[0:Inp] || -> equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c2,sk_c8),sk_c6). % 0.20/0.49 20[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c2,sk_c8),sk_c6)**. % 0.20/0.49 21[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c6)**. % 0.20/0.49 22[0:Inp] || -> equal(multiply(sk_c8,sk_c5),sk_c7)** equal(multiply(sk_c2,sk_c8),sk_c6). % 0.20/0.49 23[0:Inp] || -> equal(multiply(sk_c4,sk_c8),sk_c5) equal(multiply(sk_c2,sk_c8),sk_c6)**. % 0.20/0.49 24[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(multiply(sk_c2,sk_c8),sk_c6)**. % 0.20/0.49 25[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 26[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 27[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c2),sk_c8)**. % 0.20/0.49 28[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.49 29[0:Inp] || -> equal(inverse(sk_c2),sk_c8) equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.49 30[0:Inp] || -> equal(inverse(sk_c4),sk_c8) equal(inverse(sk_c2),sk_c8)**. % 0.20/0.49 31[0:Inp] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(inverse(x),sk_c7) equal(multiply(u,sk_c8),y)*+ equal(multiply(v,sk_c8),sk_c7)** equal(multiply(w,sk_c8),sk_c6)** equal(multiply(x,sk_c7),sk_c8)** equal(multiply(sk_c8,y),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c8) -> . % 0.20/0.49 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.20/0.49 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.20/0.49 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.20/0.49 35[1:Spt:31.0,31.4,31.8] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),v)* equal(multiply(sk_c8,v),sk_c7)** -> . % 0.20/0.49 37[2:Spt:1.1] || -> equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.49 39[3:Spt:25.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.20/0.49 41[4:Spt:13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 44[1:SpL:32.0,35.1] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.49 45[5:Spt:19.1] || -> equal(multiply(sk_c2,sk_c8),sk_c6)**. % 0.20/0.49 50[6:Spt:7.1] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 53[3:SpR:39.0,33.0] || -> equal(multiply(sk_c8,sk_c2),identity)**. % 0.20/0.49 54[4:SpR:41.0,33.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.20/0.49 55[1:SpL:33.0,35.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.49 61[3:SpR:53.0,34.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),multiply(identity,u))**. % 0.20/0.49 63[4:SpR:54.0,34.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),multiply(identity,u))**. % 0.20/0.49 65[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.49 68[3:Rew:32.0,61.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),u)**. % 0.20/0.49 69[4:Rew:32.0,63.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.20/0.49 70[0:Rew:32.0,65.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.49 74[5:SpR:45.0,68.0] || -> equal(multiply(sk_c8,sk_c6),sk_c8)**. % 0.20/0.49 80[6:SpR:50.0,69.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.20/0.49 86[0:SpR:70.0,70.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.49 89[3:SpR:53.0,70.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c2)**. % 0.20/0.49 91[5:SpR:74.0,70.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c6)**. % 0.20/0.49 92[2:SpR:37.0,70.0] || -> equal(multiply(inverse(sk_c7),sk_c8),sk_c6)**. % 0.20/0.49 93[4:SpR:54.0,70.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.20/0.49 95[6:SpR:80.0,70.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.20/0.49 97[0:SpR:33.0,70.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.49 103[5:Rew:33.0,91.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 104[5:Rew:103.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 105[5:Rew:103.0,33.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.20/0.49 106[5:Rew:103.0,53.0] || -> equal(multiply(sk_c8,sk_c2),sk_c6)**. % 0.20/0.49 109[5:Rew:103.0,55.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(sk_c6,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.49 110[5:Rew:103.0,89.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c2)**. % 0.20/0.49 114[5:Rew:103.0,93.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c1)**. % 0.20/0.49 117[6:Rew:105.0,95.0] || -> equal(sk_c8,sk_c6)**. % 0.20/0.49 119[6:Rew:117.0,37.0] || -> equal(multiply(sk_c7,sk_c6),sk_c6)**. % 0.20/0.49 120[6:Rew:117.0,39.0] || -> equal(inverse(sk_c2),sk_c6)**. % 0.20/0.49 125[6:Rew:117.0,80.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.49 132[6:Rew:117.0,106.0] || -> equal(multiply(sk_c6,sk_c2),sk_c6)**. % 0.20/0.49 134[6:Rew:119.0,125.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 136[6:Rew:134.0,104.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 141[6:Rew:134.0,117.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 142[6:Rew:134.0,120.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.49 146[6:Rew:134.0,132.0] || -> equal(multiply(sk_c7,sk_c2),sk_c7)**. % 0.20/0.49 148[6:Rew:136.0,146.0] || -> equal(sk_c2,sk_c7)**. % 0.20/0.49 149[6:Rew:148.0,142.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 181[6:Rew:136.0,109.2,141.0,109.2,134.0,109.1,149.0,109.0,149.0,109.0,141.0,109.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.49 182[6:Obv:181.1] || equal(u,sk_c7)* -> . % 0.20/0.49 183[6:UnC:182.0,70.0] || -> . % 0.20/0.49 186[6:Spt:183.0,7.1,50.0] || equal(multiply(sk_c1,sk_c7),sk_c8)** -> . % 0.20/0.49 187[6:Spt:183.0,7.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 188[5:Rew:86.0,97.0,103.0,97.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 189[5:Rew:188.0,110.0] || -> equal(inverse(sk_c8),sk_c2)**. % 0.20/0.49 190[5:Rew:188.0,114.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.20/0.49 191[5:Rew:188.0,37.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 193[5:Rew:191.0,45.0] || -> equal(multiply(sk_c2,sk_c7),sk_c6)**. % 0.20/0.49 195[6:Rew:191.0,187.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 197[6:Rew:191.0,186.0] || equal(multiply(sk_c1,sk_c7),sk_c7)** -> . % 0.20/0.49 199[5:Rew:191.0,189.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.20/0.49 200[5:Rew:199.0,190.0] || -> equal(sk_c2,sk_c1)**. % 0.20/0.49 203[5:Rew:200.0,193.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 205[6:Rew:203.0,197.0] || equal(sk_c6,sk_c7)** -> . % 0.20/0.49 214[5:Rew:203.0,9.1,191.0,9.1,191.0,9.0] || -> equal(inverse(sk_c3),sk_c7)** equal(sk_c6,sk_c7). % 0.20/0.49 215[6:MRR:214.1,205.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.49 220[5:Rew:203.0,8.1,191.0,8.1,191.0,8.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)** equal(sk_c6,sk_c7). % 0.20/0.49 221[6:MRR:220.1,205.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.49 283[6:SpR:221.0,70.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.20/0.49 285[6:Rew:195.0,283.0,215.0,283.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 286[6:MRR:285.0,205.0] || -> . % 0.20/0.49 287[5:Spt:286.0,19.1,45.0] || equal(multiply(sk_c2,sk_c8),sk_c6)** -> . % 0.20/0.49 288[5:Spt:286.0,19.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 289[0:Rew:86.0,97.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.49 290[4:Rew:289.0,93.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.20/0.49 291[3:Rew:289.0,89.0] || -> equal(inverse(sk_c8),sk_c2)**. % 0.20/0.49 292[4:Rew:290.0,92.0] || -> equal(multiply(sk_c1,sk_c8),sk_c6)**. % 0.20/0.49 295[5:MRR:24.1,287.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 297[5:MRR:23.1,287.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.49 298[5:MRR:22.1,287.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.49 314[3:SpR:291.0,70.0] || -> equal(multiply(sk_c2,multiply(sk_c8,u)),u)**. % 0.20/0.49 319[5:SpR:297.0,70.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.20/0.49 321[5:Rew:295.0,319.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.20/0.49 322[5:Rew:298.0,321.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 326[5:Rew:322.0,291.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.20/0.49 331[5:Rew:322.0,287.0] || equal(multiply(sk_c2,sk_c7),sk_c6)** -> . % 0.20/0.49 332[5:Rew:322.0,292.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 346[5:Rew:290.0,326.0] || -> equal(sk_c2,sk_c1)**. % 0.20/0.49 350[5:Rew:332.0,331.0,346.0,331.0] || equal(sk_c6,sk_c6)* -> . % 0.20/0.49 351[5:Obv:350.0] || -> . % 0.20/0.49 359[4:Spt:351.0,13.0,41.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.20/0.49 360[4:Spt:351.0,13.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 361[4:MRR:18.1,359.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 362[4:MRR:15.1,359.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.49 363[4:MRR:17.0,359.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.49 364[4:MRR:16.0,359.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.49 365[4:MRR:14.0,359.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 367[4:SpR:360.0,70.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.20/0.49 369[4:Rew:291.0,367.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.49 387[4:SpR:363.0,70.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.20/0.49 389[4:Rew:361.0,387.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.20/0.49 390[4:Rew:364.0,389.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 391[4:Rew:390.0,360.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 393[4:Rew:390.0,39.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.49 395[4:Rew:390.0,362.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.49 397[4:Rew:390.0,53.0] || -> equal(multiply(sk_c7,sk_c2),identity)**. % 0.20/0.49 400[4:Rew:390.0,314.0] || -> equal(multiply(sk_c2,multiply(sk_c7,u)),u)**. % 0.20/0.49 402[4:Rew:390.0,44.2] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 406[4:Rew:390.0,365.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.49 416[4:Rew:390.0,402.1,390.0,402.0] || equal(inverse(identity),sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 428[4:SpR:369.0,34.0] || -> equal(multiply(sk_c2,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.20/0.49 459[4:SpR:406.0,70.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.20/0.49 461[4:Rew:391.0,459.0,395.0,459.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 468[4:Rew:461.0,428.0] || -> equal(multiply(sk_c2,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.20/0.49 472[4:Rew:400.0,468.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 473[4:Rew:472.0,397.0] || -> equal(identity,sk_c2)**. % 0.20/0.49 481[4:Rew:472.0,416.2] || equal(inverse(identity),sk_c7)** equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.49 490[4:Obv:481.1] || equal(inverse(identity),sk_c7)** equal(u,sk_c7)* -> . % 0.20/0.49 491[4:Con:490.1] || equal(inverse(identity),sk_c7)** -> . % 0.20/0.49 492[4:Rew:473.0,491.0] || equal(inverse(sk_c2),sk_c7)** -> . % 0.20/0.49 493[4:Rew:393.0,492.0] || equal(sk_c7,sk_c7)* -> . % 0.20/0.49 494[4:Obv:493.0] || -> . % 0.20/0.49 495[3:Spt:494.0,25.0,39.0] || equal(inverse(sk_c2),sk_c8)** -> . % 0.20/0.49 496[3:Spt:494.0,25.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 497[3:MRR:30.1,495.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 498[3:MRR:27.1,495.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.49 499[3:MRR:29.0,495.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.49 500[3:MRR:28.0,495.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.49 501[3:MRR:26.0,495.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 503[3:SpR:496.0,70.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.20/0.49 513[3:SpR:499.0,70.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.20/0.49 515[3:Rew:497.0,513.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.20/0.49 516[3:Rew:500.0,515.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 517[3:Rew:516.0,496.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 519[3:Rew:516.0,498.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.49 523[3:Rew:516.0,92.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.49 526[3:Rew:516.0,44.2] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 528[3:Rew:516.0,501.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.49 531[3:Rew:516.0,503.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.20/0.49 536[3:Rew:33.0,523.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 537[3:Rew:536.0,289.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 538[3:Rew:536.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 541[3:Rew:537.0,531.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 546[3:Rew:516.0,526.1,536.0,526.0,516.0,526.0] || equal(inverse(sk_c6),sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 578[3:SpR:528.0,70.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.20/0.49 580[3:Rew:517.0,578.0,519.0,578.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 584[3:Rew:580.0,538.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 586[3:Rew:580.0,546.0] || equal(inverse(sk_c7),sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 611[3:Rew:541.0,586.0] || equal(sk_c7,sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 612[3:Obv:611.0] || equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 613[3:Rew:584.0,612.1] || equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.49 614[3:Obv:613.0] || equal(u,sk_c7)* -> . % 0.20/0.49 615[3:UnC:614.0,541.0] || -> . % 0.20/0.49 618[2:Spt:615.0,1.1,37.0] || equal(multiply(sk_c7,sk_c6),sk_c8)** -> . % 0.20/0.49 619[2:Spt:615.0,1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 620[2:MRR:6.1,618.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 621[2:MRR:3.1,618.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.49 622[2:MRR:5.1,618.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.49 623[2:MRR:4.1,618.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.49 624[2:MRR:2.1,618.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 626[2:SpR:619.0,70.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.20/0.49 633[2:SpR:622.0,70.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.20/0.49 635[2:Rew:620.0,633.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.20/0.49 636[2:Rew:623.0,635.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 637[2:Rew:636.0,619.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 639[2:Rew:636.0,621.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.49 642[2:Rew:636.0,623.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.20/0.49 643[2:Rew:636.0,624.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.49 647[2:Rew:636.0,55.2] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 648[2:Rew:636.0,626.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.20/0.49 656[2:Rew:636.0,647.0] || equal(inverse(inverse(sk_c7)),sk_c7) equal(identity,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 672[2:SpR:642.0,70.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c5)**. % 0.20/0.49 674[2:Rew:33.0,672.0] || -> equal(identity,sk_c5)**. % 0.20/0.49 675[2:Rew:674.0,32.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.49 676[2:Rew:674.0,289.0] || -> equal(multiply(u,sk_c5),u)**. % 0.20/0.49 677[2:Rew:674.0,33.0] || -> equal(multiply(inverse(u),u),sk_c5)**. % 0.20/0.49 680[2:Rew:674.0,656.1] || equal(inverse(inverse(sk_c7)),sk_c7) equal(sk_c5,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 684[2:SpR:643.0,70.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.20/0.49 686[2:Rew:637.0,684.0,639.0,684.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 689[2:Rew:686.0,648.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.20/0.49 693[2:Rew:677.0,689.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.49 696[2:Rew:693.0,675.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 697[2:Rew:693.0,676.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 701[2:Rew:693.0,680.1] || equal(inverse(inverse(sk_c7)),sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.49 708[2:Rew:697.0,643.0] || -> equal(sk_c3,sk_c7)**. % 0.20/0.49 710[2:Rew:708.0,639.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 722[2:Rew:696.0,701.2,710.0,701.0,710.0,701.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.49 723[2:Obv:722.1] || equal(u,sk_c7)* -> . % 0.20/0.49 724[2:UnC:723.0,636.0] || -> . % 0.20/0.49 726[1:Spt:724.0,31.1,31.2,31.3,31.5,31.6,31.7,31.9,31.10] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)**+ equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c8) -> . % 0.20/0.49 728[2:Spt:1.1] || -> equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.49 729[2:Rew:728.0,726.7] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6)** equal(sk_c8,sk_c8) -> . % 0.20/0.49 731[2:Obv:729.7] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6)** -> . % 0.20/0.49 734[2:SpR:728.0,70.0] || -> equal(multiply(inverse(sk_c7),sk_c8),sk_c6)**. % 0.20/0.49 736[3:Spt:13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 739[4:Spt:25.0] || -> equal(inverse(sk_c2),sk_c8)**. % 0.20/0.49 740[4:SpR:739.0,70.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),u)**. % 0.20/0.49 742[5:Spt:7.1] || -> equal(multiply(sk_c1,sk_c7),sk_c8)**. % 0.20/0.49 744[5:SpR:742.0,70.0] || -> equal(multiply(inverse(sk_c1),sk_c8),sk_c7)**. % 0.20/0.49 746[5:Rew:736.0,744.0] || -> equal(multiply(sk_c7,sk_c8),sk_c7)**. % 0.20/0.49 748[5:SpR:746.0,70.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c8)**. % 0.20/0.49 750[5:Rew:33.0,748.0] || -> equal(sk_c8,identity)**. % 0.20/0.49 751[5:Rew:750.0,728.0] || -> equal(multiply(sk_c7,sk_c6),identity)**. % 0.20/0.49 752[5:Rew:750.0,739.0] || -> equal(inverse(sk_c2),identity)**. % 0.20/0.49 756[5:Rew:750.0,21.0] || -> equal(inverse(sk_c3),identity) equal(multiply(sk_c2,sk_c8),sk_c6)**. % 0.20/0.49 758[5:Rew:750.0,731.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** equal(multiply(identity,sk_c7),sk_c6)** -> . % 0.20/0.49 759[5:Rew:750.0,19.0] || -> equal(multiply(identity,sk_c7),sk_c6)** equal(multiply(sk_c2,sk_c8),sk_c6). % 0.20/0.49 760[5:Rew:750.0,20.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c2,identity),sk_c6)**. % 0.20/0.49 761[5:Rew:750.0,22.1] || -> equal(multiply(sk_c8,sk_c5),sk_c7)** equal(multiply(sk_c2,identity),sk_c6). % 0.20/0.49 763[5:Rew:750.0,734.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c6)**. % 0.20/0.49 766[5:Rew:750.0,740.0] || -> equal(multiply(identity,multiply(sk_c2,u)),u)**. % 0.20/0.49 767[5:Rew:289.0,763.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.20/0.49 768[5:Rew:32.0,766.0] || -> equal(multiply(sk_c2,u),u)**. % 0.20/0.49 771[5:Rew:750.0,756.1,768.0,756.1] || -> equal(inverse(sk_c3),identity)** equal(identity,sk_c6). % 0.20/0.49 774[5:Rew:750.0,759.1,768.0,759.1,32.0,759.0] || -> equal(sk_c6,sk_c7) equal(identity,sk_c6)**. % 0.20/0.49 775[5:Rew:768.0,760.1,289.0,760.0,750.0,760.0] || -> equal(sk_c3,sk_c7) equal(identity,sk_c6)**. % 0.20/0.49 776[5:Rew:775.0,771.0] || -> equal(inverse(sk_c7),identity)** equal(identity,sk_c6). % 0.20/0.49 777[5:Rew:774.0,776.0,767.0,776.0] || -> equal(identity,sk_c7) equal(identity,sk_c6)**. % 0.20/0.49 779[5:Rew:768.0,761.1,32.0,761.0,750.0,761.0] || -> equal(sk_c5,sk_c7) equal(identity,sk_c6)**. % 0.20/0.49 783[5:Rew:32.0,758.6,750.0,758.5,289.0,758.4,750.0,758.4,289.0,758.3,750.0,758.3,750.0,758.1,750.0,758.0] || equal(inverse(u),identity)** equal(inverse(v),identity)** equal(inverse(w),sk_c7) equal(u,sk_c7) equal(v,sk_c6) equal(multiply(w,sk_c7),identity)** equal(sk_c6,sk_c7) -> . % 0.20/0.49 813[5:SpR:768.0,289.0] || -> equal(identity,sk_c2)**. % 0.20/0.49 816[5:Rew:813.0,752.0] || -> equal(inverse(sk_c2),sk_c2)**. % 0.20/0.49 818[5:Rew:813.0,751.0] || -> equal(multiply(sk_c7,sk_c6),sk_c2)**. % 0.20/0.49 820[5:Rew:813.0,289.0] || -> equal(multiply(u,sk_c2),u)**. % 0.20/0.49 824[5:Rew:813.0,779.1] || -> equal(sk_c5,sk_c7) equal(sk_c2,sk_c6)**. % 0.20/0.49 825[5:Rew:813.0,777.1] || -> equal(identity,sk_c7)** equal(sk_c2,sk_c6). % 0.20/0.49 828[5:Rew:813.0,783.0] || equal(inverse(u),sk_c2)** equal(inverse(v),identity)** equal(inverse(w),sk_c7) equal(u,sk_c7) equal(v,sk_c6) equal(multiply(w,sk_c7),identity)** equal(sk_c6,sk_c7) -> . % 0.20/0.49 832[5:Rew:813.0,825.0] || -> equal(sk_c2,sk_c7) equal(sk_c2,sk_c6)**. % 0.20/0.49 833[5:Rew:813.0,828.5,813.0,828.1] || equal(inverse(u),sk_c2)** equal(inverse(v),sk_c2)** equal(inverse(w),sk_c7) equal(u,sk_c7) equal(v,sk_c6) equal(multiply(w,sk_c7),sk_c2)** equal(sk_c6,sk_c7) -> . % 0.20/0.49 834[6:Spt:824.1] || -> equal(sk_c2,sk_c6)**. % 0.20/0.49 839[6:Rew:834.0,818.0] || -> equal(multiply(sk_c7,sk_c6),sk_c6)**. % 0.20/0.49 841[6:Rew:834.0,820.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 843[6:Rew:834.0,833.0] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c2)** equal(inverse(w),sk_c7) equal(u,sk_c7) equal(v,sk_c6) equal(multiply(w,sk_c7),sk_c2)** equal(sk_c6,sk_c7) -> . % 0.20/0.49 846[6:Rew:841.0,839.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 847[6:Rew:846.0,767.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 848[6:Rew:846.0,834.0] || -> equal(sk_c2,sk_c7)**. % 0.20/0.49 854[6:Rew:846.0,841.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 862[6:Rew:846.0,843.6,854.0,843.5,848.0,843.5,846.0,843.4,848.0,843.1,846.0,843.0] || 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) equal(sk_c7,sk_c7) -> . % 0.20/0.49 863[6:Obv:862.6] || 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.20/0.49 864[6:Con:863.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.49 892[6:SpL:847.0,864.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.49 893[6:Obv:892.1] || -> . % 0.20/0.49 894[6:Spt:893.0,824.1,834.0] || equal(sk_c2,sk_c6)** -> . % 0.20/0.49 895[6:Spt:893.0,824.0] || -> equal(sk_c5,sk_c7)**. % 0.20/0.49 896[6:MRR:832.1,894.0] || -> equal(sk_c2,sk_c7)**. % 0.20/0.49 899[6:Rew:896.0,816.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.49 900[6:Rew:896.0,894.0] || equal(sk_c6,sk_c7)** -> . % 0.20/0.49 905[6:Rew:767.0,899.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 907[6:Rew:905.0,900.0] || equal(sk_c7,sk_c7)* -> . % 0.20/0.49 908[6:Obv:907.0] || -> . % 0.20/0.49 922[5:Spt:908.0,7.1,742.0] || equal(multiply(sk_c1,sk_c7),sk_c8)** -> . % 0.20/0.49 923[5:Spt:908.0,7.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 924[5:MRR:12.1,922.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 925[5:MRR:9.1,922.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.49 926[5:MRR:11.1,922.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.49 927[5:MRR:10.1,922.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.49 928[5:MRR:8.1,922.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 945[5:SpR:926.0,70.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.20/0.49 947[5:Rew:924.0,945.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.20/0.49 948[5:Rew:927.0,947.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.49 949[5:Rew:948.0,923.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 952[5:Rew:948.0,925.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.49 955[5:Rew:948.0,734.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.49 956[5:Rew:948.0,922.0] || equal(multiply(sk_c1,sk_c7),sk_c7)** -> . % 0.20/0.49 960[5:Rew:948.0,928.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.49 967[5:Rew:33.0,955.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 968[5:Rew:967.0,289.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 969[5:Rew:967.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 970[5:Rew:967.0,33.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.20/0.49 1008[5:SpR:960.0,70.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.20/0.49 1010[5:Rew:949.0,1008.0,952.0,1008.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.49 1013[5:Rew:1010.0,968.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.49 1014[5:Rew:1010.0,969.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.49 1015[5:Rew:1010.0,970.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.20/0.49 1021[5:Rew:1013.0,956.0] || equal(sk_c1,sk_c7)** -> . % 0.20/0.49 1067[5:SpR:736.0,1015.0] || -> equal(multiply(sk_c7,sk_c1),sk_c7)**. % 0.20/0.49 1069[5:Rew:1014.0,1067.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.49 1070[5:MRR:1069.0,1021.0] || -> . % 0.20/0.49 1074[4:Spt:1070.0,25.0,739.0] || equal(inverse(sk_c2),sk_c8)** -> . % 0.20/0.49 1075[4:Spt:1070.0,25.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.49 1076[4:MRR:30.1,1074.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.49 1077[4:MRR:27.1,1074.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.49 1078[4:MRR:29.0,1074.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.49 1079[4:MRR:28.0,1074.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.49 1080[4:MRR:26.0,1074.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.49 1081[4:Rew:1075.0,731.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** equal(sk_c6,sk_c6) -> . % 0.20/0.50 1082[4:Obv:1081.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.20/0.50 1086[4:SpR:1075.0,70.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.20/0.50 1096[4:SpR:1078.0,70.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.20/0.50 1098[4:Rew:1076.0,1096.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.20/0.50 1099[4:Rew:1079.0,1098.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.50 1100[4:Rew:1099.0,1075.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.50 1102[4:Rew:1099.0,1077.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.50 1106[4:Rew:1099.0,734.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.50 1109[4:Rew:1099.0,1080.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.50 1110[4:Rew:1099.0,1082.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.20/0.50 1112[4:Rew:1099.0,1086.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.20/0.50 1116[4:Rew:33.0,1106.0] || -> equal(identity,sk_c6)**. % 0.20/0.50 1118[4:Rew:1116.0,289.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.50 1121[4:Rew:1118.0,1112.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.50 1125[4:Rew:1099.0,1110.5,1099.0,1110.4,1099.0,1110.3,1099.0,1110.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_c6)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.20/0.50 1126[4:Con:1125.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** -> . % 0.20/0.50 1155[4:SpR:1109.0,70.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.20/0.50 1157[4:Rew:1100.0,1155.0,1102.0,1155.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.50 1161[4:Rew:1157.0,1118.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.50 1164[4:Rew:1157.0,1126.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** -> . % 0.20/0.50 1181[4:Con:1164.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.20/0.50 1182[4:Rew:1161.0,1181.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.50 1247[4:SpL:1121.0,1182.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.50 1249[4:Obv:1247.1] || -> . % 0.20/0.50 1250[3:Spt:1249.0,13.0,736.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.20/0.50 1251[3:Spt:1249.0,13.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.50 1252[3:MRR:18.1,1250.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.50 1253[3:MRR:15.1,1250.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.50 1254[3:MRR:17.0,1250.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.50 1255[3:MRR:16.0,1250.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.50 1256[3:MRR:14.0,1250.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.50 1257[3:Rew:1251.0,731.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** equal(sk_c6,sk_c6) -> . % 0.20/0.50 1258[3:Obv:1257.6] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.20/0.50 1262[3:SpR:1251.0,70.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.20/0.50 1272[3:SpR:1254.0,70.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.20/0.50 1274[3:Rew:1252.0,1272.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.20/0.50 1275[3:Rew:1255.0,1274.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.50 1276[3:Rew:1275.0,1251.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.50 1278[3:Rew:1275.0,1253.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.50 1281[3:Rew:1275.0,734.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.50 1284[3:Rew:1275.0,1256.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.50 1285[3:Rew:1275.0,1258.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c8) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c7)** equal(multiply(v,sk_c8),sk_c6)** equal(multiply(w,sk_c7),sk_c8)** -> . % 0.20/0.50 1287[3:Rew:1275.0,1262.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c7)**. % 0.20/0.50 1291[3:Rew:33.0,1281.0] || -> equal(identity,sk_c6)**. % 0.20/0.50 1292[3:Rew:1291.0,289.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.50 1296[3:Rew:1292.0,1287.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.50 1300[3:Rew:1275.0,1285.5,1275.0,1285.4,1275.0,1285.3,1275.0,1285.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_c6)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.20/0.50 1301[3:Con:1300.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** -> . % 0.20/0.50 1331[3:SpR:1284.0,70.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.20/0.50 1333[3:Rew:1276.0,1331.0,1278.0,1331.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.50 1337[3:Rew:1333.0,1292.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.50 1341[3:Rew:1333.0,1301.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** -> . % 0.20/0.50 1356[3:Con:1341.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.20/0.50 1357[3:Rew:1337.0,1356.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.50 1395[3:SpL:1296.0,1357.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.50 1397[3:Obv:1395.1] || -> . % 0.20/0.50 1398[2:Spt:1397.0,1.1,728.0] || equal(multiply(sk_c7,sk_c6),sk_c8)** -> . % 0.20/0.50 1399[2:Spt:1397.0,1.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.20/0.50 1400[2:MRR:6.1,1398.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.20/0.50 1401[2:MRR:3.1,1398.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.50 1402[2:MRR:5.1,1398.0] || -> equal(multiply(sk_c4,sk_c8),sk_c5)**. % 0.20/0.50 1403[2:MRR:4.1,1398.0] || -> equal(multiply(sk_c8,sk_c5),sk_c7)**. % 0.20/0.50 1404[2:MRR:2.1,1398.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.50 1413[2:SpR:1402.0,70.0] || -> equal(multiply(inverse(sk_c4),sk_c5),sk_c8)**. % 0.20/0.50 1415[2:Rew:1400.0,1413.0] || -> equal(multiply(sk_c8,sk_c5),sk_c8)**. % 0.20/0.50 1416[2:Rew:1403.0,1415.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.50 1417[2:Rew:1416.0,1399.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.50 1419[2:Rew:1416.0,1401.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.50 1421[2:Rew:1416.0,1398.0] || equal(multiply(sk_c7,sk_c6),sk_c7)** -> . % 0.20/0.50 1423[2:Rew:1416.0,1404.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.20/0.50 1452[2:SpR:1423.0,70.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c7)**. % 0.20/0.50 1454[2:Rew:1417.0,1452.0,1419.0,1452.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.50 1455[2:Rew:1454.0,1417.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.50 1456[2:Rew:1454.0,1421.0] || equal(multiply(sk_c7,sk_c7),sk_c7)** -> . % 0.20/0.50 1459[2:Rew:1455.0,1456.0] || equal(sk_c7,sk_c7)* -> . % 0.20/0.50 1460[2:Obv:1459.0] || -> . % 0.20/0.50 % SZS output end Refutation % 0.20/0.50 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 prove_this_23 prove_this_24 prove_this_25 prove_this_26 prove_this_27 prove_this_28 prove_this_29 prove_this_30 prove_this_31 left_identity left_inverse associativity % 0.20/0.50 %------------------------------------------------------------------------------