%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP277-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n019.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:38 EDT 2022 % Result : Unsatisfiable 0.19s 0.48s % Output : Refutation 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP277-1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.13 % Command : run_spass %d %s % 0.13/0.34 % Computer : n019.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 : Tue Jun 14 06:24:54 EDT 2022 % 0.13/0.34 % CPUTime : % 0.19/0.48 % 0.19/0.48 SPASS V 3.9 % 0.19/0.48 SPASS beiseite: Proof found. % 0.19/0.48 % SZS status Theorem % 0.19/0.48 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.19/0.48 SPASS derived 809 clauses, backtracked 266 clauses, performed 9 splits and kept 650 clauses. % 0.19/0.48 SPASS allocated 63619 KBytes. % 0.19/0.48 SPASS spent 0:00:00.12 on the problem. % 0.19/0.48 0:00:00.04 for the input. % 0.19/0.48 0:00:00.00 for the FLOTTER CNF translation. % 0.19/0.48 0:00:00.01 for inferences. % 0.19/0.48 0:00:00.00 for the backtracking. % 0.19/0.48 0:00:00.05 for the reduction. % 0.19/0.48 % 0.19/0.48 % 0.19/0.48 Here is a proof with depth 5, length 264 : % 0.19/0.48 % SZS output start Refutation % 0.19/0.48 1[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5)** equal(multiply(sk_c1,sk_c7),sk_c6). % 0.19/0.48 2[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.19/0.48 3[0:Inp] || -> equal(multiply(sk_c2,sk_c6),sk_c7)** equal(multiply(sk_c1,sk_c7),sk_c6). % 0.19/0.48 4[0:Inp] || -> equal(multiply(sk_c3,sk_c4),sk_c6)** equal(multiply(sk_c1,sk_c7),sk_c6). % 0.19/0.48 5[0:Inp] || -> equal(inverse(sk_c3),sk_c4) equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.19/0.48 7[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 8[0:Inp] || -> equal(inverse(sk_c2),sk_c7)** equal(inverse(sk_c1),sk_c7). % 0.19/0.48 9[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.19/0.48 10[0:Inp] || -> equal(inverse(sk_c1),sk_c7) equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 11[0:Inp] || -> equal(inverse(sk_c3),sk_c4)** equal(inverse(sk_c1),sk_c7). % 0.19/0.48 13[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.48 14[0:Inp] || -> equal(inverse(sk_c2),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.48 15[0:Inp] || -> equal(multiply(sk_c2,sk_c6),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.48 16[0:Inp] || -> equal(multiply(sk_c3,sk_c4),sk_c6) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.48 17[0:Inp] || -> equal(inverse(sk_c3),sk_c4) equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.48 19[0:Inp] || -> equal(multiply(sk_c6,sk_c7),sk_c5) equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.48 21[0:Inp] || -> equal(multiply(sk_c2,sk_c6),sk_c7)** equal(multiply(sk_c5,sk_c6),sk_c7). % 0.19/0.48 22[0:Inp] || -> equal(multiply(sk_c3,sk_c4),sk_c6)** equal(multiply(sk_c5,sk_c6),sk_c7). % 0.19/0.48 23[0:Inp] || -> equal(inverse(sk_c3),sk_c4) equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.48 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_c5,sk_c6),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.19/0.48 26[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.19/0.48 27[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.19/0.48 28[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.19/0.48 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.19/0.48 30[2:Spt:19.1] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.48 33[3:Spt:13.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.48 35[3:SpL:33.0,29.1] || equal(inverse(sk_c7),sk_c5) equal(sk_c6,sk_c6) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.19/0.48 36[3:Obv:35.1] || equal(inverse(sk_c7),sk_c5) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.19/0.48 37[4:Spt:7.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 41[5:Spt:1.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.19/0.48 48[4:SpR:37.0,27.0] || -> equal(multiply(sk_c7,sk_c1),identity)**. % 0.19/0.48 57[2:SpR:30.0,28.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c7,u))**. % 0.19/0.48 59[4:SpR:48.0,28.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),multiply(identity,u))**. % 0.19/0.48 61[0:SpR:27.0,28.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.19/0.48 63[4:Rew:26.0,59.0] || -> equal(multiply(sk_c7,multiply(sk_c1,u)),u)**. % 0.19/0.48 64[0:Rew:26.0,61.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.19/0.48 68[5:SpR:41.0,63.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.19/0.48 76[0:SpR:64.0,64.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.19/0.48 80[3:SpR:33.0,64.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c5)**. % 0.19/0.48 81[4:SpR:48.0,64.0] || -> equal(multiply(inverse(sk_c7),identity),sk_c1)**. % 0.19/0.48 82[4:SpR:63.0,64.0] || -> equal(multiply(inverse(sk_c7),u),multiply(sk_c1,u))**. % 0.19/0.48 83[5:SpR:68.0,64.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.19/0.48 84[0:SpR:26.0,64.0] || -> equal(multiply(inverse(identity),u),u)**. % 0.19/0.48 85[0:SpR:27.0,64.0] || -> equal(multiply(inverse(inverse(u)),identity),u)**. % 0.19/0.48 90[5:Rew:27.0,83.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 91[5:Rew:90.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 93[5:Rew:90.0,48.0] || -> equal(multiply(sk_c7,sk_c1),sk_c6)**. % 0.19/0.48 97[5:Rew:90.0,81.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c1)**. % 0.19/0.48 99[5:Rew:91.0,57.0] || -> equal(multiply(sk_c7,u),multiply(sk_c5,u))**. % 0.19/0.48 105[5:Rew:80.0,97.0] || -> equal(sk_c5,sk_c1)**. % 0.19/0.48 106[5:Rew:105.0,30.0] || -> equal(multiply(sk_c1,sk_c6),sk_c7)**. % 0.19/0.48 109[5:Rew:105.0,36.0] || equal(inverse(sk_c7),sk_c1) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.19/0.48 110[5:Rew:105.0,80.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c1)**. % 0.19/0.48 114[5:Rew:105.0,99.0] || -> equal(multiply(sk_c7,u),multiply(sk_c1,u))**. % 0.19/0.48 118[5:Rew:114.0,93.0] || -> equal(multiply(sk_c1,sk_c1),sk_c6)**. % 0.19/0.48 123[5:Rew:82.0,110.0] || -> equal(multiply(sk_c1,sk_c6),sk_c1)**. % 0.19/0.48 124[5:Rew:106.0,123.0] || -> equal(sk_c7,sk_c1)**. % 0.19/0.48 126[5:Rew:124.0,37.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.19/0.48 138[5:Rew:118.0,109.1,105.0,109.1,124.0,109.1,126.0,109.0,124.0,109.0] || equal(sk_c1,sk_c1) equal(sk_c6,sk_c6)* -> . % 0.19/0.48 139[5:Obv:138.1] || -> . % 0.19/0.48 153[5:Spt:139.0,1.1,41.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.19/0.48 154[5:Spt:139.0,1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 155[0:Rew:76.0,85.0] || -> equal(multiply(u,identity),u)**. % 0.19/0.48 156[4:Rew:155.0,81.0] || -> equal(inverse(sk_c7),sk_c1)**. % 0.19/0.48 157[4:Rew:156.0,80.0] || -> equal(multiply(sk_c1,sk_c6),sk_c5)**. % 0.19/0.48 159[5:MRR:5.1,153.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.19/0.48 162[5:MRR:4.1,153.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 164[4:Rew:156.0,36.0] || equal(sk_c5,sk_c1) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.19/0.48 199[5:SpR:162.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.19/0.48 201[5:Rew:159.0,199.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.19/0.48 210[5:SpR:201.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.19/0.48 212[5:Rew:27.0,210.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 214[5:Rew:212.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 218[5:Rew:212.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 220[5:Rew:214.0,154.0] || -> equal(sk_c7,sk_c5)**. % 0.19/0.48 231[5:Rew:220.0,33.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.19/0.48 239[5:Rew:220.0,164.1] || equal(sk_c5,sk_c1) equal(multiply(sk_c5,sk_c5),sk_c6)** -> . % 0.19/0.48 250[5:Rew:218.0,157.0] || -> equal(sk_c5,sk_c1)**. % 0.19/0.48 255[5:Rew:250.0,231.0] || -> equal(multiply(sk_c1,sk_c1),sk_c6)**. % 0.19/0.48 274[5:Rew:255.0,239.1,250.0,239.1,250.0,239.0] || equal(sk_c1,sk_c1) equal(sk_c6,sk_c6)* -> . % 0.19/0.48 275[5:Obv:274.1] || -> . % 0.19/0.48 286[4:Spt:275.0,7.0,37.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.19/0.48 287[4:Spt:275.0,7.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 288[4:MRR:11.1,286.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.19/0.48 289[4:MRR:8.1,286.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.19/0.48 291[4:MRR:10.0,286.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 292[4:MRR:9.0,286.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.19/0.48 311[4:SpR:291.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.19/0.48 313[4:Rew:288.0,311.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.19/0.48 322[4:SpR:313.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.19/0.48 324[4:Rew:27.0,322.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 325[4:Rew:324.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 326[4:Rew:324.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 331[4:Rew:325.0,287.0] || -> equal(sk_c7,sk_c5)**. % 0.19/0.48 338[4:Rew:331.0,289.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.19/0.48 341[4:Rew:331.0,33.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.19/0.48 343[4:Rew:331.0,292.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.19/0.48 346[4:Rew:331.0,36.0] || equal(inverse(sk_c5),sk_c5) equal(multiply(sk_c5,sk_c7),sk_c6)** -> . % 0.19/0.48 355[4:Rew:326.0,343.0] || -> equal(sk_c2,sk_c5)**. % 0.19/0.48 356[4:Rew:355.0,338.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.48 366[4:Rew:341.0,346.1,331.0,346.1,356.0,346.0] || equal(sk_c5,sk_c5)* equal(sk_c6,sk_c6) -> . % 0.19/0.48 367[4:Obv:366.1] || -> . % 0.19/0.48 374[3:Spt:367.0,13.1,33.0] || equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.19/0.48 375[3:Spt:367.0,13.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 376[3:MRR:17.1,374.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.19/0.48 377[3:MRR:14.1,374.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.19/0.48 379[3:MRR:16.1,374.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 380[3:MRR:15.1,374.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.19/0.48 396[3:SpR:379.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.19/0.48 398[3:Rew:376.0,396.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.19/0.48 400[3:SpR:380.0,64.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c6)**. % 0.19/0.48 402[3:Rew:377.0,400.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.48 404[3:SpR:398.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.19/0.48 406[3:Rew:27.0,404.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 407[3:Rew:406.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 413[3:Rew:407.0,375.0] || -> equal(sk_c7,sk_c5)**. % 0.19/0.48 424[3:Rew:413.0,374.0] || equal(multiply(sk_c5,sk_c5),sk_c6)** -> . % 0.19/0.48 432[3:Rew:413.0,402.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.19/0.48 435[3:Rew:432.0,424.0] || equal(sk_c6,sk_c6)* -> . % 0.19/0.48 436[3:Obv:435.0] || -> . % 0.19/0.48 450[2:Spt:436.0,19.1,30.0] || equal(multiply(sk_c5,sk_c6),sk_c7)** -> . % 0.19/0.48 451[2:Spt:436.0,19.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 452[2:MRR:23.1,450.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.19/0.48 455[2:MRR:22.1,450.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 456[2:MRR:21.1,450.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.19/0.48 458[2:SpR:451.0,64.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c7)**. % 0.19/0.48 468[2:SpR:455.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.19/0.48 470[2:Rew:452.0,468.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.19/0.48 476[2:SpR:470.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.19/0.48 478[2:Rew:27.0,476.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 479[2:Rew:478.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 481[2:Rew:478.0,84.0] || -> equal(multiply(inverse(sk_c6),u),u)**. % 0.19/0.48 485[2:Rew:479.0,456.0] || -> equal(sk_c7,sk_c2)**. % 0.19/0.48 487[2:Rew:479.0,450.0] || equal(sk_c7,sk_c5)** -> . % 0.19/0.48 494[2:Rew:485.0,458.0] || -> equal(multiply(inverse(sk_c6),sk_c5),sk_c2)**. % 0.19/0.48 501[2:Rew:485.0,487.0] || equal(sk_c2,sk_c5)** -> . % 0.19/0.48 505[2:Rew:481.0,494.0] || -> equal(sk_c2,sk_c5)**. % 0.19/0.48 506[2:MRR:505.0,501.0] || -> . % 0.19/0.48 517[1:Spt:506.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_c5,sk_c6),sk_c7) equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.19/0.48 519[2:Spt:13.1] || -> equal(multiply(sk_c7,sk_c5),sk_c6)**. % 0.19/0.48 520[2:Rew:519.0,517.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_c5,sk_c6),sk_c7)** equal(sk_c6,sk_c6) -> . % 0.19/0.48 522[2:Obv:520.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_c5,sk_c6),sk_c7)** -> . % 0.19/0.48 525[2:SpR:519.0,64.0] || -> equal(multiply(inverse(sk_c7),sk_c6),sk_c5)**. % 0.19/0.48 527[3:Spt:19.1] || -> equal(multiply(sk_c5,sk_c6),sk_c7)**. % 0.19/0.48 529[3:Rew:527.0,522.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_c7,sk_c7) -> . % 0.19/0.48 530[3:Obv:529.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.19/0.48 535[4:Spt:7.0] || -> equal(inverse(sk_c1),sk_c7)**. % 0.19/0.48 538[5:Spt:1.1] || -> equal(multiply(sk_c1,sk_c7),sk_c6)**. % 0.19/0.48 540[5:SpR:538.0,64.0] || -> equal(multiply(inverse(sk_c1),sk_c6),sk_c7)**. % 0.19/0.48 542[5:Rew:535.0,540.0] || -> equal(multiply(sk_c7,sk_c6),sk_c7)**. % 0.19/0.48 547[5:SpR:542.0,64.0] || -> equal(multiply(inverse(sk_c7),sk_c7),sk_c6)**. % 0.19/0.48 549[5:Rew:27.0,547.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 550[5:Rew:549.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 551[5:Rew:549.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 552[5:Rew:549.0,27.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.19/0.48 555[5:Rew:550.0,530.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.19/0.48 559[5:Rew:551.0,527.0] || -> equal(sk_c7,sk_c5)**. % 0.19/0.48 560[5:Rew:551.0,525.0] || -> equal(inverse(sk_c7),sk_c5)**. % 0.19/0.48 561[5:Rew:559.0,519.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.19/0.48 562[5:Rew:559.0,535.0] || -> equal(inverse(sk_c1),sk_c5)**. % 0.19/0.48 566[5:Rew:559.0,560.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.48 571[5:Rew:559.0,555.4,559.0,555.3,551.0,555.2,559.0,555.2,559.0,555.1,559.0,555.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.19/0.48 572[5:Obv:571.4] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c5) equal(u,sk_c5) equal(multiply(v,sk_c5),sk_c6)** -> . % 0.19/0.48 606[5:SpR:562.0,552.0] || -> equal(multiply(sk_c5,sk_c1),sk_c6)**. % 0.19/0.48 616[5:SpR:606.0,64.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c1)**. % 0.19/0.48 618[5:Rew:551.0,616.0,566.0,616.0] || -> equal(sk_c5,sk_c1)**. % 0.19/0.48 620[5:Rew:618.0,566.0] || -> equal(inverse(sk_c1),sk_c1)**. % 0.19/0.48 622[5:Rew:618.0,561.0] || -> equal(multiply(sk_c1,sk_c1),sk_c6)**. % 0.19/0.48 628[5:Rew:618.0,572.0] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c5) equal(u,sk_c5) equal(multiply(v,sk_c5),sk_c6)** -> . % 0.19/0.48 631[5:Rew:618.0,628.3,618.0,628.2,618.0,628.1] || equal(inverse(u),sk_c1)** equal(inverse(v),sk_c1) equal(u,sk_c1) equal(multiply(v,sk_c1),sk_c6)**+ -> . % 0.19/0.48 670[5:SpL:622.0,631.3] || equal(inverse(u),sk_c1)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c1) equal(sk_c6,sk_c6) -> . % 0.19/0.48 674[5:Obv:670.3] || equal(inverse(u),sk_c1)** equal(inverse(sk_c1),sk_c1)** equal(u,sk_c1) -> . % 0.19/0.48 675[5:Rew:620.0,674.1] || equal(inverse(u),sk_c1)** equal(sk_c1,sk_c1) equal(u,sk_c1) -> . % 0.19/0.48 676[5:Obv:675.1] || equal(inverse(u),sk_c1)** equal(u,sk_c1) -> . % 0.19/0.48 699[5:SpL:620.0,676.0] || equal(sk_c1,sk_c1)* equal(sk_c1,sk_c1)* -> . % 0.19/0.48 702[5:Obv:699.1] || -> . % 0.19/0.48 703[5:Spt:702.0,1.1,538.0] || equal(multiply(sk_c1,sk_c7),sk_c6)** -> . % 0.19/0.48 704[5:Spt:702.0,1.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 705[5:MRR:5.1,703.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.19/0.48 706[5:MRR:2.1,703.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.19/0.48 708[5:MRR:4.1,703.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 709[5:MRR:3.1,703.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.19/0.48 733[5:SpR:708.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.19/0.48 735[5:Rew:705.0,733.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.19/0.48 741[5:SpR:735.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.19/0.48 743[5:Rew:27.0,741.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 744[5:Rew:743.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 745[5:Rew:743.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 747[5:Rew:743.0,27.0] || -> equal(multiply(inverse(u),u),sk_c6)**. % 0.19/0.48 748[5:Rew:744.0,704.0] || -> equal(sk_c7,sk_c5)**. % 0.19/0.48 755[5:Rew:748.0,535.0] || -> equal(inverse(sk_c1),sk_c5)**. % 0.19/0.48 756[5:Rew:748.0,706.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.19/0.48 758[5:Rew:748.0,519.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.19/0.48 760[5:Rew:748.0,709.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.19/0.48 763[5:Rew:748.0,703.0] || equal(multiply(sk_c1,sk_c5),sk_c6)** -> . % 0.19/0.48 771[5:Rew:745.0,760.0] || -> equal(sk_c2,sk_c5)**. % 0.19/0.48 772[5:Rew:771.0,756.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.48 826[5:SpR:755.0,747.0] || -> equal(multiply(sk_c5,sk_c1),sk_c6)**. % 0.19/0.48 868[5:SpR:826.0,64.0] || -> equal(multiply(inverse(sk_c5),sk_c6),sk_c1)**. % 0.19/0.48 870[5:Rew:745.0,868.0,772.0,868.0] || -> equal(sk_c5,sk_c1)**. % 0.19/0.48 875[5:Rew:870.0,758.0] || -> equal(multiply(sk_c1,sk_c1),sk_c6)**. % 0.19/0.48 876[5:Rew:870.0,763.0] || equal(multiply(sk_c1,sk_c1),sk_c6)** -> . % 0.19/0.48 883[5:Rew:875.0,876.0] || equal(sk_c6,sk_c6)* -> . % 0.19/0.48 884[5:Obv:883.0] || -> . % 0.19/0.48 888[4:Spt:884.0,7.0,535.0] || equal(inverse(sk_c1),sk_c7)** -> . % 0.19/0.48 889[4:Spt:884.0,7.1] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 890[4:MRR:11.1,888.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.19/0.48 891[4:MRR:8.1,888.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.19/0.48 893[4:MRR:10.0,888.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 894[4:MRR:9.0,888.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.19/0.48 895[4:Rew:889.0,530.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.19/0.48 896[4:Obv:895.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.19/0.48 916[4:SpR:893.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.19/0.48 918[4:Rew:890.0,916.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.19/0.48 927[4:SpR:918.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.19/0.48 929[4:Rew:27.0,927.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 930[4:Rew:929.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 931[4:Rew:929.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 934[4:Rew:930.0,889.0] || -> equal(sk_c7,sk_c5)**. % 0.19/0.48 941[4:Rew:934.0,891.0] || -> equal(inverse(sk_c2),sk_c5)**. % 0.19/0.48 942[4:Rew:934.0,519.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.19/0.48 946[4:Rew:934.0,894.0] || -> equal(multiply(sk_c2,sk_c6),sk_c5)**. % 0.19/0.48 949[4:Rew:934.0,896.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.19/0.48 955[4:Rew:931.0,946.0] || -> equal(sk_c2,sk_c5)**. % 0.19/0.48 956[4:Rew:955.0,941.0] || -> equal(inverse(sk_c5),sk_c5)**. % 0.19/0.48 966[4:Rew:934.0,949.3,931.0,949.2,934.0,949.2,934.0,949.1] || equal(inverse(u),sk_c5)** equal(inverse(v),sk_c5) equal(u,sk_c5) equal(multiply(v,sk_c5),sk_c6)**+ -> . % 0.19/0.48 1059[4:SpL:942.0,966.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c5),sk_c5)** equal(u,sk_c5) equal(sk_c6,sk_c6) -> . % 0.19/0.48 1062[4:Obv:1059.3] || equal(inverse(u),sk_c5)** equal(inverse(sk_c5),sk_c5)** equal(u,sk_c5) -> . % 0.19/0.48 1063[4:Rew:956.0,1062.1] || equal(inverse(u),sk_c5)** equal(sk_c5,sk_c5) equal(u,sk_c5) -> . % 0.19/0.48 1064[4:Obv:1063.1] || equal(inverse(u),sk_c5)** equal(u,sk_c5) -> . % 0.19/0.48 1086[4:SpL:956.0,1064.0] || equal(sk_c5,sk_c5)* equal(sk_c5,sk_c5)* -> . % 0.19/0.48 1089[4:Obv:1086.1] || -> . % 0.19/0.48 1091[3:Spt:1089.0,19.1,527.0] || equal(multiply(sk_c5,sk_c6),sk_c7)** -> . % 0.19/0.48 1092[3:Spt:1089.0,19.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 1093[3:MRR:23.1,1091.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.19/0.48 1096[3:MRR:22.1,1091.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 1112[3:SpR:1096.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.19/0.48 1114[3:Rew:1093.0,1112.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.19/0.48 1120[3:SpR:1114.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.19/0.48 1122[3:Rew:27.0,1120.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 1123[3:Rew:1122.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 1124[3:Rew:1122.0,155.0] || -> equal(multiply(u,sk_c6),u)**. % 0.19/0.48 1127[3:Rew:1123.0,1092.0] || -> equal(sk_c7,sk_c5)**. % 0.19/0.48 1138[3:Rew:1127.0,1091.0] || equal(multiply(sk_c5,sk_c6),sk_c5)** -> . % 0.19/0.48 1146[3:Rew:1124.0,1138.0] || equal(sk_c5,sk_c5)* -> . % 0.19/0.48 1147[3:Obv:1146.0] || -> . % 0.19/0.48 1155[2:Spt:1147.0,13.1,519.0] || equal(multiply(sk_c7,sk_c5),sk_c6)** -> . % 0.19/0.48 1156[2:Spt:1147.0,13.0] || -> equal(multiply(sk_c6,sk_c7),sk_c5)**. % 0.19/0.48 1157[2:MRR:17.1,1155.0] || -> equal(inverse(sk_c3),sk_c4)**. % 0.19/0.48 1158[2:MRR:14.1,1155.0] || -> equal(inverse(sk_c2),sk_c7)**. % 0.19/0.48 1160[2:MRR:16.1,1155.0] || -> equal(multiply(sk_c3,sk_c4),sk_c6)**. % 0.19/0.48 1161[2:MRR:15.1,1155.0] || -> equal(multiply(sk_c2,sk_c6),sk_c7)**. % 0.19/0.48 1173[2:SpR:1160.0,64.0] || -> equal(multiply(inverse(sk_c3),sk_c6),sk_c4)**. % 0.19/0.48 1175[2:Rew:1157.0,1173.0] || -> equal(multiply(sk_c4,sk_c6),sk_c4)**. % 0.19/0.48 1177[2:SpR:1161.0,64.0] || -> equal(multiply(inverse(sk_c2),sk_c7),sk_c6)**. % 0.19/0.48 1179[2:Rew:1158.0,1177.0] || -> equal(multiply(sk_c7,sk_c7),sk_c6)**. % 0.19/0.48 1184[2:SpR:1175.0,64.0] || -> equal(multiply(inverse(sk_c4),sk_c4),sk_c6)**. % 0.19/0.48 1186[2:Rew:27.0,1184.0] || -> equal(identity,sk_c6)**. % 0.19/0.48 1187[2:Rew:1186.0,26.0] || -> equal(multiply(sk_c6,u),u)**. % 0.19/0.48 1191[2:Rew:1187.0,1156.0] || -> equal(sk_c7,sk_c5)**. % 0.19/0.48 1199[2:Rew:1191.0,1155.0] || equal(multiply(sk_c5,sk_c5),sk_c6)** -> . % 0.19/0.48 1203[2:Rew:1191.0,1179.0] || -> equal(multiply(sk_c5,sk_c5),sk_c6)**. % 0.19/0.48 1206[2:Rew:1203.0,1199.0] || equal(sk_c6,sk_c6)* -> . % 0.19/0.48 1207[2:Obv:1206.0] || -> . % 0.19/0.48 % SZS output end Refutation % 0.19/0.48 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_21 prove_this_22 prove_this_23 prove_this_25 left_identity left_inverse associativity % 0.19/0.48 %------------------------------------------------------------------------------