%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU382+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n016.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:30 PM UTC 2025 % Result : Theorem 55.86s 56.09s % Output : Proof 56.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SEU382+1 : TPTP v9.2.0. Released v3.3.0. % 0.11/0.13 % Command : duper %s % 0.13/0.34 % Computer : n016.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:21:38 EDT 2025 % 0.13/0.35 % CPUTime : % 55.86/56.09 SZS status Theorem for theBenchmark.p % 55.86/56.09 SZS output start Proof for theBenchmark.p % 55.86/56.09 Clause #0 (by assumption #[]): Eq (∀ (A : Iota), rel_str A → strict_rel_str A → Eq A (rel_str_of (the_carrier A) (the_InternalRel A))) True % 55.86/56.09 Clause #26 (by assumption #[]): Eq (∀ (A : Iota), Eq (incl_POSet A) (rel_str_of A (inclusion_order A))) True % 55.86/56.09 Clause #30 (by assumption #[]): Eq % 55.86/56.09 (∀ (A : Iota), % 55.86/56.09 And % 55.86/56.09 (And % 55.86/56.09 (And (And (reflexive (inclusion_order A)) (antisymmetric (inclusion_order A))) (transitive (inclusion_order A))) % 55.86/56.09 (v1_partfun1 (inclusion_order A) A A)) % 55.86/56.09 (relation_of2_as_subset (inclusion_order A) A A)) % 55.86/56.09 True % 55.86/56.09 Clause #31 (by assumption #[]): Eq (∀ (A : Iota), And (strict_rel_str (incl_POSet A)) (rel_str (incl_POSet A))) True % 55.86/56.09 Clause #53 (by assumption #[]): Eq (∀ (A B : Iota), relation_of2 B A A → ∀ (C D : Iota), Eq (rel_str_of A B) (rel_str_of C D) → And (Eq A C) (Eq B D)) % 55.86/56.09 True % 55.86/56.09 Clause #70 (by assumption #[]): Eq (∀ (A B C : Iota), Iff (relation_of2_as_subset C A B) (relation_of2 C A B)) True % 55.86/56.09 Clause #76 (by assumption #[]): Eq (Not (∀ (A : Iota), Eq (the_carrier (boole_POSet A)) (powerset A))) True % 55.86/56.09 Clause #77 (by assumption #[]): Eq (∀ (A : Iota), Eq (boole_POSet A) (incl_POSet (powerset A))) True % 55.86/56.09 Clause #88 (by clausification #[0]): ∀ (a : Iota), Eq (rel_str a → strict_rel_str a → Eq a (rel_str_of (the_carrier a) (the_InternalRel a))) True % 55.86/56.09 Clause #89 (by clausification #[88]): ∀ (a : Iota), % 55.86/56.09 Or (Eq (rel_str a) False) (Eq (strict_rel_str a → Eq a (rel_str_of (the_carrier a) (the_InternalRel a))) True) % 55.86/56.09 Clause #90 (by clausification #[89]): ∀ (a : Iota), % 55.86/56.09 Or (Eq (rel_str a) False) % 55.86/56.09 (Or (Eq (strict_rel_str a) False) (Eq (Eq a (rel_str_of (the_carrier a) (the_InternalRel a))) True)) % 55.86/56.09 Clause #91 (by clausification #[90]): ∀ (a : Iota), % 55.86/56.09 Or (Eq (rel_str a) False) (Or (Eq (strict_rel_str a) False) (Eq a (rel_str_of (the_carrier a) (the_InternalRel a)))) % 55.86/56.09 Clause #232 (by clausification #[31]): ∀ (a : Iota), Eq (And (strict_rel_str (incl_POSet a)) (rel_str (incl_POSet a))) True % 55.86/56.09 Clause #233 (by clausification #[232]): ∀ (a : Iota), Eq (rel_str (incl_POSet a)) True % 55.86/56.09 Clause #234 (by clausification #[232]): ∀ (a : Iota), Eq (strict_rel_str (incl_POSet a)) True % 55.86/56.09 Clause #236 (by superposition #[233, 91]): ∀ (a : Iota), % 55.86/56.09 Or (Eq True False) % 55.86/56.09 (Or (Eq (strict_rel_str (incl_POSet a)) False) % 55.86/56.09 (Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (the_InternalRel (incl_POSet a))))) % 55.86/56.09 Clause #270 (by clausification #[77]): ∀ (a : Iota), Eq (Eq (boole_POSet a) (incl_POSet (powerset a))) True % 55.86/56.09 Clause #271 (by clausification #[270]): ∀ (a : Iota), Eq (boole_POSet a) (incl_POSet (powerset a)) % 55.86/56.09 Clause #273 (by clausification #[76]): Eq (∀ (A : Iota), Eq (the_carrier (boole_POSet A)) (powerset A)) False % 55.86/56.09 Clause #274 (by clausification #[273]): ∀ (a : Iota), Eq (Not (Eq (the_carrier (boole_POSet (skS.0 5 a))) (powerset (skS.0 5 a)))) True % 55.86/56.09 Clause #275 (by clausification #[274]): ∀ (a : Iota), Eq (Eq (the_carrier (boole_POSet (skS.0 5 a))) (powerset (skS.0 5 a))) False % 55.86/56.09 Clause #276 (by clausification #[275]): ∀ (a : Iota), Ne (the_carrier (boole_POSet (skS.0 5 a))) (powerset (skS.0 5 a)) % 55.86/56.09 Clause #415 (by clausification #[26]): ∀ (a : Iota), Eq (Eq (incl_POSet a) (rel_str_of a (inclusion_order a))) True % 55.86/56.09 Clause #416 (by clausification #[415]): ∀ (a : Iota), Eq (incl_POSet a) (rel_str_of a (inclusion_order a)) % 55.86/56.09 Clause #505 (by clausification #[30]): ∀ (a : Iota), % 55.86/56.09 Eq % 55.86/56.09 (And % 55.86/56.09 (And % 55.86/56.09 (And (And (reflexive (inclusion_order a)) (antisymmetric (inclusion_order a))) (transitive (inclusion_order a))) % 55.86/56.09 (v1_partfun1 (inclusion_order a) a a)) % 55.86/56.09 (relation_of2_as_subset (inclusion_order a) a a)) % 55.86/56.09 True % 55.86/56.09 Clause #506 (by clausification #[505]): ∀ (a : Iota), Eq (relation_of2_as_subset (inclusion_order a) a a) True % 55.86/56.09 Clause #677 (by clausification #[53]): ∀ (a : Iota), % 55.86/56.09 Eq (∀ (B : Iota), relation_of2 B a a → ∀ (C D : Iota), Eq (rel_str_of a B) (rel_str_of C D) → And (Eq a C) (Eq B D)) % 55.86/56.09 True % 55.86/56.09 Clause #678 (by clausification #[677]): ∀ (a a_1 : Iota), % 55.93/56.11 Eq (relation_of2 a a_1 a_1 → ∀ (C D : Iota), Eq (rel_str_of a_1 a) (rel_str_of C D) → And (Eq a_1 C) (Eq a D)) True % 55.93/56.11 Clause #679 (by clausification #[678]): ∀ (a a_1 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) % 55.93/56.11 (Eq (∀ (C D : Iota), Eq (rel_str_of a_1 a) (rel_str_of C D) → And (Eq a_1 C) (Eq a D)) True) % 55.93/56.11 Clause #680 (by clausification #[679]): ∀ (a a_1 a_2 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) % 55.93/56.11 (Eq (∀ (D : Iota), Eq (rel_str_of a_1 a) (rel_str_of a_2 D) → And (Eq a_1 a_2) (Eq a D)) True) % 55.93/56.11 Clause #681 (by clausification #[680]): ∀ (a a_1 a_2 a_3 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) % 55.93/56.11 (Eq (Eq (rel_str_of a_1 a) (rel_str_of a_2 a_3) → And (Eq a_1 a_2) (Eq a a_3)) True) % 55.93/56.11 Clause #682 (by clausification #[681]): ∀ (a a_1 a_2 a_3 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) % 55.93/56.11 (Or (Eq (Eq (rel_str_of a_1 a) (rel_str_of a_2 a_3)) False) (Eq (And (Eq a_1 a_2) (Eq a a_3)) True)) % 55.93/56.11 Clause #683 (by clausification #[682]): ∀ (a a_1 a_2 a_3 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) % 55.93/56.11 (Or (Eq (And (Eq a_1 a_2) (Eq a a_3)) True) (Ne (rel_str_of a_1 a) (rel_str_of a_2 a_3))) % 55.93/56.11 Clause #684 (by clausification #[683]): ∀ (a a_1 a_2 a_3 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) (Or (Ne (rel_str_of a_1 a) (rel_str_of a_2 a_3)) (Eq (Eq a a_3) True)) % 55.93/56.11 Clause #685 (by clausification #[683]): ∀ (a a_1 a_2 a_3 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) (Or (Ne (rel_str_of a_1 a) (rel_str_of a_2 a_3)) (Eq (Eq a_1 a_2) True)) % 55.93/56.11 Clause #686 (by clausification #[684]): ∀ (a a_1 a_2 a_3 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) (Or (Ne (rel_str_of a_1 a) (rel_str_of a_2 a_3)) (Eq a a_3)) % 55.93/56.11 Clause #906 (by clausification #[70]): ∀ (a : Iota), Eq (∀ (B C : Iota), Iff (relation_of2_as_subset C a B) (relation_of2 C a B)) True % 55.93/56.11 Clause #907 (by clausification #[906]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), Iff (relation_of2_as_subset C a a_1) (relation_of2 C a a_1)) True % 55.93/56.11 Clause #908 (by clausification #[907]): ∀ (a a_1 a_2 : Iota), Eq (Iff (relation_of2_as_subset a a_1 a_2) (relation_of2 a a_1 a_2)) True % 55.93/56.11 Clause #910 (by clausification #[908]): ∀ (a a_1 a_2 : Iota), Or (Eq (relation_of2_as_subset a a_1 a_2) False) (Eq (relation_of2 a a_1 a_2) True) % 55.93/56.11 Clause #914 (by superposition #[910, 506]): ∀ (a : Iota), Or (Eq (relation_of2 (inclusion_order a) a a) True) (Eq False True) % 55.93/56.11 Clause #915 (by clausification #[914]): ∀ (a : Iota), Eq (relation_of2 (inclusion_order a) a a) True % 55.93/56.11 Clause #918 (by superposition #[915, 686]): ∀ (a a_1 a_2 : Iota), % 55.93/56.11 Or (Eq True False) (Or (Ne (rel_str_of a (inclusion_order a)) (rel_str_of a_1 a_2)) (Eq (inclusion_order a) a_2)) % 55.93/56.11 Clause #925 (by clausification #[918]): ∀ (a a_1 a_2 : Iota), Or (Ne (rel_str_of a (inclusion_order a)) (rel_str_of a_1 a_2)) (Eq (inclusion_order a) a_2) % 55.93/56.11 Clause #926 (by forward demodulation #[925, 416]): ∀ (a a_1 a_2 : Iota), Or (Ne (incl_POSet a) (rel_str_of a_1 a_2)) (Eq (inclusion_order a) a_2) % 55.93/56.11 Clause #1880 (by clausification #[236]): ∀ (a : Iota), % 55.93/56.11 Or (Eq (strict_rel_str (incl_POSet a)) False) % 55.93/56.11 (Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (the_InternalRel (incl_POSet a)))) % 55.93/56.11 Clause #1881 (by forward demodulation #[1880, 234]): ∀ (a : Iota), % 55.93/56.11 Or (Eq True False) (Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (the_InternalRel (incl_POSet a)))) % 55.93/56.11 Clause #1882 (by clausification #[1881]): ∀ (a : Iota), Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (the_InternalRel (incl_POSet a))) % 55.93/56.11 Clause #1883 (by superposition #[1882, 926]): ∀ (a a_1 : Iota), Or (Ne (incl_POSet a) (incl_POSet a_1)) (Eq (inclusion_order a) (the_InternalRel (incl_POSet a_1))) % 55.93/56.11 Clause #1885 (by equality resolution #[1883]): ∀ (a : Iota), Eq (inclusion_order a) (the_InternalRel (incl_POSet a)) % 55.93/56.11 Clause #1890 (by backward demodulation #[1885, 1882]): ∀ (a : Iota), Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (inclusion_order a)) % 55.93/56.11 Clause #17068 (by clausification #[685]): ∀ (a a_1 a_2 a_3 : Iota), % 55.93/56.11 Or (Eq (relation_of2 a a_1 a_1) False) (Or (Ne (rel_str_of a_1 a) (rel_str_of a_2 a_3)) (Eq a_1 a_2)) % 56.00/56.18 Clause #17072 (by superposition #[17068, 915]): ∀ (a a_1 a_2 : Iota), Or (Ne (rel_str_of a (inclusion_order a)) (rel_str_of a_1 a_2)) (Or (Eq a a_1) (Eq False True)) % 56.00/56.18 Clause #17073 (by clausification #[17072]): ∀ (a a_1 a_2 : Iota), Or (Ne (rel_str_of a (inclusion_order a)) (rel_str_of a_1 a_2)) (Eq a a_1) % 56.00/56.18 Clause #17074 (by forward demodulation #[17073, 416]): ∀ (a a_1 a_2 : Iota), Or (Ne (incl_POSet a) (rel_str_of a_1 a_2)) (Eq a a_1) % 56.00/56.18 Clause #17077 (by superposition #[17074, 1890]): ∀ (a a_1 : Iota), Or (Ne (incl_POSet a) (incl_POSet a_1)) (Eq a (the_carrier (incl_POSet a_1))) % 56.00/56.18 Clause #17090 (by equality resolution #[17077]): ∀ (a : Iota), Eq a (the_carrier (incl_POSet a)) % 56.00/56.18 Clause #17100 (by superposition #[17090, 271]): ∀ (a : Iota), Eq (powerset a) (the_carrier (boole_POSet a)) % 56.00/56.18 Clause #17107 (by backward contextual literal cutting #[17100, 276]): False % 56.00/56.18 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------