%------------------------------------------------------------------------------ % File : SPASS---3.9 % Problem : GRP385-1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp % Command : run_spass %d %s % Computer : n027.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.49s % Output : Refutation 0.18s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.11 % Problem : GRP385-1 : TPTP v8.1.0. Released v2.5.0. % 0.10/0.12 % Command : run_spass %d %s % 0.12/0.33 % Computer : n027.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 02:27:32 EDT 2022 % 0.12/0.33 % CPUTime : % 0.18/0.49 % 0.18/0.49 SPASS V 3.9 % 0.18/0.49 SPASS beiseite: Proof found. % 0.18/0.49 % SZS status Theorem % 0.18/0.49 Problem: /export/starexec/sandbox/benchmark/theBenchmark.p % 0.18/0.49 SPASS derived 1087 clauses, backtracked 428 clauses, performed 10 splits and kept 909 clauses. % 0.18/0.49 SPASS allocated 63777 KBytes. % 0.18/0.49 SPASS spent 0:00:00.15 on the problem. % 0.18/0.49 0:00:00.03 for the input. % 0.18/0.49 0:00:00.00 for the FLOTTER CNF translation. % 0.18/0.49 0:00:00.01 for inferences. % 0.18/0.49 0:00:00.00 for the backtracking. % 0.18/0.49 0:00:00.08 for the reduction. % 0.18/0.49 % 0.18/0.49 % 0.18/0.49 Here is a proof with depth 5, length 272 : % 0.18/0.49 % SZS output start Refutation % 0.18/0.49 1[0:Inp] || -> equal(inverse(sk_c10),sk_c9)**. % 0.18/0.49 2[0:Inp] || -> equal(multiply(sk_c10,sk_c4),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.18/0.49 3[0:Inp] || -> equal(multiply(sk_c3,sk_c10),sk_c4)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.18/0.49 4[0:Inp] || -> equal(inverse(sk_c3),sk_c10) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.49 5[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c8)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.18/0.49 6[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.49 8[0:Inp] || -> equal(inverse(sk_c7),sk_c10) equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.49 9[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c10)** equal(multiply(sk_c9,sk_c8),sk_c10). % 0.18/0.49 10[0:Inp] || -> equal(multiply(sk_c10,sk_c4),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9). % 0.18/0.49 11[0:Inp] || -> equal(multiply(sk_c3,sk_c10),sk_c4) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.49 12[0:Inp] || -> equal(inverse(sk_c3),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.49 13[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c8) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.49 14[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.49 16[0:Inp] || -> equal(inverse(sk_c7),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.49 17[0:Inp] || -> equal(multiply(sk_c7,sk_c8),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.49 18[0:Inp] || -> equal(multiply(sk_c10,sk_c4),sk_c9) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.18/0.49 19[0:Inp] || -> equal(multiply(sk_c3,sk_c10),sk_c4) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.18/0.49 20[0:Inp] || -> equal(inverse(sk_c3),sk_c10) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.18/0.49 21[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c8) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.18/0.49 22[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.18/0.49 26[0:Inp] || -> equal(multiply(sk_c10,sk_c4),sk_c9)** equal(multiply(sk_c1,sk_c10),sk_c2). % 0.18/0.49 27[0:Inp] || -> equal(multiply(sk_c3,sk_c10),sk_c4) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.18/0.49 28[0:Inp] || -> equal(inverse(sk_c3),sk_c10) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.18/0.49 29[0:Inp] || -> equal(multiply(sk_c5,sk_c6),sk_c8) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.18/0.49 30[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.18/0.49 37[0:Inp] || -> equal(inverse(sk_c1),sk_c10) equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 38[0:Inp] || -> equal(inverse(sk_c5),sk_c6) equal(inverse(sk_c1),sk_c10)**. % 0.18/0.49 42[0:Inp] || equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c9,sk_c8),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c10,u),sk_c9)** equal(multiply(v,sk_c10),u)* equal(inverse(v),sk_c10) equal(multiply(sk_c10,w),sk_c9)** equal(multiply(x,sk_c10),w)* equal(inverse(x),sk_c10) equal(multiply(y,z),sk_c8)** equal(inverse(y),z) equal(multiply(z,sk_c9),sk_c8)** equal(inverse(x1),sk_c10) equal(multiply(x1,sk_c8),sk_c10)** -> . % 0.18/0.49 43[0:Inp] || -> equal(multiply(identity,u),u)**. % 0.18/0.49 44[0:Inp] || -> equal(multiply(inverse(u),u),identity)**. % 0.18/0.49 45[0:Inp] || -> equal(multiply(multiply(u,v),w),multiply(u,multiply(v,w)))**. % 0.18/0.49 46[0:Con:42.6] || equal(inverse(sk_c10),sk_c9) equal(multiply(sk_c9,sk_c8),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c10,u),sk_c9)** equal(multiply(v,sk_c10),u)* equal(inverse(v),sk_c10) equal(multiply(w,x),sk_c8)** equal(inverse(w),x) equal(multiply(x,sk_c9),sk_c8)** equal(inverse(y),sk_c10) equal(multiply(y,sk_c8),sk_c10)** -> . % 0.18/0.49 47[0:Rew:1.0,46.0] || equal(sk_c9,sk_c9) equal(multiply(sk_c9,sk_c8),sk_c10) equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c10,u),sk_c9)** equal(multiply(v,sk_c10),u)* equal(inverse(v),sk_c10) equal(multiply(w,x),sk_c8)** equal(inverse(w),x) equal(multiply(x,sk_c9),sk_c8)** equal(inverse(y),sk_c10) equal(multiply(y,sk_c8),sk_c10)** -> . % 0.18/0.49 48[0:Obv:47.0] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(inverse(x),sk_c10) equal(multiply(u,v),sk_c8)**+ equal(multiply(x,sk_c10),y)* equal(multiply(w,sk_c8),sk_c10)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(sk_c10,y),sk_c9)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) -> . % 0.18/0.49 49[1:Spt:48.2,48.4,48.7] || equal(inverse(u),sk_c10) equal(multiply(u,sk_c10),v)*+ equal(multiply(sk_c10,v),sk_c9)** -> . % 0.18/0.49 51[2:Spt:14.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.49 53[3:Spt:6.1] || -> equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.49 55[4:Spt:38.1] || -> equal(inverse(sk_c1),sk_c10)**. % 0.18/0.49 57[5:Spt:30.1] || -> equal(multiply(sk_c1,sk_c10),sk_c2)**. % 0.18/0.49 63[6:Spt:22.1] || -> equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.18/0.49 68[4:SpR:55.0,44.0] || -> equal(multiply(sk_c10,sk_c1),identity)**. % 0.18/0.49 69[0:SpR:1.0,44.0] || -> equal(multiply(sk_c9,sk_c10),identity)**. % 0.18/0.49 70[1:SpL:44.0,49.1] || equal(inverse(inverse(sk_c10)),sk_c10) equal(identity,u) equal(multiply(sk_c10,u),sk_c9)** -> . % 0.18/0.49 71[1:Rew:1.0,70.0] || equal(inverse(sk_c9),sk_c10) equal(identity,u) equal(multiply(sk_c10,u),sk_c9)** -> . % 0.18/0.49 76[2:SpR:51.0,45.0] || -> equal(multiply(sk_c10,multiply(sk_c8,u)),multiply(sk_c9,u))**. % 0.18/0.49 78[4:SpR:68.0,45.0] || -> equal(multiply(sk_c10,multiply(sk_c1,u)),multiply(identity,u))**. % 0.18/0.49 81[0:SpR:44.0,45.0] || -> equal(multiply(inverse(u),multiply(u,v)),multiply(identity,v))**. % 0.18/0.49 83[4:Rew:43.0,78.0] || -> equal(multiply(sk_c10,multiply(sk_c1,u)),u)**. % 0.18/0.49 84[0:Rew:43.0,81.0] || -> equal(multiply(inverse(u),multiply(u,v)),v)**. % 0.18/0.49 87[0:SpR:69.0,45.0] || -> equal(multiply(sk_c9,multiply(sk_c10,u)),multiply(identity,u))**. % 0.18/0.49 89[0:Rew:43.0,87.0] || -> equal(multiply(sk_c9,multiply(sk_c10,u)),u)**. % 0.18/0.49 92[5:SpR:57.0,83.0] || -> equal(multiply(sk_c10,sk_c2),sk_c10)**. % 0.18/0.49 93[6:Rew:63.0,92.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 95[6:Rew:93.0,51.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.18/0.49 99[6:Rew:93.0,1.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.18/0.49 102[6:Rew:93.0,69.0] || -> equal(multiply(sk_c9,sk_c9),identity)**. % 0.18/0.49 105[6:Rew:93.0,71.2] || equal(inverse(sk_c9),sk_c10) equal(identity,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 110[6:Rew:93.0,89.0] || -> equal(multiply(sk_c9,multiply(sk_c9,u)),u)**. % 0.18/0.49 117[6:Rew:99.0,105.0,93.0,105.0] || equal(sk_c9,sk_c9) equal(identity,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 118[6:Obv:117.0] || equal(identity,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 146[6:SpR:95.0,110.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.18/0.49 151[6:Rew:102.0,146.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 153[6:Rew:151.0,44.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.18/0.49 156[6:Rew:151.0,118.0] || equal(sk_c8,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 191[0:SpR:84.0,84.0] || -> equal(multiply(inverse(inverse(u)),v),multiply(u,v))**. % 0.18/0.49 198[6:SpR:153.0,84.0] || -> equal(multiply(inverse(inverse(u)),sk_c8),u)**. % 0.18/0.49 202[6:Rew:191.0,198.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 228[0:SpR:191.0,84.0] || -> equal(multiply(u,multiply(inverse(u),v)),v)**. % 0.18/0.49 247[6:SpL:202.0,156.1] || equal(sk_c8,sk_c8)* equal(sk_c9,sk_c9) -> . % 0.18/0.49 250[6:Obv:247.1] || -> . % 0.18/0.49 252[6:Spt:250.0,22.1,63.0] || equal(multiply(sk_c10,sk_c2),sk_c9)** -> . % 0.18/0.49 253[6:Spt:250.0,22.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 254[6:Rew:92.0,252.0] || equal(sk_c10,sk_c9)** -> . % 0.18/0.49 257[5:Rew:92.0,20.1] || -> equal(inverse(sk_c3),sk_c10)** equal(sk_c10,sk_c9). % 0.18/0.49 258[6:MRR:257.1,254.0] || -> equal(inverse(sk_c3),sk_c10)**. % 0.18/0.49 265[5:Rew:92.0,19.1] || -> equal(multiply(sk_c3,sk_c10),sk_c4)** equal(sk_c10,sk_c9). % 0.18/0.49 266[6:MRR:265.1,254.0] || -> equal(multiply(sk_c3,sk_c10),sk_c4)**. % 0.18/0.49 267[5:Rew:92.0,18.1] || -> equal(multiply(sk_c10,sk_c4),sk_c9)** equal(sk_c10,sk_c9). % 0.18/0.49 268[6:MRR:267.1,254.0] || -> equal(multiply(sk_c10,sk_c4),sk_c9)**. % 0.18/0.49 309[2:SpR:51.0,84.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.18/0.49 311[2:Rew:1.0,309.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.18/0.49 320[6:SpR:266.0,84.0] || -> equal(multiply(inverse(sk_c3),sk_c4),sk_c10)**. % 0.18/0.49 322[6:Rew:258.0,320.0] || -> equal(multiply(sk_c10,sk_c4),sk_c10)**. % 0.18/0.49 323[6:Rew:268.0,322.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 324[6:MRR:323.0,254.0] || -> . % 0.18/0.49 325[5:Spt:324.0,30.1,57.0] || equal(multiply(sk_c1,sk_c10),sk_c2)** -> . % 0.18/0.49 326[5:Spt:324.0,30.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 328[5:MRR:28.1,325.0] || -> equal(inverse(sk_c3),sk_c10)**. % 0.18/0.49 332[5:MRR:27.1,325.0] || -> equal(multiply(sk_c3,sk_c10),sk_c4)**. % 0.18/0.49 333[5:MRR:26.1,325.0] || -> equal(multiply(sk_c10,sk_c4),sk_c9)**. % 0.18/0.49 349[0:SpR:69.0,84.0] || -> equal(multiply(inverse(sk_c9),identity),sk_c10)**. % 0.18/0.49 364[5:SpR:332.0,84.0] || -> equal(multiply(inverse(sk_c3),sk_c4),sk_c10)**. % 0.18/0.49 366[5:Rew:328.0,364.0] || -> equal(multiply(sk_c10,sk_c4),sk_c10)**. % 0.18/0.49 367[5:Rew:333.0,366.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 368[5:Rew:367.0,1.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.18/0.49 375[5:Rew:367.0,69.0] || -> equal(multiply(sk_c9,sk_c9),identity)**. % 0.18/0.49 382[5:Rew:367.0,71.2] || equal(inverse(sk_c9),sk_c10) equal(identity,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 396[5:Rew:311.0,375.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 398[5:Rew:396.0,44.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.18/0.49 420[5:Rew:396.0,382.1,368.0,382.0,367.0,382.0] || equal(sk_c9,sk_c9) equal(sk_c8,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 421[5:Obv:420.0] || equal(sk_c8,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 471[5:SpR:398.0,84.0] || -> equal(multiply(inverse(inverse(u)),sk_c8),u)**. % 0.18/0.49 477[5:Rew:191.0,471.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 591[5:SpL:477.0,421.1] || equal(sk_c8,sk_c8)* equal(sk_c9,sk_c9) -> . % 0.18/0.49 595[5:Obv:591.1] || -> . % 0.18/0.49 598[4:Spt:595.0,38.1,55.0] || equal(inverse(sk_c1),sk_c10)** -> . % 0.18/0.49 599[4:Spt:595.0,38.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 604[4:MRR:37.0,598.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 608[4:SpR:599.0,228.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.49 637[4:SpR:604.0,45.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 641[4:Rew:608.0,637.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 642[4:Rew:641.0,76.0] || -> equal(multiply(sk_c10,u),multiply(sk_c9,u))**. % 0.18/0.49 647[4:Rew:642.0,51.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.18/0.49 657[4:Rew:642.0,71.2] || equal(inverse(sk_c9),sk_c10) equal(identity,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 661[4:Rew:53.0,647.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 662[4:Rew:661.0,1.0] || -> equal(inverse(sk_c9),sk_c9)**. % 0.18/0.49 665[4:Rew:661.0,69.0] || -> equal(multiply(sk_c9,sk_c9),identity)**. % 0.18/0.49 675[4:Rew:311.0,665.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 677[4:Rew:675.0,44.0] || -> equal(multiply(inverse(u),u),sk_c8)**. % 0.18/0.49 687[4:Rew:675.0,657.1,662.0,657.0,661.0,657.0] || equal(sk_c9,sk_c9) equal(sk_c8,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 688[4:Obv:687.0] || equal(sk_c8,u) equal(multiply(sk_c9,u),sk_c9)** -> . % 0.18/0.49 738[4:SpR:677.0,228.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 826[4:SpL:738.0,688.1] || equal(sk_c8,sk_c8)* equal(sk_c9,sk_c9) -> . % 0.18/0.49 829[4:Obv:826.1] || -> . % 0.18/0.49 832[3:Spt:829.0,6.1,53.0] || equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.18/0.49 833[3:Spt:829.0,6.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 836[3:MRR:9.1,832.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.49 838[3:MRR:5.1,832.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 842[3:SpR:833.0,228.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.49 857[3:SpR:836.0,45.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),multiply(sk_c10,u))**. % 0.18/0.49 868[3:SpR:838.0,45.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 872[3:Rew:842.0,868.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 874[3:Rew:872.0,76.0] || -> equal(multiply(sk_c10,u),multiply(sk_c9,u))**. % 0.18/0.49 875[3:Rew:872.0,857.0] || -> equal(multiply(sk_c10,u),multiply(sk_c7,u))**. % 0.18/0.49 877[3:Rew:874.0,51.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.18/0.49 891[3:Rew:877.0,832.0] || equal(sk_c10,sk_c9)** -> . % 0.18/0.49 899[3:Rew:874.0,875.0] || -> equal(multiply(sk_c7,u),multiply(sk_c9,u))**. % 0.18/0.49 900[3:Rew:899.0,836.0] || -> equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.49 901[3:Rew:877.0,900.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 902[3:MRR:901.0,891.0] || -> . % 0.18/0.49 907[2:Spt:902.0,14.1,51.0] || equal(multiply(sk_c10,sk_c8),sk_c9)** -> . % 0.18/0.49 908[2:Spt:902.0,14.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 910[2:MRR:12.1,907.0] || -> equal(inverse(sk_c3),sk_c10)**. % 0.18/0.49 911[2:MRR:17.1,907.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.49 913[2:MRR:13.1,907.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 914[2:MRR:11.1,907.0] || -> equal(multiply(sk_c3,sk_c10),sk_c4)**. % 0.18/0.49 915[2:MRR:10.1,907.0] || -> equal(multiply(sk_c10,sk_c4),sk_c9)**. % 0.18/0.49 917[2:SpR:908.0,228.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.49 929[2:SpR:911.0,45.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),multiply(sk_c10,u))**. % 0.18/0.49 936[2:SpR:913.0,45.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 940[2:Rew:917.0,936.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 941[2:Rew:940.0,929.0] || -> equal(multiply(sk_c10,u),multiply(sk_c7,u))**. % 0.18/0.49 946[2:Rew:941.0,915.0] || -> equal(multiply(sk_c7,sk_c4),sk_c9)**. % 0.18/0.49 956[2:Rew:941.0,907.0] || equal(multiply(sk_c7,sk_c8),sk_c9)** -> . % 0.18/0.49 957[2:Rew:911.0,956.0] || equal(sk_c10,sk_c9)** -> . % 0.18/0.49 959[2:SpR:914.0,84.0] || -> equal(multiply(inverse(sk_c3),sk_c4),sk_c10)**. % 0.18/0.49 961[2:Rew:910.0,959.0] || -> equal(multiply(sk_c10,sk_c4),sk_c10)**. % 0.18/0.49 962[2:Rew:946.0,961.0,941.0,961.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 963[2:MRR:962.0,957.0] || -> . % 0.18/0.49 965[1:Spt:963.0,48.0,48.1,48.3,48.5,48.6,48.8,48.9] || equal(inverse(u),v) equal(inverse(w),sk_c10) equal(multiply(u,v),sk_c8)**+ equal(multiply(w,sk_c8),sk_c10)** equal(multiply(v,sk_c9),sk_c8)** equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) -> . % 0.18/0.49 969[1:SpL:69.0,965.2] || equal(inverse(sk_c9),sk_c10) equal(inverse(u),sk_c10) equal(identity,sk_c8) equal(multiply(u,sk_c8),sk_c10)** equal(multiply(sk_c10,sk_c9),sk_c8) equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) -> . % 0.18/0.49 970[1:Con:969.1] || equal(inverse(sk_c9),sk_c10) equal(identity,sk_c8) equal(multiply(sk_c10,sk_c9),sk_c8) equal(multiply(sk_c10,sk_c8),sk_c9)** equal(multiply(sk_c9,sk_c8),sk_c10) -> . % 0.18/0.49 973[2:Spt:6.1] || -> equal(multiply(sk_c9,sk_c8),sk_c10)**. % 0.18/0.49 978[2:Rew:973.0,970.4] || equal(inverse(sk_c9),sk_c10) equal(identity,sk_c8) equal(multiply(sk_c10,sk_c9),sk_c8) equal(multiply(sk_c10,sk_c8),sk_c9)** equal(sk_c10,sk_c10) -> . % 0.18/0.49 979[2:Obv:978.4] || equal(inverse(sk_c9),sk_c10) equal(identity,sk_c8) equal(multiply(sk_c10,sk_c9),sk_c8) equal(multiply(sk_c10,sk_c8),sk_c9)** -> . % 0.18/0.49 984[2:SpR:973.0,45.0] || -> equal(multiply(sk_c9,multiply(sk_c8,u)),multiply(sk_c10,u))**. % 0.18/0.49 985[2:SpR:973.0,84.0] || -> equal(multiply(inverse(sk_c9),sk_c10),sk_c8)**. % 0.18/0.49 987[3:Spt:16.1] || -> equal(multiply(sk_c10,sk_c8),sk_c9)**. % 0.18/0.49 992[3:Rew:987.0,979.3] || equal(inverse(sk_c9),sk_c10) equal(identity,sk_c8) equal(multiply(sk_c10,sk_c9),sk_c8)** equal(sk_c9,sk_c9) -> . % 0.18/0.49 993[3:Obv:992.3] || equal(inverse(sk_c9),sk_c10) equal(identity,sk_c8) equal(multiply(sk_c10,sk_c9),sk_c8)** -> . % 0.18/0.49 998[3:SpR:987.0,45.0] || -> equal(multiply(sk_c10,multiply(sk_c8,u)),multiply(sk_c9,u))**. % 0.18/0.49 999[3:SpR:987.0,84.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c8)**. % 0.18/0.49 1001[3:Rew:1.0,999.0] || -> equal(multiply(sk_c9,sk_c9),sk_c8)**. % 0.18/0.49 1002[4:Spt:38.1] || -> equal(inverse(sk_c1),sk_c10)**. % 0.18/0.49 1006[5:Spt:22.1] || -> equal(multiply(sk_c10,sk_c2),sk_c9)**. % 0.18/0.49 1008[5:SpR:1006.0,84.0] || -> equal(multiply(inverse(sk_c10),sk_c9),sk_c2)**. % 0.18/0.49 1010[5:Rew:1.0,1008.0] || -> equal(multiply(sk_c9,sk_c9),sk_c2)**. % 0.18/0.49 1011[5:Rew:1001.0,1010.0] || -> equal(sk_c2,sk_c8)**. % 0.18/0.49 1015[5:Rew:1011.0,29.1] || -> equal(multiply(sk_c5,sk_c6),sk_c8) equal(multiply(sk_c1,sk_c10),sk_c8)**. % 0.18/0.49 1020[5:Rew:1011.0,30.1] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c1,sk_c10),sk_c8)**. % 0.18/0.49 1032[0:SpR:44.0,228.0] || -> equal(multiply(u,identity),u)**. % 0.18/0.49 1035[4:SpR:1002.0,44.0] || -> equal(multiply(sk_c10,sk_c1),identity)**. % 0.18/0.49 1036[0:Rew:1032.0,349.0] || -> equal(inverse(sk_c9),sk_c10)**. % 0.18/0.49 1037[2:Rew:1036.0,985.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.18/0.49 1038[3:Rew:1036.0,993.0] || equal(sk_c10,sk_c10) equal(identity,sk_c8) equal(multiply(sk_c10,sk_c9),sk_c8)** -> . % 0.18/0.49 1042[3:Obv:1038.0] || equal(identity,sk_c8) equal(multiply(sk_c10,sk_c9),sk_c8)** -> . % 0.18/0.49 1045[0:SpR:1036.0,44.0] || -> equal(multiply(sk_c10,sk_c9),identity)**. % 0.18/0.49 1047[3:Rew:1045.0,1042.1] || equal(identity,sk_c8)** equal(identity,sk_c8)** -> . % 0.18/0.49 1048[3:Obv:1047.0] || equal(identity,sk_c8)** -> . % 0.18/0.49 1050[4:SpR:1035.0,84.0] || -> equal(multiply(inverse(sk_c10),identity),sk_c1)**. % 0.18/0.49 1052[4:Rew:1.0,1050.0] || -> equal(multiply(sk_c9,identity),sk_c1)**. % 0.18/0.49 1053[4:Rew:1032.0,1052.0] || -> equal(sk_c1,sk_c9)**. % 0.18/0.49 1060[5:Rew:1053.0,1015.1] || -> equal(multiply(sk_c5,sk_c6),sk_c8)** equal(multiply(sk_c9,sk_c10),sk_c8). % 0.18/0.49 1063[5:Rew:1053.0,1020.1] || -> equal(inverse(sk_c5),sk_c6) equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.18/0.49 1068[5:Rew:69.0,1063.1] || -> equal(inverse(sk_c5),sk_c6)** equal(identity,sk_c8). % 0.18/0.49 1069[5:MRR:1068.1,1048.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 1078[5:Rew:69.0,1060.1] || -> equal(multiply(sk_c5,sk_c6),sk_c8)** equal(identity,sk_c8). % 0.18/0.49 1079[5:MRR:1078.1,1048.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 1086[5:SpR:1069.0,228.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.49 1113[5:SpR:1079.0,45.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 1117[5:Rew:1086.0,1113.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 1118[5:Rew:1117.0,984.0] || -> equal(multiply(sk_c10,u),multiply(sk_c9,u))**. % 0.18/0.49 1126[5:Rew:1118.0,987.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.18/0.49 1140[5:Rew:973.0,1126.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 1142[5:Rew:1140.0,69.0] || -> equal(multiply(sk_c9,sk_c9),identity)**. % 0.18/0.49 1154[5:Rew:1001.0,1142.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 1155[5:MRR:1154.0,1048.0] || -> . % 0.18/0.49 1166[5:Spt:1155.0,22.1,1006.0] || equal(multiply(sk_c10,sk_c2),sk_c9)** -> . % 0.18/0.49 1167[5:Spt:1155.0,22.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 1172[5:MRR:21.1,1166.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 1176[5:SpR:1167.0,228.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.49 1224[5:SpR:1172.0,45.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 1228[5:Rew:1176.0,1224.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 1231[5:Rew:1228.0,998.0] || -> equal(multiply(sk_c10,u),multiply(sk_c9,u))**. % 0.18/0.49 1237[5:Rew:1231.0,987.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.18/0.49 1253[5:Rew:973.0,1237.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 1260[5:Rew:1253.0,69.0] || -> equal(multiply(sk_c9,sk_c9),identity)**. % 0.18/0.49 1267[5:Rew:1001.0,1260.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 1268[5:MRR:1267.0,1048.0] || -> . % 0.18/0.49 1279[4:Spt:1268.0,38.1,1002.0] || equal(inverse(sk_c1),sk_c10)** -> . % 0.18/0.49 1280[4:Spt:1268.0,38.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 1285[4:MRR:37.0,1279.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 1289[4:SpR:1280.0,228.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.49 1337[4:SpR:1285.0,45.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 1341[4:Rew:1289.0,1337.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 1342[4:Rew:1341.0,984.0] || -> equal(multiply(sk_c10,u),multiply(sk_c9,u))**. % 0.18/0.49 1350[4:Rew:1342.0,987.0] || -> equal(multiply(sk_c9,sk_c8),sk_c9)**. % 0.18/0.49 1364[4:Rew:973.0,1350.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 1370[4:Rew:1364.0,69.0] || -> equal(multiply(sk_c9,sk_c9),identity)**. % 0.18/0.49 1379[4:Rew:1001.0,1370.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 1380[4:MRR:1379.0,1048.0] || -> . % 0.18/0.49 1391[3:Spt:1380.0,16.1,987.0] || equal(multiply(sk_c10,sk_c8),sk_c9)** -> . % 0.18/0.49 1392[3:Spt:1380.0,16.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.18/0.49 1394[3:MRR:14.1,1391.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 1397[3:MRR:13.1,1391.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 1417[3:SpR:1394.0,228.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.49 1445[3:SpR:1397.0,45.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 1449[3:Rew:1417.0,1445.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 1451[3:Rew:1449.0,984.0] || -> equal(multiply(sk_c10,u),multiply(sk_c9,u))**. % 0.18/0.49 1455[3:Rew:1451.0,1037.0] || -> equal(multiply(sk_c9,sk_c10),sk_c8)**. % 0.18/0.49 1466[3:Rew:1451.0,1391.0] || equal(multiply(sk_c9,sk_c8),sk_c9)** -> . % 0.18/0.49 1467[3:Rew:69.0,1455.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 1472[3:Rew:1467.0,1032.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 1496[3:Rew:1472.0,1466.0] || equal(sk_c9,sk_c9)* -> . % 0.18/0.49 1497[3:Obv:1496.0] || -> . % 0.18/0.49 1503[2:Spt:1497.0,6.1,973.0] || equal(multiply(sk_c9,sk_c8),sk_c10)** -> . % 0.18/0.49 1504[2:Spt:1497.0,6.0] || -> equal(inverse(sk_c5),sk_c6)**. % 0.18/0.49 1505[2:MRR:8.1,1503.0] || -> equal(inverse(sk_c7),sk_c10)**. % 0.18/0.49 1506[2:MRR:4.1,1503.0] || -> equal(inverse(sk_c3),sk_c10)**. % 0.18/0.49 1507[2:MRR:9.1,1503.0] || -> equal(multiply(sk_c7,sk_c8),sk_c10)**. % 0.18/0.49 1509[2:MRR:5.1,1503.0] || -> equal(multiply(sk_c5,sk_c6),sk_c8)**. % 0.18/0.49 1510[2:MRR:3.1,1503.0] || -> equal(multiply(sk_c3,sk_c10),sk_c4)**. % 0.18/0.49 1511[2:MRR:2.1,1503.0] || -> equal(multiply(sk_c10,sk_c4),sk_c9)**. % 0.18/0.49 1513[2:SpR:1504.0,228.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),u)**. % 0.18/0.49 1537[2:SpR:1507.0,45.0] || -> equal(multiply(sk_c7,multiply(sk_c8,u)),multiply(sk_c10,u))**. % 0.18/0.49 1538[2:SpR:1507.0,84.0] || -> equal(multiply(inverse(sk_c7),sk_c10),sk_c8)**. % 0.18/0.49 1540[2:Rew:1505.0,1538.0] || -> equal(multiply(sk_c10,sk_c10),sk_c8)**. % 0.18/0.49 1544[2:SpR:1509.0,45.0] || -> equal(multiply(sk_c5,multiply(sk_c6,u)),multiply(sk_c8,u))**. % 0.18/0.49 1548[2:Rew:1513.0,1544.0] || -> equal(multiply(sk_c8,u),u)**. % 0.18/0.49 1549[2:Rew:1548.0,1537.0] || -> equal(multiply(sk_c10,u),multiply(sk_c7,u))**. % 0.18/0.49 1551[2:Rew:1549.0,1045.0] || -> equal(multiply(sk_c7,sk_c9),identity)**. % 0.18/0.49 1552[2:Rew:1549.0,1540.0] || -> equal(multiply(sk_c7,sk_c10),sk_c8)**. % 0.18/0.49 1553[2:Rew:1549.0,1511.0] || -> equal(multiply(sk_c7,sk_c4),sk_c9)**. % 0.18/0.49 1561[2:SpR:1510.0,84.0] || -> equal(multiply(inverse(sk_c3),sk_c4),sk_c10)**. % 0.18/0.49 1563[2:Rew:1506.0,1561.0] || -> equal(multiply(sk_c10,sk_c4),sk_c10)**. % 0.18/0.49 1564[2:Rew:1553.0,1563.0,1549.0,1563.0] || -> equal(sk_c10,sk_c9)**. % 0.18/0.49 1572[2:Rew:1564.0,1503.0] || equal(multiply(sk_c9,sk_c8),sk_c9)** -> . % 0.18/0.49 1574[2:Rew:1564.0,1552.0] || -> equal(multiply(sk_c7,sk_c9),sk_c8)**. % 0.18/0.49 1575[2:Rew:1551.0,1574.0] || -> equal(identity,sk_c8)**. % 0.18/0.49 1577[2:Rew:1575.0,1032.0] || -> equal(multiply(u,sk_c8),u)**. % 0.18/0.49 1592[2:Rew:1577.0,1572.0] || equal(sk_c9,sk_c9)* -> . % 0.18/0.49 1593[2:Obv:1592.0] || -> . % 0.18/0.49 % SZS output end Refutation % 0.18/0.49 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_8 prove_this_9 prove_this_10 prove_this_11 prove_this_12 prove_this_13 prove_this_14 prove_this_16 prove_this_17 prove_this_18 prove_this_19 prove_this_20 prove_this_21 prove_this_22 prove_this_26 prove_this_27 prove_this_28 prove_this_29 prove_this_30 prove_this_37 prove_this_38 prove_this_42 left_identity left_inverse associativity % 0.18/0.49 %------------------------------------------------------------------------------