%------------------------------------------------------------------------------ % File : Duper---1.0 % Problem : ITP303_1 : TPTP v9.2.0. Released v8.0.0. % Transfm : none % Format : tptp:raw % Command : duper %s % Computer : n001.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:52:07 PM UTC 2025 % Result : Theorem 139.51s 139.68s % Output : Proof 139.51s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.13 % Problem : ITP303_1 : TPTP v9.2.0. Released v8.0.0. % 0.08/0.14 % Command : duper %s % 0.15/0.36 % Computer : n001.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 00:25:38 EDT 2025 % 0.15/0.36 % CPUTime : % 139.51/139.68 SZS status Theorem for theBenchmark.p % 139.51/139.68 SZS output start Proof for theBenchmark.p % 139.51/139.68 Clause #27 (by assumption #[]): Eq (Not (Eq («nTCatDom$» («yFtorNT$» «c$» «f$»)) («catDom$» («fun_app$r» «nTCod$» («yFtorNT$» «c$» «f$»))))) True % 139.51/139.68 Clause #38 (by assumption #[]): Eq % 139.51/139.68 (∀ (A__questionmark_v0 : «A_b_b_c_LSCategory_ext_Category_ext$») (A__questionmark_v1 : «B$»), % 139.51/139.68 Eq («nTCatDom$» («fun_app$t» («yFtorNT$a» A__questionmark_v0) A__questionmark_v1)) % 139.51/139.68 («fun_app$s» «oppositeCategory$» A__questionmark_v0)) % 139.51/139.68 True % 139.51/139.68 Clause #39 (by assumption #[]): Eq % 139.51/139.68 (∀ (A__questionmark_v0 : «A_b_b_c_LSCategory_ext_Category_ext$») (A__questionmark_v1 : «A$»), % 139.51/139.68 Eq («catDom$» («homFtorContra$» A__questionmark_v0 A__questionmark_v1)) % 139.51/139.68 («fun_app$s» «oppositeCategory$» A__questionmark_v0)) % 139.51/139.68 True % 139.51/139.68 Clause #40 (by assumption #[]): Eq % 139.51/139.68 (∀ (A__questionmark_v0 : «A_b_b_c_LSCategory_ext_Category_ext$») (A__questionmark_v1 : «B$»), % 139.51/139.68 Eq («fun_app$t» («yFtorNT$a» A__questionmark_v0) A__questionmark_v1) % 139.51/139.68 («makeNT$» («yFtorNT$» A__questionmark_v0 A__questionmark_v1))) % 139.51/139.68 True % 139.51/139.68 Clause #58 (by assumption #[]): Eq % 139.51/139.68 (∀ (A__questionmark_v0 : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$»), % 139.51/139.68 Eq («nTCatDom$» A__questionmark_v0) («nTCatDom$» («makeNT$» A__questionmark_v0))) % 139.51/139.68 True % 139.51/139.68 Clause #208 (by assumption #[]): Eq % 139.51/139.68 (∀ (A__questionmark_v0 A__questionmark_v1 : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$») % 139.51/139.68 (A__questionmark_v2 : «A_ZF_fun$») (A__questionmark_v3 : «Unit$»), % 139.51/139.68 Eq % 139.51/139.68 («fun_app$r» «nTCod$» % 139.51/139.68 («natTrans_ext$a» A__questionmark_v0 A__questionmark_v1 A__questionmark_v2 A__questionmark_v3)) % 139.51/139.68 A__questionmark_v1) % 139.51/139.68 True % 139.51/139.68 Clause #525 (by assumption #[]): Eq % 139.51/139.68 (∀ (A__questionmark_v0 : «A_b_b_c_LSCategory_ext_Category_ext$») (A__questionmark_v1 : «B$»), % 139.51/139.68 Eq («yFtorNT$» A__questionmark_v0 A__questionmark_v1) % 139.51/139.68 («natTrans_ext$a» % 139.51/139.68 («homFtorContra$» A__questionmark_v0 («fun_app$ab» («dom$» A__questionmark_v0) A__questionmark_v1)) % 139.51/139.68 («homFtorContra$» A__questionmark_v0 («fun_app$ab» («cod$a» A__questionmark_v0) A__questionmark_v1)) % 139.51/139.68 («uum$» A__questionmark_v0 A__questionmark_v1) «unity$»)) % 139.51/139.68 True % 139.51/139.68 Clause #1564 (by clausification #[27]): Eq (Eq («nTCatDom$» («yFtorNT$» «c$» «f$»)) («catDom$» («fun_app$r» «nTCod$» («yFtorNT$» «c$» «f$»)))) False % 139.51/139.68 Clause #1565 (by clausification #[1564]): Ne («nTCatDom$» («yFtorNT$» «c$» «f$»)) («catDom$» («fun_app$r» «nTCod$» («yFtorNT$» «c$» «f$»))) % 139.51/139.68 Clause #1838 (by clausification #[38]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$»), % 139.51/139.68 Eq % 139.51/139.68 (∀ (A__questionmark_v1 : «B$»), % 139.51/139.68 Eq («nTCatDom$» («fun_app$t» («yFtorNT$a» a) A__questionmark_v1)) («fun_app$s» «oppositeCategory$» a)) % 139.51/139.68 True % 139.51/139.68 Clause #1839 (by clausification #[1838]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.68 Eq (Eq («nTCatDom$» («fun_app$t» («yFtorNT$a» a) a_1)) («fun_app$s» «oppositeCategory$» a)) True % 139.51/139.68 Clause #1840 (by clausification #[1839]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.68 Eq («nTCatDom$» («fun_app$t» («yFtorNT$a» a) a_1)) («fun_app$s» «oppositeCategory$» a) % 139.51/139.68 Clause #1858 (by clausification #[39]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$»), % 139.51/139.68 Eq % 139.51/139.68 (∀ (A__questionmark_v1 : «A$»), % 139.51/139.68 Eq («catDom$» («homFtorContra$» a A__questionmark_v1)) («fun_app$s» «oppositeCategory$» a)) % 139.51/139.68 True % 139.51/139.68 Clause #1859 (by clausification #[1858]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «A$»), % 139.51/139.68 Eq (Eq («catDom$» («homFtorContra$» a a_1)) («fun_app$s» «oppositeCategory$» a)) True % 139.51/139.68 Clause #1860 (by clausification #[1859]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «A$»), % 139.51/139.68 Eq («catDom$» («homFtorContra$» a a_1)) («fun_app$s» «oppositeCategory$» a) % 139.51/139.68 Clause #1877 (by clausification #[40]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$»), % 139.51/139.68 Eq % 139.51/139.68 (∀ (A__questionmark_v1 : «B$»), % 139.51/139.68 Eq («fun_app$t» («yFtorNT$a» a) A__questionmark_v1) («makeNT$» («yFtorNT$» a A__questionmark_v1))) % 139.51/139.70 True % 139.51/139.70 Clause #1878 (by clausification #[1877]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.70 Eq (Eq («fun_app$t» («yFtorNT$a» a) a_1) («makeNT$» («yFtorNT$» a a_1))) True % 139.51/139.70 Clause #1879 (by clausification #[1878]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.70 Eq («fun_app$t» («yFtorNT$a» a) a_1) («makeNT$» («yFtorNT$» a a_1)) % 139.51/139.70 Clause #1880 (by clausification #[58]): ∀ (a : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$»), Eq (Eq («nTCatDom$» a) («nTCatDom$» («makeNT$» a))) True % 139.51/139.70 Clause #1881 (by clausification #[1880]): ∀ (a : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_NatTrans_ext$»), Eq («nTCatDom$» a) («nTCatDom$» («makeNT$» a)) % 139.51/139.70 Clause #1884 (by superposition #[1881, 1879]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.70 Eq («nTCatDom$» («yFtorNT$» a a_1)) («nTCatDom$» («fun_app$t» («yFtorNT$a» a) a_1)) % 139.51/139.70 Clause #1885 (by superposition #[1884, 1840]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.70 Eq («nTCatDom$» («yFtorNT$» a a_1)) («fun_app$s» «oppositeCategory$» a) % 139.51/139.70 Clause #1888 (by backward demodulation #[1885, 1565]): Ne («fun_app$s» «oppositeCategory$» «c$») («catDom$» («fun_app$r» «nTCod$» («yFtorNT$» «c$» «f$»))) % 139.51/139.70 Clause #4488 (by clausification #[208]): ∀ (a : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$»), % 139.51/139.70 Eq % 139.51/139.70 (∀ (A__questionmark_v1 : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$») (A__questionmark_v2 : «A_ZF_fun$») % 139.51/139.70 (A__questionmark_v3 : «Unit$»), % 139.51/139.70 Eq («fun_app$r» «nTCod$» («natTrans_ext$a» a A__questionmark_v1 A__questionmark_v2 A__questionmark_v3)) % 139.51/139.70 A__questionmark_v1) % 139.51/139.70 True % 139.51/139.70 Clause #4489 (by clausification #[4488]): ∀ (a a_1 : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$»), % 139.51/139.70 Eq % 139.51/139.70 (∀ (A__questionmark_v2 : «A_ZF_fun$») (A__questionmark_v3 : «Unit$»), % 139.51/139.70 Eq («fun_app$r» «nTCod$» («natTrans_ext$a» a a_1 A__questionmark_v2 A__questionmark_v3)) a_1) % 139.51/139.70 True % 139.51/139.70 Clause #4490 (by clausification #[4489]): ∀ (a a_1 : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$») (a_2 : «A_ZF_fun$»), % 139.51/139.70 Eq (∀ (A__questionmark_v3 : «Unit$»), Eq («fun_app$r» «nTCod$» («natTrans_ext$a» a a_1 a_2 A__questionmark_v3)) a_1) % 139.51/139.70 True % 139.51/139.70 Clause #4491 (by clausification #[4490]): ∀ (a a_1 : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$») (a_2 : «A_ZF_fun$») (a_3 : «Unit$»), % 139.51/139.70 Eq (Eq («fun_app$r» «nTCod$» («natTrans_ext$a» a a_1 a_2 a_3)) a_1) True % 139.51/139.70 Clause #4492 (by clausification #[4491]): ∀ (a a_1 : «A_ZF_b_ZF_b_c_LSCategory_ext_unit_unit_Functor_ext$») (a_2 : «A_ZF_fun$») (a_3 : «Unit$»), % 139.51/139.70 Eq («fun_app$r» «nTCod$» («natTrans_ext$a» a a_1 a_2 a_3)) a_1 % 139.51/139.70 Clause #13174 (by clausification #[525]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$»), % 139.51/139.70 Eq % 139.51/139.70 (∀ (A__questionmark_v1 : «B$»), % 139.51/139.70 Eq («yFtorNT$» a A__questionmark_v1) % 139.51/139.70 («natTrans_ext$a» («homFtorContra$» a («fun_app$ab» («dom$» a) A__questionmark_v1)) % 139.51/139.70 («homFtorContra$» a («fun_app$ab» («cod$a» a) A__questionmark_v1)) («uum$» a A__questionmark_v1) «unity$»)) % 139.51/139.70 True % 139.51/139.70 Clause #13175 (by clausification #[13174]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.70 Eq % 139.51/139.70 (Eq («yFtorNT$» a a_1) % 139.51/139.70 («natTrans_ext$a» («homFtorContra$» a («fun_app$ab» («dom$» a) a_1)) % 139.51/139.70 («homFtorContra$» a («fun_app$ab» («cod$a» a) a_1)) («uum$» a a_1) «unity$»)) % 139.51/139.70 True % 139.51/139.70 Clause #13176 (by clausification #[13175]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.70 Eq («yFtorNT$» a a_1) % 139.51/139.70 («natTrans_ext$a» («homFtorContra$» a («fun_app$ab» («dom$» a) a_1)) % 139.51/139.70 («homFtorContra$» a («fun_app$ab» («cod$a» a) a_1)) («uum$» a a_1) «unity$») % 139.51/139.70 Clause #13180 (by superposition #[13176, 4492]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.70 Eq («fun_app$r» «nTCod$» («yFtorNT$» a a_1)) («homFtorContra$» a («fun_app$ab» («cod$a» a) a_1)) % 139.51/139.76 Clause #13733 (by superposition #[13180, 1860]): ∀ (a : «A_b_b_c_LSCategory_ext_Category_ext$») (a_1 : «B$»), % 139.51/139.76 Eq («catDom$» («fun_app$r» «nTCod$» («yFtorNT$» a a_1))) («fun_app$s» «oppositeCategory$» a) % 139.51/139.76 Clause #13737 (by backward contextual literal cutting #[13733, 1888]): False % 139.51/139.76 SZS output end Proof for theBenchmark.p %------------------------------------------------------------------------------