%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL520+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:36:04 AM UTC 2026 % Result : Theorem 153.06s 153.37s % Output : Proof 153.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL520+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.04 % Command : duper %s % 0.10/0.35 % Computer : n015.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Fri Sep 4 13:27:56 UTC 2026 % 0.10/0.35 % CPUTime : % 153.06/153.37 SZS status Theorem for theBenchmark.p % 153.06/153.37 SZS output start Proof for theBenchmark.p % 153.06/153.37 Clause #0 (by assumption #[]): Eq (Iff modus_ponens (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (implies X Y)) → is_a_theorem Y)) True % 153.06/153.37 Clause #1 (by assumption #[]): Eq (Iff substitution_of_equivalents (∀ (X Y : Iota), is_a_theorem (equiv X Y) → Eq X Y)) True % 153.06/153.37 Clause #15 (by assumption #[]): Eq (Iff kn1 (∀ (P : Iota), is_a_theorem (implies P (and P P)))) True % 153.06/153.37 Clause #16 (by assumption #[]): Eq (Iff kn2 (∀ (P Q : Iota), is_a_theorem (implies (and P Q) P))) True % 153.06/153.37 Clause #17 (by assumption #[]): Eq (Iff kn3 (∀ (P Q R : Iota), is_a_theorem (implies (implies P Q) (implies (not (and Q R)) (not (and R P)))))) True % 153.06/153.37 Clause #23 (by assumption #[]): Eq (Iff r3 (∀ (P Q : Iota), is_a_theorem (implies (or P Q) (or Q P)))) True % 153.06/153.37 Clause #26 (by assumption #[]): Eq (op_or → ∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True % 153.06/153.37 Clause #27 (by assumption #[]): Eq (op_and → ∀ (X Y : Iota), Eq (and X Y) (not (or (not X) (not Y)))) True % 153.06/153.37 Clause #28 (by assumption #[]): Eq (op_implies_and → ∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True % 153.06/153.37 Clause #29 (by assumption #[]): Eq (op_implies_or → ∀ (X Y : Iota), Eq (implies X Y) (or (not X) Y)) True % 153.06/153.37 Clause #30 (by assumption #[]): Eq (op_equiv → ∀ (X Y : Iota), Eq (equiv X Y) (and (implies X Y) (implies Y X))) True % 153.06/153.37 Clause #31 (by assumption #[]): Eq op_or True % 153.06/153.37 Clause #32 (by assumption #[]): Eq op_implies_and True % 153.06/153.37 Clause #33 (by assumption #[]): Eq op_equiv True % 153.06/153.37 Clause #34 (by assumption #[]): Eq modus_ponens True % 153.06/153.37 Clause #35 (by assumption #[]): Eq kn1 True % 153.06/153.37 Clause #36 (by assumption #[]): Eq kn2 True % 153.06/153.37 Clause #37 (by assumption #[]): Eq kn3 True % 153.06/153.37 Clause #38 (by assumption #[]): Eq substitution_of_equivalents True % 153.06/153.37 Clause #39 (by assumption #[]): Eq op_implies_or True % 153.06/153.37 Clause #40 (by assumption #[]): Eq op_and True % 153.06/153.37 Clause #41 (by assumption #[]): Eq (Not r3) True % 153.06/153.37 Clause #43 (by clausification #[0]): Or (Eq modus_ponens False) % 153.06/153.37 (Eq (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (implies X Y)) → is_a_theorem Y) True) % 153.06/153.37 Clause #54 (by clausification #[1]): Or (Eq substitution_of_equivalents False) (Eq (∀ (X Y : Iota), is_a_theorem (equiv X Y) → Eq X Y) True) % 153.06/153.37 Clause #62 (by clausification #[41]): Eq r3 False % 153.06/153.37 Clause #63 (by clausification #[43]): ∀ (a : Iota), % 153.06/153.37 Or (Eq modus_ponens False) % 153.06/153.37 (Eq (∀ (Y : Iota), And (is_a_theorem a) (is_a_theorem (implies a Y)) → is_a_theorem Y) True) % 153.06/153.37 Clause #64 (by clausification #[63]): ∀ (a a_1 : Iota), % 153.06/153.37 Or (Eq modus_ponens False) (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1)) → is_a_theorem a_1) True) % 153.06/153.37 Clause #65 (by clausification #[64]): ∀ (a a_1 : Iota), % 153.06/153.37 Or (Eq modus_ponens False) % 153.06/153.37 (Or (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1))) False) (Eq (is_a_theorem a_1) True)) % 153.06/153.37 Clause #66 (by clausification #[65]): ∀ (a a_1 : Iota), % 153.06/153.37 Or (Eq modus_ponens False) % 153.06/153.37 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 153.06/153.37 Clause #67 (by forward demodulation #[66, 34]): ∀ (a a_1 : Iota), % 153.06/153.37 Or (Eq True False) % 153.06/153.37 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 153.06/153.37 Clause #68 (by clausification #[67]): ∀ (a a_1 : Iota), % 153.06/153.37 Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False)) % 153.06/153.37 Clause #75 (by clausification #[15]): Or (Eq kn1 False) (Eq (∀ (P : Iota), is_a_theorem (implies P (and P P))) True) % 153.06/153.37 Clause #85 (by clausification #[75]): ∀ (a : Iota), Or (Eq kn1 False) (Eq (is_a_theorem (implies a (and a a))) True) % 153.06/153.37 Clause #86 (by forward demodulation #[85, 35]): ∀ (a : Iota), Or (Eq True False) (Eq (is_a_theorem (implies a (and a a))) True) % 153.06/153.37 Clause #87 (by clausification #[86]): ∀ (a : Iota), Eq (is_a_theorem (implies a (and a a))) True % 153.06/153.37 Clause #88 (by superposition #[87, 68]): ∀ (a a_1 : Iota), % 153.06/153.37 Or (Eq (is_a_theorem a) True) (Or (Eq True False) (Eq (is_a_theorem (implies (implies a_1 (and a_1 a_1)) a)) False)) % 153.06/153.37 Clause #89 (by clausification #[54]): ∀ (a : Iota), Or (Eq substitution_of_equivalents False) (Eq (∀ (Y : Iota), is_a_theorem (equiv a Y) → Eq a Y) True) % 153.15/153.43 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), Or (Eq substitution_of_equivalents False) (Eq (is_a_theorem (equiv a a_1) → Eq a a_1) True) % 153.15/153.43 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota), % 153.15/153.43 Or (Eq substitution_of_equivalents False) (Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq (Eq a a_1) True)) % 153.15/153.43 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), Or (Eq substitution_of_equivalents False) (Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq a a_1)) % 153.15/153.43 Clause #93 (by forward demodulation #[92, 38]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq a a_1)) % 153.15/153.43 Clause #94 (by clausification #[93]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq a a_1) % 153.15/153.43 Clause #111 (by clausification #[16]): Or (Eq kn2 False) (Eq (∀ (P Q : Iota), is_a_theorem (implies (and P Q) P)) True) % 153.15/153.43 Clause #117 (by clausification #[111]): ∀ (a : Iota), Or (Eq kn2 False) (Eq (∀ (Q : Iota), is_a_theorem (implies (and a Q) a)) True) % 153.15/153.43 Clause #118 (by clausification #[117]): ∀ (a a_1 : Iota), Or (Eq kn2 False) (Eq (is_a_theorem (implies (and a a_1) a)) True) % 153.15/153.43 Clause #119 (by forward demodulation #[118, 36]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies (and a a_1) a)) True) % 153.15/153.43 Clause #120 (by clausification #[119]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (and a a_1) a)) True % 153.15/153.43 Clause #121 (by superposition #[120, 68]): ∀ (a a_1 a_2 : Iota), % 153.15/153.43 Or (Eq (is_a_theorem a) True) (Or (Eq True False) (Eq (is_a_theorem (implies (implies (and a_1 a_2) a_1) a)) False)) % 153.15/153.43 Clause #195 (by clausification #[23]): Or (Eq r3 True) (Eq (∀ (P Q : Iota), is_a_theorem (implies (or P Q) (or Q P))) False) % 153.15/153.43 Clause #197 (by clausification #[195]): ∀ (a : Iota), % 153.15/153.43 Or (Eq r3 True) (Eq (Not (∀ (Q : Iota), is_a_theorem (implies (or (skS.0 32 a) Q) (or Q (skS.0 32 a))))) True) % 153.15/153.43 Clause #198 (by clausification #[197]): ∀ (a : Iota), Or (Eq r3 True) (Eq (∀ (Q : Iota), is_a_theorem (implies (or (skS.0 32 a) Q) (or Q (skS.0 32 a)))) False) % 153.15/153.43 Clause #199 (by clausification #[198]): ∀ (a a_1 : Iota), % 153.15/153.43 Or (Eq r3 True) % 153.15/153.43 (Eq (Not (is_a_theorem (implies (or (skS.0 32 a) (skS.0 33 a a_1)) (or (skS.0 33 a a_1) (skS.0 32 a))))) True) % 153.15/153.43 Clause #200 (by clausification #[199]): ∀ (a a_1 : Iota), % 153.15/153.43 Or (Eq r3 True) % 153.15/153.43 (Eq (is_a_theorem (implies (or (skS.0 32 a) (skS.0 33 a a_1)) (or (skS.0 33 a a_1) (skS.0 32 a)))) False) % 153.15/153.43 Clause #201 (by forward demodulation #[200, 62]): ∀ (a a_1 : Iota), % 153.15/153.43 Or (Eq False True) % 153.15/153.43 (Eq (is_a_theorem (implies (or (skS.0 32 a) (skS.0 33 a a_1)) (or (skS.0 33 a a_1) (skS.0 32 a)))) False) % 153.15/153.43 Clause #202 (by clausification #[201]): ∀ (a a_1 : Iota), % 153.15/153.43 Eq (is_a_theorem (implies (or (skS.0 32 a) (skS.0 33 a a_1)) (or (skS.0 33 a a_1) (skS.0 32 a)))) False % 153.15/153.43 Clause #214 (by clausification #[29]): Or (Eq op_implies_or False) (Eq (∀ (X Y : Iota), Eq (implies X Y) (or (not X) Y)) True) % 153.15/153.43 Clause #215 (by clausification #[214]): ∀ (a : Iota), Or (Eq op_implies_or False) (Eq (∀ (Y : Iota), Eq (implies a Y) (or (not a) Y)) True) % 153.15/153.43 Clause #216 (by clausification #[215]): ∀ (a a_1 : Iota), Or (Eq op_implies_or False) (Eq (Eq (implies a a_1) (or (not a) a_1)) True) % 153.15/153.43 Clause #217 (by clausification #[216]): ∀ (a a_1 : Iota), Or (Eq op_implies_or False) (Eq (implies a a_1) (or (not a) a_1)) % 153.15/153.43 Clause #218 (by forward demodulation #[217, 39]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (implies a a_1) (or (not a) a_1)) % 153.15/153.43 Clause #219 (by clausification #[218]): ∀ (a a_1 : Iota), Eq (implies a a_1) (or (not a) a_1) % 153.15/153.43 Clause #242 (by clausification #[28]): Or (Eq op_implies_and False) (Eq (∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True) % 153.15/153.43 Clause #243 (by clausification #[242]): ∀ (a : Iota), Or (Eq op_implies_and False) (Eq (∀ (Y : Iota), Eq (implies a Y) (not (and a (not Y)))) True) % 153.15/153.43 Clause #244 (by clausification #[243]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (Eq (implies a a_1) (not (and a (not a_1)))) True) % 153.15/153.43 Clause #245 (by clausification #[244]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (implies a a_1) (not (and a (not a_1)))) % 153.15/153.49 Clause #246 (by forward demodulation #[245, 32]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (implies a a_1) (not (and a (not a_1)))) % 153.15/153.49 Clause #247 (by clausification #[246]): ∀ (a a_1 : Iota), Eq (implies a a_1) (not (and a (not a_1))) % 153.15/153.49 Clause #263 (by clausification #[17]): Or (Eq kn3 False) % 153.15/153.49 (Eq (∀ (P Q R : Iota), is_a_theorem (implies (implies P Q) (implies (not (and Q R)) (not (and R P))))) True) % 153.15/153.49 Clause #271 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (implies (and a_1 a_2) a_1) a)) False) % 153.15/153.49 Clause #276 (by clausification #[88]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (implies a_1 (and a_1 a_1)) a)) False) % 153.15/153.49 Clause #307 (by clausification #[27]): Or (Eq op_and False) (Eq (∀ (X Y : Iota), Eq (and X Y) (not (or (not X) (not Y)))) True) % 153.15/153.49 Clause #308 (by clausification #[307]): ∀ (a : Iota), Or (Eq op_and False) (Eq (∀ (Y : Iota), Eq (and a Y) (not (or (not a) (not Y)))) True) % 153.15/153.49 Clause #309 (by clausification #[308]): ∀ (a a_1 : Iota), Or (Eq op_and False) (Eq (Eq (and a a_1) (not (or (not a) (not a_1)))) True) % 153.15/153.49 Clause #310 (by clausification #[309]): ∀ (a a_1 : Iota), Or (Eq op_and False) (Eq (and a a_1) (not (or (not a) (not a_1)))) % 153.15/153.49 Clause #311 (by forward demodulation #[310, 40]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (and a a_1) (not (or (not a) (not a_1)))) % 153.15/153.49 Clause #312 (by clausification #[311]): ∀ (a a_1 : Iota), Eq (and a a_1) (not (or (not a) (not a_1))) % 153.15/153.49 Clause #313 (by forward demodulation #[312, 219]): ∀ (a a_1 : Iota), Eq (and a a_1) (not (implies a (not a_1))) % 153.15/153.49 Clause #314 (by superposition #[313, 219]): ∀ (a a_1 a_2 : Iota), Eq (implies (implies a (not a_1)) a_2) (or (and a a_1) a_2) % 153.15/153.49 Clause #329 (by superposition #[314, 313]): ∀ (a a_1 a_2 : Iota), Eq (and (implies a (not a_1)) a_2) (not (or (and a a_1) (not a_2))) % 153.15/153.49 Clause #331 (by superposition #[314, 271]): ∀ (a a_1 a_2 : Iota), Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (or (and (and (not a_1) a_2) a_1) a)) False) % 153.15/153.49 Clause #417 (by clausification #[26]): Or (Eq op_or False) (Eq (∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True) % 153.15/153.49 Clause #418 (by clausification #[417]): ∀ (a : Iota), Or (Eq op_or False) (Eq (∀ (Y : Iota), Eq (or a Y) (not (and (not a) (not Y)))) True) % 153.15/153.49 Clause #419 (by clausification #[418]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (Eq (or a a_1) (not (and (not a) (not a_1)))) True) % 153.15/153.49 Clause #420 (by clausification #[419]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 153.15/153.49 Clause #421 (by forward demodulation #[420, 31]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 153.15/153.49 Clause #422 (by clausification #[421]): ∀ (a a_1 : Iota), Eq (or a a_1) (not (and (not a) (not a_1))) % 153.15/153.49 Clause #423 (by superposition #[422, 247]): ∀ (a a_1 : Iota), Eq (implies (not a) a_1) (or a a_1) % 153.15/153.49 Clause #461 (by superposition #[423, 313]): ∀ (a a_1 : Iota), Eq (and (not a) a_1) (not (or a (not a_1))) % 153.15/153.49 Clause #462 (by superposition #[423, 314]): ∀ (a a_1 a_2 : Iota), Eq (implies (or a (not a_1)) a_2) (or (and (not a) a_1) a_2) % 153.15/153.49 Clause #504 (by superposition #[461, 329]): ∀ (a a_1 a_2 : Iota), Eq (and (implies a (not a_1)) a_2) (and (not (and a a_1)) a_2) % 153.15/153.49 Clause #545 (by clausification #[30]): Or (Eq op_equiv False) (Eq (∀ (X Y : Iota), Eq (equiv X Y) (and (implies X Y) (implies Y X))) True) % 153.15/153.49 Clause #546 (by clausification #[545]): ∀ (a : Iota), Or (Eq op_equiv False) (Eq (∀ (Y : Iota), Eq (equiv a Y) (and (implies a Y) (implies Y a))) True) % 153.15/153.49 Clause #547 (by clausification #[546]): ∀ (a a_1 : Iota), Or (Eq op_equiv False) (Eq (Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a))) True) % 153.15/153.49 Clause #548 (by clausification #[547]): ∀ (a a_1 : Iota), Or (Eq op_equiv False) (Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a))) % 153.15/153.49 Clause #549 (by forward demodulation #[548, 33]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a))) % 153.25/153.55 Clause #550 (by clausification #[549]): ∀ (a a_1 : Iota), Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a)) % 153.25/153.55 Clause #552 (by superposition #[550, 87]): ∀ (a : Iota), Eq (is_a_theorem (implies (implies a a) (equiv a a))) True % 153.25/153.55 Clause #563 (by superposition #[550, 423]): ∀ (a a_1 : Iota), Eq (equiv a (not a_1)) (and (implies a (not a_1)) (or a_1 a)) % 153.25/153.55 Clause #1264 (by superposition #[504, 247]): ∀ (a a_1 a_2 : Iota), Eq (and (implies a (not (not a_1))) a_2) (and (implies a a_1) a_2) % 153.25/153.55 Clause #1417 (by superposition #[563, 1264]): ∀ (a a_1 : Iota), Eq (equiv a (not (not a_1))) (and (implies a a_1) (or (not a_1) a)) % 153.25/153.55 Clause #1685 (by forward demodulation #[1417, 219]): ∀ (a a_1 : Iota), Eq (equiv a (not (not a_1))) (and (implies a a_1) (implies a_1 a)) % 153.25/153.55 Clause #1686 (by superposition #[1685, 550]): ∀ (a a_1 : Iota), Eq (equiv a a_1) (equiv a (not (not a_1))) % 153.25/153.55 Clause #1727 (by superposition #[1686, 94]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq a (not (not a_1))) % 153.25/153.55 Clause #1850 (by clausification #[263]): ∀ (a : Iota), % 153.25/153.55 Or (Eq kn3 False) % 153.25/153.55 (Eq (∀ (Q R : Iota), is_a_theorem (implies (implies a Q) (implies (not (and Q R)) (not (and R a))))) True) % 153.25/153.55 Clause #1851 (by clausification #[1850]): ∀ (a a_1 : Iota), % 153.25/153.55 Or (Eq kn3 False) % 153.25/153.55 (Eq (∀ (R : Iota), is_a_theorem (implies (implies a a_1) (implies (not (and a_1 R)) (not (and R a))))) True) % 153.25/153.55 Clause #1852 (by clausification #[1851]): ∀ (a a_1 a_2 : Iota), % 153.25/153.55 Or (Eq kn3 False) (Eq (is_a_theorem (implies (implies a a_1) (implies (not (and a_1 a_2)) (not (and a_2 a))))) True) % 153.25/153.55 Clause #1853 (by forward demodulation #[1852, 37]): ∀ (a a_1 a_2 : Iota), % 153.25/153.55 Or (Eq True False) (Eq (is_a_theorem (implies (implies a a_1) (implies (not (and a_1 a_2)) (not (and a_2 a))))) True) % 153.25/153.55 Clause #1854 (by clausification #[1853]): ∀ (a a_1 a_2 : Iota), Eq (is_a_theorem (implies (implies a a_1) (implies (not (and a_1 a_2)) (not (and a_2 a))))) True % 153.25/153.55 Clause #1855 (by forward demodulation #[1854, 423]): ∀ (a a_1 a_2 : Iota), Eq (is_a_theorem (implies (implies a a_1) (or (and a_1 a_2) (not (and a_2 a))))) True % 153.25/153.55 Clause #1857 (by superposition #[1855, 276]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (or (and (and a a) a_1) (not (and a_1 a)))) True) (Eq True False) % 153.25/153.55 Clause #17419 (by clausification #[1857]): ∀ (a a_1 : Iota), Eq (is_a_theorem (or (and (and a a) a_1) (not (and a_1 a)))) True % 153.25/153.55 Clause #17420 (by superposition #[17419, 331]): ∀ (a : Iota), Or (Eq (is_a_theorem (not (and a (not a)))) True) (Eq True False) % 153.25/153.55 Clause #17493 (by clausification #[17420]): ∀ (a : Iota), Eq (is_a_theorem (not (and a (not a)))) True % 153.25/153.55 Clause #17494 (by forward demodulation #[17493, 247]): ∀ (a : Iota), Eq (is_a_theorem (implies a a)) True % 153.25/153.55 Clause #17504 (by superposition #[17494, 68]): ∀ (a a_1 : Iota), % 153.25/153.55 Or (Eq (is_a_theorem a) True) (Or (Eq True False) (Eq (is_a_theorem (implies (implies a_1 a_1) a)) False)) % 153.25/153.55 Clause #20673 (by clausification #[17504]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (implies a_1 a_1) a)) False) % 153.25/153.55 Clause #20675 (by superposition #[20673, 552]): ∀ (a : Iota), Or (Eq (is_a_theorem (equiv a a)) True) (Eq False True) % 153.25/153.55 Clause #20678 (by superposition #[20673, 1855]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (or (and a a_1) (not (and a_1 a)))) True) (Eq False True) % 153.25/153.55 Clause #20719 (by clausification #[20675]): ∀ (a : Iota), Eq (is_a_theorem (equiv a a)) True % 153.25/153.55 Clause #20720 (by superposition #[20719, 1727]): ∀ (a : Iota), Or (Eq True False) (Eq a (not (not a))) % 153.25/153.55 Clause #20737 (by clausification #[20720]): ∀ (a : Iota), Eq a (not (not a)) % 153.25/153.55 Clause #20751 (by superposition #[20737, 247]): ∀ (a a_1 : Iota), Eq (implies a (not a_1)) (not (and a a_1)) % 153.25/153.55 Clause #26949 (by clausification #[20678]): ∀ (a a_1 : Iota), Eq (is_a_theorem (or (and a a_1) (not (and a_1 a)))) True % 153.25/153.55 Clause #26950 (by forward demodulation #[26949, 20751]): ∀ (a a_1 : Iota), Eq (is_a_theorem (or (and a a_1) (implies a_1 (not a)))) True % 153.25/153.55 Clause #27014 (by superposition #[26950, 20737]): ∀ (a a_1 : Iota), Eq (is_a_theorem (or (and (not a) a_1) (implies a_1 a))) True % 153.45/153.79 Clause #27046 (by forward demodulation #[27014, 462]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (or a (not a_1)) (implies a_1 a))) True % 153.45/153.79 Clause #27125 (by superposition #[27046, 20737]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (or a a_1) (implies (not a_1) a))) True % 153.45/153.79 Clause #27148 (by forward demodulation #[27125, 423]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (or a a_1) (or a_1 a))) True % 153.45/153.79 Clause #27149 (by superposition #[27148, 202]): Eq True False % 153.45/153.79 Clause #27187 (by clausification #[27149]): False % 153.45/153.79 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------