%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP386-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n006.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:08 EDT 2022 % Result : Unsatisfiable 0.18s 0.53s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : GRP386-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n006.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 : Tue Jun 14 00:25:41 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.53 % 0.18/0.53 SPASS V 3.9 % 0.18/0.53 SPASS beiseite: Proof found. % 0.18/0.53 % SZS status Theorem % 0.18/0.53 Problem: /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.18/0.53 SPASS derived 1425 clauses, backtracked 537 clauses, performed 11 splits and kept 1045 clauses. % 0.18/0.53 SPASS allocated 64160 KBytes. % 0.18/0.53 SPASS spent 0:00:00.19 on the problem. % 0.18/0.53 0:00:00.03 for the input. % 0.18/0.53 0:00:00.00 for the FLOTTER CNF translation. % 0.18/0.53 0:00:00.01 for inferences. % 0.18/0.53 0:00:00.00 for the backtracking. % 0.18/0.53 0:00:00.12 for the reduction. % 0.18/0.53 % 0.18/0.53 % 0.18/0.53 Here is a proof with depth 5, length 370 : % 0.18/0.53 % SZS output start Refutation % 0.18/0.53 1[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 2[0:Inp] || -> equal(inverse(sk_c2),sk_c10)** equal(inverse(sk_c10),sk_c9). % 0.18/0.53 5[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 6[0:Inp] || -> equal(inverse(sk_c4),sk_c7)** equal(inverse(sk_c10),sk_c9). % 0.18/0.53 7[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c7,sk_c9),sk_c10)**. % 0.18/0.53 8[0:Inp] || -> equal(inverse(sk_c6),sk_c5)** equal(inverse(sk_c10),sk_c9). % 0.18/0.53 9[0:Inp] || -> equal(inverse(sk_c5),sk_c7)** equal(inverse(sk_c10),sk_c9). % 0.18/0.53 10[0:Inp] || -> equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.53 11[0:Inp] || -> equal(multiply(sk_c2,sk_c10),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.18/0.53 12[0:Inp] || -> equal(inverse(sk_c2),sk_c10) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.53 13[0:Inp] || -> equal(multiply(sk_c3,sk_c9),sk_c8)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.18/0.53 14[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.53 15[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c10)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.18/0.53 16[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.53 19[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.53 21[0:Inp] || -> equal(multiply(sk_c2,sk_c10),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9). % 0.18/0.53 22[0:Inp] || -> equal(inverse(sk_c2),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.53 23[0:Inp] || -> equal(multiply(sk_c3,sk_c9),sk_c8)** equal(multiply(sk_c10,sk_c8),sk_c9). % 0.18/0.53 24[0:Inp] || -> equal(inverse(sk_c3),sk_c9) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.53 25[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c10)** equal(multiply(sk_c10,sk_c8),sk_c9). % 0.18/0.53 26[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.53 28[0:Inp] || -> equal(inverse(sk_c6),sk_c5) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.53 29[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.53 31[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 32[0:Inp] || -> equal(inverse(sk_c2),sk_c10) equal(inverse(sk_c1),sk_c10)**. % 0.18/0.53 35[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 36[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(inverse(sk_c1),sk_c10)**. % 0.18/0.53 39[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(inverse(sk_c1),sk_c10)**. % 0.18/0.53 45[0:Inp] || -> equal(multiply(sk_c4,sk_c7),sk_c10) equal(multiply(sk_c1,sk_c9),sk_c10)**. % 0.18/0.53 46[0:Inp] || -> equal(inverse(sk_c4),sk_c7) equal(multiply(sk_c1,sk_c9),sk_c10)**. % 0.18/0.53 47[0:Inp] || -> equal(multiply(sk_c7,sk_c9),sk_c10) equal(multiply(sk_c1,sk_c9),sk_c10)**. % 0.18/0.53 49[0:Inp] || -> equal(inverse(sk_c5),sk_c7) equal(multiply(sk_c1,sk_c9),sk_c10)**. % 0.18/0.53 51[0:Inp] || equal(inverse(u),v)* equal(inverse(w),u) equal(inverse(x),v) equal(inverse(y),sk_c9) equal(inverse(z),sk_c10) equal(inverse(x1),sk_c10) equal(inverse(sk_c10),sk_c9) equal(multiply(w,v),u)*+ equal(multiply(x,v),sk_c10)** equal(multiply(v,sk_c9),sk_c10)** equal(multiply(y,sk_c9),sk_c8)** equal(multiply(z,sk_c10),sk_c9)** equal(multiply(x1,sk_c9),sk_c10)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.18/0.53 52[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.18/0.53 53[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.18/0.53 54[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.18/0.53 55[1:Spt:51.0,51.1,51.2,51.7,51.8,51.9] || equal(inverse(u),v)* equal(inverse(w),u) equal(inverse(x),v) equal(multiply(w,v),u)*+ equal(multiply(x,v),sk_c10)** equal(multiply(v,sk_c9),sk_c10)** -> . % 0.18/0.53 57[2:Spt:9.1] || -> equal(inverse(sk_c10),sk_c9)**. % 0.18/0.53 59[3:Spt:29.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.53 61[3:SpL:59.0,55.3] || equal(inverse(u),sk_c8)** equal(inverse(sk_c10),u)* equal(inverse(v),sk_c8) equal(sk_c9,u) equal(multiply(v,sk_c8),sk_c10)** equal(multiply(sk_c8,sk_c9),sk_c10)** -> . % 0.18/0.53 62[3:Rew:57.0,61.1] || equal(inverse(u),sk_c8)** equal(sk_c9,u) equal(inverse(v),sk_c8) equal(sk_c9,u) equal(multiply(v,sk_c8),sk_c10)** equal(multiply(sk_c8,sk_c9),sk_c10)** -> . % 0.18/0.53 63[3:Obv:62.1] || equal(inverse(u),sk_c8)** equal(inverse(v),sk_c8) equal(sk_c9,u) equal(multiply(v,sk_c8),sk_c10)** equal(multiply(sk_c8,sk_c9),sk_c10)** -> . % 0.18/0.53 64[4:Spt:19.1] || -> equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.53 67[5:Spt:39.1] || -> equal(inverse(sk_c1),sk_c10)**. % 0.18/0.53 69[6:Spt:49.1] || -> equal(multiply(sk_c1,sk_c9),sk_c10)**. % 0.18/0.53 71[6:SpL:69.0,55.3] || equal(inverse(u),sk_c9)** equal(inverse(sk_c1),u)* equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c10)** equal(multiply(sk_c9,sk_c9),sk_c10)** -> . % 0.18/0.53 72[6:Rew:67.0,71.1] || equal(inverse(u),sk_c9)** equal(sk_c10,u) equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c10)** equal(multiply(sk_c9,sk_c9),sk_c10)** -> . % 0.18/0.53 73[6:Obv:72.1] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c10)** equal(multiply(sk_c9,sk_c9),sk_c10)** -> . % 0.18/0.53 77[2:SpR:57.0,53.0] || -> equal(multiply(sk_c9,sk_c10),identity)**. % 0.18/0.53 78[5:SpR:67.0,53.0] || -> equal(multiply(sk_c10,sk_c1),identity)**. % 0.18/0.53 92[0:SpR:53.0,54.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.18/0.53 93[2:SpR:77.0,54.0] || -> equal(multiply(sk_c9,multiply(sk_c10,u)),multiply(identity,u))**. % 0.18/0.53 94[5:SpR:78.0,54.0] || -> equal(multiply(sk_c10,multiply(sk_c1,u)),multiply(identity,u))**. % 0.18/0.53 96[2:Rew:52.0,93.0] || -> equal(multiply(sk_c9,multiply(sk_c10,u)),u)**. % 0.18/0.53 97[5:Rew:52.0,94.0] || -> equal(multiply(sk_c10,multiply(sk_c1,u)),u)**. % 0.18/0.53 98[0:Rew:52.0,92.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.18/0.53 102[3:SpR:59.0,96.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.18/0.53 103[5:SpR:78.0,96.0] || -> equal(multiply(sk_c9,identity),sk_c1)**. % 0.18/0.53 105[6:Rew:102.0,73.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c10)** equal(sk_c8,sk_c10) -> . % 0.18/0.53 112[5:SpR:103.0,54.0] || -> equal(multiply(sk_c9,multiply(identity,u)),multiply(sk_c1,u))**. % 0.18/0.53 115[5:Rew:52.0,112.0] || -> equal(multiply(sk_c1,u),multiply(sk_c9,u))**. % 0.18/0.53 116[6:Rew:115.0,69.0] || -> equal(multiply(sk_c9,sk_c9),sk_c10)**. % 0.18/0.53 118[5:Rew:115.0,97.0] || -> equal(multiply(sk_c10,multiply(sk_c9,u)),u)**. % 0.18/0.53 119[6:Rew:102.0,116.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.53 120[6:Rew:119.0,59.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.18/0.53 121[6:Rew:119.0,64.0] || -> equal(multiply(sk_c9,sk_c10),sk_c10)**. % 0.18/0.53 129[6:Rew:119.0,105.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c10)** equal(sk_c10,sk_c10) -> . % 0.18/0.53 130[6:Rew:77.0,121.0] || -> equal(identity,sk_c10)**. % 0.18/0.53 131[6:Rew:130.0,52.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 132[6:Rew:130.0,53.0] || -> equal(multiply(inverse(u),u),sk_c10)**. % 0.18/0.53 141[6:Rew:131.0,120.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 144[6:Rew:141.0,57.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.18/0.53 160[6:Obv:129.4] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c9) equal(sk_c10,u) equal(multiply(v,sk_c9),sk_c10)** -> . % 0.18/0.53 161[6:Rew:141.0,160.3,141.0,160.1,141.0,160.0] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(sk_c10,u) equal(multiply(v,sk_c10),sk_c10)** -> . % 0.18/0.53 188[0:SpR:98.0,98.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.18/0.53 192[6:SpR:132.0,98.0] || -> equal(multiply(inverse(inverse(u)),sk_c10),u)**. % 0.18/0.53 196[6:Rew:188.0,192.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.53 202[6:Rew:196.0,161.3] || equal(inverse(u),sk_c10)**+ equal(inverse(v),sk_c10)** equal(sk_c10,u) equal(v,sk_c10) -> . % 0.18/0.53 215[0:SpR:188.0,98.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.18/0.53 533[6:SpL:144.0,202.0] || equal(sk_c10,sk_c10) equal(inverse(u),sk_c10)** equal(sk_c10,sk_c10) equal(u,sk_c10) -> . % 0.18/0.53 537[6:Obv:533.2] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.18/0.53 539[6:SpL:144.0,537.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.18/0.53 543[6:Obv:539.1] || -> . % 0.18/0.53 544[6:Spt:543.0,49.1,69.0] || equal(multiply(sk_c1,sk_c9),sk_c10)** -> . % 0.18/0.53 545[6:Spt:543.0,49.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 546[6:Rew:115.0,544.0] || equal(multiply(sk_c9,sk_c9),sk_c10)** -> . % 0.18/0.53 547[6:Rew:102.0,546.0] || equal(sk_c8,sk_c10)** -> . % 0.18/0.53 550[5:Rew:102.0,46.1,115.0,46.1] || -> equal(inverse(sk_c4),sk_c7)** equal(sk_c8,sk_c10). % 0.18/0.53 551[6:MRR:550.1,547.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 559[5:Rew:102.0,47.1,115.0,47.1] || -> equal(multiply(sk_c7,sk_c9),sk_c10)** equal(sk_c8,sk_c10). % 0.18/0.53 560[6:MRR:559.1,547.0] || -> equal(multiply(sk_c7,sk_c9),sk_c10)**. % 0.18/0.53 561[5:Rew:102.0,45.1,115.0,45.1] || -> equal(multiply(sk_c4,sk_c7),sk_c10)** equal(sk_c8,sk_c10). % 0.18/0.53 562[6:MRR:561.1,547.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 589[6:SpR:551.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 620[6:SpR:560.0,54.0] || -> equal(multiply(sk_c7,multiply(sk_c9,u)),multiply(sk_c10,u))**. % 0.18/0.53 621[6:SpR:560.0,98.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c9)**. % 0.18/0.53 627[6:SpR:562.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 628[6:SpR:562.0,98.0] || -> equal(multiply(inverse(sk_c4),sk_c10),sk_c7)**. % 0.18/0.53 630[6:Rew:551.0,628.0] || -> equal(multiply(sk_c7,sk_c10),sk_c7)**. % 0.18/0.53 631[6:Rew:589.0,627.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 633[6:Rew:631.0,59.0] || -> equal(sk_c8,sk_c9)**. % 0.18/0.53 638[6:Rew:631.0,118.0] || -> equal(multiply(sk_c9,u),u)**. % 0.18/0.53 642[6:Rew:631.0,620.0] || -> equal(multiply(sk_c7,multiply(sk_c9,u)),u)**. % 0.18/0.53 653[6:Rew:633.0,547.0] || equal(sk_c9,sk_c10)** -> . % 0.18/0.53 687[6:Rew:638.0,642.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.53 691[6:Rew:687.0,630.0] || -> equal(sk_c7,sk_c10)**. % 0.18/0.53 701[6:Rew:691.0,621.0] || -> equal(multiply(inverse(sk_c10),sk_c10),sk_c9)**. % 0.18/0.53 712[6:Rew:57.0,701.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.18/0.53 713[6:Rew:638.0,712.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 714[6:MRR:713.0,653.0] || -> . % 0.18/0.53 722[5:Spt:714.0,39.1,67.0] || equal(inverse(sk_c1),sk_c10)** -> . % 0.18/0.53 723[5:Spt:714.0,39.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 725[5:MRR:36.1,722.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 727[5:MRR:32.1,722.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.18/0.53 730[5:MRR:35.0,722.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 732[5:MRR:31.0,722.0] || -> equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 740[5:SpR:725.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 745[5:SpR:727.0,98.0] || -> equal(multiply(sk_c10,multiply(sk_c2,u)),u)**. % 0.18/0.53 769[5:SpR:730.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 773[5:Rew:740.0,769.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 774[5:Rew:773.0,59.0] || -> equal(sk_c8,sk_c9)**. % 0.18/0.53 775[5:Rew:773.0,745.0] || -> equal(multiply(sk_c2,u),u)**. % 0.18/0.53 791[5:Rew:774.0,63.0] || equal(inverse(u),sk_c9)** equal(inverse(v),sk_c8) equal(sk_c9,u) equal(multiply(v,sk_c8),sk_c10)** equal(multiply(sk_c8,sk_c9),sk_c10)** -> . % 0.18/0.53 793[5:Rew:775.0,732.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 794[5:Rew:793.0,57.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.18/0.53 796[5:Rew:793.0,77.0] || -> equal(multiply(sk_c10,sk_c10),identity)**. % 0.18/0.53 807[5:Rew:793.0,774.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.53 813[5:Rew:773.0,796.0] || -> equal(identity,sk_c10)**. % 0.18/0.53 816[5:Rew:813.0,53.0] || -> equal(multiply(inverse(u),u),sk_c10)**. % 0.18/0.53 852[5:Rew:773.0,791.4,807.0,791.4,793.0,791.4,807.0,791.3,793.0,791.2,807.0,791.1,793.0,791.0] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(sk_c10,u) equal(multiply(v,sk_c10),sk_c10)** equal(sk_c10,sk_c10) -> . % 0.18/0.53 853[5:Obv:852.4] || equal(inverse(u),sk_c10)** equal(inverse(v),sk_c10) equal(sk_c10,u) equal(multiply(v,sk_c10),sk_c10)** -> . % 0.18/0.53 896[5:SpR:816.0,215.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.53 908[5:Rew:896.0,853.3] || equal(inverse(u),sk_c10)**+ equal(inverse(v),sk_c10)** equal(sk_c10,u) equal(v,sk_c10) -> . % 0.18/0.53 1007[5:SpL:794.0,908.0] || equal(sk_c10,sk_c10) equal(inverse(u),sk_c10)** equal(sk_c10,sk_c10) equal(u,sk_c10) -> . % 0.18/0.53 1009[5:Obv:1007.2] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.18/0.53 1011[5:SpL:794.0,1009.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.18/0.53 1013[5:Obv:1011.1] || -> . % 0.18/0.53 1014[4:Spt:1013.0,19.1,64.0] || equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.18/0.53 1015[4:Spt:1013.0,19.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 1017[4:MRR:16.1,1014.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 1019[4:MRR:12.1,1014.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.18/0.53 1022[4:MRR:15.1,1014.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 1024[4:MRR:11.1,1014.0] || -> equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 1035[4:SpR:1017.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 1040[4:SpR:1019.0,98.0] || -> equal(multiply(sk_c10,multiply(sk_c2,u)),u)**. % 0.18/0.53 1061[4:SpR:1022.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 1065[4:Rew:1035.0,1061.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 1066[4:Rew:1065.0,59.0] || -> equal(sk_c8,sk_c9)**. % 0.18/0.53 1067[4:Rew:1065.0,1040.0] || -> equal(multiply(sk_c2,u),u)**. % 0.18/0.53 1077[4:Rew:1066.0,1014.0] || equal(multiply(sk_c9,sk_c9),sk_c10)** -> . % 0.18/0.53 1082[4:Rew:1067.0,1024.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 1118[4:Rew:1065.0,1077.0,1082.0,1077.0] || equal(sk_c10,sk_c10)* -> . % 0.18/0.53 1119[4:Obv:1118.0] || -> . % 0.18/0.53 1149[3:Spt:1119.0,29.1,59.0] || equal(multiply(sk_c10,sk_c8),sk_c9)** -> . % 0.18/0.53 1150[3:Spt:1119.0,29.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 1152[3:MRR:26.1,1149.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 1153[3:MRR:24.1,1149.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.18/0.53 1154[3:MRR:22.1,1149.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.18/0.53 1157[3:MRR:25.1,1149.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 1158[3:MRR:23.1,1149.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.18/0.53 1159[3:MRR:21.1,1149.0] || -> equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 1170[3:SpR:1152.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 1173[3:SpR:1153.0,215.0] || -> equal(multiply(sk_c3,multiply(sk_c9,u)),u)**. % 0.18/0.53 1175[3:SpR:1154.0,98.0] || -> equal(multiply(sk_c10,multiply(sk_c2,u)),u)**. % 0.18/0.53 1189[3:SpR:1157.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 1193[3:Rew:1170.0,1189.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 1194[3:Rew:1193.0,1175.0] || -> equal(multiply(sk_c2,u),u)**. % 0.18/0.53 1198[3:Rew:1193.0,1149.0] || equal(sk_c8,sk_c9)** -> . % 0.18/0.53 1202[3:Rew:1194.0,1159.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 1208[3:Rew:1202.0,1173.0] || -> equal(multiply(sk_c3,multiply(sk_c10,u)),u)**. % 0.18/0.53 1209[3:Rew:1202.0,1158.0] || -> equal(multiply(sk_c3,sk_c10),sk_c8)**. % 0.18/0.53 1217[3:Rew:1202.0,1198.0] || equal(sk_c8,sk_c10)** -> . % 0.18/0.53 1240[3:Rew:1193.0,1208.0] || -> equal(multiply(sk_c3,u),u)**. % 0.18/0.53 1241[3:Rew:1240.0,1209.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.53 1242[3:MRR:1241.0,1217.0] || -> . % 0.18/0.53 1261[2:Spt:1242.0,9.1,57.0] || equal(inverse(sk_c10),sk_c9)** -> . % 0.18/0.53 1262[2:Spt:1242.0,9.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 1263[2:MRR:8.1,1261.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.18/0.53 1264[2:MRR:6.1,1261.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 1266[2:MRR:2.1,1261.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.18/0.53 1267[2:MRR:10.0,1261.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.53 1268[2:MRR:7.0,1261.0] || -> equal(multiply(sk_c7,sk_c9),sk_c10)**. % 0.18/0.53 1269[2:MRR:5.0,1261.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 1271[2:MRR:1.0,1261.0] || -> equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 1272[2:SpR:1262.0,98.0] || -> equal(multiply(sk_c7,multiply(sk_c5,u)),u)**. % 0.18/0.53 1279[2:SpR:1264.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 1284[2:SpR:1266.0,98.0] || -> equal(multiply(sk_c10,multiply(sk_c2,u)),u)**. % 0.18/0.53 1288[2:SpR:1267.0,98.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.18/0.53 1290[2:Rew:1263.0,1288.0] || -> equal(multiply(sk_c5,sk_c5),sk_c7)**. % 0.18/0.53 1294[2:SpR:1269.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 1295[2:SpR:1269.0,98.0] || -> equal(multiply(inverse(sk_c4),sk_c10),sk_c7)**. % 0.18/0.53 1297[2:Rew:1264.0,1295.0] || -> equal(multiply(sk_c7,sk_c10),sk_c7)**. % 0.18/0.53 1298[2:Rew:1279.0,1294.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 1299[2:Rew:1298.0,1284.0] || -> equal(multiply(sk_c2,u),u)**. % 0.18/0.53 1302[2:Rew:1299.0,1271.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 1304[2:Rew:1302.0,1261.0] || equal(inverse(sk_c10),sk_c10)** -> . % 0.18/0.53 1305[2:Rew:1302.0,1268.0] || -> equal(multiply(sk_c7,sk_c10),sk_c10)**. % 0.18/0.53 1315[2:Rew:1297.0,1305.0] || -> equal(sk_c7,sk_c10)**. % 0.18/0.53 1316[2:Rew:1315.0,1262.0] || -> equal(inverse(sk_c5),sk_c10)**. % 0.18/0.53 1320[2:Rew:1315.0,1272.0] || -> equal(multiply(sk_c10,multiply(sk_c5,u)),u)**. % 0.18/0.53 1325[2:Rew:1315.0,1290.0] || -> equal(multiply(sk_c5,sk_c5),sk_c10)**. % 0.18/0.53 1335[2:Rew:1298.0,1320.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.53 1336[2:Rew:1335.0,1325.0] || -> equal(sk_c5,sk_c10)**. % 0.18/0.53 1340[2:Rew:1336.0,1316.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.18/0.53 1343[2:MRR:1340.0,1304.0] || -> . % 0.18/0.53 1350[1:Spt:1343.0,51.3,51.4,51.5,51.6,51.10,51.11,51.12,51.13,51.14] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(inverse(sk_c10),sk_c9) equal(multiply(u,sk_c9),sk_c8)**+ equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.18/0.53 1352[2:Spt:8.1] || -> equal(inverse(sk_c10),sk_c9)**. % 0.18/0.53 1353[2:Rew:1352.0,1350.3] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(sk_c9,sk_c9) equal(multiply(u,sk_c9),sk_c8)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.18/0.53 1355[2:Obv:1353.3] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c9),sk_c8)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(sk_c10,sk_c8),sk_c9) equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.18/0.53 1357[2:SpR:1352.0,98.0] || -> equal(multiply(sk_c9,multiply(sk_c10,u)),u)**. % 0.18/0.53 1358[2:SpR:1352.0,215.0] || -> equal(multiply(sk_c10,multiply(sk_c9,u)),u)**. % 0.18/0.53 1360[3:Spt:19.1] || -> equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.53 1362[3:Rew:1360.0,1355.7] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c9),sk_c8)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(sk_c10,sk_c10) -> . % 0.18/0.53 1363[3:Obv:1362.7] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c9),sk_c8)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** equal(multiply(sk_c10,sk_c8),sk_c9)** -> . % 0.18/0.53 1366[3:SpR:1360.0,98.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c8)**. % 0.18/0.53 1368[4:Spt:28.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.53 1370[4:Rew:1368.0,1363.6] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c9),sk_c8)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** equal(sk_c9,sk_c9) -> . % 0.18/0.53 1371[4:Obv:1370.6] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c9),sk_c8)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** -> . % 0.18/0.53 1374[4:SpR:1368.0,98.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.18/0.53 1376[4:Rew:1352.0,1374.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.18/0.53 1377[5:Spt:39.1] || -> equal(inverse(sk_c1),sk_c10)**. % 0.18/0.53 1381[6:Spt:49.1] || -> equal(multiply(sk_c1,sk_c9),sk_c10)**. % 0.18/0.53 1383[6:SpR:1381.0,98.0] || -> equal(multiply(inverse(sk_c1),sk_c10),sk_c9)**. % 0.18/0.53 1385[6:Rew:1377.0,1383.0] || -> equal(multiply(sk_c10,sk_c10),sk_c9)**. % 0.18/0.53 1391[4:SpR:1376.0,98.0] || -> equal(multiply(inverse(sk_c9),sk_c8),sk_c9)**. % 0.18/0.53 1393[6:SpR:1385.0,54.0] || -> equal(multiply(sk_c10,multiply(sk_c10,u)),multiply(sk_c9,u))**. % 0.18/0.53 1394[6:SpR:1385.0,98.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c10)**. % 0.18/0.53 1396[6:Rew:1376.0,1394.0,1352.0,1394.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.53 1400[6:Rew:1396.0,1366.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c10)**. % 0.18/0.53 1404[6:Rew:1396.0,1371.3] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c9),sk_c10)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** -> . % 0.18/0.53 1406[6:Rew:1396.0,1391.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c9)**. % 0.18/0.53 1407[6:Rew:1400.0,1406.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 1408[6:Rew:1407.0,1352.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.18/0.53 1411[6:Rew:1407.0,1357.0] || -> equal(multiply(sk_c10,multiply(sk_c10,u)),u)**. % 0.18/0.53 1418[6:Rew:1411.0,1393.0,1407.0,1393.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 1425[6:Rew:1407.0,1404.5,1407.0,1404.4,1407.0,1404.3,1407.0,1404.0] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c10),sk_c10)** equal(multiply(v,sk_c10),sk_c10)** equal(multiply(w,sk_c10),sk_c10)** -> . % 0.18/0.53 1426[6:Con:1425.1] || equal(inverse(u),sk_c10) equal(multiply(u,sk_c10),sk_c10)** -> . % 0.18/0.53 1432[0:SpR:53.0,98.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.53 1433[0:SpR:53.0,215.0] || -> equal(multiply(u,identity),u)**. % 0.18/0.53 1435[5:SpR:1377.0,53.0] || -> equal(multiply(sk_c10,sk_c1),identity)**. % 0.18/0.53 1436[6:Rew:1418.0,1435.0] || -> equal(identity,sk_c1)**. % 0.18/0.53 1438[6:Rew:1436.0,53.0] || -> equal(multiply(inverse(u),u),sk_c1)**. % 0.18/0.53 1440[6:Rew:1436.0,1433.0] || -> equal(multiply(u,sk_c1),u)**. % 0.18/0.53 1468[6:SpR:1408.0,1438.0] || -> equal(multiply(sk_c10,sk_c10),sk_c1)**. % 0.18/0.53 1469[6:Rew:1418.0,1468.0] || -> equal(sk_c1,sk_c10)**. % 0.18/0.53 1474[6:Rew:1469.0,1440.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.53 1475[6:Rew:1474.0,1426.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.18/0.53 1500[6:SpL:1408.0,1475.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.18/0.53 1501[6:Obv:1500.1] || -> . % 0.18/0.53 1502[6:Spt:1501.0,49.1,1381.0] || equal(multiply(sk_c1,sk_c9),sk_c10)** -> . % 0.18/0.53 1503[6:Spt:1501.0,49.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 1504[0:Rew:1433.0,1432.0] || -> equal(inverse(inverse(u)),u)**. % 0.18/0.53 1506[6:MRR:46.1,1502.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 1512[6:MRR:45.1,1502.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 1529[6:SpR:1506.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 1552[5:SpR:1435.0,98.0] || -> equal(multiply(inverse(sk_c10),identity),sk_c1)**. % 0.18/0.53 1554[5:Rew:1352.0,1552.0] || -> equal(multiply(sk_c9,identity),sk_c1)**. % 0.18/0.53 1555[5:Rew:1433.0,1554.0] || -> equal(sk_c1,sk_c9)**. % 0.18/0.53 1556[5:Rew:1555.0,1377.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.53 1558[6:Rew:1555.0,1502.0] || equal(multiply(sk_c9,sk_c9),sk_c10)** -> . % 0.18/0.53 1562[5:Rew:1556.0,1366.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.18/0.53 1563[6:Rew:1376.0,1558.0] || equal(sk_c8,sk_c10)** -> . % 0.18/0.53 1572[6:SpR:1512.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 1576[6:Rew:1529.0,1572.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 1577[6:Rew:1576.0,1368.0] || -> equal(sk_c8,sk_c9)**. % 0.18/0.53 1578[6:Rew:1576.0,1562.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.53 1589[6:Rew:1577.0,1563.0] || equal(sk_c9,sk_c10)** -> . % 0.18/0.53 1594[6:Rew:1577.0,1578.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 1610[6:Rew:1594.0,1589.0] || equal(sk_c10,sk_c10)* -> . % 0.18/0.53 1611[6:Obv:1610.0] || -> . % 0.18/0.53 1661[5:Spt:1611.0,39.1,1377.0] || equal(inverse(sk_c1),sk_c10)** -> . % 0.18/0.53 1662[5:Spt:1611.0,39.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 1664[5:MRR:36.1,1661.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 1666[5:MRR:32.1,1661.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.18/0.53 1669[5:MRR:35.0,1661.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 1671[5:MRR:31.0,1661.0] || -> equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 1682[5:SpR:1664.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 1687[5:SpR:1666.0,98.0] || -> equal(multiply(sk_c10,multiply(sk_c2,u)),u)**. % 0.18/0.53 1707[5:SpR:1669.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 1711[5:Rew:1682.0,1707.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 1712[5:Rew:1711.0,1368.0] || -> equal(sk_c8,sk_c9)**. % 0.18/0.53 1713[5:Rew:1711.0,1687.0] || -> equal(multiply(sk_c2,u),u)**. % 0.18/0.53 1726[5:Rew:1712.0,1371.3] || equal(inverse(u),sk_c9) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c9),sk_c9)** equal(multiply(v,sk_c10),sk_c9)** equal(multiply(w,sk_c9),sk_c10)** -> . % 0.18/0.53 1728[5:Rew:1713.0,1671.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 1729[5:Rew:1728.0,1352.0] || -> equal(inverse(sk_c10),sk_c10)**. % 0.18/0.53 1774[5:Rew:1728.0,1726.5,1728.0,1726.4,1728.0,1726.3,1728.0,1726.0] || equal(inverse(u),sk_c10) equal(inverse(v),sk_c10) equal(inverse(w),sk_c10) equal(multiply(u,sk_c10),sk_c10)** equal(multiply(v,sk_c10),sk_c10)** equal(multiply(w,sk_c10),sk_c10)** -> . % 0.18/0.53 1775[5:Con:1774.1] || equal(inverse(u),sk_c10) equal(multiply(u,sk_c10),sk_c10)** -> . % 0.18/0.53 1842[5:SpR:1711.0,1433.0] || -> equal(identity,sk_c10)**. % 0.18/0.53 1846[5:Rew:1842.0,1433.0] || -> equal(multiply(u,sk_c10),u)**. % 0.18/0.53 1850[5:Rew:1846.0,1775.1] || equal(inverse(u),sk_c10)** equal(u,sk_c10) -> . % 0.18/0.53 1882[5:SpL:1729.0,1850.0] || equal(sk_c10,sk_c10)* equal(sk_c10,sk_c10)* -> . % 0.18/0.53 1884[5:Obv:1882.1] || -> . % 0.18/0.53 1885[4:Spt:1884.0,28.1,1368.0] || equal(multiply(sk_c10,sk_c8),sk_c9)** -> . % 0.18/0.53 1886[4:Spt:1884.0,28.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.18/0.53 1887[4:MRR:26.1,1885.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 1888[4:MRR:24.1,1885.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.18/0.53 1893[4:MRR:25.1,1885.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 1894[4:MRR:23.1,1885.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.18/0.53 1906[4:SpR:1887.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 1919[2:SpR:1352.0,1504.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.53 1921[3:Rew:1919.0,1366.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.18/0.53 1924[4:SpR:1888.0,1504.0] || -> equal(inverse(sk_c9),sk_c3)**. % 0.18/0.53 1926[4:Rew:1919.0,1924.0] || -> equal(sk_c3,sk_c10)**. % 0.18/0.53 1928[4:Rew:1926.0,1894.0] || -> equal(multiply(sk_c10,sk_c9),sk_c8)**. % 0.18/0.53 1958[4:SpR:1893.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 1962[4:Rew:1906.0,1958.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 1963[4:Rew:1962.0,1921.0] || -> equal(sk_c8,sk_c10)**. % 0.18/0.53 1964[4:Rew:1962.0,1928.0] || -> equal(sk_c8,sk_c9)**. % 0.18/0.53 1966[4:Rew:1962.0,1885.0] || equal(sk_c8,sk_c9)** -> . % 0.18/0.53 1971[4:Rew:1963.0,1964.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 1978[4:Rew:1963.0,1966.0,1971.0,1966.0] || equal(sk_c10,sk_c10)* -> . % 0.18/0.53 1979[4:Obv:1978.0] || -> . % 0.18/0.53 2002[3:Spt:1979.0,19.1,1360.0] || equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.18/0.53 2003[3:Spt:1979.0,19.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 2005[3:MRR:16.1,2002.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 2006[3:MRR:14.1,2002.0] || -> equal(inverse(sk_c3),sk_c9)**. % 0.18/0.53 2007[3:MRR:12.1,2002.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.18/0.53 2010[3:MRR:15.1,2002.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 2011[3:MRR:13.1,2002.0] || -> equal(multiply(sk_c3,sk_c9),sk_c8)**. % 0.18/0.53 2012[3:MRR:11.1,2002.0] || -> equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 2036[3:SpR:2005.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 2048[3:SpR:2006.0,1504.0] || -> equal(inverse(sk_c9),sk_c3)**. % 0.18/0.53 2050[3:Rew:1919.0,2048.0] || -> equal(sk_c3,sk_c10)**. % 0.18/0.53 2052[3:Rew:2050.0,2011.0] || -> equal(multiply(sk_c10,sk_c9),sk_c8)**. % 0.18/0.53 2057[3:SpR:2007.0,1504.0] || -> equal(inverse(sk_c10),sk_c2)**. % 0.18/0.53 2059[3:Rew:1352.0,2057.0] || -> equal(sk_c2,sk_c9)**. % 0.18/0.53 2061[3:Rew:2059.0,2012.0] || -> equal(multiply(sk_c9,sk_c10),sk_c9)**. % 0.18/0.53 2074[3:SpR:2010.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 2078[3:Rew:2036.0,2074.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 2079[3:Rew:2078.0,2052.0] || -> equal(sk_c8,sk_c9)**. % 0.18/0.53 2080[3:Rew:2078.0,1358.0] || -> equal(multiply(sk_c9,u),u)**. % 0.18/0.53 2083[3:Rew:2079.0,2002.0] || equal(multiply(sk_c9,sk_c9),sk_c10)** -> . % 0.18/0.53 2084[3:Rew:2080.0,2061.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 2108[3:Rew:2078.0,2083.0,2084.0,2083.0] || equal(sk_c10,sk_c10)* -> . % 0.18/0.53 2109[3:Obv:2108.0] || -> . % 0.18/0.53 2113[2:Spt:2109.0,8.1,1352.0] || equal(inverse(sk_c10),sk_c9)** -> . % 0.18/0.53 2114[2:Spt:2109.0,8.0] || -> equal(inverse(sk_c6),sk_c5)**. % 0.18/0.53 2115[2:MRR:6.1,2113.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.53 2117[2:MRR:2.1,2113.0] || -> equal(inverse(sk_c2),sk_c10)**. % 0.18/0.53 2118[2:MRR:9.1,2113.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.53 2119[2:MRR:10.0,2113.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.18/0.53 2120[2:MRR:7.0,2113.0] || -> equal(multiply(sk_c7,sk_c9),sk_c10)**. % 0.18/0.53 2121[2:MRR:5.0,2113.0] || -> equal(multiply(sk_c4,sk_c7),sk_c10)**. % 0.18/0.53 2123[2:MRR:1.0,2113.0] || -> equal(multiply(sk_c2,sk_c10),sk_c9)**. % 0.18/0.53 2126[2:SpR:2114.0,1504.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.53 2128[2:Rew:2118.0,2126.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.53 2129[2:Rew:2128.0,2114.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.53 2130[2:Rew:2128.0,2119.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.18/0.53 2135[2:SpR:2115.0,215.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),u)**. % 0.18/0.53 2136[2:SpR:2115.0,1504.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.18/0.53 2138[2:Rew:2129.0,2136.0] || -> equal(sk_c5,sk_c4)**. % 0.18/0.53 2140[2:Rew:2138.0,2129.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.18/0.53 2141[2:Rew:2138.0,2130.0] || -> equal(multiply(sk_c7,sk_c7),sk_c4)**. % 0.18/0.53 2149[2:SpR:2117.0,98.0] || -> equal(multiply(sk_c10,multiply(sk_c2,u)),u)**. % 0.18/0.53 2151[2:SpR:2117.0,1504.0] || -> equal(inverse(sk_c10),sk_c2)**. % 0.18/0.53 2153[2:Rew:2151.0,2113.0] || equal(sk_c2,sk_c9)** -> . % 0.18/0.53 2170[2:SpR:2121.0,54.0] || -> equal(multiply(sk_c4,multiply(sk_c7,u)),multiply(sk_c10,u))**. % 0.18/0.53 2171[2:SpR:2121.0,98.0] || -> equal(multiply(inverse(sk_c4),sk_c10),sk_c7)**. % 0.18/0.53 2173[2:Rew:2115.0,2171.0] || -> equal(multiply(sk_c7,sk_c10),sk_c7)**. % 0.18/0.53 2174[2:Rew:2135.0,2170.0] || -> equal(multiply(sk_c10,u),u)**. % 0.18/0.53 2175[2:Rew:2174.0,2149.0] || -> equal(multiply(sk_c2,u),u)**. % 0.18/0.53 2178[2:Rew:2175.0,2123.0] || -> equal(sk_c9,sk_c10)**. % 0.18/0.53 2181[2:Rew:2178.0,2153.0] || equal(sk_c2,sk_c10)** -> . % 0.18/0.53 2182[2:Rew:2178.0,2120.0] || -> equal(multiply(sk_c7,sk_c10),sk_c10)**. % 0.18/0.53 2189[2:Rew:2173.0,2182.0] || -> equal(sk_c7,sk_c10)**. % 0.18/0.53 2192[2:Rew:2189.0,2140.0] || -> equal(inverse(sk_c10),sk_c4)**. % 0.18/0.53 2194[2:Rew:2189.0,2141.0] || -> equal(multiply(sk_c10,sk_c10),sk_c4)**. % 0.18/0.53 2198[2:Rew:2151.0,2192.0] || -> equal(sk_c4,sk_c2)**. % 0.18/0.53 2204[2:Rew:2174.0,2194.0,2198.0,2194.0] || -> equal(sk_c2,sk_c10)**. % 0.18/0.53 2205[2:MRR:2204.0,2181.0] || -> . % 0.18/0.53 % SZS output end Refutation % 0.18/0.53 Formulae used in the proof : prove_this_1 prove_this_2 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_19 prove_this_21 prove_this_22 prove_this_23 prove_this_24 prove_this_25 prove_this_26 prove_this_28 prove_this_29 prove_this_31 prove_this_32 prove_this_35 prove_this_36 prove_this_39 prove_this_45 prove_this_46 prove_this_47 prove_this_49 prove_this_51 left_identity left_inverse associativity % 0.18/0.53 %------------------------------------------------------------------------------