%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : NUM393+1 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n021.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:56:25 PM UTC 2025 % Result : Theorem 8.05s 8.25s % Output : Proof 8.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : NUM393+1 : TPTP v9.2.0. Released v3.2.0. % 0.11/0.13 % Command : duper %s % 0.12/0.34 % Computer : n021.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Oct 3 06:53:38 EDT 2025 % 0.12/0.34 % CPUTime : % 8.05/8.25 SZS status Theorem for theBenchmark.p % 8.05/8.25 SZS output start Proof for theBenchmark.p % 8.05/8.25 Clause #6 (by assumption #[]): Eq (∀ (A B : Iota), And (ordinal A) (ordinal B) → Or (ordinal_subset A B) (ordinal_subset B A)) True % 8.05/8.25 Clause #7 (by assumption #[]): Eq (∀ (A B : Iota), Iff (inclusion_comparable A B) (Or (subset A B) (subset B A))) True % 8.05/8.25 Clause #23 (by assumption #[]): Eq (∀ (A B : Iota), And (ordinal A) (ordinal B) → Iff (ordinal_subset A B) (subset A B)) True % 8.05/8.25 Clause #27 (by assumption #[]): Eq (∀ (A B : Iota), inclusion_comparable A B → inclusion_comparable B A) True % 8.05/8.25 Clause #29 (by assumption #[]): Eq (Not (∀ (A : Iota), ordinal A → ∀ (B : Iota), ordinal B → inclusion_comparable A B)) True % 8.05/8.25 Clause #82 (by clausification #[27]): ∀ (a : Iota), Eq (∀ (B : Iota), inclusion_comparable a B → inclusion_comparable B a) True % 8.05/8.25 Clause #83 (by clausification #[82]): ∀ (a a_1 : Iota), Eq (inclusion_comparable a a_1 → inclusion_comparable a_1 a) True % 8.05/8.25 Clause #84 (by clausification #[83]): ∀ (a a_1 : Iota), Or (Eq (inclusion_comparable a a_1) False) (Eq (inclusion_comparable a_1 a) True) % 8.05/8.25 Clause #98 (by clausification #[6]): ∀ (a : Iota), Eq (∀ (B : Iota), And (ordinal a) (ordinal B) → Or (ordinal_subset a B) (ordinal_subset B a)) True % 8.05/8.25 Clause #99 (by clausification #[98]): ∀ (a a_1 : Iota), Eq (And (ordinal a) (ordinal a_1) → Or (ordinal_subset a a_1) (ordinal_subset a_1 a)) True % 8.05/8.25 Clause #100 (by clausification #[99]): ∀ (a a_1 : Iota), % 8.05/8.25 Or (Eq (And (ordinal a) (ordinal a_1)) False) (Eq (Or (ordinal_subset a a_1) (ordinal_subset a_1 a)) True) % 8.05/8.25 Clause #101 (by clausification #[100]): ∀ (a a_1 : Iota), % 8.05/8.25 Or (Eq (Or (ordinal_subset a a_1) (ordinal_subset a_1 a)) True) (Or (Eq (ordinal a) False) (Eq (ordinal a_1) False)) % 8.05/8.25 Clause #102 (by clausification #[101]): ∀ (a a_1 : Iota), % 8.05/8.25 Or (Eq (ordinal a) False) % 8.05/8.25 (Or (Eq (ordinal a_1) False) (Or (Eq (ordinal_subset a a_1) True) (Eq (ordinal_subset a_1 a) True))) % 8.05/8.25 Clause #112 (by clausification #[7]): ∀ (a : Iota), Eq (∀ (B : Iota), Iff (inclusion_comparable a B) (Or (subset a B) (subset B a))) True % 8.05/8.25 Clause #113 (by clausification #[112]): ∀ (a a_1 : Iota), Eq (Iff (inclusion_comparable a a_1) (Or (subset a a_1) (subset a_1 a))) True % 8.05/8.25 Clause #114 (by clausification #[113]): ∀ (a a_1 : Iota), Or (Eq (inclusion_comparable a a_1) True) (Eq (Or (subset a a_1) (subset a_1 a)) False) % 8.05/8.25 Clause #117 (by clausification #[114]): ∀ (a a_1 : Iota), Or (Eq (inclusion_comparable a a_1) True) (Eq (subset a a_1) False) % 8.05/8.25 Clause #121 (by clausification #[29]): Eq (∀ (A : Iota), ordinal A → ∀ (B : Iota), ordinal B → inclusion_comparable A B) False % 8.05/8.25 Clause #122 (by clausification #[121]): ∀ (a : Iota), Eq (Not (ordinal (skS.0 5 a) → ∀ (B : Iota), ordinal B → inclusion_comparable (skS.0 5 a) B)) True % 8.05/8.25 Clause #123 (by clausification #[122]): ∀ (a : Iota), Eq (ordinal (skS.0 5 a) → ∀ (B : Iota), ordinal B → inclusion_comparable (skS.0 5 a) B) False % 8.05/8.25 Clause #124 (by clausification #[123]): ∀ (a : Iota), Eq (ordinal (skS.0 5 a)) True % 8.05/8.25 Clause #125 (by clausification #[123]): ∀ (a : Iota), Eq (∀ (B : Iota), ordinal B → inclusion_comparable (skS.0 5 a) B) False % 8.05/8.25 Clause #129 (by superposition #[124, 102]): ∀ (a a_1 : Iota), % 8.05/8.25 Or (Eq True False) % 8.05/8.25 (Or (Eq (ordinal a) False) % 8.05/8.25 (Or (Eq (ordinal_subset (skS.0 5 a_1) a) True) (Eq (ordinal_subset a (skS.0 5 a_1)) True))) % 8.05/8.25 Clause #170 (by clausification #[125]): ∀ (a a_1 : Iota), Eq (Not (ordinal (skS.0 11 a a_1) → inclusion_comparable (skS.0 5 a) (skS.0 11 a a_1))) True % 8.05/8.25 Clause #171 (by clausification #[170]): ∀ (a a_1 : Iota), Eq (ordinal (skS.0 11 a a_1) → inclusion_comparable (skS.0 5 a) (skS.0 11 a a_1)) False % 8.05/8.25 Clause #172 (by clausification #[171]): ∀ (a a_1 : Iota), Eq (ordinal (skS.0 11 a a_1)) True % 8.05/8.25 Clause #173 (by clausification #[171]): ∀ (a a_1 : Iota), Eq (inclusion_comparable (skS.0 5 a) (skS.0 11 a a_1)) False % 8.05/8.25 Clause #178 (by clausification #[23]): ∀ (a : Iota), Eq (∀ (B : Iota), And (ordinal a) (ordinal B) → Iff (ordinal_subset a B) (subset a B)) True % 8.05/8.25 Clause #179 (by clausification #[178]): ∀ (a a_1 : Iota), Eq (And (ordinal a) (ordinal a_1) → Iff (ordinal_subset a a_1) (subset a a_1)) True % 8.12/8.28 Clause #180 (by clausification #[179]): ∀ (a a_1 : Iota), Or (Eq (And (ordinal a) (ordinal a_1)) False) (Eq (Iff (ordinal_subset a a_1) (subset a a_1)) True) % 8.12/8.28 Clause #181 (by clausification #[180]): ∀ (a a_1 : Iota), % 8.12/8.28 Or (Eq (Iff (ordinal_subset a a_1) (subset a a_1)) True) (Or (Eq (ordinal a) False) (Eq (ordinal a_1) False)) % 8.12/8.28 Clause #183 (by clausification #[181]): ∀ (a a_1 : Iota), % 8.12/8.28 Or (Eq (ordinal a) False) % 8.12/8.28 (Or (Eq (ordinal a_1) False) (Or (Eq (ordinal_subset a a_1) False) (Eq (subset a a_1) True))) % 8.12/8.28 Clause #254 (by superposition #[183, 124]): ∀ (a a_1 : Iota), % 8.12/8.28 Or (Eq (ordinal a) False) % 8.12/8.28 (Or (Eq (ordinal_subset (skS.0 5 a_1) a) False) (Or (Eq (subset (skS.0 5 a_1) a) True) (Eq False True))) % 8.12/8.28 Clause #256 (by superposition #[183, 172]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (ordinal a) False) % 8.12/8.28 (Or (Eq (ordinal_subset (skS.0 11 a_1 a_2) a) False) (Or (Eq (subset (skS.0 11 a_1 a_2) a) True) (Eq False True))) % 8.12/8.28 Clause #269 (by clausification #[129]): ∀ (a a_1 : Iota), % 8.12/8.28 Or (Eq (ordinal a) False) (Or (Eq (ordinal_subset (skS.0 5 a_1) a) True) (Eq (ordinal_subset a (skS.0 5 a_1)) True)) % 8.12/8.28 Clause #272 (by superposition #[269, 172]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (ordinal_subset (skS.0 5 a) (skS.0 11 a_1 a_2)) True) % 8.12/8.28 (Or (Eq (ordinal_subset (skS.0 11 a_1 a_2) (skS.0 5 a)) True) (Eq False True)) % 8.12/8.28 Clause #349 (by clausification #[254]): ∀ (a a_1 : Iota), % 8.12/8.28 Or (Eq (ordinal a) False) (Or (Eq (ordinal_subset (skS.0 5 a_1) a) False) (Eq (subset (skS.0 5 a_1) a) True)) % 8.12/8.28 Clause #352 (by superposition #[349, 172]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (ordinal_subset (skS.0 5 a) (skS.0 11 a_1 a_2)) False) % 8.12/8.28 (Or (Eq (subset (skS.0 5 a) (skS.0 11 a_1 a_2)) True) (Eq False True)) % 8.12/8.28 Clause #372 (by clausification #[256]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (ordinal a) False) % 8.12/8.28 (Or (Eq (ordinal_subset (skS.0 11 a_1 a_2) a) False) (Eq (subset (skS.0 11 a_1 a_2) a) True)) % 8.12/8.28 Clause #373 (by superposition #[372, 124]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (ordinal_subset (skS.0 11 a a_1) (skS.0 5 a_2)) False) % 8.12/8.28 (Or (Eq (subset (skS.0 11 a a_1) (skS.0 5 a_2)) True) (Eq False True)) % 8.12/8.28 Clause #400 (by clausification #[272]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (ordinal_subset (skS.0 5 a) (skS.0 11 a_1 a_2)) True) (Eq (ordinal_subset (skS.0 11 a_1 a_2) (skS.0 5 a)) True) % 8.12/8.28 Clause #514 (by clausification #[352]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (ordinal_subset (skS.0 5 a) (skS.0 11 a_1 a_2)) False) (Eq (subset (skS.0 5 a) (skS.0 11 a_1 a_2)) True) % 8.12/8.28 Clause #563 (by clausification #[373]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (ordinal_subset (skS.0 11 a a_1) (skS.0 5 a_2)) False) (Eq (subset (skS.0 11 a a_1) (skS.0 5 a_2)) True) % 8.12/8.28 Clause #564 (by superposition #[563, 400]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (subset (skS.0 11 a a_1) (skS.0 5 a_2)) True) % 8.12/8.28 (Or (Eq (ordinal_subset (skS.0 5 a_2) (skS.0 11 a a_1)) True) (Eq False True)) % 8.12/8.28 Clause #565 (by clausification #[564]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (subset (skS.0 11 a a_1) (skS.0 5 a_2)) True) (Eq (ordinal_subset (skS.0 5 a_2) (skS.0 11 a a_1)) True) % 8.12/8.28 Clause #566 (by superposition #[565, 514]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (subset (skS.0 11 a a_1) (skS.0 5 a_2)) True) % 8.12/8.28 (Or (Eq True False) (Eq (subset (skS.0 5 a_2) (skS.0 11 a a_1)) True)) % 8.12/8.28 Clause #567 (by clausification #[566]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (subset (skS.0 11 a a_1) (skS.0 5 a_2)) True) (Eq (subset (skS.0 5 a_2) (skS.0 11 a a_1)) True) % 8.12/8.28 Clause #574 (by superposition #[567, 117]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (subset (skS.0 11 a a_1) (skS.0 5 a_2)) True) % 8.12/8.28 (Or (Eq (inclusion_comparable (skS.0 5 a_2) (skS.0 11 a a_1)) True) (Eq True False)) % 8.12/8.28 Clause #576 (by clausification #[574]): ∀ (a a_1 a_2 : Iota), % 8.12/8.28 Or (Eq (subset (skS.0 11 a a_1) (skS.0 5 a_2)) True) (Eq (inclusion_comparable (skS.0 5 a_2) (skS.0 11 a a_1)) True) % 8.12/8.28 Clause #577 (by superposition #[576, 173]): ∀ (a a_1 : Iota), Or (Eq (subset (skS.0 11 a a_1) (skS.0 5 a)) True) (Eq True False) % 8.12/8.28 Clause #580 (by clausification #[577]): ∀ (a a_1 : Iota), Eq (subset (skS.0 11 a a_1) (skS.0 5 a)) True % 8.12/8.28 Clause #583 (by superposition #[580, 117]): ∀ (a a_1 : Iota), Or (Eq (inclusion_comparable (skS.0 11 a a_1) (skS.0 5 a)) True) (Eq True False) % 8.12/8.28 Clause #585 (by clausification #[583]): ∀ (a a_1 : Iota), Eq (inclusion_comparable (skS.0 11 a a_1) (skS.0 5 a)) True % 8.12/8.28 Clause #586 (by superposition #[585, 84]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (inclusion_comparable (skS.0 5 a) (skS.0 11 a a_1)) True) % 8.12/8.28 Clause #592 (by clausification #[586]): ∀ (a a_1 : Iota), Eq (inclusion_comparable (skS.0 5 a) (skS.0 11 a a_1)) True % 8.12/8.28 Clause #593 (by superposition #[592, 173]): Eq True False % 8.12/8.28 Clause #596 (by clausification #[593]): False % 8.12/8.28 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------