%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR129^2 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n015.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 6.66s 6.82s % Output : Proof 6.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : CSR129^2 : TPTP v9.2.0. Released v4.1.0. % 0.12/0.13 % Command : duper %s % 0.13/0.35 % Computer : n015.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 20:32:23 EDT 2025 % 0.20/0.35 % CPUTime : % 6.66/6.82 SZS status Theorem for theBenchmark.p % 6.66/6.82 SZS output start Proof for theBenchmark.p % 6.66/6.82 Clause #14 (by assumption #[]): Eq (range_THFTYPE_IiioI lWhenFn_THFTYPE_i lTimeInterval_THFTYPE_i) True % 6.66/6.82 Clause #22 (by assumption #[]): Eq % 6.66/6.82 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 6.66/6.82 (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i)) % 6.66/6.82 True % 6.66/6.82 Clause #61 (by assumption #[]): Eq % 6.66/6.82 (Not % 6.66/6.82 (Exists fun R => % 6.66/6.82 holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 6.66/6.82 (And (R lSue_THFTYPE_i lBill_THFTYPE_i) (R lMary_THFTYPE_i lBill_THFTYPE_i)))) % 6.66/6.82 True % 6.66/6.82 Clause #91 (by identity loobHoist #[22]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) % 6.66/6.82 (Eq (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i) False) % 6.66/6.82 Clause #92 (by identity boolHoist #[22]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 6.66/6.82 (Eq (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i) True) % 6.66/6.82 Clause #208 (by clausification #[61]): Eq % 6.66/6.82 (Exists fun R => % 6.66/6.82 holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 6.66/6.82 (And (R lSue_THFTYPE_i lBill_THFTYPE_i) (R lMary_THFTYPE_i lBill_THFTYPE_i))) % 6.66/6.82 False % 6.66/6.82 Clause #209 (by clausification #[208]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Eq % 6.66/6.82 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 6.66/6.82 (And (a lSue_THFTYPE_i lBill_THFTYPE_i) (a lMary_THFTYPE_i lBill_THFTYPE_i))) % 6.66/6.82 False % 6.66/6.82 Clause #210 (by identity loobHoist #[209]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 6.66/6.82 (Eq (And (a lSue_THFTYPE_i lBill_THFTYPE_i) (a lMary_THFTYPE_i lBill_THFTYPE_i)) False) % 6.66/6.82 Clause #211 (by identity boolHoist #[209]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) False) % 6.66/6.82 (Eq (And (a lSue_THFTYPE_i lBill_THFTYPE_i) (a lMary_THFTYPE_i lBill_THFTYPE_i)) True) % 6.66/6.82 Clause #212 (by clausification #[210]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 6.66/6.82 (Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False)) % 6.66/6.82 Clause #218 (by clausification #[211]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) False) % 6.66/6.82 (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) True) % 6.66/6.82 Clause #220 (by superposition #[218, 92]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) True) % 6.66/6.82 (Or (Eq False True) (Eq (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i) True)) % 6.66/6.82 Clause #236 (by clausification #[220]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) True) (Eq (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i) True) % 6.66/6.82 Clause #258 (by equality factoring #[236]): Or (Ne True True) (Eq (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i) True) % 6.66/6.82 Clause #266 (by clausification #[258]): Or (Eq (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i) True) (Or (Eq True False) (Eq True False)) % 6.66/6.82 Clause #268 (by clausification #[266]): Or (Eq (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i) True) (Eq True False) % 6.66/6.82 Clause #269 (by clausification #[268]): Eq (parent_THFTYPE_IiioI lMary_THFTYPE_i lAnna_THFTYPE_i) True % 6.66/6.82 Clause #270 (by backward demodulation #[269, 91]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) (Eq True False) % 6.66/6.82 Clause #272 (by clausification #[270]): Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True % 6.66/6.82 Clause #273 (by superposition #[272, 212]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq True False) (Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False)) % 6.66/6.82 Clause #501 (by clausification #[273]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) % 6.66/6.82 Clause #553 (by fluidLoobHoist #[501]): ∀ (a : Iota → Iota → Prop), % 6.66/6.82 Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) (Or (Eq True False) (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False)) % 6.66/6.83 Clause #554 (by clausification #[553]): ∀ (a : Iota → Iota → Prop), % 6.66/6.83 Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) % 6.66/6.83 Clause #592 (by superposition #[554, 14]): Or % 6.66/6.83 (Eq ((fun x x => range_THFTYPE_IiioI lWhenFn_THFTYPE_i lTimeInterval_THFTYPE_i) lSue_THFTYPE_i lBill_THFTYPE_i) False) % 6.66/6.83 (Eq False True) % 6.66/6.83 Clause #607 (by betaEtaReduce #[592]): Or (Eq (range_THFTYPE_IiioI lWhenFn_THFTYPE_i lTimeInterval_THFTYPE_i) False) (Eq False True) % 6.66/6.83 Clause #608 (by clausification #[607]): Eq (range_THFTYPE_IiioI lWhenFn_THFTYPE_i lTimeInterval_THFTYPE_i) False % 6.66/6.83 Clause #609 (by superposition #[608, 14]): Eq False True % 6.66/6.83 Clause #618 (by clausification #[609]): False % 6.66/6.83 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------