%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP308-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n023.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:47 EDT 2022 % Result : Unsatisfiable 0.19s 0.49s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP308-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n023.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 : Tue Jun 14 08:12:35 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.49 % 0.19/0.49 SPASS V 3.9 % 0.19/0.49 SPASS beiseite: Proof found. % 0.19/0.49 % SZS status Theorem % 0.19/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.49 SPASS derived 899 clauses, backtracked 512 clauses, performed 13 splits and kept 854 clauses. % 0.19/0.49 SPASS allocated 63695 KBytes. % 0.19/0.49 SPASS spent 0:00:00.14 on the problem. % 0.19/0.49 0:00:00.04 for the input. % 0.19/0.49 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.49 0:00:00.00 for inferences. % 0.19/0.49 0:00:00.00 for the backtracking. % 0.19/0.49 0:00:00.07 for the reduction. % 0.19/0.49 % 0.19/0.49 % 0.19/0.49 Here is a proof with depth 5, length 410 : % 0.19/0.49 % SZS output start Refutation % 0.19/0.49 1[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6). % 0.19/0.49 2[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.49 3[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c6)** equal(multiply(sk_c8,sk_c7),sk_c6). % 0.19/0.49 4[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.49 5[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.49 6[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6)** equal(multiply(sk_c8,sk_c7),sk_c6). % 0.19/0.49 7[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.19/0.49 8[0:Inp] || -> equal(inverse(sk_c3),sk_c8)** equal(inverse(sk_c8),sk_c6). % 0.19/0.49 9[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.19/0.49 10[0:Inp] || -> equal(inverse(sk_c4),sk_c7)** equal(inverse(sk_c8),sk_c6). % 0.19/0.49 11[0:Inp] || -> equal(inverse(sk_c5),sk_c6)** equal(inverse(sk_c8),sk_c6). % 0.19/0.49 12[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.49 13[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c8). % 0.19/0.49 14[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.19/0.49 15[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c8). % 0.19/0.49 16[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.19/0.49 17[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.19/0.49 18[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c8). % 0.19/0.49 19[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c8,sk_c2),sk_c7). % 0.19/0.49 20[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.19/0.49 21[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c6)** equal(multiply(sk_c8,sk_c2),sk_c7). % 0.19/0.49 22[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.19/0.49 23[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.19/0.49 26[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 27[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c6) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 28[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 29[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 30[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 32[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c1),sk_c8)**. % 0.19/0.49 33[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.19/0.49 34[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(inverse(sk_c1),sk_c8)**. % 0.19/0.49 35[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(inverse(sk_c1),sk_c8)**. % 0.19/0.49 36[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.49 37[0:Inp] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(inverse(x),sk_c8) equal(inverse(sk_c8),sk_c6) equal(multiply(x,sk_c8),y)*+ equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c8,y),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6) -> . % 0.19/0.49 38[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.49 39[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.49 40[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.49 41[1:Spt:37.3,37.5,37.9] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),v)* equal(multiply(sk_c8,v),sk_c7)** -> . % 0.19/0.49 43[2:Spt:10.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.49 45[3:Spt:11.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.19/0.49 47[4:Spt:8.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.49 49[5:Spt:9.1] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.19/0.49 52[1:SpL:38.0,41.1] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.19/0.49 53[6:Spt:7.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.19/0.49 58[7:Spt:12.1] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.49 63[2:SpR:43.0,39.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.19/0.49 64[3:SpR:45.0,39.0] || -> equal(multiply(sk_c6,sk_c5),identity)**. % 0.19/0.49 65[4:SpR:47.0,39.0] || -> equal(multiply(sk_c8,sk_c3),identity)**. % 0.19/0.49 66[1:SpL:39.0,41.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.19/0.49 75[0:SpR:39.0,40.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.49 76[2:SpR:63.0,40.0] || -> equal(multiply(sk_c7,multiply(sk_c4,u)),multiply(identity,u))**. % 0.19/0.49 77[3:SpR:64.0,40.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),multiply(identity,u))**. % 0.19/0.49 79[2:Rew:38.0,76.0] || -> equal(multiply(sk_c7,multiply(sk_c4,u)),u)**. % 0.19/0.49 80[3:Rew:38.0,77.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),u)**. % 0.19/0.49 81[0:Rew:38.0,75.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.49 88[5:SpR:49.0,79.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.19/0.49 94[7:SpR:58.0,80.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.19/0.49 97[0:SpR:81.0,81.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.49 99[6:SpR:53.0,81.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c8)**. % 0.19/0.49 101[4:SpR:65.0,81.0] || -> equal(multiply(inverse(sk_c8),identity),sk_c3)**. % 0.19/0.49 104[0:SpR:39.0,81.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.49 105[2:SpR:63.0,81.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c4)**. % 0.19/0.49 107[5:SpR:88.0,81.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.19/0.49 108[3:SpR:64.0,81.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c5)**. % 0.19/0.49 114[6:Rew:47.0,99.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.19/0.49 117[5:Rew:39.0,107.0] || -> equal(identity,sk_c6)**. % 0.19/0.49 118[5:Rew:117.0,38.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.49 121[5:Rew:117.0,64.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.19/0.49 122[5:Rew:117.0,65.0] || -> equal(multiply(sk_c8,sk_c3),sk_c6)**. % 0.19/0.49 125[5:Rew:117.0,66.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(sk_c6,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.19/0.49 126[5:Rew:117.0,101.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c3)**. % 0.19/0.49 129[7:Rew:118.0,94.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 139[7:Rew:129.0,118.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 142[7:Rew:129.0,122.0] || -> equal(multiply(sk_c8,sk_c3),sk_c8)**. % 0.19/0.49 145[7:Rew:139.0,142.0] || -> equal(sk_c3,sk_c8)**. % 0.19/0.49 147[7:Rew:139.0,114.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 152[7:Rew:145.0,47.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 194[7:Rew:139.0,125.2,147.0,125.2,129.0,125.1,152.0,125.0,152.0,125.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.19/0.49 195[7:Obv:194.1] || equal(u,sk_c8)* -> . % 0.19/0.49 196[7:UnC:195.0,81.0] || -> . % 0.19/0.49 198[7:Spt:196.0,12.1,58.0] || equal(multiply(sk_c5,sk_c8),sk_c6)** -> . % 0.19/0.49 199[7:Spt:196.0,12.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.19/0.49 200[5:Rew:118.0,121.0] || -> equal(sk_c5,sk_c6)**. % 0.19/0.49 201[5:Rew:200.0,45.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.19/0.49 205[7:Rew:118.0,126.0,199.0,126.0] || -> equal(sk_c3,sk_c6)**. % 0.19/0.49 206[7:Rew:205.0,47.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.19/0.49 207[7:Rew:205.0,122.0] || -> equal(multiply(sk_c8,sk_c6),sk_c6)**. % 0.19/0.49 208[7:Rew:205.0,53.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.19/0.49 209[7:Rew:201.0,206.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 211[7:Rew:209.0,199.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 214[7:Rew:209.0,118.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 220[7:Rew:209.0,207.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.19/0.49 221[7:Rew:220.0,208.0,209.0,208.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 254[7:Rew:214.0,125.2,221.0,125.2,209.0,125.1,211.0,125.0,211.0,125.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.19/0.49 255[7:Obv:254.1] || equal(u,sk_c8)* -> . % 0.19/0.49 256[7:UnC:255.0,81.0] || -> . % 0.19/0.49 259[6:Spt:256.0,7.1,53.0] || equal(multiply(sk_c3,sk_c8),sk_c7)** -> . % 0.19/0.49 260[6:Spt:256.0,7.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.19/0.49 261[6:Rew:118.0,126.0,260.0,126.0] || -> equal(sk_c3,sk_c6)**. % 0.19/0.49 262[6:Rew:261.0,47.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.19/0.49 264[6:Rew:201.0,262.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 266[6:Rew:264.0,117.0] || -> equal(identity,sk_c8)**. % 0.19/0.49 270[6:Rew:264.0,118.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 273[6:Rew:264.0,261.0] || -> equal(sk_c3,sk_c8)**. % 0.19/0.49 277[6:Rew:270.0,259.0,273.0,259.0] || equal(sk_c7,sk_c8)** -> . % 0.19/0.49 279[6:Rew:97.0,104.0,266.0,104.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.49 318[6:Rew:270.0,1.1,264.0,1.1,273.0,1.0,279.0,1.0] || -> equal(sk_c7,sk_c8)** equal(sk_c7,sk_c8)**. % 0.19/0.49 319[6:Obv:318.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 320[6:MRR:319.0,277.0] || -> . % 0.19/0.49 328[5:Spt:320.0,9.1,49.0] || equal(multiply(sk_c4,sk_c7),sk_c6)** -> . % 0.19/0.49 329[5:Spt:320.0,9.0] || -> equal(inverse(sk_c8),sk_c6)**. % 0.19/0.49 330[5:Rew:329.0,101.0] || -> equal(multiply(sk_c6,identity),sk_c3)**. % 0.19/0.49 331[0:Rew:97.0,104.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.49 332[5:Rew:331.0,330.0] || -> equal(sk_c3,sk_c6)**. % 0.19/0.49 333[3:Rew:331.0,108.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.19/0.49 334[2:Rew:331.0,105.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.19/0.49 335[5:Rew:332.0,47.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.19/0.49 336[5:Rew:332.0,65.0] || -> equal(multiply(sk_c8,sk_c6),identity)**. % 0.19/0.49 338[5:Rew:333.0,335.0] || -> equal(sk_c5,sk_c8)**. % 0.19/0.49 340[5:Rew:338.0,64.0] || -> equal(multiply(sk_c6,sk_c8),identity)**. % 0.19/0.49 349[5:MRR:33.1,328.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.49 358[5:MRR:27.0,328.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 359[5:MRR:21.0,328.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.19/0.49 360[5:MRR:15.0,328.0] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.19/0.49 392[5:SpR:358.0,81.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c8)**. % 0.19/0.49 394[5:Rew:349.0,392.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.19/0.49 395[5:Rew:359.0,394.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 402[5:Rew:395.0,360.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.19/0.49 406[5:Rew:395.0,52.2] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.19/0.49 413[5:Rew:340.0,402.0] || -> equal(identity,sk_c8)**. % 0.19/0.49 414[5:Rew:413.0,336.0] || -> equal(multiply(sk_c8,sk_c6),sk_c8)**. % 0.19/0.49 416[5:Rew:413.0,38.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 420[5:Rew:416.0,414.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 426[5:Rew:420.0,329.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 444[5:Rew:416.0,406.2,426.0,406.0,413.0,406.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.19/0.49 445[5:Obv:444.1] || equal(u,sk_c8)* -> . % 0.19/0.49 446[5:UnC:445.0,349.0] || -> . % 0.19/0.49 449[4:Spt:446.0,8.0,47.0] || equal(inverse(sk_c3),sk_c8)** -> . % 0.19/0.49 450[4:Spt:446.0,8.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.19/0.49 452[4:MRR:32.0,449.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.49 453[4:MRR:26.0,449.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 454[4:MRR:20.0,449.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.19/0.49 455[4:MRR:14.0,449.0] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.19/0.49 456[4:MRR:2.0,449.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.49 481[4:SpR:453.0,81.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c8)**. % 0.19/0.49 483[4:Rew:452.0,481.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.19/0.49 484[4:Rew:454.0,483.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 485[4:Rew:484.0,334.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.19/0.49 486[4:Rew:484.0,43.0] || -> equal(inverse(sk_c4),sk_c8)**. % 0.19/0.49 491[4:Rew:484.0,455.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.19/0.49 492[4:Rew:484.0,456.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.19/0.49 495[4:Rew:484.0,52.2] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.19/0.49 498[4:Rew:450.0,485.0] || -> equal(sk_c4,sk_c6)**. % 0.19/0.49 499[4:Rew:498.0,486.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.19/0.49 500[4:Rew:333.0,499.0] || -> equal(sk_c5,sk_c8)**. % 0.19/0.49 503[4:Rew:500.0,64.0] || -> equal(multiply(sk_c6,sk_c8),identity)**. % 0.19/0.49 507[4:Rew:491.0,503.0] || -> equal(identity,sk_c8)**. % 0.19/0.49 508[4:Rew:507.0,331.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.49 509[4:Rew:507.0,38.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 514[4:Rew:508.0,492.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 518[4:Rew:514.0,450.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 538[4:Rew:509.0,495.2,518.0,495.0,507.0,495.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.19/0.49 539[4:Obv:538.1] || equal(u,sk_c8)* -> . % 0.19/0.49 540[4:UnC:539.0,81.0] || -> . % 0.19/0.49 543[3:Spt:540.0,11.0,45.0] || equal(inverse(sk_c5),sk_c6)** -> . % 0.19/0.49 544[3:Spt:540.0,11.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.19/0.49 545[3:MRR:35.0,543.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.49 546[3:MRR:29.0,543.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 547[3:MRR:23.0,543.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.19/0.49 548[3:MRR:17.0,543.0] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.19/0.49 549[3:MRR:5.0,543.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.49 565[3:SpR:546.0,81.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c8)**. % 0.19/0.49 567[3:Rew:545.0,565.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.19/0.49 568[3:Rew:547.0,567.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 570[3:Rew:568.0,334.0] || -> equal(inverse(sk_c8),sk_c4)**. % 0.19/0.49 571[3:Rew:568.0,63.0] || -> equal(multiply(sk_c8,sk_c4),identity)**. % 0.19/0.49 574[3:Rew:568.0,547.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.19/0.49 575[3:Rew:568.0,548.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.19/0.49 576[3:Rew:568.0,549.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.19/0.49 579[3:Rew:568.0,52.2] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.19/0.49 582[3:Rew:544.0,570.0] || -> equal(sk_c4,sk_c6)**. % 0.19/0.49 584[3:Rew:582.0,571.0] || -> equal(multiply(sk_c8,sk_c6),identity)**. % 0.19/0.49 599[3:SpR:574.0,81.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c2)**. % 0.19/0.49 601[3:Rew:544.0,599.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.19/0.49 602[3:Rew:575.0,601.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.49 604[3:Rew:602.0,574.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.19/0.49 606[3:Rew:576.0,604.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 607[3:Rew:606.0,544.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 611[3:Rew:606.0,584.0] || -> equal(multiply(sk_c8,sk_c8),identity)**. % 0.19/0.49 613[3:Rew:606.0,575.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.19/0.49 616[3:Rew:611.0,613.0] || -> equal(identity,sk_c8)**. % 0.19/0.49 617[3:Rew:616.0,38.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 621[3:Rew:616.0,579.0] || equal(inverse(sk_c8),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.19/0.49 640[3:Rew:617.0,621.2,607.0,621.0] || equal(sk_c8,sk_c8)* equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.19/0.49 641[3:Obv:640.1] || equal(u,sk_c8)* -> . % 0.19/0.49 642[3:UnC:641.0,568.0] || -> . % 0.19/0.49 645[2:Spt:642.0,10.0,43.0] || equal(inverse(sk_c4),sk_c7)** -> . % 0.19/0.49 646[2:Spt:642.0,10.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.19/0.49 647[2:MRR:34.0,645.0] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.49 648[2:MRR:28.0,645.0] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 649[2:MRR:22.0,645.0] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.19/0.49 650[2:MRR:16.0,645.0] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.19/0.49 651[2:MRR:4.0,645.0] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.49 652[2:Rew:646.0,66.0] || equal(inverse(sk_c6),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.19/0.49 653[2:SpR:646.0,81.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),u)**. % 0.19/0.49 658[2:SpR:648.0,81.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c8)**. % 0.19/0.49 660[2:Rew:647.0,658.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.19/0.49 661[2:Rew:649.0,660.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 663[2:Rew:661.0,649.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.19/0.49 664[2:Rew:661.0,650.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.19/0.49 665[2:Rew:661.0,651.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.19/0.49 667[2:Rew:661.0,652.2] || equal(inverse(sk_c6),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.19/0.49 672[2:SpR:663.0,40.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),multiply(sk_c8,u))**. % 0.19/0.49 673[2:SpR:663.0,81.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c2)**. % 0.19/0.49 675[2:Rew:646.0,673.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.19/0.49 676[2:Rew:664.0,675.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.49 678[2:Rew:676.0,663.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.19/0.49 680[2:Rew:665.0,678.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 681[2:Rew:680.0,646.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 682[2:Rew:680.0,653.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.19/0.49 685[2:Rew:680.0,667.0] || equal(inverse(sk_c8),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c8)** -> . % 0.19/0.49 686[2:Rew:682.0,672.0,676.0,672.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 695[2:Rew:686.0,685.2,681.0,685.0] || equal(sk_c8,sk_c8) equal(identity,u)* equal(u,sk_c8) -> . % 0.19/0.49 696[2:Obv:695.0] || equal(identity,u)* equal(u,sk_c8) -> . % 0.19/0.49 714[2:SpR:686.0,331.0] || -> equal(identity,sk_c8)**. % 0.19/0.49 721[2:Rew:714.0,696.0] || equal(sk_c8,u)* equal(u,sk_c8)* -> . % 0.19/0.49 729[2:Obv:721.0] || equal(u,sk_c8)* -> . % 0.19/0.49 730[2:AED:729.0] || -> . % 0.19/0.49 731[1:Spt:730.0,37.0,37.1,37.2,37.4,37.6,37.7,37.8,37.10,37.11] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(inverse(sk_c8),sk_c6) equal(multiply(u,sk_c8),sk_c6)**+ equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6) -> . % 0.19/0.49 733[2:Spt:8.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.19/0.49 734[2:Rew:733.0,731.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(sk_c6,sk_c6) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6) -> . % 0.19/0.49 736[2:Obv:734.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c8)** equal(multiply(sk_c8,sk_c7),sk_c6) -> . % 0.19/0.49 738[2:SpR:733.0,81.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),u)**. % 0.19/0.49 740[3:Spt:16.1] || -> equal(multiply(sk_c6,sk_c7),sk_c8)**. % 0.19/0.49 742[3:Rew:740.0,736.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** equal(sk_c8,sk_c8) equal(multiply(sk_c8,sk_c7),sk_c6)** -> . % 0.19/0.49 743[3:Obv:742.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** equal(multiply(sk_c8,sk_c7),sk_c6)** -> . % 0.19/0.49 745[3:SpR:740.0,40.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),multiply(sk_c8,u))**. % 0.19/0.49 746[3:SpR:740.0,81.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c7)**. % 0.19/0.49 748[4:Spt:4.1] || -> equal(multiply(sk_c8,sk_c7),sk_c6)**. % 0.19/0.49 750[4:Rew:748.0,743.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** equal(sk_c6,sk_c6) -> . % 0.19/0.49 751[4:Obv:750.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.49 754[4:SpR:748.0,81.0] || -> equal(multiply(inverse(sk_c8),sk_c6),sk_c7)**. % 0.19/0.49 756[4:Rew:733.0,754.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.19/0.49 757[5:Spt:34.1] || -> equal(inverse(sk_c1),sk_c8)**. % 0.19/0.49 760[4:SpR:756.0,40.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.19/0.49 761[4:SpR:756.0,81.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c6)**. % 0.19/0.49 763[6:Spt:28.1] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.19/0.49 765[6:SpR:763.0,81.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c8)**. % 0.19/0.49 767[6:Rew:757.0,765.0] || -> equal(multiply(sk_c8,sk_c2),sk_c8)**. % 0.19/0.49 768[6:Rew:767.0,21.1] || -> equal(multiply(sk_c4,sk_c7),sk_c6)** equal(sk_c7,sk_c8). % 0.19/0.49 769[6:Rew:767.0,19.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(sk_c7,sk_c8). % 0.19/0.49 771[6:Rew:767.0,20.1] || -> equal(inverse(sk_c3),sk_c8)** equal(sk_c7,sk_c8). % 0.19/0.49 773[6:Rew:767.0,22.1] || -> equal(inverse(sk_c4),sk_c7)** equal(sk_c7,sk_c8). % 0.19/0.49 778[6:SpR:767.0,81.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c2)**. % 0.19/0.49 780[6:Rew:733.0,778.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.19/0.49 781[6:SpR:780.0,40.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),multiply(sk_c2,u))**. % 0.19/0.49 782[6:SpR:780.0,81.0] || -> equal(multiply(inverse(sk_c6),sk_c2),sk_c8)**. % 0.19/0.49 784[6:Rew:738.0,781.0] || -> equal(multiply(sk_c2,u),u)**. % 0.19/0.49 796[6:SpR:784.0,331.0] || -> equal(identity,sk_c2)**. % 0.19/0.49 799[6:Rew:796.0,331.0] || -> equal(multiply(u,sk_c2),u)**. % 0.19/0.49 800[6:Rew:796.0,39.0] || -> equal(multiply(inverse(u),u),sk_c2)**. % 0.19/0.49 802[6:Rew:799.0,782.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.19/0.49 803[6:Rew:802.0,746.0] || -> equal(multiply(sk_c8,sk_c8),sk_c7)**. % 0.19/0.49 806[6:SpR:800.0,81.0] || -> equal(multiply(inverse(inverse(u)),sk_c2),u)**. % 0.19/0.49 810[6:Rew:799.0,806.0] || -> equal(inverse(inverse(u)),u)**. % 0.19/0.49 833[7:Spt:771.1] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 834[7:Rew:833.0,740.0] || -> equal(multiply(sk_c6,sk_c8),sk_c8)**. % 0.19/0.49 835[7:Rew:833.0,748.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.19/0.49 837[7:Rew:833.0,803.0] || -> equal(multiply(sk_c8,sk_c8),sk_c8)**. % 0.19/0.49 842[7:Rew:833.0,751.1] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.49 844[7:Rew:780.0,834.0] || -> equal(sk_c2,sk_c8)**. % 0.19/0.49 849[7:Rew:844.0,799.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.49 852[7:Rew:835.0,837.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 853[7:Rew:852.0,733.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 868[7:Rew:849.0,842.5,833.0,842.5,849.0,842.4,833.0,842.4,852.0,842.4,849.0,842.3,852.0,842.3,852.0,842.0] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8)** equal(inverse(w),sk_c8)** equal(u,sk_c8) equal(v,sk_c8) equal(w,sk_c8) -> . % 0.19/0.49 869[7:Con:868.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.49 903[7:SpL:853.0,869.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.49 905[7:Obv:903.1] || -> . % 0.19/0.49 906[7:Spt:905.0,771.1,833.0] || equal(sk_c7,sk_c8)** -> . % 0.19/0.49 907[7:Spt:905.0,771.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.49 909[7:MRR:773.1,906.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.49 910[7:MRR:768.1,906.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.19/0.49 911[7:MRR:769.1,906.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.19/0.49 914[7:SpR:907.0,810.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.19/0.49 916[7:Rew:733.0,914.0] || -> equal(sk_c3,sk_c6)**. % 0.19/0.49 918[7:Rew:916.0,911.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.19/0.49 919[7:Rew:780.0,918.0] || -> equal(sk_c2,sk_c7)**. % 0.19/0.49 924[7:Rew:919.0,799.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.49 933[7:Rew:924.0,910.0] || -> equal(sk_c4,sk_c6)**. % 0.19/0.49 934[7:Rew:924.0,740.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 936[7:Rew:933.0,909.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.19/0.49 939[7:Rew:934.0,733.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 949[7:Rew:934.0,936.0] || -> equal(inverse(sk_c8),sk_c7)**. % 0.19/0.49 952[7:Rew:949.0,939.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 953[7:MRR:952.0,906.0] || -> . % 0.19/0.49 960[6:Spt:953.0,28.1,763.0] || equal(multiply(sk_c1,sk_c8),sk_c2)** -> . % 0.19/0.49 961[6:Spt:953.0,28.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.49 962[6:MRR:29.1,960.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.19/0.49 964[6:MRR:30.1,960.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.49 978[6:SpR:964.0,81.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.19/0.49 980[6:Rew:962.0,978.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.19/0.49 981[6:Rew:756.0,980.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.49 986[6:Rew:981.0,761.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c6)**. % 0.19/0.49 987[6:Rew:981.0,746.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c8)**. % 0.19/0.49 988[6:Rew:981.0,745.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),multiply(sk_c8,u))**. % 0.19/0.49 993[6:Rew:981.0,751.1] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.49 996[6:Rew:986.0,987.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.49 997[6:Rew:996.0,733.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.49 1000[6:Rew:996.0,738.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.19/0.49 1009[6:Rew:1000.0,988.0,996.0,988.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.49 1019[6:Rew:981.0,993.5,981.0,993.4,996.0,993.4,996.0,993.3,996.0,993.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** -> . % 0.19/0.49 1020[6:Con:1019.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.19/0.49 1046[6:SpR:1009.0,331.0] || -> equal(identity,sk_c8)**. % 0.19/0.49 1048[6:Rew:1046.0,331.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.49 1052[6:Rew:1048.0,1020.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.49 1090[6:SpL:997.0,1052.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.49 1091[6:Obv:1090.1] || -> . % 0.19/0.49 1092[5:Spt:1091.0,34.1,757.0] || equal(inverse(sk_c1),sk_c8)** -> . % 0.19/0.49 1093[5:Spt:1091.0,34.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.49 1094[5:MRR:35.1,1092.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.19/0.50 1096[5:MRR:36.0,1092.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.50 1118[5:SpR:1096.0,81.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.19/0.50 1120[5:Rew:756.0,1118.0,1094.0,1118.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.50 1125[5:Rew:1120.0,746.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c8)**. % 0.19/0.50 1126[5:Rew:1120.0,761.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c6)**. % 0.19/0.50 1127[5:Rew:1120.0,760.0] || -> equal(multiply(sk_c6,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.19/0.50 1132[5:Rew:1120.0,751.1] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.19/0.50 1135[5:Rew:1125.0,1126.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.50 1136[5:Rew:1135.0,733.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.50 1139[5:Rew:1135.0,738.0] || -> equal(multiply(sk_c8,multiply(sk_c8,u)),u)**. % 0.19/0.50 1148[5:Rew:1139.0,1127.0,1135.0,1127.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.50 1156[5:Rew:1120.0,1132.5,1120.0,1132.4,1135.0,1132.4,1135.0,1132.3,1135.0,1132.0] || equal(inverse(u),sk_c8) equal(inverse(v),sk_c8) equal(inverse(w),sk_c8) equal(multiply(u,sk_c8),sk_c8)** equal(multiply(v,sk_c8),sk_c8)** equal(multiply(w,sk_c8),sk_c8)** -> . % 0.19/0.50 1157[5:Con:1156.1] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),sk_c8)** -> . % 0.19/0.50 1183[5:SpR:1148.0,331.0] || -> equal(identity,sk_c8)**. % 0.19/0.50 1186[5:Rew:1183.0,331.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.50 1189[5:Rew:1186.0,1157.1] || equal(inverse(u),sk_c8)** equal(u,sk_c8) -> . % 0.19/0.50 1222[5:SpL:1136.0,1189.0] || equal(sk_c8,sk_c8)* equal(sk_c8,sk_c8)* -> . % 0.19/0.50 1223[5:Obv:1222.1] || -> . % 0.19/0.50 1224[4:Spt:1223.0,4.1,748.0] || equal(multiply(sk_c8,sk_c7),sk_c6)** -> . % 0.19/0.50 1225[4:Spt:1223.0,4.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.50 1226[4:MRR:5.1,1224.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.19/0.50 1227[4:MRR:2.1,1224.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.50 1228[4:MRR:6.1,1224.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.50 1229[4:MRR:1.1,1224.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.19/0.50 1230[4:MRR:3.1,1224.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.19/0.50 1243[4:SpR:1228.0,81.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.19/0.50 1245[4:Rew:1226.0,1243.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.19/0.50 1247[4:SpR:1229.0,81.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c8)**. % 0.19/0.50 1249[4:Rew:1227.0,1247.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.19/0.50 1250[4:Rew:1249.0,1224.0] || equal(sk_c6,sk_c8)** -> . % 0.19/0.50 1252[4:SpR:1230.0,81.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.19/0.50 1254[4:Rew:1225.0,1252.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.19/0.50 1256[4:SpR:1245.0,81.0] || -> equal(multiply(inverse(sk_c6),sk_c8),sk_c6)**. % 0.19/0.50 1258[4:Rew:746.0,1256.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.50 1261[4:Rew:1258.0,740.0] || -> equal(multiply(sk_c7,sk_c7),sk_c8)**. % 0.19/0.50 1263[4:Rew:1258.0,1250.0] || equal(sk_c7,sk_c8)** -> . % 0.19/0.50 1272[4:Rew:1258.0,1254.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.19/0.50 1273[4:Rew:1261.0,1272.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.50 1274[4:MRR:1273.0,1263.0] || -> . % 0.19/0.50 1276[3:Spt:1274.0,16.1,740.0] || equal(multiply(sk_c6,sk_c7),sk_c8)** -> . % 0.19/0.50 1277[3:Spt:1274.0,16.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.50 1278[3:MRR:17.1,1276.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.19/0.50 1279[3:MRR:14.1,1276.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.50 1280[3:MRR:18.1,1276.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.50 1281[3:MRR:13.1,1276.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.19/0.50 1282[3:MRR:15.1,1276.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.19/0.50 1292[3:SpR:1280.0,81.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.19/0.50 1294[3:Rew:1278.0,1292.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.19/0.50 1296[3:SpR:1281.0,81.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c8)**. % 0.19/0.50 1298[3:Rew:1279.0,1296.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.19/0.50 1300[3:SpR:1282.0,81.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.19/0.50 1302[3:Rew:1277.0,1300.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.19/0.50 1311[3:SpR:1302.0,81.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.19/0.50 1313[3:Rew:39.0,1311.0] || -> equal(identity,sk_c6)**. % 0.19/0.50 1314[3:Rew:1313.0,331.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.50 1315[3:Rew:1313.0,38.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.50 1318[3:Rew:1314.0,1294.0] || -> equal(sk_c6,sk_c8)**. % 0.19/0.50 1323[3:Rew:1318.0,1276.0] || equal(multiply(sk_c8,sk_c7),sk_c8)** -> . % 0.19/0.50 1333[3:Rew:1318.0,1315.0] || -> equal(multiply(sk_c8,u),u)**. % 0.19/0.50 1334[3:Rew:1333.0,1298.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.50 1349[3:Rew:1333.0,1323.0,1334.0,1323.0] || equal(sk_c8,sk_c8)* -> . % 0.19/0.50 1350[3:Obv:1349.0] || -> . % 0.19/0.50 1359[2:Spt:1350.0,8.1,733.0] || equal(inverse(sk_c8),sk_c6)** -> . % 0.19/0.50 1360[2:Spt:1350.0,8.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.19/0.50 1361[2:MRR:11.1,1359.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.19/0.50 1362[2:MRR:10.1,1359.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.19/0.50 1363[2:MRR:12.0,1359.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.19/0.50 1364[2:MRR:7.0,1359.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.19/0.50 1365[2:MRR:9.0,1359.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.19/0.50 1373[2:SpR:1363.0,81.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.19/0.50 1375[2:Rew:1361.0,1373.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.19/0.50 1377[2:SpR:1364.0,81.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c8)**. % 0.19/0.50 1379[2:Rew:1360.0,1377.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.19/0.50 1381[2:SpR:1365.0,81.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.19/0.50 1383[2:Rew:1362.0,1381.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.19/0.50 1391[2:SpR:1379.0,81.0] || -> equal(multiply(inverse(sk_c8),sk_c8),sk_c7)**. % 0.19/0.50 1393[2:Rew:39.0,1391.0] || -> equal(identity,sk_c7)**. % 0.19/0.50 1394[2:Rew:1393.0,38.0] || -> equal(multiply(sk_c7,u),u)**. % 0.19/0.50 1395[2:Rew:1393.0,331.0] || -> equal(multiply(u,sk_c7),u)**. % 0.19/0.50 1398[2:Rew:1394.0,1383.0] || -> equal(sk_c6,sk_c7)**. % 0.19/0.50 1403[2:Rew:1398.0,1359.0] || equal(inverse(sk_c8),sk_c7)** -> . % 0.19/0.50 1406[2:Rew:1398.0,1375.0] || -> equal(multiply(sk_c7,sk_c7),sk_c8)**. % 0.19/0.50 1411[2:Rew:1394.0,1406.0] || -> equal(sk_c7,sk_c8)**. % 0.19/0.50 1413[2:Rew:1411.0,1364.0] || -> equal(multiply(sk_c3,sk_c8),sk_c8)**. % 0.19/0.50 1418[2:Rew:1411.0,1395.0] || -> equal(multiply(u,sk_c8),u)**. % 0.19/0.50 1419[2:Rew:1411.0,1403.0] || equal(inverse(sk_c8),sk_c8)** -> . % 0.19/0.50 1422[2:Rew:1418.0,1413.0] || -> equal(sk_c3,sk_c8)**. % 0.19/0.50 1423[2:Rew:1422.0,1360.0] || -> equal(inverse(sk_c8),sk_c8)**. % 0.19/0.50 1424[2:Rew:1423.0,1419.0] || equal(sk_c8,sk_c8)* -> . % 0.19/0.50 1425[2:Obv:1424.0] || -> . % 0.19/0.50 % SZS output end Refutation % 0.19/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_26 prove_this_27 prove_this_28 prove_this_29 prove_this_30 prove_this_32 prove_this_33 prove_this_34 prove_this_35 prove_this_36 prove_this_37 left_identity left_inverse associativity % 0.19/0.50 %------------------------------------------------------------------------------