%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SYO183^6 : TPTP v9.2.0. Released v5.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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:42 PM UTC 2025 % Result : Theorem 34.99s 35.20s % Output : Proof 35.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SYO183^6 : TPTP v9.2.0. Released v5.1.0. % 0.10/0.13 % Command : duper %s % 0.13/0.34 % Computer : n021.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 12:56:23 EDT 2025 % 0.13/0.34 % CPUTime : % 34.99/35.20 SZS status Theorem for theBenchmark.p % 34.99/35.20 SZS output start Proof for theBenchmark.p % 34.99/35.20 Clause #0 (by assumption #[]): Eq (Not (∀ (Xp : Prop), Exists fun Xf => Xf Xp)) True % 34.99/35.20 Clause #1 (by clausification #[0]): Eq (∀ (Xp : Prop), Exists fun Xf => Xf Xp) False % 34.99/35.20 Clause #2 (by clausification #[1]): ∀ (a : Prop), Eq (Not (Exists fun Xf => Xf (skS.0 0 a))) True % 34.99/35.20 Clause #3 (by clausification #[2]): ∀ (a : Prop), Eq (Exists fun Xf => Xf (skS.0 0 a)) False % 34.99/35.20 Clause #4 (by clausification #[3]): ∀ (a : Prop → Prop) (a_1 : Prop), Eq (a (skS.0 0 a_1)) False % 34.99/35.20 Clause #5 (by identity loobHoist #[4]): ∀ (a : Prop → Prop) (a_1 : Prop), Or (Eq (a True) False) (Eq (skS.0 0 a_1) False) % 34.99/35.20 Clause #6 (by identity boolHoist #[4]): ∀ (a : Prop → Prop) (a_1 : Prop), Or (Eq (a False) False) (Eq (skS.0 0 a_1) True) % 34.99/35.20 Clause #7 (by identity loobHoist #[5]): ∀ (a : Prop → Prop) (a_1 : Prop), Or (Eq (a True) False) (Or (Eq (skS.0 0 True) False) (Eq a_1 False)) % 34.99/35.20 Clause #13 (by fluidLoobHoist #[7]): ∀ (a : Prop) (a_1 : Prop → Prop), % 34.99/35.20 Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Or (Eq True False) (Eq (a_1 True) False))) % 34.99/35.20 Clause #15 (by identity loobHoist #[6]): ∀ (a : Prop → Prop) (a_1 : Prop), Or (Eq (a False) False) (Or (Eq (skS.0 0 True) True) (Eq a_1 False)) % 34.99/35.20 Clause #16 (by identity boolHoist #[6]): ∀ (a : Prop → Prop) (a_1 : Prop), Or (Eq (a False) False) (Or (Eq (skS.0 0 False) True) (Eq a_1 True)) % 34.99/35.20 Clause #21 (by fluidLoobHoist #[15]): ∀ (a : Prop) (a_1 : Prop → Prop), % 34.99/35.20 Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Or (Eq True False) (Eq (a_1 False) False))) % 34.99/35.20 Clause #29 (by neHoist #[16]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 34.99/35.20 Or (Eq (skS.0 0 False) True) (Or (Eq a True) (Or (Eq True False) (Eq (a_2 False) (a_3 False)))) % 34.99/35.20 Clause #34 (by clausification #[13]): ∀ (a : Prop) (a_1 : Prop → Prop), Or (Eq (skS.0 0 True) False) (Or (Eq a False) (Eq (a_1 True) False)) % 34.99/35.20 Clause #39 (by clausification #[21]): ∀ (a : Prop) (a_1 : Prop → Prop), Or (Eq (skS.0 0 True) True) (Or (Eq a False) (Eq (a_1 False) False)) % 34.99/35.20 Clause #40 (by falseElim #[39]): ∀ (a : Prop → Prop), Or (Eq (skS.0 0 True) True) (Eq (a False) False) % 34.99/35.20 Clause #46 (by neHoist #[40]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x), % 34.99/35.20 Or (Eq (skS.0 0 True) True) (Or (Eq True False) (Eq (a_1 False) (a_2 False))) % 34.99/35.20 Clause #56 (by clausification #[46]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x), Or (Eq (skS.0 0 True) True) (Eq (a_1 False) (a_2 False)) % 34.99/35.20 Clause #57 (by superposition #[56, 34]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop) (a_4 : Prop → Prop), % 34.99/35.20 Or (Eq (a_1 False) (a_2 False)) (Or (Eq True False) (Or (Eq a_3 False) (Eq (a_4 True) False))) % 34.99/35.20 Clause #74 (by clausification #[57]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop) (a_4 : Prop → Prop), % 34.99/35.20 Or (Eq (a_1 False) (a_2 False)) (Or (Eq a_3 False) (Eq (a_4 True) False)) % 34.99/35.20 Clause #76 (by falseElim #[74]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop → Prop), % 34.99/35.20 Or (Eq (a_1 False) (a_2 False)) (Eq (a_3 True) False) % 34.99/35.20 Clause #85 (by neHoist #[76]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop → Sort _abstMVar.1) % 34.99/35.20 (a_4 a_5 : (x : Prop) → a_3 x), Or (Eq (a_1 False) (a_2 False)) (Or (Eq True False) (Eq (a_4 True) (a_5 True))) % 34.99/35.20 Clause #98 (by clausification #[85]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop → Sort _abstMVar.1) % 34.99/35.20 (a_4 a_5 : (x : Prop) → a_3 x), Or (Eq (a_1 False) (a_2 False)) (Eq (a_4 True) (a_5 True)) % 34.99/35.20 Clause #119 (by neHoist #[98]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x) % 34.99/35.20 (a_4 : Prop → Sort _abstMVar.1) (a_5 a_6 : (x : Prop) → a_4 x), % 34.99/35.20 Or (Eq (a_1 True) (a_2 True)) (Or (Eq True (a_3 False)) (Eq (a_5 False) (a_6 False))) % 34.99/35.20 Clause #236 (by betaEtaReduce #[119]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x) % 34.99/35.20 (a_4 : Prop → Sort _abstMVar.1) (a_5 a_6 : (x : Prop) → a_4 x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Eq True (a_3 False)) (Eq (a_5 False) (a_6 False))) % 34.99/35.22 Clause #261 (by equality factoring #[236]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Ne True (a_3 False)) (Eq ((fun x => False) False) (a_3 False))) % 34.99/35.22 Clause #1450 (by clausification #[29]): ∀ (a : Prop) (a_1 : Prop → Sort _abstMVar.0) (a_2 a_3 : (x : Prop) → a_1 x), % 34.99/35.22 Or (Eq (skS.0 0 False) True) (Or (Eq a True) (Eq (a_2 False) (a_3 False))) % 34.99/35.22 Clause #1813 (by betaEtaReduce #[261]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Ne True (a_3 False)) (Eq False (a_3 False))) % 34.99/35.22 Clause #1814 (by clausification #[1813]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Eq False (a_3 False)) (Or (Eq True False) (Eq (a_3 False) False))) % 34.99/35.22 Clause #1816 (by clausification #[1814]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Eq False (a_3 False)) (Eq (a_3 False) False)) % 34.99/35.22 Clause #1817 (by eliminate duplicate literals #[1816]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Eq False (a_3 False)) % 34.99/35.22 Clause #1820 (by existsHoist #[1817]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop → Sort _abstMVar.1) % 34.99/35.22 (a_4 : (x : Prop) → a_3 x → Prop) (a_5 : a_3 False), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Eq False True) (Eq ((fun x => a_4 False x) a_5) False)) % 34.99/35.22 Clause #1859 (by betaEtaReduce #[1820]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop → Sort _abstMVar.1) % 34.99/35.22 (a_4 : (x : Prop) → a_3 x → Prop) (a_5 : a_3 False), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Eq False True) (Eq (a_4 False a_5) False)) % 34.99/35.22 Clause #1860 (by clausification #[1859]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop → Sort _abstMVar.1) % 34.99/35.22 (a_4 : (x : Prop) → a_3 x → Prop) (a_5 : a_3 False), Or (Eq (a_1 True) (a_2 True)) (Eq (a_4 False a_5) False) % 34.99/35.22 Clause #1861 (by superposition #[1860, 1450]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop) (a_4 : Prop → Sort _abstMVar.1) % 34.99/35.22 (a_5 a_6 : (x : Prop) → a_4 x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Eq False True) (Or (Eq a_3 True) (Eq (a_5 False) (a_6 False)))) % 34.99/35.22 Clause #2088 (by clausification #[1861]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop) (a_4 : Prop → Sort _abstMVar.1) % 34.99/35.22 (a_5 a_6 : (x : Prop) → a_4 x), Or (Eq (a_1 True) (a_2 True)) (Or (Eq a_3 True) (Eq (a_5 False) (a_6 False))) % 34.99/35.22 Clause #2138 (by equality factoring #[2088]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x) (a_4 : Prop), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Ne (a_3 False) a_4) (Eq a_4 True)) % 34.99/35.22 Clause #2232 (by betaEtaReduce #[2138]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x) (a_4 : Prop), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Ne (a_3 False) a_4) (Eq a_4 True)) % 34.99/35.22 Clause #2234 (by clausification #[2232]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop) (a_4 : (x : Prop) → (fun x => Prop) x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Eq a_3 True) (Or (Eq (a_4 False) True) (Eq a_3 True))) % 34.99/35.22 Clause #2500 (by eliminate duplicate literals #[2234]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : Prop) (a_4 : (x : Prop) → (fun x => Prop) x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Or (Eq a_3 True) (Eq (a_4 False) True)) % 34.99/35.22 Clause #2541 (by falseElim #[2500]): ∀ (a : Prop → Sort _abstMVar.0) (a_1 a_2 : (x : Prop) → a x) (a_3 : (x : Prop) → (fun x => Prop) x), % 34.99/35.22 Or (Eq (a_1 True) (a_2 True)) (Eq (a_3 False) True) % 35.37/35.56 Clause #2747 (by equality factoring #[2541]): ∀ (a : (x : Prop) → (fun x => Prop) x), Or (Ne True (a True)) (Eq (a True) ((fun x => False) True)) % 35.37/35.56 Clause #2945 (by betaEtaReduce #[2747]): ∀ (a : (x : Prop) → (fun x => Prop) x), Or (Ne True (a True)) (Eq (a True) False) % 35.37/35.56 Clause #2946 (by clausification #[2945]): ∀ (a : (x : Prop) → (fun x => Prop) x), Or (Eq (a True) False) (Or (Eq True False) (Eq (a True) False)) % 35.37/35.56 Clause #2948 (by clausification #[2946]): ∀ (a : (x : Prop) → (fun x => Prop) x), Or (Eq (a True) False) (Eq (a True) False) % 35.37/35.56 Clause #2949 (by eliminate duplicate literals #[2948]): ∀ (a : (x : Prop) → (fun x => Prop) x), Eq (a True) False % 35.37/35.56 Clause #3009 (by fluidSup #[2949, 2541]): ∀ (a a_1 : (x : Prop) → (fun x => Prop) x), Or (Eq (a True) ((fun _ => True) False)) (Eq (a_1 False) True) % 35.37/35.56 Clause #3294 (by betaEtaReduce #[3009]): ∀ (a a_1 : (x : Prop) → (fun x => Prop) x), Or (Eq (a True) True) (Eq (a_1 False) True) % 35.37/35.56 Clause #3300 (by equality factoring #[3294]): Or (Ne True True) (Eq ((fun x => False) True) True) % 35.37/35.56 Clause #3461 (by betaEtaReduce #[3300]): Or (Ne True True) (Eq False True) % 35.37/35.56 Clause #3462 (by clausification #[3461]): Or (Eq False True) (Or (Eq True False) (Eq True False)) % 35.37/35.56 Clause #3464 (by clausification #[3462]): Or (Eq True False) (Eq True False) % 35.37/35.56 Clause #3465 (by clausification #[3464]): Eq True False % 35.37/35.56 Clause #3466 (by clausification #[3465]): False % 35.37/35.56 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------