%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP224-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n016.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:24 EDT 2022 % Result : Unsatisfiable 0.18s 0.56s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : GRP224-1 : TPTP v8.1.0. Released v2.5.0. % 0.11/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n016.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jun 13 17:53:59 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.56 % 0.18/0.56 SPASS V 3.9 % 0.18/0.56 SPASS beiseite: Proof found. % 0.18/0.56 % SZS status Theorem % 0.18/0.56 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.56 SPASS derived 1992 clauses, backtracked 567 clauses, performed 11 splits and kept 1227 clauses. % 0.18/0.56 SPASS allocated 64584 KBytes. % 0.18/0.56 SPASS spent 0:00:00.23 on the problem. % 0.18/0.56 0:00:00.04 for the input. % 0.18/0.56 0:00:00.00 for the FLOTTER CNF translation. % 0.18/0.56 0:00:00.01 for inferences. % 0.18/0.56 0:00:00.00 for the backtracking. % 0.18/0.56 0:00:00.15 for the reduction. % 0.18/0.56 % 0.18/0.56 % 0.18/0.56 Here is a proof with depth 5, length 541 : % 0.18/0.56 % SZS output start Refutation % 0.18/0.56 1[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.18/0.56 2[0:Inp] || -> equal(inverse(sk_c4),sk_c5)** equal(inverse(sk_c1),sk_c11). % 0.18/0.56 3[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.18/0.56 4[0:Inp] || -> equal(inverse(sk_c6),sk_c11)** equal(inverse(sk_c1),sk_c11). % 0.18/0.56 5[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c6,sk_c10),sk_c11)**. % 0.18/0.56 6[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.56 7[0:Inp] || -> equal(inverse(sk_c7),sk_c8)** equal(inverse(sk_c1),sk_c11). % 0.18/0.56 8[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c8,sk_c11),sk_c10)**. % 0.18/0.56 9[0:Inp] || -> equal(inverse(sk_c9),sk_c10)** equal(inverse(sk_c1),sk_c11). % 0.18/0.56 10[0:Inp] || -> equal(inverse(sk_c1),sk_c11) equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.56 16[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c10)** equal(multiply(sk_c1,sk_c10),sk_c11). % 0.18/0.56 17[0:Inp] || -> equal(inverse(sk_c7),sk_c8) equal(multiply(sk_c1,sk_c10),sk_c11)**. % 0.18/0.56 18[0:Inp] || -> equal(multiply(sk_c8,sk_c11),sk_c10)** equal(multiply(sk_c1,sk_c10),sk_c11). % 0.18/0.56 19[0:Inp] || -> equal(inverse(sk_c9),sk_c10) equal(multiply(sk_c1,sk_c10),sk_c11)**. % 0.18/0.56 20[0:Inp] || -> equal(multiply(sk_c9,sk_c11),sk_c10)** equal(multiply(sk_c1,sk_c10),sk_c11). % 0.18/0.56 21[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c11) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 22[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 23[0:Inp] || -> equal(multiply(sk_c5,sk_c10),sk_c11) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 24[0:Inp] || -> equal(inverse(sk_c6),sk_c11) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 25[0:Inp] || -> equal(multiply(sk_c6,sk_c10),sk_c11) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 26[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c10) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 27[0:Inp] || -> equal(inverse(sk_c7),sk_c8) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 29[0:Inp] || -> equal(inverse(sk_c9),sk_c10) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 30[0:Inp] || -> equal(multiply(sk_c9,sk_c11),sk_c10) equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 31[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c11) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 32[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 33[0:Inp] || -> equal(multiply(sk_c5,sk_c10),sk_c11) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 34[0:Inp] || -> equal(inverse(sk_c6),sk_c11) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 35[0:Inp] || -> equal(multiply(sk_c6,sk_c10),sk_c11) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 36[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c10) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 37[0:Inp] || -> equal(inverse(sk_c7),sk_c8) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 38[0:Inp] || -> equal(multiply(sk_c8,sk_c11),sk_c10) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 39[0:Inp] || -> equal(inverse(sk_c9),sk_c10) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 40[0:Inp] || -> equal(multiply(sk_c9,sk_c11),sk_c10) equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 41[0:Inp] || -> equal(inverse(sk_c2),sk_c11) equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.18/0.56 42[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(inverse(sk_c2),sk_c11)**. % 0.18/0.56 43[0:Inp] || -> equal(inverse(sk_c2),sk_c11) equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.18/0.56 46[0:Inp] || -> equal(inverse(sk_c2),sk_c11) equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.56 47[0:Inp] || -> equal(inverse(sk_c7),sk_c8) equal(inverse(sk_c2),sk_c11)**. % 0.18/0.56 48[0:Inp] || -> equal(inverse(sk_c2),sk_c11) equal(multiply(sk_c8,sk_c11),sk_c10)**. % 0.18/0.56 49[0:Inp] || -> equal(inverse(sk_c9),sk_c10) equal(inverse(sk_c2),sk_c11)**. % 0.18/0.56 50[0:Inp] || -> equal(inverse(sk_c2),sk_c11) equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.56 51[0:Inp] || equal(inverse(u),sk_c11) equal(multiply(u,sk_c10),sk_c11)** equal(multiply(sk_c11,v),sk_c10)** equal(multiply(w,sk_c11),v)* equal(inverse(w),sk_c11) equal(multiply(x,y),sk_c11)** equal(inverse(x),y) equal(multiply(y,sk_c10),sk_c11)** equal(inverse(z),sk_c11) equal(multiply(z,sk_c10),sk_c11)** equal(multiply(x1,x2),sk_c10)** equal(inverse(x1),x2) equal(multiply(x2,sk_c11),sk_c10)** equal(inverse(x3),sk_c10) equal(multiply(x3,sk_c11),sk_c10)** -> . % 0.18/0.56 52[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.18/0.56 53[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.18/0.56 54[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.18/0.56 55[0:Con:51.8] || equal(inverse(u),v) equal(inverse(w),x) equal(inverse(y),sk_c10) equal(inverse(z),sk_c11) equal(inverse(x1),sk_c11) equal(multiply(u,v),sk_c10)**+ equal(multiply(w,x),sk_c11)** equal(multiply(z,sk_c11),x2)* equal(multiply(y,sk_c11),sk_c10)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(x1,sk_c10),sk_c11)** equal(multiply(sk_c11,x2),sk_c10)** -> . % 0.18/0.56 56[1:Spt:55.1,55.6,55.10] || equal(inverse(u),v) equal(multiply(u,v),sk_c11)**+ equal(multiply(v,sk_c10),sk_c11)** -> . % 0.18/0.56 57[2:Spt:49.1] || -> equal(inverse(sk_c2),sk_c11)**. % 0.18/0.56 59[3:Spt:9.1] || -> equal(inverse(sk_c1),sk_c11)**. % 0.18/0.56 61[4:Spt:39.1] || -> equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.56 66[5:Spt:27.1] || -> equal(multiply(sk_c11,sk_c3),sk_c10)**. % 0.18/0.56 69[6:Spt:17.1] || -> equal(multiply(sk_c1,sk_c10),sk_c11)**. % 0.18/0.56 75[1:SpL:52.0,56.1] || equal(inverse(identity),u) equal(u,sk_c11) equal(multiply(u,sk_c10),sk_c11)** -> . % 0.18/0.56 77[2:SpR:57.0,53.0] || -> equal(multiply(sk_c11,sk_c2),identity)**. % 0.18/0.56 78[3:SpR:59.0,53.0] || -> equal(multiply(sk_c11,sk_c1),identity)**. % 0.18/0.56 91[2:SpR:77.0,54.0] || -> equal(multiply(sk_c11,multiply(sk_c2,u)),multiply(identity,u))**. % 0.18/0.56 94[0:SpR:53.0,54.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.18/0.56 96[2:Rew:52.0,91.0] || -> equal(multiply(sk_c11,multiply(sk_c2,u)),u)**. % 0.18/0.56 98[0:Rew:52.0,94.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.18/0.56 102[4:SpR:61.0,96.0] || -> equal(multiply(sk_c11,sk_c3),sk_c11)**. % 0.18/0.56 103[2:SpL:96.0,56.1] || equal(multiply(sk_c2,u),inverse(sk_c11)) equal(u,sk_c11) equal(multiply(multiply(sk_c2,u),sk_c10),sk_c11)** -> . % 0.18/0.56 104[5:Rew:66.0,102.0] || -> equal(sk_c11,sk_c10)**. % 0.18/0.56 107[5:Rew:104.0,59.0] || -> equal(inverse(sk_c1),sk_c10)**. % 0.18/0.56 108[5:Rew:104.0,61.0] || -> equal(multiply(sk_c2,sk_c10),sk_c3)**. % 0.18/0.56 109[5:Rew:104.0,66.0] || -> equal(multiply(sk_c10,sk_c3),sk_c10)**. % 0.18/0.56 110[6:Rew:104.0,69.0] || -> equal(multiply(sk_c1,sk_c10),sk_c10)**. % 0.18/0.56 111[5:Rew:104.0,77.0] || -> equal(multiply(sk_c10,sk_c2),identity)**. % 0.18/0.56 112[5:Rew:104.0,78.0] || -> equal(multiply(sk_c10,sk_c1),identity)**. % 0.18/0.56 138[2:Rew:54.0,103.2] || equal(multiply(sk_c2,u),inverse(sk_c11)) equal(u,sk_c11) equal(multiply(sk_c2,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.56 139[5:Rew:104.0,138.2,104.0,138.1,104.0,138.0] || equal(multiply(sk_c2,u),inverse(sk_c10)) equal(u,sk_c10) equal(multiply(sk_c2,multiply(u,sk_c10)),sk_c10)** -> . % 0.18/0.56 159[0:SpR:98.0,98.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.18/0.56 161[0:SpR:52.0,98.0] || -> equal(multiply(inverse(identity),u),u)**. % 0.18/0.56 162[0:SpR:53.0,98.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.56 166[5:SpR:109.0,98.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c3)**. % 0.18/0.56 167[5:SpR:111.0,98.0] || -> equal(multiply(inverse(sk_c10),identity),sk_c2)**. % 0.18/0.56 168[5:SpR:112.0,98.0] || -> equal(multiply(inverse(sk_c10),identity),sk_c1)**. % 0.18/0.56 174[5:Rew:53.0,166.0] || -> equal(identity,sk_c3)**. % 0.18/0.56 183[5:Rew:174.0,161.0] || -> equal(multiply(inverse(sk_c3),u),u)**. % 0.18/0.56 187[5:Rew:174.0,167.0] || -> equal(multiply(inverse(sk_c10),sk_c3),sk_c2)**. % 0.18/0.56 188[5:Rew:187.0,168.0,174.0,168.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.56 190[5:Rew:188.0,108.0] || -> equal(multiply(sk_c1,sk_c10),sk_c3)**. % 0.18/0.56 192[5:Rew:188.0,139.0] || equal(multiply(sk_c1,u),inverse(sk_c10)) equal(u,sk_c10) equal(multiply(sk_c2,multiply(u,sk_c10)),sk_c10)** -> . % 0.18/0.56 194[5:Rew:188.0,187.0] || -> equal(multiply(inverse(sk_c10),sk_c3),sk_c1)**. % 0.18/0.56 195[6:Rew:110.0,190.0] || -> equal(sk_c3,sk_c10)**. % 0.18/0.56 197[6:Rew:195.0,174.0] || -> equal(identity,sk_c10)**. % 0.18/0.56 204[6:Rew:195.0,183.0] || -> equal(multiply(inverse(sk_c10),u),u)**. % 0.18/0.56 205[6:Rew:204.0,194.0,195.0,194.0] || -> equal(sk_c10,sk_c1)**. % 0.18/0.56 207[6:Rew:205.0,107.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.18/0.56 215[6:Rew:205.0,197.0] || -> equal(identity,sk_c1)**. % 0.18/0.56 218[6:Rew:205.0,204.0] || -> equal(multiply(inverse(sk_c1),u),u)**. % 0.18/0.56 221[6:Rew:207.0,218.0] || -> equal(multiply(sk_c1,u),u)**. % 0.18/0.56 222[6:Rew:215.0,162.0] || -> equal(multiply(inverse(inverse(u)),sk_c1),u)**. % 0.18/0.56 228[6:Rew:159.0,222.0] || -> equal(multiply(u,sk_c1),u)**. % 0.18/0.56 244[6:Rew:221.0,192.2,188.0,192.2,228.0,192.2,205.0,192.2,205.0,192.1,221.0,192.0,207.0,192.0,205.0,192.0] || equal(u,sk_c1)* equal(u,sk_c1)* equal(u,sk_c1)* -> . % 0.18/0.56 245[6:Obv:244.1] || equal(u,sk_c1)* -> . % 0.18/0.56 246[6:UnC:245.0,98.0] || -> . % 0.18/0.56 248[6:Spt:246.0,17.1,69.0] || equal(multiply(sk_c1,sk_c10),sk_c11)** -> . % 0.18/0.56 249[6:Spt:246.0,17.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.18/0.56 250[6:Rew:190.0,248.0,104.0,248.0] || equal(sk_c3,sk_c10)** -> . % 0.18/0.57 251[5:Rew:159.0,162.0,174.0,162.0] || -> equal(multiply(u,sk_c3),u)**. % 0.18/0.57 252[5:Rew:251.0,194.0] || -> equal(inverse(sk_c10),sk_c1)**. % 0.18/0.57 266[5:Rew:190.0,18.1,104.0,18.1,104.0,18.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)** equal(sk_c3,sk_c10). % 0.18/0.57 267[6:MRR:266.1,250.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)**. % 0.18/0.57 268[5:Rew:190.0,16.1,104.0,16.1] || -> equal(multiply(sk_c7,sk_c8),sk_c10)** equal(sk_c3,sk_c10). % 0.18/0.57 269[6:MRR:268.1,250.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.57 310[6:SpR:267.0,98.0] || -> equal(multiply(inverse(sk_c8),sk_c10),sk_c10)**. % 0.18/0.57 313[6:SpR:269.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.57 315[6:Rew:267.0,313.0,249.0,313.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.57 320[6:Rew:315.0,310.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c10)**. % 0.18/0.57 322[6:Rew:190.0,320.0,252.0,320.0] || -> equal(sk_c3,sk_c10)**. % 0.18/0.57 323[6:MRR:322.0,250.0] || -> . % 0.18/0.57 325[5:Spt:323.0,27.1,66.0] || equal(multiply(sk_c11,sk_c3),sk_c10)** -> . % 0.18/0.57 326[5:Spt:323.0,27.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.18/0.57 327[5:Rew:102.0,325.0] || equal(sk_c11,sk_c10)** -> . % 0.18/0.57 328[0:Rew:159.0,162.0] || -> equal(multiply(u,identity),u)**. % 0.18/0.57 329[4:Rew:102.0,29.1] || -> equal(inverse(sk_c9),sk_c10)** equal(sk_c11,sk_c10). % 0.18/0.57 330[5:MRR:329.1,327.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.57 331[4:Rew:102.0,24.1] || -> equal(inverse(sk_c6),sk_c11)** equal(sk_c11,sk_c10). % 0.18/0.57 332[5:MRR:331.1,327.0] || -> equal(inverse(sk_c6),sk_c11)**. % 0.18/0.57 335[4:Rew:102.0,30.1] || -> equal(multiply(sk_c9,sk_c11),sk_c10)** equal(sk_c11,sk_c10). % 0.18/0.57 336[5:MRR:335.1,327.0] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.57 339[4:Rew:102.0,26.1] || -> equal(multiply(sk_c7,sk_c8),sk_c10)** equal(sk_c11,sk_c10). % 0.18/0.57 340[5:MRR:339.1,327.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.57 341[4:Rew:102.0,25.1] || -> equal(multiply(sk_c6,sk_c10),sk_c11)** equal(sk_c11,sk_c10). % 0.18/0.57 342[5:MRR:341.1,327.0] || -> equal(multiply(sk_c6,sk_c10),sk_c11)**. % 0.18/0.57 343[4:Rew:102.0,23.1] || -> equal(multiply(sk_c5,sk_c10),sk_c11)** equal(sk_c11,sk_c10). % 0.18/0.57 344[5:MRR:343.1,327.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.18/0.57 355[5:SpR:330.0,98.0] || -> equal(multiply(sk_c10,multiply(sk_c9,u)),u)**. % 0.18/0.57 362[4:SpR:102.0,98.0] || -> equal(multiply(inverse(sk_c11),sk_c11),sk_c3)**. % 0.18/0.57 364[4:Rew:53.0,362.0] || -> equal(identity,sk_c3)**. % 0.18/0.57 365[4:Rew:364.0,78.0] || -> equal(multiply(sk_c11,sk_c1),sk_c3)**. % 0.18/0.57 366[4:Rew:364.0,77.0] || -> equal(multiply(sk_c11,sk_c2),sk_c3)**. % 0.18/0.57 367[4:Rew:364.0,52.0] || -> equal(multiply(sk_c3,u),u)**. % 0.18/0.57 368[4:Rew:364.0,53.0] || -> equal(multiply(inverse(u),u),sk_c3)**. % 0.18/0.57 371[4:Rew:364.0,328.0] || -> equal(multiply(u,sk_c3),u)**. % 0.18/0.57 383[5:SpR:336.0,54.0] || -> equal(multiply(sk_c9,multiply(sk_c11,u)),multiply(sk_c10,u))**. % 0.18/0.57 391[5:SpR:340.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.57 393[5:Rew:326.0,391.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.18/0.57 406[4:SpR:365.0,98.0] || -> equal(multiply(inverse(sk_c11),sk_c3),sk_c1)**. % 0.18/0.57 408[4:Rew:371.0,406.0] || -> equal(inverse(sk_c11),sk_c1)**. % 0.18/0.57 409[4:Rew:408.0,138.0] || equal(multiply(sk_c2,u),sk_c1) equal(u,sk_c11) equal(multiply(sk_c2,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.57 417[4:SpR:366.0,98.0] || -> equal(multiply(inverse(sk_c11),sk_c3),sk_c2)**. % 0.18/0.57 419[4:Rew:408.0,417.0] || -> equal(multiply(sk_c1,sk_c3),sk_c2)**. % 0.18/0.57 420[4:Rew:371.0,419.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.57 425[4:Rew:420.0,409.0] || equal(multiply(sk_c1,u),sk_c1) equal(u,sk_c11) equal(multiply(sk_c2,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.57 431[4:Rew:420.0,425.2] || equal(multiply(sk_c1,u),sk_c1) equal(u,sk_c11) equal(multiply(sk_c1,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.57 440[5:SpR:393.0,98.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c10)**. % 0.18/0.57 442[5:Rew:368.0,440.0] || -> equal(sk_c3,sk_c10)**. % 0.18/0.57 445[5:Rew:442.0,367.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.57 449[5:Rew:442.0,371.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.57 455[5:Rew:445.0,383.0] || -> equal(multiply(sk_c9,multiply(sk_c11,u)),u)**. % 0.18/0.57 461[5:Rew:445.0,355.0] || -> equal(multiply(sk_c9,u),u)**. % 0.18/0.57 463[5:Rew:449.0,344.0] || -> equal(sk_c11,sk_c5)**. % 0.18/0.57 464[5:Rew:449.0,342.0] || -> equal(sk_c11,sk_c6)**. % 0.18/0.57 468[5:Rew:449.0,431.2] || equal(multiply(sk_c1,u),sk_c1) equal(u,sk_c11) equal(multiply(sk_c1,u),sk_c11)** -> . % 0.18/0.57 471[5:Rew:463.0,332.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.18/0.57 475[5:Rew:463.0,408.0] || -> equal(inverse(sk_c5),sk_c1)**. % 0.18/0.57 485[5:Rew:463.0,464.0] || -> equal(sk_c6,sk_c5)**. % 0.18/0.57 487[5:Rew:485.0,471.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.57 488[5:Rew:487.0,475.0] || -> equal(sk_c5,sk_c1)**. % 0.18/0.57 491[5:Rew:488.0,463.0] || -> equal(sk_c11,sk_c1)**. % 0.18/0.57 508[5:Rew:461.0,455.0,491.0,455.0] || -> equal(multiply(sk_c1,u),u)**. % 0.18/0.57 538[5:Rew:508.0,468.2,491.0,468.2,491.0,468.1,508.0,468.0] || equal(u,sk_c1)* equal(u,sk_c1)* equal(u,sk_c1)* -> . % 0.18/0.57 539[5:Obv:538.1] || equal(u,sk_c1)* -> . % 0.18/0.57 540[5:UnC:539.0,420.0] || -> . % 0.18/0.57 542[4:Spt:540.0,39.1,61.0] || equal(multiply(sk_c2,sk_c11),sk_c3)** -> . % 0.18/0.57 543[4:Spt:540.0,39.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.57 544[4:MRR:37.1,542.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.18/0.57 545[4:MRR:34.1,542.0] || -> equal(inverse(sk_c6),sk_c11)**. % 0.18/0.57 547[4:MRR:40.1,542.0] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.57 549[4:MRR:36.1,542.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.57 550[4:MRR:35.1,542.0] || -> equal(multiply(sk_c6,sk_c10),sk_c11)**. % 0.18/0.57 566[2:SpR:77.0,98.0] || -> equal(multiply(inverse(sk_c11),identity),sk_c2)**. % 0.18/0.57 568[2:Rew:328.0,566.0] || -> equal(inverse(sk_c11),sk_c2)**. % 0.18/0.57 571[2:Rew:568.0,138.0] || equal(multiply(sk_c2,u),sk_c2) equal(u,sk_c11) equal(multiply(sk_c2,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.57 577[4:SpR:547.0,98.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c11)**. % 0.18/0.57 579[4:Rew:543.0,577.0] || -> equal(multiply(sk_c10,sk_c10),sk_c11)**. % 0.18/0.57 581[3:SpR:78.0,98.0] || -> equal(multiply(inverse(sk_c11),identity),sk_c1)**. % 0.18/0.57 583[3:Rew:568.0,581.0] || -> equal(multiply(sk_c2,identity),sk_c1)**. % 0.18/0.57 584[3:Rew:328.0,583.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.57 587[3:Rew:584.0,568.0] || -> equal(inverse(sk_c11),sk_c1)**. % 0.18/0.57 592[3:Rew:584.0,571.0] || equal(multiply(sk_c1,u),sk_c1) equal(u,sk_c11) equal(multiply(sk_c2,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.57 596[3:Rew:584.0,592.2] || equal(multiply(sk_c1,u),sk_c1) equal(u,sk_c11) equal(multiply(sk_c1,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.57 604[4:SpR:549.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.57 606[4:Rew:544.0,604.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.18/0.57 625[4:SpR:606.0,98.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c10)**. % 0.18/0.57 627[4:Rew:53.0,625.0] || -> equal(identity,sk_c10)**. % 0.18/0.57 629[4:Rew:627.0,52.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.57 630[4:Rew:627.0,328.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.57 636[4:Rew:629.0,579.0] || -> equal(sk_c11,sk_c10)**. % 0.18/0.57 645[4:Rew:636.0,545.0] || -> equal(inverse(sk_c6),sk_c10)**. % 0.18/0.57 647[4:Rew:636.0,587.0] || -> equal(inverse(sk_c10),sk_c1)**. % 0.18/0.57 649[4:Rew:636.0,550.0] || -> equal(multiply(sk_c6,sk_c10),sk_c10)**. % 0.18/0.57 653[4:Rew:636.0,596.1] || equal(multiply(sk_c1,u),sk_c1) equal(u,sk_c10) equal(multiply(sk_c1,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.57 670[4:Rew:630.0,649.0] || -> equal(sk_c6,sk_c10)**. % 0.18/0.57 671[4:Rew:670.0,645.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.18/0.57 672[4:Rew:647.0,671.0] || -> equal(sk_c10,sk_c1)**. % 0.18/0.57 675[4:Rew:672.0,629.0] || -> equal(multiply(sk_c1,u),u)**. % 0.18/0.57 676[4:Rew:672.0,636.0] || -> equal(sk_c11,sk_c1)**. % 0.18/0.57 679[4:Rew:672.0,630.0] || -> equal(multiply(u,sk_c1),u)**. % 0.18/0.57 724[4:Rew:679.0,653.2,672.0,653.2,675.0,653.2,676.0,653.2,672.0,653.1,675.0,653.0] || equal(u,sk_c1)* equal(u,sk_c1)* equal(u,sk_c1)* -> . % 0.18/0.57 725[4:Obv:724.1] || equal(u,sk_c1)* -> . % 0.18/0.57 726[4:UnC:725.0,584.0] || -> . % 0.18/0.57 728[3:Spt:726.0,9.1,59.0] || equal(inverse(sk_c1),sk_c11)** -> . % 0.18/0.57 729[3:Spt:726.0,9.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.57 730[3:MRR:7.1,728.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.18/0.57 731[3:MRR:4.1,728.0] || -> equal(inverse(sk_c6),sk_c11)**. % 0.18/0.57 732[3:MRR:2.1,728.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.57 733[3:MRR:10.0,728.0] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.57 735[3:MRR:6.0,728.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.57 736[3:MRR:5.0,728.0] || -> equal(multiply(sk_c6,sk_c10),sk_c11)**. % 0.18/0.57 737[3:MRR:3.0,728.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.18/0.57 738[3:MRR:1.0,728.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.18/0.57 749[3:SpR:732.0,98.0] || -> equal(multiply(sk_c5,multiply(sk_c4,u)),u)**. % 0.18/0.57 757[3:SpR:733.0,98.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c11)**. % 0.18/0.57 759[3:Rew:729.0,757.0] || -> equal(multiply(sk_c10,sk_c10),sk_c11)**. % 0.18/0.57 764[3:SpR:735.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.57 766[3:Rew:730.0,764.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.18/0.57 785[3:SpR:766.0,98.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c10)**. % 0.18/0.57 787[3:Rew:53.0,785.0] || -> equal(identity,sk_c10)**. % 0.18/0.57 789[3:Rew:787.0,52.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.57 790[3:Rew:787.0,328.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.57 796[3:Rew:789.0,759.0] || -> equal(sk_c11,sk_c10)**. % 0.18/0.57 804[3:Rew:796.0,568.0] || -> equal(inverse(sk_c10),sk_c2)**. % 0.18/0.57 806[3:Rew:796.0,731.0] || -> equal(inverse(sk_c6),sk_c10)**. % 0.18/0.57 810[3:Rew:796.0,736.0] || -> equal(multiply(sk_c6,sk_c10),sk_c10)**. % 0.18/0.57 811[3:Rew:796.0,737.0] || -> equal(multiply(sk_c5,sk_c10),sk_c10)**. % 0.18/0.57 812[3:Rew:796.0,738.0] || -> equal(multiply(sk_c4,sk_c5),sk_c10)**. % 0.18/0.57 816[3:Rew:796.0,571.1] || equal(multiply(sk_c2,u),sk_c2) equal(u,sk_c10) equal(multiply(sk_c2,multiply(u,sk_c10)),sk_c11)** -> . % 0.18/0.57 830[3:Rew:790.0,810.0] || -> equal(sk_c6,sk_c10)**. % 0.18/0.57 831[3:Rew:830.0,806.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.18/0.57 832[3:Rew:804.0,831.0] || -> equal(sk_c2,sk_c10)**. % 0.18/0.57 835[3:Rew:790.0,811.0] || -> equal(sk_c10,sk_c5)**. % 0.18/0.57 838[3:Rew:835.0,789.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.57 839[3:Rew:835.0,796.0] || -> equal(sk_c11,sk_c5)**. % 0.18/0.57 840[3:Rew:835.0,790.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.57 845[3:Rew:835.0,832.0] || -> equal(sk_c2,sk_c5)**. % 0.18/0.57 847[3:Rew:835.0,812.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.57 852[3:Rew:838.0,749.0] || -> equal(multiply(sk_c4,u),u)**. % 0.18/0.57 854[3:Rew:840.0,847.0] || -> equal(sk_c5,sk_c4)**. % 0.18/0.57 857[3:Rew:854.0,835.0] || -> equal(sk_c10,sk_c4)**. % 0.18/0.57 859[3:Rew:854.0,839.0] || -> equal(sk_c11,sk_c4)**. % 0.18/0.57 862[3:Rew:854.0,845.0] || -> equal(sk_c2,sk_c4)**. % 0.18/0.57 866[3:Rew:854.0,840.0] || -> equal(multiply(u,sk_c4),u)**. % 0.18/0.57 895[3:Rew:852.0,816.2,862.0,816.2,866.0,816.2,857.0,816.2,859.0,816.2,857.0,816.1,852.0,816.0,862.0,816.0] || equal(u,sk_c4)* equal(u,sk_c4)* equal(u,sk_c4)* -> . % 0.18/0.57 896[3:Obv:895.1] || equal(u,sk_c4)* -> . % 0.18/0.57 897[3:UnC:896.0,98.0] || -> . % 0.18/0.57 899[2:Spt:897.0,49.1,57.0] || equal(inverse(sk_c2),sk_c11)** -> . % 0.18/0.57 900[2:Spt:897.0,49.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.57 901[2:MRR:47.1,899.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.18/0.57 904[2:MRR:50.0,899.0] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.57 905[2:MRR:48.0,899.0] || -> equal(multiply(sk_c8,sk_c11),sk_c10)**. % 0.18/0.57 906[2:MRR:46.0,899.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.57 908[2:MRR:43.0,899.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.18/0.57 909[2:MRR:41.0,899.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.18/0.57 919[2:SpR:904.0,98.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c11)**. % 0.18/0.57 921[2:Rew:900.0,919.0] || -> equal(multiply(sk_c10,sk_c10),sk_c11)**. % 0.18/0.57 926[2:SpR:906.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.57 928[2:Rew:901.0,926.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.18/0.57 944[2:SpR:928.0,98.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c10)**. % 0.18/0.57 946[2:Rew:53.0,944.0] || -> equal(identity,sk_c10)**. % 0.18/0.57 947[2:Rew:946.0,52.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.57 948[2:Rew:946.0,328.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.57 950[2:Rew:946.0,75.0] || equal(inverse(sk_c10),u) equal(u,sk_c11) equal(multiply(u,sk_c10),sk_c11)** -> . % 0.18/0.57 953[2:Rew:947.0,921.0] || -> equal(sk_c11,sk_c10)**. % 0.18/0.57 964[2:Rew:953.0,905.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)**. % 0.18/0.57 966[2:Rew:953.0,908.0] || -> equal(multiply(sk_c5,sk_c10),sk_c10)**. % 0.18/0.57 967[2:Rew:953.0,909.0] || -> equal(multiply(sk_c4,sk_c5),sk_c10)**. % 0.18/0.57 977[2:Rew:948.0,964.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.57 978[2:Rew:977.0,901.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.18/0.57 979[2:Rew:977.0,906.0] || -> equal(multiply(sk_c7,sk_c10),sk_c10)**. % 0.18/0.57 983[2:Rew:948.0,966.0] || -> equal(sk_c10,sk_c5)**. % 0.18/0.57 987[2:Rew:983.0,953.0] || -> equal(sk_c11,sk_c5)**. % 0.18/0.57 988[2:Rew:983.0,948.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.57 991[2:Rew:983.0,978.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.57 994[2:Rew:983.0,967.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.57 997[2:Rew:983.0,979.0] || -> equal(multiply(sk_c7,sk_c5),sk_c5)**. % 0.18/0.57 999[2:Rew:988.0,997.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.57 1000[2:Rew:988.0,994.0] || -> equal(sk_c5,sk_c4)**. % 0.18/0.57 1001[2:Rew:999.0,991.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.57 1003[2:Rew:1000.0,983.0] || -> equal(sk_c10,sk_c4)**. % 0.18/0.57 1005[2:Rew:1000.0,987.0] || -> equal(sk_c11,sk_c4)**. % 0.18/0.57 1011[2:Rew:1000.0,988.0] || -> equal(multiply(u,sk_c4),u)**. % 0.18/0.57 1013[2:Rew:1000.0,1001.0] || -> equal(inverse(sk_c4),sk_c4)**. % 0.18/0.57 1030[2:Rew:1011.0,950.2,1003.0,950.2,1005.0,950.2,1005.0,950.1,1013.0,950.0,1003.0,950.0] || equal(sk_c4,u)* equal(u,sk_c4)* equal(u,sk_c4)* -> . % 0.18/0.57 1031[2:Obv:1030.1] || equal(u,sk_c4)* -> . % 0.18/0.57 1032[2:UnC:1031.0,98.0] || -> . % 0.18/0.57 1037[1:Spt:1032.0,55.0,55.2,55.3,55.4,55.5,55.7,55.8,55.9,55.11,55.12] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c11) equal(inverse(y),sk_c11) equal(multiply(u,v),sk_c10)**+ equal(multiply(x,sk_c11),z)* equal(multiply(w,sk_c11),sk_c10)** equal(multiply(v,sk_c11),sk_c10)** equal(multiply(y,sk_c10),sk_c11)** equal(multiply(sk_c11,z),sk_c10)** -> . % 0.18/0.57 1041[2:Spt:9.1] || -> equal(inverse(sk_c1),sk_c11)**. % 0.18/0.57 1042[2:SpR:1041.0,98.0] || -> equal(multiply(sk_c11,multiply(sk_c1,u)),u)**. % 0.18/0.57 1044[3:Spt:47.1] || -> equal(inverse(sk_c2),sk_c11)**. % 0.18/0.57 1047[4:Spt:37.1] || -> equal(multiply(sk_c2,sk_c11),sk_c3)**. % 0.18/0.57 1049[4:SpR:1047.0,98.0] || -> equal(multiply(inverse(sk_c2),sk_c3),sk_c11)**. % 0.18/0.57 1052[4:Rew:1044.0,1049.0] || -> equal(multiply(sk_c11,sk_c3),sk_c11)**. % 0.18/0.57 1053[4:Rew:1052.0,21.1] || -> equal(multiply(sk_c4,sk_c5),sk_c11)** equal(sk_c11,sk_c10). % 0.18/0.57 1055[4:Rew:1052.0,25.1] || -> equal(multiply(sk_c6,sk_c10),sk_c11)** equal(sk_c11,sk_c10). % 0.18/0.57 1058[4:Rew:1052.0,30.1] || -> equal(multiply(sk_c9,sk_c11),sk_c10)** equal(sk_c11,sk_c10). % 0.18/0.57 1059[4:Rew:1052.0,22.1] || -> equal(inverse(sk_c4),sk_c5)** equal(sk_c11,sk_c10). % 0.18/0.57 1060[4:Rew:1052.0,24.1] || -> equal(inverse(sk_c6),sk_c11)** equal(sk_c11,sk_c10). % 0.18/0.57 1062[4:Rew:1052.0,29.1] || -> equal(inverse(sk_c9),sk_c10)** equal(sk_c11,sk_c10). % 0.18/0.57 1066[4:Rew:1062.1,19.1] || -> equal(inverse(sk_c9),sk_c10) equal(multiply(sk_c1,sk_c10),sk_c10)**. % 0.18/0.57 1072[4:Rew:1058.1,20.1] || -> equal(multiply(sk_c9,sk_c11),sk_c10)** equal(multiply(sk_c1,sk_c10),sk_c10). % 0.18/0.57 1078[1:SpL:52.0,1037.4] || equal(inverse(identity),u) equal(inverse(v),sk_c10) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11) equal(u,sk_c10) equal(multiply(w,sk_c11),y)* equal(multiply(v,sk_c11),sk_c10)** equal(multiply(u,sk_c11),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c11,y),sk_c10)** -> . % 0.18/0.57 1080[4:SpR:1052.0,98.0] || -> equal(multiply(inverse(sk_c11),sk_c11),sk_c3)**. % 0.18/0.57 1083[4:Rew:53.0,1080.0] || -> equal(identity,sk_c3)**. % 0.18/0.57 1084[4:Rew:1083.0,52.0] || -> equal(multiply(sk_c3,u),u)**. % 0.18/0.57 1085[4:Rew:1083.0,328.0] || -> equal(multiply(u,sk_c3),u)**. % 0.18/0.57 1086[4:Rew:1083.0,53.0] || -> equal(multiply(inverse(u),u),sk_c3)**. % 0.18/0.57 1108[4:SpR:1086.0,98.0] || -> equal(multiply(inverse(inverse(u)),sk_c3),u)**. % 0.18/0.57 1109[4:SpR:1086.0,1085.0] || -> equal(inverse(sk_c3),sk_c3)**. % 0.18/0.57 1111[4:SpR:1041.0,1086.0] || -> equal(multiply(sk_c11,sk_c1),sk_c3)**. % 0.18/0.57 1113[4:SpL:1086.0,1037.4] || equal(inverse(inverse(u)),u) equal(inverse(v),sk_c10) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11) equal(sk_c3,sk_c10) equal(multiply(w,sk_c11),y)* equal(multiply(v,sk_c11),sk_c10)** equal(multiply(u,sk_c11),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c11,y),sk_c10)** -> . % 0.18/0.57 1116[4:Rew:1085.0,1108.0] || -> equal(inverse(inverse(u)),u)**. % 0.18/0.57 1120[4:Rew:1116.0,1113.0] || equal(u,u) equal(inverse(v),sk_c10) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11) equal(sk_c3,sk_c10) equal(multiply(w,sk_c11),y)* equal(multiply(v,sk_c11),sk_c10)** equal(multiply(u,sk_c11),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c11,y),sk_c10)** -> . % 0.18/0.57 1121[4:Obv:1120.0] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c11) equal(sk_c3,sk_c10) equal(multiply(v,sk_c11),x)* equal(multiply(u,sk_c11),sk_c10)** equal(multiply(y,sk_c11),sk_c10)** equal(multiply(w,sk_c10),sk_c11)** equal(multiply(sk_c11,x),sk_c10)** -> . % 0.18/0.57 1122[4:Con:1121.6] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c11) equal(sk_c3,sk_c10) equal(multiply(v,sk_c11),x)* equal(multiply(u,sk_c11),sk_c10)** equal(multiply(w,sk_c10),sk_c11)** equal(multiply(sk_c11,x),sk_c10)** -> . % 0.18/0.57 1128[4:SpR:1111.0,98.0] || -> equal(multiply(inverse(sk_c11),sk_c3),sk_c1)**. % 0.18/0.57 1131[4:Rew:1085.0,1128.0] || -> equal(inverse(sk_c11),sk_c1)**. % 0.18/0.57 1135[4:SpR:1131.0,1086.0] || -> equal(multiply(sk_c1,sk_c11),sk_c3)**. % 0.18/0.57 1149[5:Spt:1059.1] || -> equal(sk_c11,sk_c10)**. % 0.18/0.57 1151[5:Rew:1149.0,1041.0] || -> equal(inverse(sk_c1),sk_c10)**. % 0.18/0.57 1153[5:Rew:1149.0,1131.0] || -> equal(inverse(sk_c10),sk_c1)**. % 0.18/0.57 1159[5:Rew:1149.0,1122.4] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c11) equal(inverse(w),sk_c11) equal(sk_c3,sk_c10) equal(multiply(v,sk_c10),x)* equal(multiply(u,sk_c11),sk_c10)** equal(multiply(w,sk_c10),sk_c11)** equal(multiply(sk_c11,x),sk_c10)** -> . % 0.18/0.57 1166[5:Rew:1149.0,1072.0] || -> equal(multiply(sk_c9,sk_c10),sk_c10)** equal(multiply(sk_c1,sk_c10),sk_c10). % 0.18/0.57 1168[5:Rew:1149.0,1135.0] || -> equal(multiply(sk_c1,sk_c10),sk_c3)**. % 0.18/0.57 1170[5:Rew:1168.0,1066.1] || -> equal(inverse(sk_c9),sk_c10)** equal(sk_c3,sk_c10). % 0.18/0.57 1178[5:Rew:1168.0,1166.1] || -> equal(multiply(sk_c9,sk_c10),sk_c10)** equal(sk_c3,sk_c10). % 0.18/0.57 1179[5:Rew:1149.0,1159.7,1149.0,1159.6,1149.0,1159.5,1149.0,1159.2,1149.0,1159.1] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(sk_c3,sk_c10) equal(multiply(v,sk_c10),x)* equal(multiply(u,sk_c10),sk_c10)** equal(multiply(w,sk_c10),sk_c10)** equal(multiply(sk_c10,x),sk_c10)** -> . % 0.18/0.57 1180[5:Con:1179.2] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(sk_c3,sk_c10) equal(multiply(v,sk_c10),w)* equal(multiply(u,sk_c10),sk_c10)** equal(multiply(sk_c10,w),sk_c10)** -> . % 0.18/0.57 1208[6:Spt:1170.1] || -> equal(sk_c3,sk_c10)**. % 0.18/0.57 1210[6:Rew:1208.0,1084.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.57 1211[6:Rew:1208.0,1085.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.57 1213[6:Rew:1208.0,1109.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.18/0.57 1216[6:Rew:1208.0,1180.2] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(sk_c10,sk_c10) equal(multiply(v,sk_c10),w)* equal(multiply(u,sk_c10),sk_c10)** equal(multiply(sk_c10,w),sk_c10)** -> . % 0.18/0.57 1220[6:Rew:1153.0,1213.0] || -> equal(sk_c10,sk_c1)**. % 0.18/0.57 1222[6:Rew:1220.0,1151.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.18/0.57 1231[6:Rew:1220.0,1210.0] || -> equal(multiply(sk_c1,u),u)**. % 0.18/0.57 1232[6:Rew:1220.0,1211.0] || -> equal(multiply(u,sk_c1),u)**. % 0.18/0.57 1236[6:Obv:1216.2] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(multiply(v,sk_c10),w)* equal(multiply(u,sk_c10),sk_c10)** equal(multiply(sk_c10,w),sk_c10)** -> . % 0.18/0.57 1237[6:Rew:1231.0,1236.4,1220.0,1236.4,1232.0,1236.3,1220.0,1236.3,1232.0,1236.2,1220.0,1236.2,1220.0,1236.1,1220.0,1236.0] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(v,w)* equal(u,sk_c1) equal(w,sk_c1)* -> . % 0.18/0.57 1260[4:SpR:1116.0,98.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.18/0.57 1406[6:SpL:1222.0,1237.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(u,v)* equal(sk_c1,sk_c1) equal(v,sk_c1)* -> . % 0.18/0.57 1408[6:Obv:1406.3] || equal(inverse(u),sk_c1)**+ equal(u,v)* equal(v,sk_c1)* -> . % 0.18/0.57 1511[6:SpL:1222.0,1408.0] || equal(sk_c1,sk_c1)* equal(sk_c1,u)* equal(u,sk_c1)* -> . % 0.18/0.57 1515[6:Obv:1511.1] || equal(u,sk_c1)* -> . % 0.18/0.57 1516[6:AED:1515.0] || -> . % 0.18/0.57 1517[6:Spt:1516.0,1170.1,1208.0] || equal(sk_c3,sk_c10)** -> . % 0.18/0.57 1518[6:Spt:1516.0,1170.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.57 1527[6:MRR:1178.1,1517.0] || -> equal(multiply(sk_c9,sk_c10),sk_c10)**. % 0.18/0.57 1530[6:SpR:1518.0,1116.0] || -> equal(inverse(sk_c10),sk_c9)**. % 0.18/0.57 1533[6:Rew:1153.0,1530.0] || -> equal(sk_c9,sk_c1)**. % 0.18/0.57 1535[6:Rew:1533.0,1527.0] || -> equal(multiply(sk_c1,sk_c10),sk_c10)**. % 0.18/0.57 1536[6:Rew:1168.0,1535.0] || -> equal(sk_c3,sk_c10)**. % 0.18/0.57 1537[6:MRR:1536.0,1517.0] || -> . % 0.18/0.57 1540[5:Spt:1537.0,1059.1,1149.0] || equal(sk_c11,sk_c10)** -> . % 0.18/0.57 1541[5:Spt:1537.0,1059.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.57 1542[5:MRR:1060.1,1540.0] || -> equal(inverse(sk_c6),sk_c11)**. % 0.18/0.57 1545[5:MRR:1053.1,1540.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.18/0.57 1547[5:MRR:1055.1,1540.0] || -> equal(multiply(sk_c6,sk_c10),sk_c11)**. % 0.18/0.57 1553[5:SpR:1541.0,1260.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),u)**. % 0.18/0.57 1571[5:SpR:1542.0,1116.0] || -> equal(inverse(sk_c11),sk_c6)**. % 0.18/0.57 1574[5:Rew:1131.0,1571.0] || -> equal(sk_c6,sk_c1)**. % 0.18/0.57 1576[5:Rew:1574.0,1547.0] || -> equal(multiply(sk_c1,sk_c10),sk_c11)**. % 0.18/0.57 1592[5:SpR:1545.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c11,u))**. % 0.18/0.57 1596[5:Rew:1553.0,1592.0] || -> equal(multiply(sk_c11,u),u)**. % 0.18/0.57 1602[5:Rew:1596.0,1042.0] || -> equal(multiply(sk_c1,u),u)**. % 0.18/0.57 1603[5:Rew:1596.0,1111.0] || -> equal(sk_c3,sk_c1)**. % 0.18/0.57 1606[5:Rew:1603.0,1109.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.18/0.57 1611[5:Rew:1041.0,1606.0] || -> equal(sk_c11,sk_c1)**. % 0.18/0.57 1612[5:Rew:1611.0,1540.0] || equal(sk_c10,sk_c1)** -> . % 0.18/0.57 1619[5:Rew:1611.0,1576.0] || -> equal(multiply(sk_c1,sk_c10),sk_c1)**. % 0.18/0.57 1638[5:Rew:1602.0,1619.0] || -> equal(sk_c10,sk_c1)**. % 0.18/0.57 1639[5:MRR:1638.0,1612.0] || -> . % 0.18/0.57 1651[4:Spt:1639.0,37.1,1047.0] || equal(multiply(sk_c2,sk_c11),sk_c3)** -> . % 0.18/0.57 1652[4:Spt:1639.0,37.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.18/0.57 1654[4:MRR:32.1,1651.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.57 1655[4:MRR:39.1,1651.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.57 1657[4:MRR:40.1,1651.0] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.57 1658[4:MRR:38.1,1651.0] || -> equal(multiply(sk_c8,sk_c11),sk_c10)**. % 0.18/0.57 1659[4:MRR:36.1,1651.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.57 1661[4:MRR:33.1,1651.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.18/0.57 1662[4:MRR:31.1,1651.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.18/0.57 1672[4:SpR:1654.0,98.0] || -> equal(multiply(sk_c5,multiply(sk_c4,u)),u)**. % 0.18/0.57 1677[4:SpR:1657.0,98.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c11)**. % 0.18/0.57 1679[4:Rew:1655.0,1677.0] || -> equal(multiply(sk_c10,sk_c10),sk_c11)**. % 0.18/0.57 1684[4:SpR:1659.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.57 1686[4:Rew:1652.0,1684.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.18/0.57 1702[4:SpR:1686.0,98.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c10)**. % 0.18/0.57 1704[4:Rew:53.0,1702.0] || -> equal(identity,sk_c10)**. % 0.18/0.57 1705[4:Rew:1704.0,52.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.57 1706[4:Rew:1704.0,328.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.57 1708[4:Rew:1704.0,1078.0] || equal(inverse(sk_c10),u) equal(inverse(v),sk_c10) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11) equal(u,sk_c10) equal(multiply(w,sk_c11),y)* equal(multiply(v,sk_c11),sk_c10)** equal(multiply(u,sk_c11),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c11,y),sk_c10)** -> . % 0.18/0.57 1709[4:Rew:1704.0,53.0] || -> equal(multiply(inverse(u),u),sk_c10)**. % 0.18/0.57 1710[4:Rew:1705.0,1679.0] || -> equal(sk_c11,sk_c10)**. % 0.18/0.57 1718[4:Rew:1710.0,1041.0] || -> equal(inverse(sk_c1),sk_c10)**. % 0.18/0.57 1722[4:Rew:1710.0,1658.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)**. % 0.18/0.57 1724[4:Rew:1710.0,1661.0] || -> equal(multiply(sk_c5,sk_c10),sk_c10)**. % 0.18/0.57 1725[4:Rew:1710.0,1662.0] || -> equal(multiply(sk_c4,sk_c5),sk_c10)**. % 0.18/0.57 1739[4:Rew:1706.0,1722.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.57 1740[4:Rew:1739.0,1652.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.18/0.57 1741[4:Rew:1739.0,1659.0] || -> equal(multiply(sk_c7,sk_c10),sk_c10)**. % 0.18/0.57 1745[4:Rew:1706.0,1724.0] || -> equal(sk_c10,sk_c5)**. % 0.18/0.57 1748[4:Rew:1745.0,1705.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.57 1749[4:Rew:1745.0,1710.0] || -> equal(sk_c11,sk_c5)**. % 0.18/0.57 1750[4:Rew:1745.0,1718.0] || -> equal(inverse(sk_c1),sk_c5)**. % 0.18/0.57 1752[4:Rew:1745.0,1706.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.57 1754[4:Rew:1745.0,1740.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.57 1757[4:Rew:1745.0,1725.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.57 1760[4:Rew:1745.0,1741.0] || -> equal(multiply(sk_c7,sk_c5),sk_c5)**. % 0.18/0.57 1761[4:Rew:1748.0,1672.0] || -> equal(multiply(sk_c4,u),u)**. % 0.18/0.57 1762[4:Rew:1752.0,1760.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.57 1763[4:Rew:1752.0,1757.0] || -> equal(sk_c5,sk_c4)**. % 0.18/0.57 1764[4:Rew:1762.0,1754.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.57 1766[4:Rew:1763.0,1745.0] || -> equal(sk_c10,sk_c4)**. % 0.18/0.57 1768[4:Rew:1763.0,1749.0] || -> equal(sk_c11,sk_c4)**. % 0.18/0.57 1772[4:Rew:1763.0,1750.0] || -> equal(inverse(sk_c1),sk_c4)**. % 0.18/0.57 1776[4:Rew:1763.0,1752.0] || -> equal(multiply(u,sk_c4),u)**. % 0.18/0.57 1778[4:Rew:1763.0,1764.0] || -> equal(inverse(sk_c4),sk_c4)**. % 0.18/0.57 1780[4:Rew:1766.0,1709.0] || -> equal(multiply(inverse(u),u),sk_c4)**. % 0.18/0.57 1797[4:Rew:1761.0,1708.9,1768.0,1708.9,1766.0,1708.9,1776.0,1708.8,1766.0,1708.8,1768.0,1708.8,1776.0,1708.7,1768.0,1708.7,1766.0,1708.7,1776.0,1708.6,1768.0,1708.6,1766.0,1708.6,1776.0,1708.5,1768.0,1708.5,1766.0,1708.4,1768.0,1708.3,1768.0,1708.2,1766.0,1708.1,1778.0,1708.0,1766.0,1708.0] || equal(sk_c4,u)* equal(inverse(v),sk_c4)** equal(inverse(w),sk_c4)** equal(inverse(x),sk_c4)** equal(u,sk_c4)* equal(w,y)* equal(v,sk_c4) equal(u,sk_c4)* equal(x,sk_c4) equal(y,sk_c4)* -> . % 0.18/0.57 1798[4:Obv:1797.4] || equal(inverse(u),sk_c4)** equal(inverse(v),sk_c4)** equal(inverse(w),sk_c4)** equal(v,x)* equal(u,sk_c4) equal(y,sk_c4)* equal(w,sk_c4) equal(x,sk_c4)* -> . % 0.18/0.57 1799[4:Con:1798.2] || equal(inverse(u),sk_c4)** equal(inverse(v),sk_c4)** equal(v,w)* equal(u,sk_c4) equal(w,sk_c4)* -> . % 0.18/0.57 1849[4:SpR:1772.0,1780.0] || -> equal(multiply(sk_c4,sk_c1),sk_c4)**. % 0.18/0.57 1851[4:Rew:1761.0,1849.0] || -> equal(sk_c4,sk_c1)**. % 0.18/0.57 1859[4:Rew:1851.0,1778.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.18/0.57 1866[4:Rew:1851.0,1799.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c4)** equal(v,w)* equal(u,sk_c4) equal(w,sk_c4)* -> . % 0.18/0.57 1874[4:Rew:1851.0,1866.4,1851.0,1866.3,1851.0,1866.1] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(v,w)* equal(u,sk_c1) equal(w,sk_c1)* -> . % 0.18/0.57 2146[4:SpL:1859.0,1874.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(u,v)* equal(sk_c1,sk_c1) equal(v,sk_c1)* -> . % 0.18/0.57 2149[4:Obv:2146.3] || equal(inverse(u),sk_c1)**+ equal(u,v)* equal(v,sk_c1)* -> . % 0.18/0.57 2194[4:SpL:1859.0,2149.0] || equal(sk_c1,sk_c1)* equal(sk_c1,u)* equal(u,sk_c1)* -> . % 0.18/0.57 2198[4:Obv:2194.1] || equal(u,sk_c1)* -> . % 0.18/0.57 2199[4:AED:2198.0] || -> . % 0.18/0.57 2200[3:Spt:2199.0,47.1,1044.0] || equal(inverse(sk_c2),sk_c11)** -> . % 0.18/0.57 2201[3:Spt:2199.0,47.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.18/0.57 2203[3:MRR:42.1,2200.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.57 2204[3:MRR:49.1,2200.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.57 2206[3:MRR:50.0,2200.0] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.57 2207[3:MRR:48.0,2200.0] || -> equal(multiply(sk_c8,sk_c11),sk_c10)**. % 0.18/0.57 2208[3:MRR:46.0,2200.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.57 2210[3:MRR:43.0,2200.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.18/0.57 2211[3:MRR:41.0,2200.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.18/0.57 2226[3:SpR:2203.0,98.0] || -> equal(multiply(sk_c5,multiply(sk_c4,u)),u)**. % 0.18/0.57 2231[3:SpR:2206.0,98.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c11)**. % 0.18/0.57 2233[3:Rew:2204.0,2231.0] || -> equal(multiply(sk_c10,sk_c10),sk_c11)**. % 0.18/0.57 2238[3:SpR:2208.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.57 2240[3:Rew:2201.0,2238.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.18/0.57 2259[3:SpR:2240.0,98.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c10)**. % 0.18/0.57 2261[3:Rew:53.0,2259.0] || -> equal(identity,sk_c10)**. % 0.18/0.57 2262[3:Rew:2261.0,52.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.57 2263[3:Rew:2261.0,328.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.57 2264[3:Rew:2261.0,53.0] || -> equal(multiply(inverse(u),u),sk_c10)**. % 0.18/0.57 2266[3:Rew:2261.0,1078.0] || equal(inverse(sk_c10),u) equal(inverse(v),sk_c10) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11) equal(u,sk_c10) equal(multiply(w,sk_c11),y)* equal(multiply(v,sk_c11),sk_c10)** equal(multiply(u,sk_c11),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c11,y),sk_c10)** -> . % 0.18/0.57 2267[3:Rew:2262.0,2233.0] || -> equal(sk_c11,sk_c10)**. % 0.18/0.57 2275[3:Rew:2267.0,1041.0] || -> equal(inverse(sk_c1),sk_c10)**. % 0.18/0.57 2279[3:Rew:2267.0,2207.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)**. % 0.18/0.57 2281[3:Rew:2267.0,2210.0] || -> equal(multiply(sk_c5,sk_c10),sk_c10)**. % 0.18/0.57 2282[3:Rew:2267.0,2211.0] || -> equal(multiply(sk_c4,sk_c5),sk_c10)**. % 0.18/0.57 2294[3:Rew:2263.0,2279.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.57 2295[3:Rew:2294.0,2201.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.18/0.57 2296[3:Rew:2294.0,2208.0] || -> equal(multiply(sk_c7,sk_c10),sk_c10)**. % 0.18/0.57 2300[3:Rew:2263.0,2281.0] || -> equal(sk_c10,sk_c5)**. % 0.18/0.57 2303[3:Rew:2300.0,2262.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.57 2304[3:Rew:2300.0,2267.0] || -> equal(sk_c11,sk_c5)**. % 0.18/0.57 2305[3:Rew:2300.0,2275.0] || -> equal(inverse(sk_c1),sk_c5)**. % 0.18/0.57 2306[3:Rew:2300.0,2263.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.57 2309[3:Rew:2300.0,2295.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.57 2312[3:Rew:2300.0,2282.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.57 2315[3:Rew:2300.0,2296.0] || -> equal(multiply(sk_c7,sk_c5),sk_c5)**. % 0.18/0.57 2316[3:Rew:2303.0,2226.0] || -> equal(multiply(sk_c4,u),u)**. % 0.18/0.57 2317[3:Rew:2306.0,2315.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.57 2318[3:Rew:2306.0,2312.0] || -> equal(sk_c5,sk_c4)**. % 0.18/0.57 2319[3:Rew:2317.0,2309.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.57 2321[3:Rew:2318.0,2300.0] || -> equal(sk_c10,sk_c4)**. % 0.18/0.57 2323[3:Rew:2318.0,2304.0] || -> equal(sk_c11,sk_c4)**. % 0.18/0.57 2327[3:Rew:2318.0,2305.0] || -> equal(inverse(sk_c1),sk_c4)**. % 0.18/0.57 2330[3:Rew:2318.0,2306.0] || -> equal(multiply(u,sk_c4),u)**. % 0.18/0.57 2332[3:Rew:2318.0,2319.0] || -> equal(inverse(sk_c4),sk_c4)**. % 0.18/0.57 2334[3:Rew:2321.0,2264.0] || -> equal(multiply(inverse(u),u),sk_c4)**. % 0.18/0.57 2350[3:Rew:2316.0,2266.9,2323.0,2266.9,2321.0,2266.9,2330.0,2266.8,2321.0,2266.8,2323.0,2266.8,2330.0,2266.7,2323.0,2266.7,2321.0,2266.7,2330.0,2266.6,2323.0,2266.6,2321.0,2266.6,2330.0,2266.5,2323.0,2266.5,2321.0,2266.4,2323.0,2266.3,2323.0,2266.2,2321.0,2266.1,2332.0,2266.0,2321.0,2266.0] || equal(sk_c4,u)* equal(inverse(v),sk_c4)** equal(inverse(w),sk_c4)** equal(inverse(x),sk_c4)** equal(u,sk_c4)* equal(w,y)* equal(v,sk_c4) equal(u,sk_c4)* equal(x,sk_c4) equal(y,sk_c4)* -> . % 0.18/0.57 2351[3:Obv:2350.4] || equal(inverse(u),sk_c4)** equal(inverse(v),sk_c4)** equal(inverse(w),sk_c4)** equal(v,x)* equal(u,sk_c4) equal(y,sk_c4)* equal(w,sk_c4) equal(x,sk_c4)* -> . % 0.18/0.57 2352[3:Con:2351.2] || equal(inverse(u),sk_c4)** equal(inverse(v),sk_c4)** equal(v,w)* equal(u,sk_c4) equal(w,sk_c4)* -> . % 0.18/0.57 2388[3:SpR:2327.0,2334.0] || -> equal(multiply(sk_c4,sk_c1),sk_c4)**. % 0.18/0.57 2392[3:Rew:2316.0,2388.0] || -> equal(sk_c4,sk_c1)**. % 0.18/0.57 2400[3:Rew:2392.0,2332.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.18/0.57 2406[3:Rew:2392.0,2352.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c4)** equal(v,w)* equal(u,sk_c4) equal(w,sk_c4)* -> . % 0.18/0.57 2412[3:Rew:2392.0,2406.4,2392.0,2406.3,2392.0,2406.1] || equal(inverse(u),sk_c1)**+ equal(inverse(v),sk_c1)** equal(v,w)* equal(u,sk_c1) equal(w,sk_c1)* -> . % 0.18/0.57 2735[3:SpL:2400.0,2412.0] || equal(sk_c1,sk_c1) equal(inverse(u),sk_c1)** equal(u,v)* equal(sk_c1,sk_c1) equal(v,sk_c1)* -> . % 0.18/0.57 2739[3:Obv:2735.3] || equal(inverse(u),sk_c1)**+ equal(u,v)* equal(v,sk_c1)* -> . % 0.18/0.57 2740[3:SpL:2400.0,2739.0] || equal(sk_c1,sk_c1)* equal(sk_c1,u)* equal(u,sk_c1)* -> . % 0.18/0.57 2744[3:Obv:2740.1] || equal(u,sk_c1)* -> . % 0.18/0.57 2745[3:AED:2744.0] || -> . % 0.18/0.57 2746[2:Spt:2745.0,9.1,1041.0] || equal(inverse(sk_c1),sk_c11)** -> . % 0.18/0.57 2747[2:Spt:2745.0,9.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.57 2748[2:MRR:7.1,2746.0] || -> equal(inverse(sk_c7),sk_c8)**. % 0.18/0.57 2750[2:MRR:2.1,2746.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.57 2752[2:MRR:10.0,2746.0] || -> equal(multiply(sk_c9,sk_c11),sk_c10)**. % 0.18/0.57 2753[2:MRR:8.0,2746.0] || -> equal(multiply(sk_c8,sk_c11),sk_c10)**. % 0.18/0.57 2754[2:MRR:6.0,2746.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.57 2756[2:MRR:3.0,2746.0] || -> equal(multiply(sk_c5,sk_c10),sk_c11)**. % 0.18/0.57 2757[2:MRR:1.0,2746.0] || -> equal(multiply(sk_c4,sk_c5),sk_c11)**. % 0.18/0.57 2772[2:SpR:2750.0,98.0] || -> equal(multiply(sk_c5,multiply(sk_c4,u)),u)**. % 0.18/0.57 2775[2:SpR:2752.0,98.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c11)**. % 0.18/0.57 2777[2:Rew:2747.0,2775.0] || -> equal(multiply(sk_c10,sk_c10),sk_c11)**. % 0.18/0.57 2782[2:SpR:2754.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.57 2784[2:Rew:2748.0,2782.0] || -> equal(multiply(sk_c8,sk_c10),sk_c8)**. % 0.18/0.57 2800[2:SpR:2784.0,98.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c10)**. % 0.18/0.57 2802[2:Rew:53.0,2800.0] || -> equal(identity,sk_c10)**. % 0.18/0.57 2803[2:Rew:2802.0,52.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.57 2804[2:Rew:2802.0,328.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.57 2806[2:Rew:2802.0,1078.0] || equal(inverse(sk_c10),u) equal(inverse(v),sk_c10) equal(inverse(w),sk_c11) equal(inverse(x),sk_c11) equal(u,sk_c10) equal(multiply(w,sk_c11),y)* equal(multiply(v,sk_c11),sk_c10)** equal(multiply(u,sk_c11),sk_c10)** equal(multiply(x,sk_c10),sk_c11)** equal(multiply(sk_c11,y),sk_c10)** -> . % 0.18/0.57 2808[2:Rew:2803.0,2777.0] || -> equal(sk_c11,sk_c10)**. % 0.18/0.57 2819[2:Rew:2808.0,2753.0] || -> equal(multiply(sk_c8,sk_c10),sk_c10)**. % 0.18/0.57 2821[2:Rew:2808.0,2756.0] || -> equal(multiply(sk_c5,sk_c10),sk_c10)**. % 0.18/0.57 2822[2:Rew:2808.0,2757.0] || -> equal(multiply(sk_c4,sk_c5),sk_c10)**. % 0.18/0.57 2833[2:Rew:2804.0,2819.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.57 2834[2:Rew:2833.0,2748.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.18/0.57 2835[2:Rew:2833.0,2754.0] || -> equal(multiply(sk_c7,sk_c10),sk_c10)**. % 0.18/0.57 2839[2:Rew:2804.0,2821.0] || -> equal(sk_c10,sk_c5)**. % 0.18/0.57 2842[2:Rew:2839.0,2803.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.57 2843[2:Rew:2839.0,2808.0] || -> equal(sk_c11,sk_c5)**. % 0.18/0.57 2844[2:Rew:2839.0,2804.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.57 2847[2:Rew:2839.0,2834.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.57 2850[2:Rew:2839.0,2822.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.57 2853[2:Rew:2839.0,2835.0] || -> equal(multiply(sk_c7,sk_c5),sk_c5)**. % 0.18/0.57 2854[2:Rew:2842.0,2772.0] || -> equal(multiply(sk_c4,u),u)**. % 0.18/0.57 2855[2:Rew:2844.0,2853.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.57 2856[2:Rew:2844.0,2850.0] || -> equal(sk_c5,sk_c4)**. % 0.18/0.57 2857[2:Rew:2855.0,2847.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.57 2859[2:Rew:2856.0,2839.0] || -> equal(sk_c10,sk_c4)**. % 0.18/0.57 2861[2:Rew:2856.0,2843.0] || -> equal(sk_c11,sk_c4)**. % 0.18/0.57 2867[2:Rew:2856.0,2844.0] || -> equal(multiply(u,sk_c4),u)**. % 0.18/0.57 2869[2:Rew:2856.0,2857.0] || -> equal(inverse(sk_c4),sk_c4)**. % 0.18/0.57 2886[2:Rew:2854.0,2806.9,2861.0,2806.9,2859.0,2806.9,2867.0,2806.8,2859.0,2806.8,2861.0,2806.8,2867.0,2806.7,2861.0,2806.7,2859.0,2806.7,2867.0,2806.6,2861.0,2806.6,2859.0,2806.6,2867.0,2806.5,2861.0,2806.5,2859.0,2806.4,2861.0,2806.3,2861.0,2806.2,2859.0,2806.1,2869.0,2806.0,2859.0,2806.0] || equal(sk_c4,u)* equal(inverse(v),sk_c4)** equal(inverse(w),sk_c4)** equal(inverse(x),sk_c4)** equal(u,sk_c4)* equal(w,y)* equal(v,sk_c4) equal(u,sk_c4)* equal(x,sk_c4) equal(y,sk_c4)* -> . % 0.18/0.57 2887[2:Obv:2886.4] || equal(inverse(u),sk_c4)** equal(inverse(v),sk_c4)** equal(inverse(w),sk_c4)** equal(v,x)* equal(u,sk_c4) equal(y,sk_c4)* equal(w,sk_c4) equal(x,sk_c4)* -> . % 0.18/0.57 2888[2:Con:2887.2] || equal(inverse(u),sk_c4)**+ equal(inverse(v),sk_c4)** equal(v,w)* equal(u,sk_c4) equal(w,sk_c4)* -> . % 0.18/0.57 3054[2:SpL:2869.0,2888.0] || equal(sk_c4,sk_c4) equal(inverse(u),sk_c4)** equal(u,v)* equal(sk_c4,sk_c4) equal(v,sk_c4)* -> . % 0.18/0.57 3056[2:Obv:3054.3] || equal(inverse(u),sk_c4)**+ equal(u,v)* equal(v,sk_c4)* -> . % 0.18/0.57 3186[2:SpL:2869.0,3056.0] || equal(sk_c4,sk_c4)* equal(sk_c4,u)* equal(u,sk_c4)* -> . % 0.18/0.57 3190[2:Obv:3186.1] || equal(u,sk_c4)* -> . % 0.18/0.57 3191[2:AED:3190.0] || -> . % 0.18/0.57 % SZS output end Refutation % 0.18/0.57 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_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_29 prove_this_30 prove_this_31 prove_this_32 prove_this_33 prove_this_34 prove_this_35 prove_this_36 prove_this_37 prove_this_38 prove_this_39 prove_this_40 prove_this_41 prove_this_42 prove_this_43 prove_this_46 prove_this_47 prove_this_48 prove_this_49 prove_this_50 prove_this_51 left_identity left_inverse associativity % 0.18/0.57 %------------------------------------------------------------------------------