%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP353-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n025.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Sat Jul 16 11:46:59 EDT 2022 % Result : Unsatisfiable 0.20s 0.49s % Output : Refutation 0.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : GRP353-1 : TPTP v8.1.0. Released v2.5.0. % 0.12/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n025.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 600 % 0.13/0.34 % DateTime : Mon Jun 13 18:06:54 EDT 2022 % 0.13/0.35 % CPUTime : % 0.20/0.49 % 0.20/0.49 SPASS V 3.9 % 0.20/0.49 SPASS beiseite: Proof found. % 0.20/0.49 % SZS status Theorem % 0.20/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.20/0.49 SPASS derived 783 clauses, backtracked 267 clauses, performed 9 splits and kept 633 clauses. % 0.20/0.49 SPASS allocated 63593 KBytes. % 0.20/0.49 SPASS spent 0:00:00.13 on the problem. % 0.20/0.49 0:00:00.04 for the input. % 0.20/0.49 0:00:00.00 for the FLOTTER CNF translation. % 0.20/0.49 0:00:00.01 for inferences. % 0.20/0.49 0:00:00.00 for the backtracking. % 0.20/0.49 0:00:00.06 for the reduction. % 0.20/0.49 % 0.20/0.49 % 0.20/0.49 Here is a proof with depth 5, length 254 : % 0.20/0.49 % SZS output start Refutation % 0.20/0.49 1[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.20/0.49 2[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.49 3[0:Inp] || -> equal(multiply(sk_c2,sk_c6),sk_c7)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.20/0.49 4[0:Inp] || -> equal(multiply(sk_c3,sk_c4),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7). % 0.20/0.49 5[0:Inp] || -> equal(inverse(sk_c3),sk_c4) equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.49 7[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 8[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 9[0:Inp] || -> equal(multiply(sk_c2,sk_c6),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 10[0:Inp] || -> equal(multiply(sk_c3,sk_c4),sk_c6) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 11[0:Inp] || -> equal(inverse(sk_c3),sk_c4) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 13[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 14[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 15[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.49 16[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 17[0:Inp] || -> equal(inverse(sk_c3),sk_c4) equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 19[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.49 20[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.49 21[0:Inp] || -> equal(multiply(sk_c2,sk_c6),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.49 22[0:Inp] || -> equal(multiply(sk_c3,sk_c4),sk_c6) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.49 23[0:Inp] || -> equal(inverse(sk_c3),sk_c4) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.49 25[0:Inp] || equal(inverse(u),v) equal(inverse(w),sk_c7) equal(inverse(x),sk_c7) equal(multiply(u,v),sk_c6)**+ equal(multiply(v,sk_c7),sk_c6)** equal(multiply(w,sk_c6),sk_c7)** equal(multiply(x,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.20/0.49 26[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.20/0.49 27[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.20/0.49 28[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.20/0.49 29[1:Spt:25.0,25.3,25.4] || equal(inverse(u),v) equal(multiply(u,v),sk_c6)**+ equal(multiply(v,sk_c7),sk_c6)** -> . % 0.20/0.49 30[2:Spt:19.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.49 32[2:SpL:30.0,29.1] || equal(inverse(sk_c7),sk_c5) equal(sk_c6,sk_c6) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.20/0.49 33[2:Obv:32.1] || equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.20/0.49 34[3:Spt:1.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.49 37[4:Spt:13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 41[5:Spt:7.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 48[4:SpR:37.0,27.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.20/0.49 60[0:SpR:27.0,28.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.20/0.49 61[4:SpR:48.0,28.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),multiply(identity,u))**. % 0.20/0.49 63[4:Rew:26.0,61.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.20/0.49 64[0:Rew:26.0,60.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.20/0.49 68[5:SpR:41.0,63.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.49 76[0:SpR:64.0,64.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.20/0.49 79[2:SpR:30.0,64.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c5)**. % 0.20/0.49 82[0:SpR:27.0,64.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.20/0.49 83[4:SpR:48.0,64.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.20/0.49 85[5:SpR:68.0,64.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.49 90[5:Rew:27.0,85.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 91[5:Rew:90.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 98[5:Rew:90.0,83.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c1)**. % 0.20/0.49 99[5:Rew:91.0,34.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 106[5:Rew:99.0,30.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 107[5:Rew:99.0,37.0] || -> equal(inverse(sk_c1),sk_c5)**. % 0.20/0.49 112[5:Rew:99.0,33.0] || equal(inverse(sk_c5),sk_c5) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.20/0.49 114[5:Rew:99.0,79.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c5)**. % 0.20/0.49 119[5:Rew:99.0,98.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c1)**. % 0.20/0.49 122[5:Rew:119.0,114.0] || -> equal(sk_c1,sk_c5)**. % 0.20/0.49 123[5:Rew:122.0,107.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.20/0.49 139[5:Rew:106.0,112.1,99.0,112.1,123.0,112.0] || equal(sk_c5,sk_c5)* equal(sk_c6,sk_c6) -> . % 0.20/0.49 140[5:Obv:139.1] || -> . % 0.20/0.49 153[5:Spt:140.0,7.1,41.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.20/0.49 154[5:Spt:140.0,7.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 155[0:Rew:76.0,82.0] || -> equal(multiply(u,identity),u)**. % 0.20/0.49 156[4:Rew:155.0,83.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.20/0.49 157[4:Rew:156.0,79.0] || -> equal(multiply(sk_c1,sk_c6),sk_c5)**. % 0.20/0.49 159[5:MRR:11.1,153.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.20/0.49 162[5:MRR:10.1,153.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 164[4:Rew:156.0,33.0] || equal(sk_c1,sk_c5) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.20/0.49 198[5:SpR:162.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.20/0.49 200[5:Rew:159.0,198.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.20/0.49 209[5:SpR:200.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.20/0.49 211[5:Rew:27.0,209.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 213[5:Rew:211.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 217[5:Rew:211.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 219[5:Rew:213.0,34.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 232[5:Rew:219.0,30.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 239[5:Rew:219.0,164.1] || equal(sk_c1,sk_c5) equal(multiply(sk_c5,sk_c5),sk_c6)** -> . % 0.20/0.49 249[5:Rew:217.0,157.0] || -> equal(sk_c1,sk_c5)**. % 0.20/0.49 268[5:Rew:232.0,239.1,249.0,239.0] || equal(sk_c5,sk_c5)* equal(sk_c6,sk_c6) -> . % 0.20/0.49 269[5:Obv:268.1] || -> . % 0.20/0.49 276[4:Spt:269.0,13.0,37.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.20/0.49 277[4:Spt:269.0,13.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 278[4:MRR:17.1,276.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.20/0.49 279[4:MRR:14.1,276.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.49 281[4:MRR:16.0,276.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 282[4:MRR:15.0,276.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.49 300[4:SpR:281.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.20/0.49 302[4:Rew:278.0,300.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.20/0.49 311[4:SpR:302.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.20/0.49 313[4:Rew:27.0,311.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 314[4:Rew:313.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 315[4:Rew:313.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 320[4:Rew:314.0,34.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 328[4:Rew:320.0,279.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.20/0.49 330[4:Rew:320.0,30.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 332[4:Rew:320.0,282.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.49 335[4:Rew:320.0,33.0] || equal(inverse(sk_c5),sk_c5) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.20/0.49 344[4:Rew:315.0,332.0] || -> equal(sk_c2,sk_c5)**. % 0.20/0.49 345[4:Rew:344.0,328.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.20/0.49 355[4:Rew:330.0,335.1,320.0,335.1,345.0,335.0] || equal(sk_c5,sk_c5)* equal(sk_c6,sk_c6) -> . % 0.20/0.49 356[4:Obv:355.1] || -> . % 0.20/0.49 362[3:Spt:356.0,1.1,34.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.49 363[3:Spt:356.0,1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 364[3:MRR:5.1,362.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.20/0.49 365[3:MRR:2.1,362.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.49 367[3:MRR:4.1,362.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 368[3:MRR:3.1,362.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.49 383[3:SpR:367.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.20/0.49 385[3:Rew:364.0,383.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.20/0.49 391[3:SpR:385.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.20/0.49 393[3:Rew:27.0,391.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 394[3:Rew:393.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 395[3:Rew:393.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 400[3:Rew:394.0,363.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 407[3:Rew:400.0,365.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.20/0.49 408[3:Rew:400.0,30.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 410[3:Rew:400.0,368.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.49 412[3:Rew:400.0,33.0] || equal(inverse(sk_c5),sk_c5) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.20/0.49 422[3:Rew:395.0,410.0] || -> equal(sk_c2,sk_c5)**. % 0.20/0.49 423[3:Rew:422.0,407.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.20/0.49 432[3:Rew:408.0,412.1,400.0,412.1,423.0,412.0] || equal(sk_c5,sk_c5)* equal(sk_c6,sk_c6) -> . % 0.20/0.49 433[3:Obv:432.1] || -> . % 0.20/0.49 437[2:Spt:433.0,19.1,30.0] || equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.20/0.49 438[2:Spt:433.0,19.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 439[2:MRR:23.1,437.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.20/0.49 440[2:MRR:20.1,437.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.49 442[2:MRR:22.1,437.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 443[2:MRR:21.1,437.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.49 455[2:SpR:442.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.20/0.49 457[2:Rew:439.0,455.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.20/0.49 459[2:SpR:443.0,64.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c6)**. % 0.20/0.49 461[2:Rew:440.0,459.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 463[2:SpR:457.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.20/0.49 465[2:Rew:27.0,463.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 466[2:Rew:465.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 467[2:Rew:465.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 472[2:Rew:466.0,443.0] || -> equal(sk_c7,sk_c2)**. % 0.20/0.49 474[2:Rew:472.0,438.0] || -> equal(multiply(sk_c6,sk_c2),sk_c5)**. % 0.20/0.49 477[2:Rew:472.0,437.0] || equal(multiply(sk_c2,sk_c5),sk_c6)** -> . % 0.20/0.49 486[2:Rew:472.0,461.0] || -> equal(multiply(sk_c2,sk_c2),sk_c6)**. % 0.20/0.49 489[2:Rew:467.0,474.0] || -> equal(sk_c2,sk_c5)**. % 0.20/0.49 494[2:Rew:489.0,486.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 495[2:Rew:494.0,477.0,489.0,477.0] || equal(sk_c6,sk_c6)* -> . % 0.20/0.49 496[2:Obv:495.0] || -> . % 0.20/0.49 509[1:Spt:496.0,25.1,25.2,25.5,25.6,25.7,25.8,25.9] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)**+ equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c7,sk_c5),sk_c6)** equal(multiply(sk_c6,sk_c5),sk_c7) -> . % 0.20/0.49 511[2:Spt:1.1] || -> equal(multiply(sk_c6,sk_c5),sk_c7)**. % 0.20/0.49 512[2:Rew:511.0,509.6] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c7,sk_c5),sk_c6)** equal(sk_c7,sk_c7) -> . % 0.20/0.49 514[2:Obv:512.6] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.20/0.49 519[3:Spt:19.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.20/0.49 521[3:Rew:519.0,514.5] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** equal(sk_c6,sk_c6) -> . % 0.20/0.49 522[3:Obv:521.5] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** equal(multiply(sk_c6,sk_c7),sk_c5)** -> . % 0.20/0.49 525[3:SpR:519.0,64.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c5)**. % 0.20/0.49 527[4:Spt:13.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.20/0.49 530[5:Spt:7.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.20/0.49 532[5:SpR:530.0,64.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.20/0.49 534[5:Rew:527.0,532.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.20/0.49 539[5:SpR:534.0,64.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.20/0.49 541[5:Rew:27.0,539.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 542[5:Rew:541.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 543[5:Rew:541.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 546[5:Rew:542.0,511.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 548[5:Rew:542.0,522.4] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** equal(sk_c7,sk_c5) -> . % 0.20/0.49 552[5:Rew:546.0,519.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 557[5:Rew:546.0,525.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c5)**. % 0.20/0.49 559[5:Rew:543.0,557.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.20/0.49 564[5:Rew:546.0,548.4,546.0,548.3,543.0,548.2,546.0,548.2,546.0,548.1,546.0,548.0] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c5) equal(u,sk_c5) equal(multiply(v,sk_c5),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.20/0.49 565[5:Obv:564.4] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c5) equal(u,sk_c5) equal(multiply(v,sk_c5),sk_c6)**+ -> . % 0.20/0.49 629[5:SpL:552.0,565.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c5),sk_c5)** equal(u,sk_c5) equal(sk_c6,sk_c6) -> . % 0.20/0.49 632[5:Obv:629.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c5),sk_c5)** equal(u,sk_c5) -> . % 0.20/0.49 633[5:Rew:559.0,632.1] || equal(inverse(u),sk_c5)** equal(sk_c5,sk_c5) equal(u,sk_c5) -> . % 0.20/0.49 634[5:Obv:633.1] || equal(inverse(u),sk_c5)** equal(u,sk_c5) -> . % 0.20/0.49 675[5:SpL:559.0,634.0] || equal(sk_c5,sk_c5)* equal(sk_c5,sk_c5)* -> . % 0.20/0.49 678[5:Obv:675.1] || -> . % 0.20/0.49 680[5:Spt:678.0,7.1,530.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.20/0.49 681[5:Spt:678.0,7.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 682[5:MRR:11.1,680.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.20/0.49 683[5:MRR:8.1,680.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.49 685[5:MRR:10.1,680.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 686[5:MRR:9.1,680.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.49 710[5:SpR:685.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.20/0.49 712[5:Rew:682.0,710.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.20/0.49 718[5:SpR:712.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.20/0.49 720[5:Rew:27.0,718.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 721[5:Rew:720.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 722[5:Rew:720.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 724[5:Rew:720.0,27.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.20/0.49 725[5:Rew:721.0,511.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 733[5:Rew:725.0,527.0] || -> equal(inverse(sk_c1),sk_c5)**. % 0.20/0.49 734[5:Rew:725.0,683.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.20/0.49 735[5:Rew:725.0,519.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 737[5:Rew:725.0,686.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.49 740[5:Rew:725.0,680.0] || equal(multiply(sk_c1,sk_c5),sk_c6)** -> . % 0.20/0.49 748[5:Rew:722.0,737.0] || -> equal(sk_c2,sk_c5)**. % 0.20/0.49 749[5:Rew:748.0,734.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.20/0.49 795[5:SpR:733.0,724.0] || -> equal(multiply(sk_c5,sk_c1),sk_c6)**. % 0.20/0.49 838[5:SpR:795.0,64.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c1)**. % 0.20/0.49 840[5:Rew:722.0,838.0,749.0,838.0] || -> equal(sk_c1,sk_c5)**. % 0.20/0.49 842[5:Rew:840.0,740.0] || equal(multiply(sk_c5,sk_c5),sk_c6)** -> . % 0.20/0.49 845[5:Rew:735.0,842.0] || equal(sk_c6,sk_c6)* -> . % 0.20/0.49 846[5:Obv:845.0] || -> . % 0.20/0.49 849[4:Spt:846.0,13.0,527.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.20/0.49 850[4:Spt:846.0,13.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 851[4:MRR:17.1,849.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.20/0.49 852[4:MRR:14.1,849.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.49 854[4:MRR:16.0,849.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 855[4:MRR:15.0,849.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.49 856[4:Rew:850.0,522.4] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** equal(sk_c5,sk_c5) -> . % 0.20/0.49 857[4:Obv:856.4] || equal(inverse(u),sk_c7) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** -> . % 0.20/0.49 877[4:SpR:854.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.20/0.49 879[4:Rew:851.0,877.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.20/0.49 888[4:SpR:879.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.20/0.49 890[4:Rew:27.0,888.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 891[4:Rew:890.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 892[4:Rew:890.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.20/0.49 895[4:Rew:891.0,511.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 903[4:Rew:895.0,852.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.20/0.49 905[4:Rew:895.0,519.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 907[4:Rew:895.0,855.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.20/0.49 910[4:Rew:895.0,857.0] || equal(inverse(u),sk_c5) equal(inverse(v),sk_c7) equal(multiply(u,sk_c6),sk_c7)** equal(multiply(v,sk_c7),sk_c6)** -> . % 0.20/0.49 916[4:Rew:892.0,907.0] || -> equal(sk_c2,sk_c5)**. % 0.20/0.49 917[4:Rew:916.0,903.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.20/0.49 927[4:Rew:895.0,910.3,892.0,910.2,895.0,910.2,895.0,910.1] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c5) equal(u,sk_c5) equal(multiply(v,sk_c5),sk_c6)**+ -> . % 0.20/0.49 1020[4:SpL:905.0,927.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c5),sk_c5)** equal(u,sk_c5) equal(sk_c6,sk_c6) -> . % 0.20/0.49 1023[4:Obv:1020.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c5),sk_c5)** equal(u,sk_c5) -> . % 0.20/0.49 1024[4:Rew:917.0,1023.1] || equal(inverse(u),sk_c5)** equal(sk_c5,sk_c5) equal(u,sk_c5) -> . % 0.20/0.49 1025[4:Obv:1024.1] || equal(inverse(u),sk_c5)** equal(u,sk_c5) -> . % 0.20/0.49 1047[4:SpL:917.0,1025.0] || equal(sk_c5,sk_c5)* equal(sk_c5,sk_c5)* -> . % 0.20/0.49 1050[4:Obv:1047.1] || -> . % 0.20/0.49 1052[3:Spt:1050.0,19.1,519.0] || equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.20/0.49 1053[3:Spt:1050.0,19.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 1054[3:MRR:23.1,1052.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.20/0.49 1055[3:MRR:20.1,1052.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.20/0.49 1057[3:MRR:22.1,1052.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 1058[3:MRR:21.1,1052.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.20/0.49 1073[3:SpR:1057.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.20/0.49 1075[3:Rew:1054.0,1073.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.20/0.49 1077[3:SpR:1058.0,64.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c6)**. % 0.20/0.49 1079[3:Rew:1055.0,1077.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.20/0.49 1081[3:SpR:1075.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.20/0.49 1083[3:Rew:27.0,1081.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 1084[3:Rew:1083.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 1088[3:Rew:1084.0,511.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 1099[3:Rew:1088.0,1052.0] || equal(multiply(sk_c5,sk_c5),sk_c6)** -> . % 0.20/0.49 1103[3:Rew:1088.0,1079.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.20/0.49 1106[3:Rew:1103.0,1099.0] || equal(sk_c6,sk_c6)* -> . % 0.20/0.49 1107[3:Obv:1106.0] || -> . % 0.20/0.49 1115[2:Spt:1107.0,1.1,511.0] || equal(multiply(sk_c6,sk_c5),sk_c7)** -> . % 0.20/0.49 1116[2:Spt:1107.0,1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.20/0.49 1117[2:MRR:5.1,1115.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.20/0.49 1120[2:MRR:4.1,1115.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.20/0.49 1133[2:SpR:1120.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.20/0.49 1135[2:Rew:1117.0,1133.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.20/0.49 1144[2:SpR:1135.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.20/0.49 1146[2:Rew:27.0,1144.0] || -> equal(identity,sk_c6)**. % 0.20/0.49 1147[2:Rew:1146.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.20/0.49 1151[2:Rew:1147.0,1116.0] || -> equal(sk_c7,sk_c5)**. % 0.20/0.49 1156[2:Rew:1147.0,1115.0] || equal(sk_c7,sk_c5)** -> . % 0.20/0.49 1164[2:Rew:1151.0,1156.0] || equal(sk_c5,sk_c5)* -> . % 0.20/0.49 1165[2:Obv:1164.0] || -> . % 0.20/0.49 % SZS output end Refutation % 0.20/0.49 Formulae used in the proof : prove_this_1 prove_this_2 prove_this_3 prove_this_4 prove_this_5 prove_this_7 prove_this_8 prove_this_9 prove_this_10 prove_this_11 prove_this_13 prove_this_14 prove_this_15 prove_this_16 prove_this_17 prove_this_19 prove_this_20 prove_this_21 prove_this_22 prove_this_23 prove_this_25 left_identity left_inverse associativity % 0.20/0.49 %------------------------------------------------------------------------------