%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU368+1 : TPTP v9.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n004.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:28 PM UTC 2025 % Result : Theorem 4.47s 4.65s % Output : Proof 4.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU368+1 : TPTP v9.2.0. Released v3.3.0. % 0.07/0.14 % Command : duper %s % 0.13/0.35 % Computer : n004.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Fri Oct 3 06:06:23 EDT 2025 % 0.13/0.35 % CPUTime : % 4.47/4.65 SZS status Theorem for theBenchmark.p % 4.47/4.65 SZS output start Proof for theBenchmark.p % 4.47/4.65 Clause #28 (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)) % 4.47/4.65 True % 4.47/4.65 Clause #29 (by assumption #[]): Eq (∀ (A : Iota), rel_str A → strict_rel_str A → Eq A (rel_str_of (the_carrier A) (the_InternalRel A))) True % 4.47/4.65 Clause #33 (by assumption #[]): Eq (∀ (A B C : Iota), Iff (relation_of2_as_subset C A B) (relation_of2 C A B)) True % 4.47/4.65 Clause #40 (by assumption #[]): Eq (∀ (A : Iota), Eq (inclusion_order A) (inclusion_relation A)) True % 4.47/4.65 Clause #41 (by assumption #[]): Eq % 4.47/4.65 (∀ (A : Iota), % 4.47/4.65 And % 4.47/4.65 (And % 4.47/4.65 (And (And (reflexive (inclusion_order A)) (antisymmetric (inclusion_order A))) (transitive (inclusion_order A))) % 4.47/4.65 (v1_partfun1 (inclusion_order A) A A)) % 4.47/4.65 (relation_of2_as_subset (inclusion_order A) A A)) % 4.47/4.65 True % 4.47/4.65 Clause #42 (by assumption #[]): Eq (∀ (A : Iota), And (strict_rel_str (incl_POSet A)) (rel_str (incl_POSet A))) True % 4.47/4.65 Clause #45 (by assumption #[]): Eq (∀ (A : Iota), Eq (incl_POSet A) (rel_str_of A (inclusion_order A))) True % 4.47/4.65 Clause #46 (by assumption #[]): Eq % 4.47/4.65 (Not % 4.47/4.65 (∀ (A : Iota), And (Eq (the_carrier (incl_POSet A)) A) (Eq (the_InternalRel (incl_POSet A)) (inclusion_order A)))) % 4.47/4.65 True % 4.47/4.65 Clause #109 (by clausification #[40]): ∀ (a : Iota), Eq (Eq (inclusion_order a) (inclusion_relation a)) True % 4.47/4.65 Clause #110 (by clausification #[109]): ∀ (a : Iota), Eq (inclusion_order a) (inclusion_relation a) % 4.47/4.65 Clause #111 (by clausification #[42]): ∀ (a : Iota), Eq (And (strict_rel_str (incl_POSet a)) (rel_str (incl_POSet a))) True % 4.47/4.65 Clause #112 (by clausification #[111]): ∀ (a : Iota), Eq (rel_str (incl_POSet a)) True % 4.47/4.65 Clause #113 (by clausification #[111]): ∀ (a : Iota), Eq (strict_rel_str (incl_POSet a)) True % 4.47/4.65 Clause #153 (by clausification #[45]): ∀ (a : Iota), Eq (Eq (incl_POSet a) (rel_str_of a (inclusion_order a))) True % 4.47/4.65 Clause #154 (by clausification #[153]): ∀ (a : Iota), Eq (incl_POSet a) (rel_str_of a (inclusion_order a)) % 4.47/4.65 Clause #155 (by forward demodulation #[154, 110]): ∀ (a : Iota), Eq (incl_POSet a) (rel_str_of a (inclusion_relation a)) % 4.47/4.65 Clause #226 (by clausification #[29]): ∀ (a : Iota), Eq (rel_str a → strict_rel_str a → Eq a (rel_str_of (the_carrier a) (the_InternalRel a))) True % 4.47/4.65 Clause #227 (by clausification #[226]): ∀ (a : Iota), % 4.47/4.65 Or (Eq (rel_str a) False) (Eq (strict_rel_str a → Eq a (rel_str_of (the_carrier a) (the_InternalRel a))) True) % 4.47/4.65 Clause #228 (by clausification #[227]): ∀ (a : Iota), % 4.47/4.65 Or (Eq (rel_str a) False) % 4.47/4.65 (Or (Eq (strict_rel_str a) False) (Eq (Eq a (rel_str_of (the_carrier a) (the_InternalRel a))) True)) % 4.47/4.65 Clause #229 (by clausification #[228]): ∀ (a : Iota), % 4.47/4.65 Or (Eq (rel_str a) False) (Or (Eq (strict_rel_str a) False) (Eq a (rel_str_of (the_carrier a) (the_InternalRel a)))) % 4.47/4.65 Clause #231 (by superposition #[229, 112]): ∀ (a : Iota), % 4.47/4.65 Or (Eq (strict_rel_str (incl_POSet a)) False) % 4.47/4.65 (Or (Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (the_InternalRel (incl_POSet a)))) (Eq False True)) % 4.47/4.65 Clause #267 (by clausification #[28]): ∀ (a : Iota), % 4.47/4.65 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)) % 4.47/4.65 True % 4.47/4.65 Clause #268 (by clausification #[267]): ∀ (a a_1 : Iota), % 4.47/4.65 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 % 4.47/4.65 Clause #269 (by clausification #[268]): ∀ (a a_1 : Iota), % 4.47/4.65 Or (Eq (relation_of2 a a_1 a_1) False) % 4.47/4.65 (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) % 4.47/4.65 Clause #270 (by clausification #[269]): ∀ (a a_1 a_2 : Iota), % 4.47/4.65 Or (Eq (relation_of2 a a_1 a_1) False) % 4.47/4.65 (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) % 4.47/4.65 Clause #271 (by clausification #[270]): ∀ (a a_1 a_2 a_3 : Iota), % 4.47/4.65 Or (Eq (relation_of2 a a_1 a_1) False) % 4.47/4.65 (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) % 4.47/4.65 Clause #272 (by clausification #[271]): ∀ (a a_1 a_2 a_3 : Iota), % 4.47/4.67 Or (Eq (relation_of2 a a_1 a_1) False) % 4.47/4.67 (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)) % 4.47/4.67 Clause #273 (by clausification #[272]): ∀ (a a_1 a_2 a_3 : Iota), % 4.47/4.67 Or (Eq (relation_of2 a a_1 a_1) False) % 4.47/4.67 (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))) % 4.47/4.67 Clause #274 (by clausification #[273]): ∀ (a a_1 a_2 a_3 : Iota), % 4.47/4.67 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)) % 4.47/4.67 Clause #275 (by clausification #[273]): ∀ (a a_1 a_2 a_3 : Iota), % 4.47/4.67 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)) % 4.47/4.67 Clause #276 (by clausification #[274]): ∀ (a a_1 a_2 a_3 : Iota), % 4.47/4.67 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)) % 4.47/4.67 Clause #287 (by clausification #[33]): ∀ (a : Iota), Eq (∀ (B C : Iota), Iff (relation_of2_as_subset C a B) (relation_of2 C a B)) True % 4.47/4.67 Clause #288 (by clausification #[287]): ∀ (a a_1 : Iota), Eq (∀ (C : Iota), Iff (relation_of2_as_subset C a a_1) (relation_of2 C a a_1)) True % 4.47/4.67 Clause #289 (by clausification #[288]): ∀ (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 % 4.47/4.67 Clause #291 (by clausification #[289]): ∀ (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) % 4.47/4.67 Clause #320 (by clausification #[41]): ∀ (a : Iota), % 4.47/4.67 Eq % 4.47/4.67 (And % 4.47/4.67 (And % 4.47/4.67 (And (And (reflexive (inclusion_order a)) (antisymmetric (inclusion_order a))) (transitive (inclusion_order a))) % 4.47/4.67 (v1_partfun1 (inclusion_order a) a a)) % 4.47/4.67 (relation_of2_as_subset (inclusion_order a) a a)) % 4.47/4.67 True % 4.47/4.67 Clause #321 (by clausification #[320]): ∀ (a : Iota), Eq (relation_of2_as_subset (inclusion_order a) a a) True % 4.47/4.67 Clause #323 (by forward demodulation #[321, 110]): ∀ (a : Iota), Eq (relation_of2_as_subset (inclusion_relation a) a a) True % 4.47/4.67 Clause #325 (by superposition #[323, 291]): ∀ (a : Iota), Or (Eq True False) (Eq (relation_of2 (inclusion_relation a) a a) True) % 4.47/4.67 Clause #326 (by clausification #[325]): ∀ (a : Iota), Eq (relation_of2 (inclusion_relation a) a a) True % 4.47/4.67 Clause #328 (by superposition #[326, 276]): ∀ (a a_1 a_2 : Iota), % 4.47/4.67 Or (Eq True False) % 4.47/4.67 (Or (Ne (rel_str_of a (inclusion_relation a)) (rel_str_of a_1 a_2)) (Eq (inclusion_relation a) a_2)) % 4.47/4.67 Clause #343 (by clausification #[328]): ∀ (a a_1 a_2 : Iota), Or (Ne (rel_str_of a (inclusion_relation a)) (rel_str_of a_1 a_2)) (Eq (inclusion_relation a) a_2) % 4.47/4.67 Clause #344 (by forward demodulation #[343, 155]): ∀ (a a_1 a_2 : Iota), Or (Ne (incl_POSet a) (rel_str_of a_1 a_2)) (Eq (inclusion_relation a) a_2) % 4.47/4.67 Clause #347 (by clausification #[46]): Eq (∀ (A : Iota), And (Eq (the_carrier (incl_POSet A)) A) (Eq (the_InternalRel (incl_POSet A)) (inclusion_order A))) % 4.47/4.67 False % 4.47/4.67 Clause #348 (by clausification #[347]): ∀ (a : Iota), % 4.47/4.67 Eq % 4.47/4.67 (Not % 4.47/4.67 (And (Eq (the_carrier (incl_POSet (skS.0 13 a))) (skS.0 13 a)) % 4.47/4.67 (Eq (the_InternalRel (incl_POSet (skS.0 13 a))) (inclusion_order (skS.0 13 a))))) % 4.47/4.67 True % 4.47/4.67 Clause #349 (by clausification #[348]): ∀ (a : Iota), % 4.47/4.67 Eq % 4.47/4.67 (And (Eq (the_carrier (incl_POSet (skS.0 13 a))) (skS.0 13 a)) % 4.47/4.67 (Eq (the_InternalRel (incl_POSet (skS.0 13 a))) (inclusion_order (skS.0 13 a)))) % 4.47/4.67 False % 4.47/4.67 Clause #350 (by clausification #[349]): ∀ (a : Iota), % 4.47/4.67 Or (Eq (Eq (the_carrier (incl_POSet (skS.0 13 a))) (skS.0 13 a)) False) % 4.47/4.67 (Eq (Eq (the_InternalRel (incl_POSet (skS.0 13 a))) (inclusion_order (skS.0 13 a))) False) % 4.47/4.67 Clause #351 (by clausification #[350]): ∀ (a : Iota), % 4.47/4.67 Or (Eq (Eq (the_InternalRel (incl_POSet (skS.0 13 a))) (inclusion_order (skS.0 13 a))) False) % 4.47/4.67 (Ne (the_carrier (incl_POSet (skS.0 13 a))) (skS.0 13 a)) % 4.47/4.67 Clause #352 (by clausification #[351]): ∀ (a : Iota), % 4.47/4.67 Or (Ne (the_carrier (incl_POSet (skS.0 13 a))) (skS.0 13 a)) % 4.47/4.67 (Ne (the_InternalRel (incl_POSet (skS.0 13 a))) (inclusion_order (skS.0 13 a))) % 4.47/4.67 Clause #353 (by forward demodulation #[352, 110]): ∀ (a : Iota), % 4.47/4.68 Or (Ne (the_carrier (incl_POSet (skS.0 13 a))) (skS.0 13 a)) % 4.47/4.68 (Ne (the_InternalRel (incl_POSet (skS.0 13 a))) (inclusion_relation (skS.0 13 a))) % 4.47/4.68 Clause #361 (by clausification #[231]): ∀ (a : Iota), % 4.47/4.68 Or (Eq (strict_rel_str (incl_POSet a)) False) % 4.47/4.68 (Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (the_InternalRel (incl_POSet a)))) % 4.47/4.68 Clause #362 (by forward demodulation #[361, 113]): ∀ (a : Iota), % 4.47/4.68 Or (Eq True False) (Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (the_InternalRel (incl_POSet a)))) % 4.47/4.68 Clause #363 (by clausification #[362]): ∀ (a : Iota), Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (the_InternalRel (incl_POSet a))) % 4.47/4.68 Clause #364 (by superposition #[363, 344]): ∀ (a a_1 : Iota), Or (Ne (incl_POSet a) (incl_POSet a_1)) (Eq (inclusion_relation a) (the_InternalRel (incl_POSet a_1))) % 4.47/4.68 Clause #365 (by equality resolution #[364]): ∀ (a : Iota), Eq (inclusion_relation a) (the_InternalRel (incl_POSet a)) % 4.47/4.68 Clause #369 (by backward demodulation #[365, 363]): ∀ (a : Iota), Eq (incl_POSet a) (rel_str_of (the_carrier (incl_POSet a)) (inclusion_relation a)) % 4.47/4.68 Clause #370 (by backward contextual literal cutting #[365, 353]): ∀ (a : Iota), Ne (the_carrier (incl_POSet (skS.0 13 a))) (skS.0 13 a) % 4.47/4.68 Clause #430 (by clausification #[275]): ∀ (a a_1 a_2 a_3 : Iota), % 4.47/4.68 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)) % 4.47/4.68 Clause #433 (by superposition #[430, 326]): ∀ (a a_1 a_2 : Iota), Or (Ne (rel_str_of a (inclusion_relation a)) (rel_str_of a_1 a_2)) (Or (Eq a a_1) (Eq False True)) % 4.47/4.68 Clause #434 (by clausification #[433]): ∀ (a a_1 a_2 : Iota), Or (Ne (rel_str_of a (inclusion_relation a)) (rel_str_of a_1 a_2)) (Eq a a_1) % 4.47/4.68 Clause #435 (by forward demodulation #[434, 155]): ∀ (a a_1 a_2 : Iota), Or (Ne (incl_POSet a) (rel_str_of a_1 a_2)) (Eq a a_1) % 4.47/4.68 Clause #436 (by superposition #[435, 369]): ∀ (a a_1 : Iota), Or (Ne (incl_POSet a) (incl_POSet a_1)) (Eq a (the_carrier (incl_POSet a_1))) % 4.47/4.68 Clause #440 (by equality resolution #[436]): ∀ (a : Iota), Eq a (the_carrier (incl_POSet a)) % 4.47/4.68 Clause #447 (by backward contextual literal cutting #[440, 370]): False % 4.47/4.68 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------