%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ005+1 : TPTP v9.2.0. Released v2.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n014.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:11 PM UTC 2025 % Result : Theorem 36.07s 36.36s % Output : Proof 36.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.23 % Problem : PUZ005+1 : TPTP v9.2.0. Released v2.2.0. % 0.12/0.24 % Command : duper %s % 0.12/0.45 % Computer : n014.cluster.edu % 0.12/0.45 % Model : x86_64 x86_64 % 0.12/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.45 % Memory : 8042.1875MB % 0.12/0.45 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.45 % CPULimit : 300 % 0.12/0.45 % WCLimit : 300 % 0.12/0.45 % DateTime : Thu Oct 2 20:48:38 EDT 2025 % 0.12/0.45 % CPUTime : % 36.07/36.36 SZS status Theorem for theBenchmark.p % 36.07/36.36 SZS output start Proof for theBenchmark.p % 36.07/36.36 Clause #3 (by assumption #[]): Eq (thursday a_thursday) True % 36.07/36.36 Clause #9 (by assumption #[]): Eq (∀ (X : Iota), wednesday X → day X) True % 36.07/36.36 Clause #10 (by assumption #[]): Eq (∀ (X : Iota), thursday X → day X) True % 36.07/36.36 Clause #17 (by assumption #[]): Eq (∀ (X : Iota), thursday X → wednesday (yesterday X)) True % 36.07/36.36 Clause #23 (by assumption #[]): Eq (∀ (X : Iota), wednesday X → lion_lies X) True % 36.07/36.36 Clause #24 (by assumption #[]): Eq (∀ (X : Iota), thursday X → Not (lion_lies X)) True % 36.07/36.36 Clause #30 (by assumption #[]): Eq (∀ (X : Iota), wednesday X → Not (unicorn_lies X)) True % 36.07/36.36 Clause #31 (by assumption #[]): Eq (∀ (X : Iota), thursday X → unicorn_lies X) True % 36.07/36.36 Clause #39 (by assumption #[]): Eq % 36.07/36.36 (∀ (X : Iota), % 36.07/36.36 day X → ∀ (Y : Iota), day Y → And (Not (lion_lies X)) (Not (lies_on_one_of a_lion X Y)) → Not (lion_lies Y)) % 36.07/36.36 True % 36.07/36.36 Clause #44 (by assumption #[]): Eq % 36.07/36.36 (∀ (X : Iota), % 36.07/36.36 day X → ∀ (Y : Iota), day Y → And (unicorn_lies X) (Not (lies_on_one_of a_unicorn X Y)) → unicorn_lies Y) % 36.07/36.36 True % 36.07/36.36 Clause #45 (by assumption #[]): Eq % 36.07/36.36 (Not % 36.07/36.36 (Exists fun X => % 36.07/36.36 And (And (day X) (lies_on_one_of a_lion X (yesterday X))) (lies_on_one_of a_unicorn X (yesterday X)))) % 36.07/36.36 True % 36.07/36.36 Clause #50 (by clausification #[31]): ∀ (a : Iota), Eq (thursday a → unicorn_lies a) True % 36.07/36.36 Clause #51 (by clausification #[50]): ∀ (a : Iota), Or (Eq (thursday a) False) (Eq (unicorn_lies a) True) % 36.07/36.36 Clause #52 (by superposition #[51, 3]): Or (Eq (unicorn_lies a_thursday) True) (Eq False True) % 36.07/36.36 Clause #53 (by clausification #[52]): Eq (unicorn_lies a_thursday) True % 36.07/36.36 Clause #66 (by clausification #[9]): ∀ (a : Iota), Eq (wednesday a → day a) True % 36.07/36.36 Clause #67 (by clausification #[66]): ∀ (a : Iota), Or (Eq (wednesday a) False) (Eq (day a) True) % 36.07/36.36 Clause #70 (by clausification #[23]): ∀ (a : Iota), Eq (wednesday a → lion_lies a) True % 36.07/36.36 Clause #71 (by clausification #[70]): ∀ (a : Iota), Or (Eq (wednesday a) False) (Eq (lion_lies a) True) % 36.07/36.36 Clause #78 (by clausification #[10]): ∀ (a : Iota), Eq (thursday a → day a) True % 36.07/36.36 Clause #79 (by clausification #[78]): ∀ (a : Iota), Or (Eq (thursday a) False) (Eq (day a) True) % 36.07/36.36 Clause #80 (by superposition #[79, 3]): Or (Eq (day a_thursday) True) (Eq False True) % 36.07/36.36 Clause #81 (by clausification #[80]): Eq (day a_thursday) True % 36.07/36.36 Clause #129 (by clausification #[17]): ∀ (a : Iota), Eq (thursday a → wednesday (yesterday a)) True % 36.07/36.36 Clause #130 (by clausification #[129]): ∀ (a : Iota), Or (Eq (thursday a) False) (Eq (wednesday (yesterday a)) True) % 36.07/36.36 Clause #131 (by superposition #[130, 3]): Or (Eq (wednesday (yesterday a_thursday)) True) (Eq False True) % 36.07/36.36 Clause #132 (by clausification #[131]): Eq (wednesday (yesterday a_thursday)) True % 36.07/36.36 Clause #133 (by superposition #[132, 67]): Or (Eq True False) (Eq (day (yesterday a_thursday)) True) % 36.07/36.36 Clause #134 (by superposition #[132, 71]): Or (Eq True False) (Eq (lion_lies (yesterday a_thursday)) True) % 36.07/36.36 Clause #136 (by clausification #[134]): Eq (lion_lies (yesterday a_thursday)) True % 36.07/36.36 Clause #137 (by clausification #[133]): Eq (day (yesterday a_thursday)) True % 36.07/36.36 Clause #152 (by clausification #[30]): ∀ (a : Iota), Eq (wednesday a → Not (unicorn_lies a)) True % 36.07/36.36 Clause #153 (by clausification #[152]): ∀ (a : Iota), Or (Eq (wednesday a) False) (Eq (Not (unicorn_lies a)) True) % 36.07/36.36 Clause #154 (by clausification #[153]): ∀ (a : Iota), Or (Eq (wednesday a) False) (Eq (unicorn_lies a) False) % 36.07/36.36 Clause #156 (by superposition #[154, 132]): Or (Eq (unicorn_lies (yesterday a_thursday)) False) (Eq False True) % 36.07/36.36 Clause #161 (by clausification #[156]): Eq (unicorn_lies (yesterday a_thursday)) False % 36.07/36.36 Clause #171 (by clausification #[24]): ∀ (a : Iota), Eq (thursday a → Not (lion_lies a)) True % 36.07/36.36 Clause #172 (by clausification #[171]): ∀ (a : Iota), Or (Eq (thursday a) False) (Eq (Not (lion_lies a)) True) % 36.07/36.36 Clause #173 (by clausification #[172]): ∀ (a : Iota), Or (Eq (thursday a) False) (Eq (lion_lies a) False) % 36.07/36.36 Clause #174 (by superposition #[173, 3]): Or (Eq (lion_lies a_thursday) False) (Eq False True) % 36.08/36.38 Clause #176 (by clausification #[174]): Eq (lion_lies a_thursday) False % 36.08/36.38 Clause #292 (by clausification #[39]): ∀ (a : Iota), % 36.08/36.38 Eq (day a → ∀ (Y : Iota), day Y → And (Not (lion_lies a)) (Not (lies_on_one_of a_lion a Y)) → Not (lion_lies Y)) True % 36.08/36.38 Clause #293 (by clausification #[292]): ∀ (a : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Eq (∀ (Y : Iota), day Y → And (Not (lion_lies a)) (Not (lies_on_one_of a_lion a Y)) → Not (lion_lies Y)) True) % 36.08/36.38 Clause #294 (by clausification #[293]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Eq (day a_1 → And (Not (lion_lies a)) (Not (lies_on_one_of a_lion a a_1)) → Not (lion_lies a_1)) True) % 36.08/36.38 Clause #295 (by clausification #[294]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Eq (And (Not (lion_lies a)) (Not (lies_on_one_of a_lion a a_1)) → Not (lion_lies a_1)) True)) % 36.08/36.38 Clause #296 (by clausification #[295]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Or (Eq (And (Not (lion_lies a)) (Not (lies_on_one_of a_lion a a_1))) False) (Eq (Not (lion_lies a_1)) True))) % 36.08/36.38 Clause #297 (by clausification #[296]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Or (Eq (Not (lion_lies a_1)) True) % 36.08/36.38 (Or (Eq (Not (lion_lies a)) False) (Eq (Not (lies_on_one_of a_lion a a_1)) False)))) % 36.08/36.38 Clause #298 (by clausification #[297]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Or (Eq (Not (lion_lies a)) False) % 36.08/36.38 (Or (Eq (Not (lies_on_one_of a_lion a a_1)) False) (Eq (lion_lies a_1) False)))) % 36.08/36.38 Clause #299 (by clausification #[298]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Or (Eq (Not (lies_on_one_of a_lion a a_1)) False) (Or (Eq (lion_lies a_1) False) (Eq (lion_lies a) True)))) % 36.08/36.38 Clause #300 (by clausification #[299]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Or (Eq (lion_lies a_1) False) (Or (Eq (lion_lies a) True) (Eq (lies_on_one_of a_lion a a_1) True)))) % 36.08/36.38 Clause #306 (by superposition #[300, 81]): ∀ (a : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (lion_lies a) False) % 36.08/36.38 (Or (Eq (lion_lies a_thursday) True) (Or (Eq (lies_on_one_of a_lion a_thursday a) True) (Eq False True)))) % 36.08/36.38 Clause #507 (by clausification #[44]): ∀ (a : Iota), % 36.08/36.38 Eq (day a → ∀ (Y : Iota), day Y → And (unicorn_lies a) (Not (lies_on_one_of a_unicorn a Y)) → unicorn_lies Y) True % 36.08/36.38 Clause #508 (by clausification #[507]): ∀ (a : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Eq (∀ (Y : Iota), day Y → And (unicorn_lies a) (Not (lies_on_one_of a_unicorn a Y)) → unicorn_lies Y) True) % 36.08/36.38 Clause #509 (by clausification #[508]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Eq (day a_1 → And (unicorn_lies a) (Not (lies_on_one_of a_unicorn a a_1)) → unicorn_lies a_1) True) % 36.08/36.38 Clause #510 (by clausification #[509]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) (Eq (And (unicorn_lies a) (Not (lies_on_one_of a_unicorn a a_1)) → unicorn_lies a_1) True)) % 36.08/36.38 Clause #511 (by clausification #[510]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Or (Eq (And (unicorn_lies a) (Not (lies_on_one_of a_unicorn a a_1))) False) (Eq (unicorn_lies a_1) True))) % 36.08/36.38 Clause #512 (by clausification #[511]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Or (Eq (unicorn_lies a_1) True) % 36.08/36.38 (Or (Eq (unicorn_lies a) False) (Eq (Not (lies_on_one_of a_unicorn a a_1)) False)))) % 36.08/36.38 Clause #513 (by clausification #[512]): ∀ (a a_1 : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (day a_1) False) % 36.08/36.38 (Or (Eq (unicorn_lies a_1) True) (Or (Eq (unicorn_lies a) False) (Eq (lies_on_one_of a_unicorn a a_1) True)))) % 36.08/36.38 Clause #519 (by superposition #[513, 81]): ∀ (a : Iota), % 36.08/36.38 Or (Eq (day a) False) % 36.08/36.38 (Or (Eq (unicorn_lies a) True) % 36.08/36.38 (Or (Eq (unicorn_lies a_thursday) False) (Or (Eq (lies_on_one_of a_unicorn a_thursday a) True) (Eq False True)))) % 36.08/36.38 Clause #558 (by clausification #[45]): Eq % 36.08/36.38 (Exists fun X => And (And (day X) (lies_on_one_of a_lion X (yesterday X))) (lies_on_one_of a_unicorn X (yesterday X))) % 36.12/36.42 False % 36.12/36.42 Clause #559 (by clausification #[558]): ∀ (a : Iota), % 36.12/36.42 Eq (And (And (day a) (lies_on_one_of a_lion a (yesterday a))) (lies_on_one_of a_unicorn a (yesterday a))) False % 36.12/36.42 Clause #560 (by clausification #[559]): ∀ (a : Iota), % 36.12/36.42 Or (Eq (And (day a) (lies_on_one_of a_lion a (yesterday a))) False) % 36.12/36.42 (Eq (lies_on_one_of a_unicorn a (yesterday a)) False) % 36.12/36.42 Clause #561 (by clausification #[560]): ∀ (a : Iota), % 36.12/36.42 Or (Eq (lies_on_one_of a_unicorn a (yesterday a)) False) % 36.12/36.42 (Or (Eq (day a) False) (Eq (lies_on_one_of a_lion a (yesterday a)) False)) % 36.12/36.42 Clause #2202 (by clausification #[306]): ∀ (a : Iota), % 36.12/36.42 Or (Eq (day a) False) % 36.12/36.42 (Or (Eq (lion_lies a) False) (Or (Eq (lion_lies a_thursday) True) (Eq (lies_on_one_of a_lion a_thursday a) True))) % 36.12/36.42 Clause #2203 (by forward demodulation #[2202, 176]): ∀ (a : Iota), % 36.12/36.42 Or (Eq (day a) False) % 36.12/36.42 (Or (Eq (lion_lies a) False) (Or (Eq False True) (Eq (lies_on_one_of a_lion a_thursday a) True))) % 36.12/36.42 Clause #2204 (by clausification #[2203]): ∀ (a : Iota), Or (Eq (day a) False) (Or (Eq (lion_lies a) False) (Eq (lies_on_one_of a_lion a_thursday a) True)) % 36.12/36.42 Clause #2213 (by superposition #[2204, 137]): Or (Eq (lion_lies (yesterday a_thursday)) False) % 36.12/36.42 (Or (Eq (lies_on_one_of a_lion a_thursday (yesterday a_thursday)) True) (Eq False True)) % 36.12/36.42 Clause #7101 (by clausification #[2213]): Or (Eq (lion_lies (yesterday a_thursday)) False) (Eq (lies_on_one_of a_lion a_thursday (yesterday a_thursday)) True) % 36.12/36.42 Clause #7102 (by forward demodulation #[7101, 136]): Or (Eq True False) (Eq (lies_on_one_of a_lion a_thursday (yesterday a_thursday)) True) % 36.12/36.42 Clause #7103 (by clausification #[7102]): Eq (lies_on_one_of a_lion a_thursday (yesterday a_thursday)) True % 36.12/36.42 Clause #7912 (by clausification #[519]): ∀ (a : Iota), % 36.12/36.42 Or (Eq (day a) False) % 36.12/36.42 (Or (Eq (unicorn_lies a) True) % 36.12/36.42 (Or (Eq (unicorn_lies a_thursday) False) (Eq (lies_on_one_of a_unicorn a_thursday a) True))) % 36.12/36.42 Clause #7913 (by forward demodulation #[7912, 53]): ∀ (a : Iota), % 36.12/36.42 Or (Eq (day a) False) % 36.12/36.42 (Or (Eq (unicorn_lies a) True) (Or (Eq True False) (Eq (lies_on_one_of a_unicorn a_thursday a) True))) % 36.12/36.42 Clause #7914 (by clausification #[7913]): ∀ (a : Iota), Or (Eq (day a) False) (Or (Eq (unicorn_lies a) True) (Eq (lies_on_one_of a_unicorn a_thursday a) True)) % 36.12/36.42 Clause #7923 (by superposition #[7914, 137]): Or (Eq (unicorn_lies (yesterday a_thursday)) True) % 36.12/36.42 (Or (Eq (lies_on_one_of a_unicorn a_thursday (yesterday a_thursday)) True) (Eq False True)) % 36.12/36.42 Clause #8394 (by clausification #[7923]): Or (Eq (unicorn_lies (yesterday a_thursday)) True) % 36.12/36.42 (Eq (lies_on_one_of a_unicorn a_thursday (yesterday a_thursday)) True) % 36.12/36.42 Clause #8395 (by forward demodulation #[8394, 161]): Or (Eq False True) (Eq (lies_on_one_of a_unicorn a_thursday (yesterday a_thursday)) True) % 36.12/36.42 Clause #8396 (by clausification #[8395]): Eq (lies_on_one_of a_unicorn a_thursday (yesterday a_thursday)) True % 36.12/36.42 Clause #8397 (by superposition #[8396, 561]): Or (Eq True False) (Or (Eq (day a_thursday) False) (Eq (lies_on_one_of a_lion a_thursday (yesterday a_thursday)) False)) % 36.12/36.42 Clause #8398 (by clausification #[8397]): Or (Eq (day a_thursday) False) (Eq (lies_on_one_of a_lion a_thursday (yesterday a_thursday)) False) % 36.12/36.42 Clause #8399 (by forward demodulation #[8398, 81]): Or (Eq True False) (Eq (lies_on_one_of a_lion a_thursday (yesterday a_thursday)) False) % 36.12/36.42 Clause #8400 (by clausification #[8399]): Eq (lies_on_one_of a_lion a_thursday (yesterday a_thursday)) False % 36.12/36.42 Clause #8401 (by superposition #[8400, 7103]): Eq False True % 36.12/36.42 Clause #8402 (by clausification #[8401]): False % 36.12/36.42 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------