%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU656^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n020.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:02:09 PM UTC 2025 % Result : Theorem 69.56s 69.75s % Output : Proof 70.37s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU656^2 : TPTP v9.2.0. Released v3.7.0. % 0.07/0.13 % Command : duper %s % 0.14/0.35 % Computer : n020.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Fri Oct 3 06:10:23 EDT 2025 % 0.14/0.35 % CPUTime : % 69.56/69.75 SZS status Theorem for theBenchmark.p % 69.56/69.75 SZS output start Proof for theBenchmark.p % 69.56/69.75 Clause #0 (by assumption #[]): Eq (Eq dsetconstrER (∀ (A : Iota) (Xphi : Iota → Prop) (Xx : Iota), in Xx (dsetconstr A fun Xy => Xphi Xy) → Xphi Xx)) % 69.56/69.75 True % 69.56/69.75 Clause #3 (by assumption #[]): Eq (Eq kpairp (∀ (Xx Xy : Iota), iskpair (kpair Xx Xy))) True % 69.56/69.75 Clause #5 (by assumption #[]): Eq (Eq theprop (∀ (X : Iota), singleton X → in (setunion X) X)) True % 69.56/69.75 Clause #6 (by assumption #[]): Eq (Eq setukpairinjR (∀ (Xx Xy Xz Xu : Iota), Eq (kpair Xx Xy) (kpair Xz Xu) → Eq Xy Xu)) True % 69.56/69.75 Clause #7 (by assumption #[]): Eq % 69.56/69.75 (Eq ksndsingleton % 69.56/69.75 (∀ (Xu : Iota), iskpair Xu → singleton (dsetconstr (setunion Xu) fun Xx => Eq Xu (kpair (kfst Xu) Xx)))) % 69.56/69.75 True % 69.56/69.75 Clause #8 (by assumption #[]): Eq (Eq ksnd fun Xu => setunion (dsetconstr (setunion Xu) fun Xx => Eq Xu (kpair (kfst Xu) Xx))) True % 69.56/69.75 Clause #9 (by assumption #[]): Eq % 69.56/69.75 (Not (dsetconstrER → kpairp → theprop → setukpairinjR → ksndsingleton → ∀ (Xx Xy : Iota), Eq (ksnd (kpair Xx Xy)) Xy)) % 69.56/69.75 True % 69.56/69.75 Clause #10 (by clausification #[5]): Eq theprop (∀ (X : Iota), singleton X → in (setunion X) X) % 69.56/69.75 Clause #20 (by clausification #[3]): Eq kpairp (∀ (Xx Xy : Iota), iskpair (kpair Xx Xy)) % 69.56/69.75 Clause #22 (by clausify Prop equality #[20]): Or (Eq kpairp False) (Eq (∀ (Xx Xy : Iota), iskpair (kpair Xx Xy)) True) % 69.56/69.75 Clause #24 (by betaEtaReduce #[0]): Eq (Eq dsetconstrER (∀ (A : Iota) (Xphi : Iota → Prop) (Xx : Iota), in Xx (dsetconstr A Xphi) → Xphi Xx)) True % 69.56/69.75 Clause #25 (by clausification #[24]): Eq dsetconstrER (∀ (A : Iota) (Xphi : Iota → Prop) (Xx : Iota), in Xx (dsetconstr A Xphi) → Xphi Xx) % 69.56/69.75 Clause #41 (by clausification #[22]): ∀ (a : Iota), Or (Eq kpairp False) (Eq (∀ (Xy : Iota), iskpair (kpair a Xy)) True) % 69.56/69.75 Clause #42 (by clausification #[41]): ∀ (a a_1 : Iota), Or (Eq kpairp False) (Eq (iskpair (kpair a a_1)) True) % 69.56/69.75 Clause #49 (by clausification #[6]): Eq setukpairinjR (∀ (Xx Xy Xz Xu : Iota), Eq (kpair Xx Xy) (kpair Xz Xu) → Eq Xy Xu) % 69.56/69.75 Clause #51 (by clausify Prop equality #[49]): Or (Eq setukpairinjR False) (Eq (∀ (Xx Xy Xz Xu : Iota), Eq (kpair Xx Xy) (kpair Xz Xu) → Eq Xy Xu) True) % 69.56/69.75 Clause #53 (by clausification #[51]): ∀ (a : Iota), Or (Eq setukpairinjR False) (Eq (∀ (Xy Xz Xu : Iota), Eq (kpair a Xy) (kpair Xz Xu) → Eq Xy Xu) True) % 69.56/69.75 Clause #54 (by clausification #[53]): ∀ (a a_1 : Iota), Or (Eq setukpairinjR False) (Eq (∀ (Xz Xu : Iota), Eq (kpair a a_1) (kpair Xz Xu) → Eq a_1 Xu) True) % 69.56/69.75 Clause #55 (by clausification #[54]): ∀ (a a_1 a_2 : Iota), Or (Eq setukpairinjR False) (Eq (∀ (Xu : Iota), Eq (kpair a a_1) (kpair a_2 Xu) → Eq a_1 Xu) True) % 69.56/69.75 Clause #56 (by clausification #[55]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq setukpairinjR False) (Eq (Eq (kpair a a_1) (kpair a_2 a_3) → Eq a_1 a_3) True) % 69.56/69.75 Clause #57 (by clausification #[56]): ∀ (a a_1 a_2 a_3 : Iota), % 69.56/69.75 Or (Eq setukpairinjR False) (Or (Eq (Eq (kpair a a_1) (kpair a_2 a_3)) False) (Eq (Eq a_1 a_3) True)) % 69.56/69.75 Clause #58 (by clausification #[57]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq setukpairinjR False) (Or (Eq (Eq a a_1) True) (Ne (kpair a_2 a) (kpair a_3 a_1))) % 69.56/69.75 Clause #59 (by clausification #[58]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq setukpairinjR False) (Or (Ne (kpair a a_1) (kpair a_2 a_3)) (Eq a_1 a_3)) % 69.56/69.75 Clause #74 (by clausification #[9]): Eq (dsetconstrER → kpairp → theprop → setukpairinjR → ksndsingleton → ∀ (Xx Xy : Iota), Eq (ksnd (kpair Xx Xy)) Xy) % 69.56/69.75 False % 69.56/69.75 Clause #75 (by clausification #[74]): Eq dsetconstrER True % 69.56/69.75 Clause #76 (by clausification #[74]): Eq (kpairp → theprop → setukpairinjR → ksndsingleton → ∀ (Xx Xy : Iota), Eq (ksnd (kpair Xx Xy)) Xy) False % 69.56/69.75 Clause #77 (by backward demodulation #[75, 25]): Eq True (∀ (A : Iota) (Xphi : Iota → Prop) (Xx : Iota), in Xx (dsetconstr A Xphi) → Xphi Xx) % 69.56/69.75 Clause #80 (by clausification #[77]): ∀ (a : Iota), Eq (∀ (Xphi : Iota → Prop) (Xx : Iota), in Xx (dsetconstr a Xphi) → Xphi Xx) True % 69.56/69.75 Clause #81 (by clausification #[80]): ∀ (a : Iota) (a_1 : Iota → Prop), Eq (∀ (Xx : Iota), in Xx (dsetconstr a a_1) → a_1 Xx) True % 69.56/69.78 Clause #82 (by clausification #[81]): ∀ (a a_1 : Iota) (a_2 : Iota → Prop), Eq (in a (dsetconstr a_1 a_2) → a_2 a) True % 69.56/69.78 Clause #83 (by clausification #[82]): ∀ (a a_1 : Iota) (a_2 : Iota → Prop), Or (Eq (in a (dsetconstr a_1 a_2)) False) (Eq (a_2 a) True) % 69.56/69.78 Clause #103 (by clausification #[76]): Eq kpairp True % 69.56/69.78 Clause #104 (by clausification #[76]): Eq (theprop → setukpairinjR → ksndsingleton → ∀ (Xx Xy : Iota), Eq (ksnd (kpair Xx Xy)) Xy) False % 69.56/69.78 Clause #106 (by backward demodulation #[103, 42]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (iskpair (kpair a a_1)) True) % 69.56/69.78 Clause #110 (by clausification #[106]): ∀ (a a_1 : Iota), Eq (iskpair (kpair a a_1)) True % 69.56/69.78 Clause #115 (by clausification #[7]): Eq ksndsingleton (∀ (Xu : Iota), iskpair Xu → singleton (dsetconstr (setunion Xu) fun Xx => Eq Xu (kpair (kfst Xu) Xx))) % 69.56/69.78 Clause #122 (by clausification #[104]): Eq theprop True % 69.56/69.78 Clause #123 (by clausification #[104]): Eq (setukpairinjR → ksndsingleton → ∀ (Xx Xy : Iota), Eq (ksnd (kpair Xx Xy)) Xy) False % 69.56/69.78 Clause #124 (by backward demodulation #[122, 10]): Eq True (∀ (X : Iota), singleton X → in (setunion X) X) % 69.56/69.78 Clause #130 (by clausification #[124]): ∀ (a : Iota), Eq (singleton a → in (setunion a) a) True % 69.56/69.78 Clause #131 (by clausification #[130]): ∀ (a : Iota), Or (Eq (singleton a) False) (Eq (in (setunion a) a) True) % 69.56/69.78 Clause #134 (by clausification #[8]): Eq ksnd fun Xu => setunion (dsetconstr (setunion Xu) fun Xx => Eq Xu (kpair (kfst Xu) Xx)) % 69.56/69.78 Clause #135 (by argument congruence #[134]): ∀ (a : Iota), Eq (ksnd a) ((fun Xu => setunion (dsetconstr (setunion Xu) fun Xx => Eq Xu (kpair (kfst Xu) Xx))) a) % 69.56/69.78 Clause #140 (by clausification #[123]): Eq setukpairinjR True % 69.56/69.78 Clause #141 (by clausification #[123]): Eq (ksndsingleton → ∀ (Xx Xy : Iota), Eq (ksnd (kpair Xx Xy)) Xy) False % 69.56/69.78 Clause #143 (by backward demodulation #[140, 59]): ∀ (a a_1 a_2 a_3 : Iota), Or (Eq True False) (Or (Ne (kpair a a_1) (kpair a_2 a_3)) (Eq a_1 a_3)) % 69.56/69.78 Clause #149 (by clausification #[143]): ∀ (a a_1 a_2 a_3 : Iota), Or (Ne (kpair a a_1) (kpair a_2 a_3)) (Eq a_1 a_3) % 69.56/69.78 Clause #160 (by clausification #[141]): Eq ksndsingleton True % 69.56/69.78 Clause #161 (by clausification #[141]): Eq (∀ (Xx Xy : Iota), Eq (ksnd (kpair Xx Xy)) Xy) False % 69.56/69.78 Clause #162 (by backward demodulation #[160, 115]): Eq True (∀ (Xu : Iota), iskpair Xu → singleton (dsetconstr (setunion Xu) fun Xx => Eq Xu (kpair (kfst Xu) Xx))) % 69.56/69.78 Clause #165 (by clausification #[161]): ∀ (a : Iota), Eq (Not (∀ (Xy : Iota), Eq (ksnd (kpair (skS.0 10 a) Xy)) Xy)) True % 69.56/69.78 Clause #166 (by clausification #[165]): ∀ (a : Iota), Eq (∀ (Xy : Iota), Eq (ksnd (kpair (skS.0 10 a) Xy)) Xy) False % 69.56/69.78 Clause #167 (by clausification #[166]): ∀ (a a_1 : Iota), Eq (Not (Eq (ksnd (kpair (skS.0 10 a) (skS.0 11 a a_1))) (skS.0 11 a a_1))) True % 69.56/69.78 Clause #168 (by clausification #[167]): ∀ (a a_1 : Iota), Eq (Eq (ksnd (kpair (skS.0 10 a) (skS.0 11 a a_1))) (skS.0 11 a a_1)) False % 69.56/69.78 Clause #169 (by clausification #[168]): ∀ (a a_1 : Iota), Ne (ksnd (kpair (skS.0 10 a) (skS.0 11 a a_1))) (skS.0 11 a a_1) % 69.56/69.78 Clause #180 (by clausification #[162]): ∀ (a : Iota), Eq (iskpair a → singleton (dsetconstr (setunion a) fun Xx => Eq a (kpair (kfst a) Xx))) True % 69.56/69.78 Clause #181 (by clausification #[180]): ∀ (a : Iota), % 69.56/69.78 Or (Eq (iskpair a) False) (Eq (singleton (dsetconstr (setunion a) fun Xx => Eq a (kpair (kfst a) Xx))) True) % 69.56/69.78 Clause #182 (by superposition #[181, 110]): ∀ (a a_1 : Iota), % 69.56/69.78 Or % 69.56/69.78 (Eq (singleton (dsetconstr (setunion (kpair a a_1)) fun Xx => Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) Xx))) % 69.56/69.78 True) % 69.56/69.78 (Eq False True) % 69.56/69.78 Clause #193 (by betaEtaReduce #[135]): ∀ (a : Iota), Eq (ksnd a) (setunion (dsetconstr (setunion a) fun Xx => Eq a (kpair (kfst a) Xx))) % 69.56/69.78 Clause #566 (by clausification #[182]): ∀ (a a_1 : Iota), % 69.56/69.78 Eq (singleton (dsetconstr (setunion (kpair a a_1)) fun Xx => Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) Xx))) True % 69.56/69.78 Clause #567 (by superposition #[566, 131]): ∀ (a a_1 : Iota), % 69.56/69.78 Or (Eq True False) % 69.56/69.78 (Eq % 69.56/69.78 (in (setunion (dsetconstr (setunion (kpair a a_1)) fun Xx => Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) Xx))) % 70.37/70.56 (dsetconstr (setunion (kpair a a_1)) fun Xx => Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) Xx))) % 70.37/70.56 True) % 70.37/70.56 Clause #8289 (by clausification #[567]): ∀ (a a_1 : Iota), % 70.37/70.56 Eq % 70.37/70.56 (in (setunion (dsetconstr (setunion (kpair a a_1)) fun Xx => Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) Xx))) % 70.37/70.56 (dsetconstr (setunion (kpair a a_1)) fun Xx => Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) Xx))) % 70.37/70.56 True % 70.37/70.56 Clause #8290 (by forward demodulation #[8289, 193]): ∀ (a a_1 : Iota), % 70.37/70.56 Eq % 70.37/70.56 (in (ksnd (kpair a a_1)) % 70.37/70.56 (dsetconstr (setunion (kpair a a_1)) fun Xx => Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) Xx))) % 70.37/70.56 True % 70.37/70.56 Clause #8291 (by superposition #[8290, 83]): ∀ (a a_1 : Iota), Or (Eq True False) (Eq (Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) (ksnd (kpair a a_1)))) True) % 70.37/70.56 Clause #8709 (by clausification #[8291]): ∀ (a a_1 : Iota), Eq (Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) (ksnd (kpair a a_1)))) True % 70.37/70.56 Clause #8710 (by clausification #[8709]): ∀ (a a_1 : Iota), Eq (kpair a a_1) (kpair (kfst (kpair a a_1)) (ksnd (kpair a a_1))) % 70.37/70.56 Clause #8712 (by superposition #[8710, 149]): ∀ (a a_1 a_2 a_3 : Iota), Or (Ne (kpair a a_1) (kpair a_2 a_3)) (Eq a_1 (ksnd (kpair a_2 a_3))) % 70.37/70.56 Clause #8779 (by equality resolution #[8712]): ∀ (a a_1 : Iota), Eq a (ksnd (kpair a_1 a)) % 70.37/70.56 Clause #8784 (by backward contextual literal cutting #[8779, 169]): False % 70.37/70.56 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------