%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : GRP683+1 : TPTP v9.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : duper %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 : 300s % DateTime : Fri Oct 3 07:49:55 PM UTC 2025 % Result : Theorem 163.75s 163.98s % Output : Proof 164.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : GRP683+1 : TPTP v9.2.0. Released v4.0.0. % 0.06/0.13 % Command : duper %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 : 300 % 0.13/0.34 % DateTime : Thu Oct 2 17:29:23 EDT 2025 % 0.13/0.34 % CPUTime : % 163.75/163.98 SZS status Theorem for theBenchmark.p % 163.75/163.98 SZS output start Proof for theBenchmark.p % 163.75/163.98 Clause #0 (by assumption #[]): Eq (∀ (A : Iota), Eq (ld A (mult A A)) A) True % 163.75/163.98 Clause #1 (by assumption #[]): Eq (∀ (A : Iota), Eq (rd (mult A A) A) A) True % 163.75/163.98 Clause #2 (by assumption #[]): Eq (∀ (B A : Iota), Eq (mult A (ld A B)) (ld A (mult A B))) True % 163.75/163.98 Clause #3 (by assumption #[]): Eq (∀ (B A : Iota), Eq (mult (rd A B) B) (rd (mult A B) B)) True % 163.75/163.98 Clause #4 (by assumption #[]): Eq (∀ (D C B A : Iota), Eq (ld (ld A B) (mult (ld A B) (mult C D))) (mult (ld A (mult A C)) D)) True % 163.75/163.98 Clause #5 (by assumption #[]): Eq (∀ (D C B A : Iota), Eq (rd (mult (mult A B) (rd C D)) (rd C D)) (mult A (rd (mult B D) D))) True % 163.75/163.98 Clause #6 (by assumption #[]): Eq (∀ (B A : Iota), Eq (ld A (mult A (ld B B))) (rd (mult (rd A A) B) B)) True % 163.75/163.98 Clause #7 (by assumption #[]): Eq % 163.75/163.98 (Not % 163.75/163.98 (∀ (X3 X4 X5 : Iota), % 163.75/163.98 And (Eq (mult X3 (ld X4 (mult X4 X5))) (mult X3 X5)) (Eq (mult (rd (mult X3 X4) X4) X5) (mult X3 X5)))) % 163.75/163.98 True % 163.75/163.98 Clause #8 (by clausification #[1]): ∀ (a : Iota), Eq (Eq (rd (mult a a) a) a) True % 163.75/163.98 Clause #9 (by clausification #[8]): ∀ (a : Iota), Eq (rd (mult a a) a) a % 163.75/163.98 Clause #10 (by clausification #[0]): ∀ (a : Iota), Eq (Eq (ld a (mult a a)) a) True % 163.75/163.98 Clause #11 (by clausification #[10]): ∀ (a : Iota), Eq (ld a (mult a a)) a % 163.75/163.98 Clause #12 (by clausification #[3]): ∀ (a : Iota), Eq (∀ (A : Iota), Eq (mult (rd A a) a) (rd (mult A a) a)) True % 163.75/163.98 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), Eq (Eq (mult (rd a a_1) a_1) (rd (mult a a_1) a_1)) True % 163.75/163.98 Clause #14 (by clausification #[13]): ∀ (a a_1 : Iota), Eq (mult (rd a a_1) a_1) (rd (mult a a_1) a_1) % 163.75/163.98 Clause #15 (by superposition #[14, 9]): ∀ (a : Iota), Eq (mult (rd a a) a) a % 163.75/163.98 Clause #16 (by superposition #[15, 14]): ∀ (a : Iota), Eq (mult (rd (rd a a) a) a) (rd a a) % 163.75/163.98 Clause #18 (by clausification #[2]): ∀ (a : Iota), Eq (∀ (A : Iota), Eq (mult A (ld A a)) (ld A (mult A a))) True % 163.75/163.98 Clause #19 (by clausification #[18]): ∀ (a a_1 : Iota), Eq (Eq (mult a (ld a a_1)) (ld a (mult a a_1))) True % 163.75/163.98 Clause #20 (by clausification #[19]): ∀ (a a_1 : Iota), Eq (mult a (ld a a_1)) (ld a (mult a a_1)) % 163.75/163.98 Clause #21 (by superposition #[20, 11]): ∀ (a : Iota), Eq (mult a (ld a a)) a % 163.75/163.98 Clause #22 (by superposition #[20, 15]): ∀ (a : Iota), Eq (mult (rd a a) (ld (rd a a) a)) (ld (rd a a) a) % 163.75/163.98 Clause #24 (by superposition #[21, 14]): ∀ (a : Iota), Eq (mult (rd a (ld a a)) (ld a a)) (rd a (ld a a)) % 163.75/163.98 Clause #25 (by superposition #[21, 20]): ∀ (a : Iota), Eq (mult a (ld a (ld a a))) (ld a a) % 163.75/163.98 Clause #34 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (C B A : Iota), Eq (ld (ld A B) (mult (ld A B) (mult C a))) (mult (ld A (mult A C)) a)) True % 163.75/163.98 Clause #35 (by clausification #[34]): ∀ (a a_1 : Iota), Eq (∀ (B A : Iota), Eq (ld (ld A B) (mult (ld A B) (mult a a_1))) (mult (ld A (mult A a)) a_1)) True % 163.75/163.98 Clause #36 (by clausification #[35]): ∀ (a a_1 a_2 : Iota), % 163.75/163.98 Eq (∀ (A : Iota), Eq (ld (ld A a) (mult (ld A a) (mult a_1 a_2))) (mult (ld A (mult A a_1)) a_2)) True % 163.75/163.98 Clause #37 (by clausification #[36]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Eq (ld (ld a a_1) (mult (ld a a_1) (mult a_2 a_3))) (mult (ld a (mult a a_2)) a_3)) True % 163.75/163.98 Clause #38 (by clausification #[37]): ∀ (a a_1 a_2 a_3 : Iota), Eq (ld (ld a a_1) (mult (ld a a_1) (mult a_2 a_3))) (mult (ld a (mult a a_2)) a_3) % 163.75/163.98 Clause #39 (by forward demodulation #[38, 20]): ∀ (a a_1 a_2 a_3 : Iota), Eq (ld (ld a a_1) (mult (ld a a_1) (mult a_2 a_3))) (mult (mult a (ld a a_2)) a_3) % 163.75/163.98 Clause #40 (by superposition #[39, 20]): ∀ (a a_1 a_2 a_3 : Iota), Eq (mult (ld a a_1) (ld (ld a a_1) (mult a_2 a_3))) (mult (mult a (ld a a_2)) a_3) % 163.75/163.98 Clause #49 (by superposition #[39, 11]): ∀ (a a_1 a_2 : Iota), Eq (ld a (mult a (mult a_1 a_2))) (mult (mult a (ld a a_1)) a_2) % 163.75/163.98 Clause #50 (by superposition #[39, 20]): ∀ (a a_1 a_2 a_3 : Iota), % 163.75/163.98 Eq (ld (mult a (ld a a_1)) (mult (mult a (ld a a_1)) (mult a_2 a_3))) (mult (mult a (ld a a_2)) a_3) % 163.75/163.98 Clause #53 (by superposition #[49, 20]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (mult a_1 a_2))) (mult (mult a (ld a a_1)) a_2) % 163.75/163.98 Clause #62 (by superposition #[49, 15]): ∀ (a a_1 : Iota), Eq (ld a (mult a a_1)) (mult (mult a (ld a (rd a_1 a_1))) a_1) % 163.85/164.01 Clause #65 (by forward demodulation #[62, 20]): ∀ (a a_1 : Iota), Eq (mult a (ld a a_1)) (mult (mult a (ld a (rd a_1 a_1))) a_1) % 163.85/164.01 Clause #72 (by superposition #[65, 21]): ∀ (a : Iota), Eq (mult (rd a a) (ld (rd a a) a)) (mult (rd a a) a) % 163.85/164.01 Clause #73 (by forward demodulation #[72, 15]): ∀ (a : Iota), Eq (mult (rd a a) (ld (rd a a) a)) a % 163.85/164.01 Clause #74 (by superposition #[73, 22]): ∀ (a : Iota), Eq a (ld (rd a a) a) % 163.85/164.01 Clause #83 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (C B A : Iota), Eq (rd (mult (mult A B) (rd C a)) (rd C a)) (mult A (rd (mult B a) a))) True % 163.85/164.01 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), % 163.85/164.01 Eq (∀ (B A : Iota), Eq (rd (mult (mult A B) (rd a a_1)) (rd a a_1)) (mult A (rd (mult B a_1) a_1))) True % 163.85/164.01 Clause #85 (by clausification #[84]): ∀ (a a_1 a_2 : Iota), % 163.85/164.01 Eq (∀ (A : Iota), Eq (rd (mult (mult A a) (rd a_1 a_2)) (rd a_1 a_2)) (mult A (rd (mult a a_2) a_2))) True % 163.85/164.01 Clause #86 (by clausification #[85]): ∀ (a a_1 a_2 a_3 : Iota), % 163.85/164.01 Eq (Eq (rd (mult (mult a a_1) (rd a_2 a_3)) (rd a_2 a_3)) (mult a (rd (mult a_1 a_3) a_3))) True % 163.85/164.01 Clause #87 (by clausification #[86]): ∀ (a a_1 a_2 a_3 : Iota), Eq (rd (mult (mult a a_1) (rd a_2 a_3)) (rd a_2 a_3)) (mult a (rd (mult a_1 a_3) a_3)) % 163.85/164.01 Clause #88 (by forward demodulation #[87, 14]): ∀ (a a_1 a_2 a_3 : Iota), Eq (rd (mult (mult a a_1) (rd a_2 a_3)) (rd a_2 a_3)) (mult a (mult (rd a_1 a_3) a_3)) % 163.85/164.01 Clause #91 (by superposition #[88, 9]): ∀ (a a_1 a_2 : Iota), Eq (rd (mult (mult a a_1) a_2) a_2) (mult a (mult (rd a_1 a_2) a_2)) % 163.85/164.01 Clause #94 (by superposition #[88, 24]): ∀ (a a_1 a_2 : Iota), % 163.85/164.01 Eq (rd (mult (rd a (ld a a)) (rd a_1 a_2)) (rd a_1 a_2)) (mult (rd a (ld a a)) (mult (rd (ld a a) a_2) a_2)) % 163.85/164.01 Clause #111 (by superposition #[53, 20]): ∀ (a a_1 a_2 : Iota), % 163.85/164.01 Eq (mult (mult a (ld a a_1)) (ld (mult a (ld a a_1)) a_2)) (ld (mult a (ld a a_1)) (mult a (ld a (mult a_1 a_2)))) % 163.85/164.01 Clause #114 (by superposition #[53, 21]): ∀ (a a_1 : Iota), Eq (mult a (ld a (mult a a_1))) (mult a a_1) % 163.85/164.01 Clause #115 (by superposition #[53, 25]): ∀ (a a_1 : Iota), Eq (mult a (ld a (mult (ld a a) a_1))) (mult (ld a a) a_1) % 163.85/164.01 Clause #117 (by superposition #[53, 20]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (mult (mult a a_1) a_2))) (mult (mult a (mult a (ld a a_1))) a_2) % 163.85/164.01 Clause #119 (by forward demodulation #[114, 20]): ∀ (a a_1 : Iota), Eq (mult a (mult a (ld a a_1))) (mult a a_1) % 163.85/164.01 Clause #128 (by superposition #[115, 53]): ∀ (a a_1 a_2 : Iota), % 163.85/164.01 Eq (mult a (ld a (mult a_1 (ld (mult a (ld a a_1)) (mult (ld (mult a (ld a a_1)) (mult a (ld a a_1))) a_2))))) % 163.85/164.01 (mult (ld (mult a (ld a a_1)) (mult a (ld a a_1))) a_2) % 163.85/164.01 Clause #131 (by superposition #[115, 20]): ∀ (a a_1 : Iota), Eq (mult a (ld a (ld a (mult (ld a a) a_1)))) (ld a (mult (ld a a) a_1)) % 163.85/164.01 Clause #137 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (A : Iota), Eq (ld A (mult A (ld a a))) (rd (mult (rd A A) a) a)) True % 163.85/164.01 Clause #138 (by clausification #[137]): ∀ (a a_1 : Iota), Eq (Eq (ld a (mult a (ld a_1 a_1))) (rd (mult (rd a a) a_1) a_1)) True % 163.85/164.01 Clause #139 (by clausification #[138]): ∀ (a a_1 : Iota), Eq (ld a (mult a (ld a_1 a_1))) (rd (mult (rd a a) a_1) a_1) % 163.85/164.01 Clause #140 (by forward demodulation #[139, 20]): ∀ (a a_1 : Iota), Eq (mult a (ld a (ld a_1 a_1))) (rd (mult (rd a a) a_1) a_1) % 163.85/164.01 Clause #148 (by superposition #[140, 15]): ∀ (a : Iota), Eq (mult a (ld a (ld a a))) (rd a a) % 163.85/164.01 Clause #149 (by superposition #[148, 25]): ∀ (a : Iota), Eq (rd a a) (ld a a) % 163.85/164.01 Clause #158 (by backward demodulation #[149, 15]): ∀ (a : Iota), Eq (mult (ld a a) a) a % 163.85/164.01 Clause #159 (by backward demodulation #[149, 16]): ∀ (a : Iota), Eq (mult (rd (ld a a) a) a) (rd a a) % 163.85/164.01 Clause #162 (by backward demodulation #[149, 74]): ∀ (a : Iota), Eq a (ld (ld a a) a) % 163.85/164.01 Clause #163 (by backward demodulation #[149, 140]): ∀ (a a_1 : Iota), Eq (mult a (ld a (ld a_1 a_1))) (rd (mult (ld a a) a_1) a_1) % 163.85/164.01 Clause #170 (by clausification #[7]): Eq % 163.85/164.01 (∀ (X3 X4 X5 : Iota), % 163.85/164.01 And (Eq (mult X3 (ld X4 (mult X4 X5))) (mult X3 X5)) (Eq (mult (rd (mult X3 X4) X4) X5) (mult X3 X5))) % 163.85/164.03 False % 163.85/164.03 Clause #171 (by clausification #[170]): ∀ (a : Iota), % 163.85/164.03 Eq % 163.85/164.03 (Not % 163.85/164.03 (∀ (X4 X5 : Iota), % 163.85/164.03 And (Eq (mult (skS.0 0 a) (ld X4 (mult X4 X5))) (mult (skS.0 0 a) X5)) % 163.85/164.03 (Eq (mult (rd (mult (skS.0 0 a) X4) X4) X5) (mult (skS.0 0 a) X5)))) % 163.85/164.03 True % 163.85/164.03 Clause #172 (by clausification #[171]): ∀ (a : Iota), % 163.85/164.03 Eq % 163.85/164.03 (∀ (X4 X5 : Iota), % 163.85/164.03 And (Eq (mult (skS.0 0 a) (ld X4 (mult X4 X5))) (mult (skS.0 0 a) X5)) % 163.85/164.03 (Eq (mult (rd (mult (skS.0 0 a) X4) X4) X5) (mult (skS.0 0 a) X5))) % 163.85/164.03 False % 163.85/164.03 Clause #173 (by clausification #[172]): ∀ (a a_1 : Iota), % 163.85/164.03 Eq % 163.85/164.03 (Not % 163.85/164.03 (∀ (X5 : Iota), % 163.85/164.03 And (Eq (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (mult (skS.0 1 a a_1) X5))) (mult (skS.0 0 a) X5)) % 163.85/164.03 (Eq (mult (rd (mult (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) X5) (mult (skS.0 0 a) X5)))) % 163.85/164.03 True % 163.85/164.03 Clause #174 (by clausification #[173]): ∀ (a a_1 : Iota), % 163.85/164.03 Eq % 163.85/164.03 (∀ (X5 : Iota), % 163.85/164.03 And (Eq (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (mult (skS.0 1 a a_1) X5))) (mult (skS.0 0 a) X5)) % 163.85/164.03 (Eq (mult (rd (mult (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) X5) (mult (skS.0 0 a) X5))) % 163.85/164.03 False % 163.85/164.03 Clause #175 (by clausification #[174]): ∀ (a a_1 a_2 : Iota), % 163.85/164.03 Eq % 163.85/164.03 (Not % 163.85/164.03 (And % 163.85/164.03 (Eq (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (mult (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 (Eq (mult (rd (mult (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))))) % 163.85/164.03 True % 163.85/164.03 Clause #176 (by clausification #[175]): ∀ (a a_1 a_2 : Iota), % 163.85/164.03 Eq % 163.85/164.03 (And % 163.85/164.03 (Eq (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (mult (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 (Eq (mult (rd (mult (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2)))) % 163.85/164.03 False % 163.85/164.03 Clause #177 (by clausification #[176]): ∀ (a a_1 a_2 : Iota), % 163.85/164.03 Or % 163.85/164.03 (Eq % 163.85/164.03 (Eq (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (mult (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 False) % 163.85/164.03 (Eq % 163.85/164.03 (Eq (mult (rd (mult (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 False) % 163.85/164.03 Clause #178 (by clausification #[177]): ∀ (a a_1 a_2 : Iota), % 163.85/164.03 Or % 163.85/164.03 (Eq % 163.85/164.03 (Eq (mult (rd (mult (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 False) % 163.85/164.03 (Ne (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (mult (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 Clause #179 (by clausification #[178]): ∀ (a a_1 a_2 : Iota), % 163.85/164.03 Or % 163.85/164.03 (Ne (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (mult (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 (Ne (mult (rd (mult (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 Clause #180 (by forward demodulation #[179, 20]): ∀ (a a_1 a_2 : Iota), % 163.85/164.03 Or % 163.85/164.03 (Ne (mult (skS.0 0 a) (mult (skS.0 1 a a_1) (ld (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 (Ne (mult (rd (mult (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 Clause #181 (by forward demodulation #[180, 14]): ∀ (a a_1 a_2 : Iota), % 163.85/164.03 Or % 163.85/164.03 (Ne (mult (skS.0 0 a) (mult (skS.0 1 a a_1) (ld (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 (Ne (mult (mult (rd (skS.0 0 a) (skS.0 1 a a_1)) (skS.0 1 a a_1)) (skS.0 2 a a_1 a_2)) % 163.85/164.03 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.03 Clause #182 (by forward demodulation #[159, 149]): ∀ (a : Iota), Eq (mult (rd (ld a a) a) a) (ld a a) % 163.85/164.03 Clause #190 (by superposition #[163, 14]): ∀ (a a_1 : Iota), Eq (mult (rd (ld a a) a_1) a_1) (mult a (ld a (ld a_1 a_1))) % 163.85/164.03 Clause #248 (by superposition #[91, 14]): ∀ (a a_1 a_2 : Iota), Eq (mult (rd (mult a a_1) a_2) a_2) (mult a (mult (rd a_1 a_2) a_2)) % 163.85/164.06 Clause #260 (by superposition #[91, 21]): ∀ (a a_1 : Iota), Eq (rd (mult a a_1) a_1) (mult a (mult (rd (ld a a) a_1) a_1)) % 163.85/164.06 Clause #351 (by forward demodulation #[260, 14]): ∀ (a a_1 : Iota), Eq (mult (rd a a_1) a_1) (mult a (mult (rd (ld a a) a_1) a_1)) % 163.85/164.06 Clause #352 (by forward demodulation #[351, 190]): ∀ (a a_1 : Iota), Eq (mult (rd a a_1) a_1) (mult a (mult a (ld a (ld a_1 a_1)))) % 163.85/164.06 Clause #353 (by superposition #[352, 119]): ∀ (a a_1 : Iota), Eq (mult (rd a a_1) a_1) (mult a (ld a_1 a_1)) % 163.85/164.06 Clause #379 (by backward demodulation #[353, 181]): ∀ (a a_1 a_2 : Iota), % 163.85/164.06 Or % 163.85/164.06 (Ne (mult (skS.0 0 a) (mult (skS.0 1 a a_1) (ld (skS.0 1 a a_1) (skS.0 2 a a_1 a_2)))) % 163.85/164.06 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.06 (Ne (mult (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (skS.0 1 a a_1))) (skS.0 2 a a_1 a_2)) % 163.85/164.06 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 163.85/164.06 Clause #380 (by backward demodulation #[353, 14]): ∀ (a a_1 : Iota), Eq (mult a (ld a_1 a_1)) (rd (mult a a_1) a_1) % 163.85/164.06 Clause #386 (by superposition #[353, 24]): ∀ (a : Iota), Eq (mult a (ld (ld a a) (ld a a))) (rd a (ld a a)) % 163.85/164.06 Clause #388 (by superposition #[353, 182]): ∀ (a : Iota), Eq (mult (ld a a) (ld a a)) (ld a a) % 163.85/164.06 Clause #390 (by superposition #[353, 190]): ∀ (a a_1 : Iota), Eq (mult (ld a a) (ld a_1 a_1)) (mult a (ld a (ld a_1 a_1))) % 163.85/164.06 Clause #417 (by superposition #[380, 353]): ∀ (a a_1 : Iota), Eq (mult (rd a a_1) (ld a_1 a_1)) (rd (mult a (ld a_1 a_1)) a_1) % 163.85/164.06 Clause #420 (by superposition #[388, 11]): ∀ (a : Iota), Eq (ld (ld a a) (ld a a)) (ld a a) % 163.85/164.06 Clause #429 (by superposition #[420, 162]): ∀ (a : Iota), Eq (ld a a) (ld (ld a a) (ld a a)) % 163.85/164.06 Clause #477 (by forward demodulation #[248, 353]): ∀ (a a_1 a_2 : Iota), Eq (mult (rd (mult a a_1) a_2) a_2) (mult a (mult a_1 (ld a_2 a_2))) % 163.85/164.06 Clause #480 (by superposition #[477, 353]): ∀ (a a_1 a_2 : Iota), Eq (mult a (mult a_1 (ld a_2 a_2))) (mult (mult a a_1) (ld a_2 a_2)) % 163.85/164.06 Clause #487 (by superposition #[477, 380]): ∀ (a a_1 : Iota), Eq (mult (mult a (ld a_1 a_1)) a_1) (mult a (mult a_1 (ld a_1 a_1))) % 163.85/164.06 Clause #629 (by forward demodulation #[40, 53]): ∀ (a a_1 a_2 a_3 : Iota), Eq (mult (ld a a_1) (ld (ld a a_1) (mult a_2 a_3))) (mult a (ld a (mult a_2 a_3))) % 163.85/164.06 Clause #658 (by superposition #[629, 21]): ∀ (a a_1 a_2 : Iota), Eq (mult (ld a a_1) (ld (ld a a_1) a_2)) (mult a (ld a a_2)) % 163.85/164.06 Clause #666 (by superposition #[658, 21]): ∀ (a a_1 : Iota), Eq (mult a (ld a (ld a a_1))) (ld a a_1) % 163.85/164.06 Clause #684 (by superposition #[666, 53]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (mult (ld a a_1) a_2))) (mult (ld a a_1) a_2) % 163.85/164.06 Clause #839 (by superposition #[684, 666]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (ld (ld a a_1) a_2))) (ld (ld a a_1) a_2) % 163.85/164.06 Clause #843 (by superposition #[684, 162]): ∀ (a a_1 : Iota), Eq (mult (ld a a) (ld (ld a a) (mult a a_1))) (mult a a_1) % 163.85/164.06 Clause #871 (by superposition #[843, 666]): ∀ (a a_1 : Iota), Eq (mult (ld a a) (ld (ld a a) (ld a a_1))) (ld a a_1) % 163.85/164.06 Clause #1006 (by forward demodulation #[487, 21]): ∀ (a a_1 : Iota), Eq (mult (mult a (ld a_1 a_1)) a_1) (mult a a_1) % 163.85/164.06 Clause #1018 (by superposition #[1006, 390]): ∀ (a a_1 : Iota), Eq (mult (mult a (ld a (ld a_1 a_1))) a_1) (mult (ld a a) a_1) % 163.85/164.06 Clause #1152 (by superposition #[1018, 53]): ∀ (a a_1 : Iota), Eq (mult a (ld a (mult (ld a_1 a_1) a_1))) (mult (ld a a) a_1) % 163.85/164.06 Clause #1171 (by forward demodulation #[1152, 158]): ∀ (a a_1 : Iota), Eq (mult a (ld a a_1)) (mult (ld a a) a_1) % 163.85/164.06 Clause #1178 (by superposition #[1171, 871]): ∀ (a a_1 : Iota), Eq (mult a (ld a (ld (ld a a) (ld a a_1)))) (ld a a_1) % 163.85/164.06 Clause #1226 (by forward demodulation #[50, 53]): ∀ (a a_1 a_2 a_3 : Iota), % 163.85/164.06 Eq (ld (mult a (ld a a_1)) (mult a (ld a (mult a_1 (mult a_2 a_3))))) (mult (mult a (ld a a_2)) a_3) % 163.85/164.06 Clause #1227 (by forward demodulation #[1226, 53]): ∀ (a a_1 a_2 a_3 : Iota), % 163.85/164.06 Eq (ld (mult a (ld a a_1)) (mult a (ld a (mult a_1 (mult a_2 a_3))))) (mult a (ld a (mult a_2 a_3))) % 163.85/164.06 Clause #1290 (by superposition #[1227, 21]): ∀ (a a_1 a_2 : Iota), Eq (ld (mult a (ld a a_1)) (mult a (ld a (mult a_1 a_2)))) (mult a (ld a a_2)) % 163.85/164.06 Clause #1441 (by forward demodulation #[386, 429]): ∀ (a : Iota), Eq (mult a (ld a a)) (rd a (ld a a)) % 163.85/164.08 Clause #1442 (by forward demodulation #[1441, 21]): ∀ (a : Iota), Eq a (rd a (ld a a)) % 163.85/164.08 Clause #1682 (by superposition #[1178, 839]): ∀ (a a_1 : Iota), Eq (ld a a_1) (ld (ld a a) (ld a a_1)) % 163.85/164.08 Clause #3565 (by forward demodulation #[94, 380]): ∀ (a a_1 a_2 : Iota), % 163.85/164.08 Eq (mult (rd a (ld a a)) (ld (rd a_1 a_2) (rd a_1 a_2))) (mult (rd a (ld a a)) (mult (rd (ld a a) a_2) a_2)) % 163.85/164.08 Clause #3566 (by forward demodulation #[3565, 1442]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld (rd a_1 a_2) (rd a_1 a_2))) (mult (rd a (ld a a)) (mult (rd (ld a a) a_2) a_2)) % 163.85/164.08 Clause #3567 (by forward demodulation #[3566, 190]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld (rd a_1 a_2) (rd a_1 a_2))) (mult (rd a (ld a a)) (mult a (ld a (ld a_2 a_2)))) % 163.85/164.08 Clause #3568 (by forward demodulation #[3567, 1442]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld (rd a_1 a_2) (rd a_1 a_2))) (mult a (mult a (ld a (ld a_2 a_2)))) % 163.85/164.08 Clause #3569 (by forward demodulation #[3568, 119]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld (rd a_1 a_2) (rd a_1 a_2))) (mult a (ld a_2 a_2)) % 163.85/164.08 Clause #3579 (by superposition #[3569, 21]): ∀ (a a_1 : Iota), Eq (mult (rd a a_1) (ld a_1 a_1)) (rd a a_1) % 163.85/164.08 Clause #3667 (by backward demodulation #[3579, 417]): ∀ (a a_1 : Iota), Eq (rd a a_1) (rd (mult a (ld a_1 a_1)) a_1) % 163.85/164.08 Clause #3694 (by superposition #[3667, 480]): ∀ (a a_1 a_2 : Iota), Eq (rd (mult a a_1) a_2) (rd (mult a (mult a_1 (ld a_2 a_2))) a_2) % 163.85/164.08 Clause #4449 (by superposition #[3694, 1171]): ∀ (a a_1 a_2 : Iota), Eq (rd (mult a (ld a_1 a_1)) a_2) (rd (mult a (mult a_1 (ld a_1 (ld a_2 a_2)))) a_2) % 163.85/164.08 Clause #5411 (by forward demodulation #[111, 53]): ∀ (a a_1 a_2 : Iota), % 163.85/164.08 Eq (mult a (ld a (mult a_1 (ld (mult a (ld a a_1)) a_2)))) (ld (mult a (ld a a_1)) (mult a (ld a (mult a_1 a_2)))) % 163.85/164.08 Clause #5412 (by superposition #[5411, 1290]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (mult a_1 (ld (mult a (ld a a_1)) a_2)))) (mult a (ld a a_2)) % 163.85/164.08 Clause #5891 (by forward demodulation #[117, 119]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (mult (mult a a_1) a_2))) (mult (mult a a_1) a_2) % 163.85/164.08 Clause #5949 (by superposition #[5891, 666]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (ld (mult a a_1) a_2))) (ld (mult a a_1) a_2) % 163.85/164.08 Clause #7064 (by forward demodulation #[128, 1171]): ∀ (a a_1 a_2 : Iota), % 163.85/164.08 Eq (mult a (ld a (mult a_1 (ld (mult a (ld a a_1)) (mult (mult a (ld a a_1)) (ld (mult a (ld a a_1)) a_2)))))) % 163.85/164.08 (mult (ld (mult a (ld a a_1)) (mult a (ld a a_1))) a_2) % 163.85/164.08 Clause #7065 (by forward demodulation #[7064, 20]): ∀ (a a_1 a_2 : Iota), % 163.85/164.08 Eq (mult a (ld a (mult a_1 (mult (mult a (ld a a_1)) (ld (mult a (ld a a_1)) (ld (mult a (ld a a_1)) a_2)))))) % 163.85/164.08 (mult (ld (mult a (ld a a_1)) (mult a (ld a a_1))) a_2) % 163.85/164.08 Clause #7066 (by forward demodulation #[7065, 666]): ∀ (a a_1 a_2 : Iota), % 163.85/164.08 Eq (mult a (ld a (mult a_1 (ld (mult a (ld a a_1)) a_2)))) (mult (ld (mult a (ld a a_1)) (mult a (ld a a_1))) a_2) % 163.85/164.08 Clause #7067 (by forward demodulation #[7066, 5412]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a a_1)) (mult (ld (mult a (ld a a_2)) (mult a (ld a a_2))) a_1) % 163.85/164.08 Clause #7209 (by superposition #[7067, 666]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a a_1)) (mult (ld (ld a a_2) (ld a a_2)) a_1) % 163.85/164.08 Clause #7215 (by superposition #[7067, 5949]): ∀ (a a_1 a_2 a_3 : Iota), Eq (mult a (ld a a_1)) (mult (ld (ld (mult a a_2) a_3) (ld (mult a a_2) a_3)) a_1) % 163.85/164.08 Clause #7459 (by superposition #[7215, 7209]): ∀ (a a_1 a_2 : Iota), Eq (mult (mult a a_1) (ld (mult a a_1) a_2)) (mult a (ld a a_2)) % 163.85/164.08 Clause #7506 (by superposition #[7215, 1682]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a a_1)) (mult (ld (mult a a_2) (mult a a_2)) a_1) % 163.85/164.08 Clause #8016 (by forward demodulation #[131, 1171]): ∀ (a a_1 : Iota), Eq (mult a (ld a (ld a (mult a (ld a a_1))))) (ld a (mult (ld a a) a_1)) % 163.85/164.08 Clause #8017 (by forward demodulation #[8016, 20]): ∀ (a a_1 : Iota), Eq (mult a (ld a (mult a (ld a (ld a a_1))))) (ld a (mult (ld a a) a_1)) % 163.85/164.08 Clause #8018 (by forward demodulation #[8017, 20]): ∀ (a a_1 : Iota), Eq (mult a (mult a (ld a (ld a (ld a a_1))))) (ld a (mult (ld a a) a_1)) % 164.16/164.33 Clause #8019 (by forward demodulation #[8018, 666]): ∀ (a a_1 : Iota), Eq (mult a (ld a (ld a a_1))) (ld a (mult (ld a a) a_1)) % 164.16/164.33 Clause #8020 (by forward demodulation #[8019, 666]): ∀ (a a_1 : Iota), Eq (ld a a_1) (ld a (mult (ld a a) a_1)) % 164.16/164.33 Clause #8021 (by forward demodulation #[8020, 1171]): ∀ (a a_1 : Iota), Eq (ld a a_1) (ld a (mult a (ld a a_1))) % 164.16/164.33 Clause #8046 (by superposition #[8021, 7459]): ∀ (a a_1 a_2 : Iota), Eq (ld (mult a a_1) a_2) (ld (mult a a_1) (mult a (ld a a_2))) % 164.16/164.33 Clause #8159 (by superposition #[8046, 1290]): ∀ (a a_1 a_2 : Iota), Eq (ld (mult a (ld a a_1)) (mult a_1 a_2)) (mult a (ld a a_2)) % 164.16/164.33 Clause #8160 (by superposition #[8046, 7506]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a a_1)) (mult (ld (mult a (ld a a_2)) a_2) a_1) % 164.16/164.33 Clause #8642 (by superposition #[8159, 21]): ∀ (a a_1 : Iota), Eq (ld (mult a (ld a a_1)) a_1) (mult a (ld a (ld a_1 a_1))) % 164.16/164.33 Clause #9076 (by backward demodulation #[8642, 8160]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a a_1)) (mult (mult a (ld a (ld a_2 a_2))) a_1) % 164.16/164.33 Clause #9320 (by superposition #[9076, 53]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (mult (ld a_1 a_1) a_2))) (mult a (ld a a_2)) % 164.16/164.33 Clause #9393 (by forward demodulation #[9320, 1171]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a (mult a_1 (ld a_1 a_2)))) (mult a (ld a a_2)) % 164.16/164.33 Clause #9406 (by superposition #[9393, 119]): ∀ (a a_1 a_2 : Iota), Eq (mult a (mult a (ld a a_1))) (mult a (mult a_2 (ld a_2 a_1))) % 164.16/164.33 Clause #9526 (by forward demodulation #[9406, 119]): ∀ (a a_1 a_2 : Iota), Eq (mult a a_1) (mult a (mult a_2 (ld a_2 a_1))) % 164.16/164.33 Clause #9528 (by backward demodulation #[9526, 4449]): ∀ (a a_1 a_2 : Iota), Eq (rd (mult a (ld a_1 a_1)) a_2) (rd (mult a (ld a_2 a_2)) a_2) % 164.16/164.33 Clause #9661 (by forward demodulation #[9528, 3667]): ∀ (a a_1 a_2 : Iota), Eq (rd (mult a (ld a_1 a_1)) a_2) (rd a a_2) % 164.16/164.33 Clause #9672 (by superposition #[9661, 353]): ∀ (a a_1 a_2 : Iota), Eq (mult (rd a a_1) a_1) (mult (mult a (ld a_2 a_2)) (ld a_1 a_1)) % 164.16/164.33 Clause #9949 (by forward demodulation #[9672, 353]): ∀ (a a_1 a_2 : Iota), Eq (mult a (ld a_1 a_1)) (mult (mult a (ld a_2 a_2)) (ld a_1 a_1)) % 164.16/164.33 Clause #9959 (by superposition #[9949, 1006]): ∀ (a a_1 a_2 : Iota), Eq (mult (mult a (ld a_1 a_1)) a_1) (mult (mult a (ld a_2 a_2)) a_1) % 164.16/164.33 Clause #10051 (by forward demodulation #[9959, 1006]): ∀ (a a_1 a_2 : Iota), Eq (mult a a_1) (mult (mult a (ld a_2 a_2)) a_1) % 164.16/164.33 Clause #36607 (by forward demodulation #[379, 9526]): ∀ (a a_1 a_2 : Iota), % 164.16/164.33 Or (Ne (mult (skS.0 0 a) (skS.0 2 a a_1 a_2)) (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 164.16/164.33 (Ne (mult (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (skS.0 1 a a_1))) (skS.0 2 a a_1 a_2)) % 164.16/164.33 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2))) % 164.16/164.33 Clause #36608 (by eliminate resolved literals #[36607]): ∀ (a a_1 a_2 : Iota), % 164.16/164.33 Ne (mult (mult (skS.0 0 a) (ld (skS.0 1 a a_1) (skS.0 1 a a_1))) (skS.0 2 a a_1 a_2)) % 164.16/164.33 (mult (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 164.16/164.33 Clause #36609 (by forward demodulation #[36608, 10051]): ∀ (a a_1 a_2 : Iota), Ne (mult (skS.0 0 a) (skS.0 2 a a_1 a_2)) (mult (skS.0 0 a) (skS.0 2 a a_1 a_2)) % 164.16/164.33 Clause #36610 (by eliminate resolved literals #[36609]): False % 164.16/164.33 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------