%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PUZ012_1 : TPTP v9.2.0. Released v5.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n026.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:12 PM UTC 2025 % Result : Theorem 3.52s 3.71s % Output : Proof 3.52s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.12 % Problem : PUZ012_1 : TPTP v9.2.0. Released v5.0.0. % 0.02/0.13 % Command : duper %s % 0.13/0.34 % Computer : n026.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Oct 2 20:45:23 EDT 2025 % 0.13/0.34 % CPUTime : % 3.52/3.71 SZS status Theorem for theBenchmark.p % 3.52/3.71 SZS output start Proof for theBenchmark.p % 3.52/3.71 Clause #2 (by assumption #[]): Eq (∀ (X : box) (Y : fruit), Not (And (label X Y) (contains X Y))) True % 3.52/3.71 Clause #3 (by assumption #[]): Eq (∀ (X : fruit), Or (Or (contains boxa X) (contains boxb X)) (contains boxc X)) True % 3.52/3.71 Clause #4 (by assumption #[]): Eq (∀ (X : box), Or (Or (contains X apples) (contains X bananas)) (contains X oranges)) True % 3.52/3.71 Clause #5 (by assumption #[]): Eq (∀ (X : box) (Y Z : fruit), And (contains X Y) (contains X Z) → equal_fruits Y Z) True % 3.52/3.71 Clause #6 (by assumption #[]): Eq (∀ (X : box) (Y : fruit) (Z : box), And (contains X Y) (contains Z Y) → equal_boxes X Z) True % 3.52/3.71 Clause #8 (by assumption #[]): Eq (Not (equal_boxes boxb boxc)) True % 3.52/3.71 Clause #10 (by assumption #[]): Eq (Not (equal_fruits apples bananas)) True % 3.52/3.71 Clause #15 (by assumption #[]): Eq (label boxc bananas) True % 3.52/3.71 Clause #16 (by assumption #[]): Eq (contains boxb apples) True % 3.52/3.71 Clause #17 (by assumption #[]): Eq (Not (And (contains boxa bananas) (contains boxc oranges))) True % 3.52/3.71 Clause #22 (by clausification #[8]): Eq (equal_boxes boxb boxc) False % 3.52/3.71 Clause #23 (by clausification #[10]): Eq (equal_fruits apples bananas) False % 3.52/3.71 Clause #26 (by clausification #[5]): ∀ (a : box), Eq (∀ (Y Z : fruit), And (contains a Y) (contains a Z) → equal_fruits Y Z) True % 3.52/3.71 Clause #27 (by clausification #[26]): ∀ (a : box) (a_1 : fruit), Eq (∀ (Z : fruit), And (contains a a_1) (contains a Z) → equal_fruits a_1 Z) True % 3.52/3.71 Clause #28 (by clausification #[27]): ∀ (a : box) (a_1 a_2 : fruit), Eq (And (contains a a_1) (contains a a_2) → equal_fruits a_1 a_2) True % 3.52/3.71 Clause #29 (by clausification #[28]): ∀ (a : box) (a_1 a_2 : fruit), Or (Eq (And (contains a a_1) (contains a a_2)) False) (Eq (equal_fruits a_1 a_2) True) % 3.52/3.71 Clause #30 (by clausification #[29]): ∀ (a a_1 : fruit) (a_2 : box), % 3.52/3.71 Or (Eq (equal_fruits a a_1) True) (Or (Eq (contains a_2 a) False) (Eq (contains a_2 a_1) False)) % 3.52/3.71 Clause #31 (by superposition #[30, 16]): ∀ (a : fruit), Or (Eq (equal_fruits apples a) True) (Or (Eq (contains boxb a) False) (Eq False True)) % 3.52/3.71 Clause #32 (by clausification #[6]): ∀ (a : box), Eq (∀ (Y : fruit) (Z : box), And (contains a Y) (contains Z Y) → equal_boxes a Z) True % 3.52/3.71 Clause #33 (by clausification #[32]): ∀ (a : box) (a_1 : fruit), Eq (∀ (Z : box), And (contains a a_1) (contains Z a_1) → equal_boxes a Z) True % 3.52/3.71 Clause #34 (by clausification #[33]): ∀ (a : box) (a_1 : fruit) (a_2 : box), Eq (And (contains a a_1) (contains a_2 a_1) → equal_boxes a a_2) True % 3.52/3.71 Clause #35 (by clausification #[34]): ∀ (a : box) (a_1 : fruit) (a_2 : box), % 3.52/3.71 Or (Eq (And (contains a a_1) (contains a_2 a_1)) False) (Eq (equal_boxes a a_2) True) % 3.52/3.71 Clause #36 (by clausification #[35]): ∀ (a a_1 : box) (a_2 : fruit), % 3.52/3.71 Or (Eq (equal_boxes a a_1) True) (Or (Eq (contains a a_2) False) (Eq (contains a_1 a_2) False)) % 3.52/3.71 Clause #37 (by superposition #[36, 16]): ∀ (a : box), Or (Eq (equal_boxes boxb a) True) (Or (Eq (contains a apples) False) (Eq False True)) % 3.52/3.71 Clause #38 (by clausification #[17]): Eq (And (contains boxa bananas) (contains boxc oranges)) False % 3.52/3.71 Clause #39 (by clausification #[38]): Or (Eq (contains boxa bananas) False) (Eq (contains boxc oranges) False) % 3.52/3.71 Clause #40 (by clausification #[37]): ∀ (a : box), Or (Eq (equal_boxes boxb a) True) (Eq (contains a apples) False) % 3.52/3.71 Clause #43 (by clausification #[2]): ∀ (a : box), Eq (∀ (Y : fruit), Not (And (label a Y) (contains a Y))) True % 3.52/3.71 Clause #44 (by clausification #[43]): ∀ (a : box) (a_1 : fruit), Eq (Not (And (label a a_1) (contains a a_1))) True % 3.52/3.71 Clause #45 (by clausification #[44]): ∀ (a : box) (a_1 : fruit), Eq (And (label a a_1) (contains a a_1)) False % 3.52/3.71 Clause #46 (by clausification #[45]): ∀ (a : box) (a_1 : fruit), Or (Eq (label a a_1) False) (Eq (contains a a_1) False) % 3.52/3.71 Clause #47 (by superposition #[46, 15]): Or (Eq (contains boxc bananas) False) (Eq False True) % 3.52/3.71 Clause #52 (by clausification #[47]): Eq (contains boxc bananas) False % 3.52/3.71 Clause #53 (by clausification #[31]): ∀ (a : fruit), Or (Eq (equal_fruits apples a) True) (Eq (contains boxb a) False) % 3.52/3.72 Clause #56 (by clausification #[3]): ∀ (a : fruit), Eq (Or (Or (contains boxa a) (contains boxb a)) (contains boxc a)) True % 3.52/3.72 Clause #57 (by clausification #[56]): ∀ (a : fruit), Or (Eq (Or (contains boxa a) (contains boxb a)) True) (Eq (contains boxc a) True) % 3.52/3.72 Clause #58 (by clausification #[57]): ∀ (a : fruit), Or (Eq (contains boxc a) True) (Or (Eq (contains boxa a) True) (Eq (contains boxb a) True)) % 3.52/3.72 Clause #59 (by superposition #[58, 39]): Or (Eq (contains boxc bananas) True) % 3.52/3.72 (Or (Eq (contains boxb bananas) True) (Or (Eq True False) (Eq (contains boxc oranges) False))) % 3.52/3.72 Clause #65 (by clausification #[4]): ∀ (a : box), Eq (Or (Or (contains a apples) (contains a bananas)) (contains a oranges)) True % 3.52/3.72 Clause #66 (by clausification #[65]): ∀ (a : box), Or (Eq (Or (contains a apples) (contains a bananas)) True) (Eq (contains a oranges) True) % 3.52/3.72 Clause #67 (by clausification #[66]): ∀ (a : box), Or (Eq (contains a oranges) True) (Or (Eq (contains a apples) True) (Eq (contains a bananas) True)) % 3.52/3.72 Clause #69 (by superposition #[67, 40]): ∀ (a : box), % 3.52/3.72 Or (Eq (contains a oranges) True) % 3.52/3.72 (Or (Eq (contains a bananas) True) (Or (Eq (equal_boxes boxb a) True) (Eq True False))) % 3.52/3.72 Clause #78 (by clausification #[59]): Or (Eq (contains boxc bananas) True) (Or (Eq (contains boxb bananas) True) (Eq (contains boxc oranges) False)) % 3.52/3.72 Clause #79 (by forward demodulation #[78, 52]): Or (Eq False True) (Or (Eq (contains boxb bananas) True) (Eq (contains boxc oranges) False)) % 3.52/3.72 Clause #80 (by clausification #[79]): Or (Eq (contains boxb bananas) True) (Eq (contains boxc oranges) False) % 3.52/3.72 Clause #101 (by clausification #[69]): ∀ (a : box), Or (Eq (contains a oranges) True) (Or (Eq (contains a bananas) True) (Eq (equal_boxes boxb a) True)) % 3.52/3.72 Clause #102 (by superposition #[101, 22]): Or (Eq (contains boxc oranges) True) (Or (Eq (contains boxc bananas) True) (Eq True False)) % 3.52/3.72 Clause #103 (by clausification #[102]): Or (Eq (contains boxc oranges) True) (Eq (contains boxc bananas) True) % 3.52/3.72 Clause #104 (by superposition #[103, 52]): Or (Eq (contains boxc oranges) True) (Eq True False) % 3.52/3.72 Clause #108 (by clausification #[104]): Eq (contains boxc oranges) True % 3.52/3.72 Clause #111 (by backward demodulation #[108, 80]): Or (Eq (contains boxb bananas) True) (Eq True False) % 3.52/3.72 Clause #115 (by clausification #[111]): Eq (contains boxb bananas) True % 3.52/3.72 Clause #117 (by superposition #[115, 53]): Or (Eq (equal_fruits apples bananas) True) (Eq True False) % 3.52/3.72 Clause #127 (by clausification #[117]): Eq (equal_fruits apples bananas) True % 3.52/3.72 Clause #128 (by superposition #[127, 23]): Eq True False % 3.52/3.72 Clause #129 (by clausification #[128]): False % 3.52/3.72 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------