%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR128^2 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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:50 PM UTC 2025 % Result : Theorem 16.31s 16.52s % Output : Proof 16.40s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : CSR128^2 : TPTP v9.2.0. Released v4.1.0. % 0.07/0.14 % Command : duper %s % 0.13/0.35 % Computer : n016.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Thu Oct 2 19:38:53 EDT 2025 % 0.13/0.35 % CPUTime : % 16.31/16.52 SZS status Theorem for theBenchmark.p % 16.31/16.52 SZS output start Proof for theBenchmark.p % 16.31/16.52 Clause #5 (by assumption #[]): Eq % 16.31/16.52 (∀ (X : Iota), % 16.31/16.52 holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 16.31/16.52 (likes_THFTYPE_IiioI lMary_THFTYPE_i X → likes_THFTYPE_IiioI lSue_THFTYPE_i X)) % 16.31/16.52 True % 16.31/16.52 Clause #34 (by assumption #[]): Eq % 16.31/16.52 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 16.31/16.52 (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i)) % 16.31/16.52 True % 16.31/16.52 Clause #189 (by assumption #[]): Eq (Not (Exists fun T => Exists fun Z => holdsDuring_THFTYPE_IiooI T (likes_THFTYPE_IiioI lSue_THFTYPE_i Z))) True % 16.31/16.52 Clause #210 (by clausification #[5]): ∀ (a : Iota), % 16.31/16.52 Eq % 16.31/16.52 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 16.31/16.52 (likes_THFTYPE_IiioI lMary_THFTYPE_i a → likes_THFTYPE_IiioI lSue_THFTYPE_i a)) % 16.31/16.52 True % 16.31/16.52 Clause #211 (by identity loobHoist #[210]): ∀ (a : Iota), % 16.31/16.52 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) % 16.31/16.52 (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a → likes_THFTYPE_IiioI lSue_THFTYPE_i a) False) % 16.31/16.52 Clause #212 (by identity boolHoist #[210]): ∀ (a : Iota), % 16.31/16.52 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 16.31/16.52 (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a → likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) % 16.31/16.52 Clause #213 (by clausification #[211]): ∀ (a : Iota), % 16.31/16.52 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) % 16.31/16.52 (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) True) % 16.31/16.52 Clause #2103 (by identity loobHoist #[34]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) % 16.31/16.52 (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) False) % 16.31/16.52 Clause #2104 (by identity boolHoist #[34]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 16.31/16.52 (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True) % 16.31/16.52 Clause #2701 (by clausification #[212]): ∀ (a : Iota), % 16.31/16.52 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 16.31/16.52 (Or (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) False) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True)) % 16.31/16.52 Clause #2910 (by clausification #[189]): Eq (Exists fun T => Exists fun Z => holdsDuring_THFTYPE_IiooI T (likes_THFTYPE_IiioI lSue_THFTYPE_i Z)) False % 16.31/16.52 Clause #2911 (by clausification #[2910]): ∀ (a : Iota), Eq (Exists fun Z => holdsDuring_THFTYPE_IiooI a (likes_THFTYPE_IiioI lSue_THFTYPE_i Z)) False % 16.31/16.52 Clause #2912 (by clausification #[2911]): ∀ (a a_1 : Iota), Eq (holdsDuring_THFTYPE_IiooI a (likes_THFTYPE_IiioI lSue_THFTYPE_i a_1)) False % 16.31/16.52 Clause #2913 (by identity loobHoist #[2912]): ∀ (a a_1 : Iota), Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a_1) False) % 16.31/16.52 Clause #2914 (by identity boolHoist #[2912]): ∀ (a a_1 : Iota), Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a_1) True) % 16.31/16.52 Clause #2915 (by superposition #[2913, 213]): ∀ (a a_1 : Iota), % 16.31/16.52 Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) False) % 16.31/16.52 (Or (Eq False True) (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a_1) True)) % 16.31/16.52 Clause #3005 (by superposition #[2914, 2104]): ∀ (a : Iota), % 16.31/16.52 Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) % 16.31/16.52 (Or (Eq False True) (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True)) % 16.31/16.52 Clause #3010 (by clausification #[2915]): ∀ (a a_1 : Iota), % 16.31/16.52 Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) False) (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a_1) True) % 16.31/16.52 Clause #3017 (by clausification #[3005]): ∀ (a : Iota), % 16.31/16.52 Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True) % 16.31/16.52 Clause #3019 (by superposition #[3017, 3010]): ∀ (a : Iota), % 16.31/16.52 Or (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True) % 16.31/16.52 (Or (Eq True False) (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) True)) % 16.31/16.52 Clause #3054 (by clausification #[3019]): ∀ (a : Iota), % 16.31/16.52 Or (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True) (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) True) % 16.31/16.52 Clause #3058 (by equality factoring #[3054]): Or (Ne True True) (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True) % 16.40/16.58 Clause #3085 (by clausification #[3058]): Or (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True) (Or (Eq True False) (Eq True False)) % 16.40/16.58 Clause #3087 (by clausification #[3085]): Or (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True) (Eq True False) % 16.40/16.58 Clause #3088 (by clausification #[3087]): Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i lBill_THFTYPE_i) True % 16.40/16.58 Clause #3089 (by backward demodulation #[3088, 2103]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) (Eq True False) % 16.40/16.58 Clause #3104 (by clausification #[3089]): Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True % 16.40/16.58 Clause #3105 (by superposition #[3104, 2913]): ∀ (a : Iota), Or (Eq True False) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) False) % 16.40/16.58 Clause #3119 (by clausification #[3105]): ∀ (a : Iota), Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) False % 16.40/16.58 Clause #3120 (by backward demodulation #[3119, 2701]): ∀ (a : Iota), % 16.40/16.58 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 16.40/16.58 (Or (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) False) (Eq False True)) % 16.40/16.58 Clause #3801 (by clausification #[3120]): ∀ (a : Iota), % 16.40/16.58 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 16.40/16.58 (Eq (likes_THFTYPE_IiioI lMary_THFTYPE_i a) False) % 16.40/16.58 Clause #3802 (by superposition #[3801, 3088]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) (Eq False True) % 16.40/16.58 Clause #3809 (by clausification #[3802]): Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True % 16.40/16.58 Clause #3810 (by superposition #[3809, 2914]): ∀ (a : Iota), Or (Eq True False) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) % 16.40/16.58 Clause #3844 (by clausification #[3810]): ∀ (a : Iota), Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True % 16.40/16.58 Clause #3845 (by superposition #[3844, 3119]): Eq True False % 16.40/16.58 Clause #3867 (by clausification #[3845]): False % 16.40/16.58 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------