%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP309-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:46:47 EDT 2022 % Result : Unsatisfiable 0.18s 0.46s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : GRP309-1 : TPTP v8.1.0. Released v2.5.0. % 0.00/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n015.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 19:32:53 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.46 % 0.18/0.46 SPASS V 3.9 % 0.18/0.46 SPASS beiseite: Proof found. % 0.18/0.46 % SZS status Theorem % 0.18/0.46 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.46 SPASS derived 766 clauses, backtracked 327 clauses, performed 10 splits and kept 590 clauses. % 0.18/0.46 SPASS allocated 63593 KBytes. % 0.18/0.46 SPASS spent 0:00:00.12 on the problem. % 0.18/0.46 0:00:00.03 for the input. % 0.18/0.46 0:00:00.00 for the FLOTTER CNF translation. % 0.18/0.46 0:00:00.00 for inferences. % 0.18/0.46 0:00:00.00 for the backtracking. % 0.18/0.46 0:00:00.05 for the reduction. % 0.18/0.46 % 0.18/0.46 % 0.18/0.46 Here is a proof with depth 5, length 305 : % 0.18/0.46 % SZS output start Refutation % 0.18/0.46 1[0:Inp] || -> equal(multiply(sk_c3,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5). % 0.18/0.46 2[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.46 3[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5)** equal(multiply(sk_c7,sk_c6),sk_c5). % 0.18/0.46 4[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.46 5[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.46 6[0:Inp] || -> equal(inverse(sk_c3),sk_c7)** equal(inverse(sk_c7),sk_c5). % 0.18/0.46 7[0:Inp] || -> equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.18/0.46 8[0:Inp] || -> equal(inverse(sk_c4),sk_c6)** equal(inverse(sk_c7),sk_c5). % 0.18/0.46 9[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.18/0.46 10[0:Inp] || -> equal(multiply(sk_c3,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c2),sk_c6). % 0.18/0.46 11[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.46 12[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5)** equal(multiply(sk_c7,sk_c2),sk_c6). % 0.18/0.46 13[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.46 14[0:Inp] || -> equal(multiply(sk_c3,sk_c7),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.46 15[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.46 16[0:Inp] || -> equal(multiply(sk_c4,sk_c6),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.46 17[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.46 18[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.46 19[0:Inp] || -> equal(inverse(sk_c3),sk_c7) equal(inverse(sk_c1),sk_c7)**. % 0.18/0.46 20[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.18/0.46 21[0:Inp] || -> equal(inverse(sk_c4),sk_c6) equal(inverse(sk_c1),sk_c7)**. % 0.18/0.46 22[0:Inp] || equal(multiply(sk_c7,sk_c6),sk_c5) equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c5,sk_c6),sk_c7)** equal(multiply(sk_c7,u),sk_c6)** equal(multiply(v,sk_c7),u)* equal(inverse(v),sk_c7) equal(multiply(w,sk_c7),sk_c6)** equal(inverse(w),sk_c7) equal(multiply(x,sk_c6),sk_c5)** equal(inverse(x),sk_c6) -> . % 0.18/0.46 23[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.18/0.46 24[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.18/0.46 25[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.18/0.46 26[0:Rew:9.0,22.2] || equal(multiply(sk_c7,sk_c6),sk_c5)** equal(inverse(sk_c7),sk_c5) equal(sk_c7,sk_c7) equal(multiply(sk_c7,u),sk_c6)** equal(multiply(v,sk_c7),u)* equal(inverse(v),sk_c7) equal(multiply(w,sk_c7),sk_c6)** equal(inverse(w),sk_c7) equal(multiply(x,sk_c6),sk_c5)** equal(inverse(x),sk_c6) -> . % 0.18/0.46 27[0:Obv:26.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(w),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(w,sk_c7),x)*+ equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c7,x),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.18/0.46 28[1:Spt:27.2,27.4,27.7] || equal(inverse(u),sk_c7) equal(multiply(u,sk_c7),v)*+ equal(multiply(sk_c7,v),sk_c6)** -> . % 0.18/0.46 30[2:Spt:8.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.46 32[3:Spt:6.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.46 35[4:Spt:7.1] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.18/0.46 37[5:Spt:5.1] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.46 43[1:SpL:23.0,28.1] || equal(inverse(identity),sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.46 45[2:SpR:30.0,24.0] || -> equal(multiply(sk_c6,sk_c4),identity)**. % 0.18/0.46 46[3:SpR:32.0,24.0] || -> equal(multiply(sk_c7,sk_c3),identity)**. % 0.18/0.46 47[1:SpL:24.0,28.1] || equal(inverse(inverse(sk_c7)),sk_c7) equal(identity,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.46 52[0:SpR:9.0,25.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.18/0.46 55[0:SpR:24.0,25.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.18/0.46 56[2:SpR:45.0,25.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),multiply(identity,u))**. % 0.18/0.46 58[2:Rew:23.0,56.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),u)**. % 0.18/0.46 59[0:Rew:23.0,55.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.18/0.46 66[4:SpR:35.0,58.0] || -> equal(multiply(sk_c6,sk_c5),sk_c6)**. % 0.18/0.46 75[0:SpR:59.0,59.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.18/0.46 78[3:SpR:46.0,59.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c3)**. % 0.18/0.46 80[0:SpR:9.0,59.0] || -> equal(multiply(inverse(sk_c5),sk_c7),sk_c6)**. % 0.18/0.46 83[0:SpR:24.0,59.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.46 84[2:SpR:45.0,59.0] || -> equal(multiply(inverse(sk_c6),identity),sk_c4)**. % 0.18/0.46 86[4:SpR:66.0,59.0] || -> equal(multiply(inverse(sk_c6),sk_c6),sk_c5)**. % 0.18/0.46 92[4:Rew:24.0,86.0] || -> equal(identity,sk_c5)**. % 0.18/0.46 93[4:Rew:92.0,23.0] || -> equal(multiply(sk_c5,u),u)**. % 0.18/0.46 96[4:Rew:92.0,46.0] || -> equal(multiply(sk_c7,sk_c3),sk_c5)**. % 0.18/0.46 99[4:Rew:92.0,47.1] || equal(inverse(inverse(sk_c7)),sk_c7) equal(sk_c5,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.46 100[4:Rew:92.0,78.0] || -> equal(multiply(inverse(sk_c7),sk_c5),sk_c3)**. % 0.18/0.46 101[4:Rew:92.0,84.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c4)**. % 0.18/0.46 102[4:Rew:93.0,9.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 108[4:Rew:102.0,35.0] || -> equal(multiply(sk_c4,sk_c7),sk_c5)**. % 0.18/0.46 109[5:Rew:102.0,37.0] || -> equal(multiply(sk_c3,sk_c7),sk_c7)**. % 0.18/0.46 119[4:Rew:100.0,101.0,102.0,101.0] || -> equal(sk_c4,sk_c3)**. % 0.18/0.46 122[4:Rew:119.0,108.0] || -> equal(multiply(sk_c3,sk_c7),sk_c5)**. % 0.18/0.46 123[5:Rew:109.0,122.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 125[5:Rew:123.0,93.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.46 126[5:Rew:123.0,96.0] || -> equal(multiply(sk_c7,sk_c3),sk_c7)**. % 0.18/0.46 132[5:Rew:125.0,126.0] || -> equal(sk_c3,sk_c7)**. % 0.18/0.46 133[5:Rew:132.0,32.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 158[5:Rew:125.0,99.2,102.0,99.2,123.0,99.1,133.0,99.0,133.0,99.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.18/0.46 159[5:Obv:158.1] || equal(u,sk_c7)* -> . % 0.18/0.46 160[5:UnC:159.0,59.0] || -> . % 0.18/0.46 163[5:Spt:160.0,5.1,37.0] || equal(multiply(sk_c3,sk_c7),sk_c6)** -> . % 0.18/0.46 164[5:Spt:160.0,5.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.46 165[5:Rew:93.0,100.0,164.0,100.0] || -> equal(sk_c3,sk_c5)**. % 0.18/0.46 168[5:Rew:165.0,122.0] || -> equal(multiply(sk_c5,sk_c7),sk_c5)**. % 0.18/0.46 170[5:Rew:93.0,168.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 172[5:Rew:170.0,164.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 174[5:Rew:170.0,93.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.46 201[5:Rew:174.0,99.2,102.0,99.2,170.0,99.1,172.0,99.0,172.0,99.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.18/0.46 202[5:Obv:201.1] || equal(u,sk_c7)* -> . % 0.18/0.46 203[5:UnC:202.0,59.0] || -> . % 0.18/0.46 206[4:Spt:203.0,7.1,35.0] || equal(multiply(sk_c4,sk_c6),sk_c5)** -> . % 0.18/0.46 207[4:Spt:203.0,7.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.46 208[4:Rew:207.0,78.0] || -> equal(multiply(sk_c5,identity),sk_c3)**. % 0.18/0.46 209[0:Rew:75.0,83.0] || -> equal(multiply(u,identity),u)**. % 0.18/0.46 210[4:Rew:209.0,208.0] || -> equal(sk_c3,sk_c5)**. % 0.18/0.46 211[2:Rew:209.0,84.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.18/0.46 212[4:Rew:210.0,32.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.46 213[4:Rew:210.0,46.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.18/0.46 215[4:Rew:212.0,80.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.18/0.46 220[4:MRR:20.1,206.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.46 224[4:MRR:16.0,206.0] || -> equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.46 225[4:MRR:12.0,206.0] || -> equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.46 226[4:MRR:3.0,206.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.46 259[4:SpR:224.0,59.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c7)**. % 0.18/0.46 261[4:Rew:220.0,259.0] || -> equal(multiply(sk_c7,sk_c2),sk_c7)**. % 0.18/0.46 262[4:Rew:225.0,261.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 267[4:Rew:262.0,215.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.18/0.46 274[4:Rew:262.0,226.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.18/0.46 277[4:Rew:262.0,43.2] || equal(inverse(identity),sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.18/0.46 283[4:Rew:267.0,274.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 284[4:Rew:283.0,207.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 287[4:Rew:283.0,213.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.18/0.46 292[4:Rew:267.0,287.0] || -> equal(identity,sk_c7)**. % 0.18/0.46 293[4:Rew:292.0,23.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.46 313[4:Rew:293.0,277.2,284.0,277.0,292.0,277.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.18/0.46 314[4:Obv:313.1] || equal(u,sk_c7)* -> . % 0.18/0.46 315[4:UnC:314.0,220.0] || -> . % 0.18/0.46 318[3:Spt:315.0,6.0,32.0] || equal(inverse(sk_c3),sk_c7)** -> . % 0.18/0.46 319[3:Spt:315.0,6.1] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.46 320[3:MRR:19.0,318.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.46 321[3:MRR:15.0,318.0] || -> equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.46 322[3:MRR:11.0,318.0] || -> equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.46 323[3:MRR:2.0,318.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.46 342[3:SpR:321.0,59.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c7)**. % 0.18/0.46 344[3:Rew:320.0,342.0] || -> equal(multiply(sk_c7,sk_c2),sk_c7)**. % 0.18/0.46 345[3:Rew:322.0,344.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 346[3:Rew:345.0,211.0] || -> equal(inverse(sk_c7),sk_c4)**. % 0.18/0.46 347[3:Rew:345.0,30.0] || -> equal(inverse(sk_c4),sk_c7)**. % 0.18/0.46 348[3:Rew:345.0,9.0] || -> equal(multiply(sk_c5,sk_c7),sk_c7)**. % 0.18/0.46 349[3:Rew:345.0,45.0] || -> equal(multiply(sk_c7,sk_c4),identity)**. % 0.18/0.46 350[3:Rew:345.0,80.0] || -> equal(multiply(inverse(sk_c5),sk_c7),sk_c7)**. % 0.18/0.46 355[3:Rew:345.0,323.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.18/0.46 358[3:Rew:345.0,43.2] || equal(inverse(identity),sk_c7) equal(sk_c7,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.18/0.46 361[3:Rew:319.0,346.0] || -> equal(sk_c4,sk_c5)**. % 0.18/0.46 362[3:Rew:361.0,347.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.46 363[3:Rew:361.0,349.0] || -> equal(multiply(sk_c7,sk_c5),identity)**. % 0.18/0.46 364[3:Rew:355.0,350.0,362.0,350.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 365[3:Rew:364.0,319.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 369[3:Rew:364.0,348.0] || -> equal(multiply(sk_c7,sk_c7),sk_c7)**. % 0.18/0.46 370[3:Rew:364.0,363.0] || -> equal(multiply(sk_c7,sk_c7),identity)**. % 0.18/0.46 372[3:Rew:369.0,370.0] || -> equal(identity,sk_c7)**. % 0.18/0.46 374[3:Rew:372.0,23.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.46 394[3:Rew:374.0,358.2,365.0,358.0,372.0,358.0] || equal(sk_c7,sk_c7)* equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.18/0.46 395[3:Obv:394.1] || equal(u,sk_c7)* -> . % 0.18/0.46 396[3:UnC:395.0,59.0] || -> . % 0.18/0.46 399[2:Spt:396.0,8.0,30.0] || equal(inverse(sk_c4),sk_c6)** -> . % 0.18/0.46 400[2:Spt:396.0,8.1] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.46 401[2:MRR:21.0,399.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.46 402[2:MRR:17.0,399.0] || -> equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.46 403[2:MRR:13.0,399.0] || -> equal(multiply(sk_c7,sk_c2),sk_c6)**. % 0.18/0.46 404[2:MRR:4.0,399.0] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.46 405[2:Rew:400.0,47.0] || equal(inverse(sk_c5),sk_c7) equal(identity,u) equal(multiply(sk_c7,u),sk_c6)** -> . % 0.18/0.46 406[2:SpR:400.0,59.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),u)**. % 0.18/0.46 414[2:SpR:402.0,59.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c7)**. % 0.18/0.46 416[2:Rew:401.0,414.0] || -> equal(multiply(sk_c7,sk_c2),sk_c7)**. % 0.18/0.46 417[2:Rew:403.0,416.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 421[2:Rew:417.0,52.0] || -> equal(multiply(sk_c5,multiply(sk_c7,u)),multiply(sk_c7,u))**. % 0.18/0.46 422[2:Rew:417.0,403.0] || -> equal(multiply(sk_c7,sk_c2),sk_c7)**. % 0.18/0.46 423[2:Rew:417.0,404.0] || -> equal(multiply(sk_c7,sk_c7),sk_c5)**. % 0.18/0.46 425[2:Rew:417.0,405.2] || equal(inverse(sk_c5),sk_c7) equal(identity,u) equal(multiply(sk_c7,u),sk_c7)** -> . % 0.18/0.46 429[2:Rew:406.0,421.0] || -> equal(multiply(sk_c7,u),u)**. % 0.18/0.46 430[2:Rew:429.0,423.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 431[2:Rew:429.0,422.0] || -> equal(sk_c2,sk_c7)**. % 0.18/0.46 435[2:Rew:430.0,400.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 443[2:Rew:429.0,425.2,435.0,425.0,430.0,425.0] || equal(sk_c7,sk_c7) equal(identity,u)* equal(u,sk_c7) -> . % 0.18/0.46 444[2:Obv:443.0] || equal(identity,u)* equal(u,sk_c7) -> . % 0.18/0.46 467[0:SpR:24.0,59.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.18/0.46 468[0:SpR:24.0,209.0] || -> equal(inverse(identity),identity)**. % 0.18/0.46 470[2:SpR:401.0,24.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.18/0.46 474[2:Rew:429.0,470.0] || -> equal(identity,sk_c1)**. % 0.18/0.46 478[2:Rew:474.0,444.0] || equal(sk_c1,u)* equal(u,sk_c7) -> . % 0.18/0.46 479[2:Rew:474.0,468.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.18/0.46 481[2:Rew:401.0,479.0] || -> equal(sk_c1,sk_c7)**. % 0.18/0.46 497[2:Rew:481.0,478.0] || equal(sk_c7,u)* equal(u,sk_c7)* -> . % 0.18/0.46 498[2:Obv:497.0] || equal(u,sk_c7)* -> . % 0.18/0.46 499[2:UnC:498.0,431.0] || -> . % 0.18/0.46 502[1:Spt:499.0,27.0,27.1,27.3,27.5,27.6,27.8] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(inverse(sk_c7),sk_c5) equal(multiply(u,sk_c6),sk_c5)**+ equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.18/0.46 503[0:Rew:209.0,467.0] || -> equal(inverse(inverse(u)),u)**. % 0.18/0.46 507[2:Spt:6.1] || -> equal(inverse(sk_c7),sk_c5)**. % 0.18/0.46 508[2:Rew:507.0,502.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(sk_c5,sk_c5) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.18/0.46 510[2:Obv:508.2] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.18/0.46 514[3:Spt:4.1] || -> equal(multiply(sk_c7,sk_c6),sk_c5)**. % 0.18/0.46 516[3:Rew:514.0,510.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.18/0.46 517[3:Obv:516.4] || equal(inverse(u),sk_c6) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** -> . % 0.18/0.46 523[4:Spt:21.1] || -> equal(inverse(sk_c1),sk_c7)**. % 0.18/0.46 529[5:Spt:17.1] || -> equal(multiply(sk_c1,sk_c7),sk_c2)**. % 0.18/0.46 531[5:SpR:529.0,59.0] || -> equal(multiply(inverse(sk_c1),sk_c2),sk_c7)**. % 0.18/0.46 533[5:Rew:523.0,531.0] || -> equal(multiply(sk_c7,sk_c2),sk_c7)**. % 0.18/0.46 534[5:Rew:533.0,12.1] || -> equal(multiply(sk_c4,sk_c6),sk_c5)** equal(sk_c6,sk_c7). % 0.18/0.46 535[5:Rew:533.0,10.1] || -> equal(multiply(sk_c3,sk_c7),sk_c6)** equal(sk_c6,sk_c7). % 0.18/0.46 536[5:Rew:533.0,11.1] || -> equal(inverse(sk_c3),sk_c7)** equal(sk_c6,sk_c7). % 0.18/0.46 537[5:Rew:533.0,13.1] || -> equal(inverse(sk_c4),sk_c6)** equal(sk_c6,sk_c7). % 0.18/0.46 545[5:SpR:533.0,59.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c2)**. % 0.18/0.46 547[5:Rew:507.0,545.0] || -> equal(multiply(sk_c5,sk_c7),sk_c2)**. % 0.18/0.46 565[0:SpR:503.0,59.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.18/0.46 568[2:SpR:507.0,503.0] || -> equal(inverse(sk_c5),sk_c7)**. % 0.18/0.46 569[4:SpR:523.0,503.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.18/0.46 574[4:Rew:507.0,569.0] || -> equal(sk_c1,sk_c5)**. % 0.18/0.46 584[2:SpR:507.0,24.0] || -> equal(multiply(sk_c5,sk_c7),identity)**. % 0.18/0.46 587[5:Rew:547.0,584.0] || -> equal(identity,sk_c2)**. % 0.18/0.46 588[5:Rew:587.0,468.0] || -> equal(inverse(sk_c2),sk_c2)**. % 0.18/0.46 590[5:Rew:587.0,209.0] || -> equal(multiply(u,sk_c2),u)**. % 0.18/0.46 646[6:Spt:536.1] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 648[6:Rew:646.0,9.0] || -> equal(multiply(sk_c5,sk_c7),sk_c7)**. % 0.18/0.46 655[6:Rew:646.0,517.0] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c5)** equal(multiply(v,sk_c7),sk_c6)** -> . % 0.18/0.46 657[6:Rew:547.0,648.0] || -> equal(sk_c2,sk_c7)**. % 0.18/0.46 660[6:Rew:657.0,588.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 664[6:Rew:657.0,590.0] || -> equal(multiply(u,sk_c7),u)**. % 0.18/0.46 667[6:Rew:507.0,660.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 668[6:Rew:667.0,507.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 682[6:Rew:664.0,655.3,646.0,655.3,664.0,655.2,646.0,655.2,667.0,655.2] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) -> . % 0.18/0.46 683[6:Con:682.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.18/0.46 723[6:SpL:668.0,683.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.18/0.46 724[6:Obv:723.1] || -> . % 0.18/0.46 725[6:Spt:724.0,536.1,646.0] || equal(sk_c6,sk_c7)** -> . % 0.18/0.46 726[6:Spt:724.0,536.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.46 727[6:MRR:537.1,725.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.46 728[6:MRR:534.1,725.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.18/0.46 729[6:MRR:535.1,725.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.46 731[6:SpR:726.0,503.0] || -> equal(inverse(sk_c7),sk_c3)**. % 0.18/0.46 733[6:Rew:507.0,731.0] || -> equal(sk_c3,sk_c5)**. % 0.18/0.46 735[6:Rew:733.0,729.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.46 736[6:Rew:547.0,735.0] || -> equal(sk_c2,sk_c6)**. % 0.18/0.46 739[6:Rew:736.0,590.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.46 746[6:Rew:739.0,728.0] || -> equal(sk_c4,sk_c5)**. % 0.18/0.46 747[6:Rew:739.0,9.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 751[6:Rew:746.0,727.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.46 754[6:Rew:747.0,507.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 763[6:Rew:747.0,751.0] || -> equal(inverse(sk_c7),sk_c6)**. % 0.18/0.46 766[6:Rew:763.0,754.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 767[6:MRR:766.0,725.0] || -> . % 0.18/0.46 777[5:Spt:767.0,17.1,529.0] || equal(multiply(sk_c1,sk_c7),sk_c2)** -> . % 0.18/0.46 778[5:Spt:767.0,17.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.46 779[5:Rew:584.0,777.0,574.0,777.0] || equal(identity,sk_c2)** -> . % 0.18/0.46 781[4:Rew:584.0,15.1,574.0,15.1] || -> equal(inverse(sk_c3),sk_c7)** equal(identity,sk_c2). % 0.18/0.46 782[5:MRR:781.1,779.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.46 783[4:Rew:584.0,14.1,574.0,14.1] || -> equal(multiply(sk_c3,sk_c7),sk_c6)** equal(identity,sk_c2). % 0.18/0.46 784[5:MRR:783.1,779.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.46 785[4:Rew:584.0,16.1,574.0,16.1] || -> equal(multiply(sk_c4,sk_c6),sk_c5)** equal(identity,sk_c2). % 0.18/0.46 786[5:MRR:785.1,779.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.18/0.46 789[5:SpR:778.0,503.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.18/0.46 803[5:SpR:782.0,503.0] || -> equal(inverse(sk_c7),sk_c3)**. % 0.18/0.46 805[5:Rew:507.0,803.0] || -> equal(sk_c3,sk_c5)**. % 0.18/0.46 807[5:Rew:805.0,784.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.46 808[5:Rew:584.0,807.0] || -> equal(identity,sk_c6)**. % 0.18/0.46 809[5:Rew:808.0,468.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.18/0.46 812[5:Rew:808.0,209.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.46 813[5:Rew:808.0,23.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.46 816[5:Rew:789.0,809.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.46 818[5:Rew:816.0,786.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.18/0.46 822[5:Rew:812.0,9.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 824[5:Rew:812.0,517.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c7) equal(u,sk_c5) equal(multiply(v,sk_c7),sk_c6)** -> . % 0.18/0.46 826[5:Rew:822.0,507.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 837[5:Rew:813.0,818.0,822.0,818.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 843[5:Rew:837.0,812.0] || -> equal(multiply(u,sk_c7),u)**. % 0.18/0.46 857[5:Rew:843.0,824.3,837.0,824.3,822.0,824.2,837.0,824.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) -> . % 0.18/0.46 858[5:Con:857.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.18/0.46 916[5:SpL:826.0,858.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.18/0.46 917[5:Obv:916.1] || -> . % 0.18/0.46 918[4:Spt:917.0,21.1,523.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.18/0.46 919[4:Spt:917.0,21.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.46 920[4:MRR:19.1,918.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.46 921[4:MRR:18.0,918.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.46 922[4:MRR:20.0,918.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.18/0.46 924[4:SpR:919.0,503.0] || -> equal(inverse(sk_c6),sk_c4)**. % 0.18/0.46 942[4:SpR:920.0,503.0] || -> equal(inverse(sk_c7),sk_c3)**. % 0.18/0.46 945[4:Rew:507.0,942.0] || -> equal(sk_c3,sk_c5)**. % 0.18/0.46 947[4:Rew:945.0,921.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.46 948[4:Rew:584.0,947.0] || -> equal(identity,sk_c6)**. % 0.18/0.46 949[4:Rew:948.0,468.0] || -> equal(inverse(sk_c6),sk_c6)**. % 0.18/0.46 950[4:Rew:948.0,23.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.46 951[4:Rew:948.0,209.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.46 955[4:Rew:924.0,949.0] || -> equal(sk_c4,sk_c6)**. % 0.18/0.46 957[4:Rew:955.0,922.0] || -> equal(multiply(sk_c6,sk_c6),sk_c5)**. % 0.18/0.46 966[4:Rew:951.0,517.2] || equal(inverse(u),sk_c6)** equal(inverse(v),sk_c7) equal(u,sk_c5) equal(multiply(v,sk_c7),sk_c6)** -> . % 0.18/0.46 967[4:Rew:951.0,9.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 969[4:Rew:967.0,568.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 976[4:Rew:950.0,957.0,967.0,957.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 982[4:Rew:976.0,951.0] || -> equal(multiply(u,sk_c7),u)**. % 0.18/0.46 996[4:Rew:982.0,966.3,976.0,966.3,967.0,966.2,976.0,966.0] || equal(inverse(u),sk_c7)** equal(inverse(v),sk_c7)** equal(u,sk_c7) equal(v,sk_c7) -> . % 0.18/0.46 997[4:Con:996.1] || equal(inverse(u),sk_c7)** equal(u,sk_c7) -> . % 0.18/0.46 1045[4:SpL:969.0,997.0] || equal(sk_c7,sk_c7)* equal(sk_c7,sk_c7)* -> . % 0.18/0.46 1046[4:Obv:1045.1] || -> . % 0.18/0.46 1047[3:Spt:1046.0,4.1,514.0] || equal(multiply(sk_c7,sk_c6),sk_c5)** -> . % 0.18/0.46 1048[3:Spt:1046.0,4.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.46 1049[3:MRR:2.1,1047.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.46 1050[3:MRR:1.1,1047.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.46 1071[3:SpR:1049.0,503.0] || -> equal(inverse(sk_c7),sk_c3)**. % 0.18/0.46 1074[3:Rew:507.0,1071.0] || -> equal(sk_c3,sk_c5)**. % 0.18/0.46 1076[3:Rew:1074.0,1050.0] || -> equal(multiply(sk_c5,sk_c7),sk_c6)**. % 0.18/0.46 1077[3:Rew:584.0,1076.0] || -> equal(identity,sk_c6)**. % 0.18/0.46 1080[3:Rew:1077.0,209.0] || -> equal(multiply(u,sk_c6),u)**. % 0.18/0.46 1090[3:Rew:1080.0,1047.0] || equal(sk_c5,sk_c7)** -> . % 0.18/0.46 1091[3:Rew:1080.0,9.0] || -> equal(sk_c5,sk_c7)**. % 0.18/0.46 1099[3:Rew:1091.0,1090.0] || equal(sk_c7,sk_c7)* -> . % 0.18/0.46 1100[3:Obv:1099.0] || -> . % 0.18/0.46 1120[2:Spt:1100.0,6.1,507.0] || equal(inverse(sk_c7),sk_c5)** -> . % 0.18/0.46 1121[2:Spt:1100.0,6.0] || -> equal(inverse(sk_c3),sk_c7)**. % 0.18/0.46 1122[2:MRR:8.1,1120.0] || -> equal(inverse(sk_c4),sk_c6)**. % 0.18/0.46 1123[2:MRR:5.0,1120.0] || -> equal(multiply(sk_c3,sk_c7),sk_c6)**. % 0.18/0.46 1124[2:MRR:7.0,1120.0] || -> equal(multiply(sk_c4,sk_c6),sk_c5)**. % 0.18/0.46 1126[2:SpR:1121.0,503.0] || -> equal(inverse(sk_c7),sk_c3)**. % 0.18/0.46 1127[2:SpR:1121.0,565.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),u)**. % 0.18/0.46 1129[2:Rew:1126.0,1120.0] || equal(sk_c3,sk_c5)** -> . % 0.18/0.46 1136[2:SpR:1122.0,59.0] || -> equal(multiply(sk_c6,multiply(sk_c4,u)),u)**. % 0.18/0.46 1151[2:SpR:1123.0,25.0] || -> equal(multiply(sk_c3,multiply(sk_c7,u)),multiply(sk_c6,u))**. % 0.18/0.46 1155[2:Rew:1127.0,1151.0] || -> equal(multiply(sk_c6,u),u)**. % 0.18/0.46 1156[2:Rew:1155.0,1136.0] || -> equal(multiply(sk_c4,u),u)**. % 0.18/0.46 1159[2:Rew:1156.0,1124.0] || -> equal(sk_c5,sk_c6)**. % 0.18/0.46 1160[2:Rew:1159.0,1129.0] || equal(sk_c3,sk_c6)** -> . % 0.18/0.46 1161[2:Rew:1159.0,9.0] || -> equal(multiply(sk_c6,sk_c6),sk_c7)**. % 0.18/0.46 1162[2:Rew:1159.0,80.0] || -> equal(multiply(inverse(sk_c6),sk_c7),sk_c6)**. % 0.18/0.46 1163[2:Rew:1155.0,1161.0] || -> equal(sk_c6,sk_c7)**. % 0.18/0.46 1170[2:Rew:1163.0,1160.0] || equal(sk_c3,sk_c7)** -> . % 0.18/0.46 1176[2:Rew:24.0,1162.0,1163.0,1162.0] || -> equal(identity,sk_c7)**. % 0.18/0.46 1177[2:Rew:1176.0,468.0] || -> equal(inverse(sk_c7),sk_c7)**. % 0.18/0.46 1182[2:Rew:1126.0,1177.0] || -> equal(sk_c3,sk_c7)**. % 0.18/0.46 1183[2:MRR:1182.0,1170.0] || -> . % 0.18/0.46 % SZS output end Refutation % 0.18/0.46 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 left_identity left_inverse associativity % 0.18/0.46 %------------------------------------------------------------------------------