%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP284-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n013.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:40 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.07/0.12 % Problem : GRP284-1 : TPTP v8.1.0. Released v2.5.0. % 0.07/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n013.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Mon Jun 13 17:48:29 EDT 2022 % 0.12/0.34 % 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 815 clauses, backtracked 374 clauses, performed 12 splits and kept 720 clauses. % 0.18/0.47 SPASS allocated 63587 KBytes. % 0.18/0.47 SPASS spent 0:00:00.12 on the problem. % 0.18/0.47 0:00:00.03 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.06 for the reduction. % 0.18/0.47 % 0.18/0.47 % 0.18/0.47 Here is a proof with depth 5, length 352 : % 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_c7,sk_c6),sk_c5). % 0.18/0.47 2[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 3[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7)** equal(multiply(sk_c7,sk_c6),sk_c5). % 0.18/0.47 4[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 5[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5). % 0.18/0.47 6[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 7[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 8[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 9[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 10[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 11[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.47 12[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 13[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.18/0.47 14[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 15[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.18/0.47 16[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 17[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 18[0:Inp] || -> equal(multiply(sk_c3,sk_c6),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 19[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 20[0:Inp] || -> equal(multiply(sk_c4,sk_c5),sk_c6) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 21[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.47 22[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 23[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.18/0.47 24[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 25[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.18/0.47 26[0:Inp] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(inverse(x),sk_c7) equal(multiply(u,sk_c5),sk_c6)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c5)** equal(multiply(x,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c7,sk_c6),sk_c5) -> . % 0.18/0.47 27[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.18/0.47 28[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.18/0.47 29[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.18/0.47 30[1:Spt:26.2,26.6] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),sk_c5)** -> . % 0.18/0.47 31[2:Spt:1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.47 33[2:SpL:31.0,30.1] || equal(inverse(sk_c6),sk_c7)** equal(sk_c5,sk_c5) -> . % 0.18/0.47 34[2:Obv:33.1] || equal(inverse(sk_c6),sk_c7)** -> . % 0.18/0.47 35[3:Spt:4.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.47 37[4:Spt:2.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.47 39[5:Spt:5.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.18/0.47 41[6:Spt:3.0] || -> equal(multiply(sk_c3,sk_c6),sk_c7)**. % 0.18/0.47 44[1:SpL:27.0,30.1] || equal(inverse(identity),sk_c7)** equal(sk_c5,sk_c7) -> . % 0.18/0.47 46[3:SpR:35.0,28.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.18/0.47 47[4:SpR:37.0,28.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.18/0.47 53[5:SpR:39.0,29.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c6,u))**. % 0.18/0.47 56[0:SpR:28.0,29.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.18/0.47 57[3:SpR:46.0,29.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),multiply(identity,u))**. % 0.18/0.47 59[3:Rew:27.0,57.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),u)**. % 0.18/0.47 60[0:Rew:27.0,56.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.18/0.47 62[4:SpR:47.0,29.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),multiply(identity,u))**. % 0.18/0.47 64[4:Rew:27.0,62.0] || -> equal(multiply(sk_c7,multiply(sk_c3,u)),u)**. % 0.18/0.47 67[5:SpR:39.0,59.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.18/0.47 73[6:SpR:41.0,64.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.18/0.47 76[0:SpR:60.0,60.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.18/0.47 78[2:SpR:31.0,60.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.18/0.47 82[0:SpR:28.0,60.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.47 83[3:SpR:46.0,60.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c4)**. % 0.18/0.47 85[5:SpR:67.0,60.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c6)**. % 0.18/0.47 87[4:SpR:47.0,60.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c3)**. % 0.18/0.47 93[5:Rew:78.0,85.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 94[5:Rew:93.0,31.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.18/0.47 95[5:Rew:93.0,35.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.47 96[5:Rew:93.0,34.0] || equal(inverse(sk_c7),sk_c7)** -> . % 0.18/0.47 99[5:Rew:93.0,46.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.18/0.47 103[5:Rew:93.0,53.0] || -> equal(multiply(sk_c4,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.18/0.47 106[6:Rew:93.0,73.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.18/0.47 107[5:Rew:93.0,78.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c7)**. % 0.18/0.47 108[5:Rew:93.0,83.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c4)**. % 0.18/0.47 109[6:Rew:94.0,106.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 116[6:Rew:109.0,107.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.18/0.47 117[6:Rew:28.0,116.0] || -> equal(identity,sk_c7)**. % 0.18/0.47 118[6:Rew:117.0,27.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.47 122[6:Rew:117.0,99.0] || -> equal(multiply(sk_c7,sk_c4),sk_c7)**. % 0.18/0.47 129[6:Rew:118.0,122.0] || -> equal(sk_c4,sk_c7)**. % 0.18/0.47 130[6:Rew:129.0,95.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 132[6:MRR:130.0,96.0] || -> . % 0.18/0.47 154[6:Spt:132.0,3.0,41.0] || equal(multiply(sk_c3,sk_c6),sk_c7)** -> . % 0.18/0.47 155[6:Spt:132.0,3.1] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 157[5:Rew:87.0,108.0] || -> equal(sk_c4,sk_c3)**. % 0.18/0.47 161[6:Rew:93.0,154.0] || equal(multiply(sk_c3,sk_c7),sk_c7)** -> . % 0.18/0.47 162[0:Rew:76.0,82.0] || -> equal(multiply(u,identity),u)**. % 0.18/0.47 163[4:Rew:162.0,87.0] || -> equal(inverse(sk_c7),sk_c3)**. % 0.18/0.47 172[5:Rew:93.0,13.1] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.18/0.47 173[6:MRR:172.1,161.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 174[5:Rew:157.0,103.0] || -> equal(multiply(sk_c3,multiply(sk_c5,u)),multiply(sk_c7,u))**. % 0.18/0.47 177[5:Rew:93.0,8.1,93.0,8.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.18/0.47 178[6:MRR:177.0,161.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.18/0.47 185[4:SpR:163.0,60.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),u)**. % 0.18/0.47 209[6:SpR:178.0,60.0] || -> equal(multiply(inverse(sk_c1),sk_c7),sk_c7)**. % 0.18/0.47 211[6:Rew:94.0,209.0,173.0,209.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 216[6:Rew:211.0,44.1] || equal(inverse(identity),sk_c7)** equal(sk_c7,sk_c7) -> . % 0.18/0.47 218[6:Rew:211.0,174.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.18/0.47 224[6:Obv:216.1] || equal(inverse(identity),sk_c7)** -> . % 0.18/0.47 225[6:Rew:185.0,218.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.47 226[6:Rew:225.0,47.0] || -> equal(identity,sk_c3)**. % 0.18/0.47 235[6:Rew:226.0,224.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.18/0.47 241[6:Rew:37.0,235.0] || equal(sk_c7,sk_c7)* -> . % 0.18/0.47 242[6:Obv:241.0] || -> . % 0.18/0.47 244[5:Spt:242.0,5.0,39.0] || equal(multiply(sk_c4,sk_c5),sk_c6)** -> . % 0.18/0.47 245[5:Spt:242.0,5.1] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 246[3:Rew:162.0,83.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.18/0.47 247[3:Rew:246.0,34.0] || equal(sk_c4,sk_c7)** -> . % 0.18/0.47 248[3:Rew:246.0,78.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.18/0.47 249[5:Rew:248.0,244.0] || equal(sk_c6,sk_c7)** -> . % 0.18/0.47 251[3:Rew:248.0,25.1] || -> equal(inverse(sk_c2),sk_c7)** equal(sk_c6,sk_c7). % 0.18/0.47 252[5:MRR:251.1,249.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 253[3:Rew:248.0,15.1] || -> equal(inverse(sk_c1),sk_c7)** equal(sk_c6,sk_c7). % 0.18/0.47 254[5:MRR:253.1,249.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 255[3:Rew:248.0,20.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 256[5:MRR:255.0,249.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 257[3:Rew:248.0,10.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 258[5:MRR:257.0,249.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 260[5:SpR:245.0,60.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c6)**. % 0.18/0.47 262[5:Rew:163.0,260.0] || -> equal(multiply(sk_c3,sk_c5),sk_c6)**. % 0.18/0.47 290[5:SpR:256.0,60.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c7)**. % 0.18/0.47 292[5:Rew:252.0,290.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.18/0.47 294[5:SpR:258.0,60.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.18/0.47 296[5:Rew:245.0,294.0,254.0,294.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 309[5:Rew:296.0,262.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.47 310[5:Rew:296.0,292.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.18/0.47 380[5:SpR:310.0,60.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.18/0.47 382[5:Rew:309.0,380.0,163.0,380.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 383[5:MRR:382.0,249.0] || -> . % 0.18/0.47 384[4:Spt:383.0,2.0,37.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.18/0.47 385[4:Spt:383.0,2.1] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 386[4:MRR:22.0,384.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 387[4:MRR:12.0,384.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 388[4:MRR:17.0,384.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 389[4:MRR:7.0,384.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 391[4:SpR:385.0,60.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c6)**. % 0.18/0.47 415[4:SpR:388.0,60.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c7)**. % 0.18/0.47 417[4:Rew:386.0,415.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.18/0.47 419[4:SpR:389.0,60.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.18/0.47 421[4:Rew:385.0,419.0,387.0,419.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 434[4:Rew:421.0,391.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.18/0.47 435[4:Rew:421.0,417.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.18/0.47 436[4:Rew:28.0,434.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 437[4:Rew:436.0,46.0] || -> equal(multiply(sk_c6,sk_c4),sk_c6)**. % 0.18/0.47 438[4:Rew:436.0,27.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 440[4:Rew:436.0,28.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.18/0.47 443[4:Rew:438.0,437.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.47 445[4:Rew:443.0,247.0] || equal(sk_c6,sk_c7)** -> . % 0.18/0.47 469[4:SpR:435.0,60.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.18/0.47 471[4:Rew:440.0,469.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 472[4:MRR:471.0,445.0] || -> . % 0.18/0.47 473[3:Spt:472.0,4.0,35.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.18/0.47 474[3:Spt:472.0,4.1] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 475[3:MRR:24.0,473.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 476[3:MRR:14.0,473.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 477[3:MRR:19.0,473.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 478[3:MRR:9.0,473.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 480[3:SpR:474.0,60.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c6)**. % 0.18/0.47 490[3:SpR:477.0,60.0] || -> equal(multiply(inverse(sk_c2),sk_c5),sk_c7)**. % 0.18/0.47 492[3:Rew:475.0,490.0] || -> equal(multiply(sk_c7,sk_c5),sk_c7)**. % 0.18/0.47 494[3:SpR:478.0,60.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.18/0.47 496[3:Rew:474.0,494.0,476.0,494.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 508[3:Rew:496.0,480.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.18/0.47 509[3:Rew:496.0,492.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.18/0.47 510[3:Rew:28.0,508.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 511[3:Rew:510.0,162.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.47 514[3:Rew:510.0,28.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.18/0.47 527[3:SpR:509.0,60.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c7)**. % 0.18/0.47 529[3:Rew:514.0,527.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 531[3:Rew:529.0,34.0] || equal(inverse(sk_c7),sk_c7)** -> . % 0.18/0.47 532[3:Rew:529.0,478.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.18/0.47 534[3:Rew:529.0,511.0] || -> equal(multiply(u,sk_c7),u)**. % 0.18/0.47 540[3:Rew:534.0,532.0] || -> equal(sk_c1,sk_c7)**. % 0.18/0.47 546[3:Rew:540.0,476.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 550[3:MRR:546.0,531.0] || -> . % 0.18/0.47 555[2:Spt:550.0,1.0,31.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.18/0.47 556[2:Spt:550.0,1.1] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 558[2:MRR:11.1,555.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 560[2:MRR:6.0,555.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 562[2:SpR:556.0,60.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c6)**. % 0.18/0.47 573[2:SpR:560.0,60.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.18/0.47 575[2:Rew:556.0,573.0,558.0,573.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 578[2:Rew:575.0,555.0] || equal(multiply(sk_c6,sk_c7),sk_c7)** -> . % 0.18/0.47 583[2:Rew:575.0,562.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.18/0.47 587[2:Rew:28.0,583.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 588[2:Rew:587.0,27.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.47 592[2:UnC:588.0,578.0] || -> . % 0.18/0.47 596[1:Spt:592.0,26.0,26.1,26.3,26.4,26.5,26.7,26.8,26.9] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c6)**+ equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c7,sk_c6),sk_c5) -> . % 0.18/0.47 598[2:Spt:1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.47 599[2:Rew:598.0,596.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c5,sk_c5) equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.18/0.47 601[2:Obv:599.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.18/0.47 604[2:SpR:598.0,60.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.18/0.47 606[3:Spt:2.1] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 608[3:Rew:606.0,601.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.18/0.47 609[3:Obv:608.6] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.18/0.47 612[3:SpR:606.0,60.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c6)**. % 0.18/0.47 614[4:Spt:24.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.47 623[5:Spt:22.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.47 631[0:SpR:28.0,60.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.47 632[0:SpR:28.0,162.0] || -> equal(inverse(identity),identity)**. % 0.18/0.47 634[4:SpR:614.0,28.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.18/0.47 635[5:SpR:623.0,28.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.18/0.47 637[0:Rew:162.0,631.0] || -> equal(inverse(inverse(u)),u)**. % 0.18/0.47 645[4:SpR:634.0,60.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c4)**. % 0.18/0.47 647[4:Rew:162.0,645.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.18/0.47 648[4:Rew:647.0,604.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.18/0.47 649[4:Rew:648.0,10.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 650[4:Rew:648.0,20.0] || -> equal(sk_c6,sk_c7) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 651[4:Rew:648.0,15.1] || -> equal(inverse(sk_c1),sk_c7)** equal(sk_c6,sk_c7). % 0.18/0.47 652[4:Rew:648.0,25.1] || -> equal(inverse(sk_c2),sk_c7)** equal(sk_c6,sk_c7). % 0.18/0.47 653[4:Rew:651.1,13.1] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.18/0.47 654[4:Rew:652.1,23.1] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.18/0.47 655[4:Rew:649.0,8.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 656[4:Rew:650.0,18.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 659[4:SpR:647.0,28.0] || -> equal(multiply(sk_c4,sk_c6),identity)**. % 0.18/0.47 662[5:SpR:635.0,60.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c3)**. % 0.18/0.47 664[5:Rew:162.0,662.0] || -> equal(inverse(sk_c7),sk_c3)**. % 0.18/0.47 665[5:Rew:664.0,612.0] || -> equal(multiply(sk_c3,sk_c5),sk_c6)**. % 0.18/0.47 667[6:Spt:651.1] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 668[6:Rew:667.0,598.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.18/0.47 672[6:Rew:667.0,647.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.18/0.47 674[6:Rew:667.0,609.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.18/0.47 679[6:Rew:667.0,655.1] || -> equal(multiply(sk_c3,sk_c7),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.18/0.47 680[6:Rew:667.0,659.0] || -> equal(multiply(sk_c4,sk_c7),identity)**. % 0.18/0.47 681[6:Rew:667.0,665.0] || -> equal(multiply(sk_c3,sk_c5),sk_c7)**. % 0.18/0.47 682[6:Rew:664.0,672.0] || -> equal(sk_c4,sk_c3)**. % 0.18/0.47 686[6:Rew:682.0,680.0] || -> equal(multiply(sk_c3,sk_c7),identity)**. % 0.18/0.47 687[6:Rew:686.0,656.0] || -> equal(identity,sk_c7) equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 688[6:Rew:686.0,654.1] || -> equal(inverse(sk_c2),sk_c7)** equal(identity,sk_c7). % 0.18/0.47 689[6:Rew:686.0,653.1] || -> equal(inverse(sk_c1),sk_c7)** equal(identity,sk_c7). % 0.18/0.47 692[6:Rew:686.0,679.0] || -> equal(identity,sk_c7) equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.18/0.47 693[6:Rew:667.0,674.5,667.0,674.4,667.0,674.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** equal(multiply(w,sk_c7),sk_c7)** -> . % 0.18/0.47 694[6:Con:693.2] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c5),sk_c7)** equal(multiply(v,sk_c7),sk_c7)** -> . % 0.18/0.47 700[5:SpR:664.0,28.0] || -> equal(multiply(sk_c3,sk_c7),identity)**. % 0.18/0.47 711[7:Spt:688.1] || -> equal(identity,sk_c7)**. % 0.18/0.47 712[7:Rew:711.0,162.0] || -> equal(multiply(u,sk_c7),u)**. % 0.18/0.47 715[7:Rew:711.0,632.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 718[7:Rew:664.0,715.0] || -> equal(sk_c3,sk_c7)**. % 0.18/0.47 719[7:Rew:718.0,623.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 725[7:Rew:712.0,668.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 727[7:Rew:712.0,694.3] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7)** equal(multiply(u,sk_c5),sk_c7)** equal(v,sk_c7) -> . % 0.18/0.47 734[7:Rew:712.0,727.2,725.0,727.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) -> . % 0.18/0.47 735[7:Con:734.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.18/0.47 774[7:SpL:719.0,735.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.18/0.47 776[7:Obv:774.1] || -> . % 0.18/0.47 777[7:Spt:776.0,688.1,711.0] || equal(identity,sk_c7)** -> . % 0.18/0.47 778[7:Spt:776.0,688.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 779[7:MRR:689.1,777.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 780[7:MRR:687.0,777.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 781[7:MRR:692.0,777.0] || -> equal(multiply(sk_c1,sk_c7),sk_c7)**. % 0.18/0.47 783[7:SpR:778.0,637.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.18/0.47 785[7:Rew:664.0,783.0] || -> equal(sk_c2,sk_c3)**. % 0.18/0.47 787[7:Rew:785.0,780.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.18/0.47 788[7:Rew:686.0,787.0] || -> equal(identity,sk_c5)**. % 0.18/0.47 790[7:Rew:788.0,777.0] || equal(sk_c5,sk_c7)** -> . % 0.18/0.47 794[7:Rew:788.0,162.0] || -> equal(multiply(u,sk_c5),u)**. % 0.18/0.47 797[7:Rew:794.0,681.0] || -> equal(sk_c3,sk_c7)**. % 0.18/0.47 801[7:Rew:797.0,664.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 814[7:SpR:779.0,637.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.47 816[7:Rew:801.0,814.0] || -> equal(sk_c1,sk_c7)**. % 0.18/0.47 818[7:Rew:816.0,781.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.18/0.47 819[7:Rew:668.0,818.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 820[7:MRR:819.0,790.0] || -> . % 0.18/0.47 822[6:Spt:820.0,651.1,667.0] || equal(sk_c6,sk_c7)** -> . % 0.18/0.47 823[6:Spt:820.0,651.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 824[6:MRR:652.1,822.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 825[6:MRR:649.0,822.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 826[6:MRR:650.0,822.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 828[6:SpR:823.0,637.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.47 830[6:Rew:664.0,828.0] || -> equal(sk_c1,sk_c3)**. % 0.18/0.47 832[6:Rew:830.0,825.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.47 833[6:Rew:700.0,832.0] || -> equal(identity,sk_c6)**. % 0.18/0.47 835[6:Rew:833.0,162.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.47 840[6:Rew:833.0,700.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.47 849[6:Rew:835.0,606.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.47 853[6:Rew:849.0,826.0] || -> equal(multiply(sk_c2,sk_c7),sk_c7)**. % 0.18/0.47 876[6:SpR:824.0,637.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.18/0.47 878[6:Rew:664.0,876.0] || -> equal(sk_c2,sk_c3)**. % 0.18/0.47 880[6:Rew:878.0,853.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.18/0.47 881[6:Rew:840.0,880.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 882[6:MRR:881.0,822.0] || -> . % 0.18/0.47 884[5:Spt:882.0,22.0,623.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.18/0.47 885[5:Spt:882.0,22.1] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 886[5:MRR:12.0,884.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 887[5:MRR:17.0,884.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 888[5:MRR:7.0,884.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 890[5:SpR:885.0,637.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.18/0.47 898[5:SpR:886.0,637.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.47 900[5:Rew:890.0,898.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.47 902[5:Rew:900.0,887.0] || -> equal(multiply(sk_c1,sk_c7),sk_c5)**. % 0.18/0.47 903[5:Rew:900.0,890.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.47 906[5:Rew:888.0,902.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 907[5:Rew:906.0,648.0] || -> equal(multiply(sk_c4,sk_c6),sk_c7)**. % 0.18/0.47 912[5:Rew:906.0,609.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.18/0.47 915[5:Rew:659.0,907.0] || -> equal(identity,sk_c7)**. % 0.18/0.47 916[5:Rew:915.0,632.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 919[5:Rew:915.0,27.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.47 920[5:Rew:915.0,162.0] || -> equal(multiply(u,sk_c7),u)**. % 0.18/0.47 922[5:Rew:903.0,916.0] || -> equal(sk_c1,sk_c7)**. % 0.18/0.47 923[5:Rew:922.0,886.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 924[5:Rew:922.0,888.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.18/0.47 928[5:Rew:919.0,924.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 945[5:Rew:920.0,912.5,928.0,912.5,920.0,912.4,928.0,912.4,920.0,912.3,928.0,912.3,928.0,912.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) equal(w,sk_c7) -> . % 0.18/0.47 946[5:Con:945.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.18/0.47 1004[5:SpL:923.0,946.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.18/0.47 1005[5:Obv:1004.1] || -> . % 0.18/0.47 1006[4:Spt:1005.0,24.0,614.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.18/0.47 1007[4:Spt:1005.0,24.1] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 1008[4:MRR:14.0,1006.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 1009[4:MRR:19.0,1006.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 1010[4:MRR:9.0,1006.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 1012[4:SpR:1007.0,637.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.18/0.47 1017[4:SpR:1008.0,637.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.47 1020[4:Rew:1012.0,1017.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.47 1022[4:Rew:1020.0,1009.0] || -> equal(multiply(sk_c1,sk_c7),sk_c5)**. % 0.18/0.47 1023[4:Rew:1020.0,1012.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.47 1027[4:Rew:1010.0,1022.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 1030[4:Rew:1027.0,604.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c7)**. % 0.18/0.47 1033[4:Rew:1027.0,609.3] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(multiply(u,sk_c6),sk_c6)** equal(multiply(v,sk_c6),sk_c7)** equal(multiply(w,sk_c7),sk_c6)** -> . % 0.18/0.47 1036[4:Rew:28.0,1030.0] || -> equal(identity,sk_c7)**. % 0.18/0.47 1037[4:Rew:1036.0,632.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 1038[4:Rew:1036.0,162.0] || -> equal(multiply(u,sk_c7),u)**. % 0.18/0.47 1039[4:Rew:1036.0,27.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.47 1041[4:Rew:1023.0,1037.0] || -> equal(sk_c1,sk_c7)**. % 0.18/0.47 1042[4:Rew:1041.0,1008.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.47 1043[4:Rew:1041.0,1010.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.18/0.47 1047[4:Rew:1039.0,1043.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 1055[4:Rew:1038.0,1033.5,1047.0,1033.5,1038.0,1033.4,1047.0,1033.4,1038.0,1033.3,1047.0,1033.3,1047.0,1033.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(inverse(w),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) equal(w,sk_c7) -> . % 0.18/0.47 1056[4:Con:1055.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.18/0.47 1104[4:SpL:1042.0,1056.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.18/0.47 1105[4:Obv:1104.1] || -> . % 0.18/0.47 1106[3:Spt:1105.0,2.1,606.0] || equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.18/0.47 1107[3:Spt:1105.0,2.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.47 1108[3:MRR:4.1,1106.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.47 1110[3:MRR:5.1,1106.0] || -> equal(multiply(sk_c4,sk_c5),sk_c6)**. % 0.18/0.47 1122[3:SpR:1108.0,637.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.18/0.47 1125[3:Rew:1122.0,604.0] || -> equal(multiply(sk_c4,sk_c5),sk_c7)**. % 0.18/0.47 1126[3:Rew:1110.0,1125.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 1128[3:Rew:1126.0,598.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.18/0.47 1129[3:Rew:1126.0,1106.0] || equal(multiply(sk_c7,sk_c7),sk_c5)** -> . % 0.18/0.47 1137[3:Rew:1128.0,1129.0] || equal(sk_c5,sk_c5)* -> . % 0.18/0.47 1138[3:Obv:1137.0] || -> . % 0.18/0.47 1141[2:Spt:1138.0,1.0,598.0] || equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.18/0.47 1142[2:Spt:1138.0,1.1] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.47 1143[2:MRR:21.1,1141.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.18/0.47 1144[2:MRR:11.1,1141.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.47 1145[2:MRR:16.0,1141.0] || -> equal(multiply(sk_c2,sk_c7),sk_c5)**. % 0.18/0.47 1146[2:MRR:6.0,1141.0] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.18/0.47 1151[2:SpR:1143.0,637.0] || -> equal(inverse(sk_c7),sk_c2)**. % 0.18/0.47 1156[2:SpR:1144.0,637.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.47 1159[2:Rew:1151.0,1156.0] || -> equal(sk_c2,sk_c1)**. % 0.18/0.47 1161[2:Rew:1159.0,1145.0] || -> equal(multiply(sk_c1,sk_c7),sk_c5)**. % 0.18/0.47 1166[2:Rew:1146.0,1161.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.47 1167[2:Rew:1166.0,1142.0] || -> equal(multiply(sk_c7,sk_c6),sk_c6)**. % 0.18/0.47 1168[2:Rew:1166.0,1141.0] || equal(multiply(sk_c6,sk_c7),sk_c6)** -> . % 0.18/0.47 1178[2:SpR:1146.0,60.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.18/0.47 1180[2:Rew:1144.0,1178.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.18/0.47 1181[2:Rew:1167.0,1180.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.47 1185[2:Rew:1181.0,1167.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.18/0.47 1186[2:Rew:1181.0,1168.0] || equal(multiply(sk_c7,sk_c7),sk_c7)** -> . % 0.18/0.47 1188[2:Rew:1185.0,1186.0] || equal(sk_c7,sk_c7)* -> . % 0.18/0.47 1189[2:Obv:1188.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_3 prove_this_4 prove_this_5 prove_this_6 prove_this_7 prove_this_8 prove_this_9 prove_this_10 prove_this_11 prove_this_12 prove_this_13 prove_this_14 prove_this_15 prove_this_16 prove_this_17 prove_this_18 prove_this_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_25 prove_this_26 left_identity left_inverse associativity % 0.18/0.47 %------------------------------------------------------------------------------