%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : LCL456+1 : TPTP v9.3.1. Bugfixed v9.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n005.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:35:59 AM UTC 2026 % Result : Theorem 98.89s 99.18s % Output : Proof 99.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL456+1 : TPTP v9.3.1. Bugfixed v9.2.0. % 0.00/0.05 % Command : duper %s % 0.09/0.36 % Computer : n005.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Fri Sep 4 18:42:51 UTC 2026 % 0.14/0.37 % CPUTime : % 98.89/99.18 SZS status Theorem for theBenchmark.p % 98.89/99.18 SZS output start Proof for theBenchmark.p % 98.89/99.18 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 % 98.89/99.18 Clause #1 (by assumption #[]): Eq (Iff substitution_of_equivalents (∀ (X Y : Iota), is_a_theorem (equiv X Y) → Eq X Y)) True % 98.89/99.18 Clause #2 (by assumption #[]): Eq (Iff modus_tollens (∀ (X Y : Iota), is_a_theorem (implies (implies (not Y) (not X)) (implies X Y)))) True % 98.89/99.18 Clause #3 (by assumption #[]): Eq (Iff implies_1 (∀ (X Y : Iota), is_a_theorem (implies X (implies Y X)))) True % 98.89/99.18 Clause #4 (by assumption #[]): Eq (Iff implies_2 (∀ (X Y : Iota), is_a_theorem (implies (implies X (implies X Y)) (implies X Y)))) True % 98.89/99.18 Clause #8 (by assumption #[]): Eq (Iff and_3 (∀ (X Y : Iota), is_a_theorem (implies X (implies Y (and X Y))))) True % 98.89/99.18 Clause #23 (by assumption #[]): Eq (Iff r3 (∀ (P Q : Iota), is_a_theorem (implies (or P Q) (or Q P)))) True % 98.89/99.18 Clause #26 (by assumption #[]): Eq (op_or → ∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True % 98.89/99.18 Clause #27 (by assumption #[]): Eq (op_and → ∀ (X Y : Iota), Eq (and X Y) (not (or (not X) (not Y)))) True % 98.89/99.18 Clause #28 (by assumption #[]): Eq (op_implies_and → ∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True % 98.89/99.18 Clause #29 (by assumption #[]): Eq (op_implies_or → ∀ (X Y : Iota), Eq (implies X Y) (or (not X) Y)) True % 98.89/99.18 Clause #30 (by assumption #[]): Eq (op_equiv → ∀ (X Y : Iota), Eq (equiv X Y) (and (implies X Y) (implies Y X))) True % 98.89/99.18 Clause #31 (by assumption #[]): Eq op_or True % 98.89/99.18 Clause #32 (by assumption #[]): Eq op_implies_and True % 98.89/99.18 Clause #33 (by assumption #[]): Eq op_equiv True % 98.89/99.18 Clause #34 (by assumption #[]): Eq modus_ponens True % 98.89/99.18 Clause #35 (by assumption #[]): Eq modus_tollens True % 98.89/99.18 Clause #36 (by assumption #[]): Eq implies_1 True % 98.89/99.18 Clause #37 (by assumption #[]): Eq implies_2 True % 98.89/99.18 Clause #41 (by assumption #[]): Eq and_3 True % 98.89/99.18 Clause #48 (by assumption #[]): Eq substitution_of_equivalents True % 98.89/99.18 Clause #49 (by assumption #[]): Eq op_implies_or True % 98.89/99.18 Clause #50 (by assumption #[]): Eq op_and True % 98.89/99.18 Clause #51 (by assumption #[]): Eq (Not r3) True % 98.89/99.18 Clause #53 (by clausification #[0]): Or (Eq modus_ponens False) % 98.89/99.18 (Eq (∀ (X Y : Iota), And (is_a_theorem X) (is_a_theorem (implies X Y)) → is_a_theorem Y) True) % 98.89/99.18 Clause #64 (by clausification #[1]): Or (Eq substitution_of_equivalents False) (Eq (∀ (X Y : Iota), is_a_theorem (equiv X Y) → Eq X Y) True) % 98.89/99.18 Clause #73 (by clausification #[2]): Or (Eq modus_tollens False) (Eq (∀ (X Y : Iota), is_a_theorem (implies (implies (not Y) (not X)) (implies X Y))) True) % 98.89/99.18 Clause #80 (by clausification #[3]): Or (Eq implies_1 False) (Eq (∀ (X Y : Iota), is_a_theorem (implies X (implies Y X))) True) % 98.89/99.18 Clause #86 (by clausification #[51]): Eq r3 False % 98.89/99.18 Clause #87 (by clausification #[53]): ∀ (a : Iota), % 98.89/99.18 Or (Eq modus_ponens False) % 98.89/99.18 (Eq (∀ (Y : Iota), And (is_a_theorem a) (is_a_theorem (implies a Y)) → is_a_theorem Y) True) % 98.89/99.18 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), % 98.89/99.18 Or (Eq modus_ponens False) (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1)) → is_a_theorem a_1) True) % 98.89/99.18 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), % 98.89/99.18 Or (Eq modus_ponens False) % 98.89/99.18 (Or (Eq (And (is_a_theorem a) (is_a_theorem (implies a a_1))) False) (Eq (is_a_theorem a_1) True)) % 98.89/99.18 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), % 98.89/99.18 Or (Eq modus_ponens False) % 98.89/99.18 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 98.89/99.18 Clause #91 (by forward demodulation #[90, 34]): ∀ (a a_1 : Iota), % 98.89/99.18 Or (Eq True False) % 98.89/99.18 (Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False))) % 98.89/99.18 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), % 98.89/99.18 Or (Eq (is_a_theorem a) True) (Or (Eq (is_a_theorem a_1) False) (Eq (is_a_theorem (implies a_1 a)) False)) % 98.89/99.18 Clause #103 (by clausification #[4]): Or (Eq implies_2 False) (Eq (∀ (X Y : Iota), is_a_theorem (implies (implies X (implies X Y)) (implies X Y))) True) % 98.89/99.18 Clause #111 (by clausification #[64]): ∀ (a : Iota), Or (Eq substitution_of_equivalents False) (Eq (∀ (Y : Iota), is_a_theorem (equiv a Y) → Eq a Y) True) % 98.96/99.24 Clause #112 (by clausification #[111]): ∀ (a a_1 : Iota), Or (Eq substitution_of_equivalents False) (Eq (is_a_theorem (equiv a a_1) → Eq a a_1) True) % 98.96/99.24 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), % 98.96/99.24 Or (Eq substitution_of_equivalents False) (Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq (Eq a a_1) True)) % 98.96/99.24 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), Or (Eq substitution_of_equivalents False) (Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq a a_1)) % 98.96/99.24 Clause #115 (by forward demodulation #[114, 48]): ∀ (a a_1 : Iota), Or (Eq True False) (Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq a a_1)) % 98.96/99.24 Clause #116 (by clausification #[115]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (equiv a a_1)) False) (Eq a a_1) % 98.96/99.24 Clause #117 (by clausification #[80]): ∀ (a : Iota), Or (Eq implies_1 False) (Eq (∀ (Y : Iota), is_a_theorem (implies a (implies Y a))) True) % 98.96/99.24 Clause #118 (by clausification #[117]): ∀ (a a_1 : Iota), Or (Eq implies_1 False) (Eq (is_a_theorem (implies a (implies a_1 a))) True) % 98.96/99.24 Clause #119 (by forward demodulation #[118, 36]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies a (implies a_1 a))) True) % 98.96/99.24 Clause #120 (by clausification #[119]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (implies a_1 a))) True % 98.96/99.24 Clause #121 (by superposition #[120, 92]): ∀ (a a_1 a_2 : Iota), % 98.96/99.24 Or (Eq (is_a_theorem a) True) % 98.96/99.24 (Or (Eq True False) (Eq (is_a_theorem (implies (implies a_1 (implies a_2 a_1)) a)) False)) % 98.96/99.24 Clause #190 (by clausification #[8]): Or (Eq and_3 False) (Eq (∀ (X Y : Iota), is_a_theorem (implies X (implies Y (and X Y)))) True) % 98.96/99.24 Clause #243 (by clausification #[29]): Or (Eq op_implies_or False) (Eq (∀ (X Y : Iota), Eq (implies X Y) (or (not X) Y)) True) % 98.96/99.24 Clause #244 (by clausification #[243]): ∀ (a : Iota), Or (Eq op_implies_or False) (Eq (∀ (Y : Iota), Eq (implies a Y) (or (not a) Y)) True) % 98.96/99.24 Clause #245 (by clausification #[244]): ∀ (a a_1 : Iota), Or (Eq op_implies_or False) (Eq (Eq (implies a a_1) (or (not a) a_1)) True) % 98.96/99.24 Clause #246 (by clausification #[245]): ∀ (a a_1 : Iota), Or (Eq op_implies_or False) (Eq (implies a a_1) (or (not a) a_1)) % 98.96/99.24 Clause #247 (by forward demodulation #[246, 49]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (implies a a_1) (or (not a) a_1)) % 98.96/99.24 Clause #248 (by clausification #[247]): ∀ (a a_1 : Iota), Eq (implies a a_1) (or (not a) a_1) % 98.96/99.24 Clause #263 (by clausification #[23]): Or (Eq r3 True) (Eq (∀ (P Q : Iota), is_a_theorem (implies (or P Q) (or Q P))) False) % 98.96/99.24 Clause #265 (by clausification #[263]): ∀ (a : Iota), % 98.96/99.24 Or (Eq r3 True) (Eq (Not (∀ (Q : Iota), is_a_theorem (implies (or (skS.0 39 a) Q) (or Q (skS.0 39 a))))) True) % 98.96/99.24 Clause #266 (by clausification #[265]): ∀ (a : Iota), Or (Eq r3 True) (Eq (∀ (Q : Iota), is_a_theorem (implies (or (skS.0 39 a) Q) (or Q (skS.0 39 a)))) False) % 98.96/99.24 Clause #267 (by clausification #[266]): ∀ (a a_1 : Iota), % 98.96/99.24 Or (Eq r3 True) % 98.96/99.24 (Eq (Not (is_a_theorem (implies (or (skS.0 39 a) (skS.0 40 a a_1)) (or (skS.0 40 a a_1) (skS.0 39 a))))) True) % 98.96/99.24 Clause #268 (by clausification #[267]): ∀ (a a_1 : Iota), % 98.96/99.24 Or (Eq r3 True) % 98.96/99.24 (Eq (is_a_theorem (implies (or (skS.0 39 a) (skS.0 40 a a_1)) (or (skS.0 40 a a_1) (skS.0 39 a)))) False) % 98.96/99.24 Clause #269 (by forward demodulation #[268, 86]): ∀ (a a_1 : Iota), % 98.96/99.24 Or (Eq False True) % 98.96/99.24 (Eq (is_a_theorem (implies (or (skS.0 39 a) (skS.0 40 a a_1)) (or (skS.0 40 a a_1) (skS.0 39 a)))) False) % 98.96/99.24 Clause #270 (by clausification #[269]): ∀ (a a_1 : Iota), % 98.96/99.24 Eq (is_a_theorem (implies (or (skS.0 39 a) (skS.0 40 a a_1)) (or (skS.0 40 a a_1) (skS.0 39 a)))) False % 98.96/99.24 Clause #274 (by clausification #[190]): ∀ (a : Iota), Or (Eq and_3 False) (Eq (∀ (Y : Iota), is_a_theorem (implies a (implies Y (and a Y)))) True) % 98.96/99.24 Clause #275 (by clausification #[274]): ∀ (a a_1 : Iota), Or (Eq and_3 False) (Eq (is_a_theorem (implies a (implies a_1 (and a a_1)))) True) % 98.96/99.24 Clause #276 (by forward demodulation #[275, 41]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies a (implies a_1 (and a a_1)))) True) % 99.06/99.30 Clause #277 (by clausification #[276]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (implies a_1 (and a a_1)))) True % 99.06/99.30 Clause #342 (by clausification #[121]): ∀ (a a_1 a_2 : Iota), % 99.06/99.30 Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (implies a_1 (implies a_2 a_1)) a)) False) % 99.06/99.30 Clause #371 (by clausification #[26]): Or (Eq op_or False) (Eq (∀ (X Y : Iota), Eq (or X Y) (not (and (not X) (not Y)))) True) % 99.06/99.30 Clause #372 (by clausification #[371]): ∀ (a : Iota), Or (Eq op_or False) (Eq (∀ (Y : Iota), Eq (or a Y) (not (and (not a) (not Y)))) True) % 99.06/99.30 Clause #373 (by clausification #[372]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (Eq (or a a_1) (not (and (not a) (not a_1)))) True) % 99.06/99.30 Clause #374 (by clausification #[373]): ∀ (a a_1 : Iota), Or (Eq op_or False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 99.06/99.30 Clause #375 (by forward demodulation #[374, 31]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (or a a_1) (not (and (not a) (not a_1)))) % 99.06/99.30 Clause #376 (by clausification #[375]): ∀ (a a_1 : Iota), Eq (or a a_1) (not (and (not a) (not a_1))) % 99.06/99.30 Clause #437 (by clausification #[27]): Or (Eq op_and False) (Eq (∀ (X Y : Iota), Eq (and X Y) (not (or (not X) (not Y)))) True) % 99.06/99.30 Clause #438 (by clausification #[437]): ∀ (a : Iota), Or (Eq op_and False) (Eq (∀ (Y : Iota), Eq (and a Y) (not (or (not a) (not Y)))) True) % 99.06/99.30 Clause #439 (by clausification #[438]): ∀ (a a_1 : Iota), Or (Eq op_and False) (Eq (Eq (and a a_1) (not (or (not a) (not a_1)))) True) % 99.06/99.30 Clause #440 (by clausification #[439]): ∀ (a a_1 : Iota), Or (Eq op_and False) (Eq (and a a_1) (not (or (not a) (not a_1)))) % 99.06/99.30 Clause #441 (by forward demodulation #[440, 50]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (and a a_1) (not (or (not a) (not a_1)))) % 99.06/99.30 Clause #442 (by clausification #[441]): ∀ (a a_1 : Iota), Eq (and a a_1) (not (or (not a) (not a_1))) % 99.06/99.30 Clause #443 (by forward demodulation #[442, 248]): ∀ (a a_1 : Iota), Eq (and a a_1) (not (implies a (not a_1))) % 99.06/99.30 Clause #444 (by superposition #[443, 248]): ∀ (a a_1 a_2 : Iota), Eq (implies (implies a (not a_1)) a_2) (or (and a a_1) a_2) % 99.06/99.30 Clause #469 (by clausification #[28]): Or (Eq op_implies_and False) (Eq (∀ (X Y : Iota), Eq (implies X Y) (not (and X (not Y)))) True) % 99.06/99.30 Clause #470 (by clausification #[469]): ∀ (a : Iota), Or (Eq op_implies_and False) (Eq (∀ (Y : Iota), Eq (implies a Y) (not (and a (not Y)))) True) % 99.06/99.30 Clause #471 (by clausification #[470]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (Eq (implies a a_1) (not (and a (not a_1)))) True) % 99.06/99.30 Clause #472 (by clausification #[471]): ∀ (a a_1 : Iota), Or (Eq op_implies_and False) (Eq (implies a a_1) (not (and a (not a_1)))) % 99.06/99.30 Clause #473 (by forward demodulation #[472, 32]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (implies a a_1) (not (and a (not a_1)))) % 99.06/99.30 Clause #474 (by clausification #[473]): ∀ (a a_1 : Iota), Eq (implies a a_1) (not (and a (not a_1))) % 99.06/99.30 Clause #475 (by superposition #[474, 376]): ∀ (a a_1 : Iota), Eq (or a a_1) (implies (not a) a_1) % 99.06/99.30 Clause #536 (by superposition #[475, 474]): ∀ (a a_1 a_2 : Iota), Eq (or (and a (not a_1)) a_2) (implies (implies a a_1) a_2) % 99.06/99.30 Clause #552 (by clausification #[30]): Or (Eq op_equiv False) (Eq (∀ (X Y : Iota), Eq (equiv X Y) (and (implies X Y) (implies Y X))) True) % 99.06/99.30 Clause #553 (by clausification #[552]): ∀ (a : Iota), Or (Eq op_equiv False) (Eq (∀ (Y : Iota), Eq (equiv a Y) (and (implies a Y) (implies Y a))) True) % 99.06/99.30 Clause #554 (by clausification #[553]): ∀ (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) % 99.06/99.30 Clause #555 (by clausification #[554]): ∀ (a a_1 : Iota), Or (Eq op_equiv False) (Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a))) % 99.06/99.30 Clause #556 (by forward demodulation #[555, 33]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a))) % 99.06/99.30 Clause #557 (by clausification #[556]): ∀ (a a_1 : Iota), Eq (equiv a a_1) (and (implies a a_1) (implies a_1 a)) % 99.06/99.30 Clause #562 (by superposition #[557, 475]): ∀ (a a_1 : Iota), Eq (equiv a (not a_1)) (and (implies a (not a_1)) (or a_1 a)) % 99.06/99.35 Clause #630 (by clausification #[73]): ∀ (a : Iota), % 99.06/99.35 Or (Eq modus_tollens False) (Eq (∀ (Y : Iota), is_a_theorem (implies (implies (not Y) (not a)) (implies a Y))) True) % 99.06/99.35 Clause #631 (by clausification #[630]): ∀ (a a_1 : Iota), % 99.06/99.35 Or (Eq modus_tollens False) (Eq (is_a_theorem (implies (implies (not a) (not a_1)) (implies a_1 a))) True) % 99.06/99.35 Clause #632 (by forward demodulation #[631, 35]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies (implies (not a) (not a_1)) (implies a_1 a))) True) % 99.06/99.35 Clause #633 (by clausification #[632]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (implies (not a) (not a_1)) (implies a_1 a))) True % 99.06/99.35 Clause #634 (by forward demodulation #[633, 475]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (or a (not a_1)) (implies a_1 a))) True % 99.06/99.35 Clause #638 (by superposition #[634, 248]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (implies a (not a_1)) (implies a_1 (not a)))) True % 99.06/99.35 Clause #661 (by clausification #[103]): ∀ (a : Iota), % 99.06/99.35 Or (Eq implies_2 False) (Eq (∀ (Y : Iota), is_a_theorem (implies (implies a (implies a Y)) (implies a Y))) True) % 99.06/99.35 Clause #662 (by clausification #[661]): ∀ (a a_1 : Iota), Or (Eq implies_2 False) (Eq (is_a_theorem (implies (implies a (implies a a_1)) (implies a a_1))) True) % 99.06/99.35 Clause #663 (by forward demodulation #[662, 37]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (is_a_theorem (implies (implies a (implies a a_1)) (implies a a_1))) True) % 99.06/99.35 Clause #664 (by clausification #[663]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (implies a (implies a a_1)) (implies a a_1))) True % 99.06/99.35 Clause #665 (by superposition #[664, 342]): ∀ (a : Iota), Or (Eq (is_a_theorem (implies a a)) True) (Eq True False) % 99.06/99.35 Clause #671 (by clausification #[665]): ∀ (a : Iota), Eq (is_a_theorem (implies a a)) True % 99.06/99.35 Clause #672 (by superposition #[671, 92]): ∀ (a a_1 : Iota), % 99.06/99.35 Or (Eq (is_a_theorem a) True) (Or (Eq True False) (Eq (is_a_theorem (implies (implies a_1 a_1) a)) False)) % 99.06/99.35 Clause #2718 (by forward demodulation #[638, 444]): ∀ (a a_1 : Iota), Eq (is_a_theorem (or (and a a_1) (implies a_1 (not a)))) True % 99.06/99.35 Clause #2722 (by superposition #[2718, 475]): ∀ (a a_1 : Iota), Eq (is_a_theorem (or (and a (not a_1)) (or a_1 (not a)))) True % 99.06/99.35 Clause #2731 (by forward demodulation #[2722, 536]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (implies a a_1) (or a_1 (not a)))) True % 99.06/99.35 Clause #2752 (by superposition #[2731, 475]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (or a a_1) (or a_1 (not (not a))))) True % 99.06/99.35 Clause #3676 (by clausification #[672]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem a) True) (Eq (is_a_theorem (implies (implies a_1 a_1) a)) False) % 99.06/99.35 Clause #3680 (by superposition #[3676, 277]): ∀ (a a_1 : Iota), Or (Eq (is_a_theorem (implies a (and (implies a_1 a_1) a))) True) (Eq False True) % 99.06/99.35 Clause #4383 (by clausification #[3680]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (and (implies a_1 a_1) a))) True % 99.06/99.35 Clause #4418 (by superposition #[4383, 475]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (and (or a_1 (not a_1)) a))) True % 99.06/99.35 Clause #4454 (by superposition #[4418, 248]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies a (and (implies a_1 (not (not a_1))) a))) True % 99.06/99.35 Clause #9154 (by superposition #[562, 4454]): ∀ (a : Iota), Eq (is_a_theorem (implies (or (not a) a) (equiv a (not (not a))))) True % 99.06/99.35 Clause #9210 (by forward demodulation #[9154, 248]): ∀ (a : Iota), Eq (is_a_theorem (implies (implies a a) (equiv a (not (not a))))) True % 99.06/99.35 Clause #9214 (by superposition #[9210, 3676]): ∀ (a : Iota), Or (Eq (is_a_theorem (equiv a (not (not a)))) True) (Eq True False) % 99.06/99.35 Clause #9234 (by clausification #[9214]): ∀ (a : Iota), Eq (is_a_theorem (equiv a (not (not a)))) True % 99.06/99.35 Clause #9235 (by superposition #[9234, 116]): ∀ (a : Iota), Or (Eq True False) (Eq a (not (not a))) % 99.06/99.35 Clause #9249 (by clausification #[9235]): ∀ (a : Iota), Eq a (not (not a)) % 99.06/99.35 Clause #9251 (by backward demodulation #[9249, 2752]): ∀ (a a_1 : Iota), Eq (is_a_theorem (implies (or a a_1) (or a_1 a))) True % 99.06/99.35 Clause #9706 (by superposition #[9251, 270]): Eq True False % 99.16/99.44 Clause #9771 (by clausification #[9706]): False % 99.16/99.44 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------