%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SET803+4 : TPTP v9.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n025.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.97s 10.13s % Output : Proof 9.97s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SET803+4 : TPTP v9.2.0. Released v3.2.0. % 0.12/0.14 % Command : duper %s % 0.15/0.35 % Computer : n025.cluster.edu % 0.15/0.35 % Model : x86_64 x86_64 % 0.15/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.35 % Memory : 8042.1875MB % 0.15/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.35 % CPULimit : 300 % 0.15/0.35 % WCLimit : 300 % 0.15/0.35 % DateTime : Thu Oct 2 13:48:08 EDT 2025 % 0.15/0.36 % CPUTime : % 9.97/10.13 SZS status Theorem for theBenchmark.p % 9.97/10.13 SZS output start Proof for theBenchmark.p % 9.97/10.13 Clause #4 (by assumption #[]): Eq (∀ (R E M : Iota), Iff (greatest M R E) (And (member M E) (∀ (X : Iota), member X E → apply R X M))) True % 9.97/10.13 Clause #6 (by assumption #[]): Eq (∀ (R E M : Iota), Iff (max M R E) (And (member M E) (∀ (X : Iota), And (member X E) (apply R M X) → Eq M X))) True % 9.97/10.13 Clause #10 (by assumption #[]): Eq % 9.97/10.13 (Not % 9.97/10.13 (∀ (R E : Iota), % 9.97/10.13 order R E → % 9.97/10.13 ∀ (M1 M2 : Iota), And (And (max M1 R E) (max M2 R E)) (Ne M1 M2) → Not (Exists fun M => greatest M R E))) % 9.97/10.13 True % 9.97/10.13 Clause #33 (by clausification #[10]): Eq % 9.97/10.13 (∀ (R E : Iota), % 9.97/10.13 order R E → ∀ (M1 M2 : Iota), And (And (max M1 R E) (max M2 R E)) (Ne M1 M2) → Not (Exists fun M => greatest M R E)) % 9.97/10.13 False % 9.97/10.13 Clause #34 (by clausification #[33]): ∀ (a : Iota), % 9.97/10.13 Eq % 9.97/10.13 (Not % 9.97/10.13 (∀ (E : Iota), % 9.97/10.13 order (skS.0 2 a) E → % 9.97/10.13 ∀ (M1 M2 : Iota), % 9.97/10.13 And (And (max M1 (skS.0 2 a) E) (max M2 (skS.0 2 a) E)) (Ne M1 M2) → % 9.97/10.13 Not (Exists fun M => greatest M (skS.0 2 a) E))) % 9.97/10.13 True % 9.97/10.13 Clause #35 (by clausification #[34]): ∀ (a : Iota), % 9.97/10.13 Eq % 9.97/10.13 (∀ (E : Iota), % 9.97/10.13 order (skS.0 2 a) E → % 9.97/10.13 ∀ (M1 M2 : Iota), % 9.97/10.13 And (And (max M1 (skS.0 2 a) E) (max M2 (skS.0 2 a) E)) (Ne M1 M2) → % 9.97/10.13 Not (Exists fun M => greatest M (skS.0 2 a) E)) % 9.97/10.13 False % 9.97/10.13 Clause #36 (by clausification #[35]): ∀ (a a_1 : Iota), % 9.97/10.13 Eq % 9.97/10.13 (Not % 9.97/10.13 (order (skS.0 2 a) (skS.0 3 a a_1) → % 9.97/10.13 ∀ (M1 M2 : Iota), % 9.97/10.13 And (And (max M1 (skS.0 2 a) (skS.0 3 a a_1)) (max M2 (skS.0 2 a) (skS.0 3 a a_1))) (Ne M1 M2) → % 9.97/10.13 Not (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1)))) % 9.97/10.13 True % 9.97/10.13 Clause #37 (by clausification #[36]): ∀ (a a_1 : Iota), % 9.97/10.13 Eq % 9.97/10.13 (order (skS.0 2 a) (skS.0 3 a a_1) → % 9.97/10.13 ∀ (M1 M2 : Iota), % 9.97/10.13 And (And (max M1 (skS.0 2 a) (skS.0 3 a a_1)) (max M2 (skS.0 2 a) (skS.0 3 a a_1))) (Ne M1 M2) → % 9.97/10.13 Not (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.13 False % 9.97/10.13 Clause #39 (by clausification #[37]): ∀ (a a_1 : Iota), % 9.97/10.13 Eq % 9.97/10.13 (∀ (M1 M2 : Iota), % 9.97/10.13 And (And (max M1 (skS.0 2 a) (skS.0 3 a a_1)) (max M2 (skS.0 2 a) (skS.0 3 a a_1))) (Ne M1 M2) → % 9.97/10.13 Not (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.13 False % 9.97/10.13 Clause #91 (by clausification #[6]): ∀ (a : Iota), % 9.97/10.13 Eq (∀ (E M : Iota), Iff (max M a E) (And (member M E) (∀ (X : Iota), And (member X E) (apply a M X) → Eq M X))) True % 9.97/10.13 Clause #92 (by clausification #[91]): ∀ (a a_1 : Iota), % 9.97/10.13 Eq (∀ (M : Iota), Iff (max M a a_1) (And (member M a_1) (∀ (X : Iota), And (member X a_1) (apply a M X) → Eq M X))) % 9.97/10.13 True % 9.97/10.13 Clause #93 (by clausification #[92]): ∀ (a a_1 a_2 : Iota), % 9.97/10.13 Eq (Iff (max a a_1 a_2) (And (member a a_2) (∀ (X : Iota), And (member X a_2) (apply a_1 a X) → Eq a X))) True % 9.97/10.13 Clause #95 (by clausification #[93]): ∀ (a a_1 a_2 : Iota), % 9.97/10.13 Or (Eq (max a a_1 a_2) False) % 9.97/10.13 (Eq (And (member a a_2) (∀ (X : Iota), And (member X a_2) (apply a_1 a X) → Eq a X)) True) % 9.97/10.13 Clause #108 (by clausification #[95]): ∀ (a a_1 a_2 : Iota), % 9.97/10.13 Or (Eq (max a a_1 a_2) False) (Eq (∀ (X : Iota), And (member X a_2) (apply a_1 a X) → Eq a X) True) % 9.97/10.13 Clause #109 (by clausification #[95]): ∀ (a a_1 a_2 : Iota), Or (Eq (max a a_1 a_2) False) (Eq (member a a_2) True) % 9.97/10.13 Clause #110 (by clausification #[108]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (max a a_1 a_2) False) (Eq (And (member a_3 a_2) (apply a_1 a a_3) → Eq a a_3) True) % 9.97/10.13 Clause #111 (by clausification #[110]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.13 Or (Eq (max a a_1 a_2) False) (Or (Eq (And (member a_3 a_2) (apply a_1 a a_3)) False) (Eq (Eq a a_3) True)) % 9.97/10.13 Clause #112 (by clausification #[111]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.13 Or (Eq (max 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 a_3) False))) % 9.97/10.13 Clause #113 (by clausification #[112]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.13 Or (Eq (max a a_1 a_2) False) (Or (Eq (member a_3 a_2) False) (Or (Eq (apply a_1 a a_3) False) (Eq a a_3))) % 9.97/10.13 Clause #147 (by clausification #[4]): ∀ (a : Iota), Eq (∀ (E M : Iota), Iff (greatest M a E) (And (member M E) (∀ (X : Iota), member X E → apply a X M))) True % 9.97/10.15 Clause #148 (by clausification #[147]): ∀ (a a_1 : Iota), % 9.97/10.15 Eq (∀ (M : Iota), Iff (greatest M a a_1) (And (member M a_1) (∀ (X : Iota), member X a_1 → apply a X M))) True % 9.97/10.15 Clause #149 (by clausification #[148]): ∀ (a a_1 a_2 : Iota), % 9.97/10.15 Eq (Iff (greatest a a_1 a_2) (And (member a a_2) (∀ (X : Iota), member X a_2 → apply a_1 X a))) True % 9.97/10.15 Clause #151 (by clausification #[149]): ∀ (a a_1 a_2 : Iota), % 9.97/10.15 Or (Eq (greatest a a_1 a_2) False) (Eq (And (member a a_2) (∀ (X : Iota), member X a_2 → apply a_1 X a)) True) % 9.97/10.15 Clause #181 (by clausification #[151]): ∀ (a a_1 a_2 : Iota), Or (Eq (greatest a a_1 a_2) False) (Eq (∀ (X : Iota), member X a_2 → apply a_1 X a) True) % 9.97/10.15 Clause #182 (by clausification #[151]): ∀ (a a_1 a_2 : Iota), Or (Eq (greatest a a_1 a_2) False) (Eq (member a a_2) True) % 9.97/10.15 Clause #183 (by clausification #[181]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq (greatest a a_1 a_2) False) (Eq (member a_3 a_2 → apply a_1 a_3 a) True) % 9.97/10.15 Clause #184 (by clausification #[183]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.15 Or (Eq (greatest a a_1 a_2) False) (Or (Eq (member a_3 a_2) False) (Eq (apply a_1 a_3 a) True)) % 9.97/10.15 Clause #219 (by clausification #[39]): ∀ (a a_1 a_2 : Iota), % 9.97/10.15 Eq % 9.97/10.15 (Not % 9.97/10.15 (∀ (M2 : Iota), % 9.97/10.15 And (And (max (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) (max M2 (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.15 (Ne (skS.0 18 a a_1 a_2) M2) → % 9.97/10.15 Not (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1)))) % 9.97/10.15 True % 9.97/10.15 Clause #220 (by clausification #[219]): ∀ (a a_1 a_2 : Iota), % 9.97/10.15 Eq % 9.97/10.15 (∀ (M2 : Iota), % 9.97/10.15 And (And (max (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) (max M2 (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.15 (Ne (skS.0 18 a a_1 a_2) M2) → % 9.97/10.15 Not (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.15 False % 9.97/10.15 Clause #221 (by clausification #[220]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.15 Eq % 9.97/10.15 (Not % 9.97/10.15 (And % 9.97/10.15 (And (max (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) % 9.97/10.15 (max (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.15 (Ne (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) → % 9.97/10.15 Not (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1)))) % 9.97/10.15 True % 9.97/10.15 Clause #222 (by clausification #[221]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.15 Eq % 9.97/10.15 (And % 9.97/10.15 (And (max (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) % 9.97/10.15 (max (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.15 (Ne (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3)) → % 9.97/10.15 Not (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.15 False % 9.97/10.15 Clause #223 (by clausification #[222]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.15 Eq % 9.97/10.15 (And % 9.97/10.15 (And (max (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) % 9.97/10.15 (max (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.15 (Ne (skS.0 18 a a_1 a_2) (skS.0 19 a a_1 a_2 a_3))) % 9.97/10.15 True % 9.97/10.15 Clause #224 (by clausification #[222]): ∀ (a a_1 : Iota), Eq (Not (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1))) False % 9.97/10.15 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.97/10.15 Clause #226 (by clausification #[223]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.15 Eq % 9.97/10.15 (And (max (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) % 9.97/10.15 (max (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1))) % 9.97/10.15 True % 9.97/10.15 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.97/10.15 Clause #228 (by clausification #[224]): ∀ (a a_1 : Iota), Eq (Exists fun M => greatest M (skS.0 2 a) (skS.0 3 a a_1)) True % 9.97/10.15 Clause #229 (by clausification #[228]): ∀ (a a_1 a_2 : Iota), Eq (greatest (skS.0 20 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) True % 9.97/10.15 Clause #230 (by superposition #[229, 184]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.15 Or (Eq True False) % 9.97/10.15 (Or (Eq (member a (skS.0 3 a_1 a_2)) False) (Eq (apply (skS.0 2 a_1) a (skS.0 20 a_1 a_2 a_3)) True)) % 9.97/10.15 Clause #231 (by superposition #[229, 182]): ∀ (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.97/10.18 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.97/10.18 Clause #364 (by clausification #[230]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.18 Or (Eq (member a (skS.0 3 a_1 a_2)) False) (Eq (apply (skS.0 2 a_1) a (skS.0 20 a_1 a_2 a_3)) True) % 9.97/10.18 Clause #838 (by clausification #[226]): ∀ (a a_1 a_2 a_3 : Iota), Eq (max (skS.0 19 a a_1 a_2 a_3) (skS.0 2 a) (skS.0 3 a a_1)) True % 9.97/10.18 Clause #839 (by clausification #[226]): ∀ (a a_1 a_2 : Iota), Eq (max (skS.0 18 a a_1 a_2) (skS.0 2 a) (skS.0 3 a a_1)) True % 9.97/10.18 Clause #840 (by superposition #[838, 113]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.97/10.18 Or (Eq True False) % 9.97/10.18 (Or (Eq (member a (skS.0 3 a_1 a_2)) False) % 9.97/10.18 (Or (Eq (apply (skS.0 2 a_1) (skS.0 19 a_1 a_2 a_3 a_4) a) False) (Eq (skS.0 19 a_1 a_2 a_3 a_4) a))) % 9.97/10.18 Clause #841 (by superposition #[838, 109]): ∀ (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.97/10.18 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.97/10.18 Clause #844 (by superposition #[842, 364]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.97/10.18 Or (Eq True False) (Eq (apply (skS.0 2 a) (skS.0 19 a a_1 a_2 a_3) (skS.0 20 a a_1 a_4)) True) % 9.97/10.18 Clause #862 (by superposition #[839, 113]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.18 Or (Eq True False) % 9.97/10.18 (Or (Eq (member a (skS.0 3 a_1 a_2)) False) % 9.97/10.18 (Or (Eq (apply (skS.0 2 a_1) (skS.0 18 a_1 a_2 a_3) a) False) (Eq (skS.0 18 a_1 a_2 a_3) a))) % 9.97/10.18 Clause #863 (by superposition #[839, 109]): ∀ (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.97/10.18 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.97/10.18 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 18 a a_1 a_2) (skS.0 20 a a_1 a_3)) True) % 9.97/10.18 Clause #886 (by clausification #[866]): ∀ (a a_1 a_2 a_3 : Iota), Eq (apply (skS.0 2 a) (skS.0 18 a a_1 a_2) (skS.0 20 a a_1 a_3)) True % 9.97/10.18 Clause #887 (by clausification #[844]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (apply (skS.0 2 a) (skS.0 19 a a_1 a_2 a_3) (skS.0 20 a a_1 a_4)) True % 9.97/10.18 Clause #889 (by clausification #[862]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.18 Or (Eq (member a (skS.0 3 a_1 a_2)) False) % 9.97/10.18 (Or (Eq (apply (skS.0 2 a_1) (skS.0 18 a_1 a_2 a_3) a) False) (Eq (skS.0 18 a_1 a_2 a_3) a)) % 9.97/10.18 Clause #890 (by superposition #[889, 232]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.18 Or (Eq (apply (skS.0 2 a) (skS.0 18 a a_1 a_2) (skS.0 20 a a_1 a_3)) False) % 9.97/10.18 (Or (Eq (skS.0 18 a a_1 a_2) (skS.0 20 a a_1 a_3)) (Eq False True)) % 9.97/10.18 Clause #921 (by clausification #[840]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.97/10.18 Or (Eq (member a (skS.0 3 a_1 a_2)) False) % 9.97/10.18 (Or (Eq (apply (skS.0 2 a_1) (skS.0 19 a_1 a_2 a_3 a_4) a) False) (Eq (skS.0 19 a_1 a_2 a_3 a_4) a)) % 9.97/10.18 Clause #926 (by superposition #[921, 864]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.97/10.18 Or (Eq (apply (skS.0 2 a) (skS.0 19 a a_1 a_2 a_3) (skS.0 18 a a_1 a_4)) False) % 9.97/10.18 (Or (Eq (skS.0 19 a a_1 a_2 a_3) (skS.0 18 a a_1 a_4)) (Eq False True)) % 9.97/10.18 Clause #999 (by clausification #[890]): ∀ (a a_1 a_2 a_3 : Iota), % 9.97/10.18 Or (Eq (apply (skS.0 2 a) (skS.0 18 a a_1 a_2) (skS.0 20 a a_1 a_3)) False) % 9.97/10.18 (Eq (skS.0 18 a a_1 a_2) (skS.0 20 a a_1 a_3)) % 9.97/10.18 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.97/10.18 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.97/10.18 Clause #1010 (by superposition #[1001, 887]): ∀ (a a_1 a_2 a_3 a_4 : Iota), Eq (apply (skS.0 2 a) (skS.0 19 a a_1 a_2 a_3) (skS.0 18 a a_1 a_4)) True % 9.97/10.18 Clause #1232 (by clausification #[926]): ∀ (a a_1 a_2 a_3 a_4 : Iota), % 9.97/10.18 Or (Eq (apply (skS.0 2 a) (skS.0 19 a a_1 a_2 a_3) (skS.0 18 a a_1 a_4)) False) % 9.97/10.18 (Eq (skS.0 19 a a_1 a_2 a_3) (skS.0 18 a a_1 a_4)) % 9.97/10.18 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.97/10.18 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.97/10.19 Clause #1236 (by backward contextual literal cutting #[1235, 227]): False % 9.97/10.19 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------