%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP033^2 : TPTP v9.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n023.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:51:04 PM UTC 2025 % Result : Theorem 4.51s 4.70s % Output : Proof 4.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : ITP033^2 : TPTP v9.2.0. Released v7.5.0. % 0.03/0.13 % Command : duper %s % 0.13/0.34 % Computer : n023.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 : Fri Oct 3 00:22:53 EDT 2025 % 0.13/0.34 % CPUTime : % 4.51/4.70 SZS status Theorem for theBenchmark.p % 4.51/4.70 SZS output start Proof for theBenchmark.p % 4.51/4.70 Clause #1 (by assumption #[]): Eq (binary1610619414edTree a h (binary210054475elle_T a t1 x t2)) True % 4.51/4.70 Clause #3 (by assumption #[]): Eq % 4.51/4.70 (∀ (A : Type) (H : A → int) (T1 : binary1291135688e_Tree A) (X : A) (T2 : binary1291135688e_Tree A), % 4.51/4.70 binary1610619414edTree A H (binary210054475elle_T A T1 X T2) → binary1610619414edTree A H T1) % 4.51/4.70 True % 4.51/4.70 Clause #257 (by assumption #[]): Eq (Not (binary1610619414edTree a h t1)) True % 4.51/4.70 Clause #265 (by clausification #[257]): Eq (binary1610619414edTree a h t1) False % 4.51/4.70 Clause #271 (by clausification #[3]): ∀ (a : Type), % 4.51/4.70 Eq % 4.51/4.70 (∀ (H : a → int) (T1 : binary1291135688e_Tree a) (X : a) (T2 : binary1291135688e_Tree a), % 4.51/4.70 binary1610619414edTree a H (binary210054475elle_T a T1 X T2) → binary1610619414edTree a H T1) % 4.51/4.70 True % 4.51/4.70 Clause #272 (by clausification #[271]): ∀ (a : Type) (a_1 : a → int), % 4.51/4.70 Eq % 4.51/4.70 (∀ (T1 : binary1291135688e_Tree a) (X : a) (T2 : binary1291135688e_Tree a), % 4.51/4.70 binary1610619414edTree a a_1 (binary210054475elle_T a T1 X T2) → binary1610619414edTree a a_1 T1) % 4.51/4.70 True % 4.51/4.70 Clause #273 (by clausification #[272]): ∀ (a : Type) (a_1 : a → int) (a_2 : binary1291135688e_Tree a), % 4.51/4.70 Eq % 4.51/4.70 (∀ (X : a) (T2 : binary1291135688e_Tree a), % 4.51/4.70 binary1610619414edTree a a_1 (binary210054475elle_T a a_2 X T2) → binary1610619414edTree a a_1 a_2) % 4.51/4.70 True % 4.51/4.70 Clause #274 (by clausification #[273]): ∀ (a : Type) (a_1 : a → int) (a_2 : binary1291135688e_Tree a) (a_3 : a), % 4.51/4.70 Eq % 4.51/4.70 (∀ (T2 : binary1291135688e_Tree a), % 4.51/4.70 binary1610619414edTree a a_1 (binary210054475elle_T a a_2 a_3 T2) → binary1610619414edTree a a_1 a_2) % 4.51/4.70 True % 4.51/4.70 Clause #275 (by clausification #[274]): ∀ (a : Type) (a_1 : a → int) (a_2 : binary1291135688e_Tree a) (a_3 : a) (a_4 : binary1291135688e_Tree a), % 4.51/4.70 Eq (binary1610619414edTree a a_1 (binary210054475elle_T a a_2 a_3 a_4) → binary1610619414edTree a a_1 a_2) True % 4.51/4.70 Clause #276 (by clausification #[275]): ∀ (a : Type) (a_1 : a → int) (a_2 : binary1291135688e_Tree a) (a_3 : a) (a_4 : binary1291135688e_Tree a), % 4.51/4.70 Or (Eq (binary1610619414edTree a a_1 (binary210054475elle_T a a_2 a_3 a_4)) False) % 4.51/4.70 (Eq (binary1610619414edTree a a_1 a_2) True) % 4.51/4.70 Clause #277 (by superposition #[276, 1]): Or (Eq (binary1610619414edTree a (fun x => h x) t1) True) (Eq False True) % 4.51/4.70 Clause #605 (by betaEtaReduce #[277]): Or (Eq (binary1610619414edTree a h t1) True) (Eq False True) % 4.51/4.70 Clause #606 (by clausification #[605]): Eq (binary1610619414edTree a h t1) True % 4.51/4.70 Clause #607 (by superposition #[606, 265]): Eq True False % 4.51/4.70 Clause #612 (by clausification #[607]): False % 4.51/4.70 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------