%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : PHI013+1 : TPTP v9.2.0. Released v7.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n019.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:57:56 PM UTC 2025 % Result : Theorem 3.99s 4.14s % Output : Proof 4.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PHI013+1 : TPTP v9.2.0. Released v7.2.0. % 0.13/0.13 % Command : duper %s % 0.14/0.34 % Computer : n019.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Fri Oct 3 09:06:53 EDT 2025 % 0.14/0.34 % CPUTime : % 3.99/4.14 SZS status Theorem for theBenchmark.p % 3.99/4.14 SZS output start Proof for theBenchmark.p % 3.99/4.14 Clause #1 (by assumption #[]): Eq % 3.99/4.14 (∀ (F : Iota), % 3.99/4.14 property F → % 3.99/4.14 (Exists fun Y => And (object Y) (is_the Y F)) → ∀ (Z : Iota), object Z → is_the Z F → exemplifies_property F Z) % 3.99/4.14 True % 3.99/4.14 Clause #2 (by assumption #[]): Eq (∀ (X F : Iota), is_the X F → And (property F) (object X)) True % 3.99/4.14 Clause #3 (by assumption #[]): Eq % 3.99/4.14 (∀ (X : Iota), % 3.99/4.14 object X → % 3.99/4.14 Iff (exemplifies_property none_greater X) % 3.99/4.14 (And (exemplifies_property conceivable X) % 3.99/4.14 (Not % 3.99/4.14 (Exists fun Y => % 3.99/4.14 And (And (object Y) (exemplifies_relation greater_than Y X)) (exemplifies_property conceivable Y))))) % 3.99/4.14 True % 3.99/4.14 Clause #6 (by assumption #[]): Eq % 3.99/4.14 (∀ (X : Iota), % 3.99/4.14 object X → % 3.99/4.14 And (is_the X none_greater) (Not (exemplifies_property existence X)) → % 3.99/4.14 Exists fun Y => % 3.99/4.14 And (And (object Y) (exemplifies_relation greater_than Y X)) (exemplifies_property conceivable Y)) % 3.99/4.14 True % 3.99/4.14 Clause #7 (by assumption #[]): Eq (is_the god none_greater) True % 3.99/4.14 Clause #8 (by assumption #[]): Eq (Not (exemplifies_property existence god)) True % 3.99/4.14 Clause #9 (by clausification #[8]): Eq (exemplifies_property existence god) False % 3.99/4.14 Clause #10 (by clausification #[2]): ∀ (a : Iota), Eq (∀ (F : Iota), is_the a F → And (property F) (object a)) True % 3.99/4.14 Clause #11 (by clausification #[10]): ∀ (a a_1 : Iota), Eq (is_the a a_1 → And (property a_1) (object a)) True % 3.99/4.14 Clause #12 (by clausification #[11]): ∀ (a a_1 : Iota), Or (Eq (is_the a a_1) False) (Eq (And (property a_1) (object a)) True) % 3.99/4.14 Clause #13 (by clausification #[12]): ∀ (a a_1 : Iota), Or (Eq (is_the a a_1) False) (Eq (object a) True) % 3.99/4.14 Clause #14 (by clausification #[12]): ∀ (a a_1 : Iota), Or (Eq (is_the a a_1) False) (Eq (property a_1) True) % 3.99/4.14 Clause #15 (by superposition #[13, 7]): Or (Eq (object god) True) (Eq False True) % 3.99/4.14 Clause #16 (by clausification #[15]): Eq (object god) True % 3.99/4.14 Clause #17 (by superposition #[14, 7]): Or (Eq (property none_greater) True) (Eq False True) % 3.99/4.14 Clause #31 (by clausification #[17]): Eq (property none_greater) True % 3.99/4.14 Clause #36 (by clausification #[1]): ∀ (a : Iota), % 3.99/4.14 Eq % 3.99/4.14 (property a → % 3.99/4.14 (Exists fun Y => And (object Y) (is_the Y a)) → ∀ (Z : Iota), object Z → is_the Z a → exemplifies_property a Z) % 3.99/4.14 True % 3.99/4.14 Clause #37 (by clausification #[36]): ∀ (a : Iota), % 3.99/4.14 Or (Eq (property a) False) % 3.99/4.14 (Eq ((Exists fun Y => And (object Y) (is_the Y a)) → ∀ (Z : Iota), object Z → is_the Z a → exemplifies_property a Z) % 3.99/4.14 True) % 3.99/4.14 Clause #38 (by clausification #[37]): ∀ (a : Iota), % 3.99/4.14 Or (Eq (property a) False) % 3.99/4.14 (Or (Eq (Exists fun Y => And (object Y) (is_the Y a)) False) % 3.99/4.14 (Eq (∀ (Z : Iota), object Z → is_the Z a → exemplifies_property a Z) True)) % 3.99/4.14 Clause #39 (by clausification #[38]): ∀ (a a_1 : Iota), % 3.99/4.14 Or (Eq (property a) False) % 3.99/4.14 (Or (Eq (∀ (Z : Iota), object Z → is_the Z a → exemplifies_property a Z) True) % 3.99/4.14 (Eq (And (object a_1) (is_the a_1 a)) False)) % 3.99/4.14 Clause #40 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 3.99/4.14 Or (Eq (property a) False) % 3.99/4.14 (Or (Eq (And (object a_1) (is_the a_1 a)) False) (Eq (object a_2 → is_the a_2 a → exemplifies_property a a_2) True)) % 3.99/4.14 Clause #41 (by clausification #[40]): ∀ (a a_1 a_2 : Iota), % 3.99/4.14 Or (Eq (property a) False) % 3.99/4.14 (Or (Eq (object a_1 → is_the a_1 a → exemplifies_property a a_1) True) % 3.99/4.14 (Or (Eq (object a_2) False) (Eq (is_the a_2 a) False))) % 3.99/4.14 Clause #42 (by clausification #[41]): ∀ (a a_1 a_2 : Iota), % 3.99/4.14 Or (Eq (property a) False) % 3.99/4.14 (Or (Eq (object a_1) False) % 3.99/4.14 (Or (Eq (is_the a_1 a) False) (Or (Eq (object a_2) False) (Eq (is_the a_2 a → exemplifies_property a a_2) True)))) % 3.99/4.14 Clause #43 (by clausification #[42]): ∀ (a a_1 a_2 : Iota), % 3.99/4.14 Or (Eq (property a) False) % 3.99/4.14 (Or (Eq (object a_1) False) % 3.99/4.14 (Or (Eq (is_the a_1 a) False) % 3.99/4.14 (Or (Eq (object a_2) False) (Or (Eq (is_the a_2 a) False) (Eq (exemplifies_property a a_2) True))))) % 3.99/4.14 Clause #44 (by superposition #[43, 31]): ∀ (a a_1 : Iota), % 3.99/4.14 Or (Eq (object a) False) % 3.99/4.14 (Or (Eq (is_the a none_greater) False) % 3.99/4.16 (Or (Eq (object a_1) False) % 3.99/4.16 (Or (Eq (is_the a_1 none_greater) False) % 3.99/4.16 (Or (Eq (exemplifies_property none_greater a_1) True) (Eq False True))))) % 3.99/4.16 Clause #45 (by clausification #[6]): ∀ (a : Iota), % 3.99/4.16 Eq % 3.99/4.16 (object a → % 3.99/4.16 And (is_the a none_greater) (Not (exemplifies_property existence a)) → % 3.99/4.16 Exists fun Y => % 3.99/4.16 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y)) % 3.99/4.16 True % 3.99/4.16 Clause #46 (by clausification #[45]): ∀ (a : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Eq % 3.99/4.16 (And (is_the a none_greater) (Not (exemplifies_property existence a)) → % 3.99/4.16 Exists fun Y => % 3.99/4.16 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y)) % 3.99/4.16 True) % 3.99/4.16 Clause #47 (by clausification #[46]): ∀ (a : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Or (Eq (And (is_the a none_greater) (Not (exemplifies_property existence a))) False) % 3.99/4.16 (Eq % 3.99/4.16 (Exists fun Y => % 3.99/4.16 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y)) % 3.99/4.16 True)) % 3.99/4.16 Clause #48 (by clausification #[47]): ∀ (a : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Or % 3.99/4.16 (Eq % 3.99/4.16 (Exists fun Y => % 3.99/4.16 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y)) % 3.99/4.16 True) % 3.99/4.16 (Or (Eq (is_the a none_greater) False) (Eq (Not (exemplifies_property existence a)) False))) % 3.99/4.16 Clause #49 (by clausification #[48]): ∀ (a a_1 : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Or (Eq (is_the a none_greater) False) % 3.99/4.16 (Or (Eq (Not (exemplifies_property existence a)) False) % 3.99/4.16 (Eq % 3.99/4.16 (And (And (object (skS.0 3 a a_1)) (exemplifies_relation greater_than (skS.0 3 a a_1) a)) % 3.99/4.16 (exemplifies_property conceivable (skS.0 3 a a_1))) % 3.99/4.16 True))) % 3.99/4.16 Clause #50 (by clausification #[49]): ∀ (a a_1 : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Or (Eq (is_the a none_greater) False) % 3.99/4.16 (Or % 3.99/4.16 (Eq % 3.99/4.16 (And (And (object (skS.0 3 a a_1)) (exemplifies_relation greater_than (skS.0 3 a a_1) a)) % 3.99/4.16 (exemplifies_property conceivable (skS.0 3 a a_1))) % 3.99/4.16 True) % 3.99/4.16 (Eq (exemplifies_property existence a) True))) % 3.99/4.16 Clause #51 (by clausification #[50]): ∀ (a a_1 : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Or (Eq (is_the a none_greater) False) % 3.99/4.16 (Or (Eq (exemplifies_property existence a) True) (Eq (exemplifies_property conceivable (skS.0 3 a a_1)) True))) % 3.99/4.16 Clause #52 (by clausification #[50]): ∀ (a a_1 : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Or (Eq (is_the a none_greater) False) % 3.99/4.16 (Or (Eq (exemplifies_property existence a) True) % 3.99/4.16 (Eq (And (object (skS.0 3 a a_1)) (exemplifies_relation greater_than (skS.0 3 a a_1) a)) True))) % 3.99/4.16 Clause #53 (by superposition #[51, 16]): ∀ (a : Iota), % 3.99/4.16 Or (Eq (is_the god none_greater) False) % 3.99/4.16 (Or (Eq (exemplifies_property existence god) True) % 3.99/4.16 (Or (Eq (exemplifies_property conceivable (skS.0 3 god a)) True) (Eq False True))) % 3.99/4.16 Clause #55 (by clausification #[3]): ∀ (a : Iota), % 3.99/4.16 Eq % 3.99/4.16 (object a → % 3.99/4.16 Iff (exemplifies_property none_greater a) % 3.99/4.16 (And (exemplifies_property conceivable a) % 3.99/4.16 (Not % 3.99/4.16 (Exists fun Y => % 3.99/4.16 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y))))) % 3.99/4.16 True % 3.99/4.16 Clause #56 (by clausification #[55]): ∀ (a : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Eq % 3.99/4.16 (Iff (exemplifies_property none_greater a) % 3.99/4.16 (And (exemplifies_property conceivable a) % 3.99/4.16 (Not % 3.99/4.16 (Exists fun Y => % 3.99/4.16 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y))))) % 3.99/4.16 True) % 3.99/4.16 Clause #58 (by clausification #[56]): ∀ (a : Iota), % 3.99/4.16 Or (Eq (object a) False) % 3.99/4.16 (Or (Eq (exemplifies_property none_greater a) False) % 3.99/4.16 (Eq % 3.99/4.16 (And (exemplifies_property conceivable a) % 3.99/4.16 (Not % 3.99/4.16 (Exists fun Y => % 3.99/4.16 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y)))) % 3.99/4.16 True)) % 4.02/4.18 Clause #79 (by clausification #[44]): ∀ (a a_1 : Iota), % 4.02/4.18 Or (Eq (object a) False) % 4.02/4.18 (Or (Eq (is_the a none_greater) False) % 4.02/4.18 (Or (Eq (object a_1) False) % 4.02/4.18 (Or (Eq (is_the a_1 none_greater) False) (Eq (exemplifies_property none_greater a_1) True)))) % 4.02/4.18 Clause #80 (by superposition #[79, 16]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (is_the god none_greater) False) % 4.02/4.18 (Or (Eq (object a) False) % 4.02/4.18 (Or (Eq (is_the a none_greater) False) (Or (Eq (exemplifies_property none_greater a) True) (Eq False True)))) % 4.02/4.18 Clause #82 (by clausification #[80]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (is_the god none_greater) False) % 4.02/4.18 (Or (Eq (object a) False) (Or (Eq (is_the a none_greater) False) (Eq (exemplifies_property none_greater a) True))) % 4.02/4.18 Clause #83 (by superposition #[82, 7]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (object a) False) % 4.02/4.18 (Or (Eq (is_the a none_greater) False) (Or (Eq (exemplifies_property none_greater a) True) (Eq False True))) % 4.02/4.18 Clause #84 (by clausification #[83]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (object a) False) (Or (Eq (is_the a none_greater) False) (Eq (exemplifies_property none_greater a) True)) % 4.02/4.18 Clause #85 (by superposition #[84, 16]): Or (Eq (is_the god none_greater) False) (Or (Eq (exemplifies_property none_greater god) True) (Eq False True)) % 4.02/4.18 Clause #93 (by clausification #[85]): Or (Eq (is_the god none_greater) False) (Eq (exemplifies_property none_greater god) True) % 4.02/4.18 Clause #94 (by superposition #[93, 7]): Or (Eq (exemplifies_property none_greater god) True) (Eq False True) % 4.02/4.18 Clause #95 (by clausification #[94]): Eq (exemplifies_property none_greater god) True % 4.02/4.18 Clause #123 (by clausification #[53]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (is_the god none_greater) False) % 4.02/4.18 (Or (Eq (exemplifies_property existence god) True) (Eq (exemplifies_property conceivable (skS.0 3 god a)) True)) % 4.02/4.18 Clause #124 (by forward demodulation #[123, 7]): ∀ (a : Iota), % 4.02/4.18 Or (Eq True False) % 4.02/4.18 (Or (Eq (exemplifies_property existence god) True) (Eq (exemplifies_property conceivable (skS.0 3 god a)) True)) % 4.02/4.18 Clause #125 (by clausification #[124]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (exemplifies_property existence god) True) (Eq (exemplifies_property conceivable (skS.0 3 god a)) True) % 4.02/4.18 Clause #126 (by forward demodulation #[125, 9]): ∀ (a : Iota), Or (Eq False True) (Eq (exemplifies_property conceivable (skS.0 3 god a)) True) % 4.02/4.18 Clause #127 (by clausification #[126]): ∀ (a : Iota), Eq (exemplifies_property conceivable (skS.0 3 god a)) True % 4.02/4.18 Clause #131 (by clausification #[52]): ∀ (a a_1 : Iota), % 4.02/4.18 Or (Eq (object a) False) % 4.02/4.18 (Or (Eq (is_the a none_greater) False) % 4.02/4.18 (Or (Eq (exemplifies_property existence a) True) (Eq (exemplifies_relation greater_than (skS.0 3 a a_1) a) True))) % 4.02/4.18 Clause #132 (by clausification #[52]): ∀ (a a_1 : Iota), % 4.02/4.18 Or (Eq (object a) False) % 4.02/4.18 (Or (Eq (is_the a none_greater) False) % 4.02/4.18 (Or (Eq (exemplifies_property existence a) True) (Eq (object (skS.0 3 a a_1)) True))) % 4.02/4.18 Clause #133 (by superposition #[131, 16]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (is_the god none_greater) False) % 4.02/4.18 (Or (Eq (exemplifies_property existence god) True) % 4.02/4.18 (Or (Eq (exemplifies_relation greater_than (skS.0 3 god a) god) True) (Eq False True))) % 4.02/4.18 Clause #134 (by superposition #[132, 16]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (is_the god none_greater) False) % 4.02/4.18 (Or (Eq (exemplifies_property existence god) True) (Or (Eq (object (skS.0 3 god a)) True) (Eq False True))) % 4.02/4.18 Clause #135 (by clausification #[134]): ∀ (a : Iota), % 4.02/4.18 Or (Eq (is_the god none_greater) False) % 4.02/4.18 (Or (Eq (exemplifies_property existence god) True) (Eq (object (skS.0 3 god a)) True)) % 4.02/4.18 Clause #136 (by forward demodulation #[135, 7]): ∀ (a : Iota), Or (Eq True False) (Or (Eq (exemplifies_property existence god) True) (Eq (object (skS.0 3 god a)) True)) % 4.02/4.18 Clause #137 (by clausification #[136]): ∀ (a : Iota), Or (Eq (exemplifies_property existence god) True) (Eq (object (skS.0 3 god a)) True) % 4.02/4.18 Clause #138 (by forward demodulation #[137, 9]): ∀ (a : Iota), Or (Eq False True) (Eq (object (skS.0 3 god a)) True) % 4.02/4.18 Clause #139 (by clausification #[138]): ∀ (a : Iota), Eq (object (skS.0 3 god a)) True % 4.02/4.18 Clause #148 (by clausification #[133]): ∀ (a : Iota), % 4.02/4.20 Or (Eq (is_the god none_greater) False) % 4.02/4.20 (Or (Eq (exemplifies_property existence god) True) % 4.02/4.20 (Eq (exemplifies_relation greater_than (skS.0 3 god a) god) True)) % 4.02/4.20 Clause #149 (by forward demodulation #[148, 7]): ∀ (a : Iota), % 4.02/4.20 Or (Eq True False) % 4.02/4.20 (Or (Eq (exemplifies_property existence god) True) % 4.02/4.20 (Eq (exemplifies_relation greater_than (skS.0 3 god a) god) True)) % 4.02/4.20 Clause #150 (by clausification #[149]): ∀ (a : Iota), % 4.02/4.20 Or (Eq (exemplifies_property existence god) True) (Eq (exemplifies_relation greater_than (skS.0 3 god a) god) True) % 4.02/4.20 Clause #151 (by forward demodulation #[150, 9]): ∀ (a : Iota), Or (Eq False True) (Eq (exemplifies_relation greater_than (skS.0 3 god a) god) True) % 4.02/4.20 Clause #152 (by clausification #[151]): ∀ (a : Iota), Eq (exemplifies_relation greater_than (skS.0 3 god a) god) True % 4.02/4.20 Clause #173 (by clausification #[58]): ∀ (a : Iota), % 4.02/4.20 Or (Eq (object a) False) % 4.02/4.20 (Or (Eq (exemplifies_property none_greater a) False) % 4.02/4.20 (Eq % 4.02/4.20 (Not % 4.02/4.20 (Exists fun Y => % 4.02/4.20 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y))) % 4.02/4.20 True)) % 4.02/4.20 Clause #175 (by clausification #[173]): ∀ (a : Iota), % 4.02/4.20 Or (Eq (object a) False) % 4.02/4.20 (Or (Eq (exemplifies_property none_greater a) False) % 4.02/4.20 (Eq % 4.02/4.20 (Exists fun Y => % 4.02/4.20 And (And (object Y) (exemplifies_relation greater_than Y a)) (exemplifies_property conceivable Y)) % 4.02/4.20 False)) % 4.02/4.20 Clause #176 (by clausification #[175]): ∀ (a a_1 : Iota), % 4.02/4.20 Or (Eq (object a) False) % 4.02/4.20 (Or (Eq (exemplifies_property none_greater a) False) % 4.02/4.20 (Eq (And (And (object a_1) (exemplifies_relation greater_than a_1 a)) (exemplifies_property conceivable a_1)) % 4.02/4.20 False)) % 4.02/4.20 Clause #177 (by clausification #[176]): ∀ (a a_1 : Iota), % 4.02/4.20 Or (Eq (object a) False) % 4.02/4.20 (Or (Eq (exemplifies_property none_greater a) False) % 4.02/4.20 (Or (Eq (And (object a_1) (exemplifies_relation greater_than a_1 a)) False) % 4.02/4.20 (Eq (exemplifies_property conceivable a_1) False))) % 4.02/4.20 Clause #178 (by clausification #[177]): ∀ (a a_1 : Iota), % 4.02/4.20 Or (Eq (object a) False) % 4.02/4.20 (Or (Eq (exemplifies_property none_greater a) False) % 4.02/4.20 (Or (Eq (exemplifies_property conceivable a_1) False) % 4.02/4.20 (Or (Eq (object a_1) False) (Eq (exemplifies_relation greater_than a_1 a) False)))) % 4.02/4.20 Clause #179 (by superposition #[178, 16]): ∀ (a : Iota), % 4.02/4.20 Or (Eq (exemplifies_property none_greater god) False) % 4.02/4.20 (Or (Eq (exemplifies_property conceivable a) False) % 4.02/4.20 (Or (Eq (object a) False) (Or (Eq (exemplifies_relation greater_than a god) False) (Eq False True)))) % 4.02/4.20 Clause #186 (by clausification #[179]): ∀ (a : Iota), % 4.02/4.20 Or (Eq (exemplifies_property none_greater god) False) % 4.02/4.20 (Or (Eq (exemplifies_property conceivable a) False) % 4.02/4.20 (Or (Eq (object a) False) (Eq (exemplifies_relation greater_than a god) False))) % 4.02/4.20 Clause #187 (by forward demodulation #[186, 95]): ∀ (a : Iota), % 4.02/4.20 Or (Eq True False) % 4.02/4.20 (Or (Eq (exemplifies_property conceivable a) False) % 4.02/4.20 (Or (Eq (object a) False) (Eq (exemplifies_relation greater_than a god) False))) % 4.02/4.20 Clause #188 (by clausification #[187]): ∀ (a : Iota), % 4.02/4.20 Or (Eq (exemplifies_property conceivable a) False) % 4.02/4.20 (Or (Eq (object a) False) (Eq (exemplifies_relation greater_than a god) False)) % 4.02/4.20 Clause #189 (by superposition #[188, 127]): ∀ (a : Iota), % 4.02/4.20 Or (Eq (object (skS.0 3 god a)) False) % 4.02/4.20 (Or (Eq (exemplifies_relation greater_than (skS.0 3 god a) god) False) (Eq False True)) % 4.02/4.20 Clause #194 (by clausification #[189]): ∀ (a : Iota), Or (Eq (object (skS.0 3 god a)) False) (Eq (exemplifies_relation greater_than (skS.0 3 god a) god) False) % 4.02/4.20 Clause #195 (by forward demodulation #[194, 139]): ∀ (a : Iota), Or (Eq True False) (Eq (exemplifies_relation greater_than (skS.0 3 god a) god) False) % 4.02/4.20 Clause #196 (by clausification #[195]): ∀ (a : Iota), Eq (exemplifies_relation greater_than (skS.0 3 god a) god) False % 4.02/4.20 Clause #197 (by superposition #[196, 152]): Eq False True % 4.02/4.20 Clause #202 (by clausification #[197]): False % 4.02/4.20 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------