%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : CSR130^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:51 PM UTC 2025 % Result : Theorem 17.93s 18.18s % Output : Proof 18.09s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : CSR130^2 : TPTP v9.2.0. Released v4.1.0. % 0.12/0.14 % 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:34:08 EDT 2025 % 0.13/0.35 % CPUTime : % 17.93/18.18 SZS status Theorem for theBenchmark.p % 17.93/18.18 SZS output start Proof for theBenchmark.p % 17.93/18.18 Clause #3 (by assumption #[]): Eq % 17.93/18.18 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 17.93/18.18 (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i)) % 17.93/18.18 True % 17.93/18.18 Clause #6 (by assumption #[]): Eq % 17.93/18.18 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 17.93/18.18 (Not (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i))) % 17.93/18.18 True % 17.93/18.18 Clause #8 (by assumption #[]): Eq % 17.93/18.18 (∀ (TIME : Iota) (SITUATION : Prop), % 17.93/18.18 holdsDuring_THFTYPE_IiooI TIME (Not SITUATION) → Not (holdsDuring_THFTYPE_IiooI TIME SITUATION)) % 17.93/18.18 True % 17.93/18.18 Clause #9 (by assumption #[]): Eq % 17.93/18.18 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 17.93/18.18 (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i)) % 17.93/18.18 True % 17.93/18.18 Clause #61 (by assumption #[]): Eq % 17.93/18.18 (Not % 17.93/18.18 (Exists fun R => % 17.93/18.18 holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 17.93/18.18 (And (And (R lSue_THFTYPE_i lBill_THFTYPE_i) (R lMary_THFTYPE_i lBill_THFTYPE_i)) % 17.93/18.18 (Not (∀ (A B : Iota), R A B))))) % 17.93/18.19 True % 17.93/18.19 Clause #75 (by identity boolHoist #[3]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 17.93/18.19 (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i) True) % 17.93/18.19 Clause #86 (by identity loobHoist #[6]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) % 17.93/18.19 (Eq (Not (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i)) False) % 17.93/18.19 Clause #87 (by identity boolHoist #[6]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 17.93/18.19 (Eq (Not (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i)) True) % 17.93/18.19 Clause #88 (by clausification #[86]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) % 17.93/18.19 (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 17.93/18.19 Clause #100 (by identity loobHoist #[9]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) % 17.93/18.19 (Eq (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i) False) % 17.93/18.19 Clause #101 (by identity boolHoist #[9]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 17.93/18.19 (Eq (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i) True) % 17.93/18.19 Clause #102 (by clausification #[8]): ∀ (a : Iota), % 17.93/18.19 Eq (∀ (SITUATION : Prop), holdsDuring_THFTYPE_IiooI a (Not SITUATION) → Not (holdsDuring_THFTYPE_IiooI a SITUATION)) % 17.93/18.19 True % 17.93/18.19 Clause #103 (by clausification #[102]): ∀ (a : Iota) (a_1 : Prop), Eq (holdsDuring_THFTYPE_IiooI a (Not a_1) → Not (holdsDuring_THFTYPE_IiooI a a_1)) True % 17.93/18.19 Clause #104 (by clausification #[103]): ∀ (a : Iota) (a_1 : Prop), % 17.93/18.19 Or (Eq (holdsDuring_THFTYPE_IiooI a (Not a_1)) False) (Eq (Not (holdsDuring_THFTYPE_IiooI a a_1)) True) % 17.93/18.19 Clause #105 (by clausification #[104]): ∀ (a : Iota) (a_1 : Prop), % 17.93/18.19 Or (Eq (holdsDuring_THFTYPE_IiooI a (Not a_1)) False) (Eq (holdsDuring_THFTYPE_IiooI a a_1) False) % 17.93/18.19 Clause #106 (by identity loobHoist #[105]): ∀ (a : Iota) (a_1 : Prop), % 17.93/18.19 Or (Eq (holdsDuring_THFTYPE_IiooI a a_1) False) % 17.93/18.19 (Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) (Eq (Not a_1) False)) % 17.93/18.19 Clause #107 (by identity boolHoist #[105]): ∀ (a : Iota) (a_1 : Prop), % 17.93/18.19 Or (Eq (holdsDuring_THFTYPE_IiooI a a_1) False) % 17.93/18.19 (Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) (Eq (Not a_1) True)) % 17.93/18.19 Clause #108 (by clausification #[106]): ∀ (a : Iota) (a_1 : Prop), % 17.93/18.19 Or (Eq (holdsDuring_THFTYPE_IiooI a a_1) False) (Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) (Eq a_1 True)) % 17.93/18.19 Clause #110 (by identity boolHoist #[108]): ∀ (a : Iota) (a_1 : Prop), % 17.93/18.19 Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) % 17.93/18.19 (Or (Eq a_1 True) (Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) (Eq a_1 True))) % 17.93/18.19 Clause #162 (by clausification #[87]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) % 17.93/18.19 (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) False) % 17.93/18.19 Clause #169 (by clausification #[107]): ∀ (a : Iota) (a_1 : Prop), % 17.93/18.19 Or (Eq (holdsDuring_THFTYPE_IiooI a a_1) False) (Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) (Eq a_1 False)) % 17.93/18.19 Clause #170 (by identity loobHoist #[169]): ∀ (a : Iota) (a_1 : Prop), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) % 18.03/18.23 (Or (Eq a_1 False) (Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) (Eq a_1 False))) % 18.03/18.23 Clause #172 (by eliminate duplicate literals #[170]): ∀ (a : Iota) (a_1 : Prop), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI a False) False) (Or (Eq a_1 False) (Eq (holdsDuring_THFTYPE_IiooI a True) False)) % 18.03/18.23 Clause #176 (by superposition #[172, 75]): ∀ (a : Prop), % 18.03/18.23 Or (Eq a False) % 18.03/18.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.23 (Or (Eq False True) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i) True))) % 18.03/18.23 Clause #186 (by eliminate duplicate literals #[110]): ∀ (a : Iota) (a_1 : Prop), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI a True) False) (Or (Eq a_1 True) (Eq (holdsDuring_THFTYPE_IiooI a False) False)) % 18.03/18.23 Clause #208 (by clausification #[61]): Eq % 18.03/18.23 (Exists fun R => % 18.03/18.23 holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 18.03/18.23 (And (And (R lSue_THFTYPE_i lBill_THFTYPE_i) (R lMary_THFTYPE_i lBill_THFTYPE_i)) (Not (∀ (A B : Iota), R A B)))) % 18.03/18.23 False % 18.03/18.23 Clause #209 (by clausification #[208]): ∀ (a : Iota → Iota → Prop), % 18.03/18.23 Eq % 18.03/18.23 (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) % 18.03/18.23 (And (And (a lSue_THFTYPE_i lBill_THFTYPE_i) (a lMary_THFTYPE_i lBill_THFTYPE_i)) (Not (∀ (A B : Iota), a A B)))) % 18.03/18.23 False % 18.03/18.23 Clause #210 (by identity loobHoist #[209]): ∀ (a : Iota → Iota → Prop), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.23 (Eq (And (And (a lSue_THFTYPE_i lBill_THFTYPE_i) (a lMary_THFTYPE_i lBill_THFTYPE_i)) (Not (∀ (A B : Iota), a A B))) % 18.03/18.23 False) % 18.03/18.23 Clause #211 (by identity boolHoist #[209]): ∀ (a : Iota → Iota → Prop), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) False) % 18.03/18.23 (Eq (And (And (a lSue_THFTYPE_i lBill_THFTYPE_i) (a lMary_THFTYPE_i lBill_THFTYPE_i)) (Not (∀ (A B : Iota), a A B))) % 18.03/18.23 True) % 18.03/18.23 Clause #212 (by clausification #[210]): ∀ (a : Iota → Iota → Prop), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.23 (Or (Eq (And (a lSue_THFTYPE_i lBill_THFTYPE_i) (a lMary_THFTYPE_i lBill_THFTYPE_i)) False) % 18.03/18.23 (Eq (Not (∀ (A B : Iota), a A B)) False)) % 18.03/18.23 Clause #213 (by clausification #[212]): ∀ (a : Iota → Iota → Prop), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.23 (Or (Eq (Not (∀ (A B : Iota), a A B)) False) % 18.03/18.23 (Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False))) % 18.03/18.23 Clause #214 (by clausification #[213]): ∀ (a : Iota → Iota → Prop), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.23 (Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.23 (Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) (Eq (∀ (A B : Iota), a A B) True))) % 18.03/18.23 Clause #215 (by clausification #[214]): ∀ (a : Iota → Iota → Prop) (a_1 : Iota), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.23 (Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.23 (Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) (Eq (∀ (B : Iota), a a_1 B) True))) % 18.03/18.23 Clause #216 (by clausification #[215]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.03/18.23 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.23 (Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.23 (Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) (Eq (a a_1 a_2) True))) % 18.03/18.23 Clause #217 (by superposition #[216, 88]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.03/18.23 Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.23 (Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.23 (Or (Eq (a a_1 a_2) True) (Or (Eq False True) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True)))) % 18.03/18.23 Clause #382 (by clausification #[176]): ∀ (a : Prop), % 18.03/18.23 Or (Eq a False) % 18.03/18.23 (Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.23 (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i) True)) % 18.03/18.27 Clause #397 (by falseElim #[382]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) False) % 18.03/18.27 (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i) True) % 18.03/18.27 Clause #477 (by clausification #[211]): ∀ (a : Iota → Iota → Prop), % 18.03/18.27 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) False) % 18.03/18.27 (Eq (And (a lSue_THFTYPE_i lBill_THFTYPE_i) (a lMary_THFTYPE_i lBill_THFTYPE_i)) True) % 18.03/18.27 Clause #491 (by clausification #[477]): ∀ (a : Iota → Iota → Prop), % 18.03/18.27 Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) False) % 18.03/18.27 (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) True) % 18.03/18.27 Clause #505 (by superposition #[491, 101]): ∀ (a : Iota → Iota → Prop), % 18.03/18.27 Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) True) % 18.03/18.27 (Or (Eq False True) (Eq (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i) True)) % 18.03/18.27 Clause #506 (by clausification #[505]): ∀ (a : Iota → Iota → Prop), % 18.03/18.27 Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) True) (Eq (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i) True) % 18.03/18.27 Clause #537 (by equality factoring #[506]): Or (Ne True True) (Eq (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i) True) % 18.03/18.27 Clause #545 (by clausification #[537]): Or (Eq (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i) True) (Or (Eq True False) (Eq True False)) % 18.03/18.27 Clause #547 (by clausification #[545]): Or (Eq (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i) True) (Eq True False) % 18.03/18.27 Clause #548 (by clausification #[547]): Eq (parent_THFTYPE_IiioI lSue_THFTYPE_i lAnna_THFTYPE_i) True % 18.03/18.27 Clause #549 (by backward demodulation #[548, 100]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True) (Eq True False) % 18.03/18.27 Clause #553 (by clausification #[217]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.03/18.27 Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.27 (Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.27 (Or (Eq (a a_1 a_2) True) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True))) % 18.03/18.27 Clause #611 (by fluidLoobHoist #[553]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.03/18.27 Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.27 (Or (Eq (a a_1 a_2) True) % 18.03/18.27 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.03/18.27 (Or (Eq True False) (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False)))) % 18.03/18.27 Clause #612 (by clausification #[549]): Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) True) True % 18.03/18.27 Clause #617 (by superposition #[612, 397]): Or (Eq True False) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i) True) % 18.03/18.27 Clause #620 (by superposition #[612, 186]): ∀ (a : Prop), % 18.03/18.27 Or (Eq True False) % 18.03/18.27 (Or (Eq a True) (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) False)) % 18.03/18.27 Clause #637 (by clausification #[617]): Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i) True % 18.03/18.27 Clause #649 (by clausification #[620]): ∀ (a : Prop), Or (Eq a True) (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) False) % 18.03/18.27 Clause #977 (by clausification #[611]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.03/18.27 Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.27 (Or (Eq (a a_1 a_2) True) % 18.03/18.27 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False))) % 18.03/18.27 Clause #1029 (by fluidLoobHoist #[977]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.03/18.27 Or (Eq (a a_1 a_2) True) % 18.03/18.27 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.03/18.27 (Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) % 18.03/18.27 (Or (Eq True False) (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False)))) % 18.03/18.27 Clause #1030 (by clausification #[1029]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.03/18.27 Or (Eq (a a_1 a_2) True) % 18.03/18.27 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.03/18.27 (Or (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False) (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False))) % 18.03/18.27 Clause #1082 (by fluidLoobHoist #[1030]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.03/18.27 Or (Eq (a a_1 a_2) True) % 18.03/18.27 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.09/18.32 (Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) % 18.09/18.32 (Or (Eq True False) (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False)))) % 18.09/18.32 Clause #1084 (by clausification #[1082]): ∀ (a : Iota → Iota → Prop) (a_1 a_2 : Iota), % 18.09/18.32 Or (Eq (a a_1 a_2) True) % 18.09/18.32 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.09/18.32 (Or (Eq (a lMary_THFTYPE_i lBill_THFTYPE_i) False) (Eq (a lSue_THFTYPE_i lBill_THFTYPE_i) False))) % 18.09/18.32 Clause #1085 (by superposition #[1084, 637]): ∀ (a a_1 : Iota), % 18.09/18.32 Or (Eq ((fun x x => likes_THFTYPE_IiioI lSue_THFTYPE_i x) a a_1) True) % 18.09/18.32 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.09/18.32 (Or (Eq ((fun x x => likes_THFTYPE_IiioI lSue_THFTYPE_i x) lSue_THFTYPE_i lBill_THFTYPE_i) False) % 18.09/18.32 (Eq False True))) % 18.09/18.32 Clause #1506 (by betaEtaReduce #[1085]): ∀ (a : Iota), % 18.09/18.32 Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) % 18.09/18.32 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.09/18.32 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i) False) (Eq False True))) % 18.09/18.32 Clause #1507 (by clausification #[1506]): ∀ (a : Iota), % 18.09/18.32 Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) % 18.09/18.32 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.09/18.32 (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lBill_THFTYPE_i) False)) % 18.09/18.32 Clause #1508 (by superposition #[1507, 637]): ∀ (a : Iota), % 18.09/18.32 Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) % 18.09/18.32 (Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) (Eq False True)) % 18.09/18.32 Clause #1526 (by clausification #[1508]): ∀ (a : Iota), % 18.09/18.32 Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i a) True) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.09/18.32 Clause #1528 (by equality factoring #[1526]): Or (Ne True True) (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) % 18.09/18.32 Clause #1554 (by clausification #[1528]): Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) (Or (Eq True False) (Eq True False)) % 18.09/18.32 Clause #1556 (by clausification #[1554]): Or (Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True) (Eq True False) % 18.09/18.32 Clause #1557 (by clausification #[1556]): Eq (likes_THFTYPE_IiioI lSue_THFTYPE_i lMary_THFTYPE_i) True % 18.09/18.32 Clause #1558 (by backward demodulation #[1557, 162]): Or (Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True) (Eq True False) % 18.09/18.32 Clause #1572 (by clausification #[1558]): Eq (holdsDuring_THFTYPE_IiooI (lYearFn_THFTYPE_IiiI n2009_THFTYPE_i) False) True % 18.09/18.32 Clause #1576 (by superposition #[1572, 649]): ∀ (a : Prop), Or (Eq a True) (Eq True False) % 18.09/18.32 Clause #1582 (by clausification #[1576]): ∀ (a : Prop), Eq a True % 18.09/18.32 Clause #1586 (by falseElim #[1582]): False % 18.09/18.32 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------