%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO020^1 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n009.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 08:08:26 PM UTC 2025 % Result : Theorem 5.02s 5.18s % Output : Proof 5.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYO020^1 : TPTP v9.2.0. Released v3.7.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n009.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 : Fri Oct 3 14:11:08 EDT 2025 % 0.13/0.34 % CPUTime : % 5.02/5.18 SZS status Theorem for theBenchmark.p % 5.02/5.18 SZS output start Proof for theBenchmark.p % 5.02/5.18 Clause #0 (by assumption #[]): Eq (Eq leibeq fun X Y => ∀ (P : Prop → Prop), P X → P Y) True % 5.02/5.18 Clause #1 (by assumption #[]): Eq (Not (∀ (X Y : Prop), leibeq (And X Y) (Not (Or (Not X) (Not Y))))) True % 5.02/5.18 Clause #2 (by clausification #[0]): Eq leibeq fun X Y => ∀ (P : Prop → Prop), P X → P Y % 5.02/5.18 Clause #3 (by argument congruence #[2]): ∀ (a : Prop), Eq (leibeq a) ((fun X Y => ∀ (P : Prop → Prop), P X → P Y) a) % 5.02/5.18 Clause #5 (by betaEtaReduce #[3]): ∀ (a : Prop), Eq (leibeq a) fun Y => ∀ (P : Prop → Prop), P a → P Y % 5.02/5.18 Clause #6 (by identity loobHoist #[5]): ∀ (a : Prop), Or (Eq (leibeq True) fun Y => ∀ (P : Prop → Prop), P a → P Y) (Eq a False) % 5.02/5.18 Clause #7 (by identity boolHoist #[5]): ∀ (a : Prop), Or (Eq (leibeq False) fun Y => ∀ (P : Prop → Prop), P a → P Y) (Eq a True) % 5.02/5.18 Clause #8 (by falseElim #[6]): Eq (leibeq True) fun Y => ∀ (P : Prop → Prop), P True → P Y % 5.02/5.18 Clause #9 (by argument congruence #[8]): ∀ (a : Prop), Eq (leibeq True a) ((fun Y => ∀ (P : Prop → Prop), P True → P Y) a) % 5.02/5.18 Clause #10 (by argument congruence #[7]): ∀ (a a_1 : Prop), Or (Eq (leibeq False a) ((fun Y => ∀ (P : Prop → Prop), P a_1 → P Y) a)) (Eq a_1 True) % 5.02/5.18 Clause #13 (by betaEtaReduce #[9]): ∀ (a : Prop), Eq (leibeq True a) (∀ (P : Prop → Prop), P True → P a) % 5.02/5.18 Clause #14 (by identity loobHoist #[13]): ∀ (a : Prop), Or (Eq (leibeq True True) (∀ (P : Prop → Prop), P True → P a)) (Eq a False) % 5.02/5.18 Clause #16 (by falseElim #[14]): Eq (leibeq True True) (∀ (P : Prop → Prop), P True → P True) % 5.02/5.18 Clause #17 (by clausification #[1]): Eq (∀ (X Y : Prop), leibeq (And X Y) (Not (Or (Not X) (Not Y)))) False % 5.02/5.18 Clause #18 (by clausification #[17]): ∀ (a : Prop), Eq (Not (∀ (Y : Prop), leibeq (And (skS.0 0 a) Y) (Not (Or (Not (skS.0 0 a)) (Not Y))))) True % 5.02/5.18 Clause #19 (by clausification #[18]): ∀ (a : Prop), Eq (∀ (Y : Prop), leibeq (And (skS.0 0 a) Y) (Not (Or (Not (skS.0 0 a)) (Not Y)))) False % 5.02/5.18 Clause #20 (by clausification #[19]): ∀ (a a_1 : Prop), % 5.02/5.18 Eq (Not (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) (Not (Or (Not (skS.0 0 a)) (Not (skS.0 1 a a_1)))))) True % 5.02/5.18 Clause #21 (by clausification #[20]): ∀ (a a_1 : Prop), Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) (Not (Or (Not (skS.0 0 a)) (Not (skS.0 1 a a_1))))) False % 5.02/5.18 Clause #22 (by identity loobHoist #[21]): ∀ (a a_1 : Prop), % 5.02/5.18 Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) True) False) % 5.02/5.18 (Eq (Not (Or (Not (skS.0 0 a)) (Not (skS.0 1 a a_1)))) False) % 5.02/5.18 Clause #23 (by identity boolHoist #[21]): ∀ (a a_1 : Prop), % 5.02/5.18 Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) False) False) % 5.02/5.18 (Eq (Not (Or (Not (skS.0 0 a)) (Not (skS.0 1 a a_1)))) True) % 5.02/5.18 Clause #24 (by clausification #[22]): ∀ (a a_1 : Prop), % 5.02/5.18 Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) True) False) (Eq (Or (Not (skS.0 0 a)) (Not (skS.0 1 a a_1))) True) % 5.02/5.18 Clause #25 (by clausification #[24]): ∀ (a a_1 : Prop), % 5.02/5.18 Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) True) False) % 5.02/5.18 (Or (Eq (Not (skS.0 0 a)) True) (Eq (Not (skS.0 1 a a_1)) True)) % 5.02/5.18 Clause #26 (by clausification #[25]): ∀ (a a_1 : Prop), % 5.02/5.18 Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) True) False) % 5.02/5.18 (Or (Eq (Not (skS.0 1 a a_1)) True) (Eq (skS.0 0 a) False)) % 5.02/5.18 Clause #27 (by clausification #[26]): ∀ (a a_1 : Prop), % 5.02/5.18 Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) True) False) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) False)) % 5.02/5.18 Clause #28 (by identity loobHoist #[27]): ∀ (a a_1 : Prop), % 5.02/5.18 Or (Eq (skS.0 0 a) False) % 5.02/5.18 (Or (Eq (skS.0 1 a a_1) False) (Or (Eq (leibeq True True) False) (Eq (And (skS.0 0 a) (skS.0 1 a a_1)) False))) % 5.02/5.18 Clause #30 (by clausification #[28]): ∀ (a a_1 : Prop), % 5.02/5.18 Or (Eq (skS.0 0 a) False) % 5.02/5.18 (Or (Eq (skS.0 1 a a_1) False) % 5.02/5.18 (Or (Eq (leibeq True True) False) (Or (Eq (skS.0 0 a) False) (Eq (skS.0 1 a a_1) False)))) % 5.02/5.18 Clause #31 (by eliminate duplicate literals #[30]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 a) False) (Or (Eq (skS.0 1 a a_1) False) (Eq (leibeq True True) False)) % 5.02/5.18 Clause #33 (by identity boolHoist #[31]): ∀ (a a_1 : Prop), % 5.03/5.21 Or (Eq (skS.0 1 a a_1) False) (Or (Eq (leibeq True True) False) (Or (Eq (skS.0 0 False) False) (Eq a True))) % 5.03/5.21 Clause #39 (by bool simp #[16]): Eq (leibeq True True) True % 5.03/5.21 Clause #67 (by betaEtaReduce #[10]): ∀ (a a_1 : Prop), Or (Eq (leibeq False a) (∀ (P : Prop → Prop), P a_1 → P a)) (Eq a_1 True) % 5.03/5.21 Clause #69 (by identity boolHoist #[67]): ∀ (a a_1 : Prop), Or (Eq a True) (Or (Eq (leibeq False False) (∀ (P : Prop → Prop), P a → P a_1)) (Eq a_1 True)) % 5.03/5.21 Clause #86 (by equality factoring #[69]): ∀ (a : Prop), Or (Eq (leibeq False False) (∀ (P : Prop → Prop), P a → P a)) (Or (Ne True True) (Eq a True)) % 5.03/5.21 Clause #104 (by clausification #[23]): ∀ (a a_1 : Prop), % 5.03/5.21 Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) False) False) (Eq (Or (Not (skS.0 0 a)) (Not (skS.0 1 a a_1))) False) % 5.03/5.21 Clause #105 (by clausification #[104]): ∀ (a a_1 : Prop), Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) False) False) (Eq (Not (skS.0 1 a a_1)) False) % 5.03/5.21 Clause #106 (by clausification #[104]): ∀ (a a_1 : Prop), Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) False) False) (Eq (Not (skS.0 0 a)) False) % 5.03/5.21 Clause #107 (by clausification #[105]): ∀ (a a_1 : Prop), Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) False) False) (Eq (skS.0 1 a a_1) True) % 5.03/5.21 Clause #109 (by identity boolHoist #[107]): ∀ (a a_1 : Prop), % 5.03/5.21 Or (Eq (skS.0 1 a a_1) True) (Or (Eq (leibeq False False) False) (Eq (And (skS.0 0 a) (skS.0 1 a a_1)) True)) % 5.03/5.21 Clause #141 (by clausification #[86]): ∀ (a : Prop), % 5.03/5.21 Or (Eq (leibeq False False) (∀ (P : Prop → Prop), P a → P a)) (Or (Eq a True) (Or (Eq True False) (Eq True False))) % 5.03/5.21 Clause #143 (by clausification #[141]): ∀ (a : Prop), Or (Eq (leibeq False False) (∀ (P : Prop → Prop), P a → P a)) (Or (Eq a True) (Eq True False)) % 5.03/5.21 Clause #144 (by clausification #[143]): ∀ (a : Prop), Or (Eq (leibeq False False) (∀ (P : Prop → Prop), P a → P a)) (Eq a True) % 5.03/5.21 Clause #145 (by bool simp #[144]): ∀ (a : Prop), Or (Eq (leibeq False False) True) (Eq a True) % 5.03/5.21 Clause #146 (by equality factoring #[145]): Or (Ne True True) (Eq (leibeq False False) True) % 5.03/5.21 Clause #148 (by forward demodulation #[33, 39]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) False) (Or (Eq True False) (Or (Eq (skS.0 0 False) False) (Eq a True))) % 5.03/5.21 Clause #149 (by clausification #[148]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) False) (Or (Eq (skS.0 0 False) False) (Eq a True)) % 5.03/5.21 Clause #150 (by identity loobHoist #[149]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 False) False) (Or (Eq a True) (Or (Eq (skS.0 1 a True) False) (Eq a_1 False))) % 5.03/5.21 Clause #153 (by identity boolHoist #[150]): ∀ (a a_1 : Prop), % 5.03/5.21 Or (Eq (skS.0 0 False) False) (Or (Eq a True) (Or (Eq a_1 False) (Or (Eq (skS.0 1 False True) False) (Eq a True)))) % 5.03/5.21 Clause #154 (by clausification #[146]): Or (Eq (leibeq False False) True) (Or (Eq True False) (Eq True False)) % 5.03/5.21 Clause #156 (by clausification #[154]): Or (Eq (leibeq False False) True) (Eq True False) % 5.03/5.21 Clause #157 (by clausification #[156]): Eq (leibeq False False) True % 5.03/5.21 Clause #257 (by clausification #[106]): ∀ (a a_1 : Prop), Or (Eq (leibeq (And (skS.0 0 a) (skS.0 1 a a_1)) False) False) (Eq (skS.0 0 a) True) % 5.03/5.21 Clause #259 (by identity boolHoist #[257]): ∀ (a a_1 : Prop), % 5.03/5.21 Or (Eq (skS.0 0 a) True) (Or (Eq (leibeq False False) False) (Eq (And (skS.0 0 a) (skS.0 1 a a_1)) True)) % 5.03/5.21 Clause #276 (by clausification #[109]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) True) (Or (Eq (leibeq False False) False) (Eq (skS.0 1 a a_1) True)) % 5.03/5.21 Clause #278 (by eliminate duplicate literals #[276]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) True) (Eq (leibeq False False) False) % 5.03/5.21 Clause #279 (by forward demodulation #[278, 157]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a a_1) True) (Eq True False) % 5.03/5.21 Clause #280 (by clausification #[279]): ∀ (a a_1 : Prop), Eq (skS.0 1 a a_1) True % 5.03/5.21 Clause #281 (by identity loobHoist #[280]): ∀ (a a_1 : Prop), Or (Eq (skS.0 1 a True) True) (Eq a_1 False) % 5.03/5.21 Clause #284 (by identity boolHoist #[281]): ∀ (a a_1 : Prop), Or (Eq a False) (Or (Eq (skS.0 1 False True) True) (Eq a_1 True)) % 5.03/5.21 Clause #339 (by eliminate duplicate literals #[153]): ∀ (a a_1 : Prop), Or (Eq (skS.0 0 False) False) (Or (Eq a True) (Or (Eq a_1 False) (Eq (skS.0 1 False True) False))) % 5.07/5.22 Clause #343 (by falseElim #[284]): ∀ (a : Prop), Or (Eq (skS.0 1 False True) True) (Eq a True) % 5.07/5.22 Clause #346 (by equality factoring #[343]): Or (Ne True True) (Eq (skS.0 1 False True) True) % 5.07/5.22 Clause #348 (by clausification #[346]): Or (Eq (skS.0 1 False True) True) (Or (Eq True False) (Eq True False)) % 5.07/5.22 Clause #350 (by clausification #[348]): Or (Eq (skS.0 1 False True) True) (Eq True False) % 5.07/5.22 Clause #351 (by clausification #[350]): Eq (skS.0 1 False True) True % 5.07/5.22 Clause #429 (by clausification #[259]): ∀ (a : Prop), Or (Eq (skS.0 0 a) True) (Or (Eq (leibeq False False) False) (Eq (skS.0 0 a) True)) % 5.07/5.22 Clause #443 (by eliminate duplicate literals #[429]): ∀ (a : Prop), Or (Eq (skS.0 0 a) True) (Eq (leibeq False False) False) % 5.07/5.22 Clause #444 (by forward demodulation #[443, 157]): ∀ (a : Prop), Or (Eq (skS.0 0 a) True) (Eq True False) % 5.07/5.22 Clause #445 (by clausification #[444]): ∀ (a : Prop), Eq (skS.0 0 a) True % 5.07/5.22 Clause #447 (by identity boolHoist #[445]): ∀ (a : Prop), Or (Eq (skS.0 0 False) True) (Eq a True) % 5.07/5.22 Clause #457 (by equality factoring #[447]): Or (Ne True True) (Eq (skS.0 0 False) True) % 5.07/5.22 Clause #461 (by clausification #[457]): Or (Eq (skS.0 0 False) True) (Or (Eq True False) (Eq True False)) % 5.07/5.22 Clause #463 (by clausification #[461]): Or (Eq (skS.0 0 False) True) (Eq True False) % 5.07/5.22 Clause #464 (by clausification #[463]): Eq (skS.0 0 False) True % 5.07/5.22 Clause #465 (by backward demodulation #[464, 339]): ∀ (a a_1 : Prop), Or (Eq True False) (Or (Eq a True) (Or (Eq a_1 False) (Eq (skS.0 1 False True) False))) % 5.07/5.22 Clause #472 (by clausification #[465]): ∀ (a a_1 : Prop), Or (Eq a True) (Or (Eq a_1 False) (Eq (skS.0 1 False True) False)) % 5.07/5.22 Clause #476 (by falseElim #[472]): ∀ (a : Prop), Or (Eq a True) (Eq (skS.0 1 False True) False) % 5.07/5.22 Clause #477 (by superposition #[476, 351]): ∀ (a : Prop), Or (Eq a True) (Eq False True) % 5.07/5.22 Clause #478 (by clausification #[477]): ∀ (a : Prop), Eq a True % 5.07/5.22 Clause #479 (by falseElim #[478]): False % 5.07/5.22 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------