%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU371+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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 08:01:29 PM UTC 2025 % Result : Theorem 45.86s 46.05s % Output : Proof 45.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SEU371+1 : TPTP v9.2.0. Released v3.3.0. % 0.06/0.13 % Command : duper %s % 0.13/0.34 % Computer : n020.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 : Fri Oct 3 05:16:53 EDT 2025 % 0.13/0.34 % CPUTime : % 45.86/46.05 SZS status Theorem for theBenchmark.p % 45.86/46.05 SZS output start Proof for theBenchmark.p % 45.86/46.05 Clause #18 (by assumption #[]): Eq (∀ (A : Iota), rel_str A → Eq (bottom_of_relstr A) (join_on_relstr A empty_set)) True % 45.86/46.05 Clause #21 (by assumption #[]): Eq (∀ (A : Iota), Eq (boole_POSet A) (poset_of_lattice (boole_lattice A))) True % 45.86/46.05 Clause #26 (by assumption #[]): Eq (∀ (A : Iota), And (strict_latt_str (boole_lattice A)) (latt_str (boole_lattice A))) True % 45.86/46.05 Clause #33 (by assumption #[]): Eq (∀ (A : Iota), And (strict_rel_str (boole_POSet A)) (rel_str (boole_POSet A))) True % 45.86/46.05 Clause #52 (by assumption #[]): Eq % 45.86/46.05 (∀ (A : Iota), % 45.86/46.05 And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And (And (Not (empty_carrier (boole_lattice A))) (strict_latt_str (boole_lattice A))) % 45.86/46.05 (join_commutative (boole_lattice A))) % 45.86/46.05 (join_associative (boole_lattice A))) % 45.86/46.05 (meet_commutative (boole_lattice A))) % 45.86/46.05 (meet_associative (boole_lattice A))) % 45.86/46.05 (meet_absorbing (boole_lattice A))) % 45.86/46.05 (join_absorbing (boole_lattice A))) % 45.86/46.05 (lattice (boole_lattice A))) % 45.86/46.05 (distributive_lattstr (boole_lattice A))) % 45.86/46.05 (modular_lattstr (boole_lattice A))) % 45.86/46.05 (lower_bounded_semilattstr (boole_lattice A))) % 45.86/46.05 (upper_bounded_semilattstr (boole_lattice A))) % 45.86/46.05 (bounded_lattstr (boole_lattice A))) % 45.86/46.05 (complemented_lattstr (boole_lattice A))) % 45.86/46.05 (boolean_lattstr (boole_lattice A))) % 45.86/46.05 (complete_latt_str (boole_lattice A))) % 45.86/46.05 True % 45.86/46.05 Clause #53 (by assumption #[]): Eq (∀ (A : Iota), And (Not (empty_carrier (boole_lattice A))) (strict_latt_str (boole_lattice A))) True % 45.86/46.05 Clause #59 (by assumption #[]): Eq % 45.86/46.05 (∀ (A : Iota), % 45.86/46.05 And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And % 45.86/46.05 (And (And (Not (empty_carrier (boole_lattice A))) (strict_latt_str (boole_lattice A))) % 45.86/46.05 (join_commutative (boole_lattice A))) % 45.86/46.05 (join_associative (boole_lattice A))) % 45.86/46.05 (meet_commutative (boole_lattice A))) % 45.86/46.05 (meet_associative (boole_lattice A))) % 45.86/46.05 (meet_absorbing (boole_lattice A))) % 45.86/46.05 (join_absorbing (boole_lattice A))) % 45.86/46.05 (lattice (boole_lattice A))) % 45.86/46.05 True % 45.86/46.05 Clause #96 (by assumption #[]): Eq (Not (∀ (A : Iota), Eq (bottom_of_relstr (boole_POSet A)) empty_set)) True % 45.86/46.05 Clause #98 (by assumption #[]): Eq % 45.86/46.05 (∀ (A : Iota), % 45.86/46.05 And (And (And (Not (empty_carrier A)) (lattice A)) (complete_latt_str A)) (latt_str A) → % 45.86/46.05 ∀ (B : Iota), % 45.86/46.05 And (Eq (join_of_latt_set A B) (join_on_relstr (poset_of_lattice A) B)) % 45.86/46.05 (Eq (meet_of_latt_set A B) (meet_on_relstr (poset_of_lattice A) B))) % 45.86/46.05 True % 45.86/46.05 Clause #101 (by assumption #[]): Eq % 45.86/46.05 (∀ (A : Iota), % 45.86/46.05 And (lower_bounded_semilattstr (boole_lattice A)) (Eq (bottom_of_semilattstr (boole_lattice A)) empty_set)) % 45.86/46.05 True % 45.86/46.05 Clause #104 (by assumption #[]): Eq % 45.86/46.05 (∀ (A : Iota), % 45.86/46.05 And (And (And (Not (empty_carrier A)) (lattice A)) (complete_latt_str A)) (latt_str A) → % 45.86/46.05 And (And (And (And (Not (empty_carrier A)) (lattice A)) (lower_bounded_semilattstr A)) (latt_str A)) % 45.86/46.05 (Eq (bottom_of_semilattstr A) (join_of_latt_set A empty_set))) % 45.86/46.05 True % 45.86/46.05 Clause #245 (by clausification #[33]): ∀ (a : Iota), Eq (And (strict_rel_str (boole_POSet a)) (rel_str (boole_POSet a))) True % 45.86/46.05 Clause #246 (by clausification #[245]): ∀ (a : Iota), Eq (rel_str (boole_POSet a)) True % 45.86/46.05 Clause #257 (by clausification #[26]): ∀ (a : Iota), Eq (And (strict_latt_str (boole_lattice a)) (latt_str (boole_lattice a))) True % 45.86/46.05 Clause #258 (by clausification #[257]): ∀ (a : Iota), Eq (latt_str (boole_lattice a)) True % 45.86/46.05 Clause #325 (by clausification #[21]): ∀ (a : Iota), Eq (Eq (boole_POSet a) (poset_of_lattice (boole_lattice a))) True % 45.86/46.07 Clause #326 (by clausification #[325]): ∀ (a : Iota), Eq (boole_POSet a) (poset_of_lattice (boole_lattice a)) % 45.86/46.07 Clause #337 (by clausification #[96]): Eq (∀ (A : Iota), Eq (bottom_of_relstr (boole_POSet A)) empty_set) False % 45.86/46.07 Clause #338 (by clausification #[337]): ∀ (a : Iota), Eq (Not (Eq (bottom_of_relstr (boole_POSet (skS.0 11 a))) empty_set)) True % 45.86/46.07 Clause #339 (by clausification #[338]): ∀ (a : Iota), Eq (Eq (bottom_of_relstr (boole_POSet (skS.0 11 a))) empty_set) False % 45.86/46.07 Clause #340 (by clausification #[339]): ∀ (a : Iota), Ne (bottom_of_relstr (boole_POSet (skS.0 11 a))) empty_set % 45.86/46.07 Clause #450 (by clausification #[18]): ∀ (a : Iota), Eq (rel_str a → Eq (bottom_of_relstr a) (join_on_relstr a empty_set)) True % 45.86/46.07 Clause #451 (by clausification #[450]): ∀ (a : Iota), Or (Eq (rel_str a) False) (Eq (Eq (bottom_of_relstr a) (join_on_relstr a empty_set)) True) % 45.86/46.07 Clause #452 (by clausification #[451]): ∀ (a : Iota), Or (Eq (rel_str a) False) (Eq (bottom_of_relstr a) (join_on_relstr a empty_set)) % 45.86/46.07 Clause #454 (by superposition #[452, 246]): ∀ (a : Iota), Or (Eq (bottom_of_relstr (boole_POSet a)) (join_on_relstr (boole_POSet a) empty_set)) (Eq False True) % 45.86/46.07 Clause #465 (by clausification #[454]): ∀ (a : Iota), Eq (bottom_of_relstr (boole_POSet a)) (join_on_relstr (boole_POSet a) empty_set) % 45.86/46.07 Clause #466 (by clausification #[53]): ∀ (a : Iota), Eq (And (Not (empty_carrier (boole_lattice a))) (strict_latt_str (boole_lattice a))) True % 45.86/46.07 Clause #467 (by clausification #[466]): ∀ (a : Iota), Eq (Not (empty_carrier (boole_lattice a))) True % 45.86/46.07 Clause #468 (by clausification #[467]): ∀ (a : Iota), Eq (empty_carrier (boole_lattice a)) False % 45.86/46.07 Clause #622 (by clausification #[101]): ∀ (a : Iota), % 45.86/46.07 Eq (And (lower_bounded_semilattstr (boole_lattice a)) (Eq (bottom_of_semilattstr (boole_lattice a)) empty_set)) True % 45.86/46.07 Clause #623 (by clausification #[622]): ∀ (a : Iota), Eq (Eq (bottom_of_semilattstr (boole_lattice a)) empty_set) True % 45.86/46.07 Clause #625 (by clausification #[623]): ∀ (a : Iota), Eq (bottom_of_semilattstr (boole_lattice a)) empty_set % 45.86/46.07 Clause #634 (by clausification #[52]): ∀ (a : Iota), % 45.86/46.07 Eq % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And (And (Not (empty_carrier (boole_lattice a))) (strict_latt_str (boole_lattice a))) % 45.86/46.07 (join_commutative (boole_lattice a))) % 45.86/46.07 (join_associative (boole_lattice a))) % 45.86/46.07 (meet_commutative (boole_lattice a))) % 45.86/46.07 (meet_associative (boole_lattice a))) % 45.86/46.07 (meet_absorbing (boole_lattice a))) % 45.86/46.07 (join_absorbing (boole_lattice a))) % 45.86/46.07 (lattice (boole_lattice a))) % 45.86/46.07 (distributive_lattstr (boole_lattice a))) % 45.86/46.07 (modular_lattstr (boole_lattice a))) % 45.86/46.07 (lower_bounded_semilattstr (boole_lattice a))) % 45.86/46.07 (upper_bounded_semilattstr (boole_lattice a))) % 45.86/46.07 (bounded_lattstr (boole_lattice a))) % 45.86/46.07 (complemented_lattstr (boole_lattice a))) % 45.86/46.07 (boolean_lattstr (boole_lattice a))) % 45.86/46.07 (complete_latt_str (boole_lattice a))) % 45.86/46.07 True % 45.86/46.07 Clause #635 (by clausification #[634]): ∀ (a : Iota), Eq (complete_latt_str (boole_lattice a)) True % 45.86/46.07 Clause #698 (by clausification #[59]): ∀ (a : Iota), % 45.86/46.07 Eq % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And % 45.86/46.07 (And (And (Not (empty_carrier (boole_lattice a))) (strict_latt_str (boole_lattice a))) % 45.86/46.07 (join_commutative (boole_lattice a))) % 45.86/46.07 (join_associative (boole_lattice a))) % 45.86/46.07 (meet_commutative (boole_lattice a))) % 45.86/46.07 (meet_associative (boole_lattice a))) % 45.86/46.07 (meet_absorbing (boole_lattice a))) % 45.86/46.09 (join_absorbing (boole_lattice a))) % 45.86/46.09 (lattice (boole_lattice a))) % 45.86/46.09 True % 45.86/46.09 Clause #699 (by clausification #[698]): ∀ (a : Iota), Eq (lattice (boole_lattice a)) True % 45.86/46.09 Clause #1186 (by clausification #[98]): ∀ (a : Iota), % 45.86/46.09 Eq % 45.86/46.09 (And (And (And (Not (empty_carrier a)) (lattice a)) (complete_latt_str a)) (latt_str a) → % 45.86/46.09 ∀ (B : Iota), % 45.86/46.09 And (Eq (join_of_latt_set a B) (join_on_relstr (poset_of_lattice a) B)) % 45.86/46.09 (Eq (meet_of_latt_set a B) (meet_on_relstr (poset_of_lattice a) B))) % 45.86/46.09 True % 45.86/46.09 Clause #1187 (by clausification #[1186]): ∀ (a : Iota), % 45.86/46.09 Or (Eq (And (And (And (Not (empty_carrier a)) (lattice a)) (complete_latt_str a)) (latt_str a)) False) % 45.86/46.09 (Eq % 45.86/46.09 (∀ (B : Iota), % 45.86/46.09 And (Eq (join_of_latt_set a B) (join_on_relstr (poset_of_lattice a) B)) % 45.86/46.09 (Eq (meet_of_latt_set a B) (meet_on_relstr (poset_of_lattice a) B))) % 45.86/46.09 True) % 45.86/46.09 Clause #1188 (by clausification #[1187]): ∀ (a : Iota), % 45.86/46.09 Or % 45.86/46.09 (Eq % 45.86/46.09 (∀ (B : Iota), % 45.86/46.09 And (Eq (join_of_latt_set a B) (join_on_relstr (poset_of_lattice a) B)) % 45.86/46.09 (Eq (meet_of_latt_set a B) (meet_on_relstr (poset_of_lattice a) B))) % 45.86/46.09 True) % 45.86/46.09 (Or (Eq (And (And (Not (empty_carrier a)) (lattice a)) (complete_latt_str a)) False) (Eq (latt_str a) False)) % 45.86/46.09 Clause #1189 (by clausification #[1188]): ∀ (a a_1 : Iota), % 45.86/46.09 Or (Eq (And (And (Not (empty_carrier a)) (lattice a)) (complete_latt_str a)) False) % 45.86/46.09 (Or (Eq (latt_str a) False) % 45.86/46.09 (Eq % 45.86/46.09 (And (Eq (join_of_latt_set a a_1) (join_on_relstr (poset_of_lattice a) a_1)) % 45.86/46.09 (Eq (meet_of_latt_set a a_1) (meet_on_relstr (poset_of_lattice a) a_1))) % 45.86/46.09 True)) % 45.86/46.09 Clause #1190 (by clausification #[1189]): ∀ (a a_1 : Iota), % 45.86/46.09 Or (Eq (latt_str a) False) % 45.86/46.09 (Or % 45.86/46.09 (Eq % 45.86/46.09 (And (Eq (join_of_latt_set a a_1) (join_on_relstr (poset_of_lattice a) a_1)) % 45.86/46.09 (Eq (meet_of_latt_set a a_1) (meet_on_relstr (poset_of_lattice a) a_1))) % 45.86/46.09 True) % 45.86/46.09 (Or (Eq (And (Not (empty_carrier a)) (lattice a)) False) (Eq (complete_latt_str a) False))) % 45.86/46.09 Clause #1192 (by clausification #[1190]): ∀ (a a_1 : Iota), % 45.86/46.09 Or (Eq (latt_str a) False) % 45.86/46.09 (Or (Eq (And (Not (empty_carrier a)) (lattice a)) False) % 45.86/46.09 (Or (Eq (complete_latt_str a) False) % 45.86/46.09 (Eq (Eq (join_of_latt_set a a_1) (join_on_relstr (poset_of_lattice a) a_1)) True))) % 45.86/46.09 Clause #1214 (by clausification #[104]): ∀ (a : Iota), % 45.86/46.09 Eq % 45.86/46.09 (And (And (And (Not (empty_carrier a)) (lattice a)) (complete_latt_str a)) (latt_str a) → % 45.86/46.09 And (And (And (And (Not (empty_carrier a)) (lattice a)) (lower_bounded_semilattstr a)) (latt_str a)) % 45.86/46.09 (Eq (bottom_of_semilattstr a) (join_of_latt_set a empty_set))) % 45.86/46.09 True % 45.86/46.09 Clause #1215 (by clausification #[1214]): ∀ (a : Iota), % 45.86/46.09 Or (Eq (And (And (And (Not (empty_carrier a)) (lattice a)) (complete_latt_str a)) (latt_str a)) False) % 45.86/46.09 (Eq % 45.86/46.09 (And (And (And (And (Not (empty_carrier a)) (lattice a)) (lower_bounded_semilattstr a)) (latt_str a)) % 45.86/46.09 (Eq (bottom_of_semilattstr a) (join_of_latt_set a empty_set))) % 45.86/46.09 True) % 45.86/46.09 Clause #1216 (by clausification #[1215]): ∀ (a : Iota), % 45.86/46.09 Or % 45.86/46.09 (Eq % 45.86/46.09 (And (And (And (And (Not (empty_carrier a)) (lattice a)) (lower_bounded_semilattstr a)) (latt_str a)) % 45.86/46.09 (Eq (bottom_of_semilattstr a) (join_of_latt_set a empty_set))) % 45.86/46.09 True) % 45.86/46.09 (Or (Eq (And (And (Not (empty_carrier a)) (lattice a)) (complete_latt_str a)) False) (Eq (latt_str a) False)) % 45.86/46.09 Clause #1217 (by clausification #[1216]): ∀ (a : Iota), % 45.86/46.09 Or (Eq (And (And (Not (empty_carrier a)) (lattice a)) (complete_latt_str a)) False) % 45.86/46.09 (Or (Eq (latt_str a) False) (Eq (Eq (bottom_of_semilattstr a) (join_of_latt_set a empty_set)) True)) % 45.86/46.09 Clause #1219 (by clausification #[1217]): ∀ (a : Iota), % 45.86/46.09 Or (Eq (latt_str a) False) % 45.86/46.09 (Or (Eq (Eq (bottom_of_semilattstr a) (join_of_latt_set a empty_set)) True) % 45.86/46.09 (Or (Eq (And (Not (empty_carrier a)) (lattice a)) False) (Eq (complete_latt_str a) False))) % 45.86/46.09 Clause #1220 (by clausification #[1219]): ∀ (a : Iota), % 45.86/46.09 Or (Eq (latt_str a) False) % 45.86/46.09 (Or (Eq (And (Not (empty_carrier a)) (lattice a)) False) % 45.94/46.11 (Or (Eq (complete_latt_str a) False) (Eq (bottom_of_semilattstr a) (join_of_latt_set a empty_set)))) % 45.94/46.11 Clause #1221 (by clausification #[1220]): ∀ (a : Iota), % 45.94/46.11 Or (Eq (latt_str a) False) % 45.94/46.11 (Or (Eq (complete_latt_str a) False) % 45.94/46.11 (Or (Eq (bottom_of_semilattstr a) (join_of_latt_set a empty_set)) % 45.94/46.11 (Or (Eq (Not (empty_carrier a)) False) (Eq (lattice a) False)))) % 45.94/46.11 Clause #1222 (by clausification #[1221]): ∀ (a : Iota), % 45.94/46.11 Or (Eq (latt_str a) False) % 45.94/46.11 (Or (Eq (complete_latt_str a) False) % 45.94/46.11 (Or (Eq (bottom_of_semilattstr a) (join_of_latt_set a empty_set)) % 45.94/46.11 (Or (Eq (lattice a) False) (Eq (empty_carrier a) True)))) % 45.94/46.11 Clause #1224 (by superposition #[1222, 258]): ∀ (a : Iota), % 45.94/46.11 Or (Eq (complete_latt_str (boole_lattice a)) False) % 45.94/46.11 (Or (Eq (bottom_of_semilattstr (boole_lattice a)) (join_of_latt_set (boole_lattice a) empty_set)) % 45.94/46.11 (Or (Eq (lattice (boole_lattice a)) False) (Or (Eq (empty_carrier (boole_lattice a)) True) (Eq False True)))) % 45.94/46.11 Clause #5126 (by clausification #[1224]): ∀ (a : Iota), % 45.94/46.11 Or (Eq (complete_latt_str (boole_lattice a)) False) % 45.94/46.11 (Or (Eq (bottom_of_semilattstr (boole_lattice a)) (join_of_latt_set (boole_lattice a) empty_set)) % 45.94/46.11 (Or (Eq (lattice (boole_lattice a)) False) (Eq (empty_carrier (boole_lattice a)) True))) % 45.94/46.11 Clause #5127 (by forward demodulation #[5126, 635]): ∀ (a : Iota), % 45.94/46.11 Or (Eq True False) % 45.94/46.11 (Or (Eq (bottom_of_semilattstr (boole_lattice a)) (join_of_latt_set (boole_lattice a) empty_set)) % 45.94/46.11 (Or (Eq (lattice (boole_lattice a)) False) (Eq (empty_carrier (boole_lattice a)) True))) % 45.94/46.11 Clause #5128 (by clausification #[5127]): ∀ (a : Iota), % 45.94/46.11 Or (Eq (bottom_of_semilattstr (boole_lattice a)) (join_of_latt_set (boole_lattice a) empty_set)) % 45.94/46.11 (Or (Eq (lattice (boole_lattice a)) False) (Eq (empty_carrier (boole_lattice a)) True)) % 45.94/46.11 Clause #5129 (by forward demodulation #[5128, 625]): ∀ (a : Iota), % 45.94/46.11 Or (Eq empty_set (join_of_latt_set (boole_lattice a) empty_set)) % 45.94/46.11 (Or (Eq (lattice (boole_lattice a)) False) (Eq (empty_carrier (boole_lattice a)) True)) % 45.94/46.11 Clause #5130 (by forward demodulation #[5129, 699]): ∀ (a : Iota), % 45.94/46.11 Or (Eq empty_set (join_of_latt_set (boole_lattice a) empty_set)) % 45.94/46.11 (Or (Eq True False) (Eq (empty_carrier (boole_lattice a)) True)) % 45.94/46.11 Clause #5131 (by clausification #[5130]): ∀ (a : Iota), % 45.94/46.11 Or (Eq empty_set (join_of_latt_set (boole_lattice a) empty_set)) (Eq (empty_carrier (boole_lattice a)) True) % 45.94/46.11 Clause #5132 (by forward demodulation #[5131, 468]): ∀ (a : Iota), Or (Eq empty_set (join_of_latt_set (boole_lattice a) empty_set)) (Eq False True) % 45.94/46.11 Clause #5133 (by clausification #[5132]): ∀ (a : Iota), Eq empty_set (join_of_latt_set (boole_lattice a) empty_set) % 45.94/46.11 Clause #7519 (by clausification #[1192]): ∀ (a a_1 : Iota), % 45.94/46.11 Or (Eq (latt_str a) False) % 45.94/46.11 (Or (Eq (complete_latt_str a) False) % 45.94/46.11 (Or (Eq (Eq (join_of_latt_set a a_1) (join_on_relstr (poset_of_lattice a) a_1)) True) % 45.94/46.11 (Or (Eq (Not (empty_carrier a)) False) (Eq (lattice a) False)))) % 45.94/46.11 Clause #7520 (by clausification #[7519]): ∀ (a a_1 : Iota), % 45.94/46.11 Or (Eq (latt_str a) False) % 45.94/46.11 (Or (Eq (complete_latt_str a) False) % 45.94/46.11 (Or (Eq (Not (empty_carrier a)) False) % 45.94/46.11 (Or (Eq (lattice a) False) (Eq (join_of_latt_set a a_1) (join_on_relstr (poset_of_lattice a) a_1))))) % 45.94/46.11 Clause #7521 (by clausification #[7520]): ∀ (a a_1 : Iota), % 45.94/46.11 Or (Eq (latt_str a) False) % 45.94/46.11 (Or (Eq (complete_latt_str a) False) % 45.94/46.11 (Or (Eq (lattice a) False) % 45.94/46.11 (Or (Eq (join_of_latt_set a a_1) (join_on_relstr (poset_of_lattice a) a_1)) (Eq (empty_carrier a) True)))) % 45.94/46.11 Clause #7523 (by superposition #[7521, 258]): ∀ (a a_1 : Iota), % 45.94/46.11 Or (Eq (complete_latt_str (boole_lattice a)) False) % 45.94/46.11 (Or (Eq (lattice (boole_lattice a)) False) % 45.94/46.11 (Or (Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (poset_of_lattice (boole_lattice a)) a_1)) % 45.94/46.11 (Or (Eq (empty_carrier (boole_lattice a)) True) (Eq False True)))) % 45.94/46.11 Clause #7533 (by clausification #[7523]): ∀ (a a_1 : Iota), % 45.94/46.11 Or (Eq (complete_latt_str (boole_lattice a)) False) % 45.94/46.11 (Or (Eq (lattice (boole_lattice a)) False) % 45.94/46.11 (Or (Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (poset_of_lattice (boole_lattice a)) a_1)) % 45.94/46.17 (Eq (empty_carrier (boole_lattice a)) True))) % 45.94/46.17 Clause #7534 (by forward demodulation #[7533, 635]): ∀ (a a_1 : Iota), % 45.94/46.17 Or (Eq True False) % 45.94/46.17 (Or (Eq (lattice (boole_lattice a)) False) % 45.94/46.17 (Or (Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (poset_of_lattice (boole_lattice a)) a_1)) % 45.94/46.17 (Eq (empty_carrier (boole_lattice a)) True))) % 45.94/46.17 Clause #7535 (by clausification #[7534]): ∀ (a a_1 : Iota), % 45.94/46.17 Or (Eq (lattice (boole_lattice a)) False) % 45.94/46.17 (Or (Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (poset_of_lattice (boole_lattice a)) a_1)) % 45.94/46.17 (Eq (empty_carrier (boole_lattice a)) True)) % 45.94/46.17 Clause #7536 (by forward demodulation #[7535, 699]): ∀ (a a_1 : Iota), % 45.94/46.17 Or (Eq True False) % 45.94/46.17 (Or (Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (poset_of_lattice (boole_lattice a)) a_1)) % 45.94/46.17 (Eq (empty_carrier (boole_lattice a)) True)) % 45.94/46.17 Clause #7537 (by clausification #[7536]): ∀ (a a_1 : Iota), % 45.94/46.17 Or (Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (poset_of_lattice (boole_lattice a)) a_1)) % 45.94/46.17 (Eq (empty_carrier (boole_lattice a)) True) % 45.94/46.17 Clause #7538 (by forward demodulation #[7537, 326]): ∀ (a a_1 : Iota), % 45.94/46.17 Or (Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (boole_POSet a) a_1)) % 45.94/46.17 (Eq (empty_carrier (boole_lattice a)) True) % 45.94/46.17 Clause #7539 (by forward demodulation #[7538, 468]): ∀ (a a_1 : Iota), Or (Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (boole_POSet a) a_1)) (Eq False True) % 45.94/46.17 Clause #7540 (by clausification #[7539]): ∀ (a a_1 : Iota), Eq (join_of_latt_set (boole_lattice a) a_1) (join_on_relstr (boole_POSet a) a_1) % 45.94/46.17 Clause #7541 (by superposition #[7540, 465]): ∀ (a : Iota), Eq (bottom_of_relstr (boole_POSet a)) (join_of_latt_set (boole_lattice a) empty_set) % 45.94/46.17 Clause #7548 (by superposition #[7541, 5133]): ∀ (a : Iota), Eq empty_set (bottom_of_relstr (boole_POSet a)) % 45.94/46.17 Clause #7565 (by backward contextual literal cutting #[7548, 340]): False % 45.94/46.17 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------