%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP361-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:01 EDT 2022 % Result : Unsatisfiable 0.18s 0.47s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP361-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n021.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 07:54:41 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.47 % 0.18/0.47 SPASS V 3.9 % 0.18/0.47 SPASS beiseite: Proof found. % 0.18/0.47 % SZS status Theorem % 0.18/0.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.47 SPASS derived 748 clauses, backtracked 338 clauses, performed 12 splits and kept 610 clauses. % 0.18/0.47 SPASS allocated 63669 KBytes. % 0.18/0.47 SPASS spent 0:00:00.12 on the problem. % 0.18/0.47 0:00:00.04 for the input. % 0.18/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.18/0.47 0:00:00.00 for inferences. % 0.18/0.47 0:00:00.00 for the backtracking. % 0.18/0.47 0:00:00.05 for the reduction. % 0.18/0.47 % 0.18/0.47 % 0.18/0.47 Here is a proof with depth 5, length 374 : % 0.18/0.47 % SZS output start Refutation % 0.18/0.47 1[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.18/0.47 2[0:Inp] || -> equal(multiply(sk_c5,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.18/0.47 4[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.18/0.47 7[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.47 8[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 9[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c7),sk_c5)**. % 0.18/0.47 10[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.18/0.47 11[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.18/0.47 12[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(inverse(sk_c7),sk_c5)**. % 0.18/0.47 14[0:Inp] || -> equal(multiply(sk_c5,sk_c7),sk_c6) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.47 16[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.47 17[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c7) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.47 18[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.47 20[0:Inp] || -> equal(multiply(sk_c5,sk_c7),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.47 22[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.47 23[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.47 24[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.47 26[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 28[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.18/0.47 29[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.18/0.47 30[0:Inp] || -> equal(inverse(sk_c4),sk_c5) equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 31[0:Inp] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(w,sk_c7),x)*+ equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c7,x),sk_c6)** equal(multiply(sk_c5,sk_c7),sk_c6) equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.18/0.47 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.18/0.47 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.18/0.47 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.18/0.47 35[1:Spt:31.2,31.4,31.7] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),v)* equal(multiply(sk_c7,v),sk_c6)** -> . % 0.18/0.47 37[2:Spt:8.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.47 39[3:Spt:2.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.18/0.47 41[4:Spt:26.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 44[1:SpL:32.0,35.1] || equal(inverse(identity),sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.47 45[5:Spt:20.1] || -> equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.47 47[5:SpL:45.0,35.1] || equal(inverse(sk_c1),sk_c7) equal(sk_c2,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.47 48[5:Rew:41.0,47.0] || equal(sk_c7,sk_c7) equal(sk_c2,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.47 49[5:Obv:48.0] || equal(sk_c2,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.47 50[6:Spt:14.1] || -> equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.47 53[2:SpR:37.0,33.0] || -> equal(multiply(sk_c5,sk_c7),identity)**. % 0.18/0.47 54[4:SpR:41.0,33.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.18/0.47 55[1:SpL:33.0,35.1] || equal(inverse(inverse(sk_c7)),sk_c7) equal(identity,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.47 56[2:Rew:37.0,55.0] || equal(inverse(sk_c5),sk_c7) equal(identity,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.47 63[2:SpR:53.0,34.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),multiply(identity,u))**. % 0.18/0.47 64[6:SpR:50.0,34.0] || -> equal(multiply(sk_c7,multiply(sk_c2,u)),multiply(sk_c6,u))**. % 0.18/0.47 65[4:SpR:54.0,34.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),multiply(identity,u))**. % 0.18/0.47 66[3:SpR:39.0,34.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.18/0.47 68[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.18/0.47 70[2:Rew:32.0,63.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.18/0.47 71[4:Rew:32.0,65.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.18/0.47 72[0:Rew:32.0,68.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.18/0.47 77[4:SpR:54.0,70.0] || -> equal(multiply(sk_c5,identity),sk_c1)**. % 0.18/0.47 81[4:SpR:77.0,34.0] || -> equal(multiply(sk_c5,multiply(identity,u)),multiply(sk_c1,u))**. % 0.18/0.47 83[4:Rew:32.0,81.0] || -> equal(multiply(sk_c1,u),multiply(sk_c5,u))**. % 0.18/0.47 84[5:Rew:83.0,45.0] || -> equal(multiply(sk_c5,sk_c7),sk_c2)**. % 0.18/0.47 86[4:Rew:83.0,71.0] || -> equal(multiply(sk_c7,multiply(sk_c5,u)),u)**. % 0.18/0.47 87[5:Rew:53.0,84.0] || -> equal(identity,sk_c2)**. % 0.18/0.47 88[5:Rew:87.0,32.0] || -> equal(multiply(sk_c2,u),u)**. % 0.18/0.47 89[5:Rew:87.0,33.0] || -> equal(multiply(inverse(u),u),sk_c2)**. % 0.18/0.47 90[5:Rew:87.0,53.0] || -> equal(multiply(sk_c5,sk_c7),sk_c2)**. % 0.18/0.47 92[5:Rew:87.0,77.0] || -> equal(multiply(sk_c5,sk_c2),sk_c1)**. % 0.18/0.47 94[5:Rew:87.0,56.1] || equal(inverse(sk_c5),sk_c7) equal(sk_c2,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.47 95[6:Rew:88.0,64.0] || -> equal(multiply(sk_c7,u),multiply(sk_c6,u))**. % 0.18/0.47 98[6:Rew:95.0,50.0] || -> equal(multiply(sk_c6,sk_c2),sk_c6)**. % 0.18/0.47 100[6:Rew:95.0,86.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),u)**. % 0.18/0.47 104[6:Rew:95.0,66.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),multiply(sk_c6,u))**. % 0.18/0.47 107[6:Rew:100.0,104.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 108[6:Rew:107.0,39.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.47 109[6:Rew:107.0,100.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.47 111[6:Rew:107.0,98.0] || -> equal(sk_c2,sk_c6)**. % 0.18/0.47 114[6:Rew:108.0,37.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.47 116[6:Rew:108.0,90.0] || -> equal(multiply(sk_c5,sk_c5),sk_c2)**. % 0.18/0.47 122[6:Rew:111.0,89.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.18/0.47 126[6:Rew:109.0,116.0,111.0,116.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 127[6:Rew:126.0,108.0] || -> equal(sk_c7,sk_c6)**. % 0.18/0.47 128[6:Rew:126.0,114.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.18/0.47 141[6:Rew:107.0,94.2,127.0,94.2,111.0,94.1,128.0,94.0,126.0,94.0,127.0,94.0] || equal(sk_c6,sk_c6)* equal(sk_c6,u)* equal(u,sk_c6)* -> . % 0.18/0.47 142[6:Obv:141.1] || equal(u,sk_c6)* -> . % 0.18/0.47 143[6:UnC:142.0,122.0] || -> . % 0.18/0.47 146[6:Spt:143.0,14.1,50.0] || equal(multiply(sk_c7,sk_c2),sk_c6)** -> . % 0.18/0.47 147[6:Spt:143.0,14.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 148[6:Rew:90.0,147.0] || -> equal(sk_c2,sk_c6)**. % 0.18/0.47 152[6:Rew:148.0,92.0] || -> equal(multiply(sk_c5,sk_c6),sk_c1)**. % 0.18/0.47 153[6:Rew:148.0,88.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 154[6:Rew:153.0,39.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.47 159[6:Rew:148.0,89.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.18/0.47 160[6:Rew:152.0,146.0,154.0,146.0,148.0,146.0] || equal(sk_c1,sk_c6)** -> . % 0.18/0.47 161[6:Rew:154.0,70.0] || -> equal(multiply(sk_c5,multiply(sk_c5,u)),u)**. % 0.18/0.47 163[6:Rew:152.0,18.1,154.0,18.1,148.0,18.1] || -> equal(inverse(sk_c4),sk_c5)** equal(sk_c1,sk_c6). % 0.18/0.47 164[6:MRR:163.1,160.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.47 169[6:Rew:152.0,17.1,154.0,17.1,148.0,17.1,154.0,17.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)** equal(sk_c1,sk_c6). % 0.18/0.47 170[6:MRR:169.1,160.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.47 171[6:Rew:152.0,16.1,154.0,16.1,148.0,16.1,154.0,16.0] || -> equal(multiply(sk_c3,sk_c6),sk_c5)** equal(sk_c1,sk_c6). % 0.18/0.47 172[6:MRR:171.1,160.0] || -> equal(multiply(sk_c3,sk_c6),sk_c5)**. % 0.18/0.47 174[6:Rew:154.0,49.1,148.0,49.0] || equal(sk_c6,u) equal(multiply(sk_c5,u),sk_c6)** -> . % 0.18/0.47 197[6:SpR:170.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c5,u))**. % 0.18/0.47 199[6:SpR:172.0,34.0] || -> equal(multiply(sk_c3,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.18/0.47 201[6:Rew:153.0,199.0] || -> equal(multiply(sk_c3,u),multiply(sk_c5,u))**. % 0.18/0.47 202[6:Rew:201.0,172.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.18/0.47 203[6:Rew:152.0,202.0] || -> equal(sk_c1,sk_c5)**. % 0.18/0.47 206[6:Rew:203.0,152.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.18/0.47 218[6:SpR:164.0,159.0] || -> equal(multiply(sk_c5,sk_c4),sk_c6)**. % 0.18/0.47 233[6:SpR:218.0,161.0] || -> equal(multiply(sk_c5,sk_c6),sk_c4)**. % 0.18/0.47 235[6:Rew:206.0,233.0] || -> equal(sk_c4,sk_c5)**. % 0.18/0.47 239[6:Rew:235.0,197.0] || -> equal(multiply(sk_c5,multiply(sk_c5,u)),multiply(sk_c5,u))**. % 0.18/0.47 247[6:Rew:161.0,239.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.47 252[6:Rew:247.0,174.1] || equal(sk_c6,u)* equal(u,sk_c6)* -> . % 0.18/0.47 258[6:Obv:252.0] || equal(u,sk_c6)* -> . % 0.18/0.47 259[6:AED:258.0] || -> . % 0.18/0.47 262[5:Spt:259.0,20.1,45.0] || equal(multiply(sk_c1,sk_c7),sk_c2)** -> . % 0.18/0.47 263[5:Spt:259.0,20.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 264[5:Rew:53.0,263.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 265[5:Rew:264.0,77.0] || -> equal(multiply(sk_c5,sk_c6),sk_c1)**. % 0.18/0.47 267[5:Rew:264.0,53.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 268[5:Rew:264.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 269[5:Rew:268.0,39.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.47 270[5:Rew:269.0,37.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.47 273[5:Rew:269.0,267.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.18/0.47 274[5:Rew:264.0,33.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.18/0.47 275[5:Rew:269.0,262.0] || equal(multiply(sk_c1,sk_c5),sk_c2)** -> . % 0.18/0.47 276[5:Rew:269.0,70.0] || -> equal(multiply(sk_c5,multiply(sk_c5,u)),u)**. % 0.18/0.47 278[5:Rew:83.0,275.0] || equal(multiply(sk_c5,sk_c5),sk_c2)** -> . % 0.18/0.47 279[5:Rew:273.0,278.0] || equal(sk_c2,sk_c6)** -> . % 0.18/0.47 283[5:Rew:273.0,24.1,269.0,24.1,83.0,24.1] || -> equal(inverse(sk_c4),sk_c5)** equal(sk_c2,sk_c6). % 0.18/0.47 284[5:MRR:283.1,279.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.47 291[5:Rew:273.0,23.1,269.0,23.1,83.0,23.1,269.0,23.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)** equal(sk_c2,sk_c6). % 0.18/0.47 292[5:MRR:291.1,279.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.47 293[5:Rew:273.0,22.1,269.0,22.1,83.0,22.1,269.0,22.0] || -> equal(multiply(sk_c3,sk_c6),sk_c5)** equal(sk_c2,sk_c6). % 0.18/0.47 294[5:MRR:293.1,279.0] || -> equal(multiply(sk_c3,sk_c6),sk_c5)**. % 0.18/0.47 299[5:Rew:269.0,44.2,269.0,44.1,264.0,44.0,269.0,44.0] || equal(inverse(sk_c6),sk_c5) equal(sk_c5,u) equal(multiply(sk_c5,u),sk_c6)** -> . % 0.18/0.47 319[5:SpR:294.0,34.0] || -> equal(multiply(sk_c3,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.18/0.47 321[5:Rew:268.0,319.0] || -> equal(multiply(sk_c3,u),multiply(sk_c5,u))**. % 0.18/0.47 322[5:Rew:321.0,294.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.18/0.47 323[5:Rew:265.0,322.0] || -> equal(sk_c1,sk_c5)**. % 0.18/0.47 325[5:Rew:323.0,265.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.18/0.47 337[5:SpR:284.0,274.0] || -> equal(multiply(sk_c5,sk_c4),sk_c6)**. % 0.18/0.47 352[5:SpR:337.0,276.0] || -> equal(multiply(sk_c5,sk_c6),sk_c4)**. % 0.18/0.47 354[5:Rew:325.0,352.0] || -> equal(sk_c4,sk_c5)**. % 0.18/0.47 356[5:Rew:354.0,292.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)**. % 0.18/0.47 364[5:Rew:273.0,356.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 366[5:Rew:364.0,270.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.18/0.47 371[5:Rew:364.0,299.2] || equal(inverse(sk_c6),sk_c5) equal(sk_c5,u) equal(multiply(sk_c6,u),sk_c6)** -> . % 0.18/0.47 392[5:Rew:268.0,371.2] || equal(inverse(sk_c6),sk_c5)** equal(sk_c5,u)* equal(u,sk_c6) -> . % 0.18/0.47 393[5:Rew:364.0,392.1,366.0,392.0,364.0,392.0] || equal(sk_c6,sk_c6)* equal(sk_c6,u)* equal(u,sk_c6)* -> . % 0.18/0.47 394[5:Obv:393.1] || equal(u,sk_c6)* -> . % 0.18/0.47 395[5:UnC:394.0,274.0] || -> . % 0.18/0.47 400[4:Spt:395.0,26.0,41.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.18/0.47 401[4:Spt:395.0,26.1] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 402[4:Rew:53.0,401.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 403[4:Rew:402.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 404[4:Rew:402.0,53.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 405[4:Rew:403.0,39.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.47 406[4:Rew:405.0,37.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.47 407[4:Rew:405.0,400.0] || equal(inverse(sk_c1),sk_c5)** -> . % 0.18/0.47 408[4:Rew:405.0,404.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.18/0.47 409[4:Rew:402.0,33.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.18/0.47 410[4:Rew:405.0,70.0] || -> equal(multiply(sk_c5,multiply(sk_c5,u)),u)**. % 0.18/0.47 411[4:Rew:405.0,30.1] || -> equal(inverse(sk_c4),sk_c5) equal(inverse(sk_c1),sk_c5)**. % 0.18/0.47 412[4:MRR:411.1,407.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.47 418[4:Rew:405.0,29.1,405.0,29.0] || -> equal(inverse(sk_c1),sk_c5) equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.47 419[4:MRR:418.0,407.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.47 420[4:Rew:405.0,28.1,405.0,28.0] || -> equal(inverse(sk_c1),sk_c5) equal(multiply(sk_c3,sk_c6),sk_c5)**. % 0.18/0.47 421[4:MRR:420.0,407.0] || -> equal(multiply(sk_c3,sk_c6),sk_c5)**. % 0.18/0.47 434[4:Rew:405.0,44.2,405.0,44.1,402.0,44.0,405.0,44.0] || equal(inverse(sk_c6),sk_c5) equal(sk_c5,u) equal(multiply(sk_c5,u),sk_c6)** -> . % 0.18/0.47 447[4:SpR:421.0,34.0] || -> equal(multiply(sk_c3,multiply(sk_c6,u)),multiply(sk_c5,u))**. % 0.18/0.47 449[4:Rew:403.0,447.0] || -> equal(multiply(sk_c3,u),multiply(sk_c5,u))**. % 0.18/0.47 450[4:Rew:449.0,421.0] || -> equal(multiply(sk_c5,sk_c6),sk_c5)**. % 0.18/0.47 458[4:SpR:412.0,409.0] || -> equal(multiply(sk_c5,sk_c4),sk_c6)**. % 0.18/0.47 474[4:SpR:458.0,410.0] || -> equal(multiply(sk_c5,sk_c6),sk_c4)**. % 0.18/0.47 476[4:Rew:450.0,474.0] || -> equal(sk_c4,sk_c5)**. % 0.18/0.47 478[4:Rew:476.0,419.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)**. % 0.18/0.47 486[4:Rew:408.0,478.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 488[4:Rew:486.0,406.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.18/0.47 493[4:Rew:486.0,434.2] || equal(inverse(sk_c6),sk_c5) equal(sk_c5,u) equal(multiply(sk_c6,u),sk_c6)** -> . % 0.18/0.47 514[4:Rew:403.0,493.2] || equal(inverse(sk_c6),sk_c5)** equal(sk_c5,u)* equal(u,sk_c6) -> . % 0.18/0.47 515[4:Rew:486.0,514.1,488.0,514.0,486.0,514.0] || equal(sk_c6,sk_c6)* equal(sk_c6,u)* equal(u,sk_c6)* -> . % 0.18/0.47 516[4:Obv:515.1] || equal(u,sk_c6)* -> . % 0.18/0.47 517[4:UnC:516.0,409.0] || -> . % 0.18/0.47 522[3:Spt:517.0,2.1,39.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.18/0.47 523[3:Spt:517.0,2.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 524[3:Rew:53.0,523.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 526[3:Rew:524.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 528[3:Rew:526.0,522.0] || equal(sk_c7,sk_c5)** -> . % 0.18/0.47 543[3:Rew:526.0,1.1,526.0,1.0] || -> equal(sk_c7,sk_c5)** equal(sk_c7,sk_c5)**. % 0.18/0.47 544[3:Obv:543.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.47 545[3:MRR:544.0,528.0] || -> . % 0.18/0.47 548[2:Spt:545.0,8.0,37.0] || equal(inverse(sk_c7),sk_c5)** -> . % 0.18/0.47 549[2:Spt:545.0,8.1] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 550[2:MRR:12.1,548.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.47 551[2:MRR:9.1,548.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.47 552[2:MRR:11.0,548.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.18/0.47 553[2:MRR:10.0,548.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.18/0.47 561[2:SpR:553.0,34.0] || -> equal(multiply(sk_c3,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.18/0.47 569[2:SpR:550.0,33.0] || -> equal(multiply(sk_c5,sk_c4),identity)**. % 0.18/0.47 570[2:SpR:551.0,33.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.18/0.47 572[2:SpR:569.0,34.0] || -> equal(multiply(sk_c5,multiply(sk_c4,u)),multiply(identity,u))**. % 0.18/0.47 574[2:Rew:32.0,572.0] || -> equal(multiply(sk_c5,multiply(sk_c4,u)),u)**. % 0.18/0.47 580[2:SpR:552.0,574.0] || -> equal(multiply(sk_c5,sk_c7),sk_c5)**. % 0.18/0.47 581[2:Rew:549.0,580.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 582[2:Rew:581.0,549.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.18/0.47 584[2:Rew:581.0,548.0] || equal(inverse(sk_c7),sk_c6)** -> . % 0.18/0.47 585[2:Rew:581.0,552.0] || -> equal(multiply(sk_c4,sk_c6),sk_c7)**. % 0.18/0.47 587[2:Rew:581.0,569.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.18/0.47 615[0:SpR:72.0,72.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.18/0.47 621[0:SpR:33.0,72.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.47 625[2:SpR:582.0,72.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c7)**. % 0.18/0.47 632[2:Rew:33.0,625.0] || -> equal(sk_c7,identity)**. % 0.18/0.47 633[2:Rew:632.0,551.0] || -> equal(inverse(sk_c3),identity)**. % 0.18/0.47 635[2:Rew:632.0,570.0] || -> equal(multiply(identity,sk_c3),identity)**. % 0.18/0.47 637[2:Rew:632.0,584.0] || equal(inverse(identity),sk_c6)** -> . % 0.18/0.47 638[2:Rew:632.0,585.0] || -> equal(multiply(sk_c4,sk_c6),identity)**. % 0.18/0.47 647[2:Rew:632.0,561.0] || -> equal(multiply(sk_c3,multiply(sk_c6,u)),multiply(identity,u))**. % 0.18/0.47 652[2:Rew:32.0,635.0] || -> equal(identity,sk_c3)**. % 0.18/0.47 653[2:Rew:652.0,32.0] || -> equal(multiply(sk_c3,u),u)**. % 0.18/0.47 655[2:Rew:652.0,587.0] || -> equal(multiply(sk_c6,sk_c4),sk_c3)**. % 0.18/0.47 658[2:Rew:652.0,633.0] || -> equal(inverse(sk_c3),sk_c3)**. % 0.18/0.47 661[2:Rew:658.0,637.0,652.0,637.0] || equal(sk_c3,sk_c6)** -> . % 0.18/0.47 662[2:Rew:652.0,638.0] || -> equal(multiply(sk_c4,sk_c6),sk_c3)**. % 0.18/0.47 679[2:Rew:653.0,647.0,653.0,647.0,652.0,647.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 681[2:Rew:679.0,655.0] || -> equal(sk_c4,sk_c3)**. % 0.18/0.47 683[2:Rew:681.0,662.0] || -> equal(multiply(sk_c3,sk_c6),sk_c3)**. % 0.18/0.47 688[2:Rew:653.0,683.0] || -> equal(sk_c3,sk_c6)**. % 0.18/0.47 689[2:MRR:688.0,661.0] || -> . % 0.18/0.47 702[1:Spt:689.0,31.0,31.1,31.3,31.5,31.6,31.8,31.9,31.10] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c5),sk_c7)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c5,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.18/0.47 703[0:Rew:615.0,621.0] || -> equal(multiply(u,identity),u)**. % 0.18/0.47 705[2:Spt:7.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.47 706[2:Rew:705.0,702.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(sk_c5,sk_c5) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c5,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.18/0.47 708[2:Obv:706.2] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c5,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.18/0.47 710[2:SpR:705.0,72.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.18/0.47 712[3:Spt:2.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.18/0.47 714[3:Rew:712.0,708.6] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c5,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(sk_c7,sk_c7) -> . % 0.18/0.47 715[3:Obv:714.6] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c5,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) -> . % 0.18/0.47 718[3:SpR:712.0,72.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c5)**. % 0.18/0.47 720[4:Spt:26.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 738[0:SpR:33.0,72.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.47 739[0:SpR:33.0,703.0] || -> equal(inverse(identity),identity)**. % 0.18/0.47 741[2:SpR:705.0,33.0] || -> equal(multiply(sk_c5,sk_c7),identity)**. % 0.18/0.47 742[4:SpR:720.0,33.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.18/0.47 745[3:Rew:741.0,715.4] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(identity,sk_c6) equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.18/0.47 746[2:Rew:741.0,20.0] || -> equal(identity,sk_c6) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.47 747[2:Rew:741.0,14.0] || -> equal(identity,sk_c6) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.47 748[0:Rew:703.0,738.0] || -> equal(inverse(inverse(u)),u)**. % 0.18/0.47 755[5:Spt:746.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 756[5:Rew:755.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 757[5:Rew:755.0,703.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.47 759[5:Rew:755.0,739.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.18/0.47 760[5:Rew:755.0,741.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 761[5:Rew:755.0,742.0] || -> equal(multiply(sk_c7,sk_c1),sk_c6)**. % 0.18/0.47 763[5:Rew:755.0,745.4] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(sk_c6,sk_c6) equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.18/0.47 766[5:Rew:756.0,712.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.47 770[5:Rew:766.0,705.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.47 775[5:Rew:766.0,17.1] || -> equal(multiply(sk_c4,sk_c5),sk_c7)** equal(multiply(sk_c5,sk_c2),sk_c6). % 0.18/0.47 776[5:Rew:766.0,18.1] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c5,sk_c2),sk_c6)**. % 0.18/0.47 778[5:Rew:766.0,23.1] || -> equal(multiply(sk_c4,sk_c5),sk_c7) equal(multiply(sk_c1,sk_c5),sk_c2)**. % 0.18/0.47 779[5:Rew:766.0,24.1] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c1,sk_c5),sk_c2)**. % 0.18/0.47 782[5:Rew:766.0,760.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.18/0.47 783[5:Rew:766.0,761.0] || -> equal(multiply(sk_c5,sk_c1),sk_c6)**. % 0.18/0.47 791[5:Rew:766.0,775.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)** equal(multiply(sk_c5,sk_c2),sk_c6). % 0.18/0.47 794[5:Rew:766.0,778.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5) equal(multiply(sk_c1,sk_c5),sk_c2)**. % 0.18/0.47 795[5:Obv:763.4] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.18/0.47 796[5:Rew:766.0,795.4,756.0,795.4,757.0,795.3,766.0,795.3,766.0,795.2,766.0,795.1] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c5)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) equal(sk_c5,sk_c5) -> . % 0.18/0.47 797[5:Obv:796.4] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c5)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) -> . % 0.18/0.47 820[5:SpR:783.0,72.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c1)**. % 0.18/0.47 822[5:Rew:770.0,820.0] || -> equal(multiply(sk_c5,sk_c6),sk_c1)**. % 0.18/0.47 823[5:Rew:757.0,822.0] || -> equal(sk_c1,sk_c5)**. % 0.18/0.47 827[5:Rew:823.0,794.1] || -> equal(multiply(sk_c4,sk_c5),sk_c5)** equal(multiply(sk_c5,sk_c5),sk_c2). % 0.18/0.47 829[5:Rew:823.0,779.1] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c5,sk_c5),sk_c2)**. % 0.18/0.47 835[5:Rew:782.0,829.1] || -> equal(inverse(sk_c4),sk_c5)** equal(sk_c2,sk_c6). % 0.18/0.47 836[5:Rew:835.1,776.1] || -> equal(inverse(sk_c4),sk_c5) equal(multiply(sk_c5,sk_c6),sk_c6)**. % 0.18/0.47 837[5:Rew:757.0,836.1] || -> equal(inverse(sk_c4),sk_c5)** equal(sk_c5,sk_c6). % 0.18/0.47 838[5:Rew:782.0,827.1] || -> equal(multiply(sk_c4,sk_c5),sk_c5)** equal(sk_c2,sk_c6). % 0.18/0.47 839[5:Rew:838.1,791.1] || -> equal(multiply(sk_c4,sk_c5),sk_c5)** equal(multiply(sk_c5,sk_c6),sk_c6). % 0.18/0.47 840[5:Rew:757.0,839.1] || -> equal(multiply(sk_c4,sk_c5),sk_c5)** equal(sk_c5,sk_c6). % 0.18/0.47 842[0:SpR:748.0,72.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.18/0.47 874[6:Spt:835.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.47 876[6:SpR:874.0,748.0] || -> equal(inverse(sk_c5),sk_c4)**. % 0.18/0.47 880[6:Rew:770.0,876.0] || -> equal(sk_c4,sk_c5)**. % 0.18/0.47 882[6:Rew:880.0,840.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)** equal(sk_c5,sk_c6). % 0.18/0.47 887[6:Rew:782.0,882.0] || -> equal(sk_c5,sk_c6)** equal(sk_c5,sk_c6)**. % 0.18/0.47 888[6:Obv:887.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 895[6:Rew:888.0,797.0] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c5)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) -> . % 0.18/0.47 900[6:Rew:888.0,895.3,888.0,895.2,888.0,895.1] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6)** equal(multiply(u,sk_c6),sk_c6)** equal(v,sk_c6) -> . % 0.18/0.47 901[6:Rew:757.0,900.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.18/0.47 902[6:Con:901.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.18/0.47 909[6:SpL:759.0,902.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.18/0.47 911[6:Obv:909.1] || -> . % 0.18/0.47 912[6:Spt:911.0,835.0,874.0] || equal(inverse(sk_c4),sk_c5)** -> . % 0.18/0.47 913[6:Spt:911.0,835.1] || -> equal(sk_c2,sk_c6)**. % 0.18/0.47 914[6:MRR:837.0,912.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 923[6:Rew:914.0,797.3,914.0,797.2,914.0,797.1,914.0,797.0] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c6)** equal(multiply(u,sk_c6),sk_c6)** equal(v,sk_c6) -> . % 0.18/0.47 924[6:Rew:757.0,923.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.18/0.47 925[6:Con:924.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.18/0.47 949[6:SpL:759.0,925.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.18/0.47 951[6:Obv:949.1] || -> . % 0.18/0.47 952[5:Spt:951.0,746.0,755.0] || equal(identity,sk_c6)** -> . % 0.18/0.47 953[5:Spt:951.0,746.1] || -> equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.47 954[5:MRR:747.0,952.0] || -> equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.47 956[5:SpR:953.0,72.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c7)**. % 0.18/0.47 958[5:Rew:954.0,956.0,720.0,956.0] || -> equal(sk_c7,sk_c6)**. % 0.18/0.47 960[5:Rew:958.0,720.0] || -> equal(inverse(sk_c1),sk_c6)**. % 0.18/0.47 961[5:Rew:958.0,705.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.18/0.47 962[5:Rew:958.0,742.0] || -> equal(multiply(sk_c6,sk_c1),identity)**. % 0.18/0.47 963[5:Rew:958.0,741.0] || -> equal(multiply(sk_c5,sk_c6),identity)**. % 0.18/0.47 965[5:Rew:958.0,718.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.18/0.47 967[5:Rew:958.0,710.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.47 971[5:Rew:963.0,965.0,961.0,965.0] || -> equal(identity,sk_c5)**. % 0.18/0.47 972[5:Rew:971.0,739.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.47 973[5:Rew:971.0,952.0] || equal(sk_c5,sk_c6)** -> . % 0.18/0.47 975[5:Rew:971.0,32.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.47 977[5:Rew:971.0,962.0] || -> equal(multiply(sk_c6,sk_c1),sk_c5)**. % 0.18/0.47 981[5:Rew:975.0,967.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 983[5:Rew:981.0,977.0] || -> equal(sk_c1,sk_c5)**. % 0.18/0.47 985[5:Rew:983.0,960.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.47 987[5:Rew:972.0,985.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 988[5:MRR:987.0,973.0] || -> . % 0.18/0.47 994[4:Spt:988.0,26.0,720.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.18/0.47 995[4:Spt:988.0,26.1] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 996[4:Rew:741.0,995.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 997[4:Rew:996.0,739.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.18/0.47 998[4:Rew:996.0,741.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 999[4:Rew:996.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 1000[4:Rew:996.0,703.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.47 1001[4:Rew:999.0,712.0] || -> equal(sk_c7,sk_c5)**. % 0.18/0.47 1002[4:Rew:1001.0,705.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.18/0.47 1003[4:Rew:1001.0,994.0] || equal(inverse(sk_c1),sk_c5)** -> . % 0.18/0.47 1004[4:Rew:1001.0,998.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.18/0.47 1008[4:Rew:1001.0,30.1] || -> equal(inverse(sk_c4),sk_c5) equal(inverse(sk_c1),sk_c5)**. % 0.18/0.47 1009[4:MRR:1008.1,1003.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.47 1015[4:Rew:1001.0,29.1,1001.0,29.0] || -> equal(inverse(sk_c1),sk_c5) equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.47 1016[4:MRR:1015.0,1003.0] || -> equal(multiply(sk_c4,sk_c5),sk_c5)**. % 0.18/0.47 1028[4:Rew:1001.0,745.5,999.0,745.5,996.0,745.4,1000.0,745.3,1001.0,745.3,1001.0,745.2,1001.0,745.1] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c5)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) equal(sk_c6,sk_c6) equal(sk_c5,sk_c5) -> . % 0.18/0.47 1029[4:Obv:1028.5] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c5)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) -> . % 0.18/0.47 1046[4:SpR:1009.0,748.0] || -> equal(inverse(sk_c5),sk_c4)**. % 0.18/0.47 1049[4:Rew:1002.0,1046.0] || -> equal(sk_c4,sk_c5)**. % 0.18/0.47 1051[4:Rew:1049.0,1016.0] || -> equal(multiply(sk_c5,sk_c5),sk_c5)**. % 0.18/0.47 1052[4:Rew:1004.0,1051.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 1059[4:Rew:1052.0,1029.0] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c5)** equal(multiply(u,sk_c5),sk_c5)** equal(v,sk_c5) -> . % 0.18/0.47 1065[4:Rew:1052.0,1059.3,1000.0,1059.2,1052.0,1059.2,1052.0,1059.1] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c6)** equal(u,sk_c6) equal(v,sk_c6) -> . % 0.18/0.47 1066[4:Con:1065.1] || equal(inverse(u),sk_c6)** equal(u,sk_c6) -> . % 0.18/0.47 1107[4:SpL:997.0,1066.0] || equal(sk_c6,sk_c6)* equal(sk_c6,sk_c6)* -> . % 0.18/0.47 1108[4:Obv:1107.1] || -> . % 0.18/0.47 1109[3:Spt:1108.0,2.1,712.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.18/0.47 1110[3:Spt:1108.0,2.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 1111[3:Rew:741.0,1110.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 1113[3:Rew:1111.0,703.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.47 1114[3:Rew:1111.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 1117[3:Rew:1114.0,1109.0] || equal(sk_c7,sk_c5)** -> . % 0.18/0.47 1135[3:Rew:1114.0,4.1,1113.0,4.0] || -> equal(sk_c7,sk_c3)** equal(sk_c7,sk_c5). % 0.18/0.47 1136[3:MRR:1135.1,1117.0] || -> equal(sk_c7,sk_c3)**. % 0.18/0.47 1139[3:Rew:1136.0,1117.0] || equal(sk_c3,sk_c5)** -> . % 0.18/0.47 1148[3:Rew:1114.0,1.1,1136.0,1.1,1136.0,1.0,1114.0,1.0] || -> equal(sk_c3,sk_c5)** equal(sk_c3,sk_c5)**. % 0.18/0.47 1149[3:Obv:1148.0] || -> equal(sk_c3,sk_c5)**. % 0.18/0.47 1150[3:MRR:1149.0,1139.0] || -> . % 0.18/0.47 1155[2:Spt:1150.0,7.0,705.0] || equal(inverse(sk_c7),sk_c5)** -> . % 0.18/0.47 1156[2:Spt:1150.0,7.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.47 1157[2:MRR:12.1,1155.0] || -> equal(inverse(sk_c4),sk_c5)**. % 0.18/0.47 1158[2:MRR:9.1,1155.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.47 1159[2:MRR:11.0,1155.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.18/0.47 1160[2:MRR:10.0,1155.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.18/0.47 1161[2:MRR:8.0,1155.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.47 1173[2:SpR:1157.0,842.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),u)**. % 0.18/0.47 1175[2:SpR:1158.0,72.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.18/0.47 1176[2:SpR:1158.0,748.0] || -> equal(inverse(sk_c7),sk_c3)**. % 0.18/0.47 1179[2:Rew:1176.0,1155.0] || equal(sk_c3,sk_c5)** -> . % 0.18/0.47 1188[2:SpR:1159.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.18/0.47 1189[2:SpR:1159.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c7),sk_c5)**. % 0.18/0.47 1191[2:Rew:1157.0,1189.0] || -> equal(multiply(sk_c5,sk_c7),sk_c5)**. % 0.18/0.47 1192[2:Rew:1161.0,1191.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 1196[2:Rew:1192.0,1179.0] || equal(sk_c3,sk_c6)** -> . % 0.18/0.47 1201[2:Rew:1192.0,1173.0] || -> equal(multiply(sk_c4,multiply(sk_c6,u)),u)**. % 0.18/0.47 1204[2:Rew:1201.0,1188.0,1192.0,1188.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.47 1205[2:Rew:1204.0,1175.0] || -> equal(multiply(sk_c3,u),u)**. % 0.18/0.47 1207[2:Rew:1205.0,1160.0] || -> equal(sk_c7,sk_c6)**. % 0.18/0.47 1208[2:Rew:1207.0,1158.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.18/0.47 1254[2:SpR:1205.0,703.0] || -> equal(identity,sk_c3)**. % 0.18/0.47 1256[2:Rew:1254.0,739.0] || -> equal(inverse(sk_c3),sk_c3)**. % 0.18/0.47 1261[2:Rew:1208.0,1256.0] || -> equal(sk_c3,sk_c6)**. % 0.18/0.47 1262[2:MRR:1261.0,1196.0] || -> . % 0.18/0.47 % SZS output end Refutation % 0.18/0.47 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_4 prove_this_7 prove_this_8 prove_this_9 prove_this_10 prove_this_11 prove_this_12 prove_this_14 prove_this_16 prove_this_17 prove_this_18 prove_this_20 prove_this_22 prove_this_23 prove_this_24 prove_this_26 prove_this_28 prove_this_29 prove_this_30 prove_this_31 left_identity left_inverse associativity % 0.18/0.47 %------------------------------------------------------------------------------