%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR148^2 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n018.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 07:46:54 PM UTC 2025 % Result : Theorem 9.76s 9.96s % Output : Proof 9.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : CSR148^2 : TPTP v9.2.0. Released v4.1.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n018.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 : Thu Oct 2 20:25:08 EDT 2025 % 0.13/0.34 % CPUTime : % 9.76/9.96 SZS status Theorem for theBenchmark.p % 9.76/9.96 SZS output start Proof for theBenchmark.p % 9.76/9.96 Clause #4 (by assumption #[]): Eq % 9.76/9.96 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 9.76/9.96 (∀ (X : Iota), likes_THFTYPE_IiioI lMary_THFTYPE_i X → likes_THFTYPE_IiioI lSue_THFTYPE_i X)) % 9.76/9.96 True % 9.76/9.96 Clause #6 (by assumption #[]): Eq (∀ (P : Prop) (Y : Iota), P → holdsDuring_THFTYPE_IiooI Y P) True % 9.76/9.96 Clause #23 (by assumption #[]): Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True % 9.76/9.96 Clause #190 (by assumption #[]): Eq % 9.76/9.96 (Not % 9.76/9.96 (Exists fun X => % 9.76/9.96 Exists fun Y => holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI Y) (likes_THFTYPE_IiioI lSue_THFTYPE_i X))) % 9.76/9.96 True % 9.76/9.96 Clause #211 (by identity boolHoist #[4]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 9.76/9.96 (Eq (∀ (X : Iota), likes_THFTYPE_IiioI lMary_THFTYPE_i X → likes_THFTYPE_IiioI lSue_THFTYPE_i X) True) % 9.76/9.96 Clause #217 (by clausification #[6]): ∀ (a : Prop), Eq (∀ (Y : Iota), a → holdsDuring_THFTYPE_IiooI Y a) True % 9.76/9.96 Clause #218 (by clausification #[217]): ∀ (a : Prop) (a_1 : Iota), Eq (a → holdsDuring_THFTYPE_IiooI a_1 a) True % 9.76/9.96 Clause #219 (by clausification #[218]): ∀ (a : Prop) (a_1 : Iota), Or (Eq a False) (Eq (holdsDuring_THFTYPE_IiooI a_1 a) True) % 9.76/9.96 Clause #220 (by identity loobHoist #[219]): ∀ (a : Prop) (a_1 : Iota), Or (Eq a False) (Or (Eq (holdsDuring_THFTYPE_IiooI a_1 True) True) (Eq a False)) % 9.76/9.96 Clause #222 (by eliminate duplicate literals #[220]): ∀ (a : Prop) (a_1 : Iota), Or (Eq a False) (Eq (holdsDuring_THFTYPE_IiooI a_1 True) True) % 9.76/9.96 Clause #225 (by falseElim #[222]): ∀ (a : Iota), Eq (holdsDuring_THFTYPE_IiooI a True) True % 9.76/9.96 Clause #2819 (by clausification #[190]): Eq % 9.76/9.96 (Exists fun X => % 9.76/9.96 Exists fun Y => holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI Y) (likes_THFTYPE_IiioI lSue_THFTYPE_i X)) % 9.76/9.96 False % 9.76/9.96 Clause #2820 (by clausification #[2819]): ∀ (a : Iota), % 9.76/9.96 Eq (Exists fun Y => holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI Y) (likes_THFTYPE_IiioI lSue_THFTYPE_i a)) False % 9.76/9.96 Clause #2821 (by clausification #[2820]): ∀ (a a_1 : Iota), Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI a) (likes_THFTYPE_IiioI lSue_THFTYPE_i a_1)) False % 9.76/9.96 Clause #2822 (by identity loobHoist #[2821]): ∀ (a a_1 : Iota), % 9.76/9.96 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI a) True) False) % 9.76/9.96 (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a_1) False) % 9.76/9.96 Clause #2823 (by identity boolHoist #[2821]): ∀ (a a_1 : Iota), % 9.76/9.96 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI a) False) False) % 9.76/9.96 (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a_1) True) % 9.76/9.96 Clause #2824 (by superposition #[2822, 225]): ∀ (a : Iota), Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) False) (Eq False True) % 9.76/9.96 Clause #2829 (by clausification #[2824]): ∀ (a : Iota), Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) False % 9.76/9.96 Clause #3141 (by clausification #[211]): ∀ (a : Iota), % 9.76/9.96 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 9.76/9.96 (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a → likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) % 9.76/9.96 Clause #3142 (by clausification #[3141]): ∀ (a : Iota), % 9.76/9.96 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 9.76/9.96 (Or (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) False) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True)) % 9.76/9.96 Clause #3143 (by forward demodulation #[3142, 2829]): ∀ (a : Iota), % 9.76/9.96 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 9.76/9.96 (Or (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) False) (Eq False True)) % 9.76/9.96 Clause #3144 (by clausification #[3143]): ∀ (a : Iota), % 9.76/9.96 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 9.76/9.96 (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) False) % 9.76/9.96 Clause #3145 (by superposition #[3144, 23]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) (Eq False True) % 9.76/9.96 Clause #3166 (by clausification #[3145]): Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True % 9.76/9.96 Clause #3167 (by superposition #[3166, 2823]): ∀ (a : Iota), Or (Eq True False) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) % 9.76/9.98 Clause #3182 (by clausification #[3167]): ∀ (a : Iota), Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True % 9.76/9.98 Clause #3183 (by superposition #[3182, 2829]): Eq True False % 9.76/9.98 Clause #3201 (by clausification #[3183]): False % 9.76/9.98 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------