%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU810^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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:02:29 PM UTC 2025 % Result : Theorem 3.52s 3.71s % Output : Proof 3.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU810^2 : TPTP v9.2.0. Released v3.7.0. % 0.06/0.13 % Command : duper %s % 0.14/0.34 % Computer : n031.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 05:53:08 EDT 2025 % 0.14/0.34 % CPUTime : % 3.52/3.71 SZS status Theorem for theBenchmark.p % 3.52/3.71 SZS output start Proof for theBenchmark.p % 3.52/3.71 Clause #0 (by assumption #[]): Eq (Eq emptysetE (∀ (Xx : Iota), in Xx emptyset → ∀ (Xphi : Prop), Xphi)) True % 3.52/3.71 Clause #1 (by assumption #[]): Eq (Eq setadjoinIL (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy))) True % 3.52/3.71 Clause #3 (by assumption #[]): Eq (Eq omegaS fun Xx => setadjoin Xx Xx) True % 3.52/3.71 Clause #4 (by assumption #[]): Eq (Not (emptysetE → setadjoinIL → in__Cong → ∀ (Xx : Iota), in Xx omega → Ne (omegaS Xx) emptyset)) True % 3.52/3.71 Clause #5 (by clausification #[0]): Eq emptysetE (∀ (Xx : Iota), in Xx emptyset → ∀ (Xphi : Prop), Xphi) % 3.52/3.71 Clause #20 (by clausification #[1]): Eq setadjoinIL (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy)) % 3.52/3.71 Clause #22 (by clausify Prop equality #[20]): Or (Eq setadjoinIL False) (Eq (∀ (Xx Xy : Iota), in Xx (setadjoin Xx Xy)) True) % 3.52/3.71 Clause #24 (by clausification #[3]): Eq omegaS fun Xx => setadjoin Xx Xx % 3.52/3.71 Clause #25 (by argument congruence #[24]): ∀ (a : Iota), Eq (omegaS a) ((fun Xx => setadjoin Xx Xx) a) % 3.52/3.71 Clause #26 (by betaEtaReduce #[25]): ∀ (a : Iota), Eq (omegaS a) (setadjoin a a) % 3.52/3.71 Clause #31 (by clausification #[22]): ∀ (a : Iota), Or (Eq setadjoinIL False) (Eq (∀ (Xy : Iota), in a (setadjoin a Xy)) True) % 3.52/3.71 Clause #32 (by clausification #[31]): ∀ (a a_1 : Iota), Or (Eq setadjoinIL False) (Eq (in a (setadjoin a a_1)) True) % 3.52/3.71 Clause #37 (by clausification #[4]): Eq (emptysetE → setadjoinIL → in__Cong → ∀ (Xx : Iota), in Xx omega → Ne (omegaS Xx) emptyset) False % 3.52/3.71 Clause #38 (by clausification #[37]): Eq emptysetE True % 3.52/3.71 Clause #39 (by clausification #[37]): Eq (setadjoinIL → in__Cong → ∀ (Xx : Iota), in Xx omega → Ne (omegaS Xx) emptyset) False % 3.52/3.71 Clause #40 (by backward demodulation #[38, 5]): Eq True (∀ (Xx : Iota), in Xx emptyset → ∀ (Xphi : Prop), Xphi) % 3.52/3.71 Clause #45 (by clausification #[40]): ∀ (a : Iota), Eq (in a emptyset → ∀ (Xphi : Prop), Xphi) True % 3.52/3.71 Clause #46 (by clausification #[45]): ∀ (a : Iota), Or (Eq (in a emptyset) False) (Eq (∀ (Xphi : Prop), Xphi) True) % 3.52/3.71 Clause #47 (by clausification #[46]): ∀ (a : Iota) (a_1 : Prop), Or (Eq (in a emptyset) False) (Eq a_1 True) % 3.52/3.71 Clause #48 (by clausification #[39]): Eq setadjoinIL True % 3.52/3.71 Clause #49 (by clausification #[39]): Eq (in__Cong → ∀ (Xx : Iota), in Xx omega → Ne (omegaS Xx) emptyset) False % 3.52/3.71 Clause #52 (by backward demodulation #[48, 32]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (in a (setadjoin a a_1)) True) % 3.52/3.71 Clause #60 (by clausification #[52]): ∀ (a a_1 : Iota), Eq (in a (setadjoin a a_1)) True % 3.52/3.71 Clause #61 (by superposition #[60, 26]): ∀ (a : Iota), Eq (in a (omegaS a)) True % 3.52/3.71 Clause #64 (by clausification #[49]): Eq (∀ (Xx : Iota), in Xx omega → Ne (omegaS Xx) emptyset) False % 3.52/3.71 Clause #67 (by clausification #[64]): ∀ (a : Iota), Eq (Not (in (skS.0 6 a) omega → Ne (omegaS (skS.0 6 a)) emptyset)) True % 3.52/3.71 Clause #68 (by clausification #[67]): ∀ (a : Iota), Eq (in (skS.0 6 a) omega → Ne (omegaS (skS.0 6 a)) emptyset) False % 3.52/3.71 Clause #70 (by clausification #[68]): ∀ (a : Iota), Eq (Ne (omegaS (skS.0 6 a)) emptyset) False % 3.52/3.71 Clause #83 (by clausification #[70]): ∀ (a : Iota), Eq (omegaS (skS.0 6 a)) emptyset % 3.52/3.71 Clause #84 (by superposition #[83, 61]): ∀ (a : Iota), Eq (in (skS.0 6 a) emptyset) True % 3.52/3.71 Clause #85 (by superposition #[84, 47]): ∀ (a : Prop), Or (Eq True False) (Eq a True) % 3.52/3.71 Clause #86 (by clausification #[85]): ∀ (a : Prop), Eq a True % 3.52/3.71 Clause #87 (by falseElim #[86]): False % 3.52/3.71 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------