%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ130+1 : TPTP v9.2.0. Released v4.1.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n002.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:58:23 PM UTC 2025 % Result : Theorem 4.58s 4.77s % Output : Proof 4.58s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PUZ130+1 : TPTP v9.2.0. Released v4.1.0. % 0.03/0.13 % Command : duper %s % 0.14/0.33 % Computer : n002.cluster.edu % 0.14/0.33 % Model : x86_64 x86_64 % 0.14/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.33 % Memory : 8042.1875MB % 0.14/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.33 % CPULimit : 300 % 0.14/0.33 % WCLimit : 300 % 0.14/0.33 % DateTime : Thu Oct 2 20:45:08 EDT 2025 % 0.14/0.33 % CPUTime : % 4.58/4.77 SZS status Theorem for theBenchmark.p % 4.58/4.77 SZS output start Proof for theBenchmark.p % 4.58/4.77 Clause #1 (by assumption #[]): Eq (cat garfield) True % 4.58/4.77 Clause #3 (by assumption #[]): Eq (dog odie) True % 4.58/4.77 Clause #5 (by assumption #[]): Eq (∀ (A : Iota), dog A → pet A) True % 4.58/4.77 Clause #6 (by assumption #[]): Eq (∀ (A : Iota), cat A → pet A) True % 4.58/4.77 Clause #8 (by assumption #[]): Eq (human jon) True % 4.58/4.77 Clause #11 (by assumption #[]): Eq (owner jon odie) True % 4.58/4.77 Clause #12 (by assumption #[]): Eq (owner jon garfield) True % 4.58/4.77 Clause #15 (by assumption #[]): Eq (∀ (X Y : Iota), And (cat X) (dog Y) → chased Y X → hates (owner_of X) (owner_of Y)) True % 4.58/4.77 Clause #16 (by assumption #[]): Eq (∀ (X Y : Iota), And (human X) (pet Y) → Iff (owner X Y) (Eq X (owner_of Y))) True % 4.58/4.77 Clause #17 (by assumption #[]): Eq (chased odie garfield) True % 4.58/4.77 Clause #18 (by assumption #[]): Eq (Not (hates jon jon)) True % 4.58/4.77 Clause #21 (by clausification #[6]): ∀ (a : Iota), Eq (cat a → pet a) True % 4.58/4.77 Clause #22 (by clausification #[21]): ∀ (a : Iota), Or (Eq (cat a) False) (Eq (pet a) True) % 4.58/4.77 Clause #23 (by superposition #[22, 1]): Or (Eq (pet garfield) True) (Eq False True) % 4.58/4.77 Clause #25 (by clausification #[23]): Eq (pet garfield) True % 4.58/4.77 Clause #26 (by clausification #[5]): ∀ (a : Iota), Eq (dog a → pet a) True % 4.58/4.77 Clause #27 (by clausification #[26]): ∀ (a : Iota), Or (Eq (dog a) False) (Eq (pet a) True) % 4.58/4.77 Clause #28 (by superposition #[27, 3]): Or (Eq (pet odie) True) (Eq False True) % 4.58/4.77 Clause #29 (by clausification #[28]): Eq (pet odie) True % 4.58/4.77 Clause #33 (by clausification #[18]): Eq (hates jon jon) False % 4.58/4.77 Clause #87 (by clausification #[15]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (cat a) (dog Y) → chased Y a → hates (owner_of a) (owner_of Y)) True % 4.58/4.77 Clause #88 (by clausification #[87]): ∀ (a a_1 : Iota), Eq (And (cat a) (dog a_1) → chased a_1 a → hates (owner_of a) (owner_of a_1)) True % 4.58/4.77 Clause #89 (by clausification #[88]): ∀ (a a_1 : Iota), Or (Eq (And (cat a) (dog a_1)) False) (Eq (chased a_1 a → hates (owner_of a) (owner_of a_1)) True) % 4.58/4.77 Clause #90 (by clausification #[89]): ∀ (a a_1 : Iota), % 4.58/4.77 Or (Eq (chased a a_1 → hates (owner_of a_1) (owner_of a)) True) (Or (Eq (cat a_1) False) (Eq (dog a) False)) % 4.58/4.77 Clause #91 (by clausification #[90]): ∀ (a a_1 : Iota), % 4.58/4.77 Or (Eq (cat a) False) % 4.58/4.77 (Or (Eq (dog a_1) False) (Or (Eq (chased a_1 a) False) (Eq (hates (owner_of a) (owner_of a_1)) True))) % 4.58/4.77 Clause #92 (by superposition #[91, 1]): ∀ (a : Iota), % 4.58/4.77 Or (Eq (dog a) False) % 4.58/4.77 (Or (Eq (chased a garfield) False) (Or (Eq (hates (owner_of garfield) (owner_of a)) True) (Eq False True))) % 4.58/4.77 Clause #126 (by clausification #[16]): ∀ (a : Iota), Eq (∀ (Y : Iota), And (human a) (pet Y) → Iff (owner a Y) (Eq a (owner_of Y))) True % 4.58/4.77 Clause #127 (by clausification #[126]): ∀ (a a_1 : Iota), Eq (And (human a) (pet a_1) → Iff (owner a a_1) (Eq a (owner_of a_1))) True % 4.58/4.77 Clause #128 (by clausification #[127]): ∀ (a a_1 : Iota), Or (Eq (And (human a) (pet a_1)) False) (Eq (Iff (owner a a_1) (Eq a (owner_of a_1))) True) % 4.58/4.77 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), Or (Eq (Iff (owner a a_1) (Eq a (owner_of a_1))) True) (Or (Eq (human a) False) (Eq (pet a_1) False)) % 4.58/4.77 Clause #131 (by clausification #[129]): ∀ (a a_1 : Iota), % 4.58/4.77 Or (Eq (human a) False) (Or (Eq (pet a_1) False) (Or (Eq (owner a a_1) False) (Eq (Eq a (owner_of a_1)) True))) % 4.58/4.77 Clause #199 (by clausification #[92]): ∀ (a : Iota), % 4.58/4.77 Or (Eq (dog a) False) (Or (Eq (chased a garfield) False) (Eq (hates (owner_of garfield) (owner_of a)) True)) % 4.58/4.77 Clause #200 (by superposition #[199, 3]): Or (Eq (chased odie garfield) False) (Or (Eq (hates (owner_of garfield) (owner_of odie)) True) (Eq False True)) % 4.58/4.77 Clause #203 (by clausification #[200]): Or (Eq (chased odie garfield) False) (Eq (hates (owner_of garfield) (owner_of odie)) True) % 4.58/4.77 Clause #204 (by forward demodulation #[203, 17]): Or (Eq True False) (Eq (hates (owner_of garfield) (owner_of odie)) True) % 4.58/4.77 Clause #205 (by clausification #[204]): Eq (hates (owner_of garfield) (owner_of odie)) True % 4.58/4.77 Clause #242 (by clausification #[131]): ∀ (a a_1 : Iota), Or (Eq (human a) False) (Or (Eq (pet a_1) False) (Or (Eq (owner a a_1) False) (Eq a (owner_of a_1)))) % 4.58/4.78 Clause #243 (by superposition #[242, 8]): ∀ (a : Iota), Or (Eq (pet a) False) (Or (Eq (owner jon a) False) (Or (Eq jon (owner_of a)) (Eq False True))) % 4.58/4.78 Clause #254 (by clausification #[243]): ∀ (a : Iota), Or (Eq (pet a) False) (Or (Eq (owner jon a) False) (Eq jon (owner_of a))) % 4.58/4.78 Clause #255 (by superposition #[254, 25]): Or (Eq (owner jon garfield) False) (Or (Eq jon (owner_of garfield)) (Eq False True)) % 4.58/4.78 Clause #256 (by superposition #[254, 29]): Or (Eq (owner jon odie) False) (Or (Eq jon (owner_of odie)) (Eq False True)) % 4.58/4.78 Clause #263 (by clausification #[256]): Or (Eq (owner jon odie) False) (Eq jon (owner_of odie)) % 4.58/4.78 Clause #264 (by superposition #[263, 11]): Or (Eq jon (owner_of odie)) (Eq False True) % 4.58/4.78 Clause #265 (by clausification #[264]): Eq jon (owner_of odie) % 4.58/4.78 Clause #266 (by backward demodulation #[265, 205]): Eq (hates (owner_of garfield) jon) True % 4.58/4.78 Clause #269 (by clausification #[255]): Or (Eq (owner jon garfield) False) (Eq jon (owner_of garfield)) % 4.58/4.78 Clause #270 (by superposition #[269, 12]): Or (Eq jon (owner_of garfield)) (Eq False True) % 4.58/4.78 Clause #272 (by clausification #[270]): Eq jon (owner_of garfield) % 4.58/4.78 Clause #274 (by backward demodulation #[272, 266]): Eq (hates jon jon) True % 4.58/4.78 Clause #277 (by superposition #[274, 33]): Eq True False % 4.58/4.78 Clause #278 (by clausification #[277]): False % 4.58/4.78 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------