%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : ITP304_1 : TPTP v9.3.1. Released v8.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n011.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 11:39:18 AM UTC 2026
% Result : CounterSatisfiable 1.89s 0.83s
% Output : Saturation 1.89s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(u2255,axiom,
~ sP6(X0) ).
cnf(u2261,axiom,
~ sP7(X0) ).
cnf(u2267,axiom,
~ sP8(X0) ).
cnf(u2273,axiom,
~ sP12(X0) ).
cnf(u2279,axiom,
~ sP15(X0) ).
cnf(u2285,axiom,
~ sP14(X0) ).
cnf(u2291,axiom,
~ sP13(X0) ).
cnf(u2294,axiom,
'preFunctor$a'(X0) ).
cnf(u2300,axiom,
'preFunctor$b'(X0) ).
cnf(u2309,axiom,
~ 'functorM$b'(X0) ).
cnf(u2314,axiom,
~ 'functor$c'(X0) ).
cnf(u2317,axiom,
'functorM$c'(X0) ).
cnf(u2342,axiom,
sP0(X0) ).
cnf(u2345,axiom,
~ sP1(X0) ).
cnf(u2349,axiom,
sP2(X0) ).
cnf(u2356,axiom,
sP4(X0) ).
cnf(u2368,axiom,
~ 'preFunctor$'(X0) ).
cnf(u2374,axiom,
sP16(X0) ).
cnf(u2384,axiom,
sP17(X0) ).
cnf(u2387,axiom,
sP18(X0) ).
cnf(u2390,axiom,
sP19(X0) ).
cnf(u2393,axiom,
sP20(X0) ).
cnf(u2407,axiom,
'category_axioms$'(X0) ).
cnf(u2417,axiom,
'extCategory$'(X0) ).
cnf(u2426,axiom,
sP21(X0) ).
cnf(u2441,axiom,
'functorM_axioms$'(X0) ).
cnf(u2444,axiom,
'functorM$'(X0) ).
cnf(u2456,axiom,
'functorExt$b'(X0) ).
cnf(u2459,axiom,
'functor$a'('makeFtor$a'(X0)) ).
cnf(u2468,axiom,
'functorM$'('identityFunctor$c'(X0)) ).
cnf(u2477,axiom,
'functorExt$'(X0) ).
cnf(u2480,axiom,
'functor$'(X0) ).
cnf(u2483,axiom,
~ 'equivalence$a'(X0) ).
cnf(u2497,axiom,
'functor$a'(X0) ).
cnf(u2518,axiom,
'category$c'('fun_app$k'('oppositeCategory$',X0)) ).
cnf(u2526,axiom,
'fun_app$b'('isOpair$',X0) ).
cnf(u2532,axiom,
'member$'(X1,X0) ).
cnf(u2541,axiom,
'member$a'(X1,X0) ).
cnf(u2563,axiom,
'member$b'(X1,X0) ).
cnf(u2572,axiom,
'member$c'(X1,X0) ).
cnf(u2581,axiom,
'member$d'(X1,X0) ).
cnf(u2622,axiom,
'fun_app$b'(X1,X0) ).
cnf(u2674,axiom,
'catCod$c'(X0) = X2 ).
cnf(u2854,axiom,
'fun_app$e'(X1,X0) ).
cnf(u2909,axiom,
'category$c'(X0) ).
cnf(u2930,axiom,
'fun_app$d'(X1,X0) ).
cnf(u2966,axiom,
~ 'equivalence_axioms$a'(X0) ).
cnf(u3000,axiom,
sP10(X0) ).
cnf(u3067,axiom,
'preFunctor$a'('makeFtor$a'(X0)) ).
cnf(u3087,axiom,
'functor$'('makeFtor$c'(X0)) ).
cnf(u3097,axiom,
'preFunctor$a'('identityFunctor$c'(X0)) ).
cnf(u3103,axiom,
'functor$'('unitFunctor$c'(X0)) ).
cnf(u3130,axiom,
'functorExt$b'('makeFtor$a'(X0)) ).
cnf(u3133,axiom,
'functorM$'('makeFtor$a'(X0)) ).
cnf(u3166,axiom,
'functor$a'('identityFunctor$c'(X0)) ).
cnf(u3217,axiom,
'catDom$'(X0) = X1 ).
cnf(u3426,axiom,
~ 'objIso$a'(X0,X1,X2) ).
cnf(u3446,axiom,
'lSCategory$'('fun_app$n'('oppositeCategory$a',X0)) ).
cnf(u3467,axiom,
~ 'inverse_rel$'(X0,X1,X2) ).
cnf(u3497,axiom,
'functor_abbrev$b'(X1,X0,'catCod$a'(X1)) ).
cnf(u3569,axiom,
sP10('identityFunctor$c'(X0)) ).
cnf(u3591,axiom,
'fun_app$c'(X1,X0) ).
cnf(u3603,axiom,
'catDom$a'(X0) = X1 ).
cnf(u3763,axiom,
'functor_abbrev$b'(X1,X2,X0) ).
cnf(u3789,axiom,
~ 'mapsTo$c'(X0,X1,X2,X3) ).
cnf(u3842,axiom,
'compDefined$c'(X0,X1,'inverse$a'(X0,X1)) ).
cnf(u3845,axiom,
~ 'isomorphism$c'(X0,X1) ).
cnf(u4192,axiom,
'member$a'(X0,'mor$'('set$a')) ).
cnf(u4202,axiom,
'member$a'(X1,'mor$'(X0)) ).
cnf(u4359,axiom,
'functorExt$'('makeFtor$c'(X0)) ).
cnf(u4362,axiom,
'functorExt$'('unitFunctor$c'(X0)) ).
cnf(u4367,axiom,
'functorM$c'('makeFtor$c'(X0)) ).
cnf(u4370,axiom,
'functorM$c'('unitFunctor$c'(X0)) ).
cnf(u4399,axiom,
'extCategory$'('catCod$a'(X0)) ).
cnf(u4491,axiom,
~ 'member$f'(X1,'obj$a'(X0)) ).
cnf(u4539,axiom,
'fun_app$a'(X1,X0) ).
cnf(u4567,axiom,
'functorM$'('constFunctor$a'(X0,X1,X2)) ).
cnf(u4657,axiom,
'functorM$a'(X0) ).
cnf(u4662,axiom,
'functorExt$c'(X0) ).
cnf(u4673,axiom,
'functor$b'(X0) ).
cnf(u4683,axiom,
'catCod$'(X0) = X2 ).
cnf(u4996,axiom,
'functor_comp_def$'(X0,X1) ).
cnf(u5044,axiom,
'catCod$a'(X0) = 'catDom$'(X1) ).
cnf(u5419,axiom,
~ 'fun_app$g'('mapsTo$a'(X0,X1,X2),X3) ).
cnf(u5535,axiom,
'functorM_axioms$a'(X0) ).
cnf(u5538,axiom,
sP9(X0) ).
cnf(u5544,axiom,
'functor$b'('makeFtor$b'(X0)) ).
cnf(u5577,axiom,
'functorExt$c'('makeFtor$b'(X0)) ).
cnf(u5585,axiom,
'functorM$a'('makeFtor$b'(X0)) ).
cnf(u5685,axiom,
'functor_comp_def$a'(X0,X1) ).
cnf(u5709,axiom,
'pair$'(sK22(X0,X1),sK23(X0,X1)) = X1 ).
cnf(u5936,axiom,
'catCod$'(X0) = 'catDom$'(X1) ).
cnf(u5999,axiom,
'catCod$'(X0) = 'catDom$a'(X1) ).
cnf(u6378,axiom,
'functor_comp_def$b'(X0,X1) ).
cnf(u6446,axiom,
'functor_abbrev$'(X1,'catDom$'(X1),X0) ).
cnf(u7413,axiom,
~ 'functor_abbrev$a'(X0,X1,X2) ).
cnf(u7515,axiom,
~ 'member$h'(X2,'obj$c'(X1)) ).
cnf(u7530,axiom,
'mapO$h'('identityFunctor$b'(X0),X1) = X1 ).
cnf(u7534,axiom,
'compDefined$d'(X0,X1,X4) ).
cnf(u7542,axiom,
~ 'member$g'(X1,'obj$b'(X0)) ).
cnf(u7545,axiom,
X3 = X7 ).
cnf(u7785,axiom,
X2 = X6 ).
cnf(u8161,axiom,
'collect$'(X1) = 'collect$'(X0) ).
cnf(u8257,axiom,
'catDom_update$'(X4,X1) = 'catDom_update$'(X3,X1) ).
cnf(u8260,axiom,
'catDom$c'(X1) = sK87('catDom$c'(X1),X3,X4) ).
cnf(u8392,axiom,
'category$a'('catExp$'('fun_app$n'('oppositeCategory$a',X1),X0)) ).
cnf(u8421,axiom,
sP3(X0) ).
cnf(u8636,axiom,
'functorM_axioms$b'(X0) ).
cnf(u8652,axiom,
~ 'fun_app$g'('objIso$b'(X0,X1),X2) ).
cnf(u8675,axiom,
'fun_app$f'('compDefined$b'(X0,X1),'inverse$'(X0,X1)) ).
cnf(u8678,axiom,
~ 'fun_app$f'('isomorphism$b'(X0),X1) ).
cnf(u8736,axiom,
'mapO$d'('identityFunctor$'(X0),X1) = X1 ).
cnf(u8879,axiom,
~ 'fun_app$f'('isomorphism$b'(X0),'id$'(X0,X1)) ).
cnf(u8887,axiom,
'fun_app$f'('compDefined$b'(X0,'id$'(X0,X1)),'id$'(X0,X1)) ).
cnf(u8908,axiom,
'inverse$'(X0,'inverse$'(X0,X1)) = X1 ).
cnf(u8921,axiom,
'mapO$i'('identityFunctor$a'(X0),X1) = X1 ).
cnf(u8930,axiom,
~ 'member$e'(X1,'mor$a'(X0)) ).
cnf(u9010,axiom,
'fun_app$f'('inverse_rel$b'(X0,'id$'(X0,X1)),'id$'(X0,X1)) ).
cnf(u9019,axiom,
'id$'(X0,X1) = 'inverse$'(X0,'id$'(X0,X1)) ).
cnf(u9033,axiom,
X2 = X3 ).
cnf(u9240,axiom,
'equivalence_axioms$'(X0) ).
cnf(u9305,axiom,
'functor_abbrev$c'('makeFtor$b'('homFtorContra$a'(X0,X1)),'fun_app$n'('oppositeCategory$a',X0),'set$a') ).
cnf(u9331,axiom,
'catCod_update$'(X4,X1) = 'catCod_update$'(X3,X1) ).
cnf(u9334,axiom,
'catCod$b'(X1) = sK29('catCod$b'(X1),X3,X4) ).
cnf(u9352,axiom,
X1 = X2 ).
cnf(u9369,axiom,
'compDefined$c'('catExp$'('fun_app$n'('oppositeCategory$a',X0),'set$a'),'fun_app$m'('yFtorNT$'(X0),X1),'fun_app$m'('yFtorNT$'(X0),X2)) ).
cnf(u9394,axiom,
'compDefined$c'(X0,X1,X4) ).
cnf(u9449,axiom,
( ~ 'member$h'(X2,'obj$c'(X1))
| ~ 'category$a'(X1) ) ).
cnf(u10506,axiom,
~ sP11(X0) ).
cnf(u10927,axiom,
'fun_app$f'('inverse_rel$b'(X1,X0),X0) ).
cnf(u11162,axiom,
X0 = X1 ).
cnf(u12616,axiom,
~ 'fun_app$g'('mapsTo$a'('catDom$b'(X0),X4,sK33(X0)),sK34(X0)) ).
cnf(u12944,axiom,
'equivalence_axioms$b'(X0) ).
cnf(u12957,axiom,
'fun_app$m'('mapM$a'(X0),'comp$a'('catDom$c'(X0),sK126(X0),sK127(X0))) != 'comp$b'('catCod$b'(X0),'fun_app$m'('mapM$a'(X0),sK126(X0)),'fun_app$m'('mapM$a'(X0),sK127(X0))) ).
cnf(u1536,axiom,
( ~ 'functor_abbrev$'(X0,X1,X2)
| 'functor$'(X0) ) ).
cnf(u1415,axiom,
'fun_app$'('uuj$',X0) = X0 ).
cnf(u2075,axiom,
'set$' = 'category_ext$'('collect$f'('uui$'),'collect$f'('isZFfun$'),'zFfunDom$','zFfunCod$','uuk$','zFfunComp$','unity$') ).
cnf(u11159,axiom,
( 'mapM$'(X0) != 'mapM$'(X1)
| 'catDom$b'(X0) != 'catDom$b'(X1)
| X0 = X1 ) ).
cnf(u3105,axiom,
( 'functorM$c'('unitFunctor$c'(X0))
| ~ 'category$c'(X0) ) ).
cnf(u10518,axiom,
( ~ 'preFunctor$'('functor_ext$b'(X1,X0,X2,X3))
| 'category$a'(X0) ) ).
cnf(u1944,axiom,
( 'category$c'('fun_app$k'('oppositeCategory$',X0))
| ~ 'category$c'(X0) ) ).
cnf(u1681,axiom,
( sK71(X0) != sK74(X0)
| ~ sP7(X0) ) ).
cnf(u1435,axiom,
( ~ 'functorM$a'(X0)
| 'functorM_axioms$a'(X0) ) ).
cnf(u1589,axiom,
'collect$f'('uuf$'(X0)) = X0 ).
cnf(u1422,axiom,
( 'preFunctor$'('makeFtor$'(X0))
| ~ 'preFunctor$'(X0) ) ).
cnf(u1821,axiom,
( 'category$c'('catCod$a'(X0))
| ~ sP10(X0) ) ).
cnf(u2135,axiom,
'fun_app$'('zFfunCod$',X0) = 'fun_app$'('snd$','fun_app$'('fst$',X0)) ).
cnf(u1587,axiom,
'collect$e'('uud$'(X0)) = X0 ).
cnf(u1819,axiom,
( ~ 'preFunctor$b'(X0)
| sP9(X0) ) ).
cnf(u1576,axiom,
( 'member$e'(X0,'collect$d'(X1))
| ~ 'fun_app$f'(X1,X0) ) ).
cnf(u1455,axiom,
( ~ 'functorExt$'(X0)
| ~ 'functorM$c'(X0)
| 'functor$'(X0) ) ).
cnf(u1426,axiom,
( ~ 'functor$a'(X0)
| 'preFunctor$a'(X0) ) ).
cnf(u5545,axiom,
( 'functorExt$c'('makeFtor$b'(X0))
| ~ 'functorM$a'(X0) ) ).
cnf(u1424,axiom,
( ~ 'functorM$a'(X0)
| 'preFunctor$b'(X0) ) ).
cnf(u11803,axiom,
( X0 != X4
| 'functor_ext$b'(X0,X1,X2,X3) = 'functor_ext$b'(X4,X1,X5,X6) ) ).
cnf(u5546,axiom,
( 'functorM$a'('makeFtor$b'(X0))
| ~ 'functorM$a'(X0) ) ).
cnf(u1693,axiom,
( sK79(X0) != sK82(X0)
| ~ sP8(X0) ) ).
cnf(u11344,axiom,
'fun_app$n'('oppositeCategory$a',X0) = 'fun_app$n'('oppositeCategory$a',X2) ).
cnf(u1989,axiom,
( ~ sP20(X0)
| sP18(X0) ) ).
cnf(u2145,axiom,
( ~ 'fun_app$b'('isZFfun$',X0)
| 'fun_app$b'('isOpair$',X0) ) ).
cnf(u1879,axiom,
( ~ 'fun_app$f'('inverse_rel$b'(X0,X1),X2)
| ~ 'category$'(X0)
| 'inverse$'(X0,X1) = X2 ) ).
cnf(u5557,axiom,
( ~ 'functorM_axioms$a'(X0)
| 'functorM$a'(X0) ) ).
cnf(u1987,axiom,
( ~ sP20(X0)
| sP16(X0) ) ).
cnf(u1832,axiom,
( 'category$a'('catCod$b'(X0))
| ~ sP11(X0) ) ).
cnf(u4554,axiom,
'uuk$' = 'id$a'('set$') ).
cnf(u4196,axiom,
'fun_app$b'('isZFfun$',X0) ).
cnf(u2134,axiom,
'fun_app$'('zFfunDom$',X0) = 'fun_app$'('fst$','fun_app$'('fst$',X0)) ).
cnf(u1884,axiom,
'catDom$c'('functor_ext$b'(X0,X1,X2,X3)) = X0 ).
cnf(u8181,axiom,
'collect$'(X1) = X0 ).
cnf(u8805,axiom,
( X0 != X1
| 'catCod$b'(X0) = 'catCod$b'(X1) ) ).
cnf(u1888,axiom,
'catCod$a'('functor_ext$a'(X0,X1,X2,X3)) = X1 ).
cnf(u1487,axiom,
( ~ 'lSCategory$'(X0)
| 'lSCategory_axioms$'(X0) ) ).
cnf(u7910,axiom,
( 'functor_ext$b'(X1,X2,X3,X4) != X0
| 'catDom$c'(X0) = X1 ) ).
cnf(u4558,axiom,
'set$' = 'category_ext$'('obj$'('set$a'),'collect$f'('isZFfun$'),'zFfunDom$','zFfunCod$','uuk$','zFfunComp$','unity$') ).
cnf(u8202,axiom,
( ~ 'member$'(X1,X0)
| 'fun_app$a'(X2,X1) ) ).
cnf(u2016,axiom,
( ~ 'category_axioms$'(X0)
| sP20(X0) ) ).
cnf(u1399,axiom,
( ~ 'fun_app$c'('uu$'(X0),X1)
| 'member$b'(X1,X0) ) ).
cnf(u1521,axiom,
( ~ 'functor_comp_def$a'(X0,X1)
| 'catCod$a'(X0) = 'catDom$'(X1) ) ).
cnf(u2062,axiom,
'set$a' = 'fun_app$k'('makeCat$','set$') ).
cnf(u3849,axiom,
'more$a'(X0) = sK142(X0) ).
cnf(u1767,axiom,
( ~ 'mapsTo$b'(X0,X1,X2,X3)
| ~ 'category$a'(X0)
| 'member$h'(X3,'obj$c'(X0)) ) ).
cnf(u1800,axiom,
( 'fun_app$f'('isomorphism$b'(X0),sK116(X0,X1,X2))
| ~ 'fun_app$g'('objIso$b'(X0,X1),X2) ) ).
cnf(u1648,axiom,
( ~ sP5(X0)
| sP4(X0) ) ).
cnf(u1527,axiom,
( ~ 'functor_comp_def$c'(X0,X1)
| 'catCod$a'(X0) = 'catDom$a'(X1) ) ).
cnf(u1537,axiom,
( ~ 'functor_abbrev$a'(X0,X1,X2)
| 'catCod$b'(X0) = X2 ) ).
cnf(u1924,axiom,
'mor$'('fun_app$k'('oppositeCategory$',X0)) = 'mor$'(X0) ).
cnf(u1772,axiom,
( ~ 'fun_app$g'('mapsTo$a'(X0,X1,X2),X3)
| ~ 'category$'(X0)
| 'member$f'(X2,'obj$a'(X0)) ) ).
cnf(u7158,axiom,
X0 = X2 ).
cnf(u3576,axiom,
( ~ 'functorExt$b'('identityFunctor$c'(X0))
| 'functor$a'('identityFunctor$c'(X0)) ) ).
cnf(u3089,axiom,
( 'functorM$c'('makeFtor$c'(X0))
| ~ 'functorM$c'(X0) ) ).
cnf(u7151,axiom,
( 'functor_comp_def$b'(X0,X1)
| ~ 'functor$a'(X1) ) ).
cnf(u12599,axiom,
X2 = X3 ).
cnf(u12940,axiom,
sP5(X0) ).
cnf(u2187,axiom,
( 'functor_abbrev$'(X0,'catDom$'(X0),'catCod$c'(X0))
| ~ 'functor$'(X0) ) ).
cnf(u1573,axiom,
( ~ 'member$d'(X0,'collect$c'(X1))
| 'fun_app$e'(X1,X0) ) ).
cnf(u1534,axiom,
( ~ 'functor_abbrev$'(X0,X1,X2)
| 'catCod$c'(X0) = X2 ) ).
cnf(u3080,axiom,
sP10('makeFtor$a'(X0)) ).
cnf(u1571,axiom,
( ~ 'member$c'(X0,'collect$b'(X1))
| 'fun_app$d'(X1,X0) ) ).
cnf(u3852,axiom,
'catDom$c'(X0) = sK139(X0) ).
cnf(u1577,axiom,
( ~ 'member$f'(X0,'collect$e'(X1))
| 'fun_app$g'(X1,X0) ) ).
cnf(u2063,axiom,
'obj$'(X0) = 'obj$'('fun_app$k'('makeCat$',X0)) ).
cnf(u3850,axiom,
'catCod$b'(X0) = sK140(X0) ).
cnf(u12951,axiom,
'equivalence$b'(X0) ).
cnf(u1590,axiom,
( 'fun_app$a'(X1,sK27(X0,X1))
| 'fun_app$a'(X0,sK27(X0,X1))
| 'collect$'(X1) = 'collect$'(X0) ) ).
cnf(u6813,axiom,
'catDom$'(X0) = 'catDom$'(X2) ).
cnf(u1398,axiom,
( 'fun_app$b'('uuf$'(X0),X1)
| ~ 'member$a'(X1,X0) ) ).
cnf(u1408,axiom,
( 'fun_app$g'('uud$'(X0),X1)
| ~ 'member$f'(X1,X0) ) ).
cnf(u2191,axiom,
( 'functor_abbrev$b'(X0,'catDom$a'(X0),'catCod$a'(X0))
| ~ 'functor$a'(X0) ) ).
cnf(u1446,axiom,
( 'functor$a'('makeFtor$a'(X0))
| ~ 'functorM$'(X0) ) ).
cnf(u1878,axiom,
'functor_ext$b'(sK139(X0),sK140(X0),sK141(X0),sK142(X0)) = X0 ).
cnf(u5434,axiom,
( ~ 'functorExt$b'(X0)
| 'functor$a'(X0) ) ).
cnf(u7584,axiom,
'functor_ext$b'('catDom$c'(X1),'catCod$b'(X1),'mapM$a'(X1),X0) = X1 ).
cnf(u1450,axiom,
( ~ 'functor$'(X0)
| 'functorM$c'(X0) ) ).
cnf(u12977,axiom,
'fun_app$m'(X0,'comp$a'('catDom$c'(X1),sK126(X1),sK127(X1))) != 'comp$b'('catCod$b'(X1),'fun_app$m'(X0,sK126(X1)),'fun_app$m'(X0,sK127(X1))) ).
cnf(u6820,axiom,
'functor_abbrev$'(X1,'catCod$'(X0),X2) ).
cnf(u1465,axiom,
( ~ 'functor$a'(X0)
| 'functorExt$b'(X0) ) ).
cnf(u3113,axiom,
( 'extCategory$'('catCod$a'(X0))
| ~ 'preFunctor$a'(X0) ) ).
cnf(u9315,axiom,
'functor_abbrev$c'('makeFtor$b'('homFtorContra$a'(X1,X2)),'fun_app$n'('oppositeCategory$a',X1),X0) ).
cnf(u1868,axiom,
( 'compDefined$c'(X0,X1,'inverse$a'(X0,X1))
| ~ 'category$a'(X0)
| ~ 'isomorphism$c'(X0,X1) ) ).
cnf(u12752,axiom,
'functor_abbrev$c'(X0,'catDom$b'(X3),'set$a') ).
cnf(u8273,axiom,
sK87(X0,X4,X5) = X0 ).
cnf(u1990,axiom,
( ~ sP20(X0)
| sP19(X0) ) ).
cnf(u3042,axiom,
'category_axioms$'('fun_app$k'('oppositeCategory$',X0)) ).
cnf(u8244,axiom,
( ~ 'fun_app$a'(X2,X1)
| 'fun_app$a'(X0,X1) ) ).
cnf(u1902,axiom,
( ~ 'inverse_rel$'(X0,X1,X2)
| ~ 'category$b'(X0)
| 'inverse_rel$'(X0,X2,X1) ) ).
cnf(u10711,axiom,
( ~ 'member$f'(X1,'obj$a'('catDom$c'(X0)))
| ~ 'preFunctor$'(X0) ) ).
cnf(u12625,axiom,
'functor_abbrev$c'('makeFtor$b'('homFtorContra$a'(X1,X2)),'catDom$b'(X0),'set$a') ).
cnf(u1645,axiom,
( ~ sP3(X0)
| 'equivalence_axioms$'(X0) ) ).
cnf(u1751,axiom,
( 'fun_app$g'('mapsTo$a'('catDom$c'(X0),sK103(X0),sK104(X0)),sK105(X0))
| 'functorM_axioms$b'(X0) ) ).
cnf(u1643,axiom,
( sK49(X0) != sK52(X0)
| sP2(X0) ) ).
cnf(u2036,axiom,
'id$a'('category_ext$'(X0,X1,X2,X3,X4,X5,X6)) = X4 ).
cnf(u1403,axiom,
( ~ 'fun_app$e'('uub$'(X0),X1)
| 'member$d'(X1,X0) ) ).
cnf(u2512,axiom,
( ~ 'equivalence_axioms$a'(X0)
| ~ 'functor$'(X0) ) ).
cnf(u3041,axiom,
'category_axioms$'('set$a') ).
cnf(u12783,axiom,
'pair$'(X0,sK23(X1,X2)) = X2 ).
cnf(u3449,axiom,
'lSCategory_axioms$'('fun_app$n'('oppositeCategory$a',X0)) ).
cnf(u1540,axiom,
( ~ 'functor_abbrev$b'(X0,X1,X2)
| 'catCod$a'(X0) = X2 ) ).
cnf(u11190,axiom,
'functor_abbrev$c'(X0,'fun_app$n'('oppositeCategory$a',X1),'set$a') ).
cnf(u1518,axiom,
( ~ 'functor_comp_def$'(X0,X1)
| 'catCod$'(X0) = 'catDom$'(X1) ) ).
cnf(u1791,axiom,
( ~ 'mapsTo$c'(X0,X4,X3,X5)
| ~ 'mapsTo$c'(X0,X1,X2,X3)
| 'compDefined$d'(X0,X1,X4) ) ).
cnf(u1790,axiom,
( ~ 'mapsTo$b'(X0,X4,X3,X5)
| ~ 'mapsTo$b'(X0,X1,X2,X3)
| 'compDefined$c'(X0,X1,X4) ) ).
cnf(u1544,axiom,
( ~ 'functor_abbrev$c'(X0,X1,X2)
| 'catDom$b'(X0) = X1 ) ).
cnf(u1423,axiom,
( ~ 'functorM$'(X0)
| 'preFunctor$a'(X0) ) ).
cnf(u1522,axiom,
( ~ 'functor_comp_def$a'(X0,X1)
| 'functor$'(X1) ) ).
cnf(u2045,axiom,
( ~ 'member$e'(X1,'mor$a'(X0))
| ~ 'lSCategory$'(X0)
| 'zF2mor$'(X0,'fun_app$l'('mor2ZF$'(X0),X1)) = X1 ) ).
cnf(u12986,axiom,
'fun_app$m'(X1,'comp$a'('catDom$c'(X2),X0,sK127(X2))) != 'comp$b'('catCod$b'(X2),'fun_app$m'(X1,X0),'fun_app$m'(X1,sK127(X2))) ).
cnf(u3450,axiom,
'category$'('fun_app$n'('oppositeCategory$a',X0)) ).
cnf(u3088,axiom,
( 'functorExt$'('makeFtor$c'(X0))
| ~ 'functorM$c'(X0) ) ).
cnf(u1520,axiom,
( ~ 'functor_comp_def$'(X0,X1)
| 'functor$b'(X0) ) ).
cnf(u1580,axiom,
( 'member$'(X0,'collect$'(X1))
| ~ 'fun_app$a'(X1,X0) ) ).
cnf(u2329,axiom,
'category$'('c$') ).
cnf(u6936,axiom,
'functor_abbrev$c'(X1,'catDom$b'(X1),X0) ).
cnf(u7585,axiom,
'functor_ext$'('catDom$b'(X1),X2,'mapM$'(X1),X0) = X1 ).
cnf(u1428,axiom,
( ~ 'functor$c'(X0)
| 'preFunctor$'(X0) ) ).
cnf(u8914,axiom,
'fun_app$f'('compDefined$b'(X1,'inverse$'(X1,X0)),X0) ).
cnf(u1432,axiom,
( ~ 'functorM$'(X0)
| 'functorM_axioms$'(X0) ) ).
cnf(u1975,axiom,
( 'fun_app$'('fun_app$h'('comp$'(X0),'fun_app$'('fun_app$h'('comp$'(X0),sK146(X0)),sK147(X0))),sK148(X0)) != 'fun_app$'('fun_app$h'('comp$'(X0),sK146(X0)),'fun_app$'('fun_app$h'('comp$'(X0),sK147(X0)),sK148(X0)))
| ~ sP13(X0) ) ).
cnf(u1445,axiom,
( 'functor$'('makeFtor$c'(X0))
| ~ 'functorM$c'(X0) ) ).
cnf(u7730,axiom,
'functor_ext$'(X1,X2,X0,X3) = 'functor_ext$'('catDom$b'('functor_ext$'(X1,X2,X0,X3)),X4,X0,X5) ).
cnf(u1468,axiom,
( ~ 'functor$b'(X0)
| 'functorExt$c'(X0) ) ).
cnf(u11666,axiom,
( 'catDom$c'(X0) != X1
| 'functor_ext$b'(X1,'catCod$b'(X0),X2,X3) = X0 ) ).
cnf(u1449,axiom,
( 'functorM$'('identityFunctor$c'(X0))
| ~ 'category$c'(X0) ) ).
cnf(u12895,axiom,
X0 = X2 ).
cnf(u12997,axiom,
'fun_app$m'(X2,X0) != 'comp$b'(X1,'fun_app$m'(X2,X3),'fun_app$m'(X2,X4)) ).
cnf(u1978,axiom,
( ~ 'fun_app$b'('mapsTo$'(X0,'fun_app$'('fun_app$h'('comp$'(X0),sK149(X0)),sK152(X0)),sK150(X0)),sK153(X0))
| ~ sP12(X0) ) ).
cnf(u1856,axiom,
'functor_ext$a'('catDom$a'(X0),'catCod$a'(X0),'mapM$b'(X0),'more$b'(X0)) = X0 ).
cnf(u1485,axiom,
( 'category$c'('catCod$a'(X0))
| ~ 'preFunctor$a'(X0) ) ).
cnf(u9324,axiom,
'makeFtor$b'('homFtorContra$a'(X0,X1)) = 'functor_ext$'('fun_app$n'('oppositeCategory$a',X0),X2,'mapM$'('makeFtor$b'('homFtorContra$a'(X0,X1))),X3) ).
cnf(u1886,axiom,
'mapM$b'('functor_ext$a'(X0,X1,X2,X3)) = X2 ).
cnf(u1489,axiom,
( ~ 'lSCategory_axioms$'(X0)
| ~ 'category$'(X0)
| 'lSCategory$'(X0) ) ).
cnf(u2158,negated_conjecture,
~ 'preFunctor$'('functor_ext$b'('c$','catExp$'('fun_app$n'('oppositeCategory$a','c$'),'set$a'),'yFtorNT$'('c$'),'unity$')) ).
cnf(u1890,axiom,
( 'fun_app$f'('inverse_rel$b'(X0,X1),'inverse$'(X0,X1))
| ~ 'category$'(X0)
| ~ 'fun_app$f'('isomorphism$b'(X0),X1) ) ).
cnf(u12954,axiom,
( 'fun_app$m'('mapM$a'(X0),'comp$a'('catDom$c'(X0),sK126(X0),sK127(X0))) != 'comp$b'('catCod$b'(X0),'fun_app$m'('mapM$a'(X0),sK126(X0)),'fun_app$m'('mapM$a'(X0),sK127(X0)))
| ~ 'category$'('catDom$c'(X0))
| ~ 'category$a'('catCod$b'(X0)) ) ).
cnf(u1896,axiom,
( ~ 'fun_app$f'('inverse_rel$b'(X0,X1),X3)
| ~ 'category$'(X0)
| ~ 'fun_app$f'('inverse_rel$b'(X0,X1),X2)
| X2 = X3 ) ).
cnf(u10452,negated_conjecture,
~ 'preFunctor$'('functor_ext$b'('c$','catExp$'('fun_app$n'('oppositeCategory$a','c$'),X0),X1,'unity$')) ).
cnf(u1407,axiom,
( ~ 'fun_app$g'('uud$'(X0),X1)
| 'member$f'(X1,X0) ) ).
cnf(u1541,axiom,
( ~ 'functor_abbrev$b'(X0,X1,X2)
| 'catDom$a'(X0) = X1 ) ).
cnf(u4198,axiom,
'fun_app$b'('isFun$','fun_app$'('snd$',X0)) ).
cnf(u1901,axiom,
( ~ 'inverse_rel$a'(X0,X1,X2)
| ~ 'category$a'(X0)
| 'inverse_rel$a'(X0,X2,X1) ) ).
cnf(u7150,axiom,
( 'functor_comp_def$c'(X0,X1)
| ~ 'functor$a'(X0)
| ~ 'functor$a'(X1) ) ).
cnf(u1535,axiom,
( ~ 'functor_abbrev$'(X0,X1,X2)
| 'catDom$'(X0) = X1 ) ).
cnf(u1669,axiom,
( sK63(X0) != sK66(X0)
| ~ sP6(X0) ) ).
cnf(u11227,axiom,
'mapM$'(X0) = X3 ).
cnf(u6835,axiom,
'functor_abbrev$'(X1,'catDom$'(X0),X2) ).
cnf(u8492,axiom,
'functor_ext$b'(X1,X2,X0,X3) = 'functor_ext$b'(X1,X2,X0,X4) ).
cnf(u7313,axiom,
( 'functor_abbrev$b'(X1,X2,X0)
| ~ 'functor$a'(X1) ) ).
cnf(u1418,axiom,
'lSCategory$'('c$') ).
cnf(u6788,axiom,
( 'catCod$'(X0) != 'catDom$'(X1)
| 'functor_comp_def$'(X0,X1) ) ).
cnf(u6923,axiom,
X0 = X2 ).
cnf(u7363,axiom,
'fun_app$a'('uul$'(X0),'pair$'(X2,X3)) ).
cnf(u1831,axiom,
( ~ sP10(X0)
| 'preFunctor$a'(X0) ) ).
cnf(u6814,axiom,
'catCod$'(X0) = 'catCod$'(X1) ).
cnf(u1416,axiom,
'fun_app$b'('uui$',X0) ).
cnf(u1406,axiom,
( 'fun_app$f'('uuc$'(X0),X1)
| ~ 'member$e'(X1,X0) ) ).
cnf(u8201,axiom,
( ~ 'fun_app$a'(X2,X1)
| 'member$'(X1,X0) ) ).
cnf(u2080,axiom,
( 'member$a'(X0,'mor$'('set$a'))
| ~ 'fun_app$b'('isZFfun$',X0) ) ).
cnf(u1429,axiom,
( ~ 'preFunctor$a'(X0)
| 'functorM$'(X0)
| ~ 'functorM_axioms$'(X0) ) ).
cnf(u1452,axiom,
( ~ 'functor$a'(X0)
| 'functorM$'(X0) ) ).
cnf(u1830,axiom,
( ~ 'preFunctor$a'(X0)
| sP10(X0) ) ).
cnf(u2213,axiom,
( 'catDom$c'(X1) = sK87('catDom$c'(X1),X3,X4)
| 'catDom_update$'(X4,X1) = 'catDom_update$'(X3,X1) ) ).
cnf(u9272,axiom,
( ~ 'fun_app$f'('isomorphism$b'(X0),'id$'(X0,X1))
| ~ 'member$f'(X1,'obj$a'(X0))
| ~ 'category$'(X0) ) ).
cnf(u9378,axiom,
'compDefined$c'('catExp$'('fun_app$n'('oppositeCategory$a',X1),X0),'fun_app$m'(X2,X3),'fun_app$m'(X2,X4)) ).
cnf(u6825,axiom,
'functor_abbrev$c'(X1,'catDom$b'(X1),'catDom$'(X0)) ).
cnf(u9376,axiom,
'compDefined$c'('catExp$'('fun_app$n'('oppositeCategory$a',X1),'set$a'),'fun_app$m'(X0,X2),'fun_app$m'(X0,X3)) ).
cnf(u1459,axiom,
( ~ 'functor$'(X0)
| 'functorExt$'(X0) ) ).
cnf(u11342,axiom,
'functor_abbrev$c'(X1,'fun_app$n'('oppositeCategory$a',X2),X0) ).
cnf(u1473,axiom,
( ~ 'lSCategory$'(X0)
| 'category$'(X0) ) ).
cnf(u1876,axiom,
( 'functor_ext$b'(X0,X1,X2,X3) != 'functor_ext$b'(X4,X5,X6,X7)
| X0 = X4 ) ).
cnf(u4555,axiom,
'obj$'('set$a') = 'collect$f'('uui$') ).
cnf(u8834,axiom,
( ~ 'fun_app$g'('mapsTo$a'(X0,X3,X1),X2)
| ~ 'fun_app$f'('isomorphism$b'(X0),X3) ) ).
cnf(u1874,axiom,
( 'functor_ext$b'(X0,X1,X2,X3) != 'functor_ext$b'(X4,X5,X6,X7)
| X2 = X6 ) ).
cnf(u1833,axiom,
( 'category$'('catDom$c'(X0))
| ~ sP11(X0) ) ).
cnf(u1880,axiom,
( ~ 'inverse_rel$a'(X0,X1,X2)
| ~ 'category$a'(X0)
| 'inverse$a'(X0,X1) = X2 ) ).
cnf(u4199,axiom,
'fun_app$b'('isFun$','fun_app$'('zFfunCod$',X0)) ).
cnf(u1479,axiom,
( ~ 'equivalence$a'(X0)
| 'functor$'(X0) ) ).
cnf(u11366,axiom,
'lSCategory$'('catDom$b'(X0)) ).
cnf(u13014,axiom,
'natTransP$a'(X0) ).
cnf(u1486,axiom,
( 'category$a'('catCod$b'(X0))
| ~ 'preFunctor$'(X0) ) ).
cnf(u1885,axiom,
'mapM$'('functor_ext$'(X0,X1,X2,X3)) = X2 ).
cnf(u1883,axiom,
'catDom$a'('functor_ext$a'(X0,X1,X2,X3)) = X0 ).
cnf(u1519,axiom,
( ~ 'functor_comp_def$'(X0,X1)
| 'functor$'(X1) ) ).
cnf(u1889,axiom,
'catCod$b'('functor_ext$b'(X0,X1,X2,X3)) = X1 ).
cnf(u1764,axiom,
( 'fun_app$g'('mapsTo$a'(X0,'id$'(X0,X1),X1),X1)
| ~ 'category$'(X0)
| ~ 'member$f'(X1,'obj$a'(X0)) ) ).
cnf(u1542,axiom,
( ~ 'functor_abbrev$b'(X0,X1,X2)
| 'functor$a'(X0) ) ).
cnf(u1768,axiom,
( ~ 'fun_app$g'('mapsTo$a'(X0,X1,X2),X3)
| ~ 'category$'(X0)
| 'member$f'(X3,'obj$a'(X0)) ) ).
cnf(u1402,axiom,
( 'fun_app$d'('uua$'(X0),X1)
| ~ 'member$c'(X1,X0) ) ).
cnf(u8478,axiom,
'functor_ext$b'('catDom$c'(X1),'catCod$b'(X1),X0,X2) = X1 ).
cnf(u2017,axiom,
( ~ sP20(X0)
| 'category_axioms$'(X0) ) ).
cnf(u1396,axiom,
( 'fun_app$a'('uue$'(X0),X1)
| ~ 'member$'(X1,X0) ) ).
cnf(u1797,axiom,
( 'isomorphism$c'(X0,sK115(X0,X1,X2))
| ~ 'objIso$a'(X0,X1,X2) ) ).
cnf(u7037,axiom,
'id$a'(X0) = X5 ).
cnf(u1400,axiom,
( 'fun_app$c'('uu$'(X0),X1)
| ~ 'member$b'(X1,X0) ) ).
cnf(u1524,axiom,
( ~ 'functor_comp_def$b'(X0,X1)
| 'catCod$'(X0) = 'catDom$a'(X1) ) ).
cnf(u6422,axiom,
( 'functor_abbrev$'(X1,'catDom$'(X1),X0)
| ~ 'functor$'(X1) ) ).
cnf(u1528,axiom,
( ~ 'functor_comp_def$c'(X0,X1)
| 'functor$a'(X1) ) ).
cnf(u1943,axiom,
'obj$'(X0) = 'obj$'('fun_app$k'('oppositeCategory$',X0)) ).
cnf(u10740,axiom,
( ~ 'member$f'(X7,'obj$a'('catDom$c'(X0)))
| ~ sP11(X0) ) ).
cnf(u3851,axiom,
'mapM$a'(X0) = sK141(X0) ).
cnf(u2197,axiom,
( 'catCod$b'(X1) = sK29('catCod$b'(X1),X3,X4)
| 'catCod_update$'(X4,X1) = 'catCod_update$'(X3,X1) ) ).
cnf(u2040,axiom,
( 'category$a'('catExp$'('fun_app$n'('oppositeCategory$a',X0),'set$a'))
| ~ 'lSCategory$'(X0) ) ).
cnf(u2093,axiom,
( ~ 'fun_app$b'('mapsTo$'('set$a',X0,X1),X2)
| 'fun_app$'('zFfunCod$',X0) = X2 ) ).
cnf(u10527,axiom,
( ~ sP11('functor_ext$b'(X1,X0,X2,X3))
| 'category$a'(X0) ) ).
cnf(u11667,axiom,
( X1 != X5
| X0 != X4
| 'functor_ext$b'(X1,X0,X2,X3) = 'functor_ext$b'(X5,X4,X6,X7) ) ).
cnf(u1453,axiom,
( ~ 'functor$b'(X0)
| 'functorM$a'(X0) ) ).
cnf(u1457,axiom,
( ~ 'functorM$'(X0)
| 'functor$a'(X0)
| ~ 'functorExt$b'(X0) ) ).
cnf(u7610,axiom,
X0 = X1 ).
cnf(u1578,axiom,
( 'member$f'(X0,'collect$e'(X1))
| ~ 'fun_app$g'(X1,X0) ) ).
cnf(u8240,axiom,
'fun_app$a'(X0,'pair$'(X1,X2)) ).
cnf(u10078,axiom,
( ~ 'mapsTo$b'(X0,X3,X1,X2)
| ~ 'isomorphism$c'(X0,X3) ) ).
cnf(u1988,axiom,
( ~ sP20(X0)
| sP17(X0) ) ).
cnf(u3104,axiom,
( 'functorExt$'('unitFunctor$c'(X0))
| ~ 'category$c'(X0) ) ).
cnf(u5554,axiom,
'category$'('catDom$b'(X0)) ).
cnf(u7001,axiom,
( 'functor_abbrev$b'(X1,X0,'catCod$a'(X1))
| ~ 'functor$a'(X1) ) ).
cnf(u10460,negated_conjecture,
~ 'preFunctor$'('functor_ext$b'('c$','catExp$'('fun_app$n'('oppositeCategory$a','c$'),X1),X2,X0)) ).
cnf(u1867,axiom,
( 'fun_app$f'('compDefined$b'(X0,X1),'inverse$'(X0,X1))
| ~ 'category$'(X0)
| ~ 'fun_app$f'('isomorphism$b'(X0),X1) ) ).
cnf(u1873,axiom,
( 'functor_ext$b'(X0,X1,X2,X3) != 'functor_ext$b'(X4,X5,X6,X7)
| X3 = X7 ) ).
cnf(u1887,axiom,
'mapM$a'('functor_ext$b'(X0,X1,X2,X3)) = X2 ).
cnf(u3044,axiom,
sP20('set$a') ).
cnf(u2520,axiom,
'extCategory$'('fun_app$k'('oppositeCategory$',X0)) ).
cnf(u4583,axiom,
'preFunctor$a'('constFunctor$a'(X0,X1,X2)) ).
cnf(u7539,axiom,
( ~ 'member$g'(X1,'obj$b'(X0))
| ~ 'category$b'(X0) ) ).
cnf(u2035,axiom,
'obj$'('category_ext$'(X0,X1,X2,X3,X4,X5,X6)) = X0 ).
cnf(u1397,axiom,
( ~ 'fun_app$b'('uuf$'(X0),X1)
| 'member$a'(X1,X0) ) ).
cnf(u8193,axiom,
X0 = X1 ).
cnf(u2048,axiom,
( ~ 'category$c'(X0)
| 'extCategory$'(X0) ) ).
cnf(u1401,axiom,
( ~ 'fun_app$d'('uua$'(X0),X1)
| 'member$c'(X1,X0) ) ).
cnf(u1525,axiom,
( ~ 'functor_comp_def$b'(X0,X1)
| 'functor$a'(X1) ) ).
cnf(u1420,axiom,
( 'preFunctor$a'('makeFtor$a'(X0))
| ~ 'preFunctor$a'(X0) ) ).
cnf(u9340,axiom,
sK29(X0,X4,X5) = X0 ).
cnf(u1798,axiom,
( 'mapsTo$b'(X0,sK115(X0,X1,X2),X1,X2)
| ~ 'objIso$a'(X0,X1,X2) ) ).
cnf(u2024,axiom,
( ~ 'category$c'(X0)
| 'category_axioms$'(X0) ) ).
cnf(u1529,axiom,
( ~ 'functor_comp_def$c'(X0,X1)
| 'functor$a'(X0) ) ).
cnf(u8233,axiom,
'member$'('pair$'(X0,X1),X2) ).
cnf(u12647,axiom,
( ~ 'member$f'(X1,'obj$a'(X0))
| ~ 'category$'(X0) ) ).
cnf(u1545,axiom,
( ~ 'functor_abbrev$c'(X0,X1,X2)
| 'functor$b'(X0) ) ).
cnf(u11189,axiom,
'catDom$b'(X0) = 'fun_app$n'('oppositeCategory$a',X1) ).
cnf(u1559,axiom,
( ~ 'member$h'(X1,'obj$c'('catDom$i'('identityFunctor$a'(X0))))
| ~ 'category$a'(X0)
| 'mapO$i'('identityFunctor$a'(X0),X1) = X1 ) ).
cnf(u8507,axiom,
'functor_ext$b'(X1,X0,X2,X3) = 'functor_ext$b'(X1,X0,X4,X5) ).
cnf(u2460,axiom,
( 'functorExt$b'('makeFtor$a'(X0))
| ~ 'functorM$'(X0) ) ).
cnf(u1936,axiom,
( 'lSCategory$'('fun_app$n'('oppositeCategory$a',X0))
| ~ 'lSCategory$'(X0) ) ).
cnf(u1441,axiom,
( 'preFunctor$a'('identityFunctor$c'(X0))
| ~ 'category$c'(X0) ) ).
cnf(u1427,axiom,
( ~ 'functor$b'(X0)
| 'preFunctor$b'(X0) ) ).
cnf(u1581,axiom,
( ~ 'member$a'(X0,'collect$f'(X1))
| 'fun_app$b'(X1,X0) ) ).
cnf(u1842,axiom,
( ~ sP11(X0)
| 'preFunctor$'(X0) ) ).
cnf(u1579,axiom,
( ~ 'member$'(X0,'collect$'(X1))
| 'fun_app$a'(X1,X0) ) ).
cnf(u1447,axiom,
( 'functor$b'('makeFtor$b'(X0))
| ~ 'functorM$a'(X0) ) ).
cnf(u1585,axiom,
'collect$c'('uub$'(X0)) = X0 ).
cnf(u1972,axiom,
( sK145(X0) != 'fun_app$'('fun_app$h'('comp$'(X0),sK145(X0)),'fun_app$'('id$a'(X0),'fun_app$'('cod$'(X0),sK145(X0))))
| ~ sP14(X0) ) ).
cnf(u2193,axiom,
( 'functor_abbrev$c'(X0,'catDom$b'(X0),'catCod$'(X0))
| ~ 'functor$b'(X0) ) ).
cnf(u1970,axiom,
( sK144(X0) != 'fun_app$'('fun_app$h'('comp$'(X0),'fun_app$'('id$a'(X0),'fun_app$'('dom$'(X0),sK144(X0)))),sK144(X0))
| ~ sP15(X0) ) ).
cnf(u8009,axiom,
( X0 != X1
| 'catDom$c'(X0) = 'catDom$c'(X1) ) ).
cnf(u7354,axiom,
'functor_ext$a'(X1,X2,X0,'more$b'(X3)) = X3 ).
cnf(u1410,axiom,
( ~ 'fun_app$a'('uul$'(X0),X1)
| 'pair$'(sK22(X0,X1),sK23(X0,X1)) = X1 ) ).
cnf(u2111,axiom,
( ~ 'natTransP$a'(X0)
| sP21(X0) ) ).
cnf(u1458,axiom,
( ~ 'functorExt$c'(X0)
| ~ 'functorM$a'(X0)
| 'functor$b'(X0) ) ).
cnf(u1608,axiom,
( ~ sP1(X0)
| sP0(X0) ) ).
cnf(u1857,axiom,
'functor_ext$b'('catDom$c'(X0),'catCod$b'(X0),'mapM$a'(X0),'more$a'(X0)) = X0 ).
cnf(u3152,axiom,
( ~ 'functorExt$b'('makeFtor$a'(X0))
| 'functor$a'('makeFtor$a'(X0)) ) ).
cnf(u12759,axiom,
'catDom$b'(X0) = 'catDom$b'(X1) ).
cnf(u1644,axiom,
( ~ 'equivalence_axioms$'(X0)
| sP3(X0) ) ).
cnf(u1766,axiom,
( ~ 'mapsTo$c'(X0,X1,X2,X3)
| ~ 'category$b'(X0)
| 'member$g'(X3,'obj$b'(X0)) ) ).
cnf(u6862,axiom,
'functor_abbrev$c'(X1,'catDom$b'(X1),'catCod$'(X0)) ).
cnf(u7000,axiom,
'functor_ext$a'(X0,'catCod$a'(X1),'mapM$b'(X1),'more$b'(X1)) = X1 ).
cnf(u1897,axiom,
( ~ 'inverse_rel$a'(X0,X1,X3)
| ~ 'category$a'(X0)
| ~ 'inverse_rel$a'(X0,X1,X2)
| X2 = X3 ) ).
cnf(u2675,axiom,
X0 = X2 ).
cnf(u10859,axiom,
'fun_app$f'('compDefined$b'(X1,X2),X0) ).
cnf(u9313,axiom,
'fun_app$n'('oppositeCategory$a',X0) = 'catDom$b'('makeFtor$b'('homFtorContra$a'(X0,X1))) ).
cnf(u8396,axiom,
~ 'equivalence$'(X0) ).
cnf(u1404,axiom,
( 'fun_app$e'('uub$'(X0),X1)
| ~ 'member$d'(X1,X0) ) ).
cnf(u2165,axiom,
( 'functor_abbrev$c'('makeFtor$b'('homFtorContra$a'(X0,X1)),'fun_app$n'('oppositeCategory$a',X0),'set$a')
| ~ 'lSCategory$'(X0)
| ~ 'member$f'(X1,'obj$a'(X0)) ) ).
cnf(u1575,axiom,
( ~ 'member$e'(X0,'collect$d'(X1))
| 'fun_app$f'(X1,X0) ) ).
cnf(u10735,axiom,
( 'member$f'(sK43(X0),'obj$a'('catDom$c'(X0)))
| sP3(X0) ) ).
cnf(u4586,axiom,
sP10('constFunctor$a'(X0,X1,X2)) ).
cnf(u1532,axiom,
( 'category$c'('catDom$a'(X0))
| ~ 'preFunctor$a'(X0) ) ).
cnf(u10454,negated_conjecture,
~ 'preFunctor$'('functor_ext$b'('c$','catExp$'('fun_app$n'('oppositeCategory$a','c$'),'set$a'),X1,X0)) ).
cnf(u11370,axiom,
'category$a'('catExp$'('catDom$b'(X0),X2)) ).
cnf(u6931,axiom,
'functor_abbrev$'(X1,X0,X2) ).
cnf(u4595,axiom,
~ 'equivalence$c'(X0) ).
cnf(u12763,axiom,
'functor_abbrev$c'(X1,'catDom$b'(X2),X0) ).
cnf(u1584,axiom,
'collect$b'('uua$'(X0)) = X0 ).
cnf(u4612,axiom,
( ~ 'category_axioms$'(X0)
| 'category$c'(X0) ) ).
cnf(u7048,negated_conjecture,
~ 'preFunctor$'('functor_ext$b'('c$','catExp$'('fun_app$n'('oppositeCategory$a','c$'),X0),'yFtorNT$'('c$'),'unity$')) ).
cnf(u1543,axiom,
( ~ 'functor_abbrev$c'(X0,X1,X2)
| 'catCod$'(X0) = X2 ) ).
cnf(u7574,axiom,
'functor_ext$a'(X1,X2,X3,X0) = X4 ).
cnf(u7036,axiom,
'obj$'(X0) = X1 ).
cnf(u10663,axiom,
( ~ 'mapsTo$b'(X0,X1,X2,X3)
| ~ 'category$a'(X0) ) ).
cnf(u1425,axiom,
( ~ 'functorM$b'(X0)
| 'preFunctor$'(X0) ) ).
cnf(u10528,axiom,
( ~ sP11('functor_ext$b'(X0,X1,X2,X3))
| 'category$'(X0) ) ).
cnf(u8232,axiom,
( ~ 'member$'(X0,X2)
| 'member$'(X0,X1) ) ).
cnf(u3098,axiom,
( sP10('identityFunctor$c'(X0))
| ~ 'category$c'(X0) ) ).
cnf(u1569,axiom,
( ~ 'member$b'(X0,'collect$a'(X1))
| 'fun_app$c'(X1,X0) ) ).
cnf(u11514,axiom,
( 'catCod$b'(X0) != 'catCod$b'(X1)
| 'catDom$c'(X0) != 'catDom$c'(X1)
| X0 = X1 ) ).
cnf(u2461,axiom,
( 'functorM$'('makeFtor$a'(X0))
| ~ 'functorM$'(X0) ) ).
cnf(u1583,axiom,
'collect$a'('uu$'(X0)) = X0 ).
cnf(u2346,axiom,
~ 'equivalence_axioms$c'(X0) ).
cnf(u2339,axiom,
'lSCategory_axioms$'('c$') ).
cnf(u1582,axiom,
( 'member$a'(X0,'collect$f'(X1))
| ~ 'fun_app$b'(X1,X0) ) ).
cnf(u12996,axiom,
'comp$b'(X0,'fun_app$m'(X1,X5),'fun_app$m'(X1,X6)) != 'fun_app$m'(X1,'comp$a'(X2,X5,X6)) ).
cnf(u1588,axiom,
'collect$'('uue$'(X0)) = X0 ).
cnf(u1451,axiom,
( ~ 'functor$c'(X0)
| 'functorM$b'(X0) ) ).
cnf(u3112,axiom,
( 'category_axioms$'('catCod$a'(X0))
| ~ 'preFunctor$a'(X0) ) ).
cnf(u7223,axiom,
X0 = X7 ).
cnf(u1586,axiom,
'collect$d'('uuc$'(X0)) = X0 ).
cnf(u7343,axiom,
'functor_ext$a'(X1,X0,'mapM$b'(X2),'more$b'(X2)) = X2 ).
cnf(u1471,axiom,
( 'functor$'('unitFunctor$c'(X0))
| ~ 'category$c'(X0) ) ).
cnf(u1841,axiom,
( ~ 'preFunctor$'(X0)
| sP11(X0) ) ).
cnf(u1855,axiom,
'functor_ext$'('catDom$b'(X0),'catCod$'(X0),'mapM$'(X0),'more$'(X0)) = X0 ).
cnf(u11367,axiom,
'lSCategory_axioms$'('catDom$b'(X0)) ).
cnf(u3136,axiom,
'functorM_axioms$'('makeFtor$a'(X0)) ).
cnf(u1628,axiom,
( ~ sP3(X0)
| sP2(X0) ) ).
cnf(u2638,axiom,
'obj$'('set$a') = 'obj$'('set$') ).
cnf(u12890,axiom,
'pair$'(X1,X0) = X3 ).
cnf(u1875,axiom,
( 'functor_ext$b'(X0,X1,X2,X3) != 'functor_ext$b'(X4,X5,X6,X7)
| X1 = X5 ) ).
cnf(u12992,axiom,
'fun_app$m'(X1,'comp$a'('catDom$c'(X2),X3,X0)) != 'comp$b'('catCod$b'(X2),'fun_app$m'(X1,X3),'fun_app$m'(X1,X0)) ).
cnf(u11306,axiom,
X0 = X4 ).
cnf(u5588,axiom,
'functorM_axioms$a'('makeFtor$b'(X0)) ).
cnf(u11983,axiom,
( X0 != X1
| 'functor_ext$b'(X2,X0,X3,X4) = 'functor_ext$b'(X2,X1,X5,X6) ) ).
cnf(u2023,axiom,
'category$c'('set$a') ).
cnf(u7026,axiom,
'functor_ext$'('catDom$b'(X1),X0,'mapM$'(X1),'more$'(X1)) = X1 ).
cnf(u1822,axiom,
( 'category$c'('catDom$a'(X0))
| ~ sP10(X0) ) ).
cnf(u1497,axiom,
( ~ 'equivalence$b'(X0)
| 'equivalence_axioms$b'(X0) ) ).
cnf(u1900,axiom,
( ~ 'fun_app$f'('inverse_rel$b'(X0,X1),X2)
| ~ 'category$'(X0)
| 'fun_app$f'('inverse_rel$b'(X0,X2),X1) ) ).
cnf(u1405,axiom,
( ~ 'fun_app$f'('uuc$'(X0),X1)
| 'member$e'(X1,X0) ) ).
cnf(u3059,axiom,
sP20('fun_app$k'('oppositeCategory$',X0)) ).
cnf(u7045,axiom,
( 'category$a'('catExp$'('fun_app$n'('oppositeCategory$a',X1),X0))
| ~ 'lSCategory$'(X1) ) ).
cnf(u2022,axiom,
'member$a'(X0,'obj$'('set$a')) ).
cnf(u2421,axiom,
'extCategory$'('set$a') ).
cnf(u1904,axiom,
'more$a'('functor_ext$b'(X0,X1,X2,X3)) = X3 ).
cnf(u7154,axiom,
( 'functor_comp_def$a'(X0,X1)
| ~ 'functor$a'(X0) ) ).
cnf(u1395,axiom,
( ~ 'fun_app$a'('uue$'(X0),X1)
| 'member$'(X1,X0) ) ).
cnf(u1533,axiom,
( 'category$'('catDom$c'(X0))
| ~ 'preFunctor$'(X0) ) ).
cnf(u4352,axiom,
'functorExt$b'('identityFunctor$c'(X0)) ).
cnf(u7810,negated_conjecture,
~ 'preFunctor$'('functor_ext$b'('c$','catExp$'('fun_app$n'('oppositeCategory$a','c$'),'set$a'),X0,'unity$')) ).
cnf(u10524,axiom,
( ~ 'preFunctor$'('functor_ext$b'(X0,X1,X2,X3))
| 'category$'(X0) ) ).
cnf(u11527,axiom,
( 'catCod$b'(X1) != X0
| 'catDom$c'(X1) != X2
| 'functor_ext$b'(X2,X0,X3,X4) = X1 ) ).
cnf(u5371,axiom,
'category$b'('catExp$a'(X0,X1)) ).
cnf(u1523,axiom,
( ~ 'functor_comp_def$a'(X0,X1)
| 'functor$a'(X0) ) ).
cnf(u8757,axiom,
( 'functor_ext$b'(X1,X2,X3,X4) != X0
| 'catCod$b'(X0) = X2 ) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP304_1 : TPTP v9.3.1. Released v8.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.38 % Computer : n011.cluster.edu
% 0.12/0.38 % Model : x86_64 x86_64
% 0.12/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.38 % Memory : 8046.5625MB
% 0.12/0.38 % OS : Linux 6.8.0-71-generic
% 0.12/0.38 % CPULimit : 300
% 0.12/0.38 % WCLimit : 300
% 0.12/0.38 % DateTime : Sun Sep 27 12:54:00 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 1.89/0.83 % (2371881)Will run a generic schedule for satisfiability detection.
% 1.89/0.83 % (2371891)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3405716584:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 1.89/0.83 % (2371887)% WARNING: option uhcvi not known.
% 1.89/0.83 % (2371886)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2798360554_2999 on theBenchmark for (2999ds/0Mi)
% 1.89/0.83 % (2371887)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1099891706:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 1.89/0.83 % (2371888)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3234987047:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 1.89/0.83 % (2371889)dis+10_1_sil=32000:sp=arity:random_seed=3874171416:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 1.89/0.83 % (2371890)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2997069914:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 1.89/0.83 % (2371892)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=457024906:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 1.89/0.83 % (2371891)Instruction limit reached!
% 1.89/0.83 % (2371891)------------------------------
% 1.89/0.83 % (2371891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.83 % (2371891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.83 % (2371891)CaDiCaL version: 2.1.3
% 1.89/0.83 % (2371891)Termination reason: Instruction limit
% 1.89/0.83 % (2371891)Termination phase: Saturation
% 1.89/0.83 % (2371891)Time elapsed: 0.042 s
% 1.89/0.83 % (2371891)Peak memory usage: 14 MB
% 1.89/0.83 % (2371891)Instructions burned: 133 (million)
% 1.89/0.83 % (2371900)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3923237890:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 1.89/0.83 % (2371889)Instruction limit reached!
% 1.89/0.83 % (2371889)------------------------------
% 1.89/0.83 % (2371889)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.83 % (2371889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.83 % (2371889)CaDiCaL version: 2.1.3
% 1.89/0.83 % (2371889)Termination reason: Instruction limit
% 1.89/0.83 % (2371889)Termination phase: Saturation
% 1.89/0.83 % (2371889)Time elapsed: 0.062 s
% 1.89/0.83 % (2371889)Peak memory usage: 14 MB
% 1.89/0.83 % (2371889)Instructions burned: 103 (million)
% 1.89/0.83 % (2371890)Instruction limit reached!
% 1.89/0.83 % (2371890)------------------------------
% 1.89/0.83 % (2371890)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.83 % (2371890)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.83 % (2371890)CaDiCaL version: 2.1.3
% 1.89/0.83 % (2371890)Termination reason: Instruction limit
% 1.89/0.83 % (2371890)Termination phase: Saturation
% 1.89/0.83 % (2371890)Time elapsed: 0.065 s
% 1.89/0.83 % (2371890)Peak memory usage: 14 MB
% 1.89/0.83 % (2371890)Instructions burned: 116 (million)
% 1.89/0.83 % (2371902)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1354652696:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 1.89/0.83 % (2371903)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2781420307:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 1.89/0.83 % (2371892)Instruction limit reached!
% 1.89/0.83 % (2371892)------------------------------
% 1.89/0.83 % (2371892)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.83 % (2371892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.83 % (2371892)CaDiCaL version: 2.1.3
% 1.89/0.83 % (2371892)Termination reason: Instruction limit
% 1.89/0.83 % (2371892)Termination phase: Saturation
% 1.89/0.83 % (2371892)Time elapsed: 0.093 s
% 1.89/0.83 % (2371892)Peak memory usage: 15 MB
% 1.89/0.83 % (2371892)Instructions burned: 159 (million)
% 1.89/0.83 % (2371906)ott-21_1_sil=16000:fs=off:random_seed=24141277:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 1.89/0.83 % TRYING [1]
% 1.89/0.83 % (2371902)Instruction limit reached!
% 1.89/0.83 % (2371902)------------------------------
% 1.89/0.83 % (2371902)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.83 % (2371902)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.83 % (2371902)CaDiCaL version: 2.1.3
% 1.89/0.83 % (2371902)Termination reason: Instruction limit
% 1.89/0.83 % (2371902)Termination phase: Saturation
% 1.89/0.83 % (2371902)Time elapsed: 0.074 s
% 1.89/0.83 % (2371902)Peak memory usage: 14 MB
% 1.89/0.83 % (2371902)Instructions burned: 131 (million)
% 1.89/0.83 % TRYING [2]
% 1.89/0.83 % (2371908)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1959652967:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 1.89/0.83 % TRYING [3]
% 1.89/0.83 % (2371906)Instruction limit reached!
% 1.89/0.83 % (2371906)------------------------------
% 1.89/0.83 % (2371906)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.83 % (2371906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.83 % (2371906)CaDiCaL version: 2.1.3
% 1.89/0.83 % (2371906)Termination reason: Instruction limit
% 1.89/0.83 % (2371906)Termination phase: Saturation
% 1.89/0.83 % (2371906)Time elapsed: 0.102 s
% 1.89/0.83 % (2371906)Peak memory usage: 14 MB
% 1.89/0.83 % (2371906)Instructions burned: 180 (million)
% 1.89/0.83 % (2371900)Instruction limit reached!
% 1.89/0.83 % (2371900)------------------------------
% 1.89/0.83 % (2371900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.83 % (2371900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.83 % (2371900)CaDiCaL version: 2.1.3
% 1.89/0.83 % (2371900)Termination reason: Instruction limit
% 1.89/0.83 % (2371900)Termination phase: Finite model building constraint generation
% 1.89/0.83 % (2371900)Time elapsed: 0.172 s
% 1.89/0.83 % (2371900)Peak memory usage: 30 MB
% 1.89/0.83 % (2371900)Instructions burned: 720 (million)
% 1.89/0.83 % (2371910)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=936847170:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 1.89/0.83 % (2371911)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=242987371:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 1.89/0.83 % (2371888) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2371881-2371888"...
% 1.89/0.83 % (2371888)...printing done.
% 1.89/0.83 % SZS status CounterSatisfiable for theBenchmark
% 1.89/0.83 % SZS output start Saturation.
% See solution above
% 1.89/0.83 % SZS output start Definitions and Model Updates.
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'homFtor$'(X0,X1) := 'makeFtor$b'('homFtor$a'(X0,X1))
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'zFfun$'(X0,X1,X2) := 'fun_app$'('fun_app$h'('opair$','fun_app$'('fun_app$h'('opair$',X0),X1)),'lambda$'(X0,X2))
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'constFunctor$b'(X0,X1,X2) := 'makeFtor$'('constFunctor$c'(X0,X1,X2))
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'homFtorContra$'(X0,X1) := 'makeFtor$b'('homFtorContra$a'(X0,X1))
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'yFtor$a'(X0) := 'makeFtor$'('functor_ext$b'(X0,'catExp$'('fun_app$n'('oppositeCategory$a',X0),'set$a'),'yFtorNT$'(X0),'unity$'))
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'constFunctor$'(X0,X1,X2) := 'makeFtor$a'('constFunctor$a'(X0,X1,X2))
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'yFtor$'(X0) := 'functor_ext$b'(X0,'catExp$'('fun_app$n'('oppositeCategory$a',X0),'set$a'),'yFtorNT$'(X0),'unity$')
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'identityFunctor$d'(X0) := 'makeFtor$a'('identityFunctor$c'(X0))
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functorM$j'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'preFunctor$c'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functor_comp_def$g'(X0,X1) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functor$j'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functor$i'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'preFunctor$e'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'preFunctor$f'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functorM$e'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'natTransP$'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functorM$m'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'preFunctor$k'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functorM$h'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functorM$i'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'nTCompDefined$'(X0,X1) := $false
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functor$o'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functorM$k'(X0) := $true
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'functor_comp_def$e'(X0,X1) := $false
% 1.89/0.83 for all inputs,
% 1.89/0.83 define 'preFunctor$j'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'natTrans$a'(X0) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'preFunctor$i'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$f'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'member$k'(X0,X1) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$g'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$m'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'preFunctor$h'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'natTrans$'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functorM$d'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'member$i'(X0,X1) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'isomorphism$a'(X0,X1) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$e'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'category$d'(X0) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$k'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'compDefined$a'(X0,X1,X2) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor_comp_def$j'(X0,X1) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'isomorphism$d'(X0,X1) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'member$j'(X0,X1) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor_comp_def$d'(X0,X1) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor_comp_def$i'(X0,X1) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$l'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functorM$g'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functorM$f'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'nt_abbrev$'(X0,X1,X2) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'preFunctor$l'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor_comp_def$h'(X0,X1) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$n'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'category_axioms$a'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$h'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor$d'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'preFunctor$m'(X0) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'preFunctor$g'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functorM$l'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor_comp_def$k'(X0,X1) := $false
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'preFunctor$d'(X0) := $true
% 1.89/0.84 for all inputs,
% 1.89/0.84 define 'functor_comp_def$f'(X0,X1) := $false
% 1.89/0.84 for all groundings,
% 1.89/0.84 whenever 'functor$a'(X0) & 'functor$'(X1) & 'catDom$'(X1) = 'catCod$a'(X0) is false, set ~'functor_comp_def$a'(X0,X1) to true
% 1.89/0.84 for all groundings,
% 1.89/0.84 whenever 'functor$b'(X0) & 'functor$a'(X1) & 'catDom$a'(X1) = 'catCod$'(X0) is false, set ~'functor_comp_def$b'(X0,X1) to true
% 1.89/0.84 for all groundings,
% 1.89/0.84 whenever 'functor$b'(X0) & 'functor$'(X1) & 'catDom$'(X1) = 'catCod$'(X0) is false, set ~'functor_comp_def$'(X0,X1) to true
% 1.89/0.84 for all groundings,
% 1.89/0.84 whenever 'functor$'(X0) & 'catDom$'(X0) = X1 & 'catCod$c'(X0) = X2 is false, set ~'functor_abbrev$'(X0,X1,X2) to true
% 1.89/0.84 for all groundings,
% 1.89/0.84 whenever 'functor$a'(X0) & 'catDom$a'(X0) = X1 & 'catCod$a'(X0) = X2 is false, set ~'functor_abbrev$b'(X0,X1,X2) to true
% 1.89/0.84 for all groundings,
% 1.89/0.84 whenever 'functor$a'(X0) & 'functor$a'(X1) & 'catDom$a'(X1) = 'catCod$a'(X0) is false, set ~'functor_comp_def$c'(X0,X1) to true
% 1.89/0.84 for all groundings,
% 1.89/0.84 whenever 'functor$c'(X0) & 'catDom$c'(X0) = X1 & 'catCod$b'(X0) = X2 is false, set ~'functor_abbrev$a'(X0,X1,X2) to true
% 1.89/0.84 % SZS output end Definitions and Model Updates.
% 1.89/0.84 % (2371888)------------------------------
% 1.89/0.84 % (2371888)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 1.89/0.84 % (2371888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.89/0.84 % (2371888)CaDiCaL version: 2.1.3
% 1.89/0.84 % (2371888)Termination reason: Satisfiable
% 1.89/0.84 % (2371888)Time elapsed: 0.330 s
% 1.89/0.84 % (2371888)Peak memory usage: 18 MB
% 1.89/0.84 % (2371888)Instructions burned: 529 (million)
% 1.89/0.84 % (2371881)Success in time 0.401 s
% 1.89/0.84 % Vampire exiting
%------------------------------------------------------------------------------