%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP358-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:47:00 EDT 2022 % Result : Unsatisfiable 0.20s 0.47s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : GRP358-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n025.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 22:52:24 EDT 2022 % 0.12/0.33 % CPUTime : % 0.20/0.47 % 0.20/0.47 SPASS V 3.9 % 0.20/0.47 SPASS beiseite: Proof found. % 0.20/0.47 % SZS status Theorem % 0.20/0.47 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.47 SPASS derived 999 clauses, backtracked 368 clauses, performed 11 splits and kept 764 clauses. % 0.20/0.47 SPASS allocated 63712 KBytes. % 0.20/0.47 SPASS spent 0:00:00.13 on the problem. % 0.20/0.47 0:00:00.03 for the input. % 0.20/0.47 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.47 0:00:00.01 for inferences. % 0.20/0.47 0:00:00.00 for the backtracking. % 0.20/0.47 0:00:00.06 for the reduction. % 0.20/0.47 % 0.20/0.47 % 0.20/0.47 Here is a proof with depth 5, length 414 : % 0.20/0.47 % SZS output start Refutation % 0.20/0.47 1[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c7,sk_c6),sk_c8). % 0.20/0.47 2[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.47 3[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c8). % 0.20/0.47 4[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.47 5[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.47 6[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c8). % 0.20/0.47 7[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.47 8[0:Inp] || -> equal(inverse(sk_c3),sk_c8)** equal(inverse(sk_c8),sk_c6). % 0.20/0.47 9[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 10[0:Inp] || -> equal(inverse(sk_c4),sk_c7)** equal(inverse(sk_c8),sk_c6). % 0.20/0.47 11[0:Inp] || -> equal(inverse(sk_c5),sk_c6)** equal(inverse(sk_c8),sk_c6). % 0.20/0.47 12[0:Inp] || -> equal(inverse(sk_c8),sk_c6) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.47 13[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(multiply(sk_c8,sk_c2),sk_c7). % 0.20/0.47 14[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.20/0.47 15[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c6)** equal(multiply(sk_c8,sk_c2),sk_c7). % 0.20/0.47 16[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.20/0.47 17[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.20/0.47 19[0:Inp] || -> equal(multiply(sk_c3,sk_c8),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.20/0.47 20[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.20/0.47 21[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c6) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.20/0.47 22[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.20/0.47 23[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.20/0.47 24[0:Inp] || -> equal(multiply(sk_c5,sk_c8),sk_c6) equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.20/0.47 25[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.47 26[0:Inp] || -> equal(inverse(sk_c3),sk_c8) equal(inverse(sk_c1),sk_c8)**. % 0.20/0.47 27[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 28[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(inverse(sk_c1),sk_c8)**. % 0.20/0.47 29[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(inverse(sk_c1),sk_c8)**. % 0.20/0.47 30[0:Inp] || -> equal(inverse(sk_c1),sk_c8) equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.47 31[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_c7,sk_c6),sk_c8) -> . % 0.20/0.47 32[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.20/0.47 33[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.20/0.47 34[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.20/0.47 35[1:Spt:31.3,31.5,31.9] || equal(inverse(u),sk_c8) equal(multiply(u,sk_c8),v)*+ equal(multiply(sk_c8,v),sk_c7)** -> . % 0.20/0.47 37[2:Spt:10.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.20/0.47 39[3:Spt:5.1] || -> equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.47 41[4:Spt:29.1] || -> equal(inverse(sk_c1),sk_c8)**. % 0.20/0.47 44[1:SpL:32.0,35.1] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.47 45[5:Spt:23.1] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.20/0.47 50[6:Spt:17.1] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.20/0.47 53[2:SpR:37.0,33.0] || -> equal(multiply(sk_c6,sk_c8),identity)**. % 0.20/0.47 54[4:SpR:41.0,33.0] || -> equal(multiply(sk_c8,sk_c1),identity)**. % 0.20/0.47 55[1:SpL:33.0,35.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.47 56[2:Rew:37.0,55.0] || equal(inverse(sk_c6),sk_c8) equal(identity,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.47 63[2:SpR:53.0,34.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),multiply(identity,u))**. % 0.20/0.47 64[6:SpR:50.0,34.0] || -> equal(multiply(sk_c8,multiply(sk_c2,u)),multiply(sk_c7,u))**. % 0.20/0.47 65[4:SpR:54.0,34.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),multiply(identity,u))**. % 0.20/0.47 66[3:SpR:39.0,34.0] || -> equal(multiply(sk_c7,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.20/0.47 68[0:SpR:33.0,34.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.47 70[2:Rew:32.0,63.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),u)**. % 0.20/0.47 71[4:Rew:32.0,65.0] || -> equal(multiply(sk_c8,multiply(sk_c1,u)),u)**. % 0.20/0.47 72[0:Rew:32.0,68.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.47 77[4:SpR:54.0,70.0] || -> equal(multiply(sk_c6,identity),sk_c1)**. % 0.20/0.47 81[4:SpR:77.0,34.0] || -> equal(multiply(sk_c6,multiply(identity,u)),multiply(sk_c1,u))**. % 0.20/0.47 83[4:Rew:32.0,81.0] || -> equal(multiply(sk_c1,u),multiply(sk_c6,u))**. % 0.20/0.47 84[5:Rew:83.0,45.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.20/0.47 86[4:Rew:83.0,71.0] || -> equal(multiply(sk_c8,multiply(sk_c6,u)),u)**. % 0.20/0.47 87[5:Rew:53.0,84.0] || -> equal(identity,sk_c2)**. % 0.20/0.47 88[5:Rew:87.0,32.0] || -> equal(multiply(sk_c2,u),u)**. % 0.20/0.47 89[5:Rew:87.0,33.0] || -> equal(multiply(inverse(u),u),sk_c2)**. % 0.20/0.47 90[5:Rew:87.0,53.0] || -> equal(multiply(sk_c6,sk_c8),sk_c2)**. % 0.20/0.47 92[5:Rew:87.0,77.0] || -> equal(multiply(sk_c6,sk_c2),sk_c1)**. % 0.20/0.47 93[5:Rew:87.0,44.0] || equal(inverse(sk_c2),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.47 94[5:Rew:87.0,56.1] || equal(inverse(sk_c6),sk_c8) equal(sk_c2,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.47 95[6:Rew:88.0,64.0] || -> equal(multiply(sk_c8,u),multiply(sk_c7,u))**. % 0.20/0.47 98[6:Rew:95.0,50.0] || -> equal(multiply(sk_c7,sk_c2),sk_c7)**. % 0.20/0.47 100[6:Rew:95.0,86.0] || -> equal(multiply(sk_c7,multiply(sk_c6,u)),u)**. % 0.20/0.47 104[6:Rew:95.0,66.0] || -> equal(multiply(sk_c7,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.20/0.47 107[6:Rew:100.0,104.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 108[6:Rew:107.0,39.0] || -> equal(sk_c8,sk_c6)**. % 0.20/0.47 109[6:Rew:107.0,100.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 111[6:Rew:107.0,98.0] || -> equal(sk_c2,sk_c7)**. % 0.20/0.47 114[6:Rew:108.0,37.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.20/0.47 116[6:Rew:108.0,90.0] || -> equal(multiply(sk_c6,sk_c6),sk_c2)**. % 0.20/0.47 122[6:Rew:111.0,89.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.20/0.47 126[6:Rew:109.0,116.0,111.0,116.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 127[6:Rew:126.0,108.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.47 128[6:Rew:126.0,114.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/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_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.47 142[6:Obv:141.1] || equal(u,sk_c7)* -> . % 0.20/0.47 143[6:UnC:142.0,122.0] || -> . % 0.20/0.47 146[6:Spt:143.0,17.1,50.0] || equal(multiply(sk_c8,sk_c2),sk_c7)** -> . % 0.20/0.47 147[6:Spt:143.0,17.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.20/0.47 148[6:MRR:16.1,146.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.47 149[6:MRR:14.1,146.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.47 152[6:MRR:15.1,146.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 153[6:MRR:13.1,146.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.47 182[6:SpR:148.0,89.0] || -> equal(multiply(sk_c7,sk_c4),sk_c2)**. % 0.20/0.47 185[6:SpR:149.0,89.0] || -> equal(multiply(sk_c8,sk_c3),sk_c2)**. % 0.20/0.47 199[6:SpR:185.0,70.0] || -> equal(multiply(sk_c6,sk_c2),sk_c3)**. % 0.20/0.47 200[6:Rew:92.0,199.0] || -> equal(sk_c1,sk_c3)**. % 0.20/0.47 204[6:Rew:200.0,83.0] || -> equal(multiply(sk_c3,u),multiply(sk_c6,u))**. % 0.20/0.47 205[6:Rew:204.0,153.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.20/0.47 208[6:Rew:90.0,205.0] || -> equal(sk_c2,sk_c7)**. % 0.20/0.47 211[6:Rew:208.0,88.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 213[6:Rew:208.0,89.0] || -> equal(multiply(inverse(u),u),sk_c7)**. % 0.20/0.47 215[6:Rew:208.0,182.0] || -> equal(multiply(sk_c7,sk_c4),sk_c7)**. % 0.20/0.47 218[6:Rew:208.0,93.0] || equal(inverse(sk_c7),sk_c8) equal(sk_c8,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.47 220[6:Rew:211.0,39.0] || -> equal(sk_c8,sk_c6)**. % 0.20/0.47 234[6:Rew:211.0,215.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.47 235[6:Rew:234.0,148.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 236[6:Rew:234.0,152.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 239[6:Rew:211.0,236.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 243[6:Rew:239.0,220.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.47 275[6:Rew:211.0,218.2,243.0,218.2,243.0,218.1,235.0,218.0,243.0,218.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.47 276[6:Obv:275.1] || equal(u,sk_c7)* -> . % 0.20/0.47 277[6:UnC:276.0,213.0] || -> . % 0.20/0.47 280[5:Spt:277.0,23.1,45.0] || equal(multiply(sk_c1,sk_c8),sk_c2)** -> . % 0.20/0.47 281[5:Spt:277.0,23.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.20/0.47 282[5:Rew:83.0,280.0] || equal(multiply(sk_c6,sk_c8),sk_c2)** -> . % 0.20/0.47 283[5:Rew:53.0,282.0] || equal(identity,sk_c2)** -> . % 0.20/0.47 284[4:Rew:53.0,22.1,83.0,22.1] || -> equal(inverse(sk_c4),sk_c7)** equal(identity,sk_c2). % 0.20/0.47 285[5:MRR:284.1,283.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.47 286[4:Rew:53.0,20.1,83.0,20.1] || -> equal(inverse(sk_c3),sk_c8)** equal(identity,sk_c2). % 0.20/0.47 287[5:MRR:286.1,283.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.47 288[4:Rew:53.0,24.1,83.0,24.1] || -> equal(multiply(sk_c5,sk_c8),sk_c6)** equal(identity,sk_c2). % 0.20/0.47 289[5:MRR:288.1,283.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.47 290[4:Rew:53.0,21.1,83.0,21.1] || -> equal(multiply(sk_c4,sk_c7),sk_c6)** equal(identity,sk_c2). % 0.20/0.47 291[5:MRR:290.1,283.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 292[4:Rew:53.0,19.1,83.0,19.1] || -> equal(multiply(sk_c3,sk_c8),sk_c7)** equal(identity,sk_c2). % 0.20/0.47 293[5:MRR:292.1,283.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.47 321[5:SpR:281.0,33.0] || -> equal(multiply(sk_c6,sk_c5),identity)**. % 0.20/0.47 337[0:SpR:72.0,72.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.47 340[3:SpR:39.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c8),sk_c6)**. % 0.20/0.47 343[5:SpR:321.0,72.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c5)**. % 0.20/0.47 345[2:SpR:53.0,72.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c8)**. % 0.20/0.47 346[5:SpR:293.0,72.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c8)**. % 0.20/0.47 349[5:SpR:291.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.20/0.47 351[0:SpR:33.0,72.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.47 358[5:Rew:343.0,345.0] || -> equal(sk_c5,sk_c8)**. % 0.20/0.47 360[5:Rew:358.0,289.0] || -> equal(multiply(sk_c8,sk_c8),sk_c6)**. % 0.20/0.47 365[5:Rew:287.0,346.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.20/0.47 373[5:Rew:39.0,349.0,285.0,349.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.47 374[5:Rew:373.0,37.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.20/0.47 376[5:Rew:373.0,39.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 377[5:Rew:373.0,53.0] || -> equal(multiply(sk_c6,sk_c7),identity)**. % 0.20/0.47 383[5:Rew:373.0,56.2] || equal(inverse(sk_c6),sk_c8) equal(identity,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.47 393[5:Rew:373.0,360.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.47 394[5:Rew:373.0,365.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 396[5:Rew:393.0,394.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 400[5:Rew:396.0,374.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 401[5:Rew:396.0,376.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.20/0.47 402[5:Rew:396.0,377.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.20/0.47 412[5:Rew:401.0,402.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 414[5:Rew:412.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 452[5:Rew:414.0,383.2,412.0,383.1,400.0,383.0,396.0,383.0,373.0,383.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.47 453[5:Obv:452.1] || equal(u,sk_c7)* -> . % 0.20/0.47 454[5:UnC:453.0,72.0] || -> . % 0.20/0.47 457[4:Spt:454.0,29.1,41.0] || equal(inverse(sk_c1),sk_c8)** -> . % 0.20/0.47 458[4:Spt:454.0,29.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.20/0.47 459[0:Rew:337.0,351.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.47 461[4:MRR:28.1,457.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.47 463[4:MRR:30.0,457.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.47 464[4:MRR:27.0,457.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 487[4:SpR:463.0,72.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.20/0.47 489[4:Rew:458.0,487.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.20/0.47 491[4:SpR:464.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.20/0.47 493[4:Rew:39.0,491.0,461.0,491.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.47 494[4:Rew:493.0,37.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.20/0.47 498[4:Rew:493.0,53.0] || -> equal(multiply(sk_c6,sk_c7),identity)**. % 0.20/0.47 501[4:Rew:493.0,340.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.47 504[4:Rew:493.0,44.2] || equal(inverse(identity),sk_c8) equal(sk_c8,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.20/0.47 513[4:Rew:493.0,489.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.20/0.47 514[4:Rew:498.0,501.0,494.0,501.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 515[4:Rew:514.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 520[4:Rew:515.0,513.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 524[4:Rew:520.0,494.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 528[4:Rew:520.0,514.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 529[4:Rew:520.0,515.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 549[4:Rew:529.0,504.2,493.0,504.1,524.0,504.0,528.0,504.0,493.0,504.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.47 550[4:Obv:549.1] || equal(u,sk_c7)* -> . % 0.20/0.47 551[4:UnC:550.0,72.0] || -> . % 0.20/0.47 554[3:Spt:551.0,5.1,39.0] || equal(multiply(sk_c7,sk_c6),sk_c8)** -> . % 0.20/0.47 555[3:Spt:551.0,5.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.20/0.47 556[3:MRR:4.1,554.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.47 557[3:MRR:2.1,554.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.47 558[3:MRR:6.1,554.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.47 559[3:MRR:3.1,554.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 560[3:MRR:1.1,554.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.47 569[3:SpR:557.0,72.0] || -> equal(multiply(sk_c8,multiply(sk_c3,u)),u)**. % 0.20/0.47 577[3:SpR:558.0,72.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.20/0.47 579[3:Rew:555.0,577.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.20/0.47 580[3:SpR:559.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.20/0.47 581[3:SpR:559.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.20/0.47 583[3:Rew:556.0,581.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 584[3:Rew:583.0,554.0] || equal(sk_c8,sk_c7)** -> . % 0.20/0.47 597[3:SpR:583.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.47 599[3:Rew:33.0,597.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 601[3:Rew:599.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 602[3:Rew:599.0,459.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.47 607[3:Rew:601.0,579.0] || -> equal(sk_c8,sk_c6)**. % 0.20/0.47 610[3:Rew:601.0,580.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.20/0.47 619[3:Rew:607.0,584.0] || equal(sk_c6,sk_c7)** -> . % 0.20/0.47 620[3:Rew:607.0,560.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 625[3:Rew:607.0,569.0] || -> equal(multiply(sk_c6,multiply(sk_c3,u)),u)**. % 0.20/0.47 630[3:Rew:602.0,620.0] || -> equal(sk_c3,sk_c7)**. % 0.20/0.47 637[3:Rew:601.0,625.0,630.0,625.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 638[3:Rew:637.0,610.0] || -> equal(multiply(sk_c4,u),u)**. % 0.20/0.47 640[3:Rew:638.0,559.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 641[3:MRR:640.0,619.0] || -> . % 0.20/0.47 650[2:Spt:641.0,10.1,37.0] || equal(inverse(sk_c8),sk_c6)** -> . % 0.20/0.47 651[2:Spt:641.0,10.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.47 652[2:MRR:11.1,650.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.20/0.47 653[2:MRR:8.1,650.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.47 654[2:MRR:12.0,650.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.47 655[2:MRR:9.0,650.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 656[2:MRR:7.0,650.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.47 664[2:SpR:654.0,72.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.20/0.47 666[2:Rew:652.0,664.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.20/0.47 668[2:SpR:655.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.20/0.47 670[2:Rew:651.0,668.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 672[2:SpR:656.0,72.0] || -> equal(multiply(inverse(sk_c3),sk_c7),sk_c8)**. % 0.20/0.47 674[2:Rew:653.0,672.0] || -> equal(multiply(sk_c8,sk_c7),sk_c8)**. % 0.20/0.47 679[2:SpR:670.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.47 681[2:Rew:33.0,679.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 682[2:Rew:681.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 683[2:Rew:681.0,459.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.47 687[2:Rew:681.0,55.1] || equal(inverse(inverse(sk_c8)),sk_c8) equal(sk_c6,u) equal(multiply(sk_c8,u),sk_c7)** -> . % 0.20/0.47 688[2:Rew:682.0,666.0] || -> equal(sk_c8,sk_c6)**. % 0.20/0.47 693[2:Rew:688.0,653.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.20/0.47 696[2:Rew:688.0,656.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.47 702[2:Rew:688.0,674.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.47 704[2:Rew:683.0,696.0] || -> equal(sk_c3,sk_c7)**. % 0.20/0.47 705[2:Rew:704.0,693.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.20/0.47 706[2:Rew:682.0,702.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 710[2:Rew:706.0,682.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 711[2:Rew:706.0,688.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.47 714[2:Rew:706.0,705.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 734[2:Rew:710.0,687.2,711.0,687.2,706.0,687.1,714.0,687.0,714.0,687.0,711.0,687.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.20/0.47 735[2:Obv:734.1] || equal(u,sk_c7)* -> . % 0.20/0.47 736[2:UnC:735.0,72.0] || -> . % 0.20/0.47 739[1:Spt:736.0,31.0,31.1,31.2,31.4,31.6,31.7,31.8,31.10] || 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_c7,sk_c6),sk_c8)** -> . % 0.20/0.47 741[2:Spt:11.1] || -> equal(inverse(sk_c8),sk_c6)**. % 0.20/0.47 742[2:Rew:741.0,739.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_c7,sk_c6),sk_c8)** -> . % 0.20/0.47 744[2:Obv:742.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_c7,sk_c6),sk_c8)** -> . % 0.20/0.47 746[2:SpR:741.0,72.0] || -> equal(multiply(sk_c6,multiply(sk_c8,u)),u)**. % 0.20/0.47 748[3:Spt:4.1] || -> equal(multiply(sk_c7,sk_c6),sk_c8)**. % 0.20/0.47 750[3:Rew:748.0,744.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) -> . % 0.20/0.47 751[3: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.20/0.47 754[3:SpR:748.0,72.0] || -> equal(multiply(inverse(sk_c7),sk_c8),sk_c6)**. % 0.20/0.47 756[4:Spt:28.1] || -> equal(inverse(sk_c1),sk_c8)**. % 0.20/0.47 759[5:Spt:17.1] || -> equal(multiply(sk_c8,sk_c2),sk_c7)**. % 0.20/0.47 761[5:SpR:759.0,72.0] || -> equal(multiply(inverse(sk_c8),sk_c7),sk_c2)**. % 0.20/0.47 763[5:Rew:741.0,761.0] || -> equal(multiply(sk_c6,sk_c7),sk_c2)**. % 0.20/0.47 767[6:Spt:23.1] || -> equal(multiply(sk_c1,sk_c8),sk_c2)**. % 0.20/0.47 769[6:SpR:767.0,72.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c8)**. % 0.20/0.47 771[6:Rew:759.0,769.0,756.0,769.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.47 772[6:Rew:771.0,741.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.20/0.47 779[6:Rew:771.0,751.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.20/0.47 781[6:Rew:771.0,754.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.47 784[6:Rew:763.0,781.0,772.0,781.0] || -> equal(sk_c2,sk_c6)**. % 0.20/0.47 785[6:Rew:784.0,763.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.47 790[6:Rew:771.0,779.5,771.0,779.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.20/0.47 799[0:SpR:33.0,72.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.47 801[6:SpR:772.0,33.0] || -> equal(multiply(sk_c6,sk_c7),identity)**. % 0.20/0.47 803[6:Rew:785.0,801.0] || -> equal(identity,sk_c6)**. % 0.20/0.47 804[6:Rew:803.0,32.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.47 806[6:Rew:803.0,459.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.47 809[6:Rew:804.0,785.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 814[6:Rew:809.0,772.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 817[6:Rew:809.0,790.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.20/0.47 822[6:Rew:809.0,806.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 835[6:Con:817.1] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c7),sk_c6)** equal(multiply(v,sk_c7),sk_c7)** -> . % 0.20/0.47 836[6:Rew:822.0,835.3,822.0,835.2,809.0,835.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) -> . % 0.20/0.47 837[6:Con:836.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.47 870[6:SpL:814.0,837.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.47 872[6:Obv:870.1] || -> . % 0.20/0.47 873[6:Spt:872.0,23.1,767.0] || equal(multiply(sk_c1,sk_c8),sk_c2)** -> . % 0.20/0.47 874[6:Spt:872.0,23.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.20/0.47 875[0:Rew:459.0,799.0] || -> equal(inverse(inverse(u)),u)**. % 0.20/0.47 876[6:MRR:22.1,873.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.47 880[6:MRR:21.1,873.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 905[5:SpR:763.0,72.0] || -> equal(multiply(inverse(sk_c6),sk_c2),sk_c7)**. % 0.20/0.47 908[6:SpR:880.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.20/0.47 910[6:Rew:748.0,908.0,876.0,908.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.47 911[6:Rew:910.0,756.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.47 912[6:Rew:910.0,741.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.20/0.47 916[6:Rew:910.0,748.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.47 917[6:Rew:910.0,754.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.47 918[6:Rew:910.0,873.0] || equal(multiply(sk_c1,sk_c7),sk_c2)** -> . % 0.20/0.47 929[6:Rew:912.0,917.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.47 930[6:Rew:763.0,929.0] || -> equal(sk_c2,sk_c6)**. % 0.20/0.47 933[6:Rew:930.0,905.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c7)**. % 0.20/0.47 935[6:Rew:930.0,918.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.20/0.47 936[6:Rew:33.0,933.0] || -> equal(identity,sk_c7)**. % 0.20/0.47 937[6:Rew:936.0,32.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.47 938[6:Rew:936.0,459.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.47 941[6:Rew:937.0,916.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 946[6:Rew:941.0,912.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.47 951[6:Rew:941.0,935.0] || equal(multiply(sk_c1,sk_c7),sk_c7)** -> . % 0.20/0.47 957[6:Rew:938.0,951.0] || equal(sk_c1,sk_c7)** -> . % 0.20/0.47 983[0:SpR:875.0,72.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.20/0.47 987[6:SpR:911.0,875.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.20/0.47 992[6:Rew:946.0,987.0] || -> equal(sk_c1,sk_c7)**. % 0.20/0.47 993[6:MRR:992.0,957.0] || -> . % 0.20/0.47 994[5:Spt:993.0,17.1,759.0] || equal(multiply(sk_c8,sk_c2),sk_c7)** -> . % 0.20/0.47 995[5:Spt:993.0,17.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.20/0.47 996[5:MRR:16.1,994.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.47 997[5:MRR:14.1,994.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.47 999[5:MRR:15.1,994.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 1000[5:MRR:13.1,994.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.47 1002[5:SpR:995.0,875.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.47 1005[5:SpR:996.0,875.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.20/0.47 1007[5:Rew:1005.0,754.0] || -> equal(multiply(sk_c4,sk_c8),sk_c6)**. % 0.20/0.47 1009[2:SpR:741.0,875.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.20/0.47 1011[5:Rew:1002.0,1009.0] || -> equal(sk_c5,sk_c8)**. % 0.20/0.47 1014[5:Rew:1011.0,1002.0] || -> equal(inverse(sk_c6),sk_c8)**. % 0.20/0.47 1026[5:SpR:997.0,875.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.20/0.47 1028[5:Rew:741.0,1026.0] || -> equal(sk_c3,sk_c6)**. % 0.20/0.47 1030[5:Rew:1028.0,1000.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.20/0.47 1043[5:SpR:999.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.20/0.47 1044[5:SpR:999.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.20/0.47 1046[5:Rew:748.0,1044.0,996.0,1044.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.47 1047[5:Rew:1046.0,741.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.20/0.47 1049[5:Rew:1046.0,1014.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.20/0.47 1052[5:Rew:1046.0,746.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.20/0.47 1054[5:Rew:1046.0,751.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.20/0.47 1056[5:Rew:1046.0,1007.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.47 1059[5:Rew:1046.0,1030.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.47 1060[5:Rew:1005.0,1047.0] || -> equal(sk_c4,sk_c6)**. % 0.20/0.47 1066[5:Rew:1060.0,1056.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.47 1067[5:Rew:1066.0,1059.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.47 1070[5:Rew:1067.0,1060.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.47 1071[5:Rew:1067.0,1049.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.48 1077[5:Rew:1067.0,1052.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.48 1081[5:Rew:1077.0,1043.0,1070.0,1043.0,1067.0,1043.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.48 1085[5:Rew:1046.0,1054.5,1067.0,1054.4,1046.0,1054.3,1067.0,1054.3,1067.0,1054.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.20/0.48 1086[5:Con:1085.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.20/0.48 1111[5:SpR:1081.0,459.0] || -> equal(identity,sk_c7)**. % 0.20/0.48 1113[5:Rew:1111.0,459.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.48 1117[5:Rew:1113.0,1086.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.48 1137[5:SpL:1071.0,1117.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.48 1138[5:Obv:1137.1] || -> . % 0.20/0.48 1139[4:Spt:1138.0,28.1,756.0] || equal(inverse(sk_c1),sk_c8)** -> . % 0.20/0.48 1140[4:Spt:1138.0,28.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.48 1142[4:MRR:26.1,1139.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.48 1144[4:MRR:27.0,1139.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.48 1145[4:MRR:25.0,1139.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.48 1147[4:SpR:1140.0,875.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.20/0.48 1149[4:Rew:1147.0,754.0] || -> equal(multiply(sk_c4,sk_c8),sk_c6)**. % 0.20/0.48 1165[4:SpR:1142.0,875.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.20/0.48 1167[4:Rew:741.0,1165.0] || -> equal(sk_c3,sk_c6)**. % 0.20/0.48 1169[4:Rew:1167.0,1145.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.20/0.48 1179[4:SpR:1144.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.20/0.48 1180[4:SpR:1144.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.20/0.48 1182[4:Rew:748.0,1180.0,1140.0,1180.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.48 1183[4:Rew:1182.0,1009.0] || -> equal(inverse(sk_c6),sk_c7)**. % 0.20/0.48 1184[4:Rew:1182.0,741.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.20/0.48 1188[4:Rew:1182.0,746.0] || -> equal(multiply(sk_c6,multiply(sk_c7,u)),u)**. % 0.20/0.48 1190[4:Rew:1182.0,751.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c8),sk_c6)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c8),sk_c7)** -> . % 0.20/0.48 1192[4:Rew:1182.0,1149.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.48 1195[4:Rew:1182.0,1169.0] || -> equal(multiply(sk_c6,sk_c7),sk_c7)**. % 0.20/0.48 1196[4:Rew:1147.0,1184.0] || -> equal(sk_c4,sk_c6)**. % 0.20/0.48 1202[4:Rew:1196.0,1192.0] || -> equal(multiply(sk_c6,sk_c7),sk_c6)**. % 0.20/0.48 1203[4:Rew:1202.0,1195.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.48 1205[4:Rew:1203.0,1183.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.20/0.48 1206[4:Rew:1203.0,1196.0] || -> equal(sk_c4,sk_c7)**. % 0.20/0.48 1212[4:Rew:1203.0,1188.0] || -> equal(multiply(sk_c7,multiply(sk_c7,u)),u)**. % 0.20/0.48 1216[4:Rew:1212.0,1179.0,1206.0,1179.0,1203.0,1179.0] || -> equal(multiply(sk_c7,u),u)**. % 0.20/0.48 1219[4:Rew:1182.0,1190.5,1203.0,1190.4,1182.0,1190.3,1203.0,1190.3,1203.0,1190.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c7),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.20/0.48 1220[4:Con:1219.1] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c7)** -> . % 0.20/0.48 1244[0:SpR:33.0,459.0] || -> equal(inverse(identity),identity)**. % 0.20/0.48 1247[4:SpR:1205.0,33.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.20/0.48 1249[4:Rew:1216.0,1247.0] || -> equal(identity,sk_c7)**. % 0.20/0.48 1251[4:Rew:1249.0,459.0] || -> equal(multiply(u,sk_c7),u)**. % 0.20/0.48 1255[4:Rew:1251.0,1220.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.20/0.48 1307[4:SpL:1205.0,1255.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.20/0.48 1308[4:Obv:1307.1] || -> . % 0.20/0.48 1309[3:Spt:1308.0,4.1,748.0] || equal(multiply(sk_c7,sk_c6),sk_c8)** -> . % 0.20/0.48 1310[3:Spt:1308.0,4.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.48 1312[3:MRR:2.1,1309.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.48 1316[3:MRR:3.1,1309.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.48 1317[3:MRR:1.1,1309.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.48 1320[3:SpR:1310.0,983.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.20/0.48 1331[3:SpR:1312.0,875.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.20/0.48 1334[3:Rew:741.0,1331.0] || -> equal(sk_c3,sk_c6)**. % 0.20/0.48 1336[3:Rew:1334.0,1317.0] || -> equal(multiply(sk_c6,sk_c8),sk_c7)**. % 0.20/0.48 1356[3:SpR:1316.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.20/0.48 1357[3:SpR:1316.0,72.0] || -> equal(multiply(inverse(sk_c4),sk_c6),sk_c7)**. % 0.20/0.48 1359[3:Rew:1310.0,1357.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.48 1360[3:Rew:1359.0,1309.0] || equal(sk_c8,sk_c7)** -> . % 0.20/0.48 1361[3:Rew:1320.0,1356.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.48 1362[3:Rew:1361.0,1336.0] || -> equal(sk_c8,sk_c7)**. % 0.20/0.48 1365[3:MRR:1362.0,1360.0] || -> . % 0.20/0.48 1373[2:Spt:1365.0,11.1,741.0] || equal(inverse(sk_c8),sk_c6)** -> . % 0.20/0.48 1374[2:Spt:1365.0,11.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.20/0.48 1375[2:MRR:8.1,1373.0] || -> equal(inverse(sk_c3),sk_c8)**. % 0.20/0.48 1376[2:MRR:10.1,1373.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.20/0.48 1377[2:MRR:12.0,1373.0] || -> equal(multiply(sk_c5,sk_c8),sk_c6)**. % 0.20/0.48 1378[2:MRR:9.0,1373.0] || -> equal(multiply(sk_c4,sk_c7),sk_c6)**. % 0.20/0.48 1379[2:MRR:7.0,1373.0] || -> equal(multiply(sk_c3,sk_c8),sk_c7)**. % 0.20/0.48 1380[2:SpR:1374.0,72.0] || -> equal(multiply(sk_c6,multiply(sk_c5,u)),u)**. % 0.20/0.48 1381[2:SpR:1374.0,875.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.20/0.48 1385[2:SpR:1375.0,875.0] || -> equal(inverse(sk_c8),sk_c3)**. % 0.20/0.48 1388[2:Rew:1385.0,1373.0] || equal(sk_c3,sk_c6)** -> . % 0.20/0.48 1391[2:SpR:1376.0,983.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.20/0.48 1406[2:SpR:1377.0,72.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c8)**. % 0.20/0.48 1408[2:Rew:1374.0,1406.0] || -> equal(multiply(sk_c6,sk_c6),sk_c8)**. % 0.20/0.48 1409[2:SpR:1378.0,34.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.20/0.48 1413[2:Rew:1391.0,1409.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.48 1414[2:Rew:1413.0,1408.0] || -> equal(sk_c8,sk_c6)**. % 0.20/0.48 1415[2:Rew:1413.0,1380.0] || -> equal(multiply(sk_c5,u),u)**. % 0.20/0.48 1418[2:Rew:1414.0,1375.0] || -> equal(inverse(sk_c3),sk_c6)**. % 0.20/0.48 1419[2:Rew:1414.0,1385.0] || -> equal(inverse(sk_c6),sk_c3)**. % 0.20/0.48 1421[2:Rew:1414.0,1379.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.20/0.48 1424[2:Rew:1381.0,1419.0] || -> equal(sk_c5,sk_c3)**. % 0.20/0.48 1427[2:Rew:1424.0,1415.0] || -> equal(multiply(sk_c3,u),u)**. % 0.20/0.48 1430[2:Rew:1427.0,1421.0] || -> equal(sk_c6,sk_c7)**. % 0.20/0.48 1431[2:Rew:1430.0,1388.0] || equal(sk_c3,sk_c7)** -> . % 0.20/0.48 1436[2:Rew:1430.0,1418.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.20/0.48 1482[2:SpR:1427.0,459.0] || -> equal(identity,sk_c3)**. % 0.20/0.48 1484[2:Rew:1482.0,1244.0] || -> equal(inverse(sk_c3),sk_c3)**. % 0.20/0.48 1489[2:Rew:1436.0,1484.0] || -> equal(sk_c3,sk_c7)**. % 0.20/0.48 1490[2:MRR:1489.0,1431.0] || -> . % 0.20/0.48 % SZS output end Refutation % 0.20/0.48 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_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_25 prove_this_26 prove_this_27 prove_this_28 prove_this_29 prove_this_30 prove_this_31 left_identity left_inverse associativity % 0.20/0.48 %------------------------------------------------------------------------------