%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET804+4 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n011.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:00:31 PM UTC 2025 % Result : Theorem 9.68s 9.88s % Output : Proof 9.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SET804+4 : TPTP v9.2.0. Released v3.2.0. % 0.07/0.13 % Command : duper %s % 0.13/0.34 % Computer : n011.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 : Thu Oct 2 14:12:08 EDT 2025 % 0.13/0.34 % CPUTime : % 9.68/9.88 SZS status Theorem for theBenchmark.p % 9.68/9.88 SZS output start Proof for theBenchmark.p % 9.68/9.88 Clause #5 (by assumption #[]): Eq (∀ (R E M : Iota), Iff (least M R E) (And (member M E) (∀ (X : Iota), member X E → apply R M X))) True % 9.68/9.88 Clause #7 (by assumption #[]): Eq (∀ (R E M : Iota), Iff (min M R E) (And (member M E) (∀ (X : Iota), And (member X E) (apply R X M) → Eq M X))) True % 9.68/9.88 Clause #10 (by assumption #[]): Eq % 9.68/9.88 (Not % 9.68/9.88 (∀ (R E : Iota), % 9.68/9.88 order R E → ∀ (M1 M2 : Iota), And (And (min M1 R E) (min M2 R E)) (Ne M1 M2) → Not (Exists fun M => least M R E))) % 9.68/9.88 True % 9.68/9.88 Clause #33 (by clausification #[10]): Eq % 9.68/9.88 (∀ (R E : Iota), % 9.68/9.88 order R E → ∀ (M1 M2 : Iota), And (And (min M1 R E) (min M2 R E)) (Ne M1 M2) → Not (Exists fun M => least M R E)) % 9.68/9.88 False % 9.68/9.88 Clause #34 (by clausification #[33]): ∀ (a : Iota), % 9.68/9.88 Eq % 9.68/9.88 (Not % 9.68/9.88 (∀ (E : Iota), % 9.68/9.88 order (skS.0 2 a) E → % 9.68/9.88 ∀ (M1 M2 : Iota), % 9.68/9.88 And (And (min M1 (skS.0 2 a) E) (min M2 (skS.0 2 a) E)) (Ne M1 M2) → % 9.68/9.88 Not (Exists fun M => least M (skS.0 2 a) E))) % 9.68/9.88 True % 9.68/9.88 Clause #35 (by clausification #[34]): ∀ (a : Iota), % 9.68/9.88 Eq % 9.68/9.88 (∀ (E : Iota), % 9.68/9.88 order (skS.0 2 a) E → % 9.68/9.88 ∀ (M1 M2 : Iota), % 9.68/9.88 And (And (min M1 (skS.0 2 a) E) (min M2 (skS.0 2 a) E)) (Ne M1 M2) → % 9.68/9.88 Not (Exists fun M => least M (skS.0 2 a) E)) % 9.68/9.88 False % 9.68/9.88 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 9.68/9.88 Eq % 9.68/9.88 (Not % 9.68/9.88 (order (skS.0 2 a) (skS.0 3 a a_1) → % 9.68/9.88 ∀ (M1 M2 : Iota), % 9.68/9.88 And (And (min M1 (skS.0 2 a) (skS.0 3 a a_1)) (min M2 (skS.0 2 a) (skS.0 3 a a_1))) (Ne M1 M2) → % 9.68/9.88 Not (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1)))) % 9.68/9.88 True % 9.68/9.88 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 9.68/9.88 Eq % 9.68/9.88 (order (skS.0 2 a) (skS.0 3 a a_1) → % 9.68/9.88 ∀ (M1 M2 : Iota), % 9.68/9.88 And (And (min M1 (skS.0 2 a) (skS.0 3 a a_1)) (min M2 (skS.0 2 a) (skS.0 3 a a_1))) (Ne M1 M2) → % 9.68/9.88 Not (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.88 False % 9.68/9.88 Clause #39 (by clausification #[37]): ∀ (a a_1 : Iota), % 9.68/9.88 Eq % 9.68/9.88 (∀ (M1 M2 : Iota), % 9.68/9.88 And (And (min M1 (skS.0 2 a) (skS.0 3 a a_1)) (min M2 (skS.0 2 a) (skS.0 3 a a_1))) (Ne M1 M2) → % 9.68/9.88 Not (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.88 False % 9.68/9.88 Clause #68 (by clausification #[7]): ∀ (a : Iota), % 9.68/9.88 Eq (∀ (E M : Iota), Iff (min M a E) (And (member M E) (∀ (X : Iota), And (member X E) (apply a X M) → Eq M X))) True % 9.68/9.88 Clause #69 (by clausification #[68]): ∀ (a a_1 : Iota), % 9.68/9.88 Eq (∀ (M : Iota), Iff (min M a a_1) (And (member M a_1) (∀ (X : Iota), And (member X a_1) (apply a X M) → Eq M X))) % 9.68/9.88 True % 9.68/9.88 Clause #70 (by clausification #[69]): ∀ (a a_1 a_2 : Iota), % 9.68/9.88 Eq (Iff (min a a_1 a_2) (And (member a a_2) (∀ (X : Iota), And (member X a_2) (apply a_1 X a) → Eq a X))) True % 9.68/9.88 Clause #72 (by clausification #[70]): ∀ (a a_1 a_2 : Iota), % 9.68/9.88 Or (Eq (min a a_1 a_2) False) % 9.68/9.88 (Eq (And (member a a_2) (∀ (X : Iota), And (member X a_2) (apply a_1 X a) → Eq a X)) True) % 9.68/9.88 Clause #85 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), % 9.68/9.88 Or (Eq (min a a_1 a_2) False) (Eq (∀ (X : Iota), And (member X a_2) (apply a_1 X a) → Eq a X) True) % 9.68/9.88 Clause #86 (by clausification #[72]): ∀ (a a_1 a_2 : Iota), Or (Eq (min a a_1 a_2) False) (Eq (member a a_2) True) % 9.68/9.88 Clause #87 (by clausification #[85]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (min a a_1 a_2) False) (Eq (And (member a_3 a_2) (apply a_1 a_3 a) → Eq a a_3) True) % 9.68/9.88 Clause #88 (by clausification #[87]): ∀ (a a_1 a_2 a_3 : Iota), % 9.68/9.88 Or (Eq (min a a_1 a_2) False) (Or (Eq (And (member a_3 a_2) (apply a_1 a_3 a)) False) (Eq (Eq a a_3) True)) % 9.68/9.88 Clause #89 (by clausification #[88]): ∀ (a a_1 a_2 a_3 : Iota), % 9.68/9.88 Or (Eq (min a a_1 a_2) False) (Or (Eq (Eq a a_3) True) (Or (Eq (member a_3 a_2) False) (Eq (apply a_1 a_3 a) False))) % 9.68/9.88 Clause #90 (by clausification #[89]): ∀ (a a_1 a_2 a_3 : Iota), % 9.68/9.88 Or (Eq (min a a_1 a_2) False) (Or (Eq (member a_3 a_2) False) (Or (Eq (apply a_1 a_3 a) False) (Eq a a_3))) % 9.68/9.88 Clause #128 (by clausification #[5]): ∀ (a : Iota), Eq (∀ (E M : Iota), Iff (least M a E) (And (member M E) (∀ (X : Iota), member X E → apply a M X))) True % 9.68/9.91 Clause #129 (by clausification #[128]): ∀ (a a_1 : Iota), % 9.68/9.91 Eq (∀ (M : Iota), Iff (least M a a_1) (And (member M a_1) (∀ (X : Iota), member X a_1 → apply a M X))) True % 9.68/9.91 Clause #130 (by clausification #[129]): ∀ (a a_1 a_2 : Iota), Eq (Iff (least a a_1 a_2) (And (member a a_2) (∀ (X : Iota), member X a_2 → apply a_1 a X))) True % 9.68/9.91 Clause #132 (by clausification #[130]): ∀ (a a_1 a_2 : Iota), % 9.68/9.91 Or (Eq (least a a_1 a_2) False) (Eq (And (member a a_2) (∀ (X : Iota), member X a_2 → apply a_1 a X)) True) % 9.68/9.91 Clause #143 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), Or (Eq (least a a_1 a_2) False) (Eq (∀ (X : Iota), member X a_2 → apply a_1 a X) True) % 9.68/9.91 Clause #144 (by clausification #[132]): ∀ (a a_1 a_2 : Iota), Or (Eq (least a a_1 a_2) False) (Eq (member a a_2) True) % 9.68/9.91 Clause #145 (by clausification #[143]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (least a a_1 a_2) False) (Eq (member a_3 a_2 → apply a_1 a a_3) True) % 9.68/9.91 Clause #146 (by clausification #[145]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (least a a_1 a_2) False) (Or (Eq (member a_3 a_2) False) (Eq (apply a_1 a a_3) True)) % 9.68/9.91 Clause #219 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 9.68/9.91 Eq % 9.68/9.91 (Not % 9.68/9.91 (∀ (M2 : Iota), % 9.68/9.91 And (And (min (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) (min M2 (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.91 (Ne (skS.0 18 a a_1 a_2) M2) → % 9.68/9.91 Not (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1)))) % 9.68/9.91 True % 9.68/9.91 Clause #220 (by clausification #[219]): ∀ (a a_1 a_2 : Iota), % 9.68/9.91 Eq % 9.68/9.91 (∀ (M2 : Iota), % 9.68/9.91 And (And (min (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) (min M2 (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.91 (Ne (skS.0 18 a a_1 a_2) M2) → % 9.68/9.91 Not (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.91 False % 9.68/9.91 Clause #221 (by clausification #[220]): ∀ (a a_1 a_2 a_3 : Iota), % 9.68/9.91 Eq % 9.68/9.91 (Not % 9.68/9.91 (And % 9.68/9.91 (And (min (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) % 9.68/9.91 (min (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.91 (Ne (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) → % 9.68/9.91 Not (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1)))) % 9.68/9.91 True % 9.68/9.91 Clause #222 (by clausification #[221]): ∀ (a a_1 a_2 a_3 : Iota), % 9.68/9.91 Eq % 9.68/9.91 (And % 9.68/9.91 (And (min (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) % 9.68/9.91 (min (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.91 (Ne (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) → % 9.68/9.91 Not (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.91 False % 9.68/9.91 Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 a_3 : Iota), % 9.68/9.91 Eq % 9.68/9.91 (And % 9.68/9.91 (And (min (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) % 9.68/9.91 (min (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.91 (Ne (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3))) % 9.68/9.91 True % 9.68/9.91 Clause #224 (by clausification #[222]): ∀ (a a_1 : Iota), Eq (Not (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1))) False % 9.68/9.91 Clause #225 (by clausification #[223]): ∀ (a a_1 a_2 a_3 : Iota), Eq (Ne (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) True % 9.68/9.91 Clause #226 (by clausification #[223]): ∀ (a a_1 a_2 a_3 : Iota), % 9.68/9.91 Eq % 9.68/9.91 (And (min (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) % 9.68/9.91 (min (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1))) % 9.68/9.91 True % 9.68/9.91 Clause #227 (by clausification #[225]): ∀ (a a_1 a_2 a_3 : Iota), Ne (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3) % 9.68/9.91 Clause #228 (by clausification #[224]): ∀ (a a_1 : Iota), Eq (Exists fun M => least M (skS.0 2 a) (skS.0 3 a a_1)) True % 9.68/9.91 Clause #229 (by clausification #[228]): ∀ (a a_1 a_2 : Iota), Eq (least (skS.0 20 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) True % 9.68/9.91 Clause #230 (by superposition #[229, 146]): ∀ (a a_1 a_2 a_3 : Iota), % 9.68/9.91 Or (Eq True False) % 9.68/9.91 (Or (Eq (member a (skS.0 3 a_1 a_2)) False) (Eq (apply (skS.0 2 a_1) (skS.0 20 a_1 a_2 a_3) a) True)) % 9.68/9.91 Clause #231 (by superposition #[229, 144]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (member (skS.0 20 a a_1 a_2) (skS.0 3 a a_1)) True) % 9.68/9.91 Clause #232 (by clausification #[231]): ∀ (a a_1 a_2 : Iota), Eq (member (skS.0 20 a a_1 a_2) (skS.0 3 a a_1)) True % 9.76/9.93 Clause #364 (by clausification #[230]): ∀ (a a_1 a_2 a_3 : Iota), % 9.76/9.93 Or (Eq (member a (skS.0 3 a_1 a_2)) False) (Eq (apply (skS.0 2 a_1) (skS.0 20 a_1 a_2 a_3) a) True) % 9.76/9.93 Clause #838 (by clausification #[226]): ∀ (a a_1 a_2 a_3 : Iota), Eq (min (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1)) True % 9.76/9.93 Clause #839 (by clausification #[226]): ∀ (a a_1 a_2 : Iota), Eq (min (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) True % 9.76/9.93 Clause #840 (by superposition #[838, 90]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.76/9.93 Or (Eq True False) % 9.76/9.93 (Or (Eq (member a (skS.0 3 a_1 a_2)) False) % 9.76/9.93 (Or (Eq (apply (skS.0 2 a_1) a (skS.0 19 a_1 a_2 a_3 a_4)) False) (Eq (skS.0 19 a_1 a_2 a_3 a_4) a))) % 9.76/9.93 Clause #841 (by superposition #[838, 86]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (member (skS.0 19 a a_1 a_2 a_3) (skS.0 3 a a_1)) True) % 9.76/9.93 Clause #842 (by clausification #[841]): ∀ (a a_1 a_2 a_3 : Iota), Eq (member (skS.0 19 a a_1 a_2 a_3) (skS.0 3 a a_1)) True % 9.76/9.93 Clause #844 (by superposition #[842, 364]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.76/9.93 Or (Eq True False) (Eq (apply (skS.0 2 a) (skS.0 20 a a_1 a_2) (skS.0 19 a a_1 a_3 a_4)) True) % 9.76/9.93 Clause #862 (by superposition #[839, 90]): ∀ (a a_1 a_2 a_3 : Iota), % 9.76/9.93 Or (Eq True False) % 9.76/9.93 (Or (Eq (member a (skS.0 3 a_1 a_2)) False) % 9.76/9.93 (Or (Eq (apply (skS.0 2 a_1) a (skS.0 18 a_1 a_2 a_3)) False) (Eq (skS.0 18 a_1 a_2 a_3) a))) % 9.76/9.93 Clause #863 (by superposition #[839, 86]): ∀ (a a_1 a_2 : Iota), Or (Eq True False) (Eq (member (skS.0 18 a a_1 a_2) (skS.0 3 a a_1)) True) % 9.76/9.93 Clause #864 (by clausification #[863]): ∀ (a a_1 a_2 : Iota), Eq (member (skS.0 18 a a_1 a_2) (skS.0 3 a a_1)) True % 9.76/9.93 Clause #866 (by superposition #[864, 364]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Eq (apply (skS.0 2 a) (skS.0 20 a a_1 a_2) (skS.0 18 a a_1 a_3)) True) % 9.76/9.93 Clause #886 (by clausification #[866]): ∀ (a a_1 a_2 a_3 : Iota), Eq (apply (skS.0 2 a) (skS.0 20 a a_1 a_2) (skS.0 18 a a_1 a_3)) True % 9.76/9.93 Clause #887 (by clausification #[844]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (apply (skS.0 2 a) (skS.0 20 a a_1 a_2) (skS.0 19 a a_1 a_3 a_4)) True % 9.76/9.93 Clause #889 (by clausification #[862]): ∀ (a a_1 a_2 a_3 : Iota), % 9.76/9.93 Or (Eq (member a (skS.0 3 a_1 a_2)) False) % 9.76/9.93 (Or (Eq (apply (skS.0 2 a_1) a (skS.0 18 a_1 a_2 a_3)) False) (Eq (skS.0 18 a_1 a_2 a_3) a)) % 9.76/9.93 Clause #890 (by superposition #[889, 232]): ∀ (a a_1 a_2 a_3 : Iota), % 9.76/9.93 Or (Eq (apply (skS.0 2 a) (skS.0 20 a a_1 a_2) (skS.0 18 a a_1 a_3)) False) % 9.76/9.93 (Or (Eq (skS.0 18 a a_1 a_3) (skS.0 20 a a_1 a_2)) (Eq False True)) % 9.76/9.93 Clause #921 (by clausification #[840]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.76/9.93 Or (Eq (member a (skS.0 3 a_1 a_2)) False) % 9.76/9.93 (Or (Eq (apply (skS.0 2 a_1) a (skS.0 19 a_1 a_2 a_3 a_4)) False) (Eq (skS.0 19 a_1 a_2 a_3 a_4) a)) % 9.76/9.93 Clause #926 (by superposition #[921, 864]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.76/9.93 Or (Eq (apply (skS.0 2 a) (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_3 a_4)) False) % 9.76/9.93 (Or (Eq (skS.0 19 a a_1 a_3 a_4) (skS.0 18 a a_1 a_2)) (Eq False True)) % 9.76/9.93 Clause #999 (by clausification #[890]): ∀ (a a_1 a_2 a_3 : Iota), % 9.76/9.93 Or (Eq (apply (skS.0 2 a) (skS.0 20 a a_1 a_2) (skS.0 18 a a_1 a_3)) False) % 9.76/9.93 (Eq (skS.0 18 a a_1 a_3) (skS.0 20 a a_1 a_2)) % 9.76/9.93 Clause #1000 (by superposition #[999, 886]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (skS.0 18 a a_1 a_2) (skS.0 20 a a_1 a_3)) (Eq False True) % 9.76/9.93 Clause #1001 (by clausification #[1000]): ∀ (a a_1 a_2 a_3 : Iota), Eq (skS.0 18 a a_1 a_2) (skS.0 20 a a_1 a_3) % 9.76/9.93 Clause #1010 (by superposition #[1001, 887]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (apply (skS.0 2 a) (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_3 a_4)) True % 9.76/9.93 Clause #1232 (by clausification #[926]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.76/9.93 Or (Eq (apply (skS.0 2 a) (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_3 a_4)) False) % 9.76/9.93 (Eq (skS.0 19 a a_1 a_3 a_4) (skS.0 18 a a_1 a_2)) % 9.76/9.93 Clause #1233 (by superposition #[1232, 1010]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Or (Eq (skS.0 19 a a_1 a_2 a_3) (skS.0 18 a a_1 a_4)) (Eq False True) % 9.76/9.93 Clause #1235 (by clausification #[1233]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (skS.0 19 a a_1 a_2 a_3) (skS.0 18 a a_1 a_4) % 9.76/9.94 Clause #1236 (by backward contextual literal cutting #[1235, 227]): False % 9.76/9.94 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------