%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : SEU771^2 : TPTP v9.2.0. Released v3.7.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n031.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:24 PM UTC 2025 % Result : Theorem 4.02s 4.21s % Output : Proof 4.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : SEU771^2 : TPTP v9.2.0. Released v3.7.0. % 0.08/0.15 % Command : duper %s % 0.15/0.36 % Computer : n031.cluster.edu % 0.15/0.36 % Model : x86_64 x86_64 % 0.15/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.36 % Memory : 8042.1875MB % 0.15/0.36 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.36 % CPULimit : 300 % 0.15/0.36 % WCLimit : 300 % 0.15/0.36 % DateTime : Fri Oct 3 04:45:23 EDT 2025 % 0.15/0.37 % CPUTime : % 4.02/4.21 SZS status Theorem for theBenchmark.p % 4.02/4.21 SZS output start Proof for theBenchmark.p % 4.02/4.21 Clause #1 (by assumption #[]): Eq % 4.02/4.21 (Eq setOfPairsIsBReln % 4.02/4.21 (∀ (A B : Iota) (Xphi : Iota → Iota → Prop), breln A B (dpsetconstr A B fun Xx Xy => Xphi Xx Xy))) % 4.02/4.21 True % 4.02/4.21 Clause #2 (by assumption #[]): Eq (Eq breln1 fun A R => breln A A R) True % 4.02/4.21 Clause #3 (by assumption #[]): Eq % 4.02/4.21 (Not % 4.02/4.21 (setOfPairsIsBReln → ∀ (A : Iota) (Xphi : Iota → Iota → Prop), breln1 A (dpsetconstr A A fun Xx Xy => Xphi Xx Xy))) % 4.02/4.21 True % 4.02/4.21 Clause #4 (by clausification #[2]): Eq breln1 fun A R => breln A A R % 4.02/4.21 Clause #5 (by argument congruence #[4]): ∀ (a : Iota), Eq (breln1 a) ((fun A R => breln A A R) a) % 4.02/4.21 Clause #7 (by betaEtaReduce #[5]): ∀ (a : Iota), Eq (breln1 a) (breln a a) % 4.02/4.21 Clause #8 (by argument congruence #[7]): ∀ (a a_1 : Iota), Eq (breln1 a a_1) (breln a a a_1) % 4.02/4.21 Clause #33 (by betaEtaReduce #[1]): Eq (Eq setOfPairsIsBReln (∀ (A B : Iota) (Xphi : Iota → Iota → Prop), breln A B (dpsetconstr A B Xphi))) True % 4.02/4.21 Clause #34 (by clausification #[33]): Eq setOfPairsIsBReln (∀ (A B : Iota) (Xphi : Iota → Iota → Prop), breln A B (dpsetconstr A B Xphi)) % 4.02/4.21 Clause #56 (by betaEtaReduce #[3]): Eq (Not (setOfPairsIsBReln → ∀ (A : Iota) (Xphi : Iota → Iota → Prop), breln1 A (dpsetconstr A A Xphi))) True % 4.02/4.21 Clause #57 (by clausification #[56]): Eq (setOfPairsIsBReln → ∀ (A : Iota) (Xphi : Iota → Iota → Prop), breln1 A (dpsetconstr A A Xphi)) False % 4.02/4.21 Clause #58 (by clausification #[57]): Eq setOfPairsIsBReln True % 4.02/4.21 Clause #59 (by clausification #[57]): Eq (∀ (A : Iota) (Xphi : Iota → Iota → Prop), breln1 A (dpsetconstr A A Xphi)) False % 4.02/4.21 Clause #60 (by backward demodulation #[58, 34]): Eq True (∀ (A B : Iota) (Xphi : Iota → Iota → Prop), breln A B (dpsetconstr A B Xphi)) % 4.02/4.21 Clause #64 (by clausification #[59]): ∀ (a : Iota), % 4.02/4.21 Eq (Not (∀ (Xphi : Iota → Iota → Prop), breln1 (skS.0 0 a) (dpsetconstr (skS.0 0 a) (skS.0 0 a) Xphi))) True % 4.02/4.21 Clause #65 (by clausification #[64]): ∀ (a : Iota), Eq (∀ (Xphi : Iota → Iota → Prop), breln1 (skS.0 0 a) (dpsetconstr (skS.0 0 a) (skS.0 0 a) Xphi)) False % 4.02/4.21 Clause #66 (by clausification #[65]): ∀ (a : Iota) (a_1 : Iota → Iota → Prop), % 4.02/4.21 Eq (Not (breln1 (skS.0 0 a) (dpsetconstr (skS.0 0 a) (skS.0 0 a) (skS.0 1 a a_1)))) True % 4.02/4.21 Clause #67 (by clausification #[66]): ∀ (a : Iota) (a_1 : Iota → Iota → Prop), % 4.02/4.21 Eq (breln1 (skS.0 0 a) (dpsetconstr (skS.0 0 a) (skS.0 0 a) (skS.0 1 a a_1))) False % 4.02/4.21 Clause #71 (by clausification #[60]): ∀ (a : Iota), Eq (∀ (B : Iota) (Xphi : Iota → Iota → Prop), breln a B (dpsetconstr a B Xphi)) True % 4.02/4.21 Clause #72 (by clausification #[71]): ∀ (a a_1 : Iota), Eq (∀ (Xphi : Iota → Iota → Prop), breln a a_1 (dpsetconstr a a_1 Xphi)) True % 4.02/4.21 Clause #73 (by clausification #[72]): ∀ (a a_1 : Iota) (a_2 : Iota → Iota → Prop), Eq (breln a a_1 (dpsetconstr a a_1 a_2)) True % 4.02/4.21 Clause #74 (by superposition #[73, 8]): ∀ (a : Iota) (a_1 : Iota → Iota → Prop), Eq (breln1 a (dpsetconstr a a a_1)) True % 4.02/4.21 Clause #79 (by superposition #[74, 67]): Eq True False % 4.02/4.21 Clause #84 (by clausification #[79]): False % 4.02/4.21 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------